From 911b8b9d8f94a82cbe2acd2d409c091f754e71c4 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Fri, 7 Apr 2023 01:00:43 -0500
Subject: [PATCH] Propogate solver options into synthesizer (#2320)

---
 kani-driver/src/call_cbmc.rs                         |  2 +-
 kani-driver/src/call_goto_synthesizer.rs             | 12 ++++++++++--
 kani-driver/src/harness_runner.rs                    |  6 +++++-
 .../main_signed/expected                             |  0
 .../main_signed/main_signed.rs                       |  0
 .../main_unsigned/expected                           |  0
 .../main_unsigned/main_unsigned.rs                   |  1 +
 7 files changed, 17 insertions(+), 4 deletions(-)
 rename tests/ui/{LoopContractsSynthesizer => loop-contracts-synthesis}/main_signed/expected (100%)
 rename tests/ui/{LoopContractsSynthesizer => loop-contracts-synthesis}/main_signed/main_signed.rs (100%)
 rename tests/ui/{LoopContractsSynthesizer => loop-contracts-synthesis}/main_unsigned/expected (100%)
 rename tests/ui/{LoopContractsSynthesizer => loop-contracts-synthesis}/main_unsigned/main_unsigned.rs (94%)

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index f637b2ed5e03..4eb7e9010eeb 100644
--- 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
index 3d6007a6b97e..97a5e54c5a6d 100644
--- 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
index d50b0c876313..4329eb77962f 100644
--- 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/tests/ui/LoopContractsSynthesizer/main_signed/expected b/tests/ui/loop-contracts-synthesis/main_signed/expected
similarity index 100%
rename from tests/ui/LoopContractsSynthesizer/main_signed/expected
rename to tests/ui/loop-contracts-synthesis/main_signed/expected
diff --git a/tests/ui/LoopContractsSynthesizer/main_signed/main_signed.rs b/tests/ui/loop-contracts-synthesis/main_signed/main_signed.rs
similarity index 100%
rename from tests/ui/LoopContractsSynthesizer/main_signed/main_signed.rs
rename to tests/ui/loop-contracts-synthesis/main_signed/main_signed.rs
diff --git a/tests/ui/LoopContractsSynthesizer/main_unsigned/expected b/tests/ui/loop-contracts-synthesis/main_unsigned/expected
similarity index 100%
rename from tests/ui/LoopContractsSynthesizer/main_unsigned/expected
rename to tests/ui/loop-contracts-synthesis/main_unsigned/expected
diff --git a/tests/ui/LoopContractsSynthesizer/main_unsigned/main_unsigned.rs b/tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs
similarity index 94%
rename from tests/ui/LoopContractsSynthesizer/main_unsigned/main_unsigned.rs
rename to tests/ui/loop-contracts-synthesis/main_unsigned/main_unsigned.rs
index e2e272f1819c..f981ca8fa12b 100644
--- a/tests/ui/LoopContractsSynthesizer/main_unsigned/main_unsigned.rs
+++ b/tests/ui/loop-contracts-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);