From c5f33acd2e5619d07ecb8402f73e51f8feb867d2 Mon Sep 17 00:00:00 2001 From: "jiawei.wang" Date: Tue, 21 Nov 2023 21:42:43 +1100 Subject: [PATCH] fix intervalValue compare operators --- svf/include/AbstractExecution/IntervalValue.h | 96 ++++++++++++++----- 1 file changed, 72 insertions(+), 24 deletions(-) diff --git a/svf/include/AbstractExecution/IntervalValue.h b/svf/include/AbstractExecution/IntervalValue.h index b43ac3730d..a000d3e45c 100644 --- a/svf/include/AbstractExecution/IntervalValue.h +++ b/svf/include/AbstractExecution/IntervalValue.h @@ -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); } } @@ -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); @@ -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); } } } @@ -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); } } }