Missing invocations to base constructors.

[michael-emmi]

$ cat Test.sol && solc-verify.py --out . Test.sol ; grep "[DE]::" -A 6 Test.sol.bpl 

/// @notice invariant x == 42
contract C {
    int x;
    constructor() public { x = 42; }
}

/// @notice invariant C.x == 42
contract D is C { }

/// @notice invariant C.x == 42
contract E is C {
    constructor() public { }
}

Verifying C::[constructor]: OK
Verifying D::[implicit_constructor]: ERROR
 - Source Test.sol, line 9, col 1: State variable initializers might violate invariant 'C.x == 42'.
Verifying E::[constructor]: ERROR
 - Source Test.sol, line 13, col 5: Invariant 'C.x == 42' might not hold at end of function.
Errors were found by the verifier.
procedure {:sourceloc "Test.sol", 9, 1} {:message "D::[implicit_constructor]"} __constructor#14(__this: address_t, __msg_sender: address_t, __msg_value: int)
    ensures {:sourceloc "Test.sol", 9, 1} {:message "State variable initializers might violate invariant 'C.x == 42'."} (x#2[__this] == 42);

{
    __balance := __balance[__this := 0];
}

--
procedure {:sourceloc "Test.sol", 13, 5} {:message "E::[constructor]"} __constructor#21(__this: address_t, __msg_sender: address_t, __msg_value: int)
    ensures {:sourceloc "Test.sol", 13, 5} {:message "Invariant 'C.x == 42' might not hold at end of function."} (x#2[__this] == 42);

{
    __balance := __balance[__this := 0];
    $return1:
}

[hajduakos]

This is work in progress, as of f9efd13 we now inline the body of base constructors so this example should work. Being able to pass arguments for the base constructors is coming soon.

[hajduakos]

Base constructor arguments are also implemented in 8a9fe1d

It works for simple cases like the following (arguments provided either in inheritance list or as modifiers): https://github.com/SRI-CSL/solidity/blob/8a9fe1d7995a97a82ab6c4cbc4e85f5308214cab/test/solc-verify/InheritanceBaseConstructorArgs.sol, but needs some more tests for complex cases

[hajduakos]

It does not yet work for cases when the base constructor has modifiers (that will require some extra inlining job), but instead of silently ignoring it, there is an appropriate error message.

[hajduakos]

However, I think this issue can be closed as the base constructor call is not missing anymore. There might be errors, but we can open separate issues for those.

[hajduakos]

Base constructors with modifiers are also working as of de5efb6.

[dddejan]

I added a new test case failing with constructors

solc-verify.py test/solc-verify/BaseConstructorOrder.sol --output .
Error while running verifier, details:
[TRACE] Using prover: /usr/local/bin/z3
Parsing ./BaseConstructorOrder.sol.bpl
./BaseConstructorOrder.sol.bpl(93,12): Error: undeclared identifier: _x#18
1 name resolution errors detected in ./BaseConstructorOrder.sol.bpl

[dddejan]

solc-verify.py test/solc-verify/BaseConstructorOrder.sol --no-modifies-analysis --output .
Verifying A::set: OK
Verifying A::[constructor]: OK
Verifying B1::[constructor]: OK
Verifying B2::[constructor]: OK
Verifying BaseConstructorOrder::[constructor]: ERROR
 - Source test/solc-verify/BaseConstructorOrder.sol, line 23, col 5: Assertion might not hold.
Verifying BaseConstructorOrder::: OK
Errors were found by the verifier.