Jerome Feret

Antoine Mine

Cezara Dragoi

Vincent Danos

Caterina Urban

Thibault Suzanne

Mehdi Bouaziz

Ferdinanda Camporesi

Lý Kim Quyên

Stan Le Cornec

Nicolas Behr

Andrea Beica

Marc Chevalier

sein de l'analyseur MemCAD et nous en avons évaluées l'impact sur l'analyse de bibliothèques existantes écrites en C et implémentant différentes structures de données, incluant des listes doublement chaînées, des arbres rouge-noir, des arbres AVL et des arbres "splay". Nos résultats expérimentaux montrent que notre approche est à même de contrôler la taille des disjonctions à des fins de performance sans pour autant nuire à la précision de l'analyse.

i Résumé L'analyse statique des programmes permet de calculer automatiquement des propriétés sémantiques valides pour toutes les exécutions. En particulier, dans le cas des programmes manipulant des structures de données complexes en mémoire, l'analyse statique peut inférer des invariants utiles pour prouver la sûreté des accès à la mémoire ou la préservation d'invariants structurels. Beaucoup d'analyses de ce type manipulent des états mémoires abstraits représentés par des conjonctions en logique de séparation dont les prédicats de base décrivent des blocs de mémoire atomiques ou bien résument des régions non-bornées de la mémoire telles que des listes ou des arbres. De telles analyses utilisent souvent des disjonctions finies d'états mémoires abstraits afin de mieux capturer leurs dissimilarités. Les analyses existantes permettent de raisonner localement sur les zones mémoires mais présentent les inconvénients suivants:

(1) Les prédicats inductifs ne sont pas assez expressifs pour décrire précisément toutes les structures de données dynamiques, du fait de la présence de pointeurs vers des parties arbitraires (i.e., non-locales) de ces structures;

(2) Les opérations abstraites correspondant à des accès en lecture ou en écriture sur ces prédicats inductifs reposent sur une opération matérialisant les cellules mémoires correspondantes. Cette opération de matérialisation crée en général de nouvelles disjonctions, ce qui nuit à l'impératif d'efficacité. Hélas, les prédicats exprimant des contraintes de structure locale ne sont pas suffisants pour déterminer de façon adéquate les ensembles de disjonctions devant être fusionnés, ni pour définir les opérations d'union et d'élargissement d'états abstraits. Cette thèse est consacrée à l'étude et la mise au point de prédicats en logique de séparation permettant de décrire des structures de données dynamiques, ainsi que des opérations abstraites afférentes. Nous portons une attention particulière aux opérations d'union et d'élargissement d'états abstraits. Nous proposons une méthode pratique permettant de raisonner globalement sur ces états mémoires au sein des méthodes existantes d'analyse de propriétés structurelles et autorisant la fusion précise et efficace de disjonctions.

Nous proposons et implémentons une abstraction structurelle basée sur les variables d'ensembles qui lorsque elle est utilisée conjointement avec les prédicats inductifs permet la spécification et l'analyse de propriétés structurelles globales. Nous avons utilisé ce domaine abstrait afin d'analyser une famille de programmes manipulant des graphes représentés par liste d'adjacence.

Nous proposons un critère sémantique permettant de fusionner les états mémoires abstraits similaires en se basant sur leur silhouette, cette dernière représentant certaines propriétés structurelles globales vérifiées par l'état correspondant. Les silhouettes s'appliquent non seulement à la fusion de termes dans les disjonctions d'états mémoires mais également à l'affaiblissement de conjonctions de prédicats de logique de séparation en prédicats inductifs. Ces contributions nous permettent de définir des opérateurs d'union et d'élargissement visant à préserver les disjonctions requises pour que l'analyse se termine avec succès. Nous avons implémenté ces contributions au

Introduction

This chapter presents the main approaches to shape analysis and introduces the motivations of this thesis. First, the benefits and problems brought by pointers and dynamic data structures in programming languages and critical software are introduced in Section 1.1 and Section 1.2 respectively. Then, in Section 1.3, several methods that can reduce software problems or prove the absence of some software problems are presented. Section 1.4 mainly focuses on static analyses targeting memory properties, including pointer analyses and shape analyses. Finally, Section 1.5 and Section 1.6 discuss some open challenges in shape analysis and the contributions of the thesis.

Dynamic Memory Allocation and Dynamic Data Structures

Pointers and dynamic data structures are often found in low-level operating system codes, device drivers and other safety critical computer controlled systems in transportation and communication. The main reason is that pointers and dynamic data structures allow efficient memory management and access. Let us begin by reviewing common uses of pointers and dynamic data structures.

Pointers. Pointers are values denoting the address of a memory cell in programming languages, like C, C++ and Java. Therefore, pointers are often used as references to program variables, dynamically allocated memory blocks, and functions. As an example, the following C program defines an integer variable i and an integer pointer p that points-to i. A pointer can be dereferenced to read the value of the memory it refers to and also to write into the memory. For example, the program statement at line 3 is equivalent to the statement i = i + 1 as dereferencing p ( that is *p ) on the right side of the assignment will produce the value of i, while, on the left side, the dereference will produce the address &i.

Chapter 1. Introduction

Pointers contribute to the expressive power of a programming language. For example, in C, pointers enable unbounded data structures and call-by-reference. In C, functions use call-byvalue to pass arguments. A function call works on a copy of the input parameters, which means that any changes to the parameters inside the function have no effect on the original arguments. However, if a function uses pointers as parameters, the function can then modify the structure pointed to by the parameters through dereferencing pointers.

Moreover, pointers can also improve the performance of a programming language, since copying a pointer is often much cheaper both in time and space than copying the data it refers to.

Dynamic Memory Allocation. Dynamic memory management is a key use of pointers. In C and C++, programmers can dynamically allocate memory on the heap when necessary by using some library functions, like malloc in C, and new in C++. Dynamically allocated memory can only be read and written through pointers. For example, the following C program uses malloc() to dynamically allocate a memory area able to hold 10 integers and uses the pointer p referring to the beginning of the memory area. If the allocation fails (for instance, when not enough memory is available), malloc will return NULL. Therefore, the program performs a null check on the pointer p at line 3. If the allocation succeeds, the program then initializes the allocated area with 0 by relying on pointer arithmetic and pointer dereferences at line 5.

1 i n t * p = ( i n t *) malloc (10 * s i z e o f ( i n t ) ) ; 2 i n t i = 0; 3 i f ( p == NULL ) return ; 4 while (i <10) { 5 *( p + i ) = 0; 6 i ++; 7 } Dynamic Data Structures. In many programs, pointers and dynamic memory allocation are used to implement dynamic data structures. Dynamic data structures refer to organizations of data elements in memory where data elements, called nodes, are stored in dynamically allocated memory blocks and are linked by pointers. Dynamic data structures play a big role in programming languages like C, C++ and Java, because they allow programmers to dynamically adjust the memory consumption according to the data size. This way, many dynamic data structures support very efficient insertion, deletion and search operations.

Linked lists and binary search trees are commonly used dynamic data structures. Linked lists store data nodes in a linear order. Singly linked lists are the most simple list data structures, where each node is made up of some data fields and a pointer to the next node in the sequence. For example, the following memory block contains a singly linked list pointed to by variable l. can easily support node insertion and deletion operations with O(1) time. However, a singly linked list can only be searched or traversed in one direction, from head to tail. In order to allow for more efficient algorithms, additional pointers are often added to list nodes. For instance, in doubly linked lists, each node contains two pointers: a pointer to the next node and a pointer to the previous node. In circular linked lists, the next pointer of the last list node points back to the head of the list instead of being null. Moreover, lists are often used to implement other more complex data structures, like, stacks, queues, dynamic arrays, adjacency lists and skip lists. However, one of the primary disadvantages of linked lists is that searching for a list element usually takes O(n) time. Binary search trees overcome this problem. A binary search tree node is usually composed of two pointers (respectively for the left child node and the right child node) and a data field. The data of the left sub-tree must be smaller than the current node, and that of the right sub-tree must be greater than the current node. As an example, Figure 1.1 shows a memory area containing a binary search tree, whose root is pointed to by pointer r. Search, insertion and deletion operations of binary search trees take O(log n) time on average (where n is the number of tree nodes). However, in the worst case when the tree is not well balanced, these operations take O(n) time complexity. To further improve the worst case efficiency of binary search trees, self-balancing binary search trees, like red-black trees and AVL trees, and self-adjusting binary search trees, like splay trees, have been proposed.

Overall, compared to static data structures, like arrays, dynamic data structures are more flexible. Dynamic data structures support more efficient addition, deletion and search operations and allow more efficient use of memory.

Software Problems Involving Pointers and Dynamic Data Structures

On the one hand, pointers and dynamic data structures are useful as they allow flexible and efficient memory management and data organization. On the other hand, pointers and dynamic data structures may be dangerous as they can cause very severe software problems, including memory safety problems, memory leaks, and security issues. Let us review these problems.

Memory Safety Problems

Basic memory safety problems. Memory safety problems are due to memory access errors, including dereferencing null, dangling or uninitialized pointers, and illegal freeing of already freed or non dynamically allocated memory areas. As an example, the following C program may lead to a null dereference error when the function malloc returns NULL. This may happen when there is no available memory.

1 i n t * p = ( i n t *) malloc ( s i z e o f ( i n t ) ) ; 2 * p = 1;

Memory safety problems often cause runtime errors. In most programming languages, including C, dereferencing null pointers will make the program crash. Dereferencing dangling pointers may cause unpredictable behaviors, such as the corruption of unrelated data, a segmentation fault or an unexpected output, because dangling pointers refer to memory which has already been deallocated and the memory may now contain completely different data. In C, the default value of a pointer is undefined. Therefore, dereferencing an uninitialized pointer can also lead to erratic program behaviors. Moreover, only dynamically allocated memory can be freed through pointers. Double freeing of a dynamically allocated memory block or freeing of a non dynamically allocated memory region will cause a segmentation fault and also result in a crash of the program. Data structure preservation. However, finding memory safety problems or proving certain memory safety properties of programs that manipulate dynamic data structures is often challenging because pointers are used as links in dynamic data structures. Memory safety properties of such programs rely on well formed dynamic data structures.

Let us consider the C program in Figure 1.2 as an example. The program defines a singly linked list type list, where each list element contains a data field that stores an integer pointer and a next pointer. The function list_min_remove takes a list head pointer hd as an input parameter and aims to remove the list element whose data field points to the minimum integer from the list. It first searches for the minimum list element using the while loop from line 9 to line 15. Pointers min, pre_min and c respectively store the minimum list element, the previous element and a cursor. Then, it removes the minimum list element from the list (lines 16 to 19) and frees the memory.

However, executing the list_min_remove function may lead to dereferencing null, uninitialized or dangling pointers, and illegal freeing.

Null pointer dereference. If the input parameter hd is NULL, pointer c will be initialized to NULL at line 7. Then, the dereference c -> next at loop head (line 9) will lead to a null pointer dereference error. Even when hd is not NULL, null pointer dereference may still happen at line 10 where the program dereferences the data field of list elements (*(c -> next -> data) and *(min -> data)), when some data fields are equal to NULL.

Uninitialized pointer dereference. In function list_min_remove, pointer pre_min is declared at line 6, but only initialized inside the while loop. When the loop is not executed, pre_min will stay uninitialized, the default value of which could be arbitrary. Therefore, the uninitialized pointer pre_min may pass the null pointer checking at line 16 and lead to an uninitialized pointer dereference error at line 17.

Dangling pointer dereference and illegal freeing. At line 20, the function frees the integer memory cell pointed by min -> data. This is fine if we assume that min -> data points to a dynamically allocated memory cell and the memory cell is only referenced by pointer min->data, but might otherwise cause illegal freeing at line 20 or cause a dangling pointer dereference error in the execution of some following code.

Therefore, in order to prove that a call to list_min_remove does not lead to any memory safety issues, we need to prove that the input parameter points to a well formed and non-empty list. That is, the list has at least one node and the data field of all the list nodes point to dynamically allocated and mutually disjoint memory cells. In turn, this requires proving the data structures are preserved by the list manipulation functions, like the list_min_remove function.

Memory Leaks. A memory leak occurs when a dynamically allocated memory block becomes unreachable or is not released after use. It can be seen as a special memory safety problem. In C and C++, programmers can dynamically allocate a chunk of memory from the system to store data. Dynamically allocated memory can only be accessed through pointers. Therefore, programmers should always make sure that there is at least one pointer to any dynamically allocated memory block until it is freed. Otherwise, the memory block will become unreachable. Moreover, C and C++ do not have built in automatic garbage collection. Programmers are responsible for freeing dynamically allocated memory after using it, otherwise the program may consume much more memory than needed. Normally, unfreed dynamically allocated memory will be returned to the system when the program exits.

Memory leaks can be a major problem as computers and portable devices have a fixed amount of available memory. If a running software uses up all the available memory, any memory allocation operation will fail, which will cause all the processes trying to allocate more memory to terminate or crash. Typically, this can be solved by terminating the leaking software, so that the operating system can clean up the memory. However, this is not very satisfactory, especially for the kernels of operating systems and software in embedded devices and servers which may be left running for many years. Generally, memory leaks are likely to induce a failure of the operating system if they occur in the kernel. The same is true for embedded systems which have no sophisticated memory management. As a memory leak example, let us consider the C program in Figure 1.3. The alloc_list function aims to dynamically allocate a list of length 100 and returns either the head pointer of the list, or NULL when the allocation fails. Specifically, it declares two pointers hd and tmp respectively for the head of the already allocated list and a temporary pointer for the newly allocated element and uses a while loop to perform the allocation: each loop iteration allocates one list element at line 10 and sets it as the list head at lines 14 to 15. However, the execution of the alloc_list function may cause memory leaks. When the memory allocation at line 10 fails, the function directly returns void without freeing all the previously allocated list elements. After the function returns, all the memory blocks allocated inside the function will become unreachable, and thus, can no longer be freed until the program exits.

Security Problems

Memory safety problems may cause not only runtime errors but also serious security problems, such as information leaks and privilege escalation.

Dangling pointer dereference bugs have frequently become security holes and have been known as "use after free" vulnerabilities. After freeing the memory a pointer refers to, the pointer becomes a dangling pointer and should not be dereferenced again as the memory may now contain completely different data. If the memory is used by higher privilege users or applications, writing or reading through a dangling pointer may cause privilege escalation. If the memory is reallocated by attackers and used to store attacker-controlled data, a dangling pointer dereference may cause the execution flow of the program to be controlled by attackercontrolled data. Moreover, if the dangling pointer is a function pointer, some malicious code written by attackers may be called.

A famous example of "use after free" vulnerability is CVE-2012-4969 [oM12], a zero-day Internet Explorer vulnerability, which was found to be exploited in-the-wild in September 2012. The main reason for the vulnerability was due to an incorrect reference count of an object which allowed the attacker to free it while it was in-use. Another example of a use-afterfree vulnerability was CVE-2012-4792 [oM13] exploited in-the-wild in December 2012. This vulnerability was also due to an incorrect reference count of an object, which caused a dangling pointer dereference after the object was freed.

Apart from dangling pointer vulnerability, null pointer dereferencing can also be a potential security problem. For example, if a security check program contains a null pointer dereference bug, it may allow the attacker to bypass security checks or reveal valuable debugging information that can be used in subsequent attacks.

Improving Software Quality Against Memory problems

As memory related software problems can often have serious consequences, it is an important task to improve software quality against memory problems.

Systematic Software Development

Software engineering is an attempt to reduce software problems by following a systematic approach to the development of software. According to the software engineering approach, detailed software requirements specifications and design specifications should be established in order to guide the developers towards its implementation. Some specific software development guidelines are used for critical software developments. For instance, in order to improve code safety, security, portability and reliability in embedded systems developments, a set of software development guidelines for the C programming language, MISRA C, was drawn up by Motor Industry Software Reliability Association. Nowadays, MISRA C has been widely followed by developers in automotive, telecom, medical devices, and railway systems. As another example, all the commercial software-based aeronautics follow the DO-178C rules. Specifically, DO-178C specifies the software safety level by examining the effects of a failure in the system and requires all software that commands, controls, and monitors safety-critical functions to be certified with respect to its level of criticality.

However, these approaches cannot prevent all bugs in programs. Firstly, programmers are humans and we know that humans can make mistakes. Secondly, critical systems are nowadays quite complex and have millions of lines of code. Code size is the worst enemy of software: as the code size grows, the number of bugs also increases. According to the book [START_REF] Mcconnell | Code complete: a practical handbook of software construction[END_REF], on average in industry, "there are about 15 -50 errors per 1000 lines of delivered code". Moreover, software guidelines are written in human languages and are verified manually. Human inspection is not always reliable.

Testing and Code Reviewing

Testing and code reviewing are important steps in software development. Software testing relies on executing software with a set of designed inputs to find software bugs. Code reviewing takes the form of a systematic examination of software source code by programmers. However, testing and code reviewing cannot identify all software problems. A large software system often has a huge number of branches and loops. Therefore, testing cannot cover all possible executions of branches and any number of loop iterations of large software systems. Besides, testing cannot cover all the possible inputs as software may have a huge of or even infinite number of inputs. For example, we cannot test on all the inputs of a program which takes any length of singly linked lists as parameters. Moreover, memory errors can be very difficult to discover by testing. For certain memory errors, there is often a long delay from the point when a memory error occurs to the point when the program crashes or produces invalid outputs, e.g. memory leaks. Memory errors may also be hard to reproduce, e.g. memory errors due to dangling pointer dereferences or memory errors with intermittent symptoms.

Code reviewing may find some serious memory errors. However, human inspection is not reliable in general.

Both testing and code reviews are very time consuming and expensive. More importantly, they cannot provide a formal guarantee of the absence of program errors and cannot establish that a software program satisfies certain properties under certain conditions.

Formal Verification

Formal verification aims to formally prove that a program is correct with respect to a specification which could state either safety properties or functional properties. One example of a safety specification could be that a program does not contain null pointers and dangling pointer dereference errors. A functional specification could be that a program preserves a list structure and outputs a sorted list for any input list.

In order to formally verify a program, we first need to define a formal language, like a logicbased language or a graphic-based language, which is expressive enough to express program semantics and program specifications. Then, it remains to prove that the program is correct with respect to the formal language. However, proving by hand is impossible for real programs which are huge in size.

In contrast, automated formal verification techniques which aim to automatically produce correctness proofs for programs have made tremendous progress in recent years. Proving the correctness of programs is an undecidable problem [START_REF] Henry | Classes of recursively enumerable sets and their decision problems[END_REF]: there does not exist a sound and complete algorithm which returns true if and only if the input program is correct. Therefore, designing an automatic sound and complete proof system is impossible. In general, formal verification techniques either rely on human intervention or drop the soundness or the completeness aspects in order to be fully-automated.

Model checking. Originally, model checking [START_REF] Emerson | Characterizing correctness properties of parallel programs using fixpoints[END_REF][START_REF] Clarke | Automatic verification of finite-state concurrent systems using temporal logic specifications[END_REF] aimed to automatically verify correctness properties of finite-state systems. Given a finite-state system, model checking proves that certain properties are satisfied by an exhaustive search of all possible states during all executions of the system. Applying model checking techniques to program verification will therefore face a state explosion problem due to the infinite state-space of programs. To overcome this problem, many model checking techniques have been proposed for handling infinite state systems, including bounded model checking and model checking based on abstraction. Bounded model checking only considers a finite subset of an infinite state space. Model checking based on abstraction relies on finding a finite abstraction of infinite states. For example, some model checking techniques use tree or forest automata to finitely represent potentially infinite memory states which contain unbounded dynamic data structures. As the problems are undecidable, most model checking work focuses on developing semi-automatic verification algorithms or decidable results for restricted cases. Automated theorem proving. Another way to prove program properties is to rely on proof assistants. A proof assistant, e.g. the Coq proof assistant1 or the PVS verification system2 , is a software tool to help develop formal proofs through collaboration between humans and theorem provers. A proof assistant is often composed of a specification language and a semiautomated theorem prover. In order to prove program properties, humans are supposed to write program specifications and guide the theorem prover to search for proofs. However, proverassisted approaches are not fully automated and human intervention may take a considerable amount of time. For hard problems, proficient users are required. Moreover, when the targeted program is slightly modified by programmers, the original proofs are hard to reuse. Usually, the whole proof process has to be run again.

Abstract interpretation. In the late 1970s, Patrick Cousot, together with Radhia Cousot, proposed abstract interpretation frameworks [CC77, CC92] that allow fully automatic static analyses to be designed. Specifically, an abstract interpretation framework provides a systematic set up that can be used by static analysis designers to derive computable and sound, but not necessarily complete, program analyses. That is, if the analysis returns true with respect to a specification, then the analyzed program satisfies the specification. However, not all the programs that satisfy the specification can be verified.

Chapter 1. Introduction

In order to design an abstract interpretation based static analysis, one should first identify the set of target programs and the program properties of interest, based on which, one can design an abstract domain. An abstract domain is a lattice over a set of abstract elements. Each abstract element represents a set of concrete elements (program states). For example, one may abstract the concrete values of integer program variables by their signs (+, -, 0). The relationship between abstract elements and concrete elements should be explicitly defined by a concretization function that maps each abstract element to a set of concrete elements.

In abstract interpretation, program semantics are described as abstract transfer functions that allow program semantics to be over-approximated at the abstract level. To compute abstract fix-points for loops and recursive procedures, abstract interpretation relies on a widening operator O that over-approximates any two abstractions and guarantees termination for any fix-point computation process.

Recently, abstract interpretation based static analysis tools have made dramatic progress. The Astrée analyzer [BCC + 03] is able to prove the absence of runtime numerical errors on avionic software [START_REF] Delmas | Astrée: from research to industry[END_REF] and spaceship control programs [BCC + 10]. Besides numerical analyses, abstract interpretation is also used in proving various memory properties of programs dealing with pointers and dynamic data structures. This will be discussed in the following section.

Pointer Analyses and Shape Analyses

As critical programs often manipulate pointers and complex dynamic data structures, pointer analyses and shape analyses, respectively aiming at discovering interesting pointer relations and structural properties are required. Section 1.4.1 presents pointer analyses. Then, Section 1.4.2 and Section 1.4.3 respectively introduce three-valued logic and separation logic based shape analyses. Finally, Section 1.4.4 briefly discusses some other graph-based and automata-based shape analyses.

Pointer analyses.

Pointer analyses [START_REF] Larus | Detecting conflicts between structure accesses[END_REF][START_REF] Choi | Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects[END_REF][START_REF] Andersen | Program Analysis and Specialization for the C Programming Language[END_REF] aim to build points-to relations (e.g., pointer "x points to y") or alias relations (e.g., pointers "x and y are aliased" i.e., they point to the same memory address) for each program point. The results of pointer analyses are often used in other more complex analyses, like escape analyses, construction of call graphs and aggressive compiler optimization.

In order to be more expressive, pointer analyses [JM82, CWZ90, HN90, HHN92] use finer memory models that are closer to the linked data structures manipulated by programs. Based on finer memory models, the analyses are able to establish relations between not only program variables but also memory locations reachable from program variables (e.g. memory location

x -> next -> next ). The analysis proposed in [START_REF] Deutsch | Interprocedural may-alias analysis for pointers: Beyond k -limiting[END_REF] further enriched pointer analyses with numerical linear equalities to track more subtle relations, such as x.(next) n = y.(next) n . To gain more precision, pointer analyses [HL11, WL95, MRR05] of flow-sensitivity (that considers the order of program statements), context-sensitivity (that considers the calling context of function calls), field-sensitivity (that treats all fields of a struct separately) and object-sensitivity (that

0 &l v 1 v 2 v 3
Figure 1.4: A concrete memory block with a singly linked list pointed to by variable l considers the objects on which a method is applied, to determine the set of objects pointed to by reference variables and reference object fields) have been well studied.

While being fast enough to analyze large pieces of code, pointer analyses are not expressive enough to capture complex data structure invariants and to verify memory safety, data structure preservation and other memory properties. Therefore, more expressive shape analyses which aim at inferring precise structural properties of memory states and verifying memory safety and complex functional properties of programs dealing with pointers and dynamic data structures have been proposed.

Three-valued Logic Based Shape Analyses

Three-valued logic based shape analysis [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF] (TVLA) is a powerful parametric framework for abstracting concrete memory states using Kleene's 3-valued logic [START_REF] Stephen | Introduction to metamathematics[END_REF]. Three-valued logic has three truth values (0, 1, 1/2), where 0 and 1 are definite values and 1/2 is an indefinite value. The figure below shows the information order on the truth values, where all definite values are smaller than the indefinite value, which means a definite value has more information than an indefinite value. 0 1/2 1 Abstract memory states. According to TVLA, a shape invariant can be characterized by a set of logical predicates describing pointer variables, types of data structure elements, connectivity properties and so on. As an example, the concrete memory shown in Figure 1.4.2 contains a singly linked list pointed to by pointer l. After naming the three list nodes v 1 , v 2 and v 3 , the concrete memory can be described as the logical formula:

l(v 1 ) ^next(v 1 , v 2 ) ^next(v 2 , v 3 ) ^next(v 3 , 0)
where, l(v 1 ) means pointer l points to node v 1 and next(v 1 , v 2 ) means the next field of v 1 refers to node v 2 . However, the set of concrete memory which contains a list is unbounded as the list could be of any length. In order to represent an unbounded set of concrete memory states, TVLA builds abstract states based on 3-valued logic formulas and summary nodes. As an example, the following abstract state abstracts all the concrete memory where l points to a singly linked list of at least length 1, including the concrete memory block shown in Figure 1.4.2.

l(v 1 ) = 1 ^next(v 1 , v 0 2 ) = 1/2 ^next(v 0 2 , v 0 2 ) = 1/2 where v 0 2 is a summary node
To concretize the abstract state into the concrete memory, we need to concretize the summary node v 0 2 into nodes v 2 and v 3 and concretize the indefinite value 1/2 into definite values. In order to perform assignment operations on abstract states, TVLA defines a "focus" operation that refines an abstract state into a set of abstract states, so that formulas related to the assignment only have definite values. In contrast to "focus", "blur" is an operation that merges nodes into summary nodes, so that abstract states can stay simple and finite.

TVLA is a general framework that can be instantiated in different ways by varying the predicates. It can also be parameterized in the model of concrete memory states for different levels of precision. For example, the fine-grained semantic model [START_REF] Kreiker | Shape analysis of low-level C with overlapping structures[END_REF] is able to precisely present overlapping data structures, while the coarse-grained semantic model leads to a lighter, but less precise analysis.

However, in the TVLA framework, 3-valued logic can not capture disjoint properties of memory cells naturally. This may cause the analysis to produce imprecise results. Moreover, updates on abstract states containing complex predicates, like connectivity predicates or cyclicity predicates, are complex and expensive to compute, which may result in a scalability problem.

Separation Logic Based Shape Analysis

Separation logic. Separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] was proposed for reasoning about memories as an extension of Hoare logic. The key feature of separation logic is the separating conjunction (⇤) which allows us to describe disjoint properties of memory cells. As an example, the concrete memory below contains two memory cells of variables x and l.

3 &l &x

The concrete memory can be described as the separation logic formula:

&x 7 ! 3 ⇤ &l 7 ! 2
where, &x 7 ! 3 destcribes the memory cell of variable x, &l 7 ! 2 describes the memory cell of l, and the separating conjunction ⇤ of the two predicates specifies that variables x and l are located in memory regions that do not overlap.

Separation logic supports the frame rule below, which plays an important role in enabling local reasoning.

φ P φ 0 φ ⇤ P φ 0 ⇤
The condition of the rule is that the execution of program P only reads or writes memory cells specified in memory state φ. It says that if executing program P from a memory state φ results in memory state φ 0 , then, executing the program in any bigger memory state φ ⇤ will not affect the additional part of the memory state. Based on this rule, we can thus only consider the local effect of a program statement on a minimal sub-memory and derive its global effect on the whole memory.

Chapter 1. Introduction 13 Abstract memory states. In addition to the separating conjunction, separation logic based shape analyses [BCC + 07, CDOY09, DOY06, CR08] often rely on user-provided or built-in inductive definitions to summarize unbounded data structures. An inductive definition is a precise description of a data structure. For example, we can define singly linked lists by induction:

↵ • list () ↵ = 0 _ ↵ 6 = 0 ^9β. ↵ 7 ! β ⇤ β • list
where, ↵ denotes the address of the list head. The definition says that either ↵ is equal to 0 (null) which indicates the list is empty, or the list contains at least one node described by a points-to predicate ↵ 7 ! β (↵ and β respectively describe the address and the value of the list node) and a list tail described by a recursive call β • list. The list tail is located at address β and located in a disjoint memory region with the list head node according to the separating conjunction ⇤.

An abstract memory state is thus defined as a separating conjunction combination of atomic heap predicates: abstract states:

m(2 M ! ) ::= p ⇤ . . . ⇤ p atomic predicates: p(2 P) ::= ↵ 7 ! β (points-to predicate) | ↵ • list (inductive predicate) | ↵ • tree (inductive predicate)
An atomic heap predicate is either a points-to predicate ↵ 7 ! β representing a single memory cell or an inductive predicate, e.g. ↵ • list, summarizing a memory region. As an example, the concrete memory shown in Figure 1.4.2 can be abstracted by the abstract state below:

9↵ 1 , . &l 7 ! ↵ 1 ⇤ ↵ 1 • list
where, &l is the symbolic address of variable l, ↵ 1 is the symbolic address of the list head node, and inductive predicate ↵ 1 • list summarizes the concrete list. Indeed, the abstract state describes an unbounded number of concrete memory regions, where the list is of any length. Inductive predicates in separation logic based shape analyses play a similar role to summary nodes in TVLA. However, inductive predicates follow a more local approach by using rule-based inductive definitions, while summary-nodes quantify global facts over sets of memory locations. Similarly to the blur and focus operations in TVLA, separation logic based analyses provide fold and unfold operations to generate and materialize inductive predicates respectively.

As the separating conjunction is able to express the disjoint properties of memory cells, strong updates and local reasoning can be performed on memory abstractions based on the separating conjunction. Studies on separation logic based shape analysis have successfully led to many shape analyzers, such as SpaceInvader [START_REF] Distefano | A local shape analysis based on separation logic[END_REF], Predator [START_REF] Dudka | Predator: A practical tool for checking manipulation of dynamic data structures using separation logic[END_REF], MemCAD [START_REF] Bor-Yuh | Modular construction of shape-numeric analyzers[END_REF] and Infer [CDD + 15].

Other Shape Analyses

Automata-based shape analyses. Another family of shape analyses [HHR + 11, HHL + 15] makes use of tree or forest automata to abstract memories with complex dynamic data structures.

Chapter 1. Introduction

Memory abstractions are usually composed of several tree automata, where each automaton represents a separate memory area. Similarly to inductive definitions, user-defined forest automata are used to encode recursive data structures and are used as alphabets in the abstractions to allow unbounded data structures to be represented. Program semantics are thus encoded as operations on automata.

Graph-based shape analyses. Some other shape analyses [START_REF] Ghiya | Is it a tree, a dag, or a cyclic graph? a shape analysis for heap-directed pointers in c[END_REF][START_REF] Marron | Efficient context-sensitive shape analysis with graph based heap models[END_REF] abstract memories as graphs and express program semantics as graph transformations. Specifically, in [START_REF] Ghiya | Is it a tree, a dag, or a cyclic graph? a shape analysis for heap-directed pointers in c[END_REF] memory areas are abstracted by considering the shape (tree, DAG, or cyclic graph) of the data structure accessible from heap directed pointers, and in [START_REF] Marron | Efficient context-sensitive shape analysis with graph based heap models[END_REF], graph nodes are used to represent memory regions and edges are used to represent pointers.

Outstanding Challenges in Shape Analysis

Shape analysis aims at inferring precise structural properties of memory states. Precision is always a major concern in shape analysis as an analysis can easily fail due to a lack of precision. On the other hand, in order to analyze real-world codes, shape analyses must be able to scale up.

As the separating conjunction make it possible to express the disjoint properties of memory cells, separation logic based shape analyses can reason about memory states locally and can perform strong updates on memory abstractions. Thus, the analyses can efficiently and precisely analyze some programs manipulating singly linked lists and some simple tree data structures.

However, real-world programs often manipulate more complex data structures, e.g. nested data structures, overlaid data structures and data structures with sharing, for which separation logic is not expressive enough to precisely describe the structural properties. To solve this problem, many ideas have been proposed, including various combinations of abstract domains [TCR14, TCR13, SR12, CR08] and abstractions based on a per-field separating conjunction [START_REF] Drăgoi | Local shape analysis for overlaid data structures[END_REF]. However, these approaches still have significant limitations when it comes to handling data structures with unstructured sharing. Section 1.5.1 will discuss the problem in detail and outline an approach that combines shape predicates with set predicates to express unstructured sharing.

Moreover, in order to precisely describe possibly dissimilar concrete memory states at a program point, shape analyses often rely on finite disjunctions of abstract memory states. Disjunctions should be kept small for scalability reasons, though precision often requires keeping additional case splits. In this context, deciding when and how to merge disjuncts and to replace them with precise over-approximations is critical both for precision and efficiency. Section 1.5.2 will set out the challenge in disjunction control and present some existing techniques in detail, as well as introducing the semantic-directed clumping of disjunctive abstract states.

Reasoning about Sharing in Separation Logic Based Shape Analysis

We say that a data structure is unshared if any node in the data structure is at most pointed to by one pointer. On the other hand, when any nodes in a data structure may be referred to by more than one pointer, the data structure is said to be shared. Singly-linked lists and binary search trees are unshared data structures, while more complex structures, such as doubly linked lists, directed-acyclic graphs (DAGs) and some data structures representing graphs in general, are shared data structures. Some shared data structures have regular sharing patterns. Such sharing patterns can be described by using a bounded number of constraints on nodes. For example, doubly-linked lists have structured sharing. In doubly linked lists, the sharing occurs because each node is pointed to by both its predecessor (except for the first node) and its successor (except for the last node). Therefore, doubly-linked lists can be described by the following inductive definition:

↵ • dll(δ) ::= (emp ^↵ = 0) _ (↵.prev 7 ! δ ⇤ ↵.next 7 ! β ⇤ β • dll(↵) ^↵ 6 = 0)
This definition says that ↵ points to a doubly-linked list if and only if it is either null (0) or a pointer to a list element: the prev field of the element points to δ and the next field of the element β points to a doubly-linked list such that the prev field of its first element should point back to ↵ itself. As in doubly linked lists, each node has exactly one predecessor, which can be specified as the parameter δ of the inductive definition. As shown in paper [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF], skip lists can also be defined following the same schema.

However, precisely and recursively summarizing data structures with unstructured sharing using the separating conjunction is much more challenging because in such data structures, a node may be pointed to by an unbounded number of pointers and the pointers could be anywhere in the structure.

In order to make the challenges more concrete, let us consider adjacency lists (a data structure for representing graphs) as an example. Figure 1.5 shows a type definition for adjacency lists: a graph is a list of nodes, each node has a list of edges, and each edge is a pointer to its destination node. Figure 1.6(b) shows an adjacency list representation of the graph shown in Figure 1.6(a), where each node i in the simple graph is described by a node located at address a i .

In order to prove memory safety or functional properties of algorithms manipulating the data structure with separation logic based shape analysis techniques, we need to recursively define this data structure using the separating conjunction. A natural approach is to exploit the list-of-lists inductive skeleton of adjacency lists. As shown in Figure 1.7: for the node at a 0 , its list of edges can be inductively summarized in the green region, while the other nodes, together with their edge lists in the graph, can be summarized in the purple region. What is implicit in this informal diagram is that, to achieve precision, these summarized regions must also capture complex, unstructured, cross pointer relations (i.e., the curving lines in Figure 1.6(b)).

To capture this unstructured sharing precisely, we observe that the correctness of the structure stems from the fact that each edge pointer points to an address in E = {a 0 , a 1 , a 2 , a 3 }. Thus, the absence of invalid edges can be captured by adjoining a set property to a conventional list predicate. We also need to ensure that all edge pointers point to nodes belonging to the set E of valid nodes in the graph for each node's edge list. To give an inductive definition for the list of nodes, we need to ensure that this list of nodes is consistent with the set E of valid nodes, and thus we require a second set variable F that captures the nodes summarized in the purple region. For the node list summary in Figure 1.7 (shown in purple), this variable F should be the set {a 1 , a 2 , a 3 }.

While we have outlined an approach to summarize adjacency lists using a combination of an inductive skeleton and relations over set-valued variables, using such summaries poses significant algorithmic challenges in abstract transfer functions, checking entailment of abstract states and computing over-approximations of abstract states.

Improving Scalability and Disjunction Control

