SVF::IntervalValue Class Reference

#include <IntervalValue.h>

Public Member Functions
bool	isTop () const
bool	isBottom () const
	IntervalValue ()
	Create default IntervalValue. More...
	IntervalValue (s64_t n)
	Create the IntervalValue [n, n]. More...
	IntervalValue (s32_t n)
	IntervalValue (u32_t n)
	IntervalValue (double n)
	IntervalValue (BoundedInt n)
	IntervalValue (BoundedInt lb, BoundedInt ub)
	Create the IntervalValue [lb, ub]. More...
	IntervalValue (s64_t lb, s64_t ub)
	IntervalValue (double lb, double ub)
	IntervalValue (float lb, float ub)
	IntervalValue (s32_t lb, s32_t ub)
	IntervalValue (u32_t lb, u32_t ub)
	IntervalValue (u64_t lb, u64_t ub)
	IntervalValue (const IntervalValue &)=default
	Copy constructor. More...
	IntervalValue (IntervalValue &&)=default
	Move constructor. More...
IntervalValue &	operator= (const IntervalValue &a)=default
	Copy assignment operator. More...
IntervalValue &	operator= (IntervalValue &&)=default
	Move assignment operator. More...
IntervalValue	operator== (const IntervalValue &other) const
	Equality comparison. More...
IntervalValue	operator!= (const IntervalValue &other) const
	Equality comparison. More...
	~IntervalValue ()=default
	Destructor. More...
const BoundedInt &	lb () const
	Return the lower bound. More...
const BoundedInt &	ub () const
	Return the upper bound. More...
bool	is_zero () const
	Return true if the IntervalValue is [0, 0]. More...
bool	is_infinite () const
	Return true if the IntervalValue is infinite IntervalValue. More...
bool	is_int () const
bool	is_real () const
s64_t	getNumeral () const
	Return. More...
s64_t	getIntNumeral () const
double	getRealNumeral () const
bool	is_numeral () const
	Return true if the IntervalValue is a number [num, num]. More...
void	set_to_bottom ()
	Set current IntervalValue as bottom. More...
void	set_to_top ()
	Set current IntervalValue as top. More...
bool	containedWithin (const IntervalValue &other) const
bool	contain (const IntervalValue &other) const
bool	leq (const IntervalValue &other) const
bool	geq (const IntervalValue &other) const
bool	equals (const IntervalValue &other) const
	Equality comparison. More...
void	join_with (const IntervalValue &other)
	Current IntervalValue joins with another IntervalValue. More...
void	widen_with (const IntervalValue &other)
	Current IntervalValue widen with another IntervalValue. More...
void	narrow_with (const IntervalValue &other)
	Current IntervalValue narrow with another IntervalValue. More...
void	meet_with (const IntervalValue &other)
	Return a intersected IntervalValue. More...
bool	contains (int n) const
	Return true if the IntervalValue contains n. More...
void	dump (std::ostream &o) const
const std::string	toString () const

Static Public Member Functions
static BoundedInt	minus_infinity ()
	Get minus infinity -inf. More...
static BoundedInt	plus_infinity ()
	Get plus infinity +inf. More...
static bool	is_infinite (const BoundedInt &e)
static IntervalValue	top ()
	Create the IntervalValue [-inf, +inf]. More...
static IntervalValue	bottom ()
	Create the bottom IntervalValue [+inf, -inf]. More...

Private Member Functions
void	setValue (const BoundedInt &lb, const BoundedInt &ub)
	Set the lower bound. More...

Static Private Member Functions
static IntervalValue	create (const BoundedInt &lb, const BoundedInt &ub)

Private Attributes
BoundedInt	_lb
BoundedInt	_ub

Friends
IntervalValue	operator+ (const IntervalValue &lhs, const IntervalValue &rhs)
	Add IntervalValues. More...
IntervalValue	operator- (const IntervalValue &lhs, const IntervalValue &rhs)
	Subtract IntervalValues. More...
IntervalValue	operator* (const IntervalValue &lhs, const IntervalValue &rhs)
	Multiply IntervalValues. More...
