Skip to content

Commit d1f7eef

Browse files
calumgrantcalumgrant
authored
Merge pull request #537 from hvitved/csharp/guards-splitting
C#: Make guards library work with CFG splitting
2 parents e069041 + 03e69e9 commit d1f7eef

File tree

12 files changed

+474
-49
lines changed

12 files changed

+474
-49
lines changed

‎csharp/ql/src/semmle/code/csharp/commons/Assertions.qll‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22
private import semmle.code.csharp.frameworks.system.Diagnostics
33
private import semmle.code.csharp.frameworks.test.VisualStudio
44
private import semmle.code.csharp.frameworks.System
5+
private import ControlFlow
6+
private import ControlFlow::BasicBlocks
57

68
/** An assertion method. */
79
abstract class AssertMethod extends Method {
@@ -46,6 +48,49 @@ class Assertion extends MethodCall {
4648
Expr getExpr() {
4749
result = this.getArgumentForParameter(target.getAssertedParameter())
4850
}
51+
52+
pragma[nomagic]
53+
private JoinBlockPredecessor getAPossiblyDominatedPredecessor(JoinBlock jb) {
54+
exists(BasicBlock bb |
55+
bb = this.getAControlFlowNode().getBasicBlock() |
56+
result = bb.getASuccessor*()
57+
) and
58+
result.getASuccessor() = jb
59+
}
60+
61+
pragma[nomagic]
62+
private predicate isPossiblyDominatedJoinBlock(JoinBlock jb) {
63+
exists(this.getAPossiblyDominatedPredecessor(jb)) and
64+
forall(BasicBlock pred |
65+
pred = jb.getAPredecessor() |
66+
pred = this.getAPossiblyDominatedPredecessor(jb)
67+
)
68+
}
69+
70+
/**
71+
* Holds if this assertion strictly dominates basic block `bb`. That is, `bb`
72+
* can only be reached from the callable entry point by going via *some* basic
73+
* block containing this element.
74+
*
75+
* This predicate is different from
76+
* `this.getAControlFlowNode().getBasicBlock().strictlyDominates(bb)`
77+
* in that it takes control flow splitting into account.
78+
*/
79+
pragma[nomagic]
80+
predicate strictlyDominates(BasicBlock bb) {
81+
this.getAControlFlowNode().getBasicBlock().immediatelyDominates(bb)
82+
or
83+
if bb instanceof JoinBlock then
84+
this.isPossiblyDominatedJoinBlock(bb) and
85+
forall(BasicBlock pred |
86+
pred = this.getAPossiblyDominatedPredecessor(bb) |
87+
this.strictlyDominates(pred)
88+
or
89+
this.getAControlFlowNode().getBasicBlock() = pred
90+
)
91+
else
92+
this.strictlyDominates(bb.getAPredecessor())
93+
}
4994
}
5095

5196
/** A trivially failing assertion, for example `Debug.Assert(false)`. */

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

Lines changed: 56 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ class BasicBlock extends TBasicBlockStart {
1515
result.getFirstNode() = getLastNode().getASuccessor()
1616
}
1717

18-
/** Gets an immediate successor of this basic block of a given flow type, if any. */
18+
/** Gets an immediate successor of this basic block of a given type, if any. */
1919
BasicBlock getASuccessorByType(ControlFlow::SuccessorType t) {
2020
result.getFirstNode() = this.getLastNode().getASuccessorByType(t)
2121
}
@@ -25,6 +25,11 @@ class BasicBlock extends TBasicBlockStart {
2525
result.getASuccessor() = this
2626
}
2727

28+
/** Gets an immediate predecessor of this basic block of a given type, if any. */
29+
BasicBlock getAPredecessorByType(ControlFlow::SuccessorType t) {
30+
result.getASuccessorByType(t) = this
31+
}
32+
2833
/**
2934
* Gets an immediate `true` successor, if any.
3035
*
@@ -134,6 +139,31 @@ class BasicBlock extends TBasicBlockStart {
134139
result = strictcount(getANode())
135140
}
136141

142+
/**
143+
* Holds if this basic block immediately dominates basic block `bb`.
144+
*
145+
* That is, all paths reaching basic block `bb` from some entry point
146+
* basic block must go through this basic block (which is an immediate
147+
* predecessor of `bb`).
148+
*
149+
* Example:
150+
*
151+
* ```
152+
* int M(string s) {
153+
* if (s == null)
154+
* throw new ArgumentNullException(nameof(s));
155+
* return s.Length;
156+
* }
157+
* ```
158+
*
159+
* The basic block starting on line 2 strictly dominates the
160+
* basic block on line 4 (all paths from the entry point of `M`
161+
* to `return s.Length;` must go through the null check).
162+
*/
163+
predicate immediatelyDominates(BasicBlock bb) {
164+
bbIDominates(this, bb)
165+
}
166+
137167
/**
138168
* Holds if this basic block strictly dominates basic block `bb`.
139169
*
@@ -419,24 +449,42 @@ private predicate exitBB(BasicBlock bb) {
419449
bb.getLastNode() instanceof ControlFlow::Nodes::ExitNode
420450
}
421451

422-
/**
423-
* A basic block with more than one predecessor.
424-
*/
452+
/** A basic block with more than one predecessor. */
425453
class JoinBlock extends BasicBlock {
426454
JoinBlock() { getFirstNode().isJoin() }
427455
}
428456

457+
/** A basic block that is an immediate predecessor of a join block. */
458+
class JoinBlockPredecessor extends BasicBlock {
459+
JoinBlockPredecessor() {
460+
this.getASuccessor() instanceof JoinBlock
461+
}
462+
}
463+
429464
/** A basic block that terminates in a condition, splitting the subsequent control flow. */
430465
class ConditionBlock extends BasicBlock {
431466
ConditionBlock() {
432467
this.getLastNode().isCondition()
433468
}
434469

470+
/**
471+
* Holds if basic block `succ` is immediately controlled by this basic
472+
* block with conditional value `s`. That is, `succ` is an immediate
473+
* successor of this block, and `succ` can only be reached from
474+
* the callable entry point by going via the `s` edge out of this basic block.
475+
*/
476+
predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
477+
succ = this.getASuccessorByType(s) and
478+
forall(BasicBlock pred |
479+
pred = succ.getAPredecessor() and pred != this |
480+
succ.dominates(pred)
481+
)
482+
}
483+
435484
/**
436485
* Holds if basic block `controlled` is controlled by this basic block with
437-
* Boolean value `testIsTrue`. That is, `controlled` can only be reached from
438-
* the callable entry point by going via the true edge (`testIsTrue = true`)
439-
* or false edge (`testIsTrue = false`) out of this basic block.
486+
* conditional value `s`. That is, `controlled` can only be reached from
487+
* the callable entry point by going via the `s` edge out of this basic block.
440488
*/
441489
predicate controls(BasicBlock controlled, ConditionalSuccessor s) {
442490
/*
@@ -473,7 +521,7 @@ class ConditionBlock extends BasicBlock {
473521
* directly.
474522
*/
475523
exists(BasicBlock succ |
476-
isCandidateSuccessor(succ, s) |
524+
this.immediatelyControls(succ, s) |
477525
succ.dominates(controlled)
478526
)
479527
}
@@ -529,14 +577,6 @@ class ConditionBlock extends BasicBlock {
529577
impliesSub(getLastNode().getElement(), cond, testIsTrue, condIsTrue) and
530578
controls(controlled, any(BooleanSuccessor s | s.getValue() = testIsTrue))
531579
}
532-
533-
private predicate isCandidateSuccessor(BasicBlock succ, ConditionalSuccessor s) {
534-
succ = this.getASuccessorByType(s) and
535-
forall(BasicBlock pred |
536-
pred = succ.getAPredecessor() and pred != this |
537-
succ.dominates(pred)
538-
)
539-
}
540580
}
541581

