Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[toolchain]
channel = "nightly-2025-03-08"
channel = "nightly-2025-09-08"
components = [ "rustc-dev", "rust-src", "llvm-tools-preview", "rust-analyzer" ]
24 changes: 11 additions & 13 deletions src/analyze.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ pub use did_cache::DefIdCache;
pub fn mir_borrowck_skip_formula_fn(
tcx: rustc_middle::ty::TyCtxt<'_>,
local_def_id: rustc_span::def_id::LocalDefId,
) -> rustc_middle::query::queries::mir_borrowck::ProvidedValue {
) -> rustc_middle::query::queries::mir_borrowck::ProvidedValue<'_> {
// TODO: unify impl with local_def::Analyzer
// if the def is closure defined in formula_fn
let root_def_id = tcx.typeck_root_def_id(local_def_id.to_def_id());
Expand All @@ -52,13 +52,8 @@ pub fn mir_borrowck_skip_formula_fn(

if is_annotated_as_formula_fn {
tracing::debug!(?local_def_id, "skipping borrow check for formula fn");
let dummy_result = rustc_middle::mir::BorrowCheckResult {
concrete_opaque_types: Default::default(),
closure_requirements: None,
used_mut_upvars: Default::default(),
tainted_by_errors: None,
};
return tcx.arena.alloc(dummy_result);
let dummy_result = rustc_middle::mir::ConcreteOpaqueTypes(Default::default());
return Ok(tcx.arena.alloc(dummy_result));
}

(rustc_interface::DEFAULT_QUERY_PROVIDERS
Expand Down Expand Up @@ -511,7 +506,9 @@ impl<'tcx> Analyzer<'tcx> {
let ret = rty::RefinedType::new(rty::Type::never(), rty::Refinement::bottom());
rty::FunctionType::new([param.vacuous()].into_iter().collect(), ret)
};
let panic_def_id = self.tcx.require_lang_item(LangItem::Panic, None);
let panic_def_id = self
.tcx
.require_lang_item(LangItem::Panic, rustc_span::DUMMY_SP);
self.register_def(panic_def_id, rty::RefinedType::unrefined(panic_ty.into()));
}

Expand Down Expand Up @@ -581,15 +578,15 @@ impl<'tcx> Analyzer<'tcx> {
local_def_id: LocalDefId,
attr_path: &[Symbol],
) -> Option<DefId> {
let map = self.tcx.hir();
let body = self.tcx.hir_maybe_body_owned_by(local_def_id)?;

let rustc_hir::ExprKind::Block(block, _) = body.value.kind else {
return None;
};
for stmt in block.stmts {
if map
.attrs(stmt.hir_id)
if self
.tcx
.hir_attrs(stmt.hir_id)
.iter()
.all(|attr| !attr.path_matches(attr_path))
{
Expand Down Expand Up @@ -724,7 +721,8 @@ impl<'tcx> Analyzer<'tcx> {
/// Whether the given `def_id` corresponds to a method of one of the `Fn` traits.
fn is_fn_trait_method(&self, def_id: DefId) -> bool {
self.tcx
.trait_of_item(def_id)
.opt_associated_item(def_id)
.and_then(|item| item.trait_container(self.tcx))
.and_then(|trait_did| self.tcx.fn_trait_kind_from_def_id(trait_did))
.is_some()
}
Expand Down
17 changes: 11 additions & 6 deletions src/analyze/basic_block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -233,7 +233,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
}
}

fn const_value_ty(&self, val: &mir::ConstValue<'tcx>, ty: &mir_ty::Ty<'tcx>) -> PlaceType {
fn const_value_ty(&self, val: &mir::ConstValue, ty: &mir_ty::Ty<'tcx>) -> PlaceType {
use mir::{interpret::Scalar, ConstValue, Mutability};
match (ty.kind(), val) {
(
Expand Down Expand Up @@ -262,9 +262,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
mir_ty::TyKind::Ref(_, elem, Mutability::Not),
ConstValue::Scalar(Scalar::Ptr(ptr, _)),
) => {
// Pointer::into_parts is OK for CtfeProvenance
// in a later version of rustc it has prov_and_relative_offset that ensures this
let (prov, offset) = ptr.into_parts();
let (prov, offset) = ptr.prov_and_relative_offset();
let global_alloc = self.tcx.global_alloc(prov.alloc_id());
match global_alloc {
mir::interpret::GlobalAlloc::Memory(alloc) => {
Expand All @@ -281,9 +279,16 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
_ => unimplemented!("const ptr alloc: {:?}", global_alloc),
}
}
(mir_ty::TyKind::Ref(_, elem, Mutability::Not), ConstValue::Slice { data, meta }) => {
(
mir_ty::TyKind::Ref(_, elem, Mutability::Not),
ConstValue::Slice { alloc_id, meta },
) => {
let end = (*meta).try_into().unwrap();
self.const_bytes_ty(*elem, *data, 0..end).immut()
let global_alloc = self.tcx.global_alloc(*alloc_id);
let mir::interpret::GlobalAlloc::Memory(alloc) = global_alloc else {
unimplemented!("const slice alloc: {:?}", global_alloc);
};
self.const_bytes_ty(*elem, alloc, 0..end).immut()
}
_ => unimplemented!("const: {:?}, ty: {:?}", val, ty),
}
Expand Down
6 changes: 3 additions & 3 deletions src/analyze/did_cache.rs
Original file line number Diff line number Diff line change
Expand Up @@ -87,17 +87,17 @@ impl<'tcx> DefIdCache<'tcx> {
}

let item = self.tcx.hir_item(item_id);
if let rustc_hir::ItemKind::Trait(_, _, _, _, trait_item_refs) = item.kind {
if let rustc_hir::ItemKind::Trait(_, _, _, _, _, _, trait_item_refs) = item.kind {
for trait_item_ref in trait_item_refs {
let def_id = trait_item_ref.id.owner_id.to_def_id();
let def_id = trait_item_ref.owner_id.to_def_id();
if self.tcx.get_attrs_by_path(def_id, path).next().is_some() {
return Some(def_id);
}
}
}
if let rustc_hir::ItemKind::Impl(impl_) = item.kind {
for impl_item_ref in impl_.items {
let def_id = impl_item_ref.id.owner_id.to_def_id();
let def_id = impl_item_ref.owner_id.to_def_id();
if self.tcx.get_attrs_by_path(def_id, path).next().is_some() {
return Some(def_id);
}
Expand Down
14 changes: 8 additions & 6 deletions src/analyze/local_def.rs
Original file line number Diff line number Diff line change
Expand Up @@ -156,9 +156,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
// names and sorts of arguments
let arg_names = self
.tcx
.fn_arg_names(self.local_def_id.to_def_id())
.fn_arg_idents(self.local_def_id.to_def_id())
.iter()
.map(|ident| ident.to_string());
.map(|ident| ident.map_or_else(String::new, |i| i.to_string()));

let sig = self.ctx.fn_sig(self.local_def_id.to_def_id());
let arg_sorts = sig
Expand Down Expand Up @@ -276,10 +276,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
.next()
.is_some();

let arg_names = self.tcx.fn_arg_names(self.local_def_id.to_def_id());
let arg_names = self.tcx.fn_arg_idents(self.local_def_id.to_def_id());
let all_params_annotated = arg_names
.iter()
.all(|ident| annotated_params.contains(ident));
.all(|ident| ident.is_some_and(|i| annotated_params.contains(&i)));
self.is_annotated_as_callable()
|| (has_requires && has_ensures)
|| (all_params_annotated && has_ret)
Expand Down Expand Up @@ -328,12 +328,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
let mut param_resolver = analyze::annot::ParamResolver::default();
for (input_ident, input_ty) in self
.tcx
.fn_arg_names(self.local_def_id.to_def_id())
.fn_arg_idents(self.local_def_id.to_def_id())
.iter()
.zip(sig.inputs())
{
let input_ty = self.type_builder.build(*input_ty);
param_resolver.push_param(input_ident.name, input_ty.to_sort());
if let Some(ident) = input_ident {
param_resolver.push_param(ident.name, input_ty.to_sort());
}
Comment on lines 335 to +338
}

let output_ty = self.type_builder.build(sig.output());
Expand Down
74 changes: 36 additions & 38 deletions src/annot.rs
Original file line number Diff line number Diff line change
Expand Up @@ -330,7 +330,7 @@ where
if t.kind == expected {
Ok(())
} else {
Err(ParseAttrError::unexpected_token(expected_str, t.clone()))
Err(ParseAttrError::unexpected_token(expected_str, *t))
}
}

Expand All @@ -339,7 +339,7 @@ where
if let Some((ident, _)) = t.ident() {
Ok(ident)
} else {
Err(ParseAttrError::unexpected_token("ident", t.clone()))
Err(ParseAttrError::unexpected_token("ident", *t))
}
}

Expand Down Expand Up @@ -418,7 +418,7 @@ where
if segments.is_empty() {
return Err(ParseAttrError::unexpected_token(
"path segment before <",
t.clone(),
*t,
));
}
let mut generic_args = Vec::new();
Expand All @@ -434,7 +434,7 @@ where
kind: TokenKind::Gt,
..
} => break,
t => return Err(ParseAttrError::unexpected_token(", or >", t.clone())),
t => return Err(ParseAttrError::unexpected_token(", or >", *t)),
}
}
segments.last_mut().unwrap().generic_args = generic_args;
Expand All @@ -449,7 +449,7 @@ where
generic_args: Vec::new(),
});
}
t => return Err(ParseAttrError::unexpected_token("ident or <", t.clone())),
t => return Err(ParseAttrError::unexpected_token("ident or <", *t)),
}
}
Ok(AnnotPath { segments })
Expand Down Expand Up @@ -623,13 +623,13 @@ where
self.expect_next_token(TokenKind::Gt, ">")?;
FormulaOrTerm::Term(chc::Term::mut_(t1, t2), chc::Sort::mut_(s1))
}
t => return Err(ParseAttrError::unexpected_token("> or ,", t.clone())),
t => return Err(ParseAttrError::unexpected_token("> or ,", *t)),
}
}
_ => {
return Err(ParseAttrError::unexpected_token(
"identifier, or literal",
t.clone(),
*t,
));
}
}
Expand All @@ -654,7 +654,7 @@ where
}) = self.look_ahead_token(0)
{
self.consume();
let t = self.next_token("field")?.clone();
let t = *self.next_token("field")?;
if let Token {
kind: TokenKind::Literal(lit),
..
Expand Down Expand Up @@ -694,7 +694,7 @@ where
}
}
}
return Err(ParseAttrError::unexpected_token("field", t.clone()));
return Err(ParseAttrError::unexpected_token("field", t));
}

