Skip to content

Commit 063733a

Browse files
committed
C#: Implement CFG for not patterns
1 parent ab85b2c commit 063733a

File tree

14 files changed

+543
-184
lines changed

14 files changed

+543
-184
lines changed

csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll

Lines changed: 83 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -232,37 +232,61 @@ private Expr getQualifier(QualifiableExpr e) {
232232
result = e.getChildExpr(-1)
233233
}
234234

235+
pragma[noinline]
236+
private predicate typePatternMustHaveMatchingCompletion(
237+
TypePatternExpr tpe, Type t, Type strippedType
238+
) {
239+
exists(Expr e, Expr stripped | mustHaveMatchingCompletion(e, tpe) |
240+
stripped = e.stripCasts() and
241+
t = tpe.getCheckedType() and
242+
strippedType = stripped.getType() and
243+
not t.containsTypeParameters() and
244+
not strippedType.containsTypeParameters()
245+
)
246+
}
247+
248+
pragma[noinline]
249+
private Type typePatternCommonSubTypeLeft(Type t) {
250+
typePatternMustHaveMatchingCompletion(_, t, _) and
251+
result.isImplicitlyConvertibleTo(t) and
252+
not result instanceof DynamicType
253+
}
254+
255+
pragma[noinline]
256+
private Type typePatternCommonSubTypeRight(Type strippedType) {
257+
typePatternMustHaveMatchingCompletion(_, _, strippedType) and
258+
result.isImplicitlyConvertibleTo(strippedType) and
259+
not result instanceof DynamicType
260+
}
261+
262+
pragma[noinline]
263+
private predicate typePatternCommonSubType(Type t, Type strippedType) {
264+
typePatternCommonSubTypeLeft(t) = typePatternCommonSubTypeRight(strippedType)
265+
}
266+
235267
/**
236-
* Holds if expression `e` constantly matches (`value = true`) or constantly
237-
* non-matches (`value = false`).
268+
* Holds if pattern expression `pe` constantly matches (`value = true`) or
269+
* constantly non-matches (`value = false`).
238270
*/
239-
private predicate isMatchingConstant(Expr e, boolean value) {
240-
exists(Switch s | mustHaveMatchingCompletion(s, e) |
241-
exists(Expr stripped | stripped = s.getExpr().stripCasts() |
242-
exists(Case c, string strippedValue |
243-
c = s.getACase() and
244-
e = c.getPattern() and
245-
strippedValue = stripped.getValue()
246-
|
247-
if strippedValue = e.getValue() then value = true else value = false
248-
)
249-
or
250-
exists(Case c, TypePatternExpr tpe, Type t, Type strippedType | c = s.getACase() |
251-
tpe = c.getPattern() and
252-
e = tpe and
253-
t = tpe.getCheckedType() and
254-
strippedType = stripped.getType() and
255-
not t.isImplicitlyConvertibleTo(strippedType) and
256-
not t instanceof Interface and
257-
not t.containsTypeParameters() and
258-
not strippedType.containsTypeParameters() and
259-
value = false
271+
private predicate isMatchingConstant(PatternExpr pe, boolean value) {
272+
exists(Expr e | mustHaveMatchingCompletion(e, pe) |
273+
exists(Expr stripped | stripped = e.stripCasts() |
274+
exists(string strippedValue, string patternValue |
275+
strippedValue = stripped.getValue() and
276+
patternValue = pe.getValue() and
277+
if strippedValue = patternValue then value = true else value = false
260278
)
261279
)
262280
or
263-
e instanceof DiscardPatternExpr and
281+
pe instanceof DiscardPatternExpr and
264282
value = true
265283
)
284+
or
285+
exists(Type t, Type strippedType |
286+
typePatternMustHaveMatchingCompletion(pe, t, strippedType) and
287+
not typePatternCommonSubType(t, strippedType) and
288+
value = false
289+
)
266290
}
267291

268292
private class Overflowable extends UnaryOperation {
@@ -518,7 +542,20 @@ predicate switchMatching(Switch s, Case c, PatternExpr pe) {
518542
pe = c.getPattern()
519543
}
520544

521-
private predicate mustHaveMatchingCompletion(Switch s, PatternExpr pe) { switchMatching(s, _, pe) }
545+
/**
546+
* Holds if `pe` must have a matching completion, and `e` is the expression
547+
* that is being matched.
548+
*/
549+
private predicate mustHaveMatchingCompletion(Expr e, PatternExpr pe) {
550+
exists(Switch s |
551+
switchMatching(s, _, pe) and
552+
e = s.getExpr()
553+
)
554+
or
555+
pe = any(IsExpr ie | inBooleanContext(ie) and e = ie.getExpr()).getPattern()
556+
or
557+
pe = any(UnaryPatternExpr upe | mustHaveMatchingCompletion(e, upe)).getPattern()
558+
}
522559

523560
/**
524561
* Holds if a normal completion of `cfe` must be a matching completion. Thats is,
@@ -565,7 +602,13 @@ class SimpleCompletion extends NonNestedNormalCompletion, TSimpleCompletion {
565602
* completion (`NullnessCompletion`), a matching completion (`MatchingCompletion`),
566603
* or an emptiness completion (`EmptinessCompletion`).
567604
*/
568-
abstract class ConditionalCompletion extends NonNestedNormalCompletion { }
605+
abstract class ConditionalCompletion extends NonNestedNormalCompletion {
606+
/** Gets the Boolean value of this completion. */
607+
abstract boolean getValue();
608+
609+
/** Gets the dual completion. */
610+
abstract ConditionalCompletion getDual();
611+
}
569612

570613
/**
571614
* A completion that represents evaluation of an expression
@@ -576,10 +619,9 @@ class BooleanCompletion extends ConditionalCompletion {
576619

577620
BooleanCompletion() { this = TBooleanCompletion(value) }
578621

579-
/** Gets the Boolean value of this completion. */
580-
boolean getValue() { result = value }
622+
override boolean getValue() { result = value }
581623

582-
BooleanCompletion getDual() { result = TBooleanCompletion(value.booleanNot()) }
624+
override BooleanCompletion getDual() { result = TBooleanCompletion(value.booleanNot()) }
583625

584626
override BooleanSuccessor getAMatchingSuccessorType() { result.getValue() = value }
585627

@@ -611,6 +653,10 @@ class NullnessCompletion extends ConditionalCompletion, TNullnessCompletion {
611653
/** Holds if the last sub expression of this expression evaluates to a non-`null` value. */
612654
predicate isNonNull() { value = false }
613655

656+
override boolean getValue() { result = value }
657+
658+
override NullnessCompletion getDual() { result = TNullnessCompletion(value.booleanNot()) }
659+
614660
override NullnessSuccessor getAMatchingSuccessorType() { result.getValue() = value }
615661

616662
override string toString() { if this.isNull() then result = "null" else result = "non-null" }
@@ -631,6 +677,10 @@ class MatchingCompletion extends ConditionalCompletion, TMatchingCompletion {
631677
/** Holds if there is not a match. */
632678
predicate isNonMatch() { value = false }
633679

680+
override boolean getValue() { result = value }
681+
682+
override MatchingCompletion getDual() { result = TMatchingCompletion(value.booleanNot()) }
683+
634684
override MatchingSuccessor getAMatchingSuccessorType() { result.getValue() = value }
635685

636686
override string toString() { if this.isMatch() then result = "match" else result = "no-match" }
@@ -648,6 +698,10 @@ class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
648698
/** Holds if the emptiness test evaluates to `true`. */
649699
predicate isEmpty() { value = true }
650700

701+
override boolean getValue() { result = value }
702+
703+
override EmptinessCompletion getDual() { result = TEmptinessCompletion(value.booleanNot()) }
704+
651705
override EmptinessSuccessor getAMatchingSuccessorType() { result.getValue() = value }
652706

653707
override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" }

csharp/ql/src/semmle/code/csharp/controlflow/internal/ControlFlowGraphImpl.qll

Lines changed: 21 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -368,7 +368,8 @@ module Expressions {
368368
not this instanceof NoNodeExpr and
369369
not this instanceof SwitchExpr and
370370
not this instanceof SwitchCaseExpr and
371-
not this instanceof ConstructorInitializer
371+
not this instanceof ConstructorInitializer and
372+
not this instanceof NotPatternExpr
372373
}
373374

374375
final override ControlFlowElement getChildElement(int i) { result = getExprChild(this, i) }
@@ -515,20 +516,14 @@ module Expressions {
515516

516517
LogicalNotExprTree() { operand = this.getOperand() }
517518

518-
final override predicate propagatesAbnormal(ControlFlowElement child) {
519-
child = this.getOperand()
520-
}
519+
final override predicate propagatesAbnormal(ControlFlowElement child) { child = operand }
521520

522521
final override predicate first(ControlFlowElement first) { first(operand, first) }
523522

524523
final override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
525524
succ = this and
526-
(
527-
last(operand, pred, c.(BooleanCompletion).getDual())
528-
or
529-
last(operand, pred, c) and
530-
c instanceof SimpleCompletion
531-
)
525+
last(operand, pred, c) and
526+
c instanceof NormalCompletion
532527
}
533528
}
534529

@@ -925,6 +920,22 @@ module Expressions {
925920
)
926921
}
927922
}
923+
924+
private class NotPatternExprTree extends PostOrderTree, NotPatternExpr {
925+
private PatternExpr operand;
926+
927+
NotPatternExprTree() { operand = this.getPattern() }
928+
929+
final override predicate propagatesAbnormal(ControlFlowElement child) { child = operand }
930+
931+
final override predicate first(ControlFlowElement first) { first(operand, first) }
932+
933+
final override predicate succ(ControlFlowElement pred, ControlFlowElement succ, Completion c) {
934+
succ = this and
935+
last(operand, pred, c) and
936+
c instanceof NormalCompletion
937+
}
938+
}
928939
}
929940

930941
module Statements {

csharp/ql/src/semmle/code/csharp/controlflow/internal/Splitting.qll

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -465,6 +465,12 @@ module ConditionalCompletionSplitting {
465465
or
466466
last(succ.(SwitchCaseExpr).getBody(), pred, c) and
467467
completion = c
468+
or
469+
last(succ.(NotPatternExpr).getPattern(), pred, c) and
470+
completion.(MatchingCompletion).getDual() = c
471+
or
472+
last(succ.(IsExpr).getPattern(), pred, c) and
473+
completion.(BooleanCompletion).getValue() = c.(MatchingCompletion).getValue()
468474
)
469475
}
470476

csharp/ql/test/library-tests/controlflow/graph/BasicBlock.expected

Lines changed: 28 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -924,11 +924,17 @@
924924
| NullCoalescing.cs:15:31:15:31 | 0 | NullCoalescing.cs:16:17:16:18 | "" | 5 |
925925
| NullCoalescing.cs:16:17:16:25 | ... ?? ... | NullCoalescing.cs:17:13:17:19 | (...) ... | 5 |
926926
| NullCoalescing.cs:17:13:17:24 | ... ?? ... | NullCoalescing.cs:13:10:13:11 | exit M6 | 4 |
927-
| Patterns.cs:5:10:5:11 | enter M1 | Patterns.cs:8:13:8:23 | ... is ... | 9 |
927+
| Patterns.cs:5:10:5:11 | enter M1 | Patterns.cs:8:18:8:23 | Int32 i1 | 8 |
928+
| Patterns.cs:8:13:8:23 | [false] ... is ... | Patterns.cs:8:13:8:23 | [false] ... is ... | 1 |
929+
| Patterns.cs:8:13:8:23 | [true] ... is ... | Patterns.cs:8:13:8:23 | [true] ... is ... | 1 |
928930
| Patterns.cs:9:9:11:9 | {...} | Patterns.cs:10:13:10:42 | call to method WriteLine | 6 |
929-
| Patterns.cs:12:14:18:9 | if (...) ... | Patterns.cs:12:18:12:31 | ... is ... | 4 |
931+
| Patterns.cs:12:14:18:9 | if (...) ... | Patterns.cs:12:23:12:31 | String s1 | 3 |
932+
| Patterns.cs:12:18:12:31 | [false] ... is ... | Patterns.cs:12:18:12:31 | [false] ... is ... | 1 |
933+
| Patterns.cs:12:18:12:31 | [true] ... is ... | Patterns.cs:12:18:12:31 | [true] ... is ... | 1 |
930934
| Patterns.cs:13:9:15:9 | {...} | Patterns.cs:14:13:14:45 | call to method WriteLine | 6 |
931-
| Patterns.cs:16:14:18:9 | if (...) ... | Patterns.cs:16:18:16:28 | ... is ... | 4 |
935+
| Patterns.cs:16:14:18:9 | if (...) ... | Patterns.cs:16:23:16:28 | Object v1 | 3 |
936+
| Patterns.cs:16:18:16:28 | [false] ... is ... | Patterns.cs:16:18:16:28 | [false] ... is ... | 1 |
937+
| Patterns.cs:16:18:16:28 | [true] ... is ... | Patterns.cs:16:18:16:28 | [true] ... is ... | 1 |
932938
| Patterns.cs:17:9:18:9 | {...} | Patterns.cs:17:9:18:9 | {...} | 1 |
933939
| Patterns.cs:20:9:38:9 | switch (...) {...} | Patterns.cs:22:18:22:22 | "xyz" | 4 |
934940
| Patterns.cs:23:17:23:22 | break; | Patterns.cs:23:17:23:22 | break; | 1 |
@@ -944,26 +950,37 @@
944950
| Patterns.cs:35:13:35:20 | default: | Patterns.cs:37:17:37:22 | break; | 5 |
945951
| Patterns.cs:40:9:42:9 | switch (...) {...} | Patterns.cs:5:10:5:11 | exit M1 | 4 |
946952
| Patterns.cs:47:24:47:25 | enter M2 | Patterns.cs:47:24:47:25 | exit M2 | 7 |
947-
| Patterns.cs:50:24:50:25 | enter M3 | Patterns.cs:51:9:51:21 | ... is ... | 5 |
953+
| Patterns.cs:50:24:50:25 | enter M3 | Patterns.cs:51:18:51:21 | null | 3 |
954+
| Patterns.cs:51:9:51:21 | [false] ... is ... | Patterns.cs:51:9:51:21 | [false] ... is ... | 1 |
955+
| Patterns.cs:51:9:51:21 | [true] ... is ... | Patterns.cs:51:9:51:21 | [true] ... is ... | 1 |
948956
| Patterns.cs:51:9:51:39 | ... ? ... : ... | Patterns.cs:50:24:50:25 | exit M3 | 3 |
957+
| Patterns.cs:51:14:51:21 | [match] not ... | Patterns.cs:51:14:51:21 | [match] not ... | 1 |
958+
| Patterns.cs:51:14:51:21 | [no-match] not ... | Patterns.cs:51:14:51:21 | [no-match] not ... | 1 |
949959
| Patterns.cs:51:25:51:25 | access to parameter c | Patterns.cs:51:25:51:30 | ... is ... | 3 |
950960
| Patterns.cs:51:34:51:34 | access to parameter c | Patterns.cs:51:34:51:39 | ... is ... | 3 |
951961
| Patterns.cs:53:24:53:25 | enter M4 | Patterns.cs:53:24:53:25 | exit M4 | 10 |
952-
| Patterns.cs:56:26:56:27 | enter M5 | Patterns.cs:60:13:60:17 | not ... | 5 |
962+
| Patterns.cs:56:26:56:27 | enter M5 | Patterns.cs:60:17:60:17 | 1 | 4 |
953963
| Patterns.cs:58:16:62:9 | ... switch { ... } | Patterns.cs:56:26:56:27 | exit M5 | 4 |
964+
| Patterns.cs:60:13:60:17 | [match] not ... | Patterns.cs:60:13:60:17 | [match] not ... | 1 |
965+
| Patterns.cs:60:13:60:17 | [no-match] not ... | Patterns.cs:60:13:60:17 | [no-match] not ... | 1 |
954966
| Patterns.cs:60:22:60:28 | "not 1" | Patterns.cs:60:13:60:28 | ... => ... | 2 |
955967
| Patterns.cs:61:13:61:13 | _ | Patterns.cs:61:13:61:13 | _ | 1 |
956968
| Patterns.cs:61:18:61:24 | "other" | Patterns.cs:61:13:61:24 | ... => ... | 2 |
957-
| Patterns.cs:65:26:65:27 | enter M6 | Patterns.cs:69:13:69:17 | not ... | 5 |
969+
| Patterns.cs:65:26:65:27 | enter M6 | Patterns.cs:69:17:69:17 | 2 | 4 |
970+
| Patterns.cs:69:13:69:17 | [no-match] not ... | Patterns.cs:69:13:69:17 | [no-match] not ... | 1 |
958971
| Patterns.cs:70:13:70:13 | 2 | Patterns.cs:70:13:70:13 | 2 | 1 |
959972
| Patterns.cs:70:18:70:27 | "possible" | Patterns.cs:65:26:65:27 | exit M6 | 6 |
960973
| PostDominance.cs:5:10:5:11 | enter M1 | PostDominance.cs:5:10:5:11 | exit M1 | 7 |
961-
| PostDominance.cs:10:10:10:11 | enter M2 | PostDominance.cs:12:13:12:21 | ... is ... | 6 |
974+
| PostDominance.cs:10:10:10:11 | enter M2 | PostDominance.cs:12:18:12:21 | null | 5 |
962975
| PostDominance.cs:10:10:10:11 | exit M2 (normal) | PostDominance.cs:10:10:10:11 | exit M2 | 2 |
976+
| PostDominance.cs:12:13:12:21 | [false] ... is ... | PostDominance.cs:12:13:12:21 | [false] ... is ... | 1 |
977+
| PostDominance.cs:12:13:12:21 | [true] ... is ... | PostDominance.cs:12:13:12:21 | [true] ... is ... | 1 |
963978
| PostDominance.cs:13:13:13:19 | return ...; | PostDominance.cs:13:13:13:19 | return ...; | 1 |
964979
| PostDominance.cs:14:9:14:29 | ...; | PostDominance.cs:14:9:14:28 | call to method WriteLine | 3 |
965-
| PostDominance.cs:17:10:17:11 | enter M3 | PostDominance.cs:19:13:19:21 | ... is ... | 6 |
980+
| PostDominance.cs:17:10:17:11 | enter M3 | PostDominance.cs:19:18:19:21 | null | 5 |
966981
| PostDominance.cs:17:10:17:11 | exit M3 | PostDominance.cs:17:10:17:11 | exit M3 | 1 |
982+
| PostDominance.cs:19:13:19:21 | [false] ... is ... | PostDominance.cs:19:13:19:21 | [false] ... is ... | 1 |
983+
| PostDominance.cs:19:13:19:21 | [true] ... is ... | PostDominance.cs:19:13:19:21 | [true] ... is ... | 1 |
967984
| PostDominance.cs:20:45:20:53 | nameof(...) | PostDominance.cs:17:10:17:11 | exit M3 (abnormal) | 4 |
968985
| PostDominance.cs:21:9:21:29 | ...; | PostDominance.cs:17:10:17:11 | exit M3 (normal) | 4 |
969986
| Qualifiers.cs:7:16:7:21 | enter Method | Qualifiers.cs:7:16:7:21 | exit Method | 4 |
@@ -1079,7 +1096,9 @@
10791096
| Switch.cs:156:50:156:52 | "b" | Switch.cs:156:41:156:52 | ... => ... | 2 |
10801097
| Switch.cs:158:13:158:49 | ...; | Switch.cs:158:13:158:48 | call to method WriteLine | 5 |
10811098
| Switch.cs:160:13:160:49 | ...; | Switch.cs:160:13:160:48 | call to method WriteLine | 5 |
1082-
| TypeAccesses.cs:3:10:3:10 | enter M | TypeAccesses.cs:7:13:7:22 | ... is ... | 14 |
1099+
| TypeAccesses.cs:3:10:3:10 | enter M | TypeAccesses.cs:7:18:7:22 | Int32 j | 13 |
1100+
| TypeAccesses.cs:7:13:7:22 | [false] ... is ... | TypeAccesses.cs:7:13:7:22 | [false] ... is ... | 1 |
1101+
| TypeAccesses.cs:7:13:7:22 | [true] ... is ... | TypeAccesses.cs:7:13:7:22 | [true] ... is ... | 1 |
10831102
| TypeAccesses.cs:7:25:7:25 | ; | TypeAccesses.cs:7:25:7:25 | ; | 1 |
10841103
| TypeAccesses.cs:8:9:8:28 | ... ...; | TypeAccesses.cs:3:10:3:10 | exit M | 5 |
10851104
| VarDecls.cs:5:18:5:19 | enter M1 | VarDecls.cs:5:18:5:19 | exit M1 | 19 |

0 commit comments

Comments
 (0)