Restored resolution during analysis

lisa-analyzer · Feb 22, 2024 · 67fe466 · 67fe466
1 parent 0a2c65f
commit 67fe466
Show file tree

Hide file tree

Showing 3 changed files with 71 additions and 57 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 = 100;
+	public static final int STACK_LIMIT = 128;
 	private static final AbstractStack BOTTOM = new AbstractStack(null);
 
 	private final LinkedList<KIntegerSet> stack;

diff --git a/src/main/java/it/unipr/cfg/Jump.java b/src/main/java/it/unipr/cfg/Jump.java
@@ -1,6 +1,13 @@
 package it.unipr.cfg;
 
+import java.math.BigDecimal;
+import java.util.Set;
+import java.util.stream.Collectors;
+
+import it.unipr.analysis.AbstractStack;
+import it.unipr.analysis.AbstractStackSet;
 import it.unipr.analysis.EVMAbstractState;
+import it.unipr.analysis.KIntegerSet;
 import it.unipr.analysis.operator.JumpOperator;
 import it.unive.lisa.analysis.AbstractState;
 import it.unive.lisa.analysis.AnalysisState;
@@ -13,6 +20,7 @@
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.CodeLocation;
 import it.unive.lisa.program.cfg.edge.Edge;
+import it.unive.lisa.program.cfg.edge.TrueEdge;
 import it.unive.lisa.program.cfg.statement.Statement;
 import it.unive.lisa.symbolic.value.Constant;
 import it.unive.lisa.type.Untyped;
