Restrict pattern type guards to account for nested record matching failures

This commit is contained in:
Chris Smowton
2023-11-16 15:15:34 +00:00
parent d40311efe9
commit 6583c72c5d
6 changed files with 115 additions and 17 deletions

View File

@@ -2658,4 +2658,22 @@ class RecordPatternExpr extends Expr, @recordpatternexpr {
* Gets the `i`th subpattern of this record pattern.
*/
PatternExpr getSubPattern(int i) { result.isNthChildOf(this, i) }
/**
* Holds if this record pattern matches any record of its type.
*
* For example, for `record R(Object o) { }`, pattern `R(Object o)` is unrestricted, whereas
* pattern `R(String s)` is not because it matches a subset of `R` instances, those containing `String`s.
*/
predicate isUnrestricted() {
forall(PatternExpr subPattern, int idx | subPattern = this.getSubPattern(idx) |
subPattern.getType() =
this.getType().(Record).getCanonicalConstructor().getParameter(idx).getType() and
(
subPattern instanceof LocalVariableDeclExpr
or
subPattern.(RecordPatternExpr).isUnrestricted()
)
)
}
}

View File

@@ -194,8 +194,38 @@ class TypeTestGuard extends Guard {
)
}
/** Holds if this guard tests whether `e` has type `t`. */
predicate appliesTypeTest(Expr e, Type t) { e = testedExpr and t = testedType }
/**
* Gets the record pattern this type test binds to, if any.
*/
PatternExpr getPattern() {
result = this.(InstanceOfExpr).getPattern()
or
result = this.(PatternCase).getPattern()
}
/**
* Holds if this guard tests whether `e` has type `t`.
*
* Note that record patterns that make at least one tighter restriction than the record's definition
* (e.g. matching `record R(Object)` with `case R(String)`) means this only guarantees the tested type
* on the true branch (i.e., entering such a case guarantees `testedExpr` is a `testedType`, but failing
* the type test could mean a nested record or binding pattern didn't match but `testedExpr` is still
* of type `testedType`.)
*/
predicate appliesTypeTest(Expr e, Type t, boolean testedBranch) {
e = testedExpr and
t = testedType and
(
testedBranch = true
or
testedBranch = false and
(
this.getPattern().asRecordPattern().isUnrestricted()
or
not this.getPattern() instanceof RecordPatternExpr
)
)
}
}
private predicate switchCaseControls(SwitchCase sc, BasicBlock bb) {

View File

@@ -418,7 +418,7 @@ private predicate downcastSuccessor(VarAccess va, RefType t) {
*/
private predicate typeTestGuarded(VarAccess va, RefType t) {
exists(TypeTestGuard typeTest, BaseSsaVariable v |
typeTest.appliesTypeTest(v.getAUse(), t) and
typeTest.appliesTypeTest(v.getAUse(), t, true) and
va = v.getAUse() and
guardControls_v1(typeTest, va.getBasicBlock(), true)
)
@@ -429,7 +429,7 @@ private predicate typeTestGuarded(VarAccess va, RefType t) {
*/
predicate arrayTypeTestGuarded(ArrayAccess aa, RefType t) {
exists(TypeTestGuard typeTest, BaseSsaVariable v1, BaseSsaVariable v2, ArrayAccess aa1 |
typeTest.appliesTypeTest(aa1, t) and
typeTest.appliesTypeTest(aa1, t, true) and
aa1.getArray() = v1.getAUse() and
aa1.getIndexExpr() = v2.getAUse() and
aa.getArray() = v1.getAUse() and

View File

@@ -197,7 +197,7 @@ private module Dispatch {
exists(TypeTestGuard typeTest, BaseSsaVariable v, Expr q, RefType t |
source.getQualifier() = q and
v.getAUse() = q and
typeTest.appliesTypeTest(v.getAUse(), t) and
typeTest.appliesTypeTest(v.getAUse(), t, false) and
guardControls_v1(typeTest, q.getBasicBlock(), false) and
tgt.getDeclaringType().getSourceDeclaration().getASourceSupertype*() = t.getErasure()
)

View File

@@ -6,24 +6,51 @@ public class Test {
interface I { void take(int x); }
static class C1 implements I { public void take(int x) { sink(x); } }
static class C2 implements I { public void take(int x) { sink(x); } }
record Wrapper(Object o) implements I { public void take(int x) { sink(x); } }
record WrapperWrapper(Wrapper w) implements I { public void take(int x) { sink(x); } }
public static void test(boolean unknown, int alsoUnknown) {
public static void test(int unknown, int alsoUnknown) {
I c1or2 = unknown ? new C1() : new C2();
I i = unknown == 0 ? new C1() : unknown == 1 ? new C2() : unknown == 2 ? new Wrapper(new Object()) : new WrapperWrapper(new Wrapper(new Object()));
switch(c1or2) {
switch(i) {
case C1 c1 when alsoUnknown == 1 -> { }
default -> c1or2.take(source()); // Could call either implementation
default -> i.take(source()); // Could call any implementation
}
switch(c1or2) {
switch(i) {
case C1 c1 -> { }
default -> c1or2.take(source()); // Can't call C1.take
default -> i.take(source()); // Can't call C1.take
}
switch(c1or2) {
switch(i) {
case C1 c1 -> { }
case null, default -> c1or2.take(source()); // Can't call C1.take
case null, default -> i.take(source()); // Can't call C1.take
}
switch(i) {
case Wrapper w -> { }
default -> i.take(source()); // Can't call Wrapper.take
}
switch(i) {
case Wrapper(Object o) -> { }
default -> i.take(source()); // Can't call Wrapper.take
}
switch(i) {
case Wrapper(String s) -> { }
default -> i.take(source()); // Could call any implementation, because this might be a Wrapper(Integer) for example.
}
switch(i) {
case WrapperWrapper(Wrapper(Object o)) -> { }
default -> i.take(source()); // Can't call WrapperWrapper.take
}
switch(i) {
case WrapperWrapper(Wrapper(String s)) -> { }
default -> i.take(source()); // Could call any implementation, because this might be a WrapperWrapper(Wrapper((Integer)) for example.
}
}

View File

@@ -1,4 +1,27 @@
| Test.java:16:29:16:36 | source(...) | Test.java:7:65:7:65 | x |
| Test.java:16:29:16:36 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:21:29:21:36 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:26:40:26:47 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:18:25:18:32 | source(...) | Test.java:7:65:7:65 | x |
| Test.java:18:25:18:32 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:18:25:18:32 | source(...) | Test.java:9:74:9:74 | x |
| Test.java:18:25:18:32 | source(...) | Test.java:10:82:10:82 | x |
| Test.java:23:25:23:32 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:23:25:23:32 | source(...) | Test.java:9:74:9:74 | x |
| Test.java:23:25:23:32 | source(...) | Test.java:10:82:10:82 | x |
| Test.java:28:36:28:43 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:28:36:28:43 | source(...) | Test.java:9:74:9:74 | x |
| Test.java:28:36:28:43 | source(...) | Test.java:10:82:10:82 | x |
| Test.java:33:25:33:32 | source(...) | Test.java:7:65:7:65 | x |
| Test.java:33:25:33:32 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:33:25:33:32 | source(...) | Test.java:10:82:10:82 | x |
| Test.java:38:25:38:32 | source(...) | Test.java:7:65:7:65 | x |
| Test.java:38:25:38:32 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:38:25:38:32 | source(...) | Test.java:10:82:10:82 | x |
| Test.java:43:25:43:32 | source(...) | Test.java:7:65:7:65 | x |
| Test.java:43:25:43:32 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:43:25:43:32 | source(...) | Test.java:9:74:9:74 | x |
| Test.java:43:25:43:32 | source(...) | Test.java:10:82:10:82 | x |
| Test.java:48:25:48:32 | source(...) | Test.java:7:65:7:65 | x |
| Test.java:48:25:48:32 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:48:25:48:32 | source(...) | Test.java:9:74:9:74 | x |
| Test.java:53:25:53:32 | source(...) | Test.java:7:65:7:65 | x |
| Test.java:53:25:53:32 | source(...) | Test.java:8:65:8:65 | x |
| Test.java:53:25:53:32 | source(...) | Test.java:9:74:9:74 | x |
| Test.java:53:25:53:32 | source(...) | Test.java:10:82:10:82 | x |