IntervalValue	operator/ (const IntervalValue &lhs, const IntervalValue &rhs)
	Divide IntervalValues. More...
IntervalValue	operator<< (const IntervalValue &lhs, const IntervalValue &rhs)
	Left binary shift of IntervalValues. More...
IntervalValue	operator>> (const IntervalValue &lhs, const IntervalValue &rhs)
	Left binary shift of IntervalValues. More...
IntervalValue	operator& (const IntervalValue &lhs, const IntervalValue &rhs)
	Bitwise AND of IntervalValues. More...
IntervalValue	operator| (const IntervalValue &lhs, const IntervalValue &rhs)
	Bitwise OR of IntervalValues. More...
IntervalValue	operator^ (const IntervalValue &lhs, const IntervalValue &rhs)
	Bitwise XOR of IntervalValues. More...

Detailed Description

IntervalValue abstract value

Implemented as a pair of bounds

Definition at line 45 of file IntervalValue.h.

Constructor & Destructor Documentation

IntervalValue() [1/15]

SVF::IntervalValue::IntervalValue ( )

inlineexplicit

Create default IntervalValue.

Definition at line 106 of file IntervalValue.h.

: _lb(minus_infinity()), _ub(plus_infinity()) {}

IntervalValue() [2/15]

SVF::IntervalValue::IntervalValue ( s64_t  n )

inlineexplicit

Create the IntervalValue [n, n].

Definition at line 109 of file IntervalValue.h.

: _lb(n), _ub(n) {}

IntervalValue() [3/15]

SVF::IntervalValue::IntervalValue ( s32_t  n )

inlineexplicit

Definition at line 111 of file IntervalValue.h.

: IntervalValue((s64_t) n) {}

IntervalValue() [4/15]

SVF::IntervalValue::IntervalValue ( u32_t  n )

inlineexplicit

Definition at line 113 of file IntervalValue.h.

: IntervalValue((s64_t) n) {}

IntervalValue() [5/15]

SVF::IntervalValue::IntervalValue ( double  n )

inlineexplicit

Definition at line 115 of file IntervalValue.h.

: _lb(n), _ub(n) {}

IntervalValue() [6/15]

SVF::IntervalValue::IntervalValue ( BoundedInt  n )

inlineexplicit

Definition at line 117 of file IntervalValue.h.

: IntervalValue(n, n) {}

IntervalValue() [7/15]

SVF::IntervalValue::IntervalValue ( BoundedInt  lb, BoundedInt  ub  )

inlineexplicit

Create the IntervalValue [lb, ub].

Definition at line 120 of file IntervalValue.h.

                                                         : _lb(std::move(lb)), _ub(std::move(ub))
    {
        assert((isBottom() || _lb.leq(_ub)) && "lower bound should be less than or equal to upper bound");
    }

IntervalValue() [8/15]

SVF::IntervalValue::IntervalValue ( s64_t  lb, s64_t  ub  )

inlineexplicit

Definition at line 125 of file IntervalValue.h.

: IntervalValue(BoundedInt(lb), BoundedInt(ub)) {}

IntervalValue() [9/15]

SVF::IntervalValue::IntervalValue ( double  lb, double  ub  )

inlineexplicit

Definition at line 127 of file IntervalValue.h.

: IntervalValue(BoundedInt(lb), BoundedInt(ub)) {}

IntervalValue() [10/15]

SVF::IntervalValue::IntervalValue ( float  lb, float  ub  )

inlineexplicit

Definition at line 129 of file IntervalValue.h.

: IntervalValue(BoundedInt(lb), BoundedInt(ub)) {}

IntervalValue() [11/15]

SVF::IntervalValue::IntervalValue ( s32_t  lb, s32_t  ub  )

inlineexplicit

Definition at line 131 of file IntervalValue.h.

: IntervalValue((s64_t) lb, (s64_t) ub) {}

IntervalValue() [12/15]

SVF::IntervalValue::IntervalValue ( u32_t  lb, u32_t  ub  )

inlineexplicit

Definition at line 133 of file IntervalValue.h.

