flux_refineck/

lib.rs

//! Refinement type checking

#![feature(
    associated_type_defaults,
    box_patterns,
    if_let_guard,
    min_specialization,
    never_type,
    rustc_private,
    unwrap_infallible
)]

extern crate rustc_abi;
extern crate rustc_data_structures;
extern crate rustc_errors;
extern crate rustc_hir;
extern crate rustc_index;
extern crate rustc_infer;
extern crate rustc_middle;
extern crate rustc_mir_dataflow;
extern crate rustc_span;
extern crate rustc_type_ir;

mod checker;
pub mod compare_impl_item;
mod ghost_statements;
pub mod invariants;
mod primops;
mod queue;
mod type_env;

use checker::{Checker, trait_impl_subtyping};
use flux_common::{dbg, dbg::SpanTrace, result::ResultExt as _};
use flux_config as config;
use flux_infer::{
    fixpoint_encoding::{FixQueryCache, SolutionTrace},
    infer::{ConstrReason, SubtypeReason, Tag},
};
use flux_macros::fluent_messages;
use flux_middle::{
    FixpointQueryKind,
    def_id::MaybeExternId,
    global_env::GlobalEnv,
    metrics::{self, Metric, TimingKind},
    rty::{self, ESpan},
};
use rustc_data_structures::unord::UnordMap;
use rustc_errors::ErrorGuaranteed;
use rustc_hir::def_id::LocalDefId;
use rustc_span::Span;

use crate::{checker::errors::ResultExt as _, ghost_statements::compute_ghost_statements};

fluent_messages! { "../locales/en-US.ftl" }

fn report_fixpoint_errors(
    genv: GlobalEnv,
    local_id: LocalDefId,
    errors: Vec<Tag>,
) -> Result<(), ErrorGuaranteed> {
    #[expect(clippy::collapsible_else_if, reason = "it looks better")]
    if genv.should_fail(local_id) {
        if errors.is_empty() { report_expected_neg(genv, local_id) } else { Ok(()) }
    } else {
        if errors.is_empty() { Ok(()) } else { report_errors(genv, errors) }
    }
}

fn check_body(
    genv: GlobalEnv,
    cache: &mut FixQueryCache,
    def_id: LocalDefId,
    poly_sig: &rty::PolyFnSig,
) -> Result<(), ErrorGuaranteed> {
    let span = genv.tcx().def_span(def_id);
    let opts = genv.infer_opts(def_id);

    let ghost_stmts = compute_ghost_statements(genv, def_id)
        .with_span(span)
        .map_err(|err| err.emit(genv, def_id))?;
    let mut closures = UnordMap::default();

    // PHASE 1: infer shape of `TypeEnv` at the entry of join points
    let shape_result =
        Checker::run_in_shape_mode(genv, def_id, &ghost_stmts, &mut closures, opts, poly_sig)
            .map_err(|err| err.emit(genv, def_id))?;

    // PHASE 2: generate refinement tree constraint
    let infcx_root = Checker::run_in_refine_mode(
        genv,
        def_id,
        &ghost_stmts,
        &mut closures,
        shape_result,
        opts,
        poly_sig,
    )
    .map_err(|err| err.emit(genv, def_id))?;

    // PHASE 3: invoke fixpoint on the constraint
    if (genv.proven_externally(def_id).is_some() && flux_config::lean().is_check())
        || flux_config::lean().is_emit()
    {
        infcx_root
            .execute_lean_query(cache, MaybeExternId::Local(def_id))
            .emit(&genv)
    } else {
        let answer = infcx_root
            .execute_fixpoint_query(cache, MaybeExternId::Local(def_id), FixpointQueryKind::Body)
            .emit(&genv)?;

        let tcx = genv.tcx();
        let hir_id = tcx.local_def_id_to_hir_id(def_id);
        let body_span = tcx.hir_span_with_body(hir_id);
        dbg::solution!(genv, &answer, body_span);

        let errors = answer.errors;
        report_fixpoint_errors(genv, def_id, errors)
    }
}

