Scribble accepts normal Solidity files and has 3 output modes:
In flat
mode, all the dependencies of the target Solidity file(s) are bunched up and emitted as one giant blob of Solidity that can be compiled or directly submitted to MythX.
In files
mode, for each file foo.sol
containing contracts with scribble annotations, Scribble emits a foo.instrumented.sol
in the same directory and leaves the original unchanged. Note that scribble
may instrument files that are not specified on the command line, but are reachable by a chain of imports.
In json
mode, Scribble behaves similarly to flat
mode, in that it first flattens all the files necessary to compile the target into one flat Solidity blob. Afterwards, it runs solc
on that flat solidity blob and outputs the standard JSON output of the compiler. Additionally to the JSON of the compiler, Scribble adds a propertyMap
field that maps property identifiers back to their source location.
We provide examples for the most common use cases. For all examples assume we have the following 2 solidity files in the current directory:
Base.sol
contract Base {}
Foo.sol
import "Base.sol";contract Foo is Base {/// if_succeeds {:msg "P1"} y == x + 1;function inc(uint x) public pure returns (uint y) {return x+1;}}
If we want to instrument Foo.sol
(and any required imports) and emit it all into a single Foo.flat.sol
we can run:
scribble Foo.sol --output-mode flat --output Foo.flat.sol
Note that both the input and the output can be --
which would make Scribble work with stdin
/stdout
. The below command uses stdin
/stdout
to do the same thing as the previous command:
cat Foo.sol | scribble -- --output-mode flat --output -- > Foo.flat.sol
The files
mode is more involved and is intended for interoperability with various user testing and deployment environments. To instrument Foo.sol
and Base.sol
in-place we run:
scribble Foo.sol --output-mode files
After running this we will have 2 new files in the directory - Foo.instrumented.sol
and __scribble_ReentrancyUtils.sol
. Foo.instrumented.sol
is the instrumented version of Foo.sol
, and __scribble_ReentrancyUtils.sol
contains a helper contract.
Note that the instrumented Foo.instrumented.sol
still imports the original Base.sol
. To actually use the instrumented files in this mode, you have to swap them with the originals, before compiling/testing/deploying. You can do so manually, or automatically with the the --arm
and --disarm
options to scribble (more details here).
Emitting an instrumented JSON artifact is almost the same as running in flat-mode:
scribble Foo.sol --output-mode json --output Foo.flat.json
The generated Foo.flat.json
contains the target solidity files and their dependencies, compiled in the standard solidity JSON format.
-h, --help Print help message-v, --version Print package version-q, --quiet Don't output anything to stderr-i, --input-mode string Input mode. Either 'source' or 'json'. When 'source' is specified, inputassumed to be a raw Solidity source code. When 'json' is specified, inputassumed to be a Solc output JSON artifact.-m, --output-mode string Output mode. Either 'flat', 'files' or 'json'. When 'flat' is specified,output all instrumented contracts toghether. When 'files' is specified, forevery file Foo.sol that contains an annotated contract emit aFoo.sol.instrumetned with the instrumented contract. When 'json' isspecified, a JSON object including the original sources, the flattenedbytecode, and a map from property IDs to their locations.-k, --keep-instrumented Keep instrumented files after disarming.-o, --output string When the output mode if 'flat' or 'json' specifies where to dump theflattened contracts. Either a path to a file, or '--' for stdout.--utils-output-path string Path to a folder where the ReentrancyUtils.sol contract should be emitted.This option is required with '--mode files' and ignore otherwise.--property-map-file string If specified, output the property map (in JSON format) in the specified file.--path-remapping string Path remapping input for Solc. A semicolon separate list of remappings'prefix=target'--compiler-version string If given, specifies the exact compiler version to use--no-assert If specified execution will not halt when an invariant is violated (only anevent will be emitted).--filter-type string If specified instrumentation will happen only for annotations, whose typesare matching supplied regular expression.--filter-message string If specified instrumentation will happen only for annotations, whose messagesare matching supplied regular expression.--arm When instrumenting files in-place ('--output-mode files') also swap theinstrumented files with the original.--disarm Find all dependencies of the traget that have been swapped with theirinstrumented version (all foo.sol s.t. there is a foo.sol.instrumented andfoo.sol.original) and swap them back for the original.--debug-events When specified for every failure an additional debug event with values ofvariables in the failing predicate is emitted.--user-assert-mode string Describe how scribble signals user assertion failures to Myhtril/Harvey. Mustbe either 'log' or 'mstore'. See wiki for more details.--solFiles string[] List of solidity files to instrument. Either a path to a file, or '--' forstdin.
--output
doesn't have any effect with --output-mode files
.
--utils-output-path
allows to specify a different directory for the helper __scribble_ReentrancyUtils.sol
file. It only works with --output-mode files
. It doesn't have any effect with --output-mode flat
.
If --no-assert
is omitted, then there is an assert(false)
emitted in the instrumented code every time an invariant is violated. For longer-running fuzzing campaigns, it may be useful to keep running the code even after a property is violated. In those cases only an AssertionFailed(string)
event is emitted, which can be caught by tools such as MythX/Mythril/Harvey.
You can't pass standard json with missing sources to scribble
.