Skip to content

Commit 86db776

Browse files
rcosta358rcosta358
authored
Add Counterexamples to Refinement Errors (#146)
1 parent 375418d commit 86db776

File tree

10 files changed

+196
-70
lines changed

10 files changed

+196
-70
lines changed

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

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

33
import liquidjava.diagnostics.TranslationTable;
4-
import liquidjava.rj_language.ast.Expression;
54
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
5+
import liquidjava.smt.Counterexample;
66
import spoon.reflect.cu.SourcePosition;
77

88
/**
@@ -14,13 +14,39 @@ public class RefinementError extends LJError {
1414

1515
private final ValDerivationNode expected;
1616
private final ValDerivationNode found;
17+
private final Counterexample counterexample;
1718

1819
public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
19-
TranslationTable translationTable, String customMessage) {
20+
TranslationTable translationTable, Counterexample counterexample, String customMessage) {
2021
super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()),
2122
position, translationTable, customMessage);
2223
this.expected = expected;
2324
this.found = found;
25+
this.counterexample = counterexample;
26+
}
27+
28+
@Override
29+
public String getDetails() {
30+
return getCounterexampleString();
31+
}
32+
33+
private String getCounterexampleString() {
34+
if (counterexample == null || counterexample.assignments().isEmpty())
35+
return "";
36+
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("");
40+
41+
// check if counterexample is trivial (same as the found value)
42+
if (counterexampleExp.equals(found.getValue().toString()))
43+
return "";
44+
45+
return "Counterexample: " + counterexampleExp;
46+
}
47+
48+
public Counterexample getCounterexample() {
49+
return counterexample;
2450
}
2551

2652
public ValDerivationNode getExpected() {

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

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import liquidjava.processor.facade.GhostDTO;
1717
import liquidjava.rj_language.Predicate;
1818
import liquidjava.rj_language.parsing.RefinementsParser;
19+
import liquidjava.smt.SMTResult;
1920
import liquidjava.utils.Utils;
2021
import liquidjava.utils.constants.Formats;
2122
import liquidjava.utils.constants.Keys;
@@ -312,13 +313,15 @@ public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElemen
312313
vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, factory);
313314
}
314315

315-
public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError {
316-
return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory);
316+
public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError {
317+
SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostState(), p,
318+
factory);
319+
return result.isOk();
317320
}
318321

319322
public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType,
320323
String customMessage) throws LJError {
321-
vcChecker.throwRefinementError(position, expectedType, foundType, customMessage);
324+
vcChecker.throwRefinementError(position, expectedType, foundType, null, customMessage);
322325
}
323326

324327
public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,

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

Lines changed: 40 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,9 @@
1212
import liquidjava.processor.VCImplication;
1313
import liquidjava.processor.context.*;
1414
import liquidjava.rj_language.Predicate;
15+
import liquidjava.smt.Counterexample;
1516
import liquidjava.smt.SMTEvaluator;
16-
import liquidjava.smt.TypeCheckError;
17+
import liquidjava.smt.SMTResult;
1718
import liquidjava.utils.constants.Keys;
1819
import spoon.reflect.cu.SourcePosition;
1920
import spoon.reflect.declaration.CtElement;
@@ -55,47 +56,43 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
5556
e.setPosition(element.getPosition());
5657
throw e;
5758
}
58-
boolean isSubtype = smtChecks(expected, premises, element.getPosition());
59-
if (!isSubtype)
59+
SMTResult result = verifySMTSubtype(expected, premises, element.getPosition());
60+
if (result.isError()) {
6061
throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(),
61-
map, customMessage);
62+
map, result.getCounterexample(), customMessage);
63+
}
6264
}
6365

6466
/**
65-
* Check that type is a subtype of expectedType Throws RefinementError otherwise
66-
*
67+
* Checks if type is a subtype of expectedType
68+
*
6769
* @param type
6870
* @param expectedType
6971
* @param list
7072
* @param element
7173
* @param f
72-
*
74+
*
7375
* @throws LJError
7476
*/
7577
public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> list, CtElement element,
7678
Factory f) throws LJError {
77-
boolean b = canProcessSubtyping(type, expectedType, list, element.getPosition(), f);
78-
if (!b)
79-
throwRefinementError(element.getPosition(), expectedType, type, null);
79+
SMTResult result = verifySMTSubtypeStates(type, expectedType, list, element.getPosition(), f);
80+
if (result.isError())
81+
throwRefinementError(element.getPosition(), expectedType, type, result.getCounterexample(), null);
8082
}
8183

