Dynamic write by helper functions - roboguy13/suslik GitHub Wiki

Motivation

In the post-assertion of Suslik specs, when a point-to clause x:->v exists, a write rule (correspond to *x = v;) is applied if possible during the pure phase. The point-to's are generated by inductive predicates for the most cases. However, when we want to have more complex modifies on x, it is restricted by the syntax.

For example, we can have a map for single linked lists with \x -> x + 2, but not for \x -> x : [2].

Solution: dynamic write

The idea is that, no matter what the list is mapped with, we abstract the function with the following format. func f(...,x) where the parameters can be any values or locations. TODO: a sugar x = f(..) ? Then instead of writing ... && v == v1 + v2; x :-> v ** y :-> v2 ... (desugared by pred) in the inductive predicates, using the more general func f(v1, y, x).

The function's spec is transformed from the Haskell-like language.

{ true ; y :-> v2 ** x :-> any }
void f (int v1, loc y, loc x)
{ v == v1 + v2 ; y :-> v2 ** x :-> v }

The new synthesis rule

{ψ ; P} --> {Φ ; Q}| c
—————————————————————————————————————————————————————————————————
{ψ ; x :-> e * P} --> {Φ ; func f(...,x) * Q}| f(...,x); c

{ψ ; x :-> e2 * P} --> {Φ ; Q}| c
—————————————————————————————————————————————————————————————————
{ψ ; x :-> e1 * P} --> {Φ ; x :~> e2 * Q}| *x = e2; c

Restriction of the helper functions

• Pure function: the helper functions should not modify other location. TODO: detection when parsing