Static Value-Flow Analysis
Loading...
Searching...
No Matches
Public Member Functions | Static Public Member Functions | Private Member Functions | Static Private Member Functions | Private Attributes | Friends | List of all members
SVF::IntervalValue Class Reference

#include <IntervalValue.h>

Public Member Functions

bool isTop () const
 
bool isBottom () const
 
 IntervalValue ()
 Create default IntervalValue.
 
 IntervalValue (s64_t n)
 Create the IntervalValue [n, n].
 
 IntervalValue (s32_t n)
 
 IntervalValue (u32_t n)
 
 IntervalValue (double n)
 
 IntervalValue (BoundedInt n)
 
 IntervalValue (BoundedInt lb, BoundedInt ub)
 Create the IntervalValue [lb, ub].
 
 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.
 
 IntervalValue (IntervalValue &&)=default
 Move constructor.
 
IntervalValueoperator= (const IntervalValue &a)=default
 Copy assignment operator.
 
IntervalValueoperator= (IntervalValue &&)=default
 Move assignment operator.
 
IntervalValue operator== (const IntervalValue &other) const
 Equality comparison.
 
IntervalValue operator!= (const IntervalValue &other) const
 Equality comparison.
 
 ~IntervalValue ()=default
 Destructor.
 
const BoundedIntlb () const
 Return the lower bound.
 
const BoundedIntub () const
 Return the upper bound.
 
bool is_zero () const
 Return true if the IntervalValue is [0, 0].
 
bool is_infinite () const
 Return true if the IntervalValue is infinite IntervalValue.
 
bool is_int () const
 
bool is_real () const
 
s64_t getNumeral () const
 Return.
 
s64_t getIntNumeral () const
 
double getRealNumeral () const
 
bool is_numeral () const
 Return true if the IntervalValue is a number [num, num].
 
void set_to_bottom ()
 Set current IntervalValue as bottom.
 
void set_to_top ()
 Set current IntervalValue as top.
 
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.
 
void join_with (const IntervalValue &other)
 Current IntervalValue joins with another IntervalValue.
 
void widen_with (const IntervalValue &other)
 Current IntervalValue widen with another IntervalValue.
 
void narrow_with (const IntervalValue &other)
 Current IntervalValue narrow with another IntervalValue.
 
void meet_with (const IntervalValue &other)
 Return a intersected IntervalValue.
 
bool contains (int n) const
 Return true if the IntervalValue contains n.
 
void dump (std::ostream &o) const
 
const std::string toString () const
 

Static Public Member Functions

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

Private Member Functions

void setValue (const BoundedInt &lb, const BoundedInt &ub)
 Set the lower bound.
 

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.
 
IntervalValue operator- (const IntervalValue &lhs, const IntervalValue &rhs)
 Subtract IntervalValues.
 
IntervalValue operator* (const IntervalValue &lhs, const IntervalValue &rhs)
 Multiply IntervalValues.
 
IntervalValue operator/ (const IntervalValue &lhs, const IntervalValue &rhs)
 Divide IntervalValues.
 
IntervalValue operator<< (const IntervalValue &lhs, const IntervalValue &rhs)
 Left binary shift of IntervalValues.
 
IntervalValue operator>> (const IntervalValue &lhs, const IntervalValue &rhs)
 Left binary shift of IntervalValues.
 
IntervalValue operator& (const IntervalValue &lhs, const IntervalValue &rhs)
 Bitwise AND of IntervalValues.
 
IntervalValue operator| (const IntervalValue &lhs, const IntervalValue &rhs)
 Bitwise OR of IntervalValues.
 
IntervalValue operator^ (const IntervalValue &lhs, const IntervalValue &rhs)
 Bitwise XOR of IntervalValues.
 

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.

static BoundedInt minus_infinity()
Get minus infinity -inf.
static BoundedInt plus_infinity()
Get plus infinity +inf.

◆ IntervalValue() [2/15]

SVF::IntervalValue::IntervalValue ( s64_t  n)
inlineexplicit

Create the IntervalValue [n, n].

Definition at line 109 of file IntervalValue.h.

109: _lb(n), _ub(n) {}
cJSON * n
Definition cJSON.cpp:2558

