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/InstructionSemantics/SymbolicSemantics.h>
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_);
214 const SmtSolverPtr&)
const override;
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&);
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
SmtSolver::Memoizer::Ptr smtMemoizer() const
Property: SMT solver memoizer.
virtual InstructionSemantics::BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr, const InstructionSemantics::BaseSemantics::SValuePtr &dflt, const InstructionSemantics::BaseSemantics::SValuePtr &cond) override
Reads a value from memory.
virtual std::vector< TagPtr > postExecute(const ExecutionUnitPtr &, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &) override
Called after execution ends.
TestMode oobRead
How to test for out-of-bounds reads.
Symbolic values with memory regions.
virtual Sawyer::Optional< InstructionSemantics::BaseSemantics::SValuePtr > createOptionalMerge(const InstructionSemantics::BaseSemantics::SValuePtr &other, const InstructionSemantics::BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
Possibly create a new value by merging two existing values.
static Ptr promote(const InstructionSemantics::BaseSemantics::StatePtr &)
Checked dynamic cast.
virtual void attachModelCheckerSolver(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &) override
Associate solver with semantics.
static Ptr instanceBottom(size_t nBits)
Instantiate a new data-flow bottom value.
virtual std::vector< TagPtr > preExecute(const ExecutionUnitPtr &, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &) override
Called before execution starts.
MemoryType
Type of memory state to use.
virtual InstructionSemantics::BaseSemantics::SValuePtr shiftRightArithmetic(const InstructionSemantics::BaseSemantics::SValuePtr &a, const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override
Returns arg shifted right arithmetically (with sign bit).
Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &)
Command-line switches for settings.
virtual InstructionSemantics::BaseSemantics::SValuePtr undefined_(size_t nBits) const override
Create a new undefined semantic value.
virtual InstructionSemantics::BaseSemantics::SValuePtr unsignedExtend(const InstructionSemantics::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...
void pushCallStack(const Partitioner2::FunctionPtr &callee, rose_addr_t initialSp, Sawyer::Optional< rose_addr_t > returnVa)
Push a function onto the call stack.
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.
void checkUninitVar(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, size_t nBytes)
Test whether the specified address accesses an uninitialized variable.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
virtual InstructionSemantics::BaseSemantics::SValuePtr extract(const InstructionSemantics::BaseSemantics::SValuePtr &, size_t begin, size_t end) override
Extracts bits from a value.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Base class for machine instructions.
virtual InstructionSemantics::BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
virtual InstructionSemantics::BaseSemantics::SValuePtr subtract(const InstructionSemantics::BaseSemantics::SValuePtr &a, const InstructionSemantics::BaseSemantics::SValuePtr &b) override
Subtract one value from another.
virtual InstructionSemantics::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) const override
Create a new concrete semantic value.
virtual std::list< ExecutionUnitPtr > parsePath(const Yaml::Node &, const std::string &sourceName) override
Construct a path from a YAML document.
virtual InstructionSemantics::BaseSemantics::SValuePtr bottom_(size_t nBits) const override
Data-flow bottom value.
TestMode uninitVar
How to test for uninitialized variable reads.
virtual InstructionSemantics::BaseSemantics::SValuePtr addCarry(const InstructionSemantics::BaseSemantics::SValuePtr &a, const InstructionSemantics::BaseSemantics::SValuePtr &b, InstructionSemantics::BaseSemantics::SValuePtr &carryOut, InstructionSemantics::BaseSemantics::SValuePtr &overflowed) override
Adds two integers of equal size and carry.
void checkOobAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode, size_t nBytes)
Test whether the specified address is out of bounds for variables.
const Variables::StackVariables & stackVariables() const
Property: Stack variables.
size_t nSolverFailures() const
Property: Number of times the SMT solver failed.
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.
virtual InstructionSemantics::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 InstructionSemantics::BaseSemantics::SValuePtr shiftLeft(const InstructionSemantics::BaseSemantics::SValuePtr &a, const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override
Returns arg shifted left.
TestMode
Mode by which comparisons are made.
RiscOperatorsPtr Ptr
Shared-ownership pointer.
virtual InstructionSemantics::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) override
Returns a number of the specified bit width.
void maybeInitCallStack(rose_addr_t insnVa)
Ensure call stack has a root function.
virtual InstructionSemantics::BaseSemantics::SValuePtr subtractCarry(const InstructionSemantics::BaseSemantics::SValuePtr &a, const InstructionSemantics::BaseSemantics::SValuePtr &b, InstructionSemantics::BaseSemantics::SValuePtr &carryOut, InstructionSemantics::BaseSemantics::SValuePtr &overflowed) override
Subtract one value from another and carry.
virtual InstructionSemantics::BaseSemantics::SValuePtr shiftRight(const InstructionSemantics::BaseSemantics::SValuePtr &a, const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override
Returns arg shifted right logically (no sign bit).
A collection of related switch declarations.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
size_t nUnitsReached() const
Property: Number of execution units reached.
virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr create(const InstructionSemantics::BaseSemantics::SValuePtr &, const SmtSolverPtr &) const override
Virtual allocating constructor.
Detection is reported only if it must occur.
virtual InstructionSemantics::BaseSemantics::SValuePtr add(const InstructionSemantics::BaseSemantics::SValuePtr &a, const InstructionSemantics::BaseSemantics::SValuePtr &b) override
Adds two integers of equal size.
void printCallStack(std::ostream &, const std::string &prefix)
Print information about the function call stack.
Main namespace for the ROSE library.
virtual InstructionSemantics::BaseSemantics::SValuePtr instructionPointer(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &) override
Address of the next instruction.
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 void reset() override
Reset internal data.
Addresses and completeness.
const Partitioner2::Partitioner & partitioner() const
Property: Partitioner.
virtual void print(std::ostream &, InstructionSemantics::BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
static Ptr instanceUndefined(size_t nBits)
Instantiate a new undefined value.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
static Ptr instance(const InstructionSemantics::BaseSemantics::RegisterStatePtr &, const InstructionSemantics::BaseSemantics::MemoryStatePtr &)
Allocating constructor.
InstructionSemantics::BaseSemantics::SValuePtr assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result)
Assign a region to an expression.
size_t nInstructions() const
Property: Number of instructions executed.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
virtual InstructionSemantics::BaseSemantics::DispatcherPtr createDispatcher(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &) override
Create an instruction dispatcher.
virtual InstructionSemantics::BaseSemantics::SValuePtr protoval() override
Create a prototypical semantic value.
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.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
virtual InstructionSemantics::BaseSemantics::SValuePtr addWithCarries(const InstructionSemantics::BaseSemantics::SValuePtr &a, const InstructionSemantics::BaseSemantics::SValuePtr &b, const InstructionSemantics::BaseSemantics::SValuePtr &c, InstructionSemantics::BaseSemantics::SValuePtr &carryOut) override
Add two values of equal size and a carry bit.
IoMode
Direction of data wrt storage.
static Ptr instanceSymbolic(const SymbolicExpr::Ptr &value)
Instantiate a new symbolic value.
virtual InstructionSemantics::BaseSemantics::StatePtr createInitialState() override
Create an initial state.
virtual void writeMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr, const InstructionSemantics::BaseSemantics::SValuePtr &value, const InstructionSemantics::BaseSemantics::SValuePtr &cond) override
Writes a value to memory.
virtual InstructionSemantics::BaseSemantics::RegisterStatePtr createInitialRegisters() override
Create an initial register state.
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.
virtual InstructionSemantics::BaseSemantics::StatePtr clone() const override
Virtual copy constructor.
virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr createRiscOperators() override
Create RISC operators.
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.
virtual InstructionSemantics::BaseSemantics::StatePtr create(const InstructionSemantics::BaseSemantics::RegisterStatePtr ®isters, const InstructionSemantics::BaseSemantics::MemoryStatePtr &memory) const override
Virtual constructor.
SmtSolver::Ptr modelCheckerSolver() const
Property: Model checker SMT solver.
virtual InstructionSemantics::BaseSemantics::SValuePtr concat(const InstructionSemantics::BaseSemantics::SValuePtr &lowBits, const InstructionSemantics::BaseSemantics::SValuePtr &highBits) override
Concatenates the bits of two values.
const FunctionCallStack & callStack() const
Function call stack.
Type of values manipulated by the SymbolicSemantics domain.
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.
virtual InstructionSemantics::BaseSemantics::SValuePtr readRegister(RegisterDescriptor, const InstructionSemantics::BaseSemantics::SValuePtr &) override
Reads a value from a register.
User-defined functions for model checking semantics.
virtual void writeRegister(RegisterDescriptor, const InstructionSemantics::BaseSemantics::SValuePtr &) override
Writes a value to a register.
StatePtr Ptr
Shared-ownership pointer for a State.
virtual bool filterOobAccess(const InstructionSemantics::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.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for semantic values.
Sawyer::Optional< rose_addr_t > returnAddress() const
Address to which function returns.
Defines RISC operators for the SymbolicSemantics domain.
void checkNullAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode)
Test whether the specified address is considered to be null.
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.
bool traceSemantics
Whether to trace all RISC operators.
UnitCounts unitsReached() const
Property: Execution units reached.
AddressInterval region() const
Property: Optional memory region.
TestMode oobWrite
How to test for out-of-bounds writes.
virtual InstructionSemantics::BaseSemantics::SValuePtr signExtend(const InstructionSemantics::BaseSemantics::SValue::Ptr &a, size_t newWidth) override
Sign extends a value.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
Base class for most instruction semantics RISC operators.
virtual void finishInstruction(SgAsmInstruction *) override
Called at the end of every instruction.
Virtual definition of semantic operations for model checking.
virtual std::vector< NextUnit > nextUnits(const PathPtr &, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &) override
Discover next execution units.
MemoryType memoryType
Type of memory state.
Partitions instructions into basic blocks and functions.
Base class for semantics machine states.
Map indexed by symbolic address hash.
bool debugNull
When debugging is enabled, show null pointer checking?
RISC operators for model checking.
virtual InstructionSemantics::BaseSemantics::MemoryStatePtr createInitialMemory() override
Create an initial memory state.
virtual CodeAddresses nextCodeAddresses(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &) override
Possible next code addresses.
bool computeMemoryRegions() const
Property: Compute memory regions for variables.
static Ptr promote(const InstructionSemantics::BaseSemantics::SValuePtr &v)
Promote a base value to a MemoryRegionSemantics value.
virtual bool filterNullDeref(const InstructionSemantics::BaseSemantics::SValuePtr &addr, SgAsmInstruction *, TestMode testMode, IoMode ioMode)
Filter null dereferences.
Description of a local stack variable within a function.
virtual void initializeState(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &) override
Initialize the initial state.
virtual InstructionSemantics::BaseSemantics::SValuePtr unspecified_(size_t nBits) const override
Create a new unspecified semantic value.
size_t nBits() const
Property: value width.
rose_addr_t framePointerDelta() const
Property: Frame pointer delta.
static Ptr instance()
Instantiate a new prototypical value.