Incorrect translation (function, quantifiers, heap-dep. triggers) causes Z3 errors

[mschwerhoff]

The program further down (distilled from ring-insert.vpr) results in Z3 warnings and errors, caused by the SMT translation of the quantifiers in lines 13 and 14: the translated triggers contain if-else expressions (causing warnings) and the translated quantifier bodies contain undeclared variables (causing errors).

field f: Int

domain Foo {
  function pure(ps: Set[Ref], p: Ref): Bool
}

function heapdep(zs: Set[Ref]): Set[Ref]
  requires forall z: Ref :: z in zs ==> acc(z.f)

function main(xs: Set[Ref], ys: Set[Ref]): Bool
  requires forall x: Ref :: x in xs ==> acc(x.f)
  requires forall x: Ref :: x in ys ==> acc(x.f)
  ensures forall u: Ref :: {pure(heapdep(xs), u)} u in xs ==>  pure(heapdep(xs), u)
  ensures forall v: Ref :: {pure(heapdep(xs), v)} v in ys ==>  !pure(heapdep(xs), v)

The problem is that Silicon's function recorder, which tracks which heap-dependent expressions use which heap snapshots, fails to differentiate between the four different uses of heapdep(xs). Taking AST positions into account would help here, but positional information isn't guaranteed to exist.

The new, semantic snapshot encoding that @maurobringolf is currently working on should resolve the issue.

[maurobringolf]

I just ran the example given above through a version of my fork and successfully verified it. The quantifiers in the postcondition of main are translated as follows (identifiers manually prettified):

    (forall ((u $Ref)) (!
      (implies
        (Set_in u xs)
        (pure<Bool> (heapdep (PHeap.restrict_heapdep h xs) xs) u))
      :pattern ((pure<Bool> (heapdep (PHeap.restrict_heapdep h xs) xs) u))
      ))
    (forall ((v $Ref)) (!
      (implies
        (Set_in v ys)
        (not
          (pure<Bool> (heapdep (PHeap.restrict_heapdep h xs) xs) v)))
      :pattern ((pure<Bool> (heapdep (PHeap.restrict_heapdep h xs) xs) v))
      ))))

which is where the error occurs with the current version.