◆ IntervalValue() [3/15]

SVF::IntervalValue::IntervalValue ( s32_t  n)
inlineexplicit

Definition at line 111 of file IntervalValue.h.

111: IntervalValue((s64_t) n) {}
IntervalValue()
Create default IntervalValue.
signed long long s64_t
Definition GeneralType.h:50

◆ IntervalValue() [4/15]

SVF::IntervalValue::IntervalValue ( u32_t  n)
inlineexplicit

Definition at line 113 of file IntervalValue.h.

113: IntervalValue((s64_t) n) {}

◆ IntervalValue() [5/15]

SVF::IntervalValue::IntervalValue ( double  n)
inlineexplicit

Definition at line 115 of file IntervalValue.h.

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

◆ IntervalValue() [6/15]

SVF::IntervalValue::IntervalValue ( BoundedInt  n)
inlineexplicit

Definition at line 117 of file IntervalValue.h.

117: 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.

120 : _lb(std::move(lb)), _ub(std::move(ub))
121 {
122 assert((isBottom() || _lb.leq(_ub)) && "lower bound should be less than or equal to upper bound");
123 }
bool leq(const BoundedInt &rhs) const
const BoundedInt & ub() const
Return the upper bound.
bool isBottom() const
const BoundedInt & lb() const
Return the lower bound.
llvm::IRBuilder IRBuilder
Definition BasicTypes.h:74

◆ IntervalValue() [8/15]

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

Definition at line 125 of file IntervalValue.h.

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

◆ IntervalValue() [9/15]

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

Definition at line 127 of file IntervalValue.h.

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

◆ IntervalValue() [10/15]

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

Definition at line 129 of file IntervalValue.h.

129: 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.

131: 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.

133: 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.

135: 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.

101 {
103 }

◆ 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.

322 {
323 if (this->isBottom())
324 {
325 return true;
326 }
327 else if (other.isBottom())
328 {
329 return false;
330 }
331 else
332 {
333 return other._lb.geq(this->_lb) && this->_ub.geq(other._ub);
334 }
335 }
bool geq(const BoundedInt &rhs) const

◆ 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.

301 {
302 if (this->isBottom())
303 {
304 return true;
305 }
306 else if (other.isBottom())
307 {
308 return false;
309 }
310 else
311 {
312 return other._lb.leq(this->_lb) && this->_ub.leq(other._ub);
313 }
314
315 }

◆ contains()

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

Return true if the IntervalValue contains n.

Definition at line 495 of file IntervalValue.h.

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

◆ create()

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

Definition at line 537 of file IntervalValue.h.

538 {
539 if (!lb.leq(ub))
540 return IntervalValue::bottom();
541 else
542 return IntervalValue(lb, ub);
543 }
static IntervalValue bottom()
Create the bottom IntervalValue [+inf, -inf].

◆ dump()

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

Definition at line 500 of file IntervalValue.h.

501 {
502 if (this->isBottom())
503 {
504 o << "⊥";
505 }
506 else
507 {
508 o << "[" << this->_lb << ", " << this->_ub << "]";
509 }
510 }

◆ equals()

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

Equality comparison.

Definition at line 375 of file IntervalValue.h.

376 {
377 if (this->isBottom())
378 {
379 return other.isBottom();
380 }
381 else if (other.isBottom())
382 {
383 return false;
384 }
385 else
386 {
387 if (this->is_real() && other.is_real())
388 {
389 return this->_lb.equal(other._lb) && this->_ub.equal(other._ub);
390 }
391 else if (this->is_int() && other.is_int())
392 {
393 return this->_lb.equal(other._lb) && this->_ub.equal(other._ub);
394 }
395 else if (this->is_int())
396 {
397 double thislb = this->_lb.getIntNumeral();
398 double thisub = this->_ub.getIntNumeral();
399 double otherlb = other._lb.getRealNumeral();
400 double otherub = other._ub.getRealNumeral();
401 return thislb == otherlb && thisub == otherub;
402 }
403 else
404 {
405 double thislb = this->_lb.getRealNumeral();
406 double thisub = this->_ub.getRealNumeral();
407 double otherlb = other._lb.getIntNumeral();
408 double otherub = other._ub.getIntNumeral();
409 return thislb == otherlb && thisub == otherub;
410 }
411 assert(false && "not implemented");
412 }
413 }
s64_t getIntNumeral() const
bool equal(const BoundedInt &rhs) const
double getRealNumeral() const
bool is_int() const
bool is_real() const

