-
Notifications
You must be signed in to change notification settings - Fork 32
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Removing non-essential type parameters from AnalysisState
- Loading branch information
Showing
112 changed files
with
1,127 additions
and
1,981 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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.<br> | ||
| * <br> | ||
| * The interaction between heap and value/type domains follows the one defined | ||
| * <a href= | ||
| * "https://www.sciencedirect.com/science/article/pii/S0304397516300299">in this | ||
| * paper</a>. | ||
| * | ||
| * @author <a href="mailto:[email protected]">Luca Negrini</a> | ||
| * | ||
|
|
@@ -42,7 +47,8 @@ | |
| public class SimpleAbstractState<H extends HeapDomain<H>, | ||
| V extends ValueDomain<V>, | ||
| T extends TypeDomain<T>> | ||
| implements BaseLattice<SimpleAbstractState<H, V, T>>, AbstractState<SimpleAbstractState<H, V, T>, H, V, T> { | ||
| implements BaseLattice<SimpleAbstractState<H, V, T>>, | ||
| AbstractState<SimpleAbstractState<H, V, T>> { | ||
|
|
||
| /** | ||
| * 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; | ||
| } | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 <a href="mailto:[email protected]">Luca Negrini</a> | ||
| * | ||
| * @param <A> the type of {@link AbstractState} that this is being partitioned | ||
| * @param <H> the type of {@link HeapDomain} embedded in the abstract states | ||
| * @param <V> the type of {@link ValueDomain} embedded in the abstract states | ||
| * @param <T> the type of {@link TypeDomain} embedded in the abstract states | ||
| * | ||
| * @see <a href= | ||
| * "https://doi.org/10.1145/1275497.1275501">https://doi.org/10.1145/1275497.1275501</a> | ||
| */ | ||
| public class TracePartitioning<A extends AbstractState<A, H, V, T>, | ||
| H extends HeapDomain<H>, | ||
| V extends ValueDomain<V>, | ||
| T extends TypeDomain<T>> | ||
| extends FunctionalLattice<TracePartitioning<A, H, V, T>, ExecutionTrace, A> | ||
| implements AbstractState<TracePartitioning<A, H, V, T>, H, V, T> { | ||
| public class TracePartitioning<A extends AbstractState<A>> | ||
| extends FunctionalLattice<TracePartitioning<A>, ExecutionTrace, A> | ||
| implements AbstractState<TracePartitioning<A>> { | ||
|
|
||
| /** | ||
| * The maximum number of {@link LoopIteration} tokens that a trace can | ||
|
|
@@ -109,17 +99,17 @@ else if (isBottom() || function == null) | |
| } | ||
|
|
||
| @Override | ||
| public TracePartitioning<A, H, V, T> top() { | ||
| public TracePartitioning<A> top() { | ||
| return new TracePartitioning<>(lattice.top(), null); | ||
| } | ||
|
|
||
| @Override | ||
| public TracePartitioning<A, H, V, T> bottom() { | ||
| public TracePartitioning<A> bottom() { | ||
| return new TracePartitioning<>(lattice.bottom(), null); | ||
| } | ||
|
|
||
| @Override | ||
| public TracePartitioning<A, H, V, T> assign(Identifier id, SymbolicExpression expression, ProgramPoint pp) | ||
| public TracePartitioning<A> assign(Identifier id, SymbolicExpression expression, ProgramPoint pp) | ||
| throws SemanticException { | ||
| if (isBottom()) | ||
| return this; | ||
|
|
@@ -134,7 +124,7 @@ public TracePartitioning<A, H, V, T> assign(Identifier id, SymbolicExpression ex | |
| } | ||
|
|
||
| @Override | ||
| public TracePartitioning<A, H, V, T> smallStepSemantics(SymbolicExpression expression, ProgramPoint pp) | ||
| public TracePartitioning<A> smallStepSemantics(SymbolicExpression expression, ProgramPoint pp) | ||
| throws SemanticException { | ||
| if (isBottom()) | ||
| return this; | ||
|
|
@@ -149,7 +139,7 @@ public TracePartitioning<A, H, V, T> smallStepSemantics(SymbolicExpression expre | |
| } | ||
|
|
||
| @Override | ||
| public TracePartitioning<A, H, V, T> assume(SymbolicExpression expression, ProgramPoint src, ProgramPoint dest) | ||
| public TracePartitioning<A> 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<A, H, V, T> forgetIdentifier(Identifier id) throws SemanticException { | ||
| public TracePartitioning<A> forgetIdentifier(Identifier id) throws SemanticException { | ||
| if (isTop() || isBottom() || function == null) | ||
| return this; | ||
|
|
||
|
|
@@ -222,7 +212,7 @@ public TracePartitioning<A, H, V, T> forgetIdentifier(Identifier id) throws Sema | |
| } | ||
|
|
||
| @Override | ||
| public TracePartitioning<A, H, V, T> forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException { | ||
| public TracePartitioning<A> forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException { | ||
| if (isTop() || isBottom() || function == null) | ||
| return this; | ||
|
|
||
|
|
@@ -251,7 +241,7 @@ public Satisfiability satisfies(SymbolicExpression expression, ProgramPoint pp) | |
| } | ||
|
|
||
| @Override | ||
| public TracePartitioning<A, H, V, T> pushScope(ScopeToken token) throws SemanticException { | ||
| public TracePartitioning<A> pushScope(ScopeToken token) throws SemanticException { | ||
| if (isTop() || isBottom() || function == null) | ||
| return this; | ||
|
|
||
|
|
@@ -262,7 +252,7 @@ public TracePartitioning<A, H, V, T> pushScope(ScopeToken token) throws Semantic | |
| } | ||
|
|
||
| @Override | ||
| public TracePartitioning<A, H, V, T> popScope(ScopeToken token) throws SemanticException { | ||
| public TracePartitioning<A> popScope(ScopeToken token) throws SemanticException { | ||
| if (isTop() || isBottom() || function == null) | ||
| return this; | ||
|
|
||
|
|
@@ -287,7 +277,7 @@ public DomainRepresentation representation() { | |
| } | ||
|
|
||
| @Override | ||
| public TracePartitioning<A, H, V, T> mk(A lattice, Map<ExecutionTrace, A> function) { | ||
| public TracePartitioning<A> mk(A lattice, Map<ExecutionTrace, A> function) { | ||
| return new TracePartitioning<>(lattice, function); | ||
| } | ||
|
|
||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.