1#ifndef ROSE_BinaryAnalysis_Partitioner2_Semantics_H
2#define ROSE_BinaryAnalysis_Partitioner2_Semantics_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_BINARY_ANALYSIS
7#include <Rose/BinaryAnalysis/MemoryMap.h>
8#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
9#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/MemoryCellMap.h>
10#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
11#include <Rose/BinaryAnalysis/SymbolicExpression.h>
13#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
14#include <boost/serialization/access.hpp>
18namespace BinaryAnalysis {
19namespace Partitioner2 {
57template<
class Super = InstructionSemantics::SymbolicSemantics::MemoryListState>
61 using Ptr = boost::shared_ptr<MemoryState>;
65 std::vector<SValuePtr> addressesRead_;
68#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
70 friend class boost::serialization::access;
71 template<
class S>
void serialize(S&,
unsigned version);
79 :
Super(protocell), enabled_(true) {}
83 :
Super(addrProtoval, valProtoval), enabled_(true) {}
107 return instance(addrProtoval, valProtoval);
127 Ptr retval = as<MemoryState>(x);
157 const std::vector<SValuePtr>&
addressesRead()
const {
return addressesRead_; }
186 bool withSideEffects);
221 static const size_t TRIM_THRESHOLD_DFLT = 100;
225#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
227 friend class boost::serialization::access;
228 template<
class S>
void serialize(S&,
unsigned version);
302 return readOrPeekMemory(addr, dflt, addrOps, valOps,
true);
311 return readOrPeekMemory(addr, dflt, addrOps, valOps,
false);
320 bool withSideEffects) {
321 using namespace InstructionSemantics;
322 ASSERT_require2(8==dflt->
nBits(),
"multi-byte reads should have been handled above this call");
337 bool isModifiable = map_->at(va).require(MemoryMap::WRITABLE).exists();
338 bool isInitialized = map_->at(va).require(MemoryMap::INITIALIZED).exists();
344 if (1 == map_->at(va).limit(1).read(&
byte).size())
354 valueRead = indeterminate;
360 auto val = SymbolicSemantics::SValue::promote(valOps->
undefined_(8));
361 val->set_expression(valueRead);
362 symbolicDefault = val;
366 const bool isPresentSymbolically = [
this, &addr]() {
367 struct CellFinder: BaseSemantics::MemoryCell::Visitor {
368 BaseSemantics::SValue::Ptr needle;
371 explicit CellFinder(
const BaseSemantics::SValue::Ptr &addr)
373 ASSERT_not_null(addr);
376 void operator()(BaseSemantics::MemoryCell::Ptr &haystack)
override {
377 ASSERT_not_null(haystack);
378 if (haystack->address()->mustEqual(needle))
382 this->traverse(cellFinder);
383 return cellFinder.found;
387 if (!isPresentSymbolically &&
isInitialized && !isModifiable)
388 return symbolicDefault;
391 if (!isPresentSymbolically) {
396 Super::writeMemory(addr, symbolicDefault, addrOps, valOps);
403 if (withSideEffects) {
404 return Super::readMemory(addr, symbolicDefault, addrOps, valOps);
406 return Super::peekMemory(addr, symbolicDefault, addrOps, valOps);
418 Super::writeMemory(addr, value, addrOps, valOps);
424 namespace BS = InstructionSemantics::BaseSemantics;
433 const bool isEmpty = as<const BS::MemoryCellState>(
this) ?
434 as<const BS::MemoryCellState>(
this)->allCells().empty() :
437 if (as<const BS::MemoryCellMap>(
this)) {
442 BS::Indent indent(fmt);
446 Super::print(out, fmt);
27namespace Semantics {
…}
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.
virtual SgAsmInstruction * currentInstruction() const
Property: Current instruction.
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.
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 an address space.
bool enabled() const
Property: Enabled.
boost::shared_ptr< MemoryState > Ptr
Shared-ownership pointer to a Semantics::MemoryState.
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::AddressSpacePtr 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.
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.
boost::shared_ptr< AddressSpace > AddressSpacePtr
Shared-ownership pointer for AddressSpace objects.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
InstructionSemantics::BaseSemantics::RegisterStateGenericPtr RegisterStatePtr
Reference counting pointer to register state.
InstructionSemantics::BaseSemantics::StatePtr StatePtr
Reference counting pointer to total state.
boost::shared_ptr< MemoryListState > MemoryListStatePtr
Shared-ownership pointer to a MemoryListState.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to the RISC operators object.
boost::shared_ptr< MemoryMapState > MemoryMapStatePtr
Shared-ownership pointer to a MemoryMapState.
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::uint64_t Address
Address.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
ROSE_DLL_API bool isInitialized()
Checks whether the library has been initialized.