Shape analyses, including TVLA and separation logic based shape analyses, rely on disjunctions of abstract states to capture precise structural properties of memory states. In separation logic m(2 M ! ) ::= p ⇤ . . . ⇤ p while, in TVLA, disjunctive abstract states are disjunctions of abstract states built on the conjunction ^. Disjunctions are necessary as programs can produce very different structures at a program point and it is often impossible to precisely abstract them all into a single abstract state either based on the conjunction ^or the separating conjunction ⇤. As an example, let us consider the program in Figure 1.8, which searches for the minimum and maximum list elements from any input singly linked list. At each program point of the while loop (line 9 to line 13), according to the input list, the program may produce a concrete memory state, where the pointer min points to a list element appearing in the list before the element pointed to by max, or a concrete memory state, where the pointer max points to a list element appearing in the list before the element pointed to by min. Figure 1.9 shows a pair of such memory states. Both memory states contain a list pointed to by the variable hd, and three "cursors" min, max, c pointing somewhere in that list. The only difference between these two memory states is the order of the cursors min, max. Shape analyses like [START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Chang | Shape analysis with structural invariant checkers[END_REF] 1.9(a) can be abstracted by:

9↵ 1 , ↵ 2 , ↵ 3 , ↵ 4 , &hd 7 ! ↵ 1 ⇤ &max 7 ! ↵ 2 ⇤ &min 7 ! ↵ 3 ⇤ &c 7 ! ↵ 4 ⇤ ↵ 1 • list ⇤= ↵ 2 • list ⇤ ↵ 2 • list ⇤= ↵ 3 • list ⇤ ↵ 3 • list ⇤= ↵ 4 • list ⇤ ↵ 4 • list
The left side of Figure 1.10 shows a graph representation of the abstract state. However, the abstract state cannot abstract the concrete memory shown in Figure 1.9(b) at the same time as min, max appear in the reverse order, which could be abstracted by the abstract state on the right side of Figure 1.10. Therefore, we need the disjunctive abstract state shown in Figure 1.10 to precisely abstract the two concrete memory states.

In practice, disjunctions are a huge challenge to static analyses. While the creation of new disjunctions occurs naturally when the analysis needs to reason about operations that read or write into summary predicates, letting the number of disjuncts grow makes the analysis slower and consumes more memory. However, getting rid of unnecessary disjuncts turns out to be a much harder task than introducing them. To clump a disjunctive abstract state d, an analysis needs:

1. to sort the disjuncts of d into sets of abstract states M 0 , . . . , M n , such that all abstract states in M i are sufficiently similar; 2. to compute for each set M i an abstract state m i that conservatively over-approximates all the elements of M i ; this weakening should infer how sets of predicates can be folded into summary predicates. Both steps are critical. The first step should determine the right set of disjuncts: leaving too many disjuncts would make it impossible to scale, whereas excessively reducing the size of the disjunction would prevent the weakening step from producing precise summaries.

Existing approaches all come with limitations and are often challenged by the first step (disjunct sorting). Canonicalization operators [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF] solve this problem by using a finite set of "canonical" abstract states, replacing each abstract state with a canonicalized version of it. Although the analysis may use an infinite domain, the precision of canonicalization outputs is limited by that of the finite set of canonical abstract states. The canonicalization operator of [START_REF] Distefano | A local shape analysis based on separation logic[END_REF] and the join operators of [CRN07, YLB + 08] utilize local rewriting rules based on the syntax of abstract states. They cannot reason about global shape properties, and thus may miss chances to clump some disjuncts. State partitioning [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF] and trace partitioning [START_REF] Rival | The trace partitioning abstract domain[END_REF][START_REF] Handjieva | Refining static analyses by trace-based partitioning using control flow[END_REF] provide frameworks for sensitivity in static analysis, but do not provide a general strategy to choose which disjunctions to preserve. We observe that static strategies based on the control flow structure of programs (conditions, loops, etc.) are likely to produce inadequate disjunct clumps as they ignore the shapes. On the other hand, disjunctive completion [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] authorizes any disjunction of abstract states (so that simplification is never required); however, it cannot deal with infinite sets of abstract predicates and is prohibitively costly when the set of abstract states is finite. Pruning disjunctions is thus a major challenge in many memory reasoning tools.

In this thesis, we observe that semantic properties of abstract states can help to characterize the clumping of disjuncts. For instance, the reason why the abstract states in Figure 1.10 cannot be clumped together lies in the order of the pointers min and max. Indeed, if we let be the relation that states that there is a link path from one pointer to another, then we get a pathbased abstraction hd min max c for the left abstract state and hd max min c for the right abstract state. Then, a "similarity" check can be performed on the two path-based abstractions, and, based on the checking result, the analysis can decide to not clump the two disjuncts in Figure 1.10.

We have described an approach that uses a path-based "silhouette" abstraction of the abstract states themselves to the clumping of disjunctive abstract states. In essence, this technique uses a form of lightweight canonicalization, but only as a guide to decide which disjuncts to clump, whereas the analysis computations (including the abstract join for clumping) all still take place in the initial, infinite lattice.

Outline and Contributions of the Thesis

This section presents an outline and the contributions of the thesis.

Chapter 2 provides some theoretical background of separation logic based shape analysis, including a simple imperative language and a basic memory abstract domain.

Chapters 4, 5, and 6 propose shape analysis for unstructured sharing: a shape analysis that tracks set properties to infer precise invariants of data structures with unstructured sharing.

• Chapter 4 formalizes memory abstractions that are parameterized by inductive definitions with set-valued parameters and set abstractions, where inductive definitions with set-valued parameters are used to summarize shared data structures and set abstractions are used to reason about relations over set variables.

• Chapter 5 introduces a general interface for set abstract domains and a formalization of a linear set domain used in our shape analysis.

• Chapter 6 proposes static analysis algorithms to infer invariants over data structures with unstructured sharing and then reports on a preliminary empirical evaluation of these algorithms implemented in the MemCAD analyzer.

Chapters 8, 9, 10 and 11 propose semantic-directed clumping of disjunctive abstract states: let silhouette abstractions of the abstract states guide the algorithms for clumping and weakening disjuncts.

• Chapter 8 sets up a path-based silhouette abstraction of abstract states to capture shape similarities and guide the weakening of abstract states.

• Chapter 9 uses silhouettes to guide the joining procedure of abstract memory states such that the procedure is more precise.

• Chapter 10 presents algorithms for the clumping and the widening of disjunctive abstract states based on silhouettes.

• Chapter 11 reports on the implementation of the silhouette-guided algorithms in the Mem-CAD analyzer and the efficiency assessment with the verification of several real-world C libraries that manipulate structures such as doubly-linked lists, red-black trees, AVL trees, and splay trees.

Finally, Chapter 12 concludes the thesis.

Chapter 2

Separation Logic Based Shape Analysis

This chapter serves as a formal introduction to separation logic based shape analysis. First, Section 2.1 sets out the formal syntax and semantics of a minimal core of C language. Section 2.2 presents some notions of abstract domains in the abstract interpretation framework. Then, Section 2.3 introduces a formal definition for separation logic based memory abstractions and Section 2.4 presents the abstract semantics of the program language. Finally, Section 2.5 sums up exhaustive signatures for the aforementioned abstract domain.

A Simple Imperative Language

The programs that are considered in this thesis are all written in the C language. For the sake of simplicity, in this section, we define a simple language that intends to establish a model for a fragment of the C language and a concrete denotational semantics for this language.

Syntax

Figure 2.1 presents the syntax of a simple imperative language that provides dynamic memory management and basic control instructions. We avoid types in the language and assume that any value is stored in a 4-byte long cell.

Program variables. We let X = {x, y, . . .} denote a fixed infinite set of program variables, though a given program manipulates only a finite number of variables. Variables must be declared using the variable declaration command shown in Figure 2.1 before being manipulated by programs.

L-values and r-values. In our programming language, expressions are of two kinds: left value expressions that correspond to memory addresses and right value expressions that correspond to values. Memory addresses a 2 V addr ranging from 1 to 2 32 -1 are also memory values v 2 V ranging from 0 to 2 32 -1. To follow the standard C notation, in the following, we present addresses as 0x followed by the hexadecimal representation of the addresses, e.g., 0x... A left value expression can be the address of a program variable x, the address l.f representing a left value l plus an offset f 2 F, or the address *l obtained by dereferencing a left value expression l. We note that the expression l.f corresponds to the field access operation of struct data in C. In the following, we let f 2 F denotes both numerical offset and field name.

Similarly, a right value expression can be an integer value n 2 N, the value of the memory cell located at address l, denoted by l, the address l of a memory cell, denoted by &l, or a value r ⊕ r obtained by applying a binary operator ⊕ to two sub-expressions.

Statements. As shown in Figure 2.1, a program p is a sequence of statements that can be of different kinds.

The variable declaration statement x declares a variable x by allocating a memory cell of size 4-byte for x.

The assignment statement l = r writes the value denoted by right value expression r into the memory cell at the address denoted by left value expression l.

The memory allocation statement l = malloc(n) dynamically allocates a memory block of n memory cells and writes the base address of the block into the memory cell at the address denoted by left value expression l.

The memory de-allocation statement free(l, n) de-allocates n memory cells starting at the base address denoted by l.

The assertion statement assert(r) crashes the execution if the value denoted by r is equal to 0.

The conditional branch statement if(r){p}else{p 0 } computes the value denoted by r and continues with the execution of p if the value of r is not equal to 0, or continues with the execution of p 0 otherwise.

The loop statement while(r){p} keeps running the program with p if the value of r is not equal to 0 and exits the loop when the value of r is equal to 0.

Concrete States

In order to define a concrete program semantics, we first need to define concrete memory states on which programs are operated.

Memory states. Intuitively, a memory state consists of two parts: an environment that relates symbolic addresses of program variables to their real addresses and a store that is made up of finite number of individual cells. However, an error may appear during the execution of a program, e.g., when a program attempts to read an invalid memory cell. Let ! denote an error state; we thus have the following definition: Definition 2.1 (Memory states). A memory state m 2 M ! is either an error state ! or a non-error state (", σ) 2 M made up of an environment " 2 E and a store σ 2 H:

(", σ) 2 M ::= E ⇥ H m 2 M ! ::= {!} ] M " 2 E ::= X & ! V addr σ 2 H ::= V addr ! V
We let X & = {&x, &y, . . .} denote the set of symbolic addresses of program variables. The environment " maps symbolic addresses of program variables into their real addresses in the store. The store σ is a partial function from memory addresses a 2 V addr to their values v 2 V.

We note that 0 is a null address. We write [ ] for an empty store, [a 1 7 ! v 1 , . . . , a k 7 ! v k ] for the store with exactly k allocated cells at addresses a 1 , . . . , a k and which contains values v 1 , . . . , v k respectively, σ 1 ] σ 2 for the "gluing" of the two stores σ 1 and σ 2 such that the intersection of the addresses of the cells of σ 1 with the addresses of the cells of σ 2 is empty, σ 1 -σ 2 for removing cells whose addresses are in dom(σ 2 ) from σ 1 , and σ[a 7 ! v] for substituting σ(a) by v.

In order to define a concrete program semantics that manipulates memory states, let us first define several primary operations over stores:

read 2 V addr ⇥ H ! V ] {!} write 2 V addr ⇥ V ⇥ H ! H ] {!} create 2 N ⇥ H ! V addr ⇥ H ] {0} delete 2 V addr ⇥ N ⇥ H ! H ] {!}
The formal characterizations of the operations are shown in Figure 2.1.2. Intuitively, read(a, σ) reads the value σ(a) of a memory cell at address a in the store σ. In the case where a is not a valid address, i.e., a 6 2 dom(σ), read(a, σ) returns a memory error !. Similarly, write(a, v, σ) writes value v into the cell at address a of the store σ and returns a memory error ! when Chapter 2. Separation Logic Based Shape Analysis read(a, σ) a is not a valid address. The functions create and delete are used to dynamically allocate and de-allocate memory cells respectively. Specifically, create(n, σ) attempts to allocate n continuous cells and adds them into the store σ. If the allocation succeeds, it returns the base address of the newly allocated block that contains n cells and the new store, and if the allocation fails to find enough space, it returns the null address 0. We note that this operation is nondeterministic as the location and the initial value of the newly allocated block depends on the implementation. Conversely, delete(a, n, σ) removes n continuous cells starting from address a in the store σ. It returns memory error ! if there exists an invalid address in the set of addresses {a, a + 4, . . . , a + 4(n -1)}.

::= ⇢ σ(a) if a 2 dom(σ) ! otherwise write(a, v, σ) ::= ⇢ σ[a 7 ! v] if a 2 dom(σ) ! otherwise create(n, σ) returns either (a, σ ] [a 7 ! v 1 , . . . , a + 4(n -1) 7 ! v n ]) such that a, . . . , a + 4(n -1) 2 V addr -dom(σ) or 0 delete(a, n, σ) ::= ⇢ σ -[a 7 ! v 1 , . . . , a + 4(n -1) 7 ! v n ] if a, . . . , a + 4(n -1) 2 dom(σ) ! otherwise
Limitations and discussion. For the sake of conciseness, we limit the complexity of our concrete memory model:

• We make no distinction between the stack region and the heap region. Thus, memory errors, such as illegal freeing of non-dynamically allocated memory blocks, do not show up in our memory model. However, our memory model can be easily extended to take these errors into account, for instance, one can augment a store σ with a set of dynamically allocated addresses or augment each address in the store with an attribute indicating a stack or heap cell.

• Our memory states are untyped. That is, we do not distinguish between pointer values and integers and assume all values, all addresses, and all memory cells are four bytes long. This can be extended by adding an environment that maps program variables to their types and a sizeof function that returns the size of any given type.

However, our memory model is rather low-level thereby allowing us to target at memory properties such as the absence of dereferencing of null pointers and dangling pointers, data structure preservation, and so on.

