1 #ifndef ROSE_BinaryAnalysis_ModelChecker_PartitionerModel_H
2 #define ROSE_BinaryAnalysis_ModelChecker_PartitionerModel_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
6 #include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
7 #include <Rose/BinaryAnalysis/ModelChecker/SemanticCallbacks.h>
8 #include <Rose/BinaryAnalysis/ModelChecker/Variables.h>
9 #include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
10 #include <Rose/BinaryAnalysis/Variables.h>
11 #include <Sawyer/CommandLine.h>
12 #include <Sawyer/Stack.h>
15 namespace BinaryAnalysis {
16 namespace ModelChecker {
26 namespace PartitionerModel {
45 rose_addr_t maxNullAddress = 4095;
46 bool debugNull =
false;
49 bool solverMemoization =
false;
50 bool traceSemantics =
false;
53 class SemanticCallbacks;
79 rose_addr_t initialStackPointer_ = 0;
80 rose_addr_t framePointerDelta_ = (rose_addr_t)(-4);
95 rose_addr_t initialStackPointer()
const;
105 rose_addr_t framePointerDelta()
const;
106 void framePointerDelta(rose_addr_t);
112 rose_addr_t framePointer(
size_t nBits)
const;
122 std::string printableName(
size_t nBits)
const;
137 class SValue:
public InstructionSemantics::SymbolicSemantics::SValue {
140 using Super = InstructionSemantics::SymbolicSemantics::SValue;
148 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
150 friend class boost::serialization::access;
154 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
155 s & BOOST_SERIALIZATION_NVP(region_);
165 SValue(
size_t nBits, uint64_t number);
173 static Ptr instance();
176 static Ptr instanceBottom(
size_t nBits);
179 static Ptr instanceUndefined(
size_t nBits);
182 static Ptr instanceUnspecified(
size_t nBits);
185 static Ptr instanceInteger(
size_t nBits, uint64_t value);
192 return instanceBottom(nBits);
196 return instanceUndefined(nBits);
200 return instanceUnspecified(nBits);
204 return instanceInteger(nBits, value);
208 return instanceInteger(1, value ? 1 : 0);
224 ASSERT_not_null(retval);
240 virtual void print(std::ostream&, InstructionSemantics::BaseSemantics::Formatter&)
const override;
241 virtual void hash(Combinatorics::Hasher&)
const override;
249 using StatePtr = boost::shared_ptr<class State>;
252 class State:
public InstructionSemantics::SymbolicSemantics::State {
255 using Super = InstructionSemantics::SymbolicSemantics::State;
258 using Ptr = StatePtr;
261 FunctionCallStack callStack_;
277 static Ptr instance(
const StatePtr&);
283 return instance(registers, memory);
298 const FunctionCallStack& callStack()
const;
299 FunctionCallStack& callStack();
308 class RiscOperators:
public InstructionSemantics::SymbolicSemantics::RiscOperators {
310 using Super = InstructionSemantics::SymbolicSemantics::RiscOperators;
315 const Settings settings_;
318 size_t nInstructions_ = 0;
319 SemanticCallbacks *semantics_ =
nullptr;
321 bool computeMemoryRegions_ =
false;
324 mutable SAWYER_THREAD_TRAITS::Mutex variableFinderMutex_;
368 bool computeMemoryRegions()
const;
369 void computeMemoryRegions(
bool);
397 size_t nInstructions()
const;
398 void nInstructions(
size_t);
402 void maybeInitCallStack(rose_addr_t insnVa);
419 size_t pruneCallStack();
422 void printCallStack(std::ostream&,
const std::string &prefix);
455 number_(
size_t nBits, uint64_t value)
override;
530 class SemanticCallbacks:
public Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks {
532 using Ptr = SemanticCallbacksPtr;
540 mutable SAWYER_THREAD_TRAITS::Mutex unitsMutex_;
543 mutable SAWYER_THREAD_TRAITS::Mutex mutex_;
544 std::set<uint64_t> seenStates_;
545 size_t nDuplicateStates_ = 0;
546 size_t nSolverFailures_ = 0;
547 UnitCounts unitsReached_;
557 bool followingOnePath_ =
false;
558 std::list<ExecutionUnitPtr> onePath_;
563 ~SemanticCallbacks();
588 void followOnePath(
const std::list<ExecutionUnitPtr>&);
601 bool followingOnePath()
const;
602 void followingOnePath(
bool);
623 size_t nDuplicateStates()
const;
632 size_t nSolverFailures()
const;
642 size_t nUnitsReached()
const;
650 UnitCounts unitsReached()
const;
660 TestMode testMode, IoMode ioMode);
680 const FoundVariable &intendedVariable,
const FoundVariable &accessedVariable);
684 SgAsmInstruction *insn, TestMode testMode,
const FoundVariable &accessedVariable);
687 virtual void reset()
override;
710 virtual CodeAddresses
713 virtual std::vector<TagPtr>
716 virtual std::vector<TagPtr>
722 virtual std::vector<NextUnit>
725 #ifdef ROSE_HAVE_YAMLCPP
726 virtual std::list<ExecutionUnitPtr>
727 parsePath(
const YAML::Node&,
const std::string &sourceName)
override;
730 virtual std::list<ExecutionUnitPtr>
731 parsePath(
const Yaml::Node&,
const std::string &sourceName)
override;
738 ExecutionUnitPtr findUnit(rose_addr_t va,
const Progress::Ptr&);
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Unsigned shiftRight(Unsigned src, size_t n, bool b=false)
Right shift a value.
const char * TestMode(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::TestMode enum constant to a string.
void copy(const Word *src, const BitRange &srcRange, Word *dst, const BitRange &dstRange)
Copy some bits.
void serialize(std::ostream &output, Graph &graph)
Serialize a graph into a stream of bytes.
Sawyer::SharedPointer< Merger > MergerPtr
Shared-ownership pointer for Merger classes.
Sawyer::Container::IntervalMap< OffsetInterval, StackVariable > StackVariables
Collection of local variables organized by frame offsets.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Base class for machine instructions.
Sawyer::SharedPointer< class SValue > SValuePtr
Smart-ownership pointer to a concrete semantic value.
Sawyer::SharedPointer< Memoizer > Ptr
Reference counting pointer.
Unsigned signExtend(Unsigned src, size_t n)
Sign extend part of a value to the full width of the src type.
Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &settings)
Command-line switches for unparser settings.
Unsigned shiftLeft(Unsigned src, size_t n, bool b=false)
Left shift a value.
Sawyer::SharedPointer< VariableFinder > VariableFinderPtr
Reference counting pointer.
A collection of related switch declarations.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
Main namespace for the ROSE library.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
Sawyer::SharedPointer< Function > FunctionPtr
Shared-ownership pointer for Function.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
void print(const StackVariables &, const Partitioner2::PartitionerConstPtr &, std::ostream &out, const std::string &prefix="")
Print info about multiple local variables.
const char * MemoryType(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::MemoryType enum constant to a...
T shiftRightArithmetic(T value, size_t count)
Shifts bits of value right by count bits with sign extension.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to concrete RISC operations.
Sawyer::SharedPointer< const Partitioner > PartitionerConstPtr
Shared-ownership pointer for Partitioner.
SValuePtr Ptr
Shared-ownership pointer.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Sawyer::SharedPointer< SValue > SValuePtr
Shared-ownership pointer to a semantic value in any domain.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
Sawyer::Container::IntervalMap< AddressInterval, GlobalVariable > GlobalVariables
Maps virtual addresses to global variables.
T extract(T bits)
Extract bits from a value.
ProgressPtr Ptr
Progress objects are reference counted.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.