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

Jesus Doménech, John Patrick Gallagher, Samir Genaim

Research output: Contribution to journalJournal articleResearchpeer-review

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 and evaluation of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers.
Original languageEnglish
JournalTheory and Practice of Logic Programming
Volume19
Issue number5-6
Pages (from-to)990–1005
ISSN1471-0684
DOIs
Publication statusPublished - Sep 2019

Keywords

  • partial evaluation
  • termination analysis
  • cost analysis

Cite this

@article{14d133defcaf4983b443dac75e5c7bd4,
title = "Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis",
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 and evaluation of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers.",
keywords = "partial evaluation, termination analysis, cost analysis",
author = "Jesus Dom{\'e}nech and Gallagher, {John Patrick} and Samir Genaim",
year = "2019",
month = "9",
doi = "10.1017/S1471068419000310",
language = "English",
volume = "19",
pages = "990–1005",
journal = "Theory and Practice of Logic Programming",
issn = "1471-0684",
publisher = "Cambridge University Press",
number = "5-6",

}

Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis. / Doménech, Jesus; Gallagher, John Patrick; Genaim, Samir.

In: Theory and Practice of Logic Programming, Vol. 19, No. 5-6, 09.2019, p. 990–1005.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

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

AU - Doménech, Jesus

AU - Gallagher, John Patrick

AU - Genaim, Samir

PY - 2019/9

Y1 - 2019/9

N2 - 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 and evaluation of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers.

AB - 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 and evaluation of the technique in a termination analyzer, and its use as a preprocessing step for several cost analyzers.

KW - partial evaluation

KW - termination analysis

KW - cost analysis

U2 - 10.1017/S1471068419000310

DO - 10.1017/S1471068419000310

M3 - Journal article

VL - 19

SP - 990

EP - 1005

JO - Theory and Practice of Logic Programming

JF - Theory and Practice of Logic Programming

SN - 1471-0684

IS - 5-6

ER -