Rewrite loops with multiple back edges to having a single back edge only (rust-lang#1117)

rustc reasonably translates if statements at end of a loop body to
backwards jumps to the loop head. This, however, causes CBMC's symbolic
execution to spuriously treat these as nested loops. This commit now
enables a rewrite step that had previously been built for exactly such
cases.

This treatment as nested loops implied that seemingly lower unwinding
bounds were sufficient (as the loop unwinding counter got reset). Three
of the tests exhibited this behaviour, which now makes larger unwinding
bounds necessary.

Fixes: rust-lang#1046

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Co-authored-by: Michael Tautschnig <[email protected]>
Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Author: 3 people

docs/src/tutorial/arbitrary-variables/Cargo.toml

@@ -11,4 +11,4 @@ vector-map = "1.0.1"
 [workspace]
 
 [workspace.metadata.kani]
-flags = { default-checks = false, unwind = "2" }
+flags = { unwind = "3" }

kani-driver/src/call_goto_instrument.rs

@@ -23,6 +23,8 @@ impl KaniSession {
             self.just_drop_unused_functions(output)?;
         }
 
+        self.rewrite_back_edges(output)?;
+
         if self.args.gen_c {
             if !self.args.quiet {
                 println!("Generated C code written to {}", output.to_string_lossy());
@@ -100,6 +102,16 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
+    fn rewrite_back_edges(&self, file: &Path) -> Result<()> {
+        let args: Vec<OsString> = vec![
+            "--ensure-one-backedge-per-target".into(),
+            file.to_owned().into_os_string(), // input
+            file.to_owned().into_os_string(), // output
+        ];
+
+        self.call_goto_instrument(args)
+    }
+
     /// Generate a .c file from a goto binary (i.e. --gen-c)
     pub fn gen_c(&self, file: &Path) -> Result<()> {
         let output_filename = alter_extension(file, "c");

tests/kani/AssociatedTypes/into_iter.rs

@@ -19,7 +19,7 @@ impl<'a> MyStruct<'a> {
 }
 
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(3)]
 pub fn check_into_iter_type() {
     let original = "h";
     let mut wrapper = MyStruct::new(original.chars());

tests/kani/Intrinsics/Count/ctpop.rs

@@ -20,11 +20,6 @@ macro_rules! test_ctpop {
                 if bit != 0 {
                     count += 1;
                 }
-                // The assertion below mitigates a low performance issue in this
-                // test due to the loop having a conditional jump at the end,
-                // see https://github.com/model-checking/kani/issues/1046 for
-                // more details.
-                assert!(count >= 0);
             }
             count
         }