Abstract Domains for Lists and Heap Structures: A Comprehensive Overview

Explore the concepts of quantified data automata on skinny trees, automatic shapes in static analysis, universally quantified properties on lists, heap configurations with skinny trees, and the extension of quantified data automata over lists. Dive into the abstract domain of automata to capture infinite sets of objects and represent properties of data stored in heaps.

• Abstract Domains
• Lists
• Heap Structures
• Data Automata
• Static Analysis

winkfield_g Follow

Uploaded on Sep 10, 2024 | 1 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists Pranav Garg1, P. Madhusudan1and Gennaro Parlato2 1University of Illinois at Urbana-Champaign 2University of Southampton, UK

2. Automatic Shapes Static analysis of heap structures - heaps with a single pointer field Properties: Universally Quantified properties over heap + data IntroduceAutomatic Shapes - abstract domain of automata Automata are classical ways to capture infinite sets of objects using finite means. Aim: - Represent properties of the data stored in the heap. - Build automata that can express universally quantified properties 2

3. Universally Quantified Properties on Lists head 5 List pointed to by head is sorted ( 2 y data y next 7 8 9 * next * .( ) ( )) y y head y data y 1 2 1 1 2 head more less 9 4 4 2 2 9 1 1 fold-split(key) splits input list into two lists. .(( 1 1 data y less y next * * next ( ) ) ( ( ) )) y key more y data y key 1 1 1 Abstract analysis of heap is hard - unbounded size of the heap - unbounded data stored in the heap 3

4. Heap Configurations and Skinny Trees Restrict to heaps with a single pointer field (acyclic). Let P: the program s pointer variables - Heap configuration skinny trees labeled by P head1 nil 5 2 $ 1 7 9 head2 3 6 4 head3 1 8 4 k- skinny tree has at most k- branching points. Heap configurations are k- skinny trees (k = number of pointer vars.) 4

5. Quantified Data Automata Extends Quantified Data Automata over lists [CAV 13] QDAs logically define universally quantified properties of lists /\ .( ( , ) ( , )) y Guard p y Data p y Example: i i i * next * next .( ( ) ( )) y y head y y data y data y 1 2 1 2 1 2 5

6. Quantified Data Automata Fix P program pointer variables Fix Y set of quantified variables Fix F data domain which forms a lattice QDA over skinny trees: - reads a tree annotated with pointers P and Y - checks whether data stored at these positions satisfy a data property QDA accepts a tree T with pointers P if it accepts all possible extensions of T with valuations for Y. * next * next .( ( ) ( )) y y head y y data y data y 1 2 1 2 1 2 y2 y1 head data(y1) <= data(y2) 6

7. Valuation Trees Valuation tree = Skinny tree over P + valuation for Y head1 2 head2 6 3 4 y1 head1 head1 y1 y2 nil nil nil Skinny Tree 5 5 5 2 2 $ $ $ 1 1 1 7 7 7 9 9 9 head2 head2 3 3 6 6 4 4 y2 Valuation Trees Universal Quantification QDA accepts a skinny tree iff it accepts ALL corresponding valuation trees. 7

8. Quantified Data Automata Bottom-up, deterministic, register automata over trees - each state labeled with a data formula f For a valuation tree, QDA reads ptr. and univ. vars. and stores the data values in the register reg. head1 head1 y2 y2 nil nil reg: head1 5 head2 3 y1 4 y2 7 nil $ 5 5 2 2 $ $ f(q) = 1 1 7 7 9 9 head2 head2 3 3 6 6 4 4 y1 y1 data(y1) < data(y2) At the final state, QDA checks if these data values satisfy the formula labeling the state. - reg satisfies f(q) Accepts the valuation tree - reg does not satisfy f(q) Rejects the valuation tree 8

9. Formula Tree Formula Tree = (Valuation Tree \ data) paired with a data formula y1 head1 nil head2 , data(y1) < data(y2) y2 - complete separation of the structure of the heap and its data Define Lf (A) = Language of formula trees accepted by A 10

