Add Counterexamples to Refinement Errors

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) {
+}

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().toString()))
+            return "";
+        return "Counterexample: " + counterexampleExp;
     }
 
     public ValDerivationNode getExpected() {

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

@@ -6,6 +6,7 @@
 import java.util.Map;
 import java.util.Optional;
 
+import liquidjava.diagnostics.Counterexample;
 import liquidjava.diagnostics.errors.*;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
@@ -312,13 +313,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,

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<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, customMessage);
+                    map, counterexample, customMessage);
     }
 
     /**
@@ -74,9 +75,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);
+        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<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;
@@ -104,13 +105,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 };
@@ -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<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/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) {

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

@@ -1,27 +1,34 @@
 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.Counterexample;
 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 +39,8 @@ public class TranslatorToZ3 implements AutoCloseable {
     private final Map<String, List<Expr<?>>> varSuperTypes = new HashMap<>();
     private final Map<String, AliasWrapper> aliasTranslation = new HashMap<>(); // this is not being used
     private final Map<String, FuncDecl<?>> funcTranslation = new HashMap<>();
+    private final Map<String, Expr<?>> funcAppTranslation = new HashMap<>();
+    private final Map<Expr<?>, String> exprToNameTranslation = new HashMap<>();
 
     public TranslatorToZ3(liquidjava.processor.context.Context c) {
         TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation);
@@ -42,10 +51,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<String> 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<String, Expr<?>> 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 +115,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 +127,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 +141,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<String, FuncDecl<?>> entry : funcTranslation.entrySet()) {
@@ -310,6 +349,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();

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