ROSE 2.20.0
Loading...
Searching...
No Matches
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_ENABLE_BOOST_SERIALIZATION
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() = default;
86
87protected:
88 SValue() = default;
89 explicit SValue(size_t nbits);
90 SValue(size_t nbits, uint64_t number);
92
94 // Static allocating constructors
95public:
98
104 static SValuePtr instance_bottom(size_t nbits);
105
107 static SValuePtr instance_undefined(size_t nbits);
108
110 static SValuePtr instance_unspecified(size_t nbits);
111
113 static SValuePtr instance_integer(size_t nbits, uint64_t value);
114
117
119 // Virtual allocating constructors
120public:
121 virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override;
122
123 /* Instantiate a new data-flow bottom value of specified width.
124 *
125 * The symbolic value is what is set to bottom in this case. The taintedness is always set to bottom by all the static
126 * allocating constructors. If you need a different taintedness then you need to change it with the @ref taintedness
127 * property. */
128 virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override;
129
130 virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override;
131 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override;
132 virtual BaseSemantics::SValuePtr boolean_(bool value) const override;
133 virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override;
134
137 const SmtSolverPtr&) const override;
138
140 // Dynamic pointer casts
141public:
144
146 // Override virtual methods...
147public:
148 virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
149
150 virtual void hash(Combinatorics::Hasher&) const override;
151
152protected: // when implementing use these names; but when calling, use the camelCase names
153 virtual bool may_equal(const BaseSemantics::SValuePtr &other,
154 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
155 virtual bool must_equal(const BaseSemantics::SValuePtr &other,
156 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
157
158
160 // Additional methods first declared in this class...
161public:
171public:
172 // Merge two taintedness values
173 static Taintedness mergeTaintedness(Taintedness, Taintedness);
174};
175
176
178// Register state
180
182using RegisterStatePtr = SymbolicSemantics::RegisterStatePtr;
183
184
186// Memory state
188
190using MemoryListStatePtr = SymbolicSemantics::MemoryListStatePtr;
191
193using MemoryMapStatePtr = SymbolicSemantics::MemoryMapStatePtr;
194
196using MemoryStatePtr = MemoryListStatePtr;
197
198
200// Complete state
202
204using StatePtr = SymbolicSemantics::StatePtr;
205
206
208// RISC operators
210
212using RiscOperatorsPtr = boost::shared_ptr<class RiscOperators>;
213
231public:
234
237
239 // Serialization
240#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
241private:
242 friend class boost::serialization::access;
243
244 template<class S>
245 void serialize(S &s, const unsigned /*version*/) {
246 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
247 }
248#endif
249
251 // Real constructors
252protected:
253 RiscOperators(); // for serialization
254
256
257 explicit RiscOperators(const BaseSemantics::StatePtr&, const SmtSolverPtr&);
258
260 // Static allocating constructors
261public:
263
267
272 const SmtSolverPtr &solver = SmtSolverPtr());
273
277
279 // Virtual constructors
280public:
282 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
283
285 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
286
288 // Dynamic pointer casts
289public:
293
295 // Override methods from base class. These are the RISC operators that are invoked by a Dispatcher.
296public:
298 const BaseSemantics::SValuePtr &b_) override;
300 const BaseSemantics::SValuePtr &b_) override;
302 const BaseSemantics::SValuePtr &b_) override;
305 size_t begin_bit, size_t end_bit) override;
307 const BaseSemantics::SValuePtr &b_) override;
311 const BaseSemantics::SValuePtr &sa_) override;
313 const BaseSemantics::SValuePtr &sa_) override;
315 const BaseSemantics::SValuePtr &sa_) override;
317 const BaseSemantics::SValuePtr &sa_) override;
319 const BaseSemantics::SValuePtr &sa_) override;
322 const BaseSemantics::SValuePtr &a_,
323 const BaseSemantics::SValuePtr &b_,
324 IteStatus&) override;
325 virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
326 virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
328 const BaseSemantics::SValuePtr &b_) override;
330 const BaseSemantics::SValuePtr &b_,
331 const BaseSemantics::SValuePtr &c_,
332 BaseSemantics::SValuePtr &carry_out/*out*/) override;
335 const BaseSemantics::SValuePtr &b_) override;
337 const BaseSemantics::SValuePtr &b_) override;
339 const BaseSemantics::SValuePtr &b_) override;
341 const BaseSemantics::SValuePtr &b_) override;
343 const BaseSemantics::SValuePtr &b_) override;
345 const BaseSemantics::SValuePtr &b_) override;
346 virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr &a, SgAsmFloatType *aType,
347 SgAsmFloatType *retType) override;
349
350private:
351 static Taintedness mergeTaintedness(const BaseSemantics::SValuePtr&, const BaseSemantics::SValue::Ptr&);
352};
353
354} // namespace
355} // namespace
356} // namespace
357} // namespace
358
359#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
362#endif
363
364#endif
365#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:50
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.
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:54
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.