Hostname: page-component-848d4c4894-x24gv Total loading time: 0 Render date: 2024-05-14T05:36:18.529Z Has data issue: false hasContentIssue false
  • English
  • Français

Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis

Published online by Cambridge University Press:  20 September 2019

JESÚS J. DOMÉNECH Open the ORCID record for JESÚS J. DOMÉNECH [Opens in a new window] ,
JOHN P. GALLAGHER Open the ORCID record for JOHN P. GALLAGHER [Opens in a new window]  and
SAMIR GENAIM Open the ORCID record for SAMIR GENAIM [Opens in a new window]
JESÚS J. DOMÉNECH
Affiliation:
Universidad Complutense de Madrid, Spain (e-mail: jdomenech@ucm.es)
JOHN P. GALLAGHER
Affiliation:
Roskilde University, Denmark and IMDEA Software Institute, Spain (e-mail: jpg@ruc.dk)
SAMIR GENAIM
Affiliation:
Universidad Complutense de Madrid, Spain (e-mail: sgenaim@ucm.es)
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Keywords

Control-flow refinementpartial evaluationtermination analysiscost analysis
Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 19 , Special Issue 5-6: 35th International Conference on Logic Programming , September 2019 , pp. 990 - 1005
Copyright
© Cambridge University Press 2019 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

*

This work was funded partially by the Spanish MICINN/FEDER, UE project RTI2018-094403-BC31, the MINECO project TIN2015-69175-C4-2-R, the CM project S2018/TCS-4314 and by the predoctoral UCM grant CT27/16-CT28/16.

References

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.CrossRefGoogle Scholar
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, Cousot, R. and Martel, M., Eds. LNCS, vol. 6337. Springer, 117–133.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
Ben-Amram, A. M. and Genaim, S. 2014. Ranking functions for linear-constraint loops. Journal of the ACM 61, 4 (July), 26:1–26:55.CrossRefGoogle Scholar
Ben-Amram, A. M. and Genaim, S. 2017. On multiphase-linear ranking functions. In Computer Aided Verification, CAV 2017, Majumdar, R. and Kuncak, V., Eds. LNCS, vol. 10427. Springer, 601–620.Google Scholar
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, Legay, A. and Margaria, T., Eds. LNCS, vol. 10205. 99–117.Google Scholar
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, Chechik, M. and Raskin, J., Eds. LNCS, vol. 9636. Springer, 387–393.Google Scholar
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.CrossRefGoogle Scholar
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, Aho, A. V., Zilles, S. N., and Szymanski, T. G., Eds. ACM Press, 84–96.Google Scholar
De Angelis, E., Fioravanti, F., Pettorossi, A., and Proietti, M. 2012. Specialization with constrained generalization for software model checking. In LOPSTR 2012, Albert, E., Ed. LNCS, vol. 7844. Springer, 51–70.Google Scholar
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.Google Scholar
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.Google Scholar
Flores-Montoya, A. 2017. Cost analysis of programs based on the refinement of cost relations. Ph.D. thesis, Darmstadt University of Technology, Germany.Google Scholar
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, Garrigue, J., Ed. LNCS, vol. 8858. Springer, 275–295.Google Scholar
Gallagher, J. P. 2019. Polyvariant program specialisation with property-based abstraction. In Pre-proceedings of Verification and Program Transformation, VPT’19, Lisitsa, A. and Nemytykh, A. P., Eds. Available at http://refal.botik.ru/vpt/vpt2019/VPT2019_paper_5.pdf. Accepted for EPTCS.Google Scholar
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, Hind, M. and Diwan, A., Eds. ACM, 375–385.Google Scholar
iRank 2019. iRankFinder. http://irankfinder.loopkiller.com.Google Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
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, Hatcliff, J. and Tip, F., Eds. ACM, 88–94.Google Scholar
Leuschel, M. and Massart, T. 2000. Infinite state model checking by abstract interpretation and program specialisation. In LOPSTR’99, Bossi, A., Ed. LNCS, vol. 1817. 63–82.Google Scholar
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, Steffen, B. and Levi, G., Eds. LNCS, vol. 2937. Springer, 239–251.Google Scholar
Puebla, G., Albert, E., and Hermenegildo, M. V. 2006. Abstract interpretation with specialized definitions. In SAS 2006, Yi, K., Ed. LNCS, vol. 4134. Springer, 107–126.Google Scholar
Puebla, G., Hermenegildo, M., and Gallagher, J. P. 1999. An integration of partial evaluation in a generic abstract interpretation framework. In PEPM’99, Danvy, O., Ed. Technical report BRICS-NS-99-1. University of Aarhus, 75–84.Google Scholar
Sharma, R., Dillig, I., Dillig, T., and Aiken, A. 2011. Simplifying loop invariant generation using splitter predicates. In Computer Aided Verification, CAV 2011, Gopalakrishnan, G. and Qadeer, S., Eds. LNCS, vol. 6806. Springer, 703–719.Google Scholar
TERMCOMP 2019. http://termination-portal.org/wiki/Termination_Competition_2019.Google Scholar
TPDB 2019. http://termination-portal.org/wiki/TPDB.Google Scholar