Issue with ensure in contracts feature

[jiten-thakkar]

Smack gives error while verifying this code:

#include <stdio.h>
#include <stdlib.h>
#include <smack.h>
#include <smack-contracts.h>

int Add(int x, int y)
{
  requires( 0 <= x && 0 <= y);

  int r = x;
  int n = y;
  //this while loop is important to introduce multiple basic blocks in the IR
  while (n != 0) {
    invariant (r == x+y-n && 0 <= n);
    r = r + 1;
    n = n - 1;
  }
  r = r + y;
  ensures(r == x + y);
  return r;
}

int main(void) {

  printf("%d\n", Add(1, 2));
  return 0;
}

Here is the error:

SMACK program verifier version 1.7.2
requires.bpl(1675,24): Error: undeclared identifier: $i2
1 name resolution errors in requires.bpl

Unhandled Exception:
cba.Util.InvalidProg: Cannot resolve requires.bpl
  at cba.Util.BoogieUtil.ReadAndOnlyResolve (System.String filename) [0x0003a] in <ab3c6580195145e799277573c16d3293>:0 
  at cba.Driver.GetInputProgram (cba.Configs config) [0x00000] in <6edd479f33b847bab00001b84b260254>:0 
  at cba.Driver.run (System.String[] args) [0x00049] in <6edd479f33b847bab00001b84b260254>:0 
  at cba.Driver.Main (System.String[] args) [0x0005d] in <6edd479f33b847bab00001b84b260254>:0 
[ERROR] FATAL UNHANDLED EXCEPTION: cba.Util.InvalidProg: Cannot resolve requires.bpl
  at cba.Util.BoogieUtil.ReadAndOnlyResolve (System.String filename) [0x0003a] in <ab3c6580195145e799277573c16d3293>:0 
  at cba.Driver.GetInputProgram (cba.Configs config) [0x00000] in <6edd479f33b847bab00001b84b260254>:0 
  at cba.Driver.run (System.String[] args) [0x00049] in <6edd479f33b847bab00001b84b260254>:0 
  at cba.Driver.Main (System.String[] args) [0x0005d] in <6edd479f33b847bab00001b84b260254>:0 

Error invoking command:
corral requires.bpl /tryCTrace /noTraceOnDisk /printDataValues:1 /k:1 /useProverEvaluate /timeLimit:1200 /cex:1 /maxStaticLoopBound:1 /recursionBound:1
corral returned non-zero.

You can look at the bpl file here: https://gist.github.com/jiten-thakkar/b4c21f53d9b63e6ae0f3474ddf47873b

[jiten-thakkar]

@michael-emmi Can you please give your thoughts on this issue? Here the problem is that in the generated boogie code, the variable in the ensure statement is not the same as the return variable. I talked with @zvonimir and we are thinking of adding a return function in contracts in smack. What do you think?

[michael-emmi]

Ah yes, the problem here is that you want to refer to the value returned from the function in the ensures specification. In general, this cannot be matched to a single LLVM register variable, so encoding this as a call to ensures with a return value as an argument will not work.

This was partially handled in an older version, e.g., in the now failing result.c regression, via the result function of smack-contracts.h:

int old(int term);
int result(void);

(There was also an old function, to refer to the pre-call value of a given expression.)

These functions need to be reimplemented. Also, they should be renamed to __CONTRACT_old and __CONTRACT_result to be consistent with the other contract functions.

By the way, as a developer, you should compile Smack in debug mode, in which case you will notice a failing assertion long before Boogie code even gets generated on this example. The failing assertion insists that procedure specifications should be declared at the start of procedures, before any loops.

[michael-emmi]

By the way, see here for the previous implementation of result.