Add Counterexamples to Refinement Errors

rcosta358 · rcosta358 · commit 089dc0ae6e8a · 2026-02-10T14:15:42.000Z
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Counterexample.java 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<String> 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
@@ -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) {
+            TranslationTable translationTable, Counterexample counterexample) {
         super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()),
                 position, translationTable);
         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
@@ -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;
@@ -292,8 +293,10 @@ 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)
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
@@ -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.*;
@@ -50,10 +51,10 @@ public void processSubtyping(Predicate expectedType, List<GhostState> 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);
+                    map, counterexample);
     }
 
     /**
@@ -69,9 +70,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);
+        Counterexample counterexample = canProcessSubtyping(type, expectedType, list, element.getPosition(), f);
+        if (counterexample != null)
+            throwRefinementError(element.getPosition(), expectedType, type, counterexample);
     }
 
     /**
@@ -81,16 +82,16 @@ 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 Counterexample smtChecks(Predicate expected, Predicate found, SourcePosition position) throws LJError {
         try {
             new SMTEvaluator().verifySubtype(found, expected, context);
-            return true;
+            return null;
         } catch (TypeCheckError e) {
-            return false;
+            return e.getCounterexample();
         } catch (LJError e) {
             e.setPosition(position);
             throw e;
@@ -99,13 +100,13 @@ public boolean smtChecks(Predicate expected, Predicate found, SourcePosition pos
         }
     }
 
-    public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<GhostState> list,
+    public Counterexample 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 null;
 
         TranslationTable map = new TranslationTable();
         String[] s = { Keys.WILDCARD, Keys.THIS };
@@ -258,12 +259,17 @@ void removePathVariableThatIncludes(String otherVar) {
 
     protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found)
             throws RefinementError {
+        throwRefinementError(position, expected, found, null);
+    }
+
+    protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found,
+            Counterexample counterexample) 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);
+        throw new RefinementError(position, expected.simplify(), premises.simplify(), map, counterexample);
     }
 
     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
@@ -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);
                 }
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
@@ -213,7 +213,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);
         }
@@ -406,7 +406,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());
             return;
         }
@@ -471,7 +471,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)
@@ -489,7 +489,6 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List<Object
             Predicate expectedStatesDisjunction = stateChanges.stream().filter(ObjectState::hasFrom)
                     .map(ObjectState::getFrom)
                     .reduce(Predicate.createLit("false", Types.BOOLEAN), Predicate::createDisjunction);
-            String simpleInvocation = invocation.toString();
             tc.throwStateRefinementError(invocation.getPosition(), prevState, expectedStatesDisjunction);
         }
     }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java
@@ -2,9 +2,12 @@
 
 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;
 
+import liquidjava.diagnostics.Counterexample;
 import liquidjava.processor.context.Context;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
@@ -17,13 +20,15 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws
         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);
+                    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
@@ -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<String> 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
@@ -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;
     }
 }

Original file line number	Diff line number	Diff line change
`@@ -81,7 +81,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF`
`81`	`81`	`if (argRef.isBooleanTrue()) {`
`82`	`82`	`arg.setRefinement(superArgRef.substituteVariable(newName, arg.getName()));`
`83`	`83`	`} else {`
`84`		`- boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition());`
	`84`	`+ boolean ok = tc.checkStateSMT(superArgRef, argRef, params.get(i).getPosition());`
`85`	`85`	`if (!ok) {`
`86`	`86`	`tc.throwRefinementError(method.getPosition(), argRef, superArgRef);`
`87`	`87`	`}`