ROSE  0.11.51.0
Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | List of all members
Rose::BinaryAnalysis::ModelChecker::P2Model::SValue Class Reference

Description

Symbolic values with memory regions.

Values are symbolic, and some values also have memory region information.

Definition at line 105 of file P2Model.h.

#include <P2Model.h>

Inheritance diagram for Rose::BinaryAnalysis::ModelChecker::P2Model::SValue:
Inheritance graph
[legend]
Collaboration diagram for Rose::BinaryAnalysis::ModelChecker::P2Model::SValue:
Collaboration graph
[legend]

Public Types

using Super = InstructionSemantics2::SymbolicSemantics::SValue
 Base class. More...
 
using Ptr = SValuePtr
 Shared-ownership pointer. More...
 
- Public Types inherited from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue
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 InstructionSemantics2::BaseSemantics::SValuePtr bottom_ (size_t nBits) const override
 Data-flow bottom value. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr undefined_ (size_t nBits) const override
 Create a new undefined semantic value. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr unspecified_ (size_t nBits) const override
 Create a new unspecified semantic value. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr number_ (size_t nBits, uint64_t value) const override
 Create a new concrete semantic value. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr boolean_ (bool value) const override
 Create a new, Boolean value. More...
 
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. More...
 
virtual Sawyer::Optional< InstructionSemantics2::BaseSemantics::SValuePtrcreateOptionalMerge (const InstructionSemantics2::BaseSemantics::SValuePtr &other, const InstructionSemantics2::BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
 Possibly create a new value by merging two existing values. More...
 
virtual void print (std::ostream &, InstructionSemantics2::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::InstructionSemantics2::SymbolicSemantics::SValue
virtual bool isBottom () const ROSE_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 ExprPtrget_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::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...
 
- Public Member Functions inherited from Sawyer::SharedObject
 SharedObject ()
 Default constructor. More...
 
 SharedObject (const SharedObject &)
 Copy constructor. More...
 
virtual ~SharedObject ()
 Virtual destructor. More...
 
SharedObjectoperator= (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 InstructionSemantics2::BaseSemantics::SValuePtr &v)
 Promote a base value to a MemoryRegionSemantics value. More...
 
- Static Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::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::InstructionSemantics2::BaseSemantics::SValue
static SValuePtr promote (const SValuePtr &x)
 
- Static Public Member Functions inherited from Sawyer::SmallObject
static SynchronizedPoolAllocatorpoolAllocator ()
 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::InstructionSemantics2::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 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 is_number () const ROSE_OVERRIDE
 Virtual API. More...
 
virtual uint64_t get_number () const ROSE_OVERRIDE
 Virtual API. More...
 
virtual std::string get_comment () const ROSE_OVERRIDE
 Some subclasses support the ability to add comments to values. More...
 
virtual void set_comment (const std::string &) const ROSE_OVERRIDE
 Some subclasses support the ability to add comments to values. More...
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue
 SValue (size_t nbits)
 
 SValue (const SValue &other)
 

Additional Inherited Members

- Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue
ExprPtr expr
 The symbolic expression for this value. More...
 
InsnSet defs
 Instructions defining this value. More...
 
- Protected Attributes inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue
size_t width
 

Member Typedef Documentation

Base class.

Definition at line 108 of file P2Model.h.

Shared-ownership pointer.

Definition at line 111 of file P2Model.h.

Member Function Documentation

static Ptr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::instance ( )
static

Instantiate a new prototypical value.

Prototypical values are only used for their virtual constructors.

static Ptr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::instanceBottom ( size_t  nBits)
static

Instantiate a new data-flow bottom value.

Referenced by bottom_().

static Ptr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::instanceUndefined ( size_t  nBits)
static

Instantiate a new undefined value.

Referenced by undefined_().

static Ptr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::instanceUnspecified ( size_t  nBits)
static

Instantiate a new unspecified value.

Referenced by unspecified_().

static Ptr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::instanceInteger ( size_t  nBits,
uint64_t  value 
)
static

Instantiate a new concrete value.

Referenced by boolean_(), and number_().

static Ptr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::instanceSymbolic ( const SymbolicExpr::Ptr value)
static

Instantiate a new symbolic value.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::bottom_ ( size_t  nBits) const
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::InstructionSemantics2::SymbolicSemantics::SValue.

Definition at line 159 of file P2Model.h.

References instanceBottom().

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::undefined_ ( size_t  nbits) const
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.

See also
unspecified_

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue.

Definition at line 163 of file P2Model.h.

References instanceUndefined().

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::unspecified_ ( size_t  nbits) const
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.

See also
undefined_

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue.

Definition at line 167 of file P2Model.h.

References instanceUnspecified().

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::number_ ( size_t  nbits,
uint64_t  number 
) const
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::InstructionSemantics2::SymbolicSemantics::SValue.

Definition at line 171 of file P2Model.h.

References instanceInteger().

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::boolean_ ( bool  value) const
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::InstructionSemantics2::SymbolicSemantics::SValue.

Definition at line 175 of file P2Model.h.

References instanceInteger().

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::copy ( size_t  new_width = 0) const
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::InstructionSemantics2::SymbolicSemantics::SValue.

virtual Sawyer::Optional<InstructionSemantics2::BaseSemantics::SValuePtr> Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::createOptionalMerge ( const InstructionSemantics2::BaseSemantics::SValuePtr other,
const InstructionSemantics2::BaseSemantics::MergerPtr merger,
const SmtSolverPtr solver 
) const
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 (SValuePtr merged = v1->createOptionalMerge(v2).orDefault()) {
std::cout <<"v1 and v2 were merged to " <<*merged <<"\n";
} else {
std::cout <<"no merge is necessary\n";
}
or
@code
SValuePtr merge;
if (v1->createOptionalMerge(v2).assignTo(merged)) {
std::cout <<"v1 and v2 were merged to " <<*merged <<"\n";
} else {
std::cout <<"v1 and v2 are equal in some sense (no merge necessary)\n";
}

If you always want a copy regardless of whether the merge is necessary, then use the createMerged convenience function instead.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue.

static Ptr Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::promote ( const InstructionSemantics2::BaseSemantics::SValuePtr v)
inlinestatic

Promote a base value to a MemoryRegionSemantics value.

The value v must have a MemoryRegionSemantics::SValue dynamic type.

Definition at line 190 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.

virtual void Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::print ( std::ostream &  ,
InstructionSemantics2::BaseSemantics::Formatter  
) const
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::InstructionSemantics2::SymbolicSemantics::SValue.

virtual void Rose::BinaryAnalysis::ModelChecker::P2Model::SValue::hash ( Combinatorics::Hasher ) const
overridevirtual

Hash this semantic value.

Hashes the value by appending it to the specified hasher.

Reimplemented from Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue.


The documentation for this class was generated from the following file: