From ab2cb50e136969c1e6d50fc1aa9f160460069e9b Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Thu, 24 Oct 2024 22:38:11 -0500
Subject: [PATCH] Call `goto-instrument` with `DFCC` only once (#3642)

DFCC should be called only once. This PR combined the two DCFF calls
into one.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 kani-driver/src/call_goto_instrument.rs | 80 ++++++++++++-------------
 1 file changed, 40 insertions(+), 40 deletions(-)

diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs
index a77e3c675aec..4ec363655491 100644
--- a/kani-driver/src/call_goto_instrument.rs
+++ b/kani-driver/src/call_goto_instrument.rs
@@ -37,16 +37,12 @@ impl KaniSession {
             self.goto_sanity_check(output)?;
         }
 
-        self.instrument_contracts(harness, output)?;
-
-        if self
+        let is_loop_contracts_enabled = self
             .args
             .common_args
             .unstable_features
-            .contains(kani_metadata::UnstableFeature::LoopContracts)
-        {
-            self.instrument_loop_contracts(harness, output)?;
-        }
+            .contains(kani_metadata::UnstableFeature::LoopContracts);
+        self.instrument_contracts(harness, is_loop_contracts_enabled, output)?;
 
         if self.args.checks.undefined_function_on() {
             self.add_library(output)?;
@@ -172,42 +168,46 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
-    /// Make CBMC enforce a function contract.
-    pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> {
-        let Some(assigns) = harness.contract.as_ref() else { return Ok(()) };
+    /// Apply annotated function contracts and loop contracts with goto-instrument.
+    pub fn instrument_contracts(
+        &self,
+        harness: &HarnessMetadata,
+        is_loop_contracts_enabled: bool,
+        file: &Path,
+    ) -> Result<()> {
+        // Do nothing if neither loop contracts nor function contracts is enabled.
+        if !is_loop_contracts_enabled && harness.contract.is_none() {
+            return Ok(());
+        }
 
-        let mut args: Vec<OsString> = vec![
-            "--dfcc".into(),
-            (&harness.mangled_name).into(),
-            "--enforce-contract".into(),
-            assigns.contracted_function_name.as_str().into(),
-            "--no-malloc-may-fail".into(),
-            file.into(),
-            file.into(),
-        ];
-        if let Some(tracker) = &assigns.recursion_tracker {
-            args.push("--nondet-static-exclude".into());
-            args.push(tracker.as_str().into());
+        let mut args: Vec<OsString> =
+            vec!["--dfcc".into(), (&harness.mangled_name).into(), "--no-malloc-may-fail".into()];
+
+        if is_loop_contracts_enabled {
+            args.append(&mut vec![
+                "--apply-loop-contracts".into(),
+                "--loop-contracts-no-unwind".into(),
+                // Because loop contracts now are wrapped in a closure which will be a side-effect expression in CBMC even they
+                // may not contain side-effect. So we disable the side-effect check for now and will implement a better check
+                // instead of simply rejecting function calls and statement expressions.
+                // See issue: diffblue/cbmc#8393
+                "--disable-loop-contracts-side-effect-check".into(),
+            ]);
         }
-        self.call_goto_instrument(&args)
-    }
 
-    /// Apply annotated loop contracts.
-    pub fn instrument_loop_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> {
-        let args: Vec<OsString> = vec![
-            "--dfcc".into(),
-            (&harness.mangled_name).into(),
-            "--apply-loop-contracts".into(),
-            "--loop-contracts-no-unwind".into(),
-            "--no-malloc-may-fail".into(),
-            // Because loop contracts now are wrapped in a closure which will be a side-effect expression in CBMC even they
-            // may not contain side-effect. So we disable the side-effect check for now and will implement a better check
-            // instead of simply rejecting function calls and statement expressions.
-            // See issue: diffblue/cbmc#8393
-            "--disable-loop-contracts-side-effect-check".into(),
-            file.into(),
-            file.into(),
-        ];
+        if let Some(assigns) = harness.contract.as_ref() {
+            args.push("--enforce-contract".into());
+            args.push(assigns.contracted_function_name.as_str().into());
+
+            if let Some(tracker) = &assigns.recursion_tracker {
+                args.push("--nondet-static-exclude".into());
+                args.push(tracker.as_str().into());
+            }
+        }
+
+        args.push(file.into());
+        args.push(file.into());
+
         self.call_goto_instrument(&args)
     }