ROSE 0.11.145.192
TaintSemantics.h
1#ifndef ROSE_BinaryAnalysis_InstructionSemantics_TaintSemantics_H
2#define ROSE_BinaryAnalysis_InstructionSemantics_TaintSemantics_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_BINARY_ANALYSIS
5#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
6
7#include <Rose/BinaryAnalysis/BasicTypes.h>
8
9namespace Rose {
10namespace BinaryAnalysis {
11namespace InstructionSemantics {
12
14namespace TaintSemantics {
15
17enum class Taintedness {
18 BOTTOM,
19 UNTAINTED,
20 TAINTED,
21 TOP
22};
23
24using ExprPtr = SymbolicSemantics::ExprPtr;
25using ExprNode = SymbolicSemantics::ExprNode;
26
28// Merging values
30
33
36
37
39// Semantic values
41
44
47
60 Taintedness taintedness_ = Taintedness::BOTTOM;
61
62public:
65
67 using Ptr = SValuePtr;
68
69protected:
71 // Serialization
72#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
73private:
74 friend class boost::serialization::access;
75
76 template<class S>
77 void serialize(S &s, const unsigned /*version*/) {
78 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
79 }
80#endif
81
83 // Real constructors
84public:
85 ~SValue();
86
87protected:
88 SValue(); // needed for serialization
89
90 explicit SValue(size_t nbits);
91 SValue(size_t nbits, uint64_t number);
93
95 // Static allocating constructors
96public:
99
105 static SValuePtr instance_bottom(size_t nbits);
106
108 static SValuePtr instance_undefined(size_t nbits);
109
111 static SValuePtr instance_unspecified(size_t nbits);
112
114 static SValuePtr instance_integer(size_t nbits, uint64_t value);
115
118
120 // Virtual allocating constructors
121public:
122 virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override;
123
124 /* Instantiate a new data-flow bottom value of specified width.
125 *
126 * The symbolic value is what is set to bottom in this case. The taintedness is always set to bottom by all the static
127 * allocating constructors. If you need a different taintedness then you need to change it with the @ref taintedness
128 * property. */
129 virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override;
130
131 virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override;
132 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override;
133 virtual BaseSemantics::SValuePtr boolean_(bool value) const override;
134 virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override;
135
138 const SmtSolverPtr&) const override;
139
141 // Dynamic pointer casts
142public:
145
147 // Override virtual methods...
148public:
149 virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
150
151 virtual void hash(Combinatorics::Hasher&) const override;
152
153protected: // when implementing use these names; but when calling, use the camelCase names
154 virtual bool may_equal(const BaseSemantics::SValuePtr &other,
155 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
156 virtual bool must_equal(const BaseSemantics::SValuePtr &other,
157 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
158
159
161 // Additional methods first declared in this class...
162public:
172public:
173 // Merge two taintedness values
174 static Taintedness mergeTaintedness(Taintedness, Taintedness);
175};
176
177
179// Register state
181
183using RegisterStatePtr = SymbolicSemantics::RegisterStatePtr;
184
185
187// Memory state
189
191using MemoryListStatePtr = SymbolicSemantics::MemoryListStatePtr;
192
194using MemoryMapStatePtr = SymbolicSemantics::MemoryMapStatePtr;
195
197using MemoryStatePtr = MemoryListStatePtr;
198
199
201// Complete state
203
205using StatePtr = SymbolicSemantics::StatePtr;
206
207
209// RISC operators
211
213using RiscOperatorsPtr = boost::shared_ptr<class RiscOperators>;
214
232public:
235
238
240 // Serialization
241#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
242private:
243 friend class boost::serialization::access;
244
245 template<class S>
246 void serialize(S &s, const unsigned /*version*/) {
247 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
248 }
249#endif
250
252 // Real constructors
253protected:
254 RiscOperators(); // for serialization
255
257
258 explicit RiscOperators(const BaseSemantics::StatePtr&, const SmtSolverPtr&);
259
261 // Static allocating constructors
262public:
264
268
273 const SmtSolverPtr &solver = SmtSolverPtr());
274
278
280 // Virtual constructors
281public:
283 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
284
286 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
287
289 // Dynamic pointer casts
290public:
294
296 // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
297public:
299 const BaseSemantics::SValuePtr &b_) override;
301 const BaseSemantics::SValuePtr &b_) override;
303 const BaseSemantics::SValuePtr &b_) override;
306 size_t begin_bit, size_t end_bit) override;
308 const BaseSemantics::SValuePtr &b_) override;
312 const BaseSemantics::SValuePtr &sa_) override;
314 const BaseSemantics::SValuePtr &sa_) override;
316 const BaseSemantics::SValuePtr &sa_) override;
318 const BaseSemantics::SValuePtr &sa_) override;
320 const BaseSemantics::SValuePtr &sa_) override;
323 const BaseSemantics::SValuePtr &a_,
324 const BaseSemantics::SValuePtr &b_,
325 IteStatus&) override;
326 virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
327 virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
329 const BaseSemantics::SValuePtr &b_) override;
331 const BaseSemantics::SValuePtr &b_,
332 const BaseSemantics::SValuePtr &c_,
333 BaseSemantics::SValuePtr &carry_out/*out*/) override;
336 const BaseSemantics::SValuePtr &b_) override;
338 const BaseSemantics::SValuePtr &b_) override;
340 const BaseSemantics::SValuePtr &b_) override;
342 const BaseSemantics::SValuePtr &b_) override;
344 const BaseSemantics::SValuePtr &b_) override;
346 const BaseSemantics::SValuePtr &b_) override;
348 SgAsmFloatType *retType) override;
350
351private:
352 static Taintedness mergeTaintedness(const BaseSemantics::SValuePtr&, const BaseSemantics::SValue::Ptr&);
353};
354
355} // namespace
356} // namespace
357} // namespace
358} // namespace
359
360#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
363#endif
364
365#endif
366#endif
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
Base class for semantics machine states.
Definition State.h:42
Defines RISC operators for the SymbolicSemantics domain.
Type of values manipulated by the SymbolicSemantics domain.
Defines RISC operators for the TaintSemantics domain.
virtual BaseSemantics::SValuePtr iteWithStatus(const BaseSemantics::SValuePtr &sel_, const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, IteStatus &) override
If-then-else with status.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiplies two signed values.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with unsigned values.
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Concatenates the bits of two values.
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise AND of two values.
virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) override
Returns position of least significant set bit; zero when no bits are set.
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise OR of two values.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override
Sign extends a value.
virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override
Extend (or shrink) operand a so it is nbits wide by adding or removing high-order bits.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the right.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) override
One's complement.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) override
Determines whether a value is equal to zero.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted left.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the left.
virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_, const BaseSemantics::SValuePtr &c_, BaseSemantics::SValuePtr &carry_out) override
Add two values of equal size and a carry bit.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two unsigned values.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise XOR of two values.
virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr &a, SgAsmFloatType *aType, SgAsmFloatType *retType) override
Convert from one floating-point type to another.
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &)
Run-time promotion of a base RiscOperators pointer to symbolic operators.
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) override
Extracts bits from a value.
static RiscOperatorsPtr instanceFromProtoval(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified prototypical values.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Adds two integers of equal size.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two signed values.
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted right logically (no sign bit).
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) override
Two's complement.
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) override
Returns position of most significant set bit; zero when no bits are set.
virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted right arithmetically (with sign bit).
virtual BaseSemantics::SValuePtr reinterpret(const BaseSemantics::SValuePtr &, SgAsmType *) override
Reinterpret an expression as a different type.
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with signed values.
static RiscOperatorsPtr instanceFromRegisters(const RegisterDictionaryPtr &, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object and configures it to use semantic values and states that are ...
static RiscOperatorsPtr instanceFromState(const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified state.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiply two unsigned values.
Type of values manipulated by the SymbolicSemantics domain.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override
Create a new unspecified semantic value.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
static SValuePtr instance()
Instantiate a new prototypical value.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
static SValuePtr instance_symbolic(const SymbolicExpression::Ptr &value)
Instantiate a new symbolic value.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override
Data-flow bottom value.
virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override
Create a new value from an existing value, changing the width if new_width is non-zero.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
static SValuePtr promote(const BaseSemantics::SValuePtr &)
Promote a base value to a TaintSemantics value.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override
Create a new concrete semantic value.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
virtual BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
static SValuePtr instance_unspecified(size_t nbits)
Instantiate a new unspecified value of specified width.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override
Create a new undefined semantic value.
static SValuePtr instance_undefined(size_t nbits)
Instantiate a new undefined value of specified width.
static SValuePtr instance_bottom(size_t nbits)
Instantiate a new data-flow bottom value of specified width.
static SValuePtr instance_integer(size_t nbits, uint64_t value)
Instantiate a new concrete value.
Taintedness taintedness() const
Property: Taintedness.
virtual Sawyer::Optional< BaseSemantics::SValuePtr > createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
Possibly create a new value by merging two existing values.
Base class for symbolic expression nodes.
Holds a value or nothing.
Definition Optional.h:56
Floating point types.
Base class for binary types.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
boost::shared_ptr< class MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to symbolic memory state.
boost::shared_ptr< class MemoryListState > MemoryListStatePtr
Shared-ownership pointer for symbolic list-based memory state.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
The ROSE library.