flux_refineck/
invariants.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
use flux_common::{cache::QueryCache, dbg, iter::IterExt, result::ResultExt};
use flux_config as config;
use flux_errors::ErrorGuaranteed;
use flux_infer::{
    fixpoint_encoding::{FixpointCtxt, KVarGen},
    infer::{ConstrReason, Tag},
    refine_tree::RefineTree,
};
use flux_middle::{fhir, global_env::GlobalEnv, rty, MaybeExternId};
use rustc_span::{Span, DUMMY_SP};

use crate::CheckerConfig;

pub fn check_invariants(
    genv: GlobalEnv,
    cache: &mut QueryCache,
    def_id: MaybeExternId,
    invariants: &[fhir::Expr],
    adt_def: &rty::AdtDef,
    checker_config: CheckerConfig,
) -> Result<(), ErrorGuaranteed> {
    adt_def
        .invariants()
        .iter()
        .enumerate()
        .try_for_each_exhaust(|(idx, invariant)| {
            let span = invariants[idx].span;
            check_invariant(genv, cache, def_id, adt_def, span, invariant, checker_config)
        })
}

fn check_invariant(
    genv: GlobalEnv,
    cache: &mut QueryCache,
    def_id: MaybeExternId,
    adt_def: &rty::AdtDef,
    span: Span,
    invariant: &rty::Invariant,
    checker_config: CheckerConfig,
) -> Result<(), ErrorGuaranteed> {
    let mut refine_tree = RefineTree::new(genv, def_id.local_id().into(), None).emit(&genv)?;

    for variant_idx in adt_def.variants().indices() {
        let mut rcx = refine_tree.refine_ctxt_at_root();

        let variant = genv
            .variant_sig(adt_def.did(), variant_idx)
            .emit(&genv)?
            .expect("cannot check opaque structs")
            .instantiate_identity()
            .replace_bound_refts_with(|sort, _, _| rcx.define_vars(sort));

        for ty in variant.fields() {
            let ty = rcx.unpack(ty);
            rcx.assume_invariants(&ty, checker_config.check_overflow);
        }
        let pred = invariant.apply(&variant.idx);
        rcx.check_pred(&pred, Tag::new(ConstrReason::Other, DUMMY_SP));
    }
    let mut fcx = FixpointCtxt::new(genv, def_id.local_id(), KVarGen::dummy());
    if config::dump_constraint() {
        dbg::dump_item_info(genv.tcx(), def_id.local_id(), "fluxc", &refine_tree).unwrap();
    }

    let cstr = refine_tree.into_fixpoint(&mut fcx).emit(&genv)?;
    let errors = fcx
        .check(cache, cstr, checker_config.scrape_quals)
        .emit(&genv)?;
    if errors.is_empty() {
        Ok(())
    } else {
        Err(genv.sess().emit_err(errors::Invalid { span }))
    }
}

mod errors {
    use flux_errors::E0999;
    use flux_macros::Diagnostic;
    use rustc_span::Span;

    #[derive(Diagnostic)]
    #[diag(refineck_invalid_invariant, code = E0999)]
    pub struct Invalid {
        #[primary_span]
        pub span: Span,
    }
}