[Boogie Backend] Add support for int-to-int casts (#2957)

Add support for int-to-int cast operations (MIR's `Rvalue::Cast` with
the `CastKind::IntToInt` kind) through implementing them as
extracts/concats in Boogie.

The PR also includes another unbounded verification example involving
the serialization of an array of words into a buffer of bytes, which
involves int-to-int cast operations.

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

boogie_ast/src/boogie_program/mod.rs

@@ -138,6 +138,9 @@ pub enum BinaryOp {
 
  /// Modulo
  Mod,
+
+ /// Bit-Vector Concat
+ Concat,
 }
 
 /// Expr types
@@ -155,6 +158,9 @@ pub enum Expr {
  /// Binary operation
  BinaryOp { op: BinaryOp, left: Box<Expr>, right: Box<Expr> },
 
+ /// Bit-vector extract operation, e.g. `x[7:2]` (half-open interval)
+ Extract { base: Box<Expr>, high: usize, low: usize },
+
  /// Function call
  FunctionCall { symbol: String, arguments: Vec<Expr> },
 
@@ -170,9 +176,26 @@ impl Expr {
  Expr::Literal(l)
  }
 
+ pub fn concat(e1: Box<Expr>, e2: Box<Expr>) -> Self {
+ Expr::BinaryOp { op: BinaryOp::Concat, left: e1, right: e2 }
+ }
+
+ pub fn extract(base: Box<Expr>, high: usize, low: usize) -> Self {
+ Expr::Extract { base, high, low }
+ }
+
  pub fn function_call(symbol: String, arguments: Vec<Expr>) -> Self {
  Expr::FunctionCall { symbol, arguments }
  }
+
+ pub fn sign_extend(e: Box<Expr>, _width: usize) -> Self {
+ let _e = e;
+ todo!()
+ }
+
+ pub fn zero_extend(e: Box<Expr>, width: usize) -> Self {
+ Expr::concat(Box::new(Expr::literal(Literal::bv(width, 0.into()))), e)
+ }
 }
 
 impl ToString for Expr {

boogie_ast/src/boogie_program/writer.rs

@@ -300,6 +300,11 @@ impl Expr {
  right.write_to(writer)?;
  write!(writer, ")")?;
  }
+ Expr::Extract { base, high, low } => {
+ write!(writer, "(")?;
+ base.write_to(writer)?;
+ write!(writer, ")[{high}:{low}]")?;
+ }
  Expr::FunctionCall { symbol, arguments } => {
  write!(writer, "{symbol}(")?;
  for (i, a) in arguments.iter().enumerate() {
@@ -521,6 +526,7 @@ impl BinaryOp {
  BinaryOp::Gt => write!(writer, ">")?,
  BinaryOp::Lte => write!(writer, "<=")?,
  BinaryOp::Gte => write!(writer, ">=")?,
+ BinaryOp::Concat => write!(writer, "++")?,
  }
  Ok(())
  }

kani-compiler/src/codegen_boogie/context/boogie_ctx.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use itertools::Itertools;
+use std::cmp::Ordering;
 use std::io::Write;
 
 use crate::kani_queries::QueryDb;
@@ -13,7 +14,7 @@ use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::mir::interpret::Scalar;
 use rustc_middle::mir::traversal::reverse_postorder;
 use rustc_middle::mir::{
- BasicBlock, BasicBlockData, BinOp, Body, Const as mirConst, ConstOperand, ConstValue,
+ BasicBlock, BasicBlockData, BinOp, Body, CastKind, Const as mirConst, ConstOperand, ConstValue,
  HasLocalDecls, Local, Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind,
  SwitchTargets, Terminator, TerminatorKind, UnOp, VarDebugInfoContents,
 };
@@ -321,6 +322,28 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
  // TODO: handle overflow check
  self.codegen_binary_op(binop, e1, e2)
  }
+ Rvalue::Cast(kind, operand, ty) => {
+ if *kind == CastKind::IntToInt {
+ let from_type = self.operand_ty(operand);
+ let o = self.codegen_operand(operand);
+ let from = self.codegen_type(from_type);
+ let to = self.codegen_type(*ty);
+ let Type::Bv(from_width) = from else { panic!("Expecting bv type in cast") };
+ let Type::Bv(to_width) = to else { panic!("Expecting bv type in cast") };
+ let op = match from_width.cmp(&to_width) {
+ Ordering::Greater => Expr::extract(Box::new(o), to_width, 0),
+ Ordering::Less => match from_type.kind() {
+ ty::Int(_) => Expr::sign_extend(Box::new(o), to_width - from_width),
+ ty::Uint(_) => Expr::zero_extend(Box::new(o), to_width - from_width),
+ _ => todo!(),
+ },
+ Ordering::Equal => o,
+ };
+ (None, op)
+ } else {
+ todo!()
+ }
+ }
  _ => todo!(),
  }
  }

