harness.rs

// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

use crate::CbmcSolver;
use serde::{Deserialize, Serialize};
use std::path::PathBuf;

/// We emit this structure for each annotated proof harness (`#[kani::proof]`) we find.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct HarnessMetadata {
    /// The fully qualified name the user gave to the function (i.e. includes the module path).
    pub pretty_name: String,
    /// The name of the function in the CBMC symbol table.
    pub mangled_name: String,
    /// The name of the crate this harness belongs to.
    pub crate_name: String,
    /// The (currently full-) path to the file this proof harness was declared within.
    pub original_file: String,
    /// The line in that file where the proof harness begins.
    pub original_start_line: usize,
    /// The line in that file where the proof harness ends.
    pub original_end_line: usize,
    /// Optional modeling file that was generated by the compiler that includes this harness.
    pub goto_file: Option<PathBuf>,
    /// The `#[kani::<>]` attributes added to a harness.
    pub attributes: HarnessAttributes,
}

/// The attributes added by the user to control how a harness is executed.
#[derive(Debug, Clone, Serialize, Deserialize, Default)]
pub struct HarnessAttributes {
    /// Whether the harness has been annotated with proof.
    pub proof: bool,
    /// Whether the harness is expected to panic or not.
    pub should_panic: bool,
    /// Optional data to store solver.
    pub solver: Option<CbmcSolver>,
    /// Optional data to store unwind value.
    pub unwind_value: Option<u32>,
    /// The stubs used in this harness.
    pub stubs: Vec<Stub>,
}

/// The stubbing type.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct Stub {
    pub original: String,
    pub replacement: String,
}

impl HarnessMetadata {
    /// get the unqualifed (i.e. without ::) harness name. If the
    /// harness name contains ::, then we use rightmost name..
    pub fn get_harness_name_unqualified(&self) -> &str {
        const PATH_SEPARATOR: &str = "::";
        if let Some(last_separator) = self.pretty_name.rfind(PATH_SEPARATOR) {
            let name_start = last_separator + PATH_SEPARATOR.len();
            &self.pretty_name[name_start..]
        } else {
            &self.pretty_name
        }
    }
}