ROSE  0.11.87.0
Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | Protected Member Functions | List of all members
Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue Class Reference

Description

Type of values manipulated by the PartialSymbolicSemantics domain.

A value is either known or unknown. Unknown values have a base name (unique ID number), offset, and sign.

Definition at line 70 of file PartialSymbolicSemantics.h.

#include <Rose/BinaryAnalysis/InstructionSemantics2/PartialSymbolicSemantics.h>

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

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 override
 Data-flow bottom value. More...
 
virtual BaseSemantics::SValuePtr undefined_ (size_t nbits) const override
 Create a new undefined semantic value. More...
 
virtual BaseSemantics::SValuePtr unspecified_ (size_t nbits) const override
 Create a new unspecified semantic value. More...
 
virtual BaseSemantics::SValuePtr number_ (size_t nbits, uint64_t value) const override
 Create a new concrete semantic value. More...
 
virtual BaseSemantics::SValuePtr copy (size_t new_width=0) const override
 Create a new value from an existing value, changing the width if new_width is non-zero. More...
 
virtual Sawyer::Optional< BaseSemantics::SValuePtrcreateOptionalMerge (const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr &, const SmtSolverPtr &) const override
 Possibly create a new value by merging two existing values. More...
 
virtual BaseSemantics::SValuePtr create (size_t nbits, uint64_t name, uint64_t offset, bool negate) const
 Virtual allocating constructor. More...
 
virtual void hash (Combinatorics::Hasher &) const override
 Hash this semantic value. More...
 
virtual void print (std::ostream &, BaseSemantics::Formatter &) const override
 Print a value to a stream using default format. More...
 
virtual bool isBottom () const override
 Determines whether a value is a data-flow bottom. More...
 
virtual void set_width (size_t nbits) override
 Virtual API. More...
 
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 bool is_number () const override
 Virtual API. More...
 
virtual uint64_t get_number () const override
 Virtual API. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue
virtual SValuePtr boolean_ (bool value) const
 Create a new, Boolean value. More...
 
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...
 
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 uint64_t nextName ()
 Returns the next available name. More...
 
static SValuePtr instance ()
 Instantiate a new prototypical value. More...
 
static SValuePtr instance (size_t nbits)
 Instantiate a new undefined value of specified width. More...
 
static SValuePtr instance (size_t nbits, uint64_t value)
 Instantiate a new concrete value. More...
 
static SValuePtr instance (size_t nbits, uint64_t name, uint64_t offset, bool negate)
 Insantiate a new value with all the necessary parts. More...
 
static SValuePtr promote (const BaseSemantics::SValuePtr &v)
 Promote a base value to a PartialSymbolicSemantics 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)
 

Public Attributes

uint64_t name
 Zero for constants; non-zero ID number for everything else. More...
 
uint64_t offset
 The constant (if name==0) or an offset w.r.t. More...
 
bool negate
 Switch between name+offset and (-name)+offset; should be false for constants. More...
 

Protected Member Functions

 SValue (size_t nbits)
 
 SValue (size_t nbits, uint64_t number)
 
 SValue (size_t nbits, uint64_t name, uint64_t offset, bool negate)
 
- 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::BaseSemantics::SValue
size_t width
 

Member Typedef Documentation

Base type.

Definition at line 73 of file PartialSymbolicSemantics.h.

Shared-ownership pointer.

Definition at line 76 of file PartialSymbolicSemantics.h.

Member Function Documentation

static uint64_t Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::nextName ( )
static

Returns the next available name.

Returns the next available name and increments it.

Thread safety: This function is thread safe.

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::instance ( )
inlinestatic

Instantiate a new prototypical value.

Prototypical values are only used for their virtual constructors.

Definition at line 117 of file PartialSymbolicSemantics.h.

Referenced by bottom_(), create(), number_(), undefined_(), and unspecified_().

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::instance ( size_t  nbits)
inlinestatic

Instantiate a new undefined value of specified width.

Definition at line 122 of file PartialSymbolicSemantics.h.

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::instance ( size_t  nbits,
uint64_t  value 
)
inlinestatic

Instantiate a new concrete value.

Definition at line 127 of file PartialSymbolicSemantics.h.

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::instance ( size_t  nbits,
uint64_t  name,
uint64_t  offset,
bool  negate 
)
inlinestatic

Insantiate a new value with all the necessary parts.

Definition at line 132 of file PartialSymbolicSemantics.h.

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::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.

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.

Definition at line 139 of file PartialSymbolicSemantics.h.

References instance().

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::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_

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.

Definition at line 142 of file PartialSymbolicSemantics.h.

References instance().

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::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_

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.

Definition at line 145 of file PartialSymbolicSemantics.h.

References instance().

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::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).

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.

Definition at line 149 of file PartialSymbolicSemantics.h.

References instance().

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::copy ( size_t  new_width = 0) const
inlineoverridevirtual

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 153 of file PartialSymbolicSemantics.h.

virtual Sawyer::Optional<BaseSemantics::SValuePtr> Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::createOptionalMerge ( const BaseSemantics::SValuePtr other,
const 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.

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.

virtual BaseSemantics::SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::create ( size_t  nbits,
uint64_t  name,
uint64_t  offset,
bool  negate 
) const
inlinevirtual

Virtual allocating constructor.

Creates a new semantic value with full control over all aspects of the value.

Definition at line 165 of file PartialSymbolicSemantics.h.

References instance().

static SValuePtr Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::promote ( const BaseSemantics::SValuePtr v)
inlinestatic

Promote a base value to a PartialSymbolicSemantics value.

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

Definition at line 174 of file PartialSymbolicSemantics.h.

References Sawyer::SharedPointer< T >::dynamicCast().

virtual void Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::hash ( Combinatorics::Hasher ) const
overridevirtual

Hash this semantic value.

Hashes the value by appending it to the specified hasher.

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.

virtual void Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::print ( std::ostream &  ,
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().

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.

virtual bool Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::isBottom ( ) const
inlineoverridevirtual

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 186 of file PartialSymbolicSemantics.h.

virtual void Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::set_width ( size_t  nbits)
inlineoverridevirtual
virtual bool Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::may_equal ( const BaseSemantics::SValuePtr other,
const SmtSolverPtr solver = SmtSolverPtr() 
) const
overridevirtual
virtual bool Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::must_equal ( const BaseSemantics::SValuePtr other,
const SmtSolverPtr solver = SmtSolverPtr() 
) const
overridevirtual
virtual bool Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::is_number ( ) const
inlineoverridevirtual

Virtual API.

See isConcrete.

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.

Definition at line 215 of file PartialSymbolicSemantics.h.

References name.

Referenced by get_number().

virtual uint64_t Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::get_number ( ) const
inlineoverridevirtual

Virtual API.

See toUnsigned and toSigned.

Implements Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::SValue.

Definition at line 220 of file PartialSymbolicSemantics.h.

References is_number(), and offset.

Member Data Documentation

uint64_t Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::name

Zero for constants; non-zero ID number for everything else.

Definition at line 79 of file PartialSymbolicSemantics.h.

Referenced by is_number().

uint64_t Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::offset

The constant (if name==0) or an offset w.r.t.

an unknown (named) base value.

Definition at line 80 of file PartialSymbolicSemantics.h.

Referenced by get_number().

bool Rose::BinaryAnalysis::InstructionSemantics2::PartialSymbolicSemantics::SValue::negate

Switch between name+offset and (-name)+offset; should be false for constants.

Definition at line 81 of file PartialSymbolicSemantics.h.


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