Abstract Heap Relations for a Compositional Shape Analysis

Hugo Illous 1, 2
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
2 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria de Paris
Abstract : Static analyses aim at inferring semantic properties of programs. We distinguish two important classes of static analyses: state analyses and relational analyses. While state analyses aim at computing an over-approximation of reachable states of programs, re- lational analyses aim at computing functional properties over the input-output states of programs. Relational analyses offer several advantages, such as their ability to infer semantics properties more expressive compared to state analyses. Moreover, they offer the ability to make the analysis compositional, using input-output relations as summaries for procedures, which is an advantage for scalability. In the case of numeric programs, several analyses have been proposed that utilize relational numerical abstract domains to describe relations. On the other hand, designing abstractions for relations over input- output memory states and taking shapes into account is challenging. In this Thesis, we propose a set of novel logical connectives to describe such relations, which rely on sep- aration logic. This logic can express that certain memory areas are unchanged, freshly allocated, or freed, or that only part of the memory is modified (and how). Using these connectives, we build an abstract domain and design a compositional static analysis by abstract interpretation that over-approximates relations over memory states containing inductive structures. We implement this approach as a plug-in of the Frama-C ana- lyzer. We evaluate it on small programs written in C that manipulate singly linked lists and binary trees, but also on a bigger program that consists of a part of Emacs. The experimental results show that our approach allows to infer more expressive semantic properties than states analyses, from a logical point of view. It is also much faster on programs with an important number of function calls without losing precision.
Keywords : Analyse statique
Document type :
Theses
Complete list of metadatas

Cited literature [106 references]  Display  Hide  Download

https://hal.inria.fr/tel-02399767
Contributor : Xavier Rival <>
Submitted on : Monday, December 9, 2019 - 7:03:38 PM
Last modification on : Wednesday, January 8, 2020 - 1:34:20 AM

File

manuscript.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-02399767, version 1

Collections

Citation

Hugo Illous. Abstract Heap Relations for a Compositional Shape Analysis. Programming Languages [cs.PL]. Ecole Normale Supérieure, 2019. English. ⟨tel-02399767⟩

Share

Metrics

Record views

43

Files downloads

111