new extension: Z3 for Separation Logic

[lequangloc]

Dear all, I plan to build a new extension in Z3 to solving satisfiability for separation logic. I would really appreciate for any advice/suggestion on the following issues.

1. SMT-LIB standard for Separation Logic. I have found a proposal at http://www-verimag.imag.fr/~serban/talks/2015.02.27-form-sl-smtlib.pdf, but I am not sure it is acceptable
2. similar projects: it is great if there are some (open source) project targeting on separation logic in Z3. I have found a recent work which is implementing the SAT extension for separation logic in CVC4.

Thank you.

[wintersteiger]

That sounds like a great plan. Various people have been interested in this topic to varying degrees and I'd recommend talk to them first to see what sort of difficulties are to be expected. Especially if integration with other theories is required this may be much harder than one would first expect. However, I think separate tactics for particular fragments would still be a great start and a valuable contribution.

Specifically, I recommend to talk to the authors of these papers:

• Botincan, Parkinson, Schulte: Separation Logic Verification of C Programs with an SMT Solver
• Piskac Wies Zufferey: Automating Separation Logic Using SMT
• Reynolds, Iosif, Serban, King: A Decision Procedure for Separation Logic in SMT
• @jberdine and @sishtiaq may be interested too.

There has been an effort to compile a proper SMT theory for SL, but I have no idea what the status of that is. It definitely hasn't been accepted yet, but apart from that I don't know much about it.

[lequangloc]

Thanks for your comments and pointing.

The third work is the most relevant. I have sent an email to Reynolds who has recently implemented a SAT solver for SL (without general inductive predicates) in CVC4.

The first work (Botincan, Parkinson, Schulte) uses a SMT solver in entailment checking. It proposes an entailment procedure based on Smallfoot. It invokes a SMT solver (e.g., Z3) when it stucks at the frame inference rule: \pure_1 | FRAME |- \pure_2 | EMPTY. This work did not implement a SAT solver for SL in SMT.

The second work (GRASShoper - Piskac Wies Zufferey) reduces a separation logic formula into a first-order logic formula and invokes a SMT solver to discharge the first-order formula. In the correspondence with SL-COMP 2014, I remember Wies noticed that GRASShoper system does not have a stand-alone decision procedure.

[NikolajBjorner]

Extensions and contributions in the form of capabilities are certainly very welcome. To engineer a good theory extension can be substantial and time consuming effort, but with a suitable use base it can have benefits.

An external method that reasons about SL using a model-based approach is:

• https://www.microsoft.com/en-us/research/publication/separation-logic-modulo-theories/

I would also consult the work on heap logics by Joxan Jaffar et. al.

The SMT2 proposal includes adding a "ref" type constructor (with ML semantics). Syntactically there are some obstacles to adding this to Z3 data-types as Z3 requires recursive data-types to appear in non-nested occurrences in the data-type definition. A workaround is to create two mutually recursive data-types, where one is a "ref" cell, and then you would have to re-interpret ref in a special way.

[ajreynol]

Hello all,

I've sketched some notes on the format for separation logic accepted by CVC4:

http://church.cims.nyu.edu/wiki/Separation_Logic

The format was developed in discussion with Radu Iosif and Cristina Serban at Verimag. We are interested in discussing possible formats for SL with a larger SMT audience.

The format we currently support in CVC4 differs from the previous proposal is that the "Ref" type constructor is not builtin. Instead, e.g. the predicate "pto" is fully parametric, e.g. given a fixed background theory T, we fix two sorts "Loc" and "Data" of that theory. Then, pto is a predicate of sort Loc x Data. We believe that allowing the separation logic extension to be fully parametric in this way comes with fewer complications and still allows for one to specify problems e.g. where Loc=(Ref T) for some user-defined type constructor Ref.

However, the challenge is how to specify what "Loc" and "Data" are. There are two possible ways we have considered doing this so far:

(1) Require the solver to infer "Loc" and "Data".

As a simple example: (set-logic QF_ALL_SUPPORTED) (declare-const x Int) (assert (pto x 0)) (check-sat) Upon parsing (pto x 0), the solver infers that Loc=Int, Data=Int.

CVC4 will throw an error if given pto's of different type: (set-logic QF_ALL_SUPPORTED) (declare-sort U 0) (declare-const x U) (assert (and (pto x 0) (pto 1 2))) (check-sat)

Requiring the solver to do this inference means that the empty heap constraint "emp" needs to be made unambiguous. To do this, we define emp as a predicate taking two dummy arguments whose types are Loc and Data. As an example: (set-logic QF_ALL_SUPPORTED) (declare-sort U 0) (declare-const x U) (assert (emp x 0)) (check-sat) Here, (emp x 0) is the empty heap constraint for Loc=U, Data=Int.

(2) Require the user to define "Loc" and "Data".

This could be done e.g. by adding a new smt2 command "define-sl-sorts": (set-logic QF_ALL_SUPPORTED) (declare-sort U 0) (define-sl-sorts U Int) (declare-const x U) (assert (pto x 0)) (check-sat) which sets Loc=U, Data=Int.

The advantage of (2) is that "emp" can be nullary since Loc and Data are established up front, and less burden is put on the solver. However, a disadvantage to (2) is that the operational semantics of the SMT2 command language becomes more complicated: Before issuing "assert", the user must issue "define-sl-sorts". However, the user may need to issue "declare-sort"/"declare-datatypes" before issuing "define-sl-sorts". This is complicates the picture in Figure 4.1 on page 49 of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf.

At the moment, we have chosen to do (1), although neither is ideal, so we're definitely interested in further discussion of a standard format for SL in SMT.

[kfriedberger]

Are there any updates on SL-theory within Z3?

[NikolajBjorner]

As Andrew pointed out, there is a theory in CVC4. I recently learned that Josh Berdine found a canonizing SMT solver to be very useful for SL so perhaps use his if it is available.

[lequangloc]

It is a shame that I have made little progress on the implementation.

One of my issue was that the SMT format for SL was not standard. Beside the format Andrew mentioned above, SL-COMP (the competition for SL solvers) made use of another format (https://sl-comp.github.io/docs/smtlib-sl.pdf).

At the end, I implemented a mini solver (to test some of my ideas) that could support the SMT format in SL-COMP.

[NikolajBjorner]

closing as no activity