Skip to content

Commit 9eb34e5

Browse files
rcosta358rcosta358
authored
Context History Tracking (#155)
1 parent 1bd08b4 commit 9eb34e5

File tree

11 files changed

+158
-40
lines changed

11 files changed

+158
-40
lines changed

liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinement.java renamed to liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinement.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
import liquidjava.specification.Refinement;
55

66
@SuppressWarnings("unused")
7-
public class ErrorSpecificVarInRefinement {
7+
public class ErrorInstanceVarInRefinement {
88
public static void main(String[] args) {
99
@Refinement("_ < 10")
1010
int a = 6;

liquidjava-example/src/main/java/testSuite/ErrorSpecificVarInRefinementIf.java renamed to liquidjava-example/src/main/java/testSuite/ErrorInstanceVarInRefinementIf.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
import liquidjava.specification.Refinement;
55

66
@SuppressWarnings("unused")
7-
public class ErrorSpecificVarInRefinementIf {
7+
public class ErrorInstanceVarInRefinementIf {
88
public static void main(String[] args) {
99
@Refinement("_ < 10")
1010
int a = 6;

‎liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88
import liquidjava.diagnostics.errors.CustomError;
99
import liquidjava.diagnostics.warnings.CustomWarning;
1010
import liquidjava.processor.RefinementProcessor;
11+
import liquidjava.processor.context.ContextHistory;
1112
import spoon.Launcher;
1213
import spoon.compiler.Environment;
1314
import spoon.processing.ProcessingManager;
@@ -18,6 +19,7 @@
1819
public class CommandLineLauncher {
1920

2021
private static final Diagnostics diagnostics = Diagnostics.getInstance();
22+
private static final ContextHistory contextHistory = ContextHistory.getInstance();
2123

2224
public static void main(String[] args) {
2325
if (args.length == 0) {
@@ -46,6 +48,7 @@ public static void launch(String... paths) {
4648
System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", ""));
4749

4850
diagnostics.clear();
51+
contextHistory.clearHistory();
4952
Launcher launcher = new Launcher();
5053
for (String path : paths) {
5154
if (!new File(path).exists()) {

‎liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java‎

Lines changed: 45 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -8,25 +8,24 @@
88
public class Context {
99
private Stack<List<RefinedVariable>> ctxVars;
1010
private List<RefinedFunction> ctxFunctions;
11-
private List<RefinedVariable> ctxSpecificVars;
12-
11+
private List<RefinedVariable> ctxInstanceVars;
1312
private final List<RefinedVariable> ctxGlobalVars;
1413

1514
private List<GhostFunction> ghosts;
1615
private Map<String, List<GhostState>> classStates;
17-
private List<AliasWrapper> alias;
16+
private List<AliasWrapper> aliases;
1817

19-
public int counter;
18+
private int counter;
2019
private static Context instance;
2120

2221
private Context() {
2322
ctxVars = new Stack<>();
2423
ctxVars.add(new ArrayList<>());
2524
ctxFunctions = new ArrayList<>();
26-
ctxSpecificVars = new ArrayList<>();
25+
ctxInstanceVars = new ArrayList<>();
2726
ctxGlobalVars = new ArrayList<>();
2827

29-
alias = new ArrayList<>();
28+
aliases = new ArrayList<>();
3029
ghosts = new ArrayList<>();
3130
classStates = new HashMap<>();
3231
counter = 0;
@@ -41,13 +40,13 @@ public static Context getInstance() {
4140
public void reinitializeContext() {
4241
ctxVars = new Stack<>();
4342
ctxVars.add(new ArrayList<>()); // global vars
44-
ctxSpecificVars = new ArrayList<>();
43+
ctxInstanceVars = new ArrayList<>();
4544
}
4645

4746
public void reinitializeAllContext() {
4847
reinitializeContext();
4948
ctxFunctions = new ArrayList<>();
50-
alias = new ArrayList<>();
49+
aliases = new ArrayList<>();
5150
ghosts = new ArrayList<>();
5251
classStates = new HashMap<>();
5352
counter = 0;
@@ -80,7 +79,7 @@ public Map<String, CtTypeReference<?>> getContext() {
8079
ret.put(var.getName(), var.getType());
8180
}
8281
}
83-
for (RefinedVariable var : ctxSpecificVars)
82+
for (RefinedVariable var : ctxInstanceVars)
8483
ret.put(var.getName(), var.getType());
8584
for (RefinedVariable var : ctxGlobalVars)
8685
ret.put(var.getName(), var.getType());
@@ -94,6 +93,10 @@ public void addGlobalVariableToContext(String simpleName, String location, CtTyp
9493
ctxGlobalVars.add(vi);
9594
}
9695

96+
public List<RefinedVariable> getCtxGlobalVars() {
97+
return ctxGlobalVars;
98+
}
99+
97100
// ---------------------- Add variables and instances ----------------------
98101
public void addVarToContext(RefinedVariable var) {
99102
ctxVars.peek().add(var);
@@ -114,8 +117,8 @@ public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference<?
114117
CtElement placementInCode) {
115118
RefinedVariable vi = new VariableInstance(simpleName, type, c);
116119
vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode));
117-
if (!ctxSpecificVars.contains(vi))
118-
addSpecificVariable(vi);
120+
if (!ctxInstanceVars.contains(vi))
121+
addInstanceVariable(vi);
119122
return vi;
120123
}
121124

@@ -154,7 +157,7 @@ public RefinedVariable getVariableByName(String name) {
154157
return var;
155158
}
156159
}
157-
for (RefinedVariable var : ctxSpecificVars) {
160+
for (RefinedVariable var : ctxInstanceVars) {
158161
if (var.getName().equals(name))
159162
return var;
160163
}
@@ -188,7 +191,7 @@ public List<RefinedVariable> getAllVariablesWithSupertypes() {
188191
if (!rv.getSuperTypes().isEmpty())
189192
lvi.add(rv);
190193
}
191-
for (RefinedVariable rv : ctxSpecificVars) {
194+
for (RefinedVariable rv : ctxInstanceVars) {
192195
if (!rv.getSuperTypes().isEmpty())
193196
lvi.add(rv);
194197
}
@@ -204,7 +207,7 @@ public void addRefinementInstanceToVariable(String name, String instanceName) {
204207

205208
((Variable) vi1).addInstance((VariableInstance) vi2);
206209
((VariableInstance) vi2).setParent((Variable) vi1);
207-
addSpecificVariable(vi2);
210+
addInstanceVariable(vi2);
208211
}
209212

210213
public Optional<VariableInstance> getLastVariableInstance(String name) {
@@ -214,14 +217,30 @@ public Optional<VariableInstance> getLastVariableInstance(String name) {
214217
return ((Variable) rv).getLastInstance();
215218
}
216219

217-
public void addSpecificVariable(RefinedVariable vi) {
218-
if (!ctxSpecificVars.contains(vi)) {
219-
ctxSpecificVars.add(vi);
220+
public void addInstanceVariable(RefinedVariable vi) {
221+
if (!ctxInstanceVars.contains(vi)) {
222+
ctxInstanceVars.add(vi);
220223
CtTypeReference<?> type = vi.getType();
221224
vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
222225
}
223226
}
224227

228+
public Variable getVariableFromInstance(VariableInstance vi) {
229+
return vi.getParent().orElse(null);
230+
}
231+
232+
public List<RefinedVariable> getCtxVars() {
233+
List<RefinedVariable> lvi = new ArrayList<>();
234+
for (List<RefinedVariable> l : ctxVars) {
235+
lvi.addAll(l);
236+
}
237+
return lvi;
238+
}
239+
240+
public List<RefinedVariable> getCtxInstanceVars() {
241+
return ctxInstanceVars;
242+
}
243+
225244
// ---------------------- Variables - if information storing ----------------------
226245
public void variablesSetBeforeIf() {
227246
for (RefinedVariable vi : getAllVariables())
@@ -290,6 +309,10 @@ public List<RefinedFunction> getAllMethodsWithNameSize(String name, int size) {
290309
return l;
291310
}
292311

312+
public List<RefinedFunction> getCtxFunctions() {
313+
return ctxFunctions;
314+
}
315+
293316
// ---------------------- Ghost Predicates ----------------------
294317
public void addGhostFunction(GhostFunction gh) {
295318
ghosts.add(gh);
@@ -314,7 +337,7 @@ public List<GhostState> getGhostState(String s) {
314337
return classStates.get(s);
315338
}
316339

317-
public List<GhostState> getGhostState() {
340+
public List<GhostState> getGhostStates() {
318341
List<GhostState> lgs = new ArrayList<>();
319342
for (List<GhostState> l : classStates.values())
320343
lgs.addAll(l);
@@ -323,12 +346,12 @@ public List<GhostState> getGhostState() {
323346

324347
// ---------------------- Alias ----------------------
325348
public void addAlias(AliasWrapper aw) {
326-
if (!alias.contains(aw))
327-
alias.add(aw);
349+
if (!aliases.contains(aw))
350+
aliases.add(aw);
328351
}
329352

330-
public List<AliasWrapper> getAlias() {
331-
return alias;
353+
public List<AliasWrapper> getAliases() {
354+
return aliases;
332355
}
333356

334357
@Override
@@ -354,8 +377,4 @@ public String toString() {
354377
sb.append(f.toString());
355378
return sb.toString();
356379
}
357-
358-
public Variable getVariableFromInstance(VariableInstance vi) {
359-
return vi.getParent().orElse(null);
360-
}
361380
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
package liquidjava.processor.context;
2+
3+
import java.util.HashMap;
4+
import java.util.HashSet;
5+
import java.util.Map;
6+
import java.util.Set;
7+
8+
import spoon.reflect.cu.SourcePosition;
9+
import spoon.reflect.declaration.CtElement;
10+
import spoon.reflect.declaration.CtExecutable;
11+
12+
public class ContextHistory {
13+
private static ContextHistory instance;
14+
15+
private Map<String, Map<String, Set<RefinedVariable>>> fileScopeVars; // file -> (scope -> variables in scope)
16+
private Set<RefinedVariable> instanceVars;
17+
private Set<RefinedVariable> globalVars;
18+
private Set<GhostState> ghosts;
19+
private Set<AliasWrapper> aliases;
20+
21+
private ContextHistory() {
22+
fileScopeVars = new HashMap<>();
23+
instanceVars = new HashSet<>();
24+
globalVars = new HashSet<>();
25+
ghosts = new HashSet<>();
26+
aliases = new HashSet<>();
27+
}
28+
29+
public static ContextHistory getInstance() {
30+
if (instance == null)
31+
instance = new ContextHistory();
32+
return instance;
33+
}
34+
35+
public void clearHistory() {
36+
fileScopeVars.clear();
37+
instanceVars.clear();
38+
globalVars.clear();
39+
ghosts.clear();
40+
aliases.clear();
41+
}
42+
43+
public void saveContext(CtElement element, Context context) {
44+
SourcePosition pos = element.getPosition();
45+
if (pos == null || pos.getFile() == null)
46+
return;
47+
48+
// add variables in scope for this position
49+
String file = pos.getFile().getAbsolutePath();
50+
String scope = getScopePosition(element);
51+
fileScopeVars.putIfAbsent(file, new HashMap<>());
52+
fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars()));
53+
54+
// add other elements in context
55+
instanceVars.addAll(context.getCtxInstanceVars());
56+
globalVars.addAll(context.getCtxGlobalVars());
57+
ghosts.addAll(context.getGhostStates());
58+
aliases.addAll(context.getAliases());
59+
}
60+
61+
public String getScopePosition(CtElement element) {
62+
SourcePosition pos = element.getPosition();
63+
SourcePosition innerPosition = pos;
64+
if (element instanceof CtExecutable<?> executable) {
65+
if (executable.getBody() != null)
66+
innerPosition = executable.getBody().getPosition();
67+
}
68+
return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(),
69+
pos.getEndColumn());
70+
}
71+
72+
public Map<String, Map<String, Set<RefinedVariable>>> getFileScopeVars() {
73+
return fileScopeVars;
74+
}
75+
76+
public Set<RefinedVariable> getInstanceVars() {
77+
return instanceVars;
78+
}
79+
80+
public Set<RefinedVariable> getGlobalVars() {
81+
return globalVars;
82+
}
83+
84+
public Set<GhostState> getGhosts() {
85+
return ghosts;
86+
}
87+
88+
public Set<AliasWrapper> getAliases() {
89+
return aliases;
90+
}
91+
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,7 @@ public class RefinementTypeChecker extends TypeChecker {
5454
OperationsChecker otc;
5555
MethodsFunctionsChecker mfc;
5656
Diagnostics diagnostics = Diagnostics.getInstance();
57+
ContextHistory contextHistory = ContextHistory.getInstance();
5758

5859
public RefinementTypeChecker(Context context, Factory factory) {
5960
super(context, factory);
@@ -95,14 +96,15 @@ public <A extends Annotation> void visitCtAnnotationType(CtAnnotationType<A> ann
9596
}
9697

9798
@Override
98-
public <T> void visitCtConstructor(CtConstructor<T> c) {
99+
public <T> void visitCtConstructor(CtConstructor<T> constructor) {
99100
context.enterContext();
100-
mfc.loadFunctionInfo(c);
101+
mfc.loadFunctionInfo(constructor);
101102
try {
102-
super.visitCtConstructor(c);
103+
super.visitCtConstructor(constructor);
103104
} catch (LJError e) {
104105
diagnostics.add(e);
105106
}
107+
contextHistory.saveContext(constructor, context);
106108
context.exitContext();
107109
}
108110

@@ -116,6 +118,7 @@ public <R> void visitCtMethod(CtMethod<R> method) {
116118
} catch (LJError e) {
117119
diagnostics.add(e);
118120
}
121+
contextHistory.saveContext(method, context);
119122
context.exitContext();
120123
}
121124

@@ -334,6 +337,7 @@ public void visitCtIf(CtIf ifElement) {
334337
context.enterContext();
335338
visitCtBlock(ifElement.getThenStatement());
336339
context.variablesSetThenIf();
340+
contextHistory.saveContext(ifElement.getThenStatement(), context);
337341
context.exitContext();
338342

339343
// VISIT ELSE
@@ -345,6 +349,7 @@ public void visitCtIf(CtIf ifElement) {
345349
context.enterContext();
346350
visitCtBlock(ifElement.getElseStatement());
347351
context.variablesSetElseIf();
352+
contextHistory.saveContext(ifElement.getElseStatement(), context);
348353
context.exitContext();
349354
}
350355
// end

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -304,17 +304,17 @@ public void checkSMT(Predicate expectedType, CtElement element) throws LJError {
304304
}
305305

306306
public void checkSMT(Predicate expectedType, CtElement element, String customMessage) throws LJError {
307-
vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory, customMessage);
307+
vcChecker.processSubtyping(expectedType, context.getGhostStates(), element, factory, customMessage);
308308
element.putMetadata(Keys.REFINEMENT, expectedType);
309309
}
310310

311311
public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo)
312312
throws LJError {
313-
vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, factory);
313+
vcChecker.processSubtyping(prevState, expectedState, context.getGhostStates(), target, factory);
314314
}
315315

316316
public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError {
317-
SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostState(), p,
317+
SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p,
318318
factory);
319319
return result.isOk();
320320
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -197,7 +197,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
197197
Predicate newElemRef = elemRef.substituteVariable(Keys.WILDCARD, newName);
198198
RefinedVariable newVi = rtc.getContext().addVarToContext(newName, elemVar.getType(), newElemRef,
199199
elemVar);
200-
rtc.getContext().addSpecificVariable(newVi);
200+
rtc.getContext().addInstanceVariable(newVi);
201201
returnName = newName;
202202
}
203203

0 commit comments

Comments
 (0)