ROSE 0.11.145.147
SourceAstSemantics.h
1// Turn instruction semantics into a C source AST
2#ifndef ROSE_BinaryAnalysis_InstructionSemantics_SourceAstSemantics_H
3#define ROSE_BinaryAnalysis_InstructionSemantics_SourceAstSemantics_H
4#include <featureTests.h>
5#ifdef ROSE_ENABLE_BINARY_ANALYSIS
6#include <Rose/BinaryAnalysis/BasicTypes.h>
7
8#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/SValue.h>
9#include <Rose/BinaryAnalysis/InstructionSemantics/NullSemantics.h>
10
11namespace Rose {
12namespace BinaryAnalysis {
13namespace InstructionSemantics {
14
50namespace SourceAstSemantics {
51
53// Value type
55
58
69public:
72
74 using Ptr = SValuePtr;
75
76protected:
77 static size_t nVariables_;
78 std::string ctext_;
79
80protected:
81 // An undefined or unspecified value is a C variable that's not initialized.
82 explicit SValue(size_t nbits);
83
84 // An integer value, various types depending on width
85 SValue(size_t nbits, uint64_t number);
86
87 // Copy constructor deep-copies the AST.
88 SValue(const SValue &other);
89
90public:
95
99 static SValuePtr instance_undefined(size_t nbits);
100
102 static SValuePtr instance_integer(size_t nbits, uint64_t value);
103
104public:
105 virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override;
106 virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override;
107 virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override;
108 virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override;
109 virtual BaseSemantics::SValuePtr boolean_(bool value) const override;
110 virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override;
111
114
115public:
118
119public:
120 virtual bool isBottom() const override;
121 virtual void hash(Combinatorics::Hasher&) const override;
122 virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;
123
124public:
125 // These are not needed since this domain never tries to compare semantic values.
126 virtual bool may_equal(const BaseSemantics::SValuePtr &/*other*/,
127 const SmtSolverPtr& = SmtSolverPtr()) const override;
128
129 virtual bool must_equal(const BaseSemantics::SValuePtr &/*other*/,
130 const SmtSolverPtr& = SmtSolverPtr()) const override;
131
132 virtual void set_width(size_t /*nbits*/) override;
133 virtual bool is_number() const override;
134 virtual uint64_t get_number() const override;
135
136public:
140 static std::string unsignedTypeNameForSize(size_t nbits);
141 static std::string signedTypeNameForSize(size_t nbits);
144public:
148 virtual const std::string& ctext() const;
149 virtual void ctext(const std::string&);
151};
152
154// State
156
157// No state is necessary for this domain because all instruction side effects are immediately attached to the AST that's
158// being generated rather than being stored in some state.
159
171// RiscOperators
173
175typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;
176
185public:
188
191
192public:
194 struct SideEffect {
199 ~SideEffect();
200
201 // Default constructor. Not normally used, but needed by <code>std::vector</code>. (DON'T DOCUMENT)
202 SideEffect();
203
204 // Used internally, not neede by users since data members are public.
207
209 bool isValid() const;
210
214 bool isSubstitution() const;
215 };
216
218 typedef std::vector<SideEffect> SideEffects;
219
220private:
221 SideEffects sideEffects_; // Side effects, including substitutions
222 bool executionHalted_; // Stop adding inputs and outputs?
223
224protected:
226
228
229public:
233
238 const SmtSolverPtr &solver = SmtSolverPtr());
239
243
245 // Virtual constructors
246public:
248 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
249
251 const SmtSolverPtr &solver = SmtSolverPtr()) const override;
252
254 // Dynamic pointer casts
255public:
259
261 // Supporting functions
262public:
264 BaseSemantics::SValuePtr makeSValue(size_t nbits, SgNode*, const std::string &ctext = "");
265
273
280
284 const SideEffects& sideEffects() const;
285
288
294
296 void reset();
297
304 void haltExecution() { executionHalted_ = true; }
305
311 BaseSemantics::SValuePtr makeMask(size_t nBits, size_t nSet, size_t sa=0);
312
314 // Override all operator methods from base class. These are the RISC operators that are invoked by a Dispatcher.
315public:
316 virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) override;
317 virtual void hlt() override;
318 virtual void cpuid() override;
319 virtual BaseSemantics::SValuePtr rdtsc() override;
321 const BaseSemantics::SValuePtr &b_) override;
323 const BaseSemantics::SValuePtr &b_) override;
325 const BaseSemantics::SValuePtr &b_) override;
328 size_t begin_bit, size_t end_bit) override;
330 const BaseSemantics::SValuePtr &b_) override;
334 const BaseSemantics::SValuePtr &sa_) override;
336 const BaseSemantics::SValuePtr &sa_) override;
338 const BaseSemantics::SValuePtr &sa_) override;
340 const BaseSemantics::SValuePtr &sa_) override;
342 const BaseSemantics::SValuePtr &sa_) override;
345 const BaseSemantics::SValuePtr &a_,
346 const BaseSemantics::SValuePtr &b_,
347 IteStatus&) override;
348 virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
349 virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
351 const BaseSemantics::SValuePtr &b_) override;
353 const BaseSemantics::SValuePtr &b_,
354 const BaseSemantics::SValuePtr &c_,
355 BaseSemantics::SValuePtr &carry_out/*out*/) override;
358 const BaseSemantics::SValuePtr &b_) override;
360 const BaseSemantics::SValuePtr &b_) override;
362 const BaseSemantics::SValuePtr &b_) override;
364 const BaseSemantics::SValuePtr &b_) override;
366 const BaseSemantics::SValuePtr &b_) override;
368 const BaseSemantics::SValuePtr &b_) override;
369 virtual void interrupt(int majr, int minr) override;
371 const BaseSemantics::SValuePtr &dflt) override;
373 const BaseSemantics::SValuePtr &dflt) override;
374 virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a) override;
376 const BaseSemantics::SValuePtr &addr,
377 const BaseSemantics::SValuePtr &dflt,
378 const BaseSemantics::SValuePtr &cond) override;
380 const BaseSemantics::SValuePtr &addr,
381 const BaseSemantics::SValuePtr &dflt) override;
382 virtual void writeMemory(RegisterDescriptor segreg,
383 const BaseSemantics::SValuePtr &addr,
384 const BaseSemantics::SValuePtr &data,
385 const BaseSemantics::SValuePtr &cond) override;
386};
387
388
389} // namespace
390} // namespace
391} // namespace
392} // namespace
393
394#endif
395#endif
Base class for most instruction semantics RISC operators.
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
static RiscOperatorsPtr instanceFromState(const BaseSemantics::StatePtr &, const SmtSolverPtr &)
Instantiates a new RiscOperators object with specified state.
virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) override
Read memory without side effects.
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 signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiplies two signed values.
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise OR of two values.
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &)
Run-time promotion of a base RiscOperators instance to an instance of this semantic domain's operator...
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted left.
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise AND of two values.
virtual BaseSemantics::SValuePtr rdtsc() override
Invoked for the x86 RDTSC instruction.
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) override
One's complement.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise XOR of two values.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override
Sign extends a value.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiply two unsigned values.
virtual void cpuid() override
Invoked for the x86 CPUID instruction.
virtual void interrupt(int majr, int minr) override
Unconditionally raise an interrupt.
virtual void writeMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) override
Writes a value to memory.
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) override
Extracts bits from a value.
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 ...
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) override
Two's complement.
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.
BaseSemantics::SValuePtr makeMask(size_t nBits, size_t nSet, size_t sa=0)
Return a bit mask.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) override
Determines whether a value is equal to zero.
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with 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::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a) override
Writes a value to a register.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Adds two integers of equal size.
std::vector< SideEffect > SideEffects
Side effects in the order they occur.
virtual void hlt() override
Invoked for the x86 HLT instruction.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the right.
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Concatenates the bits of two values.
virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) override
Reads a value from a register.
BaseSemantics::SValuePtr substitute(const BaseSemantics::SValuePtr &expression)
Save input value.
BaseSemantics::SValuePtr saveSideEffect(const BaseSemantics::SValuePtr &expression, const BaseSemantics::SValuePtr &location=BaseSemantics::SValuePtr())
Save a side effect.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the left.
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) override
Returns position of most significant set bit; zero when no bits are set.
std::string registerVariableName(RegisterDescriptor)
Global variable name for a register.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two unsigned values.
virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted right arithmetically (with sign bit).
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two signed values.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) override
Returns a new undefined value.
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::RiscOperatorsPtr create(const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
static RiscOperatorsPtr instanceFromProtoval(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified prototypical values.
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::SValuePtr peekRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) override
Obtain a register value without side effects.
virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, const BaseSemantics::SValuePtr &cond) override
Reads a value from memory.
BaseSemantics::SValuePtr makeSValue(size_t nbits, SgNode *, const std::string &ctext="")
Create a new SValue.
const SideEffects & sideEffects() const
Accumulated side effects and substitutions.
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with unsigned values.
static SValuePtr instance_undefined(size_t nbits)
Instantiate an undefined value.
virtual uint64_t get_number() const override
Virtual API.
virtual bool may_equal(const BaseSemantics::SValuePtr &, const SmtSolverPtr &=SmtSolverPtr()) const override
Virtual API.
virtual const std::string & ctext() const
C source text associated with this semantic value.
static std::string unsignedTypeNameForSize(size_t nbits)
Name of integer type used for 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 BaseSemantics::SValuePtr undefined_(size_t nbits) const override
Create a new undefined semantic value.
static SValuePtr promote(const BaseSemantics::SValuePtr &)
Promote a base instance to an instance of this class.
static SValuePtr instance_integer(size_t nbits, uint64_t value)
Instantiate an integer constant.
virtual Sawyer::Optional< BaseSemantics::SValuePtr > createOptionalMerge(const BaseSemantics::SValuePtr &, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
Possibly create a new value by merging two existing values.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override
Data-flow bottom value.
static std::string signedTypeNameForSize(size_t nbits)
Name of integer type used for value.
virtual BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
virtual void ctext(const std::string &)
C source text associated with this semantic value.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
static SValuePtr instance()
Instantiate a prototypical SValue.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override
Create a new unspecified 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 &, const SmtSolverPtr &=SmtSolverPtr()) const override
Virtual API.
virtual bool isBottom() const override
Determines whether a value is a data-flow bottom.
Describes (part of) a physical CPU register.
Holds a value or nothing.
Definition Optional.h:56
Reference-counting intrusive smart pointer.
This class represents the base class for all IR nodes within Sage III.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer for basic semantic operations.
BaseSemantics::RegisterStateGeneric RegisterState
Register state used by this domain.
BaseSemantics::State State
State used by this domain.
NullSemantics::MemoryStatePtr MemoryStatePtr
Pointer to memory states used by this domain.
NullSemantics::MemoryState MemoryState
Memory state used by this domain.
BaseSemantics::RegisterStateGenericPtr RegisterStatePtr
Pointer to register states used by this domain.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for a binary-to-source semantic value.
BaseSemantics::StatePtr StatePtr
Pointer to states used by this domain.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
The ROSE library.
bool isSubstitution() const
Predicate to determine whether side effect is rather a substitution.
bool isValid() const
Predicate to determine whether side effect is valid.