[1.11] backport Kani fixes

.buildkite/common.py

@@ -179,6 +179,12 @@ def __call__(self, parser, namespace, value, option_string=None):
     default=None,
     type=str,
 )
+COMMON_PARSER.add_argument(
+    "--no-kani",
+    help="Don't add kani step",
+    action="store_true",
+    default=False,
+)
 
 
 def random_str(k: int):

.buildkite/pipeline_pr.py

@@ -48,8 +48,10 @@
         "./tools/devtool -y make_release",
     )
 
-if not changed_files or any(
-    x.suffix in [".rs", ".toml", ".lock"] for x in changed_files
+if not pipeline.args.no_kani and (
+    not changed_files
+    or any(x.suffix in [".rs", ".toml", ".lock"] for x in changed_files)
+    or any(x.parent.name == "devctr" for x in changed_files)
 ):
     kani_grp = pipeline.build_group(
         "🔍 Kani",

src/vmm/src/arch/x86_64/interrupts.rs

@@ -7,6 +7,7 @@
 
 use kvm_bindings::kvm_lapic_state;
 use kvm_ioctls::VcpuFd;
+use zerocopy::IntoBytes;
 
 use crate::utils::byte_order;
 
@@ -28,13 +29,13 @@ const APIC_MODE_EXTINT: u32 = 0x7;
 fn get_klapic_reg(klapic: &kvm_lapic_state, reg_offset: usize) -> u32 {
     let range = reg_offset..reg_offset + 4;
     let reg = klapic.regs.get(range).expect("get_klapic_reg range");
-    byte_order::read_le_u32_from_i8(reg)
+    byte_order::read_le_u32(reg.as_bytes())
 }
 
 fn set_klapic_reg(klapic: &mut kvm_lapic_state, reg_offset: usize, value: u32) {
     let range = reg_offset..reg_offset + 4;
     let reg = klapic.regs.get_mut(range).expect("set_klapic_reg range");
-    byte_order::write_le_u32_to_i8(reg, value)
+    byte_order::write_le_u32(reg.as_mut_bytes(), value);
 }
 
 fn set_apic_delivery_mode(reg: u32, mode: u32) -> u32 {

src/vmm/src/dumbo/pdu/ethernet.rs

@@ -255,16 +255,6 @@ mod kani_proofs {
         }
     }
 
-    mod stubs {
-        // The current implementation of read_be_u16 function leads to a significant
-        // performance degradation given a necessary loop unrolling. Using this stub,
-        // we read the same information from the buffer while avoiding the loop, thus,
-        // notably improving performance.
-        pub fn read_be_u16(input: &[u8]) -> u16 {
-            u16::from_be_bytes([input[0], input[1]])
-        }
-    }
-
     // We consider the MMDS Network Stack spec for all postconditions in the harnesses.
     // See https://github.com/firecracker-microvm/firecracker/blob/main/docs/mmds/mmds-design.md#mmds-network-stack
 
@@ -519,7 +509,6 @@ mod kani_proofs {
 
     #[kani::proof]
     #[kani::solver(cadical)]
-    #[kani::stub(crate::utils::byte_order::read_be_u16, stubs::read_be_u16)]
     fn verify_with_payload_len_unchecked() {
         // Create non-deterministic stream of bytes up to MAX_FRAME_SIZE
         let mut bytes: [u8; MAX_FRAME_SIZE] = kani::Arbitrary::any_array::<MAX_FRAME_SIZE>();

src/vmm/src/utils/byte_order.rs

@@ -5,13 +5,9 @@ macro_rules! generate_read_fn {
     ($fn_name: ident, $data_type: ty, $byte_type: ty, $type_size: expr, $endian_type: ident) => {
         /// Read bytes from the slice
         pub fn $fn_name(input: &[$byte_type]) -> $data_type {
-            assert!($type_size == std::mem::size_of::<$data_type>());
-            let mut array = [0u8; $type_size];
-            #[allow(clippy::cast_sign_loss)]
-            #[allow(clippy::cast_possible_wrap)]
-            for (byte, read) in array.iter_mut().zip(input.iter().cloned()) {
-                *byte = read as u8;
-            }
+            let mut array = [0u8; std::mem::size_of::<$data_type>()];
+            let how_many = input.len().min(std::mem::size_of::<$data_type>());
+            array[..how_many].copy_from_slice(&input[..how_many]);
             <$data_type>::$endian_type(array)
         }
     };
@@ -21,32 +17,21 @@ macro_rules! generate_write_fn {
     ($fn_name: ident, $data_type: ty, $byte_type: ty, $endian_type: ident) => {
         /// Write bytes to the slice
         pub fn $fn_name(buf: &mut [$byte_type], n: $data_type) {
-            #[allow(clippy::cast_sign_loss)]
-            #[allow(clippy::cast_possible_wrap)]
-            for (byte, read) in buf
-                .iter_mut()
-                .zip(<$data_type>::$endian_type(n).iter().cloned())
-            {
-                *byte = read as $byte_type;
-            }
+            let bytes = n.$endian_type();
+            let how_much = buf.len().min(bytes.len());
+            buf[..how_much].copy_from_slice(&bytes[..how_much]);
         }
     };
 }
 
-generate_read_fn!(read_le_u16, u16, u8, 2, from_le_bytes);
 generate_read_fn!(read_le_u32, u32, u8, 4, from_le_bytes);
-generate_read_fn!(read_le_u32_from_i8, u32, i8, 4, from_le_bytes);
 generate_read_fn!(read_le_u64, u64, u8, 8, from_le_bytes);
-generate_read_fn!(read_le_i32, i32, i8, 4, from_le_bytes);
 
 generate_read_fn!(read_be_u16, u16, u8, 2, from_be_bytes);
 generate_read_fn!(read_be_u32, u32, u8, 4, from_be_bytes);
 
-generate_write_fn!(write_le_u16, u16, u8, to_le_bytes);
 generate_write_fn!(write_le_u32, u32, u8, to_le_bytes);
-generate_write_fn!(write_le_u32_to_i8, u32, i8, to_le_bytes);
 generate_write_fn!(write_le_u64, u64, u8, to_le_bytes);
-generate_write_fn!(write_le_i32, i32, i8, to_le_bytes);
 
 generate_write_fn!(write_be_u16, u16, u8, to_be_bytes);
 generate_write_fn!(write_be_u32, u32, u8, to_be_bytes);
@@ -110,10 +95,8 @@ mod tests {
         };
     }
 
-    byte_order_test_read_write!(test_le_u16, write_le_u16, read_le_u16, false, u16);
     byte_order_test_read_write!(test_le_u32, write_le_u32, read_le_u32, false, u32);
     byte_order_test_read_write!(test_le_u64, write_le_u64, read_le_u64, false, u64);
-    byte_order_test_read_write!(test_le_i32, write_le_i32, read_le_i32, false, i32);
     byte_order_test_read_write!(test_be_u16, write_be_u16, read_be_u16, true, u16);
     byte_order_test_read_write!(test_be_u32, write_be_u32, read_be_u32, true, u32);
 }

tests/integration_tests/test_kani.py

@@ -13,10 +13,12 @@
 
 PLATFORM = platform.machine()
 
+TIMEOUT = 3600
+
 
 # The `check_output` timeout will always fire before this one, but we need to
 # set a timeout here to override the default pytest timeout of 180s.
-@pytest.mark.timeout(2420)
+@pytest.mark.timeout(TIMEOUT)
 @pytest.mark.skipif(
     os.environ.get("BUILDKITE") != "true",
     reason="Kani's memory requirements likely cannot be satisfied locally",
@@ -27,13 +29,13 @@ def test_kani(results_dir):
     """
     # -Z stubbing is required to enable the stubbing feature
     # -Z function-contracts is required to enable the function contracts feature
-    # --restrict-vtable is required for some virtio queue proofs, which go out of memory otherwise
+    # -Z restrict-vtable is required for some virtio queue proofs, which go out of memory otherwise
     # -j enables kani harnesses to be verified in parallel (required to keep CI time low)
     # --output-format terse is required by -j
-    # --enable-unstable is needed to enable `-Z` flags
+    # -Z unstable-options is needed to enable the other `-Z` flags
     _, stdout, _ = utils.check_output(
-        "cargo kani --enable-unstable -Z stubbing -Z function-contracts --restrict-vtable -j --output-format terse",
-        timeout=2400,
+        "cargo kani -Z unstable-options -Z stubbing -Z function-contracts -Z restrict-vtable -j --output-format terse",
+        timeout=TIMEOUT,
     )
 
     (results_dir / "kani_log").write_text(stdout, encoding="utf-8")