Execution of contract initialization code

[nwatson22]

The solidity compiler gives us two EVM bytecode strings per contract, a deployedBytecode and bytecode field. The first is the bytecode that will actually exist on the blockchain and the second is the code that only runs once when the contract is created, returns the deployedBytecode, and then is discarded. For our purposes the bytecode is where the contract constructor code is automatically run, and any default variable assignments like in:

contract InitCodeTest is Test {
    uint a = 123;
}

Currently the bytecode field is ignored by KEVM. For engagements we had been using workarounds such as moving any variable initializations into the constructor and calling the constructor at the top of the methods we are actually executing. However this is especially important to avoid having to do for other people's foundry tests, because if you modify them like that, you arguably aren't actually verifying the same test.

While the constructor is actually contained as a function call available in deployedBytecode, from what I understand, the contract-level default variable assignments are not accessible unless we bring in the bytecode. I've done that here by creating a different macro #initBytecode which is an analogue of #binRuntime and rewrites to the initialization bytecode of the contract.

The difference between the constructor/initialization code and the setUp() function, which is built into foundry, and which we already handle, is the setUp() function is run before every test by foundry, whereas I guess there is no guarantee that this will be the case for the former, so perhaps a test like this:

contract InitCodeTest is Test {

    uint a = 1;

    function test_init() public {
        assertEq(a, 1);
    }
}

would not actually make any sense because as soon as you start adding other tests that could change the value of a, it's not necessarily going to pass depending on the order the tests are run in.

For this reason I think we need to have a discussion on what a sensible default should be for "what state should the contract be in when we execute a method". My initial thought would just be to assume the contract has just been initialized for each method, and to possibly provide some sort of interface for selecting a different option, but I would want to hear from people who have actually used the Kontrol tool in engagements.

An additional concern I have is that the implementation I am envisioning would treat the initialization as a separate execution step, similar to how we already treat the setUp() function, since the "initial state" generated from this step would be shared among all tests in the contract. But this would create yet another stage slowing down execution + slowing down the CI job, and this stage wouldn't be avoidable as the setUp() function is by not including the function. (Every contract has this initialization step, although possibly we could make it optional to skip it as in many cases it doesn't do anything for our purposes, i.e., if there is no constructor and no default values to storage vars).

[nwatson22]

I've now implemented a third execution stage for contract symbolic execution which runs the contract initialization code.
In addition proof KCFGs now extend backwards to include/show execution of any earlier stages (the contract initialization code stage and the setUp() function, if it exists). This ideally will enable us to handle branching in the setUp() function or the new initialization phase (includes the constructor execution).

One problem I'm not sure how to handle is that the constructor, if not marked payable, will branch on CALL_VALUE==0 and fail on the branch where it is not 0. Possibly we would want to keep that behavior and just allow initializing proofs on top of prior stages where some failure nodes have been reached. For now I've just marked the constructor for the test I've been using as payable.

Still to do:

• Make running the initialization stage optional, since it adds overhead and many proofs don't do anything in the init stage anyway
• Init proofs are always rerun. Figure out a way to cache them and only reinit when necessary like with the other proofs.

[palinatolmach]

Thanks @nwatson22! It's better to check this, but I'm almost certain that Foundry runs every test on the state produced by the execution of the setUp() function, which eliminates the problem of different test ordering and is the behavior I would expect.

I found this discussion in Foundry's repo which suggests that a test should be using either constructor or setUp(): foundry-rs/foundry#5471; I also came across a few issues there suggesting that constructors are used in some of the tests (though I agree that it's probably less common than setUp), e.g.,

contract adapterTestFile is Test  {
    string ARBITRUM_RPC_URL = vm.envString("ARBITRUM");
    /* ... */

    constructor() {
        uint forkheight = 53_513_381;
        vm.createSelectFork(ARBITRUM_RPC_URL, forkheight);
         /* ... */
    }
}

Considering this, I was thinking that we might execute either initialization code or setUp, but in this case we'll again be ignoring values of variables initialized outside of setUp() (such as uint a = 1; in the above example).

@ehildenb @RaoulSchaffranek @iFrostizz do you guys have any suggestions and/or experience with the contracts containing the initialization code we didn't consider?

[ehildenb]

@nwatson22 can you move this PR over to runtimeverification/kontrol repo instead?

[nwatson22]

Moved to kontrol: runtimeverification/kontrol#54
and pulled a much smaller set of changes into a separate PR #2096 to support this.