◆ 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.

358 {
359 if (this->isBottom())
360 {
361 return true;
362 }
363 else if (other.isBottom())
364 {
365 return false;
366 }
367 else
368 {
369 return this->_lb.geq(other._ub);
370 }
371 }

◆ getIntNumeral()

s64_t SVF::IntervalValue::getIntNumeral ( ) const
inline

Definition at line 264 of file IntervalValue.h.

265 {
266 assert(is_numeral() && "this IntervalValue is not numeral");
267 return _lb.getIntNumeral();
268 }
bool is_numeral() const
Return true if the IntervalValue is a number [num, num].

◆ getNumeral()

s64_t SVF::IntervalValue::getNumeral ( ) const
inline

Return.

Definition at line 258 of file IntervalValue.h.

259 {
260 assert(is_numeral() && "this IntervalValue is not numeral");
261 return _lb.getNumeral();
262 }
s64_t getNumeral() const
Retrieves the numeral value of the BoundedInt object.

◆ getRealNumeral()

double SVF::IntervalValue::getRealNumeral ( ) const
inline

Definition at line 270 of file IntervalValue.h.

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

◆ 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.

241 {
242 return _lb.is_infinity() || _ub.is_infinity();
243 }
bool is_infinity() const

◆ is_infinite() [2/2]

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

Definition at line 88 of file IntervalValue.h.

89 {
90 return e.is_infinity();
91 }

◆ is_int()

bool SVF::IntervalValue::is_int ( ) const
inline

Definition at line 245 of file IntervalValue.h.

246 {
247 return !is_real();
248 }

◆ 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.

278 {
279 return eq(_lb, _ub);
280 }

◆ is_real()

bool SVF::IntervalValue::is_real ( ) const
inline

Definition at line 250 of file IntervalValue.h.

251 {
252 bool lb_real = _lb.is_real();
253 bool ub_real = _ub.is_real();
254 return lb_real || ub_real;
255 }
bool is_real() const

◆ 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.

235 {
236 return _lb.is_zero() && _ub.is_zero();
237 }
bool is_zero() const

◆ isBottom()

bool SVF::IntervalValue::isBottom ( ) const
inline

Definition at line 71 of file IntervalValue.h.

72 {
74 }
bool is_minus_infinity() const
bool is_plus_infinity() const

◆ isTop()

bool SVF::IntervalValue::isTop ( ) const
inline

Definition at line 66 of file IntervalValue.h.

67 {
69 }

◆ 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.

417 {
418 if (this->isBottom())
419 {
420 if (other.isBottom())
421 {
422 return;
423 }
424 else
425 {
426 setValue(other.lb(), other.ub());
427 }
428 }
429 else if (other.isBottom())
430 {
431 return;
432 }
433 else
434 {
435 setValue(min(this->lb(), other.lb()), max(this->ub(), other.ub()));
436 }
437 }
void setValue(const BoundedInt &lb, const BoundedInt &ub)
Set the lower bound.

◆ lb()

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

Return the lower bound.

Definition at line 220 of file IntervalValue.h.

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

◆ 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.

340 {
341 if (this->isBottom())
342 {
343 return true;
344 }
345 else if (other.isBottom())
346 {
347 return false;
348 }
349 else
350 {
351 return this->_ub.leq(other._lb);
352 }
353 }

◆ meet_with()

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

Return a intersected IntervalValue.

Definition at line 475 of file IntervalValue.h.

476 {
477 if (this->isBottom() || other.isBottom())
478 {
479 this->set_to_bottom();
480 }
481 else
482 {
483 if (!(max(this->_lb, other.lb()).leq(min(this->_ub, other.ub()))))
484 {
485 this->set_to_bottom();
486 }
487 else
488 {
489 setValue(max(this->_lb, other.lb()), min(this->_ub, other.ub()));
490 }
491 }
492 }
void set_to_bottom()
Set current IntervalValue as bottom.

