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    let_chains,
8    map_try_insert,
9    min_specialization,
10    never_type,
11    rustc_private,
12    unwrap_infallible,
13    new_range_api
14)]
15
16extern crate rustc_abi;
17extern crate rustc_ast;
18extern crate rustc_data_structures;
19extern crate rustc_errors;
20extern crate rustc_hir;
21extern crate rustc_index;
22extern crate rustc_macros;
23extern crate rustc_middle;
24extern crate rustc_serialize;
25extern crate rustc_span;
26extern crate rustc_type_ir;
27
28extern crate self as flux_middle;
29
30pub mod big_int;
31pub mod cstore;
32pub mod def_id;
33pub mod fhir;
34pub mod global_env;
35pub mod pretty;
36pub mod queries;
37pub mod rty;
38mod sort_of;
39pub mod timings;
40
41use std::sync::LazyLock;
42
43use flux_arc_interner::List;
44use flux_config as config;
45use flux_macros::fluent_messages;
46pub use flux_rustc_bridge::def_id_to_string;
47use flux_rustc_bridge::{
48    mir::{LocalDecls, PlaceElem},
49    ty::{self, GenericArgsExt},
50};
51use flux_syntax::surface::{self, NodeId};
52use global_env::GlobalEnv;
53use liquid_fixpoint::ThyFunc;
54use queries::QueryResult;
55use rty::VariantIdx;
56use rustc_abi::FieldIdx;
57use rustc_data_structures::{
58    fx::FxIndexMap,
59    unord::{UnordMap, UnordSet},
60};
61use rustc_hir::OwnerId;
62use rustc_macros::extension;
63use rustc_middle::ty::TyCtxt;
64use rustc_span::{
65    Symbol,
66    def_id::{DefId, LocalDefId},
67    symbol::Ident,
68};
69
70fluent_messages! { "../locales/en-US.ftl" }
71
72pub struct TheoryFunc {
73    pub name: Symbol,
74    pub sort: rty::PolyFuncSort,
75    pub itf: liquid_fixpoint::ThyFunc,
76}
77
78pub static THEORY_FUNCS: LazyLock<UnordMap<liquid_fixpoint::ThyFunc, TheoryFunc>> =
79    LazyLock::new(|| {
80        use rty::{BvSize, Sort::*};
81        liquid_fixpoint::ThyFunc::ALL
82            .into_iter()
83            .filter_map(|func| {
84                let func = TheoryFunc {
85                    name: Symbol::intern(name_of_thy_func(func)?),
86                    itf: func,
87                    sort: sort_of_thy_func(func)?,
88                };
89                Some(func)
90            })
91            .chain([
92                // we can't express these as function types so we add special case
93                TheoryFunc {
94                    name: Symbol::intern("bv_zero_extend_32_to_64"),
95                    itf: liquid_fixpoint::ThyFunc::BvZeroExtend(32),
96                    sort: rty::PolyFuncSort::new(
97                        List::empty(),
98                        rty::FuncSort::new(
99                            vec![BitVec(BvSize::Fixed(32))],
100                            BitVec(BvSize::Fixed(64)),
101                        ),
102                    ),
103                },
104                TheoryFunc {
105                    name: Symbol::intern("bv_sign_extend_32_to_64"),
106                    itf: liquid_fixpoint::ThyFunc::BvSignExtend(32),
107                    sort: rty::PolyFuncSort::new(
108                        List::empty(),
109                        rty::FuncSort::new(
110                            vec![BitVec(BvSize::Fixed(32))],
111                            BitVec(BvSize::Fixed(64)),
112                        ),
113                    ),
114                },
115            ])
116            .map(|func| (func.itf, func))
117            .collect()
118    });
119
120pub fn name_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<&'static str> {
121    let name = match func {
122        ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
123        ThyFunc::StrLen => "str_len",
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::SetMem => "set_is_in",
155        ThyFunc::MapDefault => "map_default",
156        ThyFunc::MapSelect => "map_select",
157        ThyFunc::MapStore => "map_store",
158    };
159    Some(name)
160}
161
162fn sort_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<rty::PolyFuncSort> {
163    use rty::{
164        BvSize, ParamSort,
165        Sort::{self, *},
166        SortCtor::*,
167        SortParamKind,
168    };
169    let param0 = ParamSort::from_u32(0);
170    let param1 = ParamSort::from_u32(1);
171    let bv_param0 = BvSize::Param(ParamSort::from_u32(0));
172
173    let sort = match func {
174        ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
175        ThyFunc::StrLen => {
176            // str -> int
177            rty::PolyFuncSort::new(List::empty(), rty::FuncSort::new(vec![rty::Sort::Str], Int))
178        }
179        ThyFunc::IntToBv32 => {
180            // int -> BitVec<32>
181            rty::PolyFuncSort::new(
182                List::empty(),
183                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(32))),
184            )
185        }
186        ThyFunc::Bv32ToInt => {
187            // BitVec<32> -> int
188            rty::PolyFuncSort::new(
189                List::empty(),
190                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(32))], Int),
191            )
192        }
193        ThyFunc::IntToBv64 => {
194            // int -> BitVec<64>
195            rty::PolyFuncSort::new(
196                List::empty(),
197                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(64))),
198            )
199        }
200        ThyFunc::Bv64ToInt => {
201            // BitVec<64> -> int
202            rty::PolyFuncSort::new(
203                List::empty(),
204                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(64))], Int),
205            )
206        }
207        ThyFunc::BvUdiv
208        | ThyFunc::BvSdiv
209        | ThyFunc::BvSrem
210        | ThyFunc::BvUrem
211        | ThyFunc::BvLshr
212        | ThyFunc::BvAshr
213        | ThyFunc::BvAnd
214        | ThyFunc::BvOr
215        | ThyFunc::BvXor
216        | ThyFunc::BvAdd
217        | ThyFunc::BvSub
218        | ThyFunc::BvMul
219        | ThyFunc::BvShl => {
220            // ∀s. (BitVec<s>, BitVec<s>) -> BitVec<s>
221            rty::PolyFuncSort::new(
222                List::singleton(SortParamKind::BvSize),
223                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], BitVec(bv_param0)),
224            )
225        }
226        ThyFunc::BvNot | ThyFunc::BvNeg => {
227            // ∀s. BitVec<s> -> BitVec<s>
228            rty::PolyFuncSort::new(
229                List::singleton(SortParamKind::BvSize),
230                rty::FuncSort::new(vec![BitVec(bv_param0)], BitVec(bv_param0)),
231            )
232        }
233        ThyFunc::BvUgt
234        | ThyFunc::BvSgt
235        | ThyFunc::BvUlt
236        | ThyFunc::BvSlt
237        | ThyFunc::BvSle
238        | ThyFunc::BvUge
239        | ThyFunc::BvSge
240        | ThyFunc::BvUle => {
241            // ∀s. (BitVec<s>, BitVec<s>) -> bool
242            rty::PolyFuncSort::new(
243                List::singleton(SortParamKind::BvSize),
244                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
245            )
246        }
247        ThyFunc::SetEmpty => {
248            // ∀s. int -> Set<S> why does this take an int?
249            rty::PolyFuncSort::new(
250                List::singleton(SortParamKind::Sort),
251                rty::FuncSort::new(vec![Int], Sort::app(Set, List::singleton(Var(param0)))),
252            )
253        }
254        ThyFunc::SetSng => {
255            // ∀s. s -> Set<S>
256            rty::PolyFuncSort::new(
257                List::singleton(SortParamKind::Sort),
258                rty::FuncSort::new(vec![Var(param0)], Sort::app(Set, List::singleton(Var(param0)))),
259            )
260        }
261        ThyFunc::SetCup => {
262            // ∀s. (Set<S>, Set<S>) -> Set<S>
263            rty::PolyFuncSort::new(
264                List::singleton(SortParamKind::Sort),
265                rty::FuncSort::new(
266                    vec![
267                        Sort::app(Set, List::singleton(Var(param0))),
268                        Sort::app(Set, List::singleton(Var(param0))),
269                    ],
270                    Sort::app(Set, List::singleton(Var(param0))),
271                ),
272            )
273        }
274        ThyFunc::SetMem => {
275            // ∀s. (s, Set<S>) -> bool
276            rty::PolyFuncSort::new(
277                List::singleton(SortParamKind::Sort),
278                rty::FuncSort::new(
279                    vec![Var(param0), Sort::app(Set, List::singleton(Var(param0)))],
280                    Bool,
281                ),
282            )
283        }
284        ThyFunc::MapDefault => {
285            // ∀k,v. v -> Map<k,v>
286            rty::PolyFuncSort::new(
287                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
288                rty::FuncSort::new(
289                    vec![Var(param1)],
290                    Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
291                ),
292            )
293        }
294        ThyFunc::MapSelect => {
295            // ∀k,v. (Map<k,v>, k) -> v
296            rty::PolyFuncSort::new(
297                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
298                rty::FuncSort::new(
299                    vec![Sort::app(Map, List::from_arr([Var(param0), Var(param1)])), Var(param0)],
300                    Var(param1),
301                ),
302            )
303        }
304        ThyFunc::MapStore => {
305            // ∀k,v. (Map<k,v>, k, v) -> Map<k, v>
306            rty::PolyFuncSort::new(
307                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
308                rty::FuncSort::new(
309                    vec![
310                        Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
311                        Var(param0),
312                        Var(param1),
313                    ],
314                    Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
315                ),
316            )
317        }
318    };
319    Some(sort)
320}
321
322#[derive(Default)]
323pub struct Specs {
324    pub fn_sigs: UnordMap<OwnerId, surface::FnSpec>,
325    pub constants: UnordMap<OwnerId, surface::ConstantInfo>,
326    pub structs: UnordMap<OwnerId, surface::StructDef>,
327    pub traits: UnordMap<OwnerId, surface::Trait>,
328    pub impls: UnordMap<OwnerId, surface::Impl>,
329    pub enums: UnordMap<OwnerId, surface::EnumDef>,
330    pub flux_items_by_parent: FxIndexMap<OwnerId, Vec<surface::Item>>,
331    pub ty_aliases: UnordMap<OwnerId, Option<surface::TyAlias>>,
332    pub ignores: UnordMap<LocalDefId, fhir::Ignored>,
333    pub trusted: UnordMap<LocalDefId, fhir::Trusted>,
334    pub trusted_impl: UnordMap<LocalDefId, fhir::Trusted>,
335    pub infer_opts: UnordMap<LocalDefId, config::PartialInferOpts>,
336    pub should_fail: UnordSet<LocalDefId>,
337    /// Set of dummy items generated by the extern spec macro we must completely ignore. This is
338    /// not the same as [ignored items] because, for ignored items, we still need to return errors
339    /// for queries and handle them gracefully in order to report them at the use it.
340    ///
341    /// If an item is in this set, all its descendants are also consider dummy (but they may not be
342    /// in the set).
343    ///
344    /// [ignored items]: Specs::ignores
345    dummy_extern: UnordSet<LocalDefId>,
346    extern_id_to_local_id: UnordMap<DefId, LocalDefId>,
347    local_id_to_extern_id: UnordMap<LocalDefId, DefId>,
348}
349
350impl Specs {
351    pub fn insert_extern_spec_id_mapping(
352        &mut self,
353        local_id: LocalDefId,
354        extern_id: DefId,
355    ) -> Result<(), ExternSpecMappingErr> {
356        #[expect(
357            clippy::disallowed_methods,
358            reason = "we are inserting the extern spec mapping and we want to ensure it doesn't point to a local item"
359        )]
360        if let Some(local) = extern_id.as_local() {
361            return Err(ExternSpecMappingErr::IsLocal(local));
362        }
363        if let Err(err) = self.extern_id_to_local_id.try_insert(extern_id, local_id) {
364            return Err(ExternSpecMappingErr::Dup(*err.entry.get()));
365        }
366        self.local_id_to_extern_id.insert(local_id, extern_id);
367        Ok(())
368    }
369
370    pub fn insert_dummy(&mut self, owner_id: OwnerId) {
371        self.dummy_extern.insert(owner_id.def_id);
372    }
373}
374
375/// Represents errors that can occur when inserting a mapping between a `LocalDefId` and a `DefId`
376/// for an extern spec.
377pub enum ExternSpecMappingErr {
378    /// Indicates that the [`DefId`] we are trying to add extern specs to is actually local. Returns
379    /// the [`DefId`] as a [`LocalDefId`].
380    IsLocal(LocalDefId),
381
382    /// Indicates that there is an existing extern spec for the given extern id. Returns the existing
383    /// `LocalDefId` that maps to the extern id.
384    ///
385    /// NOTE: This currently only considers extern specs defined in the local crate. There could still
386    /// be duplicates if an extern spec is imported from an external crate. In such cases, the local
387    /// extern spec takes precedence. Probably, we should at least warn about this, but it's a bit
388    /// tricky because we need to look at the crate metadata which we don't have handy when
389    /// collecting specs.
390    Dup(LocalDefId),
391}
392
393#[derive(Default)]
394pub struct ResolverOutput {
395    pub path_res_map: UnordMap<NodeId, fhir::PartialRes>,
396    pub impl_trait_res_map: UnordMap<NodeId, LocalDefId>,
397    /// Resolution of explicitly and implicitly scoped parameters. The [`fhir::ParamId`] is unique
398    /// per item. The [`NodeId`] used as the key corresponds to the node introducing the parameter.
399    /// When explicit, this is the id of the [`surface::GenericArg`] or [`surface::RefineParam`],
400    /// when implicit, this is the id of the [`surface::RefineArg::Bind`] or [`surface::FnInput`].
401    pub param_res_map: UnordMap<NodeId, (fhir::ParamId, fhir::ParamKind)>,
402    /// List of implicitly scoped params defined in a scope. The [`NodeId`] used as key is the id of
403    /// the node introducing the scope, e.g., [`surface::FnSig`], [`surface::FnOutput`], or
404    /// [`surface::VariantDef`]. The [`NodeId`]s in the vectors are keys in [`Self::param_res_map`].
405    pub implicit_params: UnordMap<NodeId, Vec<(Ident, NodeId)>>,
406    pub sort_path_res_map: UnordMap<NodeId, fhir::SortRes>,
407    pub expr_path_res_map: UnordMap<NodeId, fhir::ExprRes>,
408    /// The resolved list of local qualifiers per function
409    pub qualifier_res_map: UnordMap<OwnerId, Vec<def_id::FluxLocalDefId>>,
410    /// The resolved list of local reveals per function
411    pub reveal_res_map: UnordMap<OwnerId, Vec<def_id::FluxDefId>>,
412}
413
414#[extension(pub trait PlaceExt)]
415impl flux_rustc_bridge::mir::Place {
416    fn ty(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<PlaceTy> {
417        self.projection
418            .iter()
419            .try_fold(PlaceTy::from_ty(local_decls[self.local].ty.clone()), |place_ty, elem| {
420                place_ty.projection_ty(genv, *elem)
421            })
422    }
423
424    fn behind_raw_ptr(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<bool> {
425        let mut place_ty = PlaceTy::from_ty(local_decls[self.local].ty.clone());
426        for elem in &self.projection {
427            if let (PlaceElem::Deref, ty::TyKind::RawPtr(..)) = (elem, place_ty.ty.kind()) {
428                return Ok(true);
429            }
430            place_ty = place_ty.projection_ty(genv, *elem)?;
431        }
432        Ok(false)
433    }
434}
435
436#[derive(Debug)]
437pub struct PlaceTy {
438    pub ty: ty::Ty,
439    /// Downcast to a particular variant of an enum or a generator, if included.
440    pub variant_index: Option<VariantIdx>,
441}
442
443impl PlaceTy {
444    fn from_ty(ty: ty::Ty) -> PlaceTy {
445        PlaceTy { ty, variant_index: None }
446    }
447
448    fn projection_ty(&self, genv: GlobalEnv, elem: PlaceElem) -> QueryResult<PlaceTy> {
449        if self.variant_index.is_some() && !matches!(elem, PlaceElem::Field(..)) {
450            Err(query_bug!("cannot use non field projection on downcasted place"))?;
451        }
452        let place_ty = match elem {
453            PlaceElem::Deref => PlaceTy::from_ty(self.ty.deref()),
454            PlaceElem::Field(fld) => PlaceTy::from_ty(self.field_ty(genv, fld)?),
455            PlaceElem::Downcast(_, variant_idx) => {
456                PlaceTy { ty: self.ty.clone(), variant_index: Some(variant_idx) }
457            }
458            PlaceElem::Index(_) | PlaceElem::ConstantIndex { .. } => {
459                if let ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) = self.ty.kind() {
460                    PlaceTy::from_ty(ty.clone())
461                } else {
462                    return Err(query_bug!("cannot use non field projection on downcasted place"));
463                }
464            }
465        };
466        Ok(place_ty)
467    }
468
469    fn field_ty(&self, genv: GlobalEnv, f: FieldIdx) -> QueryResult<ty::Ty> {
470        match self.ty.kind() {
471            ty::TyKind::Adt(adt_def, args) => {
472                let variant_def = match self.variant_index {
473                    None => adt_def.non_enum_variant(),
474                    Some(variant_index) => {
475                        assert!(adt_def.is_enum());
476                        adt_def.variant(variant_index)
477                    }
478                };
479                let field_def = &variant_def.fields[f];
480                let ty = genv.lower_type_of(field_def.did)?;
481                Ok(ty.subst(args))
482            }
483            ty::TyKind::Tuple(tys) => Ok(tys[f.index()].clone()),
484            ty::TyKind::Closure(_, args) => Ok(args.as_closure().upvar_tys()[f.index()].clone()),
485            _ => Err(query_bug!("extracting field of non-tuple non-adt non-closure: {self:?}")),
486        }
487    }
488}
489
490/// The different reasons we issue fixpoint queries. This is used to dissambiguate queries that
491/// are issued for the same item.
492///
493/// NOTE: This is defined here because it's also used in [`timings`]
494#[derive(Debug, Hash, Clone, Copy)]
495pub enum FixpointQueryKind {
496    /// Query issued when checking an impl method is a subtype of the trait
497    Impl,
498    /// Query issued to check the body of a function
499    Body,
500    /// Query issued to check an (enum) invariant is implied by the type definition
501    Invariant,
502}
503
504impl FixpointQueryKind {
505    pub fn ext(self) -> &'static str {
506        match self {
507            FixpointQueryKind::Impl => "sub.fluxc",
508            FixpointQueryKind::Body => "fluxc",
509            FixpointQueryKind::Invariant => "fluxc",
510        }
511    }
512
513    /// A string that uniquely identifies a query given an item `DefId`
514    pub fn task_key(self, tcx: TyCtxt, def_id: DefId) -> String {
515        format!("{}###{:?}", tcx.def_path_str(def_id), self)
516    }
517}
flux_middle/lib.rs

flux_middle/
lib.rs
