ROSE  0.9.9.139
Classes | Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue Class Referenceabstract

Description

Base class for semantic values.

A semantic value represents a datum from the specimen being analyzed. The datum could be from memory, it could be something stored in a register, it could be the result of some computation, etc. The datum in the specimen has a datum type that might be only partially known; the datum value could, for instance, be 32-bits but unknown whether it is integer or floating point.

The various semantic domains will define SValue subclasses that are appropriate for that domain–a concrete domain will define an SValue that specimen data in a concrete form, an interval domain will define an SValue that represents specimen data in intervals, etc.

Semantics value objects are allocated on the heap and reference counted. The BaseSemantics::SValue is an abstract class that defines the interface. See the Rose::BinaryAnalysis::InstructionSemantics2 namespace for an overview of how the parts fit together.

Definition at line 538 of file BaseSemantics2.h.

#include <BaseSemantics2.h>

Inheritance diagram for Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue:
Inheritance graph
[legend]
Collaboration diagram for Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue:
Collaboration graph
[legend]

Classes

class  WithFormatter
 SValue with formatter. More...
 

Public Types

typedef SValuePtr Ptr
 Shared-ownership pointer for an SValue object. More...
 

Public Member Functions

virtual SValuePtr undefined_ (size_t nbits) const =0
 Create a new undefined semantic value. More...
 
virtual SValuePtr unspecified_ (size_t nbits) const =0
 Create a new unspecified semantic value. More...
 
virtual SValuePtr bottom_ (size_t nBits) const =0
 Data-flow bottom value. More...
 
virtual SValuePtr number_ (size_t nbits, uint64_t number) const =0
 Create a new concrete semantic value. More...
 
virtual SValuePtr boolean_ (bool value) const
 Create a new, Boolean value. More...
 
virtual SValuePtr copy (size_t new_width=0) const =0
 Create a new value from an existing value, changing the width if new_width is non-zero. More...
 
virtual Sawyer::Optional< SValuePtrcreateOptionalMerge (const SValuePtr &other, const MergerPtr &merger, SmtSolver *solver) const =0
 Possibly create a new value by merging two existing values. More...
 
SValuePtr createMerged (const SValuePtr &other, const MergerPtr &merger, SmtSolver *solver) const
 Create a new value by merging two existing values. More...
 
virtual bool isBottom () const =0
 Determines whether a value is a data-flow bottom. More...
 
virtual bool is_number () const =0
 Determines if the value is a concrete number. More...
 
virtual uint64_t get_number () const =0
 Return the concrete number for this value. More...
 
virtual bool may_equal (const SValuePtr &other, SmtSolver *solver=NULL) const =0
 Returns true if two values could be equal. More...
 
virtual bool must_equal (const SValuePtr &other, SmtSolver *solver=NULL) const =0
 Returns true if two values must be equal. More...
 
bool isTrue () const
 Returns true if concrete non-zero. More...
 
bool isFalse () const
 Returns true if concrete zero. More...
 
virtual size_t get_width () const
 Accessor for value width.
 
virtual void set_width (size_t nbits)
 Accessor for value width.
 
void print (std::ostream &stream) const
 Print a value to a stream using default format. More...
 
virtual void print (std::ostream &, Formatter &) const =0
 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...
 
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...
 
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 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 ()
 Width of the value in bits. More...
 
 SValue (size_t nbits)
 
 SValue (const SValue &other)
 

Protected Attributes

size_t width
 

Member Typedef Documentation

Shared-ownership pointer for an SValue object.

See Shared ownership.

Definition at line 563 of file BaseSemantics2.h.

Constructor & Destructor Documentation

Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::SValue ( )
inlineprotected

Width of the value in bits.

Typically (not always) a power of two.

Definition at line 557 of file BaseSemantics2.h.

Referenced by Rose::BinaryAnalysis::InstructionSemantics2::NullSemantics::SValue::copy(), Rose::BinaryAnalysis::InstructionSemantics2::ConcreteSemantics::SValue::copy(), Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue::copy(), Rose::BinaryAnalysis::InstructionSemantics2::MultiSemantics::SValue::copy(), Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::copy(), Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue::copy(), Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue::copy(), Rose::BinaryAnalysis::InstructionSemantics2::MultiSemantics::SValue::create_empty(), Rose::BinaryAnalysis::InstructionSemantics2::NullSemantics::SValue::instance(), Rose::BinaryAnalysis::InstructionSemantics2::ConcreteSemantics::SValue::instance(), Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue::instance(), Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue::instance(), Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue::instance(), Rose::BinaryAnalysis::InstructionSemantics2::MultiSemantics::SValue::instance(), Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::instance(), Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue::instance_bottom(), Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue::instance_bottom(), Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue::instance_copy(), Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue::instance_hull(), Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue::instance_integer(), Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue::instance_integer(), Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue::instance_integer(), Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue::instance_intervals(), Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue::instance_undefined(), Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue::instance_undefined(), Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue::instance_undefined(), Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue::instance_unspecified(), and Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue::instance_unspecified().

