rapx 0.7.64

//! Diagnostics and summaries for the staged verifier pipeline.
//!
//! The driver and later checking stages report their per-path property results
//! through the types in this module.  Keeping these types here leaves the driver
//! focused on orchestration.

use rustc_hir::def_id::DefId;

use super::contract::Property;
use crate::verify::checkpoint::CheckpointLocation;

pub(crate) const PATH_LIMIT_DESCRIPTION: &str = "[not enumerated: path limit reached]";

/// Why a [`CheckResult::Unknown`] could not be discharged.
///
/// Carried by the `Unknown` variant so the report can identify incomplete proofs.
#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) enum UnknownReason {
    SmtUnknown(String),
    /// The inline recursion limit was reached, so the callee's body was not
    /// executed and the memory state is incomplete.
    InlineDepthExceeded,
    UnsupportedMir,
    IncompleteInlineBranch,
    UnmodeledIntrinsic,
    UnresolvedUnsafeCall,
    MissingContract,
    UnsupportedProperty,
    /// A checker cannot resolve a value or supported property shape.
    Unimplemented,
    Multiple(Vec<UnknownReason>),
}

impl UnknownReason {
    pub(crate) fn from_solver(solver: &z3::Solver<'_>) -> Self {
        Self::SmtUnknown(
            solver
                .get_reason_unknown()
                .unwrap_or_else(|| "reason unavailable".to_string()),
        )
    }

    fn description(&self) -> String {
        match self {
            Self::SmtUnknown(reason) if reason == "timeout" => "timeout".to_string(),
            Self::SmtUnknown(reason) => format!("SMT: {reason}"),
            Self::InlineDepthExceeded => "inline depth".to_string(),
            Self::UnsupportedMir => "unsupported MIR".to_string(),
            Self::IncompleteInlineBranch => "incomplete inline branch".to_string(),
            Self::UnmodeledIntrinsic => "unmodeled intrinsic".to_string(),
            Self::UnresolvedUnsafeCall => "unresolved unsafe call".to_string(),
            Self::MissingContract => "missing safety contract".to_string(),
            Self::UnsupportedProperty => "unsupported property".to_string(),
            Self::Unimplemented => "unresolved value or unsupported shape".to_string(),
            Self::Multiple(reasons) => reasons
                .iter()
                .map(Self::description)
                .collect::<Vec<_>>()
                .join("; "),
        }
    }

    pub(crate) fn merge(self, other: UnknownReason) -> UnknownReason {
        let mut reasons = match self {
            Self::Multiple(reasons) => reasons,
            reason => vec![reason],
        };
        let others = match other {
            Self::Multiple(reasons) => reasons,
            reason => vec![reason],
        };
        for reason in others {
            if !reasons.contains(&reason) {
                reasons.push(reason);
            }
        }
        if reasons.len() == 1 {
            reasons.pop().unwrap()
        } else {
            Self::Multiple(reasons)
        }
    }
}

/// Verification status for one required property on one path.
#[derive(Clone, Debug, PartialEq)]
pub(crate) enum CheckResult {
    /// Proved by a *sound structural rule* (a fast-path that needs no solver
    /// query): ZST guards, zero-element access, tracked invariants/flags,
    /// type-level transparency, provenance-origin classification.  These are
    /// the rules that must be audited for soundness.
    ProvedByRule,
    /// Proved by an *SMT query*: the solver showed the negation is unsatisfiable
    /// (numeric bounds, byte-range coverage, alignment modulo/linear checks).
    ProvedBySmt,
    /// The verifier found a possible violation for this path.
    Failed,
    /// The verifier has not implemented or completed the proof for this path;
    /// the reason is carried in the payload.
    Unknown(UnknownReason),
}

impl CheckResult {
    /// Whether this result counts as "proved" (by rule or by SMT).
    pub(crate) fn is_proved(&self) -> bool {
        matches!(self, CheckResult::ProvedByRule | CheckResult::ProvedBySmt)
    }

    /// The user-facing label for this result.
    pub(crate) fn label(&self) -> String {
        match self {
            CheckResult::ProvedByRule | CheckResult::ProvedBySmt => "Proved".to_string(),
            CheckResult::Failed => "Failed".to_string(),
            CheckResult::Unknown(reason) => format!("Unknown ({})", reason.description()),
        }
    }

