@@ -120,26 +120,23 @@ private module Cached {
120120 .getInstructionSuccessor ( getInstructionTag ( instruction ) , kind )
121121 }
122122
123- // This predicate has pragma[noopt] because otherwise the `getAChild*` calls
124- // get joined too early. The join order for the loop cases goes like this:
125- // - Find all loops of that type (tens of thousands).
126- // - Find all edges into the start of the loop (x 2).
127- // - Restrict to edges that originate within the loop (/ 2).
128- pragma [ noopt]
129- cached
130- Instruction getInstructionBackEdgeSuccessor ( Instruction instruction , EdgeKind kind ) {
123+ /**
124+ * Holds if the CFG edge (`sourceElement`, `sourceTag`) ---`kind`-->
125+ * `targetInstruction` is a back edge under the condition that
126+ * `requiredAncestor` is an ancestor of `sourceElement`.
127+ */
128+ private predicate backEdgeCandidate (
129+ TranslatedElement sourceElement , InstructionTag sourceTag , TranslatedElement requiredAncestor ,
130+ Instruction targetInstruction , EdgeKind kind
131+ ) {
131132 // While loop:
132133 // Any edge from within the body of the loop to the condition of the loop
133134 // is a back edge. This includes edges from `continue` and the fall-through
134135 // edge(s) after the last instruction(s) in the body.
135136 exists ( TranslatedWhileStmt s |
136- s instanceof TranslatedWhileStmt and
137- result = s .getFirstConditionInstruction ( ) and
138- exists ( TranslatedElement inBody , InstructionTag tag |
139- result = inBody .getInstructionSuccessor ( tag , kind ) and
140- exists ( TranslatedElement body | body = s .getBody ( ) | inBody = body .getAChild * ( ) ) and
141- instruction = inBody .getInstruction ( tag )
142- )
137+ targetInstruction = s .getFirstConditionInstruction ( ) and
138+ targetInstruction = sourceElement .getInstructionSuccessor ( sourceTag , kind ) and
139+ requiredAncestor = s .getBody ( )
143140 )
144141 or
145142 // Do-while loop:
@@ -148,15 +145,9 @@ private module Cached {
148145 // { ... } while (0)` statement. Note that all `continue` statements in a
149146 // do-while loop produce forward edges.
150147 exists ( TranslatedDoStmt s |
151- s instanceof TranslatedDoStmt and
152- exists ( TranslatedStmt body | body = s .getBody ( ) | result = body .getFirstInstruction ( ) ) and
153- exists ( TranslatedElement inCondition , InstructionTag tag |
154- result = inCondition .getInstructionSuccessor ( tag , kind ) and
155- exists ( TranslatedElement condition | condition = s .getCondition ( ) |
156- inCondition = condition .getAChild * ( )
157- ) and
158- instruction = inCondition .getInstruction ( tag )
159- )
148+ targetInstruction = s .getBody ( ) .getFirstInstruction ( ) and
149+ targetInstruction = sourceElement .getInstructionSuccessor ( sourceTag , kind ) and
150+ requiredAncestor = s .getCondition ( )
160151 )
161152 or
162153 // For loop:
@@ -166,33 +157,42 @@ private module Cached {
166157 // last instruction(s) in the body. A for loop may not have a condition, in
167158 // which case `getFirstConditionInstruction` returns the body instead.
168159 exists ( TranslatedForStmt s |
169- s instanceof TranslatedForStmt and
170- result = s .getFirstConditionInstruction ( ) and
171- exists ( TranslatedElement inLoop , InstructionTag tag |
172- result = inLoop .getInstructionSuccessor ( tag , kind ) and
173- exists ( TranslatedElement bodyOrUpdate |
174- bodyOrUpdate = s .getBody ( )
175- or
176- bodyOrUpdate = s .getUpdate ( )
177- |
178- inLoop = bodyOrUpdate .getAChild * ( )
179- ) and
180- instruction = inLoop .getInstruction ( tag )
160+ targetInstruction = s .getFirstConditionInstruction ( ) and
161+ targetInstruction = sourceElement .getInstructionSuccessor ( sourceTag , kind ) and
162+ (
163+ requiredAncestor = s .getUpdate ( )
164+ or
165+ not exists ( s .getUpdate ( ) ) and
166+ requiredAncestor = s .getBody ( )
181167 )
182168 )
183169 or
184170 // Range-based for loop:
185171 // Any edge from within the update of the loop to the condition of
186172 // the loop is a back edge.
187- exists ( TranslatedRangeBasedForStmt s , TranslatedCondition condition |
188- s instanceof TranslatedRangeBasedForStmt and
189- condition = s .getCondition ( ) and
190- result = condition .getFirstInstruction ( ) and
191- exists ( TranslatedElement inUpdate , InstructionTag tag |
192- result = inUpdate .getInstructionSuccessor ( tag , kind ) and
193- exists ( TranslatedElement update | update = s .getUpdate ( ) | inUpdate = update .getAChild * ( ) ) and
194- instruction = inUpdate .getInstruction ( tag )
195- )
173+ exists ( TranslatedRangeBasedForStmt s |
174+ targetInstruction = s .getCondition ( ) .getFirstInstruction ( ) and
175+ targetInstruction = sourceElement .getInstructionSuccessor ( sourceTag , kind ) and
176+ requiredAncestor = s .getUpdate ( )
177+ )
178+ }
179+
180+ private predicate jumpSourceHasAncestor ( TranslatedElement jumpSource , TranslatedElement ancestor ) {
181+ backEdgeCandidate ( jumpSource , _, _, _, _) and
182+ ancestor = jumpSource
183+ or
184+ // For performance, we don't want a fastTC here
185+ jumpSourceHasAncestor ( jumpSource , ancestor .getAChild ( ) )
186+ }
187+
188+ cached
189+ Instruction getInstructionBackEdgeSuccessor ( Instruction instruction , EdgeKind kind ) {
190+ exists (
191+ TranslatedElement sourceElement , InstructionTag sourceTag , TranslatedElement requiredAncestor
192+ |
193+ backEdgeCandidate ( sourceElement , sourceTag , requiredAncestor , result , kind ) and
194+ jumpSourceHasAncestor ( sourceElement , requiredAncestor ) and
195+ instruction = sourceElement .getInstruction ( sourceTag )
196196 )
197197 or
198198 // Goto statement:
@@ -202,7 +202,6 @@ private module Cached {
202202 // same location for source and target, so we conservatively assume that
203203 // such a `goto` creates a back edge.
204204 exists ( TranslatedElement s , GotoStmt goto |
205- goto instanceof GotoStmt and
206205 not isStrictlyForwardGoto ( goto ) and
207206 goto = s .getAST ( ) and
208207 exists ( InstructionTag tag |
0 commit comments