eval l JlK(!) = ! (!-strict) eval l JxK(", σ) = ⇢ "(x) if x 2 dom(") ^"(x) 2 dom(σ) ! otherwise eval l J*lK(", σ) = eval r JlK(", σ) eval l Jl.fK(", σ) = ⇢ eval l JlK(", σ) + f if eval l JlK(", σ) 6 = ! ! otherwise (a) Semantics of left value expressions eval l JlK eval r JrK(!) = ! (!-strict) eval r JnK(", σ) = n eval r J&lK(", σ) = eval l JlK(", σ) eval r Jr 1 ⊕ r 2 K(", σ) = J⊕K(eval r Jr 1 K(", σ), eval r Jr 2 K(", σ)) eval r JlK(", σ) = ⇢ read(eval l JlK(", σ), σ) if eval l JlK(", σ) 6 = ! ! otherwise (

Concrete Semantics

In this section, we define a denotational semantics of programs, which focuses on constructing all the effects of programs on concrete memory states.

Semantics of operators. The semantics J⊕K of an operator ⊕ (e.g., +, -) defined below usually denotes the mathematical meaning of the operator:

J⊕K 2 V ] {!} ⇥ V ] {!} ! V ] {!}
For example, J+K(2, 4) = 6. We note that, some inputs of an operator may lead to an error state !, e.g., J/K(2, 0) = !. Moreover, J⊕K is !-strict, i.e., J⊕K propagates the error state ! when the error state ! is an input.

Semantics of left and right value expressions. Figure 2.3 presents the formal definitions of the semantics of left and right value expressions. The semantics eval l JlK 2 M ! ! V addr ]{!} of a left value expression l is a !-strict function that propagates the error state ! 2 M ! and maps a non-error memory state (", σ) 2 M either to an address denoted by l in the given state (", σ) or to an error state !. Similarly, the semantics eval r JrK 2 M ! ! V ] {!} of a right value expression r is also a !-strict function that propagates the error state and maps a non-error memory state (", σ) 2 M either to a value denoted by r in the given state or to an error state !. The error state ! may appear both in mathematical operations and in store operations.

Denotational semantics. The denotational semantics JpK 2 P(M ! ) ! P(M ! ) of program statements is presented in Figure 2.4. Intuitively, in the denotational semantics, programs are described as functions that map sets of initial memory states to sets of final memory states at the end of the execution of the program. The semantics is defined in a standard way by

guardJrK(M) = {(", σ) | (", σ) 2 M ^eval r JrK(", σ) 6 2 {0, !}} [ {! | ! 2 M _ (", σ) 2 M, eval r JrK(", σ) = !}
Variable declaration:

JxK(M) = {! | ! 2 M _ 9(", σ) 2 M, x 2 dom(") _ 0 = create(1, σ)} [ {(" ] [x 7 ! a 1 ], σ 1 ) | (", σ) 2 M ^x 6 2 dom(") ^(a 1 , σ 1 ) = create(1, σ)} Assignment: Jl = rK(M) = {! | ! 2 M _ 9(", σ) 2 M, ! = eval l JlK(", σ) _ ! = eval r JrK(", σ)} [ {! | 9(", σ) 2 M, a = eval l JlK(", σ) ^v = eval r JrK(", σ) ^! = write(a, v, σ)} [ {(", σ 1 ) | (", σ) 2 M, a = eval l JlK(", σ) ^v = eval r JrK(", σ) ^σ1 = write(a, v, σ)} Allocation: Jl = malloc(n)K(M) = {! | ! 2 M _ 9(", σ) 2 M, ! = eval l JlK(", σ)} [ {! | 9(", σ) 2 M, a = eval l JlK(", σ) ^0 = create(n, σ) ^! = write(a, 0, σ)} [ {! | 9(", σ) 2 M, a = eval l JlK(", σ) ^(a 1 , σ 1 ) = create(n, σ) ^! = write(a, v 1 , σ 1 )} [ {(", σ 1 ) | 9(", σ) 2 M, a = eval l JlK(", σ) ^0 = create(n, σ) ^σ1 = write(a, 0, σ)} [ {(", σ 2 ) | (", σ) 2 M, a = eval l JlK(", σ) ^(a 1 , σ 1 ) = create(n, σ) ^σ2 = write(a, v 1 , σ 1 )}
De-allocation:

Jfree(l, n)K(M) = {! | ! 2 M _ 9(", σ) 2 M, ! = eval l JlK(", σ)} [ {! | 9(", σ) 2 M, a = eval l JlK(", σ) ^! = delete(a, n, σ)} [ {(", σ 1 ) | (", σ) 2 M, a = eval l JlK(", σ) ^σ1 = delete(a, n, σ)} Assertion: Jassert(r)K(M) = {! | ! 2 M _ 9(", σ) 2 M, ! = eval r JrK(", σ) _ 0 = eval r JrK(", σ)} [ {(", σ) | (", σ) 2 M, v = eval r JrK(", σ) ^v 6 = 0}
Conditional branch:

Jif(r){p 1 }else{p 2 }K(M) = Jp 1 K • guardJr 6 = 0K(M) [ Jp 2 K • guardJr == 0K(M)
Loop:

Jwhile(r){p}K(M) = guardJr == 0K(lfp ✓ λM 1 . M [ JpK • guardJr 6 = 0K(M 1 ))
Sequence:

Jp 1 ; p 2 K(M) = Jp 2 K • Jp 1 K(M)
Figure 2.4: Denotational semantics of programs induction over the syntax of programs. It relies on the store operations read, write, create and delete, and the semantics of left and right value expressions eval l JlK and eval r JrK. In order to handle control flow operations in branch statements and loop statements, it relies on a guardJrK operation that filters out memory states that do not satisfy the condition expression r:

guardJrK 2 P(M ! ) ! P(M ! )
Note that, as defined in Figure 2.4, all the program statements propagate the error state !, that is, for all p and for all M ✓ M ! ,

! 2 M =) ! 2 JpK(M)
In addition to that, the semantics of some statements on non-error states are discussed below.

The variable declaration statement, x, consists of creating a new cell for variable x for all the non-error states. If in a memory state (", σ), variable x is already declared, denoted as x 2 dom("), or the store allocation fails, denoted as 0 = create(1, σ), executing the statement will output the error state ! in the final states.

The assignment statement, l = r, is carried out on each non-error state (", σ) 2 M by evaluating the left-hand side l into an address a, evaluating the right-hand side r into a value v, and writing the value v into the cell at address a in the store σ. If one of the three steps fails, i.e., outputs the error state !, the execution of the assignment statement will also output the error state ! in the final states.

The allocation statement, l = malloc(n) first evaluates the left-hand side l into an address a on a non-error state (", σ) 2 M. If the evaluation process fails, it outputs the error state. Otherwise, it allocates a memory block of n memory cells in the store. When the allocation fails, i.e., returns a null address 0, it writes the null address 0 into the cell at address a. When the allocation succeeds, i.e., returns the base address a 1 of the newly allocated block and the new store σ 1 , it writes address a 1 into the cell at address a in the new store σ 1 .

The semantics for a loop statement, while(r){p}, is defined on the least fix-point, denoted as lfp ✓ λM 1 . M [ JpK • guardJr 6 = 0K(M 1 ), of the following function:

λM 1 . M [ JpK • guardJr 6 = 0K(M 1 )
Indeed, the function is monotone over the complete lattice (P(M ! ), ✓, [) as guardJrK and JpK are monotone. This ensures that the function always has a least fix-point. Intuitively, a loop invariant covers all the reachable states during the execution of the loop from a set of initial states.

The semantics of the other statements are all quite natural, and are thus not discussed in detail.

Extensions. The programming language presented in Figure 2.1 is a small fragment of the C language, which allows a more concise presentation of the thesis. In practice, we could also consider other features of the C language:

• C programs that contain other control statements (e.g., switch, break, goto, for) can be transformed into equivalent programs with only if and while statements.

Chapter 2. Separation Logic Based Shape Analysis

• The scopes of variables can be added into the environment in order to allow local variables to be defined in nested blocks.

• In order to support functions, we could add the call records into the environment.

• Since our language supports expressions of pointer dereference and field access, it can be easily extended to handle basic types (e.g., bool, int), pointer types, and structure types.

Abstract Interpretation

Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] is a theory that allows different program semantics to be compared by using abstractions. In this section, we recall the most basic notions of abstract interpretation, which are used in the following in order to design sound and automatic static analyzers to prove properties about programs. As shown in Section 2.1, the behavior of a program can be formalized as a function that maps sets of initial memory states into sets of final memory states. In order to abstract such behaviors, we need to design an abstract domain that includes a set of abstract states, abstract operations and some over-approximation of lattice operations.

Abstract states. An abstract state m 2 M ! describes a set of concrete states. The relationship between abstract and concrete states is explicitly given by a concretization function that maps each abstract state into a set of concrete states:

γ : M ! ! P(M ! )
where P(M ! ) is the power-set of concrete states. In addition, abstract states often include the bottom and top elements ?, > 2 M ! , which denote the empty and complete concrete sets:

γ(?) = ; γ(>) = M ! Example 2.1 (Interval abstractions). An interval abstraction m is a map from each program variable x 2 X to an interval abstraction [n 1 , n 2 ].
It abstracts away the concrete addresses of program variables and over-approximates the concrete value of program variables by intervals. The concretization function of interval abstractions is defined as:

γ(m) = {(", σ) | 8x 7 ! [n 1 , n 2 ] 2 m, n 1  σ • "(x)  n 2 }
Abstract operations. In order to describe manipulations of concrete states, abstract interpretation relies on abstract operations. Abstract operations correspond to concrete computations at the abstract level. Therefore, the abstract operations that an abstract domain should provide depend on the operations on the concrete elements. More precisely, for each concrete operation op : M ! ⇥ M ! ! M ! , the analysis should use a correspondence abstract operation op : M ! ⇥ M ! ! M ! . A sound abstract operation should over-approximate all the concrete behaviors of the concrete operation.

Definition 2.2 (Soundness of abstract operations). An abstract operation op

: M ! ⇥ M ! ! M ! is sound with respect to the concrete operation op : M ! ⇥ M ! ! M ! if and only if: 8m 1 , m 2 2 M ! , 8m 1 2 γ(m 1 ), m 2 2 γ(m 2 ), op(m 1 , m 2 ) 2 (γ • op)(m 1 , m 2 )
Example 2.2 (Abstract operations on the interval abstract domain). Corresponding to the addition + and subtractionoperations on concrete values of program variables, the interval abstract domain should define abstract operations + andon the intervals:

+([n 1 , n 2 ], [n 3 , n 4 ]) = [n 1 + n 3 , n 2 + n 4 ] -([n 1 , n 2 ], [n 3 , n 4 ]) = [n 1 + n 3 , n 2 + n 4 ]
Approximation of lattice operations. Besides basic abstract operations, the analysis also needs to use approximation of lattice operations: v M! for the entailment checking of abstract states, t M! for joining two abstract states, O M! for ensuring termination when computing abstract fix-points. These operators have to be sound in order to derive sound proofs of program properties.

Entailment checking operator v M! . In order to prove one abstract state can be overapproximated by another abstract state, the abstract domain needs to use an entailment checking operation v M! : M ! ⇥ M ! ! {true, false}. In the following, we simply write

m 1 v M! m 2 when v M! (m 1 , m 2 ) = true. Definition 2.3 (Soundness of entailment checking operator v M! ). The entailment checking operation v M! : M ! ⇥ M ! ! {true, false} is sound if and only if: 8m 1 , m 2 2 M ! , m 1 v M! m 2 =) γ(m 1 ) ✓ γ(m 2 )
Example 2.3 (A sound entailment checking operator on intervals).

[n 1 , n 2 ] v M! [n 3 , n 4 ] () n 1 ≥ n 3 ^n2  n 4
Joining operator t M! . When analyzing a program, the number of abstract states may grow exponentially due to conditional statements and abstract operations. In order to have analyses that are scalable and always terminate, abstract states may need to be merged during the analysis. The joining operator t M! : M ! ⇥ M ! ! M ! merges two abstract states and returns an over-approximation.

Definition 2.4 (Soundness of joining operator t M! ). The joining operator t

M! : M ! ⇥ M ! ! M ! is sound if and only if: 8m 1 , m 2 2 M ! , γ(m 1 ) ✓ γ(m 1 t M! m 2 ) ^γ(m 2 ) ✓ γ(m 1 t M! m 2 )
Chapter 2. Separation Logic Based Shape Analysis Example 2.4 (A sound joining operator on intervals).

[n 1 , n 2 ] t M! [n 3 , n 4 ] = [min(n 1 , n 3 ), max(n 2 , n 4 )]
Widening operator O M! . As shown in Figure 2.4, the concrete semantics of a loop while(r){p} on a set of concrete states M is defined as the least fix-point of the function λM 1 . M [ JpK • guardJr 6 = 0K(M 1 ). In practice, the fix-point can be reached when M n+1 ✓ M n with the following iterations:

( M 0 = M M n+1 = M n [ JpK • guardJr 6 = 0K(M n ) n 2 N
However, the sequences of iterates might be infinite. The same is true for the abstract iteration below in order to compute an abstract fix-point that over-approximates the concrete least fixpoint:

( m 0 = m m n+1 = m n t M! JpK • guardJr 6 = 0K(m n ) n 2 N
The abstract iteration starts from an abstract state m that over-approximates M (i.e., M ✓ γ M! (m)), and is performed on the abstract semantics JpK of the loop body and the abstract semantics guardJrK of loop condition. However, in order to design a static analysis that always terminates, the number of abstract iterates has to be finite. Therefore, a widening operator O M! : M ! ⇥ M ! ! M ! that joins abstract states and provides a convergence acceleration for the iteration process is necessary.

Definition 2.5 (Widening operator). A widening operator O

M! 2 M ! ⇥ M ! ! M !
should satisfy the two following properties for soundness and termination respectively:

1. 8m 1 , m 2 2 M ! , γ M! (m 1 ) ✓ γ M! (m 1 O M! m 2 ) ^γM! (m 2 ) ✓ γ M! (m 1 O M! m 2 ) 2. For any sequence (m n ) n2N , the sequence (m 0 n ) n2N defined below is ultimately stationary: ( m 0 0 = m 0 m 0 n+1 = m 0 n O M! m n+1 n 2 N Example 2.

(A widening operator of interval abstractions).

[

n 1 , n 2 ]O M! [n 3 , n 4 ] = [n 1  n 3 ?n 1 : -1, n 2 ≥ n 4 ?n 2 : +1]
With the widening operator O M! , we can thus have the following abstract iteration with widening:

(

m 0 = m m n+1 = m n O M! JpK • guardJr 6 = 0K(m n ) n 2 N
According to [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], the abstract iteration with widening is ultimately stationary and sound, i.e., it is able to compute a sound over-approximation of the concrete least fix-point in a finite number of iterates, which is the abstract post fix-point of the loop while(r){p} from the precondition m, denoted as

lfp v M! (λm 1 . mO M! JpK • guardJr 6 = 0K(m 1 )).
However, in practice, the widening operator O M! can lead to a huge loss in precision. In order to compute more precise loop invariants, static analyses often make use of the widening operator to accelerate the iteration convergence after several abstract iterates with the join operator t M! .

Forward analyses. An analysis based on forward abstract interpretation starts from an abstract pre-condition that takes into account all the possible initial states and aims to automatically compute an abstract post-condition that covers all the final reachable states.

Example 2.6 (An example of a forward analysis using interval abstractions). Let us consider the analysis of the simple program below with the abstract pre-condition i 7 ! [-1, +1] as an example.

1 i = 0; 2 while (i <10) { 3 i = i +1; 4 }
The abstract pre-condition states that variable i may be any integer value. Then, the assignment statement at line 1 writes 0 to i, which results in abstract state i 7 ! [0, 0]. Starting from the abstract state i 7 ! [0, 0], the analysis then needs to iterate on the while loop to compute an abstract fix-point. The iteration process is shown below: Iteration loop head loop end join or widen first:

i 7 ! [0, 0] i 7 ! [1, 1] i 7 ! [0, 0] t M! i 7 ! [1, 1] = i 7 ! [0, 1] second: i 7 ! [0, 1] i 7 ! [1, 2] i 7 ! [0, 1] t M! i 7 ! [1, 2] = i 7 ! [0, 2] third: i 7 ! [0, 2] i 7 ! [1, 3] i 7 ! [0, 2] O M! i 7 ! [1, 3] = i 7 ! [0, +1[ fourth: i 7 ! [0, +1[ i 7 ! [1, +1[ i 7 ! [0, +1[ O M! i 7 ! [1, +1[= i 7 ! [0, +1[
The first loop iteration increases the value of i by 1 at line 3, which results in abstract state i 7 ! [1, 1] at the end of the first loop iteration. Then, the analysis joins the two abstract states corresponding to the loop entry and to the end of the first iteration and gets abstract state i 7 ! [0, 1]. The second loop iteration starts from the join result i 7 ! [0, 1] and ends in abstract state i 7 ! [1, 2]. After joining the two abstract states i 7 ! [0, 1] and i 7 ! [1, 2], the analysis gets i 7 ! [0, 2]. From the third iteration, the analysis starts to widen the abstract states corresponding to the loop entry and to the end of the iteration. In both the third the fourth iterations, the analysis gets abstract state i 7 ! [0, +1[, thus the abstract iteration terminates and returns the abstract fix-point i 7 ! [0, +1[.

Chapter 2. Separation Logic Based Shape Analysis

Memory State Abstractions

This section and the next aim to introduce a memory abstract domain [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF] that is based on a fragment of separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. In particular, the memory abstractions and the concretization function are presented in this section. We note that other separation logic based shape analyses [BCC + 07, CDOY09, DOY06] all share similar principles.

Abstract values. To abstract concrete memory states, we first need to abstract concrete values by abstract values. An abstract value v 2 V is either a symbolic variable ↵ 2 V ↵ or a symbolic address of a program variable &x 2 X & . To concretize abstract values, we need a valuation function µ 2 V ! V that maps an abstract value v 2 V to a concrete value v 2 V. We let µ dX & denote the restriction of a valuation µ to symbolic addresses of program variables X & .

Abstract states. An abstract state m 2 M ! is either > (top), ? (bottom) or a pair (g, n) 2 G ⇥ N that is composed of an abstract shape graph g 2 G and a numerical abstraction n 2 N :

m 2 M ! ::= G ⇥ N ] {?, >}
Intuitively, an abstract shape graph g 2 G describes the structural properties of concrete memory states by using separating conjunction formulas parameterized by abstract values V, and thus, is concretized into a set of pairs made up of a concrete store σ 2 H and a valuation µ 2 V ! V of abstract values:

γ G : G ! P(H ⇥ (V ! V))
A numerical abstraction n 2 N abstracts the numerical properties of abstract values and is concretized into a set of valuations of abstract values:

γ N : N ! P(V ! V)
Further details of abstract shape graphs and numerical abstractions are discussed in the following.

Given the concretization of abstract shape graphs and numerical abstractions, we can thus define the concretization of abstract states γ M! : M ! ! P(M ! ) as follows:

γ M! (?) = ; γ M! (>) = M ! γ M! (g, n) = { (µ dX & , σ) | 9µ 2 γ N (n), (σ, µ) 2 γ G (g)}
Note that an abstract state is concretized into a set of concrete states, where a concrete state is either an error state ! or is a pair (", σ) made up of an environment " mapping symbolic addresses of program variables into their real addresses and a store σ. The bottom state ? is concretized into an empty set and the top state > stands for the complete set of concrete states. For each concrete state (", σ) 2 γ M! (g, n), there exists a valuation µ that is coherent with the environment " (i.e., " = µ dX & ), the abstract shape g and the numerical abstraction n, i.e., (σ, µ) 2 γ G (g) and µ 2 γ N (n), denoted as (σ, µ) ✏ (g, n).

Abstract shapes. An abstract shape g 2 G is a separating conjunction ⇤ of region predicates:

g (2 G) ::= p 1 ⇤ . . . ⇤ p n
Each region predicate p i 2 P describes a store that is disjoint from stores described by other region predicates. The concretization of an abstract shape can thus be defined as "gluing" disjoint stores, each of which concretizes a region predicate:

γ G (p 1 ⇤ . . . ⇤ p n ) = { (σ 1 ] . . . ] σ n , µ) | 81  i  n, (σ i , µ) 2 γ P (p i )}
A region predicate can be emp denoting an empty region, a points-to predicate (e.g., v 1 .f 7 ! v 2 ) denoting a single memory cell, an inductive predicate (e.g., v 2 •list) describing a store with an inductive data structure or a segment predicate (e.g., v 1 • list ⇤= v 2 • list) describing a fragment of an inductive data structure.

The empty predicate. The empty predicate emp denotes an empty store, and thus can be concretized into a set of pairs composed of an empty store and any valuation:

γ P (emp) = { ([ ], µ) | µ 2 V ! V}
In the following, we represent the emp predicate as an empty graph with only abstract values and no edges, such as the graph below with only two nodes representing abstract values:

v 1 v 2
Points-to predicates. A points-to predicate v 1 .f 7 ! v 2 abstracts a store with only a concrete cell, where given a valuation µ of abstract values v 1 and v 2 , the abstract address v 1 + f denotes the concrete address µ(v 1 ) + f in the store and the abstract value v 2 denotes the concrete value µ(v 2 ) of the cell. Formally, a points-to edge is concretized as follows:

γ P (v 1 .f 7 ! v 2 ) = { ([µ(v 1 ) + f 7 ! µ(v 2 )], µ) | v 1 , v 2 2 dom(µ)}
In the following, we represent below a points-to predicate v 1 .f 7 ! v 2 as an edge:

v 1 v 2 f
Moreover, the separating conjunction ⇤ of region predicates is represented in sub-graphs with disjoint edges. For example, the separating conjunction of the two points-to predicates v 1 .f 7 ! v 2 ⇤ v 2 .f 7 ! v 3 is represented as the following graph with two disjoint edges:

v 1 v 2 v 3 f f
Example 2.7 (An abstract shape with only points-to edges). Let us consider the abstract shape graph below which abstracts a memory block with a list pointed to by variable x:

&x ↵ 1 ↵ 2 ↵ 3 ↵ 4 ↵ 5 ↵ 6 ↵ 7 next d next d next d
The points-to edge starting at node &x abstracts the memory cell of variable x. The two points-to edges starting at node ↵ 1 respectively abstract the next field and the data field of the first list element. Similarly, the points-to edges starting at nodes ↵ 2 and ↵ 4 abstract the the following two list elements. The shape graph contains 7 points-to edges in total, and thus should be concretized into a set of pairs composed of a concrete store with exactly 7 memory cells and a valuation. One concrete example is the following pair (σ 1 , µ 1 ), where,

σ 1 is the graphical representation of [0x...010 7 ! 0x...040] ] [0x...040 + next 7 ! 0x...060] ] [0x...040 + d 7 ! 5] ] [0x...060 + next 7 ! 0x...080] ] [0x...060 + d 7 ! 9] ] [0x...080 + next 7 ! 0x0] ] [0x...060 + d 7 ! 18] : σ 1 2 H 5 9 0x0 18 0x...010 0x...040 0x...060 0x...080 µ 1 2 V ! V &x 7 ! 0x...010 ↵ 1 7 ! 0x...040 ↵ 3 7 ! 5 ↵ 2 7 ! 0x...060 ↵ 5 7 ! 9 ↵ 4 7 ! 0x...080 ↵ 7 7 ! 18 ↵ 6 7 ! 0x0
We note σ 1 contains a list of length 3 as the next pointer of the last list element is null. However, in the concretization, we could have different stores with different valuations, so that the store only contains a list fragment of length 3, such as the following one (σ 2 , µ 2 ):

σ 2 2 H 7 3 0x10 32 0x...020 0x...050 0x...070 0x...090 µ 2 2 V ! V &x 7 ! 0x...020 ↵ 1 7 ! 0x...050 ↵ 3 7 ! 7 ↵ 2 7 ! 0x...070 ↵ 5 7 ! 3 ↵ 4 7 ! 0x...090 ↵ 7 7 ! 32 ↵ 6 7 ! 0x...010
Inductive predicates. While separating shape graphs containing only points-to edges are expressive enough to abstract linked lists of a certain length, they cannot describe sets of memory states containing linked lists of any length. Intuitively, some data structures e.g., linked lists and binary trees, present a recursive pattern that can be summarized by an inductive definition.

For example, linked lists can be defined as:

↵ 0 • list ::= emp ^↵0 = 0 _ ↵ 0 .next 7 ! ↵ 1 ⇤ ↵ 0 .d 7 ! ↵ 2 ⇤ ↵ 1 • list ^↵ 6 = 0
This says that a list starting from address ↵ 0 is either empty (no list element) when ↵ 0 is null or has a list element at address ↵ 0 (which has a next field to ↵ 1 and a data field) and a list ↵ 1 • list starting from address ↵ 1 . Similarly, binary trees can be defined as:

↵ 0 • tree ::= emp ^↵0 = 0 _ ↵ 0 .l 7 ! ↵ 1 ⇤ ↵ 0 .r 7 ! ↵ 2 ⇤ ↵ 0 .d 7 ! ↵ 3 ⇤ ↵ 1 • tree ⇤ ↵ 2 • tree ^↵ 6 = 0
This says that a binary tree starting from address ↵ 0 is either empty (no tree element) when ↵ 0 is null or has a tree element at address ↵ 0 (which contains a left field to ↵ 1 , a right field to ↵ 2 and a data field), a left sub-tree ↵ 1 • tree starting from address ↵ 1 and a right sub-tree ↵ 2 • tree starting from address ↵ 2 .

Following inductive definitions, we can thus extend abstract shape graphs with inductive predicates that are parameterized by inductive definitions. For instance, linked lists rooted at abstract address ↵ can be abstracted by the inductive predicate ↵ • list which follows the list inductive definition. Similarly, binary trees rooted at abstract address β can be abstracted by the inductive predicate β • tree which follows the tree inductive definition.

In the following, we present inductive predicates as thick edges in graphs, for example, ↵•list is represented as:

↵ list

Example 2.8 (An abstract shape graph with inductive predicates). Given the list inductive definition, we can now abstract lists of any length that are pointed to by variable

x by the following abstract shape graph:

&x ↵ list
A few concrete examples that can be abstracted by the abstract shape graph are shown below:

• Variables x points to a list with one element: Segment predicates. Inductive definitions provide descriptions for complete data structures. However, in order to describe segments of data structures, we need segment definitions. Segment definitions can usually be derived fairly systematically from the initial inductive definitions. For example, the list segment definition ↵ 0 • list ⇤= ↵ 1 • list below is derived from the list inductive definition:

↵ 0 • list ⇤= ↵ 1 • list ::= emp ^↵0 = ↵ 1 _ ↵ 0 .next 7 ! ↵ 2 ⇤ ↵ 0 .d 7 ! ↵ 3 ⇤ ↵ 2 • list ⇤= ↵ 1 • list ^↵0 6 = ↵ 1
It describes a list starting at address ↵ 0 with a missing sub-list starting at address ↵ 1 , in other words by separating conjunction with a sub-list starting at address ↵ 1 , we can get a complete list starting at address ↵ 0 :

↵ 0 • list ⇤= ↵ 1 • list ⇤ ↵ 1 • list () ↵ 0 • list
Similarly, a binary tree segment definition ↵ 0 • tree ⇤= ↵ 1 • tree below is derived from the tree inductive definition:

↵ 0 • tree ⇤= ↵ 1 • tree ::= emp ^↵0 = ↵ 1 _ ↵ 0 .l 7 ! ↵ 2 ⇤ ↵ 0 .r 7 ! ↵ 3 ⇤ ↵ 0 .d 7 ! ↵ 4 ⇤ ↵ 2 • tree ⇤= ↵ 1 • tree ⇤ ↵ 3 • tree ^↵0 6 = ↵ 1 _ ↵ 0 .l 7 ! ↵ 2 ⇤ ↵ 0 .r 7 ! ↵ 3 ⇤ ↵ 0 .d 7 ! ↵ 4 ⇤ ↵ 3 • tree ⇤= ↵ 1 • tree ⇤ ↵ 2 • tree ^↵0 6 = ↵ 1
It describes a binary tree rooted at abstract address ↵ 0 with a missing sub-tree rooted at abstract address ↵ 1 , i.e., by separating conjunction with a sub-tree starting at address ↵ 1 , we can get a complete tree starting at address ↵ 0 :

↵ 0 • tree ⇤= ↵ 1 • tree ⇤ ↵ 1 • tree () ↵ 0 • tree
We note that, in the tree segment definition, the last two rules respectively describe cases where the missing sub-tree is in the left or the right branch of the tree node at ↵ 0 . Parameterized by segment definitions, we can thus extend abstract shape graphs with segment predicates to describe partial data strcutures. In the following, we present segment predicates as thick edges with a source node and a destination node in graphs. For example, the graphical representation of a tree segment ↵ • tree ⇤= β • tree is the following:

↵ β tree

When necessary (e.g., when we have different inductive predicates at both ends or have inductive predicates with parameters), we may also use the following graphical representation:

↵ β tree tree
Example 2.9 (An abstract shape graph with segment predicates). The abstract shape graph below abstracts memory states occurring in a classical list traversal algorithm, where, x is a pointer to the first list element and c is a "cursor" pointing to an element in the list:

&x &c ↵ β list list
A few concrete examples are shown in the following, where for simplicity we leave out memory cells of variables x and c:

• The list segment pointed to by variable x and c is empty:

. . . . . . . . . 0 . . .

x, c

• The list segment pointed to by variable x and c has one element: . . . . . . . . . 0 . . .

x c

• The list segment pointed to by variable x and c contains all the list elements except the last one:

. . . . . . . . . 0 . . .

x c

Further details about segment definitions and the concretization are discussed in Chapter 4.

Numerical abstractions. Numerical abstractions are used to abstract the numerical properties of abstract values, and are not the primary focus of the thesis. Therefore, in the thesis, Chapter 2. Separation Logic Based Shape Analysis we assume a numerical abstract domain N , which provides the following abstract operations:

abstract elements n 2 N concretization γ N : N ! P(V ! V) guard guard N : N ⇥ C V ! N assign assign N : N ⇥ V ⇥ R V ! N remove remove N : N ⇥ V ! N prove prove N : N ⇥ C V ! {true, false} rename rename N : N ⇥ (V ! P(V)) ! N abstract join t N : N ⇥ N ! N abstract widen O N : N ⇥ N ! N inclusion check v N : N ⇥ N ! {true, false}
We note that, guard N inputs a numerical abstraction n 2 N and a numerical constraint c V 2 C V , and returns a numerical abstraction which enforces c V ; assign N inputs a numerical abstraction n 2 N , an abstract variable v 2 V and a numerical expression r V 2 R V , and returns a numerical abstraction where abstract variable v has been assigned to a new meaning that is computed based on r V ; remove N inputs an abstraction n and an abstract variable v, and removes the abstract variable v from the abstraction n; prove N inputs an abstraction n and a numerical constraint c V , and returns true when it successfully establishes that n entails c V ; rename N inputs an abstraction n and a mapping from abstract variables in n to other abstract variables, and returns another abstraction which renames abstract variables in n according to the input mapping.

In practice, a suitable numerical domain is obtained as a reduced product of a numerical domain that only reasons about equalities and dis-equalities and any other numerical domains supported by the Apron library [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF], e.g., octagons [START_REF] Miné | The octagon abstract domain[END_REF], convex polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], intervals [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. In the following, for simplicity, we sometimes present numerical constraints directly than specific numerical abstractions, present guard N (n, c V ) as n ^cV and prove N (n, c V ) = true as n =) c V .

Disjunctive abstract states. In practice, shape analyses often rely on disjunctive abstract states

d 2 D of the form m 1 _ m 2 _ . . . _ m n (n 2 N).
The reason is that disjunctive abstract states d 2 D enable more precise abstraction of memory states than abstract states m 2 M ! . Indeed, in real-world program analyses, a single abstract state m 2 M ! often cannot capture precise structural properties of a set of concrete memory states. The concretization of disjunctive abstract states is defined as the union of the concretization of each abstract state:

γ D (m 1 _ m 2 _ . . . _ m n ) = γ M! (m 1 ) [ . . . [ γ M! (m n )

Abstract Semantics

In this section, we discuss the abstract semantics for the abstract states M ! introduced in the previous section, from which the abstract semantics for the disjunctive abstract states D can be

read(v, f, (g, n)) ::= ⇢ v 1 if 9g 1 , v 1 , g = g 1 ⇤ v.f 7 ! v 1 > otherwise write(v, f, v 1 , (g, n)) ::= ⇢ (g 1 ⇤ v.f 7 ! v 1 , n) if 9g 1 , v 2 , g = g 1 ⇤ v.f 7 ! v 2 > otherwise create(n, (g, n)) returns (↵, (g ⇤ ↵ 7 ! ↵ 1 ⇤ . . . ⇤ ↵ + 4(n -1) 7 ! ↵ n , n)), (↵, (g, n ^↵ = 0))
where ↵, ↵ 1 , . . . , ↵ n are fresh symbolic variables

delete(v, n, (g, n)) ::= ⇢ (g 1 , n) if 9g 1 , v 1 , . . . , v n , g = g 1 ⇤ v 7 ! v 1 ⇤ . . . ⇤ v + 4(n -1) 7 ! v n > otherwise

Abstract Store Operations

As presented in Figures 2.3 and 2.4, both the concrete program semantics and the expression evaluation involve the store operations shown in Figure 2.1.2. Therefore, in order to define the abstract semantics of program statements, we first need to provide abstract store operations.

For simplicity, we assume here that the memory regions that store operations operate on are fully described by points-to edges. The case where the memory cells involved are summarized in inductive or segment predicates will be dealt with unfolding operations of summary predicates in Section 2.4.2.

Corresponding to the concrete store operations read, write, create and delete, we have the following abstract store operations:

read 2 V ⇥ F ⇥ M ! ! V ] {>, ?} write 2 V ⇥ F ⇥ V ⇥ M ! ! M ! create 2 N ⇥ M ! ! (V ⇥ M ! ) 2 ] {?, >} delete 2 V ⇥ N ⇥ M ! ! M !
All the operations are ?-strict and >-strict, i.e. when the input abstract state is ?, the operation returns ? and the same for >. We note that the > abstract state accounts for crashes of program analysis either due to program errors or the loss of precision during the analysis. Further characterizations of the abstract operations are shown in Figure 2.5.

Intuitively, the abstract operation read(v, f, (g, n)) attempts to read the abstract value of the memory cell at abstract address v + f by searching a points-to edge starting at v.f, e.g. v.f 7 ! v 1 , in the abstract shape graph g and returns the abstract value v 1 . The abstract write(v, f, v 1 , (g, n)) operation attempts to write the abstract value v 1 into the memory cell at abstract address v + f. Therefore, it also searches for a points-to edge starting at v.f, e.g. v.f 7 ! v 2 , in the abstract shape graph g, and then updates the points-to edge to v.f 7 ! v 1 . Since the concrete operation create(n, σ) may succeed (returning the base address of the newly allocated block and the new store) or fail (returning the null address 0), to over-approximate such behaviors, the abstract operation create(n, (g, n)) returns a pair made up of (↵, (g ⇤ ↵ 7 ! ↵ 1 ⇤ . . . ⇤ ↵ + 4(n -1) 7 ! ↵ n , n)) and (↵, (g, n ^↵ = 0)). The first pair abstracts the concrete results of successful allocation by adding n continuous points-to edges starting at abstract addresses ↵ in the abstract shape graph g, while the second pair corresponds to the case of a failure by returning a symbolic variable ↵ that is constrained to be 0 in the numerical abstraction, denoted by n ^↵ = 0. Conversely, the abstract operation delete(v, n, (g, n)) removes n continuous points-to edges starting from abstract address v from the abstract shape graph. We note that the > abstract state may be returned during the store operations either due to imprecise abstract states or invalid store operations that cause the error state ! in the concrete part.

The abstract store operations are sound. For simplicity, we only present the soundness condition of abstract operation read and the soundness conditions of other operations are similar.

Condition 2.6 (Soundness of abstract read operation). The abstract operation read is sound if and only if the following property holds:

read(v, f, (g, n)) = v 1 =) 8(σ, µ) ✏ (g, n), read(µ(v), f, σ) 2 {µ(v 1 ) | (σ, µ) ✏ (g, n), }
Example 2.10 (Abstract store operations). Let us consider some abstract store operations on the abstract state below:

&x ↵ 1 ↵ 2 ↵ 3 ↵ 4 ↵ 5 next d next d list g : , n : ↵ 1 6 = 0 ^↵2 6 = 0 • read(↵ 1 , next, (g, n)) = ↵ 2 read(↵ 1 , d, (g, n)) = ↵ 3 • write(↵ 1 , next, ↵ 4 , (g, n)) = (g 1 , n 1 ) (the operation flips the next edge from node ↵ 1 in g to node ↵ 4 ): &x ↵ 1 ↵ 2 ↵ 3 ↵ 4 ↵ 5 next d next d list g 1 : , n 1 : ↵ 1 6 = 0 ^↵2 6 = 0 • create(2, (g, n)) = ((↵ 6 , (g 2 , n 2 )), (↵ 6 , (g 3 , n 3 ))) : &x ↵ 1 ↵ 2 ↵ 3 ↵ 4 ↵ 5 ↵ 6 ↵ 7 ↵ 8 next d next d list 0 4 g 2 : , n 2 : ↵ 1 6 = 0 ^↵2 6 = 0 &x ↵ 1 ↵ 2 ↵ 3 ↵ 4 ↵ 5 ↵ 6 next d next d list g 3 : , n 3 : ↵ 1 6 = 0 ^↵2 6 = 0 ^↵6 = 0 • delete(↵ 1 , 2, (g, n)) = (g 4 , n 4
) (the list tail can no longer be dereferenced from variable

x after the first list element has been removed):

&x ↵ 1 ↵ 2 ↵ 4 ↵ 5 next d list g 4 :
, n 4 : ↵ 1 6 = 0 ^↵2 6 = 0

Unfolding

In Section 2.4.1, we describe store operations based on the assumption that the memory regions that store operations operate on are fully described by points-to edges. However, store operations may involve memory cells that are summarized in inductive or segment predicates, for example the store operation read(↵, next, (g, n)) reads the abstract value at abstract address ↵ + next which is summarized in the inductive predicate ↵ • list:

&x ↵ list g : , n : ↵ 6 = 0
In such cases, in order to precisely support the store operations, the analysis needs to unfold summary predicates to expose points-to edges that store operations operate on.

Unfolding of inductive edges. The principle of unfolding an inductive predicate (e.g., ↵ • list) is to rewrite the inductive predicate by syntactically expanding all the rules of the inductive definition. Specifically, the unfolding operation unfold 2 V ⇥M ! ! D takes an abstract address v which is the origin of an inductive edge and memory cells from which need to be materialized, and an abstract state m 2 M ! . It outputs a disjunctive abstract state d = m 1 _ . . . _ m k 2 D, where each abstract state m i refines the abstract state m following a rule of the inductive definition. For simplicity, we present here only the soundness condition and an example of unfolding; the formal definition of unfolding is given in Chapter 6.

Condition 2.7 (Soundness of unfold). The unfolding operator unfold 2 V ⇥ M ! ! D is sound if and only if:

8m 2 M ! , unfold(v, m) = m 1 _ . . . _ m n =) γ M! (m) ✓ γ M! (m 1 ) [ . . . [ γ M! (m n ) Chapter 2.
&x ↵ 1 ↵ 2 ↵ 3 next d list g : , n : ↵ 1 6 = 0
As the list inductive definition contains two rules, one corresponding to the empty list and the other to the non-empty list, unfolding the inductive predicate ↵ 2 • list leads to the two abstract states below:

&x ↵ 1 ↵ 2 ↵ 3 next d g 1 : , n 1 : ↵ 1 6 = 0 ^↵2 = 0 &x ↵ 1 ↵ 2 ↵ 3 ↵ 4 ↵ 5 next d next d list g 2 : , n 2 : ↵ 1 6 = 0 ^↵2 6 = 0
The first abstract state (g 1 , n 1 ) corresponds to the empty list case, where the list predicate is replaced by an empty region, and the numerical abstraction n 1 guarantees that ↵ 2 is a null address. The second abstract state (g 2 , n 2 ) corresponds to the non-empty list case, where the list element at ↵ 2 is completely exposed and ↵ 2 is constrained to be non-null in

n 2 .
Unfolding of segment predicates. Segment predicates may need to be unfolded from either end, forward or backward. Forward unfolding is very useful for analyzing forward traversal programs of data structures, and conversely backward unfolding is for backward data structure traversal. Forward segment unfolding relies on rewriting the segment predicate by syntactically unfolding all the rules of the segment definition, which is similar to the unfolding of inductive predicates. while backward unfolding needs to first split a segment predicate into a separating conjunction of two segments and then performs forward unfolding at the split point. For example, backward unfolding at the previous node ↵ 4 of node ↵ 3 of the doubly linked list segment predicate

↵ 1 • dll(↵ 2 ) ⇤= ↵ 3 • dll(↵ 4
) needs to split the segment at node ↵ 4 (node ↵ 5 denotes the previous node of node ↵ 4 ):

↵ 1 ↵ 4 ↵ 3 dll(↵ 2 ) dll(↵ 5 ) dll(↵ 5 ) dll(↵ 4 )
The soundness condition of segment unfolding can be expressed in the same way as in Definition 2.7.

Example 2.12 (Unfolding a list segment predicate). Let us consider unfolding the list segment from node ↵ 1 to node ↵ 2 in the abstract state below:

&x ↵ 1 ↵ 2 list list g : , n : ↵ 1 6 = 0
According to the list segment definition, we get the two abstract states below:

&x ↵ 2 list g 1 :
,

n 1 : ↵ 1 6 = 0 ^↵1 = ↵ 2 &x ↵ 1 ↵ 3 ↵ 4 ↵ 2 next d list list g 2 :
,

n 2 : ↵ 1 6 = 0 ^↵1 6 = ↵ 2
The abstract state (g 1 , n 1 ) corresponds to the empty segment case, i.e., the segment is unfolded into an empty region and a constraint specifying ↵ 1 is equal to ↵ 2 is added into the numerical abstraction. In practice, the unfolding should then rename ↵ 2 into ↵ 1 everywhere in the graph and continue unfolding the inductive edge from node ↵ 1 to expose memory cells at ↵ 1 . The abstract state (g 2 , n 2 ) refines the list segment to a non-empty list segment, which exposes the memory cells at address ↵ 1 and imposes the constraint that ↵ 1 is not equal to ↵ 2 in n 2 .

Abstract Evaluation of Left and Right Value Expressions

As the definition of right value expressions (presented in Figure 2.1) involves arithmetic operators, therefore we first formalize the abstract semantics of arithmetic operators.

Abstract semantics of arithmetic operators. While the concrete semantics of arithmetic operators are quite simple, precisely defining the abstract semantics of the operators is fairly complex as they may involve both abstract shape graphs and numerical abstractions. Intuitively, the abstract operator J+K takes two abstract values v 1 2 V and v 2 2 V (additive operands), an abstract state (g, n) 2 M ! , and returns a pair made up of an abstract value v 3 and a new abstract state (g, guard N (n,

v 3 = v 1 +v 2 ))
where v 3 is enforced to the sum of v 1 and v 2 in the abstract state. Similarly, the abstract operator J==K also takes two abstract values v 1 and v 2 , an abstract state (g, n) 2 M ! , but returns two pairs made up of boolean values (true and false) and abstract states which respectively enforce equality and dis-equality condition on v 1 and v 2 . For precision, the equality (resp., dis-equality) condition should be not only enforced on the numerical abstraction n, denoted as guard N (n,

v 1 = v 2 )) (resp., guard N (n, v 1 6 = v 2 ))
), but also on the abstract shape graph g, denoted as guard G (g,

v 1 = v 2 ) (resp., guard G (g, v 1 6 = v 2 ).
We note that guard G 2 G ⇥ C V ! G is an operator of the abstract shape domain, which takes an abstract shape graph g 2 G, a numerical constraint c V 2 C V , and returns a new abstract shape graph where the numerical constraint has been enforced. Moreover, the abstract semantics J⊕K

J+K(v 1 , v 2 , (g, n)) = (v 3 , (g, guard N (n, v 3 = v 1 + v 2 ))) (v 3 is a fresh symbolic variable) J==K(v 1 , v 2 , (g, n)) = (true, (guard G (g, v 1 = v 2 ), guard N (n, v 1 = v 2 ))), and (false, (guard G (g, v 1 6 = v 2 ), guard N (n, v 1 6 = v 2 )))
Figure 2.6: Abstract arithmetic operators of any operator is a ?-strict and >-strict function that returns ? and > respectively when the input abstract state is ? and >.

For simplicity, we only present here the soundness condition of the abstract semantics of the additive operator and the soundness condition of other abstract arithmetic operators can be defined similarly.

Condition 2.8 (Soundness of abstract operator J+K). The abstract operation J+K is sound if and only if the following property holds:

J⊕K(v 1 , v 2 , (g, n)) = (v 3 , (g 1 , n 1 )) =) γ M! (g, n) ✓ γ M! (g 1 , n 1 ) ^{J+K(µ(v 1 ), µ(v 2 )) | (σ, µ) ✏ (g 1 , n 1 )} ✓ {µ(v 3 ) | (σ, µ) ✏ (g 1 , n 1 )}
Example 2.13 (Abstract equality test operation). Let us consider the abstract state (g, n) of Example 2.10. The abstract equality test operation J==K(↵ 1 , ↵ 2 , (g, n)) tests the equality of abstract value ↵ 1 and ↵ 2 in the abstract state (g, n). According to Figure 2.6, the abstract semantics relies on both the equality and dis-equality test operations on the shape graph (i.e., guard G (g, v 1 = v 2 ) and guard G (g, v 1 6 = v 2 )) and on the numerical abstraction (i.e., guard N (n, v 1 = v 2 ) and guard N (n, v 1 6 = v 2 )). Indeed, in the abstract graph g, the test operations can be done in an exact manner: the separating conjunction of the points-to edges ↵ 1 .next 7 ! ↵ 2 and ↵ 2 .next 7 ! ↵ 4 entails that ↵ 1 and ↵ 2 are addresses of disjoint memory cells, thus, they cannot be equal. Therefore, we can get that guard G (g,

v 1 = v 2 ) = ? and guard G (g, v 1 6 = v 2 ) = g. That is, J==K(↵ 1 , ↵ 2 , (g, n)) returns the two pairs (true, ?) and (false, (g, guard N (n, v 1 6 = v 2 ))).
Abstract evaluation of left and right value expressions. Intuitively, given an abstract state m, a left value expression l is possibly evaluated into an abstract address (v 1 , f) 2 V ⇥ F, top (>) that accounts for a failure of the analysis, or bottom (?). However, unfolding may be triggered during the evaluation, which outputs a disjunctive abstract state m 1 _ . . . _ m k , on each disjunct of which the evaluation is then performed on. Therefore, the abstract semantics of left value expressions is a ?-strict and >-strict function of the form:

eval l JlK 2 M ! ! _ ((V ⇥ F) ⇥ M ! ) ] {?, >}
We note that, in the following we sometimes write (v 1 , f) as v 1 + f or v 1 when the offset is 0. Similarly, unfolding may also be triggered in the evaluation of a right value expression r, and thus a right value expression r is either evaluated into a disjunction of pairs of abstract values and abstract states, or >, ?. The abstract semantics of right value expressions is defined as ?-strict and >-strict functions of the form:

eval r JrK 2 M ! ! _ (V ⇥ M ! ) ] {?, >}
Similar to the concrete expression evaluation shown in Figure 2.3, a formal definition of abstract expression evaluation can be derived based on the syntax of expressions and the abstract semantics read, J⊕K and unfold, and thus for simplicity is omitted here. Instead, we present the soundness condition of the abstract right value expression evaluation and the soundness condition of the abstract left value expression evaluation can be defined similarly.

Condition 2.9 (Soundness of the abstract evaluation of the right value expression). The abstract operation eval r JrK is sound if and only if the following property holds:

8 > > > > > > < > > > > > > : eval r JrK(g, n) = W 1in (v i , (g i , n i )) =) γ M! (g, n) ✓ S 1in γ M! (g i , n i ) ^81  i  n, {eval r JrK(", σ) | (", σ) 2 γ M! (g i , n i )} ✓ {µ(v i ) | (σ, µ) ✏ (g i , n i )} eval r JrK(g, n) = ? =) γ M! (g, n) = ;
Example 2.14 (Abstract evaluations). Let us consider the abstract state (g, n) of Example 2.10. The abstract left evaluation of x is the symbolic address &x of variable x, i.e., eval l JxK(g, n) = &x, while the abstract right evaluation of x is the symbolic variable ↵ 1 which abstracts the value of varibale x, i.e., eval r JxK(g, n) = ↵ 1 . Similarly, the abstract left evaluation of (*x).next is the abstract address ↵ 1 + next, i.e., eval l J(*x).nextK(g, n) = ↵ 1 + next, while the abstract right evaluation of (*x).next is the abstract value ↵ 2 at abstract address ↵ 1 + next, i.e., eval r J(*x).nextK(g, n) = ↵ 2 .

Folding

Section 2.4.2 shows the unfolding of inductive and segment edges, which is used in some abstract transfer functions. In contrast to unfolding, folding [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF] folds back memory regions into summary predicates and is required in abstract lattice operators of memory states: v M! , t M! and O M! . However, folding turns out to be much harder than unfolding, and the main difficulties lie in finding memory regions that are candidates for folding and searching for folded summary predicates. In the following, we present only the principles of the operators that need folding and refer the readers to Section 6.3 for more details.

Inclusion checking v M! . Inclusion checking takes two abstract states (g l , n l ) and (g r , n r ), and attempts to establish that the concretization of one abstract state (g l , n l ) is included in the concretization of the other abstract state (g r , n r ), that is γ M! (g l , n l ) ✓ γ M! (g r , n r ). A first use of inclusion checking is to prove an abstract loop invariant has been reached after a series of abstract iterations. A second use is to determine whether a memory region can be over-approximated by a summary predicate in joining t M! and widening O M! . In addition, inclusion checking is also used in proving post-conditions.

Specifically, the inclusion checking algorithm first aims to set up the inclusion of abstract shape graphs g l v G g r based on a series of syntactic rewriting rules. As the names of symbolic variables in g l may have nothing to do with the names in g r (symbolic variables are existential qualified variables), the rewriting rules have do deal with the renaming of symbolic variables. Thus, a rewriting rule either matches identical memory regions of g l and g r up to node renaming or weakens a memory region of g l (resp., g r ) into a memory region of g r (resp., g l ). When the inclusion holds on abstract shape graphs, it then applies the numerical inclusion checking operator v N to establish that n l v N n r .

Example 2.15 (Inclusion checking). Let us try to check the inclusion of (g l , n l ) into (g r , n r ), where:

&x ↵ 1 ↵ 2 ↵ 3 next d list g l : , n l : ↵ 1 6 = 0 &x β 1 list g r :
, n r : true As both abstract shape graphs contain a points-to edge from &x that are identical up to renaming node β 1 of g r into node ↵ 1 of g l , the inclusion checking algorithm thus binds β 1 to ↵ 1 (i.e., β 1 7 ! ↵ 1 ), and conclude that the points-to edge &x 7 ! ↵ 1 is included into &x 7 ! β 1 .

Then, the problem is reduced to checking the inclusion of (g 0 l , n l ) into (g 0 r , n r ) with node binding {β 1 7 ! ↵ 1 }, where:

&x ↵ 1 ↵ 2 ↵ 3 next d list g 0 l : , n l : ↵ 1 6 = 0 &x β 1 list g 0 r :
, n r : true As g 0 l and g 0 r no longer have identical predicates, the algorithm thus tries to weaken g 0 l into the inductive predicate β 1 • list of g 0 r . To do that, it unfolds the inductive predicate β 1 • list. One unfolding result is g 00 r with numerical constraint β 1 6 = 0, where:

&x β 1 β 2 β 3 next d list g 00 r :
The abstract graph g 00 r is identical with g 0 l up to node renaming {β 1 7 ! ↵ 1 , β 2 7 ! ↵ 2 , β 3 7 ! ↵ 3 }. The numerical constraint β 1 6 = 0 and numerical abstraction n r can be entailed by n l up to the node renaming. Therefore, the inclusion holds.

Joining t M! and widening O M! . The joining operator t M! takes two abstract states (g l , n l ) and (g r , n r ), and attempts to compute an abstract state (g o , n o ) that over-approximates both arguments, that is

γ M! (g l , n l ) ✓ γ M! (g o , n o ) and γ M! (g r , n r ) ✓ γ M! (g o , n o ).
Similar to the inclusion checking, the joining algorithm also first joins abstract shape graphs, i.e., g o = g l t G g r , based on a series of syntactic rewriting rules. Each rewriting rule outputs a memory region into g o , which is either identical to memory regions of g l and g r up to node renaming or over-approximates memory regions of g l and g r . Then, the numerical joining operator t N is applied on n l and n r to compute a common over-approximation, i.e., n o = n l t N n r .

The widening operator O M! is very similar to the joining operator, except that it relies on the numerical widening operator O N to enforce termination.

Disjunctive inclusion checking v D , joining t D and widening O D . Lifting the inclusion checking of abstract states v M! to disjunctive inclusion checking v D is obvious:

m l 1 _ . . . _ m ln v D m r 1 _ . . . _ m rm () 81  i  n, 91  j  m, m l i v M! m r j
However, an efficient disjunctive inclusion checking algorithm relies not only on efficient inclusion checking of abstract states v M! but also on an efficient algorithm (presented in Chapter 8) to choose the right abstraction m r j for each m l i such that m l i v M! m r j .

Given two disjunctive abstract states m l 1 _ . . . _ m ln and m r 1 _ . . . _ m rm , a simple disjunctive joining t D can directly return the disjunction of them m l 1 _ . . . _ m ln _ m r 1 _ . . . _ m rm . However, this joining operator can cause the disjunct number to grow exponentially. In order to limit the growth of the disjunct number, a disjunctive joining operator t D should partition the disjuncts of both arguments into different groups and compute an over-approximation for each group by repeatedly joining abstract states based on the joining operator t M! . We refer the reader to Chapter 10 for more details of the disjunctive joining operator.

A basic idea for widening two disjunctive abstract states m l 1 _ . . . _ m ln O D m r 1 _ . . . _ m rm is to partition the disjuncts of the right side into different groups according to the disjuncts of the left side, such that any disjunct m l i of the left side can be widened with an over-approximation of a subset of disjuncts of the right side. However, in practice, designing a precise disjunctive widening operator O D is usually hard, especially when the underlying abstract domain has infinite abstract states since the widening operator has to guarantee that the disjunct number of any iteration sequence will finally stabilize. Chapter 10 presents a such widening operator.

guard D Jc V K(m) = W 1in (g i , guard N (n i , v i 6 = 0)) where eval r Jc V K(m) = W 1in (v i , (g i , n i ))
Assignment:

Jl = rK(m) = W 1in W 1jk i write(v i , f i , v i j , m i j )
where

eval l JlK(m) = W 1in ((v i , f i ), m i )
and

81  i  n, eval r JrK(m i ) = W 1jk i (v i j , m i j ) Conditional branch: Jif(r){p 1 }else{p 2 }K(m) = Jp 1 K • guard D Jr 6 = 0K(m) t D Jp 2 K • guard D Jr == 0K(m) Loop: Jwhile(r){p}K(d) = guard D Jr == 0K(lfp v D λd 1 . d t D JpK • guard D Jr 6 = 0K(d 1 ))

Abstract Denotational Semantics

In this section, we formalize the abstract denotational semantics of programs that over-approximates the concrete denotational semantics defined in Figure 2.4 as:

JpK 2 D ! D
The abstract denotational semantics takes a disjunctive abstract state that over-approximates the pre-condition of the program p and outputs a disjunctive abstract state that over-approximates the concrete states after the execution of the program, and can be defined by induction over the syntax of programs in a very standard way. The soundness condition of the abstract denotational semantics is:

JpK(d 1 ) = d 2 =) {JpK(", σ) | (", σ) 2 γ D (d 1 )} ✓ γ D (d 2 )
For simplicity, we only formalize the abstract semantics of assignment, condition branch and loop statements in Figure 2.7. The abstract semantics of the other program statements can be defined similarly.

Abstract semantics of assignment statements. Intuitively, given an abstract state m 2 M ! , an abstract assignment operation Jl = rK should evaluate the left value expression into an abstract address v 1 + f, evaluate the right value expression into an abstract variable v 2 , and then write the abstract variable v 2 into the abstract address v 1 + f. However, as the abstract evaluation of left and right value expressions may trigger unfolding that produces disjunctive abstract states, therefore as shown in Figure 2.7, the abstract assignment operation on a single disjunct returns a disjunctive abstract state. Though disjuncts can be collapsed together by the joining operator t M! , precision is often lost. The opposite direction consists in keeping all disjuncts as shown in 2.7, which would lead to a very precise but very costly analysis. In practice, in order to design scalable analysis, an operator that partially collapses disjuncts to maintain a low number of disjuncts while preserving the precision is necessary. The soundness can be proved by composing the soundness of abstract operations eval l JlK, eval r JrK and write.

Abstract semantics of conditional branch statements. Figure 2.7 shows the definition of the abstract semantics of conditional branch statements on a single disjunct, which involves a guard function of the following form:

guard D 2 C V ! D ! D It inputs a numerical constraint c V 2 C V expressing
guard D (c V , d 1 ) = d 2 =) {(", σ) | (", σ) 2 γ D (d 1 ) ^eval r Jc V K(", σ) 6 2 {0, !}} ✓ γ D (d 2 )
Abstract semantics of loops. As the concrete denotational semantics of a loop while(r){p} shown in Figure 2.4 computes a least fix-point as a post-condition from a pre-condition, the abstract denotational semantics of loops defined in Soundness of the analysis. Finally, let us establish the main theorem regarding the soundness of the analysis.

Theorem 2.1 (Soundness of the abstract denotational semantics.). The abstract denotational semantics is sound with respect to the soundness condition:

JpK(d 1 ) = d 2 =) {JpK(", σ) | (", σ) 2 γ D (d 1 )} ✓ γ D (d 2 )
Proof. The proof can be done by induction over the syntax of programs, by composing:

• the soundness of the abstract store operations: read, write, create and delete;

• the soundness of abstract evaluation operations: eval l JlK and eval r JrK, and the abstract guard functions guard N and guard G ; • the soundness of abstract lattice operators:

v M! , t M! , O M! . ⌅

Domain Signatures

Thus far, we have introduced an abstract domain for abstracting memory states that takes a numerical abstract domain as a parameter, and lifted the memory abstract domain to a disjunctive abstract domain. To sum up, in this section we give an exhaustive list of signatures of these abstract domains.

Signature for numerical abstract domains.

numerical abstract elements n 2 N concretization γ N : N ! P(V ! V) guard guard N : N ⇥ C V ! N assign assign N : N ⇥ V ⇥ R V ! N remove remove N : N ⇥ V ! N prove prove N : N ⇥ C V ! {true, false} rename rename N : N ⇥ (V ! P(V)) ! N abstract join t N : N ⇥ N ! N abstract widen O N : N ⇥ N ! N inclusion check v N : N ⇥ N ! {true, false}
Signature for memory abstract domains.

abstract states m 2 M ! concretization γ M! : M ! ! P(E ⇥ H) guard guard M! : M ! ⇥ C V ! W M ! store read read : V ⇥ F ⇥ M ! ! V ] {>, ?} store write write : V ⇥ F ⇥ V ⇥ M ! ! M ! store create create : N ⇥ M ! ! (V ⇥ M ! ) 2 ] {?, >} store delete delete : V ⇥ N ⇥ M ! ! M ! left value evaluation eval l JlK : M ! ! W ((V ⇥ F) ⇥ M ! ) ] {?, >} right value evaluation eval r JrK : M ! ! W (V ⇥ M ! ) ] {?, >} abstract join t M! : M ! ⇥ M ! ! M ! abstract widen O M! : M ! ⇥ M ! ! M ! inclusion check v M! : M ! ⇥ M ! ! {true, false}

Shape Analysis for Unstructured Sharing

Chapter 3

Overview

In this part, we propose a shape analysis that tracks set properties to infer precise invariants about data structures with unstructured sharing. Before the formalization, we outline the analysis of a graph traversal algorithm, where graphs are represented as adjacency lists.

Abstraction

An adjacency list is a graph data structure with unstructured sharing as the number of predecessors of a node is unbounded and the predecessors could be anywhere in the structure. Figure 3.1 shows a type definition of adjacency lists: a graph is a list of nodes, each node has a list of edges which comprise pointers to successor nodes. Separation logic based shape analysis relies on the separating conjunction ⇤ to express dis- joint properties of memory regions and inductive definitions to summarize recursive data structures. However, summarizing adjacency lists in this framework turns out to be very challenging.

Simply exploiting the list-of-lists inductive skeleton of adjacency lists based on the separation conjunction cannot capture the cross edge pointers precisely, as the separation conjunction only allow nodes to be described once. In order to capture the unstructured sharing of adjacency lists precisely, Section 1.5.1 outlined an approach to summarize adjacency lists using a combination of an inductive skeleton and relations over set-valued variables. However, using such summaries poses significant algorithmic challenges in analyzing graph manipulation programs. To be more concrete, in this chapter we consider analyzing a representative of graph traversal algorithms that manipulates graph edges. Intuitively, traversing graph edges amounts to traversing the cross pointers of Figure 3.2(b). Such steps make the shape analysis of graph manipulation programs tricky since they do not follow the inductive skeleton of the adjacency list-instead, they "jump" to some other node in the structure.

In the rest of this section, we first present the inductive definition of adjacency lists and then discuss abstractions of memory states comprising adjacency lists. Formalizations of the abstractions are presented in Chapter 4. Graph inductive predicate. The first step towards an analysis to verify a graph algorithm is to set up inductive definitions to summarize the adjacency list structure. The set of outgoing edges of a node consists of a list of records, and thus the predicate to summarize such a region can be based on a classical list inductive definition:

↵ • list ::= (emp, ↵ = 0) _ (↵ • dest 7 ! β ⇤ ↵ • next 7 ! γ ⇤ γ • list, ↵ 6 = 0)
However, this definition does not express the fact that all instances of field dest contain a pointer to a node of the graph as the value β of that field is unconstrained. To resolve this issue, we simply need to add the constraint β 2 E , where E should denote the set of all node addresses in the graph. The abstract domain should also keep track of those predicates through folding and unfolding steps. Therefore, we obtain the inductive definition edges, as shown in Figure 3.3. The inductive definition edges takes the additional parameter E , and the value predicate of the non-empty case has been strengthened with the set predicate β 2 E . Moreover, the inductive definition of a graph needs to capture two set properties: (1) the destination of all edges are in set E (as described by inductive definition edges) and (2) the set of nodes in the adjacency list should contain the set E . Thus, the inductive definition nodes presented in Figure 3.3 takes two set parameters: (1) E is constant over the whole induction and (2) F stands for the set of nodes of a graph fragment described by an instance of nodes. We note that the set predicates F = ; (base case) and F = F 0 ] {↵} (inductive case) guarantee that F is exactly the set of nodes described by predicate ↵ • nodes(E , F ).

↵ • edges(E ) ::= (emp, ↵ = 0) _ (↵ • dest 7 ! β ⇤ ↵ • next 7 ! γ ⇤ γ • edges(E ), ↵ 6 = 0 ^β 2 E ^β 6 = 0) ↵ • nodes(E , F ) ::= (emp, ↵ = 0 ^F = ;) _ (↵ • next 7 ! β ⇤ ↵ • id 7 ! γ ⇤ ↵ • edges 7 ! δ ⇤ β • nodes(E , F 0 ) ⇤ δ • edges(E ), ↵ 6 = 0 ^F = F 0 ] {↵})
↵ 6 = 0 F = F 1 ] {↵} E ✓ F (
Abstraction of memory states. Using these definitions, the complete adjacency list pointed to by pointer g shown in Figure 3.

Analysis Algorithm

We now discuss automatic shape analysis algorithms (formalized in Chapter 6) to verify the memory safety property (the absence of null or dangling pointer dereferences) and the preservation of structural invariants of the graph random traversal program shown in Figure 3.5.

In particular, the analysis should start from a pre-condition specifying that variable h pointsto a correct graph with the set of nodes F :

m 0 : c h ↵ nodes(E , F ) E ✓ F
Then, at line 2, the cursor c is initialized to variable h:

m 1 : h, c ↵ nodes(E , F ) E ✓ F
Then, the loop body (lines 4 to 10) randomly selects a successor of the node pointed to by c (lines 4 to 8 ) and moves to that node at line 9. The analysis of the loop body needs to unfold summaries to perform mutation over summarized regions, and to utilize a widening operator for the convergence of the abstract iterates over both nested loops. However, to establish that no dangling pointer is dereferenced, the analysis should precisely track the fact that c either points to a valid node of the graph, or is a null pointer (which causes the program to exit) at all times.

To show the challenges of the analysis, let us discuss the first abstract loop iteration in detail; the other iterations are similar.

Unfolding. At line 4, variable s is initialized to a pointer to the edge list of the node pointedto by c. As variable c points-to an inductive predicate ↵ • nodes(E , F ) as shown in the abstract state m 1 , performing the abstract assignment requires unfolding the inductive predicate and other abstract operations, which leads to the abstract state below:

m 2 : c, h ↵ ↵ 0 s β next id edges edges(E )
nodes(E , F 1 )

↵ 6 = 0 ^F = {↵} ] F 1 ^E ✓ F
Moreover, the assignment at line 7 advances variable s to the pointer of its next edge, which relies on unfolding the edge predicate β • edges(E ) as shown in the abstract state m 2 and leads to the abstract state m 3 after assignment:

m 3 : c, h ↵ ↵ 0 β δ s β 0 next id edges dest next edges(E ) nodes(E , F 1 ) ↵ 6 = 0 ^β 6 = 0 ^δ 6 = 0 ^β0 6 = 0 ^F = {↵} ] F 1 ^δ 2 E ^E ✓ F
Widening with set parameters. Then, the analysis needs to infer the loop invariant of the inner loop from line 6 to line 8, which relies on applying a widening operator (O M! ) on the two abstract states below at the end of the first loop iteration:

m 0 2 : c, h ↵ ↵ 0 s β next id edges edges(E ) nodes(E , F 1 ) ↵ 6 = 0 ^β 6 = 0 ^E ✓ F ^F = {↵} ] F 1 O M! m 3 : c, h ↵ ↵ 0 β δ s β 0 next id edges dest next edges(E ) nodes(E , F 1 ) ↵ 6 = 0 ^β 6 = 0 ^δ 6 = 0 ^β0 6 = 0 ^F = {↵} ] F 1 ^δ 2 E ^E ✓ F
The two abstract shape graphs are very similar except that in m 0 2 , s is a pointer to the first element of the edge list of the node at ↵, and in m 3 , s points-to the second element. Intuitively, the widening operation should compute a shape graph declaring that s refers to an element somewhere in the edge list of the node at ↵. This can be done by introducing an edge list segment from β to β 0 in the abstract graph below:

m 4 : c, h ↵ ↵ 0 β s β 0 next id edges edges(?) edges(?)
nodes(?, ?)

↵ 6 = 0 ^β 6 = 0 ^β0 6 = 0
Moreover, the widening operation should also synthesize set parameters for summary predicates, such that the structural invariants of adjacency lists can still be tracked. The abstract state below shows an abstract shape graph with precise set parameters:

m 4 : c, h ↵ ↵ 0 β s β 0 next id edges edges(E ) edges(E ) nodes(E , F 1 ) ↵ 6 = 0 ^β 6 = 0 ^β0 6 = 0 ^F = {↵} ] F 1 ^E ✓ F
However, precise parameter synthesis requires reasoning about properties of the set parameters of the inductive definitions nodes and edges. For instance, the inference of set parameter E of the edge segment from β to β 0 is based on the fact that the inductive definition edges has a constant set parameter. Intuitively, a set parameter is said to be a constant of an inductive definition if it is propagated with no modification to all recursive calls of the inductive definition.

Non-local unfolding with set parameters. After the inner loop, variable c is set to the destination node of the edge pointed to by s at line 9, which leads to the abstract state:

m 5 : h ↵ ↵ 0 ↵ 00 β s β 0 c δ next id edges edges(E ) dest next nodes(E , F 1 ) edges(E ) ↵ 6 = 0 ^β 6 = 0 ^β0 6 = 0 ^δ 6 = 0 ^E ✓ F ^F = {↵} ] F 1 ^δ 2 E
In the abstract state m 5 , c no longer appears to point to a node in the nodes inductive backbone. Yet, the dereferencing of c -> id at line 10 requires the materialization of an edge from that node, although no edge (points-to or summary) starts from node δ. However, the analysis infers that δ 2 E ^E ✓ F ^F = {↵} ] F 1 , which indicates that either δ = ↵, or δ 2 F 1 . If δ = ↵, then the dereferencing of c -> id can be achieved by reading the value ↵ 00 of the points-to edge ↵.id 7 ! ↵ 00 . However, the case of δ 2 F 1 is more complex.

We notice that the second parameter F of the nodes inductive definition is a head parameter: F = ; in the empty rule and F = {↵} ] F 0 in the second rule, where ↵ is the address of the head of the structure and F 0 is the parameter of the tail. That is, the parameter collects the set of head nodes in all recursive inductive calls.

Therefore, in abstract state m 5 , set parameter F 1 denotes the set of addresses of graph nodes summarized in the inductive predicate ↵ 0 • nodes(E , F 1 ). Thus, δ 2 F 1 means that δ is the address of a graph node in the inductive predicate from ↵ 0 , and it can be materialized by splitting the inductive predicate into a node list segment from ↵ 0 to δ and an inductive predicate from δ as shown below:

m 0 5 : h ↵ ↵ 0 c δ ↵ 00 β s β 0 next id edges nodes(E , F 2 ) edges(E ) dest next nodes(E , F 3 ) edges(E ) ↵ 6 = 0 ^β 6 = 0 ^β0 6 = 0 ^δ 6 = 0 ^E ✓ F ^F = {↵} ] F 2 ] F 3 ^δ 2 E
The side property F = {↵} ] F 2 ] F 3 states that the set of graph nodes F 1 summarized in the inductive edge ↵ 0 • nodes(E , F 1 ) is split into the two partitions: F 2 and F 3 , where F 2 describes the set of graph nodes summarized in the segment and F 3 describes the set of graph nodes summarized in the inductive predicate from δ.

This form of unfolding is much more complex than more conventional forms of inductive predicates unfolding. Indeed, the conventional unfolding techniques (except backward unfolding) look no further than the edges going out of the node where they need to do the unfolding while the unfolding presented here needs to utilize the set properties to localize δ. To achieve this, the analysis needs to track all set predicates through unfolding, updates and widening steps and also to infer properties of set parameters, i.e., constant and head.

Chapter 4

Abstractions for Data-Structures with Unstructured Sharing

This chapter formalizes the memory abstractions for reasoning about sharing. Specifically, Section 4.1 formalizes inductive definitions parameterized by set variables. Section 4.2 proposes memory abstractions parameterized by inductive definitions and an abstract domain for constraints over value and set variables. Section 4.3 discusses properties of set parameters: constant and head, which are used to infer set parameters of summary predicates during program analysis.

Inductive Definitions with Set Predicates

The analysis presented in this thesis is parameterized by a set of inductive definitions, which means that the abstract domain is generic, and can deal with a wide family of data-structures. In this section, we extend the relational inductive definitions of [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF] with set predicates.

Inductive definitions. An inductive definition ↵ • ind(↵ 0 , . . . , ↵ m , E 0 , . . . , E n ) ::= r 0 _ r 1 _ . . . _ r k takes a main parameter ↵, a list of pointer parameters ↵ 0 , . . . , ↵ m and a list of set parameters E 0 , . . . , E n and defines a scheme to summarize heap regions that satisfy some inductive property, specified as a disjunction of rules as presented in Figure 4.1. Each rule comprises a heap part and a pure part. The heap part is a separating conjunction of memory cells (points-to predicates of the form ↵ • f 7 ! β) and recursive calls to inductive definitions. The pure part comprises not only numerical constraints, but also set constraints, over the symbolic variables exposed in the heap part and the set parameters, as shown in F Pure . The intuitive meaning of a set constraint such as ↵ 2 E is that the concretization will map ↵ into a numerical value that belongs to the concretization of E . As a simple example, the inductive definition below characterizes the singly linked list starting at address ↵, such that the set of addresses of list elements is exactly E :

↵ • l s (E ) ::= (emp, ↵ = 0 ^E = ;) _ (↵ • n 7 ! β 0 ⇤ ↵ • v 7 ! β 1 ⇤ β 0 • l s (E 0 ), ↵ 6 = 0 ^E = {↵} ] E 0 ) r ::= (F Heap , F Pure ) F Heap ::= emp | ↵ • f 7 ! β | ↵ • ind(↵ 0 , . . . , ↵ n , E 0 , . . . , E n ) | F Heap ⇤ F Heap F Pure ::= ↵ = c (c 2 V) | ↵ 6 = c (c 2 V) | ↵ 2 E | E = {↵} ] F | E = {↵} [ F | . . .
↵ • l c (E ) ::= (emp, ↵ = 0) _ (↵ • n 7 ! β 0 ⇤ ↵ • d 7 ! β 1 ⇤ β 0 • l c (E ), ↵ 6 = 0 ^β1 2 E )
Inductive definitions edges and nodes (Figure 3.3) capture set constraints over the nodes and edges of graphs in a similar way: nodes collects exactly the set of all nodes of the graph, whereas edges asserts all edges should point to one of the nodes of the graph.

Since pointer parameters are not our main contribution, we will often omit them in this part of the thesis. However, the analysis that we describe supports them together with set parameters. Similarly, and for the sake of readability, we will often write inductive predicates with a single set parameter.

Composite Memory Abstraction with Set Predicates

We now formalize abstract memory states M ! .

Concrete values V are abstracted by abstract values V. An abstract value variable v 2 V is either a symbolic variable ↵ 2 V ↵ or the symbolic address &x of a program variable x. Set variables (e.g., E , F 2 T ) abstract sets of concrete values. We let µ 2 F µ be a valuation function that maps each abstract value v 2 V (resp., set variable E 2 T ) to a numerical value µ(v) 2 V (resp., set of numerical values µ(E ) 2 P(V)).

Moreover, abstract states are parameterized by a finite set of inductive definitions defined by the syntax shown in Section 4.1 and a value-set abstract domain C that provides an abstraction for constraints over abstract values and set variables, such as value constraint ↵ 6 = 0 ^↵0 6 = 0, and set constraint F = F 1 ] F 2 ^E ✓ F . We will construct a set-value abstract domain in Chapter 5. Such a domain will be defined as a reduced product of an existing numeric abstract domain [Min06, CH78, CC77] and an abstract domain designed to describe constraints over set symbols.

&x ↵ 0 &y ↵ 1 l s (E 0 ) l c (E 1 ) , ↵ 1 6 = 0 ^E1 ✓ E 0
g ::= emp | ↵ • f 7 ! β | ↵ • ind( Ẽ ) | ↵ • ind( Ẽ ) ⇤= β • ind( Ẽ ) | g ⇤ g
An abstract shape graph g is either empty, or a single points-to edge ↵•f 7 ! β, or an inductive predicate ↵ • ind( Ẽ ) (instantiating an inductive definition ind), or a segment ↵ • ind( Ẽ ) ⇤= β • ind( Ẽ ) describing an incomplete inductive structure, or a separating product of such predicates. It should be noted that, this definition of abstract shape graphs is an extension of that given in Section 2.3. Specifically, the emp and points-to predicates are the same, yet the inductive predicates and segment predicates are extended with set parameters. Moreover, a value-set abstraction c 2 C is also an extension of a numerical abstraction n 2 N , which allows us to reason about set properties. As an example, Figure 4.2 shows an abstract state parameterized by inductive definitions l s and l c defined in Section 4.1. It states that variable y points-to a list abstracted by ↵ 1 • l c (E 1 ), where the d field of each list element points to a list element of a list ↵ 0 • l s (E 0 ) pointed to by variable x.

Concretization. A value-set abstraction c 2 C is concretized into a set of valuations that map each abstract value variable and set variable respectively to a numerical value and a set of numerical values:

γ C : C ! P(F µ )
The concretization of an abstract shape graph g 2 G is a set of pairs of concrete stores and valuations for abstract value variables and set variables, that is:

γ G : G ! P(H ⇥ F µ )
The concretization of value-set abstractions and abstract shape graphs is very similar to that of numerical abstractions and abstract shape graphs introduced in Section 2.3 except that the valuations here concretize set variables. Thus, the concretization of an abstract memory state m = (g, c) 2 M ! is defined as a set of memory states, and for each memory state, a valuation of Chapter 4. Abstractions for Data-Structures with Unstructured Sharing

([], µ) 2 γ G (emp) a = µ(↵) + f v = µ(β) ([a 7 ! v], µ) 2 γ G (↵ • f 7 ! β) 8i, (σ i , µ) 2 γ G (g i ) (σ 0 ] σ 1 , µ) 2 γ G (g 0 ⇤ g 1 ) g U (F Heap , F Pure ) (σ, µ) 2 γ G (F Heap ) µ `FPure (σ, µ) 2 γ G (g)
Figure 4.3: Concretization rules abstract value variables and set variables can be found that satisfies all constraints from g and c:

γ M! (g, c) = {(µ dX & , σ) 2 M | 9µ 2 γ C (c), (σ, µ) 2 γ G (g)}
Concretization of abstract shape graphs. Figure 4.3 shows the concretization rules for abstract shape graphs. The first three rules describe the usual concretization for empty shapes, single points-to edges and the separating conjunction. The last rule defines the concretization for inductive and segment predicates using the standard notion of syntactic unfolding [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF]: the unfolding of an inductive or segment predicate selects a rule r in the corresponding inductive or segment definition, and replaces the predicate with the heap part of r and constrains value and set valuations with the pure part of r.

Example 4.1 (Abstract shape graphs and their concretization). Figure 4.4 shows a few abstractions of the concrete memory state σ shown in Figure 4.4(a), where l stores a pointer to a list of length 3, and where v 0 , v 1 , . . . , v 7 denote numerical values / addresses. The shape of Figure 4.4(b) abstracts this state without any summarization (it contains no inductive predicate). Its concretization into m results in 8i, µ(↵ i ) = v i (in particular, µ(↵ 6 ) = v 6 = 0x0), and can be fully expressed using the points-to and separating product rules of Figure 4.3. The shape of Figure 4.4(c) summarizes the list completely into a single inductive predicate ↵ 1 • l s (E 0 ). In this case, the concretization also needs to bind E 0 to a set of concrete addresses: by the definition of l s (Section 4.1), this boils down to µ(E 0 ) = {v 1 , v 2 , v 4 }. Moreover, this concretization needs to trigger the unfolding rule (last rule in Figure 4.3) four times in order to produce the shape of Figure 4.4(b). The first three unfoldings successively generate points-to edges at ↵ 1 , ↵ 2 and ↵ 4 , and the last unfolding constrains ↵ 6 to be null. The shape of Figure 4.4(d) summarizes only the last two elements of the list (in purple) while the first element (in red) is preserved in its unfolded form. Similarly to the previous case, the unfolding of this shape needs to trigger the unfolding rule three times in order to get the shape of Figure 4.4(b) and to map E 1 to µ(E 1 ) = {v 2 , v 4 }.

Finally, the shape of Figure 4.4(e) summarizes two list elements with inductive predicate ↵ 2 • l s (E 3 ) (in purple) and the rest of the list with a segment predicate (in red). The meaning of the segment predicate ↵ 1 •l s (F 1 ) ⇤= ↵ 2 •l s (F 2 ) can be expressed by the following segment

a 0 = &l v 0 v 2 v 3 v 4 v 5 v 6 v 7 v 1 = 0x0 (a) An example concrete memory ↵ 0 ↵ 1 ↵ 2 ↵ 3 ↵ 4 ↵ 5 ↵ 6 ↵ 7 n v n v n v (b) Shape, no summarization ↵ 0 ↵ 1 l s (E 0 ) (c) Shape, summarization ↵ 0 ↵ 1 ↵ 2 ↵ 3 n v l s (E 1 ) (d) Shape, partial summarization ↵ 0 ↵ 1 ↵ 2 l s (F 1 ) l s (F 2 ) l s (E 1 ) (e) Segment and inductive summaries ↵ 0 ↵ 1 ↵ 2 l s (F ) l s (E 1 ) (f)
↵ • l s (E ) ⇤= β • l s (F ) ::= emp ^↵ = β ^E = F _ ↵ • n 7 ! ↵ 0 ⇤ ↵ • v 7 ! ↵ 1 ⇤ ↵ 0 • l s (E 0 ) ⇤= β • l s (F ) ^↵0 6 = ↵ 1 ^E = {↵} ] E 0 Thus, set variables F 1 , F 2 of the segment ↵ 1 • l s (F 1 ) ⇤= ↵ 2 • l s (F 2
) describe two sets of addresses such that the set of addresses of the list elements summarized in the segment is exactly µ(F 1 ) \ µ(F 2 ).

Properties of Set Parameters

Inductive definitions with set parameters (Section 4.1) provide a scheme to summarize data structures with sharing. However, automatically inferring accurate set parameters for summary predicates during shape analysis turns out to be a very hard task as they depend on complex properties of the data-structure shapes and contents.

As an example, let us consider folding the points-to edges from node ↵ 1 in Figure 4.4(d) into the segment edge in Figure 4.4(e) and inferring set parameters F 1 and F 2 . According to the segment definition shown in Example 4.1, the folding process infers that F 1 = {↵ 1 } ] F 2 , which means set variables F 1 and F 2 can be concretized into any sets µ(F 1 ) and µ(F 2 ) such that µ(F 1 ) \ µ(F 2 ) = µ(↵ 1 ). In other words, only the difference between these two set parameters matters. However, proving data structure preservation of the abstract state shown in Figure 4.4(e) requires the set predicate F 2 = E 1 which cannot be inferred directly according to the segment definition shown in Example 4.1. Indeed, as only the difference between set parameters F 1 and F 2 matters, the segment predicate can be simplified with only one set parameter F denoting the difference between F 1 and F 2 , such as ↵ 1 • l s ⇤= (F ) ↵ 2 • l s . Thus, set parameter F can be simply inferred as {↵ 1 } in the folding process. Figure 4.4(f) shows the graphical notation of the segment predicate

↵ 1 • l s ⇤= (F ) ↵ 2 • l s .
In the following, we identify so-called parameter kinds, that simplify the inference of segment parameters in join, and make such simplified definitions possible.

Constant parameters. Intuitively, a set parameter of an inductive definition is constant if it is propagated with no modification to all the recursive calls of the inductive definition. We note that the set parameter E of edges (Figure 3.3) and also the first set parameter E of nodes (Figure 3.3) are constant set parameters. In the following, we write ind `E : cst to denote that parameter E of inductive definition ind is constant.

Inferring constant parameters. To automatically infer whether a set parameter E of an inductive definition ↵ • ind(E ) ::= r 0 _ r 1 _ . . . _ r k is constant, we use the following derivation rules on the inductive definition ind:

• parameter E is constant if and only if it is so for each heap part of a rule of ind:

8i, 0  i  k =) r i `ind E : cst ind `E : cst F Heap `ind E : cst (F Heap , F Pure ) `ind E : cst
• when considering a part of F Heap that consists only of a call to ind, then the parameter is constant if and only if it is applied to the same set parameter as the current call:

β • ind(E ) `ind E : cst
• when considering a part of F Heap that consists only of a call to another inductive definition ind 0 , and provided that definition does not call ind (even indirectly), then the parameter is constant: ind 0 does not call ind directly or indirectly β • ind 0 (F ) `ind E : cst

• finally, the "is constant" property propagates naturally through the separating product and points-to predicate:

F Heap `ind E : cst F 0 Heap `ind E : cst F Heap ⇤ F 0 Heap `ind E : cst ↵ • f 7 ! β `ind E : cst Properties of constant parameters. When a set parameter E of an inductive definition ↵ • ind(E ) ::= r 0 _ r 1 _ . . . _ r k is constant (ind `E : cst), segment predicates (e.g., ↵ 1 • l s (E 0 ) ⇤= ↵ 2 • l s (E 1 )
) can be simplified with only one set parameter (e.g., ↵ 1 • l s ⇤= (F ) ↵ 2 • l s ) as any state (σ, µ) in the concretization of the segment

↵ 1 • l s (E 0 ) ⇤= ↵ 2 • l s (E 1 ) is such that µ(E 0 ) = µ(E 1 ).
Theorem 4.1 (Folding of summary predicates with constant parameters). Given an inductive definition ↵ • ind(E ) ::= r 0 _ r 1 _ . . . _ r k , if ind `E : cst, then:

γ G (↵ 0 • ind ⇤= (E ) ↵ 1 • ind ⇤ ↵ 1 • ind(E )) ✓ γ G (↵ 0 • ind(E )) γ G (↵ 0 • ind ⇤= (E ) ↵ 1 • ind ⇤ ↵ 1 • ind ⇤= (E ) ↵ 2 • ind) ✓ γ G (↵ 0 • ind ⇤= (E ) ↵ 2 • ind)
Proof. The theorem can be proved by induction on the unfolding depths of the segment predicate

↵ 0 • ind ⇤= (E ) ↵ 1 • ind.
⌅

Head parameters

The second parameter of nodes (Figure 3.3) is clearly not constant as it collects the set of head nodes in all recursive inductive calls, and can be computed exactly from the values of the same parameters in the recursive calls. We call such a parameter a head parameter. This definition generalizes to non-linear structures (i.e., with several recursive calls corresponding to distinct sub-structures, like trees). Parameter E of the l s definition is also a head set parameter. In the following, we write ind `E : head to denote that parameter E of inductive definition ind is head.

Inferring head parameters. To automatically infer whether a set parameter E of an inductive definition ↵ • ind(E ) ::= r 0 _ r 1 _ . . . _ r k is head, we use the following derivation rules on the inductive definition ind:

• parameter E is head for ind if and only if it is so for each inductive rule:

80  i  k, r i `ind E : head ind `E : head
• parameter E is head for a given rule that unfolds cells at ↵ if and only if it is provably equal to the disjoint union of {↵} and the arguments of the recursive sub-calls to ind, that is if it can be partitioned into a set of sets corresponding to the argument of each call and {↵}:

F Heap `ind {E i | 0  i  n} F Pure ✏ U n 0=i E i ] {↵} = E (F Heap , F Pure ) `ind E : head
• parameter E is head for a given rule that unfolds to emp if and only if E is inferred as ;:

F Pure ✏ E = ; (emp, F Pure ) `ind E : head
• rules for the separating conjunction, empty and points-to predicates express the linearity of head parameters (where, T, T 0 denote sets of set variables):

F Heap `ind T F 0 Heap `ind T 0 F Heap ⇤ F 0 Heap `ind T ] T 0 emp `ind ; ↵ • f 7 ! β `ind ;
• an inductive call to ind accounts for a single set variable corresponding to its parameter (the head addresses in the structure are exactly the head addresses of the sub-call):

β • ind(E i ) `ind {E i }
• finally, calls to other inductive definitions contribute an empty set of head addresses in a structure: ind 0 does not call ind directly or indirectly β • ind 0 (F ) `ind ;

Properties of head parameters. When a set parameter E of an inductive definition ↵ • ind(E ) ::= r 0 _ r 1 _ . . . _ r k is head (ind `E : head), segment predicates (e.g., ↵ 1 • l s (E 0 ) ⇤= ↵ 2 • l s (E 1 )) can be simplified with only one set parameter (e.g.,

↵ 1 • l s ⇤= (F ) ↵ 2 • l s ) as for any concretization (σ, µ) of the segment ↵ 1 • l s (E 0 ) ⇤= ↵ 2 • l s (E 1 )
, only the difference between E 0 and E 1 matters, that is, we can always find another valuation µ 0 (µ 0 6 = µ) such that

(σ, µ 0 ) 2 γ G (↵ 1 • l s (E 0 ) ⇤= ↵ 2 • l s (E 1 )) and µ 0 (E 0 ) \ µ 0 (E 1 ) = µ(E 0 ) \ µ(E 1 ).
Theorem 4.2 (Folding of summary predicates with head parameters). Given an inductive definition ↵ • ind(E ) :

:= r 0 _ r 1 _ . . . _ r k , if ind `E : head, then: for all (σ, µ) 2 H ⇥ F µ • (σ, µ) 2 γ G (↵ 0 • ind ⇤= (E 0 ) ↵ 1 • ind ⇤ ↵ 1 • ind(E 1 )) ^µ `E = E 0 ] E 1 =) (σ, µ) 2 γ M! (↵ 0 • ind(E )) • (σ, µ) 2 γ G (↵ 0 • ind ⇤= (E 0 ) ↵ 1 • ind ⇤ ↵ 1 • ind ⇤= (E 1 ) ↵ 2 • ind) ^µ `E = E 0 ] E 1 =) (σ, µ) 2 γ M! (↵ 0 • ind ⇤= (E ) ↵ 2 • ind)
Proof. The theorem can be proved by induction on the unfolding depths of the segment predicate

↵ 0 • ind ⇤= (E 0 ) ↵ 1 • ind. ⌅
To conclude, we have shown two kinds of set parameters, constant and head. Yet there may also be other kinds of set parameters, the abstractions that we present in this chapter and the analysis algorithm presented in Chapter 6 are not limited to constant and head set parameters. Moreover, constant and head set parameters correspond to a solution to a sharing pattern that is not limited to adjacency lists. For example, memory states that are composed of binary trees and lists with pointers to the tree can also be abstracted based on inductive definitions with constant and head set parameters and such memory states often appear in tree traversal algorithms. In addition, the study on kinds of set parameters may also allow us to design efficient shape analysis algorithms to support inductive predicates with numerical properties, such as sorted lists, lists of certain lengths and binary search trees.

Chapter 5

Abstract Domains for Set Reasoning

This chapter presents the work carried out in collaboration with Arlen Cox on set abstract domains, thus only the part strictly related to the thesis is presented. In the analysis of sharing data structures, set abstract domains are used for reasoning about set predicates. Specifically, Section 5.1 presents a common interface for set abstract domains, which is needed by the program analysis. Section 5.2 mainly presents a set abstract domain that is based on linear constraints over sets and briefly introduces a BDD-based set domain.

Set Constraints and Abstractions

In this section, we first define set predicates that a set abstract domain needs to reason about and define concrete states as models of set predicates. Then, we specify a common interface of set abstract domains.

Concrete States of Set Variables

Concrete states. We recall that V denotes the set of all concrete values, E , F 2 T are set variables, and v 1 , v 2 2 V are abstract value variables. A concrete state is a valuation function µ 2 F µ that maps each abstract value to a concrete value v 2 V and each set variable to a set of concrete values V 2 P(V).

Set predicates. We now set up the language of set predicates and its concrete semantics. Operations over set abstractions. The main operations that a set abstract domain should provide is formalized in Figure 5.2.

The abstract operator isbot S is used to conservatively determine if an abstract state describes unsatisfiable set constraints. As an example, for the singleton set domain presented in Example 5.1, isbot S (s) returns true when the abstract element s is ?. The soundness condition of the operator is that:

isbot S (s) = true =) γ S (s) = ;
The abstract operator prove S is used to conservatively determine if a set constraint c T 2 C T is implied by a set abstract element s 2 S. A singleton set abstract element can only imply set predicates of the forms E = {↵} and ↵ 2 E , e.g., prove S ({E 7 ! ↵, F 7 ! β}, β 2 F ) = true. The soundness condition of the operator is that:

prove S (s, c T ) = true =) γ S (s) ✓ γ C T (c T )
The operator guard S is used to enforce a set constraint c T 2 C T on a set abstraction s 2 S. For instance, prove S ({E 7 ! ↵}, E 0 = {↵}) enforces set predicate E 0 = {↵} on the singleton set abstract element {E 7 ! ↵} and gets abstract element {E 7 ! ↵, E 0 7 ! ↵}. The soundness condition of the operator is that:

guard S (s, c T ) = s 0 =) γ S (s) \ γ C T (c T ) ✓ γ S (s 0 )
The operator project S is used to project out set variables or abstract value variables that become redundant from a set abstraction. For example, projecting out a set variable from a singleton set abstract element can simply remove the map of the set variable. The soundness condition of the operator is that:

project S (s, E ) = s 0 =) 8µ 2 γ S (s), µ ddom(s)\E 2 γ S (s 0 ) project S (s, v) = s 0 =) 8µ 2 γ S (s), µ ddom(s)\v 2 γ S (s 0 )
The operator rename S is used to rename set variables and abstract value variables in set abstract elements and is needed in the joining process of abstract memory states (presented in Chapter 6). Let us assume that f 2 V ] T ! P(V ] T ) is a renaming map of a set abstract element s, which maps a set variable E (resp., an abstract value variable v) of s to a set of set variables (resp., a set of abstract value variables) that share the same property with E (resp., v). As an example, renaming set variable E to {E 0 , F 0 } and symbolic variable ↵ to ↵ 0 of the singleton set abstract element {E 7 ! ↵} gets {E 0 7 ! ↵ 0 , F 0 7 ! ↵ 0 }. The soundness condition of the operator is that:

rename S (s, f ) = s 0 =) 8µ 2 γ S (s), 8µ 0 , 8E 2 dom(f ), 8E 0 2 f (E ), µ 0 (E 0 ) = µ(E ) =) µ 0 2 γ S (s 0 )
The inclusion checking operator v S conservatively decides implication among set abstract elements. It is necessary in verifying the convergence of abstract iterations and proving postconditions. As an example, checking the implication between singleton set abstract elements s and s 0 , i.e., v S (s, s 0 ), simply requires proving s 0 ✓ s. The soundness condition of the operator is that:

v S (s, s 0 ) = true =) γ S (s) ✓ γ S (s 0 )
The join operator t S and the widening operator O S take two set abstract elements and aim to compute a common weakening of them. In addition to that, the widening operator O S ensures termination of any sequence of abstract iterates. As an example, joining (resp., widening) singleton set abstract elements s and s 0 , i.e., t S (s, s 0 ) (resp., O S (s, s 0 )), simply requires computing the intersection s \ s 0 . The soundness condition of the joining operator t S (which is similar for

O S ) is that: t S (s l , s r ) = s o =) γ S (s l ) ✓ γ S (s o ) ^γS (s r ) ✓ γ S (s o )

Set Domains

Set domains are needed in constructing some complex program analyses [CCR14, CCS13, LRC15] to reason about unbounded collections of elements. Different set domains usually precisely express different predicates. Several set domains have been developed including a linear set domain, a BDD-based set domain and a QUIC-graph based set domain.

• The linear set domain focuses on reasoning about linear partitions of sets and is mainly designed to be precise enough and efficient for the analysis of shared data structures in the MemCAD analyzer.

• The BDD-based set domain focuses on reasoning about symbolic set predicates, i.e., non content related set predicates, and was designed by Arlen Cox for automatic analysis of open objects in dynamic language programs [START_REF] Cox | Automatic analysis of open objects in dynamic language programs[END_REF]; it was later also used in the MemCAD analyzer. The BDD-based set domain is more general and precise than the linear domain, but less reliable in terms of scalability.

• The QUIC-graphs based set domain [START_REF] Cox | Quic graphs: Relational invariant generation for containers[END_REF] uses directed hyper-graph data structures to represent constraints of the form E 1 \ . . . \ E n ✓ F 1 [ . . . [ F m on subset relations and contents of set variables. It is used in automatically inferring relations between the set of values stored in containers such as arrays, lists, dictionaries, and sets.

Moreover, precision and scalability of set domains can also be improved by an equality domain functor [START_REF] Cox | Abstract domains and solvers for sets reasoning[END_REF] which handles equality constraints externally and prevents them being seen by the underlying abstract domains, and a packing domain functor [START_REF] Cox | Abstract domains and solvers for sets reasoning[END_REF] which dynamically reduces a complex abstraction to a set of small clusters. In this section, we only present the linear set domain and the BDD-based set domain in detail and refer the readers to [START_REF] Cox | Abstract domains and solvers for sets reasoning[END_REF] for more set abstract domains or techniques to improve the performance of set abstract domains.

Linear Set Domain

Linear set abstractions aim to precisely abstract set predicates that are composed of linear set constraints of the form E 0 = {v 0 , . . . , v n } ] E 1 ] . . . ] E m , inclusion constraints of the forms E ✓ F and v 2 E , and equality constraints of the form E = F . Such constraints are very useful in the analysis of sharing data structures and allow quite a straightforward normalization representation of set abstractions, for which efficient algorithms are possible.

Definition 5.2 (Linear set abstract elements). A linear set abstract element is either >, ? or a tuple (c l , c e , c i ) defined by the following grammar:

s 2 S ::= > | ? | (c l , c e , c i ) c l ::= true | E 0 = {v 0 , . . . , v n } ] E 1 ] . . . ] E m | c l ^cl c e ::= true | E = F | c e ^ce c i ::= true | v 2 E | F ✓ E | c i ^ci
The linear formula c l expresses linear set equality constraints over set variables and is implemented as a map, where each set variable may appear at most once as the left-hand side. Linear set equality constraints are always normalized in the abstraction by expanding nested linear equality constraints, for example, the set constraint

E = E 1 ] E 2 ^E2 = E 3 ] E 4 is rewritten as E = E 1 ] E 3 ] E 4 ^E2 = E 3 ] E 4 in c l of
a linear set abstract element. Moreover, the emptiness property of a set variable E can also be expressed in c l by mapping E to an empty set. The equality formula c e and the inclusion formula c i respectively express equality constraints and inclusion constraints.

Example 5.2 (A precise linear set abstract element). The concrete states satisfying set predicate E ✓ F ^F = {↵} ] F 2 ] F 3 ^δ 2 E can be precisely abstracted by the linear set abstract element (c l , c e , c i ), where:

c l = (F = {↵} ] F 2 ] F 3 ) c e = true c i = (E ✓ F ^δ 2 F ^δ 2 E )
Example 5.3 (An imprecise linear set abstract element). The concrete states satisfying set predicate E ✓ F ^F = {↵} [ F 2 [ F 3 ^δ 2 E can be abstracted by the linear set abstract element (c l , c e , c i ), where

c l = true c e = true c i = (E ✓ F ^δ 2 F ^↵ 2 F ^F2 ✓ F ^F3 ✓ F ^δ 2 E )
We note that, as the linear set domain cannot express non disjoint union, the set constraint

F = {↵} [ F 2 [ F 3 is weakened into ↵ 2 F ^F2 ✓ F ^F3 ✓ F .
Concretization. As any linear set abstract element can be translated into a conjunction of set constraints, the concretization γ S 2 S ! P(V) of the linear set abstract element can thus be defined as sets of concrete states that satisfy the corresponding set predicate. The abstract operation isbot S (s) simply returns true if s is ?.

The abstract operation prove S (s, c T ) encodes the set predicate c T into an equivalent normal form predicate of s and then checks that s includes the normal form predicate.

The abstract operation guard S (s, c T ) can simply enforce inclusion constraints into c i and equality constraints into c e . Linear constraints are first normalized by expanding nested linear constraints and then enforced into c l . For set predicates that are not of these forms, the operation then weakens the predicates into these forms, where precision may be lost. When a set variable E is already constrained in the linear map c l , e.g., c l = (E = {↵} ] F ), the guard S operation cannot add another linear constraint of E in c l , where weakening may be also necessary. Let f 2 V ]T ! P(V ]T ) be a mapping from set variables (resp., abstract value variables) of set abstract element s to sets of other set variables (resp., abstract value variables). The abstract rename operation rename S (s, f) then simply replaces any set variable E (resp., abstract value variable v) of set abstraction s by another set variable F 2 f(E ) (resp., v 0 2 f(v)) that it should be renamed to. When a set variable E is mapped to more than one set variable, e.g., E 1 , E 2 2 f(E ), equality between set variables E 1 and E 2 should be established in the resulting abstract element. Moreover, set variables of s that cannot be renamed are dropped.

Given s = (c l , c e , c i ) and s 0 = (c l 0 , c e 0 , c i 0 ), the inclusion checking operation v S (s, s 0 ) returns true when dom(s 0 ) = dom(s) and the set of constraints expressed by (c l 0 , c e 0 , c i 0 ) is a subset of the set of constraints expressed by (c l , c e , c i ). Finally, t S and O S over-approximate set abstract , c e 0 , c i 0 ) with dom(s) = dom(s 0 ), the over-approximation (c l 00 , c e 00 , c i 00 ) of them is the intersection of the set of constraints expressed by (c l , c e , c i ) and (c l 0 , c e 0 , c i 0 ). Moreover, as the number of constraints decreases during the over-approximation operation, the widening operation guarantees termination.

t S ((c l , c e , c i ), (c l 0 , c e 0 , c i 0 )) = (F = E 1 ] E 2 , c e , c i )

BDD-based Set Domain

In this section, we briefly introduce a set abstract domain based on binary decision diagrams (BDDs) [START_REF] Somenzi | Binary decision diagrams[END_REF] and refer the readers to [START_REF] Cox | Binary-Decision-Diagrams for Set Abstraction[END_REF] for more details. The core idea of the set domain is to encode set predicates into their Boolean algebraic forms and then represent Boolean algebraic forms as binary decision diagrams. We note that, set content reasoning, e.g., ↵ 2 E , cannot be supported directly by BDD-based set abstract domain, yet can be supported by a reduced product of BDD-based set abstract domain and the singleton set abstract domain presented in Example 5.1. Therefore, in the following, we only consider set predicates among set variables.

Encoding set predicates. A powerset with basic set operations forms a Boolean algebra with the join operator _ being the set union operator [, the meet operator ^being the the set intersection operator \, the negative operator ¬ being set complement operator, false being the empty set ; and true being the universal set. Therefore, we can encode any set predicate into its Boolean algebra formula with the translation function tr E presented in Figure 5.3. Generally, the translation is the literal replacement of set operations with the corresponding Boolean operation.

As set predicates may contain disjoint union expressions, a set expression e T is translated into an expression e with a side constraint c, i.e., tr E (e T ) = e, c, where the side constraint c enforces disjoint properties.

BDD-based set abstract elements. Canonical binary decision diagrams (BDDs) are used to canonically and efficiently represent Boolean algebras based on the if-then-else normal form and a total order ≺ of the variables. We define a BDD-based set abstract element as a canonical BDD.

Definition 5.4 (BDD-based set abstract elements). A BDD-based set abstract element is composed of three basic syntactic elements:

s ::= true | false |ITE(E , s 1 , s 2 )
where, true and false represent Boolean constants, and

ITE(E , s 1 , s 2 ) represent Boolean formula E =) s 1 ^¬E =) s 2 .
Example 5.7 (A BDD-based set abstract element). The set predicate E 1 ✓ E 2 Ê2 ✓ E 3 can be encoded as the Boolean algebraic formula E 1 =) E 2 ^E2 =) E 3 . Following the order E 1 ≺ E 2 ≺ E 3 , the Boolean algebraic formula can be represented as the BDD form:

E 1 E 2 E 2 E 3 1 0 0 1 1 1 0 0 1 0 ITE(E 1 , ITE(E 2 , ITE(E 3 , true, false), false), ITE(E 2 , ITE(E 3 , true, false), true) )
Concretization. Conversely, a BDD-based set abstract element can be transferred into an equivalent set predicate and the abstract element can thus be concretized into a set of valuation functions satisfying the set predicate. Definition 5.5 (Concretization). Let V be the set of all values. Let tr R be a function mapping a BDD-based set abstract element into a set expression:

tr R (true) = V tr R (false) = ; tr R (ITE(E , s 1 , s 2 )) = (E c [ tr R (s 1 )) \ (E [ tr R (s 2 ))
The concretization of a BDD-based set abstract element s is then defined as a set of valuations, where the semantics of the set expression tr R (s) is the set of all values V :

γ S (s) = {µ | Jtr R (s)Kµ = V)}
Abstract operators. Typical BDD implementations provide the basic logical operations ^, _, ¬, universal and existential quantifications 9, 8, and the validity checking functionality, from which the abstract operations can be derived straightforwardly. Thus, for the sake of simplicity, we only present a part of operations.

The operation project S (s, E ) uses existential quantifier elimination provided by BDDs to drop variable E :

project S (s, E ) = 9E , s
The operations prove S and v S simply rely on the validity checking functionality provided by BDDs.

The operations t S and O S can be implemented with the _ operation provided by BDDs, which is precise and does not need any rules or heuristics:

t S (s 1 , s 2 ) = O S (s 1 , s 2 ) = s 1 _ s 2 Chapter 6

Static Analysis Algorithms for Unstructured Sharing Abstractions

This chapter proposes a static analysis algorithm to infer precise properties of shared data structures. Specifically, Section 6.1 recalls the abstract domain; Section 6.2 presents some basic abstract transfer functions and a novel operation, i.e., non-local unfolding. Non-local unfolding enables "jumping" over inductive predicates. Section 6.3 shows algorithms that allow abstract memory regions to be conservatively folded into inductive predicates with inductive set parameters synthesis. Non-local unfolding and inductive set parameters synthesis are the new notions of the analysis algorithm. Finally, Section 6.5 reports on an empirical evaluation of the analysis algorithm.

Abstract states

In Section 4.2, we define an abstract state as a pair (g, c) made up of an abstract shape graph g 2 G and a value-set abstract element c 2 C. The concretization of an abstract memory state m = (g, c) 2 M ! is defined as a set of memory states such that for each memory state, a valuation of abstract value variables and set variables can be found that satisfy all constraints from g and c:

γ M! (g, c) = {(µ dX & , σ) 2 M | 9µ 2 γ C (c), (σ, µ) 2 γ G (g)}
Abstract shape graphs describe the basic structure of memory states and are defined as separating products of points-to predicates of the form ↵ • f 7 ! β, inductive predicates of the form ↵ • ind( Ẽ ), and segment predicates of the form ↵

• ind( Ẽ ) ⇤= β • ind( Ẽ ).
A value-set abstract domain C reasons about both numerical predicates and set predicates. It is built as a reduced product of a numerical domain and a set domain that is presented in Chapter 5, i.e., c 2 C ::= N ⇥ S, and thus each abstract operation of the value-set abstract domain can be simply passed to the underlying numerical domain and set domain. Let C denote the conjunction of numerical predicates C V and set predicates C T , the signature of value-set domains is defined as:

abstraction c 2 C bottom check isbot C 2 C ! {true, false} prove prove C : C ⇥ C ! {true, false} guard guard C : C ⇥ C ! C remove remove C : C ⇥ V ] T ! C rename rename C : C ⇥ (V ] T ! P(V ] T )) ! C join t C : C ⇥ C ! C widen O C : C ⇥ C ! C inclusion check v C : C ⇥ C ! {true, false}

Computation of Abstract Post-conditions

We have extended the abstract memory states defined in Section 2.3 by replacing numerical abstractions with value-set abstractions. We now need to extend the abstract operators and unfolding presented in Section 2.4 in order to design a forward abstract interpretation to compute sound abstract post-conditions from abstract pre-conditions. Moreover, the new abstract states allow a novel operator, namely non-local unfolding, which we highlight in this section.

Abstract Operators and Unfolding

Abstract operators. The basic abstract operations include the abstract store operations read, write, create and delete, and abstract arithmetic operations, e.g., J+K, J==K. These operations can be defined very similarly to those defined in Section 2.4 by simply replacing numerical abstract operations with corresponding value-set abstract operations. For simplicity, we only show here the abstract store operation create and the abstract arithmetic operation J==K.

The abstract store operation create 2

N ⇥ M ! ! (V ⇥ M ! ) 2 ] {?, >} is formalized as: create(n, (g, c)) returns (↵, (g ⇤ ↵ 7 ! ↵ 1 ⇤ . . . ⇤ ↵ + 4(n -1) 7 ! ↵ n , c
)) and (↵, (g, guard C (c, ↵ = 0))

The abstract operation create(n, (g, c)) returns a pair of abstract states respectively corresponding to a successful allocation of n cells and a failure case. In the second case, the symbolic address ↵ is constrained to be 0 in the value-set abstraction by the abstract operation guard C (c, ↵ = 0). and(false, (guard G (g, v

The abstract arithmetic operation

J==K 2 V ⇥ V ⇥ M ! ! ({true, false} ⇥ M ! ) 2 ] {?, >} is formalized as: J==K(v 1 , v 2 , (g, c)) = (true, (guard G (g, v 1 = v 2 ), guard C (c, v 1 = v 2 ))),
1 6 = v 2 ), guard C (c, v 1 6 = v 2 )))
The abstract operation J==K(v 1 , v 2 , (g, c)) takes two abstract values v 1 , v 2 and an abstract state (g, c) 2 M ! as inputs, and respectively enforces equality and dis-equality conditions of v 1 and v 2 on the abstract state (g, c).

Chapter 6. Static Analysis Algorithms for Unstructured Sharing Abstractions 83

&s The soundness condition of the abstract operation can be similarly defined as in Section 2.4 and is omitted here.

↵ 1 edges(E ) ↵ 1 6 = 0 (a) Folded "pre"-shape m ↵ 1 6 = 0 ^↵2 6 = 0 ^↵2 2 E &s ↵ 1 ↵ 3 ↵ 2 dest next edges(E ) (b) "Unfolded"-shape m 0
Unfolding. When abstract operations involve memory regions that are summarized in inductive or segment predicates, the analysis needs to unfold summary predicates to expose memory regions on which store operations act. As an example, reading the abstract value denoted by s -> next of the abstract state shown in Figure 6.1(a) needs to unfold the inductive predicate

↵ 1 • edges(E ).
The principles of unfolding inductive predicates and segment predicates are very similar, as presented in Section 2.4.2, thus, we only formalize the unfolding of inductive predicates. Generally, unfolding an inductive predicate in one abstract state follows its inductive definition to produce a disjunction of cases, where one case is for one inductive rule. Following the inductive definitions presented in Section 4.1, each inductive rule comprises a heap part and a pure part, and the pure part comprises numerical constraints and also set constraints, thus, the unfolding replaces the inductive predicate with the heap part in the abstract shape graph, and enforces the pure constraints in the value-set abstraction. Symbolic variables and set variables that are not parameters of the inductive definition are all existential variables that need to be replaced by fresh variables of the abstract state. Definition 6.1 (Unfolding). Given inductive definition ↵ • ind(E ) ::= W k i=1 (F Heap,i , F Pure,i ), the unfolding operation unfold 2 V ⇥ M ! ! D is defined as:

unfold(v, (g ⇤ v • ind(F ), c)) = W k i=1 (g ⇤ F 0 Heap,i , guard C (c, F 0 Pure,i )
where, dom(F 0

Heap,i , F 0 Pure,i ) \ dom(g, c) = {v, F } and 9f 2 V ] T ! V ] T , {↵ 7 ! v, E 7 ! F } ✓ f, F 0 Heap,i = F Heap,i • f, F 0 Pure,i = F Pure,i • f.
Example 6.1 (Unfolding). Let us consider unfolding the inductive predicate

↵ 1 •edges(E ) m 0 : β ↵ l s (E ) β 2 E m 1 : β ↵ l s (E 0 ) l s (E 1 ) β 2 E 1 E = E 0 ] E 1
↵ • edges(E ) ::= (emp, ↵ = 0) _ (↵ • dest 7 ! β ⇤ ↵ • next 7 ! γ ⇤ γ • edges(E ), ↵ 6 = 0 ^β 2 E ^β 6 = 0)
Unfolding the inductive predicate ↵ 1 • edges(E ) with the first inductive rule produces a bottom abstract state ?, since the abstract state m contains constraint ↵ 1 6 = 0 in the valueset abstraction component. Unfolding ↵ 1 •edges(E ) with the second inductive rule produces the abstract state presented in Figure 6.1(b), where symbolic variables ↵, β, γ of the rule have been renamed to ↵ 1 , ↵ 2 , ↵ 3 respectively in the abstract state. That is:

unfold(↵ 1 , (&s 7 ! ↵ 1 ⇤ ↵ 1 • edges(E ), c)) = &s 7 ! ↵ 1 ⇤ ↵ 1 • dest 7 ! ↵ 2 ⇤ ↵ 1 • next 7 ! ↵ 3 ⇤ ↵ 3 • edges(E ), guard C (c, ↵ 2 6 = 0 ^↵2 2 E )
Theorem 6.1 (Soundness of unfold). The unfolding operator unfold is sound with respect to the soundness Condition 2.7, i.e.,

8m 2 M ! , unfold(v, m) = m 1 _ . . . _ m n =) γ M! (m) ✓ γ M! (m 1 ) [ . . . [ γ M! (m n )
Proof. The soundness can be easily derived from the concretization rule of inductive predicates presented in Figure 4.3. ⌅

Non-local Unfolding

Limitations of standard unfolding. The unfolding case studied so far is quite straightforward as the node at which the inductive predicate should be unfolded is well specified by the transfer function (e.g., ↵ 1 in Figure 6.1(a)). However, the above unfolding cannot work when analyzing an instruction reading c -> id (line 10 of the graph traversal function shown in Figure 3.5) from the abstract state below:

m 5 : h ↵ ↵ 0 ↵ 00 β s β 0 c δ next id edges edges(E ) dest next nodes(E , F 1 ) edges(E ) ↵ 6 = 0 ^β 6 = 0 ^β0 6 = 0 ^δ 6 = 0 ^E ✓ F ^F = {↵} ] F 1 ^δ 2 E Chapter 6.

Static Analysis Algorithms for Unstructured Sharing Abstractions 85

In the abstract state c points to δ in the abstract level, but node δ is not the origin of a points-to predicate nor of an inductive predicate that could be unfolded.

Principle of non-local unfolding. Intuitively, δ could be any node in the graph and thus we expect the abstract memory state to reflect this. This intuitive idea is formalized as follows: the second parameter of nodes is a head parameter (Section 4.3), and the side predicates express the fact that δ 2 {↵} ] F 1 , where F 1 appears as a second parameter of the nodes predicate in the shape, which allows δ to be localized. This principle is a direct consequence of a property of head parameters: Theorem 6.2 (Non-local unfolding principle). Let ind be a single parameter inductive, such that

↵ • ind(E ) `E : head. Let (σ, µ) 2 γ G (↵ • ind(E )) such that µ(β) 2 µ(E ). Given E 0 , E 1 fresh set variables, µ can be extended into µ 0 , such that (σ, µ 0 ) 2 γ G (↵ • ind ⇤= (E 0 ) β • ind ⇤ β • ind(E 1 )), µ 0 (E ) = µ 0 (E 0 ) ] µ 0 (E 1 ) and µ 0 (β) 2 µ 0 (E 1 ).
Proof. According to the definition of head parameters,

