2 #ifndef ROSE_BinaryAnalysis_InstructionSemantics_StaticSemantics_H
3 #define ROSE_BinaryAnalysis_InstructionSemantics_StaticSemantics_H
4 #include <featureTests.h>
5 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
7 #include <Rose/BinaryAnalysis/BasicTypes.h>
8 #include <Rose/BinaryAnalysis/Disassembler/BasicTypes.h>
9 #include <Rose/BinaryAnalysis/InstructionSemantics/NullSemantics.h>
10 #include "SageBuilderAsm.h"
13 namespace BinaryAnalysis {
14 namespace InstructionSemantics {
40 namespace StaticSemantics {
88 static uint64_t nVars = 0;
89 ast_ = SageBuilderAsm::buildRiscOperation(op, SageBuilderAsm::buildValueU64(nVars++));
95 ast_ = SageBuilderAsm::buildValueInteger(number, type);
101 ASSERT_require(isSgAsmExpression(copied));
102 ast_ = isSgAsmExpression(copied);
133 return SValuePtr(
new SValue(nbits, SgAsmRiscOperation::OP_unspecified));
158 SValuePtr retval(
new SValue(*
this));
159 if (new_width!=0 && new_width!=retval->nBits())
160 retval->set_width(new_width);
173 ASSERT_not_null(retval);
181 ASSERT_not_reachable(
"no implementation necessary");
186 ASSERT_not_reachable(
"no implementation necessary");
190 ASSERT_not_reachable(
"no implementation necessary");
202 ASSERT_not_reachable(
"no implementation necessary");
206 ASSERT_not_reachable(
"no implementation necessary");
240 typedef NullSemantics::StatePtr StatePtr;
349 virtual void hlt()
override;
350 virtual void cpuid()
override;
360 size_t begin_bit,
size_t end_bit)
override;
421 virtual void interrupt(
int majr,
int minr)
override;
Base classes for instruction semantics.
virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) override
Two's complement.
virtual void startInstruction(SgAsmInstruction *) override
Called at the beginning of every instruction.
static SValuePtr instance_undefined(size_t nbits)
Instantiate an undefined value.
virtual BaseSemantics::SValuePtr isUnsignedLessThan(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Comparison for unsigned values.
static SValuePtr instance()
Instantiate a prototypical SValue.
virtual bool isBottom() const override
Determines whether a value is a data-flow bottom.
virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the right.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override
Create a new unspecified semantic value.
virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) override
Returns position of most significant set bit; zero when no bits are set.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual BaseSemantics::SValuePtr filterIndirectJumpTarget(const BaseSemantics::SValuePtr &a) override
Invoked to filter indirect jumps.
virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) override
Obtain a register value without side effects.
Base class for machine instructions.
RiscOperatorsPtr Ptr
Shared-ownership pointer.
virtual BaseSemantics::SValuePtr isEqual(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Equality comparison.
virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two signed values.
RiscOperator
One enum per RISC operator.
Basic semantic operations.
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 isSignedGreaterThanOrEqual(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Comparison for signed values.
virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) override
One's complement.
Semantic values for generating static semantic ASTs.
virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise OR of two values.
virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Rotate bits to the left.
Holds a value or nothing.
virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) override
Returns position of least significant set bit; zero when no bits are set.
static SValuePtr instance_integer(size_t nbits, uint64_t value)
Instantiate an integer constant.
virtual BaseSemantics::SValuePtr isUnsignedGreaterThanOrEqual(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Comparison for unsigned values.
virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a) override
Writes a value to a register.
Main namespace for the ROSE library.
virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) override
Determines whether a value is equal to zero.
virtual BaseSemantics::SValuePtr rdtsc() override
Invoked for the x86 RDTSC instruction.
virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_, size_t begin_bit, size_t end_bit) override
Extracts bits from a value.
virtual BaseSemantics::SValuePtr isSignedGreaterThan(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Comparison for signed values.
virtual BaseSemantics::SValuePtr isSignedLessThan(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Comparison for signed values.
static RiscOperatorsPtr instanceFromProtoval(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified prototypical values.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
virtual BaseSemantics::SValuePtr isUnsignedLessThanOrEqual(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Comparison for unsigned values.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer.
virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted right arithmetically (with sign bit).
virtual uint64_t get_number() const override
Virtual API.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
virtual void cpuid() override
Invoked for the x86 CPUID instruction.
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.
boost::shared_ptr< class RegisterState > RegisterStatePtr
Shared-ownership pointer.
virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise XOR of two values.
virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiplies two signed values.
virtual BaseSemantics::SValuePtr filterCallTarget(const BaseSemantics::SValuePtr &a) override
Invoked to filter call targets.
virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Divides two unsigned values.
static Type * registerOrDelete(Type *toInsert)
Registers a type with the type system.
virtual BaseSemantics::SValuePtr isSignedLessThanOrEqual(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Comparison for signed values.
IteStatus
Status for iteWithStatus operation.
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &)
Run-time promotion of a base RiscOperators pointer to static operators.
virtual void interrupt(int majr, int minr) override
Invoked for instructions that cause an interrupt.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer for basic semantic operations.
Describes (part of) a physical CPU register.
This class represents the base class for all IR nodes within Sage III.
virtual void ast(SgAsmExpression *x)
Property: Abstract syntax tree.
virtual BaseSemantics::SValuePtr isNotEqual(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Equality comparison.
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 peekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt) override
Read memory without side effects.
virtual BaseSemantics::SValuePtr filterReturnTarget(const BaseSemantics::SValuePtr &a) override
Invoked to filter return targets.
virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override
Sign extends a value.
virtual SgAsmExpression * ast()
Property: Abstract syntax tree.
virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &dflt) override
Reads a value from a register.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for semantic values.
Base class for expressions.
virtual BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
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 readMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, const BaseSemantics::SValuePtr &cond) override
Reads a value from memory.
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.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for a static-semantics value.
virtual void set_width(size_t) override
Virtual API.
virtual SgNode * copy(SgCopyHelp &help) const
This function clones the current IR node object recursively or not, depending on the argument...
Supporting class for "Deep" copies of the AST.
Base class for binary types.
void saveSemanticEffect(const BaseSemantics::SValuePtr &)
Save instruction side effect.
virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Adds two integers of equal size.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override
Create a new undefined semantic value.
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted left.
SgNode * get_parent() const
Access function for parent node.
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 void hlt() override
Invoked for the x86 HLT instruction.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a static semantics value.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override
Create a new concrete semantic value.
virtual BaseSemantics::SValuePtr isUnsignedGreaterThan(const BaseSemantics::SValuePtr &, const BaseSemantics::SValuePtr &) override
Comparison for unsigned values.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with signed values.
virtual void writeMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) override
Writes a value to memory.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override
Data-flow bottom value.
virtual bool is_number() const override
Virtual API.
Base class for most instruction semantics RISC operators.
virtual bool may_equal(const BaseSemantics::SValuePtr &, const SmtSolverPtr &=SmtSolverPtr()) const override
Virtual API.
virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Multiply two unsigned values.
virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Concatenates the bits of two values.
Base class for semantics machine states.
void attachInstructionSemantics(SgNode *ast, const Disassembler::BasePtr &)
Build and attach static semantics to all instructions.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &sa_) override
Returns arg shifted right logically (no sign bit).
virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Calculates modulo with unsigned values.
virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Computes bit-wise AND of two values.
static RiscOperatorsPtr instanceFromState(const BaseSemantics::StatePtr &, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified state.
virtual BaseSemantics::SValuePtr subtract(const BaseSemantics::SValuePtr &a_, const BaseSemantics::SValuePtr &b_) override
Subtract one value from another.
virtual bool must_equal(const BaseSemantics::SValuePtr &, const SmtSolverPtr &=SmtSolverPtr()) const override
Virtual API.
static SValuePtr instance_bottom(size_t nbits)
Instantiate a data-flow bottom value.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
BaseSemantics::SValuePtr makeSValue(size_t nbits, SgAsmExpression *)
Create a new SValue.
static SValuePtr instance_unspecified(size_t nbits)
Instantiate an unspecified value.