Second Adjustment

src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java

@@ -20,7 +20,6 @@
 import it.unive.lisa.util.representation.StructuredRepresentation;
 import java.util.ArrayList;
 import java.util.Collections;
-import java.util.HashSet;
 import java.util.Iterator;
 import java.util.List;
 import java.util.Set;
@@ -32,10 +31,9 @@ public abstract class TaintAbstractDomain implements ValueDomain<TaintAbstractDo
 
 
 	private final ArrayList<TaintElement> stack;
-
 
 	/**
-	 * Builds a taint abstract stack starting from a given stack and a list of elements that push taint.
+	 * Builds a taint abstract stack starting from a given stack.
 	 *
 	 * @param stack the stack of values
 	 */
@@ -66,8 +64,12 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
 
 			if (op != null) {
 				switch (op.getClass().getSimpleName()) {
+				case "OriginOperator": {
+					TaintAbstractDomain resultStack = clone();
+					resultStack.push(TaintElement.TAINT);
+					return resultStack;
+				}
 				case "TimestampOperator":
-				case "OriginOperator":
 				case "CodesizeOperator":
 				case "GaspriceOperator":
 				case "ReturndatasizeOperator":
@@ -92,6 +94,7 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
 						resultStack.push(TaintElement.TAINT);
 					else resultStack.push(TaintElement.CLEAN);
 					resultStack.toString();
+
 					return resultStack;
 				}
 
@@ -106,20 +109,20 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
 					if (hasBottomUntil(1))
 							return bottom();
 
+
 					TaintAbstractDomain resultStack = clone();
-					TaintElement opnd1 = resultStack.pop();
-					
+					resultStack.pop();
+
 					return resultStack;
 				}
 				case "JumpiOperator": { // JUMPI
-
 					if (hasBottomUntil(2))
 						return bottom();
 
 					TaintAbstractDomain resultStack = clone();
-					TaintElement opnd1 = resultStack.pop();
-					TaintElement opnd2 = resultStack.pop();
-					
+					resultStack.pop();
+					resultStack.pop();
+
 					return resultStack;
 				}
 
@@ -699,6 +702,7 @@ private TaintAbstractDomain swapX(int x, TaintAbstractDomain stack) {
 		for (int i = 0; i < clone.size(); i++)
 			result.add((TaintElement) obj[i]);
 
+
 		return mk(result);
 	}
 