↵ • ind(E ) `E : head =) 8(σ, µ) 2 γ G (↵ • ind(E )), µ(E ) = ; _ µ(↵) 2 µ(E )
As µ(β) 2 E indicates µ(E ) 6 = ;, we then need to prove that for all 1  |µ(E )|, the theorem holds:

• if |µ(E )| = 1, we have µ(↵) = µ(β). Let µ 0 = µ ] {E 0 7 ! ;, E 1 7 ! µ(E )}, the theorem obviously holds.
• if |µ(E )| = n + 1, we assume that the theorem holds when |µ(E )|  n.

In the case where µ(β) = µ(↵), let µ 0 = µ ] {E 0 7 ! ;, E 1 7 ! µ(E )}, the theorem obviously holds.

In the case where µ(β) 6 = µ(↵), the inductive predicate ↵ • ind(E ) can be unfolded as a separating conjunction of a set of inductive calls to ind and other predicates, denoted as

↵ 1 •ind(F 1 ) ⇤ . . . ⇤ ↵ k •ind(F k )
⇤ g, such that the disjoint union of {↵} and the arguments of the recursive sub-calls is equal to E , i.e., E = {↵} ] {F 1 , . . . ,

F k } and σ = σ 0 ] . . . ] σ k such that (σ i , µ) 2 γ G (↵ i • ind(F i )).
Let us assume that µ(β)

2 µ(F i ) (1  i  k), since |µ(F i )|  n, µ can be extended to µ 0 i such that (σ i , µ 0 i ) 2 γ G (↵ i • ind ⇤= (X 0 ) β • ind ⇤ β • ind(X 1 )), µ 0 i (F i ) = µ 0 i (X 0 ) ] µ 0 i (X 1 ) and µ 0 i (β) 2 µ 0 i (E 1 ). Let µ 0 = µ 0 i ] {E 1 7 ! µ 0 i (X 1 ), E 0 7 ! µ(E ) \ µ 0 i (X 1 )}, we get: (σ, µ 0 ) 2 γ G (↵ 1 •ind(F 1 ) ⇤ . . . ⇤ ↵ i •ind ⇤= (X 0 ) β •ind ⇤ β •ind(E 1 )) ⇤ . . . ↵ k •ind(F k ) ⇤ g)
According to the inductive definition, finally we get:

(σ, µ 0 ) 2 γ G (↵ • ind ⇤= (E 0 ) β • ind ⇤ β • ind(E 1 )). ⌅ Figure 6
.2 illustrates this non-local unfolding principle. While theorem 6.2 states the result for inductive definitions with a single set parameter, the result generalizes directly to the case of definitions with several parameters (only the parameter supporting non-local unfolding then needs to be a head parameter). It also generalizes to segments.

Non local unfolding algorithm. Given an inductive definition ↵•ind(E ) ::=

W k i=1 (F Heap,i , F Pure,i ), where ↵ • ind(E ) `E : head, when unfolding at an abstract address ↵ of an abstract state (g, c), the unfolding algorithm first searches for a local unfolding at ↵, that is either a segment or an inductive predicate starting from ↵. When no such local unfolding can be found, the nonlocal unfolding operation unfold nc is then performed. It searches for predicates of the form ↵ 2 {↵ 0 , . . . , ↵ k } ] E 0 ] . . . ] E l , where E 0 , . . . , E l appear as head parameters. When it finds such a predicate, the analysis produces a disjunction of cases, where either ↵ = ↵ i , or where ↵ 2 E i and it performs a non-local unfolding of the corresponding predicate (Theorem 6.2); Application to the computation of post-conditions of assignments. The analysis of an assignment statement proceeds along the following steps:

