Consensys/scribble

scribble produces invalid code given a constant let-binding used in a new context

cd1m0 opened this issue · 0 comments

cd1m0 commented

Given the following sample:

pragma solidity 0.8.10;

contract Foo {
    /// #if_succeeds let t:= Foo(0x0) in old(t.balanceOf())>0;
    function balanceOf() public view returns (uint) {}
}

Scribble will produce the following invalid code:

contract Foo is __scribble_ReentrancyUtils {
...
    function balanceOf() public returns (uint RET_0) {
        vars0 memory _v;
        unchecked {
            _v.old_0 = _v.t.balanceOf();
        }
        RET_0 = _original_Foo_balanceOf();
        unchecked {
            _v.t = Foo(0x0);
            _v.let_0 = _v.old_0 > 0;
            if (!(_v.let_0)) {
                emit AssertionFailed("0: ");
                assert(false);
            }
        }
    }

    function _original_Foo_balanceOf() private view returns (uint) {}
}

The issue is that _v.t is used before its defined.

The problem is that t was defined in the postcondition context (let t:= Foo(0x0)) but was used in the precondition context (old(t.balanceOf())). Scribble usually rejects such code as invalid, but we added an exception for the case where the let-binding is set to a constant expression. However when I added that exception I forgot to fix the transpiling code to move the definition of the let-binding to the precondition context.