Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add initial implementation of the reachability algorithm #1683

Merged
merged 12 commits into from
Sep 20, 2022

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Sep 14, 2022

Description of changes:

Add a new module reachability which implements the reachability algorithm. Add the end to end logic for the reachability starting from all the harnesses in the target crate.

Resolved issues:

Resolves #1672

Related RFC:

Optional #1588

Call-outs:

  • We still need to build the custom sysroot in order to fix the missing functions issue.
  • I added a mechanism to run the regression tests using the MIR linker inside compiletest.
  • I ran the regression manually (with the mir_linker enabled) the only tests that didn't pass were:
    • cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected: The global assembly is out of the scope so it doesn't get processed. If we want to keep that behavior, we will have to inspect all items manually.
    • cargo-kani/cargo-tests-dir/expected: This might be a legit issue that I need to fix on kani-driver logic.
    • cargo-ui/dry-run/expected: Not an issue (arguments to the compiler changes).

Testing:

  • How is this change tested? New tests + manually run the regression with RUSTFLAGS=--cfg=mir_linker

  • Is this a refactor change? No

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

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

TODO:
- Cleanup the code.
- Add more tests.
@celinval celinval requested a review from a team as a code owner September 14, 2022 19:34
@celinval celinval requested a review from danielsn September 14, 2022 19:34
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great work, @celinval! A few minor comments.

kani-compiler/src/codegen_cprover_gotoc/reachability.rs Outdated Show resolved Hide resolved
let src_ty_inner = find_pointer(tcx, src_ty);

trace!(?dst_ty_inner, ?src_ty_inner, "find_trait_conversion");
(vtable_metadata(dst_ty_inner) && !vtable_metadata(src_ty_inner)).then(|| {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What does this line mean?

Copy link
Contributor Author

@celinval celinval Sep 15, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this is the same as:

if cond {
  Some(val)
} else {
  None
}

kani-compiler/src/codegen_cprover_gotoc/reachability.rs Outdated Show resolved Hide resolved
kani-compiler/src/codegen_cprover_gotoc/reachability.rs Outdated Show resolved Hide resolved
}
}

impl<'tcx> Iterator for ReceiverIter<'tcx> {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This level of inner impls makes my head hurt

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yeah, this code needs some polishing for sure. I'll create another issue to do that.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll move these definitions to be out of the function. I also need to rewrite how we're handling unsized coercion to support custom smart pointers. I created #1683 to capture this work.

if items.is_empty() {
// There's nothing to do.
return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model());
}

// we first declare all functions
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

declare all "items"

codegen_units
.iter()
.flat_map(|cgu| cgu.items_in_deterministic_order(tcx))
.map(|(item, _)| item)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK

let harnesses = collect_harnesses(tcx, gcx);
collect_reachable_items(tcx, &harnesses).into_iter().collect()
}
ReachabilityType::None => Vec::new(),
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

comment that?


impl<'tcx> MonoItemsCollector<'tcx> {
/// Collects all reachable items starting from the given root.
pub fn collect(&mut self, root: MonoItem<'tcx>) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍

// Collect drop function.
let static_ty = instance.ty(self.tcx, ParamEnv::reveal_all());
let instance = Instance::resolve_drop_in_place(self.tcx, static_ty);
self.queue.push(MonoItem::Fn(instance.polymorphize(self.tcx)));
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good to know!

@celinval celinval merged commit d06672b into model-checking:main Sep 20, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Implement cross-crate reachability algorithm
3 participants