Using Gambit with the Prover
This is the mutation verifier which checks that variants of the original solidity program do not pass the specification. It uses mutations from the Gambit mutation generator. It also allows users to include manually generated mutants. If a mutated program passes the specification, it may indicate that the specification is vacuous or not rigorous enough. In the rest of the document, we refer to both the mutation generator and the verifier as Gambit.
Installations and Setup
To use the mutation verifier,
you will need to install the Certora Prover and its dependencies.
Mutation verification currently requires
the alpha-master
version of the Certora CLI.
To install it, run
pip install certora-cli-alpha-master
If you already have certora-cli-alpha-master
installed and
the mutationTest
command is not available,
you may need to update to a newer version by running
pip install --upgrade certora-cli-alpha-master
Running the Mutation Verifier
You will need to update your certora-cli-alpha-master
installation using pip
to get the relevant
dependencies. Then you can run Gambit from the command line:
mutationTest path/to/config/file/Example.conf
Configuration
The tool expects a configuration file (extension .conf
is required).
which is a JSON object.
Here is an example configuration file:
{
"project_folder" : "Test/10Power",
"run_script" : "Test/10Power/runDefault.sh",
"gambit" : {
"filename" : "Test/10Power/TenPower.sol",
"solc" : "solc8.10"
},
"staging" : "master",
"manual_mutations" : {
"path/to/original/file.sol" : "path/to/manual/mutations/",
"...": "..."
},
"...": "..."
}
Note: This configuration is separate from the Prover’s .conf
file and also from the
configuration file of the mutation generator (Running Gambit Through a Configuration File).
Importantly, notice that to use this tool, you can embed the configuration
for generating the mutants in this .conf
file; you don’t need to write
two separate configurations.
Required Keys for the JSON Configuration File:
"project_directory"
: the directory containing the original Prover project on which to perform mutation testing"run_script"
: the bash script used to run verification on the original project, usuallyproject_directory/run.sh
or similar. Gambit will pull the configuration forcertoraRun
from this shell script and verify each mutant using this configuration."gambit"
: the JSON configuration element for invoking Gambit. May be a path to a gambit configuration file or the explicit JSON element contained therein. See Running Gambit Through a Configuration File for more information about the gambit configuration. Thesolc
specific arguments (including the version of the compiler) should be provided here even if they are present in therun_script
.
Optional Keys for the JSON Configuration File
"num_threads"
: the maximum number of threads to use for verification, as an integer"manual_mutations"
: optionally supplement the random mutant generation with your own manually-written mutants. Expects a JSON object whose keys are the paths to the original files and whose values are paths to directories containing manually-written mutants as.sol
files.
Note
Any manual mutations files provided must follow the naming
convention
OriginalFileName.<unique-name>.sol
, where <unique-name>
is a string ID unique with respect to the other
manual mutants (for example you might name them OriginalFileName.m1.sol
, OriginalFileName.m2.sol
and so on).
Additional Optional Flags
Note
Gambit supports --staging [branch] and --cloud.
However, Gambit currently has trouble with --send_only in the run scripts. If you have this flag, please remove it for now. Apologies for the temporary inconvenience!
"offline"
: run mutation testing without internet connection, skipping the UI output and other web functions. Expects a boolean and defaults tofalse
."staging"
: if your run script does not already have--staging
, you can also add it to Gambit. Similar to the Prover, you can provide the branch name for running mutant verification on--staging
. We support"staging" : true
as an alternative to"staging" : "master"
. Omitting this key will cause verification to run locally (unless the run script has it)."cloud"
: if you instead want to run on the cloud environment you can provide the--cloud
flag. You can also add the name of a specific branch."use_cli_certora_run"
: Use CLIcertoraRun
rather thancertoraRun.py
. Expects a boolean and defaults tofalse
.
Visualization
The mutation verification results are summarized in an user-friendly visualization. Here is an example summary for the Borda example. Rules are represented by the green outer circles and the mutants are represented by the gray dots. Selecting a rule shows which mutants it detected and selecting a mutant shows which rules detected it. The coverage metric is computed as the fraction of total generated mutants that were detected. Clicking on a mutant’s patch also shows the diff with respect to the original program.