: IntervalValue((s64_t) lb, (s64_t) ub) {}

IntervalValue() [13/15]

SVF::IntervalValue::IntervalValue ( u64_t  lb, u64_t  ub  )

inlineexplicit

Definition at line 135 of file IntervalValue.h.

: IntervalValue((s64_t) lb, (s64_t) ub) {}

IntervalValue() [14/15]

SVF::IntervalValue::IntervalValue ( const IntervalValue &  )

default

Copy constructor.

IntervalValue() [15/15]

SVF::IntervalValue::IntervalValue ( IntervalValue &&  )

default

Move constructor.

~IntervalValue()

SVF::IntervalValue::~IntervalValue ( )

default

Destructor.

Member Function Documentation

bottom()

static IntervalValue SVF::IntervalValue::bottom ( )

inlinestatic

Create the bottom IntervalValue [+inf, -inf].

Definition at line 100 of file IntervalValue.h.

    {
        return IntervalValue(plus_infinity(), minus_infinity());
    }

contain()

bool SVF::IntervalValue::contain ( const IntervalValue &  other ) const

inline

Determines if the current IntervalValue fully contains another IntervalValue. Example: this: [1, 4], other: [2, 3] -> returns true Note: If the current interval is 'bottom', it is considered to contain any interval. If the other interval is 'bottom', it cannot be contained by any interval.

Definition at line 321 of file IntervalValue.h.

    {
        if (this->isBottom())
        {
            return true;
        }
        else if (other.isBottom())
        {
            return false;
        }
        else
        {
            return other._lb.geq(this->_lb) && this->_ub.geq(other._ub);
        }
    }

containedWithin()

bool SVF::IntervalValue::containedWithin ( const IntervalValue &  other ) const

inline

Determines if the current IntervalValue is fully contained within another IntervalValue. Example: this: [2, 3], other: [1, 4] -> returns true Note: If the current interval is 'bottom', it is considered contained within any interval. If the other interval is 'bottom', it cannot contain any interval.

Definition at line 300 of file IntervalValue.h.

    {
        if (this->isBottom())
        {
            return true;
        }
        else if (other.isBottom())
        {
            return false;
        }
        else
        {
            return other._lb.leq(this->_lb) && this->_ub.leq(other._ub);
        }
 
    }

contains()

bool SVF::IntervalValue::contains ( int  n ) const

inline

Return true if the IntervalValue contains n.

Definition at line 495 of file IntervalValue.h.

    {
        return this->_lb.leq(n) && this->_ub.geq(n);
    }

create()

static IntervalValue SVF::IntervalValue::create ( const BoundedInt &  lb, const BoundedInt &  ub  )

inlinestaticprivate

Definition at line 537 of file IntervalValue.h.

    {
        if (!lb.leq(ub))
            return IntervalValue::bottom();
        else
            return IntervalValue(lb, ub);
    }

dump()

void SVF::IntervalValue::dump ( std::ostream &  o ) const

inline

Definition at line 500 of file IntervalValue.h.

    {
        if (this->isBottom())
        {
            o << "⊥";
        }
        else
        {
            o << "[" << this->_lb << ", " << this->_ub << "]";
        }
    }

equals()

bool SVF::IntervalValue::equals ( const IntervalValue &  other ) const

inline

Equality comparison.

Definition at line 375 of file IntervalValue.h.

    {
        if (this->isBottom())
        {
            return other.isBottom();
        }
        else if (other.isBottom())
        {
            return false;
        }
        else
        {
            if (this->is_real() && other.is_real())
            {
                return this->_lb.equal(other._lb) && this->_ub.equal(other._ub);
            }
            else if (this->is_int() && other.is_int())
            {
                return this->_lb.equal(other._lb) && this->_ub.equal(other._ub);
            }
            else if (this->is_int())
            {
                double thislb = this->_lb.getIntNumeral();
                double thisub = this->_ub.getIntNumeral();
                double otherlb = other._lb.getRealNumeral();
                double otherub = other._ub.getRealNumeral();
                return thislb == otherlb && thisub == otherub;
            }
            else
            {
                double thislb = this->_lb.getRealNumeral();
                double thisub = this->_ub.getRealNumeral();
                double otherlb = other._lb.getIntNumeral();
                double otherub = other._ub.getIntNumeral();
                return thislb == otherlb && thisub == otherub;
            }
            assert(false && "not implemented");
        }
    }