542582
/**

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

Lines changed: 95 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
/** Provides the class `ControlFlowElement`. */
22

3-
import csharp
3+
import csharp
44
private import semmle.code.csharp.ExprOrStmtParent
5+
private import ControlFlow
6+
private import ControlFlow::BasicBlocks
7+
private import SuccessorTypes
58

69
/**
710
* A program element that can possess control flow. That is, either a statement or
@@ -25,21 +28,21 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
2528
* several `ControlFlow::Node`s, for example to represent the continuation
2629
* flow in a `try/catch/finally` construction.
2730
*/
28-
ControlFlow::Node getAControlFlowNode() {
31+
Node getAControlFlowNode() {
2932
result.getElement() = this
3033
}
3134

3235
/**
3336
* Gets a first control flow node executed within this element.
3437
*/
35-
ControlFlow::Node getAControlFlowEntryNode() {
38+
Node getAControlFlowEntryNode() {
3639
result = ControlFlowGraph::Internal::getAControlFlowEntryNode(this).getAControlFlowNode()
3740
}
3841

3942
/**
4043
* Gets a potential last control flow node executed within this element.
4144
*/
42-
ControlFlow::Node getAControlFlowExitNode() {
45+
Node getAControlFlowExitNode() {
4346
result = ControlFlowGraph::Internal::getAControlFlowExitNode(this).getAControlFlowNode()
4447
}
4548

@@ -59,7 +62,7 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
5962
/** Gets an element that is reachable from this element. */
6063
ControlFlowElement getAReachableElement() {
6164
// Reachable in same basic block
62-
exists(ControlFlow::BasicBlock bb, int i, int j |
65+
exists(BasicBlock bb, int i, int j |
6366
bb.getNode(i) = getAControlFlowNode() and
6467
bb.getNode(j) = result.getAControlFlowNode() and
6568
i < j
@@ -68,4 +71,91 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
6871
// Reachable in different basic blocks
6972
getAControlFlowNode().getBasicBlock().getASuccessor+().getANode() = result.getAControlFlowNode()
7073
}
74+
75+
/**
76+
* Holds if basic block `succ` is immediately controlled by this control flow
77+
* element with conditional value `s`. That is, `succ` can only be reached from
78+
* the callable entry point by going via the `s` edge out of *some* basic block
79+
* `pred` ending with this element, and `pred` is an immediate predecessor
80+
* of `succ`.
81+
*
82+
* This predicate is different from
83+
* `this.getAControlFlowNode().getBasicBlock().(ConditionBlock).immediatelyControls(succ, s)`
84+
* in that it takes control flow splitting into account.
85+
*/
86+
pragma[nomagic]
87+
private predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
88+
exists(ConditionBlock cb |
89+
cb.getLastNode() = this.getAControlFlowNode() |
90+
succ = cb.getASuccessorByType(s) and
91+
forall(BasicBlock pred, SuccessorType t |
92+
pred = succ.getAPredecessorByType(t) and pred != cb |
93+
succ.dominates(pred)
94+
or
95+
// `pred` might be another split of `cfe`
96+
pred.getLastNode().getElement() = this and
97+
pred.getASuccessorByType(t) = succ and
98+
t = s
99+
)
100+
)
101+
}
102+
103+
pragma[nomagic]
104+
private JoinBlockPredecessor getAPossiblyControlledPredecessor(JoinBlock controlled, ConditionalSuccessor s) {
105+
exists(BasicBlock mid |
106+
this.immediatelyControls(mid, s) |
107+
result = mid.getASuccessor*()
108+
) and
109+
result.getASuccessor() = controlled
110+
}
111+
112+
pragma[nomagic]
113+
private predicate isPossiblyControlledJoinBlock(JoinBlock controlled, ConditionalSuccessor s) {
114+
exists(this.getAPossiblyControlledPredecessor(controlled, s)) and
115+
forall(BasicBlock pred |
116+
pred = controlled.getAPredecessor() |
117+
pred = this.getAPossiblyControlledPredecessor(controlled, s)
118+
)
119+
}
120+
121+
/**
122+
* Holds if basic block `controlled` is controlled by this control flow element
123+
* with conditional value `s`. That is, `controlled` can only be reached from
124+
* the callable entry point by going via the `s` edge out of *some* basic block
125+
* ending with this element.
126+
*
127+
* This predicate is different from
128+
* `this.getAControlFlowNode().getBasicBlock().(ConditionBlock).controls(controlled, s)`
129+
* in that it takes control flow splitting into account.
130+
*/
131+
cached
132+
predicate controlsBlock(BasicBlock controlled, ConditionalSuccessor s) {
133+
this.immediatelyControls(controlled, s)
134+
or
135+
if controlled instanceof JoinBlock then
136+
this.isPossiblyControlledJoinBlock(controlled, s) and
137+
forall(BasicBlock pred |
138+
pred = this.getAPossiblyControlledPredecessor(controlled, s) |
139+
this.controlsBlock(pred, s)
140+
)
141+
else
142+
this.controlsBlock(controlled.getAPredecessor(), s)
143+
}
144+
145+
/**
146+
* Holds if control flow element `controlled` is controlled by this control flow
147+
* element with conditional value `s`. That is, `controlled` can only be reached
148+
* from the callable entry point by going via the `s` edge out of this element.
149+
*
150+
* This predicate is different from
151+
* `this.getAControlFlowNode().getBasicBlock().(ConditionBlock).controls(controlled.getAControlFlowNode().getBasicBlock(), s)`
152+
* in that it takes control flow splitting into account.
153+
*/
154+
pragma[inline] // potentially very large predicate, so must be inlined
155+
predicate controlsElement(ControlFlowElement controlled, ConditionalSuccessor s) {
156+
forex(BasicBlock bb |
157+
bb = controlled.getAControlFlowNode().getBasicBlock() |
158+
this.controlsBlock(bb, s)
159+
)
160+
}
71161
}

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,7 @@ module ControlFlow {
183183
)
184184
}
185185

186-
/** Gets a successor node of a given flow type, if any. */
186+
/** Gets a successor node of a given type, if any. */
187187
Node getASuccessorByType(SuccessorType t) {
188188
result = getASuccessorByType(this, t)
189189
}
@@ -372,6 +372,7 @@ module ControlFlow {
372372
class EntryBlock = BBs::EntryBasicBlock;
373373
class ExitBlock = BBs::ExitBasicBlock;
374374
class JoinBlock = BBs::JoinBlock;
375+
class JoinBlockPredecessor = BBs::JoinBlockPredecessor;
375376
class ConditionBlock = BBs::ConditionBlock;
376377
}
377378

@@ -2549,7 +2550,7 @@ module ControlFlow {
25492550
) > 1
25502551
}
25512552

2552-
private predicate isCandidateSuccessor(PreBasicBlock succ, ConditionalCompletion c) {
2553+
private predicate immediatelyControls(PreBasicBlock succ, ConditionalCompletion c) {
25532554
succ = succ(this.getLastElement(), c) and
25542555
forall(PreBasicBlock pred |
25552556
pred = succ.getAPredecessor() and pred != this |
@@ -2559,7 +2560,7 @@ module ControlFlow {
25592560

25602561
predicate controls(PreBasicBlock controlled, ConditionalSuccessor s) {
25612562
exists(PreBasicBlock succ, ConditionalCompletion c |
2562-
isCandidateSuccessor(succ, c) |
2563+
immediatelyControls(succ, c) |
25632564
succ.dominates(controlled) and
25642565
s.matchesCompletion(c)
25652566
)

0 commit comments

Comments
 (0)