1#![feature(
3 associated_type_defaults,
4 box_patterns,
5 closure_track_caller,
6 if_let_guard,
7 map_try_insert,
8 min_specialization,
9 never_type,
10 rustc_private,
11 unwrap_infallible,
12 new_range_api
13)]
14
15extern crate rustc_abi;
16extern crate rustc_ast;
17extern crate rustc_data_structures;
18extern crate rustc_errors;
19extern crate rustc_hir;
20extern crate rustc_index;
21extern crate rustc_macros;
22extern crate rustc_middle;
23extern crate rustc_serialize;
24extern crate rustc_span;
25extern crate rustc_type_ir;
26
27extern crate self as flux_middle;
28
29pub mod big_int;
30pub mod cstore;
31pub mod def_id;
32pub mod fhir;
33pub mod global_env;
34pub mod metrics;
35pub mod pretty;
36pub mod queries;
37pub mod rty;
38mod sort_of;
39
40use std::sync::LazyLock;
41
42use flux_arc_interner::List;
43use flux_macros::fluent_messages;
44pub use flux_rustc_bridge::def_id_to_string;
45use flux_rustc_bridge::{
46 mir::{LocalDecls, PlaceElem},
47 ty::{self, GenericArgsExt},
48};
49use flux_syntax::surface::{self, NodeId};
50use global_env::GlobalEnv;
51use liquid_fixpoint::ThyFunc;
52use queries::QueryResult;
53use rty::VariantIdx;
54use rustc_abi::FieldIdx;
55use rustc_data_structures::{
56 fx::FxIndexMap,
57 unord::{UnordMap, UnordSet},
58};
59use rustc_hir::OwnerId;
60use rustc_macros::extension;
61use rustc_middle::ty::TyCtxt;
62use rustc_span::{
63 Symbol,
64 def_id::{DefId, LocalDefId},
65 symbol::Ident,
66};
67
68fluent_messages! { "../locales/en-US.ftl" }
69
70pub struct TheoryFunc {
71 pub name: Symbol,
72 pub sort: rty::PolyFuncSort,
73 pub itf: liquid_fixpoint::ThyFunc,
74}
75
76pub static THEORY_FUNCS: LazyLock<UnordMap<liquid_fixpoint::ThyFunc, TheoryFunc>> =
77 LazyLock::new(|| {
78 use rty::{BvSize, Sort::*};
79 liquid_fixpoint::ThyFunc::ALL
80 .into_iter()
81 .filter_map(|func| {
82 let func = TheoryFunc {
83 name: Symbol::intern(name_of_thy_func(func)?),
84 itf: func,
85 sort: sort_of_thy_func(func)?,
86 };
87 Some(func)
88 })
89 .chain([
90 TheoryFunc {
92 name: Symbol::intern("bv_zero_extend_32_to_64"),
93 itf: liquid_fixpoint::ThyFunc::BvZeroExtend(32),
94 sort: rty::PolyFuncSort::new(
95 List::empty(),
96 rty::FuncSort::new(
97 vec![BitVec(BvSize::Fixed(32))],
98 BitVec(BvSize::Fixed(64)),
99 ),
100 ),
101 },
102 TheoryFunc {
103 name: Symbol::intern("bv_sign_extend_32_to_64"),
104 itf: liquid_fixpoint::ThyFunc::BvSignExtend(32),
105 sort: rty::PolyFuncSort::new(
106 List::empty(),
107 rty::FuncSort::new(
108 vec![BitVec(BvSize::Fixed(32))],
109 BitVec(BvSize::Fixed(64)),
110 ),
111 ),
112 },
113 ])
114 .map(|func| (func.itf, func))
115 .collect()
116 });
117
118pub fn name_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<&'static str> {
119 let name = match func {
120 ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
121 ThyFunc::StrLen => "str_len",
122 ThyFunc::StrConcat => "str_concat",
123 ThyFunc::StrPrefixOf => "str_prefix_of",
124 ThyFunc::StrSuffixOf => "str_suffix_of",
125 ThyFunc::StrContains => "str_contains",
126 ThyFunc::IntToBv8 => "bv_int_to_bv8",
127 ThyFunc::Bv8ToInt => "bv_bv8_to_int",
128 ThyFunc::IntToBv32 => "bv_int_to_bv32",
129 ThyFunc::Bv32ToInt => "bv_bv32_to_int",
130 ThyFunc::IntToBv64 => "bv_int_to_bv64",
131 ThyFunc::Bv64ToInt => "bv_bv64_to_int",
132 ThyFunc::BvUge => "bv_uge",
133 ThyFunc::BvSge => "bv_sge",
134 ThyFunc::BvUdiv => "bv_udiv",
135 ThyFunc::BvSdiv => "bv_sdiv",
136 ThyFunc::BvSrem => "bv_srem",
137 ThyFunc::BvUrem => "bv_urem",
138 ThyFunc::BvLshr => "bv_lshr",
139 ThyFunc::BvAshr => "bv_ashr",
140 ThyFunc::BvAnd => "bv_and",
141 ThyFunc::BvOr => "bv_or",
142 ThyFunc::BvXor => "bv_xor",
143 ThyFunc::BvNot => "bv_not",
144 ThyFunc::BvAdd => "bv_add",
145 ThyFunc::BvNeg => "bv_neg",
146 ThyFunc::BvSub => "bv_sub",
147 ThyFunc::BvMul => "bv_mul",
148 ThyFunc::BvShl => "bv_shl",
149 ThyFunc::BvUle => "bv_ule",
150 ThyFunc::BvSle => "bv_sle",
151 ThyFunc::BvUgt => "bv_ugt",
152 ThyFunc::BvSgt => "bv_sgt",
153 ThyFunc::BvUlt => "bv_ult",
154 ThyFunc::BvSlt => "bv_slt",
155 ThyFunc::SetEmpty => "set_empty",
156 ThyFunc::SetSng => "set_singleton",
157 ThyFunc::SetCup => "set_union",
158 ThyFunc::SetCap => "set_intersection",
159 ThyFunc::SetDif => "set_difference",
160 ThyFunc::SetSub => "set_subset",
161 ThyFunc::SetMem => "set_is_in",
162 ThyFunc::MapDefault => "map_default",
163 ThyFunc::MapSelect => "map_select",
164 ThyFunc::MapStore => "map_store",
165 };
166 Some(name)
167}
168
169fn sort_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<rty::PolyFuncSort> {
170 use rty::{
171 BvSize, ParamSort,
172 Sort::{self, *},
173 SortCtor::*,
174 SortParamKind,
175 };
176 let param0 = ParamSort::from_u32(0);
177 let param1 = ParamSort::from_u32(1);
178 let bv_param0 = BvSize::Param(ParamSort::from_u32(0));
179
180 let sort = match func {
181 ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
182 ThyFunc::StrLen => {
183 rty::PolyFuncSort::new(List::empty(), rty::FuncSort::new(vec![rty::Sort::Str], Int))
185 }
186 ThyFunc::StrConcat => {
187 rty::PolyFuncSort::new(
189 List::empty(),
190 rty::FuncSort::new(vec![rty::Sort::Str, rty::Sort::Str], rty::Sort::Str),
191 )
192 }
193 ThyFunc::StrPrefixOf | ThyFunc::StrSuffixOf | ThyFunc::StrContains => {
194 rty::PolyFuncSort::new(
196 List::empty(),
197 rty::FuncSort::new(vec![rty::Sort::Str, rty::Sort::Str], Bool),
198 )
199 }
200 ThyFunc::IntToBv8 => {
201 rty::PolyFuncSort::new(
203 List::empty(),
204 rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(8))),
205 )
206 }
207 ThyFunc::Bv8ToInt => {
208 rty::PolyFuncSort::new(
210 List::empty(),
211 rty::FuncSort::new(vec![BitVec(BvSize::Fixed(8))], Int),
212 )
213 }
214 ThyFunc::IntToBv32 => {
215 rty::PolyFuncSort::new(
217 List::empty(),
218 rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(32))),
219 )
220 }
221 ThyFunc::Bv32ToInt => {
222 rty::PolyFuncSort::new(
224 List::empty(),
225 rty::FuncSort::new(vec![BitVec(BvSize::Fixed(32))], Int),
226 )
227 }
228 ThyFunc::IntToBv64 => {
229 rty::PolyFuncSort::new(
231 List::empty(),
232 rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(64))),
233 )
234 }
235 ThyFunc::Bv64ToInt => {
236 rty::PolyFuncSort::new(
238 List::empty(),
239 rty::FuncSort::new(vec![BitVec(BvSize::Fixed(64))], Int),
240 )
241 }
242 ThyFunc::BvUdiv
243 | ThyFunc::BvSdiv
244 | ThyFunc::BvSrem
245 | ThyFunc::BvUrem
246 | ThyFunc::BvLshr
247 | ThyFunc::BvAshr
248 | ThyFunc::BvAnd
249 | ThyFunc::BvOr
250 | ThyFunc::BvXor
251 | ThyFunc::BvAdd
252 | ThyFunc::BvSub
253 | ThyFunc::BvMul
254 | ThyFunc::BvShl => {
255 rty::PolyFuncSort::new(
257 List::singleton(SortParamKind::BvSize),
258 rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], BitVec(bv_param0)),
259 )
260 }
261 ThyFunc::BvNot | ThyFunc::BvNeg => {
262 rty::PolyFuncSort::new(
264 List::singleton(SortParamKind::BvSize),
265 rty::FuncSort::new(vec![BitVec(bv_param0)], BitVec(bv_param0)),
266 )
267 }
268 ThyFunc::BvUgt
269 | ThyFunc::BvSgt
270 | ThyFunc::BvUlt
271 | ThyFunc::BvSlt
272 | ThyFunc::BvSle
273 | ThyFunc::BvUge
274 | ThyFunc::BvSge
275 | ThyFunc::BvUle => {
276 rty::PolyFuncSort::new(
278 List::singleton(SortParamKind::BvSize),
279 rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
280 )
281 }
282 ThyFunc::SetEmpty => {
283 rty::PolyFuncSort::new(
285 List::singleton(SortParamKind::Sort),
286 rty::FuncSort::new(vec![Int], Sort::app(Set, List::singleton(Var(param0)))),
287 )
288 }
289 ThyFunc::SetSng => {
290 rty::PolyFuncSort::new(
292 List::singleton(SortParamKind::Sort),
293 rty::FuncSort::new(vec![Var(param0)], Sort::app(Set, List::singleton(Var(param0)))),
294 )
295 }
296 ThyFunc::SetCup | ThyFunc::SetCap | ThyFunc::SetDif => {
297 rty::PolyFuncSort::new(
299 List::singleton(SortParamKind::Sort),
300 rty::FuncSort::new(
301 vec![
302 Sort::app(Set, List::singleton(Var(param0))),
303 Sort::app(Set, List::singleton(Var(param0))),
304 ],
305 Sort::app(Set, List::singleton(Var(param0))),
306 ),
307 )
308 }
309 ThyFunc::SetMem => {
310 rty::PolyFuncSort::new(
312 List::singleton(SortParamKind::Sort),
313 rty::FuncSort::new(
314 vec![Var(param0), Sort::app(Set, List::singleton(Var(param0)))],
315 Bool,
316 ),
317 )
318 }
319 ThyFunc::SetSub => {
320 rty::PolyFuncSort::new(
322 List::singleton(SortParamKind::Sort),
323 rty::FuncSort::new(
324 vec![
325 Sort::app(Set, List::singleton(Var(param0))),
326 Sort::app(Set, List::singleton(Var(param0))),
327 ],
328 Bool,
329 ),
330 )
331 }
332
333 ThyFunc::MapDefault => {
334 rty::PolyFuncSort::new(
336 List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
337 rty::FuncSort::new(
338 vec![Var(param1)],
339 Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
340 ),
341 )
342 }
343 ThyFunc::MapSelect => {
344 rty::PolyFuncSort::new(
346 List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
347 rty::FuncSort::new(
348 vec![Sort::app(Map, List::from_arr([Var(param0), Var(param1)])), Var(param0)],
349 Var(param1),
350 ),
351 )
352 }
353 ThyFunc::MapStore => {
354 rty::PolyFuncSort::new(
356 List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
357 rty::FuncSort::new(
358 vec![
359 Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
360 Var(param0),
361 Var(param1),
362 ],
363 Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
364 ),
365 )
366 }
367 };
368 Some(sort)
369}
370
371#[derive(Default)]
372pub struct Specs {
373 items: UnordMap<OwnerId, surface::Item>,
374 trait_items: UnordMap<OwnerId, surface::TraitItemFn>,
375 impl_items: UnordMap<OwnerId, surface::ImplItemFn>,
376 pub flux_items_by_parent: FxIndexMap<OwnerId, Vec<surface::FluxItem>>,
377 dummy_extern: UnordSet<LocalDefId>,
386 extern_id_to_local_id: UnordMap<DefId, LocalDefId>,
387 local_id_to_extern_id: UnordMap<LocalDefId, DefId>,
388}
389
390impl Specs {
391 pub fn insert_extern_spec_id_mapping(
392 &mut self,
393 local_id: LocalDefId,
394 extern_id: DefId,
395 ) -> Result<(), ExternSpecMappingErr> {
396 #[expect(
397 clippy::disallowed_methods,
398 reason = "we are inserting the extern spec mapping and we want to ensure it doesn't point to a local item"
399 )]
400 if let Some(local) = extern_id.as_local() {
401 return Err(ExternSpecMappingErr::IsLocal(local));
402 }
403 if let Err(err) = self.extern_id_to_local_id.try_insert(extern_id, local_id) {
404 return Err(ExternSpecMappingErr::Dup(*err.entry.get()));
405 }
406 self.local_id_to_extern_id.insert(local_id, extern_id);
407 Ok(())
408 }
409
410 pub fn insert_dummy(&mut self, def_id: LocalDefId) {
411 self.dummy_extern.insert(def_id);
412 }
413
414 pub fn get_item(&self, owner_id: OwnerId) -> Option<&surface::Item> {
415 self.items.get(&owner_id)
416 }
417
418 pub fn insert_item(&mut self, owner_id: OwnerId, item: surface::Item) -> Option<surface::Item> {
419 if let Some(old) = self.items.insert(owner_id, item) {
420 return Some(old);
421 }
422 None
423 }
424
425 pub fn get_trait_item(&self, owner_id: OwnerId) -> Option<&surface::TraitItemFn> {
426 self.trait_items.get(&owner_id)
427 }
428
429 pub fn insert_trait_item(
430 &mut self,
431 owner_id: OwnerId,
432 trait_item: surface::TraitItemFn,
433 ) -> Option<surface::TraitItemFn> {
434 if let Some(old) = self.trait_items.insert(owner_id, trait_item) {
435 return Some(old);
436 }
437 None
438 }
439
440 pub fn get_impl_item(&self, owner_id: OwnerId) -> Option<&surface::ImplItemFn> {
441 self.impl_items.get(&owner_id)
442 }
443
444 pub fn insert_impl_item(
445 &mut self,
446 owner_id: OwnerId,
447 impl_item: surface::ImplItemFn,
448 ) -> Option<surface::ImplItemFn> {
449 if let Some(old) = self.impl_items.insert(owner_id, impl_item) {
450 return Some(old);
451 }
452 None
453 }
454}
455
456pub enum ExternSpecMappingErr {
459 IsLocal(LocalDefId),
462
463 Dup(LocalDefId),
472}
473
474#[derive(Default)]
475pub struct ResolverOutput {
476 pub path_res_map: UnordMap<NodeId, fhir::PartialRes>,
477 pub param_res_map: UnordMap<NodeId, (fhir::ParamId, fhir::ParamKind)>,
482 pub implicit_params: UnordMap<NodeId, Vec<(Ident, NodeId)>>,
486 pub sort_path_res_map: UnordMap<NodeId, fhir::SortRes>,
487 pub expr_path_res_map: UnordMap<NodeId, fhir::PartialRes<fhir::ParamId>>,
488 pub qualifier_res_map: UnordMap<NodeId, Vec<def_id::FluxLocalDefId>>,
491 pub reveal_res_map: UnordMap<NodeId, Vec<def_id::FluxDefId>>,
494}
495
496#[extension(pub trait PlaceExt)]
497impl flux_rustc_bridge::mir::Place {
498 fn ty(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<PlaceTy> {
499 self.projection
500 .iter()
501 .try_fold(PlaceTy::from_ty(local_decls[self.local].ty.clone()), |place_ty, elem| {
502 place_ty.projection_ty(genv, *elem)
503 })
504 }
505
506 fn behind_raw_ptr(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<bool> {
507 let mut place_ty = PlaceTy::from_ty(local_decls[self.local].ty.clone());
508 for elem in &self.projection {
509 if let (PlaceElem::Deref, ty::TyKind::RawPtr(..)) = (elem, place_ty.ty.kind()) {
510 return Ok(true);
511 }
512 place_ty = place_ty.projection_ty(genv, *elem)?;
513 }
514 Ok(false)
515 }
516}
517
518#[derive(Debug)]
519pub struct PlaceTy {
520 pub ty: ty::Ty,
521 pub variant_index: Option<VariantIdx>,
523}
524
525impl PlaceTy {
526 fn from_ty(ty: ty::Ty) -> PlaceTy {
527 PlaceTy { ty, variant_index: None }
528 }
529
530 fn projection_ty(&self, genv: GlobalEnv, elem: PlaceElem) -> QueryResult<PlaceTy> {
531 if self.variant_index.is_some() && !matches!(elem, PlaceElem::Field(..)) {
532 Err(query_bug!("cannot use non field projection on downcasted place"))?;
533 }
534 let place_ty = match elem {
535 PlaceElem::Deref => PlaceTy::from_ty(self.ty.deref()),
536 PlaceElem::Field(fld) => PlaceTy::from_ty(self.field_ty(genv, fld)?),
537 PlaceElem::Downcast(_, variant_idx) => {
538 PlaceTy { ty: self.ty.clone(), variant_index: Some(variant_idx) }
539 }
540 PlaceElem::Index(_) | PlaceElem::ConstantIndex { .. } => {
541 if let ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) = self.ty.kind() {
542 PlaceTy::from_ty(ty.clone())
543 } else {
544 return Err(query_bug!("cannot use non field projection on downcasted place"));
545 }
546 }
547 };
548 Ok(place_ty)
549 }
550
551 fn field_ty(&self, genv: GlobalEnv, f: FieldIdx) -> QueryResult<ty::Ty> {
552 match self.ty.kind() {
553 ty::TyKind::Adt(adt_def, args) => {
554 let variant_def = match self.variant_index {
555 None => adt_def.non_enum_variant(),
556 Some(variant_index) => {
557 assert!(adt_def.is_enum());
558 adt_def.variant(variant_index)
559 }
560 };
561 let field_def = &variant_def.fields[f];
562 let ty = genv.lower_type_of(field_def.did)?;
563 Ok(ty.subst(args))
564 }
565 ty::TyKind::Tuple(tys) => Ok(tys[f.index()].clone()),
566 ty::TyKind::Closure(_, args) => Ok(args.as_closure().upvar_tys()[f.index()].clone()),
567 _ => Err(query_bug!("extracting field of non-tuple non-adt non-closure: {self:?}")),
568 }
569 }
570}
571
572#[derive(Debug, Hash, Clone, Copy)]
577pub enum FixpointQueryKind {
578 Impl,
580 Body,
582 Invariant,
584}
585
586impl FixpointQueryKind {
587 pub fn ext(self) -> &'static str {
588 match self {
589 FixpointQueryKind::Impl => "sub.fluxc",
590 FixpointQueryKind::Body => "fluxc",
591 FixpointQueryKind::Invariant => "fluxc",
592 }
593 }
594
595 pub fn task_key(self, tcx: TyCtxt, def_id: DefId) -> String {
597 format!("{}###{:?}", tcx.def_path_str(def_id), self)
598 }
599}