From 49eda2e16e39a5cd5a56714819ad87d85666fdda Mon Sep 17 00:00:00 2001 From: Luca Negrini Date: Thu, 28 Sep 2023 12:54:36 +0200 Subject: [PATCH] Supporting recursions #291 --- .../lisa/analysis/SimpleAbstractState.java | 15 +++ .../analysis/traces/TracePartitioning.java | 33 +++++ .../context/recursion/BaseCasesFinder.java | 8 +- .../it/unive/lisa/analysis/AbstractState.java | 32 ++++- .../it/unive/lisa/analysis/AnalysisState.java | 118 ++++++++++++++---- .../interprocedural/callgraph/CallGraph.java | 10 +- .../java/it/unive/lisa/TestAbstractState.java | 31 +++++ 7 files changed, 218 insertions(+), 29 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 22c929f6f..866d8f457 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 @@ -593,6 +593,21 @@ public boolean knowsIdentifier( return heapState.knowsIdentifier(id) || valueState.knowsIdentifier(id) || typeState.knowsIdentifier(id); } + @Override + public SimpleAbstractState withTopMemory() { + return new SimpleAbstractState<>(heapState.top(), valueState, typeState); + } + + @Override + public SimpleAbstractState withTopValues() { + return new SimpleAbstractState<>(heapState, valueState.top(), typeState); + } + + @Override + public SimpleAbstractState withTopTypes() { + return new SimpleAbstractState<>(heapState, valueState, typeState.top()); + } + private static class MutableOracle, V extends ValueDomain, T extends TypeDomain> implements SemanticOracle { 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 78e76e989..8fa813beb 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 @@ -411,4 +411,37 @@ public boolean knowsIdentifier(Identifier id) { return true; return false; } + + @Override + public TracePartitioning withTopMemory() { + if (isTop() || isBottom() || function == null) + return this; + + Map result = mkNewFunction(null, false); + for (Entry trace : this) + result.put(trace.getKey(), trace.getValue().withTopMemory()); + return new TracePartitioning<>(lattice, result); + } + + @Override + public TracePartitioning withTopValues() { + if (isTop() || isBottom() || function == null) + return this; + + Map result = mkNewFunction(null, false); + for (Entry trace : this) + result.put(trace.getKey(), trace.getValue().withTopValues()); + return new TracePartitioning<>(lattice, result); + } + + @Override + public TracePartitioning withTopTypes() { + if (isTop() || isBottom() || function == null) + return this; + + Map result = mkNewFunction(null, false); + for (Entry trace : this) + result.put(trace.getKey(), trace.getValue().withTopTypes()); + return new TracePartitioning<>(lattice, result); + } } 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 09054ae2c..029e1035d 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 @@ -97,7 +97,8 @@ public AnalysisState getAbstractResultOf( } @Override - protected boolean canShortcut(CFG cfg) { + protected boolean canShortcut( + CFG cfg) { // we want to compute the recursive chain with no shortcuts return !recursion.getMembers().contains(cfg); } @@ -130,6 +131,9 @@ public AnalysisState find() throws SemanticException { ExpressionSet[] params = new ExpressionSet[actuals.length]; for (int i = 0; i < params.length; i++) params[i] = entryState.intermediateStates.getState(actuals[i]).getComputedExpressions(); - return start.expressionSemantics(this, entryState.postState.top(), params, entryState.intermediateStates); + // it should be enough to send values to top, retaining all type + // information + return start.expressionSemantics(this, entryState.postState.withTopValues(), params, + entryState.intermediateStates); } } 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 cacb2090c..3a399897d 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 @@ -14,5 +14,35 @@ * @param the concrete type of the {@link AbstractState} */ public interface AbstractState> - extends SemanticOracle, Lattice, SemanticDomain { + extends + SemanticOracle, + Lattice, + SemanticDomain { + + /** + * Yields a copy of this state, but with its memory abstraction set to top. + * This is useful to represent effects of unknown calls that arbitrarily + * manipulate the memory. + * + * @return the copy with top memory + */ + A withTopMemory(); + + /** + * Yields a copy of this state, but with its value abstraction set to top. + * This is useful to represent effects of unknown calls that arbitrarily + * manipulate the values of variables. + * + * @return the copy with top values + */ + A withTopValues(); + + /** + * Yields a copy of this state, but with its type abstraction set to top. + * This is useful to represent effects of unknown calls that arbitrarily + * manipulate the values of variables (and their type accordingly). + * + * @return the copy with top types + */ + A withTopTypes(); } 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 3a70754e8..e40e706bc 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 @@ -26,7 +26,8 @@ * @param the type of {@link AbstractState} embedded in this state */ public class AnalysisState> - implements BaseLattice>, + implements + BaseLattice>, StructuredObject, ScopedObject> { @@ -53,7 +54,9 @@ public class AnalysisState> * analysis state * @param computedExpression the expression that has been computed */ - public AnalysisState(A state, SymbolicExpression computedExpression) { + public AnalysisState( + A state, + SymbolicExpression computedExpression) { this(state, new ExpressionSet(computedExpression), null); } @@ -64,7 +67,9 @@ public AnalysisState(A state, SymbolicExpression computedExpression) { * analysis state * @param computedExpressions the expressions that have been computed */ - public AnalysisState(A state, ExpressionSet computedExpressions) { + public AnalysisState( + A state, + ExpressionSet computedExpressions) { this(state, computedExpressions, null); } @@ -77,7 +82,10 @@ public AnalysisState(A state, ExpressionSet computedExpressions) { * @param info the additional information to be computed * during fixpoint computations */ - public AnalysisState(A state, SymbolicExpression computedExpression, FixpointInfo info) { + public AnalysisState( + A state, + SymbolicExpression computedExpression, + FixpointInfo info) { this(state, new ExpressionSet(computedExpression), info); } @@ -90,7 +98,10 @@ public AnalysisState(A state, SymbolicExpression computedExpression, FixpointInf * @param info the additional information to be computed * during fixpoint computations */ - public AnalysisState(A state, ExpressionSet computedExpressions, FixpointInfo info) { + public AnalysisState( + A state, + ExpressionSet computedExpressions, + FixpointInfo info) { this.state = state; this.computedExpressions = computedExpressions; this.info = info; @@ -125,7 +136,8 @@ public FixpointInfo getFixpointInformation() { * * @return the mapped information */ - public Lattice getInfo(String key) { + public Lattice getInfo( + String key) { return info == null ? null : info.get(key); } @@ -140,7 +152,9 @@ public Lattice getInfo(String key) { * * @return the mapped information */ - public T getInfo(String key, Class type) { + public T getInfo( + String key, + Class type) { return info == null ? null : info.get(key, type); } @@ -156,7 +170,9 @@ public T getInfo(String key, Class type) { * * @return a new instance with the updated mapping */ - public AnalysisState storeInfo(String key, Lattice info) { + public AnalysisState storeInfo( + String key, + Lattice info) { FixpointInfo fixinfo = this.info == null ? new FixpointInfo() : this.info; fixinfo = fixinfo.put(key, info); return new AnalysisState<>(state, computedExpressions, fixinfo); @@ -177,7 +193,10 @@ public AnalysisState storeInfo(String key, Lattice info) { * * @throws SemanticException if something goes wrong during the lub */ - public AnalysisState weakStoreInfo(String key, Lattice info) throws SemanticException { + public AnalysisState weakStoreInfo( + String key, + Lattice info) + throws SemanticException { FixpointInfo fixinfo = this.info == null ? new FixpointInfo() : this.info; fixinfo = fixinfo.putWeak(key, info); return new AnalysisState<>(state, computedExpressions, fixinfo); @@ -330,7 +349,9 @@ public SemanticDomain.Satisfiability satisfies( } @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), @@ -339,7 +360,9 @@ public AnalysisState pushScope(ScopeToken scope) throws SemanticException { private static ExpressionSet onAllExpressions( ExpressionSet computedExpressions, - ScopeToken scope, boolean push) throws SemanticException { + ScopeToken scope, + boolean push) + throws SemanticException { Set result = new HashSet<>(); for (SymbolicExpression exp : computedExpressions) result.add(push ? exp.pushScope(scope) : exp.popScope(scope)); @@ -347,7 +370,9 @@ 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), @@ -355,7 +380,9 @@ public AnalysisState popScope(ScopeToken scope) throws SemanticException { } @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), @@ -363,7 +390,9 @@ public AnalysisState lubAux(AnalysisState other) throws SemanticException } @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), @@ -371,7 +400,9 @@ public AnalysisState glbAux(AnalysisState other) throws SemanticException } @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), @@ -379,7 +410,9 @@ public AnalysisState wideningAux(AnalysisState other) throws SemanticExcep } @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), @@ -387,7 +420,9 @@ public AnalysisState narrowingAux(AnalysisState other) throws SemanticExce } @Override - public boolean lessOrEqualAux(AnalysisState other) throws SemanticException { + public boolean lessOrEqualAux( + AnalysisState other) + throws SemanticException { return state.lessOrEqual(other.state) && computedExpressions.lessOrEqual(other.computedExpressions) && (info == null ? true : info.lessOrEqual(other.info)); @@ -424,7 +459,9 @@ public boolean isBottom() { * * @throws SemanticException if an error occurs during the computation */ - public AnalysisState forgetIdentifier(Identifier id) throws SemanticException { + public AnalysisState forgetIdentifier( + Identifier id) + throws SemanticException { return new AnalysisState<>(state.forgetIdentifier(id), computedExpressions, info); } @@ -439,7 +476,9 @@ public AnalysisState forgetIdentifier(Identifier id) throws SemanticException * * @throws SemanticException if an error occurs during the computation */ - public AnalysisState forgetIdentifiersIf(Predicate test) throws SemanticException { + public AnalysisState forgetIdentifiersIf( + Predicate test) + throws SemanticException { return new AnalysisState<>(state.forgetIdentifiersIf(test), computedExpressions, info); } @@ -453,7 +492,9 @@ public AnalysisState forgetIdentifiersIf(Predicate test) throws S * * @throws SemanticException if an error occurs during the computation */ - public AnalysisState forgetIdentifiers(Iterable ids) throws SemanticException { + public AnalysisState forgetIdentifiers( + Iterable ids) + throws SemanticException { AnalysisState result = this; for (Identifier id : ids) result = result.forgetIdentifier(id); @@ -471,7 +512,8 @@ public int hashCode() { } @Override - public boolean equals(Object obj) { + public boolean equals( + Object obj) { if (this == obj) return true; if (obj == null) @@ -533,4 +575,38 @@ public StructuredRepresentation representationWithInfo() { public String toString() { return representation().toString(); } + + /** + * Yields a copy of this state, but with the {@link AbstractState}'s inner + * memory abstraction set to top. This is useful to represent effects of + * unknown calls that arbitrarily manipulate the memory. + * + * @return the copy with top memory + */ + public AnalysisState withTopMemory() { + return new AnalysisState<>(state.withTopMemory(), computedExpressions, info); + } + + /** + * Yields a copy of this state, but with the {@link AbstractState}'s inner + * value abstraction set to top. This is useful to represent effects of + * unknown calls that arbitrarily manipulate the values of variables. + * + * @return the copy with top value + */ + public AnalysisState withTopValues() { + return new AnalysisState<>(state.withTopValues(), computedExpressions, info); + } + + /** + * Yields a copy of this state, but with the {@link AbstractState}'s inner + * type abstraction set to top. This is useful to represent effects of + * unknown calls that arbitrarily manipulate the values of variables (and + * their type accordingly). + * + * @return the copy with top type + */ + public AnalysisState withTopTypes() { + return new AnalysisState<>(state.withTopTypes(), computedExpressions, info); + } } diff --git a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/callgraph/CallGraph.java b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/callgraph/CallGraph.java index 46ae2cb3d..060bf12b0 100644 --- a/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/callgraph/CallGraph.java +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/callgraph/CallGraph.java @@ -82,7 +82,7 @@ public abstract Call resolve(UnresolvedCall call, Set[] types, SymbolAlias * * @return the collection of calls that target the code members */ - public Collection getCallSites(Collection cms) { + public Collection getCallSites(Collection cms) { Set result = new HashSet<>(); cms.forEach(cm -> getCallSites(cm).stream().forEach(result::add)); return result; @@ -97,7 +97,7 @@ public Collection getCallSites(Collection cms) { * * @return the collection of callers code members */ - public Collection getCallers(Collection cms) { + public Collection getCallers(Collection cms) { Set result = new HashSet<>(); cms.forEach(cm -> getCallers(cm).stream().forEach(result::add)); return result; @@ -129,7 +129,7 @@ public Collection getCallersTransitively(CodeMember cm) { * * @return the collection of callers code members computed transitively */ - public Collection getCallersTransitively(Collection cms) { + public Collection getCallersTransitively(Collection cms) { VisitOnceWorkingSet ws = VisitOnceFIFOWorkingSet.mk(); cms.forEach(cm -> getCallers(cm).stream().forEach(ws::push)); while (!ws.isEmpty()) @@ -146,7 +146,7 @@ public Collection getCallersTransitively(Collection cms) * * @return the collection of callees code members */ - public Collection getCallees(Collection cms) { + public Collection getCallees(Collection cms) { Set result = new HashSet<>(); cms.forEach(cm -> getCallees(cm).stream().forEach(result::add)); return result; @@ -178,7 +178,7 @@ public Collection getCalleesTransitively(CodeMember cm) { * * @return the collection of callees code members computed transitively */ - public Collection getCalleesTransitively(Collection cms) { + public Collection getCalleesTransitively(Collection cms) { VisitOnceWorkingSet ws = VisitOnceFIFOWorkingSet.mk(); cms.forEach(cm -> getCallees(cm).stream().forEach(ws::push)); while (!ws.isEmpty()) 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 978fe5616..edc26b9a6 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 @@ -58,4 +58,35 @@ public Type getDynamicTypeOf( throws SemanticException { return Untyped.INSTANCE; } + + @Override + public boolean lessOrEqual( + TestAbstractState other) + throws SemanticException { + // TODO Auto-generated method stub + return false; + } + + @Override + public TestAbstractState lub( + TestAbstractState other) + throws SemanticException { + // TODO Auto-generated method stub + return null; + } + + @Override + public TestAbstractState withTopMemory() { + return this; + } + + @Override + public TestAbstractState withTopValues() { + return this; + } + + @Override + public TestAbstractState withTopTypes() { + return this; + } }