@@ -59,33 +67,33 @@ T extends TypeDomain<T>> AnalysisState<A, H, V, T> semantics(
 
 		EVMAbstractState valueState = entryState.getDomainInstance(EVMAbstractState.class);
 		EVMCFG cfg = (EVMCFG) getProgram().getAllCFGs().stream().findAny().get();
-//		Set<Statement> jumpDestinations = cfg.getAllJumpdest();
-//
-//		// If the abstract stack is top or bottom or it is empty, we do not
-//		// have enough information
-//		// to solve the jump.
-//		if (!valueState.isBottom() && !valueState.isTop()) {
-//			AbstractStackSet stacks = valueState.getStacks();
-//
-//			for (AbstractStack a : stacks) {
-//				KIntegerSet stack = a.getTop();
-//				if (!stack.isBottom() && !stack.isTop()) {
-//					Set<Statement> filteredDests = jumpDestinations.stream()
-//							.filter(t -> t.getLocation() instanceof ProgramCounterLocation)
-//							.filter(pc -> stack
-//									.contains(new BigDecimal(((ProgramCounterLocation) pc.getLocation()).getPc())))
-//							.collect(Collectors.toSet());
-//
-//					// For each JUMPDEST, add the missing edge from this node to
-//					// the JUMPDEST.
-//					for (Statement jmp : filteredDests) {
-//						if (!cfg.containsEdge(new TrueEdge(this, jmp))) {
-//							cfg.addEdge(new TrueEdge(this, jmp));
-//						}
-//					}
-//				}
-//			}
-//		}
+		Set<Statement> jumpDestinations = cfg.getAllJumpdest();
+
+		// If the abstract stack is top or bottom or it is empty, we do not
+		// have enough information
+		// to solve the jump.
+		if (!valueState.isBottom() && !valueState.isTop()) {
+			AbstractStackSet stacks = valueState.getStacks();
+
+			for (AbstractStack a : stacks) {
+				KIntegerSet stack = a.getTop();
+				if (!stack.isBottom() && !stack.isTop()) {
+					Set<Statement> filteredDests = jumpDestinations.stream()
+							.filter(t -> t.getLocation() instanceof ProgramCounterLocation)
+							.filter(pc -> stack
+									.contains(new BigDecimal(((ProgramCounterLocation) pc.getLocation()).getPc())))
+							.collect(Collectors.toSet());
+
+					// For each JUMPDEST, add the missing edge from this node to
+					// the JUMPDEST.
+					for (Statement jmp : filteredDests) {
+						if (!cfg.containsEdge(new TrueEdge(this, jmp))) {
+							cfg.addEdge(new TrueEdge(this, jmp));
+						}
+					}
+				}
+			}
+		}
 
 		Constant dummy = new Constant(Untyped.INSTANCE, this.getCFG().getOutgoingEdges(this).size(), getLocation());
 		return entryState.smallStepSemantics(new it.unive.lisa.symbolic.value.UnaryExpression(Untyped.INSTANCE, dummy,

diff --git a/src/main/java/it/unipr/cfg/Jumpi.java b/src/main/java/it/unipr/cfg/Jumpi.java
@@ -1,6 +1,11 @@
 package it.unipr.cfg;
 
+import java.math.BigDecimal;
+import java.util.Set;
+import java.util.stream.Collectors;
+
 import it.unipr.analysis.AbstractStack;
+import it.unipr.analysis.AbstractStackSet;
 import it.unipr.analysis.EVMAbstractState;
 import it.unipr.analysis.KIntegerSet;
 import it.unipr.analysis.operator.JumpiOperator;
@@ -15,6 +20,7 @@
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.CodeLocation;
 import it.unive.lisa.program.cfg.edge.Edge;
+import it.unive.lisa.program.cfg.edge.TrueEdge;
 import it.unive.lisa.program.cfg.statement.Statement;
 import it.unive.lisa.symbolic.value.Constant;
 import it.unive.lisa.type.Untyped;
@@ -59,35 +65,35 @@ T extends TypeDomain<T>> AnalysisState<A, H, V, T> semantics(
 					AnalysisState<A, H, V, T> entryState, InterproceduralAnalysis<A, H, V, T> interprocedural,
 					StatementStore<A, H, V, T> expressions) throws SemanticException {
 		EVMAbstractState valueState = entryState.getDomainInstance(EVMAbstractState.class);
-//		EVMCFG cfg = (EVMCFG) getProgram().getAllCFGs().stream().findAny().get();
-//		Set<Statement> jumpDestinations = cfg.getAllJumpdest();
-//
-//		// If the abstract stack is top or bottom or it is empty, we do not
-//		// have enough information
-//		// to solve the jump.
-//		if (!valueState.isBottom() && !valueState.isTop()) {
-//			AbstractStackSet stacks = valueState.getStacks();
-//
-//			for (AbstractStack a : stacks) {
-//
-//				KIntegerSet stack = a.getTop();
-//				if (!stack.isBottom() && !stack.isTop()) {
-//					Set<Statement> filteredDests = jumpDestinations.stream()
-//							.filter(t -> t.getLocation() instanceof ProgramCounterLocation)
-//							.filter(pc -> stack
-//									.contains(new BigDecimal(((ProgramCounterLocation) pc.getLocation()).getPc())))
-//							.collect(Collectors.toSet());
-//
-//					// For each JUMPDEST, add the missing edge from this node to
-//					// the JUMPDEST.
-//					for (Statement jmp : filteredDests) {
-//						if (!cfg.containsEdge(new TrueEdge(this, jmp))) {
-//							cfg.addEdge(new TrueEdge(this, jmp));
-//						}
-//					}
-//				}
-//			}
-//		}
+		EVMCFG cfg = (EVMCFG) getProgram().getAllCFGs().stream().findAny().get();
+		Set<Statement> jumpDestinations = cfg.getAllJumpdest();
+
+		// If the abstract stack is top or bottom or it is empty, we do not
+		// have enough information
+		// to solve the jump.
+		if (!valueState.isBottom() && !valueState.isTop()) {
+			AbstractStackSet stacks = valueState.getStacks();
+
+			for (AbstractStack a : stacks) {
+
+				KIntegerSet stack = a.getTop();
+				if (!stack.isBottom() && !stack.isTop()) {
+					Set<Statement> filteredDests = jumpDestinations.stream()
+							.filter(t -> t.getLocation() instanceof ProgramCounterLocation)
+							.filter(pc -> stack
+									.contains(new BigDecimal(((ProgramCounterLocation) pc.getLocation()).getPc())))
+							.collect(Collectors.toSet());
+
+					// For each JUMPDEST, add the missing edge from this node to
+					// the JUMPDEST.
+					for (Statement jmp : filteredDests) {
+						if (!cfg.containsEdge(new TrueEdge(this, jmp))) {
+							cfg.addEdge(new TrueEdge(this, jmp));
+						}
+					}
+				}
+			}
+		}
 
 		KIntegerSet b = KIntegerSet.BOTTOM;
 		if (!valueState.isBottom() && !valueState.isTop())