SRI-CSL / solidity

This is solc-verify, a modular verifier for Solidity.
https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md
GNU General Public License v3.0
50 stars 14 forks source link

Friendlier messages when implicit constructor cannot be created #137

Open hajduakos opened 4 years ago

hajduakos commented 4 years ago

If there is an unsupported feature in a function, we give a quite user friendly message and skip that function. However, implicit constructors are generated separately and for them this is not done, but rather some confusing errors are printed.

For the following contracts

pragma solidity >=0.5.0;

contract Base {
    constructor() public {
        assembly { /* ... */ }
    }
}

contract Derived is Base { }

we get the output

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

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

======= Impl.sol =======
Impl.sol:5:9: solc-verify error: Inline assembly is not supported
        assembly { /* ... */ }
        ^--------------------^
Impl.sol:4:5: solc-verify warning: Errors while translating function body, will be skipped
    constructor() public {
    ^ (Relevant source part starts here and spans across multiple lines).
Impl.sol:5:9: solc-verify error: Inline assembly is not supported
        assembly { /* ... */ }
        ^--------------------^

The first error and warning corresponds to skipping the constructor of Base. However there is an extra error afterwards that corresponds to inlining the constructor of Base when creating the implicit constructor of Derived, but this cannot be seen in the output. This also makes the whole translation and verification fail, instead of printing the skipped functions in a nice way. The workaround should be simple, we just have to include the error reporter swapping code from functions into implicit constructors as well.

hajduakos commented 4 years ago

If we add the constructor explicitly, it works:

pragma solidity >=0.5.0;

contract Base {
    constructor() public {
        assembly { /* ... */ }
    }
}

contract Derived is Base {
    constructor() public {}
}

gives

Base::[constructor]: SKIPPED
Derived::[constructor]: SKIPPED
Use --show-warnings to see 2 warnings.
Some functions were skipped. Use --show-warnings to see details.
No errors found.

Output should be similar if the constructor is implicit.

hajduakos commented 4 years ago

Fixed in 4beece6