Added stack-size and stack-set-size to the CLI parser

README.md

@@ -68,10 +68,12 @@ This command will initiate the analysis process for the specified smart contract
 
 ```bash
 Options:
- -a,--address <arg>         address of an Ethereum smart contract
- -c,--dump-cfg              dump the CFG
- -d,--dump-analysis <arg>   dump the analysis (html, dot)
- -f,--filepath <arg>        filepath of the Etherem smart contract
- -o,--output <arg>          output directory path
- -s,--dump-stats            dump statistics
+ -a,--address <arg>          address of an Ethereum smart contract
+ -c,--dump-cfg               dump the CFG
+ -d,--dump-analysis <arg>    dump the analysis (html, dot)
+ -f,--filepath <arg>         filepath of the Etherem smart contract
+ -o,--output <arg>           output directory path
+ -q,--stack-size <arg>       dimension of stack
+ -s,--dump-stats             dump statistics
+ -w,--stack-set-size <arg>   dimension of stack-set
 ```

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

@@ -16,6 +16,8 @@
 import org.apache.commons.cli.ParseException;
 import org.apache.commons.lang3.tuple.Triple;
 
+import it.unipr.analysis.AbstractStack;
+import it.unipr.analysis.AbstractStackSet;
 import it.unipr.analysis.EVMAbstractState;
 import it.unipr.analysis.MyLogger;
 import it.unipr.cfg.EVMCFG;
@@ -73,6 +75,14 @@ private void go(String[] args) throws Exception {
 		Option filePathOption = new Option("f", "filepath", true, "filepath of the Etherem smart contract");
 		filePathOption.setRequired(false);
 		options.addOption(filePathOption);
+
+		Option stackSizeOption = new Option("q", "stack-size", true, "dimension of stack");
+		stackSizeOption.setRequired(false);
+		options.addOption(stackSizeOption);
+
+		Option stackSetSizeOption = new Option("w", "stack-set-size", true, "dimension of stack-set");
+		stackSetSizeOption.setRequired(false);
+		options.addOption(stackSetSizeOption);
 
 		// Boolean parameters
 		Option dumpStatisticsOption = Option.builder("s")
@@ -109,10 +119,26 @@ private void go(String[] args) throws Exception {
 		String dumpAnalysis = cmd.getOptionValue("dump-analysis");
 		boolean dumpStatistics = cmd.hasOption("dump-stats");
 		String filepath = cmd.getOptionValue("filepath");
+		String stackSize = cmd.getOptionValue("stack-size");
+		String stackSetSize = cmd.getOptionValue("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);
+		}
 
 		if (addressSC == null && filepath == null) {
 			// Error: no address and no filepath
-			System.out.println("address or filepath required");
+			System.out.println("Address or filepath required");
 			formatter.printHelp("help", options);
 			System.exit(1);
 		}
@@ -175,7 +201,9 @@ else if (dumpAnalysis.equals("html"))
 					"Jumps: " + baseCfg.getAllJumps().size() + "\n" +
 					"PreciselyResolvedJumps: " + pair.getLeft() + "\n" +
 					"SoundResolvedJumps: " + pair.getMiddle() + "\n" +
-					"UnreachableJumps: " + pair.getRight() + "\n" +
+					"DefinitelyUnreachableJumps: " + pair.getRight().getLeft() + "\n" +
+					"MaybeUnreachableJumps: " + pair.getRight().getMiddle() + "\n" +
+					"NotUnreachableJumps: " + pair.getRight().getRight() + "\n" +
 					"Time (in millis): " + (finish - start) + "\n";
 
 			System.out.println(msg2);
@@ -188,9 +216,10 @@ else if (dumpAnalysis.equals("html"))
 						.preciselyResolvedJumps(pair.getLeft())
 						.soundResolvedJumps(pair.getMiddle())
 						.definitelyUnreachableJumps(pair.getRight().getLeft())
-						.definitelyUnreachableJumps(pair.getRight().getMiddle())
+						.maybeUnreachableJumps(pair.getRight().getMiddle())
 						.notSolvedJumps(pair.getRight().getRight())
 						.time(finish - start)
+						.notes("Stack.size: " + AbstractStack.getStackLimit() + " Stack-set.size: " + AbstractStackSet.getStackSetLimit())
 						.build().toString();
 
 				toFileStatistics(msg);
@@ -282,7 +311,7 @@ else if (!cfg.reachableFrom(entryPoint, jumpNode))
 	 */
 	private void toFileStatistics(String stats) {
 		synchronized (STATISTICS_FULLPATH) {
-			String init = "Smart Contract, Total Opcodes, Total Jumps, Precisely solved Jumps, Sound solved Jumps, Unreachable Jumps, Total solved Jumps, % Precisely Solved, % Total Solved, Time (millis), Thread, Notes \n";
+			String init = "Smart Contract, Total Opcodes, Total Jumps, Precisely solved Jumps, Sound solved Jumps, Definitely unreachable jumps, Maybe unreachable jumps, Total solved Jumps, Not solved jumps, % Total Solved, Time (millis), Thread, Notes \n";
 			try {
 				File idea = new File(STATISTICS_FULLPATH);
 				if (!idea.exists()) {
@@ -310,7 +339,7 @@ private void toFileStatistics(String stats) {
 	 */
 	private void toFileFailure(String stats) {
 		synchronized (FAILURE_FULLPATH) {
-			String init = "Smart Contract, Total Opcodes, Total Jumps, Precisely solved Jumps, Sound solved Jumps, Unreachable Jumps, Total solved Jumps, % Precisely Solved, % Total Solved, Time (millis), Thread, Notes \n";
+			String init = "Smart Contract, Total Opcodes, Total Jumps, Precisely solved Jumps, Sound solved Jumps, Definitely unreachable jumps, Maybe unreachable jumps, Total solved Jumps, Not solved jumps, % Total Solved, Time (millis), Thread, Notes \n";
 			try {
 				File idea = new File(FAILURE_FULLPATH);
 				if (!idea.exists()) {

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

@@ -17,7 +17,8 @@
 import java.util.function.Predicate;
 
 public class AbstractStack implements ValueDomain<AbstractStack>, BaseLattice<AbstractStack> {
-	private static int STACK_LIMIT = 128;
+
+	private static int STACK_LIMIT = 150;
 	private static final AbstractStack BOTTOM = new AbstractStack(null);
 
 	private final LinkedList<KIntegerSet> stack;

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

@@ -9,8 +9,7 @@
 
 public class AbstractStackSet extends SetLattice<AbstractStackSet, AbstractStack> {
 
-
-	private static int SIZE = 50;
+	private static int SIZE = 80;
 	private static final AbstractStackSet BOTTOM = new AbstractStackSet(null, false);
 	private static final AbstractStackSet TOP = new AbstractStackSet(Collections.emptySet(), true);
 
@@ -109,4 +108,8 @@ public String toString2() {
 	public static void setStackSetSize(int n) {
 		SIZE = n;
 	}
+
+	public static int getStackSetLimit() {
+		return SIZE;
+	}
 }