C#: Add test for guard implications logic

This commit is contained in:
Tom Hvitved
2018-11-05 16:37:46 +01:00
parent f5e6b79add
commit 2d25a04a2e
3 changed files with 136 additions and 4 deletions

View File

@@ -138,10 +138,11 @@ class DereferenceableExpr extends Expr {
exists(boolean branch |
branch = v.getValue() |
// Comparison with `null`, for example `x != null`
exists(ComparisonTest ct, ComparisonKind ck |
exists(ComparisonTest ct, ComparisonKind ck, NullLiteral nl |
ct.getExpr() = result and
ct.getAnArgument() = this and
ct.getAnArgument() instanceof NullLiteral and
ct.getAnArgument() = nl and
this != nl and
ck = ct.getComparisonKind() |
ck.isEquality() and isNull = branch
or
@@ -609,7 +610,8 @@ module Internal {
or
exists(boolean isNull |
v2 = any(NullValue nv | if nv.isNull() then isNull = true else isNull = false) |
e1 = e2.(DereferenceableExpr).getANullCheck(v1, isNull)
e1 = e2.(DereferenceableExpr).getANullCheck(v1, isNull) and
(e1 != e2 or v1 != v2)
)
or
e1 instanceof DereferenceableExpr and
@@ -624,7 +626,7 @@ module Internal {
* Holds if `e1` having some abstract value, `v`, implies that `e2` has the same
* abstract value `v`.
*/
private predicate impliesStepIdentity(Expr e1, Expr e2) {
predicate impliesStepIdentity(Expr e1, Expr e2) {
exists(PreSsa::Definition def |
def.getDefinition().getSource() = e2 |
e1 = def.getARead()

View File

@@ -0,0 +1,120 @@
impliesStep
| Guards.cs:10:13:10:25 | !... | false | Guards.cs:10:14:10:25 | !... | true |
| Guards.cs:10:13:10:25 | !... | true | Guards.cs:10:14:10:25 | !... | false |
| Guards.cs:10:14:10:25 | !... | false | Guards.cs:10:13:10:25 | !... | true |
| Guards.cs:10:14:10:25 | !... | false | Guards.cs:10:16:10:24 | ... == ... | true |
| Guards.cs:10:14:10:25 | !... | true | Guards.cs:10:13:10:25 | !... | false |
| Guards.cs:10:14:10:25 | !... | true | Guards.cs:10:16:10:24 | ... == ... | false |
| Guards.cs:10:16:10:24 | ... == ... | false | Guards.cs:10:14:10:25 | !... | true |
| Guards.cs:10:16:10:24 | ... == ... | false | Guards.cs:10:16:10:16 | access to parameter s | non-null |
| Guards.cs:10:16:10:24 | ... == ... | true | Guards.cs:10:14:10:25 | !... | false |
| Guards.cs:10:16:10:24 | ... == ... | true | Guards.cs:10:16:10:16 | access to parameter s | null |
| Guards.cs:24:13:24:21 | ... != ... | false | Guards.cs:24:13:24:13 | access to parameter s | null |
| Guards.cs:24:13:24:21 | ... != ... | true | Guards.cs:24:13:24:13 | access to parameter s | non-null |
| Guards.cs:32:13:32:36 | !... | false | Guards.cs:32:13:32:51 | ... & ... | false |
| Guards.cs:32:13:32:36 | !... | false | Guards.cs:32:14:32:36 | call to method IsNullOrEmpty | true |
| Guards.cs:32:13:32:36 | !... | true | Guards.cs:32:14:32:36 | call to method IsNullOrEmpty | false |
| Guards.cs:32:13:32:51 | ... & ... | true | Guards.cs:32:13:32:36 | !... | true |
| Guards.cs:32:13:32:51 | ... & ... | true | Guards.cs:32:40:32:51 | !... | true |
| Guards.cs:32:14:32:36 | call to method IsNullOrEmpty | false | Guards.cs:32:13:32:36 | !... | true |
| Guards.cs:32:14:32:36 | call to method IsNullOrEmpty | false | Guards.cs:32:35:32:35 | access to parameter x | non-null |
| Guards.cs:32:14:32:36 | call to method IsNullOrEmpty | true | Guards.cs:32:13:32:36 | !... | false |
| Guards.cs:32:40:32:51 | !... | false | Guards.cs:32:13:32:51 | ... & ... | false |
| Guards.cs:32:40:32:51 | !... | false | Guards.cs:32:42:32:50 | ... == ... | true |
| Guards.cs:32:40:32:51 | !... | true | Guards.cs:32:42:32:50 | ... == ... | false |
| Guards.cs:32:42:32:50 | ... == ... | false | Guards.cs:32:40:32:51 | !... | true |
| Guards.cs:32:42:32:50 | ... == ... | false | Guards.cs:32:42:32:42 | access to parameter y | non-null |
| Guards.cs:32:42:32:50 | ... == ... | true | Guards.cs:32:40:32:51 | !... | false |
| Guards.cs:32:42:32:50 | ... == ... | true | Guards.cs:32:42:32:42 | access to parameter y | null |
| Guards.cs:35:13:35:21 | ... == ... | false | Guards.cs:35:13:35:13 | access to parameter x | non-null |
| Guards.cs:35:13:35:21 | ... == ... | true | Guards.cs:35:13:35:13 | access to parameter x | null |
| Guards.cs:35:13:35:21 | ... == ... | true | Guards.cs:35:13:35:34 | ... \|\| ... | true |
| Guards.cs:35:13:35:34 | ... \|\| ... | false | Guards.cs:35:13:35:21 | ... == ... | false |
| Guards.cs:35:13:35:34 | ... \|\| ... | false | Guards.cs:35:26:35:34 | ... == ... | false |
| Guards.cs:35:26:35:34 | ... == ... | false | Guards.cs:35:26:35:26 | access to parameter y | non-null |
| Guards.cs:35:26:35:34 | ... == ... | true | Guards.cs:35:13:35:34 | ... \|\| ... | true |
| Guards.cs:35:26:35:34 | ... == ... | true | Guards.cs:35:26:35:26 | access to parameter y | null |
| Guards.cs:38:13:38:37 | !... | false | Guards.cs:38:15:38:36 | ... \|\| ... | true |
| Guards.cs:38:13:38:37 | !... | true | Guards.cs:38:15:38:36 | ... \|\| ... | false |
| Guards.cs:38:15:38:23 | ... == ... | false | Guards.cs:38:15:38:15 | access to parameter x | non-null |
| Guards.cs:38:15:38:23 | ... == ... | true | Guards.cs:38:15:38:15 | access to parameter x | null |
| Guards.cs:38:15:38:23 | ... == ... | true | Guards.cs:38:15:38:36 | ... \|\| ... | true |
| Guards.cs:38:15:38:36 | ... \|\| ... | false | Guards.cs:38:13:38:37 | !... | true |
| Guards.cs:38:15:38:36 | ... \|\| ... | false | Guards.cs:38:15:38:23 | ... == ... | false |
| Guards.cs:38:15:38:36 | ... \|\| ... | false | Guards.cs:38:28:38:36 | ... == ... | false |
| Guards.cs:38:15:38:36 | ... \|\| ... | true | Guards.cs:38:13:38:37 | !... | false |
| Guards.cs:38:28:38:36 | ... == ... | false | Guards.cs:38:28:38:28 | access to parameter y | non-null |
| Guards.cs:38:28:38:36 | ... == ... | true | Guards.cs:38:15:38:36 | ... \|\| ... | true |
| Guards.cs:38:28:38:36 | ... == ... | true | Guards.cs:38:28:38:28 | access to parameter y | null |
| Guards.cs:41:13:41:39 | !... | false | Guards.cs:41:14:41:39 | !... | true |
| Guards.cs:41:13:41:39 | !... | true | Guards.cs:41:14:41:39 | !... | false |
| Guards.cs:41:14:41:39 | !... | false | Guards.cs:41:13:41:39 | !... | true |
| Guards.cs:41:14:41:39 | !... | false | Guards.cs:41:15:41:39 | !... | true |
| Guards.cs:41:14:41:39 | !... | true | Guards.cs:41:13:41:39 | !... | false |
| Guards.cs:41:14:41:39 | !... | true | Guards.cs:41:15:41:39 | !... | false |
| Guards.cs:41:15:41:39 | !... | false | Guards.cs:41:14:41:39 | !... | true |
| Guards.cs:41:15:41:39 | !... | false | Guards.cs:41:17:41:38 | ... && ... | true |
| Guards.cs:41:15:41:39 | !... | true | Guards.cs:41:14:41:39 | !... | false |
| Guards.cs:41:15:41:39 | !... | true | Guards.cs:41:17:41:38 | ... && ... | false |
| Guards.cs:41:17:41:25 | ... != ... | false | Guards.cs:41:17:41:17 | access to parameter x | null |
| Guards.cs:41:17:41:25 | ... != ... | false | Guards.cs:41:17:41:38 | ... && ... | false |
| Guards.cs:41:17:41:25 | ... != ... | true | Guards.cs:41:17:41:17 | access to parameter x | non-null |
| Guards.cs:41:17:41:38 | ... && ... | false | Guards.cs:41:15:41:39 | !... | true |
| Guards.cs:41:17:41:38 | ... && ... | true | Guards.cs:41:15:41:39 | !... | false |
| Guards.cs:41:17:41:38 | ... && ... | true | Guards.cs:41:17:41:25 | ... != ... | true |
| Guards.cs:41:17:41:38 | ... && ... | true | Guards.cs:41:30:41:38 | ... != ... | true |
| Guards.cs:41:30:41:38 | ... != ... | false | Guards.cs:41:17:41:38 | ... && ... | false |
| Guards.cs:41:30:41:38 | ... != ... | false | Guards.cs:41:30:41:30 | access to parameter y | null |
| Guards.cs:41:30:41:38 | ... != ... | true | Guards.cs:41:30:41:30 | access to parameter y | non-null |
| Guards.cs:44:13:44:25 | ... != ... | false | Guards.cs:44:13:44:17 | access to field Field | null |
| Guards.cs:44:13:44:25 | ... != ... | true | Guards.cs:44:13:44:17 | access to field Field | non-null |
| Guards.cs:47:13:47:25 | ... != ... | false | Guards.cs:47:13:47:17 | access to field Field | null |
| Guards.cs:47:13:47:25 | ... != ... | true | Guards.cs:47:13:47:17 | access to field Field | non-null |
| Guards.cs:53:13:53:27 | ... == ... | false | Guards.cs:53:13:53:19 | access to field Field | non-null |
| Guards.cs:53:13:53:27 | ... == ... | true | Guards.cs:53:13:53:19 | access to field Field | null |
| Guards.cs:60:13:60:45 | ... == ... | false | Guards.cs:60:13:60:37 | access to field Field | non-null |
| Guards.cs:60:13:60:45 | ... == ... | true | Guards.cs:60:13:60:37 | access to field Field | null |
| Guards.cs:68:16:68:24 | ... != ... | false | Guards.cs:68:16:68:16 | access to parameter s | null |
| Guards.cs:68:16:68:24 | ... != ... | true | Guards.cs:68:16:68:16 | access to parameter s | non-null |
| Guards.cs:78:13:78:26 | ... == ... | true | Guards.cs:78:15:78:21 | access to property Length | non-null |
| Guards.cs:78:15:78:21 | access to property Length | non-null | Guards.cs:78:13:78:13 | access to parameter s | non-null |
| Guards.cs:78:15:78:21 | access to property Length | null | Guards.cs:78:13:78:13 | access to parameter s | null |
| Guards.cs:80:13:80:25 | ... > ... | true | Guards.cs:80:15:80:21 | access to property Length | non-null |
| Guards.cs:80:15:80:21 | access to property Length | non-null | Guards.cs:80:13:80:13 | access to parameter s | non-null |
| Guards.cs:80:15:80:21 | access to property Length | null | Guards.cs:80:13:80:13 | access to parameter s | null |
| Guards.cs:82:13:82:26 | ... >= ... | true | Guards.cs:82:15:82:21 | access to property Length | non-null |
| Guards.cs:82:15:82:21 | access to property Length | non-null | Guards.cs:82:13:82:13 | access to parameter s | non-null |
| Guards.cs:82:15:82:21 | access to property Length | null | Guards.cs:82:13:82:13 | access to parameter s | null |
| Guards.cs:84:13:84:26 | ... < ... | true | Guards.cs:84:15:84:21 | access to property Length | non-null |
| Guards.cs:84:15:84:21 | access to property Length | non-null | Guards.cs:84:13:84:13 | access to parameter s | non-null |
| Guards.cs:84:15:84:21 | access to property Length | null | Guards.cs:84:13:84:13 | access to parameter s | null |
| Guards.cs:86:13:86:27 | ... <= ... | true | Guards.cs:86:15:86:21 | access to property Length | non-null |
| Guards.cs:86:15:86:21 | access to property Length | non-null | Guards.cs:86:13:86:13 | access to parameter s | non-null |
| Guards.cs:86:15:86:21 | access to property Length | null | Guards.cs:86:13:86:13 | access to parameter s | null |
| Guards.cs:88:13:88:29 | ... != ... | false | Guards.cs:88:15:88:21 | access to property Length | null |
| Guards.cs:88:13:88:29 | ... != ... | true | Guards.cs:88:15:88:21 | access to property Length | non-null |
| Guards.cs:88:15:88:21 | access to property Length | non-null | Guards.cs:88:13:88:13 | access to parameter s | non-null |
| Guards.cs:88:15:88:21 | access to property Length | null | Guards.cs:88:13:88:13 | access to parameter s | null |
| Guards.cs:92:13:92:25 | ... - ... | non-null | Guards.cs:92:15:92:21 | access to property Length | non-null |
| Guards.cs:92:13:92:25 | ... - ... | null | Guards.cs:92:15:92:21 | access to property Length | null |
| Guards.cs:92:13:92:30 | ... != ... | false | Guards.cs:92:13:92:25 | ... - ... | non-null |
| Guards.cs:92:15:92:21 | access to property Length | non-null | Guards.cs:92:13:92:13 | access to parameter s | non-null |
| Guards.cs:92:15:92:21 | access to property Length | null | Guards.cs:92:13:92:13 | access to parameter s | null |
| Guards.cs:96:13:96:19 | ... == ... | true | Guards.cs:96:13:96:13 | access to parameter s | non-null |
| Guards.cs:104:13:104:45 | ... == ... | false | Guards.cs:104:13:104:37 | access to field Field | non-null |
| Guards.cs:104:13:104:45 | ... == ... | true | Guards.cs:104:13:104:37 | access to field Field | null |
| Guards.cs:125:21:125:31 | call to method Equals | non-null | Guards.cs:125:18:125:19 | access to parameter s1 | non-null |
| Guards.cs:125:21:125:31 | call to method Equals | null | Guards.cs:125:18:125:19 | access to parameter s1 | null |
| Guards.cs:130:13:130:21 | ... is ... | false | Guards.cs:130:13:130:13 | access to parameter s | non-null |
| Guards.cs:130:13:130:21 | ... is ... | true | Guards.cs:130:13:130:13 | access to parameter s | null |
| Guards.cs:137:13:137:23 | ... is ... | true | Guards.cs:137:13:137:13 | access to parameter s | non-null |
| Guards.cs:144:13:144:25 | ... is ... | true | Guards.cs:144:13:144:13 | access to parameter o | non-null |
| Guards.cs:151:17:151:17 | access to parameter o | match case ...: | Guards.cs:151:17:151:17 | access to parameter o | non-null |
| Guards.cs:151:17:151:17 | access to parameter o | match case ...: | Guards.cs:151:17:151:17 | access to parameter o | null |
| Guards.cs:151:17:151:17 | access to parameter o | match case Action<Object>: | Guards.cs:151:17:151:17 | access to parameter o | non-null |
| Guards.cs:151:17:151:17 | access to parameter o | match case Action<String> a: | Guards.cs:151:17:151:17 | access to parameter o | non-null |
| Guards.cs:151:17:151:17 | access to parameter o | non-match case ...: | Guards.cs:151:17:151:17 | access to parameter o | non-null |
impliesStepIdentity
| Guards.cs:72:31:72:31 | access to parameter s | Guards.cs:71:17:71:20 | null |
| Guards.cs:145:20:145:20 | access to local variable s | Guards.cs:144:13:144:13 | access to parameter o |
| Guards.cs:156:24:156:24 | access to local variable a | Guards.cs:151:17:151:17 | access to parameter o |

View File

@@ -0,0 +1,10 @@
import csharp
import semmle.code.csharp.controlflow.Guards
query predicate impliesStep(Expr e1, AbstractValue v1, Expr e2, AbstractValue v2) {
Internal::impliesStep(e1, v1, e2, v2)
}
query predicate impliesStepIdentity(Expr e1, Expr e2) {
Internal::impliesStepIdentity(e1, e2)
}