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.