Propogate solver options into synthesizer (#2320)

model-checking · Apr 7, 2023 · 911b8b9 · 911b8b9
1 parent f70faac
commit 911b8b9
Show file tree

Hide file tree

Showing 7 changed files with 17 additions and 4 deletions.
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
@@ -198,7 +198,7 @@ impl KaniSession {
         args
     }
 
-    fn handle_solver_args(
+    pub fn handle_solver_args(
         &self,
         harness_solver: &Option<CbmcSolver>,
         args: &mut Vec<OsString>,

diff --git a/kani-driver/src/call_goto_synthesizer.rs b/kani-driver/src/call_goto_synthesizer.rs
@@ -3,6 +3,7 @@
 
 use crate::util::warning;
 use anyhow::Result;
+use kani_metadata::HarnessMetadata;
 use std::ffi::OsString;
 use std::path::Path;
 use std::process::Command;
@@ -14,7 +15,12 @@ impl KaniSession {
     /// The synthesizer we use is `goto-synthesizer` built in CBMC codebase, which is an enumerative
     /// loop-contracts synthesizer. `goto-synthesizer` enumerates and checks if a candidate can be
     /// used to prove some assertions, and applies found invariants when all checks pass.
-    pub fn synthesize_loop_contracts(&self, input: &Path, output: &Path) -> Result<()> {
+    pub fn synthesize_loop_contracts(
+        &self,
+        input: &Path,
+        output: &Path,
+        harness_metadata: &HarnessMetadata,
+    ) -> Result<()> {
         if !self.args.quiet {
             println!("Running loop contract synthesizer.");
             warning("This process may not terminate.");
@@ -23,12 +29,14 @@ impl KaniSession {
             );
         }
 
-        let args: Vec<OsString> = vec![
+        let mut args: Vec<OsString> = vec![
             "--loop-contracts-no-unwind".into(),
             input.to_owned().into_os_string(),  // input
             output.to_owned().into_os_string(), // output
         ];
 
+        self.handle_solver_args(&harness_metadata.attributes.solver, &mut args)?;
+
         let mut cmd = Command::new("goto-synthesizer");
         cmd.args(args);
 

diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
@@ -66,7 +66,11 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
                     )?;
 
                     if self.sess.args.synthesize_loop_contracts {
-                        self.sess.synthesize_loop_contracts(&specialized_obj, &specialized_obj)?;
+                        self.sess.synthesize_loop_contracts(
+                            &specialized_obj,
+                            &specialized_obj,
+                            &harness,
+                        )?;
                     }
 
                     let result = self.sess.check_harness(&specialized_obj, &report_dir, harness)?;

diff --git a/...ContractsSynthesizer/main_signed/expected → ...-contracts-synthesis/main_signed/expected b/...ContractsSynthesizer/main_signed/expected → ...-contracts-synthesis/main_signed/expected
diff --git a/...ctsSynthesizer/main_signed/main_signed.rs → ...acts-synthesis/main_signed/main_signed.rs b/...ctsSynthesizer/main_signed/main_signed.rs → ...acts-synthesis/main_signed/main_signed.rs
diff --git a/...ntractsSynthesizer/main_unsigned/expected → ...ontracts-synthesis/main_unsigned/expected b/...ntractsSynthesizer/main_unsigned/expected → ...ontracts-synthesis/main_unsigned/expected
diff --git a/...ynthesizer/main_unsigned/main_unsigned.rs → ...-synthesis/main_unsigned/main_unsigned.rs b/...ynthesizer/main_unsigned/main_unsigned.rs → ...-synthesis/main_unsigned/main_unsigned.rs
@@ -7,6 +7,7 @@
 // loop invariants.
 
 #[kani::proof]
+#[kani::solver(kissat)]
 fn main() {
     let mut x: u64 = kani::any_where(|i| *i > 1);