Allow user to specify CBMC's solver (rust-lang#2088)

Co-authored-by: Adrian Palacios <[email protected]>
Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Author: 3 people

Cargo.lock

@@ -535,6 +535,7 @@ dependencies = [
  "tracing",
  "tracing-subscriber",
  "tracing-tree",
+ "which",
 ]
 
 [[package]]
@@ -562,6 +563,8 @@ version = "0.20.0"
 dependencies = [
  "cprover_bindings",
  "serde",
+ "strum",
+ "strum_macros",
 ]
 
 [[package]]

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -7,9 +7,9 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::attributes::{extract_integer_argument, partition_kanitool_attributes};
 use cbmc::goto_program::{Expr, Stmt, Symbol};
 use cbmc::InternString;
-use kani_metadata::HarnessMetadata;
+use kani_metadata::{CbmcSolver, HarnessMetadata};
 use kani_queries::UserInput;
-use rustc_ast::Attribute;
+use rustc_ast::{Attribute, MetaItemKind};
 use rustc_hir::def::DefKind;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::traversal::reverse_postorder;
@@ -19,6 +19,7 @@ use rustc_middle::ty::{self, Instance};
 use std::collections::BTreeMap;
 use std::convert::TryInto;
 use std::iter::FromIterator;
+use std::str::FromStr;
 use tracing::{debug, debug_span};
 
 /// Codegen MIR functions into gotoc
@@ -353,6 +354,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 original_file: loc.filename().unwrap(),
                 original_start_line: loc.start_line().unwrap() as usize,
                 original_end_line: loc.end_line().unwrap() as usize,
+                solver: None,
                 unwind_value: None,
                 // We record the actual path after codegen before we dump the metadata into a file.
                 goto_file: None,
