Skip to content

Commit e0b121c

Browse files
aschackmullaschackmull
authored
Merge pull request #7047 from hvitved/csharp/ssa/dominance-frontier
Shared SSA: Improved dominance frontier calculation
2 parents b639e82 + df69621 commit e0b121c

File tree

5 files changed

+80
-90
lines changed

5 files changed

+80
-90
lines changed

‎csharp/ql/lib/semmle/code/cil/internal/SsaImplCommon.qll

Lines changed: 16 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -141,25 +141,23 @@ private module Liveness {
141141

142142
private import Liveness
143143

144-
/** Holds if `bb1` strictly dominates `bb2`. */
145-
private predicate strictlyDominates(BasicBlock bb1, BasicBlock bb2) {
146-
bb1 = getImmediateBasicBlockDominator+(bb2)
147-
}
148-
149-
/** Holds if `bb1` dominates a predecessor of `bb2`. */
150-
private predicate dominatesPredecessor(BasicBlock bb1, BasicBlock bb2) {
151-
exists(BasicBlock pred | pred = getABasicBlockPredecessor(bb2) |
152-
bb1 = pred
153-
or
154-
strictlyDominates(bb1, pred)
155-
)
156-
}
157-
158-
/** Holds if `df` is in the dominance frontier of `bb`. */
159-
pragma[noinline]
144+
/**
145+
* Holds if `df` is in the dominance frontier of `bb`.
146+
*
147+
* This is equivalent to:
148+
*
149+
* ```ql
150+
* bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and
151+
* not bb = getImmediateBasicBlockDominator+(df)
152+
* ```
153+
*/
160154
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
161-
dominatesPredecessor(bb, df) and
162-
not strictlyDominates(bb, df)
155+
bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df)
156+
or
157+
exists(BasicBlock prev | inDominanceFrontier(prev, df) |
158+
bb = getImmediateBasicBlockDominator(prev) and
159+
not bb = getImmediateBasicBlockDominator(df)
160+
)
163161
}
164162

165163
/**

‎csharp/ql/lib/semmle/code/csharp/controlflow/internal/pressa/SsaImplCommon.qll

Lines changed: 16 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -141,25 +141,23 @@ private module Liveness {
141141

142142
private import Liveness
143143

144-
/** Holds if `bb1` strictly dominates `bb2`. */
145-
private predicate strictlyDominates(BasicBlock bb1, BasicBlock bb2) {
146-
bb1 = getImmediateBasicBlockDominator+(bb2)
147-
}
148-
149-
/** Holds if `bb1` dominates a predecessor of `bb2`. */
150-
private predicate dominatesPredecessor(BasicBlock bb1, BasicBlock bb2) {
151-
exists(BasicBlock pred | pred = getABasicBlockPredecessor(bb2) |
152-
bb1 = pred
153-
or
154-
strictlyDominates(bb1, pred)
155-
)
156-
}
157-
158-
/** Holds if `df` is in the dominance frontier of `bb`. */
159-
pragma[noinline]
144+
/**
145+
* Holds if `df` is in the dominance frontier of `bb`.
146+
*
147+
* This is equivalent to:
148+
*
149+
* ```ql
150+
* bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and
151+
* not bb = getImmediateBasicBlockDominator+(df)
152+
* ```
153+
*/
160154
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
161-
dominatesPredecessor(bb, df) and
162-
not strictlyDominates(bb, df)
155+
bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df)
156+
or
157+
exists(BasicBlock prev | inDominanceFrontier(prev, df) |
158+
bb = getImmediateBasicBlockDominator(prev) and
159+
not bb = getImmediateBasicBlockDominator(df)
160+
)
163161
}
164162

