ROSE  0.11.51.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 
42  rose_addr_t maxNullAddress = 4095;
43  bool debugNull = false;
46  bool solverMemoization = true;
47  bool traceSemantics = false;
48 };
49 
50 class SemanticCallbacks;
51 
56 
58 // Function call stack
60 
62 class FunctionCall {
63  Partitioner2::FunctionPtr function_;
64  rose_addr_t initialStackPointer_ = 0;
65  rose_addr_t framePointerDelta_ = (rose_addr_t)(-4); // Normal frame pointer w.r.t. initial stack pointer
66  Variables::StackVariables stackVariables_;
67 
68 public:
69  ~FunctionCall();
70  FunctionCall(const Partitioner2::FunctionPtr&, rose_addr_t initialSp, const Variables::StackVariables&);
71 
73  Partitioner2::FunctionPtr function() const;
74 
78  rose_addr_t initialStackPointer() const;
79 
82 
88  rose_addr_t framePointerDelta() const;
89  void framePointerDelta(rose_addr_t);
91 };
92 
97 
99 // Instruction semantics value
101 
106 public:
109 
111  using Ptr = SValuePtr;
112 
113 private:
114  AddressInterval region_;
115 
116 #ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
117 private:
118  friend class boost::serialization::access;
119 
120  template<class S>
121  void serialize(S &s, const unsigned /*version*/) {
122  s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
123  s & BOOST_SERIALIZATION_NVP(region_);
124  }
125 #endif
126 
127 public:
128  ~SValue();
129 
130 protected:
131  SValue();
132 
133  SValue(size_t nBits, uint64_t number);
134 
135  explicit SValue(const SymbolicExpr::Ptr&);
136 
137 public:
141  static Ptr instance();
142 
144  static Ptr instanceBottom(size_t nBits);
145 
147  static Ptr instanceUndefined(size_t nBits);
148 
150  static Ptr instanceUnspecified(size_t nBits);
151 
153  static Ptr instanceInteger(size_t nBits, uint64_t value);
154 
156  static Ptr instanceSymbolic(const SymbolicExpr::Ptr &value);
157 
158 public:
160  return instanceBottom(nBits);
161  }
162 
164  return instanceUndefined(nBits);
165  }
166 
168  return instanceUnspecified(nBits);
169  }
170 
171  virtual InstructionSemantics2::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) const override {
172  return instanceInteger(nBits, value);
173  }
174 
175  virtual InstructionSemantics2::BaseSemantics::SValuePtr boolean_(bool value) const override {
176  return instanceInteger(1, value ? 1 : 0);
177  }
178 
179  virtual InstructionSemantics2::BaseSemantics::SValuePtr copy(size_t newNBits = 0) const override;
180 
184  const SmtSolverPtr&) const override;
185 
186 public:
191  Ptr retval = v.dynamicCast<SValue>();
192  ASSERT_not_null(retval);
193  return retval;
194  }
195 
196 public:
203  AddressInterval region() const;
204  void region(const AddressInterval&);
207 public:
208  virtual void print(std::ostream&, InstructionSemantics2::BaseSemantics::Formatter&) const override;
209  virtual void hash(Combinatorics::Hasher&) const override;
210 };
211 
213 // Instruction semantics state
215 
217 using StatePtr = boost::shared_ptr<class State>;
218 
221 public:
224 
226  using Ptr = StatePtr;
227 
228 private:
229  FunctionCallStack callStack_;
230 
231 protected:
232  State();
235 
236  // Deep copy
237  State(const State&);
238 
239 public:
243 
245  static Ptr instance(const StatePtr&);
246 
250  const InstructionSemantics2::BaseSemantics::MemoryStatePtr &memory) const override {
251  return instance(registers, memory);
252  }
253 
255  virtual InstructionSemantics2::BaseSemantics::StatePtr clone() const override;
256 
259 
260 public:
266  const FunctionCallStack& callStack() const;
269 };
270 
272 // Instruction semantics domain
274 
277 public:
279 
280  using Ptr = RiscOperatorsPtr;
281 
282 private:
283  const Settings settings_;
284  const Partitioner2::Partitioner &partitioner_;
285  SmtSolver::Ptr modelCheckerSolver_;
286  size_t nInstructions_ = 0;
287  SemanticCallbacks *semantics_ = nullptr;
288  AddressInterval stackLimits_; // where the stack can exist in memory
289  bool computeMemoryRegions_ = false; // compute memory regions. This is needed for OOB analysis.
290 
291  mutable SAWYER_THREAD_TRAITS::Mutex variableFinderMutex_; // protects the following data m
292  Variables::VariableFinderPtr variableFinder_unsync; // shared by all RiscOperator objects
293 
294 protected:
298 
299 public: // Standard public construction-like functions
300  ~RiscOperators();
301 
305 
308 
311 
313 
314 public: // Supporting functions
318  const Partitioner2::Partitioner& partitioner() const;
319 
327  void modelCheckerSolver(const SmtSolver::Ptr&);
335  bool computeMemoryRegions() const;
336  void computeMemoryRegions(bool);
347 
352 
359  size_t nInstructions() const;
360  void nInstructions(size_t);
364  void pushCallStack(const Partitioner2::FunctionPtr &callee, rose_addr_t initialSp);
365 
372  size_t pruneCallStack();
373 
375  void printCallStack(std::ostream&);
376 
382  static std::pair<uint64_t /*sum*/, bool /*saturated?*/> saturatedAdd(uint64_t base, int64_t delta);
383 
393  static AddressInterval shiftAddresses(const AddressInterval &base, int64_t delta, const AddressInterval &limit);
394  static AddressInterval shiftAddresses(uint64_t base, const Variables::OffsetInterval &delta, const AddressInterval &limit);
413 
417 
424 public: // Override RISC operations
425  virtual void startInstruction(SgAsmInstruction*) override;
426  virtual void finishInstruction(SgAsmInstruction*) override;
427 
429  number_(size_t nBits, uint64_t value) override;
430 
432  extract(const InstructionSemantics2::BaseSemantics::SValuePtr&, size_t begin, size_t end) override;
433 
436  const InstructionSemantics2::BaseSemantics::SValuePtr &highBits) override;
437 
441 
445 
449 
451  unsignedExtend(const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
452 
454  signExtend(const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
455 
459 
464  InstructionSemantics2::BaseSemantics::SValuePtr &overflowed /*out*/) override;
465 
469 
474  InstructionSemantics2::BaseSemantics::SValuePtr &overflowed /*out*/) override;
475 
480  InstructionSemantics2::BaseSemantics::SValuePtr &carryOut /*out*/) override;
481 
484 
485  virtual void
487 
492 
493  virtual void
497 };
498 
500 // High-level semantic operations
502 
505 public:
506  using Ptr = SemanticCallbacksPtr;
508 
509 private:
510  Settings settings_; // settings are set by the constructor and not modified thereafter
511  const Partitioner2::Partitioner &partitioner_; // generally shouldn't be changed once model checking starts
512 
513  mutable SAWYER_THREAD_TRAITS::Mutex unitsMutex_; // protects only the units_ data member
514  Sawyer::Container::Map<rose_addr_t, ExecutionUnitPtr> units_; // cached execution units
515 
516  mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects the following data members
517  std::set<uint64_t> seenStates_; // states we've seen, by hash
518  size_t nDuplicateStates_ = 0; // number of times a previous state is seen again
519  size_t nSolverFailures_ = 0; // number of times the SMT solver failed
520  UnitCounts unitsReached_; // number of times basic blocks were reached
521  Variables::VariableFinderPtr variableFinder_; // also shared by all RiscOperator objects
522 
523  // This model is able to follow a single path specified by the user. In order to do that, the user should call
524  // followOnePath to provide the ordered list of execution units. The nextCodeAddresses function is overridden to
525  // return only the address of the next execution unit in this list, or none when the list is empty. The findUnit
526  // function is enhanced to return the next execution unit and remove it from the list.
527  //
528  // These are also protected by mutex_
529  bool followingOnePath_ = false;
530  std::list<ExecutionUnitPtr> onePath_; // execution units yet to be consumed by findUnit
531 
532 protected:
533  SemanticCallbacks(const ModelChecker::SettingsPtr&, const Settings&, const Partitioner2::Partitioner&);
534 public:
536 
537 public:
538  static Ptr instance(const ModelChecker::SettingsPtr&, const Settings&, const Partitioner2::Partitioner&);
539 
540 public:
542  const Partitioner2::Partitioner& partitioner() const;
543 
544 public:
560  void followOnePath(const std::list<ExecutionUnitPtr>&);
561 
573  bool followingOnePath() const;
574  void followingOnePath(bool);
584  size_t nDuplicateStates() const;
585 
593  size_t nSolverFailures() const;
594 
603  size_t nUnitsReached() const;
604 
611  UnitCounts unitsReached() const;
612 
620  virtual bool filterNullDeref(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode testMode, IoMode ioMode);
621 
622 public:
623  virtual void reset() override;
624 
626 
628 
630 
632 
634 
635  virtual void
637 
640 
641  virtual SmtSolver::Ptr createSolver() override;
642 
644  const SmtSolver::Ptr&) override;
645 
646  virtual CodeAddresses
648 
649  virtual std::vector<TagPtr>
650  preExecute(const ExecutionUnitPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) override;
651 
654 
655  virtual std::vector<NextUnit>
657 
658 #ifdef ROSE_HAVE_LIBYAML
659  virtual std::list<ExecutionUnitPtr>
660  parsePath(const YAML::Node&, const std::string &sourceName) override;
661 #endif
662 
663 private:
664  // Records the state hash and returns true if we've seen it before.
666 
667  // Find and cache the execution unit at the specified address.
668  ExecutionUnitPtr findUnit(rose_addr_t va);
669 };
670 
671 } // namespace
672 } // namespace
673 } // namespace
674 } // namespace
675 
676 #endif
677 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:39
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:105
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.
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.
void pushCallStack(const Partitioner2::FunctionPtr &callee, rose_addr_t initialSp)
Push a function onto the call stack.
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.
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.
void printCallStack(std::ostream &)
Print information about the function call stack.
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:42
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.
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.
Main namespace for the ROSE library.
bool solverMemoization
Whether the SMT solver should use memoization.
Definition: P2Model.h:46
Describes one funtion call in the call stack.
Definition: P2Model.h:62
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 void startInstruction(SgAsmInstruction *) override
Called at the beginning of every instruction.
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:44
const Partitioner2::Partitioner & partitioner() const
Property: Partitioner being used.
SValuePtr Ptr
Shared-ownership pointer.
Definition: P2Model.h:111
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.
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:159
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:175
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:217
static AddressInterval shiftAddresses(const AddressInterval &base, int64_t delta, const AddressInterval &limit)
Offset an interval by a signed amount.
virtual bool filterNullDeref(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode testMode, IoMode ioMode)
Filter null dereferences.
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
static std::pair< uint64_t, bool > saturatedAdd(uint64_t base, int64_t delta)
Saturating addition.
virtual void writeRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr &) override
Writes a value to a register.
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.
StatePtr Ptr
Shared-ownership pointer.
Definition: P2Model.h:226
rose_addr_t initialStackPointer() const
Property: Initial stack pointer.
virtual InstructionSemantics2::BaseSemantics::StatePtr create(const InstructionSemantics2::BaseSemantics::RegisterStatePtr &registers, const InstructionSemantics2::BaseSemantics::MemoryStatePtr &memory) const override
Virtual constructor.
Definition: P2Model.h:249
bool traceSemantics
Whether to trace all RISC operators.
Definition: P2Model.h:47
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:167
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:504
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:45
Partitions instructions into basic blocks and functions.
Definition: Partitioner.h:290
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:171
bool debugNull
When debugging is enabled, show null pointer checking?
Definition: P2Model.h:43
virtual InstructionSemantics2::BaseSemantics::SValuePtr undefined_(size_t nBits) const override
Create a new undefined semantic value.
Definition: P2Model.h:163
bool computeMemoryRegions() const
Property: Compute memory regions for variables.
static Ptr promote(const InstructionSemantics2::BaseSemantics::SValuePtr &v)
Promote a base value to a MemoryRegionSemantics value.
Definition: P2Model.h:190
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.
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:25
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.