From 8418f32469b15e947ab24afb749e1c376348f850 Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Thu, 7 Sep 2023 18:29:43 +0200 Subject: [PATCH] Removing non-essential type parameters from AnalysisState --- .../lisa/analysis/SimpleAbstractState.java | 39 +++-- .../analysis/traces/TracePartitioning.java | 48 +++--- .../CallGraphBasedAnalysis.java | 27 ++-- .../ModularWorstCaseAnalysis.java | 39 ++--- .../context/ContextBasedAnalysis.java | 122 +++++++-------- .../context/recursion/BaseCasesFinder.java | 33 ++--- .../context/recursion/Recursion.java | 23 +-- .../context/recursion/RecursionSolver.java | 59 +++----- .../analysis/string/CharInclusionTest.java | 4 +- .../lisa/analysis/string/PrefixTest.java | 4 +- .../lisa/analysis/string/SuffixTest.java | 4 +- .../analysis/string/bricks/BrickTest.java | 4 +- .../analysis/string/bricks/BricksTest.java | 9 +- .../nonInterference/NonInterferenceTest.java | 18 +-- .../lisa/cron/taint/TaintAnalysesTest.java | 19 +-- .../lisa/program/cfg/CFGFixpointTest.java | 31 ++-- .../lisa/program/cfg/SemanticsSanityTest.java | 28 +--- .../lisa/imp/expressions/IMPAddOrConcat.java | 22 +-- .../lisa/imp/expressions/IMPArrayAccess.java | 20 +-- .../unive/lisa/imp/expressions/IMPAssert.java | 21 +-- .../lisa/imp/expressions/IMPNewArray.java | 24 ++- .../unive/lisa/imp/expressions/IMPNewObj.java | 36 ++--- .../cfg/statement/comparison/Equal.java | 20 +-- .../statement/comparison/GreaterOrEqual.java | 20 +-- .../cfg/statement/comparison/GreaterThan.java | 20 +-- .../cfg/statement/comparison/LessOrEqual.java | 20 +-- .../cfg/statement/comparison/LessThan.java | 20 +-- .../cfg/statement/comparison/NotEqual.java | 20 +-- .../cfg/statement/global/AccessGlobal.java | 12 +- .../global/AccessInstanceGlobal.java | 20 +-- .../cfg/statement/literal/NullLiteral.java | 14 +- .../lisa/program/cfg/statement/logic/And.java | 20 +-- .../lisa/program/cfg/statement/logic/Not.java | 18 +-- .../lisa/program/cfg/statement/logic/Or.java | 20 +-- .../cfg/statement/numeric/Addition.java | 20 +-- .../cfg/statement/numeric/Division.java | 20 +-- .../program/cfg/statement/numeric/Modulo.java | 20 +-- .../cfg/statement/numeric/Multiplication.java | 20 +-- .../cfg/statement/numeric/Negation.java | 18 +-- .../cfg/statement/numeric/Remainder.java | 20 +-- .../cfg/statement/numeric/Subtraction.java | 20 +-- .../program/cfg/statement/string/Concat.java | 20 +-- .../cfg/statement/string/Contains.java | 20 +-- .../cfg/statement/string/EndsWith.java | 20 +-- .../program/cfg/statement/string/Equals.java | 20 +-- .../program/cfg/statement/string/IndexOf.java | 20 +-- .../program/cfg/statement/string/Length.java | 18 +-- .../program/cfg/statement/string/Replace.java | 22 +-- .../cfg/statement/string/StartsWith.java | 20 +-- .../cfg/statement/string/Substring.java | 22 +-- .../main/java/it/unive/lisa/LiSARunner.java | 30 ++-- .../it/unive/lisa/analysis/AbstractState.java | 19 +-- .../it/unive/lisa/analysis/AnalysisState.java | 60 ++++---- .../it/unive/lisa/analysis/AnalyzedCFG.java | 62 ++++---- .../lisa/analysis/OptimizedAnalyzedCFG.java | 140 ++++++++---------- .../unive/lisa/analysis/StatementStore.java | 27 ++-- .../CheckToolWithAnalysisResults.java | 30 ++-- .../lisa/checks/semantic/SemanticCheck.java | 11 +- .../it/unive/lisa/conf/LiSAConfiguration.java | 6 +- .../lisa/interprocedural/CFGResults.java | 42 ++---- .../lisa/interprocedural/FixpointResults.java | 36 ++--- .../InterproceduralAnalysis.java | 47 +++--- .../lisa/interprocedural/OpenCallPolicy.java | 22 +-- .../lisa/interprocedural/ReturnTopPolicy.java | 16 +- .../lisa/interprocedural/WorstCasePolicy.java | 18 +-- .../serializableGraph/SerializableCFG.java | 4 +- .../java/it/unive/lisa/program/cfg/CFG.java | 107 +++++-------- .../it/unive/lisa/program/cfg/edge/Edge.java | 15 +- .../lisa/program/cfg/edge/FalseEdge.java | 14 +- .../lisa/program/cfg/edge/SequentialEdge.java | 9 +- .../unive/lisa/program/cfg/edge/TrueEdge.java | 14 +- .../cfg/fixpoints/AscendingFixpoint.java | 32 ++-- .../program/cfg/fixpoints/CFGFixpoint.java | 88 ++++------- .../cfg/fixpoints/DescendingGLBFixpoint.java | 27 +--- .../DescendingNarrowingFixpoint.java | 31 ++-- .../cfg/fixpoints/OptimizedFixpoint.java | 49 +++--- .../program/cfg/statement/Assignment.java | 20 +-- .../cfg/statement/BinaryExpression.java | 40 ++--- .../cfg/statement/BinaryStatement.java | 40 ++--- .../program/cfg/statement/Expression.java | 12 +- .../program/cfg/statement/NaryExpression.java | 37 ++--- .../program/cfg/statement/NaryStatement.java | 37 ++--- .../lisa/program/cfg/statement/NoOp.java | 16 +- .../unive/lisa/program/cfg/statement/Ret.java | 16 +- .../lisa/program/cfg/statement/Return.java | 18 +-- .../lisa/program/cfg/statement/Statement.java | 19 +-- .../cfg/statement/TernaryExpression.java | 42 ++---- .../cfg/statement/TernaryStatement.java | 42 ++---- .../lisa/program/cfg/statement/Throw.java | 18 +-- .../cfg/statement/UnaryExpression.java | 38 ++--- .../program/cfg/statement/UnaryStatement.java | 38 ++--- .../program/cfg/statement/VariableRef.java | 14 +- .../program/cfg/statement/call/CFGCall.java | 18 +-- .../lisa/program/cfg/statement/call/Call.java | 25 +--- .../cfg/statement/call/CallWithResult.java | 38 ++--- .../program/cfg/statement/call/MultiCall.java | 20 +-- .../call/NamedParameterExpression.java | 18 +-- .../cfg/statement/call/NativeCall.java | 22 +-- .../program/cfg/statement/call/OpenCall.java | 18 +-- .../statement/call/TruncatedParamsCall.java | 20 +-- .../cfg/statement/call/UnresolvedCall.java | 20 +-- .../statement/evaluation/EvaluationOrder.java | 23 +-- .../evaluation/LeftToRightEvaluation.java | 24 ++- .../evaluation/RightToLeftEvaluation.java | 24 ++- .../cfg/statement/literal/Literal.java | 16 +- .../OrderPreservingAssigningStrategy.java | 26 ++-- .../ParameterAssigningStrategy.java | 25 +--- .../PythonLikeAssigningStrategy.java | 36 ++--- .../java/it/unive/lisa/TestAbstractState.java | 7 +- .../unive/lisa/analysis/AnalyzedCFGTest.java | 21 +-- .../CheckToolWithAnalysisResultsTest.java | 49 +++--- .../cfg/fixpoints/OptimizedFixpointTest.java | 77 +++++----- 112 files changed, 1127 insertions(+), 1981 deletions(-) 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> 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> 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> 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> 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, - TypeEnvironment> interprocedural; + private InterproceduralAnalysis, + TypeEnvironment>> interprocedural; private AnalysisState< - SimpleAbstractState, TypeEnvironment>, - MonolithicHeap, - ValueEnvironment, - TypeEnvironment> as; + SimpleAbstractState, TypeEnvironment>> as; private StatementStore< - SimpleAbstractState, TypeEnvironment>, - MonolithicHeap, - ValueEnvironment, - TypeEnvironment> store; + SimpleAbstractState, TypeEnvironment>> store; private Expression fake; @Before @@ -153,13 +144,10 @@ public String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, StatementStore expressions) - throws SemanticException { + public > AnalysisState semantics( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, StatementStore expressions) + throws SemanticException { return entryState .smallStepSemantics( new Variable(Untyped.INSTANCE, "fake", diff --git a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAddOrConcat.java b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAddOrConcat.java index de78a535b..a02c1ed98 100644 --- a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAddOrConcat.java +++ b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAddOrConcat.java @@ -5,9 +5,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.SourceCodeLocation; import it.unive.lisa.program.cfg.CFG; @@ -54,17 +51,14 @@ public IMPAddOrConcat(CFG cfg, String sourceFile, int line, int col, Expression } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { - AnalysisState result = state.bottom(); + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { + AnalysisState result = state.bottom(); BinaryOperator op; TypeSystem types = getProgram().getTypes(); diff --git a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPArrayAccess.java b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPArrayAccess.java index 457f5e633..1897d7dcc 100644 --- a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPArrayAccess.java +++ b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPArrayAccess.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.SourceCodeLocation; import it.unive.lisa.program.cfg.CFG; @@ -46,16 +43,13 @@ public IMPArrayAccess(CFG cfg, String sourceFile, int line, int col, Expression } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { Set arraytypes = new HashSet<>(); TypeSystem types = getProgram().getTypes(); for (Type t : left.getRuntimeTypes(types)) diff --git a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAssert.java b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAssert.java index e93c2bca8..bd90369b9 100644 --- a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAssert.java +++ b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAssert.java @@ -1,14 +1,9 @@ package it.unive.lisa.imp.expressions; -import java.util.Set; - import it.unive.lisa.analysis.AbstractState; 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.SourceCodeLocation; import it.unive.lisa.program.cfg.CFG; @@ -17,6 +12,7 @@ import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Skip; import it.unive.lisa.type.Type; +import java.util.Set; /** * An assertion in an IMP program. @@ -39,15 +35,12 @@ public IMPAssert(CFG cfg, String sourceFile, int line, int col, Expression expre } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException { + public > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException { Set types = state.getState().getRuntimeTypesOf(expr, this); if (types.stream().noneMatch(Type::isBooleanType)) return state.bottom(); diff --git a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewArray.java b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewArray.java index 00afb9e69..31509f0a3 100644 --- a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewArray.java +++ b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewArray.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.imp.types.ArrayType; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.SourceCodeLocation; @@ -54,23 +51,20 @@ public IMPNewArray(CFG cfg, String sourceFile, int line, int col, Type type, boo } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { MemoryAllocation alloc = new MemoryAllocation(getStaticType(), getLocation(), staticallyAllocated); - AnalysisState sem = state.smallStepSemantics(alloc, this); + AnalysisState sem = state.smallStepSemantics(alloc, this); - AnalysisState result = state.bottom(); + AnalysisState result = state.bottom(); for (SymbolicExpression loc : sem.getComputedExpressions()) { ReferenceType staticType = new ReferenceType(loc.getStaticType()); HeapReference ref = new HeapReference(staticType, loc, getLocation()); - AnalysisState refSem = sem.smallStepSemantics(ref, this); + AnalysisState refSem = sem.smallStepSemantics(ref, this); result = result.lub(refSem); } diff --git a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewObj.java b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewObj.java index 17e9b3be4..60e2fd04b 100644 --- a/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewObj.java +++ b/lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewObj.java @@ -1,18 +1,10 @@ package it.unive.lisa.imp.expressions; -import java.util.Collections; -import java.util.Objects; - -import org.apache.commons.lang3.ArrayUtils; - import it.unive.lisa.analysis.AbstractState; 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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.SourceCodeLocation; import it.unive.lisa.program.cfg.CFG; @@ -28,6 +20,9 @@ import it.unive.lisa.type.ReferenceType; import it.unive.lisa.type.Type; import it.unive.lisa.type.UnitType; +import java.util.Collections; +import java.util.Objects; +import org.apache.commons.lang3.ArrayUtils; /** * An expression modeling the object allocation and initialization operation @@ -65,15 +60,12 @@ public IMPNewObj(CFG cfg, String sourceFile, int line, int col, Type type, boole } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { Type type = getStaticType(); ReferenceType reftype = new ReferenceType(type); MemoryAllocation created = new MemoryAllocation(type, getLocation(), staticallyAllocated); @@ -86,9 +78,9 @@ T extends TypeDomain> AnalysisState expressionSemantics( Expression[] fullExpressions = ArrayUtils.insert(0, getSubExpressions(), paramThis); // we also have to add the receiver inside the state - AnalysisState callstate = paramThis.semantics(state, interprocedural, expressions); - AnalysisState tmp = state.bottom(); - for (SymbolicExpression v : callstate.getComputedExpressions()) + AnalysisState callstate = paramThis.semantics(state, interprocedural, expressions); + AnalysisState tmp = state.bottom(); + for (SymbolicExpression v : callstate.getComputedExpressions()) tmp = tmp.lub(callstate.assign(v, ref, paramThis)); ExpressionSet[] fullParams = ArrayUtils.insert(0, params, callstate.getComputedExpressions()); @@ -96,7 +88,7 @@ T extends TypeDomain> AnalysisState expressionSemantics( UnresolvedCall call = new UnresolvedCall(getCFG(), getLocation(), CallType.INSTANCE, type.toString(), type.toString(), fullExpressions); - AnalysisState sem = call.expressionSemantics(interprocedural, tmp, fullParams, expressions); + AnalysisState sem = call.expressionSemantics(interprocedural, tmp, fullParams, expressions); // now remove the instrumented receiver expressions.forget(paramThis); @@ -106,7 +98,7 @@ T extends TypeDomain> AnalysisState expressionSemantics( sem = sem.smallStepSemantics(created, this); - AnalysisState result = state.bottom(); + AnalysisState result = state.bottom(); for (SymbolicExpression loc : sem.getComputedExpressions()) { ReferenceType staticType = new ReferenceType(loc.getStaticType()); HeapReference locref = new HeapReference(staticType, loc, getLocation()); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/Equal.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/Equal.java index 20d36dbd5..5dc80ce4e 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/Equal.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/Equal.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -37,16 +34,13 @@ public Equal(CFG cfg, CodeLocation location, Expression left, Expression right) } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { return state.smallStepSemantics( new BinaryExpression( getStaticType(), diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterOrEqual.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterOrEqual.java index 3e9627ec0..8044b9630 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterOrEqual.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterOrEqual.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -41,16 +38,13 @@ public GreaterOrEqual(CFG cfg, CodeLocation location, Expression left, Expressio } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterThan.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterThan.java index 3e81bcecb..7e239766e 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterThan.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/GreaterThan.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -41,16 +38,13 @@ public GreaterThan(CFG cfg, CodeLocation location, Expression left, Expression r } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessOrEqual.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessOrEqual.java index fa6eac11e..d95737b82 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessOrEqual.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessOrEqual.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -41,16 +38,13 @@ public LessOrEqual(CFG cfg, CodeLocation location, Expression left, Expression r } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessThan.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessThan.java index 969d1fd36..54d967534 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessThan.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/LessThan.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -41,16 +38,13 @@ public LessThan(CFG cfg, CodeLocation location, Expression left, Expression righ } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/NotEqual.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/NotEqual.java index 55562e8e9..fcdb4d030 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/NotEqual.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/comparison/NotEqual.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -37,16 +34,13 @@ public NotEqual(CFG cfg, CodeLocation location, Expression left, Expression righ } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { return state.smallStepSemantics( new BinaryExpression( getStaticType(), diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessGlobal.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessGlobal.java index 4ae0a0333..588629cc9 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessGlobal.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessGlobal.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.ConstantGlobal; import it.unive.lisa.program.Global; @@ -118,12 +115,9 @@ public String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics(AnalysisState entryState, - InterproceduralAnalysis interprocedural, StatementStore expressions) - throws SemanticException { + public > AnalysisState semantics(AnalysisState entryState, + InterproceduralAnalysis interprocedural, StatementStore expressions) + throws SemanticException { if (target instanceof ConstantGlobal) return entryState.smallStepSemantics(((ConstantGlobal) target).getConstant(), this); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessInstanceGlobal.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessInstanceGlobal.java index 1cfb44229..715b0bfc8 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessInstanceGlobal.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/global/AccessInstanceGlobal.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.ClassUnit; import it.unive.lisa.program.CompilationUnit; @@ -106,18 +103,15 @@ public String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException { + public > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException { CodeLocation loc = getLocation(); - AnalysisState result = state.bottom(); + AnalysisState result = state.bottom(); boolean atLeastOne = false; TypeSystem types = getProgram().getTypes(); for (Type recType : expr.getRuntimeTypes(types)) diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/literal/NullLiteral.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/literal/NullLiteral.java index ce80b4584..36a15dcaa 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/literal/NullLiteral.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/literal/NullLiteral.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -33,13 +30,10 @@ public NullLiteral(CFG cfg, CodeLocation location) { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, InterproceduralAnalysis interprocedural, - StatementStore expressions) - throws SemanticException { + public > AnalysisState semantics( + AnalysisState entryState, InterproceduralAnalysis interprocedural, + StatementStore expressions) + throws SemanticException { return entryState.smallStepSemantics(new NullConstant(getLocation()), this); } } diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/And.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/And.java index 88ead9b68..283e4ab2b 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/And.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/And.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -40,16 +37,13 @@ public And(CFG cfg, CodeLocation location, Expression left, Expression right) { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isBooleanType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Not.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Not.java index c73f83c82..b2157a437 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Not.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Not.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -39,15 +36,12 @@ public Not(CFG cfg, CodeLocation location, Expression expression) { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException { + public > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (expr.getRuntimeTypes(types).stream().noneMatch(Type::isBooleanType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Or.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Or.java index 2ff91db94..7d4046da2 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Or.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/logic/Or.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -40,16 +37,13 @@ public Or(CFG cfg, CodeLocation location, Expression left, Expression right) { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isBooleanType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Addition.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Addition.java index 65fc737e7..07a277df5 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Addition.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Addition.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -41,16 +38,13 @@ public Addition(CFG cfg, CodeLocation location, Expression left, Expression righ } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Division.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Division.java index e868d5e02..c32c8cbf7 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Division.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Division.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -41,16 +38,13 @@ public Division(CFG cfg, CodeLocation location, Expression left, Expression righ } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Modulo.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Modulo.java index 20b4396a0..8702bbcba 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Modulo.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Modulo.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -42,16 +39,13 @@ public Modulo(CFG cfg, CodeLocation location, Expression left, Expression right) } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Multiplication.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Multiplication.java index ff69f452f..0d5ee6e2a 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Multiplication.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Multiplication.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -41,16 +38,13 @@ public Multiplication(CFG cfg, CodeLocation location, Expression left, Expressio } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Negation.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Negation.java index 668ece839..4613ffa45 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Negation.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Negation.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -39,15 +36,12 @@ public Negation(CFG cfg, CodeLocation location, Expression expression) { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException { + public > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (expr.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Remainder.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Remainder.java index 413d17110..a0d12df58 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Remainder.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Remainder.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -42,16 +39,13 @@ public Remainder(CFG cfg, CodeLocation location, Expression left, Expression rig } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Subtraction.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Subtraction.java index 8a68bb8f1..4785b3a11 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Subtraction.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/numeric/Subtraction.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -41,16 +38,13 @@ public Subtraction(CFG cfg, CodeLocation location, Expression left, Expression r } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isNumericType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Concat.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Concat.java index 3ceef0b5c..24c1fba02 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Concat.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Concat.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -63,16 +60,13 @@ public Concat(CFG cfg, CodeLocation location, Expression left, Expression right) } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isStringType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Contains.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Contains.java index 0f5581b97..185426693 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Contains.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Contains.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -64,16 +61,13 @@ public Contains(CFG cfg, CodeLocation location, Expression left, Expression righ } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isStringType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/EndsWith.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/EndsWith.java index 22c9d5de1..788f0f8a2 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/EndsWith.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/EndsWith.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -64,16 +61,13 @@ public EndsWith(CFG cfg, CodeLocation location, Expression left, Expression righ } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isStringType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Equals.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Equals.java index ed55a5585..b0f85cfce 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Equals.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Equals.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -64,16 +61,13 @@ public Equals(CFG cfg, CodeLocation location, Expression left, Expression right) } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isStringType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/IndexOf.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/IndexOf.java index 7321518b4..6f39c9333 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/IndexOf.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/IndexOf.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -64,16 +61,13 @@ public IndexOf(CFG cfg, CodeLocation location, Expression left, Expression right } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isStringType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Length.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Length.java index 1e36e3de7..eec870ed1 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Length.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Length.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -62,15 +59,12 @@ public Length(CFG cfg, CodeLocation location, Expression parameter) { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException { + public > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (expr.getRuntimeTypes(types).stream().noneMatch(Type::isStringType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Replace.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Replace.java index 1d49f29b3..764f97b52 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Replace.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Replace.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -64,17 +61,14 @@ public Replace(CFG cfg, CodeLocation location, Expression left, Expression middl } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState ternarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression middle, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState ternarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression middle, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isStringType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/StartsWith.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/StartsWith.java index 2f494ed0c..3b9f1ad55 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/StartsWith.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/StartsWith.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -64,16 +61,13 @@ public StartsWith(CFG cfg, CodeLocation location, Expression left, Expression ri } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isStringType)) return state.bottom(); diff --git a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Substring.java b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Substring.java index 88c8c01d4..c1cfbb92c 100644 --- a/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Substring.java +++ b/lisa/lisa-program/src/main/java/it/unive/lisa/program/cfg/statement/string/Substring.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -66,17 +63,14 @@ public Substring(CFG cfg, CodeLocation location, Expression left, Expression mid } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState ternarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression middle, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState ternarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression middle, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { TypeSystem types = getProgram().getTypes(); if (left.getRuntimeTypes(types).stream().noneMatch(Type::isStringType)) return state.bottom(); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java index 96e425adf..8a5f6f762 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/LiSARunner.java @@ -4,10 +4,7 @@ import it.unive.lisa.analysis.AnalysisState; import it.unive.lisa.analysis.AnalyzedCFG; import it.unive.lisa.analysis.OptimizedAnalyzedCFG; -import it.unive.lisa.analysis.heap.HeapDomain; 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.checks.ChecksExecutor; import it.unive.lisa.checks.semantic.CheckToolWithAnalysisResults; import it.unive.lisa.checks.semantic.SemanticCheck; @@ -53,17 +50,8 @@ * * @param the type of {@link AbstractState} contained into the analysis * state that will be used in the analysis fixpoint - * @param the type of {@link HeapDomain} contained into the abstract state - * that will be used in the analysis fixpoint - * @param the type of {@link ValueDomain} contained into the abstract state - * that will be used in the analysis fixpoint - * @param the type of {@link TypeDomain} contained into the abstract state - * that will be used in the analysis fixpoint */ -public class LiSARunner, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> { +public class LiSARunner> { private static final String FIXPOINT_EXCEPTION_MESSAGE = "Exception during fixpoint computation"; @@ -71,7 +59,7 @@ public class LiSARunner, private final LiSAConfiguration conf; - private final InterproceduralAnalysis interproc; + private final InterproceduralAnalysis interproc; private final CallGraph callGraph; @@ -85,7 +73,7 @@ public class LiSARunner, * @param callGraph the call graph to use * @param state the abstract state to use for the analysis */ - LiSARunner(LiSAConfiguration conf, InterproceduralAnalysis interproc, CallGraph callGraph, A state) { + LiSARunner(LiSAConfiguration conf, InterproceduralAnalysis interproc, CallGraph callGraph, A state) { this.conf = conf; this.interproc = interproc; this.callGraph = callGraph; @@ -148,14 +136,14 @@ Collection run(Application app, FileManager fileManager) { if (state != null) { analyze(allCFGs, fileManager, htmlViewer, subnodes); - Map>> results = new IdentityHashMap<>(allCFGs.size()); + Map>> results = new IdentityHashMap<>(allCFGs.size()); for (CFG cfg : allCFGs) results.put(cfg, interproc.getAnalysisResultsOf(cfg)); @SuppressWarnings({ "rawtypes", "unchecked" }) - Collection> semanticChecks = (Collection) conf.semanticChecks; + Collection> semanticChecks = (Collection) conf.semanticChecks; if (!semanticChecks.isEmpty()) { - CheckToolWithAnalysisResults tool2 = new CheckToolWithAnalysisResults<>( + CheckToolWithAnalysisResults tool2 = new CheckToolWithAnalysisResults<>( tool, results, callGraph); @@ -194,17 +182,17 @@ private void analyze(Collection allCFGs, FileManager fileManager, AtomicBoo BiFunction labeler = conf.optimize && conf.dumpForcesUnwinding - ? (cfg, st) -> ((OptimizedAnalyzedCFG) cfg) + ? (cfg, st) -> ((OptimizedAnalyzedCFG) cfg) .getUnwindedAnalysisStateAfter(st, fixconf) .representation() .toSerializableValue() - : (cfg, st) -> ((AnalyzedCFG) cfg) + : (cfg, st) -> ((AnalyzedCFG) cfg) .getAnalysisStateAfter(st) .representation() .toSerializableValue(); for (CFG cfg : IterationLogger.iterate(LOG, allCFGs, "Dumping analysis results", "cfgs")) - for (AnalyzedCFG result : interproc.getAnalysisResultsOf(cfg)) { + for (AnalyzedCFG result : interproc.getAnalysisResultsOf(cfg)) { SerializableGraph graph = result.toSerializableGraph(labeler); String filename = cfg.getDescriptor().getFullSignatureWithParNames(); if (!result.getId().isStartingId()) diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AbstractState.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AbstractState.java index ceed47535..8463e40f1 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AbstractState.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AbstractState.java @@ -1,17 +1,13 @@ package it.unive.lisa.analysis; -import java.util.Set; - -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.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.heap.HeapExpression; import it.unive.lisa.symbolic.value.Identifier; import it.unive.lisa.symbolic.value.ValueExpression; import it.unive.lisa.type.Type; +import java.util.Set; /** * An abstract state of the analysis, composed by a heap state modeling the @@ -22,15 +18,8 @@ * @author Luca Negrini * * @param the concrete type of the {@link AbstractState} - * @param the type of {@link HeapDomain} embedded in this state - * @param the type of {@link ValueDomain} embedded in this state - * @param the type of {@link ValueDomain} and {@link TypeDomain} embedded in - * this state */ -public interface AbstractState, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> +public interface AbstractState> extends Lattice, SemanticDomain { /** @@ -78,7 +67,7 @@ public ExpressionSet rewrite( * * @return the runtime types * - * @throws SemanticException + * @throws SemanticException if something goes wrong during the computation */ Set getRuntimeTypesOf(SymbolicExpression e, ProgramPoint pp) throws SemanticException; @@ -91,6 +80,8 @@ public ExpressionSet rewrite( * @param pp the program point where the types are required * * @return the dynamic type + * + * @throws SemanticException if something goes wrong during the computation */ Type getDynamicTypeOf(SymbolicExpression e, ProgramPoint pp) throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java index 2c5b32344..1fe4ff434 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalysisState.java @@ -1,22 +1,18 @@ 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.analysis.heap.HeapDomain; import it.unive.lisa.analysis.lattices.ExpressionSet; import it.unive.lisa.analysis.representation.DomainRepresentation; import it.unive.lisa.analysis.representation.ObjectRepresentation; import it.unive.lisa.analysis.symbols.Symbol; 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.program.cfg.ProgramPoint; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; +import java.util.Collection; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; +import java.util.function.Predicate; /** * The abstract analysis state at a given program point. An analysis state is @@ -28,16 +24,10 @@ * @author Luca Negrini * * @param the type of {@link AbstractState} embedded in this state - * @param the type of {@link HeapDomain} embedded in the abstract state - * @param the type of {@link ValueDomain} embedded in the abstract state - * @param the type of {@link TypeDomain} embedded in the abstract state */ -public class AnalysisState, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - implements BaseLattice>, - SemanticDomain, SymbolicExpression, Identifier> { +public class AnalysisState> + implements BaseLattice>, + SemanticDomain, SymbolicExpression, Identifier> { /** * The abstract state of program variables and memory locations @@ -127,13 +117,13 @@ public ExpressionSet getComputedExpressions() { * * @return a copy of this analysis state, with the new alias */ - public AnalysisState alias(Symbol toAlias, Symbol alias) { + public AnalysisState alias(Symbol toAlias, Symbol alias) { SymbolAliasing aliasing = this.aliasing.putState(toAlias, alias); return new AnalysisState<>(state, computedExpressions, aliasing); } @Override - public AnalysisState assign(Identifier id, SymbolicExpression value, ProgramPoint pp) + public AnalysisState assign(Identifier id, SymbolicExpression value, ProgramPoint pp) throws SemanticException { A s = state.assign(id, value, pp); return new AnalysisState<>(s, new ExpressionSet<>(id), aliasing); @@ -154,7 +144,7 @@ public AnalysisState assign(Identifier id, SymbolicExpression value, * * @throws SemanticException if an error occurs during the computation */ - public AnalysisState assign(SymbolicExpression id, SymbolicExpression expression, ProgramPoint pp) + public AnalysisState assign(SymbolicExpression id, SymbolicExpression expression, ProgramPoint pp) throws SemanticException { if (id instanceof Identifier) @@ -171,14 +161,14 @@ public AnalysisState assign(SymbolicExpression id, SymbolicExpressio } @Override - public AnalysisState smallStepSemantics(SymbolicExpression expression, ProgramPoint pp) + public AnalysisState smallStepSemantics(SymbolicExpression expression, ProgramPoint pp) throws SemanticException { A s = state.smallStepSemantics(expression, pp); return new AnalysisState<>(s, new ExpressionSet<>(expression), aliasing); } @Override - public AnalysisState assume(SymbolicExpression expression, ProgramPoint src, ProgramPoint dest) + public AnalysisState assume(SymbolicExpression expression, ProgramPoint src, ProgramPoint dest) throws SemanticException { A assume = state.assume(expression, src, dest); if (assume.isBottom()) @@ -192,7 +182,7 @@ public Satisfiability satisfies(SymbolicExpression expression, ProgramPoint pp) } @Override - public AnalysisState pushScope(ScopeToken scope) throws SemanticException { + public AnalysisState pushScope(ScopeToken scope) throws SemanticException { return new AnalysisState<>( state.pushScope(scope), onAllExpressions(this.computedExpressions, scope, true), @@ -209,7 +199,7 @@ private static ExpressionSet onAllExpressions( } @Override - public AnalysisState popScope(ScopeToken scope) throws SemanticException { + public AnalysisState popScope(ScopeToken scope) throws SemanticException { return new AnalysisState<>( state.popScope(scope), onAllExpressions(this.computedExpressions, scope, false), @@ -217,7 +207,7 @@ public AnalysisState popScope(ScopeToken scope) throws SemanticExcep } @Override - public AnalysisState lubAux(AnalysisState other) throws SemanticException { + public AnalysisState lubAux(AnalysisState other) throws SemanticException { return new AnalysisState<>( state.lub(other.state), computedExpressions.lub(other.computedExpressions), @@ -225,7 +215,7 @@ public AnalysisState lubAux(AnalysisState other) throws } @Override - public AnalysisState glbAux(AnalysisState other) throws SemanticException { + public AnalysisState glbAux(AnalysisState other) throws SemanticException { return new AnalysisState<>( state.glb(other.state), computedExpressions.glb(other.computedExpressions), @@ -233,7 +223,7 @@ public AnalysisState glbAux(AnalysisState other) throws } @Override - public AnalysisState wideningAux(AnalysisState other) throws SemanticException { + public AnalysisState wideningAux(AnalysisState other) throws SemanticException { return new AnalysisState<>( state.widening(other.state), computedExpressions.lub(other.computedExpressions), @@ -241,7 +231,7 @@ public AnalysisState wideningAux(AnalysisState other) th } @Override - public AnalysisState narrowingAux(AnalysisState other) throws SemanticException { + public AnalysisState narrowingAux(AnalysisState other) throws SemanticException { return new AnalysisState<>( state.narrowing(other.state), computedExpressions.glb(other.computedExpressions), @@ -249,19 +239,19 @@ public AnalysisState narrowingAux(AnalysisState other) t } @Override - public boolean lessOrEqualAux(AnalysisState other) throws SemanticException { + public boolean lessOrEqualAux(AnalysisState other) throws SemanticException { return state.lessOrEqual(other.state) && computedExpressions.lessOrEqual(other.computedExpressions) && aliasing.lessOrEqual(other.aliasing); } @Override - public AnalysisState top() { + public AnalysisState top() { return new AnalysisState<>(state.top(), computedExpressions.top(), aliasing.top()); } @Override - public AnalysisState bottom() { + public AnalysisState bottom() { return new AnalysisState<>(state.bottom(), computedExpressions.bottom(), aliasing.bottom()); } @@ -276,12 +266,12 @@ public boolean isBottom() { } @Override - public AnalysisState forgetIdentifier(Identifier id) throws SemanticException { + public AnalysisState forgetIdentifier(Identifier id) throws SemanticException { return new AnalysisState<>(state.forgetIdentifier(id), computedExpressions, aliasing); } @Override - public AnalysisState forgetIdentifiersIf(Predicate test) throws SemanticException { + public AnalysisState forgetIdentifiersIf(Predicate test) throws SemanticException { return new AnalysisState<>(state.forgetIdentifiersIf(test), computedExpressions, aliasing); } @@ -303,7 +293,7 @@ public boolean equals(Object obj) { return false; if (getClass() != obj.getClass()) return false; - AnalysisState other = (AnalysisState) obj; + AnalysisState other = (AnalysisState) obj; if (aliasing == null) { if (other.aliasing != null) return false; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalyzedCFG.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalyzedCFG.java index 1197de1c4..f5010a781 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalyzedCFG.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/AnalyzedCFG.java @@ -1,8 +1,5 @@ package it.unive.lisa.analysis; -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.ScopeId; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.edge.Edge; @@ -22,19 +19,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} embedded into the computed abstract - * state */ -public class AnalyzedCFG, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> +public class AnalyzedCFG> extends CFG - implements BaseLattice> { + implements BaseLattice> { /** * Error message for the inability to lub two graphs. @@ -64,12 +52,12 @@ public class AnalyzedCFG, /** * The map storing the analysis results. */ - protected final StatementStore results; + protected final StatementStore results; /** * The map storing the entry state of each entry point. */ - protected final StatementStore entryStates; + protected final StatementStore entryStates; /** * An id meant to identify this specific result, based on how it has been @@ -88,7 +76,7 @@ public class AnalyzedCFG, * abstract state of the analysis that was executed, * used to retrieve top and bottom values */ - public AnalyzedCFG(CFG cfg, ScopeId id, AnalysisState singleton) { + public AnalyzedCFG(CFG cfg, ScopeId id, AnalysisState singleton) { this(cfg, id, singleton, Collections.emptyMap(), Collections.emptyMap()); } @@ -107,9 +95,9 @@ public AnalyzedCFG(CFG cfg, ScopeId id, AnalysisState singleton) { */ public AnalyzedCFG(CFG cfg, ScopeId id, - AnalysisState singleton, - Map> entryStates, - Map> results) { + AnalysisState singleton, + Map> entryStates, + Map> results) { super(cfg); this.results = new StatementStore<>(singleton); results.forEach(this.results::put); @@ -130,8 +118,8 @@ public AnalyzedCFG(CFG cfg, */ public AnalyzedCFG(CFG cfg, ScopeId id, - StatementStore entryStates, - StatementStore results) { + StatementStore entryStates, + StatementStore results) { super(cfg); this.results = results; this.entryStates = entryStates; @@ -157,7 +145,7 @@ public ScopeId getId() { * * @throws SemanticException if the lub operator fails */ - public AnalysisState getAnalysisStateBefore(Statement st) throws SemanticException { + public AnalysisState getAnalysisStateBefore(Statement st) throws SemanticException { Statement pred = st.getEvaluationPredecessor(); if (pred != null) results.getState(pred); @@ -176,7 +164,7 @@ public AnalysisState getAnalysisStateBefore(Statement st) throws Sem * * @return the result computed at the given statement */ - public AnalysisState getAnalysisStateAfter(Statement st) { + public AnalysisState getAnalysisStateAfter(Statement st) { return results.getState(st); } @@ -187,7 +175,7 @@ public AnalysisState getAnalysisStateAfter(Statement st) { * * @throws SemanticException if the lub operator fails */ - public AnalysisState getEntryState() throws SemanticException { + public AnalysisState getEntryState() throws SemanticException { return lub(this.getEntrypoints(), true); } @@ -198,19 +186,19 @@ public AnalysisState getEntryState() throws SemanticException { * * @throws SemanticException if the lub operator fails */ - public AnalysisState getExitState() throws SemanticException { + public AnalysisState getExitState() throws SemanticException { return lub(this.getNormalExitpoints(), false); } - private AnalysisState lub(Collection statements, boolean entry) throws SemanticException { - AnalysisState result = entryStates.lattice.bottom(); + private AnalysisState lub(Collection statements, boolean entry) throws SemanticException { + AnalysisState result = entryStates.lattice.bottom(); for (Statement st : statements) result = result.lub(entry ? getAnalysisStateBefore(st) : getAnalysisStateAfter(st)); return result; } @Override - public AnalyzedCFG lubAux(AnalyzedCFG other) throws SemanticException { + public AnalyzedCFG lubAux(AnalyzedCFG other) throws SemanticException { if (!getDescriptor().equals(other.getDescriptor()) || !sameIDs(other)) throw new SemanticException(CANNOT_LUB_ERROR); @@ -222,7 +210,7 @@ public AnalyzedCFG lubAux(AnalyzedCFG other) throws Sema } @Override - public AnalyzedCFG glbAux(AnalyzedCFG other) throws SemanticException { + public AnalyzedCFG glbAux(AnalyzedCFG other) throws SemanticException { if (!getDescriptor().equals(other.getDescriptor()) || !sameIDs(other)) throw new SemanticException(CANNOT_GLB_ERROR); @@ -234,7 +222,7 @@ public AnalyzedCFG glbAux(AnalyzedCFG other) throws Sema } @Override - public AnalyzedCFG wideningAux(AnalyzedCFG other) throws SemanticException { + public AnalyzedCFG wideningAux(AnalyzedCFG other) throws SemanticException { if (!getDescriptor().equals(other.getDescriptor()) || !sameIDs(other)) throw new SemanticException(CANNOT_WIDEN_ERROR); @@ -246,7 +234,7 @@ public AnalyzedCFG wideningAux(AnalyzedCFG other) throws } @Override - public AnalyzedCFG narrowingAux(AnalyzedCFG other) throws SemanticException { + public AnalyzedCFG narrowingAux(AnalyzedCFG other) throws SemanticException { if (!getDescriptor().equals(other.getDescriptor()) || !sameIDs(other)) throw new SemanticException(CANNOT_NARROW_ERROR); @@ -258,7 +246,7 @@ public AnalyzedCFG narrowingAux(AnalyzedCFG other) throw } @Override - public boolean lessOrEqualAux(AnalyzedCFG other) throws SemanticException { + public boolean lessOrEqualAux(AnalyzedCFG other) throws SemanticException { if (!getDescriptor().equals(other.getDescriptor()) || !sameIDs(other)) throw new SemanticException(CANNOT_COMPARE_ERROR); @@ -273,7 +261,7 @@ public boolean lessOrEqualAux(AnalyzedCFG other) throws SemanticExce * * @return {@code true} if that condition holds */ - protected boolean sameIDs(AnalyzedCFG other) { + protected boolean sameIDs(AnalyzedCFG other) { if (id == null) { if (other.id == null) return true; @@ -285,7 +273,7 @@ protected boolean sameIDs(AnalyzedCFG other) { } @Override - public AnalyzedCFG top() { + public AnalyzedCFG top() { return new AnalyzedCFG<>(this, id.startingId(), entryStates.top(), results.top()); } @@ -295,7 +283,7 @@ public boolean isTop() { } @Override - public AnalyzedCFG bottom() { + public AnalyzedCFG bottom() { return new AnalyzedCFG<>(this, id.startingId(), entryStates.bottom(), results.bottom()); } @@ -322,7 +310,7 @@ public boolean equals(Object obj) { return false; if (getClass() != obj.getClass()) return false; - AnalyzedCFG other = (AnalyzedCFG) obj; + AnalyzedCFG other = (AnalyzedCFG) obj; if (entryStates == null) { if (other.entryStates != null) return false; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/OptimizedAnalyzedCFG.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/OptimizedAnalyzedCFG.java index 772176087..33dc59267 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/OptimizedAnalyzedCFG.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/OptimizedAnalyzedCFG.java @@ -1,10 +1,7 @@ package it.unive.lisa.analysis; -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.conf.LiSAConfiguration; import it.unive.lisa.interprocedural.FixpointResults; @@ -56,25 +53,14 @@ * * @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} embedded into the computed abstract - * state */ -public class OptimizedAnalyzedCFG< - A extends AbstractState, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - extends AnalyzedCFG { +public class OptimizedAnalyzedCFG> extends AnalyzedCFG { private static final Logger LOG = LogManager.getLogger(OptimizedAnalyzedCFG.class); - private final InterproceduralAnalysis interprocedural; + private final InterproceduralAnalysis interprocedural; - private StatementStore expanded; + private StatementStore expanded; /** * Builds the control flow graph, storing the given mapping between nodes @@ -93,8 +79,8 @@ public class OptimizedAnalyzedCFG< */ public OptimizedAnalyzedCFG(CFG cfg, ScopeId id, - AnalysisState singleton, - InterproceduralAnalysis interprocedural) { + AnalysisState singleton, + InterproceduralAnalysis interprocedural) { super(cfg, id, singleton); this.interprocedural = interprocedural; } @@ -118,10 +104,10 @@ public OptimizedAnalyzedCFG(CFG cfg, */ public OptimizedAnalyzedCFG(CFG cfg, ScopeId id, - AnalysisState singleton, - Map> entryStates, - Map> results, - InterproceduralAnalysis interprocedural) { + AnalysisState singleton, + Map> entryStates, + Map> results, + InterproceduralAnalysis interprocedural) { super(cfg, id, singleton, entryStates, results); this.interprocedural = interprocedural; } @@ -141,19 +127,19 @@ public OptimizedAnalyzedCFG(CFG cfg, */ public OptimizedAnalyzedCFG(CFG cfg, ScopeId id, - StatementStore entryStates, - StatementStore results, - InterproceduralAnalysis interprocedural) { + StatementStore entryStates, + StatementStore results, + InterproceduralAnalysis interprocedural) { super(cfg, id, entryStates, results); this.interprocedural = interprocedural; } private OptimizedAnalyzedCFG(CFG cfg, ScopeId id, - StatementStore entryStates, - StatementStore results, - StatementStore expanded, - InterproceduralAnalysis interprocedural) { + StatementStore entryStates, + StatementStore results, + StatementStore expanded, + InterproceduralAnalysis interprocedural) { super(cfg, id, entryStates, results); this.interprocedural = interprocedural; this.expanded = expanded; @@ -171,7 +157,7 @@ private OptimizedAnalyzedCFG(CFG cfg, * * @return the result computed at the given statement */ - public AnalysisState getUnwindedAnalysisStateAfter(Statement st, FixpointConfiguration conf) { + public AnalysisState getUnwindedAnalysisStateAfter(Statement st, FixpointConfiguration conf) { if (results.getKeys().contains(st)) return results.getState(st); @@ -192,42 +178,42 @@ public AnalysisState getUnwindedAnalysisStateAfter(Statement st, Fix * fixpoint computation */ public void unwind(FixpointConfiguration conf) { - AnalysisState bottom = results.lattice.bottom(); - StatementStore bot = new StatementStore<>(bottom); - Map> starting = new HashMap<>(); - for (Entry> entry : entryStates) + AnalysisState bottom = results.lattice.bottom(); + StatementStore bot = new StatementStore<>(bottom); + Map> starting = new HashMap<>(); + for (Entry> entry : entryStates) starting.put(entry.getKey(), CompoundState.of(entry.getValue(), bot)); - Map> existing = new HashMap<>(); - CompoundState fallback = CompoundState.of(bottom, bot); - for (Entry> entry : results) { + Map> existing = new HashMap<>(); + CompoundState fallback = CompoundState.of(bottom, bot); + for (Entry> entry : results) { Statement stmt = entry.getKey(); - AnalysisState approx = entry.getValue(); - CompoundState def = existing.getOrDefault(stmt, fallback); + AnalysisState approx = entry.getValue(); + CompoundState def = existing.getOrDefault(stmt, fallback); if (!(stmt instanceof Expression) || ((Expression) stmt).getRootStatement() == stmt) existing.put(stmt, CompoundState.of(approx, def.intermediateStates)); else { Expression e = (Expression) stmt; - CompoundState val = existing.computeIfAbsent(e.getRootStatement(), + CompoundState val = existing.computeIfAbsent(e.getRootStatement(), ex -> CompoundState.of(bottom, bot.bottom())); val.intermediateStates.put(e, approx); } } - AscendingFixpoint asc = new AscendingFixpoint<>(this, new PrecomputedAnalysis(), conf); - Fixpoint> fix = new Fixpoint<>(this, true); + AscendingFixpoint asc = new AscendingFixpoint<>(this, new PrecomputedAnalysis(), conf); + Fixpoint> fix = new Fixpoint<>(this, true); TimerLogger.execAction(LOG, "Unwinding optimizied results of " + this, () -> { try { - Map> res = fix.fixpoint( + Map> res = fix.fixpoint( starting, FIFOWorkingSet.mk(), asc, existing); expanded = new StatementStore<>(bottom); - for (Entry> e : res.entrySet()) { + for (Entry> e : res.entrySet()) { expanded.put(e.getKey(), e.getValue().postState); - for (Entry> ee : e.getValue().intermediateStates) + for (Entry> ee : e.getValue().intermediateStates) expanded.put(ee.getKey(), ee.getValue()); } } catch (FixpointException e) { @@ -255,11 +241,11 @@ public boolean hasPostStateOf(Statement st) { * @param st the statement * @param postState the poststate */ - public void storePostStateOf(Statement st, AnalysisState postState) { + public void storePostStateOf(Statement st, AnalysisState postState) { results.put(st, postState); } - private class PrecomputedAnalysis implements InterproceduralAnalysis { + private class PrecomputedAnalysis implements InterproceduralAnalysis { @Override public void init(Application app, @@ -270,7 +256,7 @@ public void init(Application app, } @Override - public void fixpoint(AnalysisState entryState, + public void fixpoint(AnalysisState entryState, Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException { @@ -278,35 +264,35 @@ public void fixpoint(AnalysisState entryState, } @Override - public Collection> getAnalysisResultsOf(CFG cfg) { + public Collection> getAnalysisResultsOf(CFG cfg) { throw new UnsupportedOperationException(); } @Override - public AnalysisState getAbstractResultOf( + public AnalysisState getAbstractResultOf( CFGCall call, - AnalysisState entryState, + AnalysisState entryState, ExpressionSet[] parameters, - StatementStore expressions) + StatementStore expressions) throws SemanticException { Call source = call.getSource() == null ? call : call.getSource(); if (results.getKeys().contains(source)) return results.getState(source); - FixpointResults precomputed = interprocedural.getFixpointResults(); + FixpointResults precomputed = interprocedural.getFixpointResults(); ScopeToken scope = new ScopeToken(call); ScopeId id = getId().push(call); - AnalysisState state = entryState.bottom(); + AnalysisState state = entryState.bottom(); for (CFG target : call.getTargetedCFGs()) { - AnalysisState res = precomputed.getState(target).getState(id).getExitState(); + AnalysisState res = precomputed.getState(target).getState(id).getExitState(); state = state.lub(unscope(call, scope, res)); } return state; } @Override - public AnalysisState getAbstractResultOf(OpenCall call, AnalysisState entryState, - ExpressionSet[] parameters, StatementStore expressions) + public AnalysisState getAbstractResultOf(OpenCall call, AnalysisState entryState, + ExpressionSet[] parameters, StatementStore expressions) throws SemanticException { return interprocedural.getAbstractResultOf(call, entryState, parameters, expressions); } @@ -318,19 +304,19 @@ public Call resolve(UnresolvedCall call, Set[] types, SymbolAliasing alias } @Override - public FixpointResults getFixpointResults() { + public FixpointResults getFixpointResults() { return interprocedural.getFixpointResults(); } } @Override - public OptimizedAnalyzedCFG lubAux(AnalyzedCFG other) throws SemanticException { + public OptimizedAnalyzedCFG lubAux(AnalyzedCFG other) throws SemanticException { if (!getDescriptor().equals(other.getDescriptor()) || !sameIDs(other) - || !(other instanceof OptimizedAnalyzedCFG)) + || !(other instanceof OptimizedAnalyzedCFG)) throw new SemanticException(CANNOT_LUB_ERROR); - OptimizedAnalyzedCFG o = (OptimizedAnalyzedCFG) other; - return new OptimizedAnalyzedCFG( + OptimizedAnalyzedCFG o = (OptimizedAnalyzedCFG) other; + return new OptimizedAnalyzedCFG( this, id, entryStates.lub(other.entryStates), @@ -340,13 +326,13 @@ public OptimizedAnalyzedCFG lubAux(AnalyzedCFG other) th } @Override - public OptimizedAnalyzedCFG glbAux(AnalyzedCFG other) throws SemanticException { + public OptimizedAnalyzedCFG glbAux(AnalyzedCFG other) throws SemanticException { if (!getDescriptor().equals(other.getDescriptor()) || !sameIDs(other) - || !(other instanceof OptimizedAnalyzedCFG)) + || !(other instanceof OptimizedAnalyzedCFG)) throw new SemanticException(CANNOT_GLB_ERROR); - OptimizedAnalyzedCFG o = (OptimizedAnalyzedCFG) other; - return new OptimizedAnalyzedCFG( + OptimizedAnalyzedCFG o = (OptimizedAnalyzedCFG) other; + return new OptimizedAnalyzedCFG( this, id, entryStates.glb(other.entryStates), @@ -356,13 +342,13 @@ public OptimizedAnalyzedCFG glbAux(AnalyzedCFG other) th } @Override - public OptimizedAnalyzedCFG wideningAux(AnalyzedCFG other) throws SemanticException { + public OptimizedAnalyzedCFG wideningAux(AnalyzedCFG other) throws SemanticException { if (!getDescriptor().equals(other.getDescriptor()) || !sameIDs(other) - || !(other instanceof OptimizedAnalyzedCFG)) + || !(other instanceof OptimizedAnalyzedCFG)) throw new SemanticException(CANNOT_WIDEN_ERROR); - OptimizedAnalyzedCFG o = (OptimizedAnalyzedCFG) other; - return new OptimizedAnalyzedCFG( + OptimizedAnalyzedCFG o = (OptimizedAnalyzedCFG) other; + return new OptimizedAnalyzedCFG( this, id, entryStates.widening(other.entryStates), @@ -372,13 +358,13 @@ public OptimizedAnalyzedCFG wideningAux(AnalyzedCFG othe } @Override - public OptimizedAnalyzedCFG narrowingAux(AnalyzedCFG other) throws SemanticException { + public OptimizedAnalyzedCFG narrowingAux(AnalyzedCFG other) throws SemanticException { if (!getDescriptor().equals(other.getDescriptor()) || !sameIDs(other) - || !(other instanceof OptimizedAnalyzedCFG)) + || !(other instanceof OptimizedAnalyzedCFG)) throw new SemanticException(CANNOT_NARROW_ERROR); - OptimizedAnalyzedCFG o = (OptimizedAnalyzedCFG) other; - return new OptimizedAnalyzedCFG( + OptimizedAnalyzedCFG o = (OptimizedAnalyzedCFG) other; + return new OptimizedAnalyzedCFG( this, id, entryStates.narrowing(other.entryStates), @@ -388,12 +374,12 @@ public OptimizedAnalyzedCFG narrowingAux(AnalyzedCFG oth } @Override - public OptimizedAnalyzedCFG top() { + public OptimizedAnalyzedCFG top() { return new OptimizedAnalyzedCFG<>(this, id.startingId(), entryStates.top(), results.top(), null, null); } @Override - public OptimizedAnalyzedCFG bottom() { + public OptimizedAnalyzedCFG bottom() { return new OptimizedAnalyzedCFG<>(this, id.startingId(), entryStates.bottom(), results.bottom(), null, null); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/StatementStore.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/StatementStore.java index a75a0099a..8a535f581 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/StatementStore.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/StatementStore.java @@ -1,9 +1,6 @@ package it.unive.lisa.analysis; -import it.unive.lisa.analysis.heap.HeapDomain; import it.unive.lisa.analysis.lattices.FunctionalLattice; -import it.unive.lisa.analysis.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.cfg.statement.Statement; import java.util.Map; @@ -15,26 +12,20 @@ * @author Luca Negrini * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} */ -public class StatementStore, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - extends FunctionalLattice, Statement, AnalysisState> { +public class StatementStore> + extends FunctionalLattice, Statement, AnalysisState> { /** * Builds the store. * * @param state an instance of the underlying lattice */ - public StatementStore(AnalysisState state) { + public StatementStore(AnalysisState state) { super(state); } - private StatementStore(AnalysisState state, Map> function) { + private StatementStore(AnalysisState state, Map> function) { super(state, function); } @@ -48,7 +39,7 @@ private StatementStore(AnalysisState state, Map put(Statement st, AnalysisState state) { + public AnalysisState put(Statement st, AnalysisState state) { if (function == null) function = mkNewFunction(null, false); return function.put(st, state); @@ -68,18 +59,18 @@ public void forget(Statement st) { } @Override - public StatementStore top() { + public StatementStore top() { return new StatementStore<>(lattice.top()); } @Override - public StatementStore bottom() { + public StatementStore bottom() { return new StatementStore<>(lattice.bottom()); } @Override - public StatementStore mk(AnalysisState lattice, - Map> function) { + public StatementStore mk(AnalysisState lattice, + Map> function) { return new StatementStore<>(lattice, function); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/CheckToolWithAnalysisResults.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/CheckToolWithAnalysisResults.java index 6db2386c8..acdc8b88f 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/CheckToolWithAnalysisResults.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/CheckToolWithAnalysisResults.java @@ -4,9 +4,6 @@ import it.unive.lisa.analysis.AnalyzedCFG; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.StatementStore; -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.checks.syntactic.CheckTool; import it.unive.lisa.conf.LiSAConfiguration; import it.unive.lisa.interprocedural.callgraph.CallGraph; @@ -27,16 +24,10 @@ * @author Luca Negrini * * @param the type of {@link AbstractState} contained in the results - * @param the type of {@link HeapDomain} contained in the results - * @param the type of {@link ValueDomain} contained in the results - * @param the type of {@link TypeDomain} contained in the results */ -public class CheckToolWithAnalysisResults, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> extends CheckTool { +public class CheckToolWithAnalysisResults> extends CheckTool { - private final Map>> results; + private final Map>> results; private final CallGraph callgraph; @@ -50,7 +41,7 @@ public class CheckToolWithAnalysisResults, * analysis */ public CheckToolWithAnalysisResults(LiSAConfiguration configuration, FileManager fileManager, - Map>> results, + Map>> results, CallGraph callgraph) { super(configuration, fileManager); this.results = results; @@ -65,7 +56,7 @@ public CheckToolWithAnalysisResults(LiSAConfiguration configuration, FileManager * @param callgraph the callgraph that has been built during the analysis */ public CheckToolWithAnalysisResults(CheckTool other, - Map>> results, + Map>> results, CallGraph callgraph) { super(other); this.results = results; @@ -80,14 +71,19 @@ public CheckToolWithAnalysisResults(CheckTool other, * * @return the results on the given cfg */ - public Collection> getResultOf(CFG cfg) { + public Collection> getResultOf(CFG cfg) { return results.get(cfg); } + /** + * Yields the {@link CallGraph} constructed during the analysis. + * + * @return the callgraph + */ public CallGraph getCallGraph() { return callgraph; } - + /** * Yields all the {@link CodeMember}s that call the given one, according to * the {@link CallGraph} that has been built during the analysis. @@ -138,8 +134,8 @@ public Collection getCallSites(CodeMember cm) { * * @throws SemanticException if something goes wrong during the computation */ - public Call getResolvedVersion(UnresolvedCall call, AnalyzedCFG result) throws SemanticException { - StatementStore store = new StatementStore<>(result.getEntryState().bottom()); + public Call getResolvedVersion(UnresolvedCall call, AnalyzedCFG result) throws SemanticException { + StatementStore store = new StatementStore<>(result.getEntryState().bottom()); for (Expression e : call.getParameters()) store.put(e, result.getAnalysisStateAfter(e)); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/SemanticCheck.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/SemanticCheck.java index b7e228d99..23ac4bf53 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/SemanticCheck.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/SemanticCheck.java @@ -1,9 +1,6 @@ package it.unive.lisa.checks.semantic; 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.checks.Check; /** @@ -15,12 +12,6 @@ * @author Luca Negrini * * @param the type of {@link AbstractState} contained in the results - * @param the type of {@link HeapDomain} contained in the results - * @param the type of {@link ValueDomain} contained in the results - * @param the type of {@link TypeDomain} contained in the results */ -public interface SemanticCheck, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> extends Check> { +public interface SemanticCheck> extends Check> { } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/LiSAConfiguration.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/LiSAConfiguration.java index 05c7353b8..5f4a2923f 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/LiSAConfiguration.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/conf/LiSAConfiguration.java @@ -138,7 +138,7 @@ public static enum DescendingPhaseType { * through {@link #callGraph}) that has been built. Defaults to an empty * set. */ - public final Collection> semanticChecks = new HashSet<>(); + public final Collection> semanticChecks = new HashSet<>(); /** * The {@link CallGraph} instance to use during the analysis. Defaults to @@ -158,7 +158,7 @@ public static enum DescendingPhaseType { * {@link LiSAFactory#getDefaultFor(Class, Object...)} in order to perform * the analysis. */ - public InterproceduralAnalysis interproceduralAnalysis; + public InterproceduralAnalysis interproceduralAnalysis; /** * The {@link AbstractState} instance to run during the analysis. This will @@ -166,7 +166,7 @@ public static enum DescendingPhaseType { * analysis, and can thus be any lattice element. If no value is set for * this field, no analysis will be executed. Defaults to {@code null}. */ - public AbstractState abstractState; + public AbstractState abstractState; /** * Sets the format to use for dumping graph files, named diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/CFGResults.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/CFGResults.java index 9f9f69155..3944b0d4b 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/CFGResults.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/CFGResults.java @@ -4,10 +4,7 @@ import it.unive.lisa.analysis.AnalyzedCFG; import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.SemanticException; -import it.unive.lisa.analysis.heap.HeapDomain; import it.unive.lisa.analysis.lattices.FunctionalLattice; -import it.unive.lisa.analysis.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import java.util.Collection; import java.util.Collections; import java.util.Map; @@ -22,18 +19,9 @@ * * @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 CFGResults, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - extends FunctionalLattice, ScopeId, AnalyzedCFG> { +public class CFGResults> + extends FunctionalLattice, ScopeId, AnalyzedCFG> { /** * Builds a new result. @@ -41,12 +29,12 @@ public class CFGResults, * @param lattice a singleton instance used for retrieving top and bottom * values */ - public CFGResults(AnalyzedCFG lattice) { + public CFGResults(AnalyzedCFG lattice) { super(lattice); } - private CFGResults(AnalyzedCFG lattice, - Map> function) { + private CFGResults(AnalyzedCFG lattice, + Map> function) { super(lattice, function); } @@ -76,8 +64,8 @@ private CFGResults(AnalyzedCFG lattice, * * @throws SemanticException if something goes wrong during the update */ - public Pair> putResult(ScopeId token, - AnalyzedCFG result) + public Pair> putResult(ScopeId token, + AnalyzedCFG result) throws SemanticException { if (function == null) { // no previous result @@ -86,7 +74,7 @@ public Pair> putResult(ScopeId token, return Pair.of(false, result); } - AnalyzedCFG previousResult = function.get(token); + AnalyzedCFG previousResult = function.get(token); if (previousResult == null) { // no previous result function.put(token, result); @@ -106,7 +94,7 @@ public Pair> putResult(ScopeId token, return Pair.of(false, previousResult); } else { // result and previous are not comparable - AnalyzedCFG lub = previousResult.lub(result); + AnalyzedCFG lub = previousResult.lub(result); function.put(token, lub); return Pair.of(true, lub); } @@ -133,7 +121,7 @@ public boolean contains(ScopeId token) { * * @return the result, or {@code null} */ - public AnalyzedCFG get(ScopeId token) { + public AnalyzedCFG get(ScopeId token) { return function == null ? null : function.get(token); } @@ -143,23 +131,23 @@ public AnalyzedCFG get(ScopeId token) { * * @return the results */ - public Collection> getAll() { + public Collection> getAll() { return function == null ? Collections.emptySet() : function.values(); } @Override - public CFGResults top() { + public CFGResults top() { return new CFGResults<>(lattice.top()); } @Override - public CFGResults bottom() { + public CFGResults bottom() { return new CFGResults<>(lattice.bottom()); } @Override - public CFGResults mk(AnalyzedCFG lattice, - Map> function) { + public CFGResults mk(AnalyzedCFG lattice, + Map> function) { return new CFGResults<>(lattice, function); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/FixpointResults.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/FixpointResults.java index f400d725e..f0793449c 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/FixpointResults.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/FixpointResults.java @@ -4,10 +4,7 @@ import it.unive.lisa.analysis.AnalyzedCFG; import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.SemanticException; -import it.unive.lisa.analysis.heap.HeapDomain; import it.unive.lisa.analysis.lattices.FunctionalLattice; -import it.unive.lisa.analysis.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.cfg.CFG; import java.util.Map; import org.apache.commons.lang3.tuple.Pair; @@ -21,18 +18,9 @@ * * @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 FixpointResults, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - extends FunctionalLattice, CFG, CFGResults> { +public class FixpointResults> + extends FunctionalLattice, CFG, CFGResults> { /** * Builds a new result. @@ -40,11 +28,11 @@ public class FixpointResults, * @param lattice a singleton instance used for retrieving top and bottom * values */ - public FixpointResults(CFGResults lattice) { + public FixpointResults(CFGResults lattice) { super(lattice); } - private FixpointResults(CFGResults lattice, Map> function) { + private FixpointResults(CFGResults lattice, Map> function) { super(lattice, function); } @@ -62,12 +50,12 @@ private FixpointResults(CFGResults lattice, Map> putResult(CFG cfg, ScopeId token, - AnalyzedCFG result) + public Pair> putResult(CFG cfg, ScopeId token, + AnalyzedCFG result) throws SemanticException { if (function == null) function = mkNewFunction(null, false); - CFGResults res = function.computeIfAbsent(cfg, c -> new CFGResults<>(result.top())); + CFGResults res = function.computeIfAbsent(cfg, c -> new CFGResults<>(result.top())); return res.putResult(token, result); } @@ -92,17 +80,17 @@ public boolean contains(CFG cfg) { * * @return the result, or {@code null} */ - public CFGResults get(CFG cfg) { + public CFGResults get(CFG cfg) { return function == null ? null : function.get(cfg); } @Override - public FixpointResults top() { + public FixpointResults top() { return new FixpointResults<>(lattice.top()); } @Override - public FixpointResults bottom() { + public FixpointResults bottom() { return new FixpointResults<>(lattice.bottom()); } @@ -120,8 +108,8 @@ public void forget(CFG cfg) { } @Override - public FixpointResults mk(CFGResults lattice, - Map> function) { + public FixpointResults mk(CFGResults lattice, + Map> function) { return new FixpointResults<>(lattice, function); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/InterproceduralAnalysis.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/InterproceduralAnalysis.java index 1e80e0270..96d1aa386 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/InterproceduralAnalysis.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/InterproceduralAnalysis.java @@ -6,11 +6,8 @@ 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.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; @@ -44,18 +41,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 interface InterproceduralAnalysis< - A extends AbstractState, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> { +public interface InterproceduralAnalysis> { /** * Initializes the interprocedural analysis of the given program. A call to @@ -92,7 +79,7 @@ public interface InterproceduralAnalysis< * @throws FixpointException if something goes wrong while evaluating the * fixpoint */ - void fixpoint(AnalysisState entryState, + void fixpoint(AnalysisState entryState, Class> fixpointWorkingSet, FixpointConfiguration conf) throws FixpointException; @@ -106,7 +93,7 @@ void fixpoint(AnalysisState entryState, * @return the result of the fixpoint computation of {@code valueDomain} * over {@code cfg} */ - Collection> getAnalysisResultsOf(CFG cfg); + Collection> getAnalysisResultsOf(CFG cfg); /** * Computes an analysis state that abstracts the execution of the possible @@ -132,11 +119,11 @@ void fixpoint(AnalysisState entryState, * * @throws SemanticException if something goes wrong during the computation */ - AnalysisState getAbstractResultOf( + AnalysisState getAbstractResultOf( CFGCall call, - AnalysisState entryState, + AnalysisState entryState, ExpressionSet[] parameters, - StatementStore expressions) + StatementStore expressions) throws SemanticException; /** @@ -160,11 +147,11 @@ AnalysisState getAbstractResultOf( * * @throws SemanticException if something goes wrong during the computation */ - AnalysisState getAbstractResultOf( + AnalysisState getAbstractResultOf( OpenCall call, - AnalysisState entryState, + AnalysisState entryState, ExpressionSet[] parameters, - StatementStore expressions) + StatementStore expressions) throws SemanticException; /** @@ -190,7 +177,7 @@ AnalysisState getAbstractResultOf( * * @return the results of the fixpoint */ - FixpointResults getFixpointResults(); + FixpointResults getFixpointResults(); /** * Converts the pre-state of {@code call} to a valid entry state for one of @@ -212,13 +199,13 @@ AnalysisState getAbstractResultOf( * @throws SemanticException if something goes wrong during the computation */ @SuppressWarnings("unchecked") - default Pair, ExpressionSet[]> scope( - AnalysisState state, + default Pair, ExpressionSet[]> scope( + AnalysisState state, ScopeToken scope, ExpressionSet[] actuals) throws SemanticException { ExpressionSet[] locals = new ExpressionSet[actuals.length]; - AnalysisState callState = state.pushScope(scope); + AnalysisState callState = state.pushScope(scope); for (int i = 0; i < actuals.length; i++) locals[i] = actuals[i].pushScope(scope); return Pair.of(callState, locals); @@ -242,15 +229,15 @@ default Pair, ExpressionSet[]> sco * * @throws SemanticException if something goes wrong during the computation */ - default AnalysisState unscope( + default AnalysisState unscope( CFGCall call, ScopeToken scope, - AnalysisState state) + AnalysisState state) throws SemanticException { if (returnsVoid(call, state)) return state.popScope(scope); - AnalysisState tmp = state.bottom(); + AnalysisState tmp = state.bottom(); Identifier meta = (Identifier) call.getMetaVariable().pushScope(scope); for (SymbolicExpression ret : state.getComputedExpressions()) tmp = tmp.lub(state.assign(meta, ret, call)); @@ -268,7 +255,7 @@ default AnalysisState unscope( * * @return {@code true} if that condition holds */ - default boolean returnsVoid(Call call, AnalysisState returned) { + default boolean returnsVoid(Call call, AnalysisState returned) { if (call.getStaticType().isVoidType()) return true; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/OpenCallPolicy.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/OpenCallPolicy.java index bdd39cb66..d3b1aa1b0 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/OpenCallPolicy.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/OpenCallPolicy.java @@ -3,10 +3,7 @@ import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.cfg.statement.call.OpenCall; import it.unive.lisa.symbolic.SymbolicExpression; @@ -24,12 +21,6 @@ public interface OpenCallPolicy { * * @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 * @param call the {@link OpenCall} under evaluation * @param entryState the state when the call is executed * @param params the symbolic expressions representing the computed @@ -40,12 +31,9 @@ public interface OpenCallPolicy { * * @throws SemanticException if something goes wrong during the computation */ - , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState apply( - OpenCall call, - AnalysisState entryState, - ExpressionSet[] params) - throws SemanticException; + > AnalysisState apply( + OpenCall call, + AnalysisState entryState, + ExpressionSet[] params) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/ReturnTopPolicy.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/ReturnTopPolicy.java index 95b01e4bb..f99559a3f 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/ReturnTopPolicy.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/ReturnTopPolicy.java @@ -3,10 +3,7 @@ import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.cfg.statement.call.OpenCall; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; @@ -32,14 +29,11 @@ private ReturnTopPolicy() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState apply( - OpenCall call, - AnalysisState entryState, - ExpressionSet[] params) - throws SemanticException { + public > AnalysisState apply( + OpenCall call, + AnalysisState entryState, + ExpressionSet[] params) + throws SemanticException { if (call.getStaticType().isVoidType()) return entryState.smallStepSemantics(new Skip(call.getLocation()), call); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/WorstCasePolicy.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/WorstCasePolicy.java index 7ebf5e212..46d4b0646 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/WorstCasePolicy.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/WorstCasePolicy.java @@ -3,10 +3,7 @@ import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.cfg.statement.call.OpenCall; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; @@ -30,15 +27,12 @@ private WorstCasePolicy() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState apply( - OpenCall call, - AnalysisState entryState, - ExpressionSet[] params) - throws SemanticException { - AnalysisState poststate = entryState.top(); + public > AnalysisState apply( + OpenCall call, + AnalysisState entryState, + ExpressionSet[] params) + throws SemanticException { + AnalysisState poststate = entryState.top(); if (call.getStaticType().isVoidType()) return poststate.smallStepSemantics(new Skip(call.getLocation()), call); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/outputs/serializableGraph/SerializableCFG.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/outputs/serializableGraph/SerializableCFG.java index f1f410e33..cd0342bc3 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/outputs/serializableGraph/SerializableCFG.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/outputs/serializableGraph/SerializableCFG.java @@ -55,8 +55,8 @@ public static SerializableGraph fromCFG(CFG source, BiFunction descriptionGenerator) { String name = source.getDescriptor().getFullSignatureWithParNames(); String desc; - if (source instanceof AnalyzedCFG && !((AnalyzedCFG) source).getId().isStartingId()) - desc = ((AnalyzedCFG) source).getId().toString(); + if (source instanceof AnalyzedCFG && !((AnalyzedCFG) source).getId().isStartingId()) + desc = ((AnalyzedCFG) source).getId().toString(); else desc = null; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/CFG.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/CFG.java index f2292afb0..dcf37b4ec 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/CFG.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/CFG.java @@ -242,12 +242,6 @@ public void simplify() { * * @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 * @param entryState the entry states to apply to each * {@link Statement} returned by * {@link #getEntrypoints()} @@ -271,16 +265,13 @@ public void simplify() { * unknown/invalid statement ends up in the * working set */ - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalyzedCFG fixpoint( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - WorkingSet ws, - FixpointConfiguration conf, - ScopeId id) throws FixpointException { - Map> start = new HashMap<>(); + public > AnalyzedCFG fixpoint( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + WorkingSet ws, + FixpointConfiguration conf, + ScopeId id) throws FixpointException { + Map> start = new HashMap<>(); entrypoints.forEach(e -> start.put(e, entryState)); return fixpoint(entryState, start, interprocedural, ws, conf, id); } @@ -301,12 +292,6 @@ T extends TypeDomain> AnalyzedCFG fixpoint( * * @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 * @param entrypoints the collection of {@link Statement}s that to use * as a starting point of the computation (that * must be nodes of this cfg) @@ -331,17 +316,14 @@ T extends TypeDomain> AnalyzedCFG fixpoint( * unknown/invalid statement ends up in the * working set */ - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalyzedCFG fixpoint( - Collection entrypoints, - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - WorkingSet ws, - FixpointConfiguration conf, - ScopeId id) throws FixpointException { - Map> start = new HashMap<>(); + public > AnalyzedCFG fixpoint( + Collection entrypoints, + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + WorkingSet ws, + FixpointConfiguration conf, + ScopeId id) throws FixpointException { + Map> start = new HashMap<>(); entrypoints.forEach(e -> start.put(e, entryState)); return fixpoint(entryState, start, interprocedural, ws, conf, id); } @@ -362,12 +344,6 @@ T extends TypeDomain> AnalyzedCFG fixpoint( * * @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 * @param singleton an instance of the {@link AnalysisState} * containing the abstract state of the analysis * to run, used to retrieve top and bottom values @@ -394,42 +370,39 @@ T extends TypeDomain> AnalyzedCFG fixpoint( * unknown/invalid statement ends up in the * working set */ - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalyzedCFG fixpoint( - AnalysisState singleton, - Map> startingPoints, - InterproceduralAnalysis interprocedural, - WorkingSet ws, - FixpointConfiguration conf, - ScopeId id) throws FixpointException { + public > AnalyzedCFG fixpoint( + AnalysisState singleton, + Map> startingPoints, + InterproceduralAnalysis interprocedural, + WorkingSet ws, + FixpointConfiguration conf, + ScopeId id) throws FixpointException { // we disable optimizations for ascending phases if there is a // descending one: the latter will need full results to start applying // glbs/narrowings from a post-fixpoint boolean isOptimized = conf.optimize && conf.descendingPhaseType == DescendingPhaseType.NONE; - Fixpoint> fix = isOptimized + Fixpoint> fix = isOptimized ? new OptimizedFixpoint<>(this, false, conf.hotspots) : new Fixpoint<>(this, false); - AscendingFixpoint asc = new AscendingFixpoint<>(this, interprocedural, conf); + AscendingFixpoint asc = new AscendingFixpoint<>(this, interprocedural, conf); - Map> starting = new HashMap<>(); - StatementStore bot = new StatementStore<>(singleton.bottom()); + Map> starting = new HashMap<>(); + StatementStore bot = new StatementStore<>(singleton.bottom()); startingPoints.forEach((st, state) -> starting.put(st, CompoundState.of(state, bot))); - Map> ascending = fix.fixpoint(starting, ws, asc); + Map> ascending = fix.fixpoint(starting, ws, asc); if (conf.descendingPhaseType == DescendingPhaseType.NONE) return flatten(isOptimized, singleton, startingPoints, interprocedural, id, ascending); fix = conf.optimize ? new OptimizedFixpoint<>(this, true, conf.hotspots) : new Fixpoint<>(this, true); - Map> descending; + Map> descending; switch (conf.descendingPhaseType) { case GLB: - DescendingGLBFixpoint dg = new DescendingGLBFixpoint<>(this, interprocedural, conf); + DescendingGLBFixpoint dg = new DescendingGLBFixpoint<>(this, interprocedural, conf); descending = fix.fixpoint(starting, ws, dg, ascending); break; case NARROWING: - DescendingNarrowingFixpoint dn = new DescendingNarrowingFixpoint<>(this, interprocedural, conf); + DescendingNarrowingFixpoint dn = new DescendingNarrowingFixpoint<>(this, interprocedural, conf); descending = fix.fixpoint(starting, ws, dn, ascending); break; case NONE: @@ -444,23 +417,23 @@ T extends TypeDomain> AnalyzedCFG fixpoint( private , T extends TypeDomain, - A extends AbstractState, - H extends HeapDomain> AnalyzedCFG flatten( + A extends AbstractState, + H extends HeapDomain> AnalyzedCFG flatten( boolean isOptimized, - AnalysisState singleton, - Map> startingPoints, - InterproceduralAnalysis interprocedural, + AnalysisState singleton, + Map> startingPoints, + InterproceduralAnalysis interprocedural, ScopeId id, - Map> fixpointResults) { - Map> finalResults = new HashMap<>(fixpointResults.size()); - for (Entry> e : fixpointResults.entrySet()) { + Map> fixpointResults) { + Map> finalResults = new HashMap<>(fixpointResults.size()); + for (Entry> e : fixpointResults.entrySet()) { finalResults.put(e.getKey(), e.getValue().postState); - for (Entry> ee : e.getValue().intermediateStates) + for (Entry> ee : e.getValue().intermediateStates) finalResults.put(ee.getKey(), ee.getValue()); } return isOptimized - ? new OptimizedAnalyzedCFG( + ? new OptimizedAnalyzedCFG( this, id, singleton, diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/Edge.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/Edge.java index 0f2068c16..781eff18a 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/Edge.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/Edge.java @@ -3,9 +3,6 @@ import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; import it.unive.lisa.analysis.SemanticException; -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.program.cfg.CFG; import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.util.datastructures.graph.GraphVisitor; @@ -100,9 +97,6 @@ public boolean equals(Object obj) { * by applying semantic assumptions. * * @param the concrete {@link AbstractState} instance - * @param the concrete {@link HeapDomain} instance - * @param the concrete {@link ValueDomain} instance - * @param the concrete {@link TypeDomain} instance * @param sourceState the {@link AnalysisState} computed at the source of * this edge * @@ -110,12 +104,9 @@ public boolean equals(Object obj) { * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState traverse( - AnalysisState sourceState) - throws SemanticException; + public abstract > AnalysisState traverse( + AnalysisState sourceState) + throws SemanticException; @Override public boolean accept(GraphVisitor visitor, V tool) { diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/FalseEdge.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/FalseEdge.java index 3a4cc5157..91da6caf0 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/FalseEdge.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/FalseEdge.java @@ -3,10 +3,7 @@ import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.UnaryExpression; @@ -38,14 +35,11 @@ public String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState traverse( - AnalysisState sourceState) - throws SemanticException { + public > AnalysisState traverse( + AnalysisState sourceState) + throws SemanticException { ExpressionSet exprs = sourceState.getComputedExpressions(); - AnalysisState result = sourceState.bottom(); + AnalysisState result = sourceState.bottom(); for (SymbolicExpression expr : exprs) { UnaryExpression negated = new UnaryExpression( expr.getStaticType(), diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/SequentialEdge.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/SequentialEdge.java index ce5eed785..47339700e 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/SequentialEdge.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/SequentialEdge.java @@ -2,9 +2,6 @@ import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; -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.program.cfg.statement.Statement; /** @@ -38,11 +35,7 @@ public String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState traverse( - AnalysisState sourceState) { + public > AnalysisState traverse(AnalysisState sourceState) { return sourceState; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/TrueEdge.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/TrueEdge.java index 147032ac5..433939465 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/TrueEdge.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/edge/TrueEdge.java @@ -3,10 +3,7 @@ import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.symbolic.SymbolicExpression; @@ -35,14 +32,11 @@ public String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState traverse( - AnalysisState sourceState) - throws SemanticException { + public > AnalysisState traverse( + AnalysisState sourceState) + throws SemanticException { ExpressionSet exprs = sourceState.getComputedExpressions(); - AnalysisState result = sourceState.bottom(); + AnalysisState result = sourceState.bottom(); for (SymbolicExpression expr : exprs) result = result.lub(sourceState.assume(expr, getSource(), getDestination())); return result; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/AscendingFixpoint.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/AscendingFixpoint.java index 67192f3b8..541fe115c 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/AscendingFixpoint.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/AscendingFixpoint.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.conf.FixpointConfiguration; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; @@ -23,18 +20,9 @@ * * @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 AscendingFixpoint, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - extends CFGFixpoint { +public class AscendingFixpoint> + extends CFGFixpoint { private final FixpointConfiguration config; private final Map lubs; @@ -49,7 +37,7 @@ public class AscendingFixpoint, * @param config the {@link FixpointConfiguration} to use */ public AscendingFixpoint(CFG target, - InterproceduralAnalysis interprocedural, + InterproceduralAnalysis interprocedural, FixpointConfiguration config) { super(target, interprocedural); this.config = config; @@ -58,9 +46,9 @@ public AscendingFixpoint(CFG target, } @Override - public CompoundState operation(Statement node, - CompoundState approx, - CompoundState old) throws SemanticException { + public CompoundState operation(Statement node, + CompoundState approx, + CompoundState old) throws SemanticException { if (config.wideningThreshold < 0) // invalid threshold means always lub return old.lub(approx); @@ -72,8 +60,8 @@ public CompoundState operation(Statement node, int lub = lubs.computeIfAbsent(node, st -> config.wideningThreshold); if (lub == 0) { - AnalysisState post = old.postState.widening(approx.postState); - StatementStore intermediate; + AnalysisState post = old.postState.widening(approx.postState); + StatementStore intermediate; if (config.useWideningPoints) // no need to widen the intermediate expressions as // well: we force convergence on the final post state @@ -89,8 +77,8 @@ public CompoundState operation(Statement node, } @Override - public boolean equality(Statement node, CompoundState approx, - CompoundState old) throws SemanticException { + public boolean equality(Statement node, CompoundState approx, + CompoundState old) throws SemanticException { return approx.lessOrEqual(old); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/CFGFixpoint.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/CFGFixpoint.java index 5e32e4e85..ec6d0255f 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/CFGFixpoint.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/CFGFixpoint.java @@ -5,9 +5,6 @@ import it.unive.lisa.analysis.Lattice; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.StatementStore; -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.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.VariableTableEntry; @@ -29,18 +26,9 @@ * * @param the type of {@link AbstractState} contained into the analysis * state computed by the fixpoint - * @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 abstract class CFGFixpoint, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - implements FixpointImplementation> { +public abstract class CFGFixpoint> + implements FixpointImplementation> { /** * The graph targeted by this implementation. @@ -50,7 +38,7 @@ public abstract class CFGFixpoint, /** * The {@link InterproceduralAnalysis} to use for semantics invocations. */ - protected final InterproceduralAnalysis interprocedural; + protected final InterproceduralAnalysis interprocedural; /** * Builds the fixpoint implementation. @@ -59,16 +47,16 @@ public abstract class CFGFixpoint, * @param interprocedural the {@link InterproceduralAnalysis} to use for * semantics invocation */ - public CFGFixpoint(CFG graph, InterproceduralAnalysis interprocedural) { + public CFGFixpoint(CFG graph, InterproceduralAnalysis interprocedural) { this.graph = graph; this.interprocedural = interprocedural; } @Override - public CompoundState semantics(Statement node, - CompoundState entrystate) throws SemanticException { - StatementStore expressions = new StatementStore<>(entrystate.postState.bottom()); - AnalysisState approx = node.semantics(entrystate.postState, interprocedural, expressions); + public CompoundState semantics(Statement node, + CompoundState entrystate) throws SemanticException { + StatementStore expressions = new StatementStore<>(entrystate.postState.bottom()); + AnalysisState approx = node.semantics(entrystate.postState, interprocedural, expressions); if (node instanceof Expression) // we forget the meta variables now as the values are popped from // the stack here @@ -77,9 +65,9 @@ public CompoundState semantics(Statement node, } @Override - public CompoundState traverse(Edge edge, - CompoundState entrystate) throws SemanticException { - AnalysisState approx = edge.traverse(entrystate.postState); + public CompoundState traverse(Edge edge, + CompoundState entrystate) throws SemanticException { + AnalysisState approx = edge.traverse(entrystate.postState); // we remove out of scope variables here List toRemove = new LinkedList<>(); @@ -101,9 +89,9 @@ public CompoundState traverse(Edge edge, } @Override - public CompoundState union(Statement node, - CompoundState left, - CompoundState right) throws SemanticException { + public CompoundState union(Statement node, + CompoundState left, + CompoundState right) throws SemanticException { return left.lub(right); } @@ -115,54 +103,36 @@ public CompoundState union(Statement node, * * @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 static final class CompoundState, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> implements Lattice> { + public static final class CompoundState> implements Lattice> { /** * Builds a compound state from the given post-states. * * @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 * @param postState the overall post-state of a statement * @param intermediateStates the post-state of intermediate expressions * * @return the generated compound state */ - public static , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> CompoundState of( - AnalysisState postState, - StatementStore intermediateStates) { + public static > CompoundState of( + AnalysisState postState, + StatementStore intermediateStates) { return new CompoundState<>(postState, intermediateStates); } /** * The overall post-state of a statement. */ - public final AnalysisState postState; + public final AnalysisState postState; /** * The post-state of intermediate expressions. */ - public final StatementStore intermediateStates; + public final StatementStore intermediateStates; - private CompoundState(AnalysisState postState, StatementStore intermediateStates) { + private CompoundState(AnalysisState postState, StatementStore intermediateStates) { this.postState = postState; this.intermediateStates = intermediateStates; } @@ -184,7 +154,7 @@ public boolean equals(Object obj) { return false; if (getClass() != obj.getClass()) return false; - CompoundState other = (CompoundState) obj; + CompoundState other = (CompoundState) obj; if (intermediateStates == null) { if (other.intermediateStates != null) return false; @@ -204,17 +174,17 @@ public String toString() { } @Override - public boolean lessOrEqual(CompoundState other) throws SemanticException { + public boolean lessOrEqual(CompoundState other) throws SemanticException { return postState.lessOrEqual(other.postState) && intermediateStates.lessOrEqual(other.intermediateStates); } @Override - public CompoundState lub(CompoundState other) throws SemanticException { + public CompoundState lub(CompoundState other) throws SemanticException { return CompoundState.of(postState.lub(other.postState), intermediateStates.lub(other.intermediateStates)); } @Override - public CompoundState top() { + public CompoundState top() { return CompoundState.of(postState.top(), intermediateStates.top()); } @@ -224,7 +194,7 @@ public boolean isTop() { } @Override - public CompoundState bottom() { + public CompoundState bottom() { return CompoundState.of(postState.bottom(), intermediateStates.bottom()); } @@ -234,18 +204,18 @@ public boolean isBottom() { } @Override - public CompoundState glb(CompoundState other) throws SemanticException { + public CompoundState glb(CompoundState other) throws SemanticException { return CompoundState.of(postState.glb(other.postState), intermediateStates.glb(other.intermediateStates)); } @Override - public CompoundState narrowing(CompoundState other) throws SemanticException { + public CompoundState narrowing(CompoundState other) throws SemanticException { return CompoundState.of(postState.narrowing(other.postState), intermediateStates.narrowing(other.intermediateStates)); } @Override - public CompoundState widening(CompoundState other) throws SemanticException { + public CompoundState widening(CompoundState other) throws SemanticException { return CompoundState.of(postState.widening(other.postState), intermediateStates.widening(other.intermediateStates)); } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/DescendingGLBFixpoint.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/DescendingGLBFixpoint.java index 4c6a59a9d..f9134b910 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/DescendingGLBFixpoint.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/DescendingGLBFixpoint.java @@ -2,9 +2,6 @@ import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.SemanticException; -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.conf.FixpointConfiguration; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; @@ -20,18 +17,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 DescendingGLBFixpoint, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - extends CFGFixpoint { +public class DescendingGLBFixpoint> extends CFGFixpoint { private final int maxGLBs; private final Map glbs; @@ -45,7 +32,7 @@ public class DescendingGLBFixpoint, * @param config the {@link FixpointConfiguration} to use */ public DescendingGLBFixpoint(CFG target, - InterproceduralAnalysis interprocedural, + InterproceduralAnalysis interprocedural, FixpointConfiguration config) { super(target, interprocedural); this.maxGLBs = config.glbThreshold; @@ -53,9 +40,9 @@ public DescendingGLBFixpoint(CFG target, } @Override - public CompoundState operation(Statement node, - CompoundState approx, - CompoundState old) throws SemanticException { + public CompoundState operation(Statement node, + CompoundState approx, + CompoundState old) throws SemanticException { if (maxGLBs < 0) return old; @@ -68,8 +55,8 @@ public CompoundState operation(Statement node, } @Override - public boolean equality(Statement node, CompoundState approx, - CompoundState old) throws SemanticException { + public boolean equality(Statement node, CompoundState approx, + CompoundState old) throws SemanticException { return old.lessOrEqual(approx); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/DescendingNarrowingFixpoint.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/DescendingNarrowingFixpoint.java index f889d3528..5f9ec5f4f 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/DescendingNarrowingFixpoint.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/DescendingNarrowingFixpoint.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.conf.FixpointConfiguration; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; @@ -20,18 +17,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 DescendingNarrowingFixpoint, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - extends CFGFixpoint { +public class DescendingNarrowingFixpoint> extends CFGFixpoint { private final FixpointConfiguration config; private final Collection wideningPoints; @@ -45,7 +32,7 @@ public class DescendingNarrowingFixpoint, * @param config the {@link FixpointConfiguration} to use */ public DescendingNarrowingFixpoint(CFG target, - InterproceduralAnalysis interprocedural, + InterproceduralAnalysis interprocedural, FixpointConfiguration config) { super(target, interprocedural); this.config = config; @@ -53,16 +40,16 @@ public DescendingNarrowingFixpoint(CFG target, } @Override - public CompoundState operation(Statement node, - CompoundState approx, - CompoundState old) throws SemanticException { + public CompoundState operation(Statement node, + CompoundState approx, + CompoundState old) throws SemanticException { if (wideningPoints == null || !wideningPoints.contains(node)) // optimization: never apply narrowing on normal instructions, // save time and precision and only apply to widening points return old.glb(approx); - AnalysisState post = old.postState.narrowing(approx.postState); - StatementStore intermediate; + AnalysisState post = old.postState.narrowing(approx.postState); + StatementStore intermediate; if (config.useWideningPoints) // no need to narrow the intermediate expressions as // well: we force convergence on the final post state @@ -74,8 +61,8 @@ public CompoundState operation(Statement node, } @Override - public boolean equality(Statement node, CompoundState approx, - CompoundState old) throws SemanticException { + public boolean equality(Statement node, CompoundState approx, + CompoundState old) throws SemanticException { return old.lessOrEqual(approx); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/OptimizedFixpoint.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/OptimizedFixpoint.java index 0bdc37a82..d857ebeaa 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/OptimizedFixpoint.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/fixpoints/OptimizedFixpoint.java @@ -5,9 +5,6 @@ import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; import it.unive.lisa.analysis.StatementStore; -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.program.cfg.CFG; import it.unive.lisa.program.cfg.edge.Edge; import it.unive.lisa.program.cfg.fixpoints.CFGFixpoint.CompoundState; @@ -15,7 +12,6 @@ import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.datastructures.graph.Graph; import it.unive.lisa.util.datastructures.graph.algorithms.Fixpoint; -import it.unive.lisa.util.datastructures.graph.algorithms.Fixpoint.FixpointImplementation; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; import java.util.Collection; import java.util.HashMap; @@ -36,18 +32,9 @@ * * @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 OptimizedFixpoint, - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> - extends Fixpoint> { +public class OptimizedFixpoint> + extends Fixpoint> { private final Predicate hotspots; @@ -68,13 +55,13 @@ public OptimizedFixpoint(CFG graph, boolean forceFullEvaluation, Predicate> fixpoint( - Map> startingPoints, + public Map> fixpoint( + Map> startingPoints, WorkingSet ws, - FixpointImplementation> implementation, - Map> initialResult) + FixpointImplementation> implementation, + Map> initialResult) throws FixpointException { - Map> result = initialResult == null + Map> result = initialResult == null ? new HashMap<>(graph.getNodesCount()) : new HashMap<>(initialResult); @@ -85,7 +72,7 @@ public Map> fixpoint( if (forceFullEvaluation) toProcess = new HashSet<>(bbs.keySet()); - CompoundState newApprox; + CompoundState newApprox; while (!ws.isEmpty()) { Statement current = ws.pop(); @@ -98,7 +85,7 @@ public Map> fixpoint( if (bb == null) throw new FixpointException("'" + current + "' is not the leader of a basic block of '" + graph + "'"); - CompoundState entrystate = getEntryState( + CompoundState entrystate = getEntryState( current, startingPoints.get(current), implementation, @@ -109,7 +96,7 @@ public Map> fixpoint( newApprox = analyze(result, implementation, entrystate, bb); Statement closing = bb[bb.length - 1]; - CompoundState oldApprox = result.get(closing); + CompoundState oldApprox = result.get(closing); if (oldApprox != null) try { newApprox = implementation.operation(closing, newApprox, oldApprox); @@ -150,17 +137,17 @@ public Map> fixpoint( return result; } - private CompoundState analyze( - Map> result, - FixpointImplementation> implementation, - CompoundState entrystate, + private CompoundState analyze( + Map> result, + FixpointImplementation> implementation, + CompoundState entrystate, Statement[] bb) throws FixpointException { - StatementStore emptyIntermediate = entrystate.intermediateStates.bottom(); - CompoundState newApprox = CompoundState.of( + StatementStore emptyIntermediate = entrystate.intermediateStates.bottom(); + CompoundState newApprox = CompoundState.of( entrystate.postState.bottom(), emptyIntermediate); - CompoundState entry = entrystate; + CompoundState entry = entrystate; for (Statement cursor : bb) try { newApprox = implementation.semantics(cursor, entry); @@ -168,7 +155,7 @@ private CompoundState analyze( // storing approximations into result is a trick: it won't ever // be used in fixpoint comparisons, but it will still make // it out as part of the final result - for (Entry> intermediate : newApprox.intermediateStates) + for (Entry> intermediate : newApprox.intermediateStates) if (intermediate.getKey().stopsExecution() || (hotspots != null && hotspots.test(intermediate.getKey()))) result.put(intermediate.getKey(), CompoundState.of(intermediate.getValue(), emptyIntermediate)); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Assignment.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Assignment.java index 9bf2dee71..6e7cdf73f 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Assignment.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Assignment.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -95,16 +92,13 @@ public final String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException { + public > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException { return state.assign(left, right, this); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/BinaryExpression.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/BinaryExpression.java index 40619207d..a4137a7ed 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/BinaryExpression.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/BinaryExpression.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -113,16 +110,13 @@ public Expression getRight() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { - AnalysisState result = state.bottom(); + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { + AnalysisState result = state.bottom(); for (SymbolicExpression left : params[0]) for (SymbolicExpression right : params[1]) result = result.lub(binarySemantics(interprocedural, state, left, right, expressions)); @@ -136,9 +130,6 @@ T extends TypeDomain> AnalysisState expressionSemantics( * sub-expressions will be forgotten after this expression returns. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param interprocedural the interprocedural analysis of the program to * analyze * @param state the state where the expression is to be evaluated @@ -158,14 +149,11 @@ T extends TypeDomain> AnalysisState expressionSemantics( * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException; + public abstract > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/BinaryStatement.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/BinaryStatement.java index 05534682a..47b7d0371 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/BinaryStatement.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/BinaryStatement.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -75,16 +72,13 @@ public Expression getRight() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState statementSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { - AnalysisState result = state.bottom(); + public > AnalysisState statementSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { + AnalysisState result = state.bottom(); for (SymbolicExpression left : params[0]) for (SymbolicExpression right : params[1]) result = result.lub(binarySemantics(interprocedural, state, left, right, expressions)); @@ -98,9 +92,6 @@ T extends TypeDomain> AnalysisState statementSemantics( * sub-expressions will be forgotten after this statement returns. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param interprocedural the interprocedural analysis of the program to * analyze * @param state the state where the statement is to be evaluated @@ -120,14 +111,11 @@ T extends TypeDomain> AnalysisState statementSemantics( * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState binarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException; + public abstract > AnalysisState binarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Expression.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Expression.java index 9b2784a3f..09944afa2 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Expression.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Expression.java @@ -1,12 +1,5 @@ package it.unive.lisa.program.cfg.statement; -import java.util.Collection; -import java.util.HashSet; -import java.util.Objects; - -import org.apache.logging.log4j.LogManager; -import org.apache.logging.log4j.Logger; - import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; import it.unive.lisa.program.cfg.statement.call.Call; @@ -14,6 +7,11 @@ 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.Objects; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; /** * An expression that is part of a statement of the program. diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NaryExpression.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NaryExpression.java index e6bd5509f..2f2dbb5ec 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NaryExpression.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NaryExpression.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -226,19 +223,15 @@ public boolean equals(Object obj) { */ @Override @SuppressWarnings("unchecked") - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions) - throws SemanticException { + public > AnalysisState semantics( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions) + throws SemanticException { ExpressionSet[] computed = new ExpressionSet[subExpressions.length]; - AnalysisState eval = order.evaluate(subExpressions, entryState, interprocedural, expressions, computed); - AnalysisState result = expressionSemantics(interprocedural, eval, computed, expressions); + AnalysisState eval = order.evaluate(subExpressions, entryState, interprocedural, expressions, computed); + AnalysisState result = expressionSemantics(interprocedural, eval, computed, expressions); Collection vars = getMetaVariables(); for (Expression sub : subExpressions) { @@ -256,9 +249,6 @@ T extends TypeDomain> AnalysisState semantics( * sub-expressions will be forgotten after this call returns. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param interprocedural the interprocedural analysis of the program to * analyze * @param state the state where the expression is to be evaluated @@ -275,12 +265,9 @@ T extends TypeDomain> AnalysisState semantics( * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, StatementStore expressions) - throws SemanticException; + public abstract > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, StatementStore expressions) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NaryStatement.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NaryStatement.java index 951d033b7..235a776ad 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NaryStatement.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NaryStatement.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -186,19 +183,15 @@ public boolean equals(Object obj) { */ @Override @SuppressWarnings("unchecked") - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions) - throws SemanticException { + public > AnalysisState semantics( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions) + throws SemanticException { ExpressionSet[] computed = new ExpressionSet[subExpressions.length]; - AnalysisState eval = order.evaluate(subExpressions, entryState, interprocedural, expressions, computed); - AnalysisState result = statementSemantics(interprocedural, eval, computed, expressions); + AnalysisState eval = order.evaluate(subExpressions, entryState, interprocedural, expressions, computed); + AnalysisState result = statementSemantics(interprocedural, eval, computed, expressions); for (Expression sub : subExpressions) // we forget the meta variables now as the values are popped from @@ -213,9 +206,6 @@ T extends TypeDomain> AnalysisState semantics( * sub-expressions will be forgotten after this call returns. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param interprocedural the interprocedural analysis of the program to * analyze * @param state the state where the statement is to be evaluated @@ -232,12 +222,9 @@ T extends TypeDomain> AnalysisState semantics( * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState statementSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, StatementStore expressions) - throws SemanticException; + public abstract > AnalysisState statementSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, StatementStore expressions) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NoOp.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NoOp.java index d61e72989..318679440 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NoOp.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/NoOp.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -60,14 +57,11 @@ public final String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions) - throws SemanticException { + public > AnalysisState semantics( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions) + throws SemanticException { return entryState.smallStepSemantics(new Skip(getLocation()), this); } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Ret.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Ret.java index 4b47a518a..ba4347ea1 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Ret.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Ret.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -66,14 +63,11 @@ public final String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions) - throws SemanticException { + public > AnalysisState semantics( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions) + throws SemanticException { return entryState.smallStepSemantics(new Skip(getLocation()), this); } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Return.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Return.java index 8d24c1396..534413e71 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Return.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Return.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -50,15 +47,12 @@ public final Identifier getMetaVariable() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException { + public > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException { Identifier meta = getMetaVariable(); return state.assign(meta, expr, this); } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Statement.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Statement.java index c81b651a7..8db283bc8 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Statement.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Statement.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -122,9 +119,6 @@ public boolean equals(Object obj) { * {@code expressions}. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param entryState the entry state that represents the abstract * values of each program variable and memory * location when the execution reaches this @@ -139,14 +133,11 @@ public boolean equals(Object obj) { * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions) - throws SemanticException; + public abstract > AnalysisState semantics( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions) + throws SemanticException; @Override public CodeLocation getLocation() { diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/TernaryExpression.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/TernaryExpression.java index 42a71f02e..b124017de 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/TernaryExpression.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/TernaryExpression.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -128,16 +125,13 @@ public Expression getRight() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { - AnalysisState result = state.bottom(); + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { + AnalysisState result = state.bottom(); for (SymbolicExpression left : params[0]) for (SymbolicExpression middle : params[1]) for (SymbolicExpression right : params[2]) @@ -152,9 +146,6 @@ T extends TypeDomain> AnalysisState expressionSemantics( * sub-expressions will be forgotten after this expression returns. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param interprocedural the interprocedural analysis of the program to * analyze * @param state the state where the expression is to be evaluated @@ -177,15 +168,12 @@ T extends TypeDomain> AnalysisState expressionSemantics( * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState ternarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression middle, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException; + public abstract > AnalysisState ternarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression middle, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/TernaryStatement.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/TernaryStatement.java index a155029a2..a3ce67f89 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/TernaryStatement.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/TernaryStatement.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -86,16 +83,13 @@ public Expression getRight() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState statementSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { - AnalysisState result = state.bottom(); + public > AnalysisState statementSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { + AnalysisState result = state.bottom(); for (SymbolicExpression left : params[0]) for (SymbolicExpression middle : params[1]) for (SymbolicExpression right : params[2]) @@ -110,9 +104,6 @@ T extends TypeDomain> AnalysisState statementSemantics( * sub-expressions will be forgotten after this statement returns. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param interprocedural the interprocedural analysis of the program to * analyze * @param state the state where the statement is to be evaluated @@ -135,15 +126,12 @@ T extends TypeDomain> AnalysisState statementSemantics( * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState ternarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression left, - SymbolicExpression middle, - SymbolicExpression right, - StatementStore expressions) - throws SemanticException; + public abstract > AnalysisState ternarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression left, + SymbolicExpression middle, + SymbolicExpression right, + StatementStore expressions) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Throw.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Throw.java index 6deccc552..0a84b2145 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Throw.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/Throw.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -45,15 +42,12 @@ public boolean throwsError() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException { + public > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException { // only temporary return state.smallStepSemantics(new Skip(getLocation()), this); } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/UnaryExpression.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/UnaryExpression.java index 331d2c1aa..e31f7fb9c 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/UnaryExpression.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/UnaryExpression.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -102,16 +99,13 @@ public Expression getSubExpression() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { - AnalysisState result = state.bottom(); + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { + AnalysisState result = state.bottom(); for (SymbolicExpression expr : params[0]) result = result.lub(unarySemantics(interprocedural, state, expr, expressions)); return result; @@ -123,9 +117,6 @@ T extends TypeDomain> AnalysisState expressionSemantics( * will be forgotten after this expression returns. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param interprocedural the interprocedural analysis of the program to * analyze * @param state the state where the expression is to be evaluated @@ -141,13 +132,10 @@ T extends TypeDomain> AnalysisState expressionSemantics( * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException; + public abstract > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/UnaryStatement.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/UnaryStatement.java index 5dcccf1c3..9fb20672c 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/UnaryStatement.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/UnaryStatement.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -63,16 +60,13 @@ public Expression getSubExpression() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState statementSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { - AnalysisState result = state.bottom(); + public > AnalysisState statementSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { + AnalysisState result = state.bottom(); for (SymbolicExpression expr : params[0]) result = result.lub(unarySemantics(interprocedural, state, expr, expressions)); return result; @@ -84,9 +78,6 @@ T extends TypeDomain> AnalysisState statementSemantics( * will be forgotten after this statement returns. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param interprocedural the interprocedural analysis of the program to * analyze * @param state the state where the statement is to be evaluated @@ -102,13 +93,10 @@ T extends TypeDomain> AnalysisState statementSemantics( * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException; + public abstract > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/VariableRef.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/VariableRef.java index 1b59438cf..a7e350e56 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/VariableRef.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/VariableRef.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.annotations.Annotation; import it.unive.lisa.program.annotations.Annotations; @@ -118,13 +115,10 @@ public Variable getVariable() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, InterproceduralAnalysis interprocedural, - StatementStore expressions) - throws SemanticException { + public > AnalysisState semantics( + AnalysisState entryState, InterproceduralAnalysis interprocedural, + StatementStore expressions) + throws SemanticException { SymbolicExpression expr = getVariable(); return entryState.smallStepSemantics(expr, this); } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CFGCall.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CFGCall.java index 5192723a6..a64f893b9 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CFGCall.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CFGCall.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.annotations.Annotation; import it.unive.lisa.program.cfg.CFG; @@ -178,15 +175,12 @@ public final Identifier getMetaVariable() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState compute( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions, - ExpressionSet[] parameters) - throws SemanticException { + public > AnalysisState compute( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions, + ExpressionSet[] parameters) + throws SemanticException { return interprocedural.getAbstractResultOf(this, entryState, parameters, expressions); } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/Call.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/Call.java index 97e1f3aca..9eeae457c 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/Call.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/Call.java @@ -1,18 +1,9 @@ package it.unive.lisa.program.cfg.statement.call; -import java.util.HashSet; -import java.util.Objects; -import java.util.Set; - -import org.apache.commons.lang3.StringUtils; - import it.unive.lisa.analysis.AbstractState; 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.callgraph.CallGraph; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -21,6 +12,10 @@ import it.unive.lisa.program.cfg.statement.evaluation.EvaluationOrder; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.type.Type; +import java.util.HashSet; +import java.util.Objects; +import java.util.Set; +import org.apache.commons.lang3.StringUtils; /** * A call to another cfg. @@ -241,9 +236,6 @@ public boolean equals(Object obj) { * call, retrieved by accessing the given {@link StatementStore}. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param expressions the store containing the computed states for the * parameters * @@ -253,15 +245,12 @@ public boolean equals(Object obj) { * types */ @SuppressWarnings("unchecked") - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> Set[] parameterTypes(StatementStore expressions) - throws SemanticException { + public > Set[] parameterTypes(StatementStore expressions) + throws SemanticException { Expression[] actuals = getParameters(); Set[] types = new Set[actuals.length]; for (int i = 0; i < actuals.length; i++) { - AnalysisState state = expressions.getState(actuals[i]); + AnalysisState state = expressions.getState(actuals[i]); Set t = new HashSet<>(); for (SymbolicExpression e : state.getComputedExpressions()) t.addAll(state.getState().getRuntimeTypesOf(e, this)); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CallWithResult.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CallWithResult.java index e679dd813..4a7e3e3b8 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CallWithResult.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CallWithResult.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -60,9 +57,6 @@ public CallWithResult(CFG cfg, CodeLocation location, CallType callType, String * @param parameters the expressions representing the actual parameters * of the call * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * * @return an abstract analysis state representing the abstract result of * the cfg call. The @@ -72,32 +66,26 @@ public CallWithResult(CFG cfg, CodeLocation location, CallType callType, String * * @throws SemanticException if something goes wrong during the computation */ - public abstract , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState compute( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions, - ExpressionSet[] parameters) - throws SemanticException; + public abstract > AnalysisState compute( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions, + ExpressionSet[] parameters) + throws SemanticException; @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { // the stack has to be empty state = new AnalysisState<>(state.getState(), new ExpressionSet<>(), state.getAliasing()); // this will contain only the information about the returned // metavariable - AnalysisState returned = compute(state, interprocedural, expressions, params); + AnalysisState returned = compute(state, interprocedural, expressions, params); if (interprocedural.returnsVoid(this, returned)) // no need to add the meta variable since nothing has been pushed on diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/MultiCall.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/MultiCall.java index 5305677a8..d7ea70283 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/MultiCall.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/MultiCall.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -170,16 +167,13 @@ public void setSource(UnresolvedCall source) { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { - AnalysisState result = state.bottom(); + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { + AnalysisState result = state.bottom(); for (Call call : calls) { result = result.lub(call.expressionSemantics(interprocedural, state, params, expressions)); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/NamedParameterExpression.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/NamedParameterExpression.java index fafef719e..96df70599 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/NamedParameterExpression.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/NamedParameterExpression.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -80,15 +77,12 @@ public boolean equals(Object obj) { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState unarySemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - SymbolicExpression expr, - StatementStore expressions) - throws SemanticException { + public > AnalysisState unarySemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + SymbolicExpression expr, + StatementStore expressions) + throws SemanticException { return state.smallStepSemantics(expr, this); } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/NativeCall.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/NativeCall.java index cf1f89b87..374e7189a 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/NativeCall.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/NativeCall.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.interprocedural.callgraph.CallResolutionException; import it.unive.lisa.program.cfg.CFG; @@ -171,22 +168,19 @@ public String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { - AnalysisState result = state.bottom(); + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { + AnalysisState result = state.bottom(); Expression[] parameters = getSubExpressions(); ParameterAssigningStrategy strategy = getProgram().getFeatures().getAssigningStrategy(); for (NativeCFG nat : targets) try { - Pair, ExpressionSet[]> prepared = strategy.prepare(this, + Pair, ExpressionSet[]> prepared = strategy.prepare(this, state, interprocedural, expressions, nat.getDescriptor().getFormals(), params); NaryExpression rewritten = nat.rewrite(this, parameters); diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/OpenCall.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/OpenCall.java index 2df377ce9..9e7ec7d25 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/OpenCall.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/OpenCall.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -137,15 +134,12 @@ public final Identifier getMetaVariable() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState compute( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions, - ExpressionSet[] parameters) - throws SemanticException { + public > AnalysisState compute( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions, + ExpressionSet[] parameters) + throws SemanticException { return interprocedural.getAbstractResultOf(this, entryState, parameters, expressions); } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/TruncatedParamsCall.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/TruncatedParamsCall.java index d22715f65..e15f20acb 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/TruncatedParamsCall.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/TruncatedParamsCall.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CodeMember; import it.unive.lisa.program.cfg.statement.Expression; @@ -78,17 +75,14 @@ public boolean equals(Object obj) { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { Expression[] actuals = getParameters(); - AnalysisState post; + AnalysisState post; if (params.length == actuals.length) { post = call.expressionSemantics(interprocedural, state, params, expressions); } else { diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/UnresolvedCall.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/UnresolvedCall.java index 6c3c9f1bb..0cb3820ce 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/UnresolvedCall.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/UnresolvedCall.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.interprocedural.callgraph.CallGraph; import it.unive.lisa.interprocedural.callgraph.CallResolutionException; @@ -114,22 +111,19 @@ public UnresolvedCall(CFG cfg, CodeLocation location, CallType callType, String } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState expressionSemantics( - InterproceduralAnalysis interprocedural, - AnalysisState state, - ExpressionSet[] params, - StatementStore expressions) - throws SemanticException { + public > AnalysisState expressionSemantics( + InterproceduralAnalysis interprocedural, + AnalysisState state, + ExpressionSet[] params, + StatementStore expressions) + throws SemanticException { Call resolved; try { resolved = interprocedural.resolve(this, parameterTypes(expressions), state.getAliasing()); } catch (CallResolutionException e) { throw new SemanticException("Unable to resolve call " + this, e); } - AnalysisState result = resolved.expressionSemantics(interprocedural, state, params, expressions); + AnalysisState result = resolved.expressionSemantics(interprocedural, state, params, expressions); getMetaVariables().addAll(resolved.getMetaVariables()); return result; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/EvaluationOrder.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/EvaluationOrder.java index 9dd9e66b9..fc8a34dfa 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/EvaluationOrder.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/EvaluationOrder.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.statement.Expression; import it.unive.lisa.program.cfg.statement.NaryExpression; @@ -73,9 +70,6 @@ public interface EvaluationOrder { * stack. * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param subExpressions the sub-expressions to evaluate * @param entryState the state to use as starting point for the * evaluation @@ -94,14 +88,11 @@ public interface EvaluationOrder { * * @throws SemanticException if something goes wrong during the evaluation */ - , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState evaluate( - Expression[] subExpressions, - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions, - ExpressionSet[] computed) - throws SemanticException; + > AnalysisState evaluate( + Expression[] subExpressions, + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions, + ExpressionSet[] computed) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/LeftToRightEvaluation.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/LeftToRightEvaluation.java index 3502034ea..1c4046fc5 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/LeftToRightEvaluation.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/LeftToRightEvaluation.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.statement.Expression; import it.unive.lisa.symbolic.SymbolicExpression; @@ -29,22 +26,19 @@ private LeftToRightEvaluation() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState evaluate( - Expression[] subExpressions, - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions, - ExpressionSet[] computed) - throws SemanticException { + public > AnalysisState evaluate( + Expression[] subExpressions, + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions, + ExpressionSet[] computed) + throws SemanticException { if (subExpressions.length == 0) return entryState; - AnalysisState postState = entryState; + AnalysisState postState = entryState; for (int i = 0; i < computed.length; i++) { - AnalysisState tmp = subExpressions[i].semantics(postState, interprocedural, expressions); + AnalysisState tmp = subExpressions[i].semantics(postState, interprocedural, expressions); expressions.put(subExpressions[i], tmp); computed[i] = tmp.getComputedExpressions(); for (SymbolicExpression e : computed[i]) diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/RightToLeftEvaluation.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/RightToLeftEvaluation.java index f9ace8e91..07cec5c72 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/RightToLeftEvaluation.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/evaluation/RightToLeftEvaluation.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.statement.Expression; import it.unive.lisa.symbolic.SymbolicExpression; @@ -29,22 +26,19 @@ private RightToLeftEvaluation() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState evaluate( - Expression[] subExpressions, - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions, - ExpressionSet[] computed) - throws SemanticException { + public > AnalysisState evaluate( + Expression[] subExpressions, + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions, + ExpressionSet[] computed) + throws SemanticException { if (subExpressions.length == 0) return entryState; - AnalysisState postState = entryState; + AnalysisState postState = entryState; for (int i = computed.length - 1; i >= 0; i--) { - AnalysisState tmp = subExpressions[i].semantics(postState, interprocedural, expressions); + AnalysisState tmp = subExpressions[i].semantics(postState, interprocedural, expressions); expressions.put(subExpressions[i], tmp); computed[i] = tmp.getComputedExpressions(); for (SymbolicExpression e : computed[i]) diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/literal/Literal.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/literal/Literal.java index 84e2ae230..794e665a3 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/literal/Literal.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/literal/Literal.java @@ -4,9 +4,6 @@ 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.value.TypeDomain; -import it.unive.lisa.analysis.value.ValueDomain; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.CodeLocation; @@ -91,14 +88,11 @@ public String toString() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> AnalysisState semantics( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - StatementStore expressions) - throws SemanticException { + public > AnalysisState semantics( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + StatementStore expressions) + throws SemanticException { return entryState.smallStepSemantics(new Constant(getStaticType(), getValue(), getLocation()), this); } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/OrderPreservingAssigningStrategy.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/OrderPreservingAssigningStrategy.java index 59257d22d..ac5d1ced4 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/OrderPreservingAssigningStrategy.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/OrderPreservingAssigningStrategy.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.Parameter; import it.unive.lisa.program.cfg.statement.call.Call; @@ -31,21 +28,18 @@ private OrderPreservingAssigningStrategy() { } @Override - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> Pair, ExpressionSet[]> prepare( - Call call, - AnalysisState callState, - InterproceduralAnalysis interprocedural, - StatementStore expressions, - Parameter[] formals, - ExpressionSet[] parameters) - throws SemanticException { + public > Pair, ExpressionSet[]> prepare( + Call call, + AnalysisState callState, + InterproceduralAnalysis interprocedural, + StatementStore expressions, + Parameter[] formals, + ExpressionSet[] parameters) + throws SemanticException { // prepare the state for the call: assign the value to each parameter - AnalysisState prepared = callState; + AnalysisState prepared = callState; for (int i = 0; i < formals.length; i++) { - AnalysisState temp = prepared.bottom(); + AnalysisState temp = prepared.bottom(); for (SymbolicExpression exp : parameters[i]) temp = temp.lub(prepared.assign(formals[i].toSymbolicVariable(), exp, call)); prepared = temp; diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/ParameterAssigningStrategy.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/ParameterAssigningStrategy.java index 65629d9e4..079aff9eb 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/ParameterAssigningStrategy.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/ParameterAssigningStrategy.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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.Parameter; import it.unive.lisa.program.cfg.statement.call.Call; @@ -38,9 +35,6 @@ public interface ParameterAssigningStrategy { * by-name (Python-like). * * @param the type of {@link AbstractState} - * @param the type of the {@link HeapDomain} - * @param the type of the {@link ValueDomain} - * @param the type of {@link TypeDomain} * @param call the call to be prepared * @param callState the analysis state where the call is to be * executed @@ -59,15 +53,12 @@ public interface ParameterAssigningStrategy { * @throws SemanticException if something goes wrong while preparing the * entry-state */ - , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> Pair, ExpressionSet[]> prepare( - Call call, - AnalysisState callState, - InterproceduralAnalysis interprocedural, - StatementStore expressions, - Parameter[] formals, - ExpressionSet[] actuals) - throws SemanticException; + > Pair, ExpressionSet[]> prepare( + Call call, + AnalysisState callState, + InterproceduralAnalysis interprocedural, + StatementStore expressions, + Parameter[] formals, + ExpressionSet[] actuals) + throws SemanticException; } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/PythonLikeAssigningStrategy.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/PythonLikeAssigningStrategy.java index d0f44947f..567738c6a 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/PythonLikeAssigningStrategy.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/language/parameterassignment/PythonLikeAssigningStrategy.java @@ -1,18 +1,10 @@ package it.unive.lisa.program.language.parameterassignment; -import java.util.HashSet; -import java.util.Set; - -import org.apache.commons.lang3.tuple.Pair; - import it.unive.lisa.analysis.AbstractState; 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.interprocedural.InterproceduralAnalysis; import it.unive.lisa.program.cfg.Parameter; import it.unive.lisa.program.cfg.statement.Expression; @@ -21,6 +13,9 @@ import it.unive.lisa.program.language.resolution.PythonLikeMatchingStrategy; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.type.Type; +import java.util.HashSet; +import java.util.Set; +import org.apache.commons.lang3.tuple.Pair; /** * A Python-like assigning strategy. Specifically:
@@ -66,17 +61,14 @@ private PythonLikeAssigningStrategy() { @Override @SuppressWarnings("unchecked") - public , - H extends HeapDomain, - V extends ValueDomain, - T extends TypeDomain> Pair, ExpressionSet[]> prepare( - Call call, - AnalysisState callState, - InterproceduralAnalysis interprocedural, - StatementStore expressions, - Parameter[] formals, - ExpressionSet[] parameters) - throws SemanticException { + public > Pair, ExpressionSet[]> prepare( + Call call, + AnalysisState callState, + InterproceduralAnalysis interprocedural, + StatementStore expressions, + Parameter[] formals, + ExpressionSet[] parameters) + throws SemanticException { ExpressionSet[] slots = new ExpressionSet[formals.length]; Set[] slotsTypes = new Set[formals.length]; @@ -97,7 +89,7 @@ T extends TypeDomain> Pair, ExpressionSet logic = PythonLikeMatchingStrategy.pythonLogic( + AnalysisState logic = PythonLikeMatchingStrategy.pythonLogic( formals, actuals, parameters, @@ -111,9 +103,9 @@ T extends TypeDomain> Pair, ExpressionSet prepared = callState; + AnalysisState prepared = callState; for (int i = 0; i < formals.length; i++) { - AnalysisState temp = prepared.bottom(); + AnalysisState temp = prepared.bottom(); for (SymbolicExpression exp : slots[i]) temp = temp.lub(prepared.assign(formals[i].toSymbolicVariable(), exp, call)); prepared = temp; diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestAbstractState.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestAbstractState.java index 152e399bf..566738e7c 100644 --- a/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestAbstractState.java +++ b/lisa/lisa-sdk/src/test/java/it/unive/lisa/TestAbstractState.java @@ -1,8 +1,5 @@ package it.unive.lisa; -import java.util.Collections; -import java.util.Set; - import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.SemanticException; import it.unive.lisa.analysis.lattices.ExpressionSet; @@ -12,9 +9,11 @@ import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.type.Type; import it.unive.lisa.type.Untyped; +import java.util.Collections; +import java.util.Set; public class TestAbstractState extends TestDomain - implements AbstractState { + implements AbstractState { @Override public DomainRepresentation representation() { diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/analysis/AnalyzedCFGTest.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/analysis/AnalyzedCFGTest.java index fb1cd3d26..5e3980920 100644 --- a/lisa/lisa-sdk/src/test/java/it/unive/lisa/analysis/AnalyzedCFGTest.java +++ b/lisa/lisa-sdk/src/test/java/it/unive/lisa/analysis/AnalyzedCFGTest.java @@ -3,11 +3,8 @@ import static org.junit.Assert.assertEquals; import it.unive.lisa.TestAbstractState; -import it.unive.lisa.TestHeapDomain; import it.unive.lisa.TestLanguageFeatures; -import it.unive.lisa.TestTypeDomain; import it.unive.lisa.TestTypeSystem; -import it.unive.lisa.TestValueDomain; import it.unive.lisa.analysis.lattices.ExpressionSet; import it.unive.lisa.analysis.symbols.SymbolAliasing; import it.unive.lisa.interprocedural.UniqueScope; @@ -36,20 +33,14 @@ public void testIssue189() throws SemanticException { OpenCall y = new OpenCall(cfg, unknown, CallType.STATIC, "bar", "foo", x); cfg.addNode(y, true); - AnalysisState state = new AnalysisState<>( - new TestAbstractState(), - new ExpressionSet<>(), new SymbolAliasing()); + AnalysisState state = new AnalysisState<>( + new TestAbstractState(), + new ExpressionSet<>(), new SymbolAliasing()); - Map> entries = Map.of(y, state); - Map> results = Map.of(y, state, x, state); + Map> entries = Map.of(y, state); + Map> results = Map.of(y, state, x, state); - AnalyzedCFG res = new AnalyzedCFG<>(cfg, new UniqueScope(), state, entries, results); + AnalyzedCFG res = new AnalyzedCFG<>(cfg, new UniqueScope(), state, entries, results); assertEquals(state, res.getAnalysisStateAfter(y)); assertEquals(state, res.getAnalysisStateBefore(y)); diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/checks/semantic/CheckToolWithAnalysisResultsTest.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/checks/semantic/CheckToolWithAnalysisResultsTest.java index 5fe2842f2..932888a56 100644 --- a/lisa/lisa-sdk/src/test/java/it/unive/lisa/checks/semantic/CheckToolWithAnalysisResultsTest.java +++ b/lisa/lisa-sdk/src/test/java/it/unive/lisa/checks/semantic/CheckToolWithAnalysisResultsTest.java @@ -4,11 +4,8 @@ import static org.junit.Assert.assertTrue; import it.unive.lisa.TestAbstractState; -import it.unive.lisa.TestHeapDomain; import it.unive.lisa.TestLanguageFeatures; -import it.unive.lisa.TestTypeDomain; import it.unive.lisa.TestTypeSystem; -import it.unive.lisa.TestValueDomain; import it.unive.lisa.analysis.AnalysisState; import it.unive.lisa.analysis.AnalyzedCFG; import it.unive.lisa.analysis.lattices.ExpressionSet; @@ -138,9 +135,8 @@ private static Warning build(CheckTool tool, Object target, String message) { @Test public void testCopy() { - CheckToolWithAnalysisResults tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), + CheckToolWithAnalysisResults< + TestAbstractState> tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), new FileManager("foo"), Map.of(), fakeCallGraph); Collection exp = new HashSet<>(); @@ -169,9 +165,8 @@ public void testCopy() { @Test public void testSimpleFill() { - CheckToolWithAnalysisResults tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), + CheckToolWithAnalysisResults< + TestAbstractState> tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), new FileManager("foo"), Map.of(), fakeCallGraph); Collection exp = new HashSet<>(); @@ -187,9 +182,8 @@ public void testSimpleFill() { @Test public void testDisjointWarnings() { - CheckToolWithAnalysisResults tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), + CheckToolWithAnalysisResults< + TestAbstractState> tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), new FileManager("foo"), Map.of(), fakeCallGraph); Collection exp = new HashSet<>(); @@ -203,9 +197,8 @@ public void testDisjointWarnings() { @Test public void testDuplicateWarnings() { - CheckToolWithAnalysisResults tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), + CheckToolWithAnalysisResults< + TestAbstractState> tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), new FileManager("foo"), Map.of(), fakeCallGraph); Collection exp = new HashSet<>(); @@ -222,25 +215,19 @@ public void testDuplicateWarnings() { @Test public void testResultRetrieval() { - AnalysisState singleton = new AnalysisState<>( - new TestAbstractState(), - new ExpressionSet<>(), new SymbolAliasing()); + AnalysisState singleton = new AnalysisState<>( + new TestAbstractState(), + new ExpressionSet<>(), new SymbolAliasing()); NoOp noop = new NoOp(cfg, new SourceCodeLocation("fake", 3, 0)); - AnalyzedCFG res1 = new AnalyzedCFG<>(cfg, new UniqueScope(), singleton, - Map.of(noop, singleton.bottom()), Map.of(noop, singleton.bottom())); + AnalyzedCFG res1 = new AnalyzedCFG<>(cfg, new UniqueScope(), singleton, + Map.of(noop, singleton.bottom()), Map.of(noop, singleton.bottom())); noop = new NoOp(cfg2, new SourceCodeLocation("fake", 30, 0)); - AnalyzedCFG res2 = new AnalyzedCFG<>(cfg2, new UniqueScope(), singleton, - Map.of(noop, singleton.bottom()), Map.of(noop, singleton.bottom())); - - CheckToolWithAnalysisResults tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), + AnalyzedCFG res2 = new AnalyzedCFG<>(cfg2, new UniqueScope(), singleton, + Map.of(noop, singleton.bottom()), Map.of(noop, singleton.bottom())); + + CheckToolWithAnalysisResults< + TestAbstractState> tool = new CheckToolWithAnalysisResults<>(new LiSAConfiguration(), new FileManager("foo"), Map.of(cfg, Collections.singleton(res1), cfg2, Collections.singleton(res2)), fakeCallGraph); diff --git a/lisa/lisa-sdk/src/test/java/it/unive/lisa/program/cfg/fixpoints/OptimizedFixpointTest.java b/lisa/lisa-sdk/src/test/java/it/unive/lisa/program/cfg/fixpoints/OptimizedFixpointTest.java index 7136bf43e..bceecbc57 100644 --- a/lisa/lisa-sdk/src/test/java/it/unive/lisa/program/cfg/fixpoints/OptimizedFixpointTest.java +++ b/lisa/lisa-sdk/src/test/java/it/unive/lisa/program/cfg/fixpoints/OptimizedFixpointTest.java @@ -5,11 +5,8 @@ import static org.junit.Assert.fail; import it.unive.lisa.TestAbstractState; -import it.unive.lisa.TestHeapDomain; import it.unive.lisa.TestLanguageFeatures; -import it.unive.lisa.TestTypeDomain; import it.unive.lisa.TestTypeSystem; -import it.unive.lisa.TestValueDomain; import it.unive.lisa.analysis.AnalysisState; import it.unive.lisa.analysis.StatementStore; import it.unive.lisa.analysis.lattices.ExpressionSet; @@ -40,44 +37,44 @@ public class OptimizedFixpointTest { private static class FixpointTester2 implements FixpointImplementation> { + CompoundState> { @Override - public CompoundState semantics( + public CompoundState semantics( Statement node, - CompoundState entrystate) + CompoundState entrystate) throws Exception { return entrystate; } @Override - public CompoundState traverse(Edge edge, - CompoundState entrystate) + public CompoundState traverse(Edge edge, + CompoundState entrystate) throws Exception { return entrystate; } @Override - public CompoundState union(Statement node, - CompoundState left, - CompoundState right) + public CompoundState union(Statement node, + CompoundState left, + CompoundState right) throws Exception { return left.lub(right); } @Override - public CompoundState operation( + public CompoundState operation( Statement node, - CompoundState approx, - CompoundState old) + CompoundState approx, + CompoundState old) throws Exception { return old.lub(approx); } @Override public boolean equality(Statement node, - CompoundState approx, - CompoundState old) + CompoundState approx, + CompoundState old) throws Exception { return approx.lessOrEqual(old); } @@ -101,16 +98,14 @@ public void testLinearGraph() { graph.computeBasicBlocks(); Map> res = null; - AnalysisState state = new AnalysisState<>( - new TestAbstractState(), - new ExpressionSet<>(), - new SymbolAliasing()); - CompoundState comp = CompoundState.of(state.bottom(), new StatementStore<>(state.bottom())); + CompoundState> res = null; + AnalysisState state = new AnalysisState<>( + new TestAbstractState(), + new ExpressionSet<>(), + new SymbolAliasing()); + CompoundState comp = CompoundState.of(state.bottom(), new StatementStore<>(state.bottom())); try { - res = new OptimizedFixpoint(graph, + res = new OptimizedFixpoint(graph, false, st -> st instanceof Call).fixpoint( Map.of(source, comp), FIFOWorkingSet.mk(), @@ -152,16 +147,14 @@ public void testBranchingGraph() { graph.computeBasicBlocks(); Map> res = null; - AnalysisState state = new AnalysisState<>( - new TestAbstractState(), - new ExpressionSet<>(), - new SymbolAliasing()); - CompoundState comp = CompoundState.of(state.bottom(), new StatementStore<>(state.bottom())); + CompoundState> res = null; + AnalysisState state = new AnalysisState<>( + new TestAbstractState(), + new ExpressionSet<>(), + new SymbolAliasing()); + CompoundState comp = CompoundState.of(state.bottom(), new StatementStore<>(state.bottom())); try { - res = new OptimizedFixpoint(graph, + res = new OptimizedFixpoint(graph, false, st -> st instanceof Call).fixpoint( Map.of(source, comp), FIFOWorkingSet.mk(), @@ -203,16 +196,14 @@ public void testCyclicGraph() { graph.computeBasicBlocks(); Map> res = null; - AnalysisState state = new AnalysisState<>( - new TestAbstractState(), - new ExpressionSet<>(), - new SymbolAliasing()); - CompoundState comp = CompoundState.of(state.bottom(), new StatementStore<>(state.bottom())); + CompoundState> res = null; + AnalysisState state = new AnalysisState<>( + new TestAbstractState(), + new ExpressionSet<>(), + new SymbolAliasing()); + CompoundState comp = CompoundState.of(state.bottom(), new StatementStore<>(state.bottom())); try { - res = new OptimizedFixpoint(graph, + res = new OptimizedFixpoint(graph, false, st -> st instanceof Call).fixpoint( Map.of(source, comp), FIFOWorkingSet.mk(),