Skip to content

Commit ea9d845

Browse files
rcosta358rcosta358
committed
Validate Ghost Invocations Before Sending to SMT
- Validate ghost invocations instead of relying on Z3 output - Throw LJErrors in AST expressions
1 parent 5880d83 commit ea9d845

28 files changed

+244
-196
lines changed

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

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -55,11 +55,10 @@ public void clear() {
5555
}
5656

5757
public String getErrorOutput() {
58-
return String.join("\n", errors.stream().map(LJError::toString).toList()) + (errors.isEmpty() ? "" : "\n");
58+
return String.join("\n", errors.stream().map(LJError::toString).toList());
5959
}
6060

6161
public String getWarningOutput() {
62-
return String.join("\n", warnings.stream().map(LJWarning::toString).toList())
63-
+ (warnings.isEmpty() ? "" : "\n");
62+
return String.join("\n", warnings.stream().map(LJWarning::toString).toList());
6463
}
6564
}

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

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -12,15 +12,14 @@
1212
public class NotFoundError extends LJError {
1313

1414
private final String name;
15-
private final String kind; // "Variable" or "Ghost"
15+
private final String kind; // "Variable" | "Ghost" | "Alias"
1616

17-
public NotFoundError(String message, String name, String kind) {
18-
this(message, null, name, kind, null);
17+
public NotFoundError(String name, String kind) {
18+
this(null, name, kind, null);
1919
}
2020

21-
public NotFoundError(String message, SourcePosition position, String name, String kind,
22-
TranslationTable translationTable) {
23-
super("Not Found Error", message, position, translationTable);
21+
public NotFoundError(SourcePosition position, String name, String kind, TranslationTable translationTable) {
22+
super("Not Found Error", String.format("%s '%s' not found", kind, name), position, translationTable);
2423
this.name = Utils.getSimpleName(name);
2524
this.kind = kind;
2625
}

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -35,14 +35,14 @@
3535

3636
public abstract class TypeChecker extends CtScanner {
3737

38-
Context context;
39-
Factory factory;
40-
VCChecker vcChecker;
38+
protected final Context context;
39+
protected final Factory factory;
40+
protected final VCChecker vcChecker;
4141

4242
public TypeChecker(Context context, Factory factory) {
4343
this.context = context;
4444
this.factory = factory;
45-
vcChecker = new VCChecker();
45+
this.vcChecker = new VCChecker();
4646
}
4747

4848
public Context getContext() {
@@ -296,16 +296,16 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour
296296
return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory);
297297
}
298298

299-
public void createError(SourcePosition position, Predicate expectedType, Predicate foundType) throws LJError {
300-
vcChecker.raiseSubtypingError(position, expectedType, foundType);
299+
public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType)
300+
throws LJError {
301+
vcChecker.throwRefinementError(position, expectedType, foundType);
301302
}
302303

303-
public void createSameStateError(SourcePosition position, Predicate expectedType, String klass) throws LJError {
304-
vcChecker.raiseSameStateError(position, expectedType);
304+
public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected) throws LJError {
305+
vcChecker.throwStateRefinementError(position, found, expected);
305306
}
306307

307-
public void createStateMismatchError(SourcePosition position, String method, Predicate found, Predicate expected)
308-
throws LJError {
309-
vcChecker.raiseStateMismatchError(position, found, expected);
308+
public void throwStateConflictError(SourcePosition position, Predicate expectedType) throws LJError {
309+
vcChecker.throwStateConflictError(position, expectedType);
310310
}
311311
}

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

Lines changed: 69 additions & 86 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
import liquidjava.processor.context.*;
1414
import liquidjava.rj_language.Predicate;
1515
import liquidjava.smt.SMTEvaluator;
16-
import liquidjava.smt.errors.TypeCheckError;
16+
import liquidjava.smt.TypeCheckError;
1717
import liquidjava.utils.constants.Keys;
1818
import spoon.reflect.cu.SourcePosition;
1919
import spoon.reflect.declaration.CtElement;
@@ -39,30 +39,64 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
3939
TranslationTable map = new TranslationTable();
4040
String[] s = { Keys.WILDCARD, Keys.THIS };
4141
Predicate premisesBeforeChange = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
42-
Predicate premises = new Predicate();
43-
Predicate et;
42+
Predicate premises;
43+
Predicate expected;
4444
try {
4545
List<GhostState> filtered = filterGhostStatesForVariables(list, mainVars, lrv);
4646
premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
47-
et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
47+
expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
4848
} catch (LJError e) {
4949
// add location info to error
5050
e.setPosition(element.getPosition());
5151
throw e;
5252
}
53-
try {
54-
smtChecking(premises, et);
55-
} catch (Exception e) {
56-
// To emit the message we use the constraints before the alias and state change
57-
raiseError(e, element.getPosition(), premisesBeforeChange, expectedType, map);
58-
}
53+
boolean isSubtype = smtChecks(expected, premises, element.getPosition());
54+
if (!isSubtype)
55+
throw new RefinementError(element.getPosition(), expectedType.getExpression(),
56+
premisesBeforeChange.simplify(), map);
5957
}
6058

59+
/**
60+
* Check that type is a subtype of expectedType Throws RefinementError otherwise
61+
*
62+
* @param type
63+
* @param expectedType
64+
* @param list
65+
* @param element
66+
* @param f
67+
*
68+
* @throws LJError
69+
*/
6170
public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, CtElement element,
6271
Factory f) throws LJError {
6372
boolean b = canProcessSubtyping(type, expectedType, list, element.getPosition(), f);
6473
if (!b)
65-
raiseSubtypingError(element.getPosition(), expectedType, type);
74+
throwRefinementError(element.getPosition(), expectedType, type);
75+
}
76+
77+
/**
78+
* Checks the expected against the found constraint
79+
*
80+
* @param expected
81+
* @param found
82+
* @param position
83+
*
84+
* @return true if expected type is subtype of found type, false otherwise
85+
*
86+
* @throws LJError
87+
*/
88+
public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError {
89+
try {
90+
new SMTEvaluator().verifySubtype(found, expected, context);
91+
return true;
92+
} catch (TypeCheckError e) {
93+
return false;
94+
} catch (LJError e) {
95+
e.setPosition(position);
96+
throw e;
97+
} catch (Exception e) {
98+
throw new CustomError(e.getMessage(), position);
99+
}
66100
}
67101

68102
public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list,
@@ -75,23 +109,14 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
75109

76110
TranslationTable map = new TranslationTable();
77111
String[] s = { Keys.WILDCARD, Keys.THIS };
78-
79-
Predicate premises;
80-
Predicate et;
81-
try {
82-
premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
83-
List<GhostState> filtered = filterGhostStatesForVariables(list, mainVars, lrv);
84-
premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s)
85-
.changeAliasToRefinement(context, f);
86-
et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
87-
} catch (LJError e) {
88-
// add location info to error
89-
e.setPosition(position);
90-
throw e;
91-
} catch (Exception e) {
92-
return false;
93-
}
94-
return smtChecks(et, premises, position, map);
112+
Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
113+
List<GhostState> filtered = filterGhostStatesForVariables(list, mainVars, lrv);
114+
premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s)
115+
.changeAliasToRefinement(context, f);
116+
Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
117+
118+
// check subtyping
119+
return smtChecks(expected, premises, position);
95120
}
96121

