With-blocks don't work with IO

[marcoeilers]

Originally reported by: Marco Eilers (Bitbucket: meilers, GitHub: meilers)

---

The with statements cannot be currently used in the IO verification because there is no way how to pass the required ghost arguments to the __exit__ that is implicitly called by with. For example, writing to a file that does not use with can be verified in this way:

#!python
def hello_file(t1: Place) -> Place:
    IOExists4(Place, Place, Place, int)(
        lambda t2, t3, t4, fp: (
            Requires(
                token(t1, 2) and
                open_io(t1, 'test', fp, t2) and
                write_io(t2, fp, 'hello', t3) and
                close_io(t3, fp, t4)
            ),
            Ensures(
                token(t4) and
                t4 == Result()
            ),
        )
    )
    fp, t2 = open(t1, 'test')
    t3 = write(t2, fp, 'hello')
    t4 = close(t3, fp)
    return t4

However, if we use with statement, then we do not need t4 = close(t3, fp) statement anymore because it is called implicitly, but we run into the problem how to return t4:

#!python
    with open(t1, 'test') as (fp, t2):
        t3 = write(t2, fp, 'hello')
    #t4 = ?
    return t4

One of the possible solutions would be to introduce LastPlace as described in
section 6.1.3:

#!python
        def open(path: str,
                 t1: Place = LastPlace()) -> Tuple[File, Place]:
            # The procedure's contract and body were omitted.
        def write_int(fp: File, number: int,
                      t1: Place = LastPlace()) -> t2: Place:
            # The procedure's contract and body were omitted.
        def close(fp: File, t1: Place = LastPlace()) -> Place:
            # The procedure's contract and body were omitted.
        def main(t1: Place) -> Place:
            IOExists4(Place, Place, Place, File)(
                lambda t2, t3, t4, fp: (
                    Requires(
                        token(t1, 2) and
                        open_io(t1, 'test', fp, t2) and
                        write_io(t2, fp, 5, t3) and
                        close_io(t3, fp, t4)
                    ),
                    Ensures(
                        token(t4) and t4 == Result()
                    )
                )
            )
            with open('test') as (fp, _):
                write_int(fp, 5)
            return LastPlace()  # Here LastPlace() refers to the place
                                # returned by close.

---

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