Satisfiability Modulo Abstraction for Separation Logic with Linked Lists

This study explores the application of satisfiability modulo abstraction in separation logic with linked lists. It presents a technique using abstract interpretation concepts to handle separation logic formulas beyond previous methods, specifically focusing on over-approximating heaps that satisfy the logic. The approach employs tools like ITVLA and abstract domains of shape graphs, demonstrating effectiveness in handling complex formulas.

• Abstraction
• Separation Logic
• Linked Lists
• Satisfiability
• Abstract Interpretation

laer813 Follow

Uploaded on Sep 10, 2024 | 0 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. Satisfiability Modulo Abstraction for Separation Logic with Linked Lists Aditya Thakur, Jason Breck, and Thomas Reps UNIVERSITY OF WISCONSIN-MADISON

2. Satisfiability Modulo Abstraction for Separation Logic with Linked Lists

3. Satisfiability Modulo Abstraction for Separation Logic with Linked Lists (program P, property Q) ? Satisfiability Solver If ? is unsatisfiable then P has property Q

4. Satisfiability Modulo Abstraction for Separation Logic with Linked Lists (program P, property Q) using linked lists ? ? Satisfiability Solver If ? is unsatisfiable then P has property Q

5. Satisfiability Modulo Abstraction for Separation Logic with Linked Lists (program P, property Q) using linked lists ? ? ?? Satisfiability Solver ? If ? is unsatisfiable then P has property Q

6. Satisfiability Modulo Abstraction for Separation Logic with Linked Lists (program P, property Q) using linked lists ? ?? Satisfiability Solver using concepts from abstract interpretation If ? is unsatisfiable then P has property Q

7. Contributions We check the unsatisfiability of separation logic formulas using concepts and tools (ITVLA) from abstract interpretation We use an abstract domain of sets of shape graphs to over-approximate the set of heaps that satisfy a separation logic formula Our technique can handle some formulas that cannot be handled by previous techniques

8. Separation Logic Store Heap x y z

9. Separation Logic atom ::= ? ? | ??(?,?) | ??? |???? | ? = ? Store Heap x y z ? ::= atom | atom |? ? |? ? |? ? |? ?

10. Separation Logic atom ::= ? ? | ??(?,?) | ??? |???? | ? = ? Store Heap x y z ? ::= atom | atom |? ? |? ? |? ? |? ?

11. Separation Logic atom ::= ? ? | ??(?,?) | ??? |???? | ? = ? Store Heap x y z ? ::= atom | atom |? ? |? ? |? ? |? ?

12. Separation Logic atom ::= ? ? | ??(?,?) | ??? |???? | ? = ? Store Heap x y z ? ::= atom | atom |? ? |? ? |? ? |? ?

13. Separation Logic atom ::= ? ? | ??(?,?) | ??? |???? | ? = ? Store Heap x y z ? ::= atom | atom |? ? |? ? |? ? |? ?

14. Separation Logic atom ::= ? ? | ??(?,?) | ??? |???? | ? = ? Store Heap x y z ? ::= atom | atom |? ? |? ? |? ? |? ?

15. Separation Logic heap ?1 ?2iff there exists a partition 1and 2 of such that 1 ?1and h2 ?2 h ?1 ?2 2 ?2 ?1 1 Example: ??(?,?) ??(?,?) ? ? ? ?

16. Strategy: Bottom-Up Evaluation ?? ?,? ? ? (? ? ? ?) ??(?,?) (? ?) ? ? ? ? Abstract domain element that over-approximates the set of heaps that satisfy ??(?,?) If this is the bottom element, the formula is unsatisfiable

17. Strategy: Bottom-Up Evaluation ?? ?,? ? ? (? ? ? ?) ??(?,?) (? ?) ? ? ? ?

18. Shape Graphs y x r[x] r[x] r[x] h ??(?,?) Abstract y Concrete x y x r[x] r[x] r[x] r[x] r[x] r[x] r[x] r[x] y x r[x] r[x] r[x] r[x]

19. Shape Graphs x y ??(?,?) r[x] y x r[x] r[x] y x r[x] r[x] r[x]

