Modular Construction of Shape-Numeric Analyzers

Bor-Yuh Evan Chang 1 Xavier Rival 2, 3
2 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : The aim of static analysis is to infer invariants about programs that are precise enough to establish semantic properties, such as the absence of run-time errors. Broadly speaking, there are two major branches of static analysis for imperative programs. Pointer and shape analyses focus on inferring properties of pointers, dynamically-allocated memory, and recursive data structures, while numeric analyses seek to derive invariants on numeric values. Although simultaneous inference of shape-numeric invariants is often needed, this case is especially challenging and is not particularly well explored. Notably, simultaneous shape-numeric inference raises complex issues in the design of the static analyzer itself. In this paper, we study the construction of such shape-numeric, static analyzers. We set up an abstract interpretation framework that allows us to reason about simultaneous shape-numeric properties by combining shape and numeric abstractions into a modular, expressive abstract domain. Such a modular structure is highly desirable to make its formalization and implementation easier to do and get correct. To achieve this, we choose a concrete semantics that can be abstracted step-by-step, while preserving a high level of expressiveness. The structure of abstract operations (i.e., transfer, join, and comparison) follows the structure of this semantics. The advantage of this construction is to divide the analyzer in modules and functors that implement abstractions of distinct features.
Type de document :
Communication dans un congrès
Anindya Banerjee and Olivier Danvy and Kyung-Goo Doh and John Hatcliff. Festschrift for Dave Schmidt, Sep 2013, Manhattan, Kansas, United States. EPTCS, 129, 2013, Festschrift for Dave Schmidt
Liste complète des métadonnées

Littérature citée [37 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00926948
Contributeur : Xavier Rival <>
Soumis le : vendredi 10 janvier 2014 - 15:20:27
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : vendredi 11 avril 2014 - 00:15:08

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00926948, version 1

Collections

Citation

Bor-Yuh Evan Chang, Xavier Rival. Modular Construction of Shape-Numeric Analyzers. Anindya Banerjee and Olivier Danvy and Kyung-Goo Doh and John Hatcliff. Festschrift for Dave Schmidt, Sep 2013, Manhattan, Kansas, United States. EPTCS, 129, 2013, Festschrift for Dave Schmidt. 〈hal-00926948〉

Partager

Métriques

Consultations de la notice

199

Téléchargements de fichiers

65