pub fn check_static(
    genv: GlobalEnv,
    cache: &mut FixQueryCache,
    def_id: LocalDefId,
    ty: rty::Ty,
) -> Result<(), ErrorGuaranteed> {
    // Build a PolyFnSig with no inputs and `ty` as the output
    let output = rty::Binder::dummy(rty::FnOutput::new(ty, vec![]));
    let fn_sig = rty::FnSig::new(
        rustc_hir::Safety::Safe,
        rustc_abi::ExternAbi::Rust,
        rty::List::empty(),
        rty::List::empty(),
        output,
        rty::Expr::ff(),
        false,
    );
    let poly_sig = rty::PolyFnSig::dummy(fn_sig);

    metrics::incr_metric(Metric::FnChecked, 1);
    metrics::time_it(TimingKind::CheckBody(def_id), || check_body(genv, cache, def_id, &poly_sig))
}

pub fn check_fn(
    genv: GlobalEnv,
    cache: &mut FixQueryCache,
    def_id: LocalDefId,
) -> Result<(), ErrorGuaranteed> {
    let span = genv.tcx().def_span(def_id);

    // HACK(nilehmann) this will ignore any code generated by a macro. This is a temporary
    // workaround to deal with a `#[derive(..)]` that generates code that flux cannot handle.
    // Note that this is required because code generated by a `#[derive(..)]` cannot be
    // manually trusted or ignored.
    if !genv.tcx().def_span(def_id).ctxt().is_root() {
        metrics::incr_metric(Metric::FnTrusted, 1);
        return Ok(());
    }

    let opts = genv.infer_opts(def_id);

    // FIXME(nilehmann) we should move this check to `compare_impl_item`
    if let Some(infcx_root) = trait_impl_subtyping(genv, def_id, opts, span)
        .with_span(span)
        .map_err(|err| err.emit(genv, def_id))?
    {
        tracing::info!("check_fn::refine-subtyping");
        let answer = infcx_root
            .execute_fixpoint_query(cache, MaybeExternId::Local(def_id), FixpointQueryKind::Impl)
            .emit(&genv)?;
        tracing::info!("check_fn::fixpoint-subtyping");
        let errors = answer.errors;
        report_fixpoint_errors(genv, def_id, errors)?;
    }

    // Skip trusted functions
    if genv.trusted(def_id) {
        metrics::incr_metric(Metric::FnTrusted, 1);
        return Ok(());
    }

    metrics::incr_metric(Metric::FnChecked, 1);
    metrics::time_it(TimingKind::CheckBody(def_id), || -> Result<(), ErrorGuaranteed> {
        let poly_sig = genv
            .fn_sig(def_id)
            .with_span(span)
            .map_err(|err| err.emit(genv, def_id))?
            .instantiate_identity();
        let poly_sig = rty::auto_strong(genv, def_id, poly_sig);

        check_body(genv, cache, def_id, &poly_sig)
    })?;

    dbg::check_fn_span!(genv.tcx(), def_id).in_scope(|| Ok(()))
}

fn call_error(genv: GlobalEnv, span: Span, dst_span: Option<ESpan>) -> ErrorGuaranteed {
    genv.sess()
        .emit_err(errors::RefineError::call(span, dst_span))
}

fn ret_error(genv: GlobalEnv, span: Span, dst_span: Option<ESpan>) -> ErrorGuaranteed {
    genv.sess()
        .emit_err(errors::RefineError::ret(span, dst_span))
}

