Daniel Lupei
Having loops in a program that is to be symbolically executed increases the size of the execution tree exponentially. For instance, executing n iterations over the body of a loop that can generate k paths has the potential of producing up to kn paths. However, in some cases, these paths are very similar and their influence on the state of the application can be deduced using theorem proving support.
A = Array[n]; sum = 0; for i = 1 to n if A[i] >= 0 then sum += A[i]; else sum += -A[i]; if sum < 0 then out_of_bounds access; else ...; The first stage in our approach would be to prove that no out-of-bounds accesses take place inside the loop which is straightforward to do since AccSet(Loop) = {A[i]| i=1..n}. In the second stage, since we have a single branch that depends on the WrSet(Loop), we will have to consider at most 2 paths from the total of 2n possible paths. We will then have to rely on a theorem prover to show that the sum of positive number can never be negative, and as a result there is no n such that the “out-of-bounds access” takes place. While this approach will end up performing a comprehensive analysis across all possible behaviors of the program, it is limited by the power of the theorem prover to reason about the operations performed by the application across sets of objects. In the absence of such support, one could incrementally try iterating for a bounded number of times over the loop in the hope that this will be sufficient for exploring all the branches following it. In case of success the analysis can be declared complete, otherwise we cannot know for sure whether the unexplored paths are infeasible for any n or our bound was too small. |

One-Pagers > OP3: One Infinite Loop >