ROSE
0.11.98.0
|
Symbolic values with memory regions.
Values are symbolic, and some values also have memory region information.
#include <Rose/BinaryAnalysis/ModelChecker/P2Model.h>
Public Types | |
using | Super = InstructionSemantics::SymbolicSemantics::SValue |
Base class. More... | |
using | Ptr = SValuePtr |
Shared-ownership pointer. More... | |
Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue | |
using | Super = BaseSemantics::SValue |
Base type. More... | |
using | Ptr = SValuePtr |
Shared-ownership pointer. More... | |
Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue | |
using | Ptr = SValuePtr |
Shared-ownership pointer for an SValue object. More... | |
Public Member Functions | |
virtual InstructionSemantics::BaseSemantics::SValuePtr | bottom_ (size_t nBits) const override |
Data-flow bottom value. More... | |
virtual InstructionSemantics::BaseSemantics::SValuePtr | undefined_ (size_t nBits) const override |
Create a new undefined semantic value. More... | |
virtual InstructionSemantics::BaseSemantics::SValuePtr | unspecified_ (size_t nBits) const override |
Create a new unspecified semantic value. More... | |
virtual InstructionSemantics::BaseSemantics::SValuePtr | number_ (size_t nBits, uint64_t value) const override |
Create a new concrete semantic value. More... | |
virtual InstructionSemantics::BaseSemantics::SValuePtr | boolean_ (bool value) const override |
Create a new, Boolean value. More... | |
virtual InstructionSemantics::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. More... | |
virtual Sawyer::Optional< InstructionSemantics::BaseSemantics::SValuePtr > | createOptionalMerge (const InstructionSemantics::BaseSemantics::SValuePtr &other, const InstructionSemantics::BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override |
Possibly create a new value by merging two existing values. More... | |
virtual void | print (std::ostream &, InstructionSemantics::BaseSemantics::Formatter &) const override |
Print a value to a stream using default format. More... | |
virtual void | hash (Combinatorics::Hasher &) const override |
Hash this semantic value. More... | |
AddressInterval | region () const |
Property: Optional memory region. More... | |
void | region (const AddressInterval &) |
Property: Optional memory region. More... | |
Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue | |
virtual bool | isBottom () const override |
Determines whether a value is a data-flow bottom. More... | |
virtual SValuePtr | substitute (const SValuePtr &from, const SValuePtr &to, const SmtSolverPtr &solver) const |
Substitute one value for another throughout a value. More... | |
virtual const ExprPtr & | get_expression () const |
Returns the expression stored in this value. More... | |
virtual const InsnSet & | get_defining_instructions () const |
Returns the set of instructions that defined this value. More... | |
virtual void | defined_by (SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2, const InsnSet &set3) |
Adds instructions to the list of defining instructions. More... | |
virtual void | defined_by (SgAsmInstruction *insn, const InsnSet &set1, const InsnSet &set2) |
Adds instructions to the list of defining instructions. More... | |
virtual void | defined_by (SgAsmInstruction *insn, const InsnSet &set1) |
Adds instructions to the list of defining instructions. More... | |
virtual void | defined_by (SgAsmInstruction *insn) |
Adds instructions to the list of defining instructions. More... | |
virtual void | set_expression (const ExprPtr &new_expr) |
Changes the expression stored in the value. | |
virtual void | set_expression (const SValuePtr &source) |
Changes the expression stored in the value. | |
virtual size_t | add_defining_instructions (const InsnSet &to_add) |
Adds definitions to the list of defining instructions. More... | |
virtual size_t | add_defining_instructions (const SValuePtr &source) |
Adds definitions to the list of defining instructions. More... | |
virtual size_t | add_defining_instructions (SgAsmInstruction *insn) |
Adds definitions to the list of defining instructions. More... | |
virtual void | set_defining_instructions (const InsnSet &new_defs) |
Set defining instructions. More... | |
virtual void | set_defining_instructions (const SValuePtr &source) |
Set defining instructions. More... | |
virtual void | set_defining_instructions (SgAsmInstruction *insn) |
Set defining instructions. More... | |
Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue | |
SValuePtr | createMerged (const SValuePtr &other, const MergerPtr &merger, const SmtSolverPtr &solver) const |
Create a new value by merging two existing values. More... | |
size_t | nBits () const |
Property: value width. More... | |
bool | isConcrete () const |
Determines if the value is a concrete number. More... | |
Sawyer::Optional< uint64_t > | toUnsigned () const |
Converts a concrete value to a native unsigned integer. More... | |
Sawyer::Optional< int64_t > | toSigned () const |
Converts a concrete value to a native signed integer. More... | |
bool | mustEqual (const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const |
Tests two values for equality. More... | |
bool | mayEqual (const SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const |
Tests two values for possible equality. More... | |
bool | isTrue () const |
Returns true if concrete non-zero. More... | |
bool | isFalse () const |
Returns true if concrete zero. More... | |
std::string | toString () const |
Render this symbolic expression as a string. More... | |
std::string | comment () const |
Property: Comment. More... | |
void | comment (const std::string &) const |
Property: Comment. More... | |
void | print (std::ostream &) const |
Print a value to a stream using default format. More... | |
WithFormatter | with_format (Formatter &fmt) |
Used for printing values with formatting. More... | |
WithFormatter | operator+ (Formatter &fmt) |
Used for printing values with formatting. More... | |
WithFormatter | operator+ (const std::string &linePrefix) |
Used for printing values with formatting. More... | |
virtual size_t | get_width () const |
Virtual API. More... | |
Public Member Functions inherited from Sawyer::SharedObject | |
SharedObject () | |
Default constructor. More... | |
SharedObject (const SharedObject &) | |
Copy constructor. More... | |
virtual | ~SharedObject () |
Virtual destructor. More... | |
SharedObject & | operator= (const SharedObject &) |
Assignment. More... | |
Public Member Functions inherited from Sawyer::SharedFromThis< SValue > | |
SharedPointer< SValue > | sharedFromThis () |
Create a shared pointer from this . More... | |
SharedPointer< const SValue > | sharedFromThis () const |
Create a shared pointer from this . More... | |
Static Public Member Functions | |
static Ptr | instance () |
Instantiate a new prototypical value. More... | |
static Ptr | instanceBottom (size_t nBits) |
Instantiate a new data-flow bottom value. More... | |
static Ptr | instanceUndefined (size_t nBits) |
Instantiate a new undefined value. More... | |
static Ptr | instanceUnspecified (size_t nBits) |
Instantiate a new unspecified value. More... | |
static Ptr | instanceInteger (size_t nBits, uint64_t value) |
Instantiate a new concrete value. More... | |
static Ptr | instanceSymbolic (const SymbolicExpr::Ptr &value) |
Instantiate a new symbolic value. More... | |
static Ptr | promote (const InstructionSemantics::BaseSemantics::SValuePtr &v) |
Promote a base value to a MemoryRegionSemantics value. More... | |
Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue | |
static SValuePtr | instance () |
Instantiate a new prototypical value. More... | |
static SValuePtr | instance_bottom (size_t nbits) |
Instantiate a new data-flow bottom value of specified width. More... | |
static SValuePtr | instance_undefined (size_t nbits) |
Instantiate a new undefined value of specified width. More... | |
static SValuePtr | instance_unspecified (size_t nbits) |
Instantiate a new unspecified value of specified width. More... | |
static SValuePtr | instance_integer (size_t nbits, uint64_t value) |
Instantiate a new concrete value. More... | |
static SValuePtr | instance_symbolic (const SymbolicExpr::Ptr &value) |
Instantiate a new symbolic value. More... | |
static SValuePtr | promote (const BaseSemantics::SValuePtr &v) |
Promote a base value to a SymbolicSemantics value. More... | |
Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue | |
static SValuePtr | promote (const SValuePtr &x) |
Static Public Member Functions inherited from Sawyer::SmallObject | |
static SynchronizedPoolAllocator & | poolAllocator () |
Return the pool allocator for this class. More... | |
static void * | operator new (size_t size) |
static void | operator delete (void *ptr, size_t size) |
Protected Member Functions | |
SValue (size_t nBits, uint64_t number) | |
SValue (const SymbolicExpr::Ptr &) | |
Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue | |
SValue (size_t nbits) | |
SValue (size_t nbits, uint64_t number) | |
SValue (ExprPtr expr) | |
virtual bool | may_equal (const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override |
Virtual API. More... | |
virtual bool | must_equal (const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const override |
Virtual API. More... | |
virtual void | set_width (size_t nbits) override |
Virtual API. More... | |
virtual bool | is_number () const override |
Virtual API. More... | |
virtual uint64_t | get_number () const override |
Virtual API. More... | |
virtual std::string | get_comment () const override |
Some subclasses support the ability to add comments to values. More... | |
virtual void | set_comment (const std::string &) const override |
Some subclasses support the ability to add comments to values. More... | |
Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue | |
SValue (size_t nbits) | |
SValue (const SValue &other) | |
Additional Inherited Members | |
Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue | |
ExprPtr | expr |
The symbolic expression for this value. More... | |
InsnSet | defs |
Instructions defining this value. More... | |
Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::SValue | |
size_t | width |
|
static |
Instantiate a new prototypical value.
Prototypical values are only used for their virtual constructors.
|
static |
Instantiate a new data-flow bottom value.
Referenced by bottom_().
|
static |
Instantiate a new undefined value.
Referenced by undefined_().
|
static |
Instantiate a new unspecified value.
Referenced by unspecified_().
|
static |
Instantiate a new concrete value.
Referenced by boolean_(), and number_().
|
static |
Instantiate a new symbolic value.
|
inlineoverridevirtual |
Data-flow bottom value.
Returns a new value that represents bottom in a data-flow analysis. If a semantic domain can represent a bottom value then the isBottom predicate is true when invoked on this method's return value. If a semantic domain cannot support a bottom value, then it may return some other value.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.
Definition at line 189 of file P2Model.h.
References instanceBottom().
|
inlineoverridevirtual |
Create a new undefined semantic value.
The new semantic value will have the same dynamic type as the value on which this virtual method is called. This is the most common way that a new value is created. The unspecified_ method is closely related.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.
Definition at line 193 of file P2Model.h.
References instanceUndefined().
|
inlineoverridevirtual |
Create a new unspecified semantic value.
The new semantic value will have the same dynamic type as the value on which this virtual method is called. Undefined (undefined_) and unspecified are closely related. Unspecified values are the same as undefined values except they're instantiated as the result of some machine instruction where the ISA documentation indicates that the value is unspecified (e.g., status flags for x86 shift and rotate instructions).
Most semantic domains make no distinction between undefined and unspecified.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.
Definition at line 197 of file P2Model.h.
References instanceUnspecified().
|
inlineoverridevirtual |
Create a new concrete semantic value.
The new value will represent the specified concrete value and have the same dynamic type as the value on which this virtual method is called. This is the most common way that a new constant is created. The number
is truncated to contain nbits
bits (higher order bits are cleared).
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.
Definition at line 201 of file P2Model.h.
References instanceInteger().
|
inlineoverridevirtual |
Create a new, Boolean value.
The new semantic value will have the same dynamic type as the value on which this virtual method is called. This is how 1-bit flag register values (among others) are created. The base implementation uses number_() to construct a 1-bit value whose bit is zero (false) or one (true).
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.
Definition at line 205 of file P2Model.h.
References instanceInteger().
|
overridevirtual |
Create a new value from an existing value, changing the width if new_width
is non-zero.
Increasing the width logically adds zero bits to the most significant side of the value; decreasing the width logically removes bits from the most significant side of the value.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.
|
overridevirtual |
Possibly create a new value by merging two existing values.
This method optionally returns a new semantic value as the data-flow merge of this
and other
. If the two inputs are "equal" in some sense of the dataflow implementation then nothing is returned, otherwise a new value is returned. Typical usage is like this:
If you always want a copy regardless of whether the merge is necessary, then use the createMerged convenience function instead.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.
|
inlinestatic |
Promote a base value to a MemoryRegionSemantics value.
The value v
must have a MemoryRegionSemantics::SValue dynamic type.
Definition at line 220 of file P2Model.h.
References Sawyer::SharedPointer< T >::dynamicCast().
AddressInterval Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::region | ( | ) | const |
Property: Optional memory region.
This property describes a contiguous region of memory into which this value points if this value were to be treated as a pointer. The region usually corresponds to a variable in the source language.
void Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::region | ( | const AddressInterval & | ) |
Property: Optional memory region.
This property describes a contiguous region of memory into which this value points if this value were to be treated as a pointer. The region usually corresponds to a variable in the source language.
|
overridevirtual |
Print a value to a stream using default format.
The value will normally occupy a single line and not contain leading space or line termination. See also, with_format().
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.
|
overridevirtual |
Hash this semantic value.
Hashes the value by appending it to the specified hasher.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue.