ROSE  0.11.82.0
P2Model.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_P2Model_H
2 #define ROSE_BinaryAnalysis_ModelChecker_P2Model_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
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/InstructionSemantics2/SymbolicSemantics.h>
11 
12 namespace Rose {
13 namespace BinaryAnalysis {
14 namespace ModelChecker {
15 
24 namespace P2Model {
25 
27 // Settings for this model checker
29 
31 struct Settings {
33  enum class MemoryType {
34  LIST,
35  MAP
36  };
37 
43  rose_addr_t maxNullAddress = 4095;
44  bool debugNull = false;
47  bool solverMemoization = false;
48  bool traceSemantics = false;
49 };
50 
51 class SemanticCallbacks;
52 
57 
63 
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();
86 
88  Partitioner2::FunctionPtr function() const;
89 
93  rose_addr_t initialStackPointer() const;
94 
97 
103  rose_addr_t framePointerDelta() const;
104  void framePointerDelta(rose_addr_t);
110  rose_addr_t framePointer(size_t nBits) const;
111 
120  std::string printableName(size_t nBits) const;
121 };
122 
127 
129 // Instruction semantics value
131 
136 public:
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 SymbolicExpr::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 SymbolicExpr::Ptr &value);
187 
188 public:
190  return instanceBottom(nBits);
191  }
192 
194  return instanceUndefined(nBits);
195  }
196 
198  return instanceUnspecified(nBits);
199  }
200 
201  virtual InstructionSemantics2::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) const override {
202  return instanceInteger(nBits, value);
203  }
204 
205  virtual InstructionSemantics2::BaseSemantics::SValuePtr boolean_(bool value) const override {
206  return instanceInteger(1, value ? 1 : 0);
207  }
208 
209  virtual InstructionSemantics2::BaseSemantics::SValuePtr copy(size_t newNBits = 0) const override;
210 
214  const SmtSolverPtr&) const override;
215 
216 public:
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&, InstructionSemantics2::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 
251 public:
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 InstructionSemantics2::BaseSemantics::MemoryStatePtr &memory) const override {
281  return instance(registers, memory);
282  }
283 
285  virtual InstructionSemantics2::BaseSemantics::StatePtr clone() const override;
286 
289 
290 public:
296  const FunctionCallStack& callStack() const;
299 };
300 
302 // Instruction semantics domain
304 
307 public:
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:
328 
329 public: // Standard public construction-like functions
330  ~RiscOperators();
331 
335 
338 
341 
343 
344 public: // Supporting functions
348  const Partitioner2::Partitioner& partitioner() const;
349 
357  void modelCheckerSolver(const SmtSolver::Ptr&);
365  bool computeMemoryRegions() const;
366  void computeMemoryRegions(bool);
377 
382 
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 
437 
441 
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 InstructionSemantics2::BaseSemantics::SValuePtr&, size_t begin, size_t end) override;
456 
459  const InstructionSemantics2::BaseSemantics::SValuePtr &highBits) override;
460 
464 
468 
472 
474  unsignedExtend(const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
475 
477  signExtend(const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
478 
482 
487  InstructionSemantics2::BaseSemantics::SValuePtr &overflowed /*out*/) override;
488 
492 
497  InstructionSemantics2::BaseSemantics::SValuePtr &overflowed /*out*/) override;
498 
503  InstructionSemantics2::BaseSemantics::SValuePtr &carryOut /*out*/) override;
504 
507 
508  virtual void
510 
515 
516  virtual void
520 };
521 
523 // High-level semantic operations
525 
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:
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);
619  size_t nDuplicateStates() const;
620 
628  size_t nSolverFailures() const;
629 
638  size_t nUnitsReached() const;
639 
646  UnitCounts unitsReached() const;
647 
656  TestMode testMode, IoMode ioMode);
657 
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 InstructionSemantics2::BaseSemantics::SValuePtr &addr,
680  const AddressInterval &referencedREgion, const AddressInterval &accessedRegion,
682  const AddressInterval &variableLocation);
683 
684 public:
685  virtual void reset() override;
686 
688 
690 
692 
694 
696 
697  virtual void
699 
702 
703  virtual SmtSolver::Ptr createSolver() override;
704 
706  const SmtSolver::Ptr&) override;
707 
708  virtual CodeAddresses
710 
711  virtual std::vector<TagPtr>
712  preExecute(const ExecutionUnitPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) override;
713 
714  virtual std::vector<TagPtr>
715  postExecute(const ExecutionUnitPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) override;
716 
719 
720  virtual std::vector<NextUnit>
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
void checkUninitVar(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, size_t nBytes)
Test whether the specified address accesses an uninitialized variable.
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:48
SmtSolver::Memoizer::Ptr smtMemoizer() const
Property: SMT solver memoizer.
virtual void print(std::ostream &, InstructionSemantics2::BaseSemantics::Formatter &) const override
Print a value to a stream using default format.
TestMode oobRead
How to test for out-of-bounds reads.
Definition: P2Model.h:40
Symbolic values with memory regions.
Definition: P2Model.h:135
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
static Ptr instanceBottom(size_t nBits)
Instantiate a new data-flow bottom value.
virtual InstructionSemantics2::BaseSemantics::SValuePtr shiftRight(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override
Returns arg shifted right logically (no sign bit).
Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &)
Command-line switches for settings.
Defines RISC operators for the SymbolicSemantics domain.
void pushCallStack(const Partitioner2::FunctionPtr &callee, rose_addr_t initialSp, Sawyer::Optional< rose_addr_t > returnVa)
Push a function onto the call stack.
virtual InstructionSemantics2::BaseSemantics::SValuePtr addCarry(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b, InstructionSemantics2::BaseSemantics::SValuePtr &carryOut, InstructionSemantics2::BaseSemantics::SValuePtr &overflowed) override
Adds two integers of equal size and carry.
static Ptr instanceUnspecified(size_t nBits)
Instantiate a new unspecified value.
TestMode nullRead
How to test for reads from the null page.
Definition: P2Model.h:38
virtual SmtSolver::Ptr createSolver() override
Create model checker solver.
virtual void writeMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr, const InstructionSemantics2::BaseSemantics::SValuePtr &value, const InstructionSemantics2::BaseSemantics::SValuePtr &cond) override
Writes a value to memory.
virtual void hash(Combinatorics::Hasher &) const override
Hash this semantic value.
Base class for machine instructions.
virtual std::list< ExecutionUnitPtr > parsePath(const Yaml::Node &, const std::string &sourceName) override
Construct a path from a YAML document.
TestMode uninitVar
How to test for uninitialized variable reads.
Definition: P2Model.h:42
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
const Variables::StackVariables & stackVariables() const
Property: Stack variables.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
virtual InstructionSemantics2::BaseSemantics::SValuePtr subtract(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b) override
Subtract one value from another.
size_t nSolverFailures() const
Property: Number of times the SMT solver failed.
void checkNullAccess(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, IoMode)
Test whether the specified address is considered to be null.
virtual InstructionSemantics2::BaseSemantics::SValuePtr instructionPointer(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Address of the next instruction.
bool followingOnePath() const
Property: Whether we are in follow-one-path mode.
rose_addr_t maxNullAddress
Maximum address of the null page.
Definition: P2Model.h:43
void followOnePath(const std::list< ExecutionUnitPtr > &)
Cause this model to follow only one path through the specimen.
TestMode
Mode by which comparisons are made.
virtual InstructionSemantics2::BaseSemantics::SValuePtr signExtend(const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override
Sign extends a value.
void maybeInitCallStack(rose_addr_t insnVa)
Ensure call stack has a root function.
virtual std::vector< TagPtr > postExecute(const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Called after execution ends.
virtual InstructionSemantics2::BaseSemantics::SValuePtr shiftRightArithmetic(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override
Returns arg shifted right arithmetically (with sign bit).
A collection of related switch declarations.
size_t nUnitsReached() const
Property: Number of execution units reached.
virtual InstructionSemantics2::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) override
Returns a number of the specified bit width.
Detection is reported only if it must occur.
virtual SValuePtr protoval() const
Property: Prototypical semantic value.
void printCallStack(std::ostream &, const std::string &prefix)
Print information about the function call stack.
Main namespace for the ROSE library.
bool solverMemoization
Whether the SMT solver should use memoization.
Definition: P2Model.h:47
Describes one funtion call in the call stack.
Definition: P2Model.h:75
TestMode nullWrite
How to test for writes from the null page.
Definition: P2Model.h:39
virtual CodeAddresses nextCodeAddresses(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Possible next code addresses.
virtual void attachModelCheckerSolver(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &) override
Associate solver with semantics.
virtual std::vector< NextUnit > nextUnits(const PathPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &) override
Discover next execution units.
virtual void reset() override
Reset internal data.
const Partitioner2::Partitioner & partitioner() const
Property: Partitioner.
static Ptr instanceUndefined(size_t nBits)
Instantiate a new undefined value.
virtual InstructionSemantics2::BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr, const InstructionSemantics2::BaseSemantics::SValuePtr &dflt, const InstructionSemantics2::BaseSemantics::SValuePtr &cond) override
Reads a value from memory.
size_t nInstructions() const
Property: Number of instructions executed.
virtual InstructionSemantics2::BaseSemantics::RegisterStatePtr createInitialRegisters() override
Create an initial register state.
virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr create(const InstructionSemantics2::BaseSemantics::SValuePtr &, const SmtSolverPtr &) const override
Virtual allocating constructor.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
Sawyer::Optional< rose_addr_t > initialStackVa
Address for initial stack pointer.
Definition: P2Model.h:45
const Partitioner2::Partitioner & partitioner() const
Property: Partitioner being used.
SValuePtr Ptr
Shared-ownership pointer.
Definition: P2Model.h:141
IoMode
Direction of data wrt storage.
static Ptr instanceSymbolic(const SymbolicExpr::Ptr &value)
Instantiate a new symbolic value.
virtual InstructionSemantics2::BaseSemantics::SValuePtr readRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr &) override
Reads a value from a register.
std::string printableName(size_t nBits) const
Some basic info about the function call.
YAML node.
Definition: Yaml.h:328
static Ptr instanceInteger(size_t nBits, uint64_t value)
Instantiate a new concrete value.
void checkOobAccess(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, IoMode, size_t nBytes)
Test whether the specified address is out of bounds for variables.
virtual InstructionSemantics2::BaseSemantics::SValuePtr unsignedExtend(const InstructionSemantics2::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...
virtual InstructionSemantics2::BaseSemantics::SValuePtr bottom_(size_t nBits) const override
Data-flow bottom value.
Definition: P2Model.h:189
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.
StatePtr Ptr
Shared-ownership pointer for a State.
Definition: State.h:42
virtual InstructionSemantics2::BaseSemantics::SValuePtr extract(const InstructionSemantics2::BaseSemantics::SValuePtr &, size_t begin, size_t end) override
Extracts bits from a value.
virtual InstructionSemantics2::BaseSemantics::SValuePtr boolean_(bool value) const override
Create a new, Boolean value.
Definition: P2Model.h:205
SmtSolver::Ptr modelCheckerSolver() const
Property: Model checker SMT solver.
Base class for semantics machine states.
Definition: State.h:39
virtual InstructionSemantics2::BaseSemantics::SValuePtr protoval() override
Create a prototypical semantic value.
const FunctionCallStack & callStack() const
Function call stack.
static Ptr promote(const InstructionSemantics2::BaseSemantics::StatePtr &)
Checked dynamic cast.
size_t nDuplicateStates() const
Property: Number of duplicate states.
boost::shared_ptr< class State > StatePtr
Shared-ownership pointer for semantic state.
Definition: P2Model.h:247
rose_addr_t framePointer(size_t nBits) const
Computed frame pointer.
User-defined functions for model checking semantics.
virtual InstructionSemantics2::BaseSemantics::SValuePtr shiftLeft(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override
Returns arg shifted left.
SharedPointer< U > dynamicCast() const
Dynamic cast.
Base class for most instruction semantics RISC operators.
Definition: RiscOperators.h:48
virtual void writeRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr &) override
Writes a value to a register.
Sawyer::Optional< rose_addr_t > returnAddress() const
Address to which function returns.
virtual InstructionSemantics2::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 bool filterOobAccess(const InstructionSemantics2::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.
Sawyer::CommandLine::SwitchGroup commandLineModelSwitches(Settings &)
Command-line switches for model settings.
StatePtr Ptr
Shared-ownership pointer.
Definition: P2Model.h:256
rose_addr_t initialStackPointer() const
Property: Initial stack pointer.
void popCallStack()
Pop a function from the call stack.
virtual InstructionSemantics2::BaseSemantics::StatePtr create(const InstructionSemantics2::BaseSemantics::RegisterStatePtr &registers, const InstructionSemantics2::BaseSemantics::MemoryStatePtr &memory) const override
Virtual constructor.
Definition: P2Model.h:279
bool traceSemantics
Whether to trace all RISC operators.
Definition: P2Model.h:48
Type of values manipulated by the SymbolicSemantics domain.
virtual std::vector< TagPtr > preExecute(const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Called before execution starts.
UnitCounts unitsReached() const
Property: Execution units reached.
AddressInterval region() const
Property: Optional memory region.
TestMode oobWrite
How to test for out-of-bounds writes.
Definition: P2Model.h:41
static Ptr instance(const InstructionSemantics2::BaseSemantics::RegisterStatePtr &, const InstructionSemantics2::BaseSemantics::MemoryStatePtr &)
Allocating constructor.
virtual void initializeState(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Initialize the initial state.
virtual InstructionSemantics2::BaseSemantics::StatePtr clone() const override
Virtual copy constructor.
virtual InstructionSemantics2::BaseSemantics::SValuePtr unspecified_(size_t nBits) const override
Create a new unspecified semantic value.
Definition: P2Model.h:197
virtual InstructionSemantics2::BaseSemantics::SValuePtr concat(const InstructionSemantics2::BaseSemantics::SValuePtr &lowBits, const InstructionSemantics2::BaseSemantics::SValuePtr &highBits) override
Concatenates the bits of two values.
virtual InstructionSemantics2::BaseSemantics::SValuePtr subtractCarry(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b, InstructionSemantics2::BaseSemantics::SValuePtr &carryOut, InstructionSemantics2::BaseSemantics::SValuePtr &overflowed) override
Subtract one value from another and carry.
virtual InstructionSemantics2::BaseSemantics::StatePtr createInitialState() override
Create an initial state.
virtual void finishInstruction(SgAsmInstruction *) override
Called at the end of every instruction.
Virtual definition of semantic operations for model checking.
Definition: P2Model.h:527
virtual InstructionSemantics2::BaseSemantics::SValuePtr add(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b) override
Adds two integers of equal size.
virtual InstructionSemantics2::BaseSemantics::DispatcherPtr createDispatcher(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
Create an instruction dispatcher.
MemoryType memoryType
Type of memory state.
Definition: P2Model.h:46
Partitions instructions into basic blocks and functions.
Definition: Partitioner.h:289
virtual InstructionSemantics2::BaseSemantics::SValuePtr addWithCarries(const InstructionSemantics2::BaseSemantics::SValuePtr &a, const InstructionSemantics2::BaseSemantics::SValuePtr &b, const InstructionSemantics2::BaseSemantics::SValuePtr &c, InstructionSemantics2::BaseSemantics::SValuePtr &carryOut) override
Add two values of equal size and a carry bit.
virtual InstructionSemantics2::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) const override
Create a new concrete semantic value.
Definition: P2Model.h:201
bool debugNull
When debugging is enabled, show null pointer checking?
Definition: P2Model.h:44
virtual InstructionSemantics2::BaseSemantics::SValuePtr undefined_(size_t nBits) const override
Create a new undefined semantic value.
Definition: P2Model.h:193
bool computeMemoryRegions() const
Property: Compute memory regions for variables.
virtual bool filterNullDeref(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, SgAsmInstruction *, TestMode testMode, IoMode ioMode)
Filter null dereferences.
static Ptr promote(const InstructionSemantics2::BaseSemantics::SValuePtr &v)
Promote a base value to a MemoryRegionSemantics value.
Definition: P2Model.h:220
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
Description of a local stack variable within a function.
Definition: Variables.h:146
InstructionSemantics2::BaseSemantics::SValuePtr assignRegion(const InstructionSemantics2::BaseSemantics::SValuePtr &result)
Assign a region to an expression.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:26
virtual Sawyer::Optional< InstructionSemantics2::BaseSemantics::SValuePtr > createOptionalMerge(const InstructionSemantics2::BaseSemantics::SValuePtr &other, const InstructionSemantics2::BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
Possibly create a new value by merging two existing values.
virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr createInitialMemory() override
Create an initial memory state.
rose_addr_t framePointerDelta() const
Property: Frame pointer delta.
virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr createRiscOperators() override
Create RISC operators.
static Ptr instance()
Instantiate a new prototypical value.