1 #ifndef ROSE_BinaryAnalysis_InstructionSemantics_SymbolicSemantics_H
2 #define ROSE_BinaryAnalysis_InstructionSemantics_SymbolicSemantics_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #ifndef __STDC_FORMAT_MACROS
7 #define __STDC_FORMAT_MACROS
11 #include <Rose/BinaryAnalysis/BasicTypes.h>
12 #include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics.h>
13 #include <Rose/BinaryAnalysis/SmtSolver.h>
14 #include <Rose/BinaryAnalysis/SymbolicExpression.h>
16 #include "Cxx_GrammarSerialization.h"
18 #include <boost/serialization/access.hpp>
19 #include <boost/serialization/base_object.hpp>
20 #include <boost/serialization/export.hpp>
21 #include <boost/serialization/set.hpp>
27 namespace BinaryAnalysis {
28 namespace InstructionSemantics {
48 namespace SymbolicSemantics {
56 using InsnSet = std::set<SgAsmInstruction*>;
63 namespace AllowSideEffects {
93 retval->setSizeLimit(n);
214 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
216 friend class boost::serialization::access;
219 void serialize(S &s,
const unsigned ) {
220 roseAstSerializationRegistration(s);
221 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
222 s & BOOST_SERIALIZATION_NVP(expr);
223 s & BOOST_SERIALIZATION_NVP(defs);
231 explicit SValue(
size_t nbits):
BaseSemantics::SValue(nbits) {
234 SValue(
size_t nbits, uint64_t number):
BaseSemantics::SValue(nbits) {
271 ASSERT_not_null(value);
294 SValuePtr retval(
new SValue(*
this));
295 if (new_width!=0 && new_width!=retval->nBits())
296 retval->set_width(new_width);
309 ASSERT_not_null(retval);
316 virtual bool isBottom()
const override;
331 ASSERT_always_require(nbits==
nBits());
335 return expr->isIntegerConstant();
341 virtual void set_comment(
const std::string&)
const override;
353 virtual SValuePtr
substitute(
const SValuePtr &from,
const SValuePtr &to,
const SmtSolverPtr &solver)
const;
388 ASSERT_not_null(new_expr);
390 width = new_expr->nBits();
558 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
560 friend class boost::serialization::access;
563 void serialize(S &s,
const unsigned ) {
564 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
573 : cellCompressor_(CellCompressorChoice::
instance()) {}
579 :
BaseSemantics::MemoryCellList(addrProtoval, valProtoval), cellCompressor_(CellCompressorChoice::
instance()) {}
581 MemoryListState(
const MemoryListState &other)
582 :
BaseSemantics::MemoryCellList(other), cellCompressor_(other.cellCompressor_) {}
600 static MemoryListStatePtr
instance(
const MemoryListStatePtr &other) {
611 return instance(addrProtoval, valProtoval);
630 MemoryListStatePtr retval = boost::dynamic_pointer_cast<
MemoryListState>(x);
631 ASSERT_not_null(retval);
663 AllowSideEffects::Flag allowSideEffects);
678 CellCompressor::Ptr get_cell_compressor() const ROSE_DEPRECATED("use
cellCompressor");
679 void set_cell_compressor(const CellCompressor::
Ptr&) ROSE_DEPRECATED("use cellCompressor");
717 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
719 friend class boost::serialization::access;
722 void serialize(S &s,
const unsigned ) {
723 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
754 static MemoryMapStatePtr
instance(
const MemoryMapStatePtr &other) {
765 return instance(addrProtoval, valProtoval);
784 MemoryMapStatePtr retval = boost::dynamic_pointer_cast<
MemoryMapState>(x);
785 ASSERT_not_null(retval);
804 typedef MemoryListState MemoryState;
805 typedef MemoryListStatePtr MemoryStatePtr;
868 uint64_t trimThreshold_;
869 bool reinterpretMemoryReads_;
870 bool reinterpretRegisterReads_;
871 size_t nTrimmed_ = 0;
876 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
878 friend class boost::serialization::access;
881 void serialize(S &s,
const unsigned ) {
882 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
883 s & BOOST_SERIALIZATION_NVP(omit_cur_insn);
884 s & BOOST_SERIALIZATION_NVP(computingDefiners_);
885 s & BOOST_SERIALIZATION_NVP(computingMemoryWriters_);
886 s & BOOST_SERIALIZATION_NVP(computingRegisterWriters_);
887 s & BOOST_SERIALIZATION_NVP(trimThreshold_);
940 retval->defined_by(currentInstruction());
947 retval->defined_by(currentInstruction());
954 SValuePtr svalueExpr(
const ExprPtr &expr,
const InsnSet &defs=InsnSet()) {
955 SValuePtr newval =
SValue::promote(protoval()->undefined_(expr->nBits()));
956 newval->set_expression(expr);
957 newval->set_defining_instructions(defs);
962 SValuePtr svalueUndefined(
size_t nbits) {
966 SValuePtr svalueBottom(
size_t nbits) {
970 SValuePtr svalueUnspecified(
size_t nbits) {
974 SValuePtr svalueNumber(
size_t nbits, uint64_t value) {
978 SValuePtr svalueBoolean(
bool b) {
1055 bool getset_omit_cur_insn(
bool b) {
bool retval = omit_cur_insn; omit_cur_insn=b;
return retval; }
1154 virtual void substitute(
const SValuePtr &from,
const SValuePtr &to);
1176 virtual void interrupt(
int majr,
int minr)
override;
1185 size_t begin_bit,
size_t end_bit)
override;
1204 IteStatus&)
override;
1250 AllowSideEffects::Flag);
1258 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
MergerPtr Ptr
Shared-ownership pointer for a Merger object.
Base classes for instruction semantics.
static const unsigned UNSPECIFIED
Value is somehow unspecified.
Sawyer::SharedPointer< Interior > InteriorPtr
Reference counting pointer.
virtual void set_expression(const ExprPtr &new_expr)
Changes the expression stored in the value.
Simple list-based memory state.
virtual size_t add_defining_instructions(const InsnSet &to_add)
Adds definitions to the list of defining instructions.
virtual BaseSemantics::SValuePtr peekMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Read a byte from memory with no side effects.
Functor for handling a memory read whose address matches more than one memory cell.
static Ptr instance()
Allocating constructor.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
size_t setSizeLimit() const
Property: Maximum set size.
Functor for handling a memory read whose address matches more than one memory cell.
virtual BaseSemantics::SValuePtr boolean_(bool b) override
Returns a Boolean value.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells) override
Compress the cells into a single value.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
static MemoryMapStatePtr promote(const BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
Base class for machine instructions.
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override
Create a new undefined semantic value.
static MemoryMapStatePtr instance(const MemoryMapStatePtr &other)
Instantiates a new deep copy of an existing state.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
static SValuePtr instance_integer(size_t nbits, uint64_t value)
Instantiate a new concrete value.
void computingDefiners(DefinersMode m)
Property: Track which instructions define a semantic value.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells) override
Compress the cells into a single value.
Functor for handling a memory read whose address matches more than one memory cell.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a SymbolicSemantics value.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
Simple map-based memory state.
RiscOperatorsPtr Ptr
Shared-ownership pointer.
Base class for symbolic expression nodes.
static Ptr instance(size_t n)
Allocating constructor.
Sawyer::SharedPointer< Leaf > LeafPtr
Reference counting pointer.
Holds a value or nothing.
void computingRegisterWriters(WritersMode m)
Property: Track latest writer to each register.
static MemoryListStatePtr promote(const BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
void reinterpretRegisterReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
DefinersMode computingDefiners() const
Property: Track which instructions define a semantic value.
bool reinterpretMemoryReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
Main namespace for the ROSE library.
WritersMode computingMemoryWriters() const
Property: Track which instructions write to each memory location.
static Ptr instance()
Allocating constructor.
boost::shared_ptr< MemoryCell > MemoryCellPtr
Shared-ownership pointer to a memory cell.
static Ptr instance()
Allocating constructor.
A RegisterState for any architecture.
ExprPtr expr
The symbolic expression for this value.
static MemoryListStatePtr instance(const MemoryListStatePtr &other)
Instantiates a new deep copy of an existing state.
virtual SValuePtr number_(size_t nbits, uint64_t value)
Returns a number of the specified bit width.
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Write a byte to memory.
Functor for handling a memory read that found more than one cell that might alias the requested addre...
static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
void reinterpretMemoryReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1)
Adds instructions to the list of defining instructions.
virtual BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
WritersMode
How to update the list of writers stored at each abstract location.
Reference-counting intrusive smart pointer.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
Functor for handling a memory read whose address matches more than one memory cell.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
boost::shared_ptr< class MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to symbolic memory state.
static SValuePtr instance_bottom(size_t nbits)
Instantiate a new data-flow bottom value of specified width.
Controls state merge operations.
CellCompressor::Ptr cellCompressor() const
Callback for handling a memory read whose address matches more than one memory cell.
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 print(std::ostream &, BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
virtual BaseSemantics::MemoryStatePtr clone() const override
Virtual copy constructor.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override
Create a new unspecified semantic value.
static SValuePtr instance_unspecified(size_t nbits)
Instantiate a new unspecified value of specified width.
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells) override
Compress the cells into a single value.
MemoryListStatePtr Ptr
Shared-ownership pointer.
static Ptr instance()
Allocating constructor.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override
Data-flow bottom value.
virtual size_t add_defining_instructions(const SValuePtr &source)
Adds definitions to the list of defining instructions.
virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const
Substitute one value for another throughout a value.
static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
virtual bool isBottom() const override
Determines whether a value is a data-flow bottom.
DefinersMode
How to update the list of definers stored in each semantic value.
virtual void set_comment(const std::string &) const override
Some subclasses support the ability to add comments to values.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override
Create a new concrete semantic value.
Describes (part of) a physical CPU register.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells)=0
Compress the cells into a single value.
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.
WritersMode computingRegisterWriters() const
Property: Track latest writer to each register.
size_t nTrimmed() const
Property: Number of symbolic expressions trimmed.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) override
Returns a number of the specified bit width.
virtual uint64_t get_number() const override
Virtual API.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Type of values manipulated by the SymbolicSemantics domain.
virtual bool is_number() const override
Virtual API.
static SValuePtr instance_symbolic(const SymbolicExpression::Ptr &value)
Instantiate a new symbolic value.
static SValuePtr instance()
Instantiate a new prototypical value.
std::list< MemoryCellPtr > CellList
List of memory cells.
boost::shared_ptr< class MemoryListState > MemoryListStatePtr
Shared-ownership pointer for symbolic list-based memory state.
virtual void set_expression(const SValuePtr &source)
Changes the expression stored in the value.
void computingMemoryWriters(WritersMode m)
Property: Track which instructions write to each memory location.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
static Ptr instance()
Allocating constructor.
SharedPointer< U > dynamicCast() const
Dynamic cast.
virtual void set_width(size_t nbits) override
Virtual API.
Base class for semantic values.
Defines RISC operators for the SymbolicSemantics domain.
virtual void set_defining_instructions(const InsnSet &new_defs)
Set defining instructions.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2)
Adds instructions to the list of defining instructions.
static SValuePtr instance_undefined(size_t nbits)
Instantiate a new undefined value of specified width.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
Base class for binary types.
Base class for reference counted objects.
virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Read a byte from memory.
Save only the latest writer.
static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
virtual SValuePtr boolean_(bool value)
Returns a Boolean value.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const override
Virtual constructor.
virtual const InsnSet & get_defining_instructions() const
Returns the set of instructions that defined this value.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
virtual void defined_by(SgAsmInstruction *insn)
Adds instructions to the list of defining instructions.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
Leaf node of an expression tree for instruction semantics.
void nTrimmed(size_t n)
Property: Number of symbolic expressions trimmed.
virtual std::string get_comment() const override
Some subclasses support the ability to add comments to values.
void trimThreshold(uint64_t n)
Property: Maximum size of expressions.
virtual const ExprPtr & get_expression() const
Returns the expression stored in this value.
InsnSet defs
Instructions defining this value.
Interior node of an expression tree for instruction semantics.
bool reinterpretRegisterReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
uint64_t trimThreshold() const
Property: Maximum size of expressions.
Base class for most instruction semantics RISC operators.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const
Virtual constructor.
Type of symbolic expression.
Base class for semantics machine states.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3)
Adds instructions to the list of defining instructions.
Save only the latest definer.
static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
void setSizeLimit(size_t n)
Property: Maximum set size.
Controls merging of symbolic values.
size_t nBits() const
Property: value width.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const BaseSemantics::CellList &cells) override
Compress the cells into a single value.
virtual void set_defining_instructions(const SValuePtr &source)
Set defining instructions.
virtual BaseSemantics::MemoryStatePtr clone() const override
Virtual copy constructor.
MemoryMapStatePtr Ptr
Shared-ownership pointer.