List Subcommand (Implementation)

[carolynzech]

Implementation of the list subcommand (and updates to the RFC).

As a larger test, I ran on the standard library (kani list -Z list -Z function-contracts -Z mem-predicates ./library --std) and manually verified that the results were correct. I pasted the output below.

Contracts:

	Function	Contract Harnesses (#[kani::proof_for_contract])
	alloc::layout::Layout::from_size_align_unchecked	alloc::layout::verify::check_from_size_align_unchecked
	ascii::ascii_char::AsciiChar::from_u8	ascii::ascii_char::verify::check_from_u8
	ascii::ascii_char::AsciiChar::from_u8_unchecked	ascii::ascii_char::verify::check_from_u8_unchecked
	char::convert::from_u32_unchecked	char::convert::verify::check_from_u32_unchecked
	char::methods::verify::as_ascii_clone	char::methods::verify::check_as_ascii_ascii_char
		char::methods::verify::check_as_ascii_non_ascii_char
	intrinsics::typed_swap	intrinsics::verify::check_typed_swap_u8
		intrinsics::verify::check_typed_swap_char
		intrinsics::verify::check_typed_swap_non_zero
	mem::swap	mem::verify::check_swap_primitive
		mem::verify::check_swap_adt_no_drop
	ptr::align_offset	ptr::verify::check_align_offset_zst
		ptr::verify::check_align_offset_u8
		ptr::verify::check_align_offset_u16
		ptr::verify::check_align_offset_u32
		ptr::verify::check_align_offset_u64
		ptr::verify::check_align_offset_u128
		ptr::verify::check_align_offset_4096
		ptr::verify::check_align_offset_5
	ptr::alignment::Alignment::as_nonzero	ptr::alignment::verify::check_as_nonzero
	ptr::alignment::Alignment::as_usize	ptr::alignment::verify::check_as_usize
	ptr::alignment::Alignment::log2	ptr::alignment::verify::check_log2
	ptr::alignment::Alignment::mask	ptr::alignment::verify::check_mask
	ptr::alignment::Alignment::new	ptr::alignment::verify::check_new
	ptr::alignment::Alignment::new_unchecked	ptr::alignment::verify::check_new_unchecked
	ptr::alignment::Alignment::of	ptr::alignment::verify::check_of_i32
	ptr::non_null::NonNull::::new	ptr::non_null::verify::non_null_check_new
	ptr::non_null::NonNull::::new_unchecked	ptr::non_null::verify::non_null_check_new_unchecked
	ptr::read_volatile	ptr::verify::check_read_u128
	ptr::unique::Unique::::as_non_null_ptr	ptr::unique::verify::check_as_non_null_ptr
	ptr::unique::Unique::::as_ptr	ptr::unique::verify::check_as_ptr
	ptr::unique::Unique::::new	ptr::unique::verify::check_new
	ptr::unique::Unique::::new_unchecked	ptr::unique::verify::check_new_unchecked
	ptr::verify::mod_inv_copy	ptr::verify::check_mod_inv
	ptr::write_volatile	NONE
Total	24	34

Standard Harnesses (#[kani::proof]):

1. ptr::unique::verify::check_as_mut
2. ptr::unique::verify::check_as_ref
3. ptr::unique::verify::check_cast

Terminal view (--pretty format):

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

I would prefer if the compiler is not aware that this is a list command.

[celinval]

What is # of contracts? Why does mem::swap has 0?

[carolynzech]

What is # of contracts? Why does mem::swap has 0?

@celinval Number of contracts is the number of contracts applied to the function. See the PR description for the explanation for mem::swap--it's because we don't currently count modifies clauses as contracts.

[celinval]

Thanks for doing this!! Per our offline discussion, I think we should remove the # of Contracts. As a bonus it should simplify the compiler changes.

[carolynzech]

@celinval Thanks for the feedback -- I removed contracts count and simplified the RFC. Also per offline discussion, I stabilized the gen_contracts_metadata function. It still uses unstable DefIds, since in this line:

else if let Some((target_name, target_def_id, _)) = attributes.interpret_for_contract_attribute()

target_def_id is an unstable DefId and AFAIK there's no way to convert an unstable DefId to a stable one. LMK if I'm mistaken and I'll fix it.

[celinval]

@celinval Thanks for the feedback -- I removed contracts count and simplified the RFC. Also per offline discussion, I stabilized the gen_contracts_metadata function. It still uses unstable DefIds, since in this line:

else if let Some((target_name, target_def_id, _)) = attributes.interpret_for_contract_attribute()

target_def_id is an unstable DefId and AFAIK there's no way to convert an unstable DefId to a stable one. LMK if I'm mistaken and I'll fix it.

You could use this function to get the FnDef:

kani/kani-compiler/src/kani_middle/codegen_units.rs

Line 118 in 68387e4

fn stub_def(tcx: TyCtxt, def_id: DefId) -> FnDef {

[feliperodri]

Thanks so much for this new feature! Only a few more minor comments to go before merging it.

[zhassan-aws]

Nice work!

[zhassan-aws]

Thanks!