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);
 }
}
The emit AssertionFailed("0: P1") statement on line 7 is used to signal to tools such as Mythril and Harvey that a user property violation was found . It can be also useful for the end user to identify which property failed in normal test runs by looking at the emitted events.
No assertions
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.
User assertion failures without event logging
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