fix: deleted pushTaintList and spotlessApply

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

@@ -498,9 +498,7 @@ void checkers(LiSAConfiguration conf, LiSA lisa, Program program, JumpSolver che
 			// Clear existing checks and add the TxOriginChecker
 			conf.semanticChecks.clear();
 			conf.semanticChecks.add(new TxOriginChecker());
-			HashSet<String> list = new HashSet<String>();
-			list.add("OriginOperator");
-			conf.abstractState = new SimpleAbstractState<>(new MonolithicHeap(), new TaintAbstractDomain(list),
+			conf.abstractState = new SimpleAbstractState<>(new MonolithicHeap(), new TaintAbstractDomain(),
 					new TypeEnvironment<>(new InferredTypes()));
 			lisa.run(program);
 

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

@@ -18,7 +18,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.function.Predicate;
@@ -27,37 +26,25 @@ public class TaintAbstractDomain implements ValueDomain<TaintAbstractDomain>, Ba
 
 	private static int STACK_LIMIT = 32;
 	private static final TaintAbstractDomain TOP = new TaintAbstractDomain(
-			new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM)), new HashSet<String>());
-	private static final TaintAbstractDomain BOTTOM = new TaintAbstractDomain(null, new HashSet<String>());
+			new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM)));
+	private static final TaintAbstractDomain BOTTOM = new TaintAbstractDomain(null);
 
 	private final ArrayList<TaintElement> stack;
-
-	private final HashSet<String> pushTaintList;
 
 	/**
 	 * Builds an initial symbolic stack.
 	 */
 	public TaintAbstractDomain() {
 		this.stack = new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM));
-		this.pushTaintList = new HashSet<String>();
-	}
-
-	/**
-	 * Builds a taint abstract stack starting from a given list of elements that push taint .
-	 */
-	public TaintAbstractDomain(HashSet<String> pushTaintList) {
-		this.stack = new ArrayList<>(Collections.nCopies(STACK_LIMIT, TaintElement.BOTTOM));
-		this.pushTaintList = pushTaintList;
 	}
 
 	/**
-	 * 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
 	 */
-	private TaintAbstractDomain(ArrayList<TaintElement> stack, HashSet<String> pushTaintList) {
+	private TaintAbstractDomain(ArrayList<TaintElement> stack) {
 		this.stack = stack;
-		this.pushTaintList = pushTaintList;
 	}
 
 	@Override
@@ -83,8 +70,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":
@@ -105,10 +96,7 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
 				case "PushOperator":
 				case "Push0Operator": {
 					TaintAbstractDomain resultStack = clone();
-					if(this.pushTaintList.contains(op.getClass().getSimpleName()))
-						resultStack.push(TaintElement.TAINT);
-					else resultStack.push(TaintElement.CLEAN);
-					resultStack.toString();
+					resultStack.push(TaintElement.CLEAN);
 					return resultStack;
 				}
 
@@ -121,22 +109,21 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra
 
 				case "JumpOperator": { // JUMP
 					if (hasBottomUntil(1))
-							return BOTTOM;
+						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;
 				}
 
@@ -716,7 +703,7 @@ private TaintAbstractDomain swapX(int x, TaintAbstractDomain stack) {
 		for (int i = 0; i < clone.size(); i++)
 			result.add((TaintElement) obj[i]);
 
-		return new TaintAbstractDomain(result, this.pushTaintList);
+		return new TaintAbstractDomain(result);
 	}
 
 	private TaintAbstractDomain dupX(int x, TaintAbstractDomain stack) {
@@ -743,7 +730,7 @@ private TaintAbstractDomain dupX(int x, TaintAbstractDomain stack) {
 		result.add(tmp);
 		result.remove(0);
 
-		return new TaintAbstractDomain(result, this.pushTaintList);
+		return new TaintAbstractDomain(result);
 	}
 
 	private ArrayList<TaintElement> getStack() {
@@ -854,7 +841,7 @@ public TaintAbstractDomain glbAux(TaintAbstractDomain other) throws SemanticExce
 			result.add(thisElement.glb(otherElement));
 		}
 
-		return new TaintAbstractDomain(result, this.pushTaintList);
+		return new TaintAbstractDomain(result);
 	}
 
 	@Override
@@ -870,7 +857,7 @@ public TaintAbstractDomain lubAux(TaintAbstractDomain other) throws SemanticExce
 			result.add(thisElement.lub(otherElement));
 		}
 
-		return new TaintAbstractDomain(result, this.pushTaintList);
+		return new TaintAbstractDomain(result);
 	}
 
 	@Override
@@ -916,9 +903,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.
 	 */
@@ -933,7 +920,7 @@ public boolean hasBottomUntil(int x) {
 	public TaintAbstractDomain clone() {
 		if (isBottom())
 			return this;
-		return new TaintAbstractDomain(new ArrayList<>(stack), new HashSet<String>(pushTaintList));
+		return new TaintAbstractDomain(new ArrayList<>(stack));
 	}
 
 	@Override
@@ -968,4 +955,4 @@ else if (isTop())
 			return TaintElement.TOP;
 		return this.stack.get(STACK_LIMIT - 1);
 	}
-}
+}

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);
+		}
 	}
 }