Fixing counting algo

Author: lucaneg

scripts/python/examine_statistics.py

@@ -5,13 +5,11 @@ def calculate_statistics(file_path):
 
     total_opcodes = 0
     total_jumps = 0
-    solved_jumps = 0
-    definitely_unreachable_jumps = 0
-    maybe_unreachable_jumps = 0
-    total_solved_jumps = 0
-    unsound_jumps = 0
-    maybe_unsound_jumps = 0
-    total_solved_percent = 0
+    resolved_jumps = 0
+    unknown_jumps = 0
+    unreachable_jumps = 0
+    erroneous_jumps = 0
+    edges = 0
     time_millis = 0
     rows = 0
 
@@ -22,56 +20,42 @@ def calculate_statistics(file_path):
 
         total_opcodes_index = header.index(" Total Opcodes")
         total_jumps_index = header.index(" Total Jumps")
-        solved_jumps_index = header.index(" Solved Jumps")
-        definitely_unreachable_jumps_index = header.index(" Definitely unreachable jumps")
-        maybe_unreachable_jumps_index = header.index(" Maybe unreachable jumps")
-        total_solved_jumps_index = header.index(" Total solved Jumps")
-        unsound_jumps_index = header.index(" Unsound jumps")
-        maybe_unsound_jumps_index = header.index(" Maybe unsound jumps")
-        total_solved_percent_index = header.index(" % Total Solved")
+        resolved_jumps_index = header.index(" Resolved Jumps")
+        unknown_jumps_index = header.index(" Unknown jumps")
+        unreachable_jumps_index = header.index(" Unreachable jumps")
+        erroneous_jumps_index = header.index(" Erroneous Jumps")
+        edges_index = header.index(" Edges")
         time_millis_index = header.index(" Time (millis)")
-        sound = 0
 
         for row in reader:
-            if int(row[maybe_unreachable_jumps_index]) == 0 and int(row[maybe_unsound_jumps_index]) == 0 and int(row[unsound_jumps_index]) == 0:
-                sound += 1
-                # print(row[header.index("Smart Contract")])
-
             rows += 1
             total_opcodes += int(row[total_opcodes_index])
             total_jumps += int(row[total_jumps_index])
-            solved_jumps += int(row[solved_jumps_index])
-            definitely_unreachable_jumps += int(row[definitely_unreachable_jumps_index])
-            maybe_unreachable_jumps += int(row[maybe_unreachable_jumps_index])
-            total_solved_jumps += int(row[total_solved_jumps_index])
-            unsound_jumps += int(row[unsound_jumps_index])
-            maybe_unsound_jumps += int(row[maybe_unsound_jumps_index])
-            total_solved_percent += float(row[total_solved_percent_index])
+            resolved_jumps += int(row[resolved_jumps_index])
+            unknown_jumps += int(row[unknown_jumps_index])
+            unreachable_jumps += int(row[unreachable_jumps_index])
+            erroneous_jumps += int(row[erroneous_jumps_index])
+            edges += int(row[edges_index])
             time_millis += int(row[time_millis_index])
 
-
-    avg_total_solved_percent = total_solved_percent / rows if rows else None
     avg_time_millis = time_millis / rows if rows else None
-    avg_unsolved = unsound_jumps / total_jumps
+    classified = resolved_jumps + unknown_jumps + unreachable_jumps + erroneous_jumps
 
     print(f"Smart contracts examined: {rows}")
-    print(f"Smart contracts sound: {sound}")
     print(f"Total Opcodes: {total_opcodes}")
     print(f"Total Jumps: {total_jumps}")
-    print(f"Solved (reachable) Jumps: {solved_jumps}")
-    print(f"Total solved Jumps: {total_solved_jumps}")
-    print(f"Definitely unreachable jumps: {definitely_unreachable_jumps}")
-    print(f"Maybe unreachable jumps: {maybe_unreachable_jumps}")
-    print(f"Unsound jumps: {unsound_jumps}")
-    print(f"Maybe unsound jumps: {maybe_unsound_jumps}")
-    print(f"Average % Total unsolved: {percentuale(avg_unsolved)}")
-    print(f"Average % Total Solved: {percentuale(1 - avg_unsolved)}")
+    print(f"Resolved Jumps: {resolved_jumps} ({percentuale(resolved_jumps,total_jumps)}%)")
+    print(f"Unknown jumps: {unknown_jumps} ({percentuale(unknown_jumps,total_jumps)}%)")
+    print(f"Unreachable jumps: {unreachable_jumps} ({percentuale(unreachable_jumps,total_jumps)}%)")
+    print(f"Erroneous jumps: {erroneous_jumps} ({percentuale(erroneous_jumps,total_jumps)}%)")
+    print(f"Total jumps with classification: {classified} ({'match' if classified == total_jumps else 'mismatch'})")
+    print(f"Edges: {edges}")
     print(f"Average Time (seconds): {avg_time_millis / 1000}")
 
-def percentuale(numero_decimale):
-    if numero_decimale is None:
+def percentuale(num, den):
+    if num is None or den is None or den == 0:
         return "N/A"
-    percentuale_str = "{:.4f}%".format(numero_decimale * 100)
+    percentuale_str = "{:.4f}%".format((num/den) * 100)
     return percentuale_str
 
 if __name__ == "__main__":

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

