flux_refineck/
invariants.rs

1use flux_common::{iter::IterExt, result::ResultExt};
2use flux_config::InferOpts;
3use flux_errors::ErrorGuaranteed;
4use flux_infer::{
5    fixpoint_encoding::FixQueryCache,
6    infer::{ConstrReason, GlobalEnvExt, Tag},
7};
8use flux_middle::{
9    FixpointQueryKind, def_id::MaybeExternId, fhir, global_env::GlobalEnv, queries::try_query, rty,
10};
11use rustc_infer::infer::TyCtxtInferExt;
12use rustc_middle::ty::TypingMode;
13use rustc_span::{DUMMY_SP, Span};
14
15pub fn check_invariants(
16    genv: GlobalEnv,
17    cache: &mut FixQueryCache,
18    def_id: MaybeExternId,
19    invariants: &[fhir::Expr],
20    adt_def: &rty::AdtDef,
21) -> Result<(), ErrorGuaranteed> {
22    // FIXME(nilehmann) maybe we should record whether the invariants were generated with overflow
23    // checking enabled and only assume them in code that also overflow checking enabled.
24    // Although, enable overflow checking locally is unsound in general.
25    //
26    // The good way would be to make overflow checking a property of a type that can be turned on
27    // and off locally. Then we consider an overflow-checked `T` distinct from a non-checked one and
28    // error/warn in case of a mismatch: overflow-checked types can flow to non-checked code but not
29    // the other way around.
30    let opts = genv.infer_opts(def_id.local_id());
31    adt_def
32        .invariants()
33        .iter_identity()
34        .enumerate()
35        .try_for_each_exhaust(|(idx, invariant)| {
36            let span = invariants[idx].span;
37            check_invariant(genv, cache, def_id, adt_def, span, invariant, opts)
38        })
39}
40
41fn check_invariant(
42    genv: GlobalEnv,
43    cache: &mut FixQueryCache,
44    def_id: MaybeExternId,
45    adt_def: &rty::AdtDef,
46    span: Span,
47    invariant: &rty::Invariant,
48    opts: InferOpts,
49) -> Result<(), ErrorGuaranteed> {
50    let resolved_id = def_id.resolved_id();
51
52    let region_infercx = genv
53        .tcx()
54        .infer_ctxt()
55        .with_next_trait_solver(true)
56        .build(TypingMode::non_body_analysis());
57
58    let mut infcx_root = try_query(|| {
59        genv.infcx_root(&region_infercx, opts)
60            .identity_for_item(resolved_id)?
61            .build()
62    })
63    .emit(&genv)?;
64
65    for variant_idx in adt_def.variants().indices() {
66        let mut rcx = infcx_root.infcx(resolved_id, &region_infercx);
67
68        let variant_sig = genv
69            .variant_sig(adt_def.did(), variant_idx)
70            .emit(&genv)?
71            .expect("cannot check opaque structs")
72            .instantiate_identity()
73            .replace_bound_refts_with(|sort, _, _| rty::Expr::fvar(rcx.define_var(sort)));
74
75        for ty in variant_sig.fields() {
76            let ty = rcx.unpack(ty);
77            rcx.assume_invariants(&ty);
78        }
79        let pred = invariant.apply(&variant_sig.idx);
80        rcx.check_pred(&pred, Tag::new(ConstrReason::Other, DUMMY_SP));
81    }
82    let errors = infcx_root
83        .execute_fixpoint_query(cache, def_id, FixpointQueryKind::Invariant)
84        .emit(&genv)?;
85
86    if errors.is_empty() { Ok(()) } else { Err(genv.sess().emit_err(errors::Invalid { span })) }
87}
88
89mod errors {
90    use flux_errors::E0999;
91    use flux_macros::Diagnostic;
92    use rustc_span::Span;
93
94    #[derive(Diagnostic)]
95    #[diag(refineck_invalid_invariant, code = E0999)]
96    pub struct Invalid {
97        #[primary_span]
98        pub span: Span,
99    }
100}
flux_refineck/invariants.rs

flux_refineck/
invariants.rs