if fields.is_empty() {
Expand Down Expand Up @@ -947,7 +947,7 @@ where
kind: TokenKind::Dot,
..
} => break,
t => return Err(ParseAttrError::unexpected_token(". or ,", t.clone())),
t => return Err(ParseAttrError::unexpected_token(". or ,", *t)),
}
}
self.formula_existentials.extend(vars.iter().cloned());
Expand Down Expand Up @@ -1035,7 +1035,7 @@ where
parser.consume();
}
None => break,
Some(t) => return Err(ParseAttrError::unexpected_token(",", t.clone())),
Some(t) => return Err(ParseAttrError::unexpected_token(",", *t)),
}
}
parser.end_of_input()?;
Expand Down Expand Up @@ -1068,33 +1068,31 @@ where
}
s => {
let sym = chc::DatatypeSymbol::new(s.to_owned());
let tys =
if self.look_ahead_token(0).map(|t| &t.kind) == Some(&TokenKind::Lt) {
self.consume();
let mut tys = IndexVec::new();
loop {
tys.push(self.parse_rty()?);
match self.next_token("> or ,")? {
Token {
kind: TokenKind::Comma,
..
} => {}
Token {
kind: TokenKind::Gt,
..
} => break,
t => {
return Err(ParseAttrError::unexpected_token(
">, or ,",
t.clone(),
))
}
let tys = if self.look_ahead_token(0).map(|t| &t.kind)
== Some(&TokenKind::Lt)
{
self.consume();
let mut tys = IndexVec::new();
loop {
tys.push(self.parse_rty()?);
match self.next_token("> or ,")? {
Token {
kind: TokenKind::Comma,
..
} => {}
Token {
kind: TokenKind::Gt,
..
} => break,
t => {
return Err(ParseAttrError::unexpected_token(">, or ,", *t))
}
}
tys
} else {
Default::default()
};
}
tys
} else {
Default::default()
};
rty::EnumType::new(sym, tys).into()
}
};
Expand Down Expand Up @@ -1142,7 +1140,7 @@ where
parser.consume();
}
None => break,
Some(t) => return Err(ParseAttrError::unexpected_token(",", t.clone())),
Some(t) => return Err(ParseAttrError::unexpected_token(",", *t)),
}
}
parser.end_of_input()?;
Expand Down Expand Up @@ -1177,7 +1175,7 @@ where
) {
let h = parser.next_token("ident")?;
let Some((ident, _)) = h.ident() else {
return Err(ParseAttrError::unexpected_token("ident", h.clone()));
return Err(ParseAttrError::unexpected_token("ident", *h));
};
parser.consume();
Some(ident)
Expand Down
2 changes: 1 addition & 1 deletion src/chc/debug.rs
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ impl DebugInfo {
self
}

pub fn display(&self, line_head: &'static str) -> Display {
pub fn display(&self, line_head: &'static str) -> Display<'_> {
Display {
inner: self,
line_head,
Expand Down
Loading