translator.rs

// © 2023, The RefinedRust Developers and Contributors
//
// This Source Code Form is subject to the terms of the BSD-3-clause License.
// If a copy of the BSD-3-clause license was not distributed with this
// file, You can obtain one at https://opensource.org/license/bsd-3-clause/.

use std::collections::{btree_map, BTreeMap, HashMap, HashSet};

use log::{info, trace, warn};
use radium::coq;
use rr_rustc_interface::hir::def_id::DefId;
use rr_rustc_interface::middle::mir::interpret::{ConstValue, ErrorHandled, Scalar};
use rr_rustc_interface::middle::mir::tcx::PlaceTy;
use rr_rustc_interface::middle::mir::{
    BasicBlock, BasicBlockData, BinOp, Body, BorrowKind, Constant, ConstantKind, Local, LocalKind, Location,
    Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue, StatementKind, Terminator,
    TerminatorKind, UnOp, VarDebugInfoContents,
};
use rr_rustc_interface::middle::ty::fold::TypeFolder;
use rr_rustc_interface::middle::ty::{ConstKind, Ty, TyKind};
use rr_rustc_interface::middle::{mir, ty};
use rr_rustc_interface::{abi, ast, middle};
use typed_arena::Arena;

use crate::arg_folder::*;
use crate::base::*;
use crate::checked_op_analysis::CheckedOpLocalAnalysis;
use crate::environment::borrowck::facts;
use crate::environment::polonius_info::PoloniusInfo;
use crate::environment::procedure::Procedure;
use crate::environment::{dump_borrowck_info, polonius_info, Environment};
use crate::inclusion_tracker::*;
use crate::spec_parsers::parse_utils::ParamLookup;
use crate::spec_parsers::verbose_function_spec_parser::{
    ClosureMetaInfo, FunctionRequirements, FunctionSpecParser, VerboseFunctionSpecParser,
};
use crate::traits::{registry, resolution};
use crate::{base, consts, procedures, regions, search, traits, types};

/// Get the syntypes of function arguments for a procedure call.
pub fn get_arg_syntypes_for_procedure_call<'tcx, 'def>(
    tcx: ty::TyCtxt<'tcx>,
    ty_translator: &types::LocalTX<'def, 'tcx>,
    callee_did: DefId,
    ty_params: &[ty::GenericArg<'tcx>],
) -> Result<Vec<radium::SynType>, TranslationError<'tcx>> {
    let caller_did = ty_translator.get_proc_did();

    // Get the type of the callee, fully instantiated
    let full_ty: ty::EarlyBinder<Ty<'tcx>> = tcx.type_of(callee_did);
    let full_ty = full_ty.instantiate(tcx, ty_params);

    // We create a dummy scope in order to make the lifetime lookups succeed, since we only want
    // syntactic types here.
    // Since we do the substitution of the generics above, we should translate generics and
    // traits in the caller's scope.
    let scope = ty_translator.scope.borrow();
    let param_env: ty::ParamEnv<'tcx> = tcx.param_env(scope.did);
    let callee_state = types::CalleeState::new(&param_env, &scope.generic_scope);
    let mut dummy_state = types::STInner::CalleeTranslation(callee_state);

    let mut syntypes = Vec::new();
    match full_ty.kind() {
        ty::TyKind::FnDef(_, _) => {
            let sig = full_ty.fn_sig(tcx);
            for ty in sig.inputs().skip_binder() {
                let st = ty_translator.translator.translate_type_to_syn_type(*ty, &mut dummy_state)?;
                syntypes.push(st);
            }
        },
        ty::TyKind::Closure(_, args) => {
            let clos_args = args.as_closure();
            let sig = clos_args.sig();
            let pre_sig = sig.skip_binder();
            // we also need to add the closure argument here

            let tuple_ty = clos_args.tupled_upvars_ty();
            match clos_args.kind() {
                ty::ClosureKind::Fn | ty::ClosureKind::FnMut => {
                    syntypes.push(radium::SynType::Ptr);
                },
                ty::ClosureKind::FnOnce => {
                    let st =
                        ty_translator.translator.translate_type_to_syn_type(tuple_ty, &mut dummy_state)?;
                    syntypes.push(st);
                },
            }
            for ty in pre_sig.inputs() {
                let st = ty_translator.translator.translate_type_to_syn_type(*ty, &mut dummy_state)?;
                syntypes.push(st);
            }
        },
        _ => unimplemented!(),
    }

    Ok(syntypes)
}

// solve the constraints for the new_regions
// we first identify what kinds of constraints these new regions are subject to
#[derive(Debug)]
enum CallRegionKind {
    // this is just an intersection of local regions.
    Intersection(HashSet<Region>),
    // this is equal to a specific region
    EqR(Region),
}