20. Shape Graphs x y ??(?,?) h r[x] y x h h r[x] r[x] y x h r[x] h h r[x] r[x]

21. Strategy: Bottom-Up Evaluation ?? ?,? ? ? (? ? ? ?) ??(?,?) (? ?) ? ? ? ? x y h x y h y x h

22. Shape Graphs ? ? x y h h r[x] r[x]

23. Strategy: Bottom-Up Evaluation ?? ?,? ? ? (? ? ? ?) ??(?,?) (? ?) ? ? ? ? x y x y h h x y h y x h

24. Strategy: Bottom-Up Evaluation ?? ?,? ? ? (? ? ? ?) ??(?,?) (? ?) ? ? ? ? x y x x y y h h h x y h y x h

25. Shape Graphs (? ?) x is not in the sub-heap the sub-heap is empty h x y y x h h r[x] h h r[x] successor to x is not y sub-heap has >1 node

26. Strategy: Bottom-Up Evaluation ?? ?,? ? ? (? ? ? ?) ??(?,?) (? ?) ? ? ? ? x y x x y y h h h x y x y y x h h y x h

27. Meet: Inputs ??(?,?) (? ?) x y h r[x] h x y y x y x h h r[x] h h r[x] h h r[x] r[x] y x h r[x] h h r[x] r[x]

28. Meet: Outputs ??(?,?) (? ?) x y h r[x] h x y y x y x h h r[x] h h r[x] h h r[x] r[x] y x h r[x] h h r[x] r[x]

29. Strategy: Bottom-Up Evaluation ?? ?,? ? ? (? ? ? ?) ??(?,?) (? ?) ? ? ? ? x x y y x y h h y x

30. Separating Conjunction x x y y h h h r[x] h r[x] r[x] r[x]

31. Separating Conjunction x x y y h1 r[x] h h1 r[x] h r[x] r[x]

32. Separating Conjunction x x y y h1 r[x] h2 r[x] h1 r[x] h2 r[x]

33. Separating Conjunction h is the disjoint union of h1 and h2 h1 h2 h h1 h2 h h1 h2 h h1 h2 h

34. Separating Conjunction x x y y h1 r[x] h2 r[x] h1 r[x] h2 r[x] h1 h2 h h1 h2 h h1 h2 h h1 h2 h

35. Separating Conjunction x x y y h1 r[x] h2 r[x] h1 r[x] h2 r[x] h1 h2 h h1 h2 h h1 h2 h h1 h2 h Result: the empty set of shape graphs

36. Strategy: Bottom-Up Evaluation ?? ?,? ? ? (? ? ? ?) ??(?,?) (? ?) ? ? ? ? x y y x

37. Strategy: Bottom-Up Evaluation ?? ?,? ? ? (? ? ? ?) ??(?,?) (? ?) ? ? ? ? x y y x Final result: the formula is unsatisfiable

38. Experiments Designed to investigate: Speed Precision Formulas not handled by other tools Setup Three groups of unsatisfiable formulas Group 1 23 formulas Included some not handled by other tools Groups 2, 3 64 and 512 formulas Built from templates taken from the literature

39. Experiments: Group 1 9 8 Running Time (s) (a1 a2 ls(e1,e2)) (a2 a3 emp) (a3 a1 (a5 a6) true) 7 6 5 4 3 2 1 0 Formula

40. Experiments: Groups 2 and 3 Formula templates based on Hou et al., POPL14: a emp (a b) 64 formulas Mean: 0.56 sec, Max: 10.31 sec emp a (b (c (emp a))) 512 Formulas Mean: 0.12 sec, Max: 9.51 sec

41. Summary We implemented a tool called SMASLTOV (based on ITVLA) https://www.github.com/smasltov-team/SMASLTOV SMASLTOV checks the unsatisfiability of separation logic formulas using concepts from abstract interpretation SMASLTOV uses an abstract domain of sets of shape graphs to over-approximate the set of heaps that satisfy a separation logic formula SMASLTOV can handle some formulas that cannot be handled by previous techniques Thank you! Any questions?