1. it attempts to transform all l-values to edges and r-values to symbolic variables; 2. when step 1 fails because no points-to edge can be found at offset ↵ • f, it unfolds points-to predicates at ↵ either by local unfolding or non-local unfolding. 3. The unfolding process usually produces a disjunction of cases. Then, the analysis performs the abstract operation write on each unfolded disjunct. Note that failure to fully materialize all required nodes would produce imprecise results, thus, in the absence of information about parameters, the analysis may fail to produce a precise postcondition as it did before. The purpose of non-local unfolding is to avoid imprecise results when dealing with structures with sharing.

Abstract Lattice Operations

While transfer functions unfold inductive predicates, inclusion checking, join and widening operators need to discover valid set parameters so as to fold them back. However, folding turns out to be much harder than unfolding, and the main difficulties for our abstract domian lie in searching for set parameters for folded summary predicates.

Inclusion Checking

As introduced in Section 2.4.4, given two abstract memory states (g l , n l ) and (g r , n r ), the inclusion checking abstract operation v M! attempts to establish that γ M! (g l , n l ) is included in γ M! (g r , n r ).

Original inclusion checking algorithm. The original inclusion checking algorithm of abstract states G ⇥ N presented in [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF] is based on a series of syntactic rewriting rules of abstract shape graphs to establish the inclusion of abstract shape graphs and an implication checking of numerical abstractions to determine whether inclusion does indeed hold. Figure 6.3 shows such a system. The i-pt and i-ind rules state that any points-to and inductive predicates are included in themselves; the same principle actually also applies to segment predicates. The i-sep rule splits abstract shapes according to the separation principle. The i-uf rule unfolds the right hand side shape and tries to match the left-hand side with one of the disjuncts. The i-segind rule applies when trying to compare a segment on the left and an inductive predicate Chapter 6. Static Analysis Algorithms for Unstructured Sharing Abstractions 87

n l `↵ • f 7 ! β v G ↵ • f 7 ! β (i -pt) n l `↵ • ind v G ↵ • ind (i -ind) n l `gl v G g r n l `g0 l v G g 0 r n l `gl ⇤ g 0 l v G g r ⇤ g 0 r (i -sep) g r U (g u , F Pure ) n l `gl v G g u prove N (n l , F Pure ) = true n l `gl v G g r (i -uf ) n l `gl v G β • ind(E ) n l `↵ • ind ⇤= β • ind ⇤ g l v G ↵ • ind (i -segind) n l `gl v G g r n l v N n r (g l , n l ) v M! (g r , n r ) (i -val)
Figure 6.3: Original inclusion checking over shapes and abstract states G ⇥ N on the right, that correspond to the same definition and the same origin. The last rule, i-val, returns true when both the comparison of shapes and of numerical abstractions return true. However, the system cannot be simply extended when summary predicates are extended with set parameters and numerical abstractions are extended with set abstractions. As an example, let us consider proving the inclusion of the following abstract states (↵ • l s (E ) `E : head):

(g l , c l ) : ↵ 1 ↵ 2 ↵ 3 n v l s (E 1 ) ↵ 1 6 = 0 (g r , c r ) : ↵ 1 l s (E 0 ) ↵ 1 6 = 0
According to Figure 6.3, we can apply the i-uf rule: unfolding the inductive predicate ↵ 1 • l s (E 0 ) of g r which produces an identical shape with g l and a set predicate E 0 = {↵ 1 } ] E 1 and proving that c l implies the set predicate by prove C (c l , E 0 = {↵ 1 } ] E 1 ), which apparently returns false. Therefore, the inclusion proof fails. However, the set of concrete memory states abstracted by (g l , c l ) is indeed included in the set of concrete memory states abstracted by (g r , c r ). Though inclusion checking is typically incomplete, we may hope that basic cases still get proved.

Extended inclusion checking algorithm. We extend the original inclusion checking algorithm as presented in Figure 6.4, where we let c 2 C be the conjunction of numerical and set predicates, c dV be the restriction of c to numerical predicates, and c dT be the restriction of c to set predicates. The major difference of the extended system is to collect set predicates c that need to be proved during the inclusion checking process over shapes g l and g r , i.e., c l , c `gl v G g r , and then, compute c 0 l by instantiation of the value of fresh set variables of c l , denoted as

c l , true `↵ • f 7 ! β v G ↵ • f 7 ! β (ei -pt) c l , true `↵ • ind(E ) v G ↵ • ind(E ) (ei -ind) c l , c `gl v G g r c l , c 0 `g0 l v G g 0 r c l , c ^c0 `gl ⇤ g 0 l v G g r ⇤ g 0 r (ei -sep) g r U (g u , F Pure ) c l , c `gl v G g u prove C (c l , F Pure dV ) = true c l , c ^FPuredT `gl v G g r (ei -uf ) c l , c `gl v G β • ind(E ) ↵ • ind(E ) `E : cst c l , c `↵ • ind ⇤= (E ) β • ind ⇤ g l v G ↵ • ind(E ) (ei -segind cst ) E 1 fresh c l , c `gl v G β • ind(E 1 ) ↵ • ind(E ) `E : head c l , c ^E = E 0 ] E 1 `↵ • ind ⇤= (E 0 ) β • ind ⇤ g l v G ↵ • ind(E ) (ei -segind head ) E 6 2 dom(c) 80  i, j  k, 0  p, q  l, (g l , c) =) ↵ i 6 = ↵ j ^↵i 6 2 E p ^Ep \ E q = ; c i guard C (c, E = {↵ 0 , . . . , ↵ k } ] E 0 ] . . . ] E l ) (ei -inst) c l , c `gl v G g r c l i ⇤ c 0 l prove C (c 0 l , c) = true c 0 l v C c r (g l , c l ) v M! (g r , c r ) (ei -val)
c l i ⇤ c 0 l , such that prove C (c 0 l , c) = true.
Inclusion rules for shapes. The ei-pt and ei-ind rules respectively correspond to the i-pt and i-ind rules of the original system, which state that any shape is included in itself and for simplicity is omitted. The ei-sep and ei-uf rules respectively correspond to the i-sep and i-uf rules of the original system. The only difference is that the ei-uf rule only proves unfolded numerical predicates F Pure dV while preserving the unfolded set predicates F PuredT in the proof condition.

The eisegind cst and eisegind head rules correspond respectively to the i-segind rule for the cases of a constant set parameter and a head set parameter when matching segments and inductive predicates. The eisegind cst rule simply requires inductive and segment to share the same set parameter while the eisegind head rule enforces the additiveness of head parameters by choosing fresh E 1 so that

E = E 0 ] E 1 .
Instantiation of fresh set variables. The ei-inst rule instantiates a fresh set variable E by enforcing an equality constraint between the fresh set variable and a set expression {↵ 0 , . . . , ↵ k }] E 0 ] . . . ] E l of non-fresh set variables. We note that a disjoint union expression e T ] e 0 T has a Chapter 6. Static Analysis Algorithms for Unstructured Sharing Abstractions 89 side constraint e T \ e 0 T = ; that needs to be proved for soundness. Specifically, the disjointness can either be proved by the value-set abstraction, i.e., prove C (c l , e T \ e 0 T = ;) = true, or be proved based on the property of the separating conjunction ⇤ and head parameters:

c l , ( E = E 0 ] E 2 ^E2 = {↵ 1 } ] E 1 `vG (ei -segind head ) c l , E 2 = {↵ 1 } ] E 1 `vG (ei-uf ) c l , true `vG (ei-pt && ei-ind) ↵ 1 ↵ 2 ↵ 3 n v l s (E 1 ) ↵ 1 ↵ 2 ↵ 3 n v l s (E 1 ) ↵ 1 ↵ 2 ↵ 3 n v l s (E 1 ) ↵ 1 l s (E 2 ) ↵ 0 ↵ 1 ↵ 2 ↵ 3 n v l s (E 0 ) l s (E 1 ) ↵ 0 l s (E )
• ↵ 1 • f 7 ! β 1 ⇤ ↵ 2 • f 7 ! β 2 ⇤ g =) ↵ 1 6 = ↵ 2 .
• in the case of

↵ • ind(E ) `E : head, ↵ 1 • ind(E 1 ) ⇤ ↵ 2 • ind(E 2 ) ⇤ g =) E 1 \ E 2 = ;. • in the case of ↵ • ind(E ) `E : head, ↵ 1 • ind(E 1 ) ⇤ ↵ 2 • f 7 ! β 2 ⇤ g =) ↵ 2 6 2 E 1 if the inductive definition ↵ • ind(E ) contains a rule r = (F Heap , F Pure ), where F Heap = ↵ • f 7 ! ↵ 0 ⇤ . . . and F Pure = E = {↵} ] . . . ^. . ..
We note that this rule is very important for folding back unfolded predicates into summary predicates with set parameters. Finally, the ei-val rule corresponding to the i-val rule decomposes the inclusion checking of abstract states into the inclusion checking over abstract shapes, the instantiation of fresh set variables, and the implication process over value-set abstractions.

Example 6.2 (Inclusion checking). Figure 6.5 illustrates the inclusion checking algorithm on abstract states (g l , c l ) and (g r , c r ), where g l and g r are the bottom shapes shown in Figure 6.5, and c l and c r are respectively an abstraction of ↵ 1 6 = 0 and true. We recall that the l s definition (presented in Section 4.1) has a head parameter (↵•l s (E ) `E : head), which behaves similarly to nodes (Figure 3.3) in its second parameter. The example resembles inclusion tests run in the analysis of the program shown in Figure 3.5.

The inclusion proof search over shapes starts from the bottom shapes g l and g r , where ↵ 0 90 Chapter 6. Static Analysis Algorithms for Unstructured Sharing Abstractions is the origin of a segment on the left, and of an inductive predicate on the right. Since l s has a head parameter, the eisegind head rule specific to this case applies, and the inclusion test "consumes" the segment, effectively removing it from the left argument, and adding a fresh E 2 variable, such that E = E 0 ] E 2 is added in the proof condition. Then, since ↵ 1 is the origin of points-to predicates on the left and of inductive predicate on the right, the ei-uf rule is applied to unfold the inductive predicate, where the constraint E 2 = {↵ 1 } ] E 1 is added into the proof condition after proving that prove C (c l , ↵ 1 6 = 0) = true. Finally, the algorithm derives that inclusion holds on the shapes after matching three pairs of identical predicates.

Then, the algorithm needs to prove that the condition

E = E 0 ] E 2 ^E2 = {↵ 1 } ] E 1 is implied by c l (dom(c l ) = dom(g l ))
. Since set variables E and E 2 do not exist in c l , the instantiation of E and E 2 is necessary. According to the ei-inst rule, we can first instantiate

E 2 to {↵ 1 } ] E 1 , i.e., c i guard C (c l , E 2 = {↵ 1 } ] E 1
). We note that, the side condition

{↵ 1 } \ E 1 =
; is implied by the abstract shape g l , in which ↵ 1 is the origin of points-to predicates and E 1 is the head parameter of inductive predicate ↵ 2 • l s (E 1 ). Then, similarly we can instantiate E to {↵ 1 } ] E 0 ] E 1 , thus we have:

c 0 l = guard C (guard C (c l , E 2 = {↵ 1 } ] E 1 ), E = {↵ 1 } ] E 0 ] E 1 ) and c l i c 0 l
Indeed, the instantiation of set variables E and E 2 is constructed according to the proof condition c in the bottom rule. Intuitively, when proving c requires an equality constraint between a fresh set variable E and a set expression e T of non-fresh set variables, we instantiate E to e T . Finally, we have (g l , c l ) v M! (g r , c r ) after verifying that prove C (c 0 l , c) = true and c 0 l v C c r .

Theorem 6.3 (Soundness condition of inclusion checking over shapes). If

c l , c `gl v G g r then: 8(σ, µ) ✏ (g l , c l ) 9µ 0 extending µ, µ 0 ✏ c =) (σ, µ 0 ) ✏ g r Proof.
The proof can be derived by induction over inclusion rules of shapes.

• For the ei-pt and ei-ind rules, it obviously holds.

• For the ei-sep rule, for all µ ✏ c l , (σ, µ) ✏ g l and (σ 0 , µ) ✏ g 0 l , according to the condition, 9µ 0 extending µ, µ 0 ✏ c =) (σ, µ 0 ) ✏ g r and µ 0 ✏ c 0 =) (σ 0 , µ 0 ) ✏ g 0 r . Thus, we have

µ 0 ✏ c ^c0 =) (σ ] σ 0 , µ 0 ) ✏ g r ⇤ g 0 r .
• For the ei-uf rule, for all µ ✏ c l and (σ, µ) ✏ g l , according to the condition c l , c `gl v G g u , 9µ 0 extending µ, µ 0 ✏ c =) (σ, µ 0 ) ✏ g u . According to prove C (c l , F Pure dV ) = true, 8µ 0 extending µ, µ 0 ✏ F Pure dV . As g r U (g u , F Pure ) and F Pure = F Pure dV ^FPuredT , according to the concretization rule in Figure 4.3, we have

9µ 0 extending µ, µ 0 ✏ c FPuredT =) µ 0 ✏ F Pure ^(σ, µ 0 ) ✏ g u =) (σ, µ 0 ) ✏ g r .

Chapter 6. Static Analysis Algorithms for Unstructured Sharing Abstractions 91

• For the eisegind cst rule, for all µ ✏ c l and (σ, µ)

✏ ↵ • ind ⇤= (E ) β • ind and (σ 0 , µ) ✏ g l , according to the condition c l , c `gl v G β • ind(E ), 9µ 0 extending µ, µ 0 ✏ c =) (σ 0 , µ 0 ) ✏ β•ind(E ). Thus, 9µ 0 extending µ, µ 0 ✏ c =) (σ]σ 0 , µ 0 ) ✏ ↵•ind ⇤= (E ) β•ind ⇤ β•ind(E ).
According to Theorem 4.1, 9µ 0 extending µ, µ 0 ✏ c =) (σ ] σ 0 , µ 0 ) ✏ ↵ • ind(E ).

• For the eisegind head rule, for all µ ✏ c l and (σ, µ)

✏ ↵•ind ⇤= (E 0 ) β•ind and (σ 0 , µ) ✏ g l , according to the condition c l , c `gl v G β • ind(E 1 ), 9µ 0 extending µ, µ 0 ✏ c =) (σ 0 , µ 0 ) ✏ β • ind(E 1 ). Thus, 9µ 0 extending µ, µ 0 ✏ c =) (σ ] σ 0 , µ 0 ) ✏ ↵ • ind ⇤= (E 0 ) β • ind ⇤ β • ind(E 1 ). According to Theorem 4.2, 9µ 0 extending µ, µ 0 ✏ c ^E = E 0 ] E 1 =) (σ ] σ 0 , µ 0 ) ✏ ↵ • ind(E ).
⌅ Theorem 6.4 (Soundness condition of instantiation). Given (g, c), if c i c 0 then:

8(σ, µ) ✏ (g, c), 9µ 0 extending µ, (σ, µ 0 ) ✏ (g, c 0 ) Proof. For all (σ, µ) ✏ (g, c), 80  i, j  k, 0  p, q  l, µ(↵ i ) 6 = µ(↵ j ) ^µ(↵ i ) 6 2 µ(E p ) μ(E p ) \ µ(E q ) = ;. Thus, let µ 0 = µ ] [E 7 ! {µ(↵ 0 ), . . . , µ(↵ k )} ] µ(E 0 ) ] . . . ] µ(E l )], we have (σ, µ 0 ) ✏ (g, guard C (c, E = {↵ 0 , . . . , ↵ k } ] E 0 ] . . . ] E l )).
⌅ Theorem 6.5 (Soundness condition of inclusion checking). Given (g l , c l ) and (g r , c r ),

if (g l , c l ) v M! (g r , c r ) then γ M! (g l , c l ) ✓ γ M! (g r , c r )
Proof. According to Theorem 6.4 and c l i ⇤ c 0 l , we have 8(σ, µ) ✏ (g l , c), 9µ 0 extending µ, (σ, µ 0 ) ✏ (g l , c 0 l ). As prove C (c 0 l , c) = true, c 0 l v C c r , and c l , c `gl v G g r , according to Theorem 6.3, we get 8(σ, µ) ✏ (g l , c),

9µ 0 extending µ, µ 0 ✏ c ^µ0 ✏ c r ^(σ, µ 0 ) ✏ g r .
Therefore, we get 8(σ, µ) ✏ (g l , c), 9µ 0 extending µ, (σ, µ 0 ) ✏ (g r , c r ). ⌅

Joining and Widening

As introduced in Section 2.4.4, the joining and widening abstract operations t M! and O M! input two abstract memory states m l and m r and return an over-approximation of them

m o , that is γ M! (m l ) ✓ γ M! (m o ) and γ M! (m r ) ✓ γ M! (m o ).
In addition to that, the widening operator will enforce termination, that is, any sequence of iterations of the widening operator will eventually become stationary. A basic version of the joining and widening algorithm is formalized in [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF], where in the shape domain G, joining and widening rely on the same algorithm. Here we extend the algorithm so as to handle set parameters. • the ej-weak rule applies when either input contains an inductive predicate and the other input contains a region that can be subsumed by the same inductive predicate proved by inclusion checking. Constraints over set parameter E may be added after the inclusion checking. In particular, in the case of a head set parameter, these constraints should capture the linearity over the head set parameter. The same principle also applies to segment predicates.

(c l , true), (c r , true) `↵ • f 7 ! β t G ↵ • f 7 ! β = ↵ • f 7 ! β (ej -pt) (c l , E = E 1 ), (c r , E = E 2 ) `↵ • ind(E 1 ) t G ↵ • ind(E 2 ) = ↵ • ind(E ) (ej -ind) c r , c r `gr v G ↵ • ind(E ) (c l , E = E 1 ), (c r , c r ) `↵ • ind(E 1 ) t G g r = ↵ • ind(E ) (ej -weak) c l , c l `gl v G ↵ • ind ⇤= (E ) β • ind c r =) ↵ = β ↵ • ind(E ) `E : head (c l , c l ), (c r , E = ;) `gl t G emp = ↵ • ind ⇤= (E ) β • ind (ej -intro head ) c l , c l `gl v G ↵ • ind ⇤= (E ) β • ind c r =) ↵ = β ↵ • ind(E ) `E : cst (c l , c l ), (c r , true) `gl t G emp = ↵ • ind ⇤= (E ) β • ind (ej -intro cst ) (c l , c l ), (c r , c r ) `gl t G g r = g o (c l , c 0 l ), (c r , c 0 r ) `g0 l t G g 0 r = g 0 o (c l , c l ^c0 l ), (c r , c r ^c0 r ) `gl ⇤ g 0 l t G g r ⇤ g 0 r = g o ⇤ g 0 o (ej -sep) (c l , c l ), (c r , c r ) `gl t G g r = g o 8i 2 {l, r}, c i i ⇤ c 0 i ^c0 i =) c i c o = c 0 l t C c 0 r (g l , c l ) t M! (g r , c r ) = (g o , c o ) (ej -val)
• the ejintro head and ejintro cst rules apply when either input contains a region subsumed by a segment between ↵ and β, and ↵ = β in the other input which corresponds to an empty segment. We note that since set parameter E is fresh, the joining algorithm needs to rely on both the inclusion checking algorithm to discover what E actually represents on one side and on the property of the set parameter (head or constant) on the other side. Specifically, when ind `E : head, the set parameter E of the empty segment is enforced to be empty, i.e., E = ;, as shown in the jintro head rule, and in the case of ind `E : cst, no new constraint is added, as shown in the jintro cst rule.

Finally, the ej-val rule instantiates fresh set variables in both value-set abstract elements c l and c r based on set constraints c l and c r collected during the shape joining and indirectly stemming from the constant or head kind of the set parameters, i.e., c l i ⇤ c 0 l and c r i ⇤ c 0 r , and then joins the enriched value-set abstract elements c o = c 0 l t C c 0 r after proving the soundness condition

c 0 l =) c l ^c0 r =) c r .
94 Chapter 6. Static Analysis Algorithms for Unstructured Sharing Abstractions

(c l , X 0 = F ), (c r , X 0 = F 1 ) s ↵ 1 nodes(E , F ) t G s ↵ 1 nodes(E , F 1 ) = s ↵ 1 nodes(E , X 0 ) (ej-ind) (c l , X 1 = ;), (c r , X 1 = {↵ 0 } ] F 0 ) s ↵ 1 c ↵ 0 t G c ↵ 0 s ↵ 1 next id edges nodes(E , F 0 ) edges(E ) = c ↵ 0 s ↵ 1 nodes(E , X 1 ) (ej -intro head &&ej -intro cst ) (c l , ( X 0 = F ^X1 = ;
), (c r , Initially, both input shapes contain nodes inductive predicates at ↵ 1 , therefore the ejind rule can be applied to output a nodes inductive predicate. The first parameter is constant, and thus is equal to E everywhere. The second parameter is a head parameter, so a new set variable X 0 is introduced, and c l (resp., c r ) is enriched with constraint X 0 = F (resp., X 0 = F 1 ).

( X 0 = F 1 ^X1 = {↵ 0 } ] F 0 ) s ↵ 1 c ↵ 0 nodes(E , F ) t G c ↵ 0 s ↵ 1 next id edges nodes(E , F 0 ) nodes(E , F 1 ) edges(E ) = c ↵ 0 s ↵ 1 nodes(E , X 1 ) nodes(E , X 0 ) (ej-sep) (ej-val) ↵ 0 = ↵ 1 ^E = F s ↵ 1 c ↵ 0 nodes(E , F ) t M! E = {↵ 0 } ] F 0 ] F 1 c ↵ 0 s ↵ 1 next id edges nodes(E , F 0 ) nodes(E , F 1 ) edges(E ) = E = X 0 ] X 1 c ↵ 0 s ↵ 1 nodes(E , X 1 ) nodes(E , X 0 )
Then, the ejintro head and ejintro cst rules are applied to introduce a segment between ↵ 0 and ↵ 1 as constraint ↵ 0 = ↵ 1 is indicated by the left value-set abstraction c l . Again, the constant parameter is equal to E everywhere. In addition, set variable X 1 is introduced as the second parameter. On the left, constraint X 1 = ; is added. On the right, the inclusion checking discovers constraint

X 1 = {↵ 0 } ] F 0 .
Finally, rule ej-sep combines the joining result of the above rules, which leads to the final joining shape. In addition, rule ej-val instantiates fresh set variables X 0 and X 1 in c l and c r according to the set constraints collected during the shape joining and then computes the final value-set abstract element as an abstraction of X 1 = {↵ 0 } ] F 0 . Theorem 6.6 (Soundness of join). Given (g l , c l ) and (g r , c r ), if

(g l , c l ) t M! (g r , c r ) = (g o , c o ) then: γ M! (g l , c l ) ✓ γ M! (g o , c o ) ^γM! (g r , c r ) ✓ γ M! (g o , c o )
Proof. According to the ej-val rule, let us assume (c l , c l ), (c r , c r ) `gl t G g r = g o , 8i 2 {l, r},