8284
/**
83-
* Checks the expected against the found constraint
84-
*
85+
* Verifies whether the found predicate is a subtype of the expected predicate
86+
*
8587
* @param expected
8688
* @param found
8789
* @param position
88-
*
89-
* @return true if expected type is subtype of found type, false otherwise
90-
*
91-
* @throws LJError
90+
*
91+
* @return the result of the verification, containing a counterexample if the verification fails
9292
*/
93-
public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError {
93+
public SMTResult verifySMTSubtype(Predicate expected, Predicate found, SourcePosition position) throws LJError {
9494
try {
95-
new SMTEvaluator().verifySubtype(found, expected, context);
96-
return true;
97-
} catch (TypeCheckError e) {
98-
return false;
95+
return new SMTEvaluator().verifySubtype(found, expected, context);
9996
} catch (LJError e) {
10097
e.setPosition(position);
10198
throw e;
@@ -104,24 +101,36 @@ public boolean smtChecks(Predicate expected, Predicate found, SourcePosition pos
104101
}
105102
}
106103

107-
public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list,
108-
SourcePosition position, Factory f) throws LJError {
104+
/**
105+
* Verifies whether the found predicate is a subtype of the expected predicate, taking into account the ghost states
106+
*
107+
* @param type
108+
* @param expectedType
109+
* @param states
110+
* @param position
111+
* @param factory
112+
*
113+
* @return the result of the verification, containing a counterexample if the verification fails
114+
*/
115+
public SMTResult verifySMTSubtypeStates(Predicate type, Predicate expectedType, List<GhostState> states,
116+
SourcePosition position, Factory factory) throws LJError {
109117
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
110118
gatherVariables(expectedType, lrv, mainVars);
111119
gatherVariables(type, lrv, mainVars);
112120
if (expectedType.isBooleanTrue() && type.isBooleanTrue())
113-
return true;
121+
return SMTResult.ok();
114122

115123
TranslationTable map = new TranslationTable();
116124
String[] s = { Keys.WILDCARD, Keys.THIS };
117125
Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions();
118-
List<GhostState> filtered = filterGhostStatesForVariables(list, mainVars, lrv);
126+
List<GhostState> filtered = filterGhostStatesForVariables(states, mainVars, lrv);
119127
premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(filtered, s)
120-
.changeAliasToRefinement(context, f);
121-
Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f);
128+
.changeAliasToRefinement(context, factory);
129+
Predicate expected = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context,
130+
factory);
122131

123132
// check subtyping
124-
return smtChecks(expected, premises, position);
133+
return verifySMTSubtype(expected, premises, position);
125134
}
126135

