v0.5.7
This PR introduces 2 new small language features, and several bug fixes.
- Language Features:
- #123 Support abi.encodePacked in scribble
scribble
now allows abi.encode
, abi.encodePacked
, abi.encodeWithSelector
and abi.encodeWithSignature
in annotations. E.g.
contract Foo {
/// #if_succeeds keccak256(abi.encode(a,b)) == keccak256(res);
function encodeArgs(uint a, uint b) public returns (bytes memory res) {
...
}
}
- #93 Support require-annotations to guide tools
Two new annotations were added - #try
and #require
. These can be applied on a specific function, or on a contract (in which case they are applied to all mutable functions in the contract).
These two DO NOT correspond to new property types. Instead they are intended to be used as guidance for any back-end tools
that are directed by branch coverage. Thus they should be used with care and not included in the official specification. Specifically:
-
#require
- as the name suggest#require <predicate>
gets translated directly as arequire(predicate);
at the start of a function.
This is intended to prevent an underlying tool from exploring certain function. A common example we have found was fuzzers
unintentionally upgrading a part of a fuzzed contract system, and thus breaking the whole system. This is not an interesting direction to explore, as users often assume that privileged operations such as upgrade will not be performed maliciously. -
#try
-#try <predicate>
is translated as a vacuous if statement:
if (predicate) {
_v.scratch = 0x42;
}
The underlying if statement has no effect, but its branch acts as a hint for underlying tools to try certain values.
For example if we have the following code that attempts to execute a swap on UniswapV2:
function swapSomeTokens(uint amountIn, uint minOut, address[] path, ...) {
...
uniswapV2.swapExactTokensForTokens(amountIn, amountOut, path, ...);
}
And a backend fuzzer exercising the backend code, it may be tricky for the fuzzer to guess valid values for the addresses in path
.
Adding the following annotation:
/// #try (address[0] == <DAI ADDR> || address[0] == <WETH>) && (address[0] == <DAI ADDR> || address[0] == <WETH>);
function swapSomeTokens(uint amountIn, uint minOut, address[] path, ...) {
...
Would generate vacuous if statements in the instrumented code that would guide the fuzzer to trying some valid combinations
of token paths, and thus exploring more of the underlying code.
- Instrumentation/command line options:
- #106 Add optional assertions for checking property coverage
In certain cases due to bugs/missing debugging data it might be tricky to tell which properties were actually covered.
We've added a new --cov-assertions
flag, that will emit a dummy user assertion for each real assertion, that is emitted if the
real assertion is ever reach. So for example for this code:
contract Foo {
/// #if_succeeds {:msg "P0"} true;
function foo() public {
}
}
The instrumented code would look like:
function foo() public {
_original_Foo_foo();
unchecked {
{
emit AssertionFailed("HIT: 0: P0");
if (!(true)) {
emit AssertionFailed("0: P0");
assert(false);
}
}
}
}
Note that if the users sees the underlying tool report HIT: 0: P0
event is reachable, then the underlying tool
has exercised the property P0
at least once.
- Bug Fixes:
- #121 Scribble grammar unnecessarily requires
forall
be wrapped in parenthesis - #104 forall broken in new #limit annotation
- #103 Broken instrumentation for overriding public variables
- #101 Type-checker needs to support library-level constants
- #100 When interposing on constructors super constructor invocations get put on the wrong function.
- #99 Don't apply contract-level if_succeeds annotations to view functions
- #98 Unable to use forall on arrays with elements of used-defined type
- #89 if_updated annotations lost when mixing in forall annotations
- #88 Scribble crashes when mixing for_all and if_updated on nested mappings