Struct Wf 

struct Wf<'a, 'genv, 'tcx> {
    infcx: &'a mut InferCtxt<'genv, 'tcx>,
    errors: Errors<'genv>,
    next_type_index: u32,
    next_region_index: u32,
    next_const_index: u32,
}

Fields

infcx: &'a mut InferCtxt<'genv, 'tcx>

errors: Errors<'genv>

next_type_index: u32

next_region_index: u32

next_const_index: u32

Implementations

impl<'a, 'genv, 'tcx> Wf<'a, 'genv, 'tcx>

fn with( infcx: &'a mut InferCtxt<'genv, 'tcx>, f: impl FnOnce(&mut Self) -> Result<(), ErrorGuaranteed>, ) -> Result<(), ErrorGuaranteed>

fn check_flux_item(&mut self, item: FluxItem<'genv>)

fn check_node(&mut self, node: &OwnerNode<'genv>)

fn check_expr(&mut self, expr: &Expr<'genv>, sort: &Sort)

fn declare_params_for_primop_prop( &mut self, primop_prop: &PrimOpProp<'genv>, ) -> Result<(), ErrorGuaranteed>

fn declare_params_for_flux_item( &mut self, item: FluxItem<'genv>, ) -> Result<(), ErrorGuaranteed>

Recursively traverse item and declare all refinement parameters

fn declare_params_for_node( &mut self, node: &OwnerNode<'genv>, ) -> Result<(), ErrorGuaranteed>

Recursively traverse node and declare all refinement parameters

fn declare_params_for_invariants( &mut self, params: &[RefineParam<'genv>], invariants: &[Expr<'genv>], ) -> Result<(), ErrorGuaranteed>

Recursively traverse invariants and declare all refinement parameters

fn declare_params_in_expr( &mut self, expr: &Expr<'genv>, ) -> Result<(), ErrorGuaranteed>

fn declare_param( &mut self, param: &RefineParam<'genv>, ) -> Result<(), ErrorGuaranteed>

fn init_infcx_for_node(&mut self, node: &OwnerNode<'genv>) -> QueryResult

To check for well-formedness we need to synthesize sorts for some nodes which is hard to compute in fhir. For example, to check if the type i32[e] is well formed, we need to know that the sort of i32 is int so we can check the expression e against it. Computing the sort from a base type is subtle and hard to do in fhir so we must do it in rty. However, to convert from fhir to rty we need elaborated information from sort checking which we do in fhir.

To break this circularity, we do conversion in two phases. In the first phase, we do conversion without elaborated information. This results in types in rty with incorrect refinements but with the right shape to compute their sorts. We use these sorts for sort checking and then do conversion again with the elaborated information.

This function initializes the inference context by running the first phase of conversion and collecting the sorts of some nodes that are hard to compute in fhir.

fn init_infcx_for_flux_item(&mut self, item: FluxItem<'genv>) -> QueryResult

fn check_output_locs(&mut self, fn_decl: &FnDecl<'_>)

Trait Implementations

impl<'genv, 'tcx> ConvPhase<'genv, 'tcx> for Wf<'_, 'genv, 'tcx>

const EXPAND_TYPE_ALIASES: bool = false

We don’t expand type aliases before sort checking because we need every base type in fhir to match a type in rty.

const HAS_ELABORATED_INFORMATION: bool = false

Whether we have elaborated information or not (in the first phase we will not, but in the second we will).

type Results = InferCtxt<'genv, 'tcx>

fn genv(&self) -> GlobalEnv<'genv, 'tcx>

fn owner(&self) -> FluxOwnerId

fn next_sort_vid(&mut self) -> SortVid

fn next_type_vid(&mut self) -> TyVid

fn next_region_vid(&mut self) -> RegionVid

fn next_const_vid(&mut self) -> ConstVid

fn results(&self) -> &Self::Results

fn insert_node_sort(&mut self, fhir_id: FhirId, sort: Sort)

Called during the first phase to collect the sort associated to a node which would be hard to recompute from fhir otherwise. Currently, this is being called when converting:

fn insert_path_args(&mut self, fhir_id: FhirId, args: GenericArgs)

Called after converting a path with the generic arguments. Using during the first phase to instantiate sort of generic refinements.

fn insert_alias_reft_sort(&mut self, fhir_id: FhirId, fsort: FuncSort)

Called after converting an fhir::ExprKind::Alias with the sort of the resulting rty::AliasReft. Used during the first phase to collect the sorts of refinement aliases.

fn into_conv_ctxt(self) -> ConvCtxt<Self>

fn as_conv_ctxt(&mut self) -> &mut ConvCtxt<Self>

impl<'genv> Visitor<'genv> for Wf<'_, 'genv, '_>

fn visit_qualifier(&mut self, qual: &Qualifier<'genv>)

fn visit_primop_prop(&mut self, primop_prop: &PrimOpProp<'genv>)

fn visit_func(&mut self, func: &SpecFunc<'genv>)

fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'genv>)

fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'genv>)

fn visit_variant_ret(&mut self, ret: &VariantRet<'genv>)

fn visit_fn_decl(&mut self, decl: &FnDecl<'genv>)

fn visit_requires(&mut self, requires: &Requires<'genv>)

fn visit_ensures(&mut self, ensures: &Ensures<'genv>)

fn visit_ty(&mut self, ty: &Ty<'genv>)

fn visit_path(&mut self, path: &Path<'genv>)

fn visit_flux_item(&mut self, item: &FluxItem<'v>)

fn visit_node(&mut self, node: &OwnerNode<'v>)

fn visit_item(&mut self, item: &Item<'v>)

fn visit_trait_item(&mut self, trait_item: &TraitItem<'v>)

fn visit_impl_item(&mut self, impl_item: &ImplItem<'v>)

fn visit_foreign_item(&mut self, foreign_item: &ForeignItem<'v>)

fn visit_generics(&mut self, generics: &Generics<'v>)

fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'v>)

fn visit_impl(&mut self, impl_: &Impl<'v>)

fn visit_struct_def(&mut self, struct_def: &StructDef<'v>)

fn visit_enum_def(&mut self, enum_def: &EnumDef<'v>)

fn visit_variant(&mut self, variant: &VariantDef<'v>)

fn visit_field_def(&mut self, field: &FieldDef<'v>)

fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'v>)

fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'v>)

fn visit_generic_bound(&mut self, bound: &GenericBound<'v>)

fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'v>)

fn visit_fn_sig(&mut self, sig: &FnSig<'v>)

fn visit_refine_param(&mut self, param: &RefineParam<'v>)

fn visit_fn_output(&mut self, output: &FnOutput<'v>)

fn visit_generic_arg(&mut self, arg: &GenericArg<'v>)

fn visit_lifetime(&mut self, _lft: &Lifetime)

fn visit_bty(&mut self, bty: &BaseTy<'v>)

fn visit_qpath(&mut self, qpath: &QPath<'v>)

fn visit_path_segment(&mut self, segment: &PathSegment<'v>)

fn visit_assoc_item_constraint(&mut self, constraint: &AssocItemConstraint<'v>)

fn visit_sort(&mut self, sort: &Sort<'v>)

fn visit_sort_path(&mut self, path: &SortPath<'v>)

fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'v>)

fn visit_func_sort(&mut self, func: &FuncSort<'v>)

fn visit_expr(&mut self, expr: &Expr<'v>)

fn visit_field_expr(&mut self, expr: &FieldExpr<'v>)

fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'v>)

fn visit_literal(&mut self, _lit: &Lit)

fn visit_path_expr(&mut self, _path: &PathExpr<'v>)