fn report_errors(genv: GlobalEnv, errors: Vec<Tag>) -> Result<(), ErrorGuaranteed> {
    let mut e = None;
    for err in errors {
        let span = err.src_span;
        e = Some(match err.reason {
            ConstrReason::Call
            | ConstrReason::Subtype(SubtypeReason::Input)
            | ConstrReason::Subtype(SubtypeReason::Requires)
            | ConstrReason::Predicate => call_error(genv, span, err.dst_span),
            ConstrReason::Assign => genv.sess().emit_err(errors::AssignError { span }),
            ConstrReason::Ret
            | ConstrReason::Subtype(SubtypeReason::Output)
            | ConstrReason::Subtype(SubtypeReason::Ensures) => ret_error(genv, span, err.dst_span),
            ConstrReason::Div => genv.sess().emit_err(errors::DivError { span }),
            ConstrReason::Rem => genv.sess().emit_err(errors::RemError { span }),
            ConstrReason::Goto(_) => genv.sess().emit_err(errors::GotoError { span }),
            ConstrReason::Assert(msg) => genv.sess().emit_err(errors::AssertError { span, msg }),
            ConstrReason::Fold | ConstrReason::FoldLocal => {
                genv.sess().emit_err(errors::FoldError { span })
            }
            ConstrReason::Overflow => genv.sess().emit_err(errors::OverflowError { span }),
            ConstrReason::Underflow => genv.sess().emit_err(errors::UnderflowError { span }),
            ConstrReason::Other => genv.sess().emit_err(errors::UnknownError { span }),
            ConstrReason::NoPanic(callee) => {
                genv.sess().emit_err(errors::PanicError {
                    span,
                    callee: genv.tcx().def_path_debug_str(callee),
                })
            }
        });
    }

    if let Some(e) = e { Err(e) } else { Ok(()) }
}

fn report_expected_neg(genv: GlobalEnv, def_id: LocalDefId) -> Result<(), ErrorGuaranteed> {
    Err(genv.sess().emit_err(errors::ExpectedNeg {
        span: genv.tcx().def_span(def_id),
        def_descr: genv.tcx().def_descr(def_id.to_def_id()),
    }))
}

mod errors {
    use flux_errors::E0999;
    use flux_macros::{Diagnostic, Subdiagnostic};
    use flux_middle::rty::ESpan;
    use rustc_span::Span;

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

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

    #[derive(Subdiagnostic)]
    #[note(refineck_condition_span_note)]
    pub(crate) struct ConditionSpanNote {
        #[primary_span]
        pub span: Span,
    }

    #[derive(Subdiagnostic)]
    #[note(refineck_call_span_note)]
    pub(crate) struct CallSpanNote {
        #[primary_span]
        pub span: Span,
    }

    #[derive(Diagnostic)]
    #[diag(refineck_refine_error, code = E0999)]
    pub struct RefineError {
        #[primary_span]
        #[label]
        pub span: Span,
        cond: &'static str,
        #[subdiagnostic]
        span_note: Option<ConditionSpanNote>,
        #[subdiagnostic]
        call_span_note: Option<CallSpanNote>,
    }

    impl RefineError {
        pub fn call(span: Span, espan: Option<ESpan>) -> Self {
            RefineError::new("precondition", span, espan)
        }

        pub fn ret(span: Span, espan: Option<ESpan>) -> Self {
            RefineError::new("postcondition", span, espan)
        }

        fn new(cond: &'static str, span: Span, espan: Option<ESpan>) -> RefineError {
            match espan {
                Some(dst_span) => {
                    let span_note = Some(ConditionSpanNote { span: dst_span.span });
                    let call_span_note = dst_span.base.map(|span| CallSpanNote { span });
                    RefineError { span, cond, span_note, call_span_note }
                }
                None => RefineError { span, cond, span_note: None, call_span_note: None },
            }
        }
    }

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

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

    #[derive(Diagnostic)]
    #[diag(refineck_assert_error, code = E0999)]
    pub struct AssertError {
        #[primary_span]
        pub span: Span,
        pub msg: &'static str,
    }

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

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

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

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

    #[derive(Diagnostic)]
    #[diag(refineck_expected_neg, code = E0999)]
    pub struct ExpectedNeg {
        #[primary_span]
        pub span: Span,
        pub def_descr: &'static str,
    }

    #[derive(Diagnostic)]
    #[diag(refineck_panic_error, code = E0999)]
    pub(super) struct PanicError {
        #[primary_span]
        pub(super) span: Span,
        pub(super) callee: String,
    }
}