Skip to content

Commit

Permalink
Removed duplicated methods, added more statistics
Browse files Browse the repository at this point in the history
  • Loading branch information
@VincenzoArceri
VincenzoArceri committed Feb 14, 2024
1 parent 58eab0d commit 56fddbe
Show file tree
Hide file tree
Showing 4 changed files with 60 additions and 88 deletions.
28 changes: 18 additions & 10 deletions src/main/java/it/unipr/EVMLiSA.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
import org.apache.commons.cli.Option;
import org.apache.commons.cli.Options;
import org.apache.commons.cli.ParseException;
import org.apache.commons.lang3.tuple.Pair;
import org.apache.commons.lang3.tuple.Triple;

public class EVMLiSA {
Expand Down Expand Up @@ -161,7 +162,7 @@ else if (dumpAnalysis.equals("html"))

EVMCFG baseCfg = checker.getComputedCFG();

Triple<Integer, Integer, Integer> pair;
Triple<Integer, Integer, Pair<Integer, Integer>> pair;

pair = dumpStatistics(checker);

Expand All @@ -185,7 +186,8 @@ else if (dumpAnalysis.equals("html"))
.jumps(baseCfg.getAllJumps().size())
.preciselyResolvedJumps(pair.getLeft())
.soundResolvedJumps(pair.getMiddle())
.unreachableJumps(pair.getRight())
.definitelyUnreachableJumps(pair.getRight().getLeft())
.definitelyUnreachableJumps(pair.getRight().getRight())
.time(finish - start)
.build().toString();

Expand Down Expand Up @@ -221,12 +223,13 @@ else if (dumpAnalysis.equals("html"))
* @return A Triple containing the counts of precisely resolved jumps, sound
* resolved jumps, and unreachable jumps.
*/
private Triple<Integer, Integer, Integer> dumpStatistics(JumpSolver checker) {
public static Triple<Integer, Integer, Pair<Integer, Integer>> dumpStatistics(JumpSolver checker) {
EVMCFG cfg = checker.getComputedCFG();
Set<Statement> unreachableJumpNodes = checker.getUnreachableJumps();
int preciselyResolvedJumps = 0;
int soundResolvedJumps = 0;
int unreachableJumps = 0;
int definitelyUnreachable = 0;
int maybeUnreachable = 0;

// we are safe supposing that we have a single entry point
Statement entryPoint = cfg.getEntrypoints().stream().findAny().get();
Expand All @@ -236,26 +239,31 @@ private Triple<Integer, Integer, Integer> dumpStatistics(JumpSolver checker) {
preciselyResolvedJumps++;
else if (cfg.getOutgoingEdges(jumpNode).size() > 1)
soundResolvedJumps++;
else if (!cfg.reachableFrom(entryPoint, jumpNode) || unreachableJumpNodes.contains(jumpNode))
unreachableJumps++;
else if (unreachableJumpNodes.contains(jumpNode))
definitelyUnreachable++;
else if (!cfg.reachableFrom(entryPoint, jumpNode))
maybeUnreachable++;
} else if (jumpNode instanceof Jumpi) {
if (cfg.getOutgoingEdges(jumpNode).size() == 2)
preciselyResolvedJumps++;
else if (cfg.getOutgoingEdges(jumpNode).size() > 2)
soundResolvedJumps++;
else if (!cfg.reachableFrom(entryPoint, jumpNode) || unreachableJumpNodes.contains(jumpNode))
unreachableJumps++;
else if (unreachableJumpNodes.contains(jumpNode))
definitelyUnreachable++;
else if (!cfg.reachableFrom(entryPoint, jumpNode))
maybeUnreachable++;
}

System.err.println("##############");
System.err.println("Total opcodes: " + cfg.getNodesCount());
System.err.println("Total jumps: " + cfg.getAllJumps().size());
System.err.println("Precisely solved jumps: " + preciselyResolvedJumps);
System.err.println("Sound solved jumps: " + soundResolvedJumps);
System.err.println("Unreachable jumps: " + unreachableJumps);
System.err.println("Definitely unreachable jumps: " + definitelyUnreachable);
System.err.println("Maybe unreachable jumps: " + maybeUnreachable);
System.err.println("##############");

return Triple.of(preciselyResolvedJumps, soundResolvedJumps, unreachableJumps);
return Triple.of(preciselyResolvedJumps, soundResolvedJumps, Pair.of(definitelyUnreachable, maybeUnreachable));
}

/**
Expand Down
2 changes: 1 addition & 1 deletion src/main/java/it/unipr/analysis/KIntegerSet.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@

public class KIntegerSet extends SetLattice<KIntegerSet, BigDecimal> {
private static final BigDecimal MAX = new BigDecimal(Math.pow(2, 256));
public static final int K = 15;
public static final int K = 20;

public static final KIntegerSet ZERO = new KIntegerSet(0);
public static final KIntegerSet ONE = new KIntegerSet(1);
Expand Down
27 changes: 18 additions & 9 deletions src/main/java/it/unipr/analysis/MyLogger.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,8 @@ public class MyLogger {
private int jumps;
private int preciselyResolvedJumps;
private int soundResolvedJumps;
private int unreachableJumps;
private int definitelyUnreachableJumps;
private int maybeUnreachableJumps;
private int totalResolvedJumps;
private double preciselySolvedJumpsPercent;
private double solvedJumpsPercent;
Expand All @@ -25,24 +26,26 @@ private MyLogger() {
this.jumps = 0;
this.preciselyResolvedJumps = 0;
this.soundResolvedJumps = 0;
this.unreachableJumps = 0;
this.definitelyUnreachableJumps = 0;
this.maybeUnreachableJumps = 0;
this.solvedJumpsPercent = 0;
this.time = 0;
this.notes = "";
this.currentThread = null;
}

private MyLogger(String address, int opcodes, int jumps, int preciselyResolvedJumps, int soundResolvedJumps,
int unreachableJumps, int totalResolvedJumps, double solvedJumpsPercent, long time, String notes) {
int definitelyUnreachableJumps, int maybeUnreachableJumps, int totalResolvedJumps, double solvedJumpsPercent, long time, String notes) {
this.address = address;
this.opcodes = opcodes;
this.jumps = jumps;
this.preciselyResolvedJumps = preciselyResolvedJumps;
this.soundResolvedJumps = soundResolvedJumps;
this.unreachableJumps = unreachableJumps;
this.definitelyUnreachableJumps = definitelyUnreachableJumps;
this.maybeUnreachableJumps = maybeUnreachableJumps;
if (jumps != 0) {
if (solvedJumpsPercent == 0)
this.solvedJumpsPercent = ((double) (preciselyResolvedJumps + soundResolvedJumps + unreachableJumps)
this.solvedJumpsPercent = ((double) (preciselyResolvedJumps + soundResolvedJumps + definitelyUnreachableJumps)
/ jumps);
this.preciselySolvedJumpsPercent = ((double) (preciselyResolvedJumps) / jumps);
} else {
Expand Down Expand Up @@ -85,8 +88,13 @@ public MyLogger soundResolvedJumps(int soundResolvedJumps) {
return this;
}

public MyLogger unreachableJumps(int unreachableJumps) {
this.unreachableJumps = unreachableJumps;
public MyLogger maybeUnreachableJumps(int maybeUnreachableJumps) {
this.maybeUnreachableJumps = maybeUnreachableJumps;
return this;
}

public MyLogger definitelyUnreachableJumps(int definitelyUnreachableJumps) {
this.definitelyUnreachableJumps = definitelyUnreachableJumps;
return this;
}

Expand All @@ -107,7 +115,7 @@ public MyLogger notes(String notes) {

public MyLogger build() {
return new MyLogger(address, opcodes, jumps, preciselyResolvedJumps, soundResolvedJumps,
unreachableJumps, totalResolvedJumps, solvedJumpsPercent, time, notes);
definitelyUnreachableJumps, maybeUnreachableJumps, totalResolvedJumps, solvedJumpsPercent, time, notes);
}

public int jumpSize() {
Expand All @@ -121,7 +129,8 @@ public String toString() {
jumps + divider +
preciselyResolvedJumps + divider +
soundResolvedJumps + divider +
unreachableJumps + divider +
definitelyUnreachableJumps + divider +
maybeUnreachableJumps + divider +
totalResolvedJumps + divider +
preciselySolvedJumpsPercent + divider +
solvedJumpsPercent + divider +
Expand Down
91 changes: 23 additions & 68 deletions src/test/java/it/unipr/analysis/cron/EVMBytecodeTest.java
View file
Original file line number Diff line number Diff line change
@@ -1,20 +1,5 @@
package it.unipr.analysis.cron;

import it.unipr.analysis.EVMAbstractState;
import it.unipr.analysis.MyLogger;
import it.unipr.cfg.EVMCFG;
import it.unipr.cfg.Jump;
import it.unipr.cfg.Jumpi;
import it.unipr.checker.JumpSolver;
import it.unipr.frontend.EVMFrontend;
import it.unive.lisa.analysis.SimpleAbstractState;
import it.unive.lisa.analysis.heap.MonolithicHeap;
import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
import it.unive.lisa.analysis.types.InferredTypes;
import it.unive.lisa.conf.LiSAConfiguration.GraphType;
import it.unive.lisa.interprocedural.ModularWorstCaseAnalysis;
import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
import it.unive.lisa.program.cfg.statement.Statement;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileWriter;
Expand All @@ -29,11 +14,26 @@
import java.util.ArrayList;
import java.util.List;
import java.util.Scanner;
import java.util.Set;

import org.apache.commons.lang3.tuple.Pair;
import org.apache.commons.lang3.tuple.Triple;
import org.junit.Before;
import org.junit.Test;

import it.unipr.EVMLiSA;
import it.unipr.analysis.EVMAbstractState;
import it.unipr.analysis.MyLogger;
import it.unipr.cfg.EVMCFG;
import it.unipr.checker.JumpSolver;
import it.unipr.frontend.EVMFrontend;
import it.unive.lisa.analysis.SimpleAbstractState;
import it.unive.lisa.analysis.heap.MonolithicHeap;
import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
import it.unive.lisa.analysis.types.InferredTypes;
import it.unive.lisa.conf.LiSAConfiguration.GraphType;
import it.unive.lisa.interprocedural.ModularWorstCaseAnalysis;
import it.unive.lisa.interprocedural.callgraph.RTACallGraph;

public class EVMBytecodeTest extends EVMBytecodeAnalysisExecutor {

// Choose whether to generate the CFG or not
Expand Down Expand Up @@ -61,11 +61,10 @@ public class EVMBytecodeTest extends EVMBytecodeAnalysisExecutor {

@Test
public void testSCFromEtherscan() throws Exception {
String SC_ADDRESS = "0x860a8c64cbc7f9aac11428ef8df989f5770cda60";
String SC_ADDRESS = "0xD4Abd907Bfead0825FE21631A4dC5B99C6fA8875";
toFileStatistics(newAnalysis(SC_ADDRESS).toString());
}

@Test
public void testEVMBytecodeAnalysisMultiThread() throws Exception {
clean();
startOfExecutionTime = System.currentTimeMillis();
Expand Down Expand Up @@ -290,7 +289,7 @@ private MyLogger newAnalysis(String CONTRACT_ADDR) throws Exception {
// Print the results
EVMCFG baseCfg = checker.getComputedCFG();

Triple<Integer, Integer, Integer> pair = dumpStatistics(checker);
Triple<Integer, Integer, Pair<Integer, Integer>> pair = EVMLiSA.dumpStatistics(checker);
long finish = System.currentTimeMillis();

return MyLogger.newLogger()
Expand All @@ -299,7 +298,8 @@ private MyLogger newAnalysis(String CONTRACT_ADDR) throws Exception {
.jumps(baseCfg.getAllJumps().size())
.preciselyResolvedJumps(pair.getLeft())
.soundResolvedJumps(pair.getMiddle())
.unreachableJumps(pair.getRight())
.definitelyUnreachableJumps(pair.getRight().getLeft())
.maybeUnreachableJumps(pair.getRight().getRight())
.time(finish - start)
.build();
}
Expand Down Expand Up @@ -369,52 +369,7 @@ public ArrayList<String> readSmartContractsFromFile() throws Exception {
return smartContractsRead;
}

/**
* Calculates and prints statistics about the control flow graph (CFG) of
* the provided EVMCFG object.
*
* @param checker The control flow graph (CFG) of the Ethereum Virtual
* Machine (EVM) bytecode.
*
* @return A Triple containing the counts of precisely resolved jumps, sound
* resolved jumps, and unreachable jumps.
*/
private Triple<Integer, Integer, Integer> dumpStatistics(JumpSolver checker) {
EVMCFG cfg = checker.getComputedCFG();
Set<Statement> unreachableJumpNodes = checker.getUnreachableJumps();
int preciselyResolvedJumps = 0;
int soundResolvedJumps = 0;
int unreachableJumps = 0;

// we are safe supposing that we have a single entry point
Statement entryPoint = cfg.getEntrypoints().stream().findAny().get();
for (Statement jumpNode : cfg.getAllJumps())
if (jumpNode instanceof Jump) {
if (cfg.getOutgoingEdges(jumpNode).size() == 1)
preciselyResolvedJumps++;
else if (cfg.getOutgoingEdges(jumpNode).size() > 1)
soundResolvedJumps++;
else if (!cfg.reachableFrom(entryPoint, jumpNode) || unreachableJumpNodes.contains(jumpNode))
unreachableJumps++;
} else if (jumpNode instanceof Jumpi) {
if (cfg.getOutgoingEdges(jumpNode).size() == 2)
preciselyResolvedJumps++;
else if (cfg.getOutgoingEdges(jumpNode).size() > 2)
soundResolvedJumps++;
else if (!cfg.reachableFrom(entryPoint, jumpNode) || unreachableJumpNodes.contains(jumpNode))
unreachableJumps++;
}

System.err.println("##############");
System.err.println("Total opcodes: " + cfg.getNodesCount());
System.err.println("Total jumps: " + cfg.getAllJumps().size());
System.err.println("Precisely solved jumps: " + preciselyResolvedJumps);
System.err.println("Sound solved jumps: " + soundResolvedJumps);
System.err.println("Unreachable jumps: " + unreachableJumps);
System.err.println("##############");

return Triple.of(preciselyResolvedJumps, soundResolvedJumps, unreachableJumps);
}


/**
* Writes the given statistics to a file.
Expand All @@ -423,7 +378,7 @@ else if (!cfg.reachableFrom(entryPoint, jumpNode) || unreachableJumpNodes.contai
*/
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, % Precisely Solved, % Total Solved, Time (millis), Thread, Notes \n";
try {
File idea = new File(STATISTICS_FULLPATH);
if (!idea.exists()) {
Expand Down Expand Up @@ -451,7 +406,7 @@ private void toFileStatistics(String stats) {
*/
private void toFileStatisticsWithZeroJumps(String stats) {
synchronized (STATISTICSZEROJUMP_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, % Precisely Solved, % Total Solved, Time (millis), Thread, Notes \n";
try {
File idea = new File(STATISTICSZEROJUMP_FULLPATH);
if (!idea.exists()) {
Expand Down

0 comments on commit 56fddbe

Please sign in to comment.