    /// AND-combine two results: any `Failed` → `Failed`; any `Unknown` →
    /// `Unknown`; only all-proved → proved (`Rule` when every conjunct was a
    /// rule, otherwise `Smt`).
    pub(crate) fn and(self, other: CheckResult) -> CheckResult {
        match (self, other) {
            (CheckResult::Failed, _) | (_, CheckResult::Failed) => CheckResult::Failed,
            (CheckResult::Unknown(a), CheckResult::Unknown(b)) => {
                CheckResult::Unknown(a.merge(b))
            }
            (CheckResult::Unknown(a), _) | (_, CheckResult::Unknown(a)) => CheckResult::Unknown(a),
            (CheckResult::ProvedByRule, CheckResult::ProvedByRule) => CheckResult::ProvedByRule,
            _ => CheckResult::ProvedBySmt,
        }
    }

    /// OR-combine two results: any proved → proved (a `Rule` proof dominates);
    /// all `Failed` → `Failed`; otherwise `Unknown`.
    pub(crate) fn or(self, other: CheckResult) -> CheckResult {
        match (self, other) {
            (CheckResult::ProvedByRule, _) | (_, CheckResult::ProvedByRule) => {
                CheckResult::ProvedByRule
            }
            (CheckResult::ProvedBySmt, _) | (_, CheckResult::ProvedBySmt) => {
                CheckResult::ProvedBySmt
            }
            (CheckResult::Failed, CheckResult::Failed) => CheckResult::Failed,
            (CheckResult::Unknown(a), CheckResult::Unknown(b)) => {
                CheckResult::Unknown(a.merge(b))
            }
            (CheckResult::Unknown(a), _) | (_, CheckResult::Unknown(a)) => CheckResult::Unknown(a),
        }
    }
}

/// Result for one required property along one path to a checkpoint.
#[derive(Clone, Debug)]
pub(crate) struct PropertyCheckResult<'tcx> {
    /// Unsafe checkpoint being checked.
    pub checkpoint: CheckpointLocation,
    /// Index of the checkpoint in the function-level checkpoint list.
    pub checkpoint_index: usize,
    /// Index of the path in the checkpoint path set.
    pub path_index: usize,
    /// Index of the property in the checkpoint-level property list.
    pub property_index: usize,
    /// Required property checked on this path.
    pub property: Property<'tcx>,
    /// Current verification status.
    pub result: CheckResult,
    /// Optional path-local diagnostic message generated by the verifier.
    pub diagnostics: Option<String>,
    /// Human-readable path description.
    pub path_description: String,
    /// Callee name for this checkpoint.
    pub callee_name: String,
}

/// Verification report for one function target.
#[derive(Clone, Debug)]
pub(crate) struct VerificationReport<'tcx> {
    /// Function that was verified.
    pub function: DefId,
    /// Per-path property results emitted by the verifier.
    pub results: Vec<PropertyCheckResult<'tcx>>,
}

impl<'tcx> VerificationReport<'tcx> {
    /// Create an empty report for a function target.
    pub(crate) fn new(function: DefId) -> Self {
        Self {
            function,
            results: Vec::new(),
        }
    }

    /// Add one path/property check result to this report.
    pub(crate) fn push(&mut self, result: PropertyCheckResult<'tcx>) {
        self.results.push(result);
    }

    /// Render the whole report as a readable multi-line diagnostic.
    pub(crate) fn describe(&self) -> String {
        let mut out = String::new();
        out.push_str(&format!(
            "[rapx::verify::diagnostics] function {:?}: {} check item(s)\n",
            self.function,
            self.results.len()
        ));

        for (index, result) in self.results.iter().enumerate() {
            out.push_str(&format!(
                "  check #{index}: checkpoint #{}, bb{}, path #{}, property #{} {:?}, result {}\n",
                result.checkpoint_index,
                result.checkpoint.block.as_usize(),
                result.path_index,
                result.property_index,
                result.property.kind(),
                result.result.label()
            ));

            if let Some(diagnostics) = &result.diagnostics {
                out.push_str(diagnostics);
                if !diagnostics.ends_with('\n') {
                    out.push('\n');
                }
            }
        }

        out
    }
}

#[cfg(test)]
mod tests {
    use super::{CheckResult, UnknownReason};

    #[test]
    fn unknown_labels_preserve_solver_reason_and_multiple_causes() {
        let timeout = CheckResult::Unknown(UnknownReason::SmtUnknown("timeout".into()));
        assert_eq!(timeout.label(), "Unknown (timeout)");

        let combined = UnknownReason::UnsupportedMir
            .merge(UnknownReason::SmtUnknown("incomplete".into()));
        assert_eq!(
            CheckResult::Unknown(combined).label(),
            "Unknown (unsupported MIR; SMT: incomplete)"
        );
    }
}