Control-flow refinement by partial evaluation, and its application to termination and cost analysis.

*(English)*Zbl 1434.68104Summary: Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming models, typically tailored to improving precision for a particular analysis. In this paper we explore the use of partial evaluation of Horn clauses as a general-purpose technique for control-flow refinement for integer transitions systems. These are control-flow graphs where edges are annotated with linear constraints describing transitions between corresponding nodes, and they are used in many program analysis tools. Using partial evaluation for control-flow refinement has the clear advantage over other approaches in that soundness follows from the general properties of partial evaluation; in particular, properties such as termination and complexity are preserved. We use a partial evaluation algorithm incorporating property-based abstraction, and show how the right choice of properties allows us to prove termination and to infer complexity of challenging programs that cannot be handled by state-of-the-art tools. We report on the integration of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers.

##### MSC:

68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |

PDF
BibTeX
XML
Cite

\textit{J. J. Doménech} et al., Theory Pract. Log. Program. 19, No. 5--6, 990--1005 (2019; Zbl 1434.68104)

Full Text:
DOI

##### References:

[1] | Albert, E., Arenas, P., Genaim, S., and Puebla, G.2011. Closed-form upper bounds in static cost analysis. J. Autom. Reasoning 46, 2, 161-203. · Zbl 1213.68200 |

[2] | Alias, C., Darte, A., Feautrier, P., and Gonnord, L.2010. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Static Analysis Symposium, SAS’10, R.Cousot and M.Martel, Eds. LNCS, vol. 6337. Springer, 117-133. · Zbl 1306.68017 |

[3] | Bagnara, R., Hill, P. M., and Zaffanella, E.2008. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72,1-2, 3-21. |

[4] | Bagnara, R., Mesnard, F., Pescetti, A., and Zaffanella, E.2012. A new look at the automatic synthesis of linear ranking functions. Inf. Comput. 215, 47-67. · Zbl 1251.68073 |

[5] | Ben-Amram, A. M. and Genaim, S.2014. Ranking functions for linear-constraint loops. Journal of the ACM61, 4 (July), 26:1-26:55. · Zbl 1321.68296 |

[6] | Ben-Amram, A. M. and Genaim, S.2017. On multiphase-linear ranking functions. In Computer Aided Verification, CAV 2017, R.Majumdar and V.Kuncak, Eds. LNCS, vol. 10427. Springer, 601-620. |

[7] | Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., and Rubio, A.2017. Proving termination through conditional termination. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS’17, A.Legay and T.Margaria, Eds. LNCS, vol. 10205. 99-117. |

[8] | Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., and Piterman, N.2016. T2: temporal property verification. In Tools and Algorithms for the Construction and Analysis of Systems TACAS 2016, M.Chechik and J.Raskin, Eds. LNCS, vol. 9636. Springer, 387-393. |

[9] | Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., and Giesl, J.2016. Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38, 4, 13:1-13:50. |

[10] | Cousot, P. and Halbwachs, N.1978. Automatic discovery of linear restraints among variables of a program. In Fifth Annual ACM Symposium on Principles of Programming Languages, POPL’78, A. V.Aho, S. N.Zilles, and T. G.Szymanski, Eds. ACM Press, 84-96. |

[11] | De Angelis, E., Fioravanti, F., Pettorossi, A., and Proietti, M.2012. Specialization with constrained generalization for software model checking. In LOPSTR 2012, E.Albert, Ed. LNCS, vol. 7844. Springer, 51-70. · Zbl 1394.68072 |

[12] | Doménech, J. J., Gallagher, J. P., and Genaim, S.2019. Control-flow refinement by partial evaluation, and its application to termination and cost analysis. CoRR abs/1907.12345. https://arxiv.org/abs/1907.12345. |

[13] | Fioravanti, F., Pettorossi, A., Proietti, M., and Senni, V.2012. Improving reachability analysis of infinite state systems by specialization. Fundam. Inform. 119, 3-4, 281-300. · Zbl 1279.68209 |

[14] | Flores-Montoya, A.2017. Cost analysis of programs based on the refinement of cost relations. Ph.D. thesis, Darmstadt University of Technology, Germany. |

[15] | Flores-Montoya, A. and Hähnle, R.2014. Resource analysis of complex programs with cost equations. In Asian Symposium on Programming Languages and Systems, APLAS 2014, J.Garrigue, Ed. LNCS, vol. 8858. Springer, 275-295. · Zbl 1453.68047 |

[16] | Gallagher, J. P.2019. Polyvariant program specialisation with property-based abstraction. In Pre-proceedings of Verification and Program Transformation, VPT’19, A.Lisitsa and A. P.Nemytykh, Eds. Available at http://refal.botik.ru/vpt/vpt2019/VPT2019_paper_5.pdf. Accepted for EPTCS. |

[17] | Gulwani, S., Jain, S., and Koskinen, E.2009. Control-flow refinement and progress invariants for bound analysis. In Programming Language Design and Implementation, PLDI’09, M.Hind and A.Diwan, Eds. ACM, 375-385. |

[18] | iRank2019. iRankFinder. http://irankfinder.loopkiller.com. |

[19] | Kafle, B., Gallagher, J. P., Gange, G., Schachte, P., Søndergaard, H., and Stuckey, P. J.2018. An iterative approach to precondition inference using constrained Horn clauses. TPLP 18, 3-4, 553-570. · Zbl 1451.68075 |

[20] | Leuschel, M.2004. A framework for the integration of partial evaluation and abstract interpretation of logic programs. ACM Trans. Program. Lang. Syst. 26,3, 413-463. |

[21] | Leuschel, M., Elphick, D., Varea, M., Craig, S., and Fontaine, M.2006. The Ecce and Logen partial evaluators and their web interfaces. In PEPM 2006, J.Hatcliff and F.Tip, Eds. ACM, 88-94. |

[22] | Leuschel, M. and Massart, T.2000. Infinite state model checking by abstract interpretation and program specialisation. In LOPSTR’99, A.Bossi, Ed. LNCS, vol. 1817. 63-82. · Zbl 0964.68086 |

[23] | Podelski, A. and Rybalchenko, A.2004. A complete method for the synthesis of linear ranking functions. In Verification, Model Checking, and Abstract Interpretation, VMCAI’04, B.Steffen and G.Levi, Eds. LNCS, vol. 2937. Springer, 239-251. · Zbl 1202.68109 |

[24] | Puebla, G., Albert, E., and Hermenegildo, M. V.2006. Abstract interpretation with specialized definitions. In SAS 2006, K.Yi, Ed. LNCS, vol. 4134. Springer, 107-126. · Zbl 1225.68076 |

[25] | Puebla, G., Hermenegildo, M., and Gallagher, J. P.1999. An integration of partial evaluation in a generic abstract interpretation framework. In PEPM’99, O.Danvy, Ed. Technical report BRICS-NS-99-1. University of Aarhus, 75-84. |

[26] | Sharma, R., Dillig, I., Dillig, T., and Aiken, A.2011. Simplifying loop invariant generation using splitter predicates. In Computer Aided Verification, CAV 2011, G.Gopalakrishnan and S.Qadeer, Eds. LNCS, vol. 6806. Springer, 703-719. |

[27] | TERMCOMP2019. http://termination-portal.org/wiki/Termination_Competition_2019. |

[28] | TPDB2019. http://termination-portal.org/wiki/TPDB. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.