geq()

bool SVF::IntervalValue::geq ( const IntervalValue &  other ) const

inline

Check the lower bound of this Interval is greater than or equal to the upper bound e.g. [3, 5] > [1, 3] return true, lhs.lb >= rhs.ub

Definition at line 357 of file IntervalValue.h.

    {
        if (this->isBottom())
        {
            return true;
        }
        else if (other.isBottom())
        {
            return false;
        }
        else
        {
            return this->_lb.geq(other._ub);
        }
    }

getIntNumeral()

s64_t SVF::IntervalValue::getIntNumeral ( ) const

inline

Definition at line 264 of file IntervalValue.h.

    {
        assert(is_numeral() && "this IntervalValue is not numeral");
        return _lb.getIntNumeral();
    }

getNumeral()

s64_t SVF::IntervalValue::getNumeral ( ) const

inline

Return.

Definition at line 258 of file IntervalValue.h.

    {
        assert(is_numeral() && "this IntervalValue is not numeral");
        return _lb.getNumeral();
    }

getRealNumeral()

double SVF::IntervalValue::getRealNumeral ( ) const

inline

Definition at line 270 of file IntervalValue.h.

    {
        assert(is_numeral() && "this IntervalValue is not numeral");
        return _lb.getRealNumeral();
    }

is_infinite() [1/2]

bool SVF::IntervalValue::is_infinite ( ) const

inline

Return true if the IntervalValue is infinite IntervalValue.

Definition at line 240 of file IntervalValue.h.

    {
        return _lb.is_infinity() || _ub.is_infinity();
    }

is_infinite() [2/2]

static bool SVF::IntervalValue::is_infinite ( const BoundedInt &  e )

inlinestatic

Definition at line 88 of file IntervalValue.h.

    {
        return e.is_infinity();
    }

is_int()

bool SVF::IntervalValue::is_int ( ) const

inline

Definition at line 245 of file IntervalValue.h.

    {
        return !is_real();
    }

is_numeral()

bool SVF::IntervalValue::is_numeral ( ) const

inline

Return true if the IntervalValue is a number [num, num].

Definition at line 277 of file IntervalValue.h.

    {
        return eq(_lb, _ub);
    }

is_real()

bool SVF::IntervalValue::is_real ( ) const

inline

Definition at line 250 of file IntervalValue.h.

    {
        bool lb_real = _lb.is_real();
        bool ub_real = _ub.is_real();
        return lb_real || ub_real;
    }

is_zero()

bool SVF::IntervalValue::is_zero ( ) const

inline

Return true if the IntervalValue is [0, 0].

Definition at line 234 of file IntervalValue.h.

    {
        return _lb.is_zero() && _ub.is_zero();
    }

isBottom()

bool SVF::IntervalValue::isBottom ( ) const

inline

Definition at line 71 of file IntervalValue.h.

    {
        return _lb.is_plus_infinity() && _ub.is_minus_infinity();
    }

isTop()

bool SVF::IntervalValue::isTop ( ) const

inline

Definition at line 66 of file IntervalValue.h.

    {
        return _lb.is_minus_infinity() && _ub.is_plus_infinity();
    }

join_with()

void SVF::IntervalValue::join_with ( const IntervalValue &  other )

inline

Current IntervalValue joins with another IntervalValue.

Definition at line 416 of file IntervalValue.h.

    {
        if (this->isBottom())
        {
            if (other.isBottom())
            {
                return;
            }
            else
            {
                setValue(other.lb(), other.ub());
            }
        }
        else if (other.isBottom())
        {
            return;
        }
        else
        {
            setValue(min(this->lb(), other.lb()), max(this->ub(), other.ub()));
        }
    }

lb()

const BoundedInt& SVF::IntervalValue::lb ( ) const

inline

Return the lower bound.

