1 #ifndef ROSE_BinaryAnalysis_InstructionSemantics2_SymbolicSemantics_H
2 #define ROSE_BinaryAnalysis_InstructionSemantics2_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/InstructionSemantics2/BaseSemantics.h>
12 #include "Cxx_GrammarSerialization.h"
13 #include <Rose/BinaryAnalysis/SmtSolver.h>
14 #include <Rose/BinaryAnalysis/SymbolicExpr.h>
16 #include <boost/serialization/access.hpp>
17 #include <boost/serialization/base_object.hpp>
18 #include <boost/serialization/export.hpp>
19 #include <boost/serialization/set.hpp>
25 namespace BinaryAnalysis {
26 namespace InstructionSemantics2 {
46 namespace SymbolicSemantics {
54 typedef std::set<SgAsmInstruction*> InsnSet;
61 namespace AllowSideEffects {
81 typedef MergerPtr
Ptr;
91 retval->setSizeLimit(n);
212 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
214 friend class boost::serialization::access;
217 void serialize(S &s,
const unsigned ) {
218 roseAstSerializationRegistration(s);
219 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
220 s & BOOST_SERIALIZATION_NVP(expr);
221 s & BOOST_SERIALIZATION_NVP(defs);
229 explicit SValue(
size_t nbits):
BaseSemantics::SValue(nbits) {
232 SValue(
size_t nbits, uint64_t number):
BaseSemantics::SValue(nbits) {
269 ASSERT_not_null(value);
292 SValuePtr retval(
new SValue(*
this));
293 if (new_width!=0 && new_width!=retval->nBits())
294 retval->set_width(new_width);
307 ASSERT_not_null(retval);
314 virtual bool isBottom()
const override;
329 ASSERT_require(nbits==
nBits());
333 return expr->isIntegerConstant();
339 virtual void set_comment(
const std::string&)
const override;
351 virtual SValuePtr
substitute(
const SValuePtr &from,
const SValuePtr &to,
const SmtSolverPtr &solver)
const;
386 ASSERT_not_null(new_expr);
388 width = new_expr->nBits();
492 const MemoryCellList::CellList &cells) = 0;
556 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
558 friend class boost::serialization::access;
561 void serialize(S &s,
const unsigned ) {
562 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
571 : cellCompressor_(CellCompressorChoice::
instance()) {}
577 :
BaseSemantics::MemoryCellList(addrProtoval, valProtoval), cellCompressor_(CellCompressorChoice::
instance()) {}
579 MemoryListState(
const MemoryListState &other)
580 :
BaseSemantics::MemoryCellList(other), cellCompressor_(other.cellCompressor_) {}
598 static MemoryListStatePtr
instance(
const MemoryListStatePtr &other) {
609 return instance(addrProtoval, valProtoval);
628 MemoryListStatePtr retval = boost::dynamic_pointer_cast<
MemoryListState>(x);
629 ASSERT_not_null(retval);
661 AllowSideEffects::Flag allowSideEffects);
676 CellCompressor::Ptr get_cell_compressor() const ROSE_DEPRECATED("use
cellCompressor");
677 void set_cell_compressor(const CellCompressor::
Ptr&) ROSE_DEPRECATED("use cellCompressor");
715 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
717 friend class boost::serialization::access;
720 void serialize(S &s,
const unsigned ) {
721 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
752 static MemoryMapStatePtr
instance(
const MemoryMapStatePtr &other) {
763 return instance(addrProtoval, valProtoval);
782 MemoryMapStatePtr retval = boost::dynamic_pointer_cast<
MemoryMapState>(x);
783 ASSERT_not_null(retval);
802 typedef MemoryListState MemoryState;
803 typedef MemoryListStatePtr MemoryStatePtr;
866 uint64_t trimThreshold_;
867 bool reinterpretMemoryReads_;
868 bool reinterpretRegisterReads_;
869 size_t nTrimmed_ = 0;
874 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
876 friend class boost::serialization::access;
879 void serialize(S &s,
const unsigned ) {
880 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
881 s & BOOST_SERIALIZATION_NVP(omit_cur_insn);
882 s & BOOST_SERIALIZATION_NVP(computingDefiners_);
883 s & BOOST_SERIALIZATION_NVP(computingMemoryWriters_);
884 s & BOOST_SERIALIZATION_NVP(computingRegisterWriters_);
885 s & BOOST_SERIALIZATION_NVP(trimThreshold_);
894 computingRegisterWriters_(
TRACK_LATEST_WRITER), trimThreshold_(0), reinterpretMemoryReads_(true),
895 reinterpretRegisterReads_(true) {}
900 reinterpretMemoryReads_(true), reinterpretRegisterReads_(true) {
902 ASSERT_always_not_null(protoval);
903 ASSERT_always_not_null2(protoval.
dynamicCast<SValue>(),
904 "SymbolicSemantics supports only symbolic SValue types or derivatives thereof");
910 reinterpretMemoryReads_(true), reinterpretRegisterReads_(true) {
912 ASSERT_always_not_null(state);
913 ASSERT_always_not_null(state->registerState());
914 ASSERT_always_not_null2(boost::dynamic_pointer_cast<RegisterState>(state->registerState()),
915 "SymbolicSemantics supports only RegisterStateGeneric or derivatives thereof");
916 ASSERT_always_not_null(state->protoval());
917 ASSERT_always_not_null2(state->protoval().dynamicCast<SValue>(),
918 "SymbolicSemantics supports only symbolic SValue types or derivatives thereof");
965 RiscOperatorsPtr retval = boost::dynamic_pointer_cast<
RiscOperators>(x);
966 ASSERT_not_null(retval);
976 retval->defined_by(currentInstruction());
983 retval->defined_by(currentInstruction());
990 SValuePtr svalueExpr(
const ExprPtr &expr,
const InsnSet &defs=InsnSet()) {
991 SValuePtr newval =
SValue::promote(protoval()->undefined_(expr->nBits()));
992 newval->set_expression(expr);
993 newval->set_defining_instructions(defs);
998 SValuePtr svalueUndefined(
size_t nbits) {
1002 SValuePtr svalueBottom(
size_t nbits) {
1006 SValuePtr svalueUnspecified(
size_t nbits) {
1010 SValuePtr svalueNumber(
size_t nbits, uint64_t value) {
1014 SValuePtr svalueBoolean(
bool b) {
1019 SValuePtr svalue_number(
size_t nbits, uint64_t value) ROSE_DEPRECATED(
"use svalueNumber instead") {
1020 return svalueNumber(nbits, value);
1024 SValuePtr svalue_boolean(
bool b) ROSE_DEPRECATED(
"use svalueBoolean instead") {
1025 return svalueBoolean(b);
1029 SValuePtr svalue_unspecified(
size_t nbits) ROSE_DEPRECATED(
"use svalueUnspecified instead") {
1030 return svalueUnspecified(nbits);
1034 SValuePtr svalue_bottom(
size_t nbits) ROSE_DEPRECATED(
"use svalueBottom instead") {
1035 return svalueBottom(nbits);
1039 SValuePtr svalue_undefined(
size_t nbits) ROSE_DEPRECATED(
"use svalueUndefined instead") {
1040 return svalueUndefined(nbits);
1044 SValuePtr svalue_expr(
const ExprPtr &expr,
const InsnSet &defs=InsnSet()) ROSE_DEPRECATED("use svalueExpr instead") {
1045 return svalueExpr(expr, defs);
1121 bool getset_omit_cur_insn(
bool b) {
bool retval = omit_cur_insn; omit_cur_insn=b;
return retval; }
1220 virtual void substitute(
const SValuePtr &from,
const SValuePtr &to);
1242 virtual void interrupt(
int majr,
int minr)
override;
1251 size_t begin_bit,
size_t end_bit)
override;
1315 AllowSideEffects::Flag);
1323 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
Sawyer::SharedPointer< class Merger > MergerPtr
Shared-ownership pointer for a merge control object.
void computingDefiners(DefinersMode m)
Property: Track which instructions define a semantic value.
InsnSet defs
Instructions defining this value.
static RegisterStateGenericPtr instance(const SValuePtr &protoval, const RegisterDictionary *regdict)
Instantiate a new register state.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
virtual void set_defining_instructions(const InsnSet &new_defs)
Set defining instructions.
virtual void print(std::ostream &, BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
bool reinterpretMemoryReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
static SValuePtr instance_integer(size_t nbits, uint64_t value)
Instantiate a new concrete value.
virtual void set_width(size_t nbits) override
Virtual API.
virtual bool must_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
Leaf node of an expression tree for instruction semantics.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
Defines RISC operators for the SymbolicSemantics domain.
boost::shared_ptr< class RegisterStateGeneric > RegisterStateGenericPtr
Shared-ownership pointer to generic register states.
virtual void set_expression(const SValuePtr &source)
Changes the expression stored in the value.
static MemoryMapStatePtr promote(const BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
Interior node of an expression tree for instruction semantics.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
static RiscOperatorsPtr instance(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified state.
virtual SValuePtr substitute(const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const
Substitute one value for another throughout a value.
Base class for machine instructions.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2)
Adds instructions to the list of defining instructions.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0)
Leaf constructor.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
static RiscOperatorsPtr instance(const RegisterDictionary *regdict, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object and configures it to use semantic values and states that are ...
void computingRegisterWriters(WritersMode m)
Property: Track latest writer to each register.
virtual size_t add_defining_instructions(const SValuePtr &source)
Adds definitions to the list of defining instructions.
static SValuePtr promote(const BaseSemantics::SValuePtr &v)
Promote a base value to a SymbolicSemantics value.
virtual void writeMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &value, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Write a byte to memory.
virtual SValuePtr operator()(const SValuePtr &address, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps, const MemoryCellList::CellList &cells)=0
Compress the cells into a single value.
Holds a value or nothing.
Save only the latest definer.
static const unsigned UNSPECIFIED
Value is somehow unspecified.
virtual void set_defining_instructions(const SValuePtr &source)
Set defining instructions.
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0)
Leaf constructor.
static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x)
Run-time promotion of a base RiscOperators pointer to symbolic operators.
Type of symbolic expression.
virtual BaseSemantics::SValuePtr boolean_(bool b) override
Returns a Boolean value.
static Ptr instance()
Allocating constructor.
void reinterpretRegisterReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual void defined_by(SgAsmInstruction *insn)
Adds instructions to the list of defining instructions.
void trimThreshold(uint64_t n)
Property: Maximum size of expressions.
virtual void set_comment(const std::string &) const override
Some subclasses support the ability to add comments to values.
virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override
Data-flow bottom value.
Main namespace for the ROSE library.
virtual void set_expression(const ExprPtr &new_expr)
Changes the expression stored in the value.
size_t setSizeLimit() const
Property: Maximum set size.
static MemoryListStatePtr promote(const BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
static MemoryListStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
virtual BaseSemantics::SValuePtr readMemory(const BaseSemantics::SValuePtr &addr, const BaseSemantics::SValuePtr &dflt, BaseSemantics::RiscOperators *addrOps, BaseSemantics::RiscOperators *valOps) override
Read a byte from memory.
Reference-counting intrusive smart pointer.
virtual SValuePtr boolean_(bool value)
Returns a Boolean value.
void reinterpretMemoryReads(bool b)
Property: Reinterpret data as unsigned integers when reading from memory or registers.
virtual bool is_number() const override
Virtual API.
virtual std::string get_comment() const override
Some subclasses support the ability to add comments to values.
static SValuePtr instance_bottom(size_t nbits)
Instantiate a new data-flow bottom value of specified width.
WritersMode computingMemoryWriters() const
Property: Track which instructions write to each memory location.
MemoryMapStatePtr Ptr
Shared-ownership pointer.
static MemoryMapStatePtr instance(const BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
Controls state merge operations.
static MemoryMapStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
Save only the latest writer.
virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override
Create a new unspecified semantic value.
DefinersMode
How to update the list of definers stored in each semantic value.
Controls merging of symbolic values.
virtual uint64_t get_number() const override
Virtual API.
void computingMemoryWriters(WritersMode m)
Property: Track which instructions write to each memory location.
Base classes for instruction semantics.
ExprPtr expr
The symbolic expression for this value.
static const unsigned BOTTOM
Value represents bottom in dataflow analysis.
WritersMode computingRegisterWriters() const
Property: Track latest writer to each register.
static SValuePtr instance_undefined(size_t nbits)
Instantiate a new undefined value of specified width.
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.
void setSizeLimit(size_t n)
Property: Maximum set size.
Describes (part of) a physical CPU register.
virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
static Ptr instance(size_t n)
Allocating constructor.
boost::shared_ptr< class MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to symbolic memory state.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const
Virtual constructor.
static SValuePtr instance()
Instantiate a new prototypical value.
size_t nTrimmed() const
Property: Number of symbolic expressions trimmed.
Base class for semantics machine states.
MemoryListStatePtr Ptr
Shared-ownership pointer.
virtual const InsnSet & get_defining_instructions() const
Returns the set of instructions that defined this value.
Functor for handling a memory read whose address matches more than one memory cell.
static MemoryListStatePtr instance(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
DefinersMode computingDefiners() const
Property: Track which instructions define a semantic value.
virtual BaseSemantics::MemoryStatePtr clone() const override
Virtual copy constructor.
Base class for semantic values.
virtual const ExprPtr & get_expression() const
Returns the expression stored in this value.
Simple map-based memory state.
CellCompressor::Ptr cellCompressor() const
Callback for handling a memory read whose address matches more than one memory cell.
bool reinterpretRegisterReads() const
Property: Reinterpret data as unsigned integers when reading from memory or registers.
uint64_t trimThreshold() const
Property: Maximum size of expressions.
static RiscOperatorsPtr instance(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr())
Instantiates a new RiscOperators object with specified prototypical values.
WritersMode
How to update the list of writers stored at each abstract location.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) override
Returns a number of the specified bit width.
virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override
Create a new concrete semantic value.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::MemoryCellPtr &protocell) const override
Virtual constructor.
boost::shared_ptr< MemoryCell > MemoryCellPtr
Shared-ownership pointer to a memory cell.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
static Ptr instance()
Allocating constructor.
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.
std::list< MemoryCellPtr > CellList
List of memory cells.
size_t nBits() const
Property: value width.
static StatePtr instance(const RegisterStatePtr ®isters, const MemoryStatePtr &memory)
Instantiate a new state object with specified register and memory states.
Base class for binary types.
Base class for reference counted objects.
Type of values manipulated by the SymbolicSemantics domain.
static Ptr instance()
Allocating constructor.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1)
Adds instructions to the list of defining instructions.
static SValuePtr instance_unspecified(size_t nbits)
Instantiate a new unspecified value of specified width.
static Ptr instance()
Allocating constructor.
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.
virtual size_t add_defining_instructions(const InsnSet &to_add)
Adds definitions to the list of defining instructions.
static MemoryMapStatePtr instance(const MemoryMapStatePtr &other)
Instantiates a new deep copy of an existing state.
Base class for symbolic expression nodes.
A RegisterState for any architecture.
virtual bool may_equal(const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual API.
Functor for handling a memory read that found more than one cell that might alias the requested addre...
virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override
Create a new undefined semantic value.
Defines registers available for a particular architecture.
Functor for handling a memory read whose address matches more than one memory cell.
virtual SValuePtr number_(size_t nbits, uint64_t value)
Returns a number of the specified bit width.
static SValuePtr instance_symbolic(const SymbolicExpr::Ptr &value)
Instantiate a new symbolic value.
virtual void defined_by(SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3)
Adds instructions to the list of defining instructions.
Simple list-based memory state.
static Ptr instance()
Allocating constructor.
static MemoryListStatePtr instance(const MemoryListStatePtr &other)
Instantiates a new deep copy of an existing state.
virtual BaseSemantics::MemoryStatePtr clone() const override
Virtual copy constructor.
MergerPtr Ptr
Shared-ownership pointer for a Merger object.
virtual BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
virtual BaseSemantics::MemoryStatePtr create(const BaseSemantics::SValuePtr &addrProtoval, const BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
void nTrimmed(size_t n)
Property: Number of symbolic expressions trimmed.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
Functor for handling a memory read whose address matches more than one memory cell.
Functor for handling a memory read whose address matches more than one memory cell.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
virtual bool isBottom() const override
Determines whether a value is a data-flow bottom.
RiscOperatorsPtr Ptr
Shared-ownership pointer.
boost::shared_ptr< class MemoryListState > MemoryListStatePtr
Shared-ownership pointer for symbolic list-based memory state.