klee
Public Member Functions | Private Attributes | List of all members
ValueRange Class Reference

Public Member Functions

 ValueRange () noexcept=default
 
 ValueRange (const ref< ConstantExpr > &ce)
 
 ValueRange (std::uint64_t value) noexcept
 
 ValueRange (std::uint64_t _min, std::uint64_t _max) noexcept
 
 ValueRange (const ValueRange &other) noexcept=default
 
ValueRange & operator= (const ValueRange &other) noexcept=default
 
 ValueRange (ValueRange &&other) noexcept=default
 
ValueRange & operator= (ValueRange &&other) noexcept=default
 
void print (llvm::raw_ostream &os) const
 
bool isEmpty () const noexcept
 
bool contains (std::uint64_t value) const
 
bool intersects (const ValueRange &b) const
 
bool isFullRange (unsigned bits) const noexcept
 
ValueRange set_intersection (const ValueRange &b) const
 
ValueRange set_union (const ValueRange &b) const
 
ValueRange set_difference (const ValueRange &b) const
 
ValueRange binaryAnd (const ValueRange &b) const
 
ValueRange binaryAnd (std::uint64_t b) const
 
ValueRange binaryOr (ValueRange b) const
 
ValueRange binaryOr (std::uint64_t b) const
 
ValueRange binaryXor (ValueRange b) const
 
ValueRange binaryShiftLeft (unsigned bits) const
 
ValueRange binaryShiftRight (unsigned bits) const
 
ValueRange concat (const ValueRange &b, unsigned bits) const
 
ValueRange extract (std::uint64_t lowBit, std::uint64_t maxBit) const
 
ValueRange add (const ValueRange &b, unsigned width) const
 
ValueRange sub (const ValueRange &b, unsigned width) const
 
ValueRange mul (const ValueRange &b, unsigned width) const
 
ValueRange udiv (const ValueRange &b, unsigned width) const
 
ValueRange sdiv (const ValueRange &b, unsigned width) const
 
ValueRange urem (const ValueRange &b, unsigned width) const
 
ValueRange srem (const ValueRange &b, unsigned width) const
 
bool isFixed () const noexcept
 
bool operator== (const ValueRange &b) const noexcept
 
bool operator!= (const ValueRange &b) const noexcept
 
bool mustEqual (const std::uint64_t b) const noexcept
 
bool mayEqual (const std::uint64_t b) const noexcept
 
bool mustEqual (const ValueRange &b) const noexcept
 
bool mayEqual (const ValueRange &b) const
 
std::uint64_t min () const noexcept
 
std::uint64_t max () const noexcept
 
std::int64_t minSigned (unsigned bits) const
 
std::int64_t maxSigned (unsigned bits) const
 

Private Attributes

std::uint64_t m_min = 1
 
std::uint64_t m_max = 0
 

Detailed Description

Definition at line 98 of file FastCexSolver.cpp.

Constructor & Destructor Documentation

◆ ValueRange() [1/6]

ValueRange::ValueRange ( )
defaultnoexcept

Referenced by add(), binaryAnd(), binaryOr(), binaryShiftLeft(), binaryShiftRight(), binaryXor(), contains(), mul(), sdiv(), set_difference(), set_intersection(), set_union(), srem(), sub(), udiv(), and urem().

Here is the caller graph for this function:

◆ ValueRange() [2/6]

ValueRange::ValueRange ( const ref< ConstantExpr > &  ce)
inline

Definition at line 104 of file FastCexSolver.cpp.

References m_max, and m_min.

◆ ValueRange() [3/6]

ValueRange::ValueRange ( std::uint64_t  value)
inlineexplicitnoexcept

Definition at line 108 of file FastCexSolver.cpp.

◆ ValueRange() [4/6]

ValueRange::ValueRange ( std::uint64_t  _min,
std::uint64_t  _max 
)
inlinenoexcept

Definition at line 110 of file FastCexSolver.cpp.

◆ ValueRange() [5/6]

ValueRange::ValueRange ( const ValueRange &  other)
defaultnoexcept

◆ ValueRange() [6/6]

ValueRange::ValueRange ( ValueRange &&  other)
defaultnoexcept

Member Function Documentation

◆ add()

ValueRange ValueRange::add ( const ValueRange &  b,
unsigned  width 
) const
inline

Definition at line 209 of file FastCexSolver.cpp.

References klee::bits32::maxValueOfNBits(), and ValueRange().

Here is the call graph for this function:

◆ binaryAnd() [1/2]

ValueRange ValueRange::binaryAnd ( const ValueRange &  b) const
inline

Definition at line 159 of file FastCexSolver.cpp.

References isEmpty(), isFixed(), m_max, m_min, maxAND(), minAND(), and ValueRange().

Referenced by binaryAnd(), extract(), and CexData::propogatePossibleValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ binaryAnd() [2/2]

ValueRange ValueRange::binaryAnd ( std::uint64_t  b) const
inline

Definition at line 169 of file FastCexSolver.cpp.

