[Boogie Backend] Add two Boogie tests (#2914)

Add a new script-based suite for running Boogie tests. Since we don't
have Boogie integrated in our CI or the Kani driver, this suite just
checks that the generated Boogie file contains certain lines that we're
expecting.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

.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

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, "");
+}