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.

Sign up for GitHub

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

Support slice::get && Ignore trait predicates when not visible to local. #1434

Merged
merged 2 commits into from
Feb 14, 2025
+35 −1
Merged

Support slice::get && Ignore trait predicates when not visible to local. #1434

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8a817b0
Support slice::get && Ignore trait predicates when not visible to local.
ziqiaozhou Jan 28, 2025
fe6ae59
skip trait bound check if path == core::slice::index::private_slice_i…
ziqiaozhou Feb 7, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 16 additions & 1 deletion source/rust_verify/src/rust_to_vir_func.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1389,7 +1389,22 @@ pub(crate) fn remove_ignored_trait_bounds_from_predicates<'tcx>(
use rustc_middle::ty::{ConstKind, ScalarInt, ValTree};
preds.retain(|p: &Clause<'tcx>| match p.kind().skip_binder() {
rustc_middle::ty::ClauseKind::<'tcx>::Trait(tp) => {
if in_trait && trait_ids.contains(&tp.trait_ref.def_id) && tp.trait_ref.args.len() >= 1
let td = tcx.trait_def(tp.trait_ref.def_id);
// Recursively check parent path visibility
let mut visible = tcx.visibility(td.def_id).is_visible_locally();
let mut def_id = td.def_id;
while let Some(parent_def_id) = tcx.opt_parent(def_id) {
if !tcx.visibility(parent_def_id).is_visible_locally() {
Copy link
Collaborator

Choose a reason for hiding this comment

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

It looks like this is rejecting some traits that actually are visible, like Iterator:

td.def_id = DefId(2:8781 ~ core[145f]::iter::traits::iterator::Iterator)
parent_def_id = DefId(2:8736 ~ core[145f]::iter::traits::iterator)

In https://github.com/rust-lang/rust/blob/master/library/core/src/iter/traits/mod.rs , it looks like Iterator is made visible via a pub use after being initially declared in a private module:

mod accum;
mod collect;
mod double_ended;
mod exact_size;
mod iterator;
mod marker;
mod unchecked_iterator;

#[unstable(issue = "none", feature = "inplace_iteration")]
pub use self::marker::InPlaceIterable;
#[unstable(issue = "none", feature = "trusted_fused")]
pub use self::marker::TrustedFused;
#[unstable(feature = "trusted_step", issue = "85731")]
pub use self::marker::TrustedStep;
pub(crate) use self::unchecked_iterator::UncheckedIterator;
#[stable(feature = "rust1", since = "1.0.0")]
pub use self::{
    accum::{Product, Sum},
    collect::{Extend, FromIterator, IntoIterator},
    double_ended::DoubleEndedIterator,
    exact_size::ExactSizeIterator,
    iterator::Iterator,
    marker::{FusedIterator, TrustedLen},
};

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Oh. I see. Then I do not know how to check whether a trait is reacheable. I did not find a correct helper function from TyCtxt. Maybe do a hard check on path?

let path = tcx.def_path_str(tp.trait_ref.def_id);
if path == "core::slice::index::private_slice_index::Sealed" {
    false
} else if

visible = false;
break;
}
def_id = parent_def_id;
}
if !visible {
false
} else if in_trait
&& trait_ids.contains(&tp.trait_ref.def_id)
&& tp.trait_ref.args.len() >= 1
{
if let GenericArgKind::Type(ty) = tp.trait_ref.args[0].unpack() {
match ty.kind() {
Expand Down
28 changes: 28 additions & 0 deletions source/vstd/slice.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,8 +103,36 @@ pub exec fn slice_subrange<T, 'a>(slice: &'a [T], i: usize, j: usize) -> (out: &
&slice[i..j]
}

#[verifier::external_trait_specification]
pub trait ExSliceIndex<T> where T: ?Sized {
type ExternalTraitSpecificationFor: core::slice::SliceIndex<T>;

type Output: ?Sized;
}

pub assume_specification<T, I>[ <[T]>::get::<I> ](slice: &[T], i: I) -> (b: Option<
&<I as core::slice::SliceIndex<[T]>>::Output,
>) where I: core::slice::SliceIndex<[T]>
returns
spec_slice_get(slice, i),
;

pub open spec fn spec_slice_get<T: ?Sized, I: core::slice::SliceIndex<T>>(
val: &T,
idx: I,
) -> Option<&<I as core::slice::SliceIndex<T>>::Output>;

pub broadcast proof fn axiom_slice_get_usize<T>(v: &[T], i: usize)
ensures
i < v.len() ==> #[trigger] spec_slice_get(v, i) === Some(&v[i as int]),
i >= v.len() ==> spec_slice_get(v, i).is_none(),
{
admit();
}

pub broadcast group group_slice_axioms {
axiom_spec_len,
axiom_slice_get_usize,
}

} // verus!