Skip to content

Commit f8d3f3e

Browse files
rcosta358rcosta358
authored
Context History Improvements (#159)
1 parent 1d79229 commit f8d3f3e

14 files changed

Lines changed: 140 additions & 96 deletions

File tree

‎liquidjava-verifier/pom.xml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@
1111

1212
<groupId>io.github.liquid-java</groupId>
1313
<artifactId>liquidjava-verifier</artifactId>
14-
<version>0.0.14</version>
14+
<version>0.0.16</version>
1515
<name>liquidjava-verifier</name>
1616
<description>LiquidJava Verifier</description>
1717
<url>https://github.com/liquid-java/liquidjava</url>

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java‎

Lines changed: 0 additions & 12 deletions
This file was deleted.

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -13,14 +13,14 @@ public class LJDiagnostic extends RuntimeException {
1313
private final String accentColor;
1414
private final String customMessage;
1515
private String file;
16-
private ErrorPosition position;
16+
private SourcePosition position;
1717
private static final String PIPE = " | ";
1818

1919
public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) {
2020
this.title = title;
2121
this.message = message;
2222
this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null;
23-
this.position = ErrorPosition.fromSpoonPosition(pos);
23+
this.position = pos;
2424
this.accentColor = accentColor;
2525
this.customMessage = customMessage;
2626
}
@@ -41,14 +41,14 @@ public String getDetails() {
4141
return ""; // to be overridden by subclasses
4242
}
4343

44-
public ErrorPosition getPosition() {
44+
public SourcePosition getPosition() {
4545
return position;
4646
}
4747

4848
public void setPosition(SourcePosition pos) {
49-
if (pos == null)
49+
if (pos == null || pos.getFile() == null)
5050
return;
51-
this.position = ErrorPosition.fromSpoonPosition(pos);
51+
this.position = pos;
5252
this.file = pos.getFile().getPath();
5353
}
5454

@@ -82,7 +82,7 @@ public String toString() {
8282

8383
// location
8484
if (file != null && position != null) {
85-
sb.append("\n").append(file).append(":").append(position.lineStart()).append(Colors.RESET).append("\n");
85+
sb.append("\n").append(file).append(":").append(position.getLine()).append(Colors.RESET).append("\n");
8686
}
8787

8888
return sb.toString();
@@ -100,8 +100,8 @@ public String getSnippet() {
100100
// before and after lines for context
101101
int contextBefore = 2;
102102
int contextAfter = 2;
103-
int startLine = Math.max(1, position.lineStart() - contextBefore);
104-
int endLine = Math.min(lines.size(), position.lineEnd() + contextAfter);
103+
int startLine = Math.max(1, position.getLine() - contextBefore);
104+
int endLine = Math.min(lines.size(), position.getEndLine() + contextAfter);
105105

106106
// calculate padding for line numbers
107107
int padding = String.valueOf(endLine).length();
@@ -115,9 +115,9 @@ public String getSnippet() {
115115
sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n");
116116

117117
// add error markers on the line(s) with the error
118-
if (i >= position.lineStart() && i <= position.lineEnd()) {
119-
int colStart = (i == position.lineStart()) ? position.colStart() : 1;
120-
int colEnd = (i == position.lineEnd()) ? position.colEnd() : rawLine.length();
118+
if (i >= position.getLine() && i <= position.getEndLine()) {
119+
int colStart = (i == position.getLine()) ? position.getColumn() : 1;
120+
int colEnd = (i == position.getEndLine()) ? position.getEndColumn() : rawLine.length();
121121

122122
if (colStart > 0 && colEnd > 0) {
123123
int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars()

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

Lines changed: 17 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -55,15 +55,15 @@ public void reinitializeAllContext() {
5555
public void enterContext() {
5656
ctxVars.push(new ArrayList<>());
5757
// make each variable enter context
58-
for (RefinedVariable vi : getAllCtxVars())
58+
for (RefinedVariable vi : getCtxVars())
5959
if (vi instanceof Variable)
6060
((Variable) vi).enterContext();
6161
}
6262

6363
public void exitContext() {
6464
ctxVars.pop();
6565
// make each variable exit context
66-
for (RefinedVariable vi : getAllCtxVars())
66+
for (RefinedVariable vi : getCtxVars())
6767
if (vi instanceof Variable)
6868
((Variable) vi).exitContext();
6969
}
@@ -104,32 +104,31 @@ public void addVarToContext(RefinedVariable var) {
104104
var.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
105105
}
106106

107-
public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> type, Predicate c,
108-
CtElement placementInCode) {
107+
public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> type, Predicate c, CtElement element) {
109108
RefinedVariable vi = new Variable(simpleName, type, c);
110-
vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode));
109+
vi.setPlacementInCode(element);
111110
vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
112111
addVarToContext(vi);
113112
return vi;
114113
}
115114

116115
public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference<?> type, Predicate c,
117-
CtElement placementInCode) {
116+
CtElement element) {
118117
RefinedVariable vi = new VariableInstance(simpleName, type, c);
119-
vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode));
118+
vi.setPlacementInCode(element);
120119
if (!ctxInstanceVars.contains(vi))
121120
addInstanceVariable(vi);
122121
return vi;
123122
}
124123

125124
public void addRefinementToVariableInContext(String name, CtTypeReference<?> type, Predicate et,
126-
CtElement placementInCode) {
125+
CtElement element) {
127126
if (hasVariable(name)) {
128127
RefinedVariable vi = getVariableByName(name);
129128
vi.setRefinement(et);
130-
vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode));
129+
vi.setPlacementInCode(element);
131130
} else {
132-
addVarToContext(name, type, et, placementInCode);
131+
addVarToContext(name, type, et, element);
133132
}
134133
}
135134

@@ -174,7 +173,7 @@ public boolean hasVariable(String name) {
174173

175174
public List<RefinedVariable> getAllVariablesWithSupertypes() {
176175
List<RefinedVariable> lvi = new ArrayList<>();
177-
for (RefinedVariable rv : getAllCtxVars()) {
176+
for (RefinedVariable rv : getCtxVars()) {
178177
if (!rv.getSuperTypes().isEmpty())
179178
lvi.add(rv);
180179
}
@@ -216,7 +215,7 @@ public Variable getVariableFromInstance(VariableInstance vi) {
216215
return vi.getParent().orElse(null);
217216
}
218217

219-
public List<RefinedVariable> getAllCtxVars() {
218+
public List<RefinedVariable> getCtxVars() {
220219
List<RefinedVariable> lvi = new ArrayList<>();
221220
for (List<RefinedVariable> l : ctxVars) {
222221
lvi.addAll(l);
@@ -230,37 +229,37 @@ public List<RefinedVariable> getCtxInstanceVars() {
230229

231230
// ---------------------- Variables - if information storing ----------------------
232231
public void variablesSetBeforeIf() {
233-
for (RefinedVariable vi : getAllCtxVars())
232+
for (RefinedVariable vi : getCtxVars())
234233
if (vi instanceof Variable)
235234
((Variable) vi).saveInstanceBeforeIf();
236235
}
237236

238237
public void variablesSetThenIf() {
239-
for (RefinedVariable vi : getAllCtxVars())
238+
for (RefinedVariable vi : getCtxVars())
240239
if (vi instanceof Variable)
241240
((Variable) vi).saveInstanceThen();
242241
}
243242

244243
public void variablesSetElseIf() {
245-
for (RefinedVariable vi : getAllCtxVars())
244+
for (RefinedVariable vi : getCtxVars())
246245
if (vi instanceof Variable)
247246
((Variable) vi).saveInstanceElse();
248247
}
249248

250249
public void variablesNewIfCombination() {
251-
for (RefinedVariable vi : getAllCtxVars())
250+
for (RefinedVariable vi : getCtxVars())
252251
if (vi instanceof Variable)
253252
((Variable) vi).newIfCombination();
254253
}
255254

256255
public void variablesFinishIfCombination() {
257-
for (RefinedVariable vi : getAllCtxVars())
256+
for (RefinedVariable vi : getCtxVars())
258257
if (vi instanceof Variable)
259258
((Variable) vi).finishIfCombination();
260259
}
261260

262261
public void variablesCombineFromIf(Predicate cond) {
263-
for (RefinedVariable vi : getAllCtxVars()) {
262+
for (RefinedVariable vi : getCtxVars()) {
264263
if (vi instanceof Variable) {
265264
Optional<VariableInstance> ovi = ((Variable) vi).getIfInstanceCombination(getCounter(), cond);
266265
if (ovi.isPresent()) {

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

Lines changed: 27 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -5,22 +5,22 @@
55
import java.util.Map;
66
import java.util.Set;
77

8+
import liquidjava.utils.Utils;
89
import spoon.reflect.cu.SourcePosition;
910
import spoon.reflect.declaration.CtElement;
10-
import spoon.reflect.declaration.CtExecutable;
1111

1212
public class ContextHistory {
1313
private static ContextHistory instance;
1414

15-
private Map<String, Map<String, Set<RefinedVariable>>> fileScopeVars; // file -> (scope -> variables in scope)
16-
private Set<RefinedVariable> instanceVars;
17-
private Set<RefinedVariable> globalVars;
15+
private Map<String, Set<String>> fileScopes;
16+
private Set<RefinedVariable> localVars;
1817
private Set<GhostState> ghosts;
1918
private Set<AliasWrapper> aliases;
19+
private Set<RefinedVariable> globalVars;
2020

2121
private ContextHistory() {
22-
fileScopeVars = new HashMap<>();
23-
instanceVars = new HashSet<>();
22+
fileScopes = new HashMap<>();
23+
localVars = new HashSet<>();
2424
globalVars = new HashSet<>();
2525
ghosts = new HashSet<>();
2626
aliases = new HashSet<>();
@@ -33,48 +33,40 @@ public static ContextHistory getInstance() {
3333
}
3434

3535
public void clearHistory() {
36-
fileScopeVars.clear();
37-
instanceVars.clear();
36+
fileScopes.clear();
37+
localVars.clear();
3838
globalVars.clear();
3939
ghosts.clear();
4040
aliases.clear();
4141
}
4242

4343
public void saveContext(CtElement element, Context context) {
44-
SourcePosition pos = element.getPosition();
45-
if (pos == null || pos.getFile() == null)
44+
String file = Utils.getFile(element);
45+
if (file == null)
4646
return;
4747

48-
// add variables in scope for this position
49-
String file = pos.getFile().getAbsolutePath();
48+
// add scope
5049
String scope = getScopePosition(element);
51-
fileScopeVars.putIfAbsent(file, new HashMap<>());
52-
fileScopeVars.get(file).put(scope, new HashSet<>(context.getAllCtxVars()));
50+
fileScopes.putIfAbsent(file, new HashSet<>());
51+
fileScopes.get(file).add(scope);
5352

54-
// add other elements in context
55-
instanceVars.addAll(context.getCtxInstanceVars());
53+
// add variables, ghosts and aliases
54+
localVars.addAll(context.getCtxVars());
55+
localVars.addAll(context.getCtxInstanceVars());
5656
globalVars.addAll(context.getCtxGlobalVars());
5757
ghosts.addAll(context.getGhostStates());
5858
aliases.addAll(context.getAliases());
5959
}
6060

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;
61+
private String getScopePosition(CtElement element) {
62+
SourcePosition startPos = Utils.getRealPosition(element);
63+
SourcePosition endPos = element.getPosition();
64+
return String.format("%d:%d-%d:%d", startPos.getLine(), startPos.getColumn(), endPos.getEndLine(),
65+
endPos.getEndColumn() - 1);
7466
}
7567

76-
public Set<RefinedVariable> getInstanceVars() {
77-
return instanceVars;
68+
public Set<RefinedVariable> getLocalVars() {
69+
return localVars;
7870
}
7971

8072
public Set<RefinedVariable> getGlobalVars() {
@@ -88,4 +80,8 @@ public Set<GhostState> getGhosts() {
8880
public Set<AliasWrapper> getAliases() {
8981
return aliases;
9082
}
83+
84+
public Map<String, Set<String>> getFileScopes() {
85+
return fileScopes;
86+
}
9187
}

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

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,12 @@ public class GhostState extends GhostFunction {
88

99
private GhostFunction parent;
1010
private Predicate refinement;
11+
private final String file;
1112

12-
public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> returnType, String prefix) {
13+
public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> returnType, String prefix,
14+
String file) {
1315
super(name, list, returnType, prefix);
16+
this.file = file;
1417
}
1518

1619
public void setGhostParent(GhostFunction parent) {
@@ -28,4 +31,8 @@ public GhostFunction getParent() {
2831
public Predicate getRefinement() {
2932
return refinement;
3033
}
34+
35+
public String getFile() {
36+
return file;
37+
}
3138
}

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

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
package liquidjava.processor.context;
22

33
import java.lang.annotation.Annotation;
4+
5+
import liquidjava.utils.Utils;
46
import spoon.reflect.code.CtComment;
57
import spoon.reflect.cu.SourcePosition;
68
import spoon.reflect.declaration.CtAnnotation;
@@ -9,10 +11,12 @@
911
public class PlacementInCode {
1012
private final String text;
1113
private final SourcePosition position;
14+
private final SourcePosition annotationPosition;
1215

13-
private PlacementInCode(String text, SourcePosition pos) {
16+
private PlacementInCode(String text, SourcePosition pos, SourcePosition annotationPosition) {
1417
this.text = text;
1518
this.position = pos;
19+
this.annotationPosition = annotationPosition;
1620
}
1721

1822
public String getText() {
@@ -23,6 +27,10 @@ public SourcePosition getPosition() {
2327
return position;
2428
}
2529

30+
public SourcePosition getAnnotationPosition() {
31+
return annotationPosition;
32+
}
33+
2634
public static PlacementInCode createPlacement(CtElement elem) {
2735
CtElement elemCopy = elem.clone();
2836
// cleanup annotations
@@ -38,7 +46,8 @@ public static PlacementInCode createPlacement(CtElement elem) {
3846
}
3947
}
4048
String elemText = elemCopy.toString();
41-
return new PlacementInCode(elemText, elem.getPosition());
49+
SourcePosition annotationPosition = Utils.getFirstLJAnnotationPosition(elem);
50+
return new PlacementInCode(elemText, elem.getPosition(), annotationPosition);
4251
}
4352

4453
public String toString() {

0 commit comments

Comments
 (0)