Unsound translation of calls with specs.

[michael-emmi]

The call to g below ought to havoc x before assuming its postcondition x == 0, but it doesn’t, resulting in the inconsistent state x == 0 && x > 0.

smart-contract-explorer $ cat a.sol && solc-verify.py a.sol 
pragma solidity ^0.5.0;

contract A {
    int x;

    /// @notice precondition x > 0
    function f() public {
        g();
        assert(false);
    }

    /// @notice modifies x
    /// @notice postcondition x == 0
    function g() public;
}
A::f: OK
A::[implicit_constructor]: OK
No errors found.

[hajduakos]

I believe this issue also holds when a function cannot be translated due to an unsupported feature.

[hajduakos]

Fixed in d5fdea1dd82273aec38252ce4a013629370c5bac

[hajduakos]

@michael-emmi please check and close issue if OK

[michael-emmi]

This seems basically OK now, but there’s still something weird happening with postconditions.

Consider the following program, where f asserts the fact that g should establish:

$ cat a.sol && solc-verify.py a.sol
pragma solidity ^0.5.0;

contract A {
    int x;

    function f() public {
        g();
        assert(x == 0);
    }

    /// @notice modifies x
    /// @notice free postcondition x == 0
    function g() public { }
}
A::f: ERROR
 - a.sol:8:9: Assertion might not hold.
A::g: OK
A::[implicit_constructor]: OK
Use --show-warnings to see 1 warning.
Errors were found by the verifier.

Yet the verifier says that f is incorrect.

[hajduakos]

I believe there are some mistakes in the example.

1. @notice free postcondition seems like a mistake, free should be removed in order for the verifier to treat the expression as a postcondition.
2. g has an empty body, which of course does not satisfy the postcondition. If you want it to be skipped, the body should be omitted: function g() public;.
3. f calls g, which modifies x so f should also include a specification that it modifies x.

$ cat a.sol && solc-verify.py a.sol
pragma solidity ^0.5.0;

contract A {
    int x;

    /// @notice modifies x
    function f() public {
        g();
        assert(x == 0);
    }

    /// @notice modifies x
    /// @notice postcondition x == 0
    function g() public;
}
A::f: OK
A::[implicit_constructor]: OK
Use --show-warnings to see 1 warning.
No errors found.

[michael-emmi]

Oh apologies, my confusion was actually due to the free syntax, which I’d somehow assumed that you supported — it was actually not a typo :-) in Boogie this let’s you say that a postcondition should be used without having to prove its validity, e.g., for cases when the prover is not able to establish it due to reasoning limits.

So in summary, the example is what I intended, but you guys don’t support free, and everything makes sense 👍