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..21a9a4c2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -1,8 +1,8 @@ package liquidjava.diagnostics.errors; import liquidjava.diagnostics.TranslationTable; -import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; +import liquidjava.smt.Counterexample; import spoon.reflect.cu.SourcePosition; /** @@ -14,13 +14,39 @@ 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() { + return getCounterexampleString(); + } + + private String getCounterexampleString() { + 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().toString())) + return ""; + + return "Counterexample: " + counterexampleExp; + } + + public Counterexample getCounterexample() { + return counterexample; } 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 31c019bc..c4358ba9 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 @@ -16,6 +16,8 @@ import liquidjava.processor.facade.GhostDTO; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.RefinementsParser; +import liquidjava.smt.Counterexample; +import liquidjava.smt.SMTResult; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -312,13 +314,14 @@ 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 { + SMTResult result = vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); + return result.isOk(); } 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..f0634a67 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 @@ -12,8 +12,9 @@ import liquidjava.processor.VCImplication; import liquidjava.processor.context.*; import liquidjava.rj_language.Predicate; +import liquidjava.smt.Counterexample; import liquidjava.smt.SMTEvaluator; -import liquidjava.smt.TypeCheckError; +import liquidjava.smt.SMTResult; import liquidjava.utils.constants.Keys; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; @@ -55,10 +56,11 @@ public void processSubtyping(Predicate expectedType, List list, CtEl e.setPosition(element.getPosition()); throw e; } - boolean isSubtype = smtChecks(expected, premises, element.getPosition()); - if (!isSubtype) + SMTResult result = smtChecks(expected, premises, element.getPosition()); + if (result.isError()) { throw new RefinementError(element.getPosition(), expectedType.simplify(), premisesBeforeChange.simplify(), - map, customMessage); + map, result.getCounterexample(), customMessage); + } } /** @@ -74,9 +76,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); + SMTResult result = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); + if (result.isError()) + throwRefinementError(element.getPosition(), expectedType, type, result.getCounterexample(), null); } /** @@ -86,16 +88,13 @@ public void processSubtyping(Predicate type, Predicate expectedType, List list, + public SMTResult 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 SMTResult.ok(); TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; @@ -262,13 +261,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 assignments) { +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index bf00f999..338a885d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -2,6 +2,8 @@ import com.martiansoftware.jsap.SyntaxException; import com.microsoft.z3.Expr; +import com.microsoft.z3.Model; +import com.microsoft.z3.Solver; import com.microsoft.z3.Status; import com.microsoft.z3.Z3Exception; @@ -11,19 +13,21 @@ public class SMTEvaluator { - public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception { + public SMTResult verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception { // Creates a parser for our SMT-ready refinement language // Discharges the verification to z3 Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate()); try { Expression exp = toVerify.getExpression(); - Status s; try (TranslatorToZ3 tz3 = new TranslatorToZ3(c)) { ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3); Expr 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); + return SMTResult.error(counterexample); } } } catch (SyntaxException e1) { @@ -32,5 +36,6 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws } catch (Z3Exception e) { throw new Z3Exception(e.getLocalizedMessage()); } + return SMTResult.ok(); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java new file mode 100644 index 00000000..6cd9869d --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTResult.java @@ -0,0 +1,29 @@ +package liquidjava.smt; + +public class SMTResult { + private final Counterexample counterexample; + + private SMTResult(Counterexample counterexample) { + this.counterexample = counterexample; + } + + public static SMTResult ok() { + return new SMTResult(null); + } + + public static SMTResult error(Counterexample counterexample) { + return new SMTResult(counterexample); + } + + public boolean isOk() { + return counterexample == null; + } + + public boolean isError() { + return !isOk(); + } + + public Counterexample getCounterexample() { + return counterexample; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index b207552f..1e960590 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -1,27 +1,33 @@ 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.Symbol; +import com.microsoft.z3.Model; + +import java.util.ArrayList; +import java.util.Arrays; import java.util.HashMap; import java.util.List; import java.util.Map; +import java.util.stream.Collectors; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; import liquidjava.processor.context.AliasWrapper; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; +import com.microsoft.z3.enumerations.Z3_sort_kind; import org.apache.commons.lang3.NotImplementedException; @@ -32,6 +38,8 @@ public class TranslatorToZ3 implements AutoCloseable { private final Map>> varSuperTypes = new HashMap<>(); private final Map aliasTranslation = new HashMap<>(); // this is not being used private final Map> funcTranslation = new HashMap<>(); + private final Map> funcAppTranslation = new HashMap<>(); + private final Map, String> exprToNameTranslation = new HashMap<>(); public TranslatorToZ3(liquidjava.processor.context.Context c) { TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation); @@ -42,10 +50,35 @@ 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<>(); + // Extract constant variable assignments + for (FuncDecl decl : model.getDecls()) { + if (decl.getArity() == 0) { + Symbol name = decl.getName(); + Expr value = model.getConstInterp(decl); + // Skip values of uninterpreted sorts + if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT) + assignments.add(name + " == " + value); + } + } + // Extract function application values + for (Map.Entry> entry : funcAppTranslation.entrySet()) { + String label = entry.getKey(); + Expr application = entry.getValue(); + Expr value = model.eval(application, true); + assignments.add(label + " = " + value); + } + return new Counterexample(assignments); } // #####################Literals and Variables##################### @@ -81,7 +114,9 @@ private Expr getVariableTranslation(String name) throws LJError { } public Expr makeVariable(String name) throws LJError { - return getVariableTranslation(name); // int[] not in varTranslation + Expr expr = getVariableTranslation(name); // int[] not in varTranslation + exprToNameTranslation.put(expr, name); // Track for readable labels + return expr; } public Expr makeFunctionInvocation(String name, Expr[] params) throws LJError { @@ -91,7 +126,7 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws LJEr return makeSelect(params); FuncDecl fd = funcTranslation.get(name); if (fd == null) - fd = resolveFunctionDeclFallback(name, params); + fd = resolveFunctionDecl(name, params); Sort[] s = fd.getDomain(); for (int i = 0; i < s.length; i++) { @@ -105,15 +140,18 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws LJEr params[i] = e; } } - return z3.mkApp(fd, params); + String label = buildFunctionLabel(name, params); + Expr app = z3.mkApp(fd, params); + funcAppTranslation.put(label, app); + return app; } /** - * Fallback resolver for function declarations when an exact qualified name lookup fails. Tries to match by simple - * name and number of parameters, preferring an exact qualified-name match if found among candidates; otherwise - * returns the first compatible candidate and relies on later coercion via var supertypes. + * Gets function declarations when an exact qualified name lookup fails. Tries to match by simple name and number of + * parameters, preferring an exact qualified-name match if found among candidates; otherwise returns the first + * compatible candidate and relies on later coercion via var supertypes. */ - private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) throws LJError { + private FuncDecl resolveFunctionDecl(String name, Expr[] params) throws LJError { String simple = Utils.getSimpleName(name); FuncDecl candidate = null; for (Map.Entry> entry : funcTranslation.entrySet()) { @@ -310,6 +348,13 @@ public Expr makeIte(Expr c, Expr t, Expr e) { throw new RuntimeException("Condition is not a boolean expression"); } + private String buildFunctionLabel(String functionName, Expr[] params) { + String simpleName = Utils.getSimpleName(functionName); + String argsString = Arrays.stream(params).map(p -> exprToNameTranslation.getOrDefault(p, p.toString())) + .collect(Collectors.joining(", ")); + return simpleName + "(" + argsString + ")"; + } + @Override public void close() throws Exception { z3.close(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java deleted file mode 100644 index 04c6c07d..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TypeCheckError.java +++ /dev/null @@ -1,8 +0,0 @@ -package liquidjava.smt; - -public class TypeCheckError extends Exception { - - public TypeCheckError(String message) { - super(message); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 1cf45bc7..1e99e3f0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -50,7 +50,6 @@ private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { private static boolean hasRefinementValue(CtAnnotation annotation, String refinement) { Map values = annotation.getValues(); - return Stream.of("value", "to", "from") - .anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); + return Stream.of("value", "to", "from").anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); } }