Skip to content

Commit e6602a6

Browse files
CatarinaGamboaCatarinaGamboa
committed
Preserve reference identity across recorded upcasts
1 parent dcfc4eb commit e6602a6

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)