Definition at line 220 of file IntervalValue.h.

    {
        assert(!this->isBottom() && "bottom interval does not have lower bound");
        return this->_lb;
    }

leq()

bool SVF::IntervalValue::leq ( const IntervalValue &  other ) const

inline

Check the upper bound of this Interval is less than or equal to the lower bound e.g. [1, 3] < [3, 5] return true, lhs.ub <= rhs.lb

Definition at line 339 of file IntervalValue.h.

    {
        if (this->isBottom())
        {
            return true;
        }
        else if (other.isBottom())
        {
            return false;
        }
        else
        {
            return this->_ub.leq(other._lb);
        }
    }

meet_with()

void SVF::IntervalValue::meet_with ( const IntervalValue &  other )

inline

Return a intersected IntervalValue.

Definition at line 475 of file IntervalValue.h.

    {
        if (this->isBottom() || other.isBottom())
        {
            this->set_to_bottom();
        }
        else
        {
            if (!(max(this->_lb, other.lb()).leq(min(this->_ub, other.ub()))))
            {
                this->set_to_bottom();
            }
            else
            {
                setValue(max(this->_lb, other.lb()), min(this->_ub, other.ub()));
            }
        }
    }

minus_infinity()

static BoundedInt SVF::IntervalValue::minus_infinity ( )

inlinestatic

Get minus infinity -inf.

Definition at line 77 of file IntervalValue.h.

    {
        return BoundedInt::minus_infinity();
    }

narrow_with()

void SVF::IntervalValue::narrow_with ( const IntervalValue &  other )

inline

Current IntervalValue narrow with another IntervalValue.

Definition at line 458 of file IntervalValue.h.

    {
        if (this->isBottom() || other.isBottom())
        {
            this->set_to_bottom();
        }
        else if (other.isBottom())
        {
            return;
        }
        else
        {
            setValue(is_infinite(this->lb()) ? other._lb : this->_lb, is_infinite(this->ub()) ? other._ub : this->_ub);
        }
    }

operator!=()

IntervalValue SVF::IntervalValue::operator!= ( const IntervalValue &  other ) const

inline

Equality comparison.

Definition at line 184 of file IntervalValue.h.

    {
        if (this->isBottom() || other.isBottom())
        {
            return bottom();
        }
        else if (this->isTop() || other.isTop())
        {
            return top();
        }
        else
        {
            if (this->is_numeral() && other.is_numeral())
            {
                return eq(this->_lb, other._lb) ? IntervalValue(0, 0) : IntervalValue(1, 1);
            }
            else
            {
                IntervalValue value = *this;
                value.meet_with(other);
                if (!value.isBottom())
                {
                    return IntervalValue(0, 1);
                }
                else
                {
                    return IntervalValue(1, 1);
                }
            }
        }
    }

operator=() [1/2]

IntervalValue& SVF::IntervalValue::operator= ( const IntervalValue &  a )

default

Copy assignment operator.

operator=() [2/2]

IntervalValue& SVF::IntervalValue::operator= ( IntervalValue &&  )

default

Move assignment operator.

operator==()

IntervalValue SVF::IntervalValue::operator== ( const IntervalValue &  other ) const

inline

Equality comparison.

Definition at line 150 of file IntervalValue.h.

    {
        if (this->isBottom() || other.isBottom())
        {
            return bottom();
        }
        else if (this->isTop() || other.isTop())
        {
            return top();
        }
        else
        {
            if (this->is_numeral() && other.is_numeral())
            {
                return eq(this->_lb, other._lb) ? IntervalValue(1, 1) : IntervalValue(0, 0);
            }
            else
            {
                IntervalValue value = *this;
                value.meet_with(other);
                if (value.isBottom())
                {
                    return IntervalValue(0, 0);
                }
                else
                {
                    // return top();
                    return IntervalValue(0, 1);
                }
            }
        }
    }

plus_infinity()

static BoundedInt SVF::IntervalValue::plus_infinity ( )

inlinestatic

Get plus infinity +inf.

Definition at line 83 of file IntervalValue.h.

    {
        return BoundedInt::plus_infinity();
    }