c i i ⇤ c 0 i ^c0 i =) c i and c o = c 0 l t C c 0 r . We first need to prove that (c l , c l ), (c r , c r ) `gl t G g r = g o =) (c l , c l ) `gl v G g o ^(c r , c r ) `gr v G g o
This can be proved by induction over the joining rules over shapes.

Then, according to the soundness condition of Theorem 6.3 and Theorem 6.4, we can get:

8i 2 {l, r}, 8(σ, µ) ✏ (g i , c i ), 9µ 0 extending µ, µ 0 ✏ c i ^µ0 ✏ c 0 i ^(σ, µ 0 ) ✏ g o Finally, according to the soundness condition of the operator t C , 8i 2 {l, r}, 8(σ, µ) ✏ (g i , c i ), 9µ 0 extending µ, (σ, µ 0 ) ✏ g o ^µ0 ✏ c o ⌅
Widening. The widening operator O M! follows the same rewriting rules on abstract shape graphs, but applies a widening operator O C on value-set abstractions instead of t C . That is,

(c l , c l ), (c r , c r ) `gl t G g r = g o 8i 2 {l, r}, c i i ⇤ c 0 i ^c0 i =) c i c o = c 0 l O C c 0 r (g l , c l )O M! (g r , c r ) = (g o , c o )
96 Chapter 6. Static Analysis Algorithms for Unstructured Sharing Abstractions Theorem 6.7 (Widening). The operator O M! is a widening operator on M ! .

Proof. Based on Theorem 6.6, the soundness of the operator O M! can be proved easily.

The property that the operator O M! can ensure convergence is originally proved in [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF]. The core idea is that the number of edges of g o will be stable:

• the number of points-to edges and inductive edges of g o is limited by the number of points-to edges and inductive edges in both inputs.

• the ej-intro rule may introduce segment edges, but this rule can only be applied when a pair of input nodes are equal, and thus it can not be applied more than a fixed number of times.

Once the abstract shape is stable, the value-set abstract element will eventually be stable since O C is a widening operator over C. ⌅

Soundness of The Analysis

Finally, with all the sound underlying abstract operations, we can build an analysis that inputs inductive definitions as parameters, a C program, and a pre-condition, and it automatically computes an abstract post-condition. The analysis is implemented by composing abstract transfer functions of each program statement. Each abstract transfer function inputs an abstract state and computes an abstract post-state that is sound with respect to the abstract semantics of the program statement shown in Figure 2.7. Thus, the analysis is sound with respect to the abstract semantics of programs, shown in Theorem 2.1.

Implementation and Experimental Evaluation

We implemented inductive definitions with set predicates into the MemCAD static analyzer [TCR13, TCR14] and extended abstract operations of the analyzer to handle set variables and set predicates. The analyzer takes a set abstract domain (Chapter 5) as a parameter to represent set constraints and a numerical domain [START_REF] Bor-Yuh | Modular construction of shape-numeric analyzers[END_REF] as a parameter to represent numerical constraints.

In the following, we consider two set abstract domains:

• a BDD-based set domain (Section 5.2.2) that is based on an encoding of set constraints into BDDs, and utilizes a BDD library [Fil]. We call this domain "BDD" in the results table; • a linear set domain (Section 5.2.1) that relies on a compact representation of constraints of the form E i = {↵ 0 , . . . , ↵ n } ] F 0 ] . . . ] F m as well as set equalities, inclusion and membership constraints. We call this domian "LIN" in the results table, since the main set constraints expressed here are of "linear" form. For the numerical domain, we consider a numerical domain that is obtained as a reduced product of a numerical domain that only reasons about equalities and dis-equalities and the convex polyhedra domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] supported by the Apron library [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]. All the abstract domains were implemented in OCaml, and integrated into the MemCAD static analyzer. We want to assess: (1) whether the analysis achieves the verification of structure preservation in the presence of sharing, and (2) whether set domains are sufficiently precise and provide scalability, (3) whether the efficiency of the extended memory abstract domain is preserved compared to the original memory abstract domain presented in Sections 2.3 and 2.4.

Therefore, we parameterize the analysis with the inductive definitions of adjacency lists shown in Figure 3.3. We ran the analysis on a basic graph library, specifically chosen to assess the handling of shared structures (addition or removal operations, structure traversals, and traversals following paths, including the program of Figure 3.5). For each program, we input a pre-condition that abstracts all the valid input data structures of the program, and a postcondition that needs to be verified by the analysis for proving data structure preservation. The results of the analysis are presented in Table 6.1.

As shown in the "Property" columns, in all cases, the analysis with both set domains successfully establishes memory safety (absence of null / dangling pointer dereferences), structural preservation for the graph modifying functions and traversal functions. Note that, in the case of path traversals, memory safety requires the analysis to localize the cursor as a valid graph node, at all times (the strongest set property, captured by the graph inductive definitions of Figure 3.3). As an example, we show in Figure 6.9 the invariants computed during the first loop iteration of the analysis of the random graph path traversal program of Figure 3.5 and in Figure 6.10 the invariants obtained after reaching an abstract post-fixpoint.

Both the BDD-based set domain and the linear set domain are sufficiently precise to analyze the benchmarks of Table 6.1. However, the linear set domain is more efficient than the BDDbased set domain as shown in the "Set" columns which are the analysis times spent on the set domain. Yet the BDD-based set domain proves to be inefficient in this situation and takes up most of the analysis time for three reasons: (1) it keeps properties that are not relevant to the analysis and (2) renaming set variables (required after joins) necessitates full re-computation of BDDs. In contrast, the linear set domain is tailored for the predicates required in the analysis, and produces very quick analysis run-times. (3) BDDs may need more iterations for convergence. To conclude, the linear set domian has reliable performance and predictable precision, which at line 1 c h nodes(E , E ) true

at line 3 c, h ↵ nodes(E , E ) true at line 5 c, h ↵ ↵ 0 s next id edges edges(E ) nodes(E , F ) ↵ 6 = 0 ^E = {↵} ] F at line 9 c, h ↵ ↵ 0 s β next id edges edges(E ) edges(E ) nodes(E , F ) ↵ 6 = 0 ^E = {↵} ] F at line 10 h ↵ ↵ 0 s β c β 0 next id edges dest next edges(E ) edges(E ) nodes(E , F ) ↵ 6 = 0 ^β 6 = 0 ^E = {↵} ] F ^β0 2 E at line 11 (loop body end) c, h ↵ ↵ 0 s β β 0 next id edges dest next edges(E ) edges(E ) nodes(E , F ) ↵ 6 = 0 ^β 6 = 0 ^β0 = ↵ ^E = {↵} ] F ^β0 2 E _ h ↵ ↵ 0 s β β 0 c β 0 ↵ 0 next id edges next id edges dest next edges(E ) edges(E ) edges(E ) nodes(E , X ) nodes(E , X 0 ) ↵ 6 = 0 ^β 6 = 0 ^β0 6 = 0 ^E = {↵} ] X ] {β 0 } ] X 0 ^β0 2 E _ h ↵ ↵ 0 s β c β 0 next id edges dest next edges(E ) edges(E ) nodes(E , F ) ↵ 6 = 0 ^β 6 = 0 ^β0 = 0 ^E = {↵} ] F ^β0 2 E
at line 3 h ↵ c ↵ 0 nodes(E , X ) nodes(E , X 0 ) E = X ] X 0 at line 5 h ↵ c ↵ 0 s nodes(E , X ) next id edges edges(E )
nodes(E , F )

↵ 0 6 = 0 ^E = X ] {↵ 0 } ] F at line 9 h ↵ c ↵ 0 s β nodes(E , X ) next id edges edges(E ) edges(E ) nodes(E , F ) ↵ 0 6 = 0 ^E = X ] {↵ 0 } ] F at line 10 h ↵ ↵ 0 s β c β 0 nodes(E , X ) next id edges dest next edges(E ) edges(E ) nodes(E , F ) ↵ 0 6 = 0 ^β 6 = 0 ^E = X ] {↵ 0 } ] F ^β0 2 E at line 11 (loop body end) h ↵ c ↵ 0 s β β 0 nodes(E , X ) next id edges dest next edges(E ) edges(E ) nodes(E , F ) ↵ 0 6 = 0 ^β 6 = 0 ^β0 = ↵ 0 ^E = X ] {↵ 0 } ] F ^β0 2 E _ h ↵ ↵ 0 s β β 0 c β 0 ↵ 0 nodes(E , X ) next id edges next id edges dest next edges(E ) edges(E ) edges(E ) nodes(E , X 0 ) nodes(E , F 0 ) ↵ 0 6 = 0 ^β 6 = 0 ^β0 6 = 0 ^E = X ] {↵ 0 } ] X 0 ] {β 0 } ] F 0 ^β0 2 E _ h ↵ ↵ 0 s β c β 0 nodes(E , X ) next id edges dest next edges(E ) edges(E ) nodes(E , F ) ↵ 0 6 = 0 ^β 6 = 0 ^β0 = 0 ^E = X ] {↵ 0 } ] F ^β0 2 E _ h ↵ c β 0 ↵ 0 s β c β 0 nodes(E , X 1 ) next id edges nodes(E , X 2 ) next id edges dest next edges(E ) edges(E ) nodes(E , F ) edges(E ) ↵ 0 6 = 0 ^β 6 = 0 ^β0 6 = 0 ^E = X 1 ] {β 0 , ↵ 0 } ] X 2 ] F ^β0 2 E Figure 6
.10: Local invariants computed after reaching a post-fixpoint can be used in a specific analysis, while the BDD-based set domain can always provide excellent precision but with a risk of less reliable performance.

The "Total" columns in Table 6.1 show the total analysis time using different set domains and the "Shape" columns show the time spent on the shape domain. We find that, in all cases, the total analysis time is less than one second, and in particular the analysis parameterized by the linear set domain takes less than 50ms run-time, even in complex cases which require nonlocal unfolding and instantiation of fresh set variables. Moreover, the time spent in the shape domain is in line with those usually observed in the analyzer [START_REF] Toubhans | Reduced product combination of abstract domains for shapes[END_REF][START_REF] Toubhans | An abstract domain combinator for separately conjoining memory abstractions[END_REF]. Therefore, the performance of the analysis is well preserved with an efficient set domain.

Related Works of The Analysis for Unstructured Sharing

A wide family of shape analysis techniques have been proposed to deal with inductive structures, often based on 3-valued logic [SRW02, LAS00] or on separation logic [BCO05, DOY06, BCC + 07, NDQC07, CDOY09, CR08]. Such analyses often deal very well with list-and tree-like structures, but are often challenged with unbounded sharing.

In this part of the thesis, we augmented a separation logic-based analysis [CRN07, CR08] with set predicates to handle unbounded sharing, both in summaries and in unfolded regions, and retain the parameterizability of this analysis.

A shape analysis tracking properties of structure contents was presented in [START_REF] Vafeiadis | Shape-value abstraction for verifying linearizability[END_REF], although with a less general set abstraction interface, and without support for unfolding guided by set parameters. Another related approach was proposed in [START_REF] Cherini | A shape analysis for non-linear data structures[END_REF], that utilizes a set of datastructure specific analysis rules and encodes sharing information into instrumentalized variables in order to analyze programs manipulating trees and graphs. In contrast, our analysis does no such instrumentation and requires no built-in inductive definitions.

Recently, a set of studies [DES13, KSV10, LYP11, TCR13] targeted overlaid structures, which feature some form of structured sharing, such as a tree overlaid on a list. Typically, these analyses combine several abstractions specific to the different layers. We believe that the problem is orthogonal to ours, since we consider a form of sharing that is not structured, and we need to achieve non-local materialization.

Another line of work that is slightly related to ours are the hybrid analyses that aim at discovering relations between the structures and their contents [CR08, FFJ12, BDES12]. Our set predicates actually fit in the domain product formalized in [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF], and can also indirectly capture relations between structures and their contents through sets. Abstractions of set properties have recently been used in order to capture relations between sets of keys of dictionaries [START_REF] Dillig | Precise reasoning for programs using containers[END_REF][START_REF] Cox | Automatic analysis of open objects in dynamic language programs[END_REF] or groups of array cells [START_REF] Liu | Abstraction of arrays based on non contiguous partitions[END_REF]. A noticeable result is that our analysis tracks very similar predicates, although for a radically different application.

Conclusion on The Analysis for Unstructured Sharing

In this part of the thesis, we have set up a shape analysis able to deal with unbounded sharing. This analysis combines separation logic-based shape abstractions and a set abstract domain to Chapter 6. Static Analysis Algorithms for Unstructured Sharing Abstractions 101 track pointer sharing properties. Reduction across domains is done lazily at non-local materialization and join. This abstraction was implemented in the MemCAD static analyzer and could cope with graphs described by adjacency lists. Future work will experiment with other set abstract domains and combine this abstraction with other memory abstractions [START_REF] Toubhans | Reduced product combination of abstract domains for shapes[END_REF][START_REF] Toubhans | An abstract domain combinator for separately conjoining memory abstractions[END_REF].

Concrete memory state 1: . . . by ranges of integers, and dictionary analysis [DDA11, CCR14] that handles structures indexed using sets of keys. However, such a set of logical predicates is often not sufficient to describe a set of concrete memory states precisely as programs can produce very different structures at a program point. As an example, it is impossible to precisely abstract the concrete memory states shown in Figure 7.1 into a single abstract state, as the relative positions of variables t, x and y in the tree are very different, yet they can be precisely abstracted by a disjunction of two abstract states. Therefore, disjunctive abstract states d(2 D) ::= m _ . . . _ m are necessary in analysis.

In practice, disjunctions are a huge challenge to static analysis. The creation of new disjunctions occurs naturally when the analysis manipulates branch statements and loops, and when the analysis needs to unfold summary predicates to reason about operations that read or write into summary predicates. However, letting the number of disjuncts grow makes the analysis slower and consumes more memory. Nonetheless, getting rid of unnecessary disjuncts turns out to be a much harder task than introducing them.

We let t M! denote a computable join operation over the set of abstract states that overapproximates unions of sets of memory states. It is always sound for the analysis to replace a disjunctive abstract state m 0 _ m 1 with a non-disjunctive abstract state t M! (m 0 , m 1 ), but this operation generally leads to a loss of information. Disjunct clumping aims at identifying a partition of a finite set of disjuncts so that each component of the partition can be joined using the join operator t M! without a significant loss of precision. However, existing approaches all come with limitations. For instance, both the local rewriting rules-based canonicalization operator of [START_REF] Distefano | A local shape analysis based on separation logic[END_REF] and the control flow structure (conditions, loops, etc.) based partition strategies are likely to produce inadequate and imprecise disjunct clumps as they either totally ignore the shapes or ignore global shape properties.

Therefore, to better solve the disjunct clumping problem, we need to:

• identify global shape properties of abstract states, such that abstract states sharing similar global shape properties can be joined using the join operator t M! without a significant loss of precision. For instance, abstract states of the concrete states shown in Figure 7.1 should have different global shape properties as the joining operation cannot produce a precise over-approximation.

• design a disjunct clumping strategy that considers global shape properties of abstract states and can quickly identify a partition of a finite set of disjuncts, such that abstract states in each partition group share similar global shape properties.

Clumping Disjuncts Based on their Abstraction

In this part, we propose an approach to disjunct clumping that is based on using silhouettes (an abstraction of abstract states) to represent global properties of abstract states:

• we design a set of logical predicates S that describe the silhouettes of abstract states in a compact and simple representation, and a computable silhouette equivalence relation ⇠ that defines which silhouettes are similar; • we define a computable abstraction function ✓ : M ! -! S that maps an abstract state into its silhouette. Using this notion of silhouette, we define the clumping algorithm clump that inputs a disjunctive abstract state d and returns another disjunctive abstract state clump(d) that overapproximates d with at most as many (though usually fewer) disjuncts:

1. it inputs a disjunctive abstract state m 0 _ . . . _ m n ; 2. it computes ✓(m 0 ), . . . , ✓(m n ), and packs together abstract states with the same image by ✓ up to the equivalence relation ⇠; 3. it reduces each group into a single abstract state, by repeatedly applying t M! , and returns a more compact disjunction.

Example 7.1 (Silhouettes in numerical analysis). In this example, we consider programs that manipulate integer variables, and perform basic arithmetic operations. A common goal for static analyses consists of verifying the absence of division by zero errors. Let us assume such an analysis relies on interval constraints over program variables: a division by x can be proved safe if the analysis computes for x either an interval of strictly negative numbers or an interval of strictly positive numbers. We note that joining together an interval of strictly negative numbers and an interval of strictly positive numbers will return an interval that contains zero. Thus, after such a join, crucial information will be lost to verify that a division by x is safe.

The sign abstraction provides an obvious characterization which interval unions will produce such an imprecise result: the sign abstract domain is made up of four abstract values ?, , ⊕, > that respectively denote the empty set, any set of strictly negative integers, any set of strictly positive integers, and any set of integers. For instance, if two intervals have sign , they can be joined without losing information with respect to zero, whereas the join of an interval with sign with an interval with sign ⊕ will cause a loss of precision.

Therefore, a principle similar to silhouettes allows us to enhance the precision of the analysis, with respect to the goal of proving variables are not equal to zero:

• disjunctive states composed of finite disjunctions of intervals can keep more precise information about sets of states where a variable x may be positive or negative; • the "silhouette" of intervals defined by their sign abstraction characterizes when joining two intervals will cause a precision loss, with respect to the property of interest.

Analysis of an AVL Tree Insertion Function

In this section, we define an instance of clumping of disjunctive predicates, by defining S, ✓ and ⇠ and we demonstrate how this approach enables the verification of a function that inserts an element into an AVL tree, while limiting the size of disjunctions.

Example: insertion into an AVL tree. AVL trees achieve balancing by enforcing that the heights of two subtrees of a single node differ by at most one, and by storing that difference on each node, so that insertion and removal algorithms can re-balance subtrees incrementally, using "rotation" operations. This property makes insertion and removal complicated, thus the preservation of structural invariants and absence of memory errors (such as illegal pointer operations or leakage of subtrees) are difficult to verify. In particular, the insertion and removal functions need to distinguish many cases, which the functions' verification should also distinguish. Thus, verification algorithms will produce large numbers of disjuncts, and could greatly benefit from clumping. Fig. 7.2 shows an extract of an AVL insertion function. While the verification of the full code (from [START_REF] Walker | AVL balanced tree library[END_REF]) is presented in Chapter 11, we study here a simplified version for the sake of clarity. We only consider the handling of disjunctions of memory shapes; in particular, we ignore the AVL trees numeric balancing constraints (for our purposes, this restriction has no impact on the analysis).

The fragment in Fig. 7.2 handles the insertion into a non-empty tree, and carries it out in three phases. First, the node p at which the new element should be inserted is localized, as well as the deepest edge (with source x and target y) in the tree where the balancing property is locally broken by this insertion (indeed, this is the only point where a re-balancing will actually be required, since a rotation at this point will prevent any other balancing constraint from being broken). Second, a new node is allocated and inserted at position p. Finally, the re-balancing itself is performed. We consider in detail only the first phase. This phase should compute pointers p, x, y. To verify this function, the analysis should compute invariants that characterize precisely the shape of trees, subtrees and the relative positions of pointers p, x, y, t in all cases, including the corner case where tree t consists of a single node, and the insertion is actually done above it.

Abstract states and analysis. To express invariants over the code in Fig. 7.2, the analysis needs inductive predicates and segment predicates parameterized by inductive definitions to describe trees of unbounded size as well as cursors inside trees. Let us assume a tree definition (introduced in Section 2.3) describing either an empty tree or a tree with an AVL node and two disjoint subtrees:

↵ 0 • tree ::= emp ^↵0 = 0 _ ↵ 0 .l 7 ! ↵ 1 ⇤ ↵ 0 .r 7 ! ↵ 2 ⇤ ↵ 0 .bal 7 ! ↵ 3 ⇤ ↵ 0 .d 7 ! ↵ 3 ⇤ ↵ 1 • tree ⇤ ↵ 2 • tree ^↵ 6 = 0
This definition boils down to a pair of fold (Section 2.4.4) / unfold (Section 2.4.2) operations , that fully characterize tree: m 1 would discard all information about either t or x, which would make the proof of structural preservation impossible. Therefore, an ideal clumping would join m 1 , m 2 , m 3 together but keep m 0 separate.

Silhouette abstraction. Intuitively, abstract states where the relative positions of cursors t, x, y in the tree are similar can be clumped together with no severe precision loss. In line with this intuition, the notion of silhouette (formalized in Chapter 8) retains only the relative positions of t, x, y and the access paths between them, as shown in the last column of Fig. 7.4. As access paths may be of unbounded length, we abstract them with regular expressions describing sequences of fields dereferenced between nodes. For instance, the silhouette s 0 of m 0 boils down to a single edge, with a single path labeled by l. Even the more complex m 3 is characterized by only two edges respectively labeled by r • (l + r) ? • l (between t and x) and by l (between x and y).

Clumping disjuncts. Silhouettes make the dissimilarity of m 0 with the other states in Fig. 7.4 obvious, due to the incompatible order of cursors. However, we can also see that the silhouettes of m 2 and m 3 , while not syntactically identical are actually equal up-to a generalization of the path regular expression for the left edge into (l + r) ? . This generalization matches the fact that any structure segment can be weakened into a tree segment predicate, whatever the sequence of "left-right" branches it encompasses:

s ⇠ = t x y (l + r) ? l
The silhouette of m 1 also corresponds to a special case of s ⇠ . Therefore, we let ⇠ denote the similarity of silhouettes up-to generalization of access paths (formalized in Chapter 10). With this notation, we have:

s 0 6 ⇠ s 1 s 0 6 ⇠ s 2 s 0 6 ⇠ s 3 s 1 ⇠ s 2 ⇠ s 3
Therefore, the groups computed here are {m 0 }, {m 1 , m 2 , m 3 }, and the four disjuncts of Fig. 7.4 are clumped into a disjunctive abstract state composed of only two disjuncts m 0 and m 1,2,3 . The computation of the m 1,2,3 (which we discuss in the next paragraph) may use any weakening algorithm for abstract states, such as canonical abstraction [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF], canonicalization of symbolic heaps [START_REF] Distefano | A local shape analysis based on separation logic[END_REF], or shape graph join [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF].

In essence, clumping relies on a weak canonicalization [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF] that returns silhouettes, and then selects groups based on an equivalence relation over the set of silhouettes. To ensure the termination of abstract iterates over loops, the clumping relation ⇠ is required to be finite (i.e., it should have a finite set of equivalence classes), though the set of silhouettes may still be infinite. However, clumping may be performed at other points than loop heads (in order to shrink abstract states, without discarding any information), and then it does not require a finite ⇠. From this point of view, clumping provides a more flexible approach to the handling of disjunctions than canonicalization, since it does not need to project abstract states into a finite set of predicates, and since it may still take advantage of precise binary operators for weakening.

Clumping region predicates. The information computed in silhouettes also provides a guideline for weakening abstract states (formalized in Chapter 9). Indeed, let us consider silhouette s ⇠ , which is weaker than the silhouettes of m 1 , m 2 , m 3 . As it contains an edge labeled by (l + r) ? between t and x, it suggests weakening the fragment of these abstract states that are between t and x into a tree segment predicate. The soundness of such a weakening can be verified by checking entailment of a fragment of m 1 (resp., m 2 , m 3 ) and a treeseg predicate. The resulting weaker abstract state m 1,2,3 is shown in Figure 7.5. Here, the role of the silhouette is to provide guidance on how abstract states may be weakened. The advantage of this approach to the computation of weakening is that it provides global semantic information about the structure of abstract states, which would be missed if weakening operators based only on syntactic rules (like the canonical heap abstraction of [START_REF] Distefano | A local shape analysis based on separation logic[END_REF] and the join of [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF]).

γ M! (m) = {(σ, µ dX ) | (σ, µ) ✏ m}
The detailed definitions of γ M! (m) and γ D (d) are omitted as they can be formalized similarly as in Sections 2.3 and 4.2. We note that symbolic variables are existentially quantified, and thus the concretization of abstract states is unchanged by renaming symbolic variables. Similarly, swapping node names or merging equal nodes preserves the meaning of abstract states.

Silhouettes. Abstract states provide a precise description of sets of concrete states. Even summarized regions are characterized by inductive predicates that convey very detailed information about their structure. The purpose of silhouettes, as introduced in Section 7.1.2, is to identify similarities among abstract states without looking into the details of the shapes of the structures. Thus, we define silhouettes as graphs, yet with edges that retain less information than region predicates. We notice that information about reachability on pointer paths is relevant to the characterization of groups of abstract states that could be clumped together. Paths can be described using basic regular expressions over fields. We let E denote the set of the regular expressions that satisfy the grammar e ::= ✏ | f | (f 0 + . . . + f n ) ? | e • e which are respectively adequate to describe equalities, points-to edges, segment edges, and sequences of edges. This leads us to the following definition: Definition 8.1 (Silhouette). A silhouette s is a graph defined by a set of nodes N ✓ V, and a set of edges E that are labeled by regular expressions in E (we write (v, e, v 0 ) for such an edge).

Concretization. A silhouette collects a conjunction of reachability constraints over paths. Thus, the concretization γ S (s) of a silhouette s is defined as the set of pairs (σ, µ) made up of a memory store σ and an evaluation function of program variables, and for each pair (σ, µ), there exists an evaluation function µ 0 of symbolic variables, such that (σ, µ ] µ 0 ) satisfies all the constraints defined by the edges of s. Deciding whether (σ, µ ] µ 0 ) satisfies the constraint defined by an edge (v, e, v 0 ) comes down to evaluating the values described by v, v 0 into values a, a 0 and checking whether dereferencing a sequence of fields described by e starting from a makes it possible to reach a 0 . This leads us to the following definition: Chapter 8. Silhouette Abstractions: Abstraction of Memory Abstract States 117 Definition 8.2 (Silhouette concretization). The following set of rules formalizes whether (σ, µ) satisfies the constraint defined by a silhouette edge (v, e, v 0 ):

(σ, µ) ✏ µ(v), e, µ(v 0 ) (σ, µ) ✏ (v, e, v 0 ) (σ, µ) ✏ a, (f 0 + . . . + f n ) ? , a σ(a + f) = a 0 (σ, µ) ✏ a, f, a 0 9i, (σ, µ) ✏ σ(a + f i ), (f 0 + . . . + f n ) ? , a 0 (σ, µ) ✏ a, (f 0 + . . . + f n ) ? , a 0 (σ, µ) ✏ a, ✏, a
9a 00 , (σ, µ) ✏ a, e, a 00 ^(σ, µ) ✏ a 00 , e 0 , a 0 (σ, µ) ✏ a, e • e 0 , a 0

Then, the concretization of silhouettes is defined as:

γ S (s) = {(σ, µ dX ) | 8(v, e, v 0 ) 2 s, (σ, µ) ✏ (v, e, v 0 )} Example 8.1 (Silhouette).
Let us consider the silhouette shown below with its graphical representation on the right:

s = {(t, (l + r) ? , x)} t x (l + r) ?
Its concretization includes memory states such as the following memory state: t x 0x0 0x0 0x0 0x0 0x0 0x0 0x0

Computation of Silhouettes

To allow silhouettes to assist in clumping abstract states, it is crucial to have an efficient way to compute them. First, empty regions, equalities/disequalities to 0x0, and full inductive predicates (of the form ↵ • ind) do not contribute to the silhouette. Second, a points-to edge v • f 7 ! v 0 simply contributes an edge (v, f, v 0 ). Last, a segment predicate v • ind ⇤= v 0 • ind contributes an edge (v, path(ind), v 0 ), where path(ind) denotes the set of paths that can be induced by a segment of inductive definition ind: in the case of the tree definition shown in Section 7.2, path(tree) = (l + r) ? . Moreover, the silhouette of an abstract state is obtained by collecting the contribution of each region predicate.

118 Chapter 8. Silhouette Abstractions: Abstraction of Memory Abstract States Definition 8.3 (Silhouette computation). The silhouette of an abstract state is defined as a set of edges computed by the translation function ⇧ defined by:

