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>
7#include <Rose/BinaryAnalysis/BasicTypes.h>
10namespace BinaryAnalysis {
11namespace InstructionSemantics {
14namespace TaintSemantics {
72#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
74 friend class boost::serialization::access;
77 void serialize(S &s,
const unsigned ) {
78 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
87 explicit SValue(
size_t nbits):
Super(nbits) {}
89 SValue(
size_t nbits, uint64_t number):
Super(nbits, number) {}
127 ASSERT_not_null(value);
161 if (new_width!=0 && new_width!=retval->nBits())
162 retval->set_width(new_width);
176 ASSERT_not_null(retval);
217using RegisterStatePtr = SymbolicSemantics::RegisterStatePtr;
231using MemoryStatePtr = MemoryListStatePtr;
239using StatePtr = SymbolicSemantics::StatePtr;
275#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
277 friend class boost::serialization::access;
280 void serialize(S &s,
const unsigned ) {
281 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
340 size_t begin_bit,
size_t end_bit)
override;
394#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
A RegisterState for any architecture.
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 semantics machine states.
Controls merging of symbolic values.
Defines RISC operators for the SymbolicSemantics domain.
Type of values manipulated by the SymbolicSemantics domain.
ExprPtr expr
The symbolic expression for this value.
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.
RiscOperatorsPtr Ptr
Shared-ownership pointer.
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.
SymbolicSemantics::SValue Super
Base type.
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.
void taintedness(Taintedness)
Property: Taintedness.
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.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for binary types.
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 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.
Taintedness
Whether a value is tainted.
@ BOTTOM
Neither tainted nor untainted.
@ TOP
Both tainted and untainted at the same time.
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.