set_to_bottom()

void SVF::IntervalValue::set_to_bottom ( )

inline

Set current IntervalValue as bottom.

Definition at line 283 of file IntervalValue.h.

    {
        this->_lb = plus_infinity();
        this->_ub = minus_infinity();
    }

set_to_top()

void SVF::IntervalValue::set_to_top ( )

inline

Set current IntervalValue as top.

Definition at line 290 of file IntervalValue.h.

    {
        this->_lb = minus_infinity();
        this->_ub = plus_infinity();
    }

setValue()

void SVF::IntervalValue::setValue ( const BoundedInt &  lb, const BoundedInt &  ub  )

inlineprivate

Set the lower bound.

Definition at line 528 of file IntervalValue.h.

    {
        assert((isBottom() || _lb.leq(_ub)) && "lower bound should be less than or equal to upper bound");
        this->_lb = lb;
        this->_ub = ub;
    }

top()

static IntervalValue SVF::IntervalValue::top ( )

inlinestatic

Create the IntervalValue [-inf, +inf].

Definition at line 94 of file IntervalValue.h.

    {
        return IntervalValue(minus_infinity(), plus_infinity());
    }

toString()

const std::string SVF::IntervalValue::toString ( ) const

inline

Definition at line 512 of file IntervalValue.h.

    {
        std::string str;
        std::stringstream rawStr(str);
        if (this->isBottom())
        {
            rawStr << "⊥";
        }
        else
        {
            rawStr << "[" << lb().to_string() << ", " << ub().to_string() << "]";
        }
        return rawStr.str();
    }

ub()

const BoundedInt& SVF::IntervalValue::ub ( ) const

inline

Return the upper bound.

Definition at line 227 of file IntervalValue.h.

    {
        assert(!this->isBottom() && "bottom interval does not have upper bound");
        return this->_ub;
    }

widen_with()

void SVF::IntervalValue::widen_with ( const IntervalValue &  other )

inline

Current IntervalValue widen with another IntervalValue.

Definition at line 440 of file IntervalValue.h.

    {
        if (this->isBottom())
        {
            this->_lb = other._lb;
            this->_ub = other._ub;
        }
        else if (other.isBottom())
        {
            return;
        }
        else
        {
            setValue(!lb().leq(other.lb()) ? minus_infinity() : this->lb(), !ub().geq(other.ub()) ? plus_infinity() : this->ub());
        }
    }

Friends And Related Function Documentation

operator&

IntervalValue operator& ( const IntervalValue &  lhs, const IntervalValue &  rhs  )

friend

Bitwise AND of IntervalValues.

Definition at line 962 of file IntervalValue.h.

{
    if (lhs.isBottom() || rhs.isBottom())
        return IntervalValue::bottom();
    else if (lhs.is_numeral() && rhs.is_numeral())
    {
        return IntervalValue(lhs.lb() & rhs.lb());
    }
    else if (lhs.lb().getNumeral() >= 0 && rhs.lb().getNumeral() >= 0)
    {
        return IntervalValue((s64_t) 0, min(lhs.ub(), rhs.ub()));
    }
    else if (lhs.lb().getNumeral() >= 0)
    {
        return IntervalValue((s64_t) 0, lhs.ub());
    }
    else if (rhs.lb().getNumeral() >= 0)
    {
        return IntervalValue((s64_t) 0, rhs.ub());
    }
    else
    {
        return IntervalValue::top();
    }
}

operator*

IntervalValue operator* ( const IntervalValue &  lhs, const IntervalValue &  rhs  )

friend

Multiply IntervalValues.

Definition at line 583 of file IntervalValue.h.

{
    if (lhs.isBottom() || rhs.isBottom())
    {
        return IntervalValue::bottom();
    }
    else
    {
        BoundedInt ll = lhs.lb() * rhs.lb();
        BoundedInt lu = lhs.lb() * rhs.ub();
        BoundedInt ul = lhs.ub() * rhs.lb();
        BoundedInt uu = lhs.ub() * rhs.ub();
        std::vector<BoundedInt> vec{ll, lu, ul, uu};
        return IntervalValue(BoundedInt::min(vec),
                             BoundedInt::max(vec));
    }
}

