Data containers, such as lists, arrays, trees, etc, raise challenges for program verification. In static analysis by abstract interpretation, one popular approach is summarization: multiple elements of a data structure are abstracted into a single one, favoring performance over precision. This technique is at the core of most container abstractions - from smashing to segmentation - of arrays, lists or algebraic data types. However, summarization approaches are unable to express relations between containers, even when relational numerical abstract domains are used. Our work introduces DelExp, a new domain able to express relations between summarized variables. DelExp can state that the content of a data structure is included in the content of another data structure, up to a given transformation. DelExp is language-agnostic, modular in the abstraction chosen for any other types (integers, strings, functions, etc.), and can be seamlessly combined with existing container abstractions. We show how DelExp allows us to infer precise summaries for compositional analyses of container-manipulating functions in a pure functional language. We present extensions to DelExp supporting polymorphism and higher-order transformations. Our implementation of DelExp within the MOPSA static analysis platform confirms that DelExp works out of the box with pre-existing container abstractions. Our evaluation targets both Python programs manipulating lists and relational summary generation for OCaml functions handling algebraic data types.

Abstract Tools that manipulate OCaml code can sometimes fail even on correct programs. Identifying and understanding the cause of the error usually involves manually reducing the size of the program, so as to obtain a shorter program causing the same error—a long, sometimes complex and rarely interesting task. Our work consists in automating this task using a minimiser, or delta-debugger. To do so, we propose a list of unitary heuristics, i.e. small-scale reductions, applied through a dichotomy-based state-of-the-art algorithm. These proposals are implemented in the free Chamelon tool. Although designed to assist the development of an OCaml compiler, Chamelon can be adapted to all kinds of projects that manipulate OCaml code. It can analyse multifile projects and efficiently minimise real-world programs, reducing their size by one to several orders of magnitude. It is currently used to assist the industrial development of the flambda2 optimising compiler.