Methods renaming #120

lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/BackwardModularWorstCaseAnalysis.java

@@ -1,12 +1,5 @@
 package it.unive.lisa.interprocedural;
 
-import java.util.Collection;
-import java.util.Set;
-import java.util.TreeSet;
-
-import org.apache.logging.log4j.LogManager;
-import org.apache.logging.log4j.Logger;
-
 import it.unive.lisa.analysis.AbstractState;
 import it.unive.lisa.analysis.AnalysisState;
 import it.unive.lisa.analysis.AnalyzedCFG;
@@ -29,6 +22,11 @@
 import it.unive.lisa.type.Type;
 import it.unive.lisa.util.collections.workset.WorkingSet;
 import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException;
+import java.util.Collection;
+import java.util.Set;
+import java.util.TreeSet;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
 
 /**
  * A worst case modular analysis were all cfg calls are treated as open calls.

lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java

@@ -133,7 +133,7 @@ public AnalysisState<A> find() throws SemanticException {
 			params[i] = entryState.intermediateStates.getState(actuals[i]).getComputedExpressions();
 		// it should be enough to send values to top, retaining all type
 		// information
-		return start.fwdSemAux(
+		return start.forwardSemanticsAux(
 				this,
 				entryState.postState.withTopValues(),
 				params,

lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/RecursionSolver.java

@@ -180,7 +180,7 @@ public void solve() throws SemanticException {
 			// we reset the analysis at the point where the starting call can be
 			// evaluated
 			token = recursion.getInvocationToken();
-			AnalysisState<A> post = start.fwdSemAux(
+			AnalysisState<A> post = start.forwardSemanticsAux(
 					this,
 					entryState.postState,
 					params,

lisa/lisa-analyses/src/test/java/it/unive/lisa/EqualityContractVerificationTest.java

@@ -4,6 +4,8 @@
 
 import it.unive.lisa.LiSAFactory.ConfigurableComponent;
 import it.unive.lisa.analysis.AnalyzedCFG;
+import it.unive.lisa.analysis.BackwardAnalyzedCFG;
+import it.unive.lisa.analysis.BackwardOptimizedAnalyzedCFG;
 import it.unive.lisa.analysis.FixpointInfo;
 import it.unive.lisa.analysis.Lattice;
 import it.unive.lisa.analysis.OptimizedAnalyzedCFG;
@@ -465,7 +467,10 @@ else if (FunctionalLattice.class.isAssignableFrom(subject)
 				verify(subject, Warning.NONFINAL_FIELDS);
 			else if (subject == StaticTypes.class)
 				verify(subject, verifier -> verifier.withIgnoredFields("types"));
-			else if (subject != AnalyzedCFG.class && subject != OptimizedAnalyzedCFG.class)
+			else if (subject != AnalyzedCFG.class
+					&& subject != OptimizedAnalyzedCFG.class
+					&& subject != BackwardAnalyzedCFG.class
+					&& subject != BackwardOptimizedAnalyzedCFG.class)
 				// we test the cfg separately
 				verify(subject);
 	}
@@ -479,10 +484,15 @@ public void testAnalysisObjects() {
 		// id is mutable
 		verify(AnalyzedCFG.class, verifier -> verifier.withOnlyTheseFields("id", "results", "entryStates"),
 				Warning.NONFINAL_FIELDS);
+		verify(BackwardAnalyzedCFG.class, verifier -> verifier.withOnlyTheseFields("id", "results", "exitStates"),
+				Warning.NONFINAL_FIELDS);
 		// we do not consider the expanded results or interprocedural
 		// as they do not identify the results
 		verify(OptimizedAnalyzedCFG.class, verifier -> verifier.withOnlyTheseFields("id", "results", "entryStates"),
 				Warning.NONFINAL_FIELDS);
+		verify(BackwardOptimizedAnalyzedCFG.class,
+				verifier -> verifier.withOnlyTheseFields("id", "results", "exitStates"),
+				Warning.NONFINAL_FIELDS);
 
 		verify(ExecutionTrace.class);
 		Reflections scanner = mkReflections();

lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java

@@ -446,7 +446,9 @@ private <T> int buildDomainsInstances(
 		nullary = unary = binary = ternary = quaternary = null;
 		T instance;
 		for (Class<? extends T> clazz : classes)
-			if (!Modifier.isAbstract(clazz.getModifiers()) && !Modifier.isInterface(clazz.getModifiers())
+			if (!Modifier.isAbstract(clazz.getModifiers())
+					&& !Modifier.isInterface(clazz.getModifiers())
+					&& !clazz.isAnonymousClass()
 					&& !Satisfiability.class.isAssignableFrom(clazz)
 					&& !CompoundState.class.isAssignableFrom(clazz)
 					// some testing domain that we do not care about end up here
@@ -464,7 +466,8 @@ else if (c.getParameterCount() == 3)
 					else if (c.getParameterCount() == 4)
 						quaternary = c;
 				}
-
+				if (clazz.getName().contains("FixpointInfo"))
+					System.out.println();
 				try {
 					if (nullary != null)
 						instance = (T) nullary.newInstance();
@@ -498,7 +501,7 @@ else if (unary != null) {
 
 					instances.add(instance);
 
-					nullary = unary = binary = ternary = null;
+					nullary = unary = binary = ternary = quaternary = null;
 				} catch (Exception e) {
 					failures.add(clazz.getName());
 					System.err.println("Instantiation of class " + clazz.getName() + " failed due to " + e);

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/constructs/ArrayLength.java

@@ -120,7 +120,7 @@ public IMPArrayLength(
 		}
 
 		@Override
-		public <A extends AbstractState<A>> AnalysisState<A> unaryFwdSemantics(
+		public <A extends AbstractState<A>> AnalysisState<A> fwdUnarySemantics(
 				InterproceduralAnalysis<A> interprocedural,
 				AnalysisState<A> state,
 				SymbolicExpression expr,

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAddOrConcat.java

@@ -57,7 +57,7 @@ public IMPAddOrConcat(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPArrayAccess.java

@@ -48,7 +48,7 @@ public IMPArrayAccess(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAssert.java

@@ -40,7 +40,7 @@ public IMPAssert(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> unaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdUnarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression expr,

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewArray.java

@@ -63,7 +63,7 @@ public IMPNewArray(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> fwdSemAux(
+	public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			ExpressionSet[] params,
@@ -100,6 +100,18 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdSemAux(
 		return refSt;
 	}
 
+	@Override
+	public <A extends AbstractState<A>> AnalysisState<A> backwardSemanticsAux(
+			InterproceduralAnalysis<A> interprocedural,
+			AnalysisState<A> state,
+			ExpressionSet[] params,
+			StatementStore<A> expressions)
+			throws SemanticException {
+		// TODO implement this when backward analysis will be out of
+		// beta
+		throw new UnsupportedOperationException();
+	}
+
 	@Override
 	public int hashCode() {
 		final int prime = 31;

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewObj.java

@@ -65,7 +65,7 @@ public IMPNewObj(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> fwdSemAux(
+	public <A extends AbstractState<A>> AnalysisState<A> forwardSemanticsAux(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			ExpressionSet[] params,
@@ -91,7 +91,7 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdSemAux(
 
 		UnresolvedCall call = new UnresolvedCall(getCFG(), getLocation(), CallType.INSTANCE, type.toString(),
 				type.toString(), fullExpressions);
-		AnalysisState<A> sem = call.fwdSemAux(interprocedural, tmp, fullParams, expressions);
+		AnalysisState<A> sem = call.forwardSemanticsAux(interprocedural, tmp, fullParams, expressions);
 
 		// now remove the instrumented receiver
 		expressions.forget(paramThis);
@@ -111,6 +111,18 @@ public <A extends AbstractState<A>> AnalysisState<A> fwdSemAux(
 		return result;
 	}
 
+	@Override
+	public <A extends AbstractState<A>> AnalysisState<A> backwardSemanticsAux(
+			InterproceduralAnalysis<A> interprocedural,
+			AnalysisState<A> state,
+			ExpressionSet[] params,
+			StatementStore<A> expressions)
+			throws SemanticException {
+		// TODO implement this when backward analysis will be out of
+		// beta
+		throw new UnsupportedOperationException();
+	}
+
 	@Override
 	public int hashCode() {
 		final int prime = 31;
@@ -131,5 +143,4 @@ public boolean equals(
 		IMPNewObj other = (IMPNewObj) obj;
 		return staticallyAllocated == other.staticallyAllocated;
 	}
-
 }

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/types/ArrayType.java

@@ -209,6 +209,17 @@ public <A extends AbstractState<A>> AnalysisState<A> forwardSemantics(
 
 				return refSt;
 			}
+
+			@Override
+			public <A extends AbstractState<A>> AnalysisState<A> backwardSemantics(
+					AnalysisState<A> exitState,
+					InterproceduralAnalysis<A> interprocedural,
+					StatementStore<A> expressions)
+					throws SemanticException {
+				// TODO implement this when backward analysis will be out of
+				// beta
+				throw new UnsupportedOperationException();
+			}
 		};
 	}
 }

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/Equal.java

@@ -38,7 +38,7 @@ public Equal(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterOrEqual.java

@@ -41,7 +41,7 @@ public GreaterOrEqual(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterThan.java

@@ -41,7 +41,7 @@ public GreaterThan(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessOrEqual.java

@@ -41,7 +41,7 @@ public LessOrEqual(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessThan.java

@@ -41,7 +41,7 @@ public LessThan(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/NotEqual.java

@@ -38,7 +38,7 @@ public NotEqual(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessInstanceGlobal.java

@@ -106,7 +106,7 @@ public String toString() {
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> unaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdUnarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression expr,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/And.java

@@ -40,7 +40,7 @@ public And(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Not.java

@@ -38,7 +38,7 @@ public Not(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> unaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdUnarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression expr,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Or.java

@@ -40,7 +40,7 @@ public Or(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Addition.java

@@ -41,7 +41,7 @@ public Addition(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Division.java

@@ -41,7 +41,7 @@ public Division(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Modulo.java

@@ -42,7 +42,7 @@ public Modulo(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Multiplication.java

@@ -41,7 +41,7 @@ public Multiplication(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Negation.java

@@ -38,7 +38,7 @@ public Negation(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> unaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdUnarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression expr,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Remainder.java

@@ -42,7 +42,7 @@ public Remainder(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Subtraction.java

@@ -41,7 +41,7 @@ public Subtraction(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,

lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Concat.java

@@ -62,7 +62,7 @@ public Concat(
 	}
 
 	@Override
-	public <A extends AbstractState<A>> AnalysisState<A> binaryFwdSemantics(
+	public <A extends AbstractState<A>> AnalysisState<A> fwdBinarySemantics(
 			InterproceduralAnalysis<A> interprocedural,
 			AnalysisState<A> state,
 			SymbolicExpression left,