fuzz-d

fuzz-d is a random program generator for the Dafny language, intended for fuzzing the Dafny compiler in order to find miscompilation bugs and crashes across its backends. This repository contains the source code for the generator, as well as information for installing and using it.

Dependencies

• Building fuzz-d from source requires Java version 19. More information about installing JDK19 is available on the OpenJDK website.
• Running programs generated by fuzz-d requires a working dafny executable, with all backend dependencies. Information about installing Dafny and its dependencies is available on the dafny-lang GitHub repository.

Build from Source

git clone --recurse-submodules git@github.com:fuzz-d/fuzz-d.git
cd fuzz-d
./gradlew build

This will create an executable jar in app/build/libs - this can be invoked using the command java -jar app/build/libs/app.jar.

Usage

fuzz-d has four available commands:

• fuzz - for generating programs and (optionally) running differential testing over the backends on the program.
• verifuzz - for generating verifiable programs and testing these on the verifier.
• interpret - using the in-built interpreter to run a Dafny program and generate an output.
• recondition - annotate a given Dafny program with mechanisms to ensure runtime safety.

The interpret and recondition commands are built for use with programs generated by fuzz-d, but may work on other Dafny programs with limited success.

Usage for Fuzzing

Usage: fuzzd fuzz options_list
Options:
    --seed, -s LONG     Generation Seed
    --verifier, -v      Generate annotated programs, used in testing both the verifier and the compilers
    --advanced, -a      Use advanced reconditioning to reduce use of safety wrappers
    --instrument, -i    Instrument control flow with print statements for debugging program paths
    --swarm, -sw        Run with swarm testing enabled
    --noRun, -n         Generate a program without running differential testing on it
    --help, -h          Usage info
    --output, -o        Directory for output (Path)

Usage for Verifier Fuzzing

Usage: fuzzd verifuzz options_list
Options: 
    --seed, -s LONG     Generation Seed
    --noRun, -n         Generate a program without running differential testing on it 
    --output, -o        Directory for output (Path)

Usage for Interpreting

Usage: fuzzd interpret options_list
Arguments:
    file -> path to .dfy file to interpret { String }
Options:
    --help, -h -> Usage info

Usage for Reconditioning

Usage: fuzzd recondition options_list
Arguments: 
    file -> path to .dfy file to recondition
Options: 
    --advanced, -a     Use advanced reconditioning to reduce use of safety wrappers 
    --help, -h         Usage info