97122
/**
@@ -196,7 +221,6 @@ private List<RefinedVariable> getVariables(Predicate c, String varName) {
196221
getVariablesFromContext(c.getVariableNames(), allVars, varName);
197222
List<String> pathNames = pathVariables.stream().map(Refined::getName).collect(Collectors.toList());
198223
getVariablesFromContext(pathNames, allVars, "");
199-
200224
return allVars;
201225
}
202226

@@ -217,30 +241,6 @@ private void recAuxGetVars(RefinedVariable var, List<RefinedVariable> newVars) {
217241
getVariablesFromContext(l, newVars, varName);
218242
}
219243

220-
public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position, TranslationTable map)
221-
throws LJError {
222-
try {
223-
new SMTEvaluator().verifySubtype(found, expected, context);
224-
} catch (TypeCheckError e) {
225-
return false;
226-
} catch (Exception e) {
227-
raiseError(e, position, found, expected, map);
228-
}
229-
return true;
230-
}
231-
232-
/**
233-
* Checks the expectedType against the cSMT constraint. If the types do not check and error is sent and the program
234-
* ends
235-
*
236-
* @param cSMT
237-
* @param expectedType
238-
*
239-
*/
240-
private void smtChecking(Predicate cSMT, Predicate expectedType) throws Exception {
241-
new SMTEvaluator().verifySubtype(cSMT, expectedType, context);
242-
}
243-
244244
public void addPathVariable(RefinedVariable rv) {
245245
pathVariables.add(rv);
246246
}
@@ -256,53 +256,36 @@ void removePathVariableThatIncludes(String otherVar) {
256256

257257
// Errors---------------------------------------------------------------------------------------------------
258258

259-
private TranslationTable createMap(Predicate expectedType) {
259+
protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found)
260+
throws RefinementError {
260261
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
261-
gatherVariables(expectedType, lrv, mainVars);
262+
gatherVariables(expected, lrv, mainVars);
263+
gatherVariables(found, lrv, mainVars);
262264
TranslationTable map = new TranslationTable();
263-
joinPredicates(expectedType, mainVars, lrv, map);
264-
return map;
265-
}
266-
267-
protected void raiseError(Exception e, SourcePosition position, Predicate found, Predicate expected,
268-
TranslationTable map) throws LJError {
269-
if (e instanceof TypeCheckError) {
270-
throw new RefinementError(position, expected.getExpression(), found.simplify(), map);
271-
} else if (e instanceof liquidjava.smt.errors.NotFoundError nfe) {
272-
throw new NotFoundError(e.getMessage(), position, nfe.getName(), nfe.getKind(), map);
273-
} else {
274-
String msg = e.getLocalizedMessage().toLowerCase();
275-
if (msg.contains("wrong number of arguments")) {
276-
throw new ArgumentMismatchError("Wrong number of arguments in ghost invocation", position, map);
277-
} else if (msg.contains("sort mismatch")) {
278-
throw new ArgumentMismatchError("Type mismatch in arguments of ghost invocation", position, map);
279-
} else {
280-
throw new CustomError(e.getMessage(), position);
281-
}
282-
}
265+
Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions();
266+
throw new RefinementError(position, expected.getExpression(), premises.simplify(), map);
283267
}
284268

285-
protected void raiseSubtypingError(SourcePosition position, Predicate expected, Predicate found) throws LJError {
269+
protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected)
270+
throws StateRefinementError {
286271
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
287-
gatherVariables(expected, lrv, mainVars);
288272
gatherVariables(found, lrv, mainVars);
289273
TranslationTable map = new TranslationTable();
290-
Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions();
291-
throw new RefinementError(position, expected.getExpression(), premises.simplify(), map);
274+
VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
275+
throw new StateRefinementError(position, expected.getExpression(),
276+
foundState.toConjunctions().simplify().getValue(), map);
292277
}
293278

294-
protected void raiseSameStateError(SourcePosition position, Predicate expected) throws LJError {
279+
protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {
295280
TranslationTable map = createMap(expected);
296281
throw new StateConflictError(position, expected.getExpression(), map);
297282
}
298283

299-
protected void raiseStateMismatchError(SourcePosition position, Predicate found, Predicate expected)
300-
throws LJError {
284+
private TranslationTable createMap(Predicate expectedType) {
301285
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
302-
gatherVariables(found, lrv, mainVars);
286+
gatherVariables(expectedType, lrv, mainVars);
303287
TranslationTable map = new TranslationTable();
304-
VCImplication foundState = joinPredicates(found, mainVars, lrv, map);
305-
throw new StateRefinementError(position, expected.getExpression(),
306-
foundState.toConjunctions().simplify().getValue(), map);
288+
joinPredicates(expectedType, mainVars, lrv, map);
289+
return map;
307290
}
308291
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF
8383
} else {
8484
boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition());
8585
if (!ok) {
86-
tc.createError(method.getPosition(), argRef, superArgRef);
86+
tc.throwRefinementError(method.getPosition(), argRef, superArgRef);
8787
}
8888
}
8989
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -215,7 +215,7 @@ private static Predicate createStatePredicate(String value, String targetClass,
215215
c = c.changeOldMentions(nameOld, name);
216216
boolean ok = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition());
217217
if (ok) {
218-
tc.createSameStateError(e.getPosition(), p, targetClass);
218+
tc.throwStateConflictError(e.getPosition(), p);
219219
}
220220
return c1;
221221
}
@@ -407,7 +407,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
407407
.changeOldMentions(vi.getName(), instanceName);
408408

