Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -120,26 +120,23 @@ private module Cached {
.getInstructionSuccessor(getInstructionTag(instruction), kind)
}

// This predicate has pragma[noopt] because otherwise the `getAChild*` calls
// get joined too early. The join order for the loop cases goes like this:
// - Find all loops of that type (tens of thousands).
// - Find all edges into the start of the loop (x 2).
// - Restrict to edges that originate within the loop (/ 2).
pragma[noopt]
cached
Instruction getInstructionBackEdgeSuccessor(Instruction instruction, EdgeKind kind) {
/**
* Holds if the CFG edge (`sourceElement`, `sourceTag`) ---`kind`-->
* `targetInstruction` is a back edge under the condition that
* `requiredAncestor` is an ancestor of `sourceElement`.
*/
private predicate backEdgeCandidate(
TranslatedElement sourceElement, InstructionTag sourceTag, TranslatedElement requiredAncestor,
Instruction targetInstruction, EdgeKind kind
) {
// While loop:
// Any edge from within the body of the loop to the condition of the loop
// is a back edge. This includes edges from `continue` and the fall-through
// edge(s) after the last instruction(s) in the body.
exists(TranslatedWhileStmt s |
s instanceof TranslatedWhileStmt and
result = s.getFirstConditionInstruction() and
exists(TranslatedElement inBody, InstructionTag tag |
result = inBody.getInstructionSuccessor(tag, kind) and
exists(TranslatedElement body | body = s.getBody() | inBody = body.getAChild*()) and
instruction = inBody.getInstruction(tag)
)
targetInstruction = s.getFirstConditionInstruction() and
targetInstruction = sourceElement.getInstructionSuccessor(sourceTag, kind) and
requiredAncestor = s.getBody()
)
or
// Do-while loop:
Expand All @@ -148,15 +145,9 @@ private module Cached {
// { ... } while (0)` statement. Note that all `continue` statements in a
// do-while loop produce forward edges.
exists(TranslatedDoStmt s |
s instanceof TranslatedDoStmt and
exists(TranslatedStmt body | body = s.getBody() | result = body.getFirstInstruction()) and
exists(TranslatedElement inCondition, InstructionTag tag |
result = inCondition.getInstructionSuccessor(tag, kind) and
exists(TranslatedElement condition | condition = s.getCondition() |
inCondition = condition.getAChild*()
) and
instruction = inCondition.getInstruction(tag)
)
targetInstruction = s.getBody().getFirstInstruction() and
targetInstruction = sourceElement.getInstructionSuccessor(sourceTag, kind) and
requiredAncestor = s.getCondition()
)
or
// For loop:
Expand All @@ -166,33 +157,42 @@ private module Cached {
// last instruction(s) in the body. A for loop may not have a condition, in
// which case `getFirstConditionInstruction` returns the body instead.
exists(TranslatedForStmt s |
s instanceof TranslatedForStmt and
result = s.getFirstConditionInstruction() and
exists(TranslatedElement inLoop, InstructionTag tag |
result = inLoop.getInstructionSuccessor(tag, kind) and
exists(TranslatedElement bodyOrUpdate |
bodyOrUpdate = s.getBody()
or
bodyOrUpdate = s.getUpdate()
|
inLoop = bodyOrUpdate.getAChild*()
) and
instruction = inLoop.getInstruction(tag)
targetInstruction = s.getFirstConditionInstruction() and
targetInstruction = sourceElement.getInstructionSuccessor(sourceTag, kind) and
(
requiredAncestor = s.getUpdate()
or
not exists(s.getUpdate()) and
requiredAncestor = s.getBody()
)
)
or
// Range-based for loop:
// Any edge from within the update of the loop to the condition of
// the loop is a back edge.
exists(TranslatedRangeBasedForStmt s, TranslatedCondition condition |
s instanceof TranslatedRangeBasedForStmt and
condition = s.getCondition() and
result = condition.getFirstInstruction() and
exists(TranslatedElement inUpdate, InstructionTag tag |
result = inUpdate.getInstructionSuccessor(tag, kind) and
exists(TranslatedElement update | update = s.getUpdate() | inUpdate = update.getAChild*()) and
instruction = inUpdate.getInstruction(tag)
)
exists(TranslatedRangeBasedForStmt s |
targetInstruction = s.getCondition().getFirstInstruction() and
targetInstruction = sourceElement.getInstructionSuccessor(sourceTag, kind) and
requiredAncestor = s.getUpdate()
)
}

private predicate jumpSourceHasAncestor(TranslatedElement jumpSource, TranslatedElement ancestor) {
backEdgeCandidate(jumpSource, _, _, _, _) and
ancestor = jumpSource
or
// For performance, we don't want a fastTC here
jumpSourceHasAncestor(jumpSource, ancestor.getAChild())
}

cached
Instruction getInstructionBackEdgeSuccessor(Instruction instruction, EdgeKind kind) {
exists(
TranslatedElement sourceElement, InstructionTag sourceTag, TranslatedElement requiredAncestor
|
backEdgeCandidate(sourceElement, sourceTag, requiredAncestor, result, kind) and
jumpSourceHasAncestor(sourceElement, requiredAncestor) and
instruction = sourceElement.getInstruction(sourceTag)
)
or
// Goto statement:
Expand All @@ -202,7 +202,6 @@ private module Cached {
// same location for source and target, so we conservatively assume that
// such a `goto` creates a back edge.
exists(TranslatedElement s, GotoStmt goto |
goto instanceof GotoStmt and
not isStrictlyForwardGoto(goto) and
goto = s.getAST() and
exists(InstructionTag tag |
Expand Down