|
| 1 | +# Mutation testing using Certora's Gambit framework |
| 2 | + |
| 3 | +[Gambit tool](https://docs.certora.com/en/latest/docs/gambit/gambit.html) takes Solidity file or list of files as input and it will generate "mutants" as output. Those are copies of original file, but each with an atomic modification of original file, ie. flipped operator, mutated 'if' condition etc. Next step is running the test suite against the mutant. If all tests still pass, mutant survived, that's bad - either there's faulty test or there is missing coverage. If some test(s) fail, mutant's been killed, that's good. |
| 4 | + |
| 5 | +## How to install Gambit |
| 6 | +To build from source (assumes Rust and Cargo are installed), clone the Gambit repo |
| 7 | +``` |
| 8 | +git clone git@github.com:Certora/gambit.git |
| 9 | +``` |
| 10 | + |
| 11 | +Then run |
| 12 | +``` |
| 13 | +cargo install --path . |
| 14 | +``` |
| 15 | + |
| 16 | +Alternatively, prebuilt binaries can be used - more info [here](https://docs.certora.com/en/latest/docs/gambit/gambit.html#installation). |
| 17 | + |
| 18 | + |
| 19 | +## Using Gambit |
| 20 | +CLI command `gambit mutate` is used to generated mutants. It can take single file as an input, ie. let's say we want to generate mutants for file `L1ERC20Gateway.sol`: |
| 21 | +``` |
| 22 | +gambit mutate --solc_remappings "@openzeppelin=node_modules/@openzeppelin" "@arbitrum=node_modules/@arbitrum" -f contracts/tokenbridge/ethereum/gateway/L1ERC20Gateway.sol |
| 23 | +``` |
| 24 | + |
| 25 | +Command will output `gambit_out` folder containing list of mutants (modified Solidity files) and `gambit_results.json` which contains info about all the generated mutants. Another way to view the mutant info is to run: |
| 26 | +``` |
| 27 | +gambit summary |
| 28 | +``` |
| 29 | + |
| 30 | +Gambit can also take set of Solidity files as input in JSON format, ie: |
| 31 | +``` |
| 32 | +gambit mutate --json test-mutation/config.json |
| 33 | +``` |
| 34 | + |
| 35 | +List of all configuration options for the JSON file can be found [here](https://docs.certora.com/en/latest/docs/gambit/gambit.html#configuration-files). |
| 36 | + |
| 37 | +Gambit only generates the mutants, it will not execute any tests. To check if mutant gets killed or survives, we need to copy modified Solidity file over the original one, re-compile the project and re-run the test suite. This process has been automated and described in next chapter. |
| 38 | + |
| 39 | +## Gambit integration with Foundry |
| 40 | +To get the most benefits from Gambit, we have integrated it with Foundry and automated testing and reporting process. This is how `gambitTester` script works: |
| 41 | +- generates mutants for files specified in test-mutation/config.json |
| 42 | +- for each mutant do in parallel (in batches): |
| 43 | + - replace original file with mutant |
| 44 | + - re-compile and run foundry suite |
| 45 | + - track results |
| 46 | +- report results |
| 47 | + |
| 48 | +Here are practical steps to run mutation test over the set of Arbitrum token bridge contracts. First we need to update `test-mutation/config.json` with the list of solidity files to be tested. In this case we use config file that was prepared in advance: |
| 49 | +``` |
| 50 | +cp test-mutation/all-configs/config.tokenbridge-ethereum.json test-mutation/config.json |
| 51 | +``` |
| 52 | + |
| 53 | +Now run the script, it will generate mutants and start compiling/testing them in parallel: |
| 54 | +``` |
| 55 | +yarn run test:mutation |
| 56 | +``` |
| 57 | + |
| 58 | +It will take some time for script to execute (depends on the underlying HW). |
| 59 | + |
| 60 | +Script output looks like this: |
| 61 | +``` |
| 62 | +❯ yarn run test:mutation |
| 63 | +
|
| 64 | +yarn run v1.22.19 |
| 65 | +$ ts-node test-mutation/gambitTester.ts |
| 66 | +====== Generating mutants |
| 67 | +Generated 209 mutants in gambit_out/ |
| 68 | +
|
| 69 | +====== Test mutants |
| 70 | +Testing mutant batch 0..7 |
| 71 | +Testing mutant batch 7..14 |
| 72 | +Testing mutant batch 14..21 |
| 73 | +Testing mutant batch 21..28 |
| 74 | +Testing mutant batch 28..35 |
| 75 | +Testing mutant batch 35..42 |
| 76 | +Testing mutant batch 42..49 |
| 77 | +Testing mutant batch 49..56 |
| 78 | +Testing mutant batch 56..63 |
| 79 | +Testing mutant batch 63..70 |
| 80 | +Testing mutant batch 70..77 |
| 81 | +Testing mutant batch 77..84 |
| 82 | +Testing mutant batch 84..91 |
| 83 | +Testing mutant batch 91..98 |
| 84 | +Testing mutant batch 98..105 |
| 85 | +Testing mutant batch 105..112 |
| 86 | +Testing mutant batch 112..119 |
| 87 | +Testing mutant batch 119..126 |
| 88 | +Testing mutant batch 126..133 |
| 89 | +Testing mutant batch 133..140 |
| 90 | +Testing mutant batch 140..147 |
| 91 | +Testing mutant batch 147..154 |
| 92 | +Testing mutant batch 154..161 |
| 93 | +Testing mutant batch 161..168 |
| 94 | +Testing mutant batch 168..175 |
| 95 | +Testing mutant batch 175..182 |
| 96 | +Testing mutant batch 182..189 |
| 97 | +Testing mutant batch 189..196 |
| 98 | +Testing mutant batch 196..203 |
| 99 | +Testing mutant batch 203..210 |
| 100 | +
|
| 101 | +====== Results |
| 102 | +
|
| 103 | +Mutant ID | File Name | Status |
| 104 | +---------------------------------------------- |
| 105 | +---------------------------------------------- |
| 106 | +1 | L1ArbitrumMessenger.sol | SURVIVED |
| 107 | +2 | L1ArbitrumMessenger.sol | SURVIVED |
| 108 | +3 | L1ArbitrumMessenger.sol | KILLED |
| 109 | +---------------------------------------------- |
| 110 | +4 | L1ArbitrumExtendedGateway.sol | KILLED |
| 111 | +5 | L1ArbitrumExtendedGateway.sol | KILLED |
| 112 | +6 | L1ArbitrumExtendedGateway.sol | KILLED |
| 113 | +7 | L1ArbitrumExtendedGateway.sol | KILLED |
| 114 | +8 | L1ArbitrumExtendedGateway.sol | KILLED |
| 115 | +9 | L1ArbitrumExtendedGateway.sol | KILLED |
| 116 | +10 | L1ArbitrumExtendedGateway.sol | KILLED |
| 117 | +11 | L1ArbitrumExtendedGateway.sol | KILLED |
| 118 | +
|
| 119 | +... |
| 120 | +
|
| 121 | +205 | L1WethGateway.sol | SURVIVED |
| 122 | +206 | L1WethGateway.sol | SURVIVED |
| 123 | +207 | L1WethGateway.sol | SURVIVED |
| 124 | +208 | L1WethGateway.sol | SURVIVED |
| 125 | +209 | L1WethGateway.sol | SURVIVED |
| 126 | +---------------------------------------------- |
| 127 | +Total Mutants: 209 |
| 128 | +Killed: 133 (63.64%) |
| 129 | +Survived: 76 (36.36%) |
| 130 | +
|
| 131 | +====== Done in 20.91 min |
| 132 | +``` |
| 133 | + |
| 134 | +We're insterested to analyze the mutants which survived. The 1st column in output, `Mutant ID`, can be used to find the exact mutation that was applied by looking into the matching entry in the `gambit_results.json` file. |
| 135 | + |
| 136 | +## Other considerations |
| 137 | +Mutation testing script is time-intensive due to all the re-compiling work. For that reason, list of input files should be optimized to give the most benefit for the limited time period available for testing. Ie. single Solidity files can be targeted and tested manually, and the broader scope of files can be tested overnight. |
| 138 | + |
| 139 | +Other params that can be adjusted are type of mutations to use, number of mutants to be generated, randomness seed to use in generation, etc. |
| 140 | + |
0 commit comments