ROSE 0.11.145.147
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
84protected:
85 SValue() {} // needed for serialization
86
87 explicit SValue(size_t nbits): Super(nbits) {}
88
89 SValue(size_t nbits, uint64_t number): Super(nbits, number) {}
90
91 SValue(ExprPtr expr): Super(expr) {}
92
94 // Static allocating constructors
95public:
100
106 static SValuePtr instance_bottom(size_t nbits) {
108 }
109
111 static SValuePtr instance_undefined(size_t nbits) {
113 }
114
119
121 static SValuePtr instance_integer(size_t nbits, uint64_t value) {
123 }
124
127 ASSERT_not_null(value);
128 return SValuePtr(new SValue(value));
129 }
130
132 // Virtual allocating constructors
133public:
134 virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override {
135 return instance_bottom(nbits);
136 }
137
138 /* Instantiate a new data-flow bottom value of specified width.
139 *
140 * The symbolic value is what is set to bottom in this case. The taintedness is always set to bottom by all the static
141 * allocating constructors. If you need a different taintedness then you need to change it with the @ref taintedness
142 * property. */
143 virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override {
144 return instance_undefined(nbits);
145 }
146
147 virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override {
148 return instance_unspecified(nbits);
149 }
150
151 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override {
152 return instance_integer(nbits, value);
153 }
154
155 virtual BaseSemantics::SValuePtr boolean_(bool value) const override {
156 return instance_integer(1, value?1:0);
157 }
158
159 virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override {
160 SValuePtr retval(new SValue(*this));
161 if (new_width!=0 && new_width!=retval->nBits())
162 retval->set_width(new_width);
163 return retval;
164 }
165
168 const SmtSolverPtr&) const override;
169
171 // Dynamic pointer casts
172public:
175 SValuePtr retval = v.dynamicCast<SValue>();
176 ASSERT_not_null(retval);
177 return retval;
178 }
179
181 // Override virtual methods...
182public:
183 virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
184
185 virtual void hash(Combinatorics::Hasher&) const override;
186
187protected: // when implementing use these names; but when calling, use the camelCase names
188 virtual bool may_equal(const BaseSemantics::SValuePtr &other,
189 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
190 virtual bool must_equal(const BaseSemantics::SValuePtr &other,
191 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
192
193
195 // Additional methods first declared in this class...
196public:
206public:
207 // Merge two taintedness values
208 static Taintedness mergeTaintedness(Taintedness, Taintedness);
209};
210
211
213// Register state
215
217using RegisterStatePtr = SymbolicSemantics::RegisterStatePtr;
218
219
221// Memory state
223
225using MemoryListStatePtr = SymbolicSemantics::MemoryListStatePtr;
226
228using MemoryMapStatePtr = SymbolicSemantics::MemoryMapStatePtr;
229
231using MemoryStatePtr = MemoryListStatePtr;
232
233
235// Complete state
237
239using StatePtr = SymbolicSemantics::StatePtr;
240
241
243// RISC operators
245
247using RiscOperatorsPtr = boost::shared_ptr<class RiscOperators>;
248
266public:
269
272
274 // Serialization
275#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
276private:
277 friend class boost::serialization::access;
278
279 template<class S>
280 void serialize(S &s, const unsigned /*version*/) {
281 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
282 }
283#endif
284
286 // Real constructors
287protected:
288 RiscOperators(); // for serialization
289
291
292 explicit RiscOperators(const BaseSemantics::StatePtr&, const SmtSolverPtr&);
293
295 // Static allocating constructors
296public:
298
302
307 const SmtSolverPtr &solver = SmtSolverPtr());
308
312
314 // Virtual constructors
315public:
317 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
318
320 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
321
323 // Dynamic pointer casts
324public:
328
330 // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
331public:
333 const BaseSemantics::SValuePtr &b_) override;
335 const BaseSemantics::SValuePtr &b_) override;
337 const BaseSemantics::SValuePtr &b_) override;
340 size_t begin_bit, size_t end_bit) override;
342 const BaseSemantics::SValuePtr &b_) override;
346 const BaseSemantics::SValuePtr &sa_) override;
348 const BaseSemantics::SValuePtr &sa_) override;
350 const BaseSemantics::SValuePtr &sa_) override;
352 const BaseSemantics::SValuePtr &sa_) override;
354 const BaseSemantics::SValuePtr &sa_) override;
357 const BaseSemantics::SValuePtr &a_,
358 const BaseSemantics::SValuePtr &b_,
359 IteStatus&) override;
360 virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
361 virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
363 const BaseSemantics::SValuePtr &b_) override;
365 const BaseSemantics::SValuePtr &b_,
366 const BaseSemantics::SValuePtr &c_,
367 BaseSemantics::SValuePtr &carry_out/*out*/) override;
370 const BaseSemantics::SValuePtr &b_) override;
372 const BaseSemantics::SValuePtr &b_) override;
374 const BaseSemantics::SValuePtr &b_) override;
376 const BaseSemantics::SValuePtr &b_) override;
378 const BaseSemantics::SValuePtr &b_) override;
380 const BaseSemantics::SValuePtr &b_) override;
382 SgAsmFloatType *retType) override;
384
385private:
386 static Taintedness mergeTaintedness(const BaseSemantics::SValuePtr&, const BaseSemantics::SValue::Ptr&);
387};
388
389} // namespace
390} // namespace
391} // namespace
392} // namespace
393
394#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
397#endif
398
399#endif
400#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:41
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.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a TaintSemantics value.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic 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.
static const unsigned UNSPECIFIED
Value is somehow unspecified.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
Holds a value or nothing.
Definition Optional.h:56
SharedPointer< U > dynamicCast() const
Dynamic cast.
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.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
The ROSE library.