Add Counterexamples to Refinement Errors

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() {

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,

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<GhostState> 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<GhostState> list, CtEl
      */
     public void processSubtyping(Predicate type, Predicate expectedType, List<GhostState> 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<GhostS
      * @param found
      * @param position
      *
-     * @return true if expected type is subtype of found type, false otherwise
+     * @return counterexample if expected type is not subtype of found type, otherwise null
      *
      * @throws LJError
      */
-    public boolean smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError {
+    public SMTResult smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError {
         try {
-            new SMTEvaluator().verifySubtype(found, expected, context);
-            return true;
-        } catch (TypeCheckError e) {
-            return false;
+            return new SMTEvaluator().verifySubtype(found, expected, context);
         } catch (LJError e) {
             e.setPosition(position);
             throw e;
@@ -104,13 +103,13 @@ public boolean smtChecks(Predicate expected, Predicate found, SourcePosition pos
         }
     }
 
-    public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list,
+    public SMTResult canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list,
             SourcePosition position, Factory f) throws LJError {
         List<RefinedVariable> 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<RefinedVariable> 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,

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());
                 }

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<Object
             }
             expectState = expectState.changeOldMentions(vi.getName(), instanceName);
 
-            found = tc.checksStateSMT(prevCheck, expectState, invocation.getPosition());
+            found = tc.checkStateSMT(prevCheck, expectState, invocation.getPosition());
             if (found && stateChange.hasTo()) {
                 String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
                 Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, newInstanceName)

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

@@ -0,0 +1,6 @@
+package liquidjava.smt;
+
+import java.util.List;
+
+public record Counterexample(List<String> assignments) {
+}

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();
     }
 }

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;
+    }
+}