flux_middle/
lib.rs

1//! This crate contains common type definitions that are used by other crates.
2#![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_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                // we can't express these as function types so we add special case
91                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::IntToBv8 => "bv_int_to_bv8",
123        ThyFunc::Bv8ToInt => "bv_bv8_to_int",
124        ThyFunc::IntToBv32 => "bv_int_to_bv32",
125        ThyFunc::Bv32ToInt => "bv_bv32_to_int",
126        ThyFunc::IntToBv64 => "bv_int_to_bv64",
127        ThyFunc::Bv64ToInt => "bv_bv64_to_int",
128        ThyFunc::BvUge => "bv_uge",
129        ThyFunc::BvSge => "bv_sge",
130        ThyFunc::BvUdiv => "bv_udiv",
131        ThyFunc::BvSdiv => "bv_sdiv",
132        ThyFunc::BvSrem => "bv_srem",
133        ThyFunc::BvUrem => "bv_urem",
134        ThyFunc::BvLshr => "bv_lshr",
135        ThyFunc::BvAshr => "bv_ashr",
136        ThyFunc::BvAnd => "bv_and",
137        ThyFunc::BvOr => "bv_or",
138        ThyFunc::BvXor => "bv_xor",
139        ThyFunc::BvNot => "bv_not",
140        ThyFunc::BvAdd => "bv_add",
141        ThyFunc::BvNeg => "bv_neg",
142        ThyFunc::BvSub => "bv_sub",
143        ThyFunc::BvMul => "bv_mul",
144        ThyFunc::BvShl => "bv_shl",
145        ThyFunc::BvUle => "bv_ule",
146        ThyFunc::BvSle => "bv_sle",
147        ThyFunc::BvUgt => "bv_ugt",
148        ThyFunc::BvSgt => "bv_sgt",
149        ThyFunc::BvUlt => "bv_ult",
150        ThyFunc::BvSlt => "bv_slt",
151        ThyFunc::SetEmpty => "set_empty",
152        ThyFunc::SetSng => "set_singleton",
153        ThyFunc::SetCup => "set_union",
154        ThyFunc::SetCap => "set_intersection",
155        ThyFunc::SetDif => "set_difference",
156        ThyFunc::SetSub => "set_subset",
157        ThyFunc::SetMem => "set_is_in",
158        ThyFunc::MapDefault => "map_default",
159        ThyFunc::MapSelect => "map_select",
160        ThyFunc::MapStore => "map_store",
161    };
162    Some(name)
163}
164
165fn sort_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<rty::PolyFuncSort> {
166    use rty::{
167        BvSize, ParamSort,
168        Sort::{self, *},
169        SortCtor::*,
170        SortParamKind,
171    };
172    let param0 = ParamSort::from_u32(0);
173    let param1 = ParamSort::from_u32(1);
174    let bv_param0 = BvSize::Param(ParamSort::from_u32(0));
175
176    let sort = match func {
177        ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
178        ThyFunc::StrLen => {
179            // str -> int
180            rty::PolyFuncSort::new(List::empty(), rty::FuncSort::new(vec![rty::Sort::Str], Int))
181        }
182        ThyFunc::IntToBv8 => {
183            // int -> BitVec<8>
184            rty::PolyFuncSort::new(
185                List::empty(),
186                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(8))),
187            )
188        }
189        ThyFunc::Bv8ToInt => {
190            // BitVec<8> -> int
191            rty::PolyFuncSort::new(
192                List::empty(),
193                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(8))], Int),
194            )
195        }
196        ThyFunc::IntToBv32 => {
197            // int -> BitVec<32>
198            rty::PolyFuncSort::new(
199                List::empty(),
200                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(32))),
201            )
202        }
203        ThyFunc::Bv32ToInt => {
204            // BitVec<32> -> int
205            rty::PolyFuncSort::new(
206                List::empty(),
207                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(32))], Int),
208            )
209        }
210        ThyFunc::IntToBv64 => {
211            // int -> BitVec<64>
212            rty::PolyFuncSort::new(
213                List::empty(),
214                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(64))),
215            )
216        }
217        ThyFunc::Bv64ToInt => {
218            // BitVec<64> -> int
219            rty::PolyFuncSort::new(
220                List::empty(),
221                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(64))], Int),
222            )
223        }
224        ThyFunc::BvUdiv
225        | ThyFunc::BvSdiv
226        | ThyFunc::BvSrem
227        | ThyFunc::BvUrem
228        | ThyFunc::BvLshr
229        | ThyFunc::BvAshr
230        | ThyFunc::BvAnd
231        | ThyFunc::BvOr
232        | ThyFunc::BvXor
233        | ThyFunc::BvAdd
234        | ThyFunc::BvSub
235        | ThyFunc::BvMul
236        | ThyFunc::BvShl => {
237            // ∀s. (BitVec<s>, BitVec<s>) -> BitVec<s>
238            rty::PolyFuncSort::new(
239                List::singleton(SortParamKind::BvSize),
240                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], BitVec(bv_param0)),
241            )
242        }
243        ThyFunc::BvNot | ThyFunc::BvNeg => {
244            // ∀s. BitVec<s> -> BitVec<s>
245            rty::PolyFuncSort::new(
246                List::singleton(SortParamKind::BvSize),
247                rty::FuncSort::new(vec![BitVec(bv_param0)], BitVec(bv_param0)),
248            )
249        }
250        ThyFunc::BvUgt
251        | ThyFunc::BvSgt
252        | ThyFunc::BvUlt
253        | ThyFunc::BvSlt
254        | ThyFunc::BvSle
255        | ThyFunc::BvUge
256        | ThyFunc::BvSge
257        | ThyFunc::BvUle => {
258            // ∀s. (BitVec<s>, BitVec<s>) -> bool
259            rty::PolyFuncSort::new(
260                List::singleton(SortParamKind::BvSize),
261                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
262            )
263        }
264        ThyFunc::SetEmpty => {
265            // ∀s. int -> Set<S> why does this take an int?
266            rty::PolyFuncSort::new(
267                List::singleton(SortParamKind::Sort),
268                rty::FuncSort::new(vec![Int], Sort::app(Set, List::singleton(Var(param0)))),
269            )
270        }
271        ThyFunc::SetSng => {
272            // ∀s. s -> Set<S>
273            rty::PolyFuncSort::new(
274                List::singleton(SortParamKind::Sort),
275                rty::FuncSort::new(vec![Var(param0)], Sort::app(Set, List::singleton(Var(param0)))),
276            )
277        }
278        ThyFunc::SetCup | ThyFunc::SetCap | ThyFunc::SetDif => {
279            // ∀s. (Set<S>, Set<S>) -> Set<S>
280            rty::PolyFuncSort::new(
281                List::singleton(SortParamKind::Sort),
282                rty::FuncSort::new(
283                    vec![
284                        Sort::app(Set, List::singleton(Var(param0))),
285                        Sort::app(Set, List::singleton(Var(param0))),
286                    ],
287                    Sort::app(Set, List::singleton(Var(param0))),
288                ),
289            )
290        }
291        ThyFunc::SetMem => {
292            // ∀s. (s, Set<S>) -> bool
293            rty::PolyFuncSort::new(
294                List::singleton(SortParamKind::Sort),
295                rty::FuncSort::new(
296                    vec![Var(param0), Sort::app(Set, List::singleton(Var(param0)))],
297                    Bool,
298                ),
299            )
300        }
301        ThyFunc::SetSub => {
302            // ∀s. (Set<s>, Set<s>) -> bool
303            rty::PolyFuncSort::new(
304                List::singleton(SortParamKind::Sort),
305                rty::FuncSort::new(
306                    vec![
307                        Sort::app(Set, List::singleton(Var(param0))),
308                        Sort::app(Set, List::singleton(Var(param0))),
309                    ],
310                    Bool,
311                ),
312            )
313        }
314
315        ThyFunc::MapDefault => {
316            // ∀k,v. v -> Map<k,v>
317            rty::PolyFuncSort::new(
318                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
319                rty::FuncSort::new(
320                    vec![Var(param1)],
321                    Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
322                ),
323            )
324        }
325        ThyFunc::MapSelect => {
326            // ∀k,v. (Map<k,v>, k) -> v
327            rty::PolyFuncSort::new(
328                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
329                rty::FuncSort::new(
330                    vec![Sort::app(Map, List::from_arr([Var(param0), Var(param1)])), Var(param0)],
331                    Var(param1),
332                ),
333            )
334        }
335        ThyFunc::MapStore => {
336            // ∀k,v. (Map<k,v>, k, v) -> Map<k, v>
337            rty::PolyFuncSort::new(
338                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
339                rty::FuncSort::new(
340                    vec![
341                        Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
342                        Var(param0),
343                        Var(param1),
344                    ],
345                    Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
346                ),
347            )
348        }
349    };
350    Some(sort)
351}
352
353#[derive(Default)]
354pub struct Specs {
355    items: UnordMap<OwnerId, surface::Item>,
356    trait_items: UnordMap<OwnerId, surface::TraitItemFn>,
357    impl_items: UnordMap<OwnerId, surface::ImplItemFn>,
358    pub flux_items_by_parent: FxIndexMap<OwnerId, Vec<surface::FluxItem>>,
359    /// Set of dummy items generated by the extern spec macro we must completely ignore. This is
360    /// not the same as [ignored items] because, for ignored items, we still need to return errors
361    /// for queries and handle them gracefully in order to report them at the use it.
362    ///
363    /// If an item is in this set, all its descendants are also consider dummy (but they may not be
364    /// in the set).
365    ///
366    /// [ignored items]: Specs::ignores
367    dummy_extern: UnordSet<LocalDefId>,
368    extern_id_to_local_id: UnordMap<DefId, LocalDefId>,
369    local_id_to_extern_id: UnordMap<LocalDefId, DefId>,
370}
371
372impl Specs {
373    pub fn insert_extern_spec_id_mapping(
374        &mut self,
375        local_id: LocalDefId,
376        extern_id: DefId,
377    ) -> Result<(), ExternSpecMappingErr> {
378        #[expect(
379            clippy::disallowed_methods,
380            reason = "we are inserting the extern spec mapping and we want to ensure it doesn't point to a local item"
381        )]
382        if let Some(local) = extern_id.as_local() {
383            return Err(ExternSpecMappingErr::IsLocal(local));
384        }
385        if let Err(err) = self.extern_id_to_local_id.try_insert(extern_id, local_id) {
386            return Err(ExternSpecMappingErr::Dup(*err.entry.get()));
387        }
388        self.local_id_to_extern_id.insert(local_id, extern_id);
389        Ok(())
390    }
391
392    pub fn insert_dummy(&mut self, def_id: LocalDefId) {
393        self.dummy_extern.insert(def_id);
394    }
395
396    pub fn get_item(&self, owner_id: OwnerId) -> Option<&surface::Item> {
397        self.items.get(&owner_id)
398    }
399
400    pub fn insert_item(&mut self, owner_id: OwnerId, item: surface::Item) -> Option<surface::Item> {
401        if let Some(old) = self.items.insert(owner_id, item) {
402            return Some(old);
403        }
404        None
405    }
406
407    pub fn get_trait_item(&self, owner_id: OwnerId) -> Option<&surface::TraitItemFn> {
408        self.trait_items.get(&owner_id)
409    }
410
411    pub fn insert_trait_item(
412        &mut self,
413        owner_id: OwnerId,
414        trait_item: surface::TraitItemFn,
415    ) -> Option<surface::TraitItemFn> {
416        if let Some(old) = self.trait_items.insert(owner_id, trait_item) {
417            return Some(old);
418        }
419        None
420    }
421
422    pub fn get_impl_item(&self, owner_id: OwnerId) -> Option<&surface::ImplItemFn> {
423        self.impl_items.get(&owner_id)
424    }
425
426    pub fn insert_impl_item(
427        &mut self,
428        owner_id: OwnerId,
429        impl_item: surface::ImplItemFn,
430    ) -> Option<surface::ImplItemFn> {
431        if let Some(old) = self.impl_items.insert(owner_id, impl_item) {
432            return Some(old);
433        }
434        None
435    }
436}
437
438/// Represents errors that can occur when inserting a mapping between a `LocalDefId` and a `DefId`
439/// for an extern spec.
440pub enum ExternSpecMappingErr {
441    /// Indicates that the [`DefId`] we are trying to add extern specs to is actually local. Returns
442    /// the [`DefId`] as a [`LocalDefId`].
443    IsLocal(LocalDefId),
444
445    /// Indicates that there is an existing extern spec for the given extern id. Returns the existing
446    /// `LocalDefId` that maps to the extern id.
447    ///
448    /// NOTE: This currently only considers extern specs defined in the local crate. There could still
449    /// be duplicates if an extern spec is imported from an external crate. In such cases, the local
450    /// extern spec takes precedence. Probably, we should at least warn about this, but it's a bit
451    /// tricky because we need to look at the crate metadata which we don't have handy when
452    /// collecting specs.
453    Dup(LocalDefId),
454}
455
456#[derive(Default)]
457pub struct ResolverOutput {
458    pub path_res_map: UnordMap<NodeId, fhir::PartialRes>,
459    /// Resolution of explicitly and implicitly scoped parameters. The [`fhir::ParamId`] is unique
460    /// per item. The [`NodeId`] used as the key corresponds to the node introducing the parameter.
461    /// When explicit, this is the id of the [`surface::GenericArg`] or [`surface::RefineParam`],
462    /// when implicit, this is the id of the [`surface::RefineArg::Bind`] or [`surface::FnInput`].
463    pub param_res_map: UnordMap<NodeId, (fhir::ParamId, fhir::ParamKind)>,
464    /// List of implicitly scoped params defined in a scope. The [`NodeId`] used as key is the id of
465    /// the node introducing the scope, e.g., [`surface::FnSig`], [`surface::FnOutput`], or
466    /// [`surface::VariantDef`]. The [`NodeId`]s in the vectors are keys in [`Self::param_res_map`].
467    pub implicit_params: UnordMap<NodeId, Vec<(Ident, NodeId)>>,
468    pub sort_path_res_map: UnordMap<NodeId, fhir::SortRes>,
469    pub expr_path_res_map: UnordMap<NodeId, fhir::PartialRes<fhir::ParamId>>,
470    /// The resolved list of local qualifiers per function.
471    /// The [`NodeId`] corresponds to the [`surface::FnSpec`].
472    pub qualifier_res_map: UnordMap<NodeId, Vec<def_id::FluxLocalDefId>>,
473    /// The resolved list of local reveals per function
474    /// The [`NodeId`] corresponds to the [`surface::FnSpec`].
475    pub reveal_res_map: UnordMap<NodeId, Vec<def_id::FluxDefId>>,
476}
477
478#[extension(pub trait PlaceExt)]
479impl flux_rustc_bridge::mir::Place {
480    fn ty(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<PlaceTy> {
481        self.projection
482            .iter()
483            .try_fold(PlaceTy::from_ty(local_decls[self.local].ty.clone()), |place_ty, elem| {
484                place_ty.projection_ty(genv, *elem)
485            })
486    }
487
488    fn behind_raw_ptr(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<bool> {
489        let mut place_ty = PlaceTy::from_ty(local_decls[self.local].ty.clone());
490        for elem in &self.projection {
491            if let (PlaceElem::Deref, ty::TyKind::RawPtr(..)) = (elem, place_ty.ty.kind()) {
492                return Ok(true);
493            }
494            place_ty = place_ty.projection_ty(genv, *elem)?;
495        }
496        Ok(false)
497    }
498}
499
500#[derive(Debug)]
501pub struct PlaceTy {
502    pub ty: ty::Ty,
503    /// Downcast to a particular variant of an enum or a generator, if included.
504    pub variant_index: Option<VariantIdx>,
505}
506
507impl PlaceTy {
508    fn from_ty(ty: ty::Ty) -> PlaceTy {
509        PlaceTy { ty, variant_index: None }
510    }
511
512    fn projection_ty(&self, genv: GlobalEnv, elem: PlaceElem) -> QueryResult<PlaceTy> {
513        if self.variant_index.is_some() && !matches!(elem, PlaceElem::Field(..)) {
514            Err(query_bug!("cannot use non field projection on downcasted place"))?;
515        }
516        let place_ty = match elem {
517            PlaceElem::Deref => PlaceTy::from_ty(self.ty.deref()),
518            PlaceElem::Field(fld) => PlaceTy::from_ty(self.field_ty(genv, fld)?),
519            PlaceElem::Downcast(_, variant_idx) => {
520                PlaceTy { ty: self.ty.clone(), variant_index: Some(variant_idx) }
521            }
522            PlaceElem::Index(_) | PlaceElem::ConstantIndex { .. } => {
523                if let ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) = self.ty.kind() {
524                    PlaceTy::from_ty(ty.clone())
525                } else {
526                    return Err(query_bug!("cannot use non field projection on downcasted place"));
527                }
528            }
529        };
530        Ok(place_ty)
531    }
532
533    fn field_ty(&self, genv: GlobalEnv, f: FieldIdx) -> QueryResult<ty::Ty> {
534        match self.ty.kind() {
535            ty::TyKind::Adt(adt_def, args) => {
536                let variant_def = match self.variant_index {
537                    None => adt_def.non_enum_variant(),
538                    Some(variant_index) => {
539                        assert!(adt_def.is_enum());
540                        adt_def.variant(variant_index)
541                    }
542                };
543                let field_def = &variant_def.fields[f];
544                let ty = genv.lower_type_of(field_def.did)?;
545                Ok(ty.subst(args))
546            }
547            ty::TyKind::Tuple(tys) => Ok(tys[f.index()].clone()),
548            ty::TyKind::Closure(_, args) => Ok(args.as_closure().upvar_tys()[f.index()].clone()),
549            _ => Err(query_bug!("extracting field of non-tuple non-adt non-closure: {self:?}")),
550        }
551    }
552}
553
554/// The different reasons we issue fixpoint queries. This is used to dissambiguate queries that
555/// are issued for the same item.
556///
557/// NOTE: This is defined here because it's also used in [`timings`]
558#[derive(Debug, Hash, Clone, Copy)]
559pub enum FixpointQueryKind {
560    /// Query issued when checking an impl method is a subtype of the trait
561    Impl,
562    /// Query issued to check the body of a function
563    Body,
564    /// Query issued to check an (enum) invariant is implied by the type definition
565    Invariant,
566}
567
568impl FixpointQueryKind {
569    pub fn ext(self) -> &'static str {
570        match self {
571            FixpointQueryKind::Impl => "sub.fluxc",
572            FixpointQueryKind::Body => "fluxc",
573            FixpointQueryKind::Invariant => "fluxc",
574        }
575    }
576
577    /// A string that uniquely identifies a query given an item `DefId`
578    pub fn task_key(self, tcx: TyCtxt, def_id: DefId) -> String {
579        format!("{}###{:?}", tcx.def_path_str(def_id), self)
580    }
581}
flux_middle/lib.rs

flux_middle/
lib.rs
