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

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...

Full description

Saved in:
Bibliographic Details
Published in:Theory and practice of logic programming 2019-09, Vol.19 (5-6), p.990-1005
Main Authors: DOMÉNECH, JESÚS J., GALLAGHER, JOHN P., GENAIM, SAMIR
Format: Article
Language:English
Subjects:
35th International Conference on Logic Programming
Algorithms
Analyzers
Complexity
Cost analysis
Flow graphs
Original Article
Properties (attributes)
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1471-0684
1475-3081
DOI:10.1017/S1471068419000310