fat32-model

FAT32 filesystem image and test program generator based on the DepTyCheck property-based testing library for Idris 2.

Building

To use fat32-model you need to install the pack package manager first, which will also install the Idris toolchain. Then run:

pack build

Beware that deriving the generators may take a few hours and a lot of RAM (a minimum of 64 GiB is recommended).

Usage

Use pack run fat32-model to run the generator. The following options are supported:

  -c <size>         --cluster-size=<size>        cluster size in bytes
  -1 <fuel1>        --fuel1=<fuel1>              fuel for the Node generator
  -2 <fuel2>        --fuel2=<fuel2>              fuel for the NameTree generator
  -s <seed>         --seed=<seed>                seed
  -m <minclust>     --minclust=<minclust>        minimum amount of data clusters
  -b <blob-limit>   --blob-limit=<blob-limit>    maximum image generation blob size
  -w <write-limit>  --write-limit=<write-limit>  maximum write operation blob size
  -N                --print-node                 print the generated Node
  -F                --print-fs                   pretty-print the generated filesystem tree
  -C                --print-cmap                 print the generated cluster map
  -I                --image-only                 generate only the image without operations
  -h                --help                       print usage information
  -o <output>       --output=<output>            output image filename

gen-images.py can be used to generate multiple test cases in parallel, as well as to additionally compress images with zstd or convert them to syzlang format:

usage: gen-images.py [-h] [-p PROCS] [--syz] [--ops] [-z] N path

positional arguments:
  N                  number of images
  path               images directory path

options:
  -h, --help         show this help message and exit
  -p, --procs PROCS  process count
  --syz              generate syzkaller seeds
  --ops              generate operations
  -z                 compress images with zstd