Skip to content

Commit aa34a81

Browse files
rcosta358rcosta358
committed
Save Context History
1 parent 375418d commit aa34a81

File tree

11 files changed

+149
-48
lines changed

11 files changed

+149
-48
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: 53 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -8,27 +8,26 @@
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;
16-
private Map<String, List<GhostState>> classStates;
17-
private List<AliasWrapper> alias;
15+
private Map<String, List<GhostState>> states;
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<>();
31-
classStates = new HashMap<>();
30+
states = new HashMap<>();
3231
counter = 0;
3332
}
3433

@@ -41,15 +40,15 @@ 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<>();
52-
classStates = new HashMap<>();
51+
states = new HashMap<>();
5352
counter = 0;
5453
}
5554

@@ -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);
@@ -300,35 +323,35 @@ public List<GhostFunction> getGhosts() {
300323
}
301324

302325
public void addGhostClass(String klass) {
303-
if (!classStates.containsKey(klass))
304-
classStates.put(klass, new ArrayList<>());
326+
if (!states.containsKey(klass))
327+
states.put(klass, new ArrayList<>());
305328
}
306329

307330
public void addToGhostClass(String klass, GhostState gs) {
308-
List<GhostState> l = classStates.get(klass);
331+
List<GhostState> l = states.get(klass);
309332
if (!l.contains(gs))
310333
l.add(gs);
311334
}
312335

313336
public List<GhostState> getGhostState(String s) {
314-
return classStates.get(s);
337+
return states.get(s);
315338
}
316339

317-
public List<GhostState> getGhostState() {
340+
public List<GhostState> getGhostStates() {
318341
List<GhostState> lgs = new ArrayList<>();
319-
for (List<GhostState> l : classStates.values())
342+
for (List<GhostState> l : states.values())
320343
lgs.addAll(l);
321344
return lgs;
322345
}
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: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
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+
11+
public class ContextHistory {
12+
private static ContextHistory instance;
13+
14+
private Map<String, Set<RefinedVariable>> vars; // scope -> variables in scope
15+
private Set<RefinedVariable> instanceVars;
16+
private Set<RefinedVariable> globalVars;
17+
private Set<GhostState> ghosts;
18+
private Set<AliasWrapper> aliases;
19+
20+
private ContextHistory() {
21+
vars = new HashMap<>();
22+
instanceVars = new HashSet<>();
23+
globalVars = new HashSet<>();
24+
ghosts = new HashSet<>();
25+
aliases = new HashSet<>();
26+
}
27+
28+
public static ContextHistory getInstance() {
29+
if (instance == null)
30+
instance = new ContextHistory();
31+
return instance;
32+
}
33+
34+
public void clearHistory() {
35+
vars.clear();
36+
instanceVars.clear();
37+
globalVars.clear();
38+
ghosts.clear();
39+
aliases.clear();
40+
}
41+
42+
public void saveContext(CtElement element, Context context) {
43+
SourcePosition pos = element.getPosition();
44+
if (pos == null || pos.getFile() == null)
45+
return;
46+
47+
String scope = String.format("%s:%d:%d", pos.getFile().getName(), pos.getLine(), pos.getColumn());
48+
vars.put(scope, new HashSet<>(context.getCtxVars()));
49+
instanceVars.addAll(context.getCtxInstanceVars());
50+
globalVars.addAll(context.getCtxGlobalVars());
51+
ghosts.addAll(context.getGhostStates());
52+
aliases.addAll(context.getAliases());
53+
}
54+
55+
public Map<String, Set<RefinedVariable>> getVars() {
56+
return vars;
57+
}
58+
59+
public Set<RefinedVariable> getInstanceVars() {
60+
return instanceVars;
61+
}
62+
63+
public Set<RefinedVariable> getGlobalVars() {
64+
return globalVars;
65+
}
66+
67+
public Set<GhostState> getGhosts() {
68+
return ghosts;
69+
}
70+
71+
public Set<AliasWrapper> getAliases() {
72+
return aliases;
73+
}
74+
}

‎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

0 commit comments

Comments
 (0)