Minor changes and spotlessApply

src/main/java/it/unipr/EVMLiSA.java

@@ -46,13 +46,13 @@
 import org.apache.commons.lang3.tuple.Triple;
 
 public class EVMLiSA {
-	private static String OUTPUT_DIR = "execution/results/";
+	private String OUTPUT_DIR = "execution/results";
 
 	// Path
-	private String STATISTICS_FULLPATH = OUTPUT_DIR + "statistics.csv";
-	private final String STATISTICSZEROJUMP_FULLPATH = OUTPUT_DIR + "statisticsZeroJumps.csv";
-	private String FAILURE_FULLPATH = OUTPUT_DIR + "failure.csv";
-	private final String LOGS_FULLPATH = OUTPUT_DIR + "logs.txt";
+	private String STATISTICS_FULLPATH = OUTPUT_DIR + "/statistics.csv";
+	private String STATISTICSZEROJUMP_FULLPATH = OUTPUT_DIR + "/statisticsZeroJumps.csv";
+	private String FAILURE_FULLPATH = OUTPUT_DIR + "/failure.csv";
+	private String LOGS_FULLPATH = OUTPUT_DIR + "/logs.txt";
 	private String SMARTCONTRACTS_FULLPATH = "";
 
 	// Statistics
@@ -62,6 +62,7 @@ public class EVMLiSA {
 	private int CORES;
 	private long startOfExecutionTime = 0;
 	private String init = "Smart Contract, Total Opcodes, Total Jumps, Solved Jumps, Definitely unreachable jumps, Maybe unreachable jumps, Total solved Jumps, Not solved jumps, % Total Solved, Time (millis), Notes \n";
+
 	/**
 	 * Generates a control flow graph (represented as a LiSA {@code Program})
 	 * from a EVM bytecode smart contract and runs the analysis on it.
@@ -106,7 +107,7 @@ private void go(String[] args) throws Exception {
 		Option benchmarkOption = new Option("b", "benchmark", true, "filepath of the benchmark");
 		benchmarkOption.setRequired(false);
 		options.addOption(benchmarkOption);
-		
+
 		Option coresOption = new Option("C", "cores", true, "number of cores used");
 		coresOption.setRequired(false);
 		options.addOption(coresOption);
@@ -150,26 +151,38 @@ private void go(String[] args) throws Exception {
 		String stackSetSize = cmd.getOptionValue("stack-set-size");
 		String benchmark = cmd.getOptionValue("benchmark");
 		String coresOpt = cmd.getOptionValue("cores");
-
+
+		// --cores
 		if (coresOpt != null && Integer.parseInt(coresOpt) > 0)
 			CORES = Integer.parseInt(coresOpt);
 		else
 			CORES = 1;
 
+		// --stack-size & --stack-set-size
 		try {
 			if (stackSize != null && Integer.parseInt(stackSize) > 0)
 				AbstractStack.setStackLimit(Integer.parseInt(stackSize));
 
 			if (stackSetSize != null && Integer.parseInt(stackSetSize) > 0)
 				AbstractStackSet.setStackSetSize(Integer.parseInt(stackSetSize));
-			
+
 		} catch (NumberFormatException e) {
 			System.out.println("Size must be an integer");
 			formatter.printHelp("help", options);
 
 			System.exit(1);
 		}
-
+
+		// --output
+		if (outputDir != null) {
+			OUTPUT_DIR = outputDir;
+			STATISTICS_FULLPATH = OUTPUT_DIR + "/statistics.csv";
+			STATISTICSZEROJUMP_FULLPATH = OUTPUT_DIR + "/statisticsZeroJumps.csv";
+			FAILURE_FULLPATH = OUTPUT_DIR + "/failure.csv";
+			LOGS_FULLPATH = OUTPUT_DIR + "/logs.txt";
+		}
+
+		// --benchmark
 		if (benchmark != null) {
 			Files.createDirectories(Paths.get(OUTPUT_DIR));
 			SMARTCONTRACTS_FULLPATH = benchmark;
@@ -192,7 +205,7 @@ private void go(String[] args) throws Exception {
 		Files.createDirectories(Paths.get(OUTPUT_DIR));
 
 		if (outputDir == null)
-			outputDir = OUTPUT_DIR + addressSC + "_REPORT";
+			outputDir = OUTPUT_DIR + "/" + addressSC + "_REPORT";
 
 		STATISTICS_FULLPATH = OUTPUT_DIR + addressSC + "_STATISTICS" + ".csv";
 		FAILURE_FULLPATH = OUTPUT_DIR + addressSC + "_FAILURE" + ".csv";
@@ -327,7 +340,7 @@ private MyLogger newAnalysis(String CONTRACT_ADDR) throws Exception {
 		conf.abstractState = new SimpleAbstractState<>(new MonolithicHeap(), new EVMAbstractState(),
 				new TypeEnvironment<>(new InferredTypes()));
 		conf.jsonOutput = true;
-		conf.workdir = OUTPUT_DIR + "benchmark/" + CONTRACT_ADDR;
+		conf.workdir = OUTPUT_DIR + "/benchmark/" + CONTRACT_ADDR;
 		conf.interproceduralAnalysis = new ModularWorstCaseAnalysis<>();
 		JumpSolver checker = new JumpSolver();
 		conf.semanticChecks.add(checker);
@@ -447,6 +460,7 @@ public void run() {
 					threads[i] = new Thread(runnable);
 					threads[i].start();
 					threadsStarted++;
+					Runtime.getRuntime().gc(); // Force Java Garbage Collection
 				}
 
 				try {
@@ -491,11 +505,11 @@ public void run() {
 			msg += "Stack size = " + AbstractStack.getStackLimit() + "\n";
 			msg += "Stack set size = " + AbstractStackSet.getStackSetLimit() + "\n";
 			msg += "\n"; // Blank line
-			
+
 			msg += "Heap size: " + new Converter().getSize(Runtime.getRuntime().totalMemory()) + "\n";
 			msg += "Heap Max size: " + new Converter().getSize(Runtime.getRuntime().maxMemory()) + "\n";
 			msg += "\n"; // Blank line
-					
+
 			System.out.println(msg);
 			toFileLogs(msg);
 
@@ -817,7 +831,7 @@ private String buildMessage(String type, String address, int smartContractsSize,
 	private String now() {
 		return DATE_FORMAT.format(System.currentTimeMillis());
 	}
-	
+
 	/**
 	 * Saves smart contracts bytecode from Etherscan.
 	 * <p>
@@ -869,13 +883,13 @@ private void saveSmartContractsFromEtherscan() throws Exception {
 			}
 		}
 	}
-	
-	public class Converter{
-	    long kilo = 1024;
-	    long mega = kilo * kilo;
-	    long giga = mega * kilo;
-	    long tera = giga * kilo;
-	    
+
+	public class Converter {
+		long kilo = 1024;
+		long mega = kilo * kilo;
+		long giga = mega * kilo;
+		long tera = giga * kilo;
+
 //	    public static void main(String[] args) {
 //	        for (String arg: args) {
 //	            try {
@@ -885,26 +899,26 @@ public class Converter{
 //	            }
 //	        }
 //	    }
-	    
-	    public String getSize(long size) {
-	        String s = "";
-	        double kb = (double)size / kilo;
-	        double mb = kb / kilo;
-	        double gb = mb / kilo;
-	        double tb = gb / kilo;
-	        if(size < kilo) {
-	            s = size + " Bytes";
-	        } else if(size >= kilo && size < mega) {
-	            s =  String.format("%.2f", kb) + " KB";
-	        } else if(size >= mega && size < giga) {
-	            s = String.format("%.2f", mb) + " MB";
-	        } else if(size >= giga && size < tera) {
-	            s = String.format("%.2f", gb) + " GB";
-	        } else if(size >= tera) {
-	            s = String.format("%.2f", tb) + " TB";
-	        }
-	        return s;
-	    }
+
+		public String getSize(long size) {
+			String s = "";
+			double kb = (double) size / kilo;
+			double mb = kb / kilo;
+			double gb = mb / kilo;
+			double tb = gb / kilo;
+			if (size < kilo) {
+				s = size + " Bytes";
+			} else if (size >= kilo && size < mega) {
+				s = String.format("%.2f", kb) + " KB";
+			} else if (size >= mega && size < giga) {
+				s = String.format("%.2f", mb) + " MB";
+			} else if (size >= giga && size < tera) {
+				s = String.format("%.2f", gb) + " GB";
+			} else if (size >= tera) {
+				s = String.format("%.2f", tb) + " TB";
+			}
+			return s;
+		}
 	}
 
 }

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

@@ -10,7 +10,6 @@
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.symbolic.value.Identifier;
 import it.unive.lisa.symbolic.value.ValueExpression;
-
 import java.util.Collections;
 import java.util.Iterator;
 import java.util.LinkedList;
@@ -31,8 +30,8 @@ public class AbstractStack implements ValueDomain<AbstractStack>, BaseLattice<Ab
 	public AbstractStack() {
 		this.stack = new LinkedList<KIntegerSet>(Collections.nCopies(STACK_LIMIT, KIntegerSet.BOTTOM));
 
-		//		for (int i = 0; i < STACK_LIMIT; i++)
-		//			stack.add(KIntegerSet.BOTTOM);
+		// for (int i = 0; i < STACK_LIMIT; i++)
+		// stack.add(KIntegerSet.BOTTOM);
 	}
 
 	/**
@@ -142,7 +141,9 @@ public AbstractStack top() {
 
 		for (int i = 0; i < STACK_LIMIT; i++)
 			result.addLast(KIntegerSet.TOP);
-		//		LinkedList<KIntegerSet> result = new LinkedList<KIntegerSet>(Collections.nCopies(STACK_LIMIT, KIntegerSet.TOP));
+		// LinkedList<KIntegerSet> result = new
+		// LinkedList<KIntegerSet>(Collections.nCopies(STACK_LIMIT,
+		// KIntegerSet.TOP));
 
 		return new AbstractStack(result);
 	}
@@ -157,9 +158,10 @@ public boolean isTop() {
 		if (isBottom())
 			return false;
 		else if (this.stack.stream()
-				.anyMatch(element -> !element.isTop())) 
+				.anyMatch(element -> !element.isTop()))
 			return false;
-		else return true;	
+		else
+			return true;
 	}
 
 	@Override
@@ -214,7 +216,7 @@ else if (isTop())
 
 	private static LinkedList<KIntegerSet> clone(LinkedList<KIntegerSet> list) {
 		LinkedList<KIntegerSet> result = new LinkedList<>();
-		for (KIntegerSet item : list) 
+		for (KIntegerSet item : list)
 			result.add(item.copy());
 
 		return result;

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

@@ -61,7 +61,7 @@ public AbstractStackSet clone() {
 			return TOP;
 		else if (isBottom())
 			return BOTTOM;
-	    return new AbstractStackSet(new HashSet<>(this.elements), false);
+		return new AbstractStackSet(new HashSet<>(this.elements), false);
 
 //		AbstractStackSet result = new AbstractStackSet(new HashSet<AbstractStack>(), false);
 //		for (AbstractStack stack : elements())

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

@@ -17,9 +17,7 @@
 import it.unive.lisa.symbolic.value.ValueExpression;
 import it.unive.lisa.symbolic.value.operator.unary.LogicalNegation;
 import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator;
-import java.math.BigDecimal;
 import java.math.BigInteger;
-import java.math.RoundingMode;
 import java.util.HashSet;
 import java.util.LinkedList;
 import java.util.List;

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

@@ -1,18 +1,17 @@
 package it.unipr.analysis;
 
+import it.unive.lisa.analysis.SemanticException;
+import it.unive.lisa.analysis.lattices.SetLattice;
 import java.math.BigInteger;
 import java.util.Collections;
 import java.util.HashSet;
 import java.util.Set;
 
-import it.unive.lisa.analysis.SemanticException;
-import it.unive.lisa.analysis.lattices.SetLattice;
-
 public class KIntegerSet extends SetLattice<KIntegerSet, BigInteger> {
 	private static final BigInteger ZERO_INT = BigInteger.valueOf(0);
-	private static final BigInteger ONE_INT = BigInteger.valueOf(1);	
+	private static final BigInteger ONE_INT = BigInteger.valueOf(1);
 	private static final BigInteger MAX = BigInteger.valueOf((long) Math.pow(2, 256));
-	
+
 	public static final int K = 2;
 
 	public static final KIntegerSet ZERO = new KIntegerSet(0);
@@ -22,7 +21,6 @@ public class KIntegerSet extends SetLattice<KIntegerSet, BigInteger> {
 	public static final KIntegerSet TOP = new KIntegerSet(Collections.emptySet(), true);
 	public static final KIntegerSet BOTTOM = new KIntegerSet(Collections.emptySet(), false);
 
-
 	public KIntegerSet(BigInteger i) {
 		this(Collections.singleton(i), false);
 	}
@@ -148,7 +146,7 @@ public KIntegerSet copy() {
 			return bottom();
 		else if (isTop())
 			return top();
-		return this; //new KIntegerSet(this.elements());
+		return this; // new KIntegerSet(this.elements());
 	}
 
 	public KIntegerSet mul(KIntegerSet other) {

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

@@ -1,11 +1,10 @@
 package it.unipr.analysis;
 
+import it.unive.lisa.analysis.lattices.FunctionalLattice;
 import java.math.BigInteger;
 import java.util.HashMap;
 import java.util.Map;
 
-import it.unive.lisa.analysis.lattices.FunctionalLattice;
-
 public class Memory extends FunctionalLattice<Memory, BigInteger, KIntegerSet> {
 
 	/**

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

@@ -1,10 +1,5 @@
 package it.unipr.checker;
 
-import java.math.BigInteger;
-import java.util.HashSet;
-import java.util.Set;
-import java.util.stream.Collectors;
-
 import it.unipr.analysis.EVMAbstractState;
 import it.unipr.analysis.KIntegerSet;
 import it.unipr.cfg.EVMCFG;
@@ -30,6 +25,10 @@
 import it.unive.lisa.program.cfg.edge.SequentialEdge;
 import it.unive.lisa.program.cfg.edge.TrueEdge;
 import it.unive.lisa.program.cfg.statement.Statement;
+import java.math.BigInteger;
+import java.util.HashSet;
+import java.util.Set;
+import java.util.stream.Collectors;
 
 /**
  * A semantic checker that aims at solving JUMP and JUMPI destinations by