127136
/**
@@ -262,13 +271,14 @@ void removePathVariableThatIncludes(String otherVar) {
262271
// Errors---------------------------------------------------------------------------------------------------
263272

264273
protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found,
265-
String customMessage) throws RefinementError {
274+
Counterexample counterexample, String customMessage) throws RefinementError {
266275
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
267276
gatherVariables(expected, lrv, mainVars);
268277
gatherVariables(found, lrv, mainVars);
269278
TranslationTable map = new TranslationTable();
270279
Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions();
271-
throw new RefinementError(position, expected.simplify(), premises.simplify(), map, customMessage);
280+
throw new RefinementError(position, expected.simplify(), premises.simplify(), map, counterexample,
281+
customMessage);
272282
}
273283

274284
protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,

‎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
@@ -81,7 +81,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF
8181
if (argRef.isBooleanTrue()) {
8282
arg.setRefinement(superArgRef.substituteVariable(newName, arg.getName()));
8383
} else {
84-
boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition());
84+
boolean ok = tc.checkStateSMT(superArgRef, argRef, params.get(i).getPosition());
8585
if (!ok) {
8686
tc.throwRefinementError(method.getPosition(), argRef, superArgRef, function.getMessage());
8787
}

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -220,7 +220,7 @@ private static Predicate createStatePredicate(String value, String targetClass,
220220
Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p;
221221
Predicate c = c1.substituteVariable(Keys.THIS, name);
222222
c = c.changeOldMentions(nameOld, name);
223-
boolean ok = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition());
223+
boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition());
224224
if (ok) {
225225
tc.throwStateConflictError(e.getPosition(), p);
226226
}
@@ -413,7 +413,7 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
413413
Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName)
414414
.changeOldMentions(vi.getName(), instanceName);
415415

416-
if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
416+
if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
417417
tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom(), stateChange.getMessage());
418418
return;
419419
}
@@ -478,7 +478,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
478478
}
479479
expectState = expectState.changeOldMentions(vi.getName(), instanceName);
480480

481-
found = tc.checksStateSMT(prevCheck, expectState, invocation.getPosition());
481+
found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
482482
if (found && stateChange.hasTo()) {
483483
String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
484484
Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, newInstanceName)

‎liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
package liquidjava.smt;
2+
3+
import java.util.List;
4+
5+
public record Counterexample(List<String> assignments) {
6+
}

‎liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java‎

Lines changed: 25 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22

33
import com.martiansoftware.jsap.SyntaxException;
44
import com.microsoft.z3.Expr;
5+
import com.microsoft.z3.Model;
6+
import com.microsoft.z3.Solver;
57
import com.microsoft.z3.Status;
68
import com.microsoft.z3.Z3Exception;
79

@@ -11,26 +13,39 @@
1113

1214
public class SMTEvaluator {
1315

14-
public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception {
15-
// Creates a parser for our SMT-ready refinement language
16-
// Discharges the verification to z3
16+
/**
17+
* Verifies that subRef is a subtype of supRef by checking the satisfiability of subRef && !supRef. Creates a parser
18+
* for our SMT-ready refinement language and discharges the verification to Z3
19+
*
20+
* @param subRef
21+
* @param supRef
22+
* @param context
23+
*
24+
* @return the result of the verification, containing a counterexample if the verification fails
25+
*/
26+
public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context context) throws Exception {
1727
Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate());
1828
try {
1929
Expression exp = toVerify.getExpression();
20-
Status s;
21-
try (TranslatorToZ3 tz3 = new TranslatorToZ3(c)) {
30+
try (TranslatorToZ3 tz3 = new TranslatorToZ3(context)) {
2231
ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3);
2332
Expr<?> e = exp.accept(visitor);
24-
s = tz3.verifyExpression(e);
25-
if (s.equals(Status.SATISFIABLE)) {
26-
throw new TypeCheckError(subRef + " not a subtype of " + supRef);
33+
Solver solver = tz3.makeSolverForExpression(e);
34+
Status result = solver.check();
35+
36+
// subRef is not a subtype of supRef
37+
if (result.equals(Status.SATISFIABLE)) {
38+
Model model = solver.getModel();
39+
Counterexample counterexample = tz3.getCounterexample(model);
40+
return SMTResult.error(counterexample);
2741
}
2842
}
29-
} catch (SyntaxException e1) {
43+
} catch (SyntaxException e) {
3044
System.out.println("Could not parse: " + toVerify);
31-
e1.printStackTrace();
45+
e.printStackTrace();
3246
} catch (Z3Exception e) {
3347
throw new Z3Exception(e.getLocalizedMessage());
3448
}
49+
return SMTResult.ok();
3550
}
3651
}

‎liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
package liquidjava.smt;
2+
3+
public class SMTResult {
4+
private final Counterexample counterexample;
5+
6+
private SMTResult(Counterexample counterexample) {
7+
this.counterexample = counterexample;
8+
}
9+
10+
public static SMTResult ok() {
11+
return new SMTResult(null);
12+
}
13+
14+
public static SMTResult error(Counterexample counterexample) {
15+
return new SMTResult(counterexample);
16+
}
17+
18+
public boolean isOk() {
19+
return counterexample == null;
20+
}
21+
22+
public boolean isError() {
23+
return !isOk();
24+
}
25+
26+
public Counterexample getCounterexample() {
27+
return counterexample;
28+
}
29+
}

0 commit comments

Comments
 (0)