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>
8#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/SValue.h>
9#include <Rose/BinaryAnalysis/InstructionSemantics/NullSemantics.h>
12namespace BinaryAnalysis {
13namespace InstructionSemantics {
50namespace SourceAstSemantics {
77 static size_t nVariables_;
82 explicit SValue(
size_t nbits);
85 SValue(
size_t nbits, uint64_t number);
148 virtual const std::string&
ctext()
const;
149 virtual void ctext(
const std::string&);
222 bool executionHalted_;
317 virtual void hlt()
override;
328 size_t begin_bit,
size_t end_bit)
override;
A RegisterState for any architecture.
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.
IteStatus
Status for iteWithStatus operation.
Base class for semantic values.
Base class for semantics machine states.
Basic semantic operations.
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...
void haltExecution()
Halt execution.
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.
void resetState()
Reset state to initial conditions.
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.
void reset()
Reset to initial state.
RiscOperatorsPtr Ptr
Shared-ownership pointer.
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.
Semantic values for generating C source code ASTs.
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.
virtual void set_width(size_t) override
Virtual API.
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 bool is_number() const override
Virtual API.
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.
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< State > StatePtr
Shared-ownership pointer to a semantic state.
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.
BaseSemantics::SValuePtr temporary
Optional Temporary variable.
BaseSemantics::SValuePtr location
Optional affected location.
bool isSubstitution() const
Predicate to determine whether side effect is rather a substitution.
BaseSemantics::SValuePtr expression
Expression.
bool isValid() const
Predicate to determine whether side effect is valid.