# Chimera

**Repository Path**: merlin7/chimera

## Basic Information

- **Project Name**: Chimera
- **Description**: A fuzz testing tool for SMT solvers
- **Primary Language**: Python
- **License**: Not specified
- **Default Branch**: asplos-artifact
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2023-12-19
- **Last Updated**: 2025-12-25

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# once4all

`once4all` is a fuzzing tool for SMT solvers (such as Z3 and CVC5) that utilizes LLM-synthesized generators to detect bugs. It supports both mutation-based fuzzing from seed formulas and standalone formula generation.

## Requirements
- Python 3.8+
- SMT solvers you want to test (e.g., Z3, CVC5)
- Python packages: `antlr4-python3-runtime==4.9.2`

### Installation
Install the required Python dependencies:
```bash
pip install antlr4-python3-runtime==4.9.2
```

## Usage

Run the tool from the repository root:

```bash
python3 once4all.py \
  --solver1 z3 --solverbin1 /path/to/z3 \
  --solver2 cvc5 --solverbin2 /path/to/cvc5 \
  --bugs ./bug_triggering_formulas \
  --option default
```

### Modes

**1. Mutation Mode (Default)**
Mutates existing SMT-LIB v2 formulas found in the specified bugs directory.

**2. Standalone Mode**
Generates formulas from scratch using the generators without seed files.
```bash
python3 once4all.py --standalone ...
```

## CLI Options

| Option | Description |
|--------|-------------|
| `--solver1` / `--solverbin1` | Name and binary path of the first solver (e.g., `z3`, `/usr/bin/z3`). |
| `--solver2` / `--solverbin2` | Name and binary path of the second solver. |
| `--bugs` | Directory containing seed SMT-LIB v2 formulas (default: `bug_triggering_formulas/`). |
| `--option` | Solver options mode: `default`, `regular`, or `comprehensive`. |
| `--processes` | Number of parallel processes to use (defaults to CPU count). |
| `--temp` | Temporary directory for solver output (default: `./temp/`). |
| `--generator_path` | Path to a custom directory containing generators. |
| `--standalone` | Run in standalone generation mode (no seed files required). |

## Output

The tool creates a timestamped directory for each run (e.g., `YYYY-MM-DD-HH-MM-SS/`) containing intermediate files.

Triaged bugs are stored in the `temp/` directory:
- `temp/crash/<N>/`: Solver crashes.
- `temp/InvalidModel/<N>/`: Invalid model bugs.
- `temp/soundness/<N>/`: Soundness bugs (disagreements between solvers).

Each folder contains the bug-triggering `.smt2` file and an `error_logs.txt` with details.

## Reproducing Experiments

To reproduce the code coverage experiments, use the `evaluation/reproduce_experiments.py` script. This script automates the process of running various fuzzers (including `once4all`) and collecting code coverage data.

### Usage

```bash
python3 evaluation/reproduce_experiments.py [options]
```

### Common Options

| Option | Description | Default |
|--------|-------------|---------|
| `--time-budget` | Time budget in seconds per run | 3600 (1 hour) |
| `--runs` | Number of runs per fuzzer | 1 |
| `--cores` | Number of cores to use | 1 |
| `--fuzzers` | List of fuzzers to evaluate (e.g., `once4all`, `histfuzz`) | `once4all`, `histfuzz`, `yinyang`, `opfuzz`, `typefuzz` |
| `--ablation` | Run ablation study (Once4All standalone mode) | False |
| `--output-dir` | Directory to store results | `./experiment_results` |
| `--z3-path` | Path to Z3 binary | Auto-detected or `z3` |
| `--cvc5-path` | Path to CVC5 binary | Auto-detected or `cvc5` |

### Example

Run the experiments and save results to `results/`:

```bash
python3 evaluation/reproduce_experiments.py  --output-dir ./results
```

**Note:** To collect coverage data, you must provide the build directories for Z3 and CVC5 using `--z3-build-dir` and `--cvc5-build-dir` if they are not in the default Docker locations.