⇧(v � 0x0) = ; ⇧(v = v 0 ) = {(v, ✏, v 0 )} ⇧(emp) = ; ⇧(v • f 7 ! v 0 ) = {(v, f, v 0 )} ⇧(ind(v)) = ; ⇧(ind(v, v 0 )) = {(v, path(ind), v 0 )} ⇧(p 0 ⇤ . . . ⇤ p k ^n0 ^. . . ^nl ) = ⇧(p 0 ) [ . . . [ ⇧(p n ) [ ⇧(n 0 ) [ . . . [ ⇧(n n )
This translation function ⇧ is sound since all concrete states described by the abstract state m are also described by its silhouette ⇧(m).

Theorem 8.1 (Soundness of silhouette computation). The silhouette translation function ⇧ is sound: for each memory state m,

γ M! (m) ✓ γ S (⇧(m))
Proof. The proof proceeds by induction over abstract states, and follows the definition of ⇧.

The cases of equality and disequality constraints, empty regions, points-to regions, and inductive predicates are trivial. The case of segments requires unrolling their concretization which is itself based on a fix-point. Finally, the case of a conjunction of predicates follows from the fact that the semantics of a silhouette seen as a set of constraints is the intersection of the concretization of each individual constraint. ⌅ Weakening silhouettes. Silhouettes describe conjunctions of constraints, thus they can be weakened into coarser approximations of sets of memory states, either by dropping or by weakening some constraints. As only a part of silhouette nodes may play a special role, we define here a weakening of silhouettes by restricting silhouettes to a subset of nodes.

Definition 8.4 (Silhouette restriction). Given a silhouette s = (N, E) and a set of nodes N 0 ✓ N, the restriction of s to N 0 , denoted as s dN 0 , is defined as (N 0 , E 0 ), i.e., the set of nodes N 0 and the set of edges E 0 obtained as acyclic concatenations of edges of s forming paths from N 0 to N 0 : This weakening effectively allows us to ignore some nodes. For instance, if X ✓ X is a set of variables that play a special role, then ⇧(m) dX is a silhouette of m that will only retain information about the variables in X. We note this silhouette ⇧(m, X). Proof. Based on the concretization rules of Definition 8.2, We can easily prove that:

8v 0 , v k 2 N 0 , (v 0 , e, v k ) 2 E 0 () 9(v 0 , e 1 , v
8(σ, µ) ✏ s, 8(v, e, v 0 ) 2 s dN 0 , (σ, µ) ✏ (v, e, v 0 ) ⌅

Silhouette-based Weak Entailment Checking

In this section, we study the relationship between entailment checking of abstract states and the silhouettes, and we hope to improve the efficiency of the entailment checking of abstract states with silhouette entailment checking.

Silhouette Entailment Check

Before introducing silhouette entailment checking, let us first recall entailment check for abstract states.

Entailment check for abstract states. As introduced in Section 6.3.1, the entailment checking of abstract states v M! [BCO05, DOY06, CRN07] is usually implemented as a proof search system based on sets of proof rules that establish inclusion locally. The proof rules shown below (for clarity, numerical constraints are elided) are able to express separation, reflexivity, and unfolding of inductive summary predicates in general: The entailment checking algorithm is in general sound and incomplete: when v M! (m 0 , m 1 ) returns true (denoted as m 0 v M! m 1 ), then γ M! (m 0 ) ✓ γ M! (m 1 ), yet the reverse implication does not hold in general. Indeed, complete proof search algorithms with backtracking are expensive and generally can not be ensured in the presence of more complex sets of numerical constraints [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF] than in the restricted set of abstract states used here. Moreover, when the inclusion does not hold, i.e., γ M! (m 0 ) 6 ✓ γ M! (m 1 ), which happens very often in the analysis, the inclusion checking algorithm still needs to apply a set of proof rules to return false, which can be costly.

m 0 v M! m 0 0 m 1 v M! m 0 1 m 0 ⇤ m 1 v M! m 0 0 ⇤ m 0 1 i -sep m is of the form v • f 7 ! v 0 or v • ind or v • ind ⇤= v 0 • ind m v M! m i -id m 0 is of the form v • ind or v • ind ⇤= v 0 • ind and m 0 unfold -! m m v M! m 0 i -uf m v M! v 0 • ind v • ind ⇤= v 0 • ind ⇤ m v M! v • ind i -segind 120

Silhouette entailment check.

As an alternative to the abstract state entailment check, we propose to first use a weaker and cheaper entailment check on silhouettes, which is based on a classical inclusion of constraints. We let L (e) denote the language of e.

Definition 8.5 (Silhouette entailment check). Let s 0 , s 1 2 S. We let v S (s 0 , s 1 ) return true (denoted as s 0 v S s 1 ) if and only if for each edge (v, e, v 0 ) of s 1 there exists a (possibly empty) sequence of edges (v 0 , e 1 , v 1 ), . . . ,

(v k-1 , e k , v k ) in s 0 such that v 0 = v, v k = v 0 and L (e 1 • . . . • e k ) ✓ L (e) (or, if the sequence is empty, ✏ 2 L (e)).
We note that v S forms an order relation, i.e., given s 0 v S s 1 and s 1 v S s 2 , we can get s 0 v S s 2 .

Example 8.4 (Silhouette entailment check). Let us consider the silhouettes below drawn from the analysis of the program searching for the minimum and maximum list elements shown in Figure 1.8:

s 0 hd min max n ⇤ n ⇤ s 1 hd max min n ⇤ n ⇤ s 2 hd, min max n • n
We have: v S (s 0 , s 1 ) = false, v S (s 1 , s 0 ) = false, v S (s 2 , s 0 ) = true.

Theorem 8.3 (Soundness). The entailment check v S is sound: given s 0 , s 1 2 S,

if s 0 v S s 1 , then γ S (s 0 ) ✓ γ S (s 1 )
Proof. Let us assume v S (s 0 , s 1 ) = true and (v, e, v 0 ) is an edge of s 1 . Then, according to Definition 8.5, there exists a (possibly empty) sequence of edges (v 0 , e 1 , v 1 ), . . . , (v k-1 , e k , v k ) in s 0 such that v 0 = v, v k = v 0 and L (e 1 • . . . • e k ) ✓ L (e) (or, if the sequence is empty, ✏ 2 L (e)). By the definition of the silhouette concretization, the concretization of {(v 0 , e 1 , v 1 ), . . . , (v k-1 , e k , v k )} is included in that of (v, e, v 0 ). As the concretization of s 1 is the intersection of the concretization of its edges, we can thus derive the theorem. ⌅ Chapter 8. Silhouette Abstractions: Abstraction of Memory Abstract States 121

Weak Entailment Checking

The most important result on silhouette entailment checking is that it is weaker than abstract states entailment checking:

Theorem 8.4 (Weak entailment). Let m 0 , m 1 2 M ! and s 0 = (N 0 , E 0 ) = ⇧(m 0 ), s 1 = (N 1 , E 1 ) = ⇧(m 1 ), then:

m 0 v M! m 1 =) s 0 v S s 1 Moreover, let N 0 ✓ N 0 ^N0 ✓ N 1 , then: m 0 v M! m 1 =) s 0dN 0 v S s 1dN 0
Proof. We can prove that m 0 v M! m 1 =) s 0 v S s 1 by induction on the derivation rules of v M! :

• Case of the i-id rule:

m is of the form v • f 7 ! v 0 or v • ind or v • ind ⇤= v 0 • ind m v M! m
Since both sides are equal, their image by ⇧ are equal too.

• Case of the i-uf rule (for inductive predicates):

v • ind unfold -! m m v M! v • ind
The right-hand side is a full inductive predicate, which thus has a silhouette with no edge, which concretizes in the set of all pairs made up of a state and a valuation.

• Case of the i-uf rule (for segment predicates):

v • ind ⇤= v 0 • ind unfold -! m m v M! v • ind ⇤= v 0 • ind
By the definition of the unfolding of a segment and of path, m is a memory state fragment such that there exists a path from v to v 0 described by an expression the whose language is included in that of path(ind). Thus, ⇧(m) v S {(v, path(ind), v 0 )}.

• Case of the i-segind rule:

m v M! v 0 • ind v • ind ⇤= v 0 • ind ⇤ m v M! v • ind
The right-hand side is a full inductive predicate, which thus has a silhouette with no edge, which concretizes in the set of all pairs made up of a state and a valuation.

Chapter 9

Silhouette-Guided Joining of Abstract Memory States

This chapter shows that silhouettes can be used to make the joining procedure of abstract memory states more precise. Specifically, Section 9.1 first recalls the existing abstract states join procedure and discusses possible loss of precision in the joining. Then, Section 9.2 introduces silhouette guided abstract states join.

Existing Abstract States Join Procedure and Precision Loss

Before introducing the silhouette-guided joining of abstract states, let us first recall the main principles of the existing abstract state joining operator t M! presented in Section 6.3.2. Based on separation [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] and local reasoning, the joining operator t M! applies two main kinds of rules on abstract shapes, as presented in Figure 6.6:

• Weakening guided by existing region predicates. The first set of rules (e.g., j-pt, j-ind, j-weak) searches for cases where g v G g 0 (resp. g 0 v G g) holds so that a valid choice for g t is g 0 (resp., g). The most common case is when g = g 0 . Another important case is when g 0 = ↵ • ind and g v G ↵ • ind; then g gets weakened into a summary predicate, that was already present in g 0 .

• Synthesis of summary predicates. The second set of rules (e.g., j-intro) synthesizes new summary predicates, in order to weaken specific patterns. For instance, the introduction of a segment predicate is a particular case of summary predicate synthesis, that weakens an empty region into a segment: We note that in m, t = x. Then, both abstract states m, m 0 can be split into two regions, and the following joining rules are applied to each region:

g i = emp ^↵ = β) g 0 i v G ↵ • ind ⇤= β • ind � g t i = ↵ • ind ⇤= β • ind 126
t, x t G t ↵ x β l r tree tree = t x ↵ tree x tree t G x tree = t tree
Therefore, the two states m, m 0 can be joined into t

• ind ⇤= x • ind ⇤ x • ind.
Challenges. In practice, however, joining rules are applied in sequential orders and it is often the case that more than one rule can be applied at one point. Yet, different rule application orders may produce very different results. However, determining which rule, when applied, can lead to a precise joining results in huge difficulty in the abstract join because of the large search space that needs to be examined. Moreover, in certain cases, there exists no rule order that produces a precise common over-approximation. Even when a solution does exist, it may be non-unique, and there may be no universally best solution, as illustrated by the following example.

Example 9.2 (Non-unique joining rule order). We let m, m 0 be defined by: • synthesizing a segment predicate between t and x by applying the j-intro rule first and then synthesizing another segment predicate between x and y by applying the same rule produces a joining result, where the fact that x, y are cursors in the tree pointed to by t is preserved, but the information that t • l points to y is lost:

t x y tree tree tree m t 2 :
In this situation, to make the best joining choice, the analysis should take into account future uses of t, x, y. If x is unused after the point in the program where the joining is performed, the first joining is the best. If the fact that x points somewhere in the tree matters, the second joining is better. Finally, if the fact that y is a child of t and the fact that x points somewhere in the tree both matter, then no precise joining result exists.

Silhouette Guided Abstract States Joining

In this section, we first define silhouette joining in Section 9.2.1 and in Section 9.2.2 we demonstrate that silhouettes can help to determine which rule to apply during abstract state join for a precise joining result. Then, in Section 9.2.3, we show that silhouettes can be restricted so as to be more concise and relevant to guiding abstract states join, by considering the analysis goal.

Silhouettes Joining

We now define a join operator over silhouettes that takes any two silhouettes as inputs and returns their over-approximation.

Definition 9.1 (Silhouette join). Let us first define the join of silhouette edges. Silhouette edges (v 0 , e, v 1 ) and (v 0 , e 0 , v 1 ) can be joined as the edge (v 0 , e t , v 1 ), where e t keeps the same left side as e and e 0 and joins the other part into the smallest and more general regular expression of the form (f 0 + . . . + f k ) ? . Then, given two silhouettes s = (N, E), s 0 = (N 0 , E 0 ), we define their silhouette join noted t S (s, s 0 ) as the silhouette s t = (N t , E t ) such that N t = N \ N 0 and E t collect the pairwise join of the edges of s dN t and of s 0 dN t . Silhouettes join acts like a "lightweight" abstract states join.

Example 9.3 (Silhouettes join). Let us consider the abstract states m and m 0 presented in Example 9.1, and let X = {t, x}, then we obtain the silhouettes below:

t, x s = ⇧(m, b X) = t x (l + r) ? • l s 0 = ⇧(m 0 , b X) =
As in s, the access path from t to x is ✏ (empty), and in s 0 , t can reach x through access path (l + r) ⇤ • l, therefore joining the two silhouettes gets the silhouette below, where the access path (l + r) ⇤ over-approximates ✏ and (l + r) ⇤ • l: t x (l + r) ? s t S s 0 = Theorem 9.1 (Soundness). The silhouette join is sound:

8s, s 0 2 S, t S (s, s 0 ) = s o =) γ S (s) [ γ S (s 0 ) ✓ γ S (s o )
Proof. According to Definition 9.1, for any (v, e o , v 0 ) 2 s o , there exists (v, e, v 0 ) 2 s and (v, e 0 , v 0 ) 2 s 0 such that, L (e) [ L (e 0 ) ✓ L (e 0 ). Therefore, γ S (s) ✓ γ S (s o ) ^γS (s 0 ) ✓ γ S (s o ). ⌅

Guided Abstract States Joining

When two abstract states can be joined into a segment, their silhouette is a refinement of the silhouette of a segment (by Th. 8.4):

Theorem 9.2 (Guided segment synthesis weak characterization). Let m, m 0 be two abstract states such that m

v M! v 0 • ind ⇤= v 1 • ind and m 0 v M! v 0 • ind ⇤= v 1 • ind, then γ S (join S (⇧(m, {v 0 , v 1 }), ⇧(m 0 , {v 0 , v 1 }))) ✓ γ S ({(v 0 , path(ind), v 1 )})
Based on the theorem, we derive the semantic guided segment introduction rule below, where the application of the rule does not rely on the syntax of abstract states, but relies on their silhouette join. Definition 9.2 (Semantic guided segment introduction rule).

let s = ⇧(m, {v 0 , v 1 }) and s 0 = ⇧(m 0 , {v 0 , v 1 }) if t S (s, s 0 ) = (f 0 + . . . + f k ) ? and v S (t S (s, s 0 ), {(v 0 , path(ind), v 1 )}) = true, then if v M! (m, v 0 • ind ⇤= v 1 • ind) = true and v M! (m 0 , v 0 • ind ⇤= v 1 • ind) = true, then, t M! (m, m 0 ) = v 0 • ind ⇤= v 1 • ind
Intuitively, this rule will only attempt to synthesize a segment when the join of the silhouettes can be weakened into the silhouette of a segment. Only in that case will it call the shape inclusion checking function v M! to determine if a segment can be introduced. This rule supersedes the classical syntactic rule and avoids many attempts to run the costly v M! , which would fail (since v S provides a cheaper, weak entailment test).

In the following, we let t M! denote a join operator for abstract states, that takes as input a third argument for a silhouette which it uses as a guide to introduce segments. Given two abstract states and a silhouette, the guided joining operator first attempts to apply the semantic guided segment introduction rule, and then applies the other joining rules, as presented in Figure 6.6. Theorem 9.3 (Soundness). The guided joining is sound:

t M! (m, m 0 , s) = m o =) γ M! (m) ✓ γ M! (m o ) ^γM! (m 0 ) ✓ γ M! (m o )
Proof. The soundness can be easily proved based on the soundness of each rule. ⌅ Example 9.4. We consider the abstract states m, m 0 of Example 9.1. Then:

s t = t S (⇧(m, {x, t}), ⇧(m 0 , {x, t})) = {(t, (l + r) ? , x)}
Thus, the semantic guided segment introduction rule can be applied to synthesize a segment predicate between t and x, and after which a normal joining rule can be applied to match the inductive predicate at x:

t M! (m, m 0 , s t ) = t • tree ⇤= x • tree ⇤ x • tree
As another example, let us consider the abstract states m, m 0 of Example 9.2, where s t = t S (⇧(m, {x, t, y}), ⇧(m 0 , {x, t, y})) = {(t, l ? , x), (x, l ? , y)}

As path(tree) = (l + r) ⇤ , thus the guided segment introduction rule can be applied to synthesize a segment predicate between t and x and a segment predicate between x and y, after which a normal joining rule can be applied to match the inductive predicate at y:

t M! (m, m 0 , s t ) = t • tree ⇤= x • tree ⇤ x • tree
We note that the silhouette guided abstract states join could compute more precise join results when the search space for the join is larger, as evaluated in Chapter 11. The syntactic rule-based join that we presented in Figure 6.6 tends to fail in such cases, and that the failure generally stems from a lack of understanding of the semantic properties of the abstract state.

Taking Advantage of the Analysis Goal

Live variables. As remarked in Example 9.2, live program variables play a big role in determining whether a joining result is precise or not. The reason is that live variables may be read later in the program being analyzed before they are overwritten. Thus the joining process of abstract states should always try to apply rules that are able to keep precise information of live variables since if, during joining, the information about live variables is lost, then the analysis is very likely to fail. As shown in Section 9.2.2, silhouettes can guide abstract state join to keep important precise information that is relevant to silhouettes. Therefore, we can make silhouettes more concise and relevant by collecting only nodes that are live variables. We note that a standard liveness compiler analysis [START_REF] Appel | Modern Compiler Implementation in C[END_REF] can compute a set of live program variables at each program point.

Branching nodes. When abstracting concrete memories, memory nodes that have nested pointers to several sub-structures which can also be accessed by dereferencing different program variables are usually important as such nodes should not be summarized in abstract states for precision. We call such a memory node a "branching node" in the following. As an example, the memory node in purple in Figure 9.1(a) is a branching node. If it were summarized, one of the cursors x, y would have to be dropped. A precise abstraction would abstract the branch node exactly with points-to edges, as shown at the top of Figure 9.1(b). As silhouettes are used to guide the synthesizing of segment predicates in abstract state join operations, which may cause precision loss when branching nodes are summarized, we need to identify "branching nodes" in silhouettes and always keep precise information about them, such as the silhouette shown at the bottom of Figure 9.1(b).

Chapter 10. Silhouette-Guided Clumping and Widening

m = t x ↵ 0 ↵ 1 l r tree tree ⇧(m, {t, x}) = t x l • (l + r) ⇤ m 0 = t x β 0 β 1 β 2 β 3 l r l r tree tree tree ⇧(m 0 , {t, x}) = t x r • (l + r) ⇤ • r
• . . . • f 0 m • (f 0 + . . . + f k ) ? • f 00 0 • . . . • f 00 n
, where {f 0 0 , . . . , f 0 m , f 00 0 , . . . , f 00 n } ✓ {f 0 , . . . , f k }, is the regular expression φ(e) = (f 0 + . . . + f k ) ? . For all other regular expressions e, we let φ(e) = e.

The generalization of a silhouette s is obtained by replacing any edge (v, e, v 0 ) of s by edge (v, φ(e), v 0 ). It is noted Φ(s).

This operation defines a weakening over silhouettes, since for all silhouettes s, we can prove that γ S (s) ✓ γ S (Φ(s)).

Example 10.1. After generalization, we obtain: Φ(⇧(m, {t, x})) = {(t, (l + r) ? , x)} = Φ(⇧(m 0 , {t, x}))

Clumping Relation

We now consider a criterion for the computation of candidate groups of abstract states for clumping based on silhouettes.

As introduced in Figure . 6.6, many the join rules implicitly rely on v M! . Therefore, we can use silhouette entailment check v S to prune out abstract state entailment checks that do not hold in the silhouettes based on Theorem. 8.4. However, silhouette-guided joining allows weakening rules to be applied on both sides, as presented in Definition 9.2, during the computation of a single join of two abstract states m, m 0 . Thus, we need a symmetric characterization of situations where a weakening may be performed either in m, in m 0 or in both, which is the purpose of the following relation ./. Definition 10.2 (Silhouette association relation). Let s 0 dN 0 be the restriction of a silhouette s 0 to a set of nodes N 0 . Let s 0 , s 1 be two silhouettes with the same set of nodes N. We let s 0 0 = Φ(s 0 ) and s 0 1 = Φ(s 1 ). We write s 0 ./ s 1 if and only if there exist N 0 , N 1 such that N = N 0 [ N 1 and:

s 0 0 = s 0 0dN 0 [ s 0 0dN 1 ^vS (s 0 0dN 0 , s 0 1dN 0 ) = true ^s0 1 = s 0 1dN 0 [ s 0 1dN 1 ^vS (s 0 1dN 1 , s 0 0dN 1 ) = true
This relation is symmetric and reflexive, but not transitive.

Example 10.2. Let s 0 , s 1 , s 2 be defined by:

s 0 = x, y z f ⇤ s 1 = x, y z f s 2 = x y, z f ⇤
Let N 0 = {x, y} and N 1 = {y, z}, we get that s 0dN 0 v S s 1dN 0 , s 0dN 0 v S s 2dN 0 , and s 1dN 1 v S s 0dN 1 , s 2dN 1 v S s 1dN 1 . Thus, we have that s 0 ./ s 1 and s 0 ./ s 2 hold. However, s 1 ./ s 2 does not hold.

The silhouette association relation soundly characterizes the cases where a precise join can be computed using rules that perform weakening guided by existing predicates: Theorem 10.1 (Silhouette association and weakening). Let m, m 0 be two abstract states.

We assume that m = m 0 ⇤ m 1 and m 0 = m 0 0 ⇤ m 0 1 . Then:

m 0 v M! m 0 0 ^m0 1 v M! m 1 =) Φ(⇧(m)) ./ Φ(⇧(m 0 )) Proof. According to Definition 8.3, ⇧(m) = ⇧(m 0 ) [ ⇧(m 1 ) and ⇧(m 0 ) = ⇧(m 0 0 ) [ ⇧(m 0 1 ). According to Theorem 8.4, m 0 v M! m 0 0 =) ⇧(m 0 ) v S ⇧(m 0 0 ) and m 0 1 v M! m 1 =) ⇧(m 0 1 ) v S ⇧(m 1 )
. Thus, we have ⇧(m) ./ ⇧(m 0 ), which implies Φ(⇧(m)) ./ Φ(⇧(m 0 )). ⌅

The theorem implies that: whenever a join can be computed by weakening part of m into predicates present in m 0 and part of m 0 into predicates present in m, then relation ./ holds. The contraposition entails that:

when ./ does not hold, no precise join can be found using only rules that weaken abstract states based on existing predicates.

Therefore, Theorem 10.1 will prevent clumping from attempting to compute some but not all joins that will fail. However, the characterization that the theorem provides is actually very accurate, as shown by our experiments in Chapter 11. Disjunct m 0 occurs in the second iteration whereas disjuncts m 0 0 , m 0 1 , m 0 2 arise in the third iteration. For clarity, we only show the nodes on the path between t, x and y. In the table below, we show their silhouettes before and after applying the bounded abstraction: silhouette bounded abstraction

m 0 {(t, l, x), (x, l, y)} {(t, l • F ? , x), (x, l • F ? , y)} m 0 0 {(t, l • l, x), (x, l, y)} {(t, l • F ? , x), (x, l • F ? , y)} m 0 1 {(t, l • l, x), (x, r, y)} {(t, l • F ? , x), (x, r • F ? , y)} m 0 2 {(t, l • r, x), (x, l, y)} {(t, l • F ? , x), (x, l • F ? , y)} Then, ⇧(m 0 ) o b ⇧(m 0 0 ) and ⇧(m 0 ) o b ⇧(m 0
2 ) hold whereas ⇧(m 0 ) o b ⇧(m 0 1 ) does not. Thus, the pairing is defined by ⇡(0) = {0, 2}. The widening will thus preserve the information which establishes whether y is the left or right child of x.

Static Analysis

We now summarize the whole analysis.

As a forward abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], it starts with an abstract pre-condition that over-approximates initial memory states with a single disjunct which abstracts either the set of all memory states, with no structure allocated for whole program analysis, or a pre-condition describing the valid call states for the analysis of a library function.

It computes disjunctive abstract post-conditions for each statement. Post-conditions of assignment, test, allocation and deallocation statements are computed locally on each disjunct in parallel as shown in Section 2.4.5. Before a control flow join that joins two disjunctive abstract The analysis is sound as formalized in Theorem 2.1, which states that the analysis returns abstract post-conditions that over-approximate final states.

Chapter 11

Experimental Evaluation of Silhouette-Directed Clumping

The silhouette-directed algorithms are implemented in the MemCAD analyzer. This chapter assesses the efficiency of silhouette-directed methods in improving the static analysis of various data structures from realworld C libraries. Specifically, Section 11.1 presents some research hypotheses, Section 11.2 sets up the benchmarks and experimental methodology and Section 11.3 evaluates the hypotheses.

Research Hypotheses

In this section, we empirically evaluate whether or not semantic-directed clumping is effective in improving the static analysis of data structures from real-world C libraries. We implemented clumping in the MemCAD analyzer [START_REF] Bor-Yuh | Modular construction of shape-numeric analyzers[END_REF]. We seek to provide evidence for or against the following hypotheses: RH1 (Clumping is effective). Semantic-directed clumping with guided join is necessary and effective for analyzing data structure operations from existing, real-world libraries. The underlying premise of this work is that inferring disjunctive loop invariants is necessary to effectively analyze real-world data structures. While certain code may be reasonably adapted to avoid the need for disjunctive invariants, analyzing existing, real-world code typically involves handling corner cases in separate disjuncts. We assess the impact of silhouettes on the analysis and make a comparision with other techniques.

RH2 (Guided join is necessary). Guided join is necessary to avoid unacceptable precision loss. Semantic-directed clumping uses silhouette abstraction to select the disjuncts to join. Guided join then subsequently uses these same silhouettes to perform the shape join. We seek to evaluate the need for this latter step.

RH3 (Clumping has a low overhead). The overhead of semantic-directed clumping is reasonable.

We hope and expect that the additional overhead in computing and comparing silhouettes is outweighed by the benefits of increased precision and improved scalability. This aspect must be tested empirically as the number of silhouette comparisons is quadratic in the number of disjuncts.

RH4 (Clumping limits disjunctive explosion). Semantic-directed clumping improves the scalability of disjunctive analysis by limiting the number of disjuncts in the abstract state. Without clumping, the number of disjuncts grows exponentially from control-flow paths and the unfolding of inductive predicates. The scalability of disjunctive analysis (and thus most shape analyses) is limited by the exponential growth in the number of disjuncts in the abstract state. Thus the technical challenge is to avoid piling up more and more unnecessary disjuncts while analyzing sequences of operations.

Experimental Methodology

To evaluate the effectiveness of semantic-based clumping, we consider 26 benchmarks of varying implementation styles and degrees of difficulty to analyze. These include operations over singlylinked and doubly-linked lists, as well as various binary trees with different kinds of invariants and pointer patterns (search, splay, red black, or AVL and with various sharing patterns). The operations consist of variants of finding an element, inserting, deleting, reversing, and sorting. Notably, 21 benchmarks are from external sources. Some of these come with typically simple, user-specified assertions (e.g., x != NULL). Each benchmark consists of a top-level function implementing a data structure operation with a pre-condition and a post-condition that specify the preservation of precise shape invariants. Some routines are recursive whereas the others contain nested loops.

Table 11.1 lists these benchmarks with metrics to get a sense of the difficulty to analyze, including the presence of recursion, lines of code, numbers of sub-routines, numbers of loops and acyclic paths. The number of loops and acyclic paths gives the number of disjuncts that a naïve path and context-sensitive analysis would have at the exit point. The final metric is the maximum number of simultaneous pointers into a data structure instance (column "Simult. Pointer"). The summary row gives total counts of LOCs, assertions, functions, loops and paths, and the average number of simultaneous pointers (As discussed in Chapter 7, the number of simultaneous pointers into an instance is related to the number of disjuncts needed to represent the program invariant).

The analysis is parameterized by the definition of ind (or infers it for basic list and tree cases). It attempts to prove memory safety, any user-specified assertions, and the (more complex) postcondition given a C program and optionally inductive predicates summarizing memory regions. Clumping is applied at the beginning and the end of functions, at loop heads, at loop exits, and at the end of branches.

We evaluate and compare the following clumping strategies:

• ClumpG and Clump do silhouette-guided clumping and widening (Chapter 10); ClumpG uses guided join (Chapter 9), whereas Clump does not; • None is the baseline technique, and does not compute silhouettes to perform clumping or guided joining. Instead, the joining keeps all disjuncts of both inputs and the widening merges all disjuncts of each input into one;

• Canon and CanonG conservatively model canonicalization operators [DOY06, SRW02]: they compute silhouettes but only join abstractions when their silhouettes are exactly the same (after folding nodes which are not pointed to by live variables); CanonG uses guided joining whereas Canon does not (we expect these strategies will still compute fewer disjunctions than a purely syntactic canonicalization would).

Experimental Evaluation

RH1: Clumping is effective. Our analyzer attempts to infer complex disjunctive shape invariants in loops, which is particularly challenging considering the benchmarks shown in Table 11.1 with not only forward and back pointers but also possibly unbounded sharing patterns. Back pointers (as in doubly-linked lists or trees with parent pointers) require not only forward unfolding of inductive summaries but also backward unfolding [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF]. The BSD red-black tree has parent pointers, which is heavily used in rebalancing. The leaves of the GDSL binary search tree all point back to the root node.

We observe a number of implementation idioms that lead to a need for disjunctions:

• First, the maximum number of simultaneous pointers into a data structure instance ("Simult. Pointer") is one driving factor as mentioned above, which typically increases as the operations get more complex (e.g., 12 for brbtree-delete).

• Second, the GDSL doubly-linked list uses sentinel nodes for the list head and tail. Because they are different to normal nodes, they cannot be summarized into the normal list segment, which yields more disjuncts to represent the possible points-to relationships between those nodes and the internal list segment.

• Third, nodes sometimes need to remain materialized between loops. Disjunctions are needed to represent the cases where the materialized node can occur but the number of disjuncts explodes exponentially in the number of materialized nodes in a tree. For example, delete in a red-black tree (brbtree-delete) requires three loops in sequence: find the node n to delete, find the minimum node m in the right subtree of n (i.e., the next in-order node to preserve the binary search invariant), rebalance the tree from the right subtree of that minimum node m. The node to delete n must be kept materialized between the first and second loop (to be able to track the swap of m and n) but becomes irrelevant between the second and the third loop (after the swap).

While maintaining a disjunct, or trace partition, for every acyclic path may be sufficiently precise in many or even most cases, it is clear from the path counts (column Path) that this choice is utterly infeasible in practice. The essence of semantic-directed clumping is to identify simultaneous pointers, sentinel nodes and the sort of relevance or irrelevance of a materialized node by computing silhouettes (i.e., "abstracting the abstraction").

In Figure 11.1(a), we compare clumping with guided join with the other strategies, showing the number of benchmarks that can be successfully verified memory safe (i.e., free of null or dangling pointer dereferences), the user-specified asserts, and the shape preservation post-condition using the different strategies (see also the bottom line of Figure 11.1(b)). We find that clumping with guided join (ClumpG) is significantly more effective (able to verify benchmarks) than the baseline and also more capable than any other strategy. CanonG fails to verify, for example, the particularly complex red-black tree insertion and deletion operations.

Clumping with guided join is able to verify these additional benchmarks with an analysis time that is comparable with any other configuration, as shown in Figure 11.1(b). The analysis time is larger for more complex benchmarks (e.g., for red-black tree delete brbtree-delete), which, as expected, raises its average analysis time, but ClumpG is also the only strategy that succeeds on this code. ClumpG is also notably faster than CanonG on javl-insert. Therefore, we conclude that ClumpG takes comparable or even less time than other strategies on benchmarks where other strategies succeed (e.g., in the bsplay benchmarks).

Another measure of effectiveness of ClumpG is that analysis logs show this strategy led to no precision loss in joins.

RH2: Guided join is necessary. Figure 11.1(a) and 11.1(b) also show not only that clumping is effective but that guided join is also necessary. While Clump does slightly improve on the baseline (11 versus 9), where two more benchmarks are verified, ClumpG (clumping with guided joining) is able to verify all the 26 benchmarks. Moreover, CanonG (canonicalization with guided joining) successfully verifies 21 benchmarks, while Canon alone only verifies 10 benchmarks. Thus, the guided join strategies (ClumpG and CanonG) are significantly better (26 and 21, respectively). Moreover, we find that Clump and Canon tend to fail more in the tree benchmarks, as there is a larger search space for the join; guiding appears more critical when the search space for join is larger.

RH3: Clumping has a low overhead. From Figure 11.1(b), we see that ClumpG is comparable in the analysis time with any other configuration, which provides some evidence that clumping has a reasonable overhead. To see this more directly, in the graph below, we show the percentage of the analysis time spent on clumping, join, and other operations for each benchmark. We find that join is a very expensive operation and still takes about half of the analysis time in many cases despite effective clumping. Moreover, we find that in all cases the time spent on clumping (which includes the time to compute silhouettes) is a very small percentage of the total analysis time (no more than a few percent), and much smaller than the time spent on join. Therefore, we can conclude that clumping has a reasonably low overhead. First, we observe that interestingly, the None baseline configuration only succeeds when the number of disjuncts at a loop head is 1. When more than one disjunct is needed for the loop invariant, the silhouette abstraction seems crucial to guiding the inference of a sufficiently precise invariant. Second, in all cases where both ClumpG and CanonG succeed, ClumpG uses fewer disjuncts in the loop invariant, and the difference can be quite significant (e.g., for javl-insert, 3 versus 18). And interestingly, ClumpG is always able to get to a single disjunct at the exit point while proving the post-condition.

From these observations, we hypothesize that being able to clump into the minimal number of necessary disjuncts is crucial to analyzing data structure operations in a client program that makes several such calls. To test this hypothesis, we perform a controlled experiment by sequentially composing a given operation with itself 32 times and trying to prove the shape preservation invariant at the end. The resulting analysis is notably more complex than for the initial code, due to increasingly complex abstract states over call sequences. The results in Figure 11.2(b) show that ClumpG keeps the number of disjuncts constant and scales well, whereas CanonG and None suffer a significant slow-down in the cases where they do not fail.

Related Work on Silhouette-guided Clumping

Several generic techniques are used to handle disjunctions in static analyses. Disjunctive completion [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] adds support for disjunctions to an abstract domain, but never collapses them, and thus is too expensive in practice. Similarly, [START_REF] Giacobazzi | Optimal domains for disjunctive abstract interpretation[END_REF] introduces the least disjunctive basis of an abstract domain as a compact domain with the same disjunctive completion, though this construction does not minimize the size of the representation of the abstract elements. State partitioning [START_REF] Cousot | Abstract interpretation and application to logic programs[END_REF][START_REF] Jeannet | Dynamic partitioning in analyses of numerical properties[END_REF] attaches abstract states to specific sets of states, which effectively allows one to support disjunctive properties while providing a way to control disjunct numbers via the definition of partitions. Trace partitioning [START_REF] Handjieva | Refining static analyses by trace-based partitioning using control flow[END_REF][START_REF] Rival | The trace partitioning abstract domain[END_REF] achieves a similar result using information about traces. However, these studies provide frameworks, and do not address the problem of finding a criterion to clump disjuncts. Silhouettes provide such a criterion, based on the properties of join.

Shape analyses based on three-valued logic [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF], and on separation logic [BCO05, BCC + 07, CRN07, DPV11, BDES12] are known to require disjunctions. The same goes for array analyses [START_REF] Halbwachs | Discovering properties about arrays in simple programs[END_REF]. Several strategies have been designed to limit the number of disjunctions. When summary predicates denote non-empty regions, possibly empty regions create an additional need for disjunctions. Thus, several proposals have been made to let summary predicates denote possibly empty regions [CRN07, YLB + 08, CCL11]. Canonicalization operators [LAS00, SRW02, BCO05, DOY06] collapse abstract states into a smaller, finite lattice, and thereby bound the number of disjuncts. While the analysis may use a larger lattice, precision after applying this operation is limited by the smaller lattice. Join operators [CRN07, YLB + 08] do not require a smaller lattice (and can therefore keep more information), but lack a mechanism to bound the cardinality of disjunctions. To apply join or canonicalization operators efficiently, several strategies have been designed. Arnold [START_REF] Arnold | Specialized 3-valued logic shape analysis using structure-based refinement and loose embedding[END_REF] groups abstract states that satisfy some inclusion relation. Moreover, [YLB + 08] performs a partial join that groups disjuncts only when it syntactically verifies the absence of precision loss. In contrast, our work proposes a criterion based on an abstraction of abstract states, and on the fact that this abstraction is cheaper to compute. A more related study is that by Manevich [START_REF] Manevich | Partially disjunctive heap abstraction[END_REF], that extends TVLA [START_REF] Lev | Tvla: A system for implementing static analyses[END_REF] with a grouping of three-valued abstract states based on a partial graph isomorphism.

Techniques to merge disjuncts have been developed in static analyses for numerical properties as well. For instance, a notion of affinity between polyhedra is used in [START_REF] Popeea | Inferring disjunctive postconditions[END_REF] in order to decide whether they can be joined without too significant a precision loss. This approach is extended in [START_REF] Pham | Fixbag: A fixpoint calculator for quantified bag constraints[END_REF] to deal with set properties. Bagnara [START_REF] Bagnara | Widening operators for powerset domains[END_REF] proposed a widening over disjunctions of polyhedra, that tests for the implication of abstract states to better bound the precision loss.

Existing off-line approaches for the parameterization of static analyses and abstract domains (such as the selection of the abstract domain to use, and of the abstract values to keep) include syntactic heuristics based on code patterns [BCC + 03], machine learning techniques [START_REF] Liang | Learning minimal abstractions[END_REF][START_REF] Oh | Learning a strategy for adapting a program analysis via bayesian optimisation[END_REF], and semantic impact pre-analysis methods [OLH + 14]. The disjunct clumping problem is tied to the abstract states that arise during the analysis, and it is therefore not surprising that it requires an on-line abstraction of these states at analysis time.

Finally, we remark that other analyses that abstract structures with summaries [CCR14], heap abstractions [START_REF] Dillig | Symbolic heap abstraction with demanddriven axiomatization of memory invariants[END_REF], rich type systems [START_REF] Kawaguchi | Type-based data structure verification[END_REF][START_REF] Maxim Rondon | Low-level liquid types[END_REF] or quantified logical assertions [START_REF] Gulwani | Lifting abstract interpreters to quantified logical domains[END_REF] may benefit from adapted forms of silhouette abstraction when facing the disjunction problem.

Conclusion on Silhouette-guided Clumping

In this part of the thesis, we introduced silhouettes that abstract the abstract states. The information enclosed in the silhouettes proves useful not only to clump disjunctions of abstract states, but also to compute better abstract joins. These results were achieved by selecting a definition of silhouettes that provides a weak entailment check over abstract states, and thereby accurately characterizes abstract states that are likely to join well. This characterization is conservative with respect to the standard analysis algorithms: while it will always suggest clumping abstract states that can be joined precisely, it may also suggest clumping abstract states that cannot be joined precisely, although we never observed this behavior in our experiments. This situation is quite similar to that of a static analysis that can be proven sound but is conservative in theory, yet computes very precise results in practice. Our experimental evaluation confirms the effectiveness of the silhouette abstraction, which allows our implementation to verify a large collection of challenging benchmarks at a reasonable cost. The overhead inherent in computing silhouettes is outweighed by the benefits of increased precision and improved scalability.

Part IV

Conclusion

Chapter 12

Conclusion and Future Directions

Conclusion

Separation-logic based shape analysis relies on the separating conjunction (⇤) to describe disjoint properties of local memory regions and inductive predicates to summarize unbounded dynamic data structures within heaps. However, the local predicates are not expressive enough to describe global properties that some complex data structures rely on, and to partition disjunctions.

In Part II, we have set up a shape analysis that is able to cope with data structures with unbounded sharing. The analysis combines separation logic based shape abstractions and a set abstract domain that tracks pointer sharing properties. The real difficulties of the analysis lie in the synthesis of set parameters for summary predicates during folding operations, and the nonlocal unfolding of summary predicates that "jumps" to somewhere in an inductive predicate. To deal with these difficulities, we have specified two kinds of set parameters of inductive predicates, head and constant, and designed an instantiation process for synthesizing set parameters. We have implemented the analysis in the MemCAD static analyzer by augmenting an existing shape domain in MemCAD with a set domain. The advantages of the analysis include that the original domain structures of MemCAD remain mostly unchanged, the analysis is still parametric in the structure to verify, and the modularity of the analyzer is preserved. We have obtained positive results in analyzing a basic graph library, where graphs are described as adjacency lists.

In Part III, we have set up a general framework for disjunct clumping based on abstraction of abstract states, i.e., silhouettes. Generally, abstract states can be clumped if their silhouettes are similar according to a computable silhouette equivalence relation. We have defined and formalized an instance of this framework in separation logic-based shape analysis, where silhouettes simply abstract access path relations between live program variables. It turns out that silhouettes apply not only to the clumping of disjuncts but also to the weakening of separating conjunctions of memory predicates into inductive summaries. We have implemented this approach in the MemCAD analyzer and evaluated it on real-world C codes from existing libraries dealing with doubly-linked lists, red-black trees, AVL-trees and splay-trees. Our experimental evaluation shows that silhouette-based clumping is effective in keeping the size of disjunctions small while preserving the case splits that are required for the analysis to succeed at a reasonable cost.

Future Directions

Several interesting routes for future work could be explored.

Numerical properties of data structures. Invariants of data structures, e.g., binary search trees and red-black trees, consist not only of shape invariants but also of numerical invariants. In order to keep precise numerical properties of data structures, the work presented in paper [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF] proposed inductive predicates with numerical parameters. However, automatically inferring numerical parameters for summary predicates during folding remains a huge challenge. Therefore, similarly to set parameters, identifying the kinds of numerical parameters and designing a precise instantiation process for the kinds of numerical parameters are necessary. In addition, a disjunct clumping that is based not only on shape properties but also on numerical properties should be explored. As a consequence, silhouettes and silhouette equivalence relations for the clumping of different numerical abstractions should be designed.

Abstractions of DAGs.

A directed acyclic graph (DAG) is a finite directed graph with a topological order of nodes, such that any node of the graph can only have out-edges to nodes later in the order. Our abstract domain does not provide a way to abstract the topological order of nodes, and thus cannot abstract DAGs precisely. As DAGs can be used to model many different kinds of data information, such as ordering the compilation operations in a makefile and representing sequences of binary choices, it is necessary to extend the domain in order to analyze programs that handle DAGs is necessary. Intuitively, the extension may require the set domain to be extended in order to abstract orders of sets.

Sharing properties of recursive procedures. Recursive procedures that manipulate dynamic data structures often lead to pointer sharing properties between the call stack and the dynamic data structure, and deferences of the data structure from the call stack. The sharing is usually unbounded. As our analysis is able to track unbounded pointer sharing properties with set abstractions and deferences of the data structure from the call stack might be handled by non-local unfolding, an application of our analysis to recursive procedures might be explored.

Clumping abstract states in other analyses. Similarly to shape analysis, array analysis (which deals with contiguous structures indexed by ranges of integers) and dictionary analysis (which handles structures indexed using sets of keys) also implicitly or explicitly use separation and summarization to abstract sets of concrete memory states, and rely on disjunctions for the sake of precision. In these analyses, deciding how to create summarization in joining and whether or not to keep case splits is also critical. Therefore, the disjunct clumping of abstract states based on silhouettes in these analyses might also be studied.

�������

  Figure 1.1: A binary search tree

s t r u

  Figure 1.2: A minimum element deletion function of a singly linked list

  Figure 1.3: A list allocation program with memory leaks

Figure 1 . 5 :

 15 Figure 1.5: Type definitions for adjacency lists

Figure 1

 1 Figure 1.6: Example of an adjacency list

  Figure 1.8: Searching the minimum and maximum list elements

Figure 1 . 9 :

 19 Figure 1.9: Concrete memories with list segments

Figure 2 . 1 :

 21 Figure 2.1: The Syntax of a C-like simple imperative language.

Figure 2 . 2 :

 22 Figure 2.2: Characterizations of store operations

  Figure 2.3: Semantics of left and right value expressions

•

  Variable x points to a list with four elements: . . . . . . . . . 0 . . . &x Further details about inductive definitions and the concretization of inductive predicates are given in Chapter 4.

Figure 2 . 5 :

 25 Figure 2.5: Abstract store operations

  Figure 2.6 shows the abstract semantics of the additive operator + and the equal test operator ==.

Figure 2

 2 Figure 2.7: Abstract denotational semantics of program statements

  Figure 2.7 thus needs to compute an abstract post fix-point for the loop, denoted as lfp v D λd 1 . d t D JpK • guard D Jr 6 = 0K(d 1 ), to over-approximate the concrete least fix-point. In practice, the abstract post fix-point can be computed by a series of iterations with the widening operator O D defined as: d 0 0 = d and d 0 n+1 = d 0 n O D JpK • guard D Jr 6 = 0K(d 0 n ). The termination and soundness properties of the widening operator O D ensure an abstract post fix-point can always be reached.

  Signature for disjunctive memory abstract domains. abstract states d 2 D concretization γ D : D ! P(E ⇥ H) guard guard D : D ⇥ C V ! D abstract join t D : D ⇥ D ! D abstract widen O D : D ⇥ D ! D inclusion check v D : D ⇥ D ! {true, false} Part II

  Figure 3.2(b) shows an adjacency list representation of the graph shown in Figure 3.2(a).

Figure

  Figure 3.1: Type definition of adjacency lists

Figure 3 . 3 :

 33 Figure 3.3: Inductive definitions of adjacency lists g ↵ nodes(E , F ) � E ✓ F (a) Fully summarized abstract state

  Figure 3.4: Abstract states of graphs

  Figure 3.5: A representative path traversal function through a graph

Figure 4

 4 Figure 4.1: Inductive rules

Figure 4 . 2 :

 42 Figure 4.2: An abstract state

  Figure 4.4: Abstract shape graphs and their concretization

Definition 5. 1 (

 1 Set predicates). Set predicates are defined by the following grammar: set predicates c T ::= c T ^cT | e T ✓ e T | e T = e T | v 2 e T | true | false set expressions e T ::= ; | {v} | E | e T [ e T | e T ] e T A set predicate c T 2 C T denotes a set of valuations which satisfy the predicate, that is {µ | µ ✏ c T }. For clarity, we give a formal definition of µ ✏ c T in Figure 5.1, where the semantics Je T Kµ of a set expression e T under a concrete valuation µ is a set of concrete values.

Chapter 5 .

 5 Abstract Domains for Set Reasoning Definition 5.3 (Concretization). Given a linear set abstract element (c l , c e , c i ) 2 S, γ S (c l , c e , c i ) = {µ | µ ✏ c l ^ce ^ci } Abstract operators. A great advantage of linear set abstract domain is that it allows fast abstract operations.

  Example 5.4 (Abstract guard operations). Let c l = (F = {↵} ] E ), c e = true and c i = true, then:guard S ((c l , c e , c i ), E = {β} ] E 1 ) = (c l ^E = {β} ] E 1 , c e , c i ) and guard S ((c l , c e , c i ), F = {β} ] E 1 ) = (c l , c e , β 2 F ^E1 ✓ F )The abstract operation project S (s, E ) either drops all the constraints related to E from c l , c e and c i of s or replaces E with another equal set variable. Example 5.5 (Abstract project operations). Let c l = (F = {↵} ] E ), c e = (E = E 1 ) and c i = true, then: project S ((c l , c e , c i ), ↵) = (true, c e , E ✓ F ) and project S ((c l , c e , c i ), E ) = (F = {↵} ] E 1 , true, true)

