Skip to content

Commit 3b0d159

Browse files
hvitvedhvitved
committed
C#: Teach guards library about unique assignments
For example, in ``` void M(object x) { var y = x == null ? 1 : 2; if (y == 2) x.ToString(); } ``` the guard `y == 2` implies that the guard `x == null` must be false, as the assignment of `2` to `y` is unique.
1 parent ab9aa7d commit 3b0d159

File tree

5 files changed

+94
-8
lines changed

5 files changed

+94
-8
lines changed

‎csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -980,6 +980,82 @@ module Internal {
980980
)
981981
}
982982

983+
/**
984+
* Holds if `def` can have a value that is not representable as an
985+
* abstract value.
986+
*/
987+
private predicate hasPossibleUnknownValue(PreSsa::Definition def) {
988+
exists(PreSsa::Definition input |
989+
input = def.getAPhiInput*() and
990+
not exists(input.getAPhiInput())
991+
|
992+
not exists(input.getDefinition().getSource())
993+
or
994+
exists(Expr e |
995+
e = stripConditionalExpr(input.getDefinition().getSource()) |
996+
not e = any(AbstractValue v).getAnExpr()
997+
)
998+
)
999+
}
1000+
1001+
/**
1002+
* Gets an ultimate definition of `def` that is not itself a phi node. The
1003+
* boolean `fromBackEdge` indicates whether the flow from `result` to `def`
1004+
* goes through a back edge.
1005+
*/
1006+
PreSsa::Definition getADefinition(PreSsa::Definition def, boolean fromBackEdge) {
1007+
result = def and
1008+
not exists(def.getAPhiInput()) and
1009+
fromBackEdge = false
1010+
or
1011+
exists(PreSsa::Definition input, PreBasicBlocks::PreBasicBlock pred, boolean fbe |
1012+
input = def.getAPhiInput() |
1013+
pred = def.getBasicBlock().getAPredecessor() and
1014+
PreSsa::ssaDefReachesEndOfBlock(pred, input, _) and
1015+
result = getADefinition(input, fbe) and
1016+
(if def.getBasicBlock().dominates(pred) then fromBackEdge = true else fromBackEdge = fbe)
1017+
)
1018+
}
1019+
1020+
/**
1021+
* Holds if `e` has abstract value `v` and may be assigned to `def`. The Boolean
1022+
* `fromBackEdge` indicates whether the flow from `e` to `def` goes through a
1023+
* back edge.
1024+
*/
1025+
private predicate possibleValue(PreSsa::Definition def, boolean fromBackEdge, Expr e, AbstractValue v) {
1026+
not hasPossibleUnknownValue(def) and
1027+
exists(PreSsa::Definition input |
1028+
input = getADefinition(def, fromBackEdge) |
1029+
e = stripConditionalExpr(input.getDefinition().getSource()) and
1030+
v.getAnExpr() = e
1031+
)
1032+
}
1033+
1034+
private predicate nonUniqueValue(PreSsa::Definition def, Expr e, AbstractValue v) {
1035+
possibleValue(def, false, e, v) and
1036+
possibleValue(def, _, any(Expr other | other != e), v)
1037+
}
1038+
1039+
/**
1040+
* Holds if `e` has abstract value `v` and may be assigned to `def` without going
1041+
* through back edges, and all other possible ultimate definitions of `def` do not
1042+
* have abstract value `v`. The trivial case where `def` is an explicit update with
1043+
* source `e is excluded.
1044+
*/
1045+
private predicate uniqueValue(PreSsa::Definition def, Expr e, AbstractValue v) {
1046+
possibleValue(def, false, e, v) and
1047+
not nonUniqueValue(def, e, v) and
1048+
exists(Expr other | possibleValue(def, _, other, _) and other != e)
1049+
}
1050+
1051+
/**
1052+
* Holds if `guard` having abstract value `vGuard` implies that `def` has
1053+
* abstract value `vDef`.
1054+
*/
1055+
private predicate guardImpliesEqual(Guard guard, AbstractValue vGuard, PreSsa::Definition def, AbstractValue vDef) {
1056+
guard = getAnEqualityCheck(def.getARead(), vGuard, vDef.getAnExpr())
1057+
}
1058+
9831059
/**
9841060
* A helper class for calculating structurally equal access/call expressions.
9851061
*/
@@ -1167,6 +1243,15 @@ module Internal {
11671243
conditionalAssignVal(g2, v2.getDualValue(), def, v) and
11681244
guardImpliesNotEqual(g1, v1, def, v)
11691245
)
1246+
or
1247+
exists(PreSsa::Definition def, Expr e, AbstractValue v |
1248+
// If `def = g2 ? v : ...` and all other assignments to `def` are different from
1249+
// `v` then a guard proving `def == v` ensures that `g2` evaluates to `v2`.
1250+
uniqueValue(def, e, v) and
1251+
guardImpliesEqual(g1, v1, def, v) and
1252+
g2.preControlsDirect(any(PreBasicBlocks::PreBasicBlock bb | e = bb.getAnElement()), v2) and
1253+
not g2.preControlsDirect(any(PreBasicBlocks::PreBasicBlock bb | g1 = bb.getAnElement()), v2)
1254+
)
11701255
}
11711256

