In order to completely unroll loops with known bound I moved the marking process (markLoopASUnrolled() function call, etc.) to the processBranch callback which takes place after the bound is already modeled. This way the bound can be checked to be known. Test cases added.
Diff Detail
Event Timeline
While this wasn't necessary in the first patch, i think here we should start cleaning up the UnrolledLoops map when we exit the loop. Because next time we encounter the loop, we may no longer want to unroll it - the value may no longer be concrete.
lib/StaticAnalyzer/Core/LoopUnrolling.cpp | ||
---|---|---|
148–149 | There's a FIXME in getKnownValue() that says that it doesn't work in some cases, eg. $x + 1 where $x$ is constrained to a constant. Could you see if this affects your code and add a test case? We can probably fix it later because now we have simplifySVal(). |
lib/StaticAnalyzer/Core/LoopUnrolling.cpp | ||
---|---|---|
148–149 | I mean $x. |
Am i understanding correctly that this patch is waiting to be rebased on top of D35684?
Yes, you understand correctly and this raises a lot of problem which I could not solve.
If I move the updateLoopStack function call to the processBranch then it means that in processCFGBlockEntrance we wont have the information if the entered block is unrolled.
It could be OK since the loop is visited at least once so we will reach processBranch and add the loop to the LoopStack. However, in case of a nested loop, the second time we would enter the inner loop we will see that the BlockVisit counter is already higher than maxBlockVisitOnPath. So we wont even enter the block even if we would mark it as a unrolled loop.
so in the following example we wont enter the inner (and unrolled) loop the second time:
for (int i=0;i<2;i++){ int& j = i; // outer loop not unrolled for (int j=0;j<5;j++){ //unrolled magic_stuff(); } }
Just to summarize the problem: the LoopStack would be updated later then we enter the first block of the loop. However, we check the counter when the block is entered.
I don't see a correct solution for that right know. The best I could come up to mark the blocks what was already unrolled and handle them as a special case.
lib/StaticAnalyzer/Core/ExprEngine.cpp | ||
---|---|---|
1507 | Asterisk on the wrong side. | |
1689 | Maybe moving this check to the next if would reduce the indentation. | |
lib/StaticAnalyzer/Core/LoopUnrolling.cpp | ||
47 | Why did you introduce expr? Wouldn't binding to the declRefExpr part be sufficient? | |
135 | This comment is not clear enough for me. Don't you already check for changes and escapes of the induction variable? | |
150 | So you do not want to introduce a hard limit on the loop bound in this patch? |
Asterisk on the wrong side.