Skip to content

Commit

Permalink
fix intervalValue compare operators
Browse files Browse the repository at this point in the history
  • Loading branch information
jiawei.wang committed Nov 21, 2023
1 parent 3788a5f commit c5f33ac
Showing 1 changed file with 72 additions and 24 deletions.
96 changes: 72 additions & 24 deletions svf/include/AbstractExecution/IntervalValue.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -580,35 +580,48 @@ inline IntervalValue operator%(const IntervalValue &lhs,
/// Greater than IntervalValues
inline IntervalValue operator>(const IntervalValue &lhs, const IntervalValue &rhs)
{
// if one of lhs and rhs is bottom, set bottom
if (lhs.isBottom() || rhs.isBottom())
{
return IntervalValue::bottom();
}
// if one of lhs and rhs is top, set top
else if (lhs.isTop() || lhs.isTop())
{
return IntervalValue::top();
}
else
{
// if lhs and rhs are both numeral (lb = ub), directly compare both value
if (lhs.is_numeral() && rhs.is_numeral())
{
return lhs.lb().leq(rhs.lb()) ? IntervalValue(0, 0) : IntervalValue(1, 1);
// call getNumeral() since compare function's return type is still NumericLiteral
return (lhs.lb() > rhs.lb()).getNumeral() == 1 ? IntervalValue(1, 1) : IntervalValue(0, 0);
}
else
{
// lhs[3,4] rhs[1,2]
if (!lhs.lb().leq(rhs.ub()))
// return [1,1] means lhs is totally > lhs
// when lhs.lb > rhs.ub, e.g. lhs:[3, 4] rhs:[1, 2]
// lhs.lb(3) > rhs.ub(2)
// call getNumeral() since compare function's return type is still NumericLiteral
if ((lhs.lb() > rhs.ub()).getNumeral() == 1)
{
return IntervalValue(1, 1);
// lhs[1,2] rhs[3,4]
}
else if (!lhs.ub().geq(rhs.lb()))
// return [0,0] means lhs is totally impossible to > lhs
// a.k.a lhs is totally <= rhs
// when lhs.ub <= rhs.lb, e.g. lhs:[3, 4] rhs:[4，5]
// lhs.ub(4) <= rhs.lb(4)
else if (lhs.ub().leq(rhs.lb()))
{
return IntervalValue(0, 0);
}
// for other cases, lhs can > rhs or not, depending on the values
// e.g. lhs: [2,4], rhs: [1,3],
// lhs can > rhs if lhs is 4, rhs is 1.
// lhs can also not > rhs if lhs is 2 rhs is 3
else
{
// lhs[1,3] rhs[2,4]
return IntervalValue(0, 1);
}
}
Expand All @@ -618,33 +631,46 @@ inline IntervalValue operator>(const IntervalValue &lhs, const IntervalValue &rh
/// Greater than IntervalValues
inline IntervalValue operator<(const IntervalValue &lhs, const IntervalValue &rhs)
{
// if one of lhs and rhs is bottom, set bottom
if (lhs.isBottom() || rhs.isBottom())
{
return IntervalValue::bottom();
}
// if one of lhs and rhs is top, set top
else if (lhs.isTop() || lhs.isTop())
{
return IntervalValue::top();
}
else
{
// if lhs and rhs are both numeral (lb = ub), directly compare both value
if (lhs.is_numeral() && rhs.is_numeral())
{
return lhs.lb().geq(rhs.lb()) ? IntervalValue(0, 0) : IntervalValue(1, 1);
// call getNumeral() since compare function's return type is still NumericLiteral
return (lhs.lb() < rhs.lb()).getNumeral() == 1 ? IntervalValue(1, 1) : IntervalValue(0, 0);
}
else
{
// lhs [1,2] rhs [3,4]
if (!lhs.ub().geq(rhs.lb()))
// return [1,1] means lhs is totally < lhs
// when lhs.ub < rhs.lb., e.g. lhs:[1, 2] rhs:[3, 4]
// lhs.ub(2) < rhs.lb(3)
// call getNumeral() since compare function's return type is still NumericLiteral
if ((lhs.ub() < rhs.lb()).getNumeral() == 1)
{
return IntervalValue(1, 1);
// lhs [3,4] rhs [1,2]
}
else if (!lhs.lb().leq(rhs.ub()))
// return [0,0] means lhs is totally impossible to < lhs
// a.k.a lhs is totally >= rhs
// when lhs.ub >= rhs.lb, e.g. lhs:[3, 4] rhs:[4，5]
// lhs.ub(4) >= rhs.lb(4)
else if (rhs.ub().geq(lhs.lb()))
{
return IntervalValue(0, 0);
// lhs [1,3] rhs [2,4]
}
// for other cases, lhs can > rhs or not, depending on the values
// e.g. lhs: [2,4], rhs: [1,3],
// lhs can < rhs if lhs is 2, rhs is 3.
// lhs can also not < rhs if lhs is 4 rhs is 1
else
{
return IntervalValue(0, 1);
Expand All @@ -657,37 +683,48 @@ inline IntervalValue operator<(const IntervalValue &lhs, const IntervalValue &rh
/// Greater than IntervalValues
inline IntervalValue operator>=(const IntervalValue &lhs, const IntervalValue &rhs)
{
// if one of lhs and rhs is bottom, set bottom
if (lhs.isBottom() || rhs.isBottom())
{
return IntervalValue::bottom();
}
// if one of lhs and rhs is top, set top
else if (lhs.isTop() || lhs.isTop())
{
return IntervalValue::top();
}
else
{
// if lhs and rhs are both numeral (lb = ub), directly compare both value
if (lhs.is_numeral() && rhs.is_numeral())
{
return lhs.lb().geq(rhs.lb()) ? IntervalValue(1, 1) : IntervalValue(0, 0);
}
else
{
// lhs [2,3] rhs [1,2]
// return [1,1] means lhs is totally >= lhs
// when lhs.lb >= rhs.ub., e.g. lhs:[2, 3] rhs:[1, 2]
// lhs.lb(2) >= rhs.ub(2)
if (lhs.lb().geq(rhs.ub()))
{
return IntervalValue(1, 1);
// lhs [1,2] rhs[3,4]
}
else if (!lhs.ub().geq(rhs.lb()))
// return [0,0] means lhs is totally impossible to >= lhs
// a.k.a lhs is totally < rhs
// when lhs.ub < rhs.lb, e.g. lhs:[1, 2] rhs:[3，4]
// lhs.ub(2) < rhs.lb(3)
// call getNumeral() since compare function's return type is still NumericLiteral
else if ((lhs.ub() < rhs.lb()).getNumeral() == 1)
{
return IntervalValue(0, 0);
// lhs [1,3] rhs [2,4]
}
// for other cases, lhs can >= rhs or not, depending on the values
// e.g. lhs: [2,4], rhs: [1,3],
// lhs can >= rhs if lhs is 3, rhs is 2.
// lhs can also not >= rhs if lhs is 2 rhs is 3
else
{
if (lhs.equals(rhs)) return IntervalValue(1, 1);
else return IntervalValue(0, 1);
return IntervalValue(0, 1);
}
}
}
Expand All @@ -696,37 +733,48 @@ inline IntervalValue operator>=(const IntervalValue &lhs, const IntervalValue &r
/// Greater than IntervalValues
inline IntervalValue operator<=(const IntervalValue &lhs, const IntervalValue &rhs)
{
// if one of lhs and rhs is bottom, set bottom
if (lhs.isBottom() || rhs.isBottom())
{
return IntervalValue::bottom();
}
// if one of lhs and rhs is top, set top
else if (lhs.isTop() || lhs.isTop())
{
return IntervalValue::top();
}
else
{
// if lhs and rhs are both numeral (lb = ub), directly compare both value
if (lhs.is_numeral() && rhs.is_numeral())
{
return lhs.lb().leq(rhs.lb()) ? IntervalValue(1, 1) : IntervalValue(0, 0);
}
else
{
// lhs [1,2] rhs [2,3]
// return [1,1] means lhs is totally <= lhs
// when lhs.ub <= rhs.lb., e.g. lhs:[1, 2] rhs:[2, 3]
// lhs.ub(2) <= rhs.lb(2)
if (lhs.ub().leq(rhs.lb()))
{
return IntervalValue(1, 1);
// lhs [3,4] rhs[1,2]
}
else if (!lhs.lb().leq(rhs.ub()))
// return [0,0] means lhs is totally impossible to <= lhs
// a.k.a lhs is totally > rhs
// when lhs.lb > rhs.ub, e.g. lhs:[3, 4] rhs:[1，2]
// lhs.lb(3) > rhs.ub(2)
// call getNumeral() since compare function's return type is still NumericLiteral
else if ((lhs.lb() > rhs.ub()).getNumeral() == 1)
{
return IntervalValue(0, 0);
// lhs [1,3] rhs [2,4]
}
// for other cases, lhs can <= rhs or not, depending on the values
// e.g. lhs: [2,4], rhs: [1,3],
// lhs can <= rhs if lhs is 3, rhs is 3.
// lhs can also not <= rhs if lhs is 3 rhs is 2
else
{
if (lhs.equals(rhs)) return IntervalValue(1, 1);
else return IntervalValue(0, 1);
return IntervalValue(0, 1);
}
}
}
Expand Down

0 comments on commit c5f33ac

Please sign in to comment.