|
1 | 1 | import csharp |
2 | 2 | import semmle.code.csharp.controlflow.internal.Completion |
3 | | -import semmle.code.csharp.controlflow.internal.PreBasicBlocks |
4 | 3 | import ControlFlow |
5 | 4 | import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl::Consistency |
6 | 5 | import semmle.code.csharp.controlflow.internal.Splitting |
7 | | - |
8 | | -private predicate splitBB(ControlFlow::BasicBlock bb) { |
9 | | - exists(ControlFlow::Node first | |
10 | | - first = bb.getFirstNode() and |
11 | | - first.isJoin() and |
12 | | - strictcount(first.getAPredecessor().getAstNode()) = 1 |
13 | | - ) |
14 | | -} |
15 | | - |
16 | | -private class RelevantBasicBlock extends ControlFlow::BasicBlock { |
17 | | - RelevantBasicBlock() { not splitBB(this) } |
18 | | -} |
19 | | - |
20 | | -predicate bbStartInconsistency(ControlFlowElement cfe) { |
21 | | - exists(RelevantBasicBlock bb | bb.getFirstNode() = cfe.getAControlFlowNode()) and |
22 | | - not cfe = any(PreBasicBlock bb).getFirstElement() |
23 | | -} |
24 | | - |
25 | | -predicate bbSuccInconsistency(ControlFlowElement pred, ControlFlowElement succ) { |
26 | | - exists(RelevantBasicBlock predBB, RelevantBasicBlock succBB | |
27 | | - predBB.getLastNode() = pred.getAControlFlowNode() and |
28 | | - succBB = predBB.getASuccessor() and |
29 | | - succBB.getFirstNode() = succ.getAControlFlowNode() |
30 | | - ) and |
31 | | - not exists(PreBasicBlock predBB, PreBasicBlock succBB | |
32 | | - predBB.getLastNode() = pred and |
33 | | - succBB = predBB.getASuccessor() and |
34 | | - succBB.getFirstElement() = succ |
35 | | - ) |
36 | | -} |
37 | | - |
38 | | -predicate bbIntraSuccInconsistency(ControlFlowElement pred, ControlFlowElement succ) { |
39 | | - exists(ControlFlow::BasicBlock bb, int i | |
40 | | - pred.getAControlFlowNode() = bb.getNode(i) and |
41 | | - succ.getAControlFlowNode() = bb.getNode(i + 1) |
42 | | - ) and |
43 | | - not exists(PreBasicBlock bb | |
44 | | - bb.getLastNode() = pred and |
45 | | - bb.getASuccessor().getFirstElement() = succ |
46 | | - ) and |
47 | | - not exists(PreBasicBlock bb, int i | |
48 | | - bb.getNode(i) = pred and |
49 | | - bb.getNode(i + 1) = succ |
50 | | - ) |
51 | | -} |
52 | | - |
53 | | -query predicate preBasicBlockConsistency(ControlFlowElement cfe1, ControlFlowElement cfe2, string s) { |
54 | | - bbStartInconsistency(cfe1) and |
55 | | - cfe2 = cfe1 and |
56 | | - s = "start inconsistency" |
57 | | - or |
58 | | - bbSuccInconsistency(cfe1, cfe2) and |
59 | | - s = "succ inconsistency" |
60 | | - or |
61 | | - bbIntraSuccInconsistency(cfe1, cfe2) and |
62 | | - s = "intra succ inconsistency" |
63 | | -} |
0 commit comments