Comment on page
Assertion Checking Modes
There are several options for what Scribble can do when an assertion fails. By default Scribble will emit an
assert (false) and an additional log statement emit AssertionFailed(".."). For example, given this annotated code:contract Foo {
/// #if_succeeds {:msg "P1"} y == x + 1;
function inc(uint x) public pure returns (uint y) {
return x+1;
}
}
The instrumented code would look like this:
contract Foo {
event AssertionFailed(string message);
function inc(uint x) public returns (uint y) {
y = _original_Foo_inc(x);
if ((!((y == (x + 1))))) {
emit AssertionFailed("0: P1");
assert(false);
}
}
function _original_Foo_inc(uint x) private pure returns (uint y) {
return (x + 1);
}
}
Sometimes for long running tests and fuzzing campaigns we don't want to interrupt the tests for every violation found. In those cases you can prevent
scribble from emitting assert(false) with the --no-assert option.In some cases signaling a user property violation using event logging may be inconvenient, since the assertion failure check may occur in a
view function. In such cases adding an emit statement changes the mutability of the instrumented function, which can change the interfaces of the compiled contracts and may break tests. For this reason scribble (and Mythril and Harvey) support an alternative mode for signaling custom property violations using memory stores with specially crafted bit-strings. You can select this mode with the --user-assert-mode mstore command line option. If you were to instrument our earlier exmaple in this mode the instrumented code would look as such:contract Foo {
struct vars0 {
uint256 __mstore_scratch__;
}
function inc(uint x) public pure returns (uint y) {
vars0 memory _v;
y = _original_Foo_inc(x);
{
_v.__mstore_scratch__ = 0xcafecafecafecafecafecafecafecafecafecafecafecafecafecafecafe1000;
if ((!((y == (x + 1))))) {
_v.__mstore_scratch__ = 0xcafecafecafecafecafecafecafecafecafecafecafecafecafecafecafe0000;
assert(false);
}
}
}
function _original_Foo_inc(uint x) private pure returns (uint y) {
return (x + 1);
}
}
In this mode the assertion failure is signaled by the store to
_v.__mstore_scratch__ on line 12. Tools such as Myhtril and Harvey can watch for assignments to memory with the 0xcafe pattern appended with the id of the failing assertion.Last modified 1yr ago