search

rust-osdev / x86_64

Library to program x86_64 hardware.
https://docs.rs/x86_64
Apache License 2.0
797 stars 132 forks source link

Add automatically generated Kani harnesses #497

Closed cvick32 closed 2 months ago

cvick32 commented 2 months ago

Adds 147 Kani harnesses and all corresponding Arbitrary derivations. These harnesses were automatically generated by a tool currently under development by the Kani team.

Summary of running cargo kani listed below.

Summary:

Verification failed for - addr::kani_harnesses::kani_harness_42_sub
Verification failed for - addr::kani_harnesses::kani_harness_41_sub_assign
Verification failed for - addr::kani_harnesses::kani_harness_40_sub
Verification failed for - addr::kani_harnesses::kani_harness_39_add_assign
Verification failed for - addr::kani_harnesses::kani_harness_38_add
Verification failed for - addr::kani_harnesses::kani_harness_37_is_aligned_u64
Verification failed for - addr::kani_harnesses::kani_harness_36_align_down_u64
Verification failed for - addr::kani_harnesses::kani_harness_29_new
Verification failed for - addr::kani_harnesses::kani_harness_25_sub
Verification failed for - addr::kani_harnesses::kani_harness_24_sub_assign
Verification failed for - addr::kani_harnesses::kani_harness_23_sub
Verification failed for - addr::kani_harnesses::kani_harness_22_add_assign
Verification failed for - addr::kani_harnesses::kani_harness_21_add
Verification failed for - addr::kani_harnesses::kani_harness_12_is_aligned_u64
Verification failed for - addr::kani_harnesses::kani_harness_11_align_down_u64
Verification failed for - addr::kani_harnesses::kani_harness_2_new
Verification failed for - addr::kani_harnesses::kani_harness_1_align_up
Verification failed for - addr::kani_harnesses::kani_harness_0_align_down
Verification failed for - kani_harnesses::kani_harness_620_from_u16
Verification failed for - structures::idt::kani_harnesses::kani_harness_490_stack_index
Verification failed for - structures::idt::kani_harnesses::kani_harness_489_set_stack_index
Verification failed for - structures::paging::frame::kani_harnesses::kani_harness_539_next
Verification failed for - structures::paging::frame::kani_harnesses::kani_harness_538_next
Verification failed for - structures::paging::frame::kani_harnesses::kani_harness_536_sub_assign
Verification failed for - structures::paging::frame::kani_harnesses::kani_harness_535_sub
Verification failed for - structures::paging::frame::kani_harnesses::kani_harness_534_add_assign
Verification failed for - structures::paging::frame::kani_harnesses::kani_harness_533_add
Verification failed for - structures::paging::page::kani_harnesses::kani_harness_560_next
Verification failed for - structures::paging::page::kani_harnesses::kani_harness_558_next
Verification failed for - structures::paging::page::kani_harnesses::kani_harness_553_sub_assign
Verification failed for - structures::paging::page::kani_harnesses::kani_harness_552_sub
Verification failed for - structures::paging::page::kani_harnesses::kani_harness_551_add_assign
Verification failed for - structures::paging::page::kani_harnesses::kani_harness_550_add
Verification failed for - structures::paging::page_table::kani_harnesses::kani_harness_612_new
Verification failed for - structures::paging::page_table::kani_harnesses::kani_harness_611_backward_checked
Verification failed for - structures::paging::page_table::kani_harnesses::kani_harness_606_new
Complete - 111 successfully verified harnesses, 36 failures, 147 total.
Freax13 commented 2 months ago

Thank you for your contribution!

Generating tests automatically is certainly a cool idea, but nonetheless I'm proposing to close this PR for the following reasons: This PR adds a very, very large chunk of auto-generated code that I'm guessing none of the maintainers have a high interest in maintaining. Furthermore, I don't think we'd want to expect contributors to update the kani proofs around the code they're changing. So far, we've only been using Kani for a few proofs, I don't think anyone has ever expressed interest in proofing the whole project. Some additional feedback: I'm not sure if the Arbitrary derives have been auto-generated as well, but some of them are wrong (e.g. not all bit patterns are valid for VirtAddr). It'd be cool if it was possible to maintain the proofs (and the code needed to support them e.g. derives) out of tree, that way normal development wouldn't be affected so drastically like I think it would be following this PR.

cvick32 commented 2 months ago

Thanks so much for your feedback!

Your idea of keeping the auto-generated code out of tree is a great one. I think that having a CI action that generates and runs these harnesses would allow you to reap the benefits of higher coverage without having to maintain the large amount of auto-generated code. Would that be something you were interested in? Let me know I'll make sure to keep you updated on that effort.

The Arbitrary derivations were auto-generated as well. Since I don't have a way of knowing all the implicit constraints on a type, like not all bit patterns being valid for VirtAddr, it leads to many spurious violations. I think that most of the failing proofs are spurious for this reason.

However, I'm curious about the following examples, and if you think that kani was justified in failing in these cases. Both cases have to do with address subtraction and their respective reproductions are listed below. Note that both of these examples panic because unwrap is called on a None value.

use std::ops::Sub;
use x86_64::PhysAddr;

fn main() {
    let p_lhs = PhysAddr::new(0x0);
    let p_rhs = PhysAddr::new(0x1);

    p_lhs.sub(p_rhs);
}
use std::ops::Sub;
use x86_64::VirtAddr;

fn main() {
    let v_lhs = VirtAddr::new(0x0);
    let v_rhs = VirtAddr::new(0x1);

    v_lhs.sub(p_rhs);
}
Freax13 commented 2 months ago

Thanks so much for your feedback!

Your idea of keeping the auto-generated code out of tree is a great one. I think that having a CI action that generates and runs these harnesses would allow you to reap the benefits of higher coverage without having to maintain the large amount of auto-generated code.

I'm not sure if auto-generating the harnesses in a CI job will always work: As we've seen here deriving Arbitrary doesn't always work because types may have internal invariants. If the CI action generates these invalid derives, there are probably many spuriously failing tests that make it difficult to focus on the cases that correctly point out bugs.

What I meant by "out of tree" was it'd be great if it was possible to have the harnesses (as well as any code needed to support them) in a separate repo outside the main project. That way it'd still be possible to define test-cases manually (or have the test cases be generated and then manually fixed) without holding up regular development.

Would that be something you were interested in? Let me know I'll make sure to keep you updated on that effort.

I'm interested in that and would appreciate being updated, thanks!

However, I'm curious about the following examples, and if you think that kani was justified in failing in these cases. Both cases have to do with address subtraction and their respective reproductions are listed below. Note that both of these examples panic because unwrap is called on a None value.

use std::ops::Sub;
use x86_64::PhysAddr;

fn main() {
    let p_lhs = PhysAddr::new(0x0);
    let p_rhs = PhysAddr::new(0x1);

    p_lhs.sub(p_rhs);
}
use std::ops::Sub;
use x86_64::VirtAddr;

fn main() {
    let v_lhs = VirtAddr::new(0x0);
    let v_rhs = VirtAddr::new(0x1);

    v_lhs.sub(p_rhs);
}

We expect both of these to panic (1, 2). VirtAddr could technically wrap, but PhyAddr can't because the resulting value wouldn't be valid (this MSB can't be set with PhysAddr).