409409
if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
410-
tc.createStateMismatchError(fw.getPosition(), fw.toString(), prevState, stateChange.getFrom());
410+
tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom());
411411
return;
412412
}
413413

@@ -490,8 +490,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
490490
.map(ObjectState::getFrom)
491491
.reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction);
492492
String simpleInvocation = invocation.toString();
493-
tc.createStateMismatchError(invocation.getPosition(), simpleInvocation, prevState,
494-
expectedStatesDisjunction);
493+
tc.throwStateRefinementError(invocation.getPosition(), prevState, expectedStatesDisjunction);
495494
}
496495
}
497496

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,8 @@ public Predicate changeAliasToRefinement(Context context, Factory f) throws LJEr
105105
}
106106

107107
ref = ref.changeAlias(alias, context, f);
108+
ref.validateGhostInvocations(context, f);
109+
108110
return new Predicate(ref);
109111
}
110112

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
import java.util.List;
55
import java.util.stream.Collectors;
66

7+
import liquidjava.diagnostics.errors.LJError;
78
import liquidjava.rj_language.visitors.ExpressionVisitor;
89

910
public class AliasInvocation extends Expression {
@@ -24,7 +25,7 @@ public List<Expression> getArgs() {
2425
}
2526

2627
@Override
27-
public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
28+
public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
2829
return visitor.visitAliasInvocation(this);
2930
}
3031

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@
22

33
import java.util.List;
44

5+
import liquidjava.diagnostics.errors.LJError;
56
import liquidjava.rj_language.visitors.ExpressionVisitor;
67

78
public class BinaryExpression extends Expression {
@@ -40,7 +41,7 @@ public boolean isArithmeticOperation() {
4041
}
4142

4243
@Override
43-
public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
44+
public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
4445
return visitor.visitBinaryExpression(this);
4546
}
4647

0 commit comments

Comments
 (0)