Refining the Control Structure of Loops Using Static Analysis.Gogul Balakrishnan , Sriram Sankaranarayanan , Franjo Ivancic, and Aarti Gupta |
|
We present a simple yet useful technique for refining the control
structure of loops that occur in imperative programs. Loops
containing complex control flow are common in synchronous embedded
controllers derived from modelling languages such as Lustre,
Esterel, and Simulink/Stateflow. Our approach uses a set of labels
to distinguish different control paths inside a given loop. The
iterations of the loop are abstracted as a finite state automaton
over these labels. We then use static analysis techniques to
identify infeasible iteration sequences. Such forbidden sequences are
subtracted from the initial language to obtain a refinement. In
practice, the refinement of control flow sequences often simplifies
the control flow patterns in the loop, identifying nested loops,
unrolling and unwinding automatically.
We have applied the refinement technique to improve the precision of abstract interpretation in the presence of widening. Our experiments on a set of complex reactive loop benchmarks clearly show the utility of our refinement techniques. Other potentially useful applications include termination analysis and reverse engineering models from source code.
|
| Embedded Software (EMSOFT), 2009. |
| Copyright (C) ACM Press. Please read copyright notification inside the paper. |