operator+

IntervalValue operator+ ( const IntervalValue &  lhs, const IntervalValue &  rhs  )

friend

Add IntervalValues.

Definition at line 547 of file IntervalValue.h.

{
    if (lhs.isBottom() || rhs.isBottom())
    {
        return IntervalValue::bottom();
    }
    else if (lhs.isTop() || rhs.isTop())
    {
        return IntervalValue::top();
    }
    else
    {
        return IntervalValue(lhs.lb() + rhs.lb(), lhs.ub() + rhs.ub());
    }
}

operator-

IntervalValue operator- ( const IntervalValue &  lhs, const IntervalValue &  rhs  )

friend

Subtract IntervalValues.

Definition at line 565 of file IntervalValue.h.

{
    if (lhs.isBottom() || rhs.isBottom())
    {
        return IntervalValue::bottom();
    }
    else if (lhs.isTop() || rhs.isTop())
    {
        return IntervalValue::top();
    }
    else
    {
        return IntervalValue(lhs.lb() - rhs.ub(), lhs.ub() - rhs.lb());
    }
}

operator/

IntervalValue operator/ ( const IntervalValue &  lhs, const IntervalValue &  rhs  )

friend

Divide IntervalValues.

Definition at line 603 of file IntervalValue.h.

{
    if (lhs.isBottom() || rhs.isBottom())
    {
        return IntervalValue::bottom();
    }
    else if (rhs.contains(0))
    {
        IntervalValue lb = IntervalValue::create(rhs.lb(), -1);
        IntervalValue ub = IntervalValue::create(1, rhs.ub());
        IntervalValue l_res = lhs / lb;
        IntervalValue r_res = lhs / ub;
        l_res.join_with(r_res);
        return l_res;
    }
    else if (lhs.contains(0))
    {
        IntervalValue lb = IntervalValue::create(lhs.lb(), -1);
        IntervalValue ub = IntervalValue::create(1, lhs.ub());
        IntervalValue l_res = lb / rhs;
        IntervalValue r_res = ub / rhs;
        l_res.join_with(r_res);
        l_res.join_with(IntervalValue(0));
        return l_res;
    }
    else
    {
        // Neither the dividend nor the divisor contains 0
        BoundedInt ll = lhs.lb() / rhs.lb();
        BoundedInt lu = lhs.lb() / rhs.ub();
        BoundedInt ul = lhs.ub() / rhs.lb();
        BoundedInt uu = lhs.ub() / rhs.ub();
        std::vector<BoundedInt> vec{ll, lu, ul, uu};
 
        IntervalValue res =  IntervalValue(BoundedInt::min(vec),
                                           BoundedInt::max(vec));
        return res;
    }
}

operator<<

IntervalValue operator<< ( const IntervalValue &  lhs, const IntervalValue &  rhs  )

friend

Left binary shift of IntervalValues.

Definition at line 888 of file IntervalValue.h.

{
    //TODO: implement <<
    if (lhs.isBottom() || rhs.isBottom())
        return IntervalValue::bottom();
    if (lhs.isTop() && rhs.isTop())
        return IntervalValue::top();
    else
    {
        IntervalValue shift = rhs;
        shift.meet_with(IntervalValue(0, IntervalValue::plus_infinity()));
        if (shift.isBottom())
            return IntervalValue::bottom();
        BoundedInt lb = 0;
        // If the shift is greater than 32, the result is always 0
        if ((s32_t) shift.lb().getNumeral() >= 32 || shift.lb().is_infinity())
        {
            lb = IntervalValue::minus_infinity();
        }
        else
        {
            lb = (1 << (s32_t) shift.lb().getNumeral());
        }
        BoundedInt ub = 0;
        if (shift.ub().is_infinity())
        {
            ub = IntervalValue::plus_infinity();
        }
        else
        {
            ub = (1 << (s32_t) shift.ub().getNumeral());
        }
        IntervalValue coeff(lb, ub);
        return lhs * coeff;
    }
}

