Generating Mutations

This is a mutation generator for Solidity. It takes as input a Solidity source file (or a configuration file as you can see below) and produces a set of uniquely mutated Solidity source files which are output in the out/ directory by default. In addition to the mutated source files, Gambit also produces a JSON report of the mutants produced, which can be found in out/results.json. The source is publicly available.

Installing Gambit

• Gambit is implemented in Rust, which you can download here.

• To run Gambit, do the following:

  • git clone git@github.com:Certora/gambit.git

  • Install by running cargo install --path . from the gambit/ directory after you clone the repository. This will add the Gambit binary to your .cargo directory.

  • If you prefer to run Gambit without installing, you can also build it by running cargo build --release from the gambit/ directory.

• You will need OS specific binaries for various versions of Solidity. The version of the binary will depend on your Solidity project. You can download them here. Make sure you add them to your PATH.

Usage

• If you installed Gambit using cargo install --path . described above, you can learn how to use Gambit by running gambit mutate -h.

• If you went for a local build, you can run cargo gambit-help for help.

• You can print log messages by setting the environment variable RUST_LOG (e.g., RUST_LOG=info cargo gambit ...). This will show colored diffs of the mutants on your standard output.

cargo gambit-help will show you the following message that lists all the command line arguments that Gambit accepts. Some of the simple arguments are num-mutants (default 5) which lets you control the number of mutants you want to generate, the seed (default 0) that controls the randomization of the generated mutants, and outdir (default out) that lets you choose where you want to output the mutant files.

Command line arguments for running Gambit. Following are the main ways to run it.

1. cargo gambit path/to/file.sol: this will apply all mutations to file.sol.

2. cargo run --release -- mutate -f path/to/file1.sol -f path/to/file2.sol: this will apply all mutations to file1.sol and file2.sol.

3. cargo gambit-cfg path/to/config.json: this gives the user finer control on what functions in which files, contracts to mutate using which types of mutations.

Usage: gambit mutate [OPTIONS]

Options:
  -j, --json <JSON>
          Json file with config

  -f, --filename <FILENAME>
          File to mutate

  -n, --num-mutants <NUM_MUTANTS>
          Number of mutants
          [default: 5]

  -o, --outdir <OUTDIR>
          Directory to store all mutants
          [default: out]

  -s, --seed <SEED>
          Seed for random number generator
          [default: 0]

      --solc <SOLC>
          Solidity binary name, e.g., --solc solc8.10, --solc 7.5, etc
          [default: solc]

      --solc-basepath <SOLC_BASEPATH>
          Basepath argument to solc

      --solc-allowpaths <SOLC_ALLOWPATHS>
          Allowpath argument to solc

      --solc-remapping <SOLC_REMAPPING>
          Solidity remappings

  -h, --help
          Print help (see a summary with '-h')

These flags are explained in the following section.

Examples of How to Run Gambit

You can run Gambit on a single Solidity file with various additional arguments. Gambit also accepts a configuration file as input where you can specify which files you want to mutate and using which mutations. You can also control which functions and contracts you want to mutate. Configuration files are the recommended way to use Gambit.

Running Gambit on a Single Solidity File

We recommend this approach only when you have a simple project with few files and no complex dependencies or mutation requirements.

• cargo gambit benchmarks/RequireMutation/RequireExample.sol is an example of how to run with a single Solidity file.

• For projects that have complex dependencies and imports, you will likely need to:

  • To specify the Solidity base path, pass the --base-path argument. For example

    cargo gambit path/to/file.sol --solc-basepath base/path/dir/.
    

  • To indicate where Solidity should find libraries, you provide an import remapping to solc using the --solc-remapping argument. For example:

    cargo gambit path/to/file.sol \
      --solc-remapping @openzepplin=node_modules/@openzeppelin \
      --solc-remapping ...
    

  • To include additional allowed paths, you provide Solidity’s allowed paths to solc using the --allow-paths argument. For example:

    cargo gambit path/to/file.sol --solc-allowpaths @openzepplin=... --solc-allowpaths ...
    

Running Gambit Through a Configuration File

This is the recommended way to run Gambit. This approach allows you to control and localize mutation generation and is easier to use than passing many command line flags.

To run gambit with a configuration file, simply pass the name of the json file:

cargo gambit-cfg benchmarks/config-jsons/test1.json

