`__CPROVER_old` is ignored when called form a spec function

[JustusAdam]

The __CPROVER_old primitive is not recognized when called from a spec function, whereas inlining the same code into the contract makes it work.

Concretely this example works

void modify(int *i)
__CPROVER_requires(*i < 10)
__CPROVER_ensures(*i == __CPROVER_old(*i) + 1)
__CPROVER_assigns(*i)
{
    *i += 1;
}


int main() {
    int i = 0;
    modify(&i);
}

but this refactor of the same code does not.

int check(int *i) {
    return *i == __CPROVER_old(*i) + 1;
}


void modify(int *i)
__CPROVER_requires(*i < 10)
__CPROVER_ensures(check(i))
__CPROVER_assigns(*i)
{
    *i += 1;
}


int main() {
    int i = 0;
    modify(&i);
}

It fails not quite silently but emits a warning before failing the verification

warning: ignoring old
  * type: signedbv
      * width: 32
      * #c_type: signed_int
  * #source_location: 
    * file: test.c
    * line: 2
    * function: check
    * working_directory: /Users/justbldr/research/kani/tests/kani/FunctionContract
  0: constant
      * type: signedbv
          * width: 32
          * #c_type: signed_int
      * value: 1

CBMC version: 5.84.0
Operating system: OSX
Exact command line resulting in the issue: goto-instrument --enforce-contract modify test.out test.out2 && cbmc test.out2
What behaviour did you expect: Verification success
What happened instead: Verification failure and warning

This is currently blocking model-checking/kani#2545

[remi-delmas-3000]

Hi, right now __CPROVER_old must apply to function parameters, modulo certain basic operations like addition or dereference. Occurrences of __CPROVER_old are replaced by snapshot variables that are defined before the function call.

old_i = *i;
assume(*i < 10);
modify(i);
assert(old_i + 1 == *i);

With this snapshot encoding, embedding __CPROVER_old in a function makes it hard to know statically (at program instrumentation time) what the argument of __CPROVER_old may refer to since there could be arbitrary computations happening before reaching __CPROVER_old, that may depend on the outputs of the function itself, or may resolve to memory locations that did not even exist before function invocation.

We have no easy way of addressing that right now (besides dynamically resolving them during symex).
The workaround is to write the post condition as

bool check(int *i, int* old_i) {
  return i  == old_i + 1;
}

and use it as

__CPROVER_ensures(check(i, __CPROVER_old(i)))

Which makes the target of __CPROVER_old unambiguous.

[JustusAdam]

Thanks for clarifying. I also just realized that the documentation actually mentions this. my bad.