diff --git a/.buildkite/common.py b/.buildkite/common.py index 1c663cdd74c..2e47ce420be 100644 --- a/.buildkite/common.py +++ b/.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): diff --git a/.buildkite/pipeline_pr.py b/.buildkite/pipeline_pr.py index 5b4693f51bd..5943b92e327 100755 --- a/.buildkite/pipeline_pr.py +++ b/.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", diff --git a/src/vmm/src/arch/x86_64/interrupts.rs b/src/vmm/src/arch/x86_64/interrupts.rs index 8b7bf8bc793..8deb5a9d44e 100644 --- a/src/vmm/src/arch/x86_64/interrupts.rs +++ b/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 { diff --git a/src/vmm/src/dumbo/pdu/ethernet.rs b/src/vmm/src/dumbo/pdu/ethernet.rs index f93a0c5d007..bec283bbd56 100644 --- a/src/vmm/src/dumbo/pdu/ethernet.rs +++ b/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::(); diff --git a/src/vmm/src/utils/byte_order.rs b/src/vmm/src/utils/byte_order.rs index 32aa9daee18..c0682c494df 100644 --- a/src/vmm/src/utils/byte_order.rs +++ b/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); } diff --git a/tests/integration_tests/test_kani.py b/tests/integration_tests/test_kani.py index 35c84e105b6..9b087a5375f 100644 --- a/tests/integration_tests/test_kani.py +++ b/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")