Increased stack and integer set limits (previous limits, 0.90)

lisa-analyzer · Feb 13, 2024 · 58eab0d · 58eab0d
1 parent fae1372
commit 58eab0d
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 6 deletions.
diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java
@@ -17,7 +17,7 @@
 import java.util.function.Predicate;
 
 public class AbstractStack implements ValueDomain<AbstractStack>, BaseLattice<AbstractStack> {
-	public static final int STACK_LIMIT = 64;
+	public static final int STACK_LIMIT = 72;
 	private static final AbstractStack BOTTOM = new AbstractStack(null);
 
 	private final LinkedList<KIntegerSet> stack;

diff --git a/src/main/java/it/unipr/analysis/EVMAbstractState.java b/src/main/java/it/unipr/analysis/EVMAbstractState.java
@@ -305,8 +305,8 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
 					// Above, operators that do not perform pop()
 
 					// from here on, top is propagated
-					if (isTop())
-						return this;
+//					if (isTop())
+//						return this;
 
 					// Below, operators that perform pop operation on the stack
 					switch (op.getClass().getSimpleName()) {
@@ -985,7 +985,8 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
 
 		if (!(expression instanceof Skip))
 			throw new SemanticException("Reachable just with the skip node");
-		return this;
+
+		return top();
 	}
 
 	/**

diff --git a/src/main/java/it/unipr/analysis/KIntegerSet.java b/src/main/java/it/unipr/analysis/KIntegerSet.java
@@ -11,7 +11,7 @@
 
 public class KIntegerSet extends SetLattice<KIntegerSet, BigDecimal> {
 	private static final BigDecimal MAX = new BigDecimal(Math.pow(2, 256));
-	public static final int K = 4;
+	public static final int K = 15;
 
 	public static final KIntegerSet ZERO = new KIntegerSet(0);
 	public static final KIntegerSet ONE = new KIntegerSet(1);

diff --git a/src/main/java/it/unipr/checker/JumpSolver.java b/src/main/java/it/unipr/checker/JumpSolver.java
@@ -176,7 +176,10 @@ public boolean visit(
 			}
 
 			KIntegerSet topStack = valueState.getTop();
-			if (topStack.isTop() || topStack.isBottom()) {
+			if (topStack.isBottom()) {
+				this.unreachableJumps.add(node);
+				continue;
+			} else if (topStack.isTop()) {
 				System.err.println(((ProgramCounterLocation) node.getLocation()).getSourceCodeLine() + " "
 						+ valueState.getStack());
 				continue;