@@ -890,9 +894,9 @@ public TaintElement pop() {
 	 * Checks whether between 0 and x-positions of the stack an element is
 	 * bottom. /** Checks whether between 0 and x-positions of the stack an
 	 * element is bottom.
-	 * 
+	 *
 	 * @param x the position
-	 * 
+	 *
 	 * @return {@code true} if between 0 and x-positions of the stack an element
 	 *             is bottom, {@code false} otherwise.
 	 */
@@ -907,6 +911,7 @@ public boolean hasBottomUntil(int x) {
 	public TaintAbstractDomain clone() {
 		if (isBottom())
 			return this;
+
 		return mk(new ArrayList<>(stack));
 	}
 
@@ -948,3 +953,4 @@ else if (isTop())
 	public abstract TaintAbstractDomain mk(ArrayList<TaintElement> list);
 
 }
+

src/main/java/it/unipr/cfg/EVMCFG.java

@@ -73,7 +73,7 @@ public Set<Statement> getAllSstore() {
 
 		return sstores;
 	}
-	
+
 	/**
 	 * Returns a set of all the SHA3 statements in the CFG. SHA3
 	 * 
@@ -150,7 +150,7 @@ public Set<Statement> getAllJumps() {
 
 		return jumpNodes;
 	}
-	
+
 	/**
 	 * Returns a set of all the JUMPI statements in the CFG.
 	 * 

src/main/java/it/unipr/cfg/Jumpi.java

@@ -50,9 +50,10 @@ public <A extends AbstractState<A>> AnalysisState<A> forwardSemantics(AnalysisSt
 			InterproceduralAnalysis<A> interprocedural, StatementStore<A> expressions) throws SemanticException {
 
 		EVMAbstractState valueState = entryState.getState().getDomainInstance(EVMAbstractState.class);
-
-		if(valueState == null) return entryState;
-
+
+		if (valueState == null)
+			return entryState;
+
 		// Split here
 		Set<AbstractStack> trueStacks = new HashSet<>();
 		Set<AbstractStack> falseStacks = new HashSet<>();

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

@@ -1,7 +1,5 @@
 package it.unipr.checker;
 
-import java.util.Set;
-
 import it.unipr.analysis.taint.TaintAbstractDomain;
 import it.unipr.cfg.Balance;
 import it.unipr.cfg.Blockhash;
@@ -16,6 +14,7 @@
 import it.unive.lisa.checks.semantic.SemanticCheck;
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.statement.Statement;
+import java.util.Set;
 
 public class TimestampDependencyChecker implements
 		SemanticCheck<SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> {
@@ -33,21 +32,20 @@ public boolean visit(
 			CheckToolWithAnalysisResults<
 					SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> tool,
 			CFG graph, Statement node) {
-
-		if (node instanceof Timestamp || node instanceof Blockhash || node instanceof Difficulty || node instanceof Balance) {
+
+		if (node instanceof Timestamp || node instanceof Blockhash || node instanceof Difficulty
+				|| node instanceof Balance) {
 			EVMCFG cfg = ((EVMCFG) graph);
 			Set<Statement> nsh = cfg.getAllSha3();
 			Set<Statement> ns = cfg.getAllSstore();
-			// The function cfg.getAllJumps() returns all jumps, whether being jump or jumpi
-			// if you want to separete the jumps, a different function need to be done
+			// The function cfg.getAllJumps() returns all jumps, whether being
+			// jump or jumpi
+			// if you want to separete the jumps, a different function need to
+			// be done
 			Set<Statement> nj = cfg.getAllJumps();
-
-
+
 		}
-
-
-
-
+
 		return SemanticCheck.super.visit(tool, graph, node);
 	}
 

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

@@ -1,9 +1,6 @@
 package it.unipr.checker;
 
-import it.unipr.analysis.AbstractStack;
-import it.unipr.analysis.EVMAbstractState;
 import it.unipr.analysis.MyCache;
-import it.unipr.analysis.StackElement;
 import it.unipr.analysis.taint.TaintAbstractDomain;
 import it.unipr.analysis.taint.TaintElement;
 import it.unipr.cfg.EVMCFG;
@@ -45,16 +42,16 @@ public boolean visit(
 				AnalysisState<SimpleAbstractState<MonolithicHeap, TaintAbstractDomain,
 						TypeEnvironment<InferredTypes>>> analysisResult = null;
 
-				for(Statement jump: jumps) {
+				for (Statement jump : jumps) {
 					try {
 						analysisResult = result.getAnalysisStateBefore(jump);
 					} catch (SemanticException e1) {
 						log.error("(TxOriginChecker): {}", e1.getMessage());
 					}
-					
+
 					// Retrieve the symbolic stack from the analysis result
 					TaintAbstractDomain taintedStack = analysisResult.getState().getValueState();
-					
+
 					// If the stack is bottom, the jump is definitely
 					// unreachable
 					if (taintedStack.isBottom())
@@ -63,36 +60,38 @@ public boolean visit(
 					else {
 						TaintElement firstStackElement = taintedStack.getFirstElement();
 						TaintElement secondStackElement = taintedStack.getSecondElement();
-						if(secondStackElement.isBottom())
+						if (secondStackElement.isBottom())
 							// Nothing to do
 							continue;
 						else {
-							// Checks if either first or second element in the stack is tainted
-							if(firstStackElement.isTaint() || secondStackElement.isTaint()) {
+							// Checks if either first or second element in the
+							// stack is tainted
+							if (firstStackElement.isTaint() || secondStackElement.isTaint()) {
 								checkForTxOrigin(origin, jump, tool, cfg);
 							}
 						}
 					}
-				}	
+				}
 			}
 
 		}
 
 		return true;
 	}
-	
+
 	private void checkForTxOrigin(Statement origin, Statement jump, CheckToolWithAnalysisResults<
-			SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> tool, EVMCFG cfg) {
-			if (cfg.reachableFrom(origin, jump)) {
-				ProgramCounterLocation jumploc = (ProgramCounterLocation) jump.getLocation();
+			SimpleAbstractState<MonolithicHeap, TaintAbstractDomain, TypeEnvironment<InferredTypes>>> tool,
+			EVMCFG cfg) {
+		if (cfg.reachableFrom(origin, jump)) {
+			ProgramCounterLocation jumploc = (ProgramCounterLocation) jump.getLocation();
 
-				log.debug("Tx. Origin attack at {} at line no. {} coming from line {}", jumploc.getPc(),
-						jumploc.getSourceCodeLine(),
-						((ProgramCounterLocation) origin.getLocation()).getSourceCodeLine());
+			log.debug("Tx. Origin attack at {} at line no. {} coming from line {}", jumploc.getPc(),
+					jumploc.getSourceCodeLine(),
+					((ProgramCounterLocation) origin.getLocation()).getSourceCodeLine());
 
-				String warn = "TxOrigin attack at " + ((ProgramCounterLocation) origin.getLocation()).getSourceCodeLine();
-				tool.warn(warn);
-				MyCache.getInstance().addTxOriginWarning(cfg.hashCode(), warn);
-			}
+			String warn = "TxOrigin attack at " + ((ProgramCounterLocation) origin.getLocation()).getSourceCodeLine();
+			tool.warn(warn);
+			MyCache.getInstance().addTxOriginWarning(cfg.hashCode(), warn);
+		}
 	}
 }

src/test/java/it/unipr/analysis/cron/EVMBytecodeGroundTruth.java

@@ -68,7 +68,8 @@ public void testGroundTruth() throws Exception {
 
 		List<String> smartContracts = EVMLiSA.readSmartContractsFromFile(SMARTCONTRACTS_FULLPATH);
 
-		ExecutorService executor = Executors.newFixedThreadPool(Runtime.getRuntime().availableProcessors());
+		int cores = Runtime.getRuntime().availableProcessors() / 3 * 2;
+		ExecutorService executor = Executors.newFixedThreadPool(cores > 0 ? cores : 1);
 
 		for (String address : smartContracts) {
 			executor.submit(() -> {

src/test/java/it/unipr/analysis/cron/EVMBytecodeSmartBugsReentrancyTruth.java

@@ -14,6 +14,8 @@
 import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
 import it.unive.lisa.program.Program;
 import java.io.File;
+import java.nio.file.Files;
+import java.nio.file.Path;
 import java.nio.file.Paths;
 import java.util.ArrayList;
 import java.util.List;
@@ -29,21 +31,26 @@ public class EVMBytecodeSmartBugsReentrancyTruth {
 
 	@Ignore
 	public void testSmartBugsReentrancyTruth() throws Exception {
-		String SMARTBUGS_BYTECODES_DIR = Paths
-				.get("evm-testcases", "ground-truth", "test-reentrancy-smartbugs-truth", "bytecode")
-				.toString();
+		Path smartbugsBytecodesDirPath = Paths
+				.get("evm-testcases", "ground-truth", "test-reentrancy-smartbugs-truth", "bytecode");
+		String SMARTBUGS_BYTECODES_DIR = smartbugsBytecodesDirPath.toString();
 
 		EVMFrontend.setUseCreationCode();
 
 		List<String> bytecodes = getFileNamesInDirectory(SMARTBUGS_BYTECODES_DIR);
 
-		ExecutorService executor = Executors.newFixedThreadPool(Runtime.getRuntime().availableProcessors() / 2);
+		int cores = Runtime.getRuntime().availableProcessors() / 3 * 2;
+		ExecutorService executor = Executors.newFixedThreadPool(cores > 0 ? cores : 1);
 
 		// Run the benchmark in parallel
 		for (String bytecodeFileName : bytecodes) {
 			executor.submit(() -> {
 				try {
-					String bytecodeFullPath = SMARTBUGS_BYTECODES_DIR + bytecodeFileName;
+					String bytecodeFullPath = smartbugsBytecodesDirPath.resolve(bytecodeFileName).toString();
+
+					String bytecode = new String(Files.readAllBytes(Paths.get(bytecodeFullPath)));
+					if (bytecode.startsWith("0x"))
+						EVMFrontend.opcodesFromBytecode(bytecode, bytecodeFullPath);
 
 					Program program = EVMFrontend.generateCfgFromFile(bytecodeFullPath);
 

src/test/java/it/unipr/analysis/cron/EVMBytecodeSolidiFIReentrancyTruth.java

@@ -15,6 +15,8 @@
 import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
 import it.unive.lisa.program.Program;
 import java.io.File;
+import java.nio.file.Files;
+import java.nio.file.Path;
 import java.nio.file.Paths;
 import java.util.ArrayList;
 import java.util.List;
@@ -32,19 +34,26 @@ public class EVMBytecodeSolidiFIReentrancyTruth {
 	@Test
 	public void testSolidiFIReentrancyTruth() throws Exception {
 		setSolidifiMap();
-		String SOLIDIFI_BYTECODES_DIR = Paths
-				.get("evm-testcases", "ground-truth", "test-reentrancy-solidifi-truth", "bytecode")
-				.toString();
 		EVMFrontend.setUseCreationCode();
+
+		Path solidifiBytecodesDirPath = Paths
+				.get("evm-testcases", "ground-truth", "test-reentrancy-solidifi-truth", "bytecode");
+		String SOLIDIFI_BYTECODES_DIR = solidifiBytecodesDirPath.toString();
+
 		List<String> bytecodes = getFileNamesInDirectory(SOLIDIFI_BYTECODES_DIR);
 
-		ExecutorService executor = Executors.newFixedThreadPool(Runtime.getRuntime().availableProcessors());
+		int cores = Runtime.getRuntime().availableProcessors() / 3 * 2;
+		ExecutorService executor = Executors.newFixedThreadPool(cores > 0 ? cores : 1);
 
 		// Run the benchmark
 		for (String bytecodeFileName : bytecodes) {
 			executor.submit(() -> {
 				try {
-					String bytecodeFullPath = SOLIDIFI_BYTECODES_DIR + bytecodeFileName;
+					String bytecodeFullPath = solidifiBytecodesDirPath.resolve(bytecodeFileName).toString();
+
+					String bytecode = new String(Files.readAllBytes(Paths.get(bytecodeFullPath)));
+					if (bytecode.startsWith("0x"))
+						EVMFrontend.opcodesFromBytecode(bytecode, bytecodeFullPath);
 
 					Program program = EVMFrontend.generateCfgFromFile(bytecodeFullPath);