function_body.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, 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, TypeFoldable};
use rr_rustc_interface::middle::{mir, ty};
use rr_rustc_interface::{abi, ast, middle};

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::verbose_function_spec_parser::{
    ClosureMetaInfo, FunctionSpecParser, VerboseFunctionSpecParser,
};
use crate::type_translator::*;
use crate::tyvars::*;
use crate::{traits, utils};

/**
 * Tracks the functions we translated and the Coq names they are available under.
 * To account for dependencies between functions, we may register translated names before we have
 * actually translated the function.
 */

#[derive(Copy, Clone, Eq, PartialEq, Debug)]
pub enum ProcedureMode {
    Prove,
    OnlySpec,
    TrustMe,
    Shim,
    Ignore,
}

impl ProcedureMode {
    pub fn is_prove(self) -> bool {
        self == Self::Prove
    }

    pub fn is_only_spec(self) -> bool {
        self == Self::OnlySpec
    }

    pub fn is_trust_me(self) -> bool {
        self == Self::TrustMe
    }

    pub fn is_shim(self) -> bool {
        self == Self::Shim
    }

    pub fn is_ignore(self) -> bool {
        self == Self::Ignore
    }

    pub fn needs_proof(self) -> bool {
        self == Self::Prove
    }

    pub fn needs_def(self) -> bool {
        self == Self::Prove || self == Self::TrustMe
    }
}

#[derive(Clone)]
pub struct ProcedureMeta {
    spec_name: String,
    name: String,
    mode: ProcedureMode,
}

impl ProcedureMeta {
    pub const fn new(spec_name: String, name: String, mode: ProcedureMode) -> Self {
        Self {
            spec_name,
            name,
            mode,
        }
    }

    pub fn get_spec_name(&self) -> &str {
        &self.spec_name
    }

    pub fn get_name(&self) -> &str {
        &self.name
    }

    pub const fn get_mode(&self) -> ProcedureMode {
        self.mode
    }
}

pub struct ProcedureScope<'def> {
    /// maps the defid to (code_name, spec_name, name)
    name_map: BTreeMap<DefId, ProcedureMeta>,
    /// track the actually translated functions
    translated_functions: BTreeMap<DefId, radium::Function<'def>>,
    /// track the functions with just a specification (rr::only_spec)
    specced_functions: BTreeMap<DefId, radium::FunctionSpec<'def>>,
}

impl<'def> ProcedureScope<'def> {
    pub fn new() -> Self {
        Self {
            name_map: BTreeMap::new(),
            translated_functions: BTreeMap::new(),
            specced_functions: BTreeMap::new(),
        }
    }

    pub fn lookup_function(&self, did: DefId) -> Option<ProcedureMeta> {
        self.name_map.get(&did).cloned()
    }

    /// Lookup the Coq spec name for a function.
    pub fn lookup_function_spec_name(&self, did: DefId) -> Option<&str> {
        self.name_map.get(&did).map(ProcedureMeta::get_spec_name)
    }

    /// Lookup the name for a function.
    pub fn lookup_function_mangled_name(&self, did: DefId) -> Option<&str> {
        self.name_map.get(&did).map(ProcedureMeta::get_name)
    }

    /// Lookup the mode for a function.
    pub fn lookup_function_mode(&self, did: DefId) -> Option<ProcedureMode> {
        self.name_map.get(&did).map(ProcedureMeta::get_mode)
    }

    /// Register a function.
    pub fn register_function(&mut self, did: DefId, meta: ProcedureMeta) -> Result<(), String> {
        if self.name_map.insert(did, meta).is_some() {
            Err(format!("function for defid {:?} has already been registered", did))
        } else {
            Ok(())
        }
    }

    /// Provide the code for a translated function.
    pub fn provide_translated_function(&mut self, did: DefId, trf: radium::Function<'def>) {
        let meta = &self.name_map[&did];
        assert!(meta.get_mode().needs_def());
        assert!(self.translated_functions.insert(did, trf).is_none());
    }

    /// Provide the specification for an `only_spec` function.
    pub fn provide_specced_function(&mut self, did: DefId, spec: radium::FunctionSpec<'def>) {
        let meta = &self.name_map[&did];
        assert!(meta.get_mode().is_only_spec());
        assert!(self.specced_functions.insert(did, spec).is_none());
    }

