Skip to Main content Skip to Navigation
Journal articles

A relational shape abstract domain

Hugo Illous 1 Matthieu Lemerre 1 Xavier Rival 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, relational analyses aim at computing functional properties over the input-output states of programs. Several advantages of relational analyses are their ability to analyze incomplete programs, such as libraries or classes, but also to make the analysis modular, using input-output relations as composable summaries for procedures. In the case of numerical 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 paper, we propose a set of novel logical connectives to describe such relations, which are inspired by separation logic. This logic can express that certain memory areas are unchanged, freshly allocated, or freed, or that only part of the memory was modified. Using these connectives, we build an abstract domain and design a static analysis that over-approximates relations over memory states containing inductive structures. We implement this analysis and report on the analysis of basic libraries of programs manipulating lists and trees.
Complete list of metadata

https://hal-cea.archives-ouvertes.fr/cea-03218896
Contributor : Matthieu Lemerre <>
Submitted on : Thursday, May 6, 2021 - 12:57:07 AM
Last modification on : Monday, May 17, 2021 - 9:30:37 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Hugo Illous, Matthieu Lemerre, Xavier Rival. A relational shape abstract domain. Formal Methods in System Design, Springer Verlag, 2020, ⟨10.1007/s10703-021-00366-4⟩. ⟨cea-03218896⟩

Share

Metrics

Record views

32

Files downloads

23