Satisfiability Modulo Abstraction for Separation Logic with Linked Lists

undefined
 
UNIVERSITY OF WISCONSIN-MADISON
 
Satisfiability Modulo
Abstraction for Separation
Logic with Linked Lists
Aditya Thakur, 
Jason Breck
, and Thomas Reps
undefined
 
Satisfiability Modulo
Abstraction for Separation
Logic with Linked Lists
undefined
Satisfiability 
Modulo
Abstraction for Separation
Logic with Linked Lists
 
(program P, property Q)
Satisfiability Solver
undefined
Satisfiability Modulo
Abstraction for Separation
Logic with 
Linked Lists
(program P, property Q)
Satisfiability Solver
using linked lists
?
undefined
Satisfiability Modulo
Abstraction for 
Separation
Logic 
with Linked Lists
(program P, property Q)
Satisfiability Solver
using linked lists
?
undefined
Satisfiability Modulo
Abstraction 
for Separation
Logic with Linked Lists
(program P, property Q)
Satisfiability Solver
using linked lists
using concepts from
abstract interpretation
undefined
 
  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
Contributions
undefined
 
Separation Logic
 
Heap
 
Store
x
y
z
undefined
 
Separation Logic
 
Heap
 
Store
x
y
z
 
undefined
 
Separation Logic
 
Heap
 
Store
x
y
z
 
undefined
 
Separation Logic
 
Heap
 
Store
x
y
z
 
undefined
 
Separation Logic
 
Heap
 
Store
x
y
z
 
undefined
 
Separation Logic
 
Heap
 
Store
x
y
z
 
undefined
Separation Logic
Heap
Store
x
y
z
 
undefined
Separation Logic
h
undefined
Strategy: Bottom-Up Evaluation
If this is the bottom element,
the formula is unsatisfiable
undefined
 
Strategy: Bottom-Up Evaluation
undefined
Shape Graphs
 
Concrete
 
Abstract
undefined
Shape Graphs
 
x
 
y
r[x]
 
r[x]
 
r[x]
r[x]
r[x]
 
r[x]
undefined
 
Shape Graphs
 
x
 
y
 
h
r[x]
 
h
r[x]
 
h
r[x]
undefined
Strategy: Bottom-Up Evaluation
undefined
 
Shape Graphs
 
h
r[x]
undefined
Strategy: Bottom-Up Evaluation
undefined
Strategy: Bottom-Up Evaluation
undefined
Shape Graphs
 
x
 
h
r[x]
 
h
 
h
 
h
 
y
 
the sub-heap is empty
 
x is not in the sub-heap
 
successor to x is not y
 
sub-heap has >1 node
undefined
Strategy: Bottom-Up Evaluation
undefined
 
Meet: Inputs
 
x
 
h
r[x]
 
h
 
h
 
h
 
y
 
x
 
y
 
h
r[x]
 
h
r[x]
 
h
r[x]
undefined
Meet: Outputs
 
x
 
h
r[x]
 
h
 
h
 
h
 
y
 
h
r[x]
undefined
Strategy: Bottom-Up Evaluation
undefined
 
Separating Conjunction
undefined
 
Separating Conjunction
undefined
 
Separating Conjunction
undefined
Separating Conjunction
h is the disjoint union of h1 and h2
 
h1
¬ 
h2
h
 
¬ 
h1
h2
h
undefined
 
Separating Conjunction
 
h1
¬ 
h2
h
 
¬ 
h1
h2
h
undefined
Separating Conjunction
 
Result: the empty set of shape graphs
h1
¬ 
h2
h
¬ 
h1
h2
h
undefined
Strategy: Bottom-Up Evaluation
undefined
Strategy: Bottom-Up Evaluation
 
Final result: the formula is unsatisfiable
undefined
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
undefined
Experiments: Group 1
(a1 
 a2 
 ls(e1,e2)) 
(a2 
 a3 
 
¬ 
emp) 
(a3 
 a1 
 
¬
 (a5 
 a6) 
 true)
undefined
Experiments: Groups 2
 and 3
 
undefined
 
  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
Summary
Thank you!
Any questions?
Slide Note
Embed
Share

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.


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.

E N D

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?

More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#