Difference between revisions of "Separation Logic"
| Line 12: | Line 12: | ||
=Semantics= | =Semantics= | ||
| − | A satisfiability relation <math>I,h \models_{SL} \varphi</math> is defined for <math>SL(T)_{Loc,Data}</math> formulas, | + | A satisfiability relation <math>I,h \models_{SL} \varphi</math> is defined for <math>SL(T)_{Loc,Data}</math> formulas <math>\varphi</math>, |
where I is an interpretation, and h is a heap. The semantics of separation logic operators are as follows: | where I is an interpretation, and h is a heap. The semantics of separation logic operators are as follows: | ||
| Line 40: | Line 40: | ||
where <math>h_1 \uplus \ldots \uplus h_n</math> denotes the disjoint union of heaps <math>h_1, \ldots, h_n</math> and | where <math>h_1 \uplus \ldots \uplus h_n</math> denotes the disjoint union of heaps <math>h_1, \ldots, h_n</math> and | ||
<math>h'\#h</math> denotes that heaps h' and h are disjoint, and <math>nil</math> is a distinguished variable of sort Loc. | <math>h'\#h</math> denotes that heaps h' and h are disjoint, and <math>nil</math> is a distinguished variable of sort Loc. | ||
| − | + | All classical Boolean connectives are interpreted as expected. | |
| + | Note that the arguments of "emp" are used to denote the type of the heap and have no meaning otherwise. | ||
=Syntax= | =Syntax= | ||
Revision as of 13:11, 28 November 2016
CVC4 supports a syntax for separation logic as an extension of the *.smt2 language.
Contents
Signature
Given a (decidable) base theory T, CVC4 supports a decision procedure for 
formulas, where "Loc" and "Data" are any sort belonging to T.
A formula is one from the following grammar:
F : L | (emp t u) | (pto t u) | (sep F1 ... Fn) | (wand F1 F2) | ~F1 | F1 op ... op Fn
where "op" is any classical Boolean connective, t and u are terms built from symbols in the signature of T of sort Loc and Data respectively, and L is a T-literal. The operator "emp" denotes the empty heap constraint, the operator "pto" denotes the points-to predicate, the operator "sep" denotes separation start and is variadic, and the operator "wand" denote magic wand.
Semantics
A satisfiability relation 
is defined for formulas 
,
where I is an interpretation, and h is a heap. The semantics of separation logic operators are as follows:
 L
|
Iff |  L, if L is a T-literal
|
(emp  )
|
Iff | 
|
| (pto )
|
Iff | 
|
(sep  )
|
Iff | there exist heaps  s.t.  and 
|
(wand  )
|
Iff | for all heaps  if  and  then 
|
where 
denotes the disjoint union of heaps and
denotes that heaps h' and h are disjoint, and 
is a distinguished variable of sort Loc.
All classical Boolean connectives are interpreted as expected.
Note that the arguments of "emp" are used to denote the type of the heap and have no meaning otherwise.
Syntax
Separation logic in CVC4 requires the "all supported" logic:
(set-logic QF_ALL_SUPPORTED)
The syntax for the operators of separation logic is summarized in the following table:
| CVC language | SMTLIB language | C++ API | |
|---|---|---|---|
| Empty heap | N/A
|
(emp X Y)
|
em.mkExpr(kind::SEP_EMP, X, Y);
|
| Points-to | N/A
|
(pto X Y)
|
em.mkExpr(kind::SEP_PTO, X, Y);
|
| Separation star | N/A
|
(sep C1 ... Cn)
|
em.mkExpr(kind::SEP_STAR, C1, ..., Cn);
|
| Magic wand | N/A
|
(wand C1 C2)
|
em.mkExpr(kind::SEP_WAND, C1, C2);
|
| Nil element | N/A
|
(as nil T)
|
em.mkUniqueVar(T,kind::SEP_NIL);
|
Examples
The following input on heaps Int -> Int is unsatisfiable:
(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-const x Int) (declare-const a Int) (declare-const b Int) (assert (and (pto x a) (pto x b))) (assert (not (= a b))) (check-sat)
The following input on heaps U -> Int is satisfiable. Notice that the formula (not (emp x 0)) is satisfied by heaps U -> Int (the types of x and 0 respectively) whose domain is non-empty.
(set-logic QF_ALL_SUPPORTED) (set-info :status unsat) (declare-sort U 0) (declare-const x U) (declare-const a Int) (assert (and (not (emp x 0)) (pto x a)) (check-sat)
The following input on heaps Int -> Node is satisfiable, where Node denotes a user-defined inductive datatype:
(set-logic QF_ALL_SUPPORTED) (set-info :status sat) (declare-const x Int) (declare-const y Int) (declare-const z Int) (declare-datatypes () ((Node (node (data Int) (left Int) (right Int))))) (assert (pto x (node 0 y z))) (check-sat)
Given a separation logic input, the sorts Loc and Data are inferred by CVC4, and must be consistent across all predicates occurring in an input. CVC4 does not accept an input such as:
(set-logic QF_ALL_SUPPORTED) (declare-sort U 0) (declare-const x U) (assert (and (pto x 0) (pto 1 2)))
since the sorts of the first arguments of the points-to predicates do not agree.
