veripb 3.0.0

use std::{
    io::BufRead,
    path::{Path, PathBuf},
};

use anyhow::Context;

// NOTE: integration tests that should be ignored (typically because they are known to fail) can be
// marked with the following on the second line of the derivation file:
// <cmt> INTEGRATION-TEST: ignore(<what>)
// where <cmt> is * for version 2 or % for version 3, and <what> is one of check, elaborate, or both.

fn main() {
    let args = libtest_mimic::Arguments::from_args();
    let mut tests = vec![];

    for correct in [true, false] {
        for version in ["version2", "version3"] {
            let ignore_both_string = if version == "version2" {
                "* INTEGRATION-TEST: ignore(both)"
            } else {
                "% INTEGRATION-TEST: ignore(both)"
            };
            for derivation in glob::glob(&format!(
                "./tests/instances/{}/{version}/*.pbp",
                if correct { "correct" } else { "incorrect" }
            ))
            .unwrap()
            .flatten()
            {
                let id = derivation.file_stem().unwrap().to_str().unwrap();
                let mut second_line = String::new();
                let mut reader = std::io::BufReader::new(
                    std::fs::File::open(&derivation).expect("failed to read derivation"),
                );
                reader
                    .read_line(&mut second_line)
                    .expect("failed to read first line of derivation file");
                second_line.clear();
                reader
                    .read_line(&mut second_line)
                    .expect("failed to read second line of derivation file");
                let second_line = second_line;
                for elaborate in [true, false] {
                    let deriv = derivation.clone();
                    let trial = libtest_mimic::Trial::test(
                        format!(
                            "{version}::{id} ({} - expected {})",
                            if elaborate { "elaborate" } else { "check" },
                            if correct { "correct" } else { "incorrect" }
                        ),
                        move || {
                            run_test(deriv, correct, elaborate).map_err(|e| format!("{e:#}").into())
                        },
                    );
                    // If the test is known-bad, ignore it
                    let ignored = second_line.trim() == ignore_both_string
                        || second_line.trim()
                            == format!(
                                "{} INTEGRATION-TEST: ignore({})",
                                if version == "version2" { "*" } else { "%" },
                                if elaborate { "elaborate" } else { "check" }
                            );
                    tests.push(trial.with_ignored_flag(ignored));
                }
            }
        }
    }

    libtest_mimic::run(&args, tests).exit();
}

fn run_test<P>(derivation: P, correct: bool, elaborate: bool) -> anyhow::Result<()>
where
    P: AsRef<Path>,
{
    // Temporary kernel file if elaborating
    // This is automatically deleted when `kernel_proof` is dropped
    let kernel_proof = if elaborate {
        Some(tempfile::NamedTempFile::new().expect("failed to create temporary kernel proof file"))
    } else {
        None
    };

    let formula = derivation.as_ref().with_extension("opb");
    let output_formula = derivation.as_ref().with_extension("outopb");
    let output_formula = if output_formula.exists() {
        Some(output_formula)
    } else {
        None
    };
    let res = run_veripb(
        formula.clone(),
        derivation.as_ref().to_path_buf(),
        output_formula.clone(),
        kernel_proof
            .as_ref()
            .map(|kernel| kernel.path().to_path_buf()),
    );

    verify_veripb_result(res, correct).with_context(|| {
        format!(
            "{} proof yielded unexpected result",
            if elaborate { "elaborating" } else { "checking" }
        )
    })?;

    if let Some(kernel_proof) = kernel_proof {
        assert!(elaborate);
        if correct {
            test_elaborated_proof(formula, kernel_proof.path().to_path_buf(), output_formula)?;
        }
    } else {
        assert!(!elaborate);
    }

    Ok(())
}

fn test_elaborated_proof(
    formula: PathBuf,
    kernel_proof: PathBuf,
    output_formula: Option<PathBuf>,
) -> anyhow::Result<()> {
    // Run VeriPB on the kernel proof
    let res = run_veripb(
        formula.clone(),
        kernel_proof.clone(),
        output_formula.clone(),
        None,
    );

    verify_veripb_result(res, true).context("checking kernel proof yielded unexpected result")?;

    // TODO: Enable testing against CakePB as soon as CakePB is updated.
    // // Run kernel proof through formally verified checker.
    // let mut cake_pb = std::process::Command::new("cake_pb");
    // cake_pb.args([formula.to_str().unwrap(), kernel_proof.to_str().unwrap()]);
    // match cake_pb.output() {
    //     Ok(o) => {
    //         anyhow::ensure!(
    //             o.stderr.is_empty(),
    //             format!(
    //                 "checking kernel proof with CakePB yielded unexpected result:\n\t{}",
    //                 String::from_utf8(o.stderr).unwrap(),
    //             )
    //         );
    //     }
    //     // Handle errors with running CakePB, like CakePB not being installed.
    //     Err(err) => match err.kind() {
    //         std::io::ErrorKind::NotFound => {}
    //         _ => return Err(err).context("failed to run CakePB"),
    //     },
    // }

    Ok(())
}

fn verify_veripb_result(result: anyhow::Result<()>, expected_correct: bool) -> anyhow::Result<()> {
    if expected_correct {
        result?;
        Ok(())
    } else {
        let Err(err) = result else {
            anyhow::bail!("expected proof to be incorrect, but VeriPB returned no error");
        };
        // List of "good" errors for incorrect instances
        let Err(err) = err.downcast::<veripb::error::VeriPBError>() else {
            return Ok(());
        };
        let Err(err) = err.downcast::<veripb::error::CheckingError>() else {
            return Ok(());
        };
        let Err(err) = err.downcast::<veripb::elaborator::ElaborationError>() else {
            return Ok(());
        };
        let Err(err) = err.downcast::<veripb_propagator::error::PropagatorError>() else {
            return Ok(());
        };
        let Err(err) = err.downcast::<veripb_parser::error::ParserError>() else {
            return Ok(());
        };
        Err(err)
    }
}

fn run_veripb(
    formula: PathBuf,
    derivation: PathBuf,
    output_formula: Option<PathBuf>,
    kernel_proof: Option<PathBuf>,
) -> anyhow::Result<()> {
    let args = veripb::args::Args {
        formula,
        derivation,
        output_formula,
        elaborate: kernel_proof,
        print_verification_result: false,
        force_checked_deletion: true,
        ..Default::default()
    };
    veripb::run_checker(args)
}