◆ minus_infinity()

static BoundedInt SVF::IntervalValue::minus_infinity ( )
inlinestatic

Get minus infinity -inf.

Definition at line 77 of file IntervalValue.h.

78 {
80 }
static 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.

459 {
460 if (this->isBottom() || other.isBottom())
461 {
462 this->set_to_bottom();
463 }
464 else if (other.isBottom())
465 {
466 return;
467 }
468 else
469 {
470 setValue(is_infinite(this->lb()) ? other._lb : this->_lb, is_infinite(this->ub()) ? other._ub : this->_ub);
471 }
472 }
bool is_infinite() const
Return true if the IntervalValue is infinite IntervalValue.

◆ operator!=()

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

Equality comparison.

Definition at line 184 of file IntervalValue.h.

185 {
186 if (this->isBottom() || other.isBottom())
187 {
188 return bottom();
189 }
190 else if (this->isTop() || other.isTop())
191 {
192 return top();
193 }
194 else
195 {
196 if (this->is_numeral() && other.is_numeral())
197 {
198 return eq(this->_lb, other._lb) ? IntervalValue(0, 0) : IntervalValue(1, 1);
199 }
200 else
201 {
202 IntervalValue value = *this;
203 value.meet_with(other);
204 if (!value.isBottom())
205 {
206 return IntervalValue(0, 1);
207 }
208 else
209 {
210 return IntervalValue(1, 1);
211 }
212 }
213 }
214 }
bool isTop() const
static IntervalValue top()
Create the IntervalValue [-inf, +inf].

◆ 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.

151 {
152 if (this->isBottom() || other.isBottom())
153 {
154 return bottom();
155 }
156 else if (this->isTop() || other.isTop())
157 {
158 return top();
159 }
160 else
161 {
162 if (this->is_numeral() && other.is_numeral())
163 {
164 return eq(this->_lb, other._lb) ? IntervalValue(1, 1) : IntervalValue(0, 0);
165 }
166 else
167 {
168 IntervalValue value = *this;
169 value.meet_with(other);
170 if (value.isBottom())
171 {
172 return IntervalValue(0, 0);
173 }
174 else
175 {
176 // return top();
177 return IntervalValue(0, 1);
178 }
179 }
180 }
181 }

◆ plus_infinity()

static BoundedInt SVF::IntervalValue::plus_infinity ( )
inlinestatic

Get plus infinity +inf.

Definition at line 83 of file IntervalValue.h.

84 {
86 }
static 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.

284 {
285 this->_lb = plus_infinity();
286 this->_ub = minus_infinity();
287 }

◆ set_to_top()

void SVF::IntervalValue::set_to_top ( )
inline

Set current IntervalValue as top.

Definition at line 290 of file IntervalValue.h.

291 {
292 this->_lb = minus_infinity();
293 this->_ub = plus_infinity();
294 }

◆ setValue()

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

Set the lower bound.

Definition at line 528 of file IntervalValue.h.

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

◆ top()

static IntervalValue SVF::IntervalValue::top ( )
inlinestatic

Create the IntervalValue [-inf, +inf].

Definition at line 94 of file IntervalValue.h.

95 {
97 }

◆ toString()

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

Definition at line 512 of file IntervalValue.h.

513 {
514 std::string str;
515 std::stringstream rawStr(str);
516 if (this->isBottom())
517 {
518 rawStr << "⊥";
519 }
520 else
521 {
522 rawStr << "[" << lb().to_string() << ", " << ub().to_string() << "]";
523 }
524 return rawStr.str();
525 }
virtual const std::string to_string() const

◆ ub()

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

Return the upper bound.

Definition at line 227 of file IntervalValue.h.

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

◆ 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.

441 {
442 if (this->isBottom())
443 {
444 this->_lb = other._lb;
445 this->_ub = other._ub;
446 }
447 else if (other.isBottom())
448 {
449 return;
450 }
451 else
452 {
453 setValue(!lb().leq(other.lb()) ? minus_infinity() : this->lb(), !ub().geq(other.ub()) ? plus_infinity() : this->ub());
454 }
455 }
bool leq(const IntervalValue &other) const
bool geq(const IntervalValue &other) const