References binaryAnd(), and ValueRange().

Here is the call graph for this function:

◆ binaryOr() [1/2]

ValueRange ValueRange::binaryOr ( std::uint64_t  b) const
inline

Definition at line 182 of file FastCexSolver.cpp.

References binaryOr(), and ValueRange().

Referenced by binaryOr().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ binaryOr() [2/2]

ValueRange ValueRange::binaryOr ( ValueRange  b) const
inline

Definition at line 172 of file FastCexSolver.cpp.

References isEmpty(), isFixed(), m_max, m_min, maxOR(), minOR(), and ValueRange().

Referenced by concat().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ binaryShiftLeft()

ValueRange ValueRange::binaryShiftLeft ( unsigned  bits) const
inline

Definition at line 194 of file FastCexSolver.cpp.

References m_max, m_min, and ValueRange().

Referenced by concat().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ binaryShiftRight()

ValueRange ValueRange::binaryShiftRight ( unsigned  bits) const
inline

Definition at line 197 of file FastCexSolver.cpp.

References m_max, m_min, and ValueRange().

Referenced by extract().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ binaryXor()

ValueRange ValueRange::binaryXor ( ValueRange  b) const
inline

Definition at line 183 of file FastCexSolver.cpp.

References isFixed(), klee::bits32::isPowerOfTwo(), m_max, m_min, ValueRange(), and klee::bits32::withoutRightmostBit().

Here is the call graph for this function:

◆ concat()

ValueRange ValueRange::concat ( const ValueRange &  b,
unsigned  bits 
) const
inline

Definition at line 201 of file FastCexSolver.cpp.

References binaryOr(), and binaryShiftLeft().

Here is the call graph for this function:

◆ contains()

bool ValueRange::contains ( std::uint64_t  value) const
inline

Definition at line 126 of file FastCexSolver.cpp.

References intersects(), and ValueRange().

Here is the call graph for this function:

◆ extract()

ValueRange ValueRange::extract ( std::uint64_t  lowBit,
std::uint64_t  maxBit 
) const
inline

Definition at line 204 of file FastCexSolver.cpp.

References binaryAnd(), binaryShiftRight(), and klee::bits32::maxValueOfNBits().

Referenced by CexData::propogatePossibleValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ intersects()

bool ValueRange::intersects ( const ValueRange &  b) const
inline

Definition at line 129 of file FastCexSolver.cpp.

References isEmpty(), and set_intersection().

Referenced by contains(), and mayEqual().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isEmpty()

bool ValueRange::isEmpty ( ) const
inlinenoexcept

Definition at line 125 of file FastCexSolver.cpp.

References m_max, and m_min.

Referenced by binaryAnd(), binaryOr(), intersects(), max(), min(), CexData::propogatePossibleValues(), and set_difference().

Here is the caller graph for this function:

◆ isFixed()

bool ValueRange::isFixed ( ) const
inlinenoexcept

Definition at line 233 of file FastCexSolver.cpp.

References m_max, and m_min.

Referenced by binaryAnd(), binaryOr(), binaryXor(), CexRangeEvaluator::getInitialReadRange(), CexExactEvaluator::getInitialValue(), mustEqual(), print(), CexData::propogateExactValues(), and CexData::propogatePossibleValues().

Here is the caller graph for this function:

◆ isFullRange()

bool ValueRange::isFullRange ( unsigned  bits) const
inlinenoexcept

Definition at line 133 of file FastCexSolver.cpp.

References m_max, m_min, and klee::bits32::maxValueOfNBits().

Here is the call graph for this function:

◆ max()

std::uint64_t ValueRange::max ( ) const
inlinenoexcept

Definition at line 257 of file FastCexSolver.cpp.

References isEmpty(), and m_max.

Referenced by CexObjectData::getPossibleValue(), CexData::propogateExactValues(), and CexData::propogatePossibleValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ maxSigned()

std::int64_t ValueRange::maxSigned ( unsigned  bits) const
inline

Definition at line 278 of file FastCexSolver.cpp.

References m_max, m_min, and klee::ints::sext().

Here is the call graph for this function:

◆ mayEqual() [1/2]

bool ValueRange::mayEqual ( const std::uint64_t  b) const
inlinenoexcept

Definition at line 243 of file FastCexSolver.cpp.

Referenced by CexData::propogateExactValues().

Here is the caller graph for this function:

◆ mayEqual() [2/2]

bool ValueRange::mayEqual ( const ValueRange &  b) const
inline

Definition at line 250 of file FastCexSolver.cpp.

References intersects().

Here is the call graph for this function:

◆ min()

std::uint64_t ValueRange::min ( ) const
inlinenoexcept

Definition at line 252 of file FastCexSolver.cpp.

References isEmpty(), and m_min.

Referenced by CexRangeEvaluator::getInitialReadRange(), CexExactEvaluator::getInitialValue(), CexObjectData::getPossibleValue(), CexData::propogateExactValues(), and CexData::propogatePossibleValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ minSigned()

