scribbleis still beta software and bugs will happen. In such cases it may be useful for you to understand how Scribble generates instrumented code. For this we will look at two examples.
addfunction now lives in the new private function
add()we invoke the renamed original function (line 13), and check the
if_succeedsannotation after the call (lines 14-17).
oldexpressions are evaluated before the call (line 12) and require a temporary variable. However, instead of just adding multiple temporary variables, we group all of the temporary variables needed inside of a single struct (
vars0) defined on lines 4-6. This is done to reduce the extra stack space used by instrumented code.
AssertionFailedevent (line 15).
0: test(line 15) is emitted. The
testpart is the original user-readable label in the annotation.
0is an internally assigned id. Scribble assigns such an id for each annotation we write. It is possible to hint Scribble to also output a metadata with map from ids to the original property. See more about the metadata format in section JSON output specification.
-m json) command line option as part of JSON output in
--instrumentation-metadata-file path/to/meta-file.jsoncommand line option to get it in a standalone JSON file at specified path.
__scribble_ReentrancyUtils(lines 2-4) was added. This contract was also added as a base contract of
Foo. (line 6).
__scribble_ReentrancyUtilscontains a single boolean property that is used for tracking whether the current stack frame is the root frame of an external call. This is useful as public functions can be called both internally and externally, but we only want to check contract invariants in them when they are called externally.
__scribble_Foo_check_state_invariants_internalwas added (lines 36-41) which actually checks whether the invariant is true. It is only called indirectly, by
__scribble_check_state_invariantswhich is itself called by the wrapped functions.
addfunction (lines 22-33) was wrapped similarly to functions in the previous section. The wrapper (lines 22-29) invokes the
__scribble_check_state_invariantsfunction at the end of execution (line 27) to check whether the invariant is preserved by the call to
externalthen the call on line 27 would be unconditional.
__scribble_out_of_contractstate variable defined in the contract. This is used to keep track of whether we are just entering the contract or not. The logic is particularly involved for public functions. Note that in the public function
add, whether we check the invariants at the end depends on the value of
__scribble_out_of_contractat the start of the function (which was stored in
_v.__scrible_check_invs_at_endon line 24). This reflects the intuition that we want to check contract invariants only at the end of external calls, not internal calls (for more details on contract invariants see Contract Invariants).