Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis. Issue 5 (September 2019)

• Record Type: Journal Article
• Authors: DOMÉNECH, JESÚS J.; GALLAGHER, JOHN P.; GENAIM, SAMIR
• Is Part Of: Theory and practice of logic programming. Volume 19:Issue 5/6(2019)
• Page Start: 990
• Page End: 1005
• Publication Date: 2019-09
• Subjects: Control-flow refinement, -- partial evaluation, -- termination analysis, -- cost analysis; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S1471068419000310
• Languages: English
• ISSNs: 1471-0684

Abstract

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.