From 4690827047b2404080b90ff1b995e7bc3f773c67 Mon Sep 17 00:00:00 2001 From: lucaneg Date: Wed, 12 Jan 2022 11:33:38 +0100 Subject: [PATCH 1/4] #151 adding OpenCallPolicy to control how open calls are treated --- .../java/it/unive/lisa/LiSAConfiguration.java | 40 +++++- .../main/java/it/unive/lisa/LiSARunner.java | 9 +- .../CallGraphBasedAnalysis.java | 16 ++- .../interprocedural/ContextBasedAnalysis.java | 23 ++-- .../ModularWorstCaseAnalysis.java | 28 +++-- .../lisa/program/cfg/CFGFixpointTest.java | 3 +- .../lisa/program/cfg/SemanticsSanityTest.java | 3 +- .../InterproceduralAnalysis.java | 37 +++++- .../lisa/interprocedural/OpenCallPolicy.java | 52 ++++++++ .../lisa/interprocedural/WorstCasePolicy.java | 48 ++++++++ .../program/cfg/statement/call/CFGCall.java | 79 +++--------- .../cfg/statement/call/CallWithResult.java | 115 ++++++++++++++++++ .../program/cfg/statement/call/OpenCall.java | 27 ++-- 13 files changed, 371 insertions(+), 109 deletions(-) create mode 100644 lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/OpenCallPolicy.java create mode 100644 lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/WorstCasePolicy.java create mode 100644 lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CallWithResult.java diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java b/lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java index e44e5727b..0a7ca053c 100644 --- a/lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java +++ b/lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java @@ -6,9 +6,12 @@ import it.unive.lisa.checks.syntactic.SyntacticCheck; import it.unive.lisa.checks.warnings.Warning; import it.unive.lisa.interprocedural.InterproceduralAnalysis; +import it.unive.lisa.interprocedural.OpenCallPolicy; +import it.unive.lisa.interprocedural.WorstCasePolicy; import it.unive.lisa.interprocedural.callgraph.CallGraph; import it.unive.lisa.program.cfg.CFG; import it.unive.lisa.program.cfg.statement.Statement; +import it.unive.lisa.program.cfg.statement.call.OpenCall; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.type.Type; import it.unive.lisa.util.collections.externalSet.ExternalSet; @@ -120,6 +123,12 @@ public class LiSAConfiguration { */ private Class fixpointWorkingSet; + /** + * The {@link OpenCallPolicy} to be used for computing the result of + * {@link OpenCall}s. + */ + private OpenCallPolicy openCallPolicy; + /** * Builds a new configuration object, with default settings. By default: * */ public LiSAConfiguration() { @@ -143,6 +153,7 @@ public LiSAConfiguration() { this.workdir = Paths.get(".").toAbsolutePath().normalize().toString(); this.wideningThreshold = DEFAULT_WIDENING_THRESHOLD; this.fixpointWorkingSet = FIFOWorkingSet.class; + this.openCallPolicy = WorstCasePolicy.INSTANCE; } /** @@ -400,6 +411,18 @@ public LiSAConfiguration setWideningThreshold(int wideningThreshold) { return this; } + /** + * Sets the {@link OpenCallPolicy} to use during the analysis. + * + * @param openCallPolicy the policy to use + * + * @return the current (modified) configuration + */ + public LiSAConfiguration setOpenCallPolicy(OpenCallPolicy openCallPolicy) { + this.openCallPolicy = openCallPolicy; + return this; + } + /** * Yields the {@link CallGraph} for the analysis. Might be {@code null} if * none was set. @@ -553,6 +576,15 @@ public int getWideningThreshold() { return wideningThreshold; } + /** + * Yields the {@link OpenCallPolicy} to use during the analysis. + * + * @return the policy + */ + public OpenCallPolicy getOpenCallPolicy() { + return openCallPolicy; + } + @Override public int hashCode() { final int prime = 31; @@ -572,6 +604,7 @@ public int hashCode() { result = prime * result + ((syntacticChecks == null) ? 0 : syntacticChecks.hashCode()); result = prime * result + wideningThreshold; result = prime * result + ((workdir == null) ? 0 : workdir.hashCode()); + result = prime * result + ((openCallPolicy == null) ? 0 : openCallPolicy.hashCode()); return result; } @@ -641,6 +674,11 @@ public boolean equals(Object obj) { return false; } else if (!workdir.equals(other.workdir)) return false; + if (openCallPolicy == null) { + if (other.openCallPolicy != null) + return false; + } else if (!openCallPolicy.equals(other.openCallPolicy)) + return false; return true; } @@ -664,7 +702,7 @@ public String toString() { .append(syntacticChecks.size()) .append(" syntactic checks to execute") .append((syntacticChecks.isEmpty() ? "" : ":")); - + // TODO automatic way to keep this updated? for (SyntacticCheck check : syntacticChecks) res.append("\n ") .append(check.getClass().getSimpleName()); diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/LiSARunner.java b/lisa/lisa-core/src/main/java/it/unive/lisa/LiSARunner.java index f525aefea..2b302f478 100644 --- a/lisa/lisa-core/src/main/java/it/unive/lisa/LiSARunner.java +++ b/lisa/lisa-core/src/main/java/it/unive/lisa/LiSARunner.java @@ -16,6 +16,7 @@ import it.unive.lisa.checks.warnings.Warning; import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.interprocedural.InterproceduralAnalysisException; +import it.unive.lisa.interprocedural.OpenCallPolicy; import it.unive.lisa.interprocedural.callgraph.CallGraph; import it.unive.lisa.interprocedural.callgraph.CallGraphConstructionException; import it.unive.lisa.logging.IterationLogger; @@ -135,7 +136,7 @@ Collection run(Program program, FileManager fileManager) { } try { - interproc.init(program, callGraph); + interproc.init(program, callGraph, conf.getOpenCallPolicy()); } catch (InterproceduralAnalysisException e) { LOG.fatal("Exception while building the interprocedural analysis for the input program", e); throw new AnalysisExecutionException( @@ -143,7 +144,7 @@ Collection run(Program program, FileManager fileManager) { } if (conf.isInferTypes()) - inferTypes(fileManager, program, allCFGs); + inferTypes(fileManager, program, allCFGs, conf.getOpenCallPolicy()); else LOG.warn("Type inference disabled: dynamic type information will not be available for following analysis"); @@ -191,7 +192,7 @@ private void analyze(Collection allCFGs, FileManager fileManager) { } @SuppressWarnings("unchecked") - private void inferTypes(FileManager fileManager, Program program, Collection allCFGs) { + private void inferTypes(FileManager fileManager, Program program, Collection allCFGs, OpenCallPolicy policy) { T typesState = this.typeState.top(); InterproceduralAnalysis typesInterproc; CallGraph typesCg; @@ -199,7 +200,7 @@ private void inferTypes(FileManager fileManager, Program program, Collection, */ protected Program program; + /** + * The policy to evaluate results of open calls. + */ + protected OpenCallPolicy policy; + @Override - public void init(Program program, CallGraph callgraph) throws InterproceduralAnalysisException { + public void init(Program program, CallGraph callgraph, OpenCallPolicy policy) + throws InterproceduralAnalysisException { this.callgraph = callgraph; this.program = program; } @@ -75,4 +83,10 @@ protected AnalysisState prepareEntryStateOfEntryPoint(AnalysisState(prepared.getState(), new ExpressionSet<>()); } + + @Override + public AnalysisState getAbstractResultOf(OpenCall call, AnalysisState entryState, + ExpressionSet[] parameters) throws SemanticException { + return policy.apply(call, entryState, parameters); + } } diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java b/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java index 046fb3f7e..c823d35af 100644 --- a/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java +++ b/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java @@ -1,5 +1,15 @@ package it.unive.lisa.interprocedural; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.Map; +import java.util.Optional; + +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.analysis.AbstractState; @@ -24,14 +34,6 @@ import it.unive.lisa.util.collections.workset.VisitOnceWorkingSet; import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; -import java.util.Collection; -import java.util.Collections; -import java.util.HashSet; -import java.util.Map; -import java.util.Optional; -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 @@ -148,7 +150,7 @@ private void fixpointAux(AnalysisState entryState, iter++; } while (!fixpointTriggers.isEmpty()); } - + @Override public Collection> getAnalysisResultsOf(CFG cfg) { if (results.contains(cfg)) @@ -228,7 +230,7 @@ public AnalysisState getAbstractResultOf(CFGCall call, AnalysisState computeFixpoint(CFG cfg, ContextSensitivityToken localToken, AnalysisState computedEntryState) throws FixpointException, SemanticException, AnalysisSetupException { @@ -240,5 +242,4 @@ private CFGWithAnalysisResults computeFixpoint(CFG cfg, ContextSensitiv fixpointTriggers.add(cfg); return res.getRight(); } - } diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java b/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java index d1ae387a3..2f566624c 100644 --- a/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java +++ b/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java @@ -36,7 +36,7 @@ import org.apache.logging.log4j.Logger; /** - * A worst case modular analysis were all method calls return top. + * 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 @@ -53,6 +53,11 @@ public class ModularWorstCaseAnalysis, */ private Program program; + /** + * The policy used for computing the result of cfg calls. + */ + private OpenCallPolicy policy; + /** * The cash of the fixpoints' results. {@link Map#keySet()} will contain all * the cfgs that have been added. If a key's values's @@ -62,7 +67,7 @@ public class ModularWorstCaseAnalysis, private final Map>> results; /** - * Builds the call graph. + * Builds the interprocedural analysis. */ public ModularWorstCaseAnalysis() { this.results = new ConcurrentHashMap<>(); @@ -97,18 +102,23 @@ public Collection> getAnalysisResultsOf(CFG cfg) @Override public AnalysisState getAbstractResultOf(CFGCall call, AnalysisState entryState, - ExpressionSet[] parameters) - throws SemanticException { - if (call.getStaticType().isVoidType()) - return entryState.top(); + ExpressionSet[] parameters) throws SemanticException { + OpenCall open = new OpenCall(call.getCFG(), call.getLocation(), call.getQualifiedName(), + call.getStaticType(), call.getParameters()); + return getAbstractResultOf(open, entryState, parameters); + } - return entryState.top() - .smallStepSemantics(new Variable(call.getRuntimeTypes(), "ret_value", call.getLocation()), call); + @Override + public AnalysisState getAbstractResultOf(OpenCall call, AnalysisState entryState, + ExpressionSet[] parameters) throws SemanticException { + return policy.apply(call, entryState, parameters); } @Override - public void init(Program program, CallGraph callgraph) throws InterproceduralAnalysisException { + public void init(Program program, CallGraph callgraph, OpenCallPolicy policy) + throws InterproceduralAnalysisException { this.program = program; + this.policy = policy; } @Override diff --git a/lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java b/lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java index 30b764d77..ab847dd61 100644 --- a/lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java +++ b/lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java @@ -12,6 +12,7 @@ import it.unive.lisa.imp.ParsingException; import it.unive.lisa.interprocedural.InterproceduralAnalysisException; import it.unive.lisa.interprocedural.ModularWorstCaseAnalysis; +import it.unive.lisa.interprocedural.WorstCasePolicy; import it.unive.lisa.interprocedural.callgraph.CallGraphConstructionException; import it.unive.lisa.interprocedural.callgraph.RTACallGraph; import it.unive.lisa.program.Program; @@ -28,7 +29,7 @@ ValueEnvironment> mkAnalysis(Program p) ValueEnvironment> analysis = new ModularWorstCaseAnalysis<>(); RTACallGraph callgraph = new RTACallGraph(); callgraph.init(p); - analysis.init(p, callgraph); + analysis.init(p, callgraph, WorstCasePolicy.INSTANCE); return analysis; } diff --git a/lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java b/lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java index 9b1576ee6..32707a8c0 100644 --- a/lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java +++ b/lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java @@ -36,6 +36,7 @@ import it.unive.lisa.interprocedural.InterproceduralAnalysis; import it.unive.lisa.interprocedural.InterproceduralAnalysisException; import it.unive.lisa.interprocedural.ModularWorstCaseAnalysis; +import it.unive.lisa.interprocedural.WorstCasePolicy; import it.unive.lisa.interprocedural.callgraph.CallGraph; import it.unive.lisa.interprocedural.callgraph.CallGraphConstructionException; import it.unive.lisa.interprocedural.callgraph.RTACallGraph; @@ -103,7 +104,7 @@ public void setup() throws CallGraphConstructionException, InterproceduralAnalys cg = new RTACallGraph(); cg.init(p); interprocedural = new ModularWorstCaseAnalysis<>(); - interprocedural.init(p, cg); + interprocedural.init(p, cg, WorstCasePolicy.INSTANCE); as = new AnalysisState<>(new SimpleAbstractState<>(new MonolithicHeap(), new ValueEnvironment<>(new Sign())), new ExpressionSet<>()); store = new StatementStore<>(as); 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 943e78744..fe67d8faf 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 @@ -15,6 +15,7 @@ import it.unive.lisa.program.cfg.statement.Statement; import it.unive.lisa.program.cfg.statement.call.CFGCall; import it.unive.lisa.program.cfg.statement.call.Call; +import it.unive.lisa.program.cfg.statement.call.OpenCall; import it.unive.lisa.program.cfg.statement.call.UnresolvedCall; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; @@ -41,12 +42,14 @@ public interface InterproceduralAnalysis, * * @param callgraph the callgraph used to resolve method calls * @param program the program + * @param policy the {@link OpenCallPolicy} to be used for computing the + * result of {@link OpenCall}s * * @throws InterproceduralAnalysisException if an exception happens while * performing the * interprocedural analysis */ - void init(Program program, CallGraph callgraph) throws InterproceduralAnalysisException; + void init(Program program, CallGraph callgraph, OpenCallPolicy policy) throws InterproceduralAnalysisException; /** * Computes a fixpoint over the whole control flow graph, producing a @@ -85,16 +88,15 @@ void fixpoint(AnalysisState entryState, Collection> getAnalysisResultsOf(CFG cfg); /** - * Resolves the given call to all of its possible runtime targets, and then - * computes an analysis state that abstracts the execution of the possible + * Computes an analysis state that abstracts the execution of the possible * targets considering that they were given {@code parameters} as actual - * parameters. The abstract value of each parameter is computed on + * parameters, and the state when the call is executed is * {@code entryState}.
*
* Note that the interprocedural analysis is also responsible for * registering the call to the {@link CallGraph}, if needed. * - * @param call the call to resolve and evaluate + * @param call the call to evaluate * @param entryState the abstract analysis state when the call is reached * @param parameters the expressions representing the actual parameters of * the call @@ -103,7 +105,7 @@ void fixpoint(AnalysisState entryState, * the cfg call. The * {@link AnalysisState#getComputedExpressions()} will contain * an {@link Identifier} pointing to the meta variable - * containing the abstraction of the returned value + * containing the abstraction of the returned value, if any * * @throws SemanticException if something goes wrong during the computation */ @@ -111,6 +113,29 @@ AnalysisState getAbstractResultOf(CFGCall call, AnalysisState ExpressionSet[] parameters) throws SemanticException; + /** + * Computes an analysis state that abstracts the execution of an unknown + * target considering that they were given {@code parameters} as actual + * parameters, and the state when the call is executed is + * {@code entryState}. + * + * @param call the call to evaluate + * @param entryState the abstract analysis state when the call is reached + * @param parameters the expressions representing the actual parameters of + * the call + * + * @return an abstract analysis state representing the abstract result of + * the open call. The + * {@link AnalysisState#getComputedExpressions()} will contain + * an {@link Identifier} pointing to the meta variable + * containing the abstraction of the returned value, if any + * + * @throws SemanticException if something goes wrong during the computation + */ + AnalysisState getAbstractResultOf(OpenCall call, AnalysisState entryState, + ExpressionSet[] parameters) + throws SemanticException; + /** * Yields a {@link Call} implementation that corresponds to the resolution * of the given {@link UnresolvedCall}. This method will forward the call to 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 new file mode 100644 index 000000000..95f0c8631 --- /dev/null +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/OpenCallPolicy.java @@ -0,0 +1,52 @@ +package it.unive.lisa.interprocedural; + +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.ValueDomain; +import it.unive.lisa.program.cfg.statement.call.OpenCall; +import it.unive.lisa.symbolic.SymbolicExpression; + +/** + * Policy that determines what happens to the {@link AnalysisState} when an + * {@link OpenCall} is encountered during the fixpoint. The state is directly + * transformed by this policy. + * + * @author Luca Negrini + */ +public interface OpenCallPolicy { + + /** + * The name of the variable storing the return value of the call, if any. + */ + public static final String RETURNED_VARIABLE_NAME = "open_call_return"; + + /** + * Applies the policy to the given open call. + * + * @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 call the {@link OpenCall} under evaluation + * @param entryState the state when the call is executed + * @param params the symbolic expressions representing the computed + * values of the parameters of the call + * + * @return the {@link AnalysisState} representing the abstract result of the + * execution of this call + * + * @throws SemanticException if something goes wrong during the computation + */ + , + H extends HeapDomain, + V extends ValueDomain> AnalysisState apply( + OpenCall call, + AnalysisState entryState, + ExpressionSet[] params) + throws SemanticException; +} 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 new file mode 100644 index 000000000..16d1deb93 --- /dev/null +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/WorstCasePolicy.java @@ -0,0 +1,48 @@ +package it.unive.lisa.interprocedural; + +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.ValueDomain; +import it.unive.lisa.program.cfg.statement.call.OpenCall; +import it.unive.lisa.symbolic.SymbolicExpression; +import it.unive.lisa.symbolic.value.Skip; +import it.unive.lisa.symbolic.value.Variable; + +/** + * A worst-case {@link OpenCallPolicy}, where the whole analysis state becomes + * top and all information is lost. The return value, if any, is stored in a + * variable named {@value OpenCallPolicy#RETURNED_VARIABLE_NAME}. + * + * @author Luca Negrini + */ +public class WorstCasePolicy implements OpenCallPolicy { + + /** + * The singleton instance of this class. + */ + public static final WorstCasePolicy INSTANCE = new WorstCasePolicy(); + + private WorstCasePolicy() { + } + + @Override + public , + H extends HeapDomain, + V extends ValueDomain> 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); + else + return poststate.smallStepSemantics( + new Variable(call.getRuntimeTypes(), RETURNED_VARIABLE_NAME, call.getLocation()), call); + } + +} 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 5ab5bb7db..07c8e6f20 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 @@ -1,5 +1,12 @@ package it.unive.lisa.program.cfg.statement.call; +import java.util.Collection; +import java.util.Collections; +import java.util.Iterator; +import java.util.Objects; + +import org.apache.commons.lang3.StringUtils; + import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; import it.unive.lisa.analysis.SemanticException; @@ -14,22 +21,16 @@ import it.unive.lisa.program.cfg.statement.MetaVariableCreator; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; -import it.unive.lisa.symbolic.value.Skip; import it.unive.lisa.symbolic.value.Variable; import it.unive.lisa.type.Type; import it.unive.lisa.type.Untyped; -import java.util.Collection; -import java.util.Collections; -import java.util.Iterator; -import java.util.Objects; -import org.apache.commons.lang3.StringUtils; /** * A call to one or more of the CFGs under analysis. * * @author Luca Negrini */ -public class CFGCall extends Call implements MetaVariableCreator { +public class CFGCall extends CallWithResult implements MetaVariableCreator { /** * The targets of this call @@ -154,63 +155,23 @@ public String toString() { @Override public final Identifier getMetaVariable() { - return new Variable(getRuntimeTypes(), "call_ret_value@" + getLocation(), getLocation()); - } - - @Override - public , - H extends HeapDomain, - V extends ValueDomain> AnalysisState callSemantics( - AnalysisState entryState, - InterproceduralAnalysis interprocedural, - AnalysisState[] computedStates, - ExpressionSet[] params) - throws SemanticException { - // it corresponds to the analysis state after the evaluation of all the - // parameters of this call, it is the entry state if this call has no - // parameters (the semantics of this call does not need information - // about the intermediate analysis states) - AnalysisState callState = computedStates.length == 0 - ? entryState - : computedStates[computedStates.length - 1]; - // the stack has to be empty - callState = new AnalysisState<>(callState.getState(), new ExpressionSet<>()); - - // this will contain only the information about the returned - // metavariable - AnalysisState returned = interprocedural.getAbstractResultOf(this, callState, params); - - if (getStaticType().isVoidType() || - (getStaticType().isUntyped() && returned.getComputedExpressions().isEmpty()) || - (returned.getComputedExpressions().size() == 1 - && returned.getComputedExpressions().iterator().next() instanceof Skip)) - // no need to add the meta variable since nothing has been pushed on - // the stack - return returned.smallStepSemantics(new Skip(getLocation()), this); - - Identifier meta = getMetaVariable(); - for (SymbolicExpression expr : returned.getComputedExpressions()) - // It might be the case it chose a - // target with void return type - getMetaVariables().add((Identifier) expr); - + Variable meta = new Variable(getRuntimeTypes(), "call_ret_value@" + getLocation(), getLocation()); // propagates the annotations of the targets // to the metavariable of this cfg call for (CFG target : targets) for (Annotation ann : target.getDescriptor().getAnnotations()) meta.addAnnotation(ann); + return meta; + } - getMetaVariables().add(meta); - - AnalysisState result = returned.bottom(); - for (SymbolicExpression expr : returned.getComputedExpressions()) { - AnalysisState tmp = returned.assign(meta, expr, this); - result = result.lub(tmp.smallStepSemantics(meta, this)); - // We need to perform this evaluation of the identifier not pushed - // with the scope since otherwise - // the value associated with the returned variable would be lost - } - - return result; + @Override + protected , + H extends HeapDomain, + V extends ValueDomain> AnalysisState compute( + InterproceduralAnalysis interprocedural, + AnalysisState entryState, + ExpressionSet[] parameters) + throws SemanticException { + return interprocedural.getAbstractResultOf(this, entryState, parameters); } } 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 new file mode 100644 index 000000000..c181caebe --- /dev/null +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/program/cfg/statement/call/CallWithResult.java @@ -0,0 +1,115 @@ +package it.unive.lisa.program.cfg.statement.call; + +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.ValueDomain; +import it.unive.lisa.interprocedural.InterproceduralAnalysis; +import it.unive.lisa.program.cfg.CFG; +import it.unive.lisa.program.cfg.CodeLocation; +import it.unive.lisa.program.cfg.statement.Expression; +import it.unive.lisa.program.cfg.statement.MetaVariableCreator; +import it.unive.lisa.symbolic.SymbolicExpression; +import it.unive.lisa.symbolic.value.Identifier; +import it.unive.lisa.symbolic.value.Skip; +import it.unive.lisa.type.Type; + +/** + * A call to one or more of the CFGs under analysis. + * + * @author Luca Negrini + */ +public abstract class CallWithResult extends Call implements MetaVariableCreator { + + /** + * Builds the CFG call, happening at the given location in the program. + * + * @param cfg the cfg that this expression belongs to + * @param location the location where this expression is defined within + * the source file. If unknown, use {@code null} + * @param parameters the parameters of this call + */ + public CallWithResult(CFG cfg, CodeLocation location, Type returnType, Expression... parameters) { + super(cfg, location, returnType, parameters); + } + + /** + * Computes an analysis state that abstracts the result of this call when + * {@code parameters} are used as actual parameters, and the state when the + * call is executed is {@code entryState}. + * + * @param interprocedural the interprocedural analysis of the program to + * analyze + * @param entryState the abstract analysis state when the call is + * reached + * @param parameters the expressions representing the actual parameters + * of the call + * + * @return an abstract analysis state representing the abstract result of + * the cfg call. The + * {@link AnalysisState#getComputedExpressions()} will contain + * an {@link Identifier} pointing to the meta variable + * containing the abstraction of the returned value, if any + * + * @throws SemanticException if something goes wrong during the computation + */ + protected abstract , + H extends HeapDomain, + V extends ValueDomain> AnalysisState compute( + InterproceduralAnalysis interprocedural, + AnalysisState entryState, + ExpressionSet[] parameters) throws SemanticException; + + @Override + public , + H extends HeapDomain, + V extends ValueDomain> AnalysisState callSemantics( + AnalysisState entryState, + InterproceduralAnalysis interprocedural, + AnalysisState[] computedStates, + ExpressionSet[] params) + throws SemanticException { + // it corresponds to the analysis state after the evaluation of all the + // parameters of this call, it is the entry state if this call has no + // parameters (the semantics of this call does not need information + // about the intermediate analysis states) + AnalysisState callState = computedStates.length == 0 + ? entryState + : computedStates[computedStates.length - 1]; + // the stack has to be empty + callState = new AnalysisState<>(callState.getState(), new ExpressionSet<>()); + + // this will contain only the information about the returned + // metavariable + AnalysisState returned = compute(interprocedural, callState, params); + + if (getStaticType().isVoidType() || + (getStaticType().isUntyped() && returned.getComputedExpressions().isEmpty()) || + (returned.getComputedExpressions().size() == 1 + && returned.getComputedExpressions().iterator().next() instanceof Skip)) + // no need to add the meta variable since nothing has been pushed on + // the stack + return returned.smallStepSemantics(new Skip(getLocation()), this); + + Identifier meta = getMetaVariable(); + for (SymbolicExpression expr : returned.getComputedExpressions()) + // It might be the case it chose a + // target with void return type + getMetaVariables().add((Identifier) expr); + + getMetaVariables().add(meta); + + AnalysisState result = returned.bottom(); + for (SymbolicExpression expr : returned.getComputedExpressions()) { + // We need to perform this evaluation of the identifier not pushed + // with the scope since otherwise the value associated with the + // returned variable would be lost + AnalysisState tmp = returned.assign(meta, expr, this); + result = result.lub(tmp.smallStepSemantics(meta, this)); + } + + return result; + } +} 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 f86b91ec8..60d42d6c9 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 @@ -1,5 +1,9 @@ package it.unive.lisa.program.cfg.statement.call; +import java.util.Objects; + +import org.apache.commons.lang3.StringUtils; + import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; import it.unive.lisa.analysis.SemanticException; @@ -13,18 +17,15 @@ import it.unive.lisa.program.cfg.statement.MetaVariableCreator; import it.unive.lisa.symbolic.SymbolicExpression; import it.unive.lisa.symbolic.value.Identifier; -import it.unive.lisa.symbolic.value.Skip; import it.unive.lisa.symbolic.value.Variable; import it.unive.lisa.type.Type; -import java.util.Objects; -import org.apache.commons.lang3.StringUtils; /** * A call to a CFG that is not under analysis. * * @author Luca Negrini */ -public class OpenCall extends Call implements MetaVariableCreator { +public class OpenCall extends CallWithResult implements MetaVariableCreator { /** * The name of the target of this call @@ -93,19 +94,13 @@ public final Identifier getMetaVariable() { } @Override - public , + protected , H extends HeapDomain, - V extends ValueDomain> AnalysisState callSemantics( - AnalysisState entryState, InterproceduralAnalysis interprocedural, - AnalysisState[] computedStates, - ExpressionSet[] params) + V extends ValueDomain> AnalysisState compute( + InterproceduralAnalysis interprocedural, + AnalysisState entryState, + ExpressionSet[] parameters) throws SemanticException { - // TODO too coarse - AnalysisState poststate = entryState.top(); - - if (getStaticType().isVoidType()) - return poststate.smallStepSemantics(new Skip(getLocation()), this); - else - return poststate.smallStepSemantics(getMetaVariable(), this); + return interprocedural.getAbstractResultOf(this, entryState, parameters); } } From 975f442d306448630083a37e6434b39b06613a41 Mon Sep 17 00:00:00 2001 From: lucaneg Date: Wed, 12 Jan 2022 11:34:17 +0100 Subject: [PATCH 2/4] #151 adding an open call policy where the state does not change --- .../lisa/interprocedural/ReturnTopPolicy.java | 50 +++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/ReturnTopPolicy.java 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 new file mode 100644 index 000000000..1ef46be2a --- /dev/null +++ b/lisa/lisa-sdk/src/main/java/it/unive/lisa/interprocedural/ReturnTopPolicy.java @@ -0,0 +1,50 @@ +package it.unive.lisa.interprocedural; + +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.ValueDomain; +import it.unive.lisa.program.cfg.statement.call.OpenCall; +import it.unive.lisa.symbolic.SymbolicExpression; +import it.unive.lisa.symbolic.value.PushAny; +import it.unive.lisa.symbolic.value.Skip; +import it.unive.lisa.symbolic.value.Variable; + +/** + * An {@link OpenCallPolicy}, where the post state is exactly the entry state, + * with the only difference of having a synthetic variable named + * {@value OpenCallPolicy#RETURNED_VARIABLE_NAME} assigned to top only if + * the call returns a value. This variable, that is also stored as computed + * expression, represent the unknown result of the call, if any. + * + * @author Luca Negrini + */ +public class ReturnTopPolicy implements OpenCallPolicy { + + /** + * The singleton instance of this class. + */ + public static final ReturnTopPolicy INSTANCE = new ReturnTopPolicy(); + + private ReturnTopPolicy() { + } + + @Override + public , + H extends HeapDomain, + V extends ValueDomain> AnalysisState apply( + OpenCall call, + AnalysisState entryState, + ExpressionSet[] params) + throws SemanticException { + + if (call.getStaticType().isVoidType()) + return entryState.smallStepSemantics(new Skip(call.getLocation()), call); + else + return entryState.assign(new Variable(call.getRuntimeTypes(), RETURNED_VARIABLE_NAME, call.getLocation()), + new PushAny(call.getRuntimeTypes(), call.getLocation()), call); + } + +} From f31796a59ea57e1a54d328060895a4d0b5acaf6f Mon Sep 17 00:00:00 2001 From: lucaneg Date: Wed, 12 Jan 2022 11:36:57 +0100 Subject: [PATCH 3/4] Spotless apply --- .../java/it/unive/lisa/LiSAConfiguration.java | 2 +- .../interprocedural/ContextBasedAnalysis.java | 22 +++++++++---------- .../ModularWorstCaseAnalysis.java | 2 +- .../program/cfg/statement/call/CFGCall.java | 12 +++++----- .../program/cfg/statement/call/OpenCall.java | 6 ++--- 5 files changed, 19 insertions(+), 25 deletions(-) diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java b/lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java index 0a7ca053c..e53931284 100644 --- a/lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java +++ b/lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java @@ -702,7 +702,7 @@ public String toString() { .append(syntacticChecks.size()) .append(" syntactic checks to execute") .append((syntacticChecks.isEmpty() ? "" : ":")); - // TODO automatic way to keep this updated? + // TODO automatic way to keep this updated? for (SyntacticCheck check : syntacticChecks) res.append("\n ") .append(check.getClass().getSimpleName()); diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java b/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java index c823d35af..29f7af081 100644 --- a/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java +++ b/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java @@ -1,15 +1,5 @@ package it.unive.lisa.interprocedural; -import java.util.Collection; -import java.util.Collections; -import java.util.HashSet; -import java.util.Map; -import java.util.Optional; - -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.analysis.AbstractState; @@ -34,6 +24,14 @@ import it.unive.lisa.util.collections.workset.VisitOnceWorkingSet; import it.unive.lisa.util.collections.workset.WorkingSet; import it.unive.lisa.util.datastructures.graph.algorithms.FixpointException; +import java.util.Collection; +import java.util.Collections; +import java.util.HashSet; +import java.util.Map; +import java.util.Optional; +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 @@ -150,7 +148,7 @@ private void fixpointAux(AnalysisState entryState, iter++; } while (!fixpointTriggers.isEmpty()); } - + @Override public Collection> getAnalysisResultsOf(CFG cfg) { if (results.contains(cfg)) @@ -230,7 +228,7 @@ public AnalysisState getAbstractResultOf(CFGCall call, AnalysisState computeFixpoint(CFG cfg, ContextSensitivityToken localToken, AnalysisState computedEntryState) throws FixpointException, SemanticException, AnalysisSetupException { diff --git a/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java b/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java index 2f566624c..70bfa197f 100644 --- a/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java +++ b/lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java @@ -104,7 +104,7 @@ public Collection> getAnalysisResultsOf(CFG cfg) public AnalysisState getAbstractResultOf(CFGCall call, AnalysisState entryState, ExpressionSet[] parameters) throws SemanticException { OpenCall open = new OpenCall(call.getCFG(), call.getLocation(), call.getQualifiedName(), - call.getStaticType(), call.getParameters()); + call.getStaticType(), call.getParameters()); return getAbstractResultOf(open, entryState, parameters); } 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 07c8e6f20..f1498aa4f 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 @@ -1,12 +1,5 @@ package it.unive.lisa.program.cfg.statement.call; -import java.util.Collection; -import java.util.Collections; -import java.util.Iterator; -import java.util.Objects; - -import org.apache.commons.lang3.StringUtils; - import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; import it.unive.lisa.analysis.SemanticException; @@ -24,6 +17,11 @@ import it.unive.lisa.symbolic.value.Variable; import it.unive.lisa.type.Type; import it.unive.lisa.type.Untyped; +import java.util.Collection; +import java.util.Collections; +import java.util.Iterator; +import java.util.Objects; +import org.apache.commons.lang3.StringUtils; /** * A call to one or more of the CFGs under analysis. 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 60d42d6c9..54e1a2949 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 @@ -1,9 +1,5 @@ package it.unive.lisa.program.cfg.statement.call; -import java.util.Objects; - -import org.apache.commons.lang3.StringUtils; - import it.unive.lisa.analysis.AbstractState; import it.unive.lisa.analysis.AnalysisState; import it.unive.lisa.analysis.SemanticException; @@ -19,6 +15,8 @@ import it.unive.lisa.symbolic.value.Identifier; import it.unive.lisa.symbolic.value.Variable; import it.unive.lisa.type.Type; +import java.util.Objects; +import org.apache.commons.lang3.StringUtils; /** * A call to a CFG that is not under analysis. From a7a3f1ef9b0bc622ad94f37cd65cade5a39191a9 Mon Sep 17 00:00:00 2001 From: lucaneg Date: Wed, 12 Jan 2022 11:57:22 +0100 Subject: [PATCH 4/4] Javadoc and fixing tests --- ...___untyped_tests.subtyping(tests_this).dot | 22 +++++++++---------- ...___untyped_tests.subtyping(tests_this).dot | 18 +++++++-------- .../cfg/statement/call/CallWithResult.java | 8 +++++-- 3 files changed, 26 insertions(+), 22 deletions(-) diff --git a/lisa/lisa-core/imp-testcases/interprocedural/CHA/analysis___untyped_tests.subtyping(tests_this).dot b/lisa/lisa-core/imp-testcases/interprocedural/CHA/analysis___untyped_tests.subtyping(tests_this).dot index c58ad5f31..47e35aaed 100644 --- a/lisa/lisa-core/imp-testcases/interprocedural/CHA/analysis___untyped_tests.subtyping(tests_this).dot +++ b/lisa/lisa-core/imp-testcases/interprocedural/CHA/analysis___untyped_tests.subtyping(tests_this).dot @@ -1,16 +1,16 @@ digraph { "node0" [shape="rect",color="black",label={{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [a]>]; - "node1" [shape="rect",color="black",peripheries="2",label={{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [skip]>]; - "node2" [shape="rect",color="gray",label={{
heap [[ monolith ]]
value [[ b: 0 ]]
}} -> [b]>]; - "node3" [shape="rect",color="gray",label=<<(b, 10)
{{
heap [[ monolith ]]
value [[ b: 0 ]]
}} -> [b < 10]>]; - "node4" [shape="rect",color="gray",label={{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [a]>]; - "node5" [shape="rect",color="gray",label=<[unresolved]foo(a)
{{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11]>]; - "node2" -> "node3" [color="black"]; - "node3" -> "node4" [color="blue",style="dashed"]; - "node3" -> "node5" [color="red",style="dashed"]; - "node4" -> "node5" [color="black"]; - "node5" -> "node1" [color="black"]; - "node0" -> "node2" [color="black"]; + "node1" [shape="rect",color="gray",label=<<(b, 10)
{{
heap [[ monolith ]]
value [[ b: 0 ]]
}} -> [b < 10]>]; + "node2" [shape="rect",color="gray",label={{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [a]>]; + "node3" [shape="rect",color="gray",label={{
heap [[ monolith ]]
value [[ b: 0 ]]
}} -> [b]>]; + "node4" [shape="rect",color="black",peripheries="2",label={{
heap [[ monolith ]]
value [[ open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11: #TOP# ]]
}} -> [skip]>]; + "node5" [shape="rect",color="gray",label=<[unresolved]foo(a)
{{
heap [[ monolith ]]
value [[ open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11: #TOP# ]]
}} -> [open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11]>]; + "node1" -> "node2" [color="blue",style="dashed"]; + "node1" -> "node5" [color="red",style="dashed"]; + "node2" -> "node5" [color="black"]; + "node3" -> "node1" [color="black"]; + "node5" -> "node4" [color="black"]; + "node0" -> "node3" [color="black"]; subgraph cluster_legend { label="Legend"; style=dotted; diff --git a/lisa/lisa-core/imp-testcases/interprocedural/RTA/analysis___untyped_tests.subtyping(tests_this).dot b/lisa/lisa-core/imp-testcases/interprocedural/RTA/analysis___untyped_tests.subtyping(tests_this).dot index 0827e092b..47e35aaed 100644 --- a/lisa/lisa-core/imp-testcases/interprocedural/RTA/analysis___untyped_tests.subtyping(tests_this).dot +++ b/lisa/lisa-core/imp-testcases/interprocedural/RTA/analysis___untyped_tests.subtyping(tests_this).dot @@ -1,16 +1,16 @@ digraph { "node0" [shape="rect",color="black",label={{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [a]>]; - "node1" [shape="rect",color="black",peripheries="2",label={{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [skip]>]; - "node2" [shape="rect",color="gray",label=<[unresolved]foo(a)
{{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11]>]; + "node1" [shape="rect",color="gray",label=<<(b, 10)
{{
heap [[ monolith ]]
value [[ b: 0 ]]
}} -> [b < 10]>]; + "node2" [shape="rect",color="gray",label={{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [a]>]; "node3" [shape="rect",color="gray",label={{
heap [[ monolith ]]
value [[ b: 0 ]]
}} -> [b]>]; - "node4" [shape="rect",color="gray",label=<<(b, 10)
{{
heap [[ monolith ]]
value [[ b: 0 ]]
}} -> [b < 10]>]; - "node5" [shape="rect",color="gray",label={{
heap [[ monolith ]]
value [[ #TOP# ]]
}} -> [a]>]; + "node4" [shape="rect",color="black",peripheries="2",label={{
heap [[ monolith ]]
value [[ open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11: #TOP# ]]
}} -> [skip]>]; + "node5" [shape="rect",color="gray",label=<[unresolved]foo(a)
{{
heap [[ monolith ]]
value [[ open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11: #TOP# ]]
}} -> [open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11]>]; + "node1" -> "node2" [color="blue",style="dashed"]; + "node1" -> "node5" [color="red",style="dashed"]; + "node2" -> "node5" [color="black"]; + "node3" -> "node1" [color="black"]; + "node5" -> "node4" [color="black"]; "node0" -> "node3" [color="black"]; - "node2" -> "node1" [color="black"]; - "node3" -> "node4" [color="black"]; - "node4" -> "node2" [color="red",style="dashed"]; - "node4" -> "node5" [color="blue",style="dashed"]; - "node5" -> "node2" [color="black"]; subgraph cluster_legend { label="Legend"; style=dotted; 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 c181caebe..d0fac98d1 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 @@ -29,10 +29,11 @@ public abstract class CallWithResult extends Call implements MetaVariableCreator * @param cfg the cfg that this expression belongs to * @param location the location where this expression is defined within * the source file. If unknown, use {@code null} + * @param staticType the static type of this call * @param parameters the parameters of this call */ - public CallWithResult(CFG cfg, CodeLocation location, Type returnType, Expression... parameters) { - super(cfg, location, returnType, parameters); + public CallWithResult(CFG cfg, CodeLocation location, Type staticType, Expression... parameters) { + super(cfg, location, staticType, parameters); } /** @@ -40,6 +41,9 @@ public CallWithResult(CFG cfg, CodeLocation location, Type returnType, Expressio * {@code parameters} are used as actual parameters, and the state when the * call is executed is {@code entryState}. * + * @param the type of {@link AbstractState} + * @param the type of the {@link HeapDomain} + * @param the type of the {@link ValueDomain} * @param interprocedural the interprocedural analysis of the program to * analyze * @param entryState the abstract analysis state when the call is