    /// Iterate over the functions we have generated code for.
    pub fn iter_code(&self) -> btree_map::Iter<'_, DefId, radium::Function<'def>> {
        self.translated_functions.iter()
    }

    /// Iterate over the functions we have generated only specs for.
    pub fn iter_only_spec(&self) -> btree_map::Iter<'_, DefId, radium::FunctionSpec<'def>> {
        self.specced_functions.iter()
    }
}

/// Scope of consts that are available
pub struct ConstScope<'def> {
    pub statics: HashMap<DefId, radium::StaticMeta<'def>>,
}

// 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>,
}

pub struct FunctionTranslator<'a, 'def, 'tcx> {
    env: &'def Environment<'tcx>,
    /// this needs to be annotated with the right borrowck things
    proc: &'def Procedure<'tcx>,
    /// the Caesium function buildder
    translated_fn: radium::FunctionBuilder<'def>,
    /// tracking lifetime inclusions for the generation of lifetime inclusions
    inclusion_tracker: InclusionTracker<'a, 'tcx>,

    /// registry of other procedures
    procedure_registry: &'a ProcedureScope<'def>,
    /// registry of consts
    const_registry: &'a ConstScope<'def>,
    /// attributes on this function
    attrs: &'a [&'a ast::ast::AttrItem],
    /// polonius info for this function
    info: &'a PoloniusInfo<'a, 'tcx>,
    /// translator for types
    ty_translator: LocalTypeTranslator<'a, 'def, 'tcx>,
    /// argument types (from the signature, with generics substituted)
    inputs: Vec<Ty<'tcx>>,
}

impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
    pub fn process_lifetimes_of_args(
        env: &Environment<'tcx>,
        params: &[ty::GenericArg<'tcx>],
        sig: ty::Binder<'tcx, ty::FnSig<'tcx>>,
        _body: &mir::Body<'tcx>,
    ) -> (Vec<ty::Ty<'tcx>>, ty::Ty<'tcx>, HashMap<ty::RegionVid, (String, Option<String>)>) {
        let mut universal_lifetimes = HashMap::new();

        // we create a substitution that replaces early bound regions with their Polonius
        // region variables
        let mut subst_early_bounds: Vec<ty::GenericArg<'tcx>> = Vec::new();
        let mut num_early_bounds = 0;
        for a in params {
            match a.unpack() {
                ty::GenericArgKind::Lifetime(r) => {
                    // skip over 0 = static
                    let next_id = ty::RegionVid::from_u32(num_early_bounds + 1);
                    let revar = ty::Region::new_var(env.tcx(), next_id);
                    num_early_bounds += 1;
                    subst_early_bounds.push(ty::GenericArg::from(revar));

                    match *r {
                        ty::RegionKind::ReEarlyBound(r) => {
                            let name = strip_coq_ident(r.name.as_str());
                            universal_lifetimes.insert(next_id, (format!("ulft_{}", name), Some(name)));
                        },
                        _ => {
                            universal_lifetimes.insert(next_id, (format!("ulft_{}", num_early_bounds), None));
                        },
                    }
                },
                _ => {
                    subst_early_bounds.push(*a);
                },
            }
        }
        let subst_early_bounds = env.tcx().mk_args(&subst_early_bounds);

        // add names for late bound region variables
        let mut num_late_bounds = 0;
        for b in sig.bound_vars() {
            let next_id = ty::RegionVid::from_u32(num_early_bounds + num_late_bounds + 1);

            let ty::BoundVariableKind::Region(r) = b else {
                continue;
            };

            match r {
                ty::BoundRegionKind::BrNamed(_, sym) => {
                    let mut region_name = strip_coq_ident(sym.as_str());
                    if region_name == "_" {
                        region_name = next_id.as_usize().to_string();
                        universal_lifetimes.insert(next_id, (format!("ulft_{}", region_name), None));
                    } else {
                        universal_lifetimes
                            .insert(next_id, (format!("ulft_{}", region_name), Some(region_name)));
                    }
                },
                ty::BoundRegionKind::BrAnon(_) => {
                    universal_lifetimes.insert(next_id, (format!("ulft_{}", next_id.as_usize()), None));
                },
                _ => (),
            }

            num_late_bounds += 1;
        }

        // replace late-bound region variables by re-enumerating them in the same way as the MIR
        // type checker does (that this happens in the same way is important to make the names
        // line up!)
        let mut next_index = num_early_bounds + 1; // skip over one additional due to static
        let mut folder = |_| {
            let cur_index = next_index;
            next_index += 1;
            ty::Region::new_var(env.tcx(), ty::RegionVid::from_u32(cur_index))
        };
        let (late_sig, _late_region_map) = env.tcx().replace_late_bound_regions(sig, &mut folder);

        // replace early bound variables
        let inputs: Vec<_> = late_sig
            .inputs()
            .iter()
            .map(|ty| ty_instantiate(*ty, env.tcx(), subst_early_bounds))
            .collect();

        let output = ty_instantiate(late_sig.output(), env.tcx(), subst_early_bounds);

        (inputs, output, universal_lifetimes)
    }

    /// At the start of the function, there's a universal (placeholder) region for reference argument.
    /// These get subsequently relabeled.
    /// Given the relabeled region, find the original placeholder region.
    fn find_placeholder_region_for(r: ty::RegionVid, info: &PoloniusInfo) -> Option<ty::RegionVid> {
        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,
        });

        for (r1, r2, p) in &info.borrowck_in_facts.subset_base {
            if *p == root_point && *r2 == r {
                info!("find placeholder region for: {:?} ⊑ {:?} = r = {:?}", r1, r2, r);
                return Some(*r1);
            }
        }
        None
    }

    /// Create a translation instance for a closure.
    pub fn new_closure(
        env: &'def Environment<'tcx>,
        meta: &ProcedureMeta,
        proc: Procedure<'tcx>,
        attrs: &'a [&'a ast::ast::AttrItem],
        ty_translator: &'def TypeTranslator<'def, 'tcx>,
        proc_registry: &'a ProcedureScope<'def>,
        const_registry: &'a ConstScope<'def>,
    ) -> Result<Self, TranslationError> {
        let mut translated_fn = radium::FunctionBuilder::new(&meta.name, &meta.spec_name);

        // TODO can we avoid the leak
        let proc: &'def Procedure = &*Box::leak(Box::new(proc));
        let body = proc.get_mir();
        Self::dump_body(body);

        let ty: ty::EarlyBinder<Ty<'tcx>> = env.tcx().type_of(proc.get_id());
        let ty = ty.instantiate_identity();

        let closure_kind = match ty.kind() {
            TyKind::Closure(_def, closure_args) => {
                assert!(ty.is_closure());
                closure_args.as_closure().kind()
            },
            _ => panic!("can not handle non-closures"),
        };

        let local_decls = &body.local_decls;
        let closure_arg = local_decls.get(Local::from_usize(1)).unwrap();

        let closure_ty = match closure_kind {
            ty::ClosureKind::Fn => {
                let ty::TyKind::Ref(_, ty, _) = closure_arg.ty.kind() else {
                    unreachable!();
                };

                ty
            },

            ty::ClosureKind::FnMut => {
                let ty::TyKind::Ref(_, ty, _) = closure_arg.ty.kind() else {
                    unreachable!("unexpected type {:?}", closure_arg.ty);
                };

                ty
            },

            ty::ClosureKind::FnOnce => &closure_arg.ty,
        };

        let mut capture_regions = Vec::new();

        let ty::TyKind::Closure(did, closure_args) = closure_ty.kind() else {
            unreachable!();
        };

        let clos = closure_args.as_closure();

        let tupled_upvars_tys = clos.tupled_upvars_ty();
        let upvars_tys = clos.upvar_tys();
        let parent_args = clos.parent_args();
        let unnormalized_sig = clos.sig();

        let sig = normalize_in_function(proc.get_id(), env.tcx(), unnormalized_sig)?;
        info!("closure sig: {:?}", sig);

        let captures = env.tcx().closure_captures(did.as_local().unwrap());
        info!("Closure has captures: {:?}", captures);

        // find additional lifetime parameters
        for (place, ty) in captures.iter().zip(clos.upvar_tys().iter()) {
            if place.region.is_some() {
                // find region from ty
                if let ty::TyKind::Ref(region, _, _) = ty.kind() {
                    capture_regions.push(*region);
                }
            }
        }

        info!("Closure capture regions: {:?}", capture_regions);
        info!("Closure arg upvar_tys: {:?}", tupled_upvars_tys);
        info!("Function signature: {:?}", sig);
        info!("Closure generic args: {:?}", parent_args);

        let info = match PoloniusInfo::new(env, proc) {
            Ok(info) => info,
            Err(err) => return Err(TranslationError::UnknownError(format!("{:?}", err))),
        };

        // TODO: avoid leak
        let info: &'def PoloniusInfo = &*Box::leak(Box::new(info));

        // For closures, we only handle the parent's args here!
        // TODO: do we need to do something special for the parent's late-bound region
        // parameters?
        // TODO: should we always take the lifetime parameters?
        let params = parent_args;
        //proc.get_type_params();
        info!("Function generic args: {:?}", params);

        // dump graphviz files
        // color code: red: dying loan, pink: becoming a zombie; green: is zombie
        if rrconfig::dump_borrowck_info() {
            dump_borrowck_info(env, proc.get_id(), info);
        }

        let (tupled_inputs, output, mut universal_lifetimes) =
            Self::process_lifetimes_of_args(env, params, sig, body);

        // Process the lifetime parameters that come from the captures
        for r in capture_regions {
            // TODO: problem: we're introducing inconsistent names here.
            let ty::RegionKind::ReVar(r) = r.kind() else {
                unreachable!();
            };

            let lft = info.mk_atomic_region(r);
            let name = format_atomic_region_direct(&lft, None);
            universal_lifetimes.insert(r, (name, None));
        }

        // also add the lifetime for the outer reference
        let mut maybe_outer_lifetime = None;
        if let ty::TyKind::Ref(r, _, _) = closure_arg.ty.kind() {
            let ty::RegionKind::ReVar(r) = r.kind() else {
                unreachable!();
            };

            // We need to do some hacks here to find the right Polonius region:
            // `r` is the non-placeholder region that the variable gets, but we are
            // looking for the corresponding placeholder region
            let r2 = Self::find_placeholder_region_for(r, info).unwrap();

            info!("using lifetime {:?} for closure universal", r2);
            let lft = info.mk_atomic_region(r2);
            let name = format_atomic_region_direct(&lft, None);
            universal_lifetimes.insert(r2, (name, None));

            maybe_outer_lifetime = Some(r2);
        }

        // detuple the inputs
        assert!(tupled_inputs.len() == 1);
        let input_tuple_ty = tupled_inputs[0];
        let mut inputs = Vec::new();

        // push the closure as the first argument
        /*
        if let Some(r2) = maybe_outer_lifetime {
            // in this case, we need to patch the region first
            if let ty::TyKind::Ref(_, ty, m) = closure_arg.ty.kind() {
                let new_region = ty::Region::new_var(env.tcx(), r2);
                inputs.push(env.tcx().mk_ty_from_kind(ty::TyKind::Ref(new_region, *ty, *m)));
            }
        }
        else {
            inputs.push(closure_arg.ty);
        }
        */

        if let ty::TyKind::Tuple(args) = input_tuple_ty.kind() {
            inputs.extend(args.iter());
        }

        info!("inputs({}): {:?}, output: {:?}", inputs.len(), inputs, output);
        info!("Have lifetime parameters: {:?}", universal_lifetimes);

        // add universal lifetimes to the spec
        for (lft, name) in universal_lifetimes.values() {
            //let lft = info::AtomicRegion::Universal(info::UniversalRegionKind::Local,
            // ty::RegionVid::from_u32(1+r));
            translated_fn
                .add_universal_lifetime(name.clone(), lft.to_string())
                .map_err(TranslationError::UnknownError)?;
        }

        let mut inclusion_tracker = InclusionTracker::new(info);
        // add placeholder subsets
        let initial_point: facts::Point = facts::Point {
            location: BasicBlock::from_u32(0).start_location(),
            typ: facts::PointType::Start,
        };
        for (r1, r2) in &info.borrowck_in_facts.known_placeholder_subset {
            inclusion_tracker.add_static_inclusion(*r1, *r2, info.interner.get_point_index(&initial_point));
        }

        // enter the procedure
        let universal_lifetime_map: HashMap<_, _> =
            universal_lifetimes.into_iter().map(|(x, y)| (x, y.0)).collect();
        let type_scope =
            TypeTranslationScope::new(proc.get_id(), env.tcx().mk_args(params), universal_lifetime_map)?;
        // add generic args to the fn
        let generics = &type_scope.generic_scope;
        for t in generics.iter().flatten() {
            translated_fn.add_generic_type(t.clone());
        }

        let mut t = Self {
            env,
            proc,
            info,
            translated_fn,
            inclusion_tracker,
            procedure_registry: proc_registry,
            attrs,
            ty_translator: LocalTypeTranslator::new(ty_translator, type_scope),
            const_registry,
            inputs: inputs.clone(),
        };

        // add universal constraints
        let universal_constraints = t.get_relevant_universal_constraints();
        info!("univeral constraints: {:?}", universal_constraints);
        for (lft1, lft2) in universal_constraints {
            t.translated_fn
                .add_universal_lifetime_constraint(lft1, lft2)
                .map_err(TranslationError::UnknownError)?;
        }

        // compute meta information needed to generate the spec
        let mut translated_upvars_types = Vec::new();
        for ty in upvars_tys {
            let translated_ty = t.ty_translator.translate_type(ty)?;
            translated_upvars_types.push(translated_ty);
        }

        let meta = {
            let scope = t.ty_translator.scope.borrow();

            ClosureMetaInfo {
                kind: closure_kind,
                captures,
                capture_tys: &translated_upvars_types,
                closure_lifetime: maybe_outer_lifetime.map(|x| scope.lookup_universal_region(x).unwrap()),
            }
        };

        // process attributes
        t.process_closure_attrs(&inputs, output, meta)?;
        Ok(t)
    }

    /// Translate the body of a function.
    pub fn new(
        env: &'def Environment<'tcx>,
        meta: &ProcedureMeta,
        proc: Procedure<'tcx>,
        attrs: &'a [&'a ast::ast::AttrItem],
        ty_translator: &'def TypeTranslator<'def, 'tcx>,
        proc_registry: &'a ProcedureScope<'def>,
        const_registry: &'a ConstScope<'def>,
    ) -> Result<Self, TranslationError> {
        let mut translated_fn = radium::FunctionBuilder::new(&meta.name, &meta.spec_name);

        // TODO can we avoid the leak
        let proc: &'def Procedure = &*Box::leak(Box::new(proc));

        let body = proc.get_mir();
        Self::dump_body(body);

        let ty: ty::EarlyBinder<Ty<'tcx>> = env.tcx().type_of(proc.get_id());
        let ty = ty.instantiate_identity();
        // substs are the generic args of this function (including lifetimes)
        // sig is the function signature
        let sig = match ty.kind() {
            TyKind::FnDef(_def, _args) => {
                assert!(ty.is_fn());
                ty.fn_sig(env.tcx())
            },
            _ => panic!("can not handle non-fns"),
        };

        let sig = normalize_in_function(proc.get_id(), env.tcx(), sig)?;
        info!("Function signature: {:?}", sig);

        let info = match PoloniusInfo::new(env, proc) {
            Ok(info) => info,
            Err(err) => return Err(TranslationError::UnknownError(format!("{:?}", err))),
        };

        // TODO: avoid leak
        let info: &'def PoloniusInfo = &*Box::leak(Box::new(info));

        let params = proc.get_type_params();
        info!("Function generic args: {:?}", params);

        // dump graphviz files
        // color code: red: dying loan, pink: becoming a zombie; green: is zombie
        if rrconfig::dump_borrowck_info() {
            dump_borrowck_info(env, proc.get_id(), info);
        }

        let (inputs, output, universal_lifetimes) = Self::process_lifetimes_of_args(env, params, sig, body);
        info!("Have lifetime parameters: {:?}", universal_lifetimes);
        info!("inputs: {:?}, output: {:?}", inputs, output);

        // add universal lifetimes to the spec
        for (lft, name) in universal_lifetimes.values() {
            translated_fn
                .add_universal_lifetime(name.clone(), lft.to_string())
                .map_err(TranslationError::UnknownError)?;
        }

        let mut inclusion_tracker = InclusionTracker::new(info);
        // add placeholder subsets
        let initial_point: facts::Point = facts::Point {
            location: BasicBlock::from_u32(0).start_location(),
            typ: facts::PointType::Start,
        };
        for (r1, r2) in &info.borrowck_in_facts.known_placeholder_subset {
            inclusion_tracker.add_static_inclusion(*r1, *r2, info.interner.get_point_index(&initial_point));
        }

        // enter the procedure
        let universal_lifetime_map: HashMap<_, _> =
            universal_lifetimes.into_iter().map(|(x, y)| (x, y.0)).collect();

        let type_scope = TypeTranslationScope::new(proc.get_id(), params, universal_lifetime_map)?;
        // add generic args to the fn
        for t in type_scope.generic_scope.iter().flatten() {
            translated_fn.add_generic_type(t.clone());
        }

        let mut t = Self {
            env,
            proc,
            info,
            translated_fn,
            inclusion_tracker,
            procedure_registry: proc_registry,
            attrs,
            ty_translator: LocalTypeTranslator::new(ty_translator, type_scope),
            const_registry,
            inputs: inputs.clone(),
        };

        // add universal constraints
        let universal_constraints = t.get_relevant_universal_constraints();
        info!("univeral constraints: {:?}", universal_constraints);
        for (lft1, lft2) in universal_constraints {
            t.translated_fn
                .add_universal_lifetime_constraint(lft1, lft2)
                .map_err(TranslationError::UnknownError)?;
        }

        // process attributes
        t.process_attrs(inputs.as_slice(), output)?;

        Ok(t)
    }

    /// Filter the "interesting" constraints between universal lifetimes that need to hold
    /// (this does not include the constraints that need to hold for all universal lifetimes,
    /// e.g. that they outlive the function lifetime and are outlived by 'static).
    fn get_relevant_universal_constraints(&mut self) -> Vec<(radium::UniversalLft, radium::UniversalLft)> {
        let info = &self.info;
        let input_facts = &info.borrowck_in_facts;
        let placeholder_subset = &input_facts.known_placeholder_subset;

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

        let mut universal_constraints = Vec::new();

        for (r1, r2) in placeholder_subset {
            if let polonius_info::RegionKind::Universal(uk1) = info.get_region_kind(*r1) {
                if let polonius_info::RegionKind::Universal(uk2) = info.get_region_kind(*r2) {
                    // if LHS is static, ignore.
                    if uk1 == polonius_info::UniversalRegionKind::Static {
                        continue;
                    }
                    // if RHS is the function lifetime, ignore
                    if uk2 == polonius_info::UniversalRegionKind::Function {
                        continue;
                    }

                    let to_universal = || {
                        let x = self.to_universal_lft(uk1, *r2)?;
                        let y = self.to_universal_lft(uk2, *r1)?;
                        Some((x, y))
                    };
                    // else, add this constraint
                    // for the purpose of this analysis, it is fine to treat it as a dynamic inclusion
                    if let Some((x, y)) = to_universal() {
                        self.inclusion_tracker.add_dynamic_inclusion(*r1, *r2, root_point);
                        universal_constraints.push((x, y));
                    };
                }
            }
        }
        universal_constraints
    }

    /// Parse and process attributes of this closure.
    fn process_closure_attrs<'b>(
        &mut self,
        normalized_inputs: &[Ty<'tcx>],
        normalized_output: Ty<'tcx>,
        meta: ClosureMetaInfo<'b, 'tcx, 'def>,
    ) -> Result<(), TranslationError> {
        trace!("entering process_closure_attrs");
        let v = self.attrs;

        info!("inputs: {:?}, output: {:?}", normalized_inputs, normalized_output);
        let mut translated_arg_types: Vec<radium::Type<'def>> = Vec::new();
        for arg in normalized_inputs {
            let translated: radium::Type<'def> = self.ty_translator.translate_type_no_normalize(*arg)?;
            translated_arg_types.push(translated);
        }
        let translated_ret_type: radium::Type<'def> =
            // output is already normalized
            self.ty_translator.translate_type_no_normalize(normalized_output)?;
        info!("translated function type: {:?} → {}", translated_arg_types, translated_ret_type);

        let parser = rrconfig::attribute_parser();

        if parser.as_str() != "verbose" {
            trace!("leaving process_closure_attrs");
            return Err(TranslationError::UnknownAttributeParser(parser));
        }

        let ty_translator = &self.ty_translator;
        let mut parser = VerboseFunctionSpecParser::new(&translated_arg_types, &translated_ret_type, |lit| {
            ty_translator.translator.intern_literal(lit)
        });

        parser
            .parse_closure_spec(v, &mut self.translated_fn, meta, |x| ty_translator.make_tuple_use(x))
            .map_err(TranslationError::AttributeError)?;

        trace!("leaving process_closure_attrs");
        Ok(())
    }

    /// Parse and process attributes of this function.
    fn process_attrs(
        &mut self,
        normalized_inputs: &[Ty<'tcx>],
        normalized_output: Ty<'tcx>,
    ) -> Result<(), TranslationError> {
        let v = self.attrs;

        info!("inputs: {:?}, output: {:?}", normalized_inputs, normalized_output);
        let mut translated_arg_types: Vec<radium::Type<'def>> = Vec::new();
        for arg in normalized_inputs {
            let translated: radium::Type<'def> = self.ty_translator.translate_type_no_normalize(*arg)?;
            translated_arg_types.push(translated);
        }
        let translated_ret_type: radium::Type<'def> =
            self.ty_translator.translate_type_no_normalize(normalized_output)?;
        info!("translated function type: {:?} → {}", translated_arg_types, translated_ret_type);

        let parser = rrconfig::attribute_parser();
        match parser.as_str() {
            "verbose" => {
                let ty_translator = &self.ty_translator;
                let mut parser: VerboseFunctionSpecParser<'_, 'def, _> =
                    VerboseFunctionSpecParser::new(&translated_arg_types, &translated_ret_type, |lit| {
                        ty_translator.translator.intern_literal(lit)
                    });

                parser
                    .parse_function_spec(v, &mut self.translated_fn)
                    .map_err(TranslationError::AttributeError)?;

                Ok(())
            },
            _ => Err(TranslationError::UnknownAttributeParser(parser)),
        }
    }

    // TODO refactor/ move
    fn to_universal_lft(
        &self,
        k: polonius_info::UniversalRegionKind,
        r: Region,
    ) -> Option<radium::UniversalLft> {
        match k {
            polonius_info::UniversalRegionKind::Function => Some(radium::UniversalLft::Function),
            polonius_info::UniversalRegionKind::Static => Some(radium::UniversalLft::Static),

            polonius_info::UniversalRegionKind::Local => self
                .ty_translator
                .scope
                .borrow()
                .lookup_universal_region(r)
                .map(radium::UniversalLft::Local),

            polonius_info::UniversalRegionKind::External => self
                .ty_translator
                .scope
                .borrow()
                .lookup_universal_region(r)
                .map(radium::UniversalLft::External),
        }
    }

    /// Translation that only generates a specification.
    pub fn generate_spec(self) -> radium::FunctionSpec<'def> {
        self.translated_fn.into()
    }

    /// 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 = 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;
            match *val {
                VarDebugInfoContents::Place(l) => {
                    // 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());
                            }
                        }
                    }
                },
                VarDebugInfoContents::Const(_) => {
                    // is this case used when constant propagation happens during MIR construction?
                },
            }
        }

        None
    }

    fn dump_body(body: &Body) {
        // TODO: print to file
        let basic_blocks = &body.basic_blocks;
        for (bb_idx, bb) in basic_blocks.iter_enumerated() {
            Self::dump_basic_block(bb_idx, bb);
        }
    }

    /// Dump a basic block as info debug output.
    fn dump_basic_block(bb_idx: BasicBlock, bb: &BasicBlockData) {
        info!("Basic block {:?}:", bb_idx);
        let mut i = 0;
        for s in &bb.statements {
            info!("{}\t{:?}", i, s);
            i += 1;
        }
        info!("{}\t{:?}", i, bb.terminator());
    }

    pub fn translate(mut self) -> Result<radium::Function<'def>, TranslationError> {
        let body = self.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(self.env.tcx(), body);
        checked_op_analyzer.analyze();
        let checked_op_locals = checked_op_analyzer.results();

        // map to translate between locals and the string names we use in radium::
        let mut radium_name_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_locals.get(&local) {
                *rewritten_ty
            } else {
                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 self.procedure_registry.lookup_function_mode(*id).map_or(false, ProcedureMode::is_ignore) {
                    // this is a spec fn
                    info!("skipping local which has specfn closure type: {:?}", local);
                    continue;
                }
            }

            // type:
            let tr_ty = self.ty_translator.translate_type(ty)?;
            let st = tr_ty.get_syn_type();

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

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

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

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

        let translator = BodyTranslator {
            env: self.env,
            proc: self.proc,
            info: self.info,