From adc1f0df9728e39149996fad7f35068275619e88 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 8 Jun 2024 17:02:41 +0200 Subject: [PATCH] Do not turn trivially diverging loops into assume(false) (#3223) CBMC's symbolic execution by default turns `while(true) {}` loops into `assume(false)` to counter trivial non-termination of symbolic execution. When unwinding assertions are enabled, however, we should report the non-termination of such loops. Resolves: #2909 --- kani-driver/src/call_cbmc.rs | 2 ++ .../function-contract/diverging_loop.expected | 3 +++ .../expected/function-contract/diverging_loop.rs | 15 +++++++++++++++ 3 files changed, 20 insertions(+) create mode 100644 tests/expected/function-contract/diverging_loop.expected create mode 100644 tests/expected/function-contract/diverging_loop.rs diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 7d0edf6f50e5..7a623253f3a3 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -182,7 +182,9 @@ impl KaniSession { } if self.args.checks.unwinding_on() { + // TODO: With CBMC v6 the below can be removed as those are defaults. args.push("--unwinding-assertions".into()); + args.push("--no-self-loops-to-assumptions".into()); } if self.args.extra_pointer_checks { diff --git a/tests/expected/function-contract/diverging_loop.expected b/tests/expected/function-contract/diverging_loop.expected new file mode 100644 index 000000000000..05c2856a7c31 --- /dev/null +++ b/tests/expected/function-contract/diverging_loop.expected @@ -0,0 +1,3 @@ +Failed Checks: unwinding assertion loop 0 + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/diverging_loop.rs b/tests/expected/function-contract/diverging_loop.rs new file mode 100644 index 000000000000..219f723494f7 --- /dev/null +++ b/tests/expected/function-contract/diverging_loop.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::ensures(|result : &i32| *result == 1)] +fn foo() -> i32 { + loop {} + 2 +} + +#[kani::proof_for_contract(foo)] +#[kani::unwind(1)] +fn check_foo() { + let _ = foo(); +}