pure formulas, separating conjunction, and maybe, disjunctions,

[dzufferey]

Something funny seems to be going on with pure formulas and the separating conjunction. My understanding is that GRASShopper threats pure formula has having an empty footprint. Therefore, && and &*& should be the same for pure formula. However, I got example where they differ.

Below there are two tests which shows this effect. The difference in the input is the specification of send Here is the diff between the two:

48,49c48,49
<   requires (c.act.msg == SendCons(x) &*& flag == flagCons)
<         || (c.act.msg == SendNil &*& flag == flagNil)
---
>   requires (c.act.msg == SendCons(x) && flag == flagCons)
>         || (c.act.msg == SendNil && flag == flagNil)
[1]+  Done                    nautilus .

Test 1, verifies fines:

options "-abspreds"

include "tests/spl/adt/lists.spl"

struct Node {
  var next: Node;
  var data: Int;
}

predicate lseg(x: Node, y: Node, lst: List) {
  (x == y &*& lst == nil) ||
  (x != y &*& lst != nil &*& acc(x) &*& x.data == lst.hd &*& lseg(x.next, y, lst.tl))
}

predicate list(x: Node, lst: List) {
  lseg(x, null, lst)
}

datatype Message = SendCons(sx: Int)
                 | SendNil

const flagCons: Int
const flagNil: Int
axiom flagCons == 1
axiom flagNil == 0

struct Action {
  var nextAct: Action;
  var msg: Message;
}

struct Chan {
  var act: Action;
}

predicate protocol1(act: Action, lst: List) {
     (lst != nil &*& acc(act) &*& act.msg == SendCons(lst.hd) &*& protocol1(act.nextAct, lst.tl))
  || (lst == nil &*& acc(act) &*& act.msg == SendNil &*& act.nextAct == null)
}

predicate protocol(c: Chan, lst: List) {
  acc(c) &*& protocol1(c.act, lst)
}


procedure send(c: Chan, flag: Int, x: Int)
  requires acc(c) &*& acc(c.act)
  requires (c.act.msg == SendCons(x) && flag == flagCons)
        || (c.act.msg == SendNil && flag == flagNil)
  ensures acc(c) &*& c.act == old(c.act.nextAct)

procedure thread1(c1: Chan, n: Node, ghost lst: List)
  requires protocol(c1, lst)
  requires list(n, lst)
  ensures emp
{
  pure assume n != null; // not end of list
  send(c1, flagCons, n.data);
  var n1 := n.next;
  free(n);
  pure assume lst.tl == nil; // recursive call with end of list
  thread1(c1, n1, lst.tl);
}

Test 2, fails (Memory footprint for type Action, takes about 8min):

options "-abspreds"

include "tests/spl/adt/lists.spl"

struct Node {
  var next: Node;
  var data: Int;
}

predicate lseg(x: Node, y: Node, lst: List) {
  (x == y &*& lst == nil) ||
  (x != y &*& lst != nil &*& acc(x) &*& x.data == lst.hd &*& lseg(x.next, y, lst.tl))
}

predicate list(x: Node, lst: List) {
  lseg(x, null, lst)
}

datatype Message = SendCons(sx: Int)
                 | SendNil

const flagCons: Int
const flagNil: Int
axiom flagCons == 1
axiom flagNil == 0

struct Action {
  var nextAct: Action;
  var msg: Message;
}

struct Chan {
  var act: Action;
}

predicate protocol1(act: Action, lst: List) {
     (lst != nil &*& acc(act) &*& act.msg == SendCons(lst.hd) &*& protocol1(act.nextAct, lst.tl))
  || (lst == nil &*& acc(act) &*& act.msg == SendNil &*& act.nextAct == null)
}

predicate protocol(c: Chan, lst: List) {
  acc(c) &*& protocol1(c.act, lst)
}


procedure send(c: Chan, flag: Int, x: Int)
  requires acc(c) &*& acc(c.act)
  requires (c.act.msg == SendCons(x) &*& flag == flagCons)
        || (c.act.msg == SendNil &*& flag == flagNil)
  ensures acc(c) &*& c.act == old(c.act.nextAct)

procedure thread1(c1: Chan, n: Node, ghost lst: List)
  requires protocol(c1, lst)
  requires list(n, lst)
  ensures emp
{
  pure assume n != null; // not end of list
  send(c1, flagCons, n.data);
  var n1 := n.next;
  free(n);
  pure assume lst.tl == nil; // recursive call with end of list
  thread1(c1, n1, lst.tl);
}

[wies]

This looks like an incompleteness issue further down in the backend solver. The GRASS translation is correct for both versions, but yields slightly different but equivalent results. For the version that uses the pure requires clause, we get a precondition of send in the translation of the form:

FP_Chan == {c}

and similarly for FP_Action. The other version results in the equivalent precondition

{c} subsetof FP_Chan && 
FP_Chan -- {c} == {}

It seems that the explicit equality helps solve the first version whereas it gets stuck in the second version. I am still investigating what exactly is causing the incompleteness.