Integrate goto-synthesizer into Kani

kani-driver/src/args.rs

@@ -224,6 +224,16 @@ pub struct KaniArgs {
     #[arg(long, hide_short_help = true, requires("enable_unstable"))]
     pub no_slice_formula: bool,
 
+    /// Synthesize loop contracts for all loops.
+    #[arg(
+        long,
+        hide_short_help = true,
+        requires("enable_unstable"),
+        conflicts_with("unwind"),
+        conflicts_with("default_unwind")
+    )]
+    pub synthesize_loop_contracts: bool,
+
     /// Randomize the layout of structures. This option can help catching code that relies on
     /// a specific layout chosen by the compiler that is not guaranteed to be stable in the future.
     /// If a value is given, it will be used as the seed for randomization

kani-driver/src/call_goto_synthesizer.rs

@@ -0,0 +1,36 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use crate::util::warning;
+use anyhow::Result;
+use std::ffi::OsString;
+use std::path::Path;
+use std::process::Command;
+
+use crate::session::KaniSession;
+
+impl KaniSession {
+    /// Synthesize loop contracts for a goto binary `input` and produce a new goto binary `output`
+    /// 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 return found invariants when all checks pass.
+    pub fn synthesize_loop_contracts(&self, input: &Path, output: &Path) -> Result<()> {
+        if !self.args.quiet {
+            warning("Start to synthesize loop contracts for all loops.");
+            warning("WARNING: this process may not terminate.");
+        }
+
+        let args: Vec<OsString> = vec![
+            "--loop-contracts-no-unwind".into(),
+            input.to_owned().into_os_string(),  // input
+            output.to_owned().into_os_string(), // output
+        ];
+
+        let mut cmd = Command::new("goto-synthesizer");
+        cmd.args(args);
+
+        self.run_suppress(cmd)?;
+
+        Ok(())
+    }
+}

kani-driver/src/harness_runner.rs

@@ -65,6 +65,10 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
                         &harness,
                     )?;
 
+                    if self.sess.args.synthesize_loop_contracts {
+                        self.sess.synthesize_loop_contracts(&specialized_obj, &specialized_obj)?;
+                    }
+
                     let result = self.sess.check_harness(&specialized_obj, &report_dir, harness)?;
                     Ok(HarnessResult { harness, result })
                 })

kani-driver/src/main.rs

@@ -23,6 +23,7 @@ mod call_cbmc;
 mod call_cbmc_viewer;
 mod call_goto_cc;
 mod call_goto_instrument;
+mod call_goto_synthesizer;
 mod call_single_file;
 mod cbmc_output_parser;
 mod cbmc_property_renderer;

tests/ui/LoopContractsSynthesizer/main_signed/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/ui/LoopContractsSynthesizer/main_unsigned/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL