Add initial implementation of the reachability algorithm#1683
Merged
celinval merged 12 commits intomodel-checking:mainfrom Sep 20, 2022
Merged
Add initial implementation of the reachability algorithm#1683celinval merged 12 commits intomodel-checking:mainfrom
celinval merged 12 commits intomodel-checking:mainfrom
Conversation
TODO: - Cleanup the code. - Add more tests.
zhassan-aws
reviewed
Sep 14, 2022
Contributor
zhassan-aws
left a comment
zhassan-aws
left a comment
There was a problem hiding this comment.
Great work, @celinval! A few minor comments.
zhassan-aws
approved these changes
Sep 15, 2022
danielsn
reviewed
Sep 15, 2022
| 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(|| { |
Contributor
There was a problem hiding this comment.
What does this line mean?
Contributor
Author
There was a problem hiding this comment.
this is the same as:
if cond {
Some(val)
} else {
None
}| } | ||
| } | ||
|
|
||
| impl<'tcx> Iterator for ReceiverIter<'tcx> { |
Contributor
There was a problem hiding this comment.
This level of inner impls makes my head hurt
Contributor
Author
There was a problem hiding this comment.
yeah, this code needs some polishing for sure. I'll create another issue to do that.
Contributor
Author
There was a problem hiding this comment.
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.
Thus, we no longer print "Failed to compile crate"
danielsn
approved these changes
Sep 20, 2022
| return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()); | ||
| } | ||
|
|
||
| // we first declare all functions |
| codegen_units | ||
| .iter() | ||
| .flat_map(|cgu| cgu.items_in_deterministic_order(tcx)) | ||
| .map(|(item, _)| item) |
| let harnesses = collect_harnesses(tcx, gcx); | ||
| collect_reachable_items(tcx, &harnesses).into_iter().collect() | ||
| } | ||
| ReachabilityType::None => Vec::new(), |
|
|
||
| impl<'tcx> MonoItemsCollector<'tcx> { | ||
| /// Collects all reachable items starting from the given root. | ||
| pub fn collect(&mut self, root: MonoItem<'tcx>) { |
| // 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))); |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description of changes:
Add a new module
reachabilitywhich 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:
compiletest.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 onkani-driverlogic.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_linkerIs this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.