Fixed sanity checks

The foreach was erroneously labelling the `True` and `False` edges as backedges.
Added a case for the compiler generated while in the predicate `getInstructionBackEdgeSuccessor/2`
from the file `IRConstruction.qll` so that only the edges from inside the body are labeled as back edges.
This commit is contained in:
AndreiDiaconu1
2019-08-30 12:17:10 +01:00
parent 46d7b9e3bf
commit db213bbf80
3 changed files with 21 additions and 6 deletions

View File

@@ -7,6 +7,7 @@ private import TranslatedCondition
private import TranslatedElement
private import TranslatedExpr
private import TranslatedStmt
private import desugar.Foreach
private import TranslatedFunction
private import semmle.code.csharp.ir.Util
private import semmle.code.csharp.ir.internal.IRCSharpLanguage as Language
@@ -135,6 +136,18 @@ private module Cached {
)
)
or
// Compiler generated foreach while loop:
// Same as above
exists(TranslatedForeachWhile s |
s instanceof TranslatedForeachWhile and
result = s.getFirstInstruction() 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)
)
)
or
// Do-while loop:
// The back edge should be the edge(s) from the condition to the
// body. This ensures that it's the back edge that will be pruned in a `do

View File

@@ -117,8 +117,10 @@ private class TranslatedForeachFinally extends TranslatedCompilerGeneratedBlock,
/**
* The compiler generated while loop.
* Note that this class is not private since it is needed in `IRConstruction.qll`,
* to correctly mark which edges should be back edges.
*/
private class TranslatedForeachWhile extends TranslatedCompilerGeneratedStmt, ConditionContext,
class TranslatedForeachWhile extends TranslatedCompilerGeneratedStmt, ConditionContext,
TTranslatedCompilerGeneratedElement {
override ForeachStmt generatedBy;
@@ -159,18 +161,18 @@ private class TranslatedForeachWhile extends TranslatedCompilerGeneratedStmt, Co
child = getCondition() and result = getParent().getChildSuccessor(this)
}
private TranslatedStmt getBody() {
TranslatedStmt getBody() {
result = getTranslatedStmt(generatedBy.getBody())
}
private TranslatedElement getInit() {
TranslatedElement getInit() {
exists(TranslatedForeachIterVar iv |
iv.getAST() = generatedBy and
result = iv
)
}
private ValueConditionBlueprint getCondition() {
ValueConditionBlueprint getCondition() {
exists(TranslatedForeachWhileCondition cond |
cond.getAST() = generatedBy and
result = cond

View File

@@ -406,8 +406,8 @@ foreach.cs:
# 7| r1_3(Boolean) = Call : func:r1_2, this:r1_1
# 7| mu1_4(null) = ^CallSideEffect : ~mu0_2
# 7| v1_5(Void) = ConditionalBranch : r1_3
#-----| False (back edge) -> Block 3
#-----| True (back edge) -> Block 2
#-----| False -> Block 3
#-----| True -> Block 2
# 7| Block 2
# 7| r2_0(glval<Int32>) = VariableAddress[items] :