From beeeefbf78c9eb041138609a3c813e2f8cd79678 Mon Sep 17 00:00:00 2001 From: Egor Lazarchuk Date: Thu, 6 Mar 2025 10:56:55 +0000 Subject: [PATCH 1/6] feat: add option to not add kani bk step In some cases running kani steps is not useful and only results in longer pipeline runs. Add option to disable it if needed. (cherry picked from commit 83119b8ad9f7bfd613d9d5d43bb0ee7426b50ab6) Signed-off-by: Egor Lazarchuk --- .buildkite/common.py | 6 ++++++ .buildkite/pipeline_pr.py | 5 +++-- 2 files changed, 9 insertions(+), 2 deletions(-) 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..46a8f6880be 100755 --- a/.buildkite/pipeline_pr.py +++ b/.buildkite/pipeline_pr.py @@ -48,8 +48,9 @@ "./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) ): kani_grp = pipeline.build_group( "🔍 Kani", From 129571dfc72d255df7fbdc4234cd4dccef7e65e1 Mon Sep 17 00:00:00 2001 From: Egor Lazarchuk Date: Thu, 6 Mar 2025 11:03:34 +0000 Subject: [PATCH 2/6] chore: increase timeout for kani tests Kani tests run very close to the current timeout values. Increase timeout to 1h. (cherry picked from commit ed0d202f43987f5f01c0db47a35826352e5bfae6) Signed-off-by: Egor Lazarchuk --- tests/integration_tests/test_kani.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/integration_tests/test_kani.py b/tests/integration_tests/test_kani.py index 35c84e105b6..0583fa4837b 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", @@ -33,7 +35,7 @@ def test_kani(results_dir): # --enable-unstable is needed to enable `-Z` flags _, stdout, _ = utils.check_output( "cargo kani --enable-unstable -Z stubbing -Z function-contracts --restrict-vtable -j --output-format terse", - timeout=2400, + timeout=TIMEOUT, ) (results_dir / "kani_log").write_text(stdout, encoding="utf-8") From 8812502605f34e8f088e8a188fd1ade93379de5e Mon Sep 17 00:00:00 2001 From: Patrick Roy Date: Thu, 13 Mar 2025 12:07:50 +0000 Subject: [PATCH 3/6] kani: stop using deprecated cli args --enable-unstable and --restrict-vtable got deprecated in kani 0.59.0 in favor of variants based on -Z flags. So use the -Z flags instead (cherry picked from commit 8495af962404da2fbea7621cd8d44dfd7be21f1b) Signed-off-by: Patrick Roy --- tests/integration_tests/test_kani.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/integration_tests/test_kani.py b/tests/integration_tests/test_kani.py index 0583fa4837b..9b087a5375f 100644 --- a/tests/integration_tests/test_kani.py +++ b/tests/integration_tests/test_kani.py @@ -29,12 +29,12 @@ 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", + "cargo kani -Z unstable-options -Z stubbing -Z function-contracts -Z restrict-vtable -j --output-format terse", timeout=TIMEOUT, ) From 5681ec0745a478ef00ca702e02f367faab48c16b Mon Sep 17 00:00:00 2001 From: Patrick Roy Date: Thu, 13 Mar 2025 13:43:43 +0000 Subject: [PATCH 4/6] buildkite: run kani if devctr is modified rebuilding the docker container can upgrade kani, and we'd like to know at the PR stage if that causes issues (such as timeouts). (cherry picked from commit 0fff2c8884a6f0839170c01c192574df2418ba95) Signed-off-by: Patrick Roy --- .buildkite/pipeline_pr.py | 1 + 1 file changed, 1 insertion(+) diff --git a/.buildkite/pipeline_pr.py b/.buildkite/pipeline_pr.py index 46a8f6880be..5943b92e327 100755 --- a/.buildkite/pipeline_pr.py +++ b/.buildkite/pipeline_pr.py @@ -51,6 +51,7 @@ 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", From 0f88d3a4d6f8fc48b7e50cdc283305e9c573bcdd Mon Sep 17 00:00:00 2001 From: Patrick Roy Date: Thu, 13 Mar 2025 14:22:01 +0000 Subject: [PATCH 5/6] refactor: stop using loops in byte_order.rs Instead of copying the buffers byte-by-byte in a loop, just use copy_from_slice, which compiles to a memcpy. While we're at it, drop some unused function definitions. Also remove the special snowflake functions for dealing with i8 slices, and instead just use zerocopy to safely transmute these into u8 slices, on which the normal functions work. (cherry picked from commit 35d6afd2f6ac11c932e5081b810db82576abe664) Signed-off-by: Patrick Roy --- src/vmm/src/arch/x86_64/interrupts.rs | 5 +++-- src/vmm/src/utils/byte_order.rs | 29 ++++++--------------------- 2 files changed, 9 insertions(+), 25 deletions(-) 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/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); } From 1452ec2d31a9bef5944903aa5a4c9cb3377b9465 Mon Sep 17 00:00:00 2001 From: Patrick Roy Date: Thu, 13 Mar 2025 14:26:29 +0000 Subject: [PATCH 6/6] kani: remove stubbing from dumbo harnesses with the byte_order modules no longer using loops, this is no longer needed. (cherry picked from commit dd0d9328341b636c634da5fb028c7f46bdd424cd) Signed-off-by: Patrick Roy --- src/vmm/src/dumbo/pdu/ethernet.rs | 11 ----------- 1 file changed, 11 deletions(-) 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::();