Skip to content

Commit 1b9d5ac

Browse files
cheestreecheestree
authored
Merge branch 'liquid-java:main' into main
2 parents 64fe267 + f8d3f3e commit 1b9d5ac

File tree

27 files changed

+382
-249
lines changed

27 files changed

+382
-249
lines changed

‎liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/Test.java‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
package testSuite.classes.overload_constructors_correct;
2+
3+
public class Test{
4+
void test3(){
5+
Throwable t = new Throwable("Example");
6+
t.initCause(null);
7+
t.getCause();
8+
}
9+
10+
void test4(){
11+
Throwable originT = new Throwable();
12+
Throwable t = new Throwable(originT);
13+
t.getCause();
14+
}
15+
16+
}

‎liquidjava-example/src/main/java/testSuite/classes/overload_constructors_correct/ThrowableRefinements.java‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
package testSuite.classes.overload_constructors_correct;
2+
3+
import liquidjava.specification.StateSet;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.ExternalRefinementsFor;
6+
7+
@StateSet({"start", "hasMessage", "hasCause"})
8+
@ExternalRefinementsFor("java.lang.Throwable")
9+
public interface ThrowableRefinements {
10+
11+
// ##### Constructors #######
12+
@StateRefinement(to="hasMessage(this)")
13+
public void Throwable(String message);
14+
15+
@StateRefinement(to="hasCause(this)")
16+
public void Throwable(Throwable cause);
17+
18+
@StateRefinement(from="!hasCause(this)", to="hasCause(this)")
19+
public Throwable initCause(Throwable cause);
20+
}

‎liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/.expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
State Refinement Error

‎liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/Test.java‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite.classes.overload_constructors_error;
2+
3+
public class Test{
4+
void test3(){
5+
Throwable t = new Throwable("Example");
6+
t.initCause(null);
7+
t.getCause();
8+
}
9+
10+
void test4(){
11+
Throwable originT = new Throwable();
12+
Throwable t = new Throwable(originT);
13+
t.initCause(null);// should be an error but its not
14+
t.getCause();
15+
}
16+
17+
}

‎liquidjava-example/src/main/java/testSuite/classes/overload_constructors_error/ThrowableRefinements.java‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
package testSuite.classes.overload_constructors_error;
2+
3+
import liquidjava.specification.StateSet;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.ExternalRefinementsFor;
6+
7+
@StateSet({"start", "hasMessage", "hasCause"})
8+
@ExternalRefinementsFor("java.lang.Throwable")
9+
public interface ThrowableRefinements {
10+
11+
// ##### Constructors #######
12+
@StateRefinement(to="hasMessage(this)")
13+
public void Throwable(String message);
14+
15+
@StateRefinement(to="hasCause(this)")
16+
public void Throwable(Throwable cause);
17+
18+
@StateRefinement(from="!hasCause(this)", to="hasCause(this)")
19+
public Throwable initCause(Throwable cause);
20+
}

