Open calls

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=<a = new B()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
-	"node1" [shape="rect",color="black",peripheries="2",label=<ret<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [skip]>];
-	"node2" [shape="rect",color="gray",label=<b = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b]>];
-	"node3" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b &lt; 10]>];
-	"node4" [shape="rect",color="gray",label=<a = new A()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
-	"node5" [shape="rect",color="gray",label=<[unresolved]foo(a)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [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=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b &lt; 10]>];
+	"node2" [shape="rect",color="gray",label=<a = new A()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
+	"node3" [shape="rect",color="gray",label=<b = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b]>];
+	"node4" [shape="rect",color="black",peripheries="2",label=<ret<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11: #TOP# ]]<BR/>}} -&gt; [skip]>];
+	"node5" [shape="rect",color="gray",label=<[unresolved]foo(a)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11: #TOP# ]]<BR/>}} -&gt; [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;

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=<a = new B()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
-	"node1" [shape="rect",color="black",peripheries="2",label=<ret<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [skip]>];
-	"node2" [shape="rect",color="gray",label=<[unresolved]foo(a)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11]>];
+	"node1" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b &lt; 10]>];
+	"node2" [shape="rect",color="gray",label=<a = new A()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
 	"node3" [shape="rect",color="gray",label=<b = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b]>];
-	"node4" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b &lt; 10]>];
-	"node5" [shape="rect",color="gray",label=<a = new A()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
+	"node4" [shape="rect",color="black",peripheries="2",label=<ret<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11: #TOP# ]]<BR/>}} -&gt; [skip]>];
+	"node5" [shape="rect",color="gray",label=<[unresolved]foo(a)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ open_call_ret_value@'imp-testcases/interprocedural/program.imp':20:11: #TOP# ]]<BR/>}} -&gt; [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;

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:
 	 * <ul>
@@ -135,6 +144,7 @@ public class LiSAConfiguration {
 	 * <li>the json report will not be dumped</li>
 	 * <li>the default warning threshold ({@value #DEFAULT_WIDENING_THRESHOLD})
 	 * will be used</li>
+	 * <li>the open call policy used is {@link WorstCasePolicy}</li>
 	 * </ul>
 	 */
 	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());

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,15 +136,15 @@ Collection<Warning> 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(
 					"Exception while building the interprocedural analysis for the input program", e);
 		}
 
 		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,15 +192,15 @@ private void analyze(Collection<CFG> allCFGs, FileManager fileManager) {
 	}
 
 	@SuppressWarnings("unchecked")
-	private void inferTypes(FileManager fileManager, Program program, Collection<CFG> allCFGs) {
+	private void inferTypes(FileManager fileManager, Program program, Collection<CFG> allCFGs, OpenCallPolicy policy) {
 		T typesState = this.typeState.top();
 		InterproceduralAnalysis<T, HT, VT> typesInterproc;
 		CallGraph typesCg;
 		try {
 			typesCg = getInstance(callGraph.getClass());
 			typesInterproc = getInstance(interproc.getClass());
 			typesCg.init(program);
-			typesInterproc.init(program, typesCg);
+			typesInterproc.init(program, typesCg, policy);
 		} catch (AnalysisSetupException | InterproceduralAnalysisException | CallGraphConstructionException e) {
 			throw new AnalysisExecutionException("Unable to initialize type inference", e);
 		}

lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/CallGraphBasedAnalysis.java

@@ -13,7 +13,9 @@
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.Parameter;
 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.PushAny;
 import it.unive.lisa.symbolic.value.Variable;
 import it.unive.lisa.type.Type;
@@ -40,8 +42,14 @@ public abstract class CallGraphBasedAnalysis<A extends AbstractState<A, H, V>,
 	 */
 	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<A, H, V> prepareEntryStateOfEntryPoint(AnalysisState<A,
 		// the stack has to be empty
 		return new AnalysisState<>(prepared.getState(), new ExpressionSet<>());
 	}
+
+	@Override
+	public AnalysisState<A, H, V> getAbstractResultOf(OpenCall call, AnalysisState<A, H, V> entryState,
+			ExpressionSet<SymbolicExpression>[] parameters) throws SemanticException {
+		return policy.apply(call, entryState, parameters);
+	}
 }

lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java

@@ -240,5 +240,4 @@ private CFGWithAnalysisResults<A, H, V> computeFixpoint(CFG cfg, ContextSensitiv
 			fixpointTriggers.add(cfg);
 		return res.getRight();
 	}
-
 }

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 <A> the abstract state of the analysis
  * @param <H> the heap domain
@@ -53,6 +53,11 @@ public class ModularWorstCaseAnalysis<A extends AbstractState<A, H, V>,
 	 */
 	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<A extends AbstractState<A, H, V>,
 	private final Map<CFG, Optional<CFGWithAnalysisResults<A, H, V>>> results;
 
 	/**
-	 * Builds the call graph.
+	 * Builds the interprocedural analysis.
 	 */
 	public ModularWorstCaseAnalysis() {
 		this.results = new ConcurrentHashMap<>();
@@ -97,18 +102,23 @@ public Collection<CFGWithAnalysisResults<A, H, V>> getAnalysisResultsOf(CFG cfg)
 
 	@Override
 	public AnalysisState<A, H, V> getAbstractResultOf(CFGCall call, AnalysisState<A, H, V> entryState,
-			ExpressionSet<SymbolicExpression>[] parameters)
-			throws SemanticException {
-		if (call.getStaticType().isVoidType())
-			return entryState.top();
+			ExpressionSet<SymbolicExpression>[] 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<A, H, V> getAbstractResultOf(OpenCall call, AnalysisState<A, H, V> entryState,
+			ExpressionSet<SymbolicExpression>[] 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

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<Sign>> mkAnalysis(Program p)
 				ValueEnvironment<Sign>> analysis = new ModularWorstCaseAnalysis<>();
 		RTACallGraph callgraph = new RTACallGraph();
 		callgraph.init(p);
-		analysis.init(p, callgraph);
+		analysis.init(p, callgraph, WorstCasePolicy.INSTANCE);
 		return analysis;
 	}
 

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);