Evaluation partielle symbolique : une analyse sémantique des programmes C en vue de leur vérification.

P. FONTALBE

IBP-Litp 1996/Th/04: THÈSE de DOCTORAT de l'UNIVERSITÉ PARIS 6 Litp / Litp research reports
216 pages - Mai/May 1996 - French document.

PostScript : Ko /Kb

Titre / Title: Evaluation partielle symbolique : une analyse sémantique des programmes C en vue de leur vérification.

Résumé : Nous proposons dans cette thèse une technique d'analyse sémantique statique des programmes C élaborée à partir de l'évaluation partielle et de l'évaluation symbolique. La première méthode consiste à réduire un programme en fixant la valeur d'un sous-ensemble de ses paramètres pour obtenir un programme résiduel ayant la même sémantique que l'original pour ces valeurs ; la seconde consiste à évaluer le programme en propageant dans son code des symboles de valeurs donnés arbitrairement à ses variables d'entrée.
L'évaluation partielle symbolique (EPS) que nous proposons est une synthèse de ces deux méthodes. Son but est non seulement de vérifier statiquement la sémantique d'un programme C donné, en détectant statiquement des erreurs "run-time" comme dans l'évaluation symbolique, mais également de calculer un programme résiduel dont la sémantique est une abstraction de celle du programme original (et non pas une sémantique équivalente comme dans le cas de l'évaluation partielle).
Cette méthode présente le caractère statique "off-line" de l'évaluation partielle le caractère "flow sensitive" de l'évaluation symbolique. Ainsi l'intérêt du programme résiduel est double : d'une part, sa représentation est débarrassée de tout ce qui ne contribue pas directement à sa sémantique, d'autre part, chacun de ses chemins d'exécutions possibles est distingué des autres ; ainsi il se prête à diverses utilisations ultérieures, par exemple d'autres analyses ou des séries de tests, une bonne partie du travail étant alors déjà effectuée.

Abstract : We introduce in this work a static semantical technique for C programs, built from partial evaluation and symbolic evaluation. The former consists in reducing a given program by fixing the value of a subset of its parametres, thus obtaining a residual program which semantics is equivalent to the original's for these values; the latter consists in evaluating the program by propagating into its code some symbols given arbitrarily as a value to its parametres.
The Symbolic Partial Evaluation (SPE) proposed in this work is a synthesis of these two methods. Its goal is not only to verify statically the semantics of a given C program, by statically detecting some "run-time" errors like in symbolic evaluation, but also to compute a residual program which semantics is an abstraction of the original's (and not an equivalent one like in partial evaluation).
This method presents the "off-line" aspect of a partial evaluation, and the "flow sensitive" aspect of symbolic evaluation. Thus, the interest of the residual program is twofold: first, its representation gets rid of everything that does not contribute directly to its semantics; second, each possible execution path is distinguished from each other. Thus, this provides an interesting aspect for various operations, e.g. further analyses or test series, a great part of the work being already done.

Publications internes Litp 1996 / Litp research reports 1996