‎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: 12 additions & 12 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()
@@ -129,7 +129,7 @@ public String getSnippet() {
129129

130130
// line number padding + pipe + column offset
131131
String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
132-
+ " ".repeat(visualColStart - 1);
132+
+ " ".repeat(visualColStart - 1);
133133
String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
134134
sb.append(indent).append(markers);
135135

‎liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java‎

Lines changed: 21 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
package liquidjava.diagnostics.errors;
22

3+
import java.util.ArrayList;
4+
import java.util.List;
5+
import java.util.stream.Collectors;
6+
37
import liquidjava.diagnostics.TranslationTable;
48
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
59
import liquidjava.smt.Counterexample;
@@ -27,22 +31,30 @@ public RefinementError(SourcePosition position, ValDerivationNode expected, ValD
2731

2832
@Override
2933
public String getDetails() {
30-
return "Counterexample: " + getCounterExampleString();
34+
String counterexampleString = getCounterExampleString();
35+
if (counterexampleString == null)
36+
return "";
37+
return "Counterexample: " + counterexampleString;
3138
}
3239

3340
public String getCounterExampleString() {
3441
if (counterexample == null || counterexample.assignments().isEmpty())
35-
return "";
42+
return null;
3643

37-
// filter fresh variables and join assignements with &&
38-
String counterexampleExp = counterexample.assignments().stream().filter(a -> !a.startsWith("#fresh_"))
39-
.reduce((a, b) -> a + " && " + b).orElse("");
44+
List<String> foundVarNames = new ArrayList<>();
45+
found.getValue().getVariableNames(foundVarNames);
46+
String counterexampleString = counterexample.assignments().stream()
47+
// only include variables that appear in the found value
48+
.filter(a -> foundVarNames.contains(a.first()))
49+
// format as "var == value"
50+
.map(a -> a.first() + " == " + a.second())
51+
// join with "&&"
52+
.collect(Collectors.joining(" && "));
4053

41-
// check if counterexample is trivial (same as the found value)
42-
if (counterexampleExp.equals(found.getValue().toString()))
43-
return "";
54+
if (counterexampleString.isEmpty() || counterexampleString.equals(found.getValue().toString()))
55+
return null;
4456

45-
return counterexampleExp;
57+
return counterexampleString;
4658
}
4759

4860
public Counterexample getCounterexample() {

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

Lines changed: 39 additions & 30 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 : getAllVariables())
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 : getAllVariables())
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

@@ -172,22 +171,9 @@ public boolean hasVariable(String name) {
172171
return getVariableByName(name) != null;
173172
}
174173

175-
/**
176-
* Lists all variables inside the stack
177-
*
178-
* @return list of all variables
179-
*/
180-
public List<RefinedVariable> getAllVariables() {
181-
List<RefinedVariable> lvi = new ArrayList<>();
182-
for (List<RefinedVariable> l : ctxVars) {
183-
lvi.addAll(l);
184-
}
185-
return lvi;
186-
}
187-
188174
public List<RefinedVariable> getAllVariablesWithSupertypes() {
189175
List<RefinedVariable> lvi = new ArrayList<>();
190-
for (RefinedVariable rv : getAllVariables()) {
176+
for (RefinedVariable rv : getCtxVars()) {
191177
if (!rv.getSuperTypes().isEmpty())
192178
lvi.add(rv);
193179
}
@@ -243,37 +229,37 @@ public List<RefinedVariable> getCtxInstanceVars() {
243229

244230
// ---------------------- Variables - if information storing ----------------------
245231
public void variablesSetBeforeIf() {
246-
for (RefinedVariable vi : getAllVariables())
232+
for (RefinedVariable vi : getCtxVars())
247233
if (vi instanceof Variable)
248234
((Variable) vi).saveInstanceBeforeIf();
249235
}
250236

251237
public void variablesSetThenIf() {
252-
for (RefinedVariable vi : getAllVariables())
238+
for (RefinedVariable vi : getCtxVars())
253239
if (vi instanceof Variable)
254240
((Variable) vi).saveInstanceThen();
255241
}
256242

257243
public void variablesSetElseIf() {
258-
for (RefinedVariable vi : getAllVariables())
244+
for (RefinedVariable vi : getCtxVars())
259245
if (vi instanceof Variable)
260246
((Variable) vi).saveInstanceElse();
261247
}
262248

263249
public void variablesNewIfCombination() {
264-
for (RefinedVariable vi : getAllVariables())
250+
for (RefinedVariable vi : getCtxVars())
265251
if (vi instanceof Variable)
266252
((Variable) vi).newIfCombination();
267253
}
268254

269255
public void variablesFinishIfCombination() {
270-
for (RefinedVariable vi : getAllVariables())
256+
for (RefinedVariable vi : getCtxVars())
271257
if (vi instanceof Variable)
272258
((Variable) vi).finishIfCombination();
273259
}
274260

275261
public void variablesCombineFromIf(Predicate cond) {
276-
for (RefinedVariable vi : getAllVariables()) {
262+
for (RefinedVariable vi : getCtxVars()) {
277263
if (vi instanceof Variable) {
278264
Optional<VariableInstance> ovi = ((Variable) vi).getIfInstanceCombination(getCounter(), cond);
279265
if (ovi.isPresent()) {
@@ -300,6 +286,29 @@ public RefinedFunction getFunction(String name, String target, int size) {
300286
return null;
301287
}
302288

289+
public RefinedFunction getFunction(String name, String target, List<CtTypeReference<?>> paramTypes) {
290+
for (RefinedFunction fi : ctxFunctions) {
291+
if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target)
292+
&& argumentTypesMatch(fi.getArguments(), paramTypes))
293+
return fi;
294+
}
295+
return getFunction(name, target, paramTypes.size());
296+
}
297+
298+
private boolean argumentTypesMatch(List<Variable> args, List<CtTypeReference<?>> paramTypes) {
299+
if (args.size() != paramTypes.size())
300+
return false;
301+
for (int i = 0; i < args.size(); i++) {
302+
CtTypeReference<?> argType = args.get(i).getType();
303+
CtTypeReference<?> paramType = paramTypes.get(i);
304+
if (argType == null || paramType == null)
305+
return false;
306+
if (!argType.getQualifiedName().equals(paramType.getQualifiedName()))
307+
return false;
308+
}
309+
return true;
310+
}
311+
303312
public List<RefinedFunction> getAllMethodsWithNameSize(String name, int size) {
304313
List<RefinedFunction> l = new ArrayList<>();
305314
for (RefinedFunction fi : ctxFunctions) {

0 commit comments

Comments
 (0)