10. QDAs as a Partial Order Natural Partial Order -- set inclusion over the language of QDAs - not closed under disjunctions ) ( . . y y y Alternate partial order: if such that and 2 1 A A ( t ( f ( , ) ) ( ) t df L A A t 1 L 1 f df df , ) df 1 2 2 2 df - Least upper bound associates every tree to - Infinite sets of QDAs might not have a least upper bound. Hence do not form a complete lattice. df 1 2 11

11. Elastic QDAs Require a notion of widening for analysis of loops - Ignore lengths of stretches of the heap not pointed by variables. head y1 nil nil y1 head y1 head QDA: y1 head Elastic QDA: q = = q ( , ) q b q -Restriction: All transitions on blank symbols must be self-loops 1 2 1 1 2 12

12. Theorems about EQDAs 1. Number of states in a minimal EQDA is bounded - Finite number of EQDAs modulo the data formulas - widening proc. for EQDAs given widening for data formulas. 2. For every QDA, there is a most-precise over-approximating EQDA (in terms of their accepting languages) elastification EQDAs form a complete lattice abstract domain 3. EQDAs correspond to decidable STRAND logic [POPL 11] over lists. - Abstract interpretation using EQDAs can be used for checking STRAND assertions. 13

13. Abstract transformer over EQDAs Strongest post condition involves existential quantification of the pre-state + constraining post-state acc. to the semantics of the stmt. Example: strongest-post( ) = i y p A y : , . /\ Guard => Data p = '. j = . [ / ] ' p y A p p p p i f i i i j These precise post-conditions are not expressible by QDAs. Over-approximate the post-condition to: - eliminate existential quantifier via quantifier elimination for the structure (Guard) using automata, and data-formulas (Data) separately. * * . = '. [ / ] ' y p A p p p p i f i i i j 14

14. Abstract transformer over EQDAs Pointer Assignment statement pi := pj . [ ( / ) i p ] p d data d = ( ) ( ) data p data i j pi := pj pj pj , pi b pi pi pi := pj ' A A Similar abstract transformer for structure manipulating statements: Pointer Lookup pi:= pj .next Pointer Mutate pi .next := pj Allocate new pi 15

15. Abstract transformer over EQDAs Data Assignment statement pi .data := data_exp ( .( ) [ data ( _ / ) i exp[ ] d i= data p d data ( / ) i ]) data p p d pi .data := data_exp pi pi Slightly more involved: - Also account for all variables which point to the same node as pi 16

16. Abstract transformer over EQDAs elastification stmt ' ' A ' A A EQDA QDA EQDA A might not be elastic. Use the most-precise over-approximation result to get an EQDA. - defines the actual abstract transformer over EQDAs Fix-point computation of the abstract semantics terminates - widening for the data domain 17

17. Experiments Simple programming language consisting of heap allocation, pointer assignment, pointer lookup, pointer mutate, Given a STRAND formula as pre-condition, construct the corresponding EQDA. Compute the abstract semantics of the program over EQDAs using the abstract transformer. Fix-point EQDAs are translated to decidable STRAND formulas over lists to verify program assertions, post-conditions. - Instantiate data-formulas with the octagonal domain (using Apron). - Prototype implementation available at http://web.engr.illinois.edu/~garg11/qsdas.html 18

18. Experiments Programs #PV #Y #DV Property #Iter. Max. size of QSDA Time (s) INIT 2 1 1 Init, List 4 19 0.0 MAX 2 1 1 Max, List 4 19 0.1 CLONE 4 1 1 Init, List 4 44 0.7 FOLD-CLONE 5 1 1 Init, List 5 57 3.2 COPY-GE5 4 1 0 Gek, List 9 53 2.6 FOLD-SPLIT 3 1 1 Gek, List 4 33 0.3 CONCAT 4 1 1 Init, List 5 44 0.7 SORTED-FIND 2 2 2 Sort, List 5 38 0.3 SORTED-INSERT 4 2 1 Sort, List 6 163 5.8 BUBBLE-SORT 4 2 1 Sort, List 5/18 191 42.8 SORTED-REVERSE 3 2 0 Sort, List 5 43 1.5 EXPRESSOS-LOOKUP-PREV 3 2 1 Sort, List 6 73 2.2 GSLIST-CUSTOM-FIND 3 1 1 Gek, List 4 29 0.1 GSLIST-REMOVE-ALL 5 1 1 Gek, List 5 51 0.6 GSLIST-INSERT-SORTED 5 2 1 Sort, List 6 279 27.4 19

19. Related Work (Shape Analysis) Merges nodes that satisfy the same predicates - unary + instrumentation predicates Instrumentation predicates provided by the user - often complex, - very particular to the program being verified Example: sub-list before pointer i is sorted, that is .(( , y x y x next * * next ) ( ) ( )) y i data x data y - instrumentation predicate required .(( ) ( x y x s = * next * next ) ( ) ( )) y y i data x data y Clearly, - s(x) too dependent on the property being verified - complex (writing binary property as a unary predicate) 20

20. Conclusion Automatic Shapes an abstract domain of automata - can express universally quantified properties of lists - can prove these properties precisely and efficiently Future Work Extensions to trees to capture universally quantified properties like binary-search-tree, max-heap, Extensions to general graphs using graph automatons. Thank You ! 21