The configuration file is a json file containing the command line arguments for gambit and additional configuration options. For example, the following configuration is equivalent to gambit benchmarks/10Power/TenPower.sol --solc-remapping @openzepplin=node_modules/@openzeppelin:

{
    "filename": "benchmarks/10Power/TenPower.sol",
    "remappings": [
        "@openzeppelin=node_modules/@openzeppelin"
    ]
}

In addition to specifying the command line arguments, you can list the specific types of mutations that you want to apply, the specific functions you wish to mutate, and more. See Running Gambit Through a Configuration File for more details, and the benchmark/config-jsons directory for examples.

Configuring the Set of Mutations, Functions, and Contracts

If you are using Gambit through a configuration file, you can localize the mutations to some functions and contracts. You can also choose which mutations you want (see Mutation Types for the list of possible mutations). Here is an example that shows how to configure these options.

[
    {
        "filename": "Foo.sol",
        "contract": "C",
        "functions": ["bar", "baz"],
        "solc": "solc8.12"
    },
    {
        "filename": "Blip.sol",
        "contract": "D",
        "functions": ["bang"],
        "solc": "solc8.12"
        "mutations": [
          "binary-op-mutation",
          "swap-arguments-operator-mutation"
        ]
    }
]

This configuration file will perform all mutations on Foo.sol’s functions bar and baz in the contract C, and only binary-op-mutation and swap-arguments-operator-mutation mutations on the function bang in the contract D. Both will compile using the Solidity compiler version solc8.12.

Output of Gambit

Gambit produces a set of uniquely mutated Solidity source files which are, by default, dumped in the out/ directory. Each mutant file has a comment that describes the exact mutation that was done. For example, one of the mutant files for benchmarks/10Power/TenPower.sol that Gambit generated contains:

/// SwapArgumentsOperatorMutation of: uint256 res = a ** decimals;
uint256 res = decimals ** a;

Also included in the out/ directory is a JSON summary of all mutants produced, out/results.json. The results include the filename and a unique string ID of each mutant, along with a brief description and the diff between the mutant and the original file. For example,

[
  {
    "description": "<brief summary of mutant>",
    "diff": "<stdout of `diff` command on the mutant and original file>",
    "id": "0",
    "name": "out/path/to/mutant.sol"
  },
  "..."
]

Mutation Types

At the moment, Gambit implements the following types of mutations, detailed below:

Many of these mutations may lead to invalid mutants that do not compile. At the moment, Gambit simply compiles the mutants and only keeps valid ones — we are working on using additional type information to reduce the generation of invalid mutants by constructions.

Gambit does not apply any mutations to libraries unless they are explicitly passed as arguments.

Change binary operators: binary-op-mutation

Change a binary operator like +, -, < to a different operator. For example:

x = y + z - 8

might become

x = y * z - 8

Change unary operators: unary-operator-mutation

Change a unary operator like ++ or -- to a different operator. For example,

x++

might become

x--

Change require statements: require-mutation

Negate or change the condition. For example,

require (x + y > 6)

might become

require (true)

or

require (!(x + y > 6))

Change assignment statements: assignment-mutation

Change the right hand side of an assignment. For example,

x = true;

might become

x = false

Delete expressions: delete-expression-mutation

Comment out some expression. For example,

for (uint256 i = 0; i < x; i++)

might become

for (uint256 i = 0; i < x; /* i++ */)

Replace function calls: function-call-mutation

Randomly replace a function call with one of its operands. For example,

return foo(x, y)

might become

return y

Change if statements: if-statement-mutation

Change the condition. For example,

if (cond)

might become

if (false)

Swap function arguments: swap-arguments-function-mutation

Swap the arguments to a function. For example,

foo(a, b)

might become

foo(b, a)

Swap operator arguments: swap-arguments-operator-mutation

Swap the operands of a non-commutative binary operator. For example,

a - b

might become

b - a

Swap adjacent lines: swap-lines-mutation

Swap two lines. For example,

x = foo (y, z);
x += 2;

might become

x += 2;
x = foo (y, z);

Eliminate Delegate Call: elim-delegate-mutation

Replace a delegate call by call. For example,

_contract.delegatecall(abi.encodeWithSignature("setVars(uint256)", _num)

might become

_contract.call(abi.encodeWithSignature("setVars(uint256)", _num)