fix: handle panics for bit_vector (#2334)

Author: Marsman1996

source/rust_verify_test/tests/bitvector.rs

@@ -245,6 +245,32 @@ test_verify_one_bv_file! {
     } => Ok(())
 }
 
+test_verify_one_bv_file! {
+    #[test] strslice_len_not_supported_in_by_bit_vector verus_code! {
+        proof fn test() {
+            use verus_builtin::*;
+            assert(strslice_len::<u64>(7u64) == 0int) by(bit_vector);
+        }
+    } => Err(err) => assert_vir_error_msg(err, "string slice length not supported in bit_vector assert")
+}
+
+test_verify_one_bv_file! {
+    #[test] float_to_bits_not_supported_in_by_bit_vector verus_code! {
+        proof fn test() {
+            use verus_builtin::*;
+            assert(f32_to_bits(0.0f32) == 0u32) by(bit_vector);
+        }
+    } => Err(err) => assert_vir_error_msg(err, "float-to-bits coercion not supported in bit_vector assert")
+}
+
+test_verify_one_bv_file! {
+    #[test] real_to_int_not_supported_in_by_bit_vector verus_code! {
+        proof fn test() {
+            assert(1.0real.floor() == 1int) by(bit_vector);
+        }
+    } => Err(err) => assert_vir_error_msg(err, "real-to-int coercion not supported in bit_vector assert")
+}
+
 test_verify_one_bv_file! {
     #[test] usize_cast_in_by_bit_vector verus_code! {
         proof fn test_usize(x: u64) {

source/vir/src/bitvector_to_air.rs

@@ -442,9 +442,24 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<BvExpr, Vir
                 let bv_typ = if is_bool { BvTyp::Bool } else { bv_typ };
                 Ok(BvExpr { expr: Arc::new(ExprX::Unary(op, expr)), bv_typ })
             }
-            UnaryOp::IntToReal => panic!("internal error: unexpected int to real coercion"),
-            UnaryOp::RealToInt => panic!("internal error: unexpected real to int coercion"),
-            UnaryOp::FloatToBits => panic!("internal error: unexpected float to bits coercion"),
+            UnaryOp::IntToReal => {
+                return Err(error(
+                    &exp.span,
+                    "int-to-real coercion not supported in bit_vector assert",
+                ));
+            }
+            UnaryOp::RealToInt => {
+                return Err(error(
+                    &exp.span,
+                    "real-to-int coercion not supported in bit_vector assert",
+                ));
+            }
+            UnaryOp::FloatToBits => {
+                return Err(error(
+                    &exp.span,
+                    "float-to-bits coercion not supported in bit_vector assert",
+                ));
+            }
             UnaryOp::HeightTrigger => panic!("internal error: unexpected HeightTrigger"),
             UnaryOp::Trigger(_) => bv_exp_to_expr(ctx, state, arg),
             UnaryOp::CoerceMode { .. } => {
@@ -453,11 +468,17 @@ fn bv_exp_to_expr(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<BvExpr, Vir
             UnaryOp::MustBeFinalized | UnaryOp::MustBeElaborated => {
                 panic!("internal error: Exp not finalized: {:?}", arg)
             }
-            UnaryOp::StrLen => panic!(
-                "internal error: matching for bit vector ops on this match should be impossible"
-            ),
+            UnaryOp::StrLen => {
+                return Err(error(
+                    &exp.span,
+                    "string slice length not supported in bit_vector assert",
+                ));
+            }
             UnaryOp::InferSpecForLoopIter { .. } => {
-                panic!("internal error: unexpected Option type (from InferSpecForLoopIter)")
+                return Err(error(
+                    &exp.span,
+                    "loop-iterator inference hint not supported in bit_vector assert",
+                ));
             }
             UnaryOp::CastToInteger => {
                 panic!("internal error: unexpected CastToInteger")