ROSE  0.11.109.0
PartitionerModel.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_PartitionerModel_H
2 #define ROSE_BinaryAnalysis_ModelChecker_PartitionerModel_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_MODEL_CHECKER
5 
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>
11 
12 namespace Rose {
13 namespace BinaryAnalysis {
14 namespace ModelChecker {
15 
24 namespace PartitionerModel {
25 
27 // Settings for this model checker
29 
31 struct Settings {
33  enum class MemoryType {
34  LIST,
35  MAP
36  };
37 
38  TestMode nullRead = TestMode::MUST;
39  TestMode nullWrite = TestMode::MUST;
40  TestMode oobRead = TestMode::OFF;
41  TestMode oobWrite = TestMode::OFF;
42  TestMode uninitVar = TestMode::OFF;
43  rose_addr_t maxNullAddress = 4095;
44  bool debugNull = false;
45  Sawyer::Optional<rose_addr_t> initialStackVa;
46  MemoryType memoryType = MemoryType::MAP;
47  bool solverMemoization = false;
48  bool traceSemantics = false;
49 };
50 
51 class SemanticCallbacks;
52 
56 void commandLineDebugSwitches(Sawyer::CommandLine::SwitchGroup&, Settings&);
57 
62 Sawyer::CommandLine::SwitchGroup commandLineModelSwitches(Settings&);
63 
68 Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings&);
69 
71 // Function call stack
73 
75 class FunctionCall {
76  Partitioner2::FunctionPtr function_;
77  rose_addr_t initialStackPointer_ = 0;
78  rose_addr_t framePointerDelta_ = (rose_addr_t)(-4); // Normal frame pointer w.r.t. initial stack pointer
79  Sawyer::Optional<rose_addr_t> returnAddress_;
80  Variables::StackVariables stackVariables_;
81 
82 public:
83  ~FunctionCall();
84  FunctionCall(const Partitioner2::FunctionPtr&, rose_addr_t initialSp, Sawyer::Optional<rose_addr_t> returnAddress,
86 
88  Partitioner2::FunctionPtr function() const;
89 
93  rose_addr_t initialStackPointer() const;
94 
96  const Variables::StackVariables& stackVariables() const;
97 
103  rose_addr_t framePointerDelta() const;
104  void framePointerDelta(rose_addr_t);
110  rose_addr_t framePointer(size_t nBits) const;
111 
115  Sawyer::Optional<rose_addr_t> returnAddress() const;
116  void returnAddress(Sawyer::Optional<rose_addr_t>);
120  std::string printableName(size_t nBits) const;
121 };
122 
126 using FunctionCallStack = Sawyer::Container::Stack<FunctionCall>;
127 
129 // Instruction semantics value
131 
135 class SValue: public InstructionSemantics::SymbolicSemantics::SValue {
136 public:
138  using Super = InstructionSemantics::SymbolicSemantics::SValue;
139 
141  using Ptr = SValuePtr;
142 
143 private:
144  AddressInterval region_;
145 
146 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
147 private:
148  friend class boost::serialization::access;
149 
150  template<class S>
151  void serialize(S &s, const unsigned /*version*/) {
152  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
153  s & BOOST_SERIALIZATION_NVP(region_);
154  }
155 #endif
156 
157 public:
158  ~SValue();
159 
160 protected:
161  SValue();
162 
163  SValue(size_t nBits, uint64_t number);
164 
165  explicit SValue(const SymbolicExpression::Ptr&);
166 
167 public:
171  static Ptr instance();
172 
174  static Ptr instanceBottom(size_t nBits);
175 
177  static Ptr instanceUndefined(size_t nBits);
178 
180  static Ptr instanceUnspecified(size_t nBits);
181 
183  static Ptr instanceInteger(size_t nBits, uint64_t value);
184 
186  static Ptr instanceSymbolic(const SymbolicExpression::Ptr &value);
187 
188 public:
189  virtual InstructionSemantics::BaseSemantics::SValuePtr bottom_(size_t nBits) const override {
190  return instanceBottom(nBits);
191  }
192 
193  virtual InstructionSemantics::BaseSemantics::SValuePtr undefined_(size_t nBits) const override {
194  return instanceUndefined(nBits);
195  }
196 
197  virtual InstructionSemantics::BaseSemantics::SValuePtr unspecified_(size_t nBits) const override {
198  return instanceUnspecified(nBits);
199  }
200 
201  virtual InstructionSemantics::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) const override {
202  return instanceInteger(nBits, value);
203  }
204 
205  virtual InstructionSemantics::BaseSemantics::SValuePtr boolean_(bool value) const override {
206  return instanceInteger(1, value ? 1 : 0);
207  }
208 
209  virtual InstructionSemantics::BaseSemantics::SValuePtr copy(size_t newNBits = 0) const override;
210 
212  createOptionalMerge(const InstructionSemantics::BaseSemantics::SValuePtr &other,
214  const SmtSolverPtr&) const override;
215 
216 public:
220  static Ptr promote(const InstructionSemantics::BaseSemantics::SValuePtr &v) { // hot
221  Ptr retval = v.dynamicCast<SValue>();
222  ASSERT_not_null(retval);
223  return retval;
224  }
225 
226 public:
233  AddressInterval region() const;
234  void region(const AddressInterval&);
237 public:
238  virtual void print(std::ostream&, InstructionSemantics::BaseSemantics::Formatter&) const override;
239  virtual void hash(Combinatorics::Hasher&) const override;
240 };
241 
243 // Instruction semantics state
245 
247 using StatePtr = boost::shared_ptr<class State>;
248 
250 class State: public InstructionSemantics::SymbolicSemantics::State {
251 public:
253  using Super = InstructionSemantics::SymbolicSemantics::State;
254 
256  using Ptr = StatePtr;
257 
258 private:
259  FunctionCallStack callStack_;
260 
261 protected:
262  State();
265 
266  // Deep copy
267  State(const State&);
268 
269 public:
273 
275  static Ptr instance(const StatePtr&);
276 
280  const InstructionSemantics::BaseSemantics::MemoryStatePtr &memory) const override {
281  return instance(registers, memory);
282  }
283 
285  virtual InstructionSemantics::BaseSemantics::StatePtr clone() const override;
286 
288  static Ptr promote(const InstructionSemantics::BaseSemantics::StatePtr&);
289 
290 public:
296  const FunctionCallStack& callStack() const;
297  FunctionCallStack& callStack();
299 };
300 
302 // Instruction semantics domain
304 
306 class RiscOperators: public InstructionSemantics::SymbolicSemantics::RiscOperators {
307 public:
308  using Super = InstructionSemantics::SymbolicSemantics::RiscOperators;
309 
310  using Ptr = RiscOperatorsPtr;
311 
312 private:
313  const Settings settings_;
314  const Partitioner2::Partitioner &partitioner_;
315  SmtSolver::Ptr modelCheckerSolver_; // solver used for model checking, different than RISC operators
316  size_t nInstructions_ = 0;
317  SemanticCallbacks *semantics_ = nullptr;
318  AddressInterval stackLimits_; // where the stack can exist in memory
319  bool computeMemoryRegions_ = false; // compute memory regions. This is needed for OOB analysis.
320 
321  mutable SAWYER_THREAD_TRAITS::Mutex variableFinderMutex_; // protects the following data m
322  Variables::VariableFinderPtr variableFinder_unsync; // shared by all RiscOperator objects
323 
324 protected:
325  RiscOperators(const Settings&, const Partitioner2::Partitioner&, ModelChecker::SemanticCallbacks*,
328 
329 public: // Standard public construction-like functions
330  ~RiscOperators();
331 
332  static Ptr instance(const Settings&, const Partitioner2::Partitioner&, ModelChecker::SemanticCallbacks*,
335 
337  create(const InstructionSemantics::BaseSemantics::SValuePtr&, const SmtSolverPtr&) const override;
338 
340  create(const InstructionSemantics::BaseSemantics::StatePtr&, const SmtSolverPtr&) const override;
341 
343 
344 public: // Supporting functions
348  const Partitioner2::Partitioner& partitioner() const;
349 
356  SmtSolver::Ptr modelCheckerSolver() const;
357  void modelCheckerSolver(const SmtSolver::Ptr&);
365  bool computeMemoryRegions() const;
366  void computeMemoryRegions(bool);
376  void checkNullAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode);
377 
381  void checkOobAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode, size_t nBytes);
382 
386  void checkUninitVar(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, size_t nBytes);
387 
394  size_t nInstructions() const;
395  void nInstructions(size_t);
399  void maybeInitCallStack(rose_addr_t insnVa);
400 
402  void pushCallStack(const Partitioner2::FunctionPtr &callee, rose_addr_t initialSp, Sawyer::Optional<rose_addr_t> returnVa);
403 
408  void popCallStack();
409 
416  size_t pruneCallStack();
417 
419  void printCallStack(std::ostream&, const std::string &prefix);
420 
436  assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result);
437 
439  assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result,
441 
443  assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result,
448 public: // Override RISC operations
449  virtual void finishInstruction(SgAsmInstruction*) override;
450 
452  number_(size_t nBits, uint64_t value) override;
453 
455  extract(const InstructionSemantics::BaseSemantics::SValuePtr&, size_t begin, size_t end) override;
456 
459  const InstructionSemantics::BaseSemantics::SValuePtr &highBits) override;
460 
463  const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override;
464 
467  const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override;
468 
471  const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override;
472 
474  unsignedExtend(const InstructionSemantics::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
475 
477  signExtend(const InstructionSemantics::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
478 
482 
487  InstructionSemantics::BaseSemantics::SValuePtr &overflowed /*out*/) override;
488 
492 
494  subtractCarry(const InstructionSemantics::BaseSemantics::SValuePtr &a,
497  InstructionSemantics::BaseSemantics::SValuePtr &overflowed /*out*/) override;
498 
500  addWithCarries(const InstructionSemantics::BaseSemantics::SValuePtr &a,
503  InstructionSemantics::BaseSemantics::SValuePtr &carryOut /*out*/) override;
504 
506  readRegister(RegisterDescriptor, const InstructionSemantics::BaseSemantics::SValuePtr&) override;
507 
508  virtual void
509  writeRegister(RegisterDescriptor, const InstructionSemantics::BaseSemantics::SValuePtr&) override;
510 
512  readMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr,
515 
516  virtual void
517  writeMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr,
520 };
521 
523 // High-level semantic operations
525 
527 class SemanticCallbacks: public Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks {
528 public:
529  using Ptr = SemanticCallbacksPtr;
531 
532 private:
533  Settings settings_; // settings are set by the constructor and not modified thereafter
534  const Partitioner2::Partitioner &partitioner_; // generally shouldn't be changed once model checking starts
535  SmtSolver::Memoizer::Ptr smtMemoizer_; // memoizer shared among all solvers
536 
537  mutable SAWYER_THREAD_TRAITS::Mutex unitsMutex_; // protects only the units_ data member
538  Sawyer::Container::Map<rose_addr_t, ExecutionUnitPtr> units_; // cached execution units
539 
540  mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects the following data members
541  std::set<uint64_t> seenStates_; // states we've seen, by hash
542  size_t nDuplicateStates_ = 0; // number of times a previous state is seen again
543  size_t nSolverFailures_ = 0; // number of times the SMT solver failed
544  UnitCounts unitsReached_; // number of times basic blocks were reached
545  Variables::VariableFinderPtr variableFinder_; // also shared by all RiscOperator objects
546 
547  // This model is able to follow a single path specified by the user. In order to do that, the user should call
548  // followOnePath to provide the ordered list of execution units. The nextCodeAddresses function is overridden to
549  // return only the address of the next execution unit in this list, or none when the list is empty. The findUnit
550  // function is enhanced to return the next execution unit and remove it from the list.
551  //
552  // These are also protected by mutex_
553  bool followingOnePath_ = false;
554  std::list<ExecutionUnitPtr> onePath_; // execution units yet to be consumed by findUnit
555 
556 protected:
557  SemanticCallbacks(const ModelChecker::SettingsPtr&, const Settings&, const Partitioner2::Partitioner&);
558 public:
559  ~SemanticCallbacks();
560 
561 public:
562  static Ptr instance(const ModelChecker::SettingsPtr&, const Settings&, const Partitioner2::Partitioner&);
563 
564 public:
566  const Partitioner2::Partitioner& partitioner() const;
567 
568 public:
584  void followOnePath(const std::list<ExecutionUnitPtr>&);
585 
597  bool followingOnePath() const;
598  void followingOnePath(bool);
608  SmtSolver::Memoizer::Ptr smtMemoizer() const;
609  void smtMemoizer(const SmtSolver::Memoizer::Ptr&);
619  size_t nDuplicateStates() const;
620 
628  size_t nSolverFailures() const;
629 
638  size_t nUnitsReached() const;
639 
646  UnitCounts unitsReached() const;
647 
655  virtual bool filterNullDeref(const InstructionSemantics::BaseSemantics::SValuePtr &addr, SgAsmInstruction*,
656  TestMode testMode, IoMode ioMode);
657 
673  virtual bool filterOobAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
674  const AddressInterval &referencedRegion, const AddressInterval &accessedRegion,
675  SgAsmInstruction *insn, TestMode testMode, IoMode ioMode,
676  const Variables::StackVariable &intendedVariable, const AddressInterval &intendedVariableLocation,
677  const Variables::StackVariable &accessedVariable, const AddressInterval &accessedVariableLocation);
678 
679  virtual bool filterUninitVar(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
680  const AddressInterval &referencedREgion, const AddressInterval &accessedRegion,
681  SgAsmInstruction *insn, TestMode testMode, const Variables::StackVariable &variable,
682  const AddressInterval &variableLocation);
683 
684 public:
685  virtual void reset() override;
686 
687  virtual InstructionSemantics::BaseSemantics::SValuePtr protoval() override;
688 
689  virtual InstructionSemantics::BaseSemantics::RegisterStatePtr createInitialRegisters() override;
690 
691  virtual InstructionSemantics::BaseSemantics::MemoryStatePtr createInitialMemory() override;
692 
693  virtual InstructionSemantics::BaseSemantics::StatePtr createInitialState() override;
694 
695  virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr createRiscOperators() override;
696 
697  virtual void
698  initializeState(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
699 
701  createDispatcher(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
702 
703  virtual SmtSolver::Ptr createSolver() override;
704 
705  virtual void attachModelCheckerSolver(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
706  const SmtSolver::Ptr&) override;
707 
708  virtual CodeAddresses
709  nextCodeAddresses(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
710 
711  virtual std::vector<TagPtr>
712  preExecute(const ExecutionUnitPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
713 
714  virtual std::vector<TagPtr>
715  postExecute(const ExecutionUnitPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
716 
718  instructionPointer(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
719 
720  virtual std::vector<NextUnit>
721  nextUnits(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&) override;
722 
723 #ifdef ROSE_HAVE_YAMLCPP
724  virtual std::list<ExecutionUnitPtr>
725  parsePath(const YAML::Node&, const std::string &sourceName) override;
726 #endif
727 
728  virtual std::list<ExecutionUnitPtr>
729  parsePath(const Yaml::Node&, const std::string &sourceName) override;
730 
731 private:
732  // Records the state hash and returns true if we've seen it before.
734 
735  // Find and cache the execution unit at the specified address.
736  ExecutionUnitPtr findUnit(rose_addr_t va, const Progress::Ptr&);
737 };
738 
739 } // namespace
740 } // namespace
741 } // namespace
742 } // namespace
743 
744 #endif
745 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:45
Unsigned shiftRight(Unsigned src, size_t n, bool b=false)
Right shift a value.
Definition: BitOps.h:106
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.
Definition: GraphUtility.h:17
Sawyer::SharedPointer< Merger > MergerPtr
Shared-ownership pointer for Merger classes.
Sawyer::Container::IntervalMap< OffsetInterval, StackVariable > StackVariables
Collection of local variables organized by frame offsets.
Definition: Variables.h:267
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.
Definition: SmtSolver.h:231
Unsigned signExtend(Unsigned src, size_t n)
Sign extend part of a value to the full width of the src type.
Definition: BitOps.h:272
Unsigned shiftLeft(Unsigned src, size_t n, bool b=false)
Left shift a value.
Definition: BitOps.h:76
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.
Definition: integerOps.h:131
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to concrete RISC operations.
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.
Stack-based container.
Definition: Stack.h:22
T extract(T bits)
Extract bits from a value.
Definition: integerOps.h:255
Sawyer::SharedPointer< Progress > Ptr
Progress objects are reference counted.
Definition: Progress.h:168
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.
State
Decoder state.
Definition: String.h:198