1 #ifndef ROSE_BinaryAnalysis_ModelChecker_P2Model_H
2 #define ROSE_BinaryAnalysis_ModelChecker_P2Model_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <Rose/BinaryAnalysis/ModelChecker/SemanticCallbacks.h>
7 #include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
8 #include <Sawyer/CommandLine.h>
9 #include <Sawyer/Stack.h>
10 #include <Rose/BinaryAnalysis/InstructionSemantics2/SymbolicSemantics.h>
13 namespace BinaryAnalysis {
14 namespace ModelChecker {
77 rose_addr_t initialStackPointer_ = 0;
78 rose_addr_t framePointerDelta_ = (rose_addr_t)(-4);
146 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
148 friend class boost::serialization::access;
151 void serialize(S &s,
const unsigned ) {
152 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(
Super);
153 s & BOOST_SERIALIZATION_NVP(region_);
222 ASSERT_not_null(retval);
310 using Ptr = RiscOperatorsPtr;
316 size_t nInstructions_ = 0;
319 bool computeMemoryRegions_ =
false;
321 mutable SAWYER_THREAD_TRAITS::Mutex variableFinderMutex_;
452 number_(
size_t nBits, uint64_t value)
override;
529 using Ptr = SemanticCallbacksPtr;
537 mutable SAWYER_THREAD_TRAITS::Mutex unitsMutex_;
540 mutable SAWYER_THREAD_TRAITS::Mutex mutex_;
541 std::set<uint64_t> seenStates_;
542 size_t nDuplicateStates_ = 0;
543 size_t nSolverFailures_ = 0;
553 bool followingOnePath_ =
false;
554 std::list<ExecutionUnitPtr> onePath_;
685 virtual void reset()
override;
711 virtual std::vector<TagPtr>
714 virtual std::vector<TagPtr>
720 virtual std::vector<NextUnit>
723 #ifdef ROSE_HAVE_YAMLCPP
724 virtual std::list<ExecutionUnitPtr>
725 parsePath(
const YAML::Node&,
const std::string &sourceName)
override;
728 virtual std::list<ExecutionUnitPtr>
736 ExecutionUnitPtr findUnit(rose_addr_t va,
const Progress::Ptr&);
void checkUninitVar(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, size_t nBytes)
Test whether the specified address accesses an uninitialized variable.
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
SmtSolver::Memoizer::Ptr smtMemoizer() const
Property: SMT solver memoizer.
virtual void print(std::ostream &, InstructionSemantics2::BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
TestMode oobRead
How to test for out-of-bounds reads.
Symbolic values with memory regions.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
static Ptr instanceBottom(size_t nBits)
Instantiate a new data-flow bottom value.
MemoryType
Type of memory state to use.
virtual InstructionSemantics2::BaseSemantics::SValuePtr shiftRight(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override
Returns arg shifted right logically (no sign bit).
Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &)
Command-line switches for settings.
Defines RISC operators for the SymbolicSemantics domain.
void pushCallStack(const Partitioner2::FunctionPtr &callee, rose_addr_t initialSp, Sawyer::Optional< rose_addr_t > returnVa)
Push a function onto the call stack.
virtual InstructionSemantics2::BaseSemantics::SValuePtr addCarry(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b, InstructionSemantics2::BaseSemantics::SValuePtr &carryOut, InstructionSemantics2::BaseSemantics::SValuePtr &overflowed) override
Adds two integers of equal size and carry.
static Ptr instanceUnspecified(size_t nBits)
Instantiate a new unspecified value.
TestMode nullRead
How to test for reads from the null page.
virtual SmtSolver::Ptr createSolver() override
Create model checker solver.
virtual void writeMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr, const InstructionSemantics2::BaseSemantics::SValuePtr &value, const InstructionSemantics2::BaseSemantics::SValuePtr &cond) override
Writes a value to memory.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
Base class for machine instructions.
virtual std::list< ExecutionUnitPtr > parsePath(const Yaml::Node &, const std::string &sourceName) override
Construct a path from a YAML document.
TestMode uninitVar
How to test for uninitialized variable reads.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
const Variables::StackVariables & stackVariables() const
Property: Stack variables.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
virtual InstructionSemantics2::BaseSemantics::SValuePtr subtract(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b) override
Subtract one value from another.
size_t nSolverFailures() const
Property: Number of times the SMT solver failed.
void checkNullAccess(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, IoMode)
Test whether the specified address is considered to be null.
virtual InstructionSemantics2::BaseSemantics::SValuePtr instructionPointer(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Address of the next instruction.
Reverse chronological list.
bool followingOnePath() const
Property: Whether we are in follow-one-path mode.
rose_addr_t maxNullAddress
Maximum address of the null page.
void followOnePath(const std::list< ExecutionUnitPtr > &)
Cause this model to follow only one path through the specimen.
TestMode
Mode by which comparisons are made.
virtual InstructionSemantics2::BaseSemantics::SValuePtr signExtend(const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override
Sign extends a value.
void maybeInitCallStack(rose_addr_t insnVa)
Ensure call stack has a root function.
virtual std::vector< TagPtr > postExecute(const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Called after execution ends.
virtual InstructionSemantics2::BaseSemantics::SValuePtr shiftRightArithmetic(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override
Returns arg shifted right arithmetically (with sign bit).
A collection of related switch declarations.
size_t nUnitsReached() const
Property: Number of execution units reached.
virtual InstructionSemantics2::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) override
Returns a number of the specified bit width.
Detection is reported only if it must occur.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
void printCallStack(std::ostream &, const std::string &prefix)
Print information about the function call stack.
Main namespace for the ROSE library.
bool solverMemoization
Whether the SMT solver should use memoization.
Describes one funtion call in the call stack.
TestMode nullWrite
How to test for writes from the null page.
virtual CodeAddresses nextCodeAddresses(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Possible next code addresses.
virtual void attachModelCheckerSolver(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &) override
Associate solver with semantics.
virtual std::vector< NextUnit > nextUnits(const PathPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &) override
Discover next execution units.
virtual void reset() override
Reset internal data.
Addresses and completeness.
const Partitioner2::Partitioner & partitioner() const
Property: Partitioner.
static Ptr instanceUndefined(size_t nBits)
Instantiate a new undefined value.
virtual InstructionSemantics2::BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr, const InstructionSemantics2::BaseSemantics::SValuePtr &dflt, const InstructionSemantics2::BaseSemantics::SValuePtr &cond) override
Reads a value from memory.
size_t nInstructions() const
Property: Number of instructions executed.
virtual InstructionSemantics2::BaseSemantics::RegisterStatePtr createInitialRegisters() override
Create an initial register state.
virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr create(const InstructionSemantics2::BaseSemantics::SValuePtr &, const SmtSolverPtr &) const override
Virtual allocating constructor.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
Sawyer::Optional< rose_addr_t > initialStackVa
Address for initial stack pointer.
const Partitioner2::Partitioner & partitioner() const
Property: Partitioner being used.
SValuePtr Ptr
Shared-ownership pointer.
IoMode
Direction of data wrt storage.
static Ptr instanceSymbolic(const SymbolicExpr::Ptr &value)
Instantiate a new symbolic value.
virtual InstructionSemantics2::BaseSemantics::SValuePtr readRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr &) override
Reads a value from a register.
std::string printableName(size_t nBits) const
Some basic info about the function call.
static Ptr instanceInteger(size_t nBits, uint64_t value)
Instantiate a new concrete value.
void checkOobAccess(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, IoMode, size_t nBytes)
Test whether the specified address is out of bounds for variables.
virtual InstructionSemantics2::BaseSemantics::SValuePtr unsignedExtend(const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override
Extend (or shrink) operand a so it is nbits wide by adding or removing high-order bits...
virtual InstructionSemantics2::BaseSemantics::SValuePtr bottom_(size_t nBits) const override
Data-flow bottom value.
void commandLineDebugSwitches(Sawyer::CommandLine::SwitchGroup &, Settings &)
Command-line switches for debug settings.
size_t pruneCallStack()
Remove old call stack entries.
Describes (part of) a physical CPU register.
StatePtr Ptr
Shared-ownership pointer for a State.
virtual InstructionSemantics2::BaseSemantics::SValuePtr extract(const InstructionSemantics2::BaseSemantics::SValuePtr &, size_t begin, size_t end) override
Extracts bits from a value.
virtual InstructionSemantics2::BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
SmtSolver::Ptr modelCheckerSolver() const
Property: Model checker SMT solver.
Base class for semantics machine states.
virtual InstructionSemantics2::BaseSemantics::SValuePtr protoval() override
Create a prototypical semantic value.
const FunctionCallStack & callStack() const
Function call stack.
static Ptr promote(const InstructionSemantics2::BaseSemantics::StatePtr &)
Checked dynamic cast.
Base class for semantic values.
size_t nDuplicateStates() const
Property: Number of duplicate states.
boost::shared_ptr< class State > StatePtr
Shared-ownership pointer for semantic state.
rose_addr_t framePointer(size_t nBits) const
Computed frame pointer.
User-defined functions for model checking semantics.
virtual InstructionSemantics2::BaseSemantics::SValuePtr shiftLeft(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override
Returns arg shifted left.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
virtual void writeRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr &) override
Writes a value to a register.
Sawyer::Optional< rose_addr_t > returnAddress() const
Address to which function returns.
virtual InstructionSemantics2::BaseSemantics::SValuePtr copy(size_t newNBits=0) const override
Create a new value from an existing value, changing the width if new_width is non-zero.
virtual bool filterOobAccess(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, const AddressInterval &referencedRegion, const AddressInterval &accessedRegion, SgAsmInstruction *insn, TestMode testMode, IoMode ioMode, const Variables::StackVariable &intendedVariable, const AddressInterval &intendedVariableLocation, const Variables::StackVariable &accessedVariable, const AddressInterval &accessedVariableLocation)
Filter out of bounds access.
Sawyer::CommandLine::SwitchGroup commandLineModelSwitches(Settings &)
Command-line switches for model settings.
StatePtr Ptr
Shared-ownership pointer.
rose_addr_t initialStackPointer() const
Property: Initial stack pointer.
void popCallStack()
Pop a function from the call stack.
size_t nBits() const
Property: value width.
virtual InstructionSemantics2::BaseSemantics::StatePtr create(const InstructionSemantics2::BaseSemantics::RegisterStatePtr ®isters, const InstructionSemantics2::BaseSemantics::MemoryStatePtr &memory) const override
Virtual constructor.
bool traceSemantics
Whether to trace all RISC operators.
Type of values manipulated by the SymbolicSemantics domain.
virtual std::vector< TagPtr > preExecute(const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Called before execution starts.
UnitCounts unitsReached() const
Property: Execution units reached.
AddressInterval region() const
Property: Optional memory region.
TestMode oobWrite
How to test for out-of-bounds writes.
static Ptr instance(const InstructionSemantics2::BaseSemantics::RegisterStatePtr &, const InstructionSemantics2::BaseSemantics::MemoryStatePtr &)
Allocating constructor.
virtual void initializeState(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Initialize the initial state.
virtual InstructionSemantics2::BaseSemantics::StatePtr clone() const override
Virtual copy constructor.
virtual InstructionSemantics2::BaseSemantics::SValuePtr unspecified_(size_t nBits) const override
Create a new unspecified semantic value.
virtual InstructionSemantics2::BaseSemantics::SValuePtr concat(const InstructionSemantics2::BaseSemantics::SValuePtr &lowBits, const InstructionSemantics2::BaseSemantics::SValuePtr &highBits) override
Concatenates the bits of two values.
virtual InstructionSemantics2::BaseSemantics::SValuePtr subtractCarry(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b, InstructionSemantics2::BaseSemantics::SValuePtr &carryOut, InstructionSemantics2::BaseSemantics::SValuePtr &overflowed) override
Subtract one value from another and carry.
virtual InstructionSemantics2::BaseSemantics::StatePtr createInitialState() override
Create an initial state.
virtual void finishInstruction(SgAsmInstruction *) override
Called at the end of every instruction.
Virtual definition of semantic operations for model checking.
virtual InstructionSemantics2::BaseSemantics::SValuePtr add(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b) override
Adds two integers of equal size.
virtual InstructionSemantics2::BaseSemantics::DispatcherPtr createDispatcher(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Create an instruction dispatcher.
MemoryType memoryType
Type of memory state.
Partitions instructions into basic blocks and functions.
virtual InstructionSemantics2::BaseSemantics::SValuePtr addWithCarries(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b, const InstructionSemantics2::BaseSemantics::SValuePtr &c, InstructionSemantics2::BaseSemantics::SValuePtr &carryOut) override
Add two values of equal size and a carry bit.
Map indexed by symbolic address hash.
virtual InstructionSemantics2::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) const override
Create a new concrete semantic value.
bool debugNull
When debugging is enabled, show null pointer checking?
RISC operators for model checking.
virtual InstructionSemantics2::BaseSemantics::SValuePtr undefined_(size_t nBits) const override
Create a new undefined semantic value.
bool computeMemoryRegions() const
Property: Compute memory regions for variables.
virtual bool filterNullDeref(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, SgAsmInstruction *, TestMode testMode, IoMode ioMode)
Filter null dereferences.
static Ptr promote(const InstructionSemantics2::BaseSemantics::SValuePtr &v)
Promote a base value to a MemoryRegionSemantics value.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
Description of a local stack variable within a function.
InstructionSemantics2::BaseSemantics::SValuePtr assignRegion(const InstructionSemantics2::BaseSemantics::SValuePtr &result)
Assign a region to an expression.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
virtual Sawyer::Optional< InstructionSemantics2::BaseSemantics::SValuePtr > createOptionalMerge(const InstructionSemantics2::BaseSemantics::SValuePtr &other, const InstructionSemantics2::BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
Possibly create a new value by merging two existing values.
virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr createInitialMemory() override
Create an initial memory state.
rose_addr_t framePointerDelta() const
Property: Frame pointer delta.
virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr createRiscOperators() override
Create RISC operators.
RiscOperatorsPtr Ptr
Shared-ownership pointer.
static Ptr instance()
Instantiate a new prototypical value.