Verified Validation of Program Slicing

2 downloads 180 Views 424KB Size Report
Keywords program slicing, verified compiler, verified static anal- ysis. 1. Introduction. Program slicing is a ..... the
banner above paper title

Verified Validation of Program Slicing Sandrine Blazy

Andre Maroneze

David Pichardie

IRISA - University of Rennes 1 [email protected]

IRISA - University of Rennes 1 [email protected]

IRISA - ENS Rennes [email protected]

Abstract

slicing is also often used in conjunction with other analyses, as a preprocessing step, thus improving both precision and efficiency of the analyses. For instance, reference tools for estimating the worst case execution time (WCET) of programs perform a preliminary program slicing step when estimating loop bounds of programs; improvements due to program slicing are crystal clear on programs with nested loops. State of the art program slicers operate mainly over program dependence graphs (PDG), a sophisticated data structure representing explicitly data and control dependences [13]. Constructing a slice consists mainly in traversing a PDG (in order to compute paths) and performing a post-dominance analysis. Program slicers that construct executable slices in the presence of jump statements implement delicate and error-prone graph algorithms. A few paper-andpencil proofs related to the correctness of program slicing exist in the litterature [24, 23, 2]. The key ingredients to these proofs are presented in [23, 2], where the authors define the notions of relevant variables and specific vertices called next observable vertices that are used only in the proof. To the best of our knowledge, the only mechanized proof of program slicing is detailed in [28]. It uses the Isabelle/HOL proof assistant to formalize in a non-constructive way a PDG and its use to produce program slices. We follow a different approach, called a posteriori validation [19, 26] to formally verify a program slicer operating over PDG. Instead of formalizing a PDG, we write in OCaml an unverified program slicer and we validate the results of each of its runs. Our validator is written in Coq; it is efficient and proved correct. We chose this pragmatic approach to formal verification because our program slicer relies on sophisticated data structures and delicate algorithms. Program slicing is also interesting for a posteriori validation because the correctness proof of program slicing requires to compute new supplementary information from the PDG (relying on relevant variables and next observable vertices), thus decoupling the slicing algorithm from its proof. Our semantics-preserving program slicer is integrated into the CompCert formally verified compiler [17]. It operates over an intermediate language of the compiler having the same expressiveness as C. Our work has been currently used for formally verifying a loop bound estimation analysis [7]. Some details about this analysis and comparisons with the current work are given in the related work section. All results presented in this paper have been mechanically verified using the Coq proof assistant. The complete development is available online [1]. This paper makes the following contributions:

Program slicing is a well-known program transformation which simplifies a program with respect to a given criterion while preserving its semantics. Since the seminal paper published by Weiser in 1981, program slicing is still widely used in various application domains. State of the art program slicers operate over program dependence graphs (PDG), a sophisticated data structure combining data and control dependences. In this paper, we follow the a posteriori validation approach to formally verify (in Coq) a general program slicer. Our validator for program slicing is efficient and validates the results of a run of an unverified program slicer. Program slicing is interesting for a posteriori validation because the correctness proof of program slicing requires to compute new supplementary information from the PDG, thus decoupling the slicing algorithm from its proof. Our semantics-preserving program slicer is integrated into the CompCert formally verified compiler. It operates over an intermediate language of the compiler having the same expressiveness as C. Our experiments show that our formally verified validator scales on large realistic programs. Keywords program slicing, verified compiler, verified static analysis

1.

Introduction

Program slicing is a technique to simplify a program with respect to a criterion, that is, a variable at a given program point. It consists in the removal of statements that have no influence on the criterion, and are said to have been sliced away. The result of this process, which is called a sliced program, is another program, a simplified version of the original one which behaves in the same way, with respect to the slicing criterion. Since the seminal paper published by Weiser [29] in 1981, a great deal of papers on different kinds of program slicing, operating over various kinds of programming languages were published, including several surveys (e.g. [25] and [30]). The main application domains of program slicing are debugging, program understanding and software maintenance. Recent application domains are still emerging. For instance, program slicing is used in automatic program proof to simplify programs and specifications so that they can be easier to prove with deductive verification tools [3]. Program

1. a validation algorithm for program slicing, formally verified in Coq, 2. a fully executable program slicer, integrated in the CompCert C compiler, 3. experiments showing that our validator is efficient and scales on large realistic programs.

[Copyright notice will appear here once ’preprint’ option is removed.]

Verified Validation of Program Slicing

1

2014/10/11

by replacing every statement not in the slice either with an empty statement (written as skip) or with an empty conditional statement. The condition of an empty statement is either true or false. In Figure 1, as there is no dependence from the condition i