diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java
index 82d87de36..37f2d5fc3 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java
@@ -1,11 +1,5 @@
package it.unive.lisa.analysis;
-import java.util.Collection;
-import java.util.HashSet;
-import java.util.Map;
-import java.util.Set;
-import java.util.function.Predicate;
-
import it.unive.lisa.DefaultParameters;
import it.unive.lisa.FallbackImplementation;
import it.unive.lisa.analysis.heap.HeapDomain;
@@ -25,11 +19,22 @@
import it.unive.lisa.symbolic.value.ValueExpression;
import it.unive.lisa.type.Type;
import it.unive.lisa.type.Untyped;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+import java.util.function.Predicate;
/**
* An abstract state of the analysis, composed by a heap state modeling the
- * memory layout and a value state modeling values of program variables and
- * memory locations.
+ * memory layout, a value state modeling values of program variables and memory
+ * locations, and a type state that can give types to expressions knowing the
+ * ones of variables.
+ *
+ * The interaction between heap and value/type domains follows the one defined
+ * in this
+ * paper.
*
* @author Luca Negrini
*
@@ -42,7 +47,8 @@
public class SimpleAbstractState,
V extends ValueDomain,
T extends TypeDomain>
- implements BaseLattice>, AbstractState, H, V, T> {
+ implements BaseLattice>,
+ AbstractState> {
/**
* The key that should be used to store the instance of {@link HeapDomain}
@@ -99,14 +105,29 @@ public SimpleAbstractState(H heapState, V valueState, T typeState) {
this.typeState = typeState;
}
+ /**
+ * Yields the {@link HeapDomain} contained in this state.
+ *
+ * @return the heap domain
+ */
public H getHeapState() {
return heapState;
}
+ /**
+ * Yields the {@link ValueDomain} contained in this state.
+ *
+ * @return the value domain
+ */
public V getValueState() {
return valueState;
}
+ /**
+ * Yields the {@link TypeDomain} contained in this state.
+ *
+ * @return the type domain
+ */
public T getTypeState() {
return typeState;
}
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java
index d399da364..a61f187e1 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java
@@ -1,25 +1,15 @@
package it.unive.lisa.analysis.traces;
-import java.util.Collection;
-import java.util.HashSet;
-import java.util.Map;
-import java.util.Map.Entry;
-import java.util.Set;
-import java.util.function.Predicate;
-
import it.unive.lisa.analysis.AbstractState;
import it.unive.lisa.analysis.Lattice;
import it.unive.lisa.analysis.ScopeToken;
import it.unive.lisa.analysis.SemanticDomain;
import it.unive.lisa.analysis.SemanticException;
-import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.lattices.ExpressionSet;
import it.unive.lisa.analysis.lattices.FunctionalLattice;
import it.unive.lisa.analysis.representation.DomainRepresentation;
import it.unive.lisa.analysis.representation.MapRepresentation;
import it.unive.lisa.analysis.representation.StringRepresentation;
-import it.unive.lisa.analysis.value.TypeDomain;
-import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.program.cfg.ProgramPoint;
import it.unive.lisa.program.cfg.controlFlow.ControlFlowStructure;
import it.unive.lisa.program.cfg.controlFlow.IfThenElse;
@@ -28,6 +18,12 @@
import it.unive.lisa.symbolic.value.Identifier;
import it.unive.lisa.type.Type;
import it.unive.lisa.type.Untyped;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Set;
+import java.util.function.Predicate;
/**
* The trace partitioning abstract domain that splits execution traces to
@@ -56,19 +52,13 @@
* @author Luca Negrini
*
* @param the type of {@link AbstractState} that this is being partitioned
- * @param the type of {@link HeapDomain} embedded in the abstract states
- * @param the type of {@link ValueDomain} embedded in the abstract states
- * @param the type of {@link TypeDomain} embedded in the abstract states
*
* @see https://doi.org/10.1145/1275497.1275501
*/
-public class TracePartitioning,
- H extends HeapDomain,
- V extends ValueDomain,
- T extends TypeDomain>
- extends FunctionalLattice, ExecutionTrace, A>
- implements AbstractState, H, V, T> {
+public class TracePartitioning>
+ extends FunctionalLattice, ExecutionTrace, A>
+ implements AbstractState> {
/**
* The maximum number of {@link LoopIteration} tokens that a trace can
@@ -109,17 +99,17 @@ else if (isBottom() || function == null)
}
@Override
- public TracePartitioning top() {
+ public TracePartitioning top() {
return new TracePartitioning<>(lattice.top(), null);
}
@Override
- public TracePartitioning bottom() {
+ public TracePartitioning bottom() {
return new TracePartitioning<>(lattice.bottom(), null);
}
@Override
- public TracePartitioning assign(Identifier id, SymbolicExpression expression, ProgramPoint pp)
+ public TracePartitioning assign(Identifier id, SymbolicExpression expression, ProgramPoint pp)
throws SemanticException {
if (isBottom())
return this;
@@ -134,7 +124,7 @@ public TracePartitioning assign(Identifier id, SymbolicExpression ex
}
@Override
- public TracePartitioning smallStepSemantics(SymbolicExpression expression, ProgramPoint pp)
+ public TracePartitioning smallStepSemantics(SymbolicExpression expression, ProgramPoint pp)
throws SemanticException {
if (isBottom())
return this;
@@ -149,7 +139,7 @@ public TracePartitioning smallStepSemantics(SymbolicExpression expre
}
@Override
- public TracePartitioning assume(SymbolicExpression expression, ProgramPoint src, ProgramPoint dest)
+ public TracePartitioning assume(SymbolicExpression expression, ProgramPoint src, ProgramPoint dest)
throws SemanticException {
if (isBottom())
return this;
@@ -211,7 +201,7 @@ else if (prev instanceof LoopIteration) {
}
@Override
- public TracePartitioning forgetIdentifier(Identifier id) throws SemanticException {
+ public TracePartitioning forgetIdentifier(Identifier id) throws SemanticException {
if (isTop() || isBottom() || function == null)
return this;
@@ -222,7 +212,7 @@ public TracePartitioning forgetIdentifier(Identifier id) throws Sema
}
@Override
- public TracePartitioning forgetIdentifiersIf(Predicate test) throws SemanticException {
+ public TracePartitioning forgetIdentifiersIf(Predicate test) throws SemanticException {
if (isTop() || isBottom() || function == null)
return this;
@@ -251,7 +241,7 @@ public Satisfiability satisfies(SymbolicExpression expression, ProgramPoint pp)
}
@Override
- public TracePartitioning pushScope(ScopeToken token) throws SemanticException {
+ public TracePartitioning pushScope(ScopeToken token) throws SemanticException {
if (isTop() || isBottom() || function == null)
return this;
@@ -262,7 +252,7 @@ public TracePartitioning pushScope(ScopeToken token) throws Semantic
}
@Override
- public TracePartitioning popScope(ScopeToken token) throws SemanticException {
+ public TracePartitioning popScope(ScopeToken token) throws SemanticException {
if (isTop() || isBottom() || function == null)
return this;
@@ -287,7 +277,7 @@ public DomainRepresentation representation() {
}
@Override
- public TracePartitioning mk(A lattice, Map function) {
+ public TracePartitioning mk(A lattice, Map function) {
return new TracePartitioning<>(lattice, function);
}
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/CallGraphBasedAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/CallGraphBasedAnalysis.java
index 9d7c7655d..4e80dbd2e 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/CallGraphBasedAnalysis.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/CallGraphBasedAnalysis.java
@@ -4,11 +4,8 @@
import it.unive.lisa.analysis.AnalysisState;
import it.unive.lisa.analysis.SemanticException;
import it.unive.lisa.analysis.StatementStore;
-import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.lattices.ExpressionSet;
import it.unive.lisa.analysis.symbols.SymbolAliasing;
-import it.unive.lisa.analysis.value.TypeDomain;
-import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.interprocedural.callgraph.CallGraph;
import it.unive.lisa.interprocedural.callgraph.CallResolutionException;
import it.unive.lisa.program.Application;
@@ -26,16 +23,10 @@
/**
* An interprocedural analysis based on a call graph.
*
- * @param The abstract state of the analysis
- * @param The heap domain
- * @param The value domain
- * @param The type domain
+ * @param The {@link AbstractState} of the analysis
*/
-public abstract class CallGraphBasedAnalysis,
- H extends HeapDomain,
- V extends ValueDomain,
- T extends TypeDomain>
- implements InterproceduralAnalysis {
+public abstract class CallGraphBasedAnalysis>
+ implements InterproceduralAnalysis {
/**
* The call graph used to resolve method calls.
@@ -63,7 +54,7 @@ protected CallGraphBasedAnalysis() {
*
* @param other the original analysis to copy
*/
- protected CallGraphBasedAnalysis(CallGraphBasedAnalysis other) {
+ protected CallGraphBasedAnalysis(CallGraphBasedAnalysis other) {
this.callgraph = other.callgraph;
this.app = other.app;
this.policy = other.policy;
@@ -94,9 +85,9 @@ public Call resolve(UnresolvedCall call, Set[] types, SymbolAliasing alias
*
* @throws SemanticException if the analysis fails
*/
- public AnalysisState prepareEntryStateOfEntryPoint(AnalysisState entryState, CFG cfg)
+ public AnalysisState prepareEntryStateOfEntryPoint(AnalysisState entryState, CFG cfg)
throws SemanticException {
- AnalysisState prepared = entryState;
+ AnalysisState prepared = entryState;
for (Parameter arg : cfg.getDescriptor().getFormals()) {
Variable id = new Variable(arg.getStaticType(), arg.getName(), arg.getAnnotations(), arg.getLocation());
@@ -109,11 +100,11 @@ public AnalysisState prepareEntryStateOfEntryPoint(AnalysisState getAbstractResultOf(
+ public AnalysisState getAbstractResultOf(
OpenCall call,
- AnalysisState entryState,
+ AnalysisState entryState,
ExpressionSet[] parameters,
- StatementStore expressions)
+ StatementStore expressions)
throws SemanticException {
return policy.apply(call, entryState, parameters);
}
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java
index a4389b05f..faf130a74 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java
@@ -8,11 +8,8 @@
import it.unive.lisa.analysis.OptimizedAnalyzedCFG;
import it.unive.lisa.analysis.SemanticException;
import it.unive.lisa.analysis.StatementStore;
-import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.lattices.ExpressionSet;
import it.unive.lisa.analysis.symbols.SymbolAliasing;
-import it.unive.lisa.analysis.value.TypeDomain;
-import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.conf.FixpointConfiguration;
import it.unive.lisa.interprocedural.callgraph.CallGraph;
import it.unive.lisa.interprocedural.callgraph.CallResolutionException;
@@ -40,16 +37,10 @@
/**
* A worst case modular analysis were all cfg calls are treated as open calls.
*
- * @param the abstract state of the analysis
- * @param the heap domain
- * @param the value domain
- * @param the type domain
+ * @param the {@link AbstractState} of the analysis
*/
@FallbackImplementation
-public class ModularWorstCaseAnalysis,
- H extends HeapDomain,
- V extends ValueDomain,
- T extends TypeDomain> implements InterproceduralAnalysis {
+public class ModularWorstCaseAnalysis> implements InterproceduralAnalysis {
private static final Logger LOG = LogManager.getLogger(ModularWorstCaseAnalysis.class);
@@ -68,7 +59,7 @@ public class ModularWorstCaseAnalysis,
/**
* The cash of the fixpoints' results.
*/
- private FixpointResults results;
+ private FixpointResults results;
/**
* Builds the interprocedural analysis.
@@ -77,7 +68,7 @@ public ModularWorstCaseAnalysis() {
}
@Override
- public void fixpoint(AnalysisState entryState,
+ public void fixpoint(AnalysisState entryState,
Class extends WorkingSet> fixpointWorkingSet,
FixpointConfiguration conf)
throws FixpointException {
@@ -92,14 +83,14 @@ public void fixpoint(AnalysisState entryState,
"cfgs"))
try {
if (results == null) {
- AnalyzedCFG graph = conf.optimize
+ AnalyzedCFG graph = conf.optimize
? new OptimizedAnalyzedCFG<>(cfg, ID, entryState.bottom(), this)
: new AnalyzedCFG<>(cfg, ID, entryState);
- CFGResults value = new CFGResults<>(graph);
+ CFGResults value = new CFGResults<>(graph);
this.results = new FixpointResults<>(value.top());
}
- AnalysisState prepared = entryState;
+ AnalysisState prepared = entryState;
for (Parameter arg : cfg.getDescriptor().getFormals()) {
Variable id = new Variable(arg.getStaticType(), arg.getName(), arg.getAnnotations(),
arg.getLocation());
@@ -114,16 +105,16 @@ public void fixpoint(AnalysisState entryState,
}
@Override
- public Collection> getAnalysisResultsOf(CFG cfg) {
+ public Collection> getAnalysisResultsOf(CFG cfg) {
return results.getState(cfg).getAll();
}
@Override
- public AnalysisState getAbstractResultOf(
+ public AnalysisState getAbstractResultOf(
CFGCall call,
- AnalysisState entryState,
+ AnalysisState entryState,
ExpressionSet[] parameters,
- StatementStore expressions)
+ StatementStore expressions)
throws SemanticException {
OpenCall open = new OpenCall(call.getCFG(), call.getLocation(), call.getCallType(), call.getQualifier(),
call.getTargetName(), call.getStaticType(), call.getParameters());
@@ -131,11 +122,11 @@ public AnalysisState getAbstractResultOf(
}
@Override
- public AnalysisState getAbstractResultOf(
+ public AnalysisState getAbstractResultOf(
OpenCall call,
- AnalysisState entryState,
+ AnalysisState entryState,
ExpressionSet[] parameters,
- StatementStore expressions)
+ StatementStore expressions)
throws SemanticException {
return policy.apply(call, entryState, parameters);
}
@@ -155,7 +146,7 @@ public Call resolve(UnresolvedCall call, Set[] types, SymbolAliasing alias
}
@Override
- public FixpointResults getFixpointResults() {
+ public FixpointResults getFixpointResults() {
return results;
}
}
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java
index 2ca03e5c3..87c1e16b6 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/ContextBasedAnalysis.java
@@ -1,19 +1,5 @@
package it.unive.lisa.interprocedural.context;
-import java.util.ArrayList;
-import java.util.Collection;
-import java.util.Collections;
-import java.util.HashSet;
-import java.util.List;
-import java.util.Map.Entry;
-import java.util.Set;
-import java.util.TreeSet;
-import java.util.stream.Collectors;
-
-import org.apache.commons.lang3.tuple.Pair;
-import org.apache.logging.log4j.LogManager;
-import org.apache.logging.log4j.Logger;
-
import it.unive.lisa.AnalysisExecutionException;
import it.unive.lisa.AnalysisSetupException;
import it.unive.lisa.DefaultParameters;
@@ -24,10 +10,7 @@
import it.unive.lisa.analysis.ScopeToken;
import it.unive.lisa.analysis.SemanticException;
import it.unive.lisa.analysis.StatementStore;
-import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.lattices.ExpressionSet;
-import it.unive.lisa.analysis.value.TypeDomain;
-import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.conf.FixpointConfiguration;
import it.unive.lisa.interprocedural.CFGResults;
import it.unive.lisa.interprocedural.CallGraphBasedAnalysis;
@@ -54,6 +37,18 @@
import it.unive.lisa.util.StringUtilities;
import it.unive.lisa.util.collections.workset.WorkingSet;
import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map.Entry;
+import java.util.Set;
+import java.util.TreeSet;
+import java.util.stream.Collectors;
+import org.apache.commons.lang3.tuple.Pair;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
/**
* A context sensitive interprocedural analysis. The context sensitivity is
@@ -61,17 +56,10 @@
* approximated applying the iterates of the recursion starting from bottom and
* using the same widening threshold of cfg fixpoints.
*
- * @param the abstract state of the analysis
- * @param the heap domain
- * @param the value domain
- * @param the type domain
+ * @param the {@link AbstractState} of the analysis
*/
@DefaultParameters({ FullStackToken.class })
-public class ContextBasedAnalysis,
- H extends HeapDomain,
- V extends ValueDomain,
- T extends TypeDomain>
- extends CallGraphBasedAnalysis {
+public class ContextBasedAnalysis> extends CallGraphBasedAnalysis {
private static final Logger LOG = LogManager.getLogger(ContextBasedAnalysis.class);
@@ -91,7 +79,7 @@ public class ContextBasedAnalysis,
/**
* The results computed by this analysis.
*/
- protected FixpointResults results;
+ protected FixpointResults results;
/**
* The kind of {@link WorkingSet} to use during this analysis.
@@ -131,7 +119,7 @@ public ContextBasedAnalysis(ContextSensitivityToken token) {
*
* @param other the original analysis to copy
*/
- protected ContextBasedAnalysis(ContextBasedAnalysis other) {
+ protected ContextBasedAnalysis(ContextBasedAnalysis other) {
super(other);
this.conf = other.conf;
this.results = other.results;
@@ -158,7 +146,7 @@ public void init(
@Override
public void fixpoint(
- AnalysisState entryState,
+ AnalysisState entryState,
Class extends WorkingSet> fixpointWorkingSet,
FixpointConfiguration conf)
throws FixpointException {
@@ -185,9 +173,9 @@ public void fixpoint(
processEntrypoints(entryState, empty, entryPoints);
if (pendingRecursions) {
- Set> recursions = new HashSet<>();
+ Set> recursions = new HashSet<>();
- for (Collection rec : callgraph.getRecursions())
+ for (Collection rec : callgraph.getRecursions())
buildRecursion(entryState, recursions, rec);
solveRecursions(recursions);
@@ -204,9 +192,9 @@ public void fixpoint(
} while (!triggers.isEmpty());
}
- private void solveRecursions(Set> recursions) {
- List> orderedRecursions = new ArrayList<>(recursions.size());
- for (Recursion rec : recursions) {
+ private void solveRecursions(Set> recursions) {
+ List> orderedRecursions = new ArrayList<>(recursions.size());
+ for (Recursion rec : recursions) {
int pos = 0;
for (; pos < orderedRecursions.size(); pos++)
if (orderedRecursions.get(pos).getMembers().contains(rec.getInvocation().getCFG()))
@@ -221,7 +209,7 @@ private void solveRecursions(Set> recursions) {
}
try {
- for (Recursion rec : orderedRecursions) {
+ for (Recursion rec : orderedRecursions) {
new RecursionSolver<>(this, rec).solve();
triggers.addAll(rec.getMembers());
}
@@ -230,7 +218,7 @@ private void solveRecursions(Set> recursions) {
}
}
- private void buildRecursion(AnalysisState entryState, Set> recursions,
+ private void buildRecursion(AnalysisState entryState, Set> recursions,
Collection rec) {
// these are the calls that start the recursion by invoking
// one of its members
@@ -246,13 +234,13 @@ private void buildRecursion(AnalysisState entryState, Set>> entries = new HashSet<>();
- for (Entry> res : results.get(starter.getCFG())) {
- StatementStore params = new StatementStore<>(entryState.bottom());
+ Set>> entries = new HashSet<>();
+ for (Entry> res : results.get(starter.getCFG())) {
+ StatementStore params = new StatementStore<>(entryState.bottom());
Expression[] parameters = starter.getParameters();
if (conf.optimize)
for (Expression actual : parameters)
- params.put(actual, ((OptimizedAnalyzedCFG) res.getValue())
+ params.put(actual, ((OptimizedAnalyzedCFG) res.getValue())
.getUnwindedAnalysisStateAfter(actual, conf));
else
for (Expression actual : parameters)
@@ -263,8 +251,8 @@ private void buildRecursion(AnalysisState entryState, Set> entry : entries) {
- Recursion recursion = new Recursion<>(
+ for (Pair> entry : entries) {
+ Recursion recursion = new Recursion<>(
starter,
entry.getLeft(),
entry.getRight(),
@@ -275,20 +263,20 @@ private void buildRecursion(AnalysisState entryState, Set entryState, ContextSensitivityToken empty,
+ private void processEntrypoints(AnalysisState entryState, ContextSensitivityToken empty,
Collection entryPoints) {
for (CFG cfg : IterationLogger.iterate(LOG, entryPoints, "Processing entrypoints", "entries"))
try {
if (results == null) {
- AnalyzedCFG graph = conf.optimize
+ AnalyzedCFG graph = conf.optimize
? new OptimizedAnalyzedCFG<>(cfg, empty, entryState.bottom(), this)
: new AnalyzedCFG<>(cfg, empty, entryState);
- CFGResults value = new CFGResults<>(graph);
+ CFGResults value = new CFGResults<>(graph);
this.results = new FixpointResults<>(value.top());
}
token = empty;
- AnalysisState entryStateCFG = prepareEntryStateOfEntryPoint(entryState, cfg);
+ AnalysisState entryStateCFG = prepareEntryStateOfEntryPoint(entryState, cfg);
results.putResult(cfg, empty,
cfg.fixpoint(entryStateCFG, this, WorkingSet.of(workingSet), conf, empty));
} catch (SemanticException | AnalysisSetupException e) {
@@ -299,7 +287,7 @@ private void processEntrypoints(AnalysisState entryState, ContextSen
}
@Override
- public Collection> getAnalysisResultsOf(CFG cfg) {
+ public Collection> getAnalysisResultsOf(CFG cfg) {
if (results.contains(cfg))
return results.getState(cfg).getAll();
else
@@ -321,19 +309,19 @@ public Collection> getAnalysisResultsOf(CFG cfg) {
* @throws AnalysisSetupException if the {@link WorkingSet} for the fixpoint
* cannot be created
*/
- private AnalyzedCFG computeFixpoint(
+ private AnalyzedCFG computeFixpoint(
CFG cfg,
ContextSensitivityToken token,
- AnalysisState entryState)
+ AnalysisState entryState)
throws FixpointException, SemanticException, AnalysisSetupException {
- AnalyzedCFG fixpointResult = cfg.fixpoint(
+ AnalyzedCFG fixpointResult = cfg.fixpoint(
entryState,
this,
WorkingSet.of(workingSet),
conf,
token);
if (shouldStoreFixpointResults()) {
- Pair> res = results.putResult(cfg, token, fixpointResult);
+ Pair> res = results.putResult(cfg, token, fixpointResult);
if (shouldStoreFixpointResults() && Boolean.TRUE.equals(res.getLeft()))
triggers.add(cfg);
fixpointResult = res.getRight();
@@ -376,31 +364,31 @@ protected boolean shouldStoreFixpointResults() {
}
@Override
- public FixpointResults getFixpointResults() {
+ public FixpointResults getFixpointResults() {
return results;
}
- private Pair, ExpressionSet[]> prepareEntryState(
+ private Pair, ExpressionSet[]> prepareEntryState(
CFGCall call,
- AnalysisState entryState,
+ AnalysisState entryState,
ExpressionSet[] parameters,
- StatementStore expressions,
+ StatementStore expressions,
ScopeToken scope,
CFG cfg)
throws SemanticException {
Parameter[] formals = cfg.getDescriptor().getFormals();
// prepare the state for the call: hide the visible variables
- Pair, ExpressionSet[]> scoped = scope(
+ Pair, ExpressionSet[]> scoped = scope(
entryState,
scope,
parameters);
- AnalysisState callState = scoped.getLeft();
+ AnalysisState callState = scoped.getLeft();
ExpressionSet[] locals = scoped.getRight();
// assign parameters between the caller and the callee contexts
ParameterAssigningStrategy strategy = call.getProgram().getFeatures().getAssigningStrategy();
- Pair, ExpressionSet[]> prepared = strategy.prepare(
+ Pair, ExpressionSet[]> prepared = strategy.prepare(
call,
callState,
this,
@@ -411,11 +399,11 @@ private Pair, ExpressionSet[]> pre
}
@Override
- public AnalysisState getAbstractResultOf(
+ public AnalysisState getAbstractResultOf(
CFGCall call,
- AnalysisState entryState,
+ AnalysisState entryState,
ExpressionSet[] parameters,
- StatementStore expressions)
+ StatementStore expressions)
throws SemanticException {
callgraph.registerCall(call);
@@ -440,14 +428,14 @@ public AnalysisState getAbstractResultOf(
ContextSensitivityToken callerToken = token;
token = token.push(call);
ScopeToken scope = new ScopeToken(call);
- AnalysisState result = entryState.bottom();
+ AnalysisState result = entryState.bottom();
// compute the result over all possible targets, and take the lub of
// the results
for (CFG cfg : call.getTargetedCFGs()) {
- CFGResults localResults = results.get(cfg);
- AnalyzedCFG states = localResults == null ? null : localResults.get(token);
- Pair, ExpressionSet[]> prepared = prepareEntryState(
+ CFGResults localResults = results.get(cfg);
+ AnalyzedCFG states = localResults == null ? null : localResults.get(token);
+ Pair, ExpressionSet[]> prepared = prepareEntryState(
call,
entryState,
parameters,
@@ -455,7 +443,7 @@ public AnalysisState getAbstractResultOf(
scope,
cfg);
- AnalysisState exitState;
+ AnalysisState exitState;
if (canShortcut(cfg) && states != null && prepared.getLeft().lessOrEqual(states.getEntryState()))
// no need to compute the fixpoint: we already have an
// (over-)approximation of the result computed starting from
@@ -463,7 +451,7 @@ public AnalysisState getAbstractResultOf(
exitState = states.getExitState();
else {
// compute the result with a fixpoint iteration
- AnalyzedCFG fixpointResult = null;
+ AnalyzedCFG fixpointResult = null;
try {
fixpointResult = computeFixpoint(cfg, token, prepared.getLeft());
} catch (FixpointException | AnalysisSetupException e) {
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java
index 3850c15ed..c8b1c23c0 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/BaseCasesFinder.java
@@ -4,10 +4,7 @@
import it.unive.lisa.analysis.AnalysisState;
import it.unive.lisa.analysis.SemanticException;
import it.unive.lisa.analysis.StatementStore;
-import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.lattices.ExpressionSet;
-import it.unive.lisa.analysis.value.TypeDomain;
-import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.conf.FixpointConfiguration;
import it.unive.lisa.interprocedural.InterproceduralAnalysisException;
import it.unive.lisa.interprocedural.OpenCallPolicy;
@@ -35,20 +32,10 @@
*
* @param the type of {@link AbstractState} contained into the analysis
* state
- * @param the type of {@link HeapDomain} contained into the computed
- * abstract state
- * @param the type of {@link ValueDomain} contained into the computed
- * abstract state
- * @param the type of {@link TypeDomain} contained into the computed
- * abstract state
*/
-public class BaseCasesFinder,
- H extends HeapDomain,
- V extends ValueDomain,
- T extends TypeDomain>
- extends ContextBasedAnalysis {
+public class BaseCasesFinder> extends ContextBasedAnalysis {
- private final Recursion recursion;
+ private final Recursion recursion;
private final boolean returnsVoid;
@@ -61,8 +48,8 @@ public class BaseCasesFinder,
* @param returnsVoid whether or not the recursion returns void
*/
public BaseCasesFinder(
- ContextBasedAnalysis backing,
- Recursion recursion,
+ ContextBasedAnalysis backing,
+ Recursion recursion,
boolean returnsVoid) {
super(backing);
this.recursion = recursion;
@@ -82,7 +69,7 @@ public void init(
@Override
public void fixpoint(
- AnalysisState entryState,
+ AnalysisState entryState,
Class extends WorkingSet> fixpointWorkingSet,
FixpointConfiguration conf)
throws FixpointException {
@@ -92,11 +79,11 @@ public void fixpoint(
}
@Override
- public AnalysisState getAbstractResultOf(
+ public AnalysisState getAbstractResultOf(
CFGCall call,
- AnalysisState entryState,
+ AnalysisState entryState,
ExpressionSet[] parameters,
- StatementStore expressions)
+ StatementStore expressions)
throws SemanticException {
boolean inRecursion = recursion.getMembers().contains(call.getCFG());
if (inRecursion && call.getTargetedCFGs().contains(recursion.getRecursionHead())) {
@@ -136,9 +123,9 @@ protected boolean shouldStoreFixpointResults() {
*
* @throws SemanticException if an exception happens during the computation
*/
- public AnalysisState find() throws SemanticException {
+ public AnalysisState find() throws SemanticException {
Call start = recursion.getInvocation();
- CompoundState entryState = recursion.getEntryState();
+ CompoundState entryState = recursion.getEntryState();
// we reset the analysis at the point where the starting call can be
// evaluated
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/Recursion.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/Recursion.java
index ccebf8d8a..7d74b97bc 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/Recursion.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/Recursion.java
@@ -1,9 +1,6 @@
package it.unive.lisa.interprocedural.context.recursion;
import it.unive.lisa.analysis.AbstractState;
-import it.unive.lisa.analysis.heap.HeapDomain;
-import it.unive.lisa.analysis.value.TypeDomain;
-import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.interprocedural.context.ContextSensitivityToken;
import it.unive.lisa.program.cfg.CFG;
import it.unive.lisa.program.cfg.CodeMember;
@@ -18,18 +15,8 @@
*
* @param the type of {@link AbstractState} contained into the analysis
* state
- * @param the type of {@link HeapDomain} contained into the computed
- * abstract state
- * @param the type of {@link ValueDomain} contained into the computed
- * abstract state
- * @param the type of {@link TypeDomain} contained into the computed
- * abstract state
*/
-public class Recursion<
- A extends AbstractState,
- H extends HeapDomain,
- V extends ValueDomain,
- T extends TypeDomain> {
+public class Recursion> {
private final Call start;
@@ -39,7 +26,7 @@ public class Recursion<
private final ContextSensitivityToken invocationToken;
- private final CompoundState entryState;
+ private final CompoundState entryState;
/**
* Builds the recursion.
@@ -57,7 +44,7 @@ public class Recursion<
public Recursion(
Call invocation,
ContextSensitivityToken invocationToken,
- CompoundState entryState,
+ CompoundState entryState,
CFG recursionHead,
Collection members) {
this.start = invocation;
@@ -87,7 +74,7 @@ public boolean equals(Object obj) {
return false;
if (getClass() != obj.getClass())
return false;
- Recursion, ?, ?, ?> other = (Recursion, ?, ?, ?>) obj;
+ Recursion> other = (Recursion>) obj;
if (entryState == null) {
if (other.entryState != null)
return false;
@@ -153,7 +140,7 @@ public ContextSensitivityToken getInvocationToken() {
*
* @return the entry state
*/
- public CompoundState getEntryState() {
+ public CompoundState getEntryState() {
return entryState;
}
diff --git a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/RecursionSolver.java b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/RecursionSolver.java
index 3808a0ca8..d1ffa0faa 100644
--- a/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/RecursionSolver.java
+++ b/lisa/lisa-analyses/src/main/java/it/unive/lisa/interprocedural/context/recursion/RecursionSolver.java
@@ -5,11 +5,8 @@
import it.unive.lisa.analysis.OptimizedAnalyzedCFG;
import it.unive.lisa.analysis.SemanticException;
import it.unive.lisa.analysis.StatementStore;
-import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.lattices.ExpressionSet;
import it.unive.lisa.analysis.lattices.GenericMapLattice;
-import it.unive.lisa.analysis.value.TypeDomain;
-import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.conf.FixpointConfiguration;
import it.unive.lisa.interprocedural.InterproceduralAnalysisException;
import it.unive.lisa.interprocedural.OpenCallPolicy;
@@ -45,34 +42,24 @@
*
* @param the type of {@link AbstractState} contained into the analysis
* state
- * @param the type of {@link HeapDomain} contained into the computed
- * abstract state
- * @param the type of {@link ValueDomain} contained into the computed
- * abstract state
- * @param the type of {@link TypeDomain} contained into the computed
- * abstract state
*/
-public class RecursionSolver,
- H extends HeapDomain,
- V extends ValueDomain,
- T extends TypeDomain>
- extends ContextBasedAnalysis {
+public class RecursionSolver> extends ContextBasedAnalysis {
private static final Logger LOG = LogManager.getLogger(RecursionSolver.class);
- private final Recursion recursion;
+ private final Recursion recursion;
private final boolean returnsVoid;
- private final Map, ContextSensitivityToken>> finalEntryStates;
+ private final Map, ContextSensitivityToken>> finalEntryStates;
- private final BaseCasesFinder baseCases;
+ private final BaseCasesFinder baseCases;
- private GenericMapLattice> previousApprox;
+ private GenericMapLattice> previousApprox;
- private GenericMapLattice> recursiveApprox;
+ private GenericMapLattice> recursiveApprox;
- private AnalysisState base;
+ private AnalysisState base;
/**
* Builds the solver.
@@ -81,7 +68,7 @@ public class RecursionSolver,
* used to query call results
* @param recursion the recursion to solve
*/
- public RecursionSolver(ContextBasedAnalysis backing, Recursion recursion) {
+ public RecursionSolver(ContextBasedAnalysis backing, Recursion recursion) {
super(backing);
this.recursion = recursion;
finalEntryStates = new HashMap<>();
@@ -104,7 +91,7 @@ public void init(
@Override
public void fixpoint(
- AnalysisState entryState,
+ AnalysisState entryState,
Class extends WorkingSet> fixpointWorkingSet,
FixpointConfiguration conf)
throws FixpointException {
@@ -114,18 +101,18 @@ public void fixpoint(
}
@Override
- public AnalysisState getAbstractResultOf(
+ public AnalysisState getAbstractResultOf(
CFGCall call,
- AnalysisState entryState,
+ AnalysisState entryState,
ExpressionSet[] parameters,
- StatementStore expressions)
+ StatementStore expressions)
throws SemanticException {
boolean inRecursion = recursion.getMembers().contains(call.getCFG());
if (inRecursion && call.getTargetedCFGs().contains(recursion.getRecursionHead())) {
// this is a back call
finalEntryStates.put(call, Pair.of(entryState, token));
- AnalysisState approx = null;
+ AnalysisState approx = null;
if (recursiveApprox.getMap() != null)
approx = recursiveApprox.getMap().get(call);
if (approx == null)
@@ -157,7 +144,7 @@ public void solve() throws SemanticException {
int recursionCount = 0;
Call start = recursion.getInvocation();
Collection ends = finalEntryStates.keySet();
- CompoundState entryState = recursion.getEntryState();
+ CompoundState entryState = recursion.getEntryState();
LOG.info("Solving recursion at " + start.getLocation() + " for context " + recursion.getInvocationToken());
@@ -181,7 +168,7 @@ public void solve() throws SemanticException {
// we reset the analysis at the point where the starting call can be
// evaluated
token = recursion.getInvocationToken();
- AnalysisState post = start.expressionSemantics(
+ AnalysisState post = start.expressionSemantics(
this,
entryState.postState,
params,
@@ -205,12 +192,12 @@ else if (recursionCount == conf.recursionWideningThreshold)
// recursive call, we need to store the approximation for the
// recursive call manually or the unwinding won't manage to solve it
for (CFGCall call : ends) {
- Pair, ContextSensitivityToken> pair = finalEntryStates.get(call);
- AnalysisState callEntry = pair.getLeft();
+ Pair, ContextSensitivityToken> pair = finalEntryStates.get(call);
+ AnalysisState callEntry = pair.getLeft();
ContextSensitivityToken callingToken = pair.getRight();
// we get the cfg containing the call
- OptimizedAnalyzedCFG caller = (OptimizedAnalyzedCFG) results.get(call.getCFG())
+ OptimizedAnalyzedCFG caller = (OptimizedAnalyzedCFG) results.get(call.getCFG())
.get(callingToken);
// we get the actual call that is part of the cfg
@@ -223,8 +210,8 @@ else if (recursionCount == conf.recursionWideningThreshold)
if (!caller.hasPostStateOf(source)) {
// we add the value to the entry state, bringing in also the
// base case
- AnalysisState local = transferToCallsite(start, call, base);
- AnalysisState returned = callEntry.lub(recursiveApprox.getState(call).lub(local));
+ AnalysisState local = transferToCallsite(start, call, base);
+ AnalysisState returned = callEntry.lub(recursiveApprox.getState(call).lub(local));
// finally, we store it in the result
caller.storePostStateOf(source, returned);
@@ -232,12 +219,12 @@ else if (recursionCount == conf.recursionWideningThreshold)
}
}
- private AnalysisState transferToCallsite(
+ private AnalysisState transferToCallsite(
Call original,
CFGCall destination,
- AnalysisState state)
+ AnalysisState state)
throws SemanticException {
- AnalysisState res = state.bottom();
+ AnalysisState res = state.bottom();
Identifier meta = destination.getMetaVariable();
if (returnsVoid)
res = state;
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/CharInclusionTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/CharInclusionTest.java
index daf16df8e..521a98237 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/CharInclusionTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/CharInclusionTest.java
@@ -1,6 +1,8 @@
package it.unive.lisa.analysis.string;
-import static org.junit.Assert.*;
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
import it.unive.lisa.analysis.SemanticException;
import java.util.Set;
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/PrefixTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/PrefixTest.java
index fee62fe0c..bb3c08a59 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/PrefixTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/PrefixTest.java
@@ -1,6 +1,8 @@
package it.unive.lisa.analysis.string;
-import static org.junit.Assert.*;
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
import it.unive.lisa.analysis.SemanticException;
import org.junit.Test;
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/SuffixTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/SuffixTest.java
index 2d15ef100..9c5b24c50 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/SuffixTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/SuffixTest.java
@@ -1,6 +1,8 @@
package it.unive.lisa.analysis.string;
-import static org.junit.Assert.*;
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
import it.unive.lisa.analysis.SemanticException;
import org.junit.Test;
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/bricks/BrickTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/bricks/BrickTest.java
index 718da93c6..3a8dde802 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/bricks/BrickTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/bricks/BrickTest.java
@@ -1,6 +1,8 @@
package it.unive.lisa.analysis.string.bricks;
-import static org.junit.Assert.*;
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
import it.unive.lisa.analysis.SemanticException;
import java.util.HashSet;
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/bricks/BricksTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/bricks/BricksTest.java
index 95fc7d926..18d6fa600 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/bricks/BricksTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/string/bricks/BricksTest.java
@@ -1,11 +1,16 @@
package it.unive.lisa.analysis.string.bricks;
-import static org.junit.Assert.*;
+import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertFalse;
+import static org.junit.Assert.assertTrue;
import it.unive.lisa.analysis.SemanticException;
import it.unive.lisa.util.numeric.IntInterval;
import it.unive.lisa.util.numeric.MathNumber;
-import java.util.*;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Set;
+import java.util.TreeSet;
import org.junit.Test;
public class BricksTest {
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/nonInterference/NonInterferenceTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/nonInterference/NonInterferenceTest.java
index 255670fdc..eaae5d8e6 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/nonInterference/NonInterferenceTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/nonInterference/NonInterferenceTest.java
@@ -81,20 +81,14 @@ public void testDeclassification() throws AnalysisSetupException {
private static class NICheck
implements SemanticCheck<
SimpleAbstractState,
- TypeEnvironment>,
- MonolithicHeap,
- InferenceSystem,
- TypeEnvironment> {
+ TypeEnvironment>> {
@Override
@SuppressWarnings({ "unchecked" })
public boolean visit(
CheckToolWithAnalysisResults<
SimpleAbstractState,
- TypeEnvironment>,
- MonolithicHeap,
- InferenceSystem,
- TypeEnvironment> tool,
+ TypeEnvironment>> tool,
CFG graph, Statement node) {
if (!(node instanceof Assignment))
return true;
@@ -104,12 +98,12 @@ public boolean visit(
for (Object res : results)
try {
- AnalyzedCFG, ?, ?, ?> result = (AnalyzedCFG, ?, ?, ?>) res;
- AnalysisState, ?, ?, ?> post = result.getAnalysisStateAfter(assign);
+ AnalyzedCFG> result = (AnalyzedCFG>) res;
+ AnalysisState> post = result.getAnalysisStateAfter(assign);
InferenceSystem state = post.getDomainInstance(InferenceSystem.class);
- AnalysisState, ?, ?, ?> postL = result.getAnalysisStateAfter(assign.getLeft());
+ AnalysisState> postL = result.getAnalysisStateAfter(assign.getLeft());
InferenceSystem left = postL.getDomainInstance(InferenceSystem.class);
- AnalysisState, ?, ?, ?> postR = result.getAnalysisStateAfter(assign.getRight());
+ AnalysisState> postR = result.getAnalysisStateAfter(assign.getRight());
InferenceSystem right = postR.getDomainInstance(InferenceSystem.class);
for (SymbolicExpression l : postL.getState().rewrite(postL.getComputedExpressions(), assign))
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/taint/TaintAnalysesTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/taint/TaintAnalysesTest.java
index d073a41fe..b532ef610 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/taint/TaintAnalysesTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/taint/TaintAnalysesTest.java
@@ -77,18 +77,12 @@ public void testThreeLevelsTaint() throws AnalysisSetupException {
private static class TaintCheck>
implements SemanticCheck<
- SimpleAbstractState, TypeEnvironment>,
- MonolithicHeap,
- ValueEnvironment,
- TypeEnvironment> {
+ SimpleAbstractState, TypeEnvironment>> {
@Override
public boolean visit(
CheckToolWithAnalysisResults<
- SimpleAbstractState, TypeEnvironment>,
- MonolithicHeap,
- ValueEnvironment,
- TypeEnvironment> tool,
+ SimpleAbstractState, TypeEnvironment>> tool,
CFG graph, Statement node) {
if (!(node instanceof UnresolvedCall))
return true;
@@ -100,10 +94,7 @@ public boolean visit(
SimpleAbstractState<
MonolithicHeap,
ValueEnvironment,
- TypeEnvironment>,
- MonolithicHeap,
- ValueEnvironment,
- TypeEnvironment> result : tool.getResultOf(call.getCFG())) {
+ TypeEnvironment>> result : tool.getResultOf(call.getCFG())) {
Call resolved = (Call) tool.getResolvedVersion(call, result);
if (resolved instanceof CFGCall) {
@@ -113,9 +104,7 @@ public boolean visit(
for (int i = 0; i < parameters.length; i++)
if (parameters[i].getAnnotations().contains(BaseTaint.CLEAN_MATCHER)) {
AnalysisState,
- TypeEnvironment>,
- MonolithicHeap, ValueEnvironment,
- TypeEnvironment> post = result
+ TypeEnvironment>> post = result
.getAnalysisStateAfter(call.getParameters()[i]);
for (SymbolicExpression e : post.getState().rewrite(post.getComputedExpressions(),
node)) {
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java
index 4407f547b..834c83c85 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java
@@ -51,16 +51,12 @@ public static void init() {
}
private ModularWorstCaseAnalysis<
- SimpleAbstractState, TypeEnvironment>,
- MonolithicHeap,
- ValueEnvironment,
- TypeEnvironment> mkAnalysis(Program p)
+ SimpleAbstractState, TypeEnvironment>> mkAnalysis(
+ Program p)
throws InterproceduralAnalysisException, CallGraphConstructionException {
ModularWorstCaseAnalysis<
- SimpleAbstractState, TypeEnvironment>,
- MonolithicHeap,
- ValueEnvironment,
- TypeEnvironment> analysis = new ModularWorstCaseAnalysis<>();
+ SimpleAbstractState,
+ TypeEnvironment>> analysis = new ModularWorstCaseAnalysis<>();
RTACallGraph callgraph = new RTACallGraph();
Application app = new Application(p);
callgraph.init(app);
@@ -69,10 +65,7 @@ TypeEnvironment> mkAnalysis(Program p)
}
private AnalysisState<
- SimpleAbstractState, TypeEnvironment>,
- MonolithicHeap,
- ValueEnvironment,
- TypeEnvironment> mkState() {
+ SimpleAbstractState, TypeEnvironment>> mkState() {
return new AnalysisState<>(
new SimpleAbstractState<>(
new MonolithicHeap(),
@@ -129,16 +122,12 @@ public void testMetaVariablesOfRootExpressions()
cfg.addNode(call, true);
AnalysisState<
- SimpleAbstractState, TypeEnvironment>,
- MonolithicHeap,
- ValueEnvironment,
- TypeEnvironment> domain = mkState();
+ SimpleAbstractState,
+ TypeEnvironment>> domain = mkState();
AnalyzedCFG<
- SimpleAbstractState, TypeEnvironment>,
- MonolithicHeap,
- ValueEnvironment,
- TypeEnvironment> result = cfg.fixpoint(domain,
- mkAnalysis(program), FIFOWorkingSet.mk(), conf, new UniqueScope());
+ SimpleAbstractState,
+ TypeEnvironment>> result = cfg.fixpoint(domain,
+ mkAnalysis(program), FIFOWorkingSet.mk(), conf, new UniqueScope());
assertTrue(result.getAnalysisStateAfter(call).getState().getValueState().getKeys().isEmpty());
}
diff --git a/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java b/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java
index a5d13a1e5..79f96365a 100644
--- a/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java
+++ b/lisa/lisa-analyses/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java
@@ -100,21 +100,12 @@ public class SemanticsSanityTest {
private ClassUnit unit;
private CFG cfg;
private CallGraph cg;
- private InterproceduralAnalysis<
- SimpleAbstractState, TypeEnvironment>,
- MonolithicHeap,
- ValueEnvironment