Generated code is not self-framing

[marcoeilers]

Originally reported by: Vytautas Astrauskas (Bitbucket: vakaras, GitHub: vakaras)

---

When translating parallelTreeProcessing example from the Chalice2Silver test suite:

#!python
from py2viper_contracts.contracts import (
    Acc,
    Assert,
    Requires,
    Invariant,
    Implies,
    Predicate,
    Fold,
    Ensures,
    Unfold,
    Unfolding,
)
from py2viper_contracts.obligations import *


class Tree:

    @Predicate
    def valid(self) -> bool:
        return (Acc(self.left) and Acc(self.right) and
                Acc(self.height, 1/10) and self.height >= 0 and
                Implies(
                    self.left is not None,
                    self.left.valid() and Acc(self.left.height, 1/10) and
                    self.left.height == self.height - 1) and
                Implies(
                    self.right is not None,
                    self.right.valid() and Acc(self.right.height, 1/10) and
                    self.right.height == self.height - 1)
                )

    def __init__(self, left: 'Tree', right: 'Tree', height: int) -> None:
        Requires(left.valid() and Acc(left.height, 1/10) and
                 left.height == height-1)
        Requires(right.valid() and Acc(right.height, 1/10) and
                 right.height == height-1)
        Requires(height >= 0)
        Ensures(self.valid())
        self.left = left        # type: Tree
        self.right = right      # type: Tree
        self.height = height    # type: int
        Fold(self.valid())


    def work(self, call_height: int) -> None:
        Requires(self.valid())
        Requires(call_height >= 0)
        Requires(Unfolding(self.valid(), self.height == call_height))
        Requires(MustTerminate(call_height + 1))
        Ensures(self.valid())

        if call_height > 0:
            Unfold(self.valid())
            if self.left is not None:
                self.left.work(call_height - 1)
            if self.right is not None:
                self.right.work(call_height - 1)
            Fold(self.valid())

py2viper emits the Silver code that can be reduced to:

#!silver
function check(self: Ref): Bool

field foo: Int

predicate valid(self: Ref) {
    check(self) ==> acc(self.foo, write)
}

method test(self: Ref)
    requires check(self)
    requires [acc(valid(self)), true]
    requires (unfolding acc(valid(self), write) in self.foo == 2)
{
}

and which fails well-formedness check in Carbon because self.foo might be not framed.

---

• Bitbucket: https://bitbucket.org/viperproject/py2viper-translation/issue/52

[marcoeilers]

Original comment by Vytautas Astrauskas (Bitbucket: vakaras, GitHub: vakaras):

---

Note: [acc(valid(self)), true] in original code is [issubtype(typeof(self), Tree()), true].