165163
/**

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll

Lines changed: 16 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -141,25 +141,23 @@ private module Liveness {
141141

142142
private import Liveness
143143

144-
/** Holds if `bb1` strictly dominates `bb2`. */
145-
private predicate strictlyDominates(BasicBlock bb1, BasicBlock bb2) {
146-
bb1 = getImmediateBasicBlockDominator+(bb2)
147-
}
148-
149-
/** Holds if `bb1` dominates a predecessor of `bb2`. */
150-
private predicate dominatesPredecessor(BasicBlock bb1, BasicBlock bb2) {
151-
exists(BasicBlock pred | pred = getABasicBlockPredecessor(bb2) |
152-
bb1 = pred
153-
or
154-
strictlyDominates(bb1, pred)
155-
)
156-
}
157-
158-
/** Holds if `df` is in the dominance frontier of `bb`. */
159-
pragma[noinline]
144+
/**
145+
* Holds if `df` is in the dominance frontier of `bb`.
146+
*
147+
* This is equivalent to:
148+
*
149+
* ```ql
150+
* bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and
151+
* not bb = getImmediateBasicBlockDominator+(df)
152+
* ```
153+
*/
160154
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
161-
dominatesPredecessor(bb, df) and
162-
not strictlyDominates(bb, df)
155+
bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df)
156+
or
157+
exists(BasicBlock prev | inDominanceFrontier(prev, df) |
158+
bb = getImmediateBasicBlockDominator(prev) and
159+
not bb = getImmediateBasicBlockDominator(df)
160+
)
163161
}
164162

165163
/**

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/basessa/SsaImplCommon.qll

Lines changed: 16 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -141,25 +141,23 @@ private module Liveness {
141141

142142
private import Liveness
143143

144-
/** Holds if `bb1` strictly dominates `bb2`. */
145-
private predicate strictlyDominates(BasicBlock bb1, BasicBlock bb2) {
146-
bb1 = getImmediateBasicBlockDominator+(bb2)
147-
}
148-
149-
/** Holds if `bb1` dominates a predecessor of `bb2`. */
150-
private predicate dominatesPredecessor(BasicBlock bb1, BasicBlock bb2) {
151-
exists(BasicBlock pred | pred = getABasicBlockPredecessor(bb2) |
152-
bb1 = pred
153-
or
154-
strictlyDominates(bb1, pred)
155-
)
156-
}
157-
158-
/** Holds if `df` is in the dominance frontier of `bb`. */
159-
pragma[noinline]
144+
/**
145+
* Holds if `df` is in the dominance frontier of `bb`.
146+
*
147+
* This is equivalent to:
148+
*
149+
* ```ql
150+
* bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and
151+
* not bb = getImmediateBasicBlockDominator+(df)
152+
* ```
153+
*/
160154
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
161-
dominatesPredecessor(bb, df) and
162-
not strictlyDominates(bb, df)
155+
bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df)
156+
or
157+
exists(BasicBlock prev | inDominanceFrontier(prev, df) |
158+
bb = getImmediateBasicBlockDominator(prev) and
159+
not bb = getImmediateBasicBlockDominator(df)
160+
)
163161
}
164162

165163
/**

‎ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImplCommon.qll

Lines changed: 16 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -141,25 +141,23 @@ private module Liveness {
141141

142142
private import Liveness
143143

144-
/** Holds if `bb1` strictly dominates `bb2`. */
145-
private predicate strictlyDominates(BasicBlock bb1, BasicBlock bb2) {
146-
bb1 = getImmediateBasicBlockDominator+(bb2)
147-
}
148-
149-
/** Holds if `bb1` dominates a predecessor of `bb2`. */
150-
private predicate dominatesPredecessor(BasicBlock bb1, BasicBlock bb2) {
151-
exists(BasicBlock pred | pred = getABasicBlockPredecessor(bb2) |
152-
bb1 = pred
153-
or
154-
strictlyDominates(bb1, pred)
155-
)
156-
}
157-
158-
/** Holds if `df` is in the dominance frontier of `bb`. */
159-
pragma[noinline]
144+
/**
145+
* Holds if `df` is in the dominance frontier of `bb`.
146+
*
147+
* This is equivalent to:
148+
*
149+
* ```ql
150+
* bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and
151+
* not bb = getImmediateBasicBlockDominator+(df)
152+
* ```
153+
*/
160154
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
161-
dominatesPredecessor(bb, df) and
162-
not strictlyDominates(bb, df)
155+
bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df)
156+
or
157+
exists(BasicBlock prev | inDominanceFrontier(prev, df) |
158+
bb = getImmediateBasicBlockDominator(prev) and
159+
not bb = getImmediateBasicBlockDominator(df)
160+
)
163161
}
164162

165163
/**

0 commit comments

Comments
 (0)