Optimized representation and spotlessApply

src/main/java/it/unipr/analysis/AbstractStack.java

@@ -90,12 +90,27 @@ public DomainRepresentation representation() {
 		else if (isTop())
 			return Lattice.topRepresentation();
 
-		return new StringRepresentation(stack);
+		return new StringRepresentation(this.toString());
 	}
 
 	@Override
 	public String toString() {
-		return stack.toString();
+		String result = "{";
+
+		for (int i = STACK_LIMIT - size(); i < STACK_LIMIT; i++) {
+			if (stack.get(i).isBottom())
+				result += Lattice.bottomRepresentation();
+			else if (stack.get(i).isBottom())
+				result += Lattice.topRepresentation();
+			else
+				result += stack.get(i);
+
+			if ((i + 1) != STACK_LIMIT)
+				result += ", ";
+		}
+
+		result += "}";
+		return result;
 	}
 
 	@Override

src/main/java/it/unipr/analysis/AbstractStackSet.java

@@ -1,12 +1,12 @@
 package it.unipr.analysis;
 
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.lattices.SetLattice;
 import java.util.Collections;
 import java.util.HashSet;
+import java.util.Iterator;
 import java.util.Set;
 
-import it.unive.lisa.analysis.SemanticException;
-import it.unive.lisa.analysis.lattices.SetLattice;
-
 public class AbstractStackSet extends SetLattice<AbstractStackSet, AbstractStack> {
 
 	private static final AbstractStackSet BOTTOM = new AbstractStackSet(null, false);
@@ -88,4 +88,19 @@ public boolean equals(Object obj) {
 	public AbstractStackSet mk(Set<AbstractStack> set) {
 		return new AbstractStackSet(set, false);
 	}
+
+	public String toString2() {
+		String result = "{";
+		Iterator<AbstractStack> it = elements.iterator();
+
+		while (it.hasNext()) {
+			result += it.next().toString();
+			if (it.hasNext())
+				result += ", ";
+		}
+
+		result += "}";
+
+		return result;
+	}
 }

src/main/java/it/unipr/analysis/EVMAbstractState.java

@@ -954,9 +954,9 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
 					for (AbstractStack stack : stacks) {
 						AbstractStack resultStack = stack.clone();
 						KIntegerSet new_mu_i = null;
-						
+
 						KIntegerSet offset = resultStack.pop();
-						
+
 						if (mu_i.equals(KIntegerSet.ZERO)) {
 							// This is an error. We cannot read from memory if
 							// there is no active words saved
@@ -1807,7 +1807,8 @@ else if (isTop())
 			return Lattice.topRepresentation();
 
 		// TODO to create a more optimized version
-		return new StringRepresentation("{ stacks: " + stacks + ", memory: " + memory + ", mu_i: " + mu_i + " }");
+		return new StringRepresentation(
+				"{ stacks: " + stacks.toString2() + ", memory: " + memory + ", mu_i: " + mu_i + " }");
 	}
 
 	@Override

src/main/java/it/unipr/cfg/Jump.java

@@ -1,9 +1,6 @@
 package it.unipr.cfg;
 
-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;
@@ -16,14 +13,10 @@
 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;
 import it.unive.lisa.util.datastructures.graph.GraphVisitor;
-import java.math.BigDecimal;
-import java.util.Set;
-import java.util.stream.Collectors;
 
 /**
  * Jump opcode of the program to analyze.

src/main/java/it/unipr/cfg/Jumpi.java

@@ -1,7 +1,6 @@
 package it.unipr.cfg;
 
 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;
@@ -16,14 +15,10 @@
 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;
 import it.unive.lisa.util.datastructures.graph.GraphVisitor;
-import java.math.BigDecimal;
-import java.util.Set;
-import java.util.stream.Collectors;
 
 /**
  * Jumpi opcode of the program to analyze.

src/main/java/it/unipr/checker/JumpSolver.java

@@ -170,7 +170,12 @@ public boolean visit(
 
 			for (KIntegerSet topStack : valueState.getTop()) {
 				if (topStack.isBottom()) {
-					this.unreachableJumps.add(node); // FIXME: this is wrong: a jump is unreachable if all the top of the stacks are bottom or do not contain jump dest
+					this.unreachableJumps.add(node); // FIXME: this is wrong: a
+														// jump is unreachable
+														// if all the top of the
+														// stacks are bottom or
+														// do not contain jump
+														// dest
 					continue;
 				} else if (topStack.isTop()) {
 					System.err.println("Not solved jump (top of the stack is top): " + node + "["
@@ -183,11 +188,16 @@ public boolean visit(
 						.filter(pc -> topStack
 								.contains(new BigDecimal(((ProgramCounterLocation) pc.getLocation()).getPc())))
 						.collect(Collectors.toSet());
-				
+
 				// If there are no JUMPDESTs for this value, skip to the
 				// next one.
 				if (filteredDests.isEmpty()) {
-					this.unreachableJumps.add(node); // FIXME: this is wrong: a jump is unreachable if all the top of the stacks do not contains jump dests or are bottom
+					this.unreachableJumps.add(node); // FIXME: this is wrong: a
+														// jump is unreachable
+														// if all the top of the
+														// stacks do not
+														// contains jump dests
+														// or are bottom
 					continue;
 				}
 

src/test/java/it/unipr/analysis/cron/EVMBytecodeControlFlowStructureTest.java

@@ -70,7 +70,7 @@ public void testIfElse() throws AnalysisSetupException, IOException {
 
 	@Test
 	public void testWhile() throws AnalysisSetupException, IOException {
-		CronConfiguration conf = createConfiguration("cfs/while", "while_eth.sol", false);
+		CronConfiguration conf = createConfiguration("cfs/while", "while_eth.sol", true);
 		perform(conf);
 	}
 

src/test/java/it/unipr/analysis/cron/EVMBytecodeTest.java

@@ -62,7 +62,7 @@ public void testSCFromEtherscan() throws Exception {
 		String SC_ADDRESS = "0xb0b14701a4bbAD3Ac093621008E11247e67B8368";
 		toFileStatistics(newAnalysis(SC_ADDRESS).toString());
 	}
-	
+
 	public static void main(String[] args) throws Exception {
 		new EVMBytecodeTest().testEVMBytecodeAnalysisMultiThread();
 	}