Description
Semantic values for generating static semantic ASTs.
Each SValue has a pointer to a partly-constructed AST. In general, the parent pointers in these AST nodes are not initialized because many of these nodes are being shared across multiple subtrees. ROSE's instruction semantics framework relies very heavily on node sharing, but the AST was not designed for this. Do not expect AST traversals and analysis to work correctly for ASTs pointed to by an SValue. But never fear, the SValue's AST will be fixed when it's actually attached to an instruction node.
Definition at line 74 of file StaticSemantics.h.
#include <StaticSemantics.h>
Public Types | |
| using | Super = BaseSemantics::SValue |
| Base type. More... | |
| using | Ptr = SValuePtr |
| Shared-ownership pointer. More... | |
 Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue | |
| using | Ptr = SValuePtr |
| Shared-ownership pointer for an SValue object. More... | |
Public Member Functions | |
| virtual BaseSemantics::SValuePtr | bottom_ (size_t nbits) const ROSE_OVERRIDE |
| Data-flow bottom value. More... | |
| virtual BaseSemantics::SValuePtr | undefined_ (size_t nbits) const ROSE_OVERRIDE |
| Create a new undefined semantic value. More... | |
| virtual BaseSemantics::SValuePtr | unspecified_ (size_t nbits) const ROSE_OVERRIDE |
| Create a new unspecified semantic value. More... | |
| virtual BaseSemantics::SValuePtr | number_ (size_t nbits, uint64_t value) const ROSE_OVERRIDE |
| Create a new concrete semantic value. More... | |
| virtual BaseSemantics::SValuePtr | boolean_ (bool value) const ROSE_OVERRIDE |
| Create a new, Boolean value. More... | |
| virtual BaseSemantics::SValuePtr | copy (size_t new_width=0) const ROSE_OVERRIDE |
Create a new value from an existing value, changing the width if new_width is non-zero. More... | |
| virtual Sawyer::Optional< BaseSemantics::SValuePtr > | createOptionalMerge (const BaseSemantics::SValuePtr &, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const ROSE_OVERRIDE |
| Possibly create a new value by merging two existing values. More... | |
| virtual bool | may_equal (const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE |
| Virtual API. More... | |
| virtual bool | must_equal (const BaseSemantics::SValuePtr &other, const SmtSolverPtr &solver=SmtSolverPtr()) const ROSE_OVERRIDE |
| Virtual API. More... | |
| virtual void | set_width (size_t nbits) ROSE_OVERRIDE |
| Virtual API. More... | |
| virtual bool | isBottom () const ROSE_OVERRIDE |
| Determines whether a value is a data-flow bottom. More... | |
| virtual bool | is_number () const ROSE_OVERRIDE |
| Virtual API. More... | |
| virtual uint64_t | get_number () const ROSE_OVERRIDE |
| Virtual API. More... | |
| virtual void | hash (Combinatorics::Hasher &) const override |
| Hash this semantic value. More... | |
| virtual void | print (std::ostream &, BaseSemantics::Formatter &) const ROSE_OVERRIDE |
| Print a value to a stream using default format. More... | |
| virtual SgAsmExpression * | ast () |
| Property: Abstract syntax tree. | |
| virtual void | ast (SgAsmExpression *x) |
| Property: Abstract syntax tree. | |
| Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::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 | 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... | |
| virtual std::string | get_comment () const |
| Some subclasses support the ability to add comments to values. More... | |
| virtual void | set_comment (const std::string &) const |
| Some subclasses support the ability to add comments to values. 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 SValuePtr | instance () |
| Instantiate a prototypical SValue. More... | |
| static SValuePtr | instance_bottom (size_t nbits) |
| Instantiate a data-flow bottom value. More... | |
| static SValuePtr | instance_undefined (size_t nbits) |
| Instantiate an undefined value. More... | |
| static SValuePtr | instance_unspecified (size_t nbits) |
| Instantiate an unspecified value. More... | |
| static SValuePtr | instance_integer (size_t nbits, uint64_t value) |
| Instantiate an integer constant. More... | |
| static SValuePtr | promote (const BaseSemantics::SValuePtr &v) |
| Promote a base value to a static semantics value. More... | |
| Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::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, SgAsmRiscOperation::RiscOperator op) | |
| SValue (size_t nbits, uint64_t number) | |
| SValue (const SValue &other) | |
| Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue | |
| SValue (size_t nbits) | |
| SValue (const SValue &other) | |
Protected Attributes | |
| SgAsmExpression * | ast_ |
| Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue | |
| size_t | width |
Member Typedef Documentation
| using Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue::Super = BaseSemantics::SValue |
Base type.
Definition at line 77 of file StaticSemantics.h.
Shared-ownership pointer.
Definition at line 80 of file StaticSemantics.h.
Member Function Documentation
|
inlinestatic |
Instantiate a prototypical SValue.
This SValue will be used only for its virtual constructors and will never appear in an expression.
Definition at line 108 of file StaticSemantics.h.
Referenced by Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::RiscOperators::instance().
|
inlinestatic |
Instantiate a data-flow bottom value.
Definition at line 113 of file StaticSemantics.h.
Referenced by bottom_().
|
inlinestatic |
Instantiate an undefined value.
Undefined values end up being a SgAsmRiscOperation of type OP_undefined which has a single child which is an integer identification number. This allows two such nodes in the AST to be resolved to the same or different undefined value by virtue of their ID number.
Definition at line 122 of file StaticSemantics.h.
Referenced by undefined_().
|
inlinestatic |
Instantiate an unspecified value.
Unspecified values end up being a SgAsmRiscOperation of type OP_unspecified which has a single child which is an integer identification number. This allows two such nodes in the AST to be resolved to the same or different unspecified value by virtue of their ID number.
Definition at line 131 of file StaticSemantics.h.
Referenced by unspecified_().
|
inlinestatic |
Instantiate an integer constant.
Definition at line 136 of file StaticSemantics.h.
Referenced by boolean_(), and number_().
|
inlinevirtual |
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.
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 141 of file StaticSemantics.h.
References instance_bottom().
|
inlinevirtual |
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.
- See also
- unspecified_
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 144 of file StaticSemantics.h.
References instance_undefined().
|
inlinevirtual |
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.
- See also
- undefined_
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 147 of file StaticSemantics.h.
References instance_unspecified().
|
inlinevirtual |
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).
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 150 of file StaticSemantics.h.
References instance_integer().
|
inlinevirtual |
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::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 153 of file StaticSemantics.h.
References instance_integer().
|
inlinevirtual |
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.
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 156 of file StaticSemantics.h.
|
inlinevirtual |
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.
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 163 of file StaticSemantics.h.
|
inlinestatic |
Promote a base value to a static semantics value.
Definition at line 170 of file StaticSemantics.h.
References Sawyer::SharedPointer< T >::dynamicCast().
|
inlinevirtual |
Virtual API.
See mayEqual.
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 178 of file StaticSemantics.h.
|
inlinevirtual |
Virtual API.
See mustEqual.
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 183 of file StaticSemantics.h.
|
inlinevirtual |
Virtual API.
See nBits.
Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 188 of file StaticSemantics.h.
|
inlinevirtual |
Determines whether a value is a data-flow bottom.
Returns true if this value represents a bottom value for data-flow analysis. Any RiscOperation performed on an operand whose isBottom predicate returns true will itself return a bottom value. This includes operations like "xor x x" which would normally return zero.
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 192 of file StaticSemantics.h.
|
inlinevirtual |
Virtual API.
See isConcrete.
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 196 of file StaticSemantics.h.
|
inlinevirtual |
Virtual API.
See toUnsigned and toSigned.
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 200 of file StaticSemantics.h.
|
inlineoverridevirtual |
Hash this semantic value.
Hashes the value by appending it to the specified hasher.
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
Definition at line 204 of file StaticSemantics.h.
|
virtual |
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().
Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.
The documentation for this class was generated from the following file:
