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

flux_middle/
lib.rs
