Using maybe unsound jumps to saturate edge set

Author: lucaneg

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

@@ -35,6 +35,8 @@
 import org.apache.commons.cli.Option;
 import org.apache.commons.cli.Options;
 import org.apache.commons.cli.ParseException;
+import org.apache.commons.collections4.SetUtils;
+import org.apache.commons.collections4.SetUtils.SetView;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
@@ -696,18 +698,22 @@ private static Set<Statement> getSoundlySolvedJumps(JumpSolver checker, LiSA lis
 				fixpoint = false;
 				EVMCFG cfg = checker.getComputedCFG();
 				Set<Statement> jumpdestNodes = cfg.getAllJumpdest();
-				for (Statement unsoundNode : checker.getUnsoundJumps())
+				Set<Statement> unsoundJumps = checker.getUnsoundJumps();
+				Set<Statement> maybeUnsoundJumps = checker.getMaybeUnsoundJumps();
+				Set<Statement> unsound = unsoundJumps == null ? Collections.emptySet() : unsoundJumps;
+				unsound = maybeUnsoundJumps == null ? unsound : SetUtils.union(unsound, maybeUnsoundJumps);
+				for (Statement unsoundNode : unsound)
 					if (!soundlySolved.contains(unsoundNode)) {
 						fixpoint = true;
 						for (Statement jumpdest : jumpdestNodes)
 							cfg.addEdge(new SequentialEdge(unsoundNode, jumpdest));
 					}
 
-				soundlySolved.addAll(checker.getUnsoundJumps());
+				soundlySolved.addAll(unsound);
 
 				program.addCodeMember(cfg);
 				lisa.run(program);
-			} while (fixpoint && checker.getUnsoundJumps() != null && ++currentIteration < MAX_ITER);
+			} while (fixpoint && ++currentIteration < MAX_ITER);
 		}
 		return soundlySolved;
 	}

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

@@ -75,18 +75,37 @@ public EVMCFG getComputedCFG() {
 		return cfgToAnalyze;
 	}
 
+	/**
+	 * Yields the jumps where the whole value state is bottom (i.e., the jump is
+	 * unreachable).
+	 * @return the set of unreachable jumps
+	 */
 	public Set<Statement> getUnreachableJumps() {
 		return unreachableJumps;
 	}
 
+	/**
+	 * Yields the jumps where the whole value state is top (i.e., the jump is
+	 * maybe unsound).
+	 * @return the set of maybe unsound jumps
+	 */
 	public Set<Statement> getMaybeUnsoundJumps() {
 		return maybeUnsoundJumps;
 	}
 
+	/**
+	 * Yields the jumps where at least one of the top stack values is top (i.e., the jump is
+	 * unsound).
+	 * @return the set of unsound jumps
+	 */
 	public Set<Statement> getUnsoundJumps() {
 		return unsoundJumps;
 	}
 
+	/**
+	 * The set of top stack values per jump. This only exists for jumps that are
+	 * not in {@link #getMaybeUnsoundJumps()} and {@link #getUnreachableJumps()}.
+	 */
 	public Set<StackElement> getTopStackValuesPerJump(Statement node) {
 		return topStackValuesPerJump.get(node);
 	}