@@ -378,6 +380,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let mut harness = self.default_kanitool_proof();
         for attr in other_attributes.iter() {
             match attr.0.as_str() {
+                "solver" => self.handle_kanitool_solver(attr.1, &mut harness),
                 "stub" => {
                     if !self.queries.get_stubbing_enabled() {
                         self.tcx.sess.span_warn(
@@ -412,6 +415,7 @@ impl<'tcx> GotocCtx<'tcx> {
             original_file: loc.filename().unwrap(),
             original_start_line: loc.start_line().unwrap() as usize,
             original_end_line: loc.end_line().unwrap() as usize,
+            solver: None,
             unwind_value: None,
             // We record the actual path after codegen before we dump the metadata into a file.
             goto_file: None,
@@ -445,4 +449,68 @@ impl<'tcx> GotocCtx<'tcx> {
             }
         }
     }
+
+    /// Set the solver for this proof harness
+    fn handle_kanitool_solver(&mut self, attr: &Attribute, harness: &mut HarnessMetadata) {
+        // Make sure the solver is not already set
+        if harness.solver.is_some() {
+            self.tcx
+                .sess
+                .span_err(attr.span, "only one '#[kani::solver]' attribute is allowed per harness");
+            return;
+        }
+        harness.solver = self.extract_solver_argument(attr);
+    }
+
+    fn extract_solver_argument(&mut self, attr: &Attribute) -> Option<CbmcSolver> {
+        // TODO: Argument validation should be done as part of the `kani_macros` crate
+        // <https://github.com/model-checking/kani/issues/2192>
+        const ATTRIBUTE: &str = "#[kani::solver]";
+        let invalid_arg_err = |attr: &Attribute| {
+            self.tcx.sess.span_err(
+                attr.span,
+                format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `custom=\"<SAT_SOLVER_BINARY>\"`)")
+            )
+        };
+
+        let attr_args = attr.meta_item_list().unwrap();
+        if attr_args.len() != 1 {
+            self.tcx.sess.span_err(
+                attr.span,
+                format!(
+                    "the `{ATTRIBUTE}` attribute expects a single argument. Got {} arguments.",
+                    attr_args.len()
+                ),
+            );
+            return None;
+        }
+        let attr_arg = &attr_args[0];
+        let meta_item = attr_arg.meta_item();
+        if meta_item.is_none() {
+            invalid_arg_err(attr);
+            return None;
+        }
+        let meta_item = meta_item.unwrap();
+        let ident = meta_item.ident().unwrap();
+        let ident_str = ident.as_str();
+        match &meta_item.kind {
+            MetaItemKind::Word => {
+                let solver = CbmcSolver::from_str(ident_str);
+                match solver {
+                    Ok(solver) => Some(solver),
+                    Err(_) => {
+                        self.tcx.sess.span_err(attr.span, format!("unknown solver `{ident_str}`"));
+                        None
+                    }
+                }
+            }
+            MetaItemKind::NameValue(lit) if ident_str == "custom" && lit.kind.is_str() => {
+                Some(CbmcSolver::Custom(lit.token_lit.symbol.to_string()))
+            }
+            _ => {
+                invalid_arg_err(attr);
+                None
+            }
+        }
+    }
 }

kani-driver/Cargo.toml

@@ -37,6 +37,7 @@ strum_macros = {version = "0.24.0"}
 tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
 tracing-tree = "0.2.2"
+which = "4.4.0"
 
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml

kani-driver/src/args.rs

@@ -4,10 +4,17 @@
 #[cfg(feature = "unsound_experiments")]
 use crate::unsound_experiments::UnsoundExperimentArgs;
 use crate::util::warning;
+use kani_metadata::CbmcSolver;
 
-use clap::{error::Error, error::ErrorKind, CommandFactory, ValueEnum};
+use clap::builder::{PossibleValue, TypedValueParser};
+use clap::{
+    error::ContextKind, error::ContextValue, error::Error, error::ErrorKind, CommandFactory,
+    ValueEnum,
+};
 use std::ffi::OsString;
 use std::path::PathBuf;
+use std::str::FromStr;
+use strum::VariantNames;
 
 // By default we configure CBMC to use 16 bits to represent the object bits in pointers.
 const DEFAULT_OBJECT_BITS: u32 = 16;
@@ -150,6 +157,9 @@ pub struct KaniArgs {
     /// Specify the value used for loop unwinding for the specified harness in CBMC
     #[arg(long, requires("harness"))]
     pub unwind: Option<u32>,
+    /// Specify the CBMC solver to use. Overrides the harness `solver` attribute.
+    #[arg(long, value_parser = CbmcSolverValueParser::new(CbmcSolver::VARIANTS))]
+    pub solver: Option<CbmcSolver>,
     /// Pass through directly to CBMC; must be the last flag.
     /// This feature is unstable and it requires `--enable_unstable` to be used
     #[arg(
@@ -549,6 +559,61 @@ impl KaniArgs {
     }
 }
 
+/// clap parser for `CbmcSolver`
+#[derive(Clone, Debug)]
+pub struct CbmcSolverValueParser(Vec<PossibleValue>);
+
+impl CbmcSolverValueParser {
+    pub fn new(values: impl Into<CbmcSolverValueParser>) -> Self {
+        values.into()
+    }
+}
+
+impl TypedValueParser for CbmcSolverValueParser {
+    type Value = CbmcSolver;
+
+    fn parse_ref(
+        &self,
+        cmd: &clap::builder::Command,
+        arg: Option<&clap::builder::Arg>,
+        value: &std::ffi::OsStr,
+    ) -> Result<Self::Value, clap::error::Error> {
+        let value = value.to_str().unwrap();
+        // `value` is one of the possible `CbmcSolver` values or `custom=<binary>`
+        let segments: Vec<&str> = value.split('=').collect();
+
+        let mut err = clap::Error::new(ErrorKind::InvalidValue).with_cmd(cmd);
+        err.insert(ContextKind::InvalidArg, ContextValue::String(arg.unwrap().to_string()));
+        err.insert(ContextKind::InvalidValue, ContextValue::String(value.to_string()));
+
+        if segments.len() == 2 {
+            if segments[0] != "custom" {
+                return Err(err);
+            }
+            return Ok(CbmcSolver::Custom(segments[1].into()));
+        } else if segments.len() == 1 {
+            let solver = CbmcSolver::from_str(value);
+            return solver.map_err(|_| err);
+        }
+        Err(err)
+    }
+
+    /// Used for the help message
+    fn possible_values(&self) -> Option<Box<dyn Iterator<Item = PossibleValue> + '_>> {
+        Some(Box::new(self.0.iter().cloned()))
+    }
+}
+
+impl<I, T> From<I> for CbmcSolverValueParser
+where
+    I: IntoIterator<Item = T>,
+    T: Into<PossibleValue>,
+{
+    fn from(values: I) -> Self {
+        Self(values.into_iter().map(|t| t.into()).collect())
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use clap::Parser;

kani-driver/src/call_cbmc.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::{bail, Result};
-use kani_metadata::HarnessMetadata;
+use kani_metadata::{CbmcSolver, HarnessMetadata};
 use std::ffi::OsString;
 use std::fmt::Write;
 use std::path::Path;
@@ -123,6 +123,8 @@ impl KaniSession {
             args.push(unwind_value.to_string().into());
         }
 
+        self.handle_solver_args(&harness_metadata.solver, &mut args)?;
+
         if self.args.run_sanity_checks {
             args.push("--validate-goto-model".into());
             args.push("--validate-ssa-equation".into());
@@ -186,6 +188,42 @@ impl KaniSession {
 
         args
     }
+
+    fn handle_solver_args(
+        &self,
+        harness_solver: &Option<CbmcSolver>,
+        args: &mut Vec<OsString>,
+    ) -> Result<()> {
+        let solver = if let Some(solver) = &self.args.solver {
+            // `--solver` option takes precedence over attributes
+            solver
+        } else if let Some(solver) = harness_solver {
+            solver
+        } else {
+            // Nothing to do
+            return Ok(());
+        };
+
+        match solver {
+            CbmcSolver::Kissat => {
+                args.push("--external-sat-solver".into());
+                args.push("kissat".into());
+            }
+            CbmcSolver::Minisat => {
+                // Minisat is currently CBMC's default solver, so no need to
+                // pass any arguments
+            }
+            CbmcSolver::Custom(custom_solver) => {
+                // Check if the specified binary exists in path
+                if which::which(custom_solver).is_err() {
+                    bail!("the specified solver \"{custom_solver}\" was not found in path")
+                }
+                args.push("--external-sat-solver".into());
+                args.push(custom_solver.into());
+            }
+        }
+        Ok(())
+    }
 }
 
 impl VerificationResult {

kani-driver/src/metadata.rs

@@ -149,6 +149,7 @@ pub fn mock_proof_harness(
         original_file: "<unknown>".into(),
         original_start_line: 0,
         original_end_line: 0,
+        solver: None,
         unwind_value,
         goto_file: None,
     }

kani_metadata/Cargo.toml

@@ -13,3 +13,5 @@ publish = false
 [dependencies]
 serde = {version = "1", features = ["derive"]}
 cbmc = { path = "../cprover_bindings", package = "cprover_bindings" }
+strum = "0.24.1"
+strum_macros = "0.24.3"

kani_metadata/src/cbmc_solver.rs

@@ -0,0 +1,33 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use serde::{Deserialize, Serialize};
+use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
+
+/// An enum for CBMC solver options. All variants are handled by Kani, except for
+/// the `Custom` one, which it passes as is to CBMC's `--external-sat-solver`
+/// option.
+#[derive(
+    Debug,
+    Clone,
+    AsRefStr,
+    EnumString,
+    EnumVariantNames,
+    PartialEq,
+    Eq,
+    Serialize,
+    Deserialize
+)]
+#[strum(serialize_all = "snake_case")]
+pub enum CbmcSolver {
+    /// The kissat solver that is included in the Kani bundle
+    Kissat,
+
+    /// MiniSAT (CBMC's default solver)
+    Minisat,
+
+    /// A custom solver variant whose argument gets passed to
+    /// `--external-sat-solver`. The specified binary must exist in path.
+    #[strum(disabled, serialize = "custom=<SAT_SOLVER_BINARY>")]
+    Custom(String),
+}

kani_metadata/src/harness.rs

@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+use crate::CbmcSolver;
 use serde::{Deserialize, Serialize};
 use std::path::PathBuf;
 
@@ -19,6 +20,8 @@ pub struct HarnessMetadata {
     pub original_start_line: usize,
     /// The line in that file where the proof harness ends.
     pub original_end_line: usize,
+    /// Optional data to store solver.
+    pub solver: Option<CbmcSolver>,
     /// Optional data to store unwind value.
     pub unwind_value: Option<u32>,
     /// Optional modeling file that was generated by the compiler that includes this harness.

kani_metadata/src/lib.rs

@@ -4,10 +4,12 @@
 use serde::{Deserialize, Serialize};
 
 pub use artifact::ArtifactType;
+pub use cbmc_solver::CbmcSolver;
 pub use harness::*;
 pub use vtable::*;
 
 pub mod artifact;
+mod cbmc_solver;
 mod harness;
 mod vtable;
 

library/kani_macros/src/lib.rs

@@ -148,6 +148,29 @@ pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream {
     result
 }
 
+#[cfg(not(kani))]
+#[proc_macro_attribute]
+pub fn solver(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    // No-op in non-kani mode
+    item
+}
+
+/// Select the SAT solver to use with CBMC for this harness
+/// The attribute `#[kani::solver(arg)]` can only be used alongside `#[kani::proof]``
+///
+/// arg - name of solver, e.g. kissat
+#[cfg(kani)]
+#[proc_macro_attribute]
+pub fn solver(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let mut result = TokenStream::new();
+    // Translate `#[kani::solver(arg)]` to `#[kanitool::solver(arg)]`
+    let insert_string = "#[kanitool::solver(".to_owned() + &attr.to_string() + ")]";
+    result.extend(insert_string.parse::<TokenStream>().unwrap());
+
+    result.extend(item);
+    result
+}
+
 /// Allow users to auto generate Arbitrary implementations by using `#[derive(Arbitrary)]` macro.
 #[proc_macro_error]
 #[proc_macro_derive(Arbitrary)]