operator>>

IntervalValue operator>> ( const IntervalValue &  lhs, const IntervalValue &  rhs  )

friend

Left binary shift of IntervalValues.

Definition at line 926 of file IntervalValue.h.

{
    //TODO: implement >>
    if (lhs.isBottom() || rhs.isBottom())
        return IntervalValue::bottom();
    else if (lhs.isTop() && rhs.isTop())
        return IntervalValue::top();
    else
    {
        IntervalValue shift = rhs;
        shift.meet_with(IntervalValue(0, IntervalValue::plus_infinity()));
        if (shift.isBottom())
            return IntervalValue::bottom();
        if (lhs.contains(0))
        {
            IntervalValue l = IntervalValue::create(lhs.lb(), -1);
            IntervalValue u = IntervalValue::create(1, lhs.ub());
            IntervalValue tmp = l >> rhs;
            tmp.join_with(u >> rhs);
            tmp.join_with(IntervalValue(0));
            return tmp;
        }
        else
        {
            BoundedInt ll = lhs.lb() >> shift.lb();
            BoundedInt lu = lhs.lb() >> shift.ub();
            BoundedInt ul = lhs.ub() >> shift.lb();
            BoundedInt uu = lhs.ub() >> shift.ub();
            std::vector<BoundedInt> vec{ll, lu, ul, uu};
            return IntervalValue(BoundedInt::min(vec),
                                 BoundedInt::max(vec));
        }
    }
}

operator^

IntervalValue operator^ ( const IntervalValue &  lhs, const IntervalValue &  rhs  )

friend

Bitwise XOR of IntervalValues.

Definition at line 1018 of file IntervalValue.h.

{
    auto next_power_of_2 = [](s64_t num)
    {
        int i = 1;
        while ((num >> i) != 0)
        {
            ++i;
        }
        return 1 << i;
    };
    if (lhs.isBottom() || rhs.isBottom())
        return IntervalValue::bottom();
    else if (lhs.is_numeral() && rhs.is_numeral())
        return IntervalValue(lhs.lb() ^ rhs.lb());
    else if (lhs.lb().getNumeral() >= 0 && !lhs.ub().is_infinity() &&
             rhs.lb().getNumeral() >= 0 && !rhs.ub().is_infinity())
    {
        s64_t m = std::max(lhs.ub().getNumeral(), rhs.ub().getNumeral());
        s64_t ub = next_power_of_2(s64_t(m)) - 1;
        return IntervalValue((s64_t) 0, (s64_t) ub);
    }
    else
    {
        return IntervalValue::top();
    }
}

operator|

IntervalValue operator| ( const IntervalValue &  lhs, const IntervalValue &  rhs  )

friend

Bitwise OR of IntervalValues.

Definition at line 989 of file IntervalValue.h.

{
    auto next_power_of_2 = [](s64_t num)
    {
        int i = 1;
        while ((num >> i) != 0)
        {
            ++i;
        }
        return 1 << i;
    };
    if (lhs.isBottom() || rhs.isBottom())
        return IntervalValue::bottom();
    else if (lhs.is_numeral() && rhs.is_numeral())
        return IntervalValue(lhs.lb() | rhs.lb());
    else if (lhs.lb().getNumeral() >= 0 && !lhs.ub().is_infinity() &&
             rhs.lb().getNumeral() >= 0 && !rhs.ub().is_infinity())
    {
        s64_t m = std::max(lhs.ub().getNumeral(), rhs.ub().getNumeral());
        s64_t ub = next_power_of_2(s64_t(m)) - 1;
        return IntervalValue((s64_t) 0, (s64_t) ub);
    }
    else
    {
        return IntervalValue::top();
    }
}

Member Data Documentation

_lb

BoundedInt SVF::IntervalValue::_lb

private

Definition at line 49 of file IntervalValue.h.

_ub

BoundedInt SVF::IntervalValue::_ub

private

Definition at line 52 of file IntervalValue.h.

---

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

• /home/runner/work/SVF/SVF/svf/include/AE/Core/IntervalValue.h