Constructor chaining broken

[shuvendu-lahiri]

pragma solidity ^0.4.24;

contract A {
    uint x;
    constructor (uint a) {x= a;}
}

contract B is A {
    constructor (uint a) A(a) {x++;}
}

contract C is B {
    constructor (uint a) B(a) {x++; assert (x == a + 2);}
}

[shuvendu-lahiri]

Each base constructor is invoked only once. To figure out the argument with which to invoke a base constructor that is transitively reachable such as A reachable from C, C has to look at B's constructor to figure out A's constructor argument.

[shuvendu-lahiri]

File ConstructorChaining.sol highlights the issue.

[shuvendu-lahiri]

Example to handle before closing the issue

pragma solidity ^0.5.1;

contract A {
    uint x;
    constructor () public {x++;}
}

contract B is A {
    constructor () A() public {}
}

contract C is B {
    constructor () public {assert (x == 1);}
}

[shuvendu-lahiri]

The above example added as ConstructorChaining2.sol. Even though VeriSol calls A's constructor is invoked twice by VeriSol, the second time, we reset the state back to 0 again.

[ellab123]

After the partial fix (pull request #225) there is an issue of a base constructor being called more than once. Here's a (failing) test that reproduces the issue: D constructor is called twice, as can be seen in corral.txt.

pragma solidity >=0.4.24 <0.6.0;
 contract D {
    uint x;
     constructor () public { x++; }
 }

 contract B is D {
     constructor () D() public {}
 }

 contract C is B {
     constructor () public { assert (x == 2); }   
 }

[shuvendu-lahiri]

An example that shows unsoundness of the current implementation:

pragma solidity ^0.5.2;

contract A {
    // need a struct as a 
    //   scalar variable is explicitly initialized
    //   map variables get a new address 
    struct A {
        mapping (int => bool) x;    
    } 
    A a;

    constructor () internal {
       require(!a.x[0]);
       a.x[0] = true;
    }
}

contract B is A {
}

contract C is A, B {
    constructor()
    public {
    assert(false);
    }   
}