diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java new file mode 100644 index 00000000..5a14c528 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java @@ -0,0 +1,6 @@ +package liquidjava.diagnostics; + +import java.util.List; + +public record Counterexample(List assignments) { +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index de40bd7f..620be6a6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,7 +1,7 @@ package liquidjava.diagnostics.errors; +import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import spoon.reflect.cu.SourcePosition; @@ -14,13 +14,30 @@ public class RefinementError extends LJError { private final ValDerivationNode expected; private final ValDerivationNode found; + private final Counterexample counterexample; public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found, - TranslationTable translationTable, String customMessage) { + TranslationTable translationTable, Counterexample counterexample, String customMessage) { super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()), position, translationTable, customMessage); this.expected = expected; this.found = found; + this.counterexample = counterexample; + } + + @Override + public String getDetails() { + if (counterexample == null || counterexample.assignments().isEmpty()) + return ""; + + // filter fresh variables and join assignements with && + String counterexampleExp = counterexample.assignments().stream().filter(a -> !a.startsWith("#fresh_")) + .reduce((a, b) -> a + " && " + b).orElse(""); + + // check if counterexample is trivial (same as the found value) + if (counterexampleExp.equals(found.getValue().toSimplifiedString())) + return ""; + return "Counterexample: " + counterexampleExp; } public ValDerivationNode getExpected() { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 73d68e25..69adfb4e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -5,6 +5,7 @@ import java.util.List; import java.util.Optional; +import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.errors.*; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -309,13 +310,15 @@ public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElemen vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, factory); } - public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError { - return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); + public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError { + Counterexample counterexample = vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), + p, factory); + return counterexample == null; } public void throwRefinementError(SourcePosition position, Predicate expectedType, Predicate foundType, String customMessage) throws LJError { - vcChecker.throwRefinementError(position, expectedType, foundType, customMessage); + vcChecker.throwRefinementError(position, expectedType, foundType, null, customMessage); } public void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected, diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 6a0fe977..693ab5f4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -8,6 +8,7 @@ import java.util.stream.Collectors; import liquidjava.diagnostics.errors.*; +import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.TranslationTable; import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; @@ -55,10 +56,10 @@ public void processSubtyping(Predicate expectedType, List list, CtEl e.setPosition(element.getPosition()); throw e; } - boolean isSubtype = smtChecks(expected, premises, element.getPosition()); - if (!isSubtype) + Counterexample counterexample = smtChecks(expected, premises, element.getPosition()); + if (counterexample != null) throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(), - map, customMessage); + map, counterexample, customMessage); } /** @@ -74,9 +75,9 @@ public void processSubtyping(Predicate expectedType, List list, CtEl */ public void processSubtyping(Predicate type, Predicate expectedType, List list, CtElement element, Factory f) throws LJError { - boolean b = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); - if (!b) - throwRefinementError(element.getPosition(), expectedType, type, null); + Counterexample counterexample = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); + if (counterexample != null) + throwRefinementError(element.getPosition(), expectedType, type, counterexample, null); } /** @@ -86,16 +87,16 @@ public void processSubtyping(Predicate type, Predicate expectedType, List list, + public Counterexample canProcessSubtyping(Predicate type, Predicate expectedType, List list, SourcePosition position, Factory f) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); if (expectedType.isBooleanTrue() && type.isBooleanTrue()) - return true; + return null; TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; @@ -262,13 +263,14 @@ void removePathVariableThatIncludes(String otherVar) { // Errors--------------------------------------------------------------------------------------------------- protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found, - String customMessage) throws RefinementError { + Counterexample counterexample, String customMessage) throws RefinementError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expected, lrv, mainVars); gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); Predicate premises = joinPredicates(expected, mainVars, lrv, map).toConjunctions(); - throw new RefinementError(position, expected.simplify(), premises.simplify(), map, customMessage); + throw new RefinementError(position, expected.simplify(), premises.simplify(), map, counterexample, + customMessage); } protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected, diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index 455e8276..26f68bb6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java @@ -81,7 +81,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF if (argRef.isBooleanTrue()) { arg.setRefinement(superArgRef.substituteVariable(newName, arg.getName())); } else { - boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); + boolean ok = tc.checkStateSMT(superArgRef, argRef, params.get(i).getPosition()); if (!ok) { tc.throwRefinementError(method.getPosition(), argRef, superArgRef, function.getMessage()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index facbd2c1..c615581e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -220,7 +220,7 @@ private static Predicate createStatePredicate(String value, String targetClass, Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p; Predicate c = c1.substituteVariable(Keys.THIS, name); c = c.changeOldMentions(nameOld, name); - boolean ok = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition()); + boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition()); if (ok) { tc.throwStateConflictError(e.getPosition(), p); } @@ -413,7 +413,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName) .changeOldMentions(vi.getName(), instanceName); - if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition + if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom(), stateChange.getMessage()); return; } @@ -478,7 +478,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List e = exp.accept(visitor); - s = tz3.verifyExpression(e); - if (s.equals(Status.SATISFIABLE)) { - throw new TypeCheckError(subRef + " not a subtype of " + supRef); + Solver solver = tz3.makeSolverForExpression(e); + Status result = solver.check(); + if (result.equals(Status.SATISFIABLE)) { + Model model = solver.getModel(); + Counterexample counterexample = tz3.getCounterexample(model); + throw new TypeCheckError(counterexample); } } } catch (SyntaxException e1) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index b207552f..404e1943 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -1,22 +1,25 @@ package liquidjava.smt; -import com.martiansoftware.jsap.SyntaxException; import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; +import com.microsoft.z3.FuncInterp; import com.microsoft.z3.IntExpr; import com.microsoft.z3.IntNum; import com.microsoft.z3.RealExpr; import com.microsoft.z3.Solver; import com.microsoft.z3.Sort; -import com.microsoft.z3.Status; +import com.microsoft.z3.Model; + +import java.util.ArrayList; import java.util.HashMap; import java.util.List; import java.util.Map; +import liquidjava.diagnostics.Counterexample; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.context.AliasWrapper; @@ -42,10 +45,27 @@ public TranslatorToZ3(liquidjava.processor.context.Context c) { } @SuppressWarnings("unchecked") - public Status verifyExpression(Expr e) { - Solver s = z3.mkSolver(); - s.add((BoolExpr) e); - return s.check(); + public Solver makeSolverForExpression(Expr e) { + Solver solver = z3.mkSolver(); + solver.add((BoolExpr) e); + return solver; + } + + /** + * Extracts the counterexample from the Z3 model + */ + public Counterexample getCounterexample(Model model) { + List assignments = new ArrayList<>(); + for (FuncDecl decl : model.getDecls()) { + // extract variable assignments with constants + if (decl.getArity() == 0) { + String name = decl.getName().toString(); + String value = model.getConstInterp(decl).toString(); + assignments.add(name + " == " + value); + } + // TODO: extract function assignments (arity > 0)? + } + return new Counterexample(assignments); } // #####################Literals and Variables##################### diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java index 04c6c07d..a96f6f69 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java @@ -1,8 +1,17 @@ package liquidjava.smt; +import liquidjava.diagnostics.Counterexample; + public class TypeCheckError extends Exception { - public TypeCheckError(String message) { - super(message); + private final Counterexample counterexample; + + public TypeCheckError(Counterexample counterexample) { + super("Refinement was violated"); + this.counterexample = counterexample; + } + + public Counterexample getCounterexample() { + return counterexample; } }