`create_slice()` issues when calling another function with array arguments

[JunmingZhao42]

Currently if an array argument is used when calling another function, the transpiler adds create_slice() of the original array which seems to drop the predicates of the original array. For example:

/* @ predicate my_array(array: IArray) {
  alen(array) == 2 && acc(array[0..2])
}
@*/

fun main() {
    var test = <1,2>;
    /*@ inhale my_array(test) @*/
    var 1 result = tuple_equal(test);
    return 0;
}

fun tuple_equal({1,1} buffer) {
    /*@ requires my_array(buffer) @*/
    /*@ ensures (retval == 1) || (retval == 0) @*/
    /*@ unfold my_array(buffer) @*/
    var ret = (buffer.0 == buffer.1);
    return ret;
}

In main() function when calling tuple_equal(test), there's a copy of test created in the transpiled silver code, where the copied one doesn't preserve my_array().

[alegnani]

The problem here is that, in order for all arguments to have copy semantics, we need to explicitly copy the IArray used to represent <1, 2>. The issue would be fixed by something like this:

unfold pred(x)
copied_x := create_slice(x)
fold pred(copied_x)

function_call(copied_x)

// this would only be needed if the predicate is in the post condition
unfold pred(copied_x)
fold pred(x)

This could be added automatically by scanning the predicates in the pre- and postconditions of the called function.

Issues arise if we have more complicated examples like the following:

predicate marker()

method foo(x: Int)
requires x != 0 ==> marker()

method bar() {
    var x: Int
    if (x != 0) {
        inhale marker()
    }
    foo(x)
}

This might be complicated to generate with the transpiler.

Note: inhale my_array(test) should be fold my_array(test), as unfolding the predicate my_array would prove false, by providing 2 write permissions to the struct.

[alegnani]

The fix we agreed on is to try to encode everything in the predicate s.t. we only have pre-/postconditions of the following type:

requires predicate(x, y, ...)
ensures predicate(x, y, ...)

We can then collect these annotations and generate unfol/fold statements when doing the method call.

[JunmingZhao42]

The fix we agreed on is to try to encode everything in the predicate s.t. we only have pre-/postconditions of the following type:

requires predicate(x, y, ...)
ensures predicate(x, y, ...)

We can then collect these annotations and generate unfol/fold statements when doing the method call.

What about post conditions like ensures x == old(x) when x is of type Int?