Fix verifier reference equality across recorded upcasts

liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_correct/Test.java

@@ -0,0 +1,29 @@
+package testSuite.classes.subtype_assignment_correct;
+
+import java.io.IOException;
+import liquidjava.specification.Refinement;
+
+public class Test {
+    static void load() throws IOException {
+        throw new IOException("truncated");
+    }
+
+    static void knownState(@Refinement("noThrowable(_)") IOException original, Exception previous) {
+        Exception failure = original;
+        Exception copy = failure;
+        copy.initCause(previous);
+    }
+
+    static void run(Exception previous) {
+        Exception failure = null;
+        try {
+            load();
+        } catch (IOException e) {
+            failure = e;
+        }
+        if (failure != null) {
+            Exception copy = failure;
+            @Refinement("_ == 1") int checked = 1;
+        }
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_correct/ThrowableRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.subtype_assignment_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.lang.Throwable")
+@StateSet({"withThrowable", "noThrowable"})
+public interface ThrowableRefinements {
+    @StateRefinement(to = "noThrowable(this)")
+    void Throwable(String message);
+
+    @StateRefinement(to = "withThrowable(this)")
+    void Throwable(String message, Throwable cause);
+
+    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
+    Throwable initCause(Throwable cause);
+}

liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_error/Test.java

@@ -0,0 +1,27 @@
+package testSuite.classes.subtype_assignment_error;
+
+import java.io.IOException;
+import liquidjava.specification.Refinement;
+
+public class Test {
+    static void load() throws IOException {
+        throw new IOException("truncated");
+    }
+
+    static void alreadyHasCause(@Refinement("withThrowable(_)") IOException original, Exception previous) {
+        Exception failure = original;
+        failure.initCause(previous); // Expect: State Refinement Error
+    }
+
+    static void run(Exception previous) {
+        Exception failure = null;
+        try {
+            load();
+        } catch (IOException e) {
+            failure = e;
+        }
+        if (failure != null) {
+            failure.initCause(previous); // Expect: State Refinement Error
+        }
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_error/ThrowableRefinements.java

@@ -0,0 +1,18 @@
+package testSuite.classes.subtype_assignment_error;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@ExternalRefinementsFor("java.lang.Throwable")
+@StateSet({"withThrowable", "noThrowable"})
+public interface ThrowableRefinements {
+    @StateRefinement(to = "noThrowable(this)")
+    void Throwable(String message);
+
+    @StateRefinement(to = "withThrowable(this)")
+    void Throwable(String message, Throwable cause);
+
+    @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
+    Throwable initCause(Throwable cause);
+}

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

@@ -17,8 +17,10 @@
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
+import java.util.Set;
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.errors.LJError;
@@ -53,6 +55,8 @@ public class TranslatorToZ3 implements AutoCloseable {
      * appears symbolically in counterexample models.
      */
     private final List<BoolExpr> staticConstantAxioms = new ArrayList<>();
+    private final List<BoolExpr> referenceIdentityAxioms = new ArrayList<>();
+    private final Set<Set<String>> referenceIdentityPairs = new HashSet<>();
 
     public TranslatorToZ3(liquidjava.processor.context.Context context) {
         TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation);
@@ -67,6 +71,8 @@ public Solver makeSolverForExpression(Expr<?> e) {
         Solver solver = z3.mkSolver();
         for (BoolExpr axiom : staticConstantAxioms)
             solver.add(axiom);
+        for (BoolExpr axiom : referenceIdentityAxioms)
+            solver.add(axiom);
         solver.add((BoolExpr) e);
         return solver;
     }
@@ -253,9 +259,68 @@ public Expr<?> makeEquals(Expr<?> e1, Expr<?> e2) {
             return z3.mkFPEq(toFP(e1), toFP(e2));
         if (e1 instanceof RealExpr || e2 instanceof RealExpr)
             return z3.mkEq(toReal(e1), toReal(e2));
+        if (isReference(e1) && isReference(e2))
+            addReferenceIdentityAxioms(e1, e2);
+        if (!e1.getSort().equals(e2.getSort()) && isReference(e1) && isReference(e2)) {
+            Expr<?> view = supertypeView(e2, e1.getSort());
+            if (view != null)
+                e2 = view;
+            else {
+                view = supertypeView(e1, e2.getSort());
+                if (view != null)
+                    e1 = view;
+            }
+        }
         return z3.mkEq(e1, e2);
     }
 
+    private static boolean isReference(Expr<?> expression) {
+        return expression.getSort().getSortKind() == Z3_sort_kind.Z3_UNINTERPRETED_SORT;
+    }
+
+    private Expr<?> supertypeView(Expr<?> expression, Sort sort) {
+        String name = exprToNameTranslation.get(expression);
+        if (name == null)
+            return null;
+        for (Expr<?> view : varSuperTypes.getOrDefault(name, List.of()))
+            if (view.getSort().equals(sort))
+                return view;
+        return null;
+    }
+
+    /**
+     * Each reference has separate constants for its Java type views. Identity must agree across every shared view,
+     * including under negation: changing the view of an alias cannot change equality or inequality.
+     */
+    private void addReferenceIdentityAxioms(Expr<?> e1, Expr<?> e2) {
+        String name1 = exprToNameTranslation.get(e1);
+        String name2 = exprToNameTranslation.get(e2);
+        if (name1 == null || name2 == null || name1.equals(name2) || !referenceIdentityPairs.add(Set.of(name1, name2)))
+            return;
+        Map<Sort, Expr<?>> left = referenceViews(name1, e1);
+        Map<Sort, Expr<?>> right = referenceViews(name2, e2);
+        BoolExpr identity = null;
+        for (Map.Entry<Sort, Expr<?>> view : left.entrySet()) {
+            Expr<?> other = right.get(view.getKey());
+            if (other == null)
+                continue;
+            BoolExpr equality = z3.mkEq(view.getValue(), other);
+            if (identity == null)
+                identity = equality;
+            else
+                referenceIdentityAxioms.add(z3.mkEq(identity, equality));
+        }
+    }
+
+    private Map<Sort, Expr<?>> referenceViews(String name, Expr<?> nativeView) {
+        Map<Sort, Expr<?>> views = new HashMap<>();
+        views.put(nativeView.getSort(), nativeView);
+        for (Expr<?> view : varSuperTypes.getOrDefault(name, List.of()))
+            if (isReference(view))
+                views.put(view.getSort(), view);
+        return views;
+    }
+
     @SuppressWarnings({ "unchecked", "rawtypes" })
     public Expr<?> makeLt(Expr<?> e1, Expr<?> e2) {
         if (e1 instanceof FPExpr || e2 instanceof FPExpr)

liquidjava-verifier/src/test/java/liquidjava/smt/ReferenceEqualityTest.java

@@ -0,0 +1,58 @@
+package liquidjava.smt;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.Status;
+import liquidjava.processor.context.Context;
+import liquidjava.rj_language.Predicate;
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.Test;
+import spoon.Launcher;
+
+class ReferenceEqualityTest {
+    private final Context context = Context.getInstance();
+
+    @AfterEach
+    void resetContext() {
+        context.reinitializeAllContext();
+    }
+
+    @Test
+    void referenceIdentityAgreesAcrossNativeAndAncestorViews() throws Exception {
+        var factory = new Launcher().getFactory();
+        context.addVarToContext("child", factory.Type().createReference(java.io.IOException.class), new Predicate(),
+                factory.Code().createCodeSnippetStatement(""));
+        context.addVarToContext("parent", factory.Type().createReference(Exception.class), new Predicate(),
+                factory.Code().createCodeSnippetStatement(""));
+        context.addVarToContext("ancestor", factory.Type().createReference(Throwable.class), new Predicate(),
+                factory.Code().createCodeSnippetStatement(""));
+        try (TranslatorToZ3 translator = new TranslatorToZ3(context)) {
+            Expr<?> child = translator.makeVariable("child");
+            Expr<?> parent = translator.makeVariable("parent");
+            Expr<?> forward = translator.makeEquals(child, parent);
+            Expr<?> reverse = translator.makeEquals(parent, child);
+            assertEquals(Status.UNSATISFIABLE, translator
+                    .makeSolverForExpression(translator.mkNot(translator.makeEquals(forward, reverse))).check());
+            Expr<?> ancestor = translator.makeVariable("ancestor");
+            Expr<?> childAncestor = translator.makeEquals(child, ancestor);
+            Expr<?> parentAncestor = translator.makeEquals(parent, ancestor);
+            for (Expr<?> equality : new Expr<?>[] { forward, reverse }) {
+                Expr<?> sameAncestor = translator.makeAnd(childAncestor, parentAncestor);
+                assertEquals(Status.UNSATISFIABLE, translator
+                        .makeSolverForExpression(translator.makeAnd(sameAncestor, translator.mkNot(equality))).check());
+                assertEquals(Status.UNSATISFIABLE,
+                        translator.makeSolverForExpression(translator
+                                .makeAnd(translator.makeAnd(equality, childAncestor), translator.mkNot(parentAncestor)))
+                                .check());
+                assertEquals(Status.UNSATISFIABLE,
+                        translator
+                                .makeSolverForExpression(translator.makeAnd(
+                                        translator.makeAnd(equality, parentAncestor), translator.mkNot(childAncestor)))
+                                .check());
+            }
+            assertEquals(Status.SATISFIABLE, translator.makeSolverForExpression(forward).check());
+            assertEquals(Status.SATISFIABLE, translator.makeSolverForExpression(translator.mkNot(reverse)).check());
+        }
+    }
+}