struct CallRegions {
    pub early_regions: Vec<Region>,
    pub late_regions: Vec<Region>,
    pub classification: HashMap<Region, CallRegionKind>,
}

/// Struct that keeps track of all information necessary to translate a MIR Body to a `radium::Function`.
/// `'a` is the lifetime of the translator and ends after translation has finished.
/// `'def` is the lifetime of the generated code (the code may refer to struct defs).
/// `'tcx` is the lifetime of the rustc tctx.
pub struct TX<'a, 'def, 'tcx> {
    env: &'def Environment<'tcx>,
    /// registry of other procedures
    procedure_registry: &'a procedures::Scope<'def>,
    /// scope of used consts
    const_registry: &'a consts::Scope<'def>,
    /// trait registry
    trait_registry: &'def registry::TR<'tcx, 'def>,
    /// translator for types
    ty_translator: types::LocalTX<'def, 'tcx>,

    /// this needs to be annotated with the right borrowck things
    proc: &'def Procedure<'tcx>,
    /// attributes on this function
    attrs: &'a [&'a ast::ast::AttrItem],
    /// polonius info for this function
    info: &'a PoloniusInfo<'a, 'tcx>,

    /// maps locals to variable names
    variable_map: HashMap<Local, String>,

    /// name of the return variable
    return_name: String,
    /// syntactic type of the thing to return
    return_synty: radium::SynType,
    /// all the other procedures used by this function, and:
    /// (code_loc_parameter_name, spec_name, type_inst, syntype_of_all_args)
    collected_procedures: HashMap<(DefId, types::GenericsKey<'tcx>), radium::UsedProcedure<'def>>,
    /// used statics
    collected_statics: HashSet<DefId>,

    /// tracking lifetime inclusions for the generation of lifetime inclusions
    inclusion_tracker: InclusionTracker<'a, 'tcx>,
    /// initial Polonius constraints that hold at the start of the function
    initial_constraints: Vec<(polonius_info::AtomicRegion, polonius_info::AtomicRegion)>,

    /// local lifetimes: the LHS is the lifetime name, the RHS are the super lifetimes
    local_lifetimes: Vec<(radium::specs::Lft, Vec<radium::specs::Lft>)>,
    /// data structures for tracking which basic blocks still need to be translated
    /// (we only translate the basic blocks which are actually reachable, in particular when
    /// skipping unwinding)
    bb_queue: Vec<BasicBlock>,
    /// set of already processed blocks
    processed_bbs: HashSet<BasicBlock>,

    /// map of loop heads to their optional spec closure defid
    loop_specs: HashMap<BasicBlock, Option<DefId>>,

    /// relevant locals: (local, name, type)
    fn_locals: Vec<(Local, String, radium::Type<'def>)>,

    /// result temporaries of checked ops that we rewrite
    /// we assume that this place is typed at (result_type, bool)
    /// and rewrite accesses to the first component to directly use the place,
    /// while rewriting accesses to the second component to true.
    /// TODO: once we handle panics properly, we should use a different translation.
    /// NOTE: we only rewrite for uses, as these are the only places these are used.
    checked_op_temporaries: HashMap<Local, Ty<'tcx>>,

    /// the Caesium function buildder
    translated_fn: radium::FunctionBuilder<'def>,
}

impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
    pub fn new(
        env: &'def Environment<'tcx>,
        procedure_registry: &'a procedures::Scope<'def>,
        const_registry: &'a consts::Scope<'def>,
        trait_registry: &'def registry::TR<'tcx, 'def>,
        ty_translator: types::LocalTX<'def, 'tcx>,

        proc: &'def Procedure<'tcx>,
        attrs: &'a [&'a ast::ast::AttrItem],
        info: &'a PoloniusInfo<'a, 'tcx>,
        inputs: &[ty::Ty<'tcx>],

        mut inclusion_tracker: InclusionTracker<'a, 'tcx>,
        mut translated_fn: radium::FunctionBuilder<'def>,
    ) -> Result<Self, TranslationError<'tcx>> {
        let body = proc.get_mir();

        // analyze which locals are used for the result of checked-ops, because we will
        // override their types (eliminating the tuples)
        let mut checked_op_analyzer = CheckedOpLocalAnalysis::new(env.tcx(), body);
        checked_op_analyzer.analyze();
        let checked_op_temporaries = checked_op_analyzer.results();

        // map to translate between locals and the string names we use in radium::
        let mut variable_map: HashMap<Local, String> = HashMap::new();

        let local_decls = &body.local_decls;
        info!("Have {} local decls\n", local_decls.len());

        let debug_info = &body.var_debug_info;
        info!("using debug info: {:?}", debug_info);

        let mut return_synty = radium::SynType::Unit; // default
        let mut fn_locals = Vec::new();
        let mut opt_return_name =
            Err(TranslationError::UnknownError("could not find local for return value".to_owned()));
        let mut used_names = HashSet::new();
        let mut arg_tys = Vec::new();

        // go over local_decls and create the right radium:: stack layout
        for (local, local_decl) in local_decls.iter_enumerated() {
            let kind = body.local_kind(local);
            let ty: Ty<'tcx>;
            if let Some(rewritten_ty) = checked_op_temporaries.get(&local) {
                ty = *rewritten_ty;
            } else {
                ty = local_decl.ty;
            }

            // check if the type is of a spec fn -- in this case, we can skip this temporary
            if let TyKind::Closure(id, _) = ty.kind() {
                if procedure_registry.lookup_function_mode(*id).map_or(false, procedures::Mode::is_ignore) {
                    // this is a spec fn
                    info!("skipping local which has specfn closure type: {:?}", local);
                    continue;
                }
            }

            // type:
            info!("Trying to translate type of local {local:?}: {:?}", ty);
            let tr_ty = ty_translator.translate_type(ty)?;
            let st = (&tr_ty).into();

            let name = Self::make_local_name(body, local, &mut used_names);
            variable_map.insert(local, name.clone());

            fn_locals.push((local, name.clone(), tr_ty));

            match kind {
                LocalKind::Arg => {
                    translated_fn.code.add_argument(&name, st);
                    arg_tys.push(ty);
                },
                //LocalKind::Var => translated_fn.code.add_local(&name, st),
                LocalKind::Temp => translated_fn.code.add_local(&name, st),
                LocalKind::ReturnPointer => {
                    return_synty = st.clone();
                    translated_fn.code.add_local(&name, st);
                    opt_return_name = Ok(name);
                },
            }
        }
        info!("radium name map: {:?}", variable_map);
        // create the function
        let return_name = opt_return_name?;

        // add lifetime parameters to the map
        let initial_constraints = Self::get_initial_universal_arg_constraints(
            info,
            &mut inclusion_tracker,
            inputs,
            arg_tys.as_slice(),
        );
        info!("initial constraints: {:?}", initial_constraints);

        Ok(Self {
            env,
            proc,
            info,
            variable_map,
            translated_fn,
            return_name,
            return_synty,
            inclusion_tracker,
            collected_procedures: HashMap::new(),
            procedure_registry,
            attrs,
            local_lifetimes: Vec::new(),
            bb_queue: Vec::new(),
            processed_bbs: HashSet::new(),
            ty_translator,
            loop_specs: HashMap::new(),
            fn_locals,
            checked_op_temporaries,
            initial_constraints,
            const_registry,
            trait_registry,
            collected_statics: HashSet::new(),
        })
    }

    /// Determine initial constraints between universal regions and local place regions.
    /// Returns an initial mapping for the name _map that initializes place regions of arguments
    /// with universals.
    fn get_initial_universal_arg_constraints(
        info: &'a PoloniusInfo<'a, 'tcx>,
        inclusion_tracker: &mut InclusionTracker<'a, 'tcx>,
        _sig_args: &[Ty<'tcx>],
        _local_args: &[Ty<'tcx>],
    ) -> Vec<(polonius_info::AtomicRegion, polonius_info::AtomicRegion)> {
        // Polonius generates a base subset constraint uregion ⊑ pregion.
        // We turn that into pregion = uregion, as we do strong updates at the top-level.
        let input_facts = &info.borrowck_in_facts;
        let subset_base = &input_facts.subset_base;

        let root_location = Location {
            block: BasicBlock::from_u32(0),
            statement_index: 0,
        };
        let root_point = info.interner.get_point_index(&facts::Point {
            location: root_location,
            typ: facts::PointType::Start,
        });

        // TODO: for nested references, this doesn't really seem to work.
        // Problem is that we don't have constraints for the mapping of nested references.
        // Potentially, we should instead just equalize the types

        let mut initial_arg_mapping = Vec::new();
        for (r1, r2, _) in subset_base {
            let lft1 = info.mk_atomic_region(*r1);
            let lft2 = info.mk_atomic_region(*r2);

            let polonius_info::AtomicRegion::Universal(polonius_info::UniversalRegionKind::Local, _) = lft1
            else {
                continue;
            };

            // this is a constraint we care about here, add it
            if inclusion_tracker.check_inclusion(*r1, *r2, root_point) {
                continue;
            }

            inclusion_tracker.add_static_inclusion(*r1, *r2, root_point);
            inclusion_tracker.add_static_inclusion(*r2, *r1, root_point);

            assert!(matches!(lft2, polonius_info::AtomicRegion::PlaceRegion(_)));

            initial_arg_mapping.push((lft1, lft2));
        }
        initial_arg_mapping
    }

    fn get_initial_universal_arg_constraints2(
        sig_args: &[Ty<'tcx>],
        local_args: &[Ty<'tcx>],
    ) -> Vec<(polonius_info::AtomicRegion, polonius_info::AtomicRegion)> {
        // Polonius generates a base subset constraint uregion ⊑ pregion.
        // We turn that into pregion = uregion, as we do strong updates at the top-level.
        assert!(sig_args.len() == local_args.len());

        // TODO: implement a bitypefolder to solve this issue.
        Vec::new()
    }

    /// Generate a string identifier for a Local.
    /// Tries to find the Rust source code name of the local, otherwise simply enumerates.
    /// `used_names` keeps track of the Rust source code names that have already been used.
    fn make_local_name(mir_body: &Body<'tcx>, local: Local, used_names: &mut HashSet<String>) -> String {
        if let Some(mir_name) = Self::find_name_for_local(mir_body, local, used_names) {
            let name = base::strip_coq_ident(&mir_name);
            used_names.insert(mir_name);
            name
        } else {
            let mut name = "__".to_owned();
            name.push_str(&local.index().to_string());
            name
        }
    }

    /// Find a source name for a local of a MIR body, if possible.
    fn find_name_for_local(
        body: &mir::Body<'tcx>,
        local: mir::Local,
        used_names: &HashSet<String>,
    ) -> Option<String> {
        let debug_info = &body.var_debug_info;

        for dbg in debug_info {
            let name = &dbg.name;
            let val = &dbg.value;
            if let VarDebugInfoContents::Place(l) = *val {
                // make sure that the place projection is empty -- otherwise this might just
                // refer to the capture of a closure
                if let Some(this_local) = l.as_local() {
                    if this_local == local {
                        // around closures, multiple symbols may be mapped to the same name.
                        // To prevent this from happening, we check that the name hasn't been
                        // used already
                        // TODO: find better solution
                        if !used_names.contains(name.as_str()) {
                            return Some(name.as_str().to_owned());
                        }
                    }
                }
            } else {
                // is this case used when constant propagation happens during MIR construction?
            }
        }

        None
    }

    /// Main translation function that actually does the translation and returns a `radium::Function`
    /// if successful.
    pub fn translate(
        mut self,
        spec_arena: &'def Arena<radium::FunctionSpec<'def, radium::InnerFunctionSpec<'def>>>,
    ) -> Result<radium::Function<'def>, TranslationError<'tcx>> {
        // add loop info
        let loop_info = self.proc.loop_info();
        loop_info.dump_body_head();

        // translate the function's basic blocks
        let basic_blocks = &self.proc.get_mir().basic_blocks;

        // first translate the initial basic block; we add some additional annotations to the front
        let initial_bb_idx = BasicBlock::from_u32(0);
        if let Some(bb) = basic_blocks.get(initial_bb_idx) {
            let mut translated_bb = self.translate_basic_block(initial_bb_idx, bb)?;
            // push annotation for initial constraints that relate argument's place regions to universals
            for (r1, r2) in &self.initial_constraints {
                translated_bb = radium::Stmt::Annot {
                    a: radium::Annotation::CopyLftName(
                        self.ty_translator.format_atomic_region(r1),
                        self.ty_translator.format_atomic_region(r2),
                    ),
                    s: Box::new(translated_bb),
                    why: Some("initialization".to_owned()),
                };
            }
            self.translated_fn.code.add_basic_block(initial_bb_idx.as_usize(), translated_bb);
        } else {
            info!("No basic blocks");
        }

        while let Some(bb_idx) = self.bb_queue.pop() {
            let bb = &basic_blocks[bb_idx];
            let translated_bb = self.translate_basic_block(bb_idx, bb)?;
            self.translated_fn.code.add_basic_block(bb_idx.as_usize(), translated_bb);
        }

        // assume that all generics are layoutable
        {
            let scope = self.ty_translator.scope.borrow();
            for ty in scope.generic_scope.tyvars() {
                self.translated_fn.assume_synty_layoutable(radium::SynType::Literal(ty.syn_type));
            }
        }
        // assume that all used literals are layoutable
        for g in self.ty_translator.scope.borrow().shim_uses.values() {
            self.translated_fn.assume_synty_layoutable(g.generate_syn_type_term());
        }
        // assume that all used tuples are layoutable
        for g in self.ty_translator.scope.borrow().tuple_uses.values() {
            self.translated_fn.assume_synty_layoutable(g.generate_syn_type_term());
        }

        // TODO: process self.loop_specs
        // - collect the relevant bb -> def_id mappings for this function (so we can eventually generate the
        //   definition)
        // - have a function that takes the def_id and then parses the attributes into a loop invariant
        for (head, did) in &self.loop_specs {
            let spec = self.parse_attributes_on_loop_spec_closure(*head, *did);
            self.translated_fn.register_loop_invariant(head.as_usize(), spec);
        }

        // generate dependencies on other procedures.
        for used_proc in self.collected_procedures.values() {
            self.translated_fn.require_function(used_proc.clone());
        }

        // generate dependencies on statics
        for did in &self.collected_statics {
            let s = self.const_registry.get_static(*did)?;
            self.translated_fn.require_static(s.to_owned());
        }

        Ok(self.translated_fn.into_function(spec_arena))
    }
}

impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
    /// Internally register that we have used a procedure with a particular instantiation of generics, and
    /// return the code parameter name.
    /// Arguments:
    /// - `callee_did`: the `DefId` of the callee
    /// - `ty_params`: the instantiation for the callee's type parameters
    /// - `trait_spec_terms`: if the callee has any trait assumptions, these are specification parameter terms
    ///   for these traits
    /// - `trait_assoc_tys`: if the callee has any trait assumptions, these are the instantiations for all
    ///   associated types
    fn register_use_procedure(
        &mut self,
        callee_did: DefId,
        extra_spec_args: Vec<String>,
        ty_params: ty::GenericArgsRef<'tcx>,
        trait_specs: Vec<radium::TraitReqInst<'def, ty::Ty<'tcx>>>,
    ) -> Result<(String, Vec<radium::Type<'def>>, Vec<radium::Lft>), TranslationError<'tcx>> {
        trace!("enter register_use_procedure callee_did={callee_did:?} ty_params={ty_params:?}");
        // The key does not include the associated types, as the resolution of the associated types
        // should always be unique for one combination of type parameters, as long as we remain in
        // the same environment (which is the case within this procedure).
        // Therefore, already the type parameters are sufficient to distinguish different
        // instantiations.
        let key = types::generate_args_inst_key(self.env.tcx(), ty_params)?;

        // re-quantify
        let quantified_args = self.ty_translator.get_generic_abstraction_for_procedure(
            callee_did,
            ty_params,
            &trait_specs,
            true,
        )?;

        let tup = (callee_did, key);
        let res;
        if let Some(proc_use) = self.collected_procedures.get(&tup) {
            res = proc_use.loc_name.clone();
        } else {
            let meta = self
                .procedure_registry
                .lookup_function(callee_did)
                .ok_or_else(|| TranslationError::UnknownProcedure(format!("{:?}", callee_did)))?;
            // explicit instantiation is needed sometimes
            let spec_name = format!("{} (RRGS:=RRGS)", meta.get_spec_name());
            let code_name = meta.get_name();
            let loc_name = format!("{}_loc", types::mangle_name_with_tys(code_name, tup.1.as_slice()));

            let syntypes = get_arg_syntypes_for_procedure_call(
                self.env.tcx(),
                &self.ty_translator,
                callee_did,
                ty_params.as_slice(),
            )?;

            let mut translated_params = quantified_args.fn_ty_param_inst;

            info!(
                "Registered procedure instance {} of {:?} with {:?} and layouts {:?}",
                loc_name, callee_did, translated_params, syntypes
            );

            let specs = trait_specs.into_iter().map(|x| x.try_into().unwrap()).collect();

            let proc_use = radium::UsedProcedure::new(
                loc_name,
                spec_name,
                extra_spec_args,
                quantified_args.scope,
                specs,
                translated_params,
                quantified_args.fn_lft_param_inst,
                syntypes,
            );

            res = proc_use.loc_name.clone();
            self.collected_procedures.insert(tup, proc_use);
        }
        trace!("leave register_use_procedure");
        Ok((res, quantified_args.callee_ty_param_inst, quantified_args.callee_lft_param_inst))
    }

    /// Internally register that we have used a trait method with a particular instantiation of
    /// generics, and return the code parameter name.
    fn register_use_trait_method<'c>(
        &'c mut self,
        callee_did: DefId,
        ty_params: ty::GenericArgsRef<'tcx>,
        trait_specs: Vec<radium::TraitReqInst<'def, ty::Ty<'tcx>>>,
    ) -> Result<(String, Vec<radium::Type<'def>>, Vec<radium::Lft>), TranslationError<'tcx>> {
        trace!("enter register_use_trait_method did={:?} ty_params={:?}", callee_did, ty_params);
        // Does not include the associated types in the key; see `register_use_procedure` for an
        // explanation.
        let key = types::generate_args_inst_key(self.env.tcx(), ty_params)?;

        let (method_loc_name, method_spec_term, method_params) =
            self.ty_translator.register_use_trait_procedure(self.env, callee_did, ty_params)?;
        // re-quantify
        let quantified_args = self.ty_translator.get_generic_abstraction_for_procedure(
            callee_did,
            method_params,
            &trait_specs,
            false,
        )?;

        let tup = (callee_did, key);
        let res;
        if let Some(proc_use) = self.collected_procedures.get(&tup) {
            res = proc_use.loc_name.clone();
        } else {
            // TODO: should we use ty_params or method_params?
            let syntypes = get_arg_syntypes_for_procedure_call(
                self.env.tcx(),
                &self.ty_translator,
                callee_did,
                ty_params.as_slice(),
            )?;

            let mut translated_params = quantified_args.fn_ty_param_inst;

            info!(
                "Registered procedure instance {} of {:?} with {:?} and layouts {:?}",
                method_loc_name, callee_did, translated_params, syntypes
            );

            let specs = trait_specs.into_iter().map(|x| x.try_into().unwrap()).collect();
            let proc_use = radium::UsedProcedure::new(
                method_loc_name,
                method_spec_term,
                vec![],
                quantified_args.scope,
                specs,
                translated_params,
                quantified_args.fn_lft_param_inst,
                syntypes,
            );

            res = proc_use.loc_name.clone();
            self.collected_procedures.insert(tup, proc_use);
        }
        trace!("leave register_use_procedure");
        Ok((res, quantified_args.callee_ty_param_inst, quantified_args.callee_lft_param_inst))
    }

    /// Enqueues a basic block for processing, if it has not already been processed,
    /// and marks it as having been processed.
    fn enqueue_basic_block(&mut self, bb: BasicBlock) {
        if !self.processed_bbs.contains(&bb) {
            self.bb_queue.push(bb);
            self.processed_bbs.insert(bb);
        }
    }

    fn format_region(&self, r: facts::Region) -> String {
        let lft = self.info.mk_atomic_region(r);
        self.ty_translator.format_atomic_region(&lft)
    }

    /// Parse the attributes on spec closure `did` as loop annotations and add it as an invariant
    /// to the generated code.
    fn parse_attributes_on_loop_spec_closure(
        &self,
        loop_head: BasicBlock,
        did: Option<DefId>,
    ) -> radium::LoopSpec {
        // for now: just make invariants True.

        // need to do:
        // - find out the locals in the right order, make parameter names for them. based on their type and
        //   initialization status, get the refinement type.
        // - output/pretty-print this map when generating the typing proof of each function. [done]
        //  + should not be a separate definition, but rather a "set (.. := ...)" with a marker type so
        //    automation can find it.

        // representation of loop invariants:
        // - introduce parameters for them.

        let mut rfn_binders = Vec::new();
        let prop_body = radium::IProp::True;

        // determine invariant on initialization:
        // - we need this both for the refinement invariant (though this could be removed if we make uninit
        //   generic over the refinement)
        // - in order to establish the initialization invariant in each loop iteration, since we don't have
        //   proper subtyping for uninit => maybe we could fix this too by making uninit variant in the
        //   refinement type? then we could have proper subtyping lemmas.
        //  + to bring it to the right refinement type initially, maybe have some automation /
        //  annotation
        // TODO: consider changing it like that.
        //
        // Note that StorageDead will not help us for determining initialization/ making it invariant, since
        // it only applies to full stack slots, not individual paths. one thing that makes it more
        // complicated in the frontend: initialization may in practice also be path-dependent.
        //  - this does not cause issues with posing a too strong loop invariant,
        //  - but this poses an issue for annotations
        //
        //

        // get locals
        for (_, name, ty) in &self.fn_locals {
            // get the refinement type
            let mut rfn_ty = ty.get_rfn_type();
            // wrap it in place_rfn, since we reason about places
            rfn_ty = coq::term::Type::PlaceRfn(Box::new(rfn_ty));

            // determine their initialization status
            //let initialized = true; // TODO
            // determine the actual refinement type for the current initialization status.

            let rfn_name = format!("r_{}", name);
            rfn_binders.push(coq::binder::Binder::new(Some(rfn_name), rfn_ty));
        }

        // TODO what do we do about stuff connecting borrows?
        if let Some(did) = did {
            let attrs = self.env.get_attributes(did);
            info!("attrs for loop {:?}: {:?}", loop_head, attrs);
        } else {
            info!("no attrs for loop {:?}", loop_head);
        }

        let pred = radium::IPropPredicate::new(rfn_binders, prop_body);
        radium::LoopSpec {
            func_predicate: pred,
        }
    }

    /// Checks whether a place access descends below a reference.
    fn check_place_below_reference(&self, place: &Place<'tcx>) -> bool {
        if self.checked_op_temporaries.contains_key(&place.local) {
            // temporaries are never below references
            return false;
        }

        for (pl, _) in place.iter_projections() {
            // check if the current ty is a reference that we then descend under with proj
            let cur_ty_kind = pl.ty(&self.proc.get_mir().local_decls, self.env.tcx()).ty.kind();
            if let TyKind::Ref(_, _, _) = cur_ty_kind {
                return true;
            }
        }

        false
    }

    fn get_assignment_strong_update_constraints(
        &mut self,
        loc: Location,
    ) -> HashSet<(Region, Region, PointIndex)> {
        let info = &self.info;
        let input_facts = &info.borrowck_in_facts;
        let subset_base = &input_facts.subset_base;

        let mut constraints = HashSet::new();
        // Polonius subset constraint are spawned for the midpoint
        let midpoint = self.info.interner.get_point_index(&facts::Point {
            location: loc,
            typ: facts::PointType::Mid,
        });

        // for strong update: emit mutual equalities
        // TODO: alternative implementation: structurally compare regions in LHS type and RHS type
        for (s1, s2, point) in subset_base {
            if *point == midpoint {
                let lft1 = self.info.mk_atomic_region(*s1);
                let lft2 = self.info.mk_atomic_region(*s2);

                // We only care about inclusions into a place lifetime.
                // Moreover, we want to filter out the universal inclusions which are always
                // replicated at every point.
                if lft2.is_place() && !lft1.is_universal() {
                    // take this constraint and the reverse constraint
                    constraints.insert((*s1, *s2, *point));
                    //constraints.insert((*s2, *s1, *point));
                }
            }
        }
        constraints
    }

    fn get_assignment_weak_update_constraints(
        &mut self,
        loc: Location,
    ) -> HashSet<(Region, Region, PointIndex)> {
        let info = &self.info;
        let input_facts = &info.borrowck_in_facts;
        let subset_base = &input_facts.subset_base;

        let mut constraints = HashSet::new();
        // Polonius subset constraint are spawned for the midpoint
        let midpoint = self.info.interner.get_point_index(&facts::Point {
            location: loc,
            typ: facts::PointType::Mid,
        });

        // for weak updates: should mirror the constraints generated by Polonius
        for (s1, s2, point) in subset_base {
            if *point == midpoint {
                // take this constraint
                // TODO should there be exceptions to this?

                if !self.inclusion_tracker.check_inclusion(*s1, *s2, *point) {
                    // only add it if it does not hold already, since we will enforce this
                    // constraint dynamically.
                    constraints.insert((*s1, *s2, *point));
                }
            }
        }
        constraints
    }

    /// Split the type of a function operand of a call expression to a base type and an instantiation for
    /// generics.
    fn call_expr_op_split_inst(
        &self,
        constant: &Constant<'tcx>,
    ) -> Result<
        (DefId, ty::PolyFnSig<'tcx>, ty::GenericArgsRef<'tcx>, ty::PolyFnSig<'tcx>),
        TranslationError<'tcx>,
    > {
        match constant.literal {
            ConstantKind::Ty(c) => {
                match c.ty().kind() {
                    TyKind::FnDef(def, args) => {
                        let ty: ty::EarlyBinder<Ty<'tcx>> = self.env.tcx().type_of(def);
                        let ty_ident = ty.instantiate_identity();
                        assert!(ty_ident.is_fn());
                        let ident_sig = ty_ident.fn_sig(self.env.tcx());

                        let ty_instantiated = ty.instantiate(self.env.tcx(), args.as_slice());
                        let instantiated_sig = ty_instantiated.fn_sig(self.env.tcx());

                        Ok((*def, ident_sig, args, instantiated_sig))
                    },
                    // TODO handle FnPtr, closure
                    _ => Err(TranslationError::Unimplemented {
                        description: "implement function pointers".to_owned(),
                    }),
                }
            },
            ConstantKind::Val(_, ty) => {
                match ty.kind() {
                    TyKind::FnDef(def, args) => {
                        let ty: ty::EarlyBinder<Ty<'tcx>> = self.env.tcx().type_of(def);

                        let ty_ident = ty.instantiate_identity();
                        assert!(ty_ident.is_fn());
                        let ident_sig = ty_ident.fn_sig(self.env.tcx());

                        let ty_instantiated = ty.instantiate(self.env.tcx(), args.as_slice());
                        let instantiated_sig = ty_instantiated.fn_sig(self.env.tcx());

                        Ok((*def, ident_sig, args, instantiated_sig))
                    },
                    // TODO handle FnPtr, closure
                    _ => Err(TranslationError::Unimplemented {
                        description: "implement function pointers".to_owned(),
                    }),
                }
            },
            ConstantKind::Unevaluated(_, _) => Err(TranslationError::Unimplemented {
                description: "implement ConstantKind::Unevaluated".to_owned(),
            }),
        }
    }

    /// Find the optional `DefId` of the closure giving the invariant for the loop with head `head_bb`.
    fn find_loop_spec_closure(&self, head_bb: BasicBlock) -> Result<Option<DefId>, TranslationError<'tcx>> {
        let bodies = self.proc.loop_info().get_loop_body(head_bb);
        let basic_blocks = &self.proc.get_mir().basic_blocks;

        // we go in order through the bodies in order to not stumble upon an annotation for a
        // nested loop!
        for body in bodies {
            // check that we did not go below a nested loop
            if self.proc.loop_info().get_loop_head(*body) == Some(head_bb) {
                // check the statements for an assignment
                let data = basic_blocks.get(*body).unwrap();
                for stmt in &data.statements {
                    if let StatementKind::Assign(box (pl, _)) = stmt.kind {
                        if let Some(did) = self.is_spec_closure_local(pl.local)? {
                            return Ok(Some(did));
                        }
                    }
                }
            }
        }

        Ok(None)
    }

    /// Translate a goto-like jump to `target`.
    fn translate_goto_like(
        &mut self,
        _loc: &Location,
        target: BasicBlock,
    ) -> Result<radium::Stmt, TranslationError<'tcx>> {
        self.enqueue_basic_block(target);
        let res_stmt = radium::Stmt::GotoBlock(target.as_usize());

        let loop_info = self.proc.loop_info();
        if loop_info.is_loop_head(target) && !self.loop_specs.contains_key(&target) {
            let spec_defid = self.find_loop_spec_closure(target)?;
            self.loop_specs.insert(target, spec_defid);
        }

        Ok(res_stmt)
    }

    /// Check if a call goes to `std::rt::begin_panic`
    fn is_call_destination_panic(&mut self, func: &Operand) -> bool {
        let Operand::Constant(box c) = func else {
            return false;
        };

        let ConstantKind::Val(_, ty) = c.literal else {
            return false;
        };

        let TyKind::FnDef(did, _) = ty.kind() else {
            return false;
        };

        if let Some(panic_id_std) =
            search::try_resolve_did(self.env.tcx(), &["std", "panicking", "begin_panic"])
        {
            if panic_id_std == *did {
                return true;
            }
        } else {
            warn!("Failed to determine DefId of std::panicking::begin_panic");
        }

        if let Some(panic_id_core) = search::try_resolve_did(self.env.tcx(), &["core", "panicking", "panic"])
        {
            if panic_id_core == *did {
                return true;
            }
        } else {
            warn!("Failed to determine DefId of core::panicking::panic");
        }

        false
    }

    /// Registers a drop shim for a particular type for the translation.
    #[allow(clippy::unused_self)]
    const fn register_drop_shim_for(&self, _ty: Ty<'tcx>) {
        // TODO!
        //let drop_in_place_did: DefId = search::try_resolve_did(self.env.tcx(), &["std", "ptr",
        // "drop_in_place"]).unwrap();

        //let x: ty::InstanceDef = ty::InstanceDef::DropGlue(drop_in_place_did, Some(ty));
        //let body: &'tcx mir::Body = self.env.tcx().mir_shims(x);

        //info!("Generated drop shim for {:?}", ty);
        //Self::dump_body(body);
    }

    fn compute_call_regions(
        &self,
        func: &Constant<'tcx>,
        loc: Location,
    ) -> Result<CallRegions, TranslationError<'tcx>> {
        let midpoint = self.info.interner.get_point_index(&facts::Point {
            location: loc,
            typ: facts::PointType::Mid,
        });

        // first identify substitutions for the early-bound regions
        let (target_did, sig, substs, _) = self.call_expr_op_split_inst(func)?;
        info!("calling function {:?}", target_did);
        let mut early_regions = Vec::new();
        info!("call substs: {:?} = {:?}, {:?}", func, sig, substs);
        for a in substs {
            if let ty::GenericArgKind::Lifetime(r) = a.unpack() {
                if let ty::RegionKind::ReVar(r) = r.kind() {
                    early_regions.push(r);
                }
            }
        }
        info!("call region instantiations (early): {:?}", early_regions);

        // this is a hack to identify the inference variables introduced for the
        // call's late-bound universals.
        // TODO: Can we get this information in a less hacky way?
        // One approach: compute the early + late bound regions for a given DefId, similarly to how
        // we do it when starting to translate a function
        // Problem: this doesn't give a straightforward way to compute their instantiation

        // now find all the regions that appear in type parameters we instantiate.
        // These are regions that the callee doesn't know about.
        let mut generic_regions = HashSet::new();
        let mut clos = |r: ty::Region<'tcx>, _| match r.kind() {
            ty::RegionKind::ReVar(rv) => {
                generic_regions.insert(rv);
                r
            },
            _ => r,
        };

        for a in substs {
            if let ty::GenericArgKind::Type(c) = a.unpack() {
                let mut folder = ty::fold::RegionFolder::new(self.env.tcx(), &mut clos);
                folder.fold_ty(c);
            }
        }