From ab51a624e1c3b33f7e86b5efe5ddd06bf02e04d4 Mon Sep 17 00:00:00 2001 From: sjfink Date: Fri, 9 Nov 2007 21:47:19 +0000 Subject: [PATCH] improved LE logic git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1997 f5eafffb-2e1d-0410-98e4-8ec43c5233c4 --- .../logic/AdHocSemiDecisionProcedure.java | 49 ++++++++++++++++--- 1 file changed, 41 insertions(+), 8 deletions(-) diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/AdHocSemiDecisionProcedure.java b/com.ibm.wala.core/src/com/ibm/wala/logic/AdHocSemiDecisionProcedure.java index aa203a55d..a256563ea 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/AdHocSemiDecisionProcedure.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/AdHocSemiDecisionProcedure.java @@ -227,10 +227,8 @@ public class AdHocSemiDecisionProcedure extends AbstractSemiDecisionProcedure { } else if (r.getRelation().equals(BinaryRelation.GE)) { ITerm lhs = r.getTerms().get(0); ITerm rhs = r.getTerms().get(1); - if (lhs instanceof IntConstant && rhs instanceof IntConstant) { - IntConstant x = (IntConstant) lhs; - IntConstant y = (IntConstant) rhs; - return x.getVal().intValue() >= y.getVal().intValue(); + if (isLE(rhs, lhs)) { + return true; } } else if (r.getRelation().equals(BinaryRelation.LT)) { ITerm lhs = r.getTerms().get(0); @@ -243,14 +241,49 @@ public class AdHocSemiDecisionProcedure extends AbstractSemiDecisionProcedure { } else if (r.getRelation().equals(BinaryRelation.LE)) { ITerm lhs = r.getTerms().get(0); ITerm rhs = r.getTerms().get(1); - if (lhs instanceof IntConstant && rhs instanceof IntConstant) { - IntConstant x = (IntConstant) lhs; - IntConstant y = (IntConstant) rhs; - return x.getVal().intValue() <= y.getVal().intValue(); + if (isLE(lhs, rhs)) { + return true; } } break; } return false; } + + /** + * do we know a <= b ? + * + * @return false if no or maybe + */ + public boolean isLE(ITerm a, ITerm b) { + + if (a.equals(b)) { + return true; + } + + if (a instanceof IntConstant && b instanceof IntConstant) { + IntConstant ac = (IntConstant) a; + IntConstant bc = (IntConstant) b; + return ac.getVal().intValue() <= bc.getVal().intValue(); + } + if (a instanceof LongConstant && b instanceof LongConstant) { + LongConstant ac = (LongConstant) a; + LongConstant bc = (LongConstant) b; + return ac.getVal().longValue() <= bc.getVal().longValue(); + } + if (a instanceof DoubleConstant && b instanceof DoubleConstant) { + DoubleConstant ac = (DoubleConstant) a; + DoubleConstant bc = (DoubleConstant) b; + return ac.getVal().doubleValue() <= bc.getVal().doubleValue(); + } + if (a instanceof FloatConstant && b instanceof FloatConstant) { + FloatConstant ac = (FloatConstant) a; + FloatConstant bc = (FloatConstant) b; + return ac.getVal().floatValue() <= bc.getVal().floatValue(); + } + + return false; + } + + }