Merge pull request #16 from lisa-analyzer/assume-jumpi

`assume` method for `JUMPI`
lisa-analyzer · Feb 12, 2024 · 5344f95 · 5344f95
2 parents ec2630b + 912d4a7
commit 5344f95
Show file tree

Hide file tree

Showing 2 changed files with 47 additions and 15 deletions.
diff --git a/src/main/java/it/unipr/analysis/EVMAbstractState.java b/src/main/java/it/unipr/analysis/EVMAbstractState.java
@@ -1083,15 +1083,13 @@ public EVMAbstractState assume(ValueExpression expression, ProgramPoint src, Pro
 					result.pop();
 					KIntegerSet condition = result.pop();
 
-					if (condition.equals(KIntegerSet.ZERO)) {
-						// Condition is surely false (interval [0,0])
-						// Return BOTTOM
+					if (condition.isDefinitelyFalse()) {
+						// if condition is surely false, return bottom
 						return bottom();
-					} else if (condition.equals(KIntegerSet.ONE)) {
-						// Condition is surely true (interval [1,1])
-						// Return the result
+					} else if (condition.isDefinitelyTrue()) {
+						// if condition is surely true, return the result
 						return new EVMAbstractState(result, memory, mu_i);
-					} else if (condition.equals(KIntegerSet.ZERO_OR_ONE)) {
+					} else if (condition.isUnknown()) {
 						// Condition could be either true or false
 						// Return the result
 						return new EVMAbstractState(result, memory, mu_i);
@@ -1111,15 +1109,15 @@ public EVMAbstractState assume(ValueExpression expression, ProgramPoint src, Pro
 							result.pop();
 							KIntegerSet condition = result.pop();
 
-							if (condition.equals(KIntegerSet.ZERO)) {
-								// Condition is surely false (interval [0,0])
-								// Return the result
+							if (condition.isDefinitelyFalse()) {
+								// if condition is surely false, return the
+								// result
 								return new EVMAbstractState(result, memory, mu_i);
-							} else if (condition.equals(KIntegerSet.ONE)) {
-								// Condition is surely true (interval [1,1])
-								// Return BOTTOM
+							} else if (condition.isDefinitelyTrue()) {
+								// if condition is surely true, return the
+								// bottom
 								return bottom();
-							} else if (condition.equals(KIntegerSet.ZERO_OR_ONE)) {
+							} else if (condition.isUnknown()) {
 								// Condition could be either true or false
 								// Return the result
 								return new EVMAbstractState(result, memory, mu_i);

diff --git a/src/main/java/it/unipr/analysis/KIntegerSet.java b/src/main/java/it/unipr/analysis/KIntegerSet.java
@@ -15,7 +15,6 @@ public class KIntegerSet extends SetLattice<KIntegerSet, BigDecimal> {
 
 	public static final KIntegerSet ZERO = new KIntegerSet(0);
 	public static final KIntegerSet ONE = new KIntegerSet(1);
-	public static final KIntegerSet MINUS_ONE = new KIntegerSet(-1);
 	public static final KIntegerSet ZERO_OR_ONE = new KIntegerSet(0, 1);
 
 	public static final KIntegerSet TOP = new KIntegerSet(Collections.emptySet(), true);
@@ -604,4 +603,39 @@ public static byte[] shiftArithmeticRight(byte[] byteArray, int shiftBitCount) {
 		}
 		return byteArray;
 	}
+
+	/**
+	 * Checks whether this set it is definitely evaluated to {@code true}, i.e.,
+	 * if it does not contains zero.
+	 * 
+	 * @return {@code true} if this set does not contains zero, {@code false}
+	 *             otherwise.
+	 */
+	public boolean isDefinitelyTrue() {
+		if (isTop() || isBottom())
+			return false;
+		return !this.elements().contains(new BigDecimal(0));
+	}
+
+	/**
+	 * Checks whether this set it is definitely evaluated to {@code false},
+	 * i.e., if it is equal to zero.
+	 * 
+	 * @return {@code true} if this set is zero, {@code false} otherwise.
+	 */
+	public boolean isDefinitelyFalse() {
+		if (isTop() || isBottom())
+			return false;
+		return this.equals(ZERO);
+	}
+
+	/**
+	 * Checks whether the Boolean value of this set cannot be determined.
+	 * 
+	 * @return {@code true} if the Boolean value of this set cannot be
+	 *             determined, {@code false} otherwise
+	 */
+	public boolean isUnknown() {
+		return isTop() || (!isBottom() && !isDefinitelyFalse() && !isDefinitelyTrue());
+	}
 }