CLI Usage

Overview

Scribble accepts normal Solidity files and has 3 output modes:

1. In flat mode, all the dependencies of the target Solidity file(s) are bunched up and emitted as one giant blob of Solidity. This is useful for submitting the instrumented code to services like ` MythX.

2. 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.

3. 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 slightly modified standard JSON output of the used compiler version.

Quick recipes

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;
    }
}

Emitting a flat instrumented file

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

Instrumenting files in-place

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

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 compiled version of the flattened instrumented solidity, along with some extra info. (For more details see this section).

Command line options reference

Scribble

  A Solidity runtime verification tool for property based testing. 

Options

  -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, input      
                                           assumed to be a raw Solidity source code. When 'json' is specified, input     
                                           assumed 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, for   
                                           every file Foo.sol that contains an annotated contract emit a                 
                                           Foo.sol.instrumetned with the instrumented contract. When 'json' is           
                                           specified, a JSON object including the original sources, the flattened        
                                           bytecode, 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 the          
                                           flattened 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.             
  --instrumentation-metadata-file string   If specified, output instrumentation metadata (src-to-src maps, property      
                                           maps) to the specified file.                                                  
  --macro-path string                      Path to look for a macro definition file. If path is a directory, then it     
                                           would be recusively scanned for macro files.                                  
  --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                         
  --compiler-kind string                   If given, specifies the type of Solidity compiler to use. Supported values    
                                           are 'wasm' and 'native'. Default value is 'native' (can be configured via     
                                           environment variable SCRIBBLE_DEFAULT_COMPILER_KIND).                         
  --compiler-settings string               If given, specifies additional settings to pass to the underlying compiler as 
                                           a JSON string. (e.g. --compiler-settings '{"optimizer:": {"enabled":          
                                           true}}'). For more info see https://docs.soliditylang.org/en/latest/using-    
                                           the-compiler.html#input-description                                           
  --no-assert                              If specified execution will not halt when an invariant is violated (only an   
                                           event will be emitted).                                                       
  --filter-type string                     If specified instrumentation will happen only for annotations, whose types    
                                           are matching supplied regular expression.                                     
  --filter-message string                  If specified instrumentation will happen only for annotations, whose messages 
                                           are matching supplied regular expression.                                     
  --arm                                    When instrumenting files in-place ('--output-mode files') also swap the       
                                           instrumented files with the original.                                         
  --disarm                                 Find all dependencies of the target that have been swapped with their         
                                           instrumented version (all foo.sol s.t. there is a foo.sol.instrumented and    
                                           foo.sol.original) and swap them back for the original.                        
  --debug-events                           When specified for every failure an additional debug event with values of     
                                           variables in the failing predicate is emitted.                                
  --user-assert-mode string                Describe how scribble signals user assertion failures to Myhtril/Harvey. Must 
                                           be either 'log' or 'mstore'. See wiki for more details.                       
  --cov-assertions                         When specified emit an extra user-assertion for each property whenever its    
                                           reached. This allows an easy (albeit noisy) way to check which propterties    
                                           were reached.                                                                 
  --solFiles string[]                      List of solidity files to instrument. Either a list of paths to files, or     
                                           '--' for stdin. 

Important caveats

1. --output option doesn't have any effect with --output-mode files.

2. --utils-output-path allows to specify a different directory for the __scribble_ReentrancyUtils.sol file. It only works with --output-mode files. It doesn't have any effect with --output-mode flat.

3. 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 Dili-Faas/MythX/Mythril/Harvey.

4. You will get an error if you pass standard json with missing sources to scribble. Scribble needs the source code to fill in missing information in the AST in certain compiler versions.

5. With the --compiler-kind option you have the choice between using a binary compiler (native) or a WASM based compiler (wasm). If a binary compiler is not available for your environment (e.g. M1 Macs) please use `--compiler-kind wasm`.

6. When instrumenting in-place (i.e. with the option --output-mode files --arm) scribble will always emit an instrumentation metadata file. By default this is placed in the root of the current project tree. The root is defined as the closest directory with a node_modules/ folder in it. If a root folder is not detected, scribble will throw an error requiring you to supply a location for the metadata with the `--instrumentation-metadata-file` option.