diff --git a/src/main/java/it/unipr/EVMLiSA.java b/src/main/java/it/unipr/EVMLiSA.java index 4edd45feb..e69b3a583 100644 --- a/src/main/java/it/unipr/EVMLiSA.java +++ b/src/main/java/it/unipr/EVMLiSA.java @@ -650,15 +650,13 @@ public static MyLogger dumpStatistics(JumpSolver checker, Set soundly log.info("### Calculating statistics ###"); - Set unreachableJumpNodes = checker.getUnreachableJumps(); + Set unreachableJumpNodes = checker.getUnreachableJumps(); // LN: BOTTOM - int resolvedJumps = 0; - int definitelyUnreachable = 0; - int maybeUnreachable = 0; - int unsoundJumps = 0; - int maybeUnsoundJumps = 0; // checker.getMaybeUnsoundJumps().size(); - - boolean allJumpAreSound = true; + 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."); @@ -666,20 +664,6 @@ public static MyLogger dumpStatistics(JumpSolver checker, Set soundly } Statement entryPoint = cfg.getEntrypoints().stream().findAny().get(); - Set pushedJumps = cfg.getAllPushedJumps(); - - if (!JumpSolver.getLinkUnsoundJumpsToAllJumpdest()) - for (Statement jumpNode : cfg.getAllJumps()) { - if (pushedJumps.contains(jumpNode)) - continue; - - Set topStackValuesPerJump = checker.getTopStackValuesPerJump(jumpNode); - - if (topStackValuesPerJump != null && topStackValuesPerJump.contains(StackElement.NUMERIC_TOP)) { - allJumpAreSound = false; - break; - } - } // we are safe supposing that we have a single entry point for (Statement jumpNode : cfg.getAllJumps()) { @@ -696,65 +680,44 @@ public static MyLogger dumpStatistics(JumpSolver checker, Set soundly } Set topStackValuesPerJump = checker.getTopStackValuesPerJump(jumpNode); - - if (pushedJumps.contains(jumpNode)) { - resolvedJumps++; - continue; - } - if (reachableFrom && unreachableJumpNodes.contains(jumpNode)) { - definitelyUnreachable++; - continue; - } - if (!reachableFrom) { - if (allJumpAreSound) - definitelyUnreachable++; + + if (cfg.getAllPushedJumps().contains(jumpNode)) + resolved++; + else if (checker.getMaybeUnsoundJumps().contains(jumpNode)) + conservative++; + else if (checker.getUnreachableJumps().contains(jumpNode) || !reachableFrom || topStackValuesPerJump.isEmpty()) + unreachable++; + else { + boolean allBot = true, oneTop = false; + for (StackElement e : topStackValuesPerJump) { + allBot &= e.isBottom(); + oneTop |= e.isTop(); + } + + if (allBot) + bottom++; + else if (oneTop) + conservative++; else - maybeUnreachable++; - continue; - } - if (topStackValuesPerJump == null) { - // If all stacks are bottom, then we have a - // maybeFakeMissedJump - definitelyUnreachable++; - continue; + resolved++; } - if (!topStackValuesPerJump.contains(StackElement.NUMERIC_TOP)) { - // If the elements at the top of the stacks are all - // different from NUMERIC_TOP, then we are sure that it - // is definitelyFakeMissedJumps - resolvedJumps++; - continue; - } - if (soundlySolved != null && !soundlySolved.contains(jumpNode)) { - unsoundJumps++; - log.error("{} not solved", jumpNode); - log.error("getTopStackValuesPerJump: {}", topStackValuesPerJump); - continue; - } - if (checker.getMaybeUnsoundJumps().contains(jumpNode)) { - maybeUnsoundJumps++; - continue; - } - - resolvedJumps++; } } log.info("Total opcodes: {}", cfg.getOpcodeCount()); log.info("Total jumps: {}", cfg.getAllJumps().size()); - log.info("Resolved jumps: {}", resolvedJumps); - log.info("Definitely unreachable jumps: {}", definitelyUnreachable); - log.info("Maybe unreachable jumps: {}", maybeUnreachable); - log.info("Unsound jumps: {}", unsoundJumps); - log.info("Maybe unsound jumps: {}", maybeUnsoundJumps); + log.info("Resolved jumps: {}", resolved); + log.info("Unreachable jumps: {}", unreachable); + log.info("Bottom jumps: {}", bottom); + log.info("Conservative jumps: {}", conservative); return MyLogger.newLogger() .opcodes(cfg.getOpcodeCount()) .jumps(cfg.getAllJumps().size()) - .preciselyResolvedJumps(resolvedJumps) - .definitelyUnreachableJumps(definitelyUnreachable) - .maybeUnreachableJumps(maybeUnreachable) - .unsoundJumps(unsoundJumps) + .preciselyResolvedJumps(resolved) + .definitelyUnreachableJumps(unreachable) + .maybeUnreachableJumps(bottom) + .unsoundJumps(conservative) .maybeUnsoundJumps(maybeUnsoundJumps); } diff --git a/src/main/java/it/unipr/analysis/AbstractStack.java b/src/main/java/it/unipr/analysis/AbstractStack.java index b9633306f..699e0f20c 100644 --- a/src/main/java/it/unipr/analysis/AbstractStack.java +++ b/src/main/java/it/unipr/analysis/AbstractStack.java @@ -189,7 +189,7 @@ public void push(StackElement target) { */ public StackElement pop() { StackElement result = stack.remove(stack.size() - 1); - if (!stack.get(0).isTop()) + if (stack.get(0).isBottom()) stack.add(0, StackElement.BOTTOM); else stack.add(0, StackElement.NUMERIC_TOP); diff --git a/src/main/java/it/unipr/analysis/MyLogger.java b/src/main/java/it/unipr/analysis/MyLogger.java index da2439db9..1b0c09bd9 100644 --- a/src/main/java/it/unipr/analysis/MyLogger.java +++ b/src/main/java/it/unipr/analysis/MyLogger.java @@ -196,6 +196,6 @@ public String toString() { time + divider + timeLostToGetStorage + divider + actualTime + divider + - json.toString() + "\n"; + notes + "\n"; } }