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 pretty;
35pub mod queries;
36pub mod rty;
37mod sort_of;
38pub mod timings;
39
40use std::sync::LazyLock;
41
42use flux_arc_interner::List;
43use flux_config as config;
44use flux_macros::fluent_messages;
45pub use flux_rustc_bridge::def_id_to_string;
46use flux_rustc_bridge::{
47 mir::{LocalDecls, PlaceElem},
48 ty::{self, GenericArgsExt},
49};
50use flux_syntax::surface::{self, NodeId};
51use global_env::GlobalEnv;
52use liquid_fixpoint::ThyFunc;
53use queries::QueryResult;
54use rty::VariantIdx;
55use rustc_abi::FieldIdx;
56use rustc_data_structures::{
57 fx::FxIndexMap,
58 unord::{UnordMap, UnordSet},
59};
60use rustc_hir::OwnerId;
61use rustc_macros::extension;
62use rustc_middle::ty::TyCtxt;
63use rustc_span::{
64 Symbol,
65 def_id::{DefId, LocalDefId},
66 symbol::Ident,
67};
68
69fluent_messages! { "../locales/en-US.ftl" }
70
71pub struct TheoryFunc {
72 pub name: Symbol,
73 pub sort: rty::PolyFuncSort,
74 pub itf: liquid_fixpoint::ThyFunc,
75}
76
77pub static THEORY_FUNCS: LazyLock<UnordMap<liquid_fixpoint::ThyFunc, TheoryFunc>> =
78 LazyLock::new(|| {
79 use rty::{BvSize, Sort::*};
80 liquid_fixpoint::ThyFunc::ALL
81 .into_iter()
82 .filter_map(|func| {
83 let func = TheoryFunc {
84 name: Symbol::intern(name_of_thy_func(func)?),
85 itf: func,
86 sort: sort_of_thy_func(func)?,
87 };
88 Some(func)
89 })
90 .chain([
91 TheoryFunc {
93 name: Symbol::intern("bv_zero_extend_32_to_64"),
94 itf: liquid_fixpoint::ThyFunc::BvZeroExtend(32),
95 sort: rty::PolyFuncSort::new(
96 List::empty(),
97 rty::FuncSort::new(
98 vec![BitVec(BvSize::Fixed(32))],
99 BitVec(BvSize::Fixed(64)),
100 ),
101 ),
102 },
103 TheoryFunc {
104 name: Symbol::intern("bv_sign_extend_32_to_64"),
105 itf: liquid_fixpoint::ThyFunc::BvSignExtend(32),
106 sort: rty::PolyFuncSort::new(
107 List::empty(),
108 rty::FuncSort::new(
109 vec![BitVec(BvSize::Fixed(32))],
110 BitVec(BvSize::Fixed(64)),
111 ),
112 ),
113 },
114 ])
115 .map(|func| (func.itf, func))
116 .collect()
117 });
118
119pub fn name_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<&'static str> {
120 let name = match func {
121 ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
122 ThyFunc::StrLen => "str_len",
123 ThyFunc::IntToBv8 => "bv_int_to_bv8",
124 ThyFunc::Bv8ToInt => "bv_bv8_to_int",
125 ThyFunc::IntToBv32 => "bv_int_to_bv32",
126 ThyFunc::Bv32ToInt => "bv_bv32_to_int",
127 ThyFunc::IntToBv64 => "bv_int_to_bv64",
128 ThyFunc::Bv64ToInt => "bv_bv64_to_int",
129 ThyFunc::BvUge => "bv_uge",
130 ThyFunc::BvSge => "bv_sge",
131 ThyFunc::BvUdiv => "bv_udiv",
132 ThyFunc::BvSdiv => "bv_sdiv",
133 ThyFunc::BvSrem => "bv_srem",
134 ThyFunc::BvUrem => "bv_urem",
135 ThyFunc::BvLshr => "bv_lshr",
136 ThyFunc::BvAshr => "bv_ashr",
137 ThyFunc::BvAnd => "bv_and",
138 ThyFunc::BvOr => "bv_or",
139 ThyFunc::BvXor => "bv_xor",
140 ThyFunc::BvNot => "bv_not",
141 ThyFunc::BvAdd => "bv_add",
142 ThyFunc::BvNeg => "bv_neg",
143 ThyFunc::BvSub => "bv_sub",
144 ThyFunc::BvMul => "bv_mul",
145 ThyFunc::BvShl => "bv_shl",
146 ThyFunc::BvUle => "bv_ule",
147 ThyFunc::BvSle => "bv_sle",
148 ThyFunc::BvUgt => "bv_ugt",
149 ThyFunc::BvSgt => "bv_sgt",
150 ThyFunc::BvUlt => "bv_ult",
151 ThyFunc::BvSlt => "bv_slt",
152 ThyFunc::SetEmpty => "set_empty",
153 ThyFunc::SetSng => "set_singleton",
154 ThyFunc::SetCup => "set_union",
155 ThyFunc::SetMem => "set_is_in",
156 ThyFunc::MapDefault => "map_default",
157 ThyFunc::MapSelect => "map_select",
158 ThyFunc::MapStore => "map_store",
159 };
160 Some(name)
161}
162
163fn sort_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<rty::PolyFuncSort> {
164 use rty::{
165 BvSize, ParamSort,
166 Sort::{self, *},
167 SortCtor::*,
168 SortParamKind,
169 };
170 let param0 = ParamSort::from_u32(0);
171 let param1 = ParamSort::from_u32(1);
172 let bv_param0 = BvSize::Param(ParamSort::from_u32(0));
173
174 let sort = match func {
175 ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
176 ThyFunc::StrLen => {
177 rty::PolyFuncSort::new(List::empty(), rty::FuncSort::new(vec![rty::Sort::Str], Int))
179 }
180 ThyFunc::IntToBv8 => {
181 rty::PolyFuncSort::new(
183 List::empty(),
184 rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(8))),
185 )
186 }
187 ThyFunc::Bv8ToInt => {
188 rty::PolyFuncSort::new(
190 List::empty(),
191 rty::FuncSort::new(vec![BitVec(BvSize::Fixed(8))], Int),
192 )
193 }
194 ThyFunc::IntToBv32 => {
195 rty::PolyFuncSort::new(
197 List::empty(),
198 rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(32))),
199 )
200 }
201 ThyFunc::Bv32ToInt => {
202 rty::PolyFuncSort::new(
204 List::empty(),
205 rty::FuncSort::new(vec![BitVec(BvSize::Fixed(32))], Int),
206 )
207 }
208 ThyFunc::IntToBv64 => {
209 rty::PolyFuncSort::new(
211 List::empty(),
212 rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(64))),
213 )
214 }
215 ThyFunc::Bv64ToInt => {
216 rty::PolyFuncSort::new(
218 List::empty(),
219 rty::FuncSort::new(vec![BitVec(BvSize::Fixed(64))], Int),
220 )
221 }
222 ThyFunc::BvUdiv
223 | ThyFunc::BvSdiv
224 | ThyFunc::BvSrem
225 | ThyFunc::BvUrem
226 | ThyFunc::BvLshr
227 | ThyFunc::BvAshr
228 | ThyFunc::BvAnd
229 | ThyFunc::BvOr
230 | ThyFunc::BvXor
231 | ThyFunc::BvAdd
232 | ThyFunc::BvSub
233 | ThyFunc::BvMul
234 | ThyFunc::BvShl => {
235 rty::PolyFuncSort::new(
237 List::singleton(SortParamKind::BvSize),
238 rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], BitVec(bv_param0)),
239 )
240 }
241 ThyFunc::BvNot | ThyFunc::BvNeg => {
242 rty::PolyFuncSort::new(
244 List::singleton(SortParamKind::BvSize),
245 rty::FuncSort::new(vec![BitVec(bv_param0)], BitVec(bv_param0)),
246 )
247 }
248 ThyFunc::BvUgt
249 | ThyFunc::BvSgt
250 | ThyFunc::BvUlt
251 | ThyFunc::BvSlt
252 | ThyFunc::BvSle
253 | ThyFunc::BvUge
254 | ThyFunc::BvSge
255 | ThyFunc::BvUle => {
256 rty::PolyFuncSort::new(
258 List::singleton(SortParamKind::BvSize),
259 rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
260 )
261 }
262 ThyFunc::SetEmpty => {
263 rty::PolyFuncSort::new(
265 List::singleton(SortParamKind::Sort),
266 rty::FuncSort::new(vec![Int], Sort::app(Set, List::singleton(Var(param0)))),
267 )
268 }
269 ThyFunc::SetSng => {
270 rty::PolyFuncSort::new(
272 List::singleton(SortParamKind::Sort),
273 rty::FuncSort::new(vec![Var(param0)], Sort::app(Set, List::singleton(Var(param0)))),
274 )
275 }
276 ThyFunc::SetCup => {
277 rty::PolyFuncSort::new(
279 List::singleton(SortParamKind::Sort),
280 rty::FuncSort::new(
281 vec![
282 Sort::app(Set, List::singleton(Var(param0))),
283 Sort::app(Set, List::singleton(Var(param0))),
284 ],
285 Sort::app(Set, List::singleton(Var(param0))),
286 ),
287 )
288 }
289 ThyFunc::SetMem => {
290 rty::PolyFuncSort::new(
292 List::singleton(SortParamKind::Sort),
293 rty::FuncSort::new(
294 vec![Var(param0), Sort::app(Set, List::singleton(Var(param0)))],
295 Bool,
296 ),
297 )
298 }
299 ThyFunc::MapDefault => {
300 rty::PolyFuncSort::new(
302 List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
303 rty::FuncSort::new(
304 vec![Var(param1)],
305 Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
306 ),
307 )
308 }
309 ThyFunc::MapSelect => {
310 rty::PolyFuncSort::new(
312 List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
313 rty::FuncSort::new(
314 vec![Sort::app(Map, List::from_arr([Var(param0), Var(param1)])), Var(param0)],
315 Var(param1),
316 ),
317 )
318 }
319 ThyFunc::MapStore => {
320 rty::PolyFuncSort::new(
322 List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
323 rty::FuncSort::new(
324 vec![
325 Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
326 Var(param0),
327 Var(param1),
328 ],
329 Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
330 ),
331 )
332 }
333 };
334 Some(sort)
335}
336
337#[derive(Default)]
338pub struct Specs {
339 pub fn_sigs: UnordMap<OwnerId, surface::FnSpec>,
340 pub constants: UnordMap<OwnerId, surface::ConstantInfo>,
341 pub structs: UnordMap<OwnerId, surface::StructDef>,
342 pub traits: UnordMap<OwnerId, surface::Trait>,
343 pub impls: UnordMap<OwnerId, surface::Impl>,
344 pub enums: UnordMap<OwnerId, surface::EnumDef>,
345 pub flux_items_by_parent: FxIndexMap<OwnerId, Vec<surface::FluxItem>>,
346 pub ty_aliases: UnordMap<OwnerId, Option<surface::TyAlias>>,
347 pub ignores: UnordMap<LocalDefId, fhir::Ignored>,
348 pub trusted: UnordMap<LocalDefId, fhir::Trusted>,
349 pub trusted_impl: UnordMap<LocalDefId, fhir::Trusted>,
350 pub infer_opts: UnordMap<LocalDefId, config::PartialInferOpts>,
351 pub should_fail: UnordSet<LocalDefId>,
352 dummy_extern: UnordSet<LocalDefId>,
361 extern_id_to_local_id: UnordMap<DefId, LocalDefId>,
362 local_id_to_extern_id: UnordMap<LocalDefId, DefId>,
363}
364
365impl Specs {
366 pub fn insert_extern_spec_id_mapping(
367 &mut self,
368 local_id: LocalDefId,
369 extern_id: DefId,
370 ) -> Result<(), ExternSpecMappingErr> {
371 #[expect(
372 clippy::disallowed_methods,
373 reason = "we are inserting the extern spec mapping and we want to ensure it doesn't point to a local item"
374 )]
375 if let Some(local) = extern_id.as_local() {
376 return Err(ExternSpecMappingErr::IsLocal(local));
377 }
378 if let Err(err) = self.extern_id_to_local_id.try_insert(extern_id, local_id) {
379 return Err(ExternSpecMappingErr::Dup(*err.entry.get()));
380 }
381 self.local_id_to_extern_id.insert(local_id, extern_id);
382 Ok(())
383 }
384
385 pub fn insert_dummy(&mut self, def_id: LocalDefId) {
386 self.dummy_extern.insert(def_id);
387 }
388}
389
390pub enum ExternSpecMappingErr {
393 IsLocal(LocalDefId),
396
397 Dup(LocalDefId),
406}
407
408#[derive(Default)]
409pub struct ResolverOutput {
410 pub path_res_map: UnordMap<NodeId, fhir::PartialRes>,
411 pub impl_trait_res_map: UnordMap<NodeId, LocalDefId>,
412 pub param_res_map: UnordMap<NodeId, (fhir::ParamId, fhir::ParamKind)>,
417 pub implicit_params: UnordMap<NodeId, Vec<(Ident, NodeId)>>,
421 pub sort_path_res_map: UnordMap<NodeId, fhir::SortRes>,
422 pub expr_path_res_map: UnordMap<NodeId, fhir::Res<fhir::ParamId>>,
423 pub qualifier_res_map: UnordMap<OwnerId, Vec<def_id::FluxLocalDefId>>,
425 pub reveal_res_map: UnordMap<OwnerId, Vec<def_id::FluxDefId>>,
427}
428
429#[extension(pub trait PlaceExt)]
430impl flux_rustc_bridge::mir::Place {
431 fn ty(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<PlaceTy> {
432 self.projection
433 .iter()
434 .try_fold(PlaceTy::from_ty(local_decls[self.local].ty.clone()), |place_ty, elem| {
435 place_ty.projection_ty(genv, *elem)
436 })
437 }
438
439 fn behind_raw_ptr(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<bool> {
440 let mut place_ty = PlaceTy::from_ty(local_decls[self.local].ty.clone());
441 for elem in &self.projection {
442 if let (PlaceElem::Deref, ty::TyKind::RawPtr(..)) = (elem, place_ty.ty.kind()) {
443 return Ok(true);
444 }
445 place_ty = place_ty.projection_ty(genv, *elem)?;
446 }
447 Ok(false)
448 }
449}
450
451#[derive(Debug)]
452pub struct PlaceTy {
453 pub ty: ty::Ty,
454 pub variant_index: Option<VariantIdx>,
456}
457
458impl PlaceTy {
459 fn from_ty(ty: ty::Ty) -> PlaceTy {
460 PlaceTy { ty, variant_index: None }
461 }
462
463 fn projection_ty(&self, genv: GlobalEnv, elem: PlaceElem) -> QueryResult<PlaceTy> {
464 if self.variant_index.is_some() && !matches!(elem, PlaceElem::Field(..)) {
465 Err(query_bug!("cannot use non field projection on downcasted place"))?;
466 }
467 let place_ty = match elem {
468 PlaceElem::Deref => PlaceTy::from_ty(self.ty.deref()),
469 PlaceElem::Field(fld) => PlaceTy::from_ty(self.field_ty(genv, fld)?),
470 PlaceElem::Downcast(_, variant_idx) => {
471 PlaceTy { ty: self.ty.clone(), variant_index: Some(variant_idx) }
472 }
473 PlaceElem::Index(_) | PlaceElem::ConstantIndex { .. } => {
474 if let ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) = self.ty.kind() {
475 PlaceTy::from_ty(ty.clone())
476 } else {
477 return Err(query_bug!("cannot use non field projection on downcasted place"));
478 }
479 }
480 };
481 Ok(place_ty)
482 }
483
484 fn field_ty(&self, genv: GlobalEnv, f: FieldIdx) -> QueryResult<ty::Ty> {
485 match self.ty.kind() {
486 ty::TyKind::Adt(adt_def, args) => {
487 let variant_def = match self.variant_index {
488 None => adt_def.non_enum_variant(),
489 Some(variant_index) => {
490 assert!(adt_def.is_enum());
491 adt_def.variant(variant_index)
492 }
493 };
494 let field_def = &variant_def.fields[f];
495 let ty = genv.lower_type_of(field_def.did)?;
496 Ok(ty.subst(args))
497 }
498 ty::TyKind::Tuple(tys) => Ok(tys[f.index()].clone()),
499 ty::TyKind::Closure(_, args) => Ok(args.as_closure().upvar_tys()[f.index()].clone()),
500 _ => Err(query_bug!("extracting field of non-tuple non-adt non-closure: {self:?}")),
501 }
502 }
503}
504
505#[derive(Debug, Hash, Clone, Copy)]
510pub enum FixpointQueryKind {
511 Impl,
513 Body,
515 Invariant,
517}
518
519impl FixpointQueryKind {
520 pub fn ext(self) -> &'static str {
521 match self {
522 FixpointQueryKind::Impl => "sub.fluxc",
523 FixpointQueryKind::Body => "fluxc",
524 FixpointQueryKind::Invariant => "fluxc",
525 }
526 }
527
528 pub fn task_key(self, tcx: TyCtxt, def_id: DefId) -> String {
530 format!("{}###{:?}", tcx.def_path_str(def_id), self)
531 }
532}