Member Function Documentation

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::undefined_ ( size_t  nbits) const
pure virtual
virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::unspecified_ ( size_t  nbits) const
pure virtual

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_

Implemented in Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::MultiSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::ConcreteSemantics::SValue, and Rose::BinaryAnalysis::InstructionSemantics2::NullSemantics::SValue.

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::bottom_ ( size_t  nBits) const
pure virtual
virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::number_ ( size_t  nbits,
uint64_t  number 
) const
pure virtual
virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::boolean_ ( bool  value) const
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 in Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue, and Rose::BinaryAnalysis::InstructionSemantics2::ConcreteSemantics::SValue.

Definition at line 613 of file BaseSemantics2.h.

References number_().

virtual SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::copy ( size_t  new_width = 0) const
pure virtual
virtual Sawyer::Optional<SValuePtr> Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::createOptionalMerge ( const SValuePtr other,
const MergerPtr merger,
SmtSolver solver 
) const
pure virtual

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.

Implemented in Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::StaticSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::IntervalSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::MultiSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::SourceAstSemantics::SValue, Rose::BinaryAnalysis::InstructionSemantics2::ConcreteSemantics::SValue, and Rose::BinaryAnalysis::InstructionSemantics2::NullSemantics::SValue.

Referenced by createMerged().

SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::createMerged ( const SValuePtr other,
const MergerPtr merger,
SmtSolver solver 
) const
inline

Create a new value by merging two existing values.

This is a convenience wrapper around createOptionalMerge. It always returns a newly constructed semantic value regardless of whether a merge was necessary. In order to determine if a merge was necessary one can compare the return value to this using must_equal, although doing so is more expensive than calling createOptionalMerge.

Definition at line 655 of file BaseSemantics2.h.

References copy(), and createOptionalMerge().

virtual bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::isBottom ( ) const
pure virtual
virtual bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::is_number ( ) const
pure virtual
virtual uint64_t Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::get_number ( ) const
pure virtual
virtual bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::may_equal ( const SValuePtr other,
SmtSolver solver = NULL 
) const
pure virtual
virtual bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::must_equal ( const SValuePtr other,
SmtSolver solver = NULL 
) const
pure virtual
bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::isTrue ( ) const
inline

Returns true if concrete non-zero.

This is not virtual since it can be implemented in terms of is_number and get_number.

Definition at line 699 of file BaseSemantics2.h.

References get_number(), and is_number().

bool Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::isFalse ( ) const
inline

Returns true if concrete zero.

This is not virtual since it can be implemented in terms of is_number and get_number.

Definition at line 705 of file BaseSemantics2.h.

References get_number(), and is_number().

void Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::print ( std::ostream &  stream) const
inline

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().

Definition at line 712 of file BaseSemantics2.h.

References print().

Referenced by print().

virtual void Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::print ( std::ostream &  ,
Formatter  
) const
pure virtual
WithFormatter Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::with_format ( Formatter fmt)
inline

Used for printing values with formatting.

The usual way to use this is:

SValuePtr val = ...;
Formatter fmt = ...;
std::cout <<"The value is: " <<(*val+fmt) <<"\n";

Definition at line 732 of file BaseSemantics2.h.

Referenced by operator+().

WithFormatter Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::operator+ ( Formatter fmt)
inline

Used for printing values with formatting.

The usual way to use this is:

SValuePtr val = ...;
Formatter fmt = ...;
std::cout <<"The value is: " <<(*val+fmt) <<"\n";

Definition at line 733 of file BaseSemantics2.h.

References with_format().

virtual std::string Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::get_comment ( ) const
inlinevirtual

Some subclasses support the ability to add comments to values.

We define no-op versions of these methods here because it makes things easier. The base class tries to be as small as possible by not storing comments at all. Comments should not affect any computation (comparisons, hash values, etc), and therefore are allowed to be modified even for const objects.

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

Definition at line 741 of file BaseSemantics2.h.

virtual void Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue::set_comment ( const std::string &  ) const
inlinevirtual

Some subclasses support the ability to add comments to values.

We define no-op versions of these methods here because it makes things easier. The base class tries to be as small as possible by not storing comments at all. Comments should not affect any computation (comparisons, hash values, etc), and therefore are allowed to be modified even for const objects.

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

Definition at line 742 of file BaseSemantics2.h.


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