scribble icon indicating copy to clipboard operation
scribble copied to clipboard

Using state variable comparison in annotations with `mstore` mode

Open blitz-1306 opened this issue 2 years ago • 1 comments

Here is a small example:

contract Sample {
    uint public a;

    /// #try a == 1;
    function foo(uint256 x, uint256 y, uint256 z) pure public returns (uint256) {
        return x + y + z;
    }
}

With current Scribble version (0.6.22) it produces following output:

scribble ./sample.sol --instrumentation-metadata-file ./test.json --user-assert-mode mstore
/// This file is auto-generated by Scribble and shouldn't be edited directly.
/// Use --disarm prior to make any changes.
pragma solidity 0.8.19;

contract Sample {
    struct vars0 {
        uint256 __mstore_scratch__;
    }

    uint public a;

    function foo(uint256 x, uint256 y, uint256 z) public pure returns (uint256 RET_0) {
        vars0 memory _v;
        unchecked {
            if (a == 1) _v.__mstore_scratch__ = 42;
        }
        RET_0 = _original_Sample_foo(x, y, z);
    }

    function _original_Sample_foo(uint256 x, uint256 y, uint256 z) private pure returns (uint256) {
        return (x + y) + z;
    }
}

Output is not compiled due to foo() is declared as pure, but it should be view as it now contains state variable check:

if (a == 1) _v.__mstore_scratch__ = 42;

Diggig code for finding a root cause led me to following: https://github.com/ConsenSys/scribble/blob/d397fc877baf3490c9a60d1e2b0bea7793fb96d7/src/instrumenter/instrument.ts#L99-L103 Then in interpose() we have https://github.com/ConsenSys/scribble/blob/d397fc877baf3490c9a60d1e2b0bea7793fb96d7/src/instrumenter/interpose.ts#L212-L216 and basic assumption of following somehwere there also https://github.com/ConsenSys/scribble/blob/d397fc877baf3490c9a60d1e2b0bea7793fb96d7/src/instrumenter/interpose.ts#L370-L384

Seems that we still have edge-cases when annotations can cause state muntability elevation from pure to view or non-payable due to instrumentation. Unless I miss something. If so, we should at least throw an error so user would get idea that something is wrong with the annotation.

Regards.

blitz-1306 avatar May 15 '23 17:05 blitz-1306

if (a == 1) _v.mstore_scratch = 42;

Vanessaishot avatar Mar 18 '24 02:03 Vanessaishot