Control-Flow Refinment via Partial Evaluation

Its execution has two implicit phases: in the first one, variable y is incremented until it reaches the value of z, and in the second phase the value of x is decremented until it reaches the value 0. Control-flow refinement techniques can transform this program into the one on the right, in which the two phases are explicit. In the context of termination analysis, such a transformation simplifies the termination proof; while the original program requires a lexicographic termination argument, the transformed one requires only linear ones. In addition, in the context of resource usage (cost) analysis, tools that are based on bounding loop iterations using linear ranking functions fail to infer the cost of the first program, while they succeed in inferring a linear upper-bound on the cost of the second one. In general, splitting the control-flow might also help in inferring more precise invariants, without the need for expensive disjunctive abstract domains, and thus improve any analysis that relies on such invariants (e.g. termination and cost analyses). In the context of cost (and implicitly termination) analysis, control-flow refinement has been studied in [8] and [10]. The first [8] considers a general form of recurrence relations called cost equations, and the latter [10] considers structured imperative programs. Both handle programs with integer variables. These works demonstrated that control-flow refinement is crucial for handling programs that were considered challenging by the cost analysis community. We started with the obvious observation that control-flow refinement is based on a special kind of partial evaluation tailored for a very particular analysis. We decided to explore what we would get, in terms of precision of cost and termination analysis, if instead, we use an existing off-the-shelf partial evaluation tool. This would allow integrating control-flow refinement into existing static analysis tools without any effort. In this extended abstract, we describe preliminary experimental results obtained by using an off-the-shelf partial evaluation tool for control-flow refinement, and its impact on the precision of termination and cost analysis. Our experiments are done for Integer Transition Systems, which are graphs where edges are annotated with linear constraints describing transition relations between corresponding nodes.