tests/script-based-boogie/unbounded_array_serde/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/unbounded_array_serde/expected

@@ -0,0 +1,69 @@
+// Datatypes:
+datatype $Array<T> { $Array(data: [bv64]T, len: bv64) }
+
+// Functions:
+function {:bvbuiltin "bvult"} $BvUnsignedLessThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvslt"} $BvSignedLessThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvugt"} $BvUnsignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvsgt"} $BvSignedGreaterThan<T>(lhs: T, rhs: T) returns (bool);
+
+function {:bvbuiltin "bvadd"} $BvAdd<T>(lhs: T, rhs: T) returns (T);
+
+function {:bvbuiltin "bvor"} $BvOr<T>(lhs: T, rhs: T) returns (T);
+
+function {:bvbuiltin "bvand"} $BvAnd<T>(lhs: T, rhs: T) returns (T);
+
+function {:bvbuiltin "bvshl"} $BvShl<T>(lhs: T, rhs: T) returns (T);
+
+function {:bvbuiltin "bvlshr"} $BvShr<T>(lhs: T, rhs: T) returns (T);
+
+// Procedures:
+procedure
+{
+ var src: $Array bv16;
+ var buf: $Array bv8;
+ var src_len: bv64;
+ var buf_len: bv64;
+ var i: bv64;
+ var x: bv16;
+ var byte0: bv8;
+ var byte1: bv8;
+ var j: bv64;
+ var dst: $Array bv16;
+ bb
+ havoc src; 
+ goto bb
+ havoc buf; 
+ src_len := src->len;
+ buf_len := buf->len;
+ := $BvShr(buf_len, 1bv64);
+ := !($BvUnsignedLessThan(
+ assume
+ i := 0bv64;
+ := $BvUnsignedLessThan(
+ if (\
+ goto bb\
+ } else {
+ goto bb\
+ }
+ havoc dst; 
+ return;
+ := src->data[
+ := dst->data[
+ assert
+ := $BvAdd(i, 1bv64);
+ := $BvShl(
+ := buf->data[
+ := (0bv8 ++
+ := $BvOr(
+ := $BvAnd(x, 255bv16);
+ )[8:0];
+ := $BvShr(x, 8bv16);
+ byte1 :=
+ j := $BvShl(
+ buf->data[(j)] := byte0;
+ := $BvAdd(j, 1bv64);
+}

tests/script-based-boogie/unbounded_array_serde/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/unbounded_array_serde/test.rs

@@ -0,0 +1,50 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! A test that demonstrates unbounded verification of array-based programs.
+//! The test uses `any_array` which creates arrays with non-deterministic
+//! content and length.
+//! The `src` array of words is serialized into the `buf` byte array and then
+//! deserialized back into `dst`.
+//! The test checks that the round trip of serialization and deserialization is
+//! the identity.
+
+#[kani::proof]
+fn serde() {
+ let src = kani::array::any_array::<u16>();
+ let mut buf = kani::array::any_array::<u8>();
+ let src_len: usize = src.len();
+ let buf_len: usize = buf.len();
+ kani::assume(buf_len >> 1u64 >= src_len);
+
+ // serialize
+ let mut i: usize = 0;
+ //Loop_invariant: forall j: usize :: j < i => ((buf[j << 1u64 + 1] ++ buf[j << 1u64]) == src[j])
+ while i < src_len {
+ let x = src[i];
+ let byte0: u8 = (x & 0xFF) as u8;
+ let byte1: u8 = ((x >> 8u16) & 0xFF) as u8;
+ let j: usize = i << 1u64;
+ buf[j] = byte0;
+ buf[j + 1] = byte1;
+ i += 1;
+ }
+
+ // deserialize
+ let mut dst = kani::array::any_array::<u16>();
+ kani::assume(dst.len() >= src_len);
+ i = 0;
+ //Loop_invariant: forall j: usize :: j < i => ((buf[j << 1u64 + 1] ++ buf[j << 1u64]) == dst[j])
+ while i < src_len {
+ let j: usize = i << 1u64;
+ dst[i] = ((buf[j + 1] as u16) << 8u16) | (buf[j] as u16);
+ i += 1;
+ }
+
+ // Check the round trip
+ i = 0;
+ while i < src_len {
+ kani::assert(src[i] == dst[i], "serialization/deserialization failed");
+ i += 1;
+ }
+}