11721257
cached

‎csharp/ql/test/query-tests/Nullness/D.cs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ public void NullGuards()
7575
var o8 = maybe ? null : "";
7676
int track = o8 == null ? 42 : 1 + 1;
7777
if (track == 2)
78-
o8.ToString(); // GOOD (false positive)
78+
o8.ToString(); // GOOD
7979
if (track != 42)
8080
o8.ToString(); // GOOD (false positive)
8181
if (track < 42)

‎csharp/ql/test/query-tests/Nullness/E.cs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -90,12 +90,12 @@ public void Ex6(int[] vals, bool b1, bool b2)
9090
switch (switchguard)
9191
{
9292
case MY_CONST_A:
93-
vals[0] = 0; // GOOD (false positive)
93+
vals[0] = 0; // GOOD
9494
break;
9595
case MY_CONST_C:
9696
break;
9797
case MY_CONST_B:
98-
vals[0] = 0; // GOOD (false positive)
98+
vals[0] = 0; // GOOD
9999
break;
100100
default:
101101
throw new Exception();

‎csharp/ql/test/query-tests/Nullness/Implications.expected‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -717,8 +717,10 @@
717717
| D.cs:76:21:76:30 | ... == ... | false | D.cs:76:21:76:22 | access to local variable o8 | non-null |
718718
| D.cs:76:21:76:30 | ... == ... | true | D.cs:75:18:75:22 | access to field maybe | true |
719719
| D.cs:76:21:76:30 | ... == ... | true | D.cs:76:21:76:22 | access to local variable o8 | null |
720+
| D.cs:77:13:77:22 | ... == ... | true | D.cs:76:21:76:30 | ... == ... | false |
720721
| D.cs:78:13:78:14 | access to local variable o8 | non-null | D.cs:75:18:75:34 | ... ? ... : ... | non-null |
721722
| D.cs:78:13:78:14 | access to local variable o8 | null | D.cs:75:18:75:34 | ... ? ... : ... | null |
723+
| D.cs:79:13:79:23 | ... != ... | false | D.cs:76:21:76:30 | ... == ... | true |
722724
| D.cs:80:13:80:14 | access to local variable o8 | non-null | D.cs:75:18:75:34 | ... ? ... : ... | non-null |
723725
| D.cs:80:13:80:14 | access to local variable o8 | null | D.cs:75:18:75:34 | ... ? ... : ... | null |
724726
| D.cs:82:13:82:14 | access to local variable o8 | non-null | D.cs:75:18:75:34 | ... ? ... : ... | non-null |
@@ -1152,6 +1154,10 @@
11521154
| E.cs:85:18:85:29 | ... != ... | true | E.cs:85:18:85:21 | access to parameter vals | non-null |
11531155
| E.cs:85:18:85:35 | ... && ... | true | E.cs:85:18:85:29 | ... != ... | true |
11541156
| E.cs:85:18:85:35 | ... && ... | true | E.cs:85:34:85:35 | access to parameter b2 | true |
1157+
| E.cs:90:17:90:27 | access to local variable switchguard | match case ...: | E.cs:83:13:83:24 | ... != ... | true |
1158+
| E.cs:90:17:90:27 | access to local variable switchguard | match case ...: | E.cs:83:29:83:30 | access to parameter b1 | true |
1159+
| E.cs:90:17:90:27 | access to local variable switchguard | match case ...: | E.cs:85:18:85:29 | ... != ... | true |
1160+
| E.cs:90:17:90:27 | access to local variable switchguard | match case ...: | E.cs:85:34:85:35 | access to parameter b2 | true |
11551161
| E.cs:107:15:107:25 | Int32[] arr2 = ... | non-null | E.cs:107:15:107:18 | access to local variable arr2 | non-null |
11561162
| E.cs:107:15:107:25 | Int32[] arr2 = ... | null | E.cs:107:15:107:18 | access to local variable arr2 | null |
11571163
| E.cs:109:13:109:39 | ... = ... | non-null | E.cs:109:13:109:16 | access to local variable arr2 | non-null |

‎csharp/ql/test/query-tests/Nullness/NullMaybe.expected‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@
1010
| D.cs:32:9:32:13 | access to parameter param | Variable '$@' may be null here as suggested by $@ null check. | D.cs:26:32:26:36 | param | param | D.cs:28:13:28:25 | ... != ... | this |
1111
| D.cs:62:13:62:14 | access to local variable o5 | Variable '$@' may be null here because of $@ assignment. | D.cs:58:13:58:14 | o5 | o5 | D.cs:58:13:58:41 | String o5 = ... | this |
1212
| D.cs:73:13:73:14 | access to local variable o7 | Variable '$@' may be null here because of $@ assignment. | D.cs:68:13:68:14 | o7 | o7 | D.cs:68:13:68:34 | String o7 = ... | this |
13-
| D.cs:78:13:78:14 | access to local variable o8 | Variable '$@' may be null here because of $@ assignment. | D.cs:75:13:75:14 | o8 | o8 | D.cs:75:13:75:34 | String o8 = ... | this |
1413
| D.cs:80:13:80:14 | access to local variable o8 | Variable '$@' may be null here because of $@ assignment. | D.cs:75:13:75:14 | o8 | o8 | D.cs:75:13:75:34 | String o8 = ... | this |
1514
| D.cs:82:13:82:14 | access to local variable o8 | Variable '$@' may be null here because of $@ assignment. | D.cs:75:13:75:14 | o8 | o8 | D.cs:75:13:75:34 | String o8 = ... | this |
1615
| D.cs:84:13:84:14 | access to local variable o8 | Variable '$@' may be null here because of $@ assignment. | D.cs:75:13:75:14 | o8 | o8 | D.cs:75:13:75:34 | String o8 = ... | this |
@@ -55,10 +54,6 @@
5554
| E.cs:43:13:43:16 | access to local variable last | Variable '$@' may be null here because of $@ assignment. | E.cs:32:16:32:19 | last | last | E.cs:37:9:37:19 | ... = ... | this |
5655
| E.cs:61:13:61:17 | access to local variable slice | Variable '$@' may be null here because of $@ assignment. | E.cs:51:22:51:26 | slice | slice | E.cs:51:22:51:33 | List<String> slice = ... | this |
5756
| E.cs:73:13:73:15 | access to parameter arr | Variable '$@' may be null here as suggested by $@ null check. | E.cs:66:40:66:42 | arr | arr | E.cs:70:22:70:32 | ... == ... | this |
58-
| E.cs:93:17:93:20 | access to parameter vals | Variable '$@' may be null here as suggested by $@ null check. | E.cs:80:27:80:30 | vals | vals | E.cs:83:13:83:24 | ... != ... | this |
59-
| E.cs:93:17:93:20 | access to parameter vals | Variable '$@' may be null here as suggested by $@ null check. | E.cs:80:27:80:30 | vals | vals | E.cs:85:18:85:29 | ... != ... | this |
60-
| E.cs:98:17:98:20 | access to parameter vals | Variable '$@' may be null here as suggested by $@ null check. | E.cs:80:27:80:30 | vals | vals | E.cs:83:13:83:24 | ... != ... | this |
61-
| E.cs:98:17:98:20 | access to parameter vals | Variable '$@' may be null here as suggested by $@ null check. | E.cs:80:27:80:30 | vals | vals | E.cs:85:18:85:29 | ... != ... | this |
6257
| E.cs:112:13:112:16 | access to local variable arr2 | Variable '$@' may be null here because of $@ assignment. | E.cs:107:15:107:18 | arr2 | arr2 | E.cs:107:15:107:25 | Int32[] arr2 = ... | this |
6358
| E.cs:125:33:125:35 | access to local variable obj | Variable '$@' may be null here because of $@ assignment. | E.cs:119:13:119:15 | obj | obj | E.cs:137:25:137:34 | ... = ... | this |
6459
| E.cs:159:13:159:16 | access to local variable obj2 | Variable '$@' may be null here as suggested by $@ null check. | E.cs:152:16:152:19 | obj2 | obj2 | E.cs:153:13:153:24 | ... != ... | this |

0 commit comments

Comments
 (0)