Figure 5 . 3 :

 53 Figure 5.3: Translation function tr E

  Example 5.6 (Abstract joining operation). Let c l = (F = {E 1 } ^E2 = ;), c e = true and c i = true, and c l 0 = (F = {↵} ] E 1 ^E2 = {↵}), c e 0 = true and c i 0 = true then:

Figure 6 . 1 :

 61 Figure 6.1: Abstract states and unfolding

Figure 6

 6 Figure 6.2: Non-local unfolding

Figure 6 . 4 :

 64 Figure 6.4: Extended inclusion checking over shapes and abstract states G ⇥ C

Figure 6 . 5 :

 65 Figure 6.5: An example of inclusion checking over shapes

Figure 6 . 7 :

 67 Figure 6.7: Extended joining over shapes and abstract states G ⇥ C

Figure 6 . 8 :

 68 Figure 6.8: An example of joining

  Figure 6.8 shows a simplified instance of a join taken from the analysis of the program of Figure 3.5. The input abstract states and output abstract state are shown at the bottom.

Figure 6 . 9 :

 69 Figure 6.9: Local invariants computed over the first iteration

Figure 7

 7 Figure 7.1: Tree fragments and need for disjunctions

i

  Figure 7.4: Selected abstract states from the analysis of an insertion into an AVL tree (4 disjuncts out of 32).

Figure 7 . 5 :

 75 Figure 7.5: Weakened abstract state m 1,2,3 .

  Figure 8.1: Definition of abstract states

Example 8. 2 (

 2 Silhouette computation). Let us consider the abstract state m below: t ↵ x β tree tree We have ⇧(↵ • tree ⇤= β • tree) = {(↵, (l + r) ⇤ , β)} and ⇧(β • tree) = ;. Thus, ⇧(m) is the silhouette shown in Example 8.1.

  Example 8.3 (Silhouette restriction). Let us consider the abstract state shown in Example 8.2, ⇧(m, {t}) is ; and ⇧(m, {x}) is ;. Theorem 8.2 (Soundness of silhouette restriction). Given a silhouette s = (N, E) and a set of nodes N 0 ✓ N, γ S (s) ✓ γ S (s dN 0 )

  Chapter 8. Silhouette Abstractions: Abstraction of Memory Abstract States

Chapter 9 .

 9 Silhouette-Guided Joining of Abstract Memory StatesExample 9.1 (Abstract states join). As an example, let us consider the abstract states below:

  Chapter 9. Silhouette-Guided Joining of Abstract Memory States 127There are several possible joinings, two of which are presented below:• first pairing each of the four edges of m with an edge of m 0 by applying the j-pt rule produces a joining result with very precise information about t, y, but which discards all information about x:

  Figure 9.1: Branching node

Figure 10 . 1 :

 101 Figure 10.1: Abstract state candidates for clumping.

Figure 10 . 4 :

 104 Figure 10.4: Widening disjunctive abstract states.

Chapter 10 .

 10 Silhouette-Guided Clumping and Widening 141 states d and d 0 , the analysis either simply returns d _ d 0 or applies clumping (Section 10.1) to d _ d 0 in order to reduce the disjunction size. For loops, the silhouette-guided O D operator (Section 10.2) enforces the convergence of sequences of disjunctive abstract states in order to compute an abstract fix-point.

  Number of benchmarks verified using each strategy.

Figure 11 . 1 :

 111 Figure11.1: Successful verification times with different analysis strategies. The clumping with guided join strategy can verify significantly more benchmarks than any other strategy and over 3x more than the None baseline-and all at similar costs in analysis time.

Figure 11 . 2 :

 112 Figure 11.2: Clumping limits disjunctive explosion.

156

  Chapter 12. Conclusion and Future Directions

  Pointer Analyses and Shape Analyses . . . . . . . . . . . . . . . . . . . . . . . . . Other Shape Analyses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.5 Outstanding Challenges in Shape Analysis . . . . . . . . . . . . . . . . . . . . . . 1.5.1 Reasoning about Sharing in Separation Logic Based Shape Analysis . . . 1.5.2 Improving Scalability and Disjunction Control . . . . . . . . . . . . . . . . 1.6 Outline and Contributions of the Thesis . . . . . . . . . . . . . . . . . . . . . . . 2 Separation Logic Based Shape Analysis 2.1 A Simple Imperative Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.2 Concrete States . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1.3 Concrete Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Abstract Interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

I Introduction to Shape Analysis v

1

Introduction 1.1 Dynamic Memory Allocation and Dynamic Data Structures . . . . . . . . . . . . 1.2 Software Problems Involving Pointers and Dynamic Data Structures . . . . . . . 1.2.1 Memory Safety Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2.2 Security Problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3 Improving Software Quality Against Memory problems . . . . . . . . . . . . . . . 1.3.1 Systematic Software Development . . . . . . . . . . . . . . . . . . . . . . . 1.3.2 Testing and Code Reviewing . . . . . . . . . . . . . . . . . . . . . . . . . 1.3.3 Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4 1.4.1 Pointer analyses. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4.2 Three-valued Logic Based Shape Analyses . . . . . . . . . . . . . . . . . . 1.4.3 Separation Logic Based Shape Analysis . . . . . . . . . . . . . . . . . . . 1.4.4

  instantiate a generic list segment predicate

												Chapter 1. Introduction
	hd ↵ 1	list	min ↵ 2	list	max ↵ 3	list	c ↵ 4	list	_	hd ↵ 1	list	max ↵ 2	list	min ↵ 3	list	c ↵ 4	list
			Figure 1.10: A disjunctive abstract state with list segments
	↵ • list ⇤= β • list to abstract a segment of the list starting at ↵ and finishing with a pointer to
	β. Using this abstraction, the concrete memory state in Figure

  080.

		Chapter 2. Separation Logic Based Shape Analysis
	Binary operators	⊕ ::=
		| == | 6 = | < | <= | . . .
	Left value expressions	l ::=
		| x	variable
		| *l	pointer dereference
		| l.f	field access
	Right value expressions	r ::=
		| n	integer
		| l	l-value read
		| r ⊕ r	binary operation
		| &l	address of l-value
	Statements	p ::=
		| x	variable declaration
		| l = r	assigment
		| l = malloc(n)	memory allocation
		| free(l, n)	memory de-allocation
		| assert(r)	assertion
		| if(r){p}else{p 0 }	conditional branch
		| while(r){p}	loop
		| p; p	sequence

  Separation Logic Based Shape Analysis Example 2.11 (Unfolding a list inductive predicate). Let us consider the unfolding of the inductive predicate ↵ 2 • list from the abstract state below:

Table 6 .

 6 Chapter 6. Static Analysis Algorithms for Unstructured Sharing Abstractions 97 1: Analysis of a set of fundamental graph manipulation functions. Analysis times (in milliseconds) are measured on one core of an Intel Xeon at 3.20GHz with 16GB of RAM running Ubuntu 14.04.2 LTS (we show overall time including front-end and iterator shape domain and set domain), with "BDD" and "LIN" set domains. "Property" columns: inference of structural properties.

	Description	LOCs Nested	"BDD" time (ms)	"BDD"	"LIN" time (ms)		"LIN"
			loops Total Shape Set Property Total Shape Set Property
	Node: add	27	0	44	0.3	11	yes	28	0.3 0.2	yes
	Edge: add	26	0	31	0.2	4	yes	27	0.2 0.1	yes
	Edge: delete	22	0	45	0.4	16	yes	30	0.3 0.2	yes
	Node list traversal	25	1	117	1.5	87	yes	28	0.5 0.3	yes
	Edge list iteration + dest. read	34	1	332	2.7 293	yes	36	3.5 2.4	yes
	Graph path: deterministic	31	2	360	2.7 323	yes	35	2.4	2	yes
	Graph path: random	43	2	765	7.1 711	yes	41	4.1	3	yes

  1 ), . . . , (v k-1 , e k , v k ) 2 E, e = e 1 • . . . • e k Chapter 8. Silhouette Abstractions: Abstraction of Memory Abstract States 119

  Analysis times are only reported if all assertions are successfully verified, including the preservation invariant in post-conditions. > indicates a failure to verify (due to precision loss). Run times (in seconds) measured on one core of a 3.20GHz Intel Xeon with 16GB of RAM. Times are reported as an average of three runs.

	Benchmark	ClumpG	Clump	CanonG	Canon	None
	sll-delmin	0.04	>	0.05	>	>
	sll-delmin †	0.04	0.05	>	>	>
	sll-delminmax	0.12	>	0.42	>	>
	sll-delminmax †	0.20	0.20	>	>	>
	bstree-find	0.03	>	0.05	>	>
	bstree-find †	0.04	0.04	0.11	0.11	>
	psll-reverse	0.02	0.02	0.02	0.02	0.02
	psll-isort	0.03	0.03	0.04	0.04	>
	psll-bsort	0.04	0.04	0.04	0.04	0.06
	gdll-findmin	0.61	0.61	0.62	>	0.61
	gdll-index	0.61	>	0.62	>	0.61
	gdll-findmax	0.61	0.61	0.62	>	0.60
	gdll-find	0.62	0.62	0.63	0.65	>
	gdll-delete	0.62	0.63	0.63	0.64	>
	gbstree-find	0.59	>	0.59	>	0.58
	gbstree-insert	0.65	>	>	>	>
	gbstree-delete	1.64	>	1.71	>	1.39
	bsplay-find	0.28	>	0.56	0.56	>
	bsplay-delete	0.48	>	1.08	1.07	>
	bsplay-insert	0.30	>	0.62	0.62	>
	brbtree-find	0.36	>	0.36	>	>
	brbtree-insert	1.07	>	>	>	>
	brbtree-delete	6.06	>	>	>	>
	javl-find	0.19	>	0.19	>	0.19
	javl-free	0.18	0.19	0.19	0.18	0.19
	javl-insert	1.84	>	5.22	>	>
	average (all)	0.66	0.28	0.68	0.39	0.47
	verified	26	11	21	10	9
	(b)

  The maximum number of disjuncts at a loop head (Fix), at any program point (Max), and at the exit point (Post) produced by the ClumpG, CanonG, and None analysis configurations. Synthesize a new benchmark by sequentially composing a data structure operation 32 times to simulate multiple operations in sequence (times in seconds).

	Chapter 11. Experimental Evaluation of Silhouette-Directed Clumping	149
			ClumpG			CanonG			None
	Benchmark	Fix	Max	Post	Fix	Max	Post	Fix	Max	Post
	gdll-find		2	6	1	2	6	2	>	>	>
	gdll-delete		2	6	1	2	6	2	>	>	>
	gbstree-find		1	3	1	1	3	3	1	3	3
	gbstree-insert		2	4	1	>	>	>	>	>	>
	gbstree-delete		1	69	1	2	68	1	1	54	54
	bsplay-find		3	42	1	5	89	1	>	>	>
	bsplay-delete		3	42	1	5	89	1	>	>	>
	bsplay-insert		3	42	1	5	89	1	>	>	>
	brbtree-find		1	13	1	2	8	2	>	>	>
	brbtree-insert		3	51	1	>	>	>	>	>	>
	brbtree-delete		3	108	1	>	>	>	>	>	>
	javl-find		1	3	1	1	3	1	1	3	3
	javl-free		1	2	1	1	2	1	1	>	>
	javl-insert		3	120	1	18	240	1	>	>	>
	max		3	120	1	18	240	3	1	54	54
	(a) ClumpG			CanonG			None
	Benchmark		Time		Post		Time	Post		Time	Post
	gbstree-find		3.3	1		2.18	1		40.79	158
	brbtree-insert		60.2	1		>	>		>	>
	javl-find		0.63	1		>	>		3.77	158
	javl-insert average (all)	sll sll	129.9 48.5075	1 1	526.17 264.175	1 1	clump	> 22.28	> 158
	(b)	dll
		gbst bst							join
		spt							other
		rbt
		avl						% time spent

  ���������� ��������� ���� ����������� ������� ��� ��������� ���������������� ���� ����������� ������������ �������� ����� ������� ���� ������������ ��� ������������� ����� ��� ���� ���� ����������� ����������� ���� ����������� ��� �������� ���������� ��� ��������� ���������� ��������� ����� �������� ���� ����������� ������� ����� �������� ��� ������� ���� ������ �� ��� �������� ��� ��� ������������� ������������� ������������� ��������� ����������� ��� ��� ����� ����������� ���� ������ ��������� ���������� ������������ ���� ���� ������������� ��� �������� ��� ����������� ����� ���� ���������� ��� ����� ���������� ���� ������ ��� �������� ���������� ��� ����� ��������� ���� �������� ������������ ��� ��� �������� ������� ���� ���� ������� ��� ���� �������� ��� ������� ��������� ���������� �������� ���� ������������� ������� �������� ��������� ���������� ����� ��� ������ ��������� ������ ���������������� ���� ��������� ����������� ���������������������������������������������������������� �������������������������������������������� �������������������������������������������������������������� �������� ������������ ������� ���� ����������� ��� �������� ������������ ��� ����� ��� ��� ��������� ��� ���������� ����� ���� ������������������������������������������������������������ ���� ���� ����������� ����������� �������������� �� ���� ������ ��� �������� ��� ��� ��������� ���� ���� ���������� ���������� ��������� ���� ���� ���������� �������������� ���� ��������� ��������� ������������������������������������������������������������ �������� ��� ���������� �������������� ��� ���� ����� �� ������������ �������������� ������� ���� ���������� ���������� ���� ������������ �������������������������������������������������������������� ������ ��������� ���� ���������� ��� ������������� ������� ����� ����������� ��� ����� �������� ���� ����������� �������� ��� ���������������� �������� ����������� ������ ������ ���� ���������� �� �������� ��� ��� ����� ��� ������ ��� ���������� ��� �������� ��� ����������������������������������������������������������� ������������ ������ ���� ���� ����������� ����������� ������������ ����� �������� ���� ���������� ������������� ���� ����������� ������������������������������������������������������������� ���� �������� ��������� ����������� ��� ���������� ������������ ���� ���� ������ ��������� ��� ����� ���� ��������� ����������� ���������� ��� ����������� �������������� ��� ����������� ��� ������� �������������������������������������� ����� ���������� ��� ������������� ���� ������������ ������������� ������ ���� ���� ���������� ������������ ���� �������� ����� ���� ��������� �������������� ����� ���� ���������� ���������� ������� ��� �������������� ��� ���������� ��� ����������� �������������� ���������� ����� ������ �������� ��� �������� ��������� ����� ����������� ���� �������� ��� ����������� ���������������������������������������������������������� ����� ���������� ��� �������� ����������� ����������� ��� ���������� ���� ������ ��������� ���������� ����������� ��� ��� ������� ���� ����� ������������ ������ ��������� ������������� ����������������������������������������������������������������� ������������������������������������������������������������ ��� ������� ��� ������� ����� ���� ������������� �������� ��������� ����� ���������� �� ������������������ ��� ������������� ��� ����������������������������������������������������������� ������������������������������������������������������������ ��������������������������������������������������������������� ��������� ����� ���� ���������� ��� �������� ����� �������� ����� ������ ����������� ���� �������������� ��� ����� ��� ������������ ������� ��� ����� ��� ������ ��������� ��������� ���� ���������� ��� �������������� ����������� �������� ��� �� ��� ������������� ������������ ����������� ��� ��������� ��������� ���� ������� ������������������������������������������������������� ���� ��� ���� ������� ����������� ���� ���������� �������������� ��������� ���� ������ ��������� ���� �� ����� ��� ���������� ��� ������� ���� ������������� �� ���� ����� ��� ������������ ����� ����� ����������������������������������������� ���������� ���������������������������������������������������� ������������������������������������ ��������� ������ ��������� ����� ��� ����������� ��������� ��� �������� ����������� ��� ������ �������� ����������� ������������ ����� ����� ������� �������� ���������� ������������� � ���� ������ ������� ����������� ��� ��������� �������� ����� �������� ����� ����������� ���� ��� �������������� ���������� ����� ����� ��������� ����������� ��������� ������� ������� ����� �������� ��� ����������� ������������� ��� ������ ����������� ����������� ������� ������� ��� �������� ����������� ����� ��������� ���������� ������������������������������������������������������������������������ ����� ���� ������� ������������� ��� ��������� ������� ������� ��� ������ ��� ����� ����� �������� ����������� �������� ��������� ��������� ��������� ����������������������������������������������������������������� ���������������������� ����������������������������������������������������������������� ������������������������������������������������������������������������� ������������������������������������������������������������������ ��������������������������������������������������� ���� ��������� ����������� ����� ����� ��� ������ ����� ���������� ����� ��� ���������������� ��� ������� ������� ���� ���������������� ���������� ��� ���������������������������������������������������������������������� ��� ����� ������ ���� ���� ����� ��� ������������ ��������� ������ ����������� ���������������������������������������������������������������������� �������� ��������� ���� ��� ������� �������� ��������� ����� ���� ������ ������������ ��� ����� �������� ��� ������ ����������� ������������������ ������ ����������� ���� ���� �������� ��������� ������������ ��� ������������ ��������� �������� ���� ��������� ����������� ����� ����� ��� ��������� �������������� ��� ��������� �������� � ��� ����� �� ������������ ���� ��� ������������������������������������������������������������������ ������ ����������� ���� ����� ����������� ���� ������������ ����� ����������� ����� ���������� �������� ���� ���������� ���� ��� �������� ��������������������������� ���������������������������������������������������������������� ����������� ����� ���������� ������������ �������� ���� �������������� ���� ������ ��������� ��� ����������� ����� ���������� ��������� ��� ���������������������������������������������������������������� ��������������������������������������������������������������� ���� ��������� �������� ������ ���� ���� ������������� ���� ����� ��� ������ ���������� �������� �������� ������������ ������ ��� ����� ��������� �������� ��� ��������� �� ������ ��� ��������� �������� ����� ���������� ����������������� ��� ������� �� �������� ��������� ���������� ��� ������ ��������� ������� ������� ������ ��� ������ ������������ ����� �������� ������� ������ ������������ ����� ��������� ��������� ������� ����� ������ ������������ ���� ��������� ������������ ������ ���� ����� ��� ���� ������������� ������ ��� ���������� ���� ����� ��� ���� ���������� ��� ����������� ������������� ��� ���������������������������������������������������������������� ��� ��� ������� ������ ���� ��������� ���������� ����� ���� ��� ����������� ���� ����� ������� ����� ���� ��������� ���� ���� ��������� ��� ��������� ��� ���������� ����� ��������� ��� ���� ������� ��������� ���� ��������� ��� ��� ����������� �� ���������� ���� ���������� ����� ������������ ���������� �������������� ������� ���������� ����������������� ���� ����������������� ������������� �������� ����� ����� ���� ��������� ��� ����� ��� ����� ���� ����� ��� ������������� ������ ���� ������������ ���� ��������� ����� ������� ���������������������������������������������������������

	���������
	������������������������������������������������������������ �������������

i n t i = 3;

i n t * p = & i ;

* p = * p + 1;

https://coq.inria.fr

http://pvs.csl.sri.com

Chapter 10. Silhouette-Guided Clumping and Widening

Set Abstractions

A set abstraction s 2 S is concretized into a set of concrete states:

Moreover, we assume that set abstract domains always contain the ? and > abstract elements, which are respectively concretized into the empty set ; and the full set V.

Example 5.1 (Singleton set domain). A very basic example of such a domain is the singleton set domain that comprises: ?, > and a function from set variables T into their singleton value V. For instance, the abstract element {E 7 ! ↵, F 7 ! β} stands for E = {↵} ^F = {β} and can be concretized into {µ | µ ✏ E = {↵} ^F = {β}}. Original joining algorithm. The original joining process designed for abstract states G ⇥ N is formalized in Figure 6.6, and consists of a joining process over abstract shapes and a joining process over numerical abstractions, as shown by the j-val rule. The principle of the joining algorithm over abstract shapes is to select pairs of regions in both input shapes and compute an over-approximation for each pair of regions relying on the j-sep rule. Specifically, based on the j-pt and j-ind rules, when both input regions contain syntactically equal atomic predicates, the join then simply returns the same shape as an over-approximation. When one input region contains a summary predicate, the j-weak rule attempts to weaken the other region into the summary predicate with the inclusion checking algorithm. In addition, the j-intro rule synthesizes a segment between ↵ and β when either input contains a region subsumed by the segment, and the other input implies ↵ = β which corresponds to an empty segment.

Extended joining algorithm. Figure 6.7 shows the extended joining algorithm of abstract states G ⇥ C that is able to handle set parameters of summary predicates. Similarly to the join system shown in Figure 6.6, the extended join algorithm over shapes first selects regions of both inputs that can be over-approximated based on the ej-sep rule and then relies on two generic sets of rules to join each region. The first set of rules states that, if both inputs contain a same region g, then these regions can be joined immediately. It is applied for points-to and inductive predicates as shown by the ej-pt and ej-ind rules, and segment predicates, for which the rule is omitted for simplicity. The second set of rules applies to cases where the input regions are different and thus weakening is necessary: if a common over-approximation g o for g l and g r can be found and checked with v G , abstract join can rewrite these into g o . We note that this set of rules may extend the set predicates, as fresh set variables are introduced by the inclusion check algorithm. Nevertheless, this process is non-trivial, since the joining algorithm needs to infer relations over the new set variables, from the results of the inclusion checking. Specifically, the joining algorithm attempts to perform the weakening in the following cases:

Part III

Silhouette-guided Disjunct Clumping

Chapter 7

Overview

In this part, we propose semantic-directed clumping of disjunctive abstract states: a semantic criterion to clump abstract states based on their silhouette, which applies not only to the conservative union of disjuncts but also to the weakening of separating conjunctions of memory predicates into inductive summaries. Before the formalization, in this chapter, we first introduce the disjunct clumping problem and describe the core idea of using silhouettes in disjunct clumping of abstract memory states at a high level.

Semantic-Directed Disjunct Clumping

In this section, we first recall the disjunct clumping problem in shape analysis, which is originally introduced in Section 1.5.2. Then, we overview our approach to disjunct clumping based on the use of an abstraction of abstract states. h -> l = y = p = t ; x = h ; // phase 1: insertion point localization while ( 1 ) { i f ( i < p -> d ) q = p -> l ; e l s e q = p -> r ; i f ( q == null ) break ; i f ( q -> bal != 0 ) { x = p ; y = q ; } p = q ; } // phase 2: insertion at position p ... // phase 3: rebalancing at position x , y ... }

Disjunct Clumping Problem

Following the inductive definition, the abstract state on the right hand side of Figure 7.3 describes states where t points to a tree, and x points to a (possibly non-strict) subtree of the tree pointed to by t. It is made up of the separating conjunction of a tree segment ↵•tree ⇤= β •tree summary and an inductive predicate β • tree. An example of concrete memory is shown on the left hand side of the figure.

The analysis performs a forward abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], starting from an abstract precondition that takes into account all the possible valid call states, that is all the memory states where t points to a non-empty, well-formed tree (described by tree). It computes abstract post-conditions for each statement, and unfolds summaries on-demand: for instance, in the first iteration p = t, and at line 14, the reading of field d of the node pointed to by p requires unfolding the tree summary predicate attached to t. Such unfoldings generate disjunctions of case splits. Conversely, join and widening applied at loop head should fold back case splits, so as to compute a loop invariant.

The disjuncts merging challenge. Fig. 7.4 describes a few abstract states that are observed at line 25, at the exit of the first loop, and that illustrate the challenges of clumping disjuncts.

The figure shows abstract states, the generic form of concrete memories they represent and their silhouettes, which will be explained below. For concision, and as only the relative positions of cursors matter, we focus on t, x, y and omit fields d, bal, and variables h, p, q. Labels t, x, y decorate the nodes that represent their value. Moreover, we show only a sample of 4 out of 32 disjuncts:

• Abstract state m 0 abstracts memories where x, y were not advanced.

• Abstract state m 1 abstracts memories where x was advanced to the root of the tree, and the search continued in the left subtree.

• Abstract state m 2 abstracts memories where the search visits the left subtree of t, x is advanced into that subtree, and y is the left child of x.

• Abstract state m 3 describes a similar condition to m 2 but when the search visits the right subtree of t and x is a left child.

Some of these abstract states are very similar to each other and can be joined to reduce the cost without significantly affecting the precision of the analysis. Indeed, x and y occupy the same relative positions in m 2 and m 3 ; moreover, in both cases the two cursors point to subtrees of t. Thus, both m 2 and m 3 can be approximated by an abstract state with a segment from t to x and where y is the left child of x. Furthermore, m 1 can also be weakened similarly: the relative positions of x, y are the same, and the only minor difference is that x is not a strict subtree of t since t = x, but this equality can also be described by an (empty) segment. On the other hand, m 0 abstracts very different memories, where x is not a subtree of t, so it cannot be described with a segment from t to x. Any abstract state that over-approximates both m 0 and Chapter 8

Silhouette Abstractions: Abstraction of Memory Abstract States

This chapter formalizes silhouettes, and shows that they provide a useful abstraction to reason about the weakening of abstract states. Specifically, Section 8.1 formalizes silhouettes and their computation; Section 8.2 studies the relationship between entailment checking of abstract states and silhouettes.

Silhouette Abstraction

In this section, we first formalize silhouettes in Section 8.1.1, and then provide the computation of silhouettes in Section 8.1.2.

Definitions

Before formalizing silhouettes, we first simplify the abstract states introduced in Section 2.3 so as to be able to give a clear presentation of the principle underlying our approach. Specifically, we omit abstracting memory cells of program variables as they do not have any effect on clumping disjuncts, and we replace numerical abstractions with simple numerical constraints expressing equalities and disequalities.

Abstract states. An abstract value v 2 V is either a symbolic variable ↵ 2 V ↵ or the symbolic value of a program variable x 2 X . An abstract state m 2 M ! (formalized in Figure 8.1) describes a set of concrete memory states. It is either ?, > or a separating conjunction of region predicates that abstract separate memory regions [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] in conjunction with numerical constraints such as equalities and disequalities.

The logical meaning of an abstract state m is defined by its concretization γ M! (m) ✓ H ⇥ (X ! V), as a set of pairs made up of a memory store σ 2 H and an evaluation function µ 2 X ! V that maps each program variable to its concrete value. In addition, for each concrete state (σ, µ) 2 γ M! (m), there exists a valuation function µ 0 2 V ↵ ! V mapping each symbolic is_leq false; q 0; 3 :

while q <= k && is_leq == false 4 :

if v S (s p , s 0 q ) then is_leq =v M! (m p , m 0 q ); 5 :

q + +; 6 :

if is_leq == false then return false; 7 : return true; • Case of the i-sep rule:

Applying the induction hypothesis to the proofs of

1 ) and by definition of v S , ⇧(m 0 ⇤ m 1 ) v S ⇧(m 0 0 ⇤ m 0 1 ). Then, based on Definition 8.4 and Definition 8.5, given s 0 v S s 1 , we can easily prove that for every edge (v 0 , e, v 1 ) of s 1dN 0 , there exists (v 0 , e 0 , v 1 ) of s 0dN 0 , such that L (e 0 ) ✓ L (e). That is, s 0dN 0 v S s 1dN 0 . ⌅ Weak entailment check algorithm. From this theorem follows the core principle of our approach: while the most direct way to check if γ M! (m 0 ) ✓ γ M! (m 1 ) consists in applying the (fairly expensive) v M! (m 0 , m 1 ) proof search algorithm, an alternative approach consists in computing v S (⇧(m 0 ), ⇧(m 1 )) first and computing v M! only when v S returns true. Indeed, if v S returns false, then v M! will also definitely return false, though at a much higher computational cost. Following the same principle, in Figure 8.2 we show the silhouette-based weak entailment check algorithm on disjunctive abstract states.

Example 8.5 (Entailment). Figure 8.3 shows a few abstract states and their silhouettes drawn from the example given in Chapter 7. Let us consider checking the disjunctive abstract state d = m 0 _ m 1 _ m 2 is included in itself according to the algorithm shown in Figure 8.2. First, as v S (s 0 , s 0 ) = true, we thus need to prove v M! (m 0 , m 0 ) = true. Then, as v S (s 1 , s 0 ) = false, we can omit a complex computation of v M! (m 1 , m 0 ), which will definitely return false. Moreover, as v S (s 2 , s 0 ) = false and v S (s 2 , s 1 ) = false, we can also omit complex computations of v M! (m 2 , m 0 ) and v M! (m 2 , m 1 ). Indeed, with the

Silhouette-Guided Clumping and Widening

This chapter demonstrates that silhouettes can be used in order to precisely compute the clumping and widening of disjunctive abstract states. Specifically, Section 10.1 presents silhouette-guided clumping based on an equivalence relation of silhouettes and silhouette-guided joining. Furthermore, Section 10.2 defines silhouette-based widening of disjunctive abstract states, i.e., relying on silhouettes to select which pair of disjuncts to be widened together for more precise widening results.

Silhouette Guided Clumping of Abstract States

In this section, we first show that silhouettes need to be generalized in order to easily recognize silhouette similarities at the silhouette level in Section 10.1.1. Then, we define a silhouette clumping equivalence relation in Section 10.1.2. Intuitively, the relation is used to indicate whether abstract states can be joined precisely. In Section 10.1.3, we present a clumping algorithm.

Silhouette Generalization

While the silhouettes of abstract states defined in Sect. 9.2.3 are restrictions of silhouettes directed to live variables, they still adhere too closely to the structure of the abstract states to highlight all the possibilities for clumping. For instance, Fig. 10.1 shows two abstract states m, m 0 taken from the abstract states of the analysis of the AVL tree insertion program shown in Figure 7.2. The silhouettes of m and m 0 are shown on the right side, and apparently are not equal. Yet, the two abstract states could be clumped as they both can be weakened into a tree segment predicate from t to x without harming the analysis as discussed in Section 7.2.

To recognize silhouette similarities in configurations such as that given in Figure 10.1, constraints should be generalized so as to make segment patterns easier to recognize at the silhouette level. Since segments correspond to regular expressions of the form (f 0 + . . . + f k ) ? , the following generalization function makes such patterns appear more prominently:

Chapter 10. Silhouette-Guided Clumping and Widening

. Thus, Φ(⇧(m, s)) ./ Φ(⇧(m 0 , s)) holds. As observed in Example. 9.2, joining these two states is precise with respect to X.

On the other hand, if X = {t, x, y}, we obtain ⇧(m, b X) = {(t, ✏, x), (x, l, y)} and ⇧(m 0 , b X) = {(t, l, x), (x, ✏, y)}, and thus Φ(⇧(m, b X)) ./ Φ(⇧(m 0 , b X)) does not hold. Indeed, we observed that joining them would incur a precision loss.

With the silhouette association relation, we now can define the equivalence silhouette clumping relation ⇠.

Definition 10.3 (Clumping relation ⇠). Given a set of silhouettes S = {s 0 , . . . , s n }, the clumping relation ⇠ is defined as the transitive closure of ./:

The clumping relation ⇠ is symmetric, reflexive, and transitive.

Example 10.4 (Clumping relation). Let us consider the silhouette in Example 10.2, we can get that: s 0 ⇠ s 1 ⇠ s 2 . 1. It first computes the silhouette of all the abstract states and the generalized form of these silhouettes, where the generalized forms are used in order to compute ./.

Clumping Algorithm

2. It then groups silhouettes that are connected components of the silhouette association relation ./, such that each group is an equivalence class of silhouette clumping relation ⇠. Moreover, each group is sorted as a sequence of silhouettes such that any silhouette (except the first one) in the sequence is associated with a previous silhouette.

3. For each group, the sequence of silhouettes suggests a sequence of abstract state joins, that are expected to preserve silhouette joins by utilizing silhouette-guided joins to enable semantic-guided synthesis of summary predicates as shown in Chapter 9. We note that this join order has no relevance to the soundness of the algorithm.

This clumping algorithm is sound : it returns a disjunctive abstract state that over-approximates m 0 , . . . , m n :

Theorem 10.2 (Clumping soundness). For each disjunctive abstract state m 0 _ . . . _ m n and for every set of variables X, we have:

Proof. The soundness is a direct consequence of the soundness of silhouette-guided joining. ⌅

for p = 1 to l 9 : Following Theorem 10.1 and Theorem 9.2, this algorithm will not attempt to compute abstract state joins that will not succeed in producing a precise result in the silhouette level. However, clumping may propose to clump states that do not join well, for example, when the join of silhouettes indicates synthesizing a segment in abstract states join, yet the synthesizing fails. However, the experimental results of Sect. 11 do not show any occurrence of such a precision loss. We note that the segment predicate in the abstract state is synthesized with the silhouetteguided segment introduction rule (Definition 9.2). At the same time, it keeps m 0 separate.

Here, the clumping result is precise for the analysis to infer interesting properties, as discussed in Chapter 7, and in addition, it is also optimal regarding the number of disjuncts. 7.2) with their respective silhouettes section, we assume that O M! is a widening over abstract states, using similar algorithms to t M! . Such an operator can often be based on t M! [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF].

Silhouette-guided Widening of Disjunctive Abstract states

Widening based on silhouette-guided pairing. Intuitively, a widening of d with d 0 should widen disjuncts of d with disjuncts of d 0 , using some sort of pairing to select which pairs of disjuncts are to be widened together. Since silhouettes aim at capturing abstract states that can be joined precisely, we build our widening around a pairing function that we build based on the silhouette.

This operator always returns a sound over-approximation of its arguments. Yet, depending on the pairing family, it may fail to guarantee termination. In the following, we define a pairing family that ensures termination so that widen D does indeed define a widening.

A good pairing should map abstract states that produce a precise widening, in the same way as clumping for join. It should also drive the introduction of summary predicates. As observed in Chapter 9, silhouettes hold information capable of guiding this process. However, for termination, we need to bound silhouettes. Thus, we define a pairing that is parameterized by an integer bound b, and that associates abstract states with silhouettes that are equivalent when regular expressions are smashed upon exceeding length b (in the following, let b = 1): Definition 10.6 (Silhouette-based pairing). Let F denote the set of all field names and let b be an integer bound.

We define the regular expression bounded abstraction by: [START_REF] Dudka | Predator: A practical tool for checking manipulation of dynamic data structures using separation logic[END_REF], the GNU Data Structure Library (GDSL), the BSD library, and a tutorial implementation of AVL trees (JSW) [START_REF] Walker | AVL balanced tree library[END_REF]. Some external libraries include typically simple, user-specified assertions (User Assert). A † indicates that the routine is recursive, while a ⇤ indicates that the loops are nested. The subsequent columns provide metrics for the complexity of the code, including the total number of functions (Fun), the number of loops (Loop), the number of acyclic paths (Path), and the maximum number of simultaneous pointers into a data structure instance (Simult. Pointer).