Function calls in specifications (modifies, require, assert)

[dddejan]

Using functions as getters is quite common and it would be good to support them in specs, such as modifies or require. The following currently fails for two reasons:

1. modifies spec fails because it introduces new statements
2. require just puts true in the assume

pragma solidity >=0.5.0;
contract Issue78 {
  bool b;
  function isSet() public view returns (bool set) {
    return b;
  }
  /// @notice modifies b if !isSet()
  function set() public {
    require(!isSet());
    b = true;
  }
}

Current output

solc-verify.py Issue78.sol 
Error while running compiler, details:
Warning: This is a pre-release compiler version, please do not use it in production.

======= Converting to Boogie IVL =======

======= Issue78.sol =======
Issue78.sol:12:3: solc-verify error: Annotation expression introduces intermediate statements
  function set() public {
  ^ (Relevant source part starts here and spans across multiple lines).
Issue78.sol:12:3: solc-verify error: Annotation expression introduces intermediate declarations
  function set() public {
  ^ (Relevant source part starts here and spans across multiple lines).
solc-verify warning: Balance modifications due to gas consumption or miner rewards are not modeled
Issue78.sol:12:3: solc-verify error: Error(s) while processing annotation for node
  function set() public {
  ^ (Relevant source part starts here and spans across multiple lines).

[hajduakos]

To me (2) seems to work: require(!isSet()); is translated to a function call and an assume. However, the function call also introduces an extra assume ... true with traceability information. Is it possible that you overlooked the "real" assume?

[hajduakos]

(1) is a good question. Strictly speaking in the terminology of Solidity, this is actually not a getter and we do support "real" getters (see test/solc-verify/specs/Getter.sol). But I see your point. Such "simple" functions could be translated to Boogie functions (instead of procedures) and then they could appear as part of an expression in the specs. Two questions:

1a. Who should decide if a Solidity function is translated to a Boogie function or a procedure? Should we introduce an annotation or should we try to do it automatically?

1b. If a Solidity function is translated to a Boogie function, it cannot be annotated with specs. In this case should we have two copies: one Boogie function (to be used in specs) and one Boogie procedure (to be reasoned about).

For example, we could stay at translating functions to procedures, and when we see a call to a function in specs, we inspect that function if it is "simple" enough to be translated to a Boogie function. If yes, we introduce this function and use it in the specs, otherwise we report an error. For example, if the body of the function is a single return statement with an expression with no side effects, we should be able do it.

[dddejan]

To me (2) seems to work: require(!isSet()); is translated to a function call and an assume. However, the function call also introduces an extra assume ... true with traceability information. Is it possible that you overlooked the "real" assume?

True, I think I simplified the case too much. Consider a bit more complex contract.

pragma solidity >=0.5.0;

contract Issue78 {
  mapping(address=>bool) marked;
  function isMarked() public view returns (bool m) {
    return marked[msg.sender];
  }
  /// @notice modifies marked[msg.sender] if !marked[msg.sender]
  function mark() public {
    require(!isMarked());
    marked[msg.sender] = true;
  }
}=

Here we get

$solc-verify.py Issue78.sol --output .
Issue78::isSet: OK
Issue78::set: ERROR
 - Issue78.sol:12:3: Function might modify 'marked' illegally
Issue78::[implicit_constructor]: OK

Somehow the call to the view function doesn't cary over that nothing gets modified. Is that a separate issue: "view functions should have modifies none spec"?

I was thinking that when modifies clauses exist in the spec of some function, we assume modifies none spec for other functions that don't have modifies spec.

[dddejan]

(1) is a good question. Strictly speaking in the terminology of Solidity, this is actually not a getter and we do support "real" getters (see test/solc-verify/specs/Getter.sol). But I see your point. Such "simple" functions could be translated to Boogie functions (instead of procedures) and then they could appear as part of an expression in the specs. Two questions:

I see. Maybe best to just require the users to specify their manually implemented getters. For example, in the more complex example, have the spec @notice returns marked[msg.sender].

[hajduakos]

As for the old(...) stuff, it should be easy to automatically add it to the if part of modifies. We should decide what we like and precisely document it.

This makes sense to me as default. Any arguments against?

[dddejan]

Ah, somehow my reply turned into an edit :(

[hajduakos]

Here is the fixed example again:

$ cat test.sol && solc-verify.py test.sol
pragma solidity >=0.5.0;

contract Issue78 {
  mapping(address=>bool) marked;
  /// @notice postcondition m == marked[msg.sender]
  function isMarked() internal view returns (bool m) {
    return marked[msg.sender];
  }
  /// @notice modifies marked[msg.sender] if __verifier_old_bool(!marked[msg.sender])
  function mark() public {
    require(!isMarked());
    marked[msg.sender] = true;
  }
}
Issue78::mark: OK
Issue78::[implicit_constructor]: OK
Use --show-warnings to see 1 warning.
No errors found.

You need specs for isMarked because it is public and the modifies clause needs old(...).

[hajduakos]

As for the old(...) stuff, it should be easy to automatically add it to the if part of modifies. We should decide what we like and precisely document it.

This makes sense to me as default. Any arguments against?

Makes sense, I will fix that

[dddejan]

Yes, above works and it doesn't need the postcondition on isMarked().

I guess the solution is to

1. have function annotation for returns
2. use this annotation is function is used in specs and doesn't modify state