From 3e2e28efa111d6c17962415fba7caffeb034eb76 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 24 Oct 2024 13:48:41 -0500 Subject: [PATCH 1/3] Call DFCC only once --- kani-driver/src/call_goto_instrument.rs | 30 +++++++++++++++++++------ 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index a77e3c675aec..3a32957f6fcb 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -37,15 +37,15 @@ impl KaniSession { self.goto_sanity_check(output)?; } - self.instrument_contracts(harness, output)?; - if self .args .common_args .unstable_features .contains(kani_metadata::UnstableFeature::LoopContracts) { - self.instrument_loop_contracts(harness, output)?; + self.instrument_contracts_with_loop_contracts(harness, output)?; + } else { + self.instrument_contracts(harness, output)?; } if self.args.checks.undefined_function_on() { @@ -193,8 +193,12 @@ impl KaniSession { } /// Apply annotated loop contracts. - pub fn instrument_loop_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> { - let args: Vec = vec![ + pub fn instrument_contracts_with_loop_contracts( + &self, + harness: &HarnessMetadata, + file: &Path, + ) -> Result<()> { + let mut args: Vec = vec![ "--dfcc".into(), (&harness.mangled_name).into(), "--apply-loop-contracts".into(), @@ -205,9 +209,21 @@ impl KaniSession { // 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) } From 7e78b01732d333e83482bd5fba6d06232dfeb12c Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 24 Oct 2024 20:04:56 -0500 Subject: [PATCH 2/3] Combine two instrument_contracts functions --- kani-driver/src/call_goto_instrument.rs | 66 ++++++++++--------------- 1 file changed, 25 insertions(+), 41 deletions(-) diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 3a32957f6fcb..eec73a4ee3bf 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)?; } - if self + let is_loop_contracts_enabled = self .args .common_args .unstable_features - .contains(kani_metadata::UnstableFeature::LoopContracts) - { - self.instrument_contracts_with_loop_contracts(harness, output)?; - } else { - self.instrument_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,44 +168,32 @@ 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(()) }; - - let mut args: Vec = 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()); - } - self.call_goto_instrument(&args) - } - - /// Apply annotated loop contracts. - pub fn instrument_contracts_with_loop_contracts( + /// 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<()> { - let mut args: Vec = 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(), - ]; + // 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 = vec!["--dfcc".into(), (&harness.mangled_name).into()]; + + if is_loop_contracts_enabled { + args.append(&mut vec![ + "--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(), + ]); + } if let Some(assigns) = harness.contract.as_ref() { args.push("--enforce-contract".into()); From 728d985b7482031853bfaa16fd907e0040a335d0 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 24 Oct 2024 21:27:55 -0500 Subject: [PATCH 3/3] Always assume mallo not fail in goto-instrument --- kani-driver/src/call_goto_instrument.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index eec73a4ee3bf..4ec363655491 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -180,13 +180,13 @@ impl KaniSession { return Ok(()); } - let mut args: Vec = vec!["--dfcc".into(), (&harness.mangled_name).into()]; + let mut args: Vec = + 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(), - "--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.