@@ -143,26 +143,23 @@ private module Cached {
143143 .getInstructionSuccessor ( getInstructionTag ( instruction ) , kind )
144144 }
145145
146- // This predicate has pragma[noopt] because otherwise the `getAChild*` calls
147- // get joined too early. The join order for the loop cases goes like this:
148- // - Find all loops of that type (tens of thousands).
149- // - Find all edges into the start of the loop (x 2).
150- // - Restrict to edges that originate within the loop (/ 2).
151- pragma [ noopt]
152- cached
153- Instruction getInstructionBackEdgeSuccessor ( Instruction instruction , EdgeKind kind ) {
146+ /**
147+ * Holds if the CFG edge (`sourceElement`, `sourceTag`) ---`kind`-->
148+ * `targetInstruction` is a back edge under the condition that
149+ * `requiredAncestor` is an ancestor of `sourceElement`.
150+ */
151+ private predicate backEdgeCandidate (
152+ TranslatedElement sourceElement , InstructionTag sourceTag , TranslatedElement requiredAncestor ,
153+ Instruction targetInstruction , EdgeKind kind
154+ ) {
154155 // While loop:
155156 // Any edge from within the body of the loop to the condition of the loop
156157 // is a back edge. This includes edges from `continue` and the fall-through
157158 // edge(s) after the last instruction(s) in the body.
158159 exists ( TranslatedWhileStmt s |
159- s instanceof TranslatedWhileStmt and
160- result = s .getFirstConditionInstruction ( ) and
161- exists ( TranslatedElement inBody , InstructionTag tag |
162- result = inBody .getInstructionSuccessor ( tag , kind ) and
163- exists ( TranslatedElement body | body = s .getBody ( ) | inBody = body .getAChild * ( ) ) and
164- instruction = inBody .getInstruction ( tag )
165- )
160+ targetInstruction = s .getFirstConditionInstruction ( ) and
161+ targetInstruction = sourceElement .getInstructionSuccessor ( sourceTag , kind ) and
162+ requiredAncestor = s .getBody ( )
166163 )
167164 or
168165 // Do-while loop:
@@ -171,15 +168,9 @@ private module Cached {
171168 // { ... } while (0)` statement. Note that all `continue` statements in a
172169 // do-while loop produce forward edges.
173170 exists ( TranslatedDoStmt s |
174- s instanceof TranslatedDoStmt and
175- exists ( TranslatedStmt body | body = s .getBody ( ) | result = body .getFirstInstruction ( ) ) and
176- exists ( TranslatedElement inCondition , InstructionTag tag |
177- result = inCondition .getInstructionSuccessor ( tag , kind ) and
178- exists ( TranslatedElement condition | condition = s .getCondition ( ) |
179- inCondition = condition .getAChild * ( )
180- ) and
181- instruction = inCondition .getInstruction ( tag )
182- )
171+ targetInstruction = s .getBody ( ) .getFirstInstruction ( ) and
172+ targetInstruction = sourceElement .getInstructionSuccessor ( sourceTag , kind ) and
173+ requiredAncestor = s .getCondition ( )
183174 )
184175 or
185176 // For loop:
@@ -189,33 +180,42 @@ private module Cached {
189180 // last instruction(s) in the body. A for loop may not have a condition, in
190181 // which case `getFirstConditionInstruction` returns the body instead.
191182 exists ( TranslatedForStmt s |
192- s instanceof TranslatedForStmt and
193- result = s .getFirstConditionInstruction ( ) and
194- exists ( TranslatedElement inLoop , InstructionTag tag |
195- result = inLoop .getInstructionSuccessor ( tag , kind ) and
196- exists ( TranslatedElement bodyOrUpdate |
197- bodyOrUpdate = s .getBody ( )
198- or
199- bodyOrUpdate = s .getUpdate ( )
200- |
201- inLoop = bodyOrUpdate .getAChild * ( )
202- ) and
203- instruction = inLoop .getInstruction ( tag )
183+ targetInstruction = s .getFirstConditionInstruction ( ) and
184+ targetInstruction = sourceElement .getInstructionSuccessor ( sourceTag , kind ) and
185+ (
186+ requiredAncestor = s .getUpdate ( )
187+ or
188+ not exists ( s .getUpdate ( ) ) and
189+ requiredAncestor = s .getBody ( )
204190 )
205191 )
206192 or
207193 // Range-based for loop:
208194 // Any edge from within the update of the loop to the condition of
209195 // the loop is a back edge.
210- exists ( TranslatedRangeBasedForStmt s , TranslatedCondition condition |
211- s instanceof TranslatedRangeBasedForStmt and
212- condition = s .getCondition ( ) and
213- result = condition .getFirstInstruction ( ) and
214- exists ( TranslatedElement inUpdate , InstructionTag tag |
215- result = inUpdate .getInstructionSuccessor ( tag , kind ) and
216- exists ( TranslatedElement update | update = s .getUpdate ( ) | inUpdate = update .getAChild * ( ) ) and
217- instruction = inUpdate .getInstruction ( tag )
218- )
196+ exists ( TranslatedRangeBasedForStmt s |
197+ targetInstruction = s .getCondition ( ) .getFirstInstruction ( ) and
198+ targetInstruction = sourceElement .getInstructionSuccessor ( sourceTag , kind ) and
199+ requiredAncestor = s .getUpdate ( )
200+ )
201+ }
202+
203+ private predicate jumpSourceHasAncestor ( TranslatedElement jumpSource , TranslatedElement ancestor ) {
204+ backEdgeCandidate ( jumpSource , _, _, _, _) and
205+ ancestor = jumpSource
206+ or
207+ // For performance, we don't want a fastTC here
208+ jumpSourceHasAncestor ( jumpSource , ancestor .getAChild ( ) )
209+ }
210+
211+ cached
212+ Instruction getInstructionBackEdgeSuccessor ( Instruction instruction , EdgeKind kind ) {
213+ exists (
214+ TranslatedElement sourceElement , InstructionTag sourceTag , TranslatedElement requiredAncestor
215+ |
216+ backEdgeCandidate ( sourceElement , sourceTag , requiredAncestor , result , kind ) and
217+ jumpSourceHasAncestor ( sourceElement , requiredAncestor ) and
218+ instruction = sourceElement .getInstruction ( sourceTag )
219219 )
220220 or
221221 // Goto statement:
@@ -225,7 +225,6 @@ private module Cached {
225225 // same location for source and target, so we conservatively assume that
226226 // such a `goto` creates a back edge.
227227 exists ( TranslatedElement s , GotoStmt goto |
228- goto instanceof GotoStmt and
229228 not isStrictlyForwardGoto ( goto ) and
230229 goto = s .getAST ( ) and
231230 exists ( InstructionTag tag |
0 commit comments