std::int64_t ValueRange::minSigned ( unsigned  bits) const
inline

Definition at line 262 of file FastCexSolver.cpp.

References m_max, m_min, and klee::ints::sext().

Here is the call graph for this function:

◆ mul()

ValueRange ValueRange::mul ( const ValueRange &  b,
unsigned  width 
) const
inline

Definition at line 215 of file FastCexSolver.cpp.

References klee::bits32::maxValueOfNBits(), and ValueRange().

Here is the call graph for this function:

◆ mustEqual() [1/2]

bool ValueRange::mustEqual ( const std::uint64_t  b) const
inlinenoexcept

Definition at line 240 of file FastCexSolver.cpp.

References m_max, and m_min.

Referenced by CexData::propogateExactValues(), and CexData::propogatePossibleValues().

Here is the caller graph for this function:

◆ mustEqual() [2/2]

bool ValueRange::mustEqual ( const ValueRange &  b) const
inlinenoexcept

Definition at line 247 of file FastCexSolver.cpp.

References isFixed(), and m_min.

Here is the call graph for this function:

◆ operator!=()

bool ValueRange::operator!= ( const ValueRange &  b) const
inlinenoexcept

Definition at line 238 of file FastCexSolver.cpp.

◆ operator=() [1/2]

ValueRange & ValueRange::operator= ( const ValueRange &  other)
defaultnoexcept

◆ operator=() [2/2]

ValueRange & ValueRange::operator= ( ValueRange &&  other)
defaultnoexcept

◆ operator==()

bool ValueRange::operator== ( const ValueRange &  b) const
inlinenoexcept

Definition at line 235 of file FastCexSolver.cpp.

References m_max, and m_min.

◆ print()

void ValueRange::print ( llvm::raw_ostream &  os) const
inline

Definition at line 117 of file FastCexSolver.cpp.

References isFixed(), m_max, and m_min.

Referenced by operator<<().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ sdiv()

ValueRange ValueRange::sdiv ( const ValueRange &  b,
unsigned  width 
) const
inline

Definition at line 221 of file FastCexSolver.cpp.

References klee::bits32::maxValueOfNBits(), and ValueRange().

Here is the call graph for this function:

◆ set_difference()

ValueRange ValueRange::set_difference ( const ValueRange &  b) const
inline

Definition at line 143 of file FastCexSolver.cpp.

References isEmpty(), m_max, m_min, and ValueRange().

Referenced by CexData::propogatePossibleValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ set_intersection()

ValueRange ValueRange::set_intersection ( const ValueRange &  b) const
inline

Definition at line 137 of file FastCexSolver.cpp.

References m_max, m_min, and ValueRange().

Referenced by intersects(), and CexData::propogatePossibleValues().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ set_union()

ValueRange ValueRange::set_union ( const ValueRange &  b) const
inline

Definition at line 140 of file FastCexSolver.cpp.

References m_max, m_min, and ValueRange().

Here is the call graph for this function:

◆ srem()

ValueRange ValueRange::srem ( const ValueRange &  b,
unsigned  width 
) const
inline

Definition at line 227 of file FastCexSolver.cpp.

References klee::bits32::maxValueOfNBits(), and ValueRange().

Here is the call graph for this function:

◆ sub()

ValueRange ValueRange::sub ( const ValueRange &  b,
unsigned  width 
) const
inline

Definition at line 212 of file FastCexSolver.cpp.

References klee::bits32::maxValueOfNBits(), and ValueRange().

Here is the call graph for this function:

◆ udiv()

ValueRange ValueRange::udiv ( const ValueRange &  b,
unsigned  width 
) const
inline

Definition at line 218 of file FastCexSolver.cpp.

References klee::bits32::maxValueOfNBits(), and ValueRange().

Here is the call graph for this function:

◆ urem()

ValueRange ValueRange::urem ( const ValueRange &  b,
unsigned  width 
) const
inline

Definition at line 224 of file FastCexSolver.cpp.

References klee::bits32::maxValueOfNBits(), and ValueRange().

Here is the call graph for this function:

Member Data Documentation

◆ m_max

std::uint64_t ValueRange::m_max = 0
private

Definition at line 100 of file FastCexSolver.cpp.

Referenced by binaryAnd(), binaryOr(), binaryShiftLeft(), binaryShiftRight(), binaryXor(), isEmpty(), isFixed(), isFullRange(), max(), maxSigned(), minSigned(), mustEqual(), operator==(), print(), set_difference(), set_intersection(), set_union(), and ValueRange().

◆ m_min

std::uint64_t ValueRange::m_min = 1
private

Definition at line 100 of file FastCexSolver.cpp.

Referenced by binaryAnd(), binaryOr(), binaryShiftLeft(), binaryShiftRight(), binaryXor(), isEmpty(), isFixed(), isFullRange(), maxSigned(), min(), minSigned(), mustEqual(), operator==(), print(), set_difference(), set_intersection(), set_union(), and ValueRange().

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