@@ -650,75 +650,59 @@ public static MyLogger dumpStatistics(JumpSolver checker, Set<Statement> soundly
 
 		log.info("### Calculating statistics ###");
 
-		Set<Statement> unreachableJumpNodes = checker.getUnreachableJumps(); // LN: BOTTOM
-
-		int resolved = 0; // LN: RESOLVED
-		int unreachable = 0; // LN: UNREACHABLE
-		int bottom = unreachableJumpNodes.size(); // LN: BOTTOM 
-		int conservative = 0; // LN: CONSERVATIVE
-		final int maybeUnsoundJumps = 0; // checker.getMaybeUnsoundJumps().size();
-
 		if (cfg.getEntrypoints().stream().findAny().isEmpty()) {
 			log.warn("There are no entrypoints.");
 			return null;
 		}
 
 		Statement entryPoint = cfg.getEntrypoints().stream().findAny().get();
+		int total = cfg.getAllJumps().size();
+		int resolved = 0;
+		int unreachable = 0;
+		int erroneous = 0; 
+		int unknown = 0; 
 
 		// we are safe supposing that we have a single entry point
-		for (Statement jumpNode : cfg.getAllJumps()) {
-			if ((jumpNode instanceof Jump) || (jumpNode instanceof Jumpi)) {
-				boolean reachableFrom;
-				int key = cfg.hashCode() + entryPoint.hashCode() + jumpNode.hashCode();
-
-				if (MyCache.getInstance().existsInReachableFrom(key)) {
-					reachableFrom = MyCache.getInstance().isReachableFrom(key); // Caching
-					log.debug("Value cached");
-				} else {
-					reachableFrom = cfg.reachableFrom(entryPoint, jumpNode);
-					MyCache.getInstance().addReachableFrom(key, reachableFrom);
-				}
-
-				Set<StackElement> topStackValuesPerJump = checker.getTopStackValuesPerJump(jumpNode);
-				
-				if (cfg.getAllPushedJumps().contains(jumpNode))
-					resolved++;
-				else if (checker.getMaybeUnsoundJumps().contains(jumpNode))
-					conservative++;
-				else if (checker.getUnreachableJumps().contains(jumpNode) || !reachableFrom || topStackValuesPerJump.isEmpty())
+		for (Statement jumpNode : cfg.getAllJumps()) 
+			if ((jumpNode instanceof Jump) || (jumpNode instanceof Jumpi)) 
+				if (!cfg.reachableFrom(entryPoint, jumpNode) || checker.getUnreachableJumps().contains(jumpNode))
+					// getUnreachableJumps() contains jumps where the whole value state went to bottom
 					unreachable++;
+				else if (checker.getMaybeUnsoundJumps().contains(jumpNode))
+					// getMaybeUnsoundJumps() contains jumps where the whole value state went to top
+					unknown++;
+				else if (cfg.getAllPushedJumps().contains(jumpNode))
+					// stacks of pushed jumps are not stored for optimization
+					resolved++;
 				else {
-					boolean allBot = true, oneTop = false;
-					for (StackElement e : topStackValuesPerJump) {
-						allBot &= e.isBottom();
-						oneTop |= e.isTop();
-					}
-					
-					if (allBot)
-						bottom++;
-					else if (oneTop)
-						conservative++;
+					Set<StackElement> topStacks = checker.getTopStackValuesPerJump(jumpNode);
+					if (topStacks.isEmpty())
+						unreachable++;
+					else if (topStacks.stream().allMatch(StackElement::isBottom))
+						erroneous++;
+					else if (topStacks.stream().anyMatch(StackElement::isTop))
+						unknown++;
 					else
 						resolved++;
 				}
-			}
-		}
 
 		log.info("Total opcodes: {}", cfg.getOpcodeCount());
-		log.info("Total jumps: {}", cfg.getAllJumps().size());
+		log.info("Total jumps: {}", total);
 		log.info("Resolved jumps: {}", resolved);
+		log.info("Unknown jumps: {}", unknown);
 		log.info("Unreachable jumps: {}", unreachable);
-		log.info("Bottom jumps: {}", bottom);
-		log.info("Conservative jumps: {}", conservative);
+		log.info("Erroneous jumps: {}", erroneous);
+		int edges = cfg.getEdgesCount();
+		log.info("Edges: {}", edges);
 
 		return MyLogger.newLogger()
 				.opcodes(cfg.getOpcodeCount())
-				.jumps(cfg.getAllJumps().size())
-				.preciselyResolvedJumps(resolved)
-				.definitelyUnreachableJumps(unreachable)
-				.maybeUnreachableJumps(bottom)
-				.unsoundJumps(conservative)
-				.maybeUnsoundJumps(maybeUnsoundJumps);
+				.jumps(total)
+				.resolvedJumps(resolved)
+				.unreachableJumps(unreachable)
+				.erroneousJumps(erroneous)
+				.unknownJumps(unknown)
+				.edges(edges);
 	}
 
 	/**
@@ -812,10 +796,20 @@ public static void toFile(String FILE_PATH, String stats) {
 				if (!idea.exists()) {
 					FileWriter myWriter = new FileWriter(idea, true);
 
-					String init = "Smart Contract, Total Opcodes, Total Jumps, Solved Jumps, Definitely unreachable jumps, Maybe unreachable jumps, Total solved Jumps, "
-							+ "Unsound jumps, Maybe unsound jumps, % Total Solved, Time (millis), Time lost to get Storage, Actual time, Notes \n";
-
-					myWriter.write(init + stats);
+					String header = "Smart Contract, "
+							+ "Total Opcodes, "
+							+ "Total Jumps, "
+							+ "Resolved Jumps, "
+							+ "Unknown jumps, "
+							+ "Unreachable jumps, "
+							+ "Erroneous Jumps, "
+							+ "Edges, "
+							+ "Time (millis), "
+							+ "Time lost to get Storage, "
+							+ "Actual time, "
+							+ "Notes";
+
+					myWriter.write(header + "\n" + stats);
 					myWriter.close();
 
 				} else {