Skip to content

Commit 943c8e5

Browse files
VincenzoArceriVincenzoArceri
authored
Merge pull request #156 from UniVE-SSV/open-calls
Open calls
2 parents ea27871 + a7a3f1e commit 943c8e5

File tree

16 files changed

+422
-112
lines changed

16 files changed

+422
-112
lines changed

‎lisa/lisa-core/imp-testcases/interprocedural/CHA/analysis___untyped_tests.subtyping(tests_this).dot‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<a = new B()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
3-
"node1" [shape="rect",color="black",peripheries="2",label=<ret<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [skip]>];
4-
"node2" [shape="rect",color="gray",label=<b = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b]>];
5-
"node3" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b &lt; 10]>];
6-
"node4" [shape="rect",color="gray",label=<a = new A()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
7-
"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]>];
8-
"node2" -> "node3" [color="black"];
9-
"node3" -> "node4" [color="blue",style="dashed"];
10-
"node3" -> "node5" [color="red",style="dashed"];
11-
"node4" -> "node5" [color="black"];
12-
"node5" -> "node1" [color="black"];
13-
"node0" -> "node2" [color="black"];
3+
"node1" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b &lt; 10]>];
4+
"node2" [shape="rect",color="gray",label=<a = new A()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
5+
"node3" [shape="rect",color="gray",label=<b = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b]>];
6+
"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]>];
7+
"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]>];
8+
"node1" -> "node2" [color="blue",style="dashed"];
9+
"node1" -> "node5" [color="red",style="dashed"];
10+
"node2" -> "node5" [color="black"];
11+
"node3" -> "node1" [color="black"];
12+
"node5" -> "node4" [color="black"];
13+
"node0" -> "node3" [color="black"];
1414
subgraph cluster_legend {
1515
label="Legend";
1616
style=dotted;

‎lisa/lisa-core/imp-testcases/interprocedural/RTA/analysis___untyped_tests.subtyping(tests_this).dot‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,16 @@
11
digraph {
22
"node0" [shape="rect",color="black",label=<a = new B()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
3-
"node1" [shape="rect",color="black",peripheries="2",label=<ret<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [skip]>];
4-
"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]>];
3+
"node1" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b &lt; 10]>];
4+
"node2" [shape="rect",color="gray",label=<a = new A()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
55
"node3" [shape="rect",color="gray",label=<b = 0<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b]>];
6-
"node4" [shape="rect",color="gray",label=<&lt;(b, 10)<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ b: 0 ]]<BR/>}} -&gt; [b &lt; 10]>];
7-
"node5" [shape="rect",color="gray",label=<a = new A()<BR/>{{<BR/>heap [[ monolith ]]<BR/>value [[ #TOP# ]]<BR/>}} -&gt; [a]>];
6+
"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]>];
7+
"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]>];
8+
"node1" -> "node2" [color="blue",style="dashed"];
9+
"node1" -> "node5" [color="red",style="dashed"];
10+
"node2" -> "node5" [color="black"];
11+
"node3" -> "node1" [color="black"];
12+
"node5" -> "node4" [color="black"];
813
"node0" -> "node3" [color="black"];
9-
"node2" -> "node1" [color="black"];
10-
"node3" -> "node4" [color="black"];
11-
"node4" -> "node2" [color="red",style="dashed"];
12-
"node4" -> "node5" [color="blue",style="dashed"];
13-
"node5" -> "node2" [color="black"];
1414
subgraph cluster_legend {
1515
label="Legend";
1616
style=dotted;

‎lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java‎

Lines changed: 39 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,12 @@
66
import it.unive.lisa.checks.syntactic.SyntacticCheck;
77
import it.unive.lisa.checks.warnings.Warning;
88
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
9+
import it.unive.lisa.interprocedural.OpenCallPolicy;
10+
import it.unive.lisa.interprocedural.WorstCasePolicy;
911
import it.unive.lisa.interprocedural.callgraph.CallGraph;
1012
import it.unive.lisa.program.cfg.CFG;
1113
import it.unive.lisa.program.cfg.statement.Statement;
14+
import it.unive.lisa.program.cfg.statement.call.OpenCall;
1215
import it.unive.lisa.symbolic.SymbolicExpression;
1316
import it.unive.lisa.type.Type;
1417
import it.unive.lisa.util.collections.externalSet.ExternalSet;
@@ -120,6 +123,12 @@ public class LiSAConfiguration {
120123
*/
121124
private Class<?> fixpointWorkingSet;
122125

126+
/**
127+
* The {@link OpenCallPolicy} to be used for computing the result of
128+
* {@link OpenCall}s.
129+
*/
130+
private OpenCallPolicy openCallPolicy;
131+
123132
/**
124133
* Builds a new configuration object, with default settings. By default:
125134
* <ul>
@@ -135,6 +144,7 @@ public class LiSAConfiguration {
135144
* <li>the json report will not be dumped</li>
136145
* <li>the default warning threshold ({@value #DEFAULT_WIDENING_THRESHOLD})
137146
* will be used</li>
147+
* <li>the open call policy used is {@link WorstCasePolicy}</li>
138148
* </ul>
139149
*/
140150
public LiSAConfiguration() {
@@ -143,6 +153,7 @@ public LiSAConfiguration() {
143153
this.workdir = Paths.get(".").toAbsolutePath().normalize().toString();
144154
this.wideningThreshold = DEFAULT_WIDENING_THRESHOLD;
145155
this.fixpointWorkingSet = FIFOWorkingSet.class;
156+
this.openCallPolicy = WorstCasePolicy.INSTANCE;
146157
}
147158

148159
/**
@@ -400,6 +411,18 @@ public LiSAConfiguration setWideningThreshold(int wideningThreshold) {
400411
return this;
401412
}
402413

414+
/**
415+
* Sets the {@link OpenCallPolicy} to use during the analysis.
416+
*
417+
* @param openCallPolicy the policy to use
418+
*
419+
* @return the current (modified) configuration
420+
*/
421+
public LiSAConfiguration setOpenCallPolicy(OpenCallPolicy openCallPolicy) {
422+
this.openCallPolicy = openCallPolicy;
423+
return this;
424+
}
425+
403426
/**
404427
* Yields the {@link CallGraph} for the analysis. Might be {@code null} if
405428
* none was set.
@@ -553,6 +576,15 @@ public int getWideningThreshold() {
553576
return wideningThreshold;
554577
}
555578

579+
/**
580+
* Yields the {@link OpenCallPolicy} to use during the analysis.
581+
*
582+
* @return the policy
583+
*/
584+
public OpenCallPolicy getOpenCallPolicy() {
585+
return openCallPolicy;
586+
}
587+
556588
@Override
557589
public int hashCode() {
558590
final int prime = 31;
@@ -572,6 +604,7 @@ public int hashCode() {
572604
result = prime * result + ((syntacticChecks == null) ? 0 : syntacticChecks.hashCode());
573605
result = prime * result + wideningThreshold;
574606
result = prime * result + ((workdir == null) ? 0 : workdir.hashCode());
607+
result = prime * result + ((openCallPolicy == null) ? 0 : openCallPolicy.hashCode());
575608
return result;
576609
}
577610

@@ -641,6 +674,11 @@ public boolean equals(Object obj) {
641674
return false;
642675
} else if (!workdir.equals(other.workdir))
643676
return false;
677+
if (openCallPolicy == null) {
678+
if (other.openCallPolicy != null)
679+
return false;
680+
} else if (!openCallPolicy.equals(other.openCallPolicy))
681+
return false;
644682
return true;
645683
}
646684

@@ -664,7 +702,7 @@ public String toString() {
664702
.append(syntacticChecks.size())
665703
.append(" syntactic checks to execute")
666704
.append((syntacticChecks.isEmpty() ? "" : ":"));
667-
705+
// TODO automatic way to keep this updated?
668706
for (SyntacticCheck check : syntacticChecks)
669707
res.append("\n ")
670708
.append(check.getClass().getSimpleName());

‎lisa/lisa-core/src/main/java/it/unive/lisa/LiSARunner.java‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import it.unive.lisa.checks.warnings.Warning;
1717
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
1818
import it.unive.lisa.interprocedural.InterproceduralAnalysisException;
19+
import it.unive.lisa.interprocedural.OpenCallPolicy;
1920
import it.unive.lisa.interprocedural.callgraph.CallGraph;
2021
import it.unive.lisa.interprocedural.callgraph.CallGraphConstructionException;
2122
import it.unive.lisa.logging.IterationLogger;
@@ -135,15 +136,15 @@ Collection<Warning> run(Program program, FileManager fileManager) {
135136
}
136137

137138
try {
138-
interproc.init(program, callGraph);
139+
interproc.init(program, callGraph, conf.getOpenCallPolicy());
139140
} catch (InterproceduralAnalysisException e) {
140141
LOG.fatal("Exception while building the interprocedural analysis for the input program", e);
141142
throw new AnalysisExecutionException(
142143
"Exception while building the interprocedural analysis for the input program", e);
143144
}
144145

145146
if (conf.isInferTypes())
146-
inferTypes(fileManager, program, allCFGs);
147+
inferTypes(fileManager, program, allCFGs, conf.getOpenCallPolicy());
147148
else
148149
LOG.warn("Type inference disabled: dynamic type information will not be available for following analysis");
149150

@@ -191,15 +192,15 @@ private void analyze(Collection<CFG> allCFGs, FileManager fileManager) {
191192
}
192193

193194
@SuppressWarnings("unchecked")
194-
private void inferTypes(FileManager fileManager, Program program, Collection<CFG> allCFGs) {
195+
private void inferTypes(FileManager fileManager, Program program, Collection<CFG> allCFGs, OpenCallPolicy policy) {
195196
T typesState = this.typeState.top();
196197
InterproceduralAnalysis<T, HT, VT> typesInterproc;
197198
CallGraph typesCg;
198199
try {
199200
typesCg = getInstance(callGraph.getClass());
200201
typesInterproc = getInstance(interproc.getClass());
201202
typesCg.init(program);
202-
typesInterproc.init(program, typesCg);
203+
typesInterproc.init(program, typesCg, policy);
203204
} catch (AnalysisSetupException | InterproceduralAnalysisException | CallGraphConstructionException e) {
204205
throw new AnalysisExecutionException("Unable to initialize type inference", e);
205206
}

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

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,9 @@
1313
import it.unive.lisa.program.cfg.CFG;
1414
import it.unive.lisa.program.cfg.Parameter;
1515
import it.unive.lisa.program.cfg.statement.call.Call;
16+
import it.unive.lisa.program.cfg.statement.call.OpenCall;
1617
import it.unive.lisa.program.cfg.statement.call.UnresolvedCall;
18+
import it.unive.lisa.symbolic.SymbolicExpression;
1719
import it.unive.lisa.symbolic.value.PushAny;
1820
import it.unive.lisa.symbolic.value.Variable;
1921
import it.unive.lisa.type.Type;
@@ -40,8 +42,14 @@ public abstract class CallGraphBasedAnalysis<A extends AbstractState<A, H, V>,
4042
*/
4143
protected Program program;
4244

45+
/**
46+
* The policy to evaluate results of open calls.
47+
*/
48+
protected OpenCallPolicy policy;
49+
4350
@Override
44-
public void init(Program program, CallGraph callgraph) throws InterproceduralAnalysisException {
51+
public void init(Program program, CallGraph callgraph, OpenCallPolicy policy)
52+
throws InterproceduralAnalysisException {
4553
this.callgraph = callgraph;
4654
this.program = program;
4755
}
@@ -75,4 +83,10 @@ protected AnalysisState<A, H, V> prepareEntryStateOfEntryPoint(AnalysisState<A,
7583
// the stack has to be empty
7684
return new AnalysisState<>(prepared.getState(), new ExpressionSet<>());
7785
}
86+
87+
@Override
88+
public AnalysisState<A, H, V> getAbstractResultOf(OpenCall call, AnalysisState<A, H, V> entryState,
89+
ExpressionSet<SymbolicExpression>[] parameters) throws SemanticException {
90+
return policy.apply(call, entryState, parameters);
91+
}
7892
}

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -240,5 +240,4 @@ private CFGWithAnalysisResults<A, H, V> computeFixpoint(CFG cfg, ContextSensitiv
240240
fixpointTriggers.add(cfg);
241241
return res.getRight();
242242
}
243-
244243
}

‎lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java‎

Lines changed: 19 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@
3636
import org.apache.logging.log4j.Logger;
3737

3838
/**
39-
* A worst case modular analysis were all method calls return top.
39+
* A worst case modular analysis were all cfg calls are treated as open calls.
4040
*
4141
* @param <A> the abstract state of the analysis
4242
* @param <H> the heap domain
@@ -53,6 +53,11 @@ public class ModularWorstCaseAnalysis<A extends AbstractState<A, H, V>,
5353
*/
5454
private Program program;
5555

56+
/**
57+
* The policy used for computing the result of cfg calls.
58+
*/
59+
private OpenCallPolicy policy;
60+
5661
/**
5762
* The cash of the fixpoints' results. {@link Map#keySet()} will contain all
5863
* 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>,
6267
private final Map<CFG, Optional<CFGWithAnalysisResults<A, H, V>>> results;
6368

6469
/**
65-
* Builds the call graph.
70+
* Builds the interprocedural analysis.
6671
*/
6772
public ModularWorstCaseAnalysis() {
6873
this.results = new ConcurrentHashMap<>();
@@ -97,18 +102,23 @@ public Collection<CFGWithAnalysisResults<A, H, V>> getAnalysisResultsOf(CFG cfg)
97102

98103
@Override
99104
public AnalysisState<A, H, V> getAbstractResultOf(CFGCall call, AnalysisState<A, H, V> entryState,
100-
ExpressionSet<SymbolicExpression>[] parameters)
101-
throws SemanticException {
102-
if (call.getStaticType().isVoidType())
103-
return entryState.top();
105+
ExpressionSet<SymbolicExpression>[] parameters) throws SemanticException {
106+
OpenCall open = new OpenCall(call.getCFG(), call.getLocation(), call.getQualifiedName(),
107+
call.getStaticType(), call.getParameters());
108+
return getAbstractResultOf(open, entryState, parameters);
109+
}
104110

105-
return entryState.top()
106-
.smallStepSemantics(new Variable(call.getRuntimeTypes(), "ret_value", call.getLocation()), call);
111+
@Override
112+
public AnalysisState<A, H, V> getAbstractResultOf(OpenCall call, AnalysisState<A, H, V> entryState,
113+
ExpressionSet<SymbolicExpression>[] parameters) throws SemanticException {
114+
return policy.apply(call, entryState, parameters);
107115
}
108116

109117
@Override
110-
public void init(Program program, CallGraph callgraph) throws InterproceduralAnalysisException {
118+
public void init(Program program, CallGraph callgraph, OpenCallPolicy policy)
119+
throws InterproceduralAnalysisException {
111120
this.program = program;
121+
this.policy = policy;
112122
}
113123

114124
@Override

‎lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/CFGFixpointTest.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import it.unive.lisa.imp.ParsingException;
1313
import it.unive.lisa.interprocedural.InterproceduralAnalysisException;
1414
import it.unive.lisa.interprocedural.ModularWorstCaseAnalysis;
15+
import it.unive.lisa.interprocedural.WorstCasePolicy;
1516
import it.unive.lisa.interprocedural.callgraph.CallGraphConstructionException;
1617
import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
1718
import it.unive.lisa.program.Program;
@@ -28,7 +29,7 @@ ValueEnvironment<Sign>> mkAnalysis(Program p)
2829
ValueEnvironment<Sign>> analysis = new ModularWorstCaseAnalysis<>();
2930
RTACallGraph callgraph = new RTACallGraph();
3031
callgraph.init(p);
31-
analysis.init(p, callgraph);
32+
analysis.init(p, callgraph, WorstCasePolicy.INSTANCE);
3233
return analysis;
3334
}
3435

‎lisa/lisa-core/src/test/java/it/unive/lisa/program/cfg/SemanticsSanityTest.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@
3636
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
3737
import it.unive.lisa.interprocedural.InterproceduralAnalysisException;
3838
import it.unive.lisa.interprocedural.ModularWorstCaseAnalysis;
39+
import it.unive.lisa.interprocedural.WorstCasePolicy;
3940
import it.unive.lisa.interprocedural.callgraph.CallGraph;
4041
import it.unive.lisa.interprocedural.callgraph.CallGraphConstructionException;
4142
import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
@@ -103,7 +104,7 @@ public void setup() throws CallGraphConstructionException, InterproceduralAnalys
103104
cg = new RTACallGraph();
104105
cg.init(p);
105106
interprocedural = new ModularWorstCaseAnalysis<>();
106-
interprocedural.init(p, cg);
107+
interprocedural.init(p, cg, WorstCasePolicy.INSTANCE);
107108
as = new AnalysisState<>(new SimpleAbstractState<>(new MonolithicHeap(), new ValueEnvironment<>(new Sign())),
108109
new ExpressionSet<>());
109110
store = new StatementStore<>(as);

0 commit comments

Comments
 (0)