[Move Prover] Incomplete display of havocked variables

[junkil-park]

Problem

When a struct is havocked, Prover's error trace does not say that the struct was havocked.

How to reproduce

module 0x42::loop_inv {
    use std::vector;

    struct R has key {
        v1: vector<u64>,
        v2: vector<u64>,
    }

    spec fun spec_all_zeros(v: vector<u64>): bool {
        forall i in 0..len(v): v[i] == 0
    }


   fun f() acquires R {
        let r = borrow_global_mut<R>(@0x42);
        spec {
            assume spec_all_zeros(r.v1);
            assume spec_all_zeros(r.v2);
        };

    let i = 0;
        while (i < 5) {
            vector::push_back(&mut r.v1, 0);
            i = i + 1;
        };

         spec {
            assert spec_all_zeros(r.v1);
            assert spec_all_zeros(r.v2);
        };
   }

Prover produces the following error:

RUST_BACKTRACE=1 move prove -t loop_inv.move
[INFO] preparing module 0x42::loop_inv
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 1 verification conditions
[INFO] running solver
[INFO] 0.031s build, 0.005s trafo, 0.005s gen, 1.479s verify, total 1.521s
error: unknown assertion failed
   ┌─ ./sources/loop_inv.move:30:13
   │
30 │             assert spec_all_zeros(r.v1);
   │             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at ./sources/loop_inv.move:14: f
   =     at ./sources/loop_inv.move:15: f
   =         r =
   =           &loop_inv.R{
   =             v1 = vector{(size): 24464, default: 5706},
   =             v2 = vector{(size): 26962, default: 5706}}
   =     at ./sources/loop_inv.move:17: f
   =     at ./sources/loop_inv.move:18: f
   =     at ./sources/loop_inv.move:21: f
   =         i = 0
   =     at ./sources/loop_inv.move:23: f
   =     enter loop, variable(s) i havocked and reassigned      <---  missing the info that `r` is also havocked.
   =         i = 18472
   =     at ./sources/loop_inv.move:22: f
   =     at ./sources/loop_inv.move:30: f
...
...
...

[junkil-park]

@jyao15 is looking at this issue.

[jyao15]

The problem lies in the is_temporary function in model.rs. The function tells whether a bytecode variable is temporary (i.e., compiler-introduced instead of user-defined). Its current implementation simply checks whether the bytecode variable ID is greater than the number of user-defined variables. This is correct in stackless bytecode, but may not be correct after a sequence of bytecode transformations.

In this example, in the stackless bytecode, bytecode variable $t0 corresponds to user-defined variable i, and bytecode variable $t1 corresponds to user-defined variable r. The number of user-defined variables is 2, so both $t0 and $t1 are correctly recognized as non-temporary. But after 10 transformation passes, at the time we do loop analysis, $t1 is no longer used in the bytecode. Instead, $t3 corresponds to r, but it is recognized as temporary, so r is missing in the error trace.

I do not know how this can be easily solved.

[wrwg]

This one maybe hard to fix and requires tracking of variables derived from user defined variables. For example, there can be two temporary variables derived from the same user variable. Lower priority for now.

One option is to have a flag that temporary variables are also displayed.