Friends And Related Symbol Documentation

◆ operator&

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

Bitwise AND of IntervalValues.

Definition at line 960 of file IntervalValue.h.

961{
962 if (lhs.isBottom() || rhs.isBottom())
963 return IntervalValue::bottom();
964 else if (lhs.is_numeral() && rhs.is_numeral())
965 {
966 return IntervalValue(lhs.lb() & rhs.lb());
967 }
968 else if (lhs.lb().getNumeral() >= 0 && rhs.lb().getNumeral() >= 0)
969 {
970 return IntervalValue((s64_t) 0, min(lhs.ub(), rhs.ub()));
971 }
972 else if (lhs.lb().getNumeral() >= 0)
973 {
974 return IntervalValue((s64_t) 0, lhs.ub());
975 }
976 else if (rhs.lb().getNumeral() >= 0)
977 {
978 return IntervalValue((s64_t) 0, rhs.ub());
979 }
980 else
981 {
982 return IntervalValue::top();
983 }
984}

◆ operator*

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

Multiply IntervalValues.

Definition at line 583 of file IntervalValue.h.

585{
586 if (lhs.isBottom() || rhs.isBottom())
587 {
588 return IntervalValue::bottom();
589 }
590 else
591 {
592 BoundedInt ll = lhs.lb() * rhs.lb();
593 BoundedInt lu = lhs.lb() * rhs.ub();
594 BoundedInt ul = lhs.ub() * rhs.lb();
595 BoundedInt uu = lhs.ub() * rhs.ub();
596 std::vector<BoundedInt> vec{ll, lu, ul, uu};
599 }
600}
friend BoundedInt max(const BoundedInt &lhs, const BoundedInt &rhs)
friend BoundedInt min(const BoundedInt &lhs, const BoundedInt &rhs)

◆ operator+

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

Add IntervalValues.

Definition at line 547 of file IntervalValue.h.

549{
550 if (lhs.isBottom() || rhs.isBottom())
551 {
552 return IntervalValue::bottom();
553 }
554 else if (lhs.isTop() || rhs.isTop())
555 {
556 return IntervalValue::top();
557 }
558 else
559 {
560 return IntervalValue(lhs.lb() + rhs.lb(), lhs.ub() + rhs.ub());
561 }
562}

◆ operator-

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

Subtract IntervalValues.

Definition at line 565 of file IntervalValue.h.

567{
568 if (lhs.isBottom() || rhs.isBottom())
569 {
570 return IntervalValue::bottom();
571 }
572 else if (lhs.isTop() || rhs.isTop())
573 {
574 return IntervalValue::top();
575 }
576 else
577 {
578 return IntervalValue(lhs.lb() - rhs.ub(), lhs.ub() - rhs.lb());
579 }
580}

◆ operator/

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

Divide IntervalValues.

Definition at line 603 of file IntervalValue.h.

605{
606 if (lhs.isBottom() || rhs.isBottom())
607 {
608 return IntervalValue::bottom();
609 }
610 else if (rhs.contains(0))
611 {
616 l_res.join_with(r_res);
617 return l_res;
618 }
619 else if (lhs.contains(0))
620 {
625 l_res.join_with(r_res);
626 l_res.join_with(IntervalValue(0));
627 return l_res;
628 }
629 else
630 {
631 // Neither the dividend nor the divisor contains 0
632 BoundedInt ll = lhs.lb() / rhs.lb();
633 BoundedInt lu = lhs.lb() / rhs.ub();
634 BoundedInt ul = lhs.ub() / rhs.lb();
635 BoundedInt uu = lhs.ub() / rhs.ub();
636 std::vector<BoundedInt> vec{ll, lu, ul, uu};
637
640 return res;
641 }
642}
static IntervalValue create(const BoundedInt &lb, const BoundedInt &ub)

◆ operator<<

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

Left binary shift of IntervalValues.

Definition at line 888 of file IntervalValue.h.

889{
890 if (lhs.isBottom() || rhs.isBottom())
891 return IntervalValue::bottom();
892 if (lhs.isTop() && rhs.isTop())
893 return IntervalValue::top();
894 else
895 {
898 if (shift.isBottom())
899 return IntervalValue::bottom();
900 BoundedInt lb = 0;
901 // If the shift is greater than 32, the result is always 0
902 if ((s32_t) shift.lb().getNumeral() >= 32 || shift.lb().is_infinity())
903 {
905 }
906 else
907 {
908 lb = (1 << (s32_t) shift.lb().getNumeral());
909 }
910 BoundedInt ub = 0;
911 if (shift.ub().is_infinity())
912 {
914 }
915 else
916 {
917 ub = (1 << (s32_t) shift.ub().getNumeral());
918 }
920 return lhs * coeff;
921 }
922}
signed s32_t
Definition GeneralType.h:48

◆ operator>>

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

Left binary shift of IntervalValues.

Definition at line 925 of file IntervalValue.h.

926{
927 if (lhs.isBottom() || rhs.isBottom())
928 return IntervalValue::bottom();
929 else if (lhs.isTop() && rhs.isTop())
930 return IntervalValue::top();
931 else
932 {
935 if (shift.isBottom())
936 return IntervalValue::bottom();
937 if (lhs.contains(0))
938 {
941 IntervalValue tmp = l >> rhs;
942 tmp.join_with(u >> rhs);
943 tmp.join_with(IntervalValue(0));
944 return tmp;
945 }
946 else
947 {
948 BoundedInt ll = lhs.lb() >> shift.lb();
949 BoundedInt lu = lhs.lb() >> shift.ub();
950 BoundedInt ul = lhs.ub() >> shift.lb();
951 BoundedInt uu = lhs.ub() >> shift.ub();
952 std::vector<BoundedInt> vec{ll, lu, ul, uu};
955 }
956 }
957}

◆ operator^

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

Bitwise XOR of IntervalValues.

Definition at line 1016 of file IntervalValue.h.

1017{
1018 auto next_power_of_2 = [](s64_t num)
1019 {
1020 int i = 1;
1021 while ((num >> i) != 0)
1022 {
1023 ++i;
1024 }
1025 return 1 << i;
1026 };
1027 if (lhs.isBottom() || rhs.isBottom())
1028 return IntervalValue::bottom();
1029 else if (lhs.is_numeral() && rhs.is_numeral())
1030 return IntervalValue(lhs.lb() ^ rhs.lb());
1031 else if (lhs.lb().getNumeral() >= 0 && !lhs.ub().is_infinity() &&
1032 rhs.lb().getNumeral() >= 0 && !rhs.ub().is_infinity())
1033 {
1034 s64_t m = std::max(lhs.ub().getNumeral(), rhs.ub().getNumeral());
1035 s64_t ub = next_power_of_2(s64_t(m)) - 1;
1036 return IntervalValue((s64_t) 0, (s64_t) ub);
1037 }
1038 else
1039 {
1040 return IntervalValue::top();
1041 }
1042}

◆ operator|

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

Bitwise OR of IntervalValues.

Definition at line 987 of file IntervalValue.h.

988{
989 auto next_power_of_2 = [](s64_t num)
990 {
991 int i = 1;
992 while ((num >> i) != 0)
993 {
994 ++i;
995 }
996 return 1 << i;
997 };
998 if (lhs.isBottom() || rhs.isBottom())
999 return IntervalValue::bottom();
1000 else if (lhs.is_numeral() && rhs.is_numeral())
1001 return IntervalValue(lhs.lb() | rhs.lb());
1002 else if (lhs.lb().getNumeral() >= 0 && !lhs.ub().is_infinity() &&
1003 rhs.lb().getNumeral() >= 0 && !rhs.ub().is_infinity())
1004 {
1005 s64_t m = std::max(lhs.ub().getNumeral(), rhs.ub().getNumeral());
1006 s64_t ub = next_power_of_2(s64_t(m)) - 1;
1007 return IntervalValue((s64_t) 0, (s64_t) ub);
1008 }
1009 else
1010 {
1011 return IntervalValue::top();
1012 }
1013}

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: