1#ifndef ROSE_BinaryAnalysis_Partitioner2_Semantics_H
2#define ROSE_BinaryAnalysis_Partitioner2_Semantics_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_BINARY_ANALYSIS
6#include <Rose/BinaryAnalysis/MemoryMap.h>
7#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
8#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
9#include <Rose/BinaryAnalysis/SymbolicExpression.h>
11#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
12#include <boost/serialization/access.hpp>
16namespace BinaryAnalysis {
17namespace Partitioner2 {
55template<
class Super = InstructionSemantics::SymbolicSemantics::MemoryListState>
59 typedef boost::shared_ptr<MemoryState>
Ptr;
63 std::vector<SValuePtr> addressesRead_;
66#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
68 friend class boost::serialization::access;
69 template<
class S>
void serialize(S&,
unsigned version);
77 :
Super(protocell), enabled_(true) {}
81 :
Super(addrProtoval, valProtoval), enabled_(true) {}
105 return instance(addrProtoval, valProtoval);
125 Ptr retval = boost::dynamic_pointer_cast<MemoryState>(x);
155 const std::vector<SValuePtr>&
addressesRead()
const {
return addressesRead_; }
184 bool withSideEffects);
219 static const size_t TRIM_THRESHOLD_DFLT = 100;
223#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
225 friend class boost::serialization::access;
226 template<
class S>
void serialize(S&,
unsigned version);
304 return readOrPeekMemory(addr, dflt, addrOps, valOps,
true);
313 return readOrPeekMemory(addr, dflt, addrOps, valOps,
false);
322 bool withSideEffects) {
323 using namespace InstructionSemantics;
330 ASSERT_require2(8==dflt->
nBits(),
"multi-byte reads should have been handled above this call");
332 bool isModifiable = map_->at(va).require(MemoryMap::WRITABLE).exists();
333 bool isInitialized = map_->at(va).require(MemoryMap::INITIALIZED).exists();
336 if (1 == map_->at(va).limit(1).read(&
byte).size()) {
342 SymbolicSemantics::SValuePtr val = SymbolicSemantics::SValue::promote(valOps->
undefined_(8));
343 val->set_expression(expr);
349 if (withSideEffects) {
350 return Super::readMemory(addr, dflt, addrOps, valOps);
352 return Super::peekMemory(addr, dflt, addrOps, valOps);
364 Super::writeMemory(addr, value, addrOps, valOps);
376 Super::print(out, fmt);
Simple list-based memory state.
A RegisterState for any architecture.
Base class for most instruction semantics RISC operators.
virtual SValuePtr undefined_(size_t nbits)
Returns a new undefined value.
virtual SmtSolverPtr solver() const
Property: Satisfiability module theory (SMT) solver.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
Sawyer::Optional< uint64_t > toUnsigned() const
Converts a concrete value to a native unsigned integer.
size_t nBits() const
Property: value width.
Base class for semantics machine states.
BaseSemantics::MemoryCellList Super
Base type.
Defines RISC operators for the SymbolicSemantics domain.
Type of values manipulated by the SymbolicSemantics domain.
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 &)
Promote a base value to a SymbolicSemantics value.
boost::shared_ptr< MemoryState > Ptr
Shared-ownership pointer to a Semantics::MemoryState.
std::vector< SValuePtr > & addressesRead()
Property: concrete virtual addresses that were read.
const std::vector< SValuePtr > & addressesRead() const
Property: concrete virtual addresses that were read.
virtual void writeMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr, const InstructionSemantics::BaseSemantics::SValuePtr &value, InstructionSemantics::BaseSemantics::RiscOperators *addrOps, InstructionSemantics::BaseSemantics::RiscOperators *valOps) override
Write a byte to memory.
void print(std::ostream &, InstructionSemantics::BaseSemantics::Formatter &) const override
Print a memory state to more than one line of output.
bool enabled() const
Property: Enabled.
virtual InstructionSemantics::BaseSemantics::MemoryStatePtr create(const InstructionSemantics::BaseSemantics::SValuePtr &addrProtoval, const InstructionSemantics::BaseSemantics::SValuePtr &valProtoval) const override
Virtual constructor.
static Ptr instance(const InstructionSemantics::BaseSemantics::MemoryCellPtr &protocell)
Instantiates a new memory state having specified prototypical cells and value.
void enabled(bool b)
Property: Enabled.
void memoryMap(const MemoryMapPtr &map)
The memory map for the specimen.
virtual InstructionSemantics::BaseSemantics::MemoryStatePtr create(const InstructionSemantics::BaseSemantics::MemoryCellPtr &protocell) const override
Virtual constructor.
MemoryMapPtr memoryMap() const
The memory map for the specimen.
virtual InstructionSemantics::BaseSemantics::MemoryStatePtr clone() const override
Virtual copy constructor.
static Ptr instance(const Ptr &other)
Instantiates a new deep copy of an existing state.
virtual InstructionSemantics::BaseSemantics::SValuePtr readMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr, const InstructionSemantics::BaseSemantics::SValuePtr &dflt, InstructionSemantics::BaseSemantics::RiscOperators *addrOps, InstructionSemantics::BaseSemantics::RiscOperators *valOps) override
Read a byte from memory.
static Ptr promote(const InstructionSemantics::BaseSemantics::MemoryStatePtr &x)
Recasts a base pointer to a symbolic memory state.
static Ptr instance(const InstructionSemantics::BaseSemantics::SValuePtr &addrProtoval, const InstructionSemantics::BaseSemantics::SValuePtr &valProtoval)
Instantiates a new memory state having specified prototypical value.
virtual InstructionSemantics::BaseSemantics::SValuePtr peekMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr, const InstructionSemantics::BaseSemantics::SValuePtr &dflt, InstructionSemantics::BaseSemantics::RiscOperators *addrOps, InstructionSemantics::BaseSemantics::RiscOperators *valOps) override
Read a byte from memory with no side effects.
static RiscOperatorsPtr promote(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &)
Run-time promotion of a base RiscOperators pointer to our operators.
static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::StatePtr &, const SmtSolverPtr &)
Instantiate a new RiscOperators with specified state.
static RiscOperatorsPtr instance(const RegisterDictionaryPtr &, const SmtSolverPtr &, SemanticMemoryParadigm memoryParadigm=LIST_BASED_MEMORY)
Instantiate a new RiscOperators object and configure it using default values.
virtual void startInstruction(SgAsmInstruction *) override
Called at the beginning of every instruction.
static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &)
Instantiate a new RiscOperators object with specified prototypical values.
static RiscOperatorsPtr instance(const RegisterDictionaryPtr &)
Instantiate a new RiscOperators object and configure it using default values.
static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::StatePtr &)
Instantiate a new RiscOperators with specified state.
virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr create(const InstructionSemantics::BaseSemantics::StatePtr &state, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr create(const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver=SmtSolverPtr()) const override
Virtual allocating constructor.
static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::SValuePtr &protoval)
Instantiate a new RiscOperators object with specified prototypical values.
const Value & get() const
Dereference to obtain value.
Reference-counting intrusive smart pointer.
Base class for machine instructions.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
boost::shared_ptr< MemoryCell > MemoryCellPtr
Shared-ownership pointer to a memory cell.
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.
InstructionSemantics::SymbolicSemantics::SValue SValue
Semantic value in the partitioner.
MemoryState< InstructionSemantics::SymbolicSemantics::MemoryListState > MemoryListState
Memory state using a chronological list of cells.
MemoryState< InstructionSemantics::SymbolicSemantics::MemoryMapState > MemoryMapState
Memory state indexed by hash of address expressions.
InstructionSemantics::BaseSemantics::RegisterStateGenericPtr RegisterStatePtr
Reference counting pointer to register state.
InstructionSemantics::BaseSemantics::State State
Total state (registers and memory) for the partitioner.
boost::shared_ptr< MemoryListState > MemoryListStatePtr
Shared-ownership pointer to a MemoryListState.
InstructionSemantics::BaseSemantics::RegisterStateGeneric RegisterState
Register state for the partitioner.
boost::shared_ptr< MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to a MemoryMapState.
InstructionSemantics::BaseSemantics::StatePtr StatePtr
Reference counting pointer to total state.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to the RISC operators object.
InstructionSemantics::SymbolicSemantics::SValuePtr SValuePtr
Reference counting pointer to semantic value.
SemanticMemoryParadigm
Organization of semantic memory.
@ LIST_BASED_MEMORY
Precise but slow.
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.
Ptr makeSet(const Ptr &a, const Ptr &b, const SmtSolverPtr &solver=SmtSolverPtr(), const std::string &comment="", unsigned flags=0)
Interior node constructor.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
ROSE_DLL_API bool isInitialized()
Checks whether the library has been initialized.