Add two Boogie tests

.gitignore

@@ -72,6 +72,9 @@ package-lock.json
 ## Rustdoc GUI tests
 tests/rustdoc-gui/src/**.lock
 
+## Boogie files
+*.bpl
+
 # Before adding new lines, see the comment at the top.
 /.litani_cache_dir
 /.ninja_deps

kani-compiler/src/codegen_boogie/compiler_interface.rs

@@ -171,7 +171,7 @@ impl BoogieCodegenBackend {
         if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() {
             let mut pb = boogie_file.to_path_buf();
             pb.set_extension("bpl");
-            info!("Writing Boogie file to {}", pb.display());
+            println!("Writing Boogie file to {}", pb.display());
             let file = File::create(&pb).unwrap();
             let mut writer = BufWriter::new(file);
             bcx.write(&mut writer).unwrap();

scripts/kani-regression.sh

@@ -59,6 +59,7 @@ TESTS=(
     "smack kani"
     "cargo-kani cargo-kani"
     "cargo-ui cargo-kani"
+    "script-based-boogie exec"
     "kani-docs cargo-kani"
     "kani-fixme kani-fixme"
 )

tests/script-based-boogie/assign/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: gen_boogie_and_dump.sh
+expected: expected

tests/script-based-boogie/assign/expected

@@ -0,0 +1,7 @@
+procedure
+  var x: bv32;
+  var y: bv32;
+  x := 1bv32;
+  y := x;
+  x := 2bv32;
+  assert

tests/script-based-boogie/assign/gen_boogie_and_dump.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+# Delete any leftover Boogie files
+rm *.bpl
+
+echo "[TEST] Run verification..."
+kani -Zboogie test.rs
+
+cat *.bpl

tests/script-based-boogie/assign/test.rs

@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! A simple test that checks that assignment statements and asserts are
+//! translated to Boogie correctly.
+//!
+//! The `expected` file checks some elements of the expected output Boogie.
+//!
+//! This is a possible Boogie output (which may change with MIR changes):
+//! ```
+//! // Procedures:
+//! procedure _RNvCshNorBqfmMTU_4test19check_assign_assert()
+//! {
+//!   var x: bv32;
+//!   var y: bv32;
+//!   var _4: bool;
+//!   var _5: bv32;
+//!   var _7: bool;
+//!   x := 1bv32;
+//!   y := x;
+//!   x := 2bv32;
+//!   _5 := x;
+//!   _4 := (_5 == 2bv32);
+//!   assert _4;
+//!   _7 := (y == 1bv32);
+//!   assert _7;
+//!   return;
+//! }
+//! ```
+
+#[kani::proof]
+fn check_assign_assert() {
+    let mut x = 1;
+    let y = x;
+    x = 2;
+    kani::assert(x == 2, "");
+    kani::assert(y == 1, "");
+}

tests/script-based-boogie/binop/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: gen_boogie_and_dump.sh
+expected: expected

tests/script-based-boogie/binop/expected

@@ -0,0 +1,19 @@
+function {:bvbuiltin "bvslt"} $BvSignedLessThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvsgt"} $BvSignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvor"} $BvOr<T>(lhs: T, rhs: T) returns (T);
+
+procedure
+  var _1: bv32;
+  var _2: bv32;
+  var _4: bool;
+  var z: bv32;
+  var _7: bool;
+  _1 := 1bv32;
+  _2 := 2bv32;
+  _4 := $BvSignedGreaterThan(_2, _1);
+  assert _4;
+  z := $BvOr(_1, _2);
+  _7 := $BvSignedLessThan(_1, z);
+  assert _7;

tests/script-based-boogie/binop/gen_boogie_and_dump.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+# Delete any leftover Boogie files
+rm *.bpl
+
+echo "[TEST] Run verification..."
+kani -Zboogie test.rs
+
+cat *.bpl

tests/script-based-boogie/binop/test.rs

@@ -0,0 +1,44 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! A simple test that checks that binary operations are translated to a
+//! function call to an SMT bv operator
+//!
+//! The `expected` file checks some elements of the expected output Boogie.
+//!
+//! This is a possible Boogie output (which may change with MIR changes):
+//! ```
+//! function {:bvbuiltin "bvslt"} $BvSignedLessThan<T>(lhs: T, rhs: T) returns (bool);
+//!
+//! function {:bvbuiltin "bvsgt"} $BvSignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
+//!
+//! function {:bvbuiltin "bvor"} $BvOr<T>(lhs: T, rhs: T) returns (T);
+//!
+//! // Procedures:
+//! procedure _RNvCshNorBqfmMTU_4test14check_binop_gt()
+//! {
+//!   var _1: bv32;
+//!   var _2: bv32;
+//!   var _4: bool;
+//!   var z: bv32;
+//!   var _7: bool;
+//!   _1 := 1bv32;
+//!   _2 := 2bv32;
+//!   _4 := $BvSignedGreaterThan(_2, _1);
+//!   assert _4;
+//!   z := $BvAnd(_1, _2);
+//!   _7 := $BvSignedLessThan(_1, z);
+//!   assert _7;
+//!   return;
+//! }
+//!
+//! ````
+
+#[kani::proof]
+fn check_binop_gt() {
+    let x = 1;
+    let y = 2;
+    kani::assert(y > x, "");
+    let z = x | y;
+    kani::assert(x < z, "");
+}