diff --git a/liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_correct/Test.java new file mode 100644 index 00000000..32a3ff4a --- /dev/null +++ b/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; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_correct/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_correct/ThrowableRefinements.java new file mode 100644 index 00000000..633f1305 --- /dev/null +++ b/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); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_error/Test.java new file mode 100644 index 00000000..19fe6b15 --- /dev/null +++ b/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 + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_error/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/subtype_assignment_error/ThrowableRefinements.java new file mode 100644 index 00000000..74aae33a --- /dev/null +++ b/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); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index ac3eadd4..4c622832 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/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 staticConstantAxioms = new ArrayList<>(); + private final List referenceIdentityAxioms = new ArrayList<>(); + private final Set> 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> left = referenceViews(name1, e1); + Map> right = referenceViews(name2, e2); + BoolExpr identity = null; + for (Map.Entry> 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> referenceViews(String name, Expr nativeView) { + Map> 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) diff --git a/liquidjava-verifier/src/test/java/liquidjava/smt/ReferenceEqualityTest.java b/liquidjava-verifier/src/test/java/liquidjava/smt/ReferenceEqualityTest.java new file mode 100644 index 00000000..8e036ae9 --- /dev/null +++ b/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()); + } + } +}