Issue with casting and verifier functions

[dddejan]

pragma solidity >=0.5.0;

contract FunctionArgs {

  uint8 x;
  uint y;

  /// postcondition x == __verifier_old_uint(x)
  function noop() public view returns (bool ok) {
    assert(x == y);
    return true;
  }
}

Gives

$ solc-verify.py FunctionArgs.sol --arith bv --output .
Error while running verifier, details:
Parsing ./FunctionArgs.sol.bpl
./FunctionArgs.sol.bpl(23,172): Error: invalid argument types (bv256 and bv8) to binary operator ==
1 type checking errors detected in ./FunctionArgs.sol.bpl

The culprit is the old expression bvzeroext_8_to_256(x#3[__this]) == old(x#3[__this]).

[hajduakos]

#85 is also related

[hajduakos]

A straightforward solution would be of course to have __verifier_old_uintN for N=8, ..., 256. But if I remember correctly, our plan was to rather support some kind of polymorphism.

[dddejan]

This happens because in the case of VERIFIER_* functions there is an if statement when converting arguments that skips temp variables for arguments. I guess this is a hack to prevent side-effects. We need a more pragmatic way to deal with functions that can be used in specification. I am trying to figure out, e.g., how to use keccak in specification and I'm running into similar issues.

[hajduakos]

Incorporating those temp variables could make this example work, because it would translate to bvzeroext_8_to_256(x#3[__this]) == old(bvzeroext_8_to_256(x#3[__this])). However, this would not work for #85. What we'd really like to have here is x#3[__this] == old(x#3[__this]), i.e., no casts at all. For this, we would need the Solidity AST for the spec expression to have the old expression return type uint8. Then the operator == will see that both of its arguments are uint8 and no casting is needed.

[hajduakos]

Of course there might be some special functions where the casting is needed, e.g., if keccak takes uint256 then the temp variables should be included because those will do the cast. But for old, there should be no casting.