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/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>
13 namespace BinaryAnalysis {
14 namespace ModelChecker {
24 namespace PartitionerModel {
43 rose_addr_t maxNullAddress = 4095;
44 bool debugNull =
false;
47 bool solverMemoization =
false;
48 bool traceSemantics =
false;
51 class SemanticCallbacks;
77 rose_addr_t initialStackPointer_ = 0;
78 rose_addr_t framePointerDelta_ = (rose_addr_t)(-4);
93 rose_addr_t initialStackPointer()
const;
103 rose_addr_t framePointerDelta()
const;
104 void framePointerDelta(rose_addr_t);
110 rose_addr_t framePointer(
size_t nBits)
const;
120 std::string printableName(
size_t nBits)
const;
135 class SValue:
public InstructionSemantics::SymbolicSemantics::SValue {
138 using Super = InstructionSemantics::SymbolicSemantics::SValue;
146 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
148 friend class boost::serialization::access;
152 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
153 s & BOOST_SERIALIZATION_NVP(region_);
163 SValue(
size_t nBits, uint64_t number);
171 static Ptr instance();
174 static Ptr instanceBottom(
size_t nBits);
177 static Ptr instanceUndefined(
size_t nBits);
180 static Ptr instanceUnspecified(
size_t nBits);
183 static Ptr instanceInteger(
size_t nBits, uint64_t value);
190 return instanceBottom(nBits);
194 return instanceUndefined(nBits);
198 return instanceUnspecified(nBits);
202 return instanceInteger(nBits, value);
206 return instanceInteger(1, value ? 1 : 0);
222 ASSERT_not_null(retval);
238 virtual void print(std::ostream&, InstructionSemantics::BaseSemantics::Formatter&)
const override;
239 virtual void hash(Combinatorics::Hasher&)
const override;
247 using StatePtr = boost::shared_ptr<class State>;
250 class State:
public InstructionSemantics::SymbolicSemantics::State {
253 using Super = InstructionSemantics::SymbolicSemantics::State;
256 using Ptr = StatePtr;
259 FunctionCallStack callStack_;
275 static Ptr instance(
const StatePtr&);
281 return instance(registers, memory);
296 const FunctionCallStack& callStack()
const;
297 FunctionCallStack& callStack();
306 class RiscOperators:
public InstructionSemantics::SymbolicSemantics::RiscOperators {
308 using Super = InstructionSemantics::SymbolicSemantics::RiscOperators;
313 const Settings settings_;
314 const Partitioner2::Partitioner &partitioner_;
316 size_t nInstructions_ = 0;
317 SemanticCallbacks *semantics_ =
nullptr;
319 bool computeMemoryRegions_ =
false;
321 mutable SAWYER_THREAD_TRAITS::Mutex variableFinderMutex_;
325 RiscOperators(
const Settings&,
const Partitioner2::Partitioner&, ModelChecker::SemanticCallbacks*,
332 static Ptr instance(
const Settings&,
const Partitioner2::Partitioner&, ModelChecker::SemanticCallbacks*,
348 const Partitioner2::Partitioner& partitioner()
const;
365 bool computeMemoryRegions()
const;
366 void computeMemoryRegions(
bool);
394 size_t nInstructions()
const;
395 void nInstructions(
size_t);
399 void maybeInitCallStack(rose_addr_t insnVa);
416 size_t pruneCallStack();
419 void printCallStack(std::ostream&,
const std::string &prefix);
452 number_(
size_t nBits, uint64_t value)
override;
527 class SemanticCallbacks:
public Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks {
529 using Ptr = SemanticCallbacksPtr;
534 const Partitioner2::Partitioner &partitioner_;
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;
544 UnitCounts unitsReached_;
553 bool followingOnePath_ =
false;
554 std::list<ExecutionUnitPtr> onePath_;
557 SemanticCallbacks(
const ModelChecker::SettingsPtr&,
const Settings&,
const Partitioner2::Partitioner&);
559 ~SemanticCallbacks();
562 static Ptr instance(
const ModelChecker::SettingsPtr&,
const Settings&,
const Partitioner2::Partitioner&);
566 const Partitioner2::Partitioner& partitioner()
const;
584 void followOnePath(
const std::list<ExecutionUnitPtr>&);
597 bool followingOnePath()
const;
598 void followingOnePath(
bool);
619 size_t nDuplicateStates()
const;
628 size_t nSolverFailures()
const;
638 size_t nUnitsReached()
const;
646 UnitCounts unitsReached()
const;
656 TestMode testMode, IoMode ioMode);
676 const Variables::StackVariable &intendedVariable,
const AddressInterval &intendedVariableLocation,
677 const Variables::StackVariable &accessedVariable,
const AddressInterval &accessedVariableLocation);
685 virtual void reset()
override;
708 virtual CodeAddresses
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>
729 parsePath(
const Yaml::Node&,
const std::string &sourceName)
override;
736 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.
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.
void print(const StackVariables &, const Partitioner2::Partitioner &, std::ostream &out, const std::string &prefix="")
Print info about multiple local variables.
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.
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.
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.
T extract(T bits)
Extract bits from a value.
Sawyer::SharedPointer< Progress > Ptr
Progress objects are reference counted.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.