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>
12#include <Sawyer/CommandLine.h>
13#include <Sawyer/Stack.h>
16namespace BinaryAnalysis {
17namespace ModelChecker {
27namespace PartitionerModel {
47 bool debugNull =
false;
50 bool solverMemoization =
false;
51 bool traceSemantics =
false;
54class SemanticCallbacks;
79 Partitioner2::FunctionPtr function_;
80 Address initialStackPointer_ = 0;
83 Variables::StackVariables stackVariables_;
88 const Variables::StackVariables&);
91 Partitioner2::FunctionPtr function()
const;
96 Address initialStackPointer()
const;
99 const Variables::StackVariables& stackVariables()
const;
106 Address framePointerDelta()
const;
107 void framePointerDelta(Address);
113 Address framePointer(
size_t nBits)
const;
123 std::string printableName(
size_t nBits)
const;
138class SValue:
public InstructionSemantics::SymbolicSemantics::SValue {
141 using Super = InstructionSemantics::SymbolicSemantics::SValue;
149#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
151 friend class boost::serialization::access;
155 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
156 s & BOOST_SERIALIZATION_NVP(region_);
166 SValue(
size_t nBits, uint64_t number);
168 explicit SValue(
const SymbolicExpression::Ptr&);
174 static Ptr instance();
177 static Ptr instanceBottom(
size_t nBits);
180 static Ptr instanceUndefined(
size_t nBits);
183 static Ptr instanceUnspecified(
size_t nBits);
186 static Ptr instanceInteger(
size_t nBits, uint64_t value);
189 static Ptr instanceSymbolic(
const SymbolicExpression::Ptr &value);
192 virtual InstructionSemantics::BaseSemantics::SValuePtr bottom_(
size_t nBits)
const override;
193 virtual InstructionSemantics::BaseSemantics::SValuePtr undefined_(
size_t nBits)
const override;
194 virtual InstructionSemantics::BaseSemantics::SValuePtr unspecified_(
size_t nBits)
const override;
195 virtual InstructionSemantics::BaseSemantics::SValuePtr number_(
size_t nBits, uint64_t value)
const override;
196 virtual InstructionSemantics::BaseSemantics::SValuePtr boolean_(
bool value)
const override;
197 virtual InstructionSemantics::BaseSemantics::SValuePtr
copy(
size_t newNBits = 0)
const override;
200 createOptionalMerge(
const InstructionSemantics::BaseSemantics::SValuePtr &other,
201 const InstructionSemantics::BaseSemantics::MergerPtr&,
202 const SmtSolverPtr&)
const override;
208 static Ptr promote(
const InstructionSemantics::BaseSemantics::SValuePtr&);
218 void region(
const AddressInterval&);
222 virtual void print(std::ostream&, InstructionSemantics::BaseSemantics::Formatter&)
const override;
223 virtual void hash(Combinatorics::Hasher&)
const override;
231using StatePtr = boost::shared_ptr<class State>;
234class State:
public InstructionSemantics::SymbolicSemantics::State {
237 using Super = InstructionSemantics::SymbolicSemantics::State;
240 using Ptr = StatePtr;
243 FunctionCallStack callStack_;
247 State(
const InstructionSemantics::BaseSemantics::RegisterStatePtr&,
248 const InstructionSemantics::BaseSemantics::MemoryStatePtr&);
255 static Ptr instance(
const InstructionSemantics::BaseSemantics::RegisterStatePtr&,
256 const InstructionSemantics::BaseSemantics::MemoryStatePtr&);
259 static Ptr instance(
const StatePtr&);
262 virtual InstructionSemantics::BaseSemantics::StatePtr
263 create(
const InstructionSemantics::BaseSemantics::RegisterStatePtr&,
264 const InstructionSemantics::BaseSemantics::MemoryStatePtr&)
const override;
267 virtual InstructionSemantics::BaseSemantics::StatePtr clone()
const override;
270 static Ptr promote(
const InstructionSemantics::BaseSemantics::StatePtr&);
278 const FunctionCallStack& callStack()
const;
279 FunctionCallStack& callStack();
288class RiscOperators:
public InstructionSemantics::SymbolicSemantics::RiscOperators {
290 using Super = InstructionSemantics::SymbolicSemantics::RiscOperators;
295 const Settings settings_;
296 Partitioner2::PartitionerConstPtr partitioner_;
297 SmtSolver::Ptr modelCheckerSolver_;
298 size_t nInstructions_ = 0;
299 SemanticCallbacks *semantics_ =
nullptr;
301 bool computeMemoryRegions_ =
false;
302 const Variables::GlobalVariables &gvars_;
304 mutable SAWYER_THREAD_TRAITS::Mutex variableFinderMutex_;
305 Variables::VariableFinderPtr variableFinder_unsync;
308 RiscOperators(
const Settings&,
const Partitioner2::PartitionerConstPtr&, ModelChecker::SemanticCallbacks*,
309 const InstructionSemantics::BaseSemantics::SValuePtr &protoval,
const SmtSolverPtr&,
310 const Variables::VariableFinderPtr&,
const Variables::GlobalVariables&);
313 const RiscOperators &,
const InstructionSemantics::BaseSemantics::SValuePtr &protoval,
const SmtSolverPtr &
319 static Ptr instance(
const Settings&,
const Partitioner2::PartitionerConstPtr&, ModelChecker::SemanticCallbacks*,
320 const InstructionSemantics::BaseSemantics::SValuePtr &protoval,
const SmtSolverPtr&,
321 const Variables::VariableFinderPtr&,
const Variables::GlobalVariables&);
323 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
324 create(
const InstructionSemantics::BaseSemantics::SValuePtr&,
const SmtSolverPtr&)
const override;
326 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
327 create(
const InstructionSemantics::BaseSemantics::StatePtr&,
const SmtSolverPtr&)
const override;
329 static Ptr promote(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &x);
335 Partitioner2::PartitionerConstPtr partitioner()
const;
343 SmtSolver::Ptr modelCheckerSolver()
const;
344 void modelCheckerSolver(
const SmtSolver::Ptr&);
350 SemanticCallbacks* semanticCallbacks()
const;
357 bool computeMemoryRegions()
const;
358 void computeMemoryRegions(
bool);
368 void checkNullAccess(
const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode);
373 void checkOobAccess(
const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode,
size_t nBytes);
378 void checkUninitVar(
const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode,
size_t nBytes);
386 size_t nInstructions()
const;
387 void nInstructions(
size_t);
391 void maybeInitCallStack(Address insnVa);
408 size_t pruneCallStack();
411 void printCallStack(std::ostream&,
const std::string &prefix);
427 InstructionSemantics::BaseSemantics::SValuePtr
428 assignRegion(
const InstructionSemantics::BaseSemantics::SValuePtr &result);
430 InstructionSemantics::BaseSemantics::SValuePtr
431 assignRegion(
const InstructionSemantics::BaseSemantics::SValuePtr &result,
432 const InstructionSemantics::BaseSemantics::SValuePtr &a);
434 InstructionSemantics::BaseSemantics::SValuePtr
435 assignRegion(
const InstructionSemantics::BaseSemantics::SValuePtr &result,
436 const InstructionSemantics::BaseSemantics::SValuePtr &a,
437 const InstructionSemantics::BaseSemantics::SValuePtr &b);
443 virtual InstructionSemantics::BaseSemantics::SValuePtr
444 number_(
size_t nBits, uint64_t value)
override;
446 virtual InstructionSemantics::BaseSemantics::SValuePtr
447 extract(
const InstructionSemantics::BaseSemantics::SValuePtr&,
size_t begin,
size_t end)
override;
449 virtual InstructionSemantics::BaseSemantics::SValuePtr
450 concat(
const InstructionSemantics::BaseSemantics::SValuePtr &lowBits,
451 const InstructionSemantics::BaseSemantics::SValuePtr &highBits)
override;
453 virtual InstructionSemantics::BaseSemantics::SValuePtr
454 shiftLeft(
const InstructionSemantics::BaseSemantics::SValuePtr &a,
455 const InstructionSemantics::BaseSemantics::SValuePtr &nBits)
override;
457 virtual InstructionSemantics::BaseSemantics::SValuePtr
458 shiftRight(
const InstructionSemantics::BaseSemantics::SValuePtr &a,
459 const InstructionSemantics::BaseSemantics::SValuePtr &nBits)
override;
461 virtual InstructionSemantics::BaseSemantics::SValuePtr
463 const InstructionSemantics::BaseSemantics::SValuePtr &nBits)
override;
465 virtual InstructionSemantics::BaseSemantics::SValuePtr
466 unsignedExtend(
const InstructionSemantics::BaseSemantics::SValue::Ptr &a,
size_t newWidth)
override;
468 virtual InstructionSemantics::BaseSemantics::SValuePtr
469 signExtend(
const InstructionSemantics::BaseSemantics::SValue::Ptr &a,
size_t newWidth)
override;
471 virtual InstructionSemantics::BaseSemantics::SValuePtr
472 add(
const InstructionSemantics::BaseSemantics::SValuePtr &a,
473 const InstructionSemantics::BaseSemantics::SValuePtr &b)
override;
475 virtual InstructionSemantics::BaseSemantics::SValuePtr
476 addCarry(
const InstructionSemantics::BaseSemantics::SValuePtr &a,
477 const InstructionSemantics::BaseSemantics::SValuePtr &b,
478 InstructionSemantics::BaseSemantics::SValuePtr &carryOut ,
479 InstructionSemantics::BaseSemantics::SValuePtr &overflowed )
override;
481 virtual InstructionSemantics::BaseSemantics::SValuePtr
482 subtract(
const InstructionSemantics::BaseSemantics::SValuePtr &a,
483 const InstructionSemantics::BaseSemantics::SValuePtr &b)
override;
485 virtual InstructionSemantics::BaseSemantics::SValuePtr
486 subtractCarry(
const InstructionSemantics::BaseSemantics::SValuePtr &a,
487 const InstructionSemantics::BaseSemantics::SValuePtr &b,
488 InstructionSemantics::BaseSemantics::SValuePtr &carryOut ,
489 InstructionSemantics::BaseSemantics::SValuePtr &overflowed )
override;
491 virtual InstructionSemantics::BaseSemantics::SValuePtr
492 addWithCarries(
const InstructionSemantics::BaseSemantics::SValuePtr &a,
493 const InstructionSemantics::BaseSemantics::SValuePtr &b,
494 const InstructionSemantics::BaseSemantics::SValuePtr &c,
495 InstructionSemantics::BaseSemantics::SValuePtr &carryOut )
override;
497 virtual InstructionSemantics::BaseSemantics::SValuePtr
498 readRegister(RegisterDescriptor,
const InstructionSemantics::BaseSemantics::SValuePtr&)
override;
501 writeRegister(RegisterDescriptor,
const InstructionSemantics::BaseSemantics::SValuePtr&)
override;
503 virtual InstructionSemantics::BaseSemantics::SValuePtr
504 readMemory(RegisterDescriptor segreg,
const InstructionSemantics::BaseSemantics::SValuePtr &addr,
505 const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
506 const InstructionSemantics::BaseSemantics::SValuePtr &cond)
override;
509 writeMemory(RegisterDescriptor segreg,
const InstructionSemantics::BaseSemantics::SValuePtr &addr,
510 const InstructionSemantics::BaseSemantics::SValuePtr &value,
511 const InstructionSemantics::BaseSemantics::SValuePtr &cond)
override;
519class SemanticCallbacks:
public Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks {
521 using Ptr = SemanticCallbacksPtr;
526 Partitioner2::PartitionerConstPtr partitioner_;
527 SmtSolver::Memoizer::Ptr smtMemoizer_;
530 mutable SAWYER_THREAD_TRAITS::Mutex unitsMutex_;
533 mutable SAWYER_THREAD_TRAITS::Mutex mutex_;
534 std::set<uint64_t> seenStates_;
535 size_t nDuplicateStates_ = 0;
536 size_t nSolverFailures_ = 0;
537 UnitCounts unitsReached_;
538 Variables::VariableFinderPtr variableFinder_;
539 Variables::GlobalVariables gvars_;
547 bool followingOnePath_ =
false;
548 std::list<ExecutionUnitPtr> onePath_;
551 SemanticCallbacks(
const ModelChecker::SettingsPtr&,
const Settings&,
const Partitioner2::PartitionerConstPtr&);
553 ~SemanticCallbacks();
556 static Ptr instance(
const ModelChecker::SettingsPtr&,
const Settings&,
const Partitioner2::PartitionerConstPtr&);
560 Partitioner2::PartitionerConstPtr partitioner()
const;
564 const Settings& p2Settings()
const;
581 void followOnePath(
const std::list<ExecutionUnitPtr>&);
594 bool followingOnePath()
const;
595 void followingOnePath(
bool);
605 SmtSolver::Memoizer::Ptr smtMemoizer()
const;
606 void smtMemoizer(
const SmtSolver::Memoizer::Ptr&);
621 size_t nDuplicateStates()
const;
630 size_t nSolverFailures()
const;
640 size_t nUnitsReached()
const;
648 UnitCounts unitsReached()
const;
657 virtual bool filterNullDeref(
const InstructionSemantics::BaseSemantics::SValuePtr &addr,
SgAsmInstruction*,
658 TestMode testMode, IoMode ioMode);
675 virtual bool filterOobAccess(
const InstructionSemantics::BaseSemantics::SValuePtr &addr,
676 const AddressInterval &referencedRegion,
const AddressInterval &accessedRegion,
678 const FoundVariable &intendedVariable,
const FoundVariable &accessedVariable);
680 virtual bool filterUninitVar(
const InstructionSemantics::BaseSemantics::SValuePtr &addr,
681 const AddressInterval &referencedREgion,
const AddressInterval &accessedRegion,
682 SgAsmInstruction *insn, TestMode testMode,
const FoundVariable &accessedVariable);
685 virtual void reset()
override;
687 virtual InstructionSemantics::BaseSemantics::SValuePtr protoval()
override;
689 virtual InstructionSemantics::BaseSemantics::RegisterStatePtr createInitialRegisters()
override;
691 virtual InstructionSemantics::BaseSemantics::MemoryStatePtr createInitialMemory()
override;
693 virtual InstructionSemantics::BaseSemantics::StatePtr createInitialState()
override;
695 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr createRiscOperators()
override;
697 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
698 configureRiscOperators(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&)
override;
701 initializeState(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&)
override;
703 virtual InstructionSemantics::BaseSemantics::DispatcherPtr
704 createDispatcher(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&)
override;
706 virtual SmtSolver::Ptr createSolver()
override;
708 virtual void attachModelCheckerSolver(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
709 const SmtSolver::Ptr&)
override;
711 virtual CodeAddresses
712 nextCodeAddresses(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&)
override;
714 virtual std::vector<TagPtr>
715 preExecute(
const PathNodePtr&,
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&)
override;
717 virtual std::vector<TagPtr>
718 postExecute(
const PathNodePtr&,
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&)
override;
720 virtual InstructionSemantics::BaseSemantics::SValuePtr
721 instructionPointer(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&)
override;
723 virtual std::vector<NextUnit>
724 nextUnits(
const PathPtr&,
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
const SmtSolver::Ptr&)
override;
726#ifdef ROSE_HAVE_YAMLCPP
727 virtual std::list<ExecutionUnitPtr>
728 parsePath(
const YAML::Node&,
const std::string &sourceName)
override;
731 virtual std::list<ExecutionUnitPtr>
732 parsePath(
const Yaml::Node&,
const std::string &sourceName)
override;
735 Variables::VariableFinderPtr variableFinder()
const;
736 Variables::GlobalVariables& globalVariables();
740 bool seenState(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
743 ExecutionUnitPtr findUnit(Address va,
const Progress::Ptr&);
A collection of related switch declarations.
Container associating values with keys.
Holds a value or nothing.
Base class for machine instructions.
T shiftRightArithmetic(T value, size_t count)
Shifts bits of value right by count bits with sign extension.
T extract(T bits)
Extract bits from a value.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to concrete RISC operations.
Sawyer::SharedPointer< class SValue > SValuePtr
Smart-ownership pointer to a concrete semantic value.
Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &)
Define command-line switches.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.
void print(const GlobalVariables &, const Partitioner2::PartitionerConstPtr &, std::ostream &out, const std::string &prefix="")
Print info about multiple global variables.
std::uint64_t Address
Address.
Sawyer::Container::Interval< Address > AddressInterval
An interval of addresses.
Unsigned shiftRight(Unsigned src, size_t n, bool b=false)
Right shift a value.
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.
void serialize(std::ostream &output, Graph &graph)
Serialize a graph into a stream of bytes.
void copy(const Word *src, const BitRange &srcRange, Word *dst, const BitRange &dstRange)
Copy some bits.
const char * MemoryType(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::MemoryType enum constant to a...
const char * TestMode(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::TestMode enum constant to a string.