# Violation Analyzer Tool

A tool to download Certora Prover run outputs, extract them, and automatically analyze violations using CexAnalyzer.

## Overview

The violation analyzer tool streamlines the process of analyzing counterexamples from Certora Prover runs. It:

1. Extracts the job ID from the URL to use as a unique directory name
2. Checks if the job has already been downloaded (caching)
3. Downloads the run output using `certora_wget.py` with `/zipOutput` (if not cached)
4. Extracts the `out.tar.gz` archive (if not cached)
5. Cleans up by removing the tar.gz file (optional)
6. Parses `Reports/output.json` to identify failed rules
7. Runs CexAnalyzer on specified rule(s)

## Prerequisites

- Python 3.x
- `certora_wget.py` (included in this directory)
- CexAnalyzer script (path must be provided)
- Valid Certora cookies in your browser (Chrome, Firefox, or Safari)

## Installation

No installation required. The script is ready to use from this directory.

```bash
chmod +x analyze_violations.py
```

## Usage

### Basic Syntax

```bash
python3 analyze_violations.py <url> [OPTIONS]
```

### Required Arguments

- `url`: URL of the Certora run (e.g., `https://prover.certora.com/output/12345/abc`)

### Options

- `--cexanalyzer PATH`: Path to CexAnalyzer script (alternative to environment variable)
- `--rule RULE_NAME`: Analyze a specific rule by name
- `--all`: Analyze all failed rules found in the run
- `--keep-tar`: Keep the downloaded tar.gz file (default: delete after extraction)
- `--output-dir DIR`: Directory name for extracted output (default: auto-detected from job ID)

**Note:** You must specify either `--rule` or `--all`, but not both.

## Examples

### Example 1: Analyze a specific rule

```bash
python3 analyze_violations.py https://prover.certora.com/output/12345/abc --rule myRule
```

### Example 2: Analyze all failed rules

```bash
python3 analyze_violations.py https://prover.certora.com/output/12345/abc --all 
```

### Example 3: Keep the downloaded archive

```bash
python3 analyze_violations.py https://prover.certora.com/output/12345/abc --all --keep-tar
```

### Example 4: Use cached data (automatic)

The tool automatically caches downloaded jobs by their ID. Running the same URL twice will skip the download:

```bash
# First run - downloads and extracts
python3 analyze_violations.py https://prover.certora.com/output/60724/abc123def --all

# Second run - uses cached data (no download)
python3 analyze_violations.py https://prover.certora.com/output/60724/abc123def --all
```

Output directory will be: `60724_abc123def/`

### Example 5: Use custom output directory

```bash
python3 analyze_violations.py https://prover.certora.com/output/12345/abc --rule unwindDepositMaintainsBacking --output-dir my_analysis
```

### Example 6: Analyze all rules and save reports

Using `--all` automatically saves all analyses to markdown files:

```bash
python3 analyze_violations.py https://prover.certora.com/output/60724/abc123def --all
```

Output:
```
Found 2 failed rule(s): collateralAccountingConsistency, unwindDepositMaintainsBacking
  collateralAccountingConsistency: 9 failed method(s)
  unwindDepositMaintainsBacking: no specific methods (simple failure)

Running CexAnalyzer...
[Analysis output for each rule/method...]

============================================================
Analysis complete! Created 10 report file(s):
  📄 .certora_internal/violated_rules/collateralAccountingConsistency/CorkPool.withdraw/1730400000_60724_abc123def_1.md
  📄 .certora_internal/violated_rules/collateralAccountingConsistency/CorkPool.redeem/1730400000_60724_abc123def_1.md
  ...
  📄 .certora_internal/violated_rules/unwindDepositMaintainsBacking/1730400000_60724_abc123def_1.md
============================================================
```

### Example 7: Analyze specific rule with multiple methods

When using `--rule` with a rule that has multiple methods, reports are saved:

```bash
python3 analyze_violations.py https://prover.certora.com/output/60724/abc --rule collateralAccountingConsistency
```

Output:
```
Created 9 report file(s):
  📄 .certora_internal/violated_rules/collateralAccountingConsistency/CorkPool.withdraw/1730400000_60724_abc123def_1.md
  ...
```

### Example 8: Analyze specific rule with single method

Single method failures go to console only (no files created):

```bash
python3 analyze_violations.py https://prover.certora.com/output/12345/abc --rule simpleFailureRule
```

Output displayed in console only, no report files created.

## How It Works

### Step 0: Job ID Detection and Caching
- Extracts job ID from URL (format: `{NUMBER}_{HASH}`)
- Example: `https://prover.certora.com/output/60724/abc123def` → job ID: `60724_abc123def`
- Checks if directory `60724_abc123def/Reports/output.json` already exists
- If exists: Skips download and extraction, uses cached data
- If not exists: Proceeds with download

### Step 1: Download (if not cached)
Uses `certora_wget.py` with the `--zip-output` flag to convert the URL from `/output` to `/zipOutput` and download the compressed archive.

### Step 2: Extract (if not cached)
Extracts the `out.tar.gz` file to the job-specific directory (e.g., `60724_abc123def/`).

### Step 3: Cleanup
Removes the `out.tar.gz` file unless `--keep-tar` is specified.

### Step 4: Parse Failed Rules
Reads `Reports/output.json` and identifies rules with "FAIL" status. The tool supports two formats:

**Simple format:**
```json
{
  "rules": {
    "envfreeFuncsStaticCheck": {
      "SUCCESS": [...]
    },
    "unwindDepositMaintainsBacking": "FAIL"
  }
}
```

**Nested format with specific methods:**
```json
{
  "rules": {
    "collateralAccountingConsistency": {
      "Induction step: after external methods": {
        "Using general requirements": {
          "FAIL": [
            "CorkPool.withdraw(bytes32,uint256,address,address)",
            "CorkPool.redeem(bytes32,uint256,address,address)"
          ],
          "SUCCESS": [...]
        }
      }
    }
  }
}
```

The tool recursively searches for "FAIL" keys and extracts the associated method names when available.

### Step 5: Run CexAnalyzer
Executes CexAnalyzer for each failed rule (or the specified rule).
Uses `--quiet` option.

The tool automatically detects which format is used and runs CexAnalyzer appropriately. For rules with multiple failed methods, it runs CexAnalyzer separately for each method.

## Report File Generation

The tool automatically saves CexAnalyzer output to markdown files for easier tracking and comparison:

### When Reports Are Created

**`--all` mode:**
- Reports are ALWAYS created for every analyzed rule
- Each analysis is saved to a timestamped markdown file

**`--rule` mode:**
- Reports are created ONLY when the rule has multiple violated methods
- Single method or simple failures go to console only

### Report File Naming

Files are named with the pattern: `{UNIX_TIMESTAMP}_{JOB_ID}_{SERIAL}.md`

- **UNIX_TIMESTAMP**: When the analysis was performed (e.g., `1730400000`)
- **JOB_ID**: The job identifier from the URL (e.g., `60724_abc123def`)
- **SERIAL**: Sequential number to prevent collisions (1, 2, 3, ...)

Example: `1730400000_60724_abc123def_1.md`

### Report Directory Structure

**For rules with specific methods:**
```
.certora_internal/
  violated_rules/
    {RULE_NAME}/
      {METHOD_NAME_NO_ARGS}/
        {TIMESTAMP}_{JOB_ID}_{SERIAL}.md
```

Example:
```
.certora_internal/
  violated_rules/
    collateralAccountingConsistency/
      CorkPool.withdraw/
        1730400000_60724_abc123def_1.md
        1730400100_60724_abc123def_2.md
      CorkPool.redeem/
        1730400000_60724_abc123def_1.md
```

**For simple failures (no specific methods):**
```
.certora_internal/
  violated_rules/
    {RULE_NAME}/
      {TIMESTAMP}_{JOB_ID}_{SERIAL}.md
```

Example:
```
.certora_internal/
  violated_rules/
    unwindDepositMaintainsBacking/
      1730400000_60724_abc123def_1.md
      1730400200_60724_abc123def_2.md
```

### Report File Format

Each markdown file contains:
```markdown
# CexAnalyzer Report

**Rule:** ruleName
**Method:** ContractName.methodName(args) [if applicable]
**Job ID:** 60724_abc123def
**Generated:** 2024-10-31T12:00:00

---

[CexAnalyzer output here...]
```

### Benefits of Report Files

- **Historical tracking**: Compare analyses over time using timestamps
- **Organized by context**: Easy to find all failures for a specific rule/method
- **Serial numbers**: Handles method overloading gracefully
- **Portable**: Markdown format is readable anywhere
- **Version control friendly**: Text-based format works well with git

## Features

- **Automatic report generation**: Saves CexAnalyzer output to timestamped markdown files
- **Progress tracking**: Each analysis is saved with timestamp for historical comparison
- **Smart file organization**: Reports organized by rule name and method name
- **Automatic caching**: Downloads are cached by job ID - rerunning the same URL skips download
- **Job ID-based organization**: Each job is stored in its own directory (format: `{NUMBER}_{HASH}`)
- **Automatic cookie handling**: Uses `certora_wget.py` to automatically extract browser cookies
- **Smart rule detection**: Parses output.json to find all failed rules in multiple formats
- **Method-specific analysis**: Automatically detects and analyzes specific methods that caused failures
- **Batch analysis**: Analyze all violations in a single command with `--all`
- **Flexible configuration**: Support for both environment variables and command-line arguments
- **Clean workspace**: Automatically removes temporary files
- **Clear progress output**: Shows each step of the process with detailed failure information
- **Error handling**: Provides clear error messages for common issues
- **Recursive failure detection**: Handles deeply nested output.json structures

## Troubleshooting

### Error: "CexAnalyzer path not specified"
Set the `CEXANALYZER_PATH` environment variable or use the `--cexanalyzer` flag.

### Error: "certora_wget.py not found"
Ensure you're running the script from the correct directory or that `certora_wget.py` is in the same directory.

### Error: "Could not find a complete set of certora cookies"
Make sure you're logged into https://prover.certora.com in one of your browsers (Chrome, Firefox, or Safari).

### Error: "output.json not found at expected location"
The extracted archive may have a different structure. Check the contents of the extracted directory.

## Dependencies

### certora_wget.py
This tool depends on `certora_wget.py` which handles:
- Browser cookie extraction (Chrome, Firefox, Safari)
- Authenticated downloads from prover.certora.com
- URL transformation (`/output` to `/zipOutput`)

### Python Modules
- `sys`, `os`, `argparse` (standard library)
- `subprocess`, `json` (standard library)
- `tarfile`, `shutil` (standard library)
- `pathlib`, `typing` (standard library)

No additional packages required beyond Python 3's standard library.

## License

This tool is provided as-is for use with Certora Prover.
