Skip to content

Commit 9fb4cca

Browse files
CatarinaGamboaCatarinaGamboa
authored
Fix verifier reference equality across recorded upcasts (#383)
Assigning a caught `IOException` to an `Exception` local currently crashes verification with incompatible Z3 sorts. Translate mixed reference equality through an exact recorded supertype view, symmetrically for either operand order. Preserve alias identity across native and inherited reference views with cached, on-demand solver equivalences between their equality propositions. Equality itself remains a single typed equality, so negating it for `!=` preserves the same identity semantics. Numeric handling is unchanged; unrelated mixed reference sorts remain outside this fix. Adds passing caught-upcast and inherited Throwable state/alias cases, failing unknown-state and already-initialized-cause cases, and solver regressions covering both equality/inequality operand orders and satisfiable distinct references. Validation: `ReferenceEqualityTest` passes; both CLI fixtures produce exactly their expected outcomes. The full Java 20 CI suite passed on the final on-demand implementation; an earlier local `mvn test` passed 390 tests. Fixes #377.
1 parent 37c3594 commit 9fb4cca

6 files changed

Lines changed: 215 additions & 0 deletions

File tree

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

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
package testSuite.classes.subtype_assignment_correct;
2+
3+
import java.io.IOException;
4+
import liquidjava.specification.Refinement;
5+
6+
public class Test {
7+
static void load() throws IOException {
8+
throw new IOException("truncated");
9+
}
10+
11+
static void knownState(@Refinement("noThrowable(_)") IOException original, Exception previous) {
12+
Exception failure = original;
13+
Exception copy = failure;
14+
copy.initCause(previous);
15+
}
16+
17+
static void run(Exception previous) {
18+
Exception failure = null;
19+
try {
20+
load();
21+
} catch (IOException e) {
22+
failure = e;
23+
}
24+
if (failure != null) {
25+
Exception copy = failure;
26+
@Refinement("_ == 1") int checked = 1;
27+
}
28+
}
29+
}

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package testSuite.classes.subtype_assignment_correct;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@ExternalRefinementsFor("java.lang.Throwable")
8+
@StateSet({"withThrowable", "noThrowable"})
9+
public interface ThrowableRefinements {
10+
@StateRefinement(to = "noThrowable(this)")
11+
void Throwable(String message);
12+
13+
@StateRefinement(to = "withThrowable(this)")
14+
void Throwable(String message, Throwable cause);
15+
16+
@StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
17+
Throwable initCause(Throwable cause);
18+
}

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
package testSuite.classes.subtype_assignment_error;
2+
3+
import java.io.IOException;
4+
import liquidjava.specification.Refinement;
5+
6+
public class Test {
7+
static void load() throws IOException {
8+
throw new IOException("truncated");
9+
}
10+
11+
static void alreadyHasCause(@Refinement("withThrowable(_)") IOException original, Exception previous) {
12+
Exception failure = original;
13+
failure.initCause(previous); // Expect: State Refinement Error
14+
}
15+
16+
static void run(Exception previous) {
17+
Exception failure = null;
18+
try {
19+
load();
20+
} catch (IOException e) {
21+
failure = e;
22+
}
23+
if (failure != null) {
24+
failure.initCause(previous); // Expect: State Refinement Error
25+
}
26+
}
27+
}

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package testSuite.classes.subtype_assignment_error;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@ExternalRefinementsFor("java.lang.Throwable")
8+
@StateSet({"withThrowable", "noThrowable"})
9+
public interface ThrowableRefinements {
10+
@StateRefinement(to = "noThrowable(this)")
11+
void Throwable(String message);
12+
13+
@StateRefinement(to = "withThrowable(this)")
14+
void Throwable(String message, Throwable cause);
15+
16+
@StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
17+
Throwable initCause(Throwable cause);
18+
}

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

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,10 @@
1717
import java.util.ArrayList;
1818
import java.util.Arrays;
1919
import java.util.HashMap;
20+
import java.util.HashSet;
2021
import java.util.List;
2122
import java.util.Map;
23+
import java.util.Set;
2224
import java.util.stream.Collectors;
2325

2426
import liquidjava.diagnostics.errors.LJError;
@@ -53,6 +55,8 @@ public class TranslatorToZ3 implements AutoCloseable {
5355
* appears symbolically in counterexample models.
5456
*/
5557
private final List<BoolExpr> staticConstantAxioms = new ArrayList<>();
58+
private final List<BoolExpr> referenceIdentityAxioms = new ArrayList<>();
59+
private final Set<Set<String>> referenceIdentityPairs = new HashSet<>();
5660

5761
public TranslatorToZ3(liquidjava.processor.context.Context context) {
5862
TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation);
@@ -67,6 +71,8 @@ public Solver makeSolverForExpression(Expr<?> e) {
6771
Solver solver = z3.mkSolver();
6872
for (BoolExpr axiom : staticConstantAxioms)
6973
solver.add(axiom);
74+
for (BoolExpr axiom : referenceIdentityAxioms)
75+
solver.add(axiom);
7076
solver.add((BoolExpr) e);
7177
return solver;
7278
}
@@ -253,9 +259,68 @@ public Expr<?> makeEquals(Expr<?> e1, Expr<?> e2) {
253259
return z3.mkFPEq(toFP(e1), toFP(e2));
254260
if (e1 instanceof RealExpr || e2 instanceof RealExpr)
255261
return z3.mkEq(toReal(e1), toReal(e2));
262+
if (isReference(e1) && isReference(e2))
263+
addReferenceIdentityAxioms(e1, e2);
264+
if (!e1.getSort().equals(e2.getSort()) && isReference(e1) && isReference(e2)) {
265+
Expr<?> view = supertypeView(e2, e1.getSort());
266+
if (view != null)
267+
e2 = view;
268+
else {
269+
view = supertypeView(e1, e2.getSort());
270+
if (view != null)
271+
e1 = view;
272+
}
273+
}
256274
return z3.mkEq(e1, e2);
257275
}
258276

277+
private static boolean isReference(Expr<?> expression) {
278+
return expression.getSort().getSortKind() == Z3_sort_kind.Z3_UNINTERPRETED_SORT;
279+
}
280+
281+
private Expr<?> supertypeView(Expr<?> expression, Sort sort) {
282+
String name = exprToNameTranslation.get(expression);
283+
if (name == null)
284+
return null;
285+
for (Expr<?> view : varSuperTypes.getOrDefault(name, List.of()))
286+
if (view.getSort().equals(sort))
287+
return view;
288+
return null;
289+
}
290+
291+
/**
292+
* Each reference has separate constants for its Java type views. Identity must agree across every shared view,
293+
* including under negation: changing the view of an alias cannot change equality or inequality.
294+
*/
295+
private void addReferenceIdentityAxioms(Expr<?> e1, Expr<?> e2) {
296+
String name1 = exprToNameTranslation.get(e1);
297+
String name2 = exprToNameTranslation.get(e2);
298+
if (name1 == null || name2 == null || name1.equals(name2) || !referenceIdentityPairs.add(Set.of(name1, name2)))
299+
return;
300+
Map<Sort, Expr<?>> left = referenceViews(name1, e1);
301+
Map<Sort, Expr<?>> right = referenceViews(name2, e2);
302+
BoolExpr identity = null;
303+
for (Map.Entry<Sort, Expr<?>> view : left.entrySet()) {
304+
Expr<?> other = right.get(view.getKey());
305+
if (other == null)
306+
continue;
307+
BoolExpr equality = z3.mkEq(view.getValue(), other);
308+
if (identity == null)
309+
identity = equality;
310+
else
311+
referenceIdentityAxioms.add(z3.mkEq(identity, equality));
312+
}
313+
}
314+
315+
private Map<Sort, Expr<?>> referenceViews(String name, Expr<?> nativeView) {
316+
Map<Sort, Expr<?>> views = new HashMap<>();
317+
views.put(nativeView.getSort(), nativeView);
318+
for (Expr<?> view : varSuperTypes.getOrDefault(name, List.of()))
319+
if (isReference(view))
320+
views.put(view.getSort(), view);
321+
return views;
322+
}
323+
259324
@SuppressWarnings({ "unchecked", "rawtypes" })
260325
public Expr<?> makeLt(Expr<?> e1, Expr<?> e2) {
261326
if (e1 instanceof FPExpr || e2 instanceof FPExpr)

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

Lines changed: 58 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,58 @@
1+
package liquidjava.smt;
2+
3+
import static org.junit.jupiter.api.Assertions.assertEquals;
4+
5+
import com.microsoft.z3.Expr;
6+
import com.microsoft.z3.Status;
7+
import liquidjava.processor.context.Context;
8+
import liquidjava.rj_language.Predicate;
9+
import org.junit.jupiter.api.AfterEach;
10+
import org.junit.jupiter.api.Test;
11+
import spoon.Launcher;
12+
13+
class ReferenceEqualityTest {
14+
private final Context context = Context.getInstance();
15+
16+
@AfterEach
17+
void resetContext() {
18+
context.reinitializeAllContext();
19+
}
20+
21+
@Test
22+
void referenceIdentityAgreesAcrossNativeAndAncestorViews() throws Exception {
23+
var factory = new Launcher().getFactory();
24+
context.addVarToContext("child", factory.Type().createReference(java.io.IOException.class), new Predicate(),
25+
factory.Code().createCodeSnippetStatement(""));
26+
context.addVarToContext("parent", factory.Type().createReference(Exception.class), new Predicate(),
27+
factory.Code().createCodeSnippetStatement(""));
28+
context.addVarToContext("ancestor", factory.Type().createReference(Throwable.class), new Predicate(),
29+
factory.Code().createCodeSnippetStatement(""));
30+
try (TranslatorToZ3 translator = new TranslatorToZ3(context)) {
31+
Expr<?> child = translator.makeVariable("child");
32+
Expr<?> parent = translator.makeVariable("parent");
33+
Expr<?> forward = translator.makeEquals(child, parent);
34+
Expr<?> reverse = translator.makeEquals(parent, child);
35+
assertEquals(Status.UNSATISFIABLE, translator
36+
.makeSolverForExpression(translator.mkNot(translator.makeEquals(forward, reverse))).check());
37+
Expr<?> ancestor = translator.makeVariable("ancestor");
38+
Expr<?> childAncestor = translator.makeEquals(child, ancestor);
39+
Expr<?> parentAncestor = translator.makeEquals(parent, ancestor);
40+
for (Expr<?> equality : new Expr<?>[] { forward, reverse }) {
41+
Expr<?> sameAncestor = translator.makeAnd(childAncestor, parentAncestor);
42+
assertEquals(Status.UNSATISFIABLE, translator
43+
.makeSolverForExpression(translator.makeAnd(sameAncestor, translator.mkNot(equality))).check());
44+
assertEquals(Status.UNSATISFIABLE,
45+
translator.makeSolverForExpression(translator
46+
.makeAnd(translator.makeAnd(equality, childAncestor), translator.mkNot(parentAncestor)))
47+
.check());
48+
assertEquals(Status.UNSATISFIABLE,
49+
translator
50+
.makeSolverForExpression(translator.makeAnd(
51+
translator.makeAnd(equality, parentAncestor), translator.mkNot(childAncestor)))
52+
.check());
53+
}
54+
assertEquals(Status.SATISFIABLE, translator.makeSolverForExpression(forward).check());
55+
assertEquals(Status.SATISFIABLE, translator.makeSolverForExpression(translator.mkNot(reverse)).check());
56+
}
57+
}
58+
}

0 commit comments

Comments
 (0)