diff --git a/rr_frontend/translation/src/body/mod.rs b/rr_frontend/translation/src/body/mod.rs
index 91e53cf310e6a02851bcf6507dcbc94a5f9813e3..52c25f7db2d73b54f9593c7bc2ab4226044fc7e1 100644
--- a/rr_frontend/translation/src/body/mod.rs
+++ b/rr_frontend/translation/src/body/mod.rs
@@ -37,7 +37,7 @@ use crate::traits::{registry, resolution};
use crate::{base, consts, procedures, regions, search, traits, types};
pub mod signature;
-pub mod translator;
+mod translation;
/// Get the syntypes of function arguments for a procedure call.
pub fn get_arg_syntypes_for_procedure_call<'tcx, 'def>(
@@ -98,22 +98,6 @@ pub fn get_arg_syntypes_for_procedure_call<'tcx, 'def>(
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>,
-}
-
/// A scope of trait attributes mapping to Coq names to be used in a function's spec
struct TraitSpecNameScope {
attrs: HashMap<String, String>,
diff --git a/rr_frontend/translation/src/body/signature.rs b/rr_frontend/translation/src/body/signature.rs
index ea7e044fb6a2e97d61486c54a664c38caf6640de..a00d22a8b60416c38cb61d21b7bb2ee1770d62cc 100644
--- a/rr_frontend/translation/src/body/signature.rs
+++ b/rr_frontend/translation/src/body/signature.rs
@@ -26,7 +26,7 @@ use typed_arena::Arena;
use crate::base::*;
use crate::body::checked_op_analysis::CheckedOpLocalAnalysis;
-use crate::body::translator;
+use crate::body::translation;
use crate::environment::borrowck::facts;
use crate::environment::polonius_info::PoloniusInfo;
use crate::environment::procedure::Procedure;
@@ -532,7 +532,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
mut self,
spec_arena: &'def Arena<radium::FunctionSpec<'def, radium::InnerFunctionSpec<'def>>>,
) -> Result<radium::Function<'def>, TranslationError<'tcx>> {
- let translator = translator::TX::new(
+ let translator = translation::TX::new(
self.env,
self.procedure_registry,
self.const_registry,
diff --git a/rr_frontend/translation/src/body/translation/basicblock.rs b/rr_frontend/translation/src/body/translation/basicblock.rs
new file mode 100644
index 0000000000000000000000000000000000000000..927fcf2d08a5abe828ba0b4135e8a9bfccca16c1
--- /dev/null
+++ b/rr_frontend/translation/src/body/translation/basicblock.rs
@@ -0,0 +1,257 @@
+// © 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 super::TX;
+use crate::base::*;
+use crate::body::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::regions::inclusion_tracker::InclusionTracker;
+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};
+
+impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
+ /// Translate a single basic block.
+ pub(super) fn translate_basic_block(
+ &mut self,
+ bb_idx: BasicBlock,
+ bb: &BasicBlockData<'tcx>,
+ ) -> Result<radium::Stmt, TranslationError<'tcx>> {
+ // we translate from back to front, starting with the terminator, since Caesium statements
+ // have a continuation (the next statement to execute)
+
+ // first do the endlfts for the things right before the terminator
+ let mut idx = bb.statements.len();
+ let loc = Location {
+ block: bb_idx,
+ statement_index: idx,
+ };
+ let dying = self.info.get_dying_loans(loc);
+ // TODO zombie?
+ let _dying_zombie = self.info.get_dying_zombie_loans(loc);
+ let mut cont_stmt: radium::Stmt = self.translate_terminator(bb.terminator(), loc, dying)?;
+
+ //cont_stmt = self.prepend_endlfts(cont_stmt, loc, dying);
+ //cont_stmt = self.prepend_endlfts(cont_stmt, loc, dying_zombie);
+
+ for stmt in bb.statements.iter().rev() {
+ idx -= 1;
+ let loc = Location {
+ block: bb_idx,
+ statement_index: idx,
+ };
+
+ // get all dying loans, and emit endlfts for these.
+ // We loop over all predecessor locations, since some loans may end at the start of a
+ // basic block (in particular related to NLL stuff)
+ let pred = self.get_loc_predecessors(loc);
+ let mut dying_loans = HashSet::new();
+ for p in pred {
+ let dying_between = self.info.get_loans_dying_between(p, loc, false);
+ for l in &dying_between {
+ dying_loans.insert(*l);
+ }
+ // also include zombies
+ let dying_between = self.info.get_loans_dying_between(p, loc, true);
+ for l in &dying_between {
+ dying_loans.insert(*l);
+ }
+ }
+ // we prepend them before the current statement
+
+ match &stmt.kind {
+ StatementKind::Assign(b) => {
+ let (plc, val) = b.as_ref();
+
+ if (self.is_spec_closure_local(plc.local)?).is_some() {
+ info!("skipping assignment to spec closure local: {:?}", plc);
+ } else if let Some(rewritten_ty) = self.checked_op_temporaries.get(&plc.local) {
+ // if this is a checked op, be sure to remember it
+ info!("rewriting assignment to checked op: {:?}", plc);
+
+ let synty = self.ty_translator.translate_type_to_syn_type(*rewritten_ty)?;
+
+ let translated_val = self.translate_rvalue(loc, val)?;
+ let translated_place = self.translate_place(plc)?;
+
+ // this should be a temporary
+ assert!(plc.projection.is_empty());
+
+ let ot = synty.into();
+ cont_stmt = radium::Stmt::Assign {
+ ot,
+ e1: translated_place,
+ e2: translated_val,
+ s: Box::new(cont_stmt),
+ };
+ } else {
+ let plc_ty = self.get_type_of_place(plc);
+ let rhs_ty = val.ty(&self.proc.get_mir().local_decls, self.env.tcx());
+
+ let borrow_annots = regions::assignment::get_assignment_loan_annots(
+ &mut self.inclusion_tracker, &self.ty_translator,
+ loc, val);
+
+ let plc_ty = self.get_type_of_place(plc);
+ let plc_strongly_writeable = !self.check_place_below_reference(plc);
+ let (expr_annot, pre_stmt_annots, post_stmt_annots) =
+ regions::assignment::get_assignment_annots(
+ self.env, &mut self.inclusion_tracker, &self.ty_translator,
+ loc, plc_strongly_writeable, plc_ty, rhs_ty);
+
+ // TODO; maybe move this to rvalue
+ let composite_annots = regions::composite::get_composite_rvalue_creation_annots(
+ self.env, &mut self.inclusion_tracker, &self.ty_translator, loc, rhs_ty);
+
+ cont_stmt = radium::Stmt::with_annotations(
+ cont_stmt,
+ post_stmt_annots,
+ &Some("post-assignment".to_owned()),
+ );
+
+ let translated_val = radium::Expr::with_optional_annotation(
+ self.translate_rvalue(loc, val)?,
+ expr_annot,
+ Some("assignment".to_owned()),
+ );
+ let translated_place = self.translate_place(plc)?;
+ let synty = self.ty_translator.translate_type_to_syn_type(plc_ty.ty)?;
+ cont_stmt = radium::Stmt::Assign {
+ ot: synty.into(),
+ e1: translated_place,
+ e2: translated_val,
+ s: Box::new(cont_stmt),
+ };
+ cont_stmt = radium::Stmt::with_annotations(
+ cont_stmt,
+ pre_stmt_annots,
+ &Some("assignment".to_owned()),
+ );
+ cont_stmt = radium::Stmt::with_annotations(
+ cont_stmt,
+ borrow_annots,
+ &Some("borrow".to_owned()),
+ );
+ cont_stmt = radium::Stmt::with_annotations(
+ cont_stmt,
+ composite_annots,
+ &Some("composite".to_owned()),
+ );
+ }
+ },
+
+ StatementKind::Deinit(_) => {
+ // TODO: find out where this is emitted
+ return Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support Deinit".to_owned(),
+ });
+ },
+
+ StatementKind::FakeRead(b) => {
+ // we can probably ignore this, but I'm not sure
+ info!("Ignoring FakeRead: {:?}", b);
+ },
+
+ StatementKind::Intrinsic(intrinsic) => {
+ match intrinsic.as_ref() {
+ NonDivergingIntrinsic::Assume(_) => {
+ // ignore
+ info!("Ignoring Assume: {:?}", intrinsic);
+ },
+ NonDivergingIntrinsic::CopyNonOverlapping(_) => {
+ return Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support the CopyNonOverlapping Intrinsic".to_owned(),
+ });
+ },
+ }
+ },
+
+ StatementKind::PlaceMention(place) => {
+ // TODO: this is missed UB
+ info!("Ignoring PlaceMention: {:?}", place);
+ },
+
+ StatementKind::SetDiscriminant {
+ place: _place,
+ variant_index: _variant_index,
+ } => {
+ // TODO
+ return Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support SetDiscriminant".to_owned(),
+ });
+ },
+
+ // don't need that info
+ | StatementKind::AscribeUserType(_, _)
+ // don't need that
+ | StatementKind::Coverage(_)
+ // no-op
+ | StatementKind::ConstEvalCounter
+ // ignore
+ | StatementKind::Nop
+ // just ignore
+ | StatementKind::StorageLive(_)
+ // just ignore
+ | StatementKind::StorageDead(_)
+ // just ignore retags
+ | StatementKind::Retag(_, _) => (),
+ }
+
+ cont_stmt = self.prepend_endlfts(cont_stmt, dying_loans.into_iter());
+ }
+
+ Ok(cont_stmt)
+ }
+
+ /// Get predecessors in the CFG.
+ fn get_loc_predecessors(&self, loc: Location) -> Vec<Location> {
+ if loc.statement_index > 0 {
+ let pred = Location {
+ block: loc.block,
+ statement_index: loc.statement_index - 1,
+ };
+ vec![pred]
+ } else {
+ // check for gotos that go to this basic block
+ let pred_bbs = self.proc.predecessors(loc.block);
+ let basic_blocks = &self.proc.get_mir().basic_blocks;
+ pred_bbs
+ .iter()
+ .map(|bb| {
+ let data = &basic_blocks[*bb];
+ Location {
+ block: *bb,
+ statement_index: data.statements.len(),
+ }
+ })
+ .collect()
+ }
+ }
+}
diff --git a/rr_frontend/translation/src/body/translation/calls.rs b/rr_frontend/translation/src/body/translation/calls.rs
new file mode 100644
index 0000000000000000000000000000000000000000..3be93470555480ac58dc92392d2c5e212cef6b3a
--- /dev/null
+++ b/rr_frontend/translation/src/body/translation/calls.rs
@@ -0,0 +1,626 @@
+// © 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 super::TX;
+use crate::base::*;
+use crate::body::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::regions::inclusion_tracker::InclusionTracker;
+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.
+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(¶m_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)
+}
+
+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))
+ }
+
+ /// Resolve the trait requirements of a function call.
+ /// The target of the call, [did], should have been resolved as much as possible,
+ /// as the requirements of a call can be different depending on which impl we consider.
+ fn resolve_trait_requirements_of_call(
+ &self,
+ did: DefId,
+ params: ty::GenericArgsRef<'tcx>,
+ ) -> Result<Vec<radium::TraitReqInst<'def, Ty<'tcx>>>, TranslationError<'tcx>> {
+ let mut scope = self.ty_translator.scope.borrow_mut();
+ let mut state = types::STInner::InFunction(&mut scope);
+ self.trait_registry.resolve_trait_requirements_in_state(&mut state, did, params)
+ }
+
+ /// Translate the use of an `FnDef`, registering that the current function needs to link against
+ /// a particular monomorphization of the used function.
+ /// Is guaranteed to return a `radium::Expr::CallTarget` with the parameter instantiation of
+ /// this function annotated.
+ pub(super) fn translate_fn_def_use(
+ &mut self,
+ ty: Ty<'tcx>,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ let TyKind::FnDef(defid, params) = ty.kind() else {
+ return Err(TranslationError::UnknownError("not a FnDef type".to_owned()));
+ };
+
+ let current_param_env: ty::ParamEnv<'tcx> = self.env.tcx().param_env(self.proc.get_id());
+
+ // Check whether we are calling into a trait method.
+ // This works since we did not resolve concrete instances, so this is always an abstract
+ // reference to the trait.
+ let calling_trait = self.env.tcx().trait_of_item(*defid);
+
+ // Check whether we are calling a plain function or a trait method
+ let Some(calling_trait) = calling_trait else {
+ // resolve the trait requirements
+ let trait_spec_terms = self.resolve_trait_requirements_of_call(*defid, params)?;
+
+ // track that we are using this function and generate the Coq location name
+ let (code_param_name, ty_hint, lft_hint) =
+ self.register_use_procedure(*defid, vec![], params, trait_spec_terms)?;
+
+ let ty_hint = ty_hint.into_iter().map(|x| radium::RustType::of_type(&x)).collect();
+
+ return Ok(radium::Expr::CallTarget(code_param_name, ty_hint, lft_hint));
+ };
+
+ // Otherwise, we are calling a trait method
+ // Resolve the trait instance using trait selection
+ let Some((resolved_did, resolved_params, kind)) =
+ resolution::resolve_assoc_item(self.env.tcx(), current_param_env, *defid, params)
+ else {
+ return Err(TranslationError::TraitResolution(format!("Could not resolve trait {:?}", defid)));
+ };
+
+ info!(
+ "Resolved trait method {:?} as {:?} with substs {:?} and kind {:?}",
+ defid, resolved_did, resolved_params, kind
+ );
+
+ match kind {
+ resolution::TraitResolutionKind::UserDefined => {
+ // We can statically resolve the particular trait instance,
+ // but need to apply the spec to the instance's spec attributes
+
+ // resolve the trait requirements
+ let trait_spec_terms =
+ self.resolve_trait_requirements_of_call(resolved_did, resolved_params)?;
+
+ let (param_name, ty_hint, lft_hint) =
+ self.register_use_procedure(resolved_did, vec![], resolved_params, trait_spec_terms)?;
+ let ty_hint = ty_hint.into_iter().map(|x| radium::RustType::of_type(&x)).collect();
+
+ Ok(radium::Expr::CallTarget(param_name, ty_hint, lft_hint))
+ },
+
+ resolution::TraitResolutionKind::Param => {
+ // In this case, we have already applied it to the spec attribute
+
+ // resolve the trait requirements
+ let trait_spec_terms = self.resolve_trait_requirements_of_call(*defid, params)?;
+
+ let (param_name, ty_hint, lft_hint) =
+ self.register_use_trait_method(resolved_did, resolved_params, trait_spec_terms)?;
+ let ty_hint = ty_hint.into_iter().map(|x| radium::RustType::of_type(&x)).collect();
+
+ Ok(radium::Expr::CallTarget(param_name, ty_hint, lft_hint))
+ },
+
+ resolution::TraitResolutionKind::Closure => {
+ // TODO: here, we should first generate an instance of the trait
+ //let body = self.env.tcx().instance_mir(middle::ty::InstanceDef::Item(resolved_did));
+ //let body = self.env.tcx().instance_mir(middle::ty::InstanceDef::FnPtrShim(*defid, ty));
+ //info!("closure body: {:?}", body);
+
+ //FunctionTranslator::dump_body(body);
+
+ //let res_result = ty::Instance::resolve(self.env.tcx(), callee_param_env, *defid, params);
+ //info!("Resolution {:?}", res_result);
+
+ // the args are just the closure args. We can ignore them.
+ let _clos_args = resolved_params.as_closure();
+
+ // resolve the trait requirements
+ let trait_spec_terms = self.resolve_trait_requirements_of_call(*defid, params)?;
+
+ let (param_name, ty_hint, lft_hint) =
+ self.register_use_procedure(resolved_did, vec![], ty::List::empty(), trait_spec_terms)?;
+ let ty_hint = ty_hint.into_iter().map(|x| radium::RustType::of_type(&x)).collect();
+
+ Ok(radium::Expr::CallTarget(param_name, ty_hint, lft_hint))
+ },
+ }
+ }
+
+ /// 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(),
+ }),
+ }
+ }
+
+ pub(super) fn translate_function_call(
+ &mut self,
+ func: &Operand<'tcx>,
+ args: &[Operand<'tcx>],
+ destination: &Place<'tcx>,
+ target: Option<middle::mir::BasicBlock>,
+ loc: Location,
+ dying_loans: &[facts::Loan],
+ ) -> Result<radium::Stmt, TranslationError<'tcx>> {
+ let startpoint = self.info.interner.get_point_index(&facts::Point {
+ location: loc,
+ typ: facts::PointType::Start,
+ });
+
+ let Operand::Constant(box func_constant) = func else {
+ return Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support this kind of call operand (got: {:?})",
+ func
+ ),
+ });
+ };
+
+ // Get the type of the return value from the function
+ let (target_did, sig, generic_args, inst_sig) = self.call_expr_op_split_inst(func_constant)?;
+ info!("calling function {:?}", target_did);
+ info!("call substs: {:?} = {:?}, {:?}", func, sig, generic_args);
+
+ // for lifetime annotations:
+ // 1. get the regions involved here. for that, get the instantiation of the function.
+ // + if it's a FnDef type, that should be easy.
+ // + for a function pointer: ?
+ // + for a closure: ?
+ // (Polonius does not seem to distinguish early/late bound in any way, except
+ // that they are numbered in different passes)
+ // 2. find the constraints here involving the regions.
+ // 3. solve for the regions.
+ // + transitively propagate the constraints
+ // + check for equalities
+ // + otherwise compute intersection. singleton intersection just becomes an equality def.
+ // 4. add annotations accordingly
+ // + either a startlft
+ // + or a copy name
+ // 5. add shortenlft annotations to line up arguments.
+ // + for that, we need the type of the LHS, and what the argument types (with
+ // substituted regions) should be.
+ // 6. annotate the return value on assignment and establish constraints.
+
+ let classification =
+ regions::calls::compute_call_regions(self.env, &self.inclusion_tracker, generic_args, loc);
+
+ // update the inclusion tracker with the new regions we have introduced
+ // We just add the inclusions and ignore that we resolve it in a "tight" way.
+ // the cases where we need the reverse inclusion should be really rare.
+ for (r, c) in &classification.classification {
+ match c {
+ regions::calls::CallRegionKind::EqR(r2) => {
+ // put it at the start point, because the inclusions come into effect
+ // at the point right before.
+ self.inclusion_tracker.add_static_inclusion(*r, *r2, startpoint);
+ self.inclusion_tracker.add_static_inclusion(*r2, *r, startpoint);
+ },
+ regions::calls::CallRegionKind::Intersection(lfts) => {
+ // all the regions represented by lfts need to be included in r
+ for r2 in lfts {
+ self.inclusion_tracker.add_static_inclusion(*r2, *r, startpoint);
+ }
+ },
+ }
+ }
+
+ // translate the function expression.
+ let func_expr = self.translate_operand(func, false)?;
+ // We expect this to be an Expr::CallTarget, being annotated with the type parameters we
+ // instantiate it with.
+ let radium::Expr::CallTarget(func_lit, ty_param_annots, mut lft_param_annots) = func_expr else {
+ unreachable!("Logic error in call target translation");
+ };
+ let func_expr = radium::Expr::MetaParam(func_lit);
+
+ // translate the arguments
+ let mut translated_args = Vec::new();
+ for arg in args {
+ // to_ty is the type the function expects
+
+ //let ty = arg.ty(&self.proc.get_mir().local_decls, self.env.tcx());
+ let translated_arg = self.translate_operand(arg, true)?;
+ translated_args.push(translated_arg);
+ }
+
+ // We have to add the late regions, since we do not requantify over them.
+ for late in &classification.late_regions {
+ let lft = self.format_region(*late);
+ lft_param_annots.push(lft);
+ }
+ info!("Call lifetime instantiation (early): {:?}", classification.early_regions);
+ info!("Call lifetime instantiation (late): {:?}", classification.late_regions);
+
+ // TODO: do we need to do something with late bounds?
+ let output_ty = inst_sig.output().skip_binder();
+ info!("call has instantiated type {:?}", inst_sig);
+
+ // compute the resulting annotations
+ let lhs_ty = self.get_type_of_place(destination);
+ let lhs_strongly_writeable = !self.check_place_below_reference(destination);
+ let (rhs_annots, pre_stmt_annots, post_stmt_annots) = regions::assignment::get_assignment_annots(
+ self.env,
+ &mut self.inclusion_tracker,
+ &self.ty_translator,
+ loc,
+ lhs_strongly_writeable,
+ lhs_ty,
+ output_ty,
+ );
+ info!(
+ "assignment annots after call: expr: {:?}, pre-stmt: {:?}, post-stmt: {:?}",
+ rhs_annots, pre_stmt_annots, post_stmt_annots
+ );
+
+ // TODO: add annotations for the assignment
+ // for that:
+ // - get the type of the place
+ // - enforce constraints as necessary. this might spawn dyninclusions with some of the new regions =>
+ // In Coq, also the aliases should get proper endlft events to resolve the dyninclusions.
+ // - update the name map
+ let call_expr = radium::Expr::Call {
+ f: Box::new(func_expr),
+ lfts: lft_param_annots,
+ tys: ty_param_annots,
+ args: translated_args,
+ };
+ let stmt = match target {
+ Some(target) => {
+ let mut cont_stmt = self.translate_goto_like(&loc, target)?;
+ // end loans before the goto, but after the call.
+ // TODO: may cause duplications?
+ cont_stmt = self.prepend_endlfts(cont_stmt, dying_loans.iter().copied());
+
+ let cont_stmt = radium::Stmt::with_annotations(
+ cont_stmt,
+ post_stmt_annots,
+ &Some("post_function_call".to_owned()),
+ );
+
+ // assign stmt with call; then jump to bb
+ let place_ty = self.get_type_of_place(destination);
+ let place_st = self.ty_translator.translate_type_to_syn_type(place_ty.ty)?;
+ let place_expr = self.translate_place(destination)?;
+ let ot = place_st.into();
+
+ let annotated_rhs = radium::Expr::with_optional_annotation(
+ call_expr,
+ rhs_annots,
+ Some("function_call".to_owned()),
+ );
+ let assign_stmt = radium::Stmt::Assign {
+ ot,
+ e1: place_expr,
+ e2: annotated_rhs,
+ s: Box::new(cont_stmt),
+ };
+ radium::Stmt::with_annotations(
+ assign_stmt,
+ pre_stmt_annots,
+ &Some("function_call".to_owned()),
+ )
+ },
+ None => {
+ // expr stmt with call; then stuck (we have not provided a continuation, after all)
+ radium::Stmt::ExprS {
+ e: call_expr,
+ s: Box::new(radium::Stmt::Stuck),
+ }
+ },
+ };
+
+ let mut stmt_annots = Vec::new();
+
+ // add annotations to initialize the regions for the call (before the call)
+ for (r, class) in &classification.classification {
+ let lft = self.format_region(*r);
+ match class {
+ regions::calls::CallRegionKind::EqR(r2) => {
+ let lft2 = self.format_region(*r2);
+ stmt_annots.push(radium::Annotation::CopyLftName(lft2, lft));
+ },
+
+ regions::calls::CallRegionKind::Intersection(rs) => {
+ match rs.len() {
+ 0 => {
+ return Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support unconstrained lifetime"
+ .to_owned(),
+ });
+ },
+ 1 => {
+ // this is really just an equality constraint
+ if let Some(r2) = rs.iter().next() {
+ let lft2 = self.format_region(*r2);
+ stmt_annots.push(radium::Annotation::CopyLftName(lft2, lft));
+ }
+ },
+ _ => {
+ // a proper intersection
+ let lfts: Vec<_> = rs.iter().map(|r| self.format_region(*r)).collect();
+ stmt_annots.push(radium::Annotation::AliasLftIntersection(lft, lfts));
+ },
+ };
+ },
+ }
+ }
+
+ let stmt = radium::Stmt::with_annotations(stmt, stmt_annots, &Some("function_call".to_owned()));
+ Ok(stmt)
+ }
+}
diff --git a/rr_frontend/translation/src/body/translation/constants.rs b/rr_frontend/translation/src/body/translation/constants.rs
new file mode 100644
index 0000000000000000000000000000000000000000..34e616362265b033316feb4833d01814bcce08df
--- /dev/null
+++ b/rr_frontend/translation/src/body/translation/constants.rs
@@ -0,0 +1,211 @@
+// © 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 super::TX;
+use crate::base::*;
+use crate::body::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::regions::inclusion_tracker::InclusionTracker;
+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};
+
+impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
+ /// Translate a scalar at a specific type to a `radium::Expr`.
+ // TODO: Use `TryFrom` instead
+ fn translate_scalar(
+ &mut self,
+ sc: &Scalar,
+ ty: Ty<'tcx>,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ // TODO: Use `TryFrom` instead
+ fn translate_literal<'tcx, T, U>(
+ sc: Result<T, U>,
+ fptr: fn(T) -> radium::Literal,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ sc.map_or(Err(TranslationError::InvalidLayout), |lit| Ok(radium::Expr::Literal(fptr(lit))))
+ }
+
+ match ty.kind() {
+ TyKind::Bool => translate_literal(sc.to_bool(), radium::Literal::Bool),
+
+ TyKind::Int(it) => match it {
+ ty::IntTy::I8 => translate_literal(sc.to_i8(), radium::Literal::I8),
+ ty::IntTy::I16 => translate_literal(sc.to_i16(), radium::Literal::I16),
+ ty::IntTy::I32 => translate_literal(sc.to_i32(), radium::Literal::I32),
+ ty::IntTy::I128 => translate_literal(sc.to_i128(), radium::Literal::I128),
+
+ // For Radium, the pointer size is 8 bytes
+ ty::IntTy::I64 | ty::IntTy::Isize => translate_literal(sc.to_i64(), radium::Literal::I64),
+ },
+
+ TyKind::Uint(it) => match it {
+ ty::UintTy::U8 => translate_literal(sc.to_u8(), radium::Literal::U8),
+ ty::UintTy::U16 => translate_literal(sc.to_u16(), radium::Literal::U16),
+ ty::UintTy::U32 => translate_literal(sc.to_u32(), radium::Literal::U32),
+ ty::UintTy::U128 => translate_literal(sc.to_u128(), radium::Literal::U128),
+
+ // For Radium, the pointer is 8 bytes
+ ty::UintTy::U64 | ty::UintTy::Usize => translate_literal(sc.to_u64(), radium::Literal::U64),
+ },
+
+ TyKind::Char => translate_literal(sc.to_char(), radium::Literal::Char),
+
+ TyKind::FnDef(_, _) => self.translate_fn_def_use(ty),
+
+ TyKind::Tuple(tys) => {
+ if tys.is_empty() {
+ return Ok(radium::Expr::Literal(radium::Literal::ZST));
+ }
+
+ Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support compound construction of tuples using literals (got: {:?})",
+ ty
+ ),
+ })
+ },
+
+ TyKind::Ref(_, _, _) => match sc {
+ Scalar::Int(_) => unreachable!(),
+
+ Scalar::Ptr(pointer, _) => {
+ let glob_alloc = self.env.tcx().global_alloc(pointer.provenance);
+ match glob_alloc {
+ middle::mir::interpret::GlobalAlloc::Static(did) => {
+ info!(
+ "Found static GlobalAlloc {:?} for Ref scalar {:?} at type {:?}",
+ did, sc, ty
+ );
+
+ let s = self.const_registry.get_static(did)?;
+ self.collected_statics.insert(did);
+ Ok(radium::Expr::Literal(radium::Literal::Loc(s.loc_name.clone())))
+ },
+ middle::mir::interpret::GlobalAlloc::Memory(alloc) => {
+ // TODO: this is needed
+ Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support GlobalAlloc {:?} for scalar {:?} at type {:?}",
+ glob_alloc, sc, ty
+ ),
+ })
+ },
+ _ => Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support GlobalAlloc {:?} for scalar {:?} at type {:?}",
+ glob_alloc, sc, ty
+ ),
+ }),
+ }
+ },
+ },
+
+ _ => Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support layout for const value: (got: {:?})",
+ ty
+ ),
+ }),
+ }
+ }
+
+ /// Translate a constant value from const evaluation.
+ fn translate_constant_value(
+ &mut self,
+ v: mir::interpret::ConstValue<'tcx>,
+ ty: Ty<'tcx>,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ match v {
+ ConstValue::Scalar(sc) => self.translate_scalar(&sc, ty),
+ ConstValue::ZeroSized => {
+ // TODO are there more special cases we need to handle somehow?
+ match ty.kind() {
+ TyKind::FnDef(_, _) => {
+ info!("Translating ZST val for function call target: {:?}", ty);
+ self.translate_fn_def_use(ty)
+ },
+ _ => Ok(radium::Expr::Literal(radium::Literal::ZST)),
+ }
+ },
+ _ => {
+ // TODO: do we actually care about this case or is this just something that can
+ // appear as part of CTFE/MIRI?
+ Err(TranslationError::UnsupportedFeature {
+ description: format!("Unsupported Constant: ConstValue; {:?}", v),
+ })
+ },
+ }
+ }
+
+ /// Translate a Constant to a `radium::Expr`.
+ pub(super) fn translate_constant(
+ &mut self,
+ constant: &Constant<'tcx>,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ match constant.literal {
+ ConstantKind::Ty(v) => {
+ let const_ty = v.ty();
+
+ match v.kind() {
+ ConstKind::Value(v) => {
+ // this doesn't contain the necessary structure anymore. Need to reconstruct using the
+ // type.
+ match v.try_to_scalar() {
+ Some(sc) => self.translate_scalar(&sc, const_ty),
+ _ => Err(TranslationError::UnsupportedFeature {
+ description: format!("const value not supported: {:?}", v),
+ }),
+ }
+ },
+ _ => Err(TranslationError::UnsupportedFeature {
+ description: "Unsupported ConstKind".to_owned(),
+ }),
+ }
+ },
+ ConstantKind::Val(val, ty) => self.translate_constant_value(val, ty),
+ ConstantKind::Unevaluated(c, ty) => {
+ // call const evaluation
+ let param_env: ty::ParamEnv<'tcx> = self.env.tcx().param_env(self.proc.get_id());
+ match self.env.tcx().const_eval_resolve(param_env, c, None) {
+ Ok(res) => self.translate_constant_value(res, ty),
+ Err(e) => match e {
+ ErrorHandled::Reported(_) => Err(TranslationError::UnsupportedFeature {
+ description: "Cannot interpret constant".to_owned(),
+ }),
+ ErrorHandled::TooGeneric => Err(TranslationError::UnsupportedFeature {
+ description: "Const use is too generic".to_owned(),
+ }),
+ },
+ }
+ },
+ }
+ }
+}
diff --git a/rr_frontend/translation/src/body/translation/loops.rs b/rr_frontend/translation/src/body/translation/loops.rs
new file mode 100644
index 0000000000000000000000000000000000000000..6f8ef41f6d78cc3fb695c0ad3c94b1308dbc640c
--- /dev/null
+++ b/rr_frontend/translation/src/body/translation/loops.rs
@@ -0,0 +1,137 @@
+// © 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 super::TX;
+use crate::base::*;
+use crate::body::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::regions::inclusion_tracker::InclusionTracker;
+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};
+
+impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
+ /// Parse the attributes on spec closure `did` as loop annotations and add it as an invariant
+ /// to the generated code.
+ pub(super) 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,
+ }
+ }
+
+ /// Find the optional `DefId` of the closure giving the invariant for the loop with head `head_bb`.
+ pub(super) 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)
+ }
+}
diff --git a/rr_frontend/translation/src/body/translation/mod.rs b/rr_frontend/translation/src/body/translation/mod.rs
new file mode 100644
index 0000000000000000000000000000000000000000..5c3f407e2e31f247b403eb610f5287b014cb4b77
--- /dev/null
+++ b/rr_frontend/translation/src/body/translation/mod.rs
@@ -0,0 +1,498 @@
+// © 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/.
+
+mod basicblock;
+mod calls;
+mod constants;
+mod loops;
+mod place;
+mod rvalue;
+mod terminator;
+
+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::base::*;
+use crate::body::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::regions::inclusion_tracker::InclusionTracker;
+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};
+
+/// 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 = regions::init::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(),
+ })
+ }
+
+ /// 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> {
+ /// 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
+ }
+
+ fn format_region(&self, r: facts::Region) -> String {
+ let lft = self.info.mk_atomic_region(r);
+ self.ty_translator.format_atomic_region(&lft)
+ }
+
+ /// 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
+ }
+
+ /// 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);
+ }
+
+ /// 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)
+ }
+
+ /// 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);
+ }
+ }
+
+ /// Prepend endlft annotations for dying loans to a statement.
+ fn prepend_endlfts<I>(&self, st: radium::Stmt, dying: I) -> radium::Stmt
+ where
+ I: ExactSizeIterator<Item = facts::Loan>,
+ {
+ let mut cont_stmt = st;
+ if dying.len() > 0 {
+ //info!("Dying at {:?}: {:?}", loc, dying);
+ for d in dying {
+ let lft = self.info.atomic_region_of_loan(d);
+ cont_stmt = radium::Stmt::Annot {
+ a: radium::Annotation::EndLft(self.ty_translator.format_atomic_region(&lft)),
+ s: Box::new(cont_stmt),
+ why: Some("endlft".to_owned()),
+ };
+ }
+ }
+ cont_stmt
+ }
+
+ /// Make a trivial place accessing `local`.
+ fn make_local_place(&self, local: Local) -> Place<'tcx> {
+ Place {
+ local,
+ projection: self.env.tcx().mk_place_elems(&[]),
+ }
+ }
+
+ /// Get the type of a local in a body.
+ fn get_type_of_local(&self, local: Local) -> Result<Ty<'tcx>, TranslationError<'tcx>> {
+ self.proc
+ .get_mir()
+ .local_decls
+ .get(local)
+ .map(|decl| decl.ty)
+ .ok_or_else(|| TranslationError::UnknownVar(String::new()))
+ }
+
+ /// Get the type of a place expression.
+ fn get_type_of_place(&self, pl: &Place<'tcx>) -> PlaceTy<'tcx> {
+ pl.ty(&self.proc.get_mir().local_decls, self.env.tcx())
+ }
+
+ /// Get the type of a const.
+ fn get_type_of_const(cst: &Constant<'tcx>) -> Ty<'tcx> {
+ match cst.literal {
+ ConstantKind::Ty(cst) => cst.ty(),
+ ConstantKind::Val(_, ty) | ConstantKind::Unevaluated(_, ty) => ty,
+ }
+ }
+
+ /// Get the type of an operand.
+ fn get_type_of_operand(&self, op: &Operand<'tcx>) -> Ty<'tcx> {
+ op.ty(&self.proc.get_mir().local_decls, self.env.tcx())
+ }
+
+ /// Check if a local is used for a spec closure.
+ fn is_spec_closure_local(&self, l: Local) -> Result<Option<DefId>, TranslationError<'tcx>> {
+ // check if we should ignore this
+ let local_type = self.get_type_of_local(l)?;
+
+ let TyKind::Closure(did, _) = local_type.kind() else {
+ return Ok(None);
+ };
+
+ Ok(self
+ .procedure_registry
+ .lookup_function_mode(*did)
+ .and_then(|m| m.is_ignore().then_some(*did)))
+ }
+}
diff --git a/rr_frontend/translation/src/body/translation/place.rs b/rr_frontend/translation/src/body/translation/place.rs
new file mode 100644
index 0000000000000000000000000000000000000000..e25574446872ee6f7d0b44466ff6222d284af1ff
--- /dev/null
+++ b/rr_frontend/translation/src/body/translation/place.rs
@@ -0,0 +1,139 @@
+// © 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 super::TX;
+use crate::base::*;
+use crate::body::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::regions::inclusion_tracker::InclusionTracker;
+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};
+
+impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
+ /// Translate a place to a Caesium lvalue.
+ pub(super) fn translate_place(
+ &mut self,
+ pl: &Place<'tcx>,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ // Get the type of the underlying local. We will use this to
+ // get the necessary layout information for dereferencing
+ let mut cur_ty = self.get_type_of_local(pl.local).map(PlaceTy::from_ty)?;
+
+ let local_name = self
+ .variable_map
+ .get(&pl.local)
+ .ok_or_else(|| TranslationError::UnknownVar(format!("{:?}", pl.local)))?;
+
+ let mut acc_expr = radium::Expr::Var(local_name.to_string());
+
+ // iterate in evaluation order
+ for it in pl.projection {
+ match &it {
+ ProjectionElem::Deref => {
+ // use the type of the dereferencee
+ let st = self.ty_translator.translate_type_to_syn_type(cur_ty.ty)?;
+ acc_expr = radium::Expr::Deref {
+ ot: st.into(),
+ e: Box::new(acc_expr),
+ };
+ },
+ ProjectionElem::Field(f, _) => {
+ // `t` is the type of the field we are accessing!
+ let lit = self.ty_translator.generate_structlike_use(cur_ty.ty, cur_ty.variant_index)?;
+ // TODO: does not do the right thing for accesses to fields of zero-sized objects.
+ let struct_sls = lit.map_or(radium::SynType::Unit, |x| x.generate_raw_syn_type_term());
+ let name = self.ty_translator.translator.get_field_name_of(
+ *f,
+ cur_ty.ty,
+ cur_ty.variant_index.map(abi::VariantIdx::as_usize),
+ )?;
+
+ acc_expr = radium::Expr::FieldOf {
+ e: Box::new(acc_expr),
+ name,
+ sls: struct_sls.to_string(),
+ };
+ },
+ ProjectionElem::Index(_v) => {
+ //TODO
+ return Err(TranslationError::UnsupportedFeature {
+ description: "places: implement index access".to_owned(),
+ });
+ },
+ ProjectionElem::ConstantIndex { .. } => {
+ //TODO
+ return Err(TranslationError::UnsupportedFeature {
+ description: "places: implement const index access".to_owned(),
+ });
+ },
+ ProjectionElem::Subslice { .. } => {
+ return Err(TranslationError::UnsupportedFeature {
+ description: "places: implement subslicing".to_owned(),
+ });
+ },
+ ProjectionElem::Downcast(_, variant_idx) => {
+ info!("Downcast of ty {:?} to {:?}", cur_ty, variant_idx);
+ if let ty::TyKind::Adt(def, args) = cur_ty.ty.kind() {
+ if def.is_enum() {
+ let enum_use = self.ty_translator.generate_enum_use(*def, args.iter())?;
+ let els = enum_use.generate_raw_syn_type_term();
+
+ let variant_name = types::TX::get_variant_name_of(cur_ty.ty, *variant_idx)?;
+
+ acc_expr = radium::Expr::EnumData {
+ els: els.to_string(),
+ variant: variant_name,
+ e: Box::new(acc_expr),
+ }
+ } else {
+ return Err(TranslationError::UnknownError(
+ "places: ADT downcasting on non-enum type".to_owned(),
+ ));
+ }
+ } else {
+ return Err(TranslationError::UnknownError(
+ "places: ADT downcasting on non-enum type".to_owned(),
+ ));
+ }
+ },
+ ProjectionElem::OpaqueCast(_) => {
+ return Err(TranslationError::UnsupportedFeature {
+ description: "places: implement opaque casts".to_owned(),
+ });
+ },
+ };
+ // update cur_ty
+ cur_ty = cur_ty.projection_ty(self.env.tcx(), it);
+ }
+ info!("translating place {:?} to {:?}", pl, acc_expr);
+ Ok(acc_expr)
+ }
+}
diff --git a/rr_frontend/translation/src/body/translation/rvalue.rs b/rr_frontend/translation/src/body/translation/rvalue.rs
new file mode 100644
index 0000000000000000000000000000000000000000..426d3c021455f5ac5c86f1c404016c9c4b6b2cdc
--- /dev/null
+++ b/rr_frontend/translation/src/body/translation/rvalue.rs
@@ -0,0 +1,638 @@
+// © 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::index::IndexVec;
+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 super::TX;
+use crate::base::*;
+use crate::body::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::regions::inclusion_tracker::InclusionTracker;
+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};
+
+impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
+ /// Translate an aggregate expression.
+ fn translate_aggregate(
+ &mut self,
+ loc: Location,
+ kind: &mir::AggregateKind<'tcx>,
+ op: &IndexVec<abi::FieldIdx, mir::Operand<'tcx>>,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ // translate operands
+ let mut translated_ops: Vec<radium::Expr> = Vec::new();
+ let mut operand_types: Vec<Ty<'tcx>> = Vec::new();
+
+ for o in op {
+ let translated_o = self.translate_operand(o, true)?;
+ let type_of_o = self.get_type_of_operand(o);
+ translated_ops.push(translated_o);
+ operand_types.push(type_of_o);
+ }
+
+ match *kind {
+ mir::AggregateKind::Tuple => {
+ if operand_types.is_empty() {
+ // translate to unit literal
+ return Ok(radium::Expr::Literal(radium::Literal::ZST));
+ }
+
+ let struct_use = self.ty_translator.generate_tuple_use(operand_types.iter().copied())?;
+ let sl = struct_use.generate_raw_syn_type_term();
+ let initializers: Vec<_> =
+ translated_ops.into_iter().enumerate().map(|(i, o)| (i.to_string(), o)).collect();
+
+ Ok(radium::Expr::StructInitE {
+ sls: coq::term::App::new_lhs(sl.to_string()),
+ components: initializers,
+ })
+ },
+
+ mir::AggregateKind::Adt(did, variant, args, ..) => {
+ // get the adt def
+ let adt_def: ty::AdtDef<'tcx> = self.env.tcx().adt_def(did);
+
+ if adt_def.is_struct() {
+ let variant = adt_def.variant(variant);
+ let struct_use = self.ty_translator.generate_struct_use(variant.def_id, args)?;
+
+ let Some(struct_use) = struct_use else {
+ // if not, it's replaced by unit
+ return Ok(radium::Expr::Literal(radium::Literal::ZST));
+ };
+
+ let sl = struct_use.generate_raw_syn_type_term();
+ let initializers: Vec<_> = translated_ops
+ .into_iter()
+ .zip(variant.fields.iter())
+ .map(|(o, field)| (field.name.to_string(), o))
+ .collect();
+
+ return Ok(radium::Expr::StructInitE {
+ sls: coq::term::App::new_lhs(sl.to_string()),
+ components: initializers,
+ });
+ }
+
+ if adt_def.is_enum() {
+ let variant_def = adt_def.variant(variant);
+
+ let struct_use =
+ self.ty_translator.generate_enum_variant_use(variant_def.def_id, args)?;
+ let sl = struct_use.generate_raw_syn_type_term();
+
+ let initializers: Vec<_> = translated_ops
+ .into_iter()
+ .zip(variant_def.fields.iter())
+ .map(|(o, field)| (field.name.to_string(), o))
+ .collect();
+
+ let variant_e = radium::Expr::StructInitE {
+ sls: coq::term::App::new_lhs(sl.to_string()),
+ components: initializers,
+ };
+
+ let enum_use = self.ty_translator.generate_enum_use(adt_def, args)?;
+ let els = enum_use.generate_raw_syn_type_term();
+
+ info!("generating enum annotation for type {:?}", enum_use);
+ let ty = radium::RustType::of_type(&radium::Type::Literal(enum_use));
+ let variant_name = variant_def.name.to_string();
+
+ return Ok(radium::Expr::EnumInitE {
+ els: coq::term::App::new_lhs(els.to_string()),
+ variant: variant_name,
+ ty,
+ initializer: Box::new(variant_e),
+ });
+ }
+
+ // TODO
+ Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support aggregate rvalue for other ADTs (got: {kind:?}, {op:?})"
+ ),
+ })
+ },
+ mir::AggregateKind::Closure(def, _args) => {
+ trace!("Translating Closure aggregate value for {:?}", def);
+
+ // We basically translate this to a tuple
+ if operand_types.is_empty() {
+ // translate to unit literal
+ return Ok(radium::Expr::Literal(radium::Literal::ZST));
+ }
+
+ let struct_use = self.ty_translator.generate_tuple_use(operand_types.iter().copied())?;
+ let sl = struct_use.generate_raw_syn_type_term();
+
+ let initializers: Vec<_> =
+ translated_ops.into_iter().enumerate().map(|(i, o)| (i.to_string(), o)).collect();
+
+ Ok(radium::Expr::StructInitE {
+ sls: coq::term::App::new_lhs(sl.to_string()),
+ components: initializers,
+ })
+ },
+
+ _ => {
+ // TODO
+ Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support this kind of aggregate rvalue (got: {kind:?}, {op:?})"
+ ),
+ })
+ },
+ }
+ }
+
+ fn translate_cast(
+ &mut self,
+ kind: mir::CastKind,
+ op: &mir::Operand<'tcx>,
+ to_ty: ty::Ty<'tcx>,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ let op_ty = self.get_type_of_operand(op);
+ let op_st = self.ty_translator.translate_type_to_syn_type(op_ty)?;
+ let op_ot = op_st.into();
+
+ let translated_op = self.translate_operand(op, true)?;
+
+ let target_st = self.ty_translator.translate_type_to_syn_type(to_ty)?;
+ let target_ot = target_st.into();
+
+ match kind {
+ mir::CastKind::PointerCoercion(x) => {
+ match x {
+ ty::adjustment::PointerCoercion::MutToConstPointer => {
+ // this is a NOP in our model
+ Ok(translated_op)
+ },
+
+ ty::adjustment::PointerCoercion::ArrayToPointer
+ | ty::adjustment::PointerCoercion::ClosureFnPointer(_)
+ | ty::adjustment::PointerCoercion::ReifyFnPointer
+ | ty::adjustment::PointerCoercion::UnsafeFnPointer
+ | ty::adjustment::PointerCoercion::Unsize => Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support this kind of pointer coercion (got: {kind:?})"
+ ),
+ }),
+ }
+ },
+
+ mir::CastKind::DynStar => Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support dyn* cast".to_owned(),
+ }),
+
+ mir::CastKind::IntToInt => {
+ // Cast integer to integer
+ Ok(radium::Expr::UnOp {
+ o: radium::Unop::Cast(target_ot),
+ ot: op_ot,
+ e: Box::new(translated_op),
+ })
+ },
+
+ mir::CastKind::IntToFloat => Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support int-to-float cast".to_owned(),
+ }),
+
+ mir::CastKind::FloatToInt => Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support float-to-int cast".to_owned(),
+ }),
+
+ mir::CastKind::FloatToFloat => Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support float-to-float cast".to_owned(),
+ }),
+
+ mir::CastKind::PtrToPtr => {
+ match (op_ty.kind(), to_ty.kind()) {
+ (TyKind::RawPtr(_), TyKind::RawPtr(_)) => {
+ // Casts between raw pointers are NOPs for us
+ Ok(translated_op)
+ },
+
+ _ => {
+ // TODO: any other cases we should handle?
+ Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support ptr-to-ptr cast (got: {kind:?}, {op:?}, {to_ty:?})"
+ ),
+ })
+ },
+ }
+ },
+
+ mir::CastKind::FnPtrToPtr => Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support fnptr-to-ptr cast (got: {kind:?}, {op:?}, {to_ty:?})"
+ ),
+ }),
+
+ mir::CastKind::Transmute => Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support transmute cast (got: {kind:?}, {op:?}, {to_ty:?})"
+ ),
+ }),
+
+ mir::CastKind::PointerExposeAddress => {
+ // Cast pointer to integer
+ Ok(radium::Expr::UnOp {
+ o: radium::Unop::Cast(target_ot),
+ ot: radium::OpType::Ptr,
+ e: Box::new(translated_op),
+ })
+ },
+
+ mir::CastKind::PointerFromExposedAddress => Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support this kind of cast (got: {kind:?}, {op:?}, {to_ty:?})"
+ ),
+ }),
+ }
+ }
+
+ /// Translate an operand.
+ /// This will either generate an lvalue (in case of Move or Copy) or an rvalue (in most cases
+ /// of Constant). How this is used depends on the context. (e.g., Use of an integer constant
+ /// does not typecheck, and produces a stuck program).
+ pub(super) fn translate_operand(
+ &mut self,
+ op: &Operand<'tcx>,
+ to_rvalue: bool,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ match op {
+ // In Caesium: typed_place needs deref (not use) for place accesses.
+ // use is used top-level to convert an lvalue to an rvalue, which is why we use it here.
+ Operand::Copy(place) | Operand::Move(place) => {
+ // check if this goes to a temporary of a checked op
+ let place_kind = if self.checked_op_temporaries.contains_key(&place.local) {
+ assert!(place.projection.len() == 1);
+
+ let ProjectionElem::Field(f, _0) = place.projection[0] else {
+ unreachable!("invariant violation for access to checked op temporary");
+ };
+
+ if f.index() != 0 {
+ // make this a constant false -- our semantics directly checks for overflows
+ // and otherwise throws UB.
+ return Ok(radium::Expr::Literal(radium::Literal::Bool(false)));
+ }
+
+ // access to the result of the op
+ self.make_local_place(place.local)
+ } else {
+ *place
+ };
+
+ let translated_place = self.translate_place(&place_kind)?;
+ let ty = self.get_type_of_place(place);
+
+ let st = self.ty_translator.translate_type_to_syn_type(ty.ty)?;
+
+ if to_rvalue {
+ Ok(radium::Expr::Use {
+ ot: st.into(),
+ e: Box::new(translated_place),
+ })
+ } else {
+ Ok(translated_place)
+ }
+ },
+ Operand::Constant(constant) => {
+ // TODO: possibly need different handling of the rvalue flag
+ // when this also handles string literals etc.
+ return self.translate_constant(constant.as_ref());
+ },
+ }
+ }
+
+ /// Translates an Rvalue.
+ pub(super) fn translate_rvalue(
+ &mut self,
+ loc: Location,
+ rval: &Rvalue<'tcx>,
+ ) -> Result<radium::Expr, TranslationError<'tcx>> {
+ match rval {
+ Rvalue::Use(op) => {
+ // converts an lvalue to an rvalue
+ self.translate_operand(op, true)
+ },
+
+ Rvalue::Ref(region, bk, pl) => {
+ let translated_pl = self.translate_place(pl)?;
+ let translated_bk = TX::translate_borrow_kind(*bk)?;
+ let ty_annot = self.get_type_annotation_for_borrow(*bk, pl)?;
+
+ if let Some(loan) = self.info.get_optional_loan_at_location(loc) {
+ let atomic_region = self.info.atomic_region_of_loan(loan);
+ let lft = self.ty_translator.format_atomic_region(&atomic_region);
+ Ok(radium::Expr::Borrow {
+ lft,
+ bk: translated_bk,
+ ty: ty_annot,
+ e: Box::new(translated_pl),
+ })
+ } else {
+ info!("Didn't find loan at {:?}: {:?}; region {:?}", loc, rval, region);
+ let region = regions::region_to_region_vid(*region);
+ let lft = self.format_region(region);
+
+ Ok(radium::Expr::Borrow {
+ lft,
+ bk: translated_bk,
+ ty: ty_annot,
+ e: Box::new(translated_pl),
+ })
+ }
+ },
+
+ Rvalue::AddressOf(mt, pl) => {
+ let translated_pl = self.translate_place(pl)?;
+ let translated_mt = TX::translate_mutability(*mt);
+
+ Ok(radium::Expr::AddressOf {
+ mt: translated_mt,
+ e: Box::new(translated_pl),
+ })
+ },
+
+ Rvalue::BinaryOp(op, operands) => {
+ let e1 = &operands.as_ref().0;
+ let e2 = &operands.as_ref().1;
+
+ let e1_ty = self.get_type_of_operand(e1);
+ let e2_ty = self.get_type_of_operand(e2);
+ let e1_st = self.ty_translator.translate_type_to_syn_type(e1_ty)?;
+ let e2_st = self.ty_translator.translate_type_to_syn_type(e2_ty)?;
+
+ let translated_e1 = self.translate_operand(e1, true)?;
+ let translated_e2 = self.translate_operand(e2, true)?;
+ let translated_op = self.translate_binop(*op, &operands.as_ref().0, &operands.as_ref().1)?;
+
+ Ok(radium::Expr::BinOp {
+ o: translated_op,
+ ot1: e1_st.into(),
+ ot2: e2_st.into(),
+ e1: Box::new(translated_e1),
+ e2: Box::new(translated_e2),
+ })
+ },
+
+ Rvalue::CheckedBinaryOp(op, operands) => {
+ let e1 = &operands.as_ref().0;
+ let e2 = &operands.as_ref().1;
+
+ let e1_ty = self.get_type_of_operand(e1);
+ let e2_ty = self.get_type_of_operand(e2);
+ let e1_st = self.ty_translator.translate_type_to_syn_type(e1_ty)?;
+ let e2_st = self.ty_translator.translate_type_to_syn_type(e2_ty)?;
+
+ let translated_e1 = self.translate_operand(e1, true)?;
+ let translated_e2 = self.translate_operand(e2, true)?;
+ let translated_op = TX::translate_checked_binop(*op)?;
+
+ Ok(radium::Expr::BinOp {
+ o: translated_op,
+ ot1: e1_st.into(),
+ ot2: e2_st.into(),
+ e1: Box::new(translated_e1),
+ e2: Box::new(translated_e2),
+ })
+ },
+
+ Rvalue::UnaryOp(op, operand) => {
+ let translated_e1 = self.translate_operand(operand, true)?;
+ let e1_ty = self.get_type_of_operand(operand);
+ let e1_st = self.ty_translator.translate_type_to_syn_type(e1_ty)?;
+ let translated_op = TX::translate_unop(*op, e1_ty)?;
+
+ Ok(radium::Expr::UnOp {
+ o: translated_op,
+ ot: e1_st.into(),
+ e: Box::new(translated_e1),
+ })
+ },
+
+ Rvalue::NullaryOp(op, _ty) => {
+ // TODO: SizeOf
+ Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support nullary ops (AlignOf, Sizeof)"
+ .to_owned(),
+ })
+ },
+
+ Rvalue::Discriminant(pl) => {
+ let ty = self.get_type_of_place(pl);
+ let translated_pl = self.translate_place(pl)?;
+ info!("getting discriminant of {:?} at type {:?}", pl, ty);
+
+ let ty::TyKind::Adt(adt_def, args) = ty.ty.kind() else {
+ return Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support discriminant accesses on non-enum types ({:?}, got {:?})",
+ rval, ty.ty
+ ),
+ });
+ };
+
+ let enum_use = self.ty_translator.generate_enum_use(*adt_def, args.iter())?;
+ let els = enum_use.generate_raw_syn_type_term();
+
+ let discriminant_acc = radium::Expr::EnumDiscriminant {
+ els: els.to_string(),
+ e: Box::new(translated_pl),
+ };
+
+ // need to do a load from this place
+ let it = ty.ty.discriminant_ty(self.env.tcx());
+ let translated_it = self.ty_translator.translate_type(it)?;
+
+ let radium::Type::Int(translated_it) = translated_it else {
+ return Err(TranslationError::UnknownError(format!(
+ "type of discriminant is not an integer type {:?}",
+ it
+ )));
+ };
+
+ let ot = radium::OpType::Int(translated_it);
+
+ Ok(radium::Expr::Use {
+ ot,
+ e: Box::new(discriminant_acc),
+ })
+ },
+
+ Rvalue::Aggregate(kind, op) => self.translate_aggregate(loc, kind.as_ref(), op),
+
+ Rvalue::Cast(kind, op, to_ty) => self.translate_cast(*kind, op, *to_ty),
+
+ Rvalue::CopyForDeref(_)
+ | Rvalue::Len(..)
+ | Rvalue::Repeat(..)
+ | Rvalue::ThreadLocalRef(..)
+ | Rvalue::ShallowInitBox(_, _) => Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support this kind of rvalue (got: {:?})",
+ rval
+ ),
+ }),
+ }
+ }
+
+ /// Get the type to annotate a borrow with.
+ fn get_type_annotation_for_borrow(
+ &self,
+ bk: BorrowKind,
+ pl: &Place<'tcx>,
+ ) -> Result<Option<radium::RustType>, TranslationError<'tcx>> {
+ let BorrowKind::Mut { .. } = bk else {
+ return Ok(None);
+ };
+
+ let ty = self.get_type_of_place(pl);
+
+ // For borrows, we can safely ignore the downcast type -- we cannot borrow a particularly variant
+ let translated_ty = self.ty_translator.translate_type(ty.ty)?;
+ let annot_ty = radium::RustType::of_type(&translated_ty);
+
+ Ok(Some(annot_ty))
+ }
+
+ /// Translate binary operators.
+ /// We need access to the operands, too, to handle the offset operator and get the right
+ /// Caesium layout annotation.
+ fn translate_binop(
+ &self,
+ op: BinOp,
+ e1: &Operand<'tcx>,
+ _e2: &Operand<'tcx>,
+ ) -> Result<radium::Binop, TranslationError<'tcx>> {
+ match op {
+ BinOp::Add | BinOp::AddUnchecked => Ok(radium::Binop::Add),
+ BinOp::Sub | BinOp::SubUnchecked => Ok(radium::Binop::Sub),
+ BinOp::Mul | BinOp::MulUnchecked => Ok(radium::Binop::Mul),
+ BinOp::Div => Ok(radium::Binop::Div),
+ BinOp::Rem => Ok(radium::Binop::Mod),
+
+ BinOp::BitXor => Ok(radium::Binop::BitXor),
+ BinOp::BitAnd => Ok(radium::Binop::BitAnd),
+ BinOp::BitOr => Ok(radium::Binop::BitOr),
+ BinOp::Shl | BinOp::ShlUnchecked => Ok(radium::Binop::Shl),
+ BinOp::Shr | BinOp::ShrUnchecked => Ok(radium::Binop::Shr),
+
+ BinOp::Eq => Ok(radium::Binop::Eq),
+ BinOp::Lt => Ok(radium::Binop::Lt),
+ BinOp::Le => Ok(radium::Binop::Le),
+ BinOp::Ne => Ok(radium::Binop::Ne),
+ BinOp::Ge => Ok(radium::Binop::Ge),
+ BinOp::Gt => Ok(radium::Binop::Gt),
+
+ BinOp::Offset => {
+ // we need to get the layout of the thing we're offsetting
+ // try to get the type of e1.
+ let e1_ty = self.get_type_of_operand(e1);
+ let off_ty = TX::get_offset_ty(e1_ty)?;
+ let st = self.ty_translator.translate_type_to_syn_type(off_ty)?;
+ let ly = st.into();
+ Ok(radium::Binop::PtrOffset(ly))
+ },
+ }
+ }
+
+ /// Get the inner type of a type to which we can apply the offset operator.
+ fn get_offset_ty(ty: Ty<'tcx>) -> Result<Ty<'tcx>, TranslationError<'tcx>> {
+ match ty.kind() {
+ TyKind::Array(t, _) | TyKind::Slice(t) | TyKind::Ref(_, t, _) => Ok(*t),
+ TyKind::RawPtr(tm) => Ok(tm.ty),
+ _ => Err(TranslationError::UnknownError(format!("cannot take offset of {}", ty))),
+ }
+ }
+
+ /// Translate checked binary operators.
+ /// We need access to the operands, too, to handle the offset operator and get the right
+ /// Caesium layout annotation.
+ fn translate_checked_binop(op: BinOp) -> Result<radium::Binop, TranslationError<'tcx>> {
+ match op {
+ BinOp::Add => Ok(radium::Binop::CheckedAdd),
+ BinOp::Sub => Ok(radium::Binop::CheckedSub),
+ BinOp::Mul => Ok(radium::Binop::CheckedMul),
+ BinOp::Shl => Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support checked Shl".to_owned(),
+ }),
+ BinOp::Shr => Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support checked Shr".to_owned(),
+ }),
+ _ => Err(TranslationError::UnknownError(
+ "unexpected checked binop that is not Add, Sub, Mul, Shl, or Shr".to_owned(),
+ )),
+ }
+ }
+
+ /// Translate unary operators.
+ fn translate_unop(op: UnOp, ty: Ty<'tcx>) -> Result<radium::Unop, TranslationError<'tcx>> {
+ match op {
+ UnOp::Not => match ty.kind() {
+ ty::TyKind::Bool => Ok(radium::Unop::NotBool),
+ ty::TyKind::Int(_) | ty::TyKind::Uint(_) => Ok(radium::Unop::NotInt),
+ _ => Err(TranslationError::UnknownError(
+ "application of UnOp::Not to non-{Int, Bool}".to_owned(),
+ )),
+ },
+ UnOp::Neg => Ok(radium::Unop::Neg),
+ }
+ }
+
+ /// Translate a `BorrowKind`.
+ fn translate_borrow_kind(kind: BorrowKind) -> Result<radium::BorKind, TranslationError<'tcx>> {
+ match kind {
+ BorrowKind::Shared => Ok(radium::BorKind::Shared),
+ BorrowKind::Shallow => {
+ // TODO: figure out what to do with this
+ // arises in match lowering
+ Err(TranslationError::UnsupportedFeature {
+ description: "RefinedRust does currently not support shallow borrows".to_owned(),
+ })
+ },
+ BorrowKind::Mut { .. } => {
+ // TODO: handle two-phase borrows?
+ Ok(radium::BorKind::Mutable)
+ },
+ }
+ }
+
+ const fn translate_mutability(mt: Mutability) -> radium::Mutability {
+ match mt {
+ Mutability::Mut => radium::Mutability::Mut,
+ Mutability::Not => radium::Mutability::Shared,
+ }
+ }
+}
diff --git a/rr_frontend/translation/src/body/translation/terminator.rs b/rr_frontend/translation/src/body/translation/terminator.rs
new file mode 100644
index 0000000000000000000000000000000000000000..4f73ccc98d3ee82256d03940440b826317569d0b
--- /dev/null
+++ b/rr_frontend/translation/src/body/translation/terminator.rs
@@ -0,0 +1,254 @@
+// © 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 super::TX;
+use crate::base::*;
+use crate::body::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::regions::inclusion_tracker::InclusionTracker;
+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};
+
+impl<'a, 'def: 'a, 'tcx: 'def> TX<'a, 'def, 'tcx> {
+ /// 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
+ }
+
+ /// Translate a terminator.
+ /// We pass the dying loans during this terminator. They need to be added at the right
+ /// intermediate point.
+ pub(super) fn translate_terminator(
+ &mut self,
+ term: &Terminator<'tcx>,
+ loc: Location,
+ dying_loans: Vec<facts::Loan>,
+ ) -> Result<radium::Stmt, TranslationError<'tcx>> {
+ match &term.kind {
+ TerminatorKind::Goto { target } => self.translate_goto_like(&loc, *target),
+
+ TerminatorKind::Call {
+ func,
+ args,
+ destination,
+ target,
+ ..
+ } => {
+ trace!("translating Call {:?}", term);
+ if self.is_call_destination_panic(func) {
+ info!("Replacing call to std::panicking::begin_panic with Stuck");
+ return Ok(radium::Stmt::Stuck);
+ }
+
+ self.translate_function_call(func, args, destination, *target, loc, dying_loans.as_slice())
+ },
+
+ TerminatorKind::Return => {
+ // TODO: this requires additional handling for reborrows
+
+ // read from the return place
+ // Is this semantics accurate wrt what the intended MIR semantics is?
+ // Possibly handle this differently by making the first argument of a function a dedicated
+ // return place? See also discussion at https://github.com/rust-lang/rust/issues/71117
+ let stmt = radium::Stmt::Return(radium::Expr::Use {
+ ot: (&self.return_synty).into(),
+ e: Box::new(radium::Expr::Var(self.return_name.clone())),
+ });
+
+ // TODO is this right?
+ Ok(self.prepend_endlfts(stmt, dying_loans.into_iter()))
+ },
+
+ //TerminatorKind::Abort => {
+ //res_stmt = radium::Stmt::Stuck;
+ //res_stmt = self.prepend_endlfts(res_stmt, dying_loans.into_iter());
+ //},
+ TerminatorKind::SwitchInt { discr, targets } => {
+ let operand = self.translate_operand(discr, true)?;
+ let all_targets: &[BasicBlock] = targets.all_targets();
+
+ if self.get_type_of_operand(discr).is_bool() {
+ // we currently special-case this as Caesium has a built-in if and this is more
+ // convenient to handle for the type-checker
+
+ // implementation detail: the first index is the `false` branch, the second the
+ // `true` branch
+ let true_target = all_targets[1];
+ let false_target = all_targets[0];
+
+ let true_branch = self.translate_goto_like(&loc, true_target)?;
+ let false_branch = self.translate_goto_like(&loc, false_target)?;
+
+ let stmt = radium::Stmt::If {
+ e: operand,
+ ot: radium::OpType::Bool,
+ s1: Box::new(true_branch),
+ s2: Box::new(false_branch),
+ };
+
+ // TODO: is this right?
+ return Ok(self.prepend_endlfts(stmt, dying_loans.into_iter()));
+ }
+
+ //info!("switchint: {:?}", term.kind);
+ let operand = self.translate_operand(discr, true)?;
+ let ty = self.get_type_of_operand(discr);
+
+ let mut target_map: HashMap<u128, usize> = HashMap::new();
+ let mut translated_targets: Vec<radium::Stmt> = Vec::new();
+
+ for (idx, (tgt, bb)) in targets.iter().enumerate() {
+ let bb: BasicBlock = bb;
+ let translated_target = self.translate_goto_like(&loc, bb)?;
+
+ target_map.insert(tgt, idx);
+ translated_targets.push(translated_target);
+ }
+
+ let translated_default = self.translate_goto_like(&loc, targets.otherwise())?;
+ // TODO: need to put endlfts infront of gotos?
+
+ let translated_ty = self.ty_translator.translate_type(ty)?;
+ let radium::Type::Int(it) = translated_ty else {
+ return Err(TranslationError::UnknownError(
+ "SwitchInt switching on non-integer type".to_owned(),
+ ));
+ };
+
+ Ok(radium::Stmt::Switch {
+ e: operand,
+ it,
+ index_map: target_map,
+ bs: translated_targets,
+ def: Box::new(translated_default),
+ })
+ },
+
+ TerminatorKind::Assert {
+ cond,
+ expected,
+ target,
+ ..
+ } => {
+ // this translation gets stuck on failure
+ let cond_translated = self.translate_operand(cond, true)?;
+ let comp = radium::Expr::BinOp {
+ o: radium::Binop::Eq,
+ ot1: radium::OpType::Bool,
+ ot2: radium::OpType::Bool,
+ e1: Box::new(cond_translated),
+ e2: Box::new(radium::Expr::Literal(radium::Literal::Bool(*expected))),
+ };
+
+ let stmt = self.translate_goto_like(&loc, *target)?;
+
+ // TODO: should we really have this?
+ let stmt = self.prepend_endlfts(stmt, dying_loans.into_iter());
+
+ Ok(radium::Stmt::AssertS {
+ e: comp,
+ s: Box::new(stmt),
+ })
+ },
+
+ TerminatorKind::Drop { place, target, .. } => {
+ let ty = self.get_type_of_place(place);
+ self.register_drop_shim_for(ty.ty);
+
+ let place_translated = self.translate_place(place)?;
+ let _drope = radium::Expr::DropE(Box::new(place_translated));
+
+ let stmt = self.translate_goto_like(&loc, *target)?;
+
+ Ok(self.prepend_endlfts(stmt, dying_loans.into_iter()))
+
+ //res_stmt = radium::Stmt::ExprS { e: drope, s: Box::new(res_stmt)};
+ },
+
+ // just a goto for our purposes
+ TerminatorKind::FalseEdge { real_target, .. }
+ // this is just a virtual edge for the borrowchecker, we can translate this to a normal goto
+ | TerminatorKind::FalseUnwind { real_target, .. } => {
+ self.translate_goto_like(&loc, *real_target)
+ },
+
+ TerminatorKind::Unreachable => Ok(radium::Stmt::Stuck),
+
+ TerminatorKind::UnwindResume => Err(TranslationError::Unimplemented {
+ description: "implement UnwindResume".to_owned(),
+ }),
+
+ TerminatorKind::UnwindTerminate(_) => Err(TranslationError::Unimplemented {
+ description: "implement UnwindTerminate".to_owned(),
+ }),
+
+ TerminatorKind::GeneratorDrop
+ | TerminatorKind::InlineAsm { .. }
+ | TerminatorKind::Yield { .. } => Err(TranslationError::UnsupportedFeature {
+ description: format!(
+ "RefinedRust does currently not support this kind of terminator (got: {:?})",
+ term
+ ),
+ }),
+ }
+ }
+}
diff --git a/rr_frontend/translation/src/body/translator.rs b/rr_frontend/translation/src/body/translator.rs
deleted file mode 100644
index bfb76258e500b8f8834dd9d4d29b2f5c85eda33a..0000000000000000000000000000000000000000
--- a/rr_frontend/translation/src/body/translator.rs
+++ /dev/null
@@ -1,2460 +0,0 @@
-// © 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::base::*;
-use crate::body::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::regions::inclusion_tracker::InclusionTracker;
-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(¶m_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)
-}
-
-/// 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 = regions::init::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(),
- })
- }
-
- /// 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
- }
-
- /// 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 translate_function_call(
- &mut self,
- func: &Operand<'tcx>,
- args: &[Operand<'tcx>],
- destination: &Place<'tcx>,
- target: Option<middle::mir::BasicBlock>,
- loc: Location,
- dying_loans: &[facts::Loan],
- ) -> Result<radium::Stmt, TranslationError<'tcx>> {
- let startpoint = self.info.interner.get_point_index(&facts::Point {
- location: loc,
- typ: facts::PointType::Start,
- });
-
- let Operand::Constant(box func_constant) = func else {
- return Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support this kind of call operand (got: {:?})",
- func
- ),
- });
- };
-
- // Get the type of the return value from the function
- let (target_did, sig, generic_args, inst_sig) = self.call_expr_op_split_inst(func_constant)?;
- info!("calling function {:?}", target_did);
- info!("call substs: {:?} = {:?}, {:?}", func, sig, generic_args);
-
- // for lifetime annotations:
- // 1. get the regions involved here. for that, get the instantiation of the function.
- // + if it's a FnDef type, that should be easy.
- // + for a function pointer: ?
- // + for a closure: ?
- // (Polonius does not seem to distinguish early/late bound in any way, except
- // that they are numbered in different passes)
- // 2. find the constraints here involving the regions.
- // 3. solve for the regions.
- // + transitively propagate the constraints
- // + check for equalities
- // + otherwise compute intersection. singleton intersection just becomes an equality def.
- // 4. add annotations accordingly
- // + either a startlft
- // + or a copy name
- // 5. add shortenlft annotations to line up arguments.
- // + for that, we need the type of the LHS, and what the argument types (with
- // substituted regions) should be.
- // 6. annotate the return value on assignment and establish constraints.
-
- let classification =
- regions::calls::compute_call_regions(self.env, &self.inclusion_tracker, generic_args, loc);
-
- // update the inclusion tracker with the new regions we have introduced
- // We just add the inclusions and ignore that we resolve it in a "tight" way.
- // the cases where we need the reverse inclusion should be really rare.
- for (r, c) in &classification.classification {
- match c {
- regions::calls::CallRegionKind::EqR(r2) => {
- // put it at the start point, because the inclusions come into effect
- // at the point right before.
- self.inclusion_tracker.add_static_inclusion(*r, *r2, startpoint);
- self.inclusion_tracker.add_static_inclusion(*r2, *r, startpoint);
- },
- regions::calls::CallRegionKind::Intersection(lfts) => {
- // all the regions represented by lfts need to be included in r
- for r2 in lfts {
- self.inclusion_tracker.add_static_inclusion(*r2, *r, startpoint);
- }
- },
- }
- }
-
- // translate the function expression.
- let func_expr = self.translate_operand(func, false)?;
- // We expect this to be an Expr::CallTarget, being annotated with the type parameters we
- // instantiate it with.
- let radium::Expr::CallTarget(func_lit, ty_param_annots, mut lft_param_annots) = func_expr else {
- unreachable!("Logic error in call target translation");
- };
- let func_expr = radium::Expr::MetaParam(func_lit);
-
- // translate the arguments
- let mut translated_args = Vec::new();
- for arg in args {
- // to_ty is the type the function expects
-
- //let ty = arg.ty(&self.proc.get_mir().local_decls, self.env.tcx());
- let translated_arg = self.translate_operand(arg, true)?;
- translated_args.push(translated_arg);
- }
-
- // We have to add the late regions, since we do not requantify over them.
- for late in &classification.late_regions {
- let lft = self.format_region(*late);
- lft_param_annots.push(lft);
- }
- info!("Call lifetime instantiation (early): {:?}", classification.early_regions);
- info!("Call lifetime instantiation (late): {:?}", classification.late_regions);
-
- // TODO: do we need to do something with late bounds?
- let output_ty = inst_sig.output().skip_binder();
- info!("call has instantiated type {:?}", inst_sig);
-
- // compute the resulting annotations
- let lhs_ty = self.get_type_of_place(destination);
- let lhs_strongly_writeable = !self.check_place_below_reference(destination);
- let (rhs_annots, pre_stmt_annots, post_stmt_annots) = regions::assignment::get_assignment_annots(
- self.env,
- &mut self.inclusion_tracker,
- &self.ty_translator,
- loc,
- lhs_strongly_writeable,
- lhs_ty,
- output_ty,
- );
- info!(
- "assignment annots after call: expr: {:?}, pre-stmt: {:?}, post-stmt: {:?}",
- rhs_annots, pre_stmt_annots, post_stmt_annots
- );
-
- // TODO: add annotations for the assignment
- // for that:
- // - get the type of the place
- // - enforce constraints as necessary. this might spawn dyninclusions with some of the new regions =>
- // In Coq, also the aliases should get proper endlft events to resolve the dyninclusions.
- // - update the name map
- let call_expr = radium::Expr::Call {
- f: Box::new(func_expr),
- lfts: lft_param_annots,
- tys: ty_param_annots,
- args: translated_args,
- };
- let stmt = match target {
- Some(target) => {
- let mut cont_stmt = self.translate_goto_like(&loc, target)?;
- // end loans before the goto, but after the call.
- // TODO: may cause duplications?
- cont_stmt = self.prepend_endlfts(cont_stmt, dying_loans.iter().copied());
-
- let cont_stmt = radium::Stmt::with_annotations(
- cont_stmt,
- post_stmt_annots,
- &Some("post_function_call".to_owned()),
- );
-
- // assign stmt with call; then jump to bb
- let place_ty = self.get_type_of_place(destination);
- let place_st = self.ty_translator.translate_type_to_syn_type(place_ty.ty)?;
- let place_expr = self.translate_place(destination)?;
- let ot = place_st.into();
-
- let annotated_rhs = radium::Expr::with_optional_annotation(
- call_expr,
- rhs_annots,
- Some("function_call".to_owned()),
- );
- let assign_stmt = radium::Stmt::Assign {
- ot,
- e1: place_expr,
- e2: annotated_rhs,
- s: Box::new(cont_stmt),
- };
- radium::Stmt::with_annotations(
- assign_stmt,
- pre_stmt_annots,
- &Some("function_call".to_owned()),
- )
- },
- None => {
- // expr stmt with call; then stuck (we have not provided a continuation, after all)
- radium::Stmt::ExprS {
- e: call_expr,
- s: Box::new(radium::Stmt::Stuck),
- }
- },
- };
-
- let mut stmt_annots = Vec::new();
-
- // add annotations to initialize the regions for the call (before the call)
- for (r, class) in &classification.classification {
- let lft = self.format_region(*r);
- match class {
- regions::calls::CallRegionKind::EqR(r2) => {
- let lft2 = self.format_region(*r2);
- stmt_annots.push(radium::Annotation::CopyLftName(lft2, lft));
- },
-
- regions::calls::CallRegionKind::Intersection(rs) => {
- match rs.len() {
- 0 => {
- return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support unconstrained lifetime"
- .to_owned(),
- });
- },
- 1 => {
- // this is really just an equality constraint
- if let Some(r2) = rs.iter().next() {
- let lft2 = self.format_region(*r2);
- stmt_annots.push(radium::Annotation::CopyLftName(lft2, lft));
- }
- },
- _ => {
- // a proper intersection
- let lfts: Vec<_> = rs.iter().map(|r| self.format_region(*r)).collect();
- stmt_annots.push(radium::Annotation::AliasLftIntersection(lft, lfts));
- },
- };
- },
- }
- }
-
- let stmt = radium::Stmt::with_annotations(stmt, stmt_annots, &Some("function_call".to_owned()));
- Ok(stmt)
- }
-
- /// Translate a terminator.
- /// We pass the dying loans during this terminator. They need to be added at the right
- /// intermediate point.
- fn translate_terminator(
- &mut self,
- term: &Terminator<'tcx>,
- loc: Location,
- dying_loans: Vec<facts::Loan>,
- ) -> Result<radium::Stmt, TranslationError<'tcx>> {
- match &term.kind {
- TerminatorKind::Goto { target } => self.translate_goto_like(&loc, *target),
-
- TerminatorKind::Call {
- func,
- args,
- destination,
- target,
- ..
- } => {
- trace!("translating Call {:?}", term);
- if self.is_call_destination_panic(func) {
- info!("Replacing call to std::panicking::begin_panic with Stuck");
- return Ok(radium::Stmt::Stuck);
- }
-
- self.translate_function_call(func, args, destination, *target, loc, dying_loans.as_slice())
- },
-
- TerminatorKind::Return => {
- // TODO: this requires additional handling for reborrows
-
- // read from the return place
- // Is this semantics accurate wrt what the intended MIR semantics is?
- // Possibly handle this differently by making the first argument of a function a dedicated
- // return place? See also discussion at https://github.com/rust-lang/rust/issues/71117
- let stmt = radium::Stmt::Return(radium::Expr::Use {
- ot: (&self.return_synty).into(),
- e: Box::new(radium::Expr::Var(self.return_name.clone())),
- });
-
- // TODO is this right?
- Ok(self.prepend_endlfts(stmt, dying_loans.into_iter()))
- },
-
- //TerminatorKind::Abort => {
- //res_stmt = radium::Stmt::Stuck;
- //res_stmt = self.prepend_endlfts(res_stmt, dying_loans.into_iter());
- //},
- TerminatorKind::SwitchInt { discr, targets } => {
- let operand = self.translate_operand(discr, true)?;
- let all_targets: &[BasicBlock] = targets.all_targets();
-
- if self.get_type_of_operand(discr).is_bool() {
- // we currently special-case this as Caesium has a built-in if and this is more
- // convenient to handle for the type-checker
-
- // implementation detail: the first index is the `false` branch, the second the
- // `true` branch
- let true_target = all_targets[1];
- let false_target = all_targets[0];
-
- let true_branch = self.translate_goto_like(&loc, true_target)?;
- let false_branch = self.translate_goto_like(&loc, false_target)?;
-
- let stmt = radium::Stmt::If {
- e: operand,
- ot: radium::OpType::Bool,
- s1: Box::new(true_branch),
- s2: Box::new(false_branch),
- };
-
- // TODO: is this right?
- return Ok(self.prepend_endlfts(stmt, dying_loans.into_iter()));
- }
-
- //info!("switchint: {:?}", term.kind);
- let operand = self.translate_operand(discr, true)?;
- let ty = self.get_type_of_operand(discr);
-
- let mut target_map: HashMap<u128, usize> = HashMap::new();
- let mut translated_targets: Vec<radium::Stmt> = Vec::new();
-
- for (idx, (tgt, bb)) in targets.iter().enumerate() {
- let bb: BasicBlock = bb;
- let translated_target = self.translate_goto_like(&loc, bb)?;
-
- target_map.insert(tgt, idx);
- translated_targets.push(translated_target);
- }
-
- let translated_default = self.translate_goto_like(&loc, targets.otherwise())?;
- // TODO: need to put endlfts infront of gotos?
-
- let translated_ty = self.ty_translator.translate_type(ty)?;
- let radium::Type::Int(it) = translated_ty else {
- return Err(TranslationError::UnknownError(
- "SwitchInt switching on non-integer type".to_owned(),
- ));
- };
-
- Ok(radium::Stmt::Switch {
- e: operand,
- it,
- index_map: target_map,
- bs: translated_targets,
- def: Box::new(translated_default),
- })
- },
-
- TerminatorKind::Assert {
- cond,
- expected,
- target,
- ..
- } => {
- // this translation gets stuck on failure
- let cond_translated = self.translate_operand(cond, true)?;
- let comp = radium::Expr::BinOp {
- o: radium::Binop::Eq,
- ot1: radium::OpType::Bool,
- ot2: radium::OpType::Bool,
- e1: Box::new(cond_translated),
- e2: Box::new(radium::Expr::Literal(radium::Literal::Bool(*expected))),
- };
-
- let stmt = self.translate_goto_like(&loc, *target)?;
-
- // TODO: should we really have this?
- let stmt = self.prepend_endlfts(stmt, dying_loans.into_iter());
-
- Ok(radium::Stmt::AssertS {
- e: comp,
- s: Box::new(stmt),
- })
- },
-
- TerminatorKind::Drop { place, target, .. } => {
- let ty = self.get_type_of_place(place);
- self.register_drop_shim_for(ty.ty);
-
- let place_translated = self.translate_place(place)?;
- let _drope = radium::Expr::DropE(Box::new(place_translated));
-
- let stmt = self.translate_goto_like(&loc, *target)?;
-
- Ok(self.prepend_endlfts(stmt, dying_loans.into_iter()))
-
- //res_stmt = radium::Stmt::ExprS { e: drope, s: Box::new(res_stmt)};
- },
-
- // just a goto for our purposes
- TerminatorKind::FalseEdge { real_target, .. }
- // this is just a virtual edge for the borrowchecker, we can translate this to a normal goto
- | TerminatorKind::FalseUnwind { real_target, .. } => {
- self.translate_goto_like(&loc, *real_target)
- },
-
- TerminatorKind::Unreachable => Ok(radium::Stmt::Stuck),
-
- TerminatorKind::UnwindResume => Err(TranslationError::Unimplemented {
- description: "implement UnwindResume".to_owned(),
- }),
-
- TerminatorKind::UnwindTerminate(_) => Err(TranslationError::Unimplemented {
- description: "implement UnwindTerminate".to_owned(),
- }),
-
- TerminatorKind::GeneratorDrop
- | TerminatorKind::InlineAsm { .. }
- | TerminatorKind::Yield { .. } => Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support this kind of terminator (got: {:?})",
- term
- ),
- }),
- }
- }
-
- /// Prepend endlft annotations for dying loans to a statement.
- fn prepend_endlfts<I>(&self, st: radium::Stmt, dying: I) -> radium::Stmt
- where
- I: ExactSizeIterator<Item = facts::Loan>,
- {
- let mut cont_stmt = st;
- if dying.len() > 0 {
- //info!("Dying at {:?}: {:?}", loc, dying);
- for d in dying {
- let lft = self.info.atomic_region_of_loan(d);
- cont_stmt = radium::Stmt::Annot {
- a: radium::Annotation::EndLft(self.ty_translator.format_atomic_region(&lft)),
- s: Box::new(cont_stmt),
- why: Some("endlft".to_owned()),
- };
- }
- }
- cont_stmt
- }
-
- /// Get predecessors in the CFG.
- fn get_loc_predecessors(&self, loc: Location) -> Vec<Location> {
- if loc.statement_index > 0 {
- let pred = Location {
- block: loc.block,
- statement_index: loc.statement_index - 1,
- };
- vec![pred]
- } else {
- // check for gotos that go to this basic block
- let pred_bbs = self.proc.predecessors(loc.block);
- let basic_blocks = &self.proc.get_mir().basic_blocks;
- pred_bbs
- .iter()
- .map(|bb| {
- let data = &basic_blocks[*bb];
- Location {
- block: *bb,
- statement_index: data.statements.len(),
- }
- })
- .collect()
- }
- }
-
- /// Check if a local is used for a spec closure.
- fn is_spec_closure_local(&self, l: Local) -> Result<Option<DefId>, TranslationError<'tcx>> {
- // check if we should ignore this
- let local_type = self.get_type_of_local(l)?;
-
- let TyKind::Closure(did, _) = local_type.kind() else {
- return Ok(None);
- };
-
- Ok(self
- .procedure_registry
- .lookup_function_mode(*did)
- .and_then(|m| m.is_ignore().then_some(*did)))
- }
-
- /**
- * Translate a single basic block.
- */
- fn translate_basic_block(
- &mut self,
- bb_idx: BasicBlock,
- bb: &BasicBlockData<'tcx>,
- ) -> Result<radium::Stmt, TranslationError<'tcx>> {
- // we translate from back to front, starting with the terminator, since Caesium statements
- // have a continuation (the next statement to execute)
-
- // first do the endlfts for the things right before the terminator
- let mut idx = bb.statements.len();
- let loc = Location {
- block: bb_idx,
- statement_index: idx,
- };
- let dying = self.info.get_dying_loans(loc);
- // TODO zombie?
- let _dying_zombie = self.info.get_dying_zombie_loans(loc);
- let mut cont_stmt: radium::Stmt = self.translate_terminator(bb.terminator(), loc, dying)?;
-
- //cont_stmt = self.prepend_endlfts(cont_stmt, loc, dying);
- //cont_stmt = self.prepend_endlfts(cont_stmt, loc, dying_zombie);
-
- for stmt in bb.statements.iter().rev() {
- idx -= 1;
- let loc = Location {
- block: bb_idx,
- statement_index: idx,
- };
-
- // get all dying loans, and emit endlfts for these.
- // We loop over all predecessor locations, since some loans may end at the start of a
- // basic block (in particular related to NLL stuff)
- let pred = self.get_loc_predecessors(loc);
- let mut dying_loans = HashSet::new();
- for p in pred {
- let dying_between = self.info.get_loans_dying_between(p, loc, false);
- for l in &dying_between {
- dying_loans.insert(*l);
- }
- // also include zombies
- let dying_between = self.info.get_loans_dying_between(p, loc, true);
- for l in &dying_between {
- dying_loans.insert(*l);
- }
- }
- // we prepend them before the current statement
-
- match &stmt.kind {
- StatementKind::Assign(b) => {
- let (plc, val) = b.as_ref();
-
- if (self.is_spec_closure_local(plc.local)?).is_some() {
- info!("skipping assignment to spec closure local: {:?}", plc);
- } else if let Some(rewritten_ty) = self.checked_op_temporaries.get(&plc.local) {
- // if this is a checked op, be sure to remember it
- info!("rewriting assignment to checked op: {:?}", plc);
-
- let synty = self.ty_translator.translate_type_to_syn_type(*rewritten_ty)?;
-
- let translated_val = self.translate_rvalue(loc, val)?;
- let translated_place = self.translate_place(plc)?;
-
- // this should be a temporary
- assert!(plc.projection.is_empty());
-
- let ot = synty.into();
- cont_stmt = radium::Stmt::Assign {
- ot,
- e1: translated_place,
- e2: translated_val,
- s: Box::new(cont_stmt),
- };
- } else {
- let plc_ty = self.get_type_of_place(plc);
- let rhs_ty = val.ty(&self.proc.get_mir().local_decls, self.env.tcx());
-
- let borrow_annots = regions::assignment::get_assignment_loan_annots(
- &mut self.inclusion_tracker, &self.ty_translator,
- loc, val);
-
- let plc_ty = self.get_type_of_place(plc);
- let plc_strongly_writeable = !self.check_place_below_reference(plc);
- let (expr_annot, pre_stmt_annots, post_stmt_annots) =
- regions::assignment::get_assignment_annots(
- self.env, &mut self.inclusion_tracker, &self.ty_translator,
- loc, plc_strongly_writeable, plc_ty, rhs_ty);
-
- // TODO; maybe move this to rvalue
- let composite_annots = regions::composite::get_composite_rvalue_creation_annots(
- self.env, &mut self.inclusion_tracker, &self.ty_translator, loc, rhs_ty);
-
- cont_stmt = radium::Stmt::with_annotations(
- cont_stmt,
- post_stmt_annots,
- &Some("post-assignment".to_owned()),
- );
-
- let translated_val = radium::Expr::with_optional_annotation(
- self.translate_rvalue(loc, val)?,
- expr_annot,
- Some("assignment".to_owned()),
- );
- let translated_place = self.translate_place(plc)?;
- let synty = self.ty_translator.translate_type_to_syn_type(plc_ty.ty)?;
- cont_stmt = radium::Stmt::Assign {
- ot: synty.into(),
- e1: translated_place,
- e2: translated_val,
- s: Box::new(cont_stmt),
- };
- cont_stmt = radium::Stmt::with_annotations(
- cont_stmt,
- pre_stmt_annots,
- &Some("assignment".to_owned()),
- );
- cont_stmt = radium::Stmt::with_annotations(
- cont_stmt,
- borrow_annots,
- &Some("borrow".to_owned()),
- );
- cont_stmt = radium::Stmt::with_annotations(
- cont_stmt,
- composite_annots,
- &Some("composite".to_owned()),
- );
- }
- },
-
- StatementKind::Deinit(_) => {
- // TODO: find out where this is emitted
- return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support Deinit".to_owned(),
- });
- },
-
- StatementKind::FakeRead(b) => {
- // we can probably ignore this, but I'm not sure
- info!("Ignoring FakeRead: {:?}", b);
- },
-
- StatementKind::Intrinsic(intrinsic) => {
- match intrinsic.as_ref() {
- NonDivergingIntrinsic::Assume(_) => {
- // ignore
- info!("Ignoring Assume: {:?}", intrinsic);
- },
- NonDivergingIntrinsic::CopyNonOverlapping(_) => {
- return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support the CopyNonOverlapping Intrinsic".to_owned(),
- });
- },
- }
- },
-
- StatementKind::PlaceMention(place) => {
- // TODO: this is missed UB
- info!("Ignoring PlaceMention: {:?}", place);
- },
-
- StatementKind::SetDiscriminant {
- place: _place,
- variant_index: _variant_index,
- } => {
- // TODO
- return Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support SetDiscriminant".to_owned(),
- });
- },
-
- // don't need that info
- | StatementKind::AscribeUserType(_, _)
- // don't need that
- | StatementKind::Coverage(_)
- // no-op
- | StatementKind::ConstEvalCounter
- // ignore
- | StatementKind::Nop
- // just ignore
- | StatementKind::StorageLive(_)
- // just ignore
- | StatementKind::StorageDead(_)
- // just ignore retags
- | StatementKind::Retag(_, _) => (),
- }
-
- cont_stmt = self.prepend_endlfts(cont_stmt, dying_loans.into_iter());
- }
-
- Ok(cont_stmt)
- }
-
- /// Translate a `BorrowKind`.
- fn translate_borrow_kind(kind: BorrowKind) -> Result<radium::BorKind, TranslationError<'tcx>> {
- match kind {
- BorrowKind::Shared => Ok(radium::BorKind::Shared),
- BorrowKind::Shallow => {
- // TODO: figure out what to do with this
- // arises in match lowering
- Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support shallow borrows".to_owned(),
- })
- },
- BorrowKind::Mut { .. } => {
- // TODO: handle two-phase borrows?
- Ok(radium::BorKind::Mutable)
- },
- }
- }
-
- const fn translate_mutability(mt: Mutability) -> radium::Mutability {
- match mt {
- Mutability::Mut => radium::Mutability::Mut,
- Mutability::Not => radium::Mutability::Shared,
- }
- }
-
- /// Get the inner type of a type to which we can apply the offset operator.
- fn get_offset_ty(ty: Ty<'tcx>) -> Result<Ty<'tcx>, TranslationError<'tcx>> {
- match ty.kind() {
- TyKind::Array(t, _) | TyKind::Slice(t) | TyKind::Ref(_, t, _) => Ok(*t),
- TyKind::RawPtr(tm) => Ok(tm.ty),
- _ => Err(TranslationError::UnknownError(format!("cannot take offset of {}", ty))),
- }
- }
-
- /// Translate binary operators.
- /// We need access to the operands, too, to handle the offset operator and get the right
- /// Caesium layout annotation.
- fn translate_binop(
- &self,
- op: BinOp,
- e1: &Operand<'tcx>,
- _e2: &Operand<'tcx>,
- ) -> Result<radium::Binop, TranslationError<'tcx>> {
- match op {
- BinOp::Add | BinOp::AddUnchecked => Ok(radium::Binop::Add),
- BinOp::Sub | BinOp::SubUnchecked => Ok(radium::Binop::Sub),
- BinOp::Mul | BinOp::MulUnchecked => Ok(radium::Binop::Mul),
- BinOp::Div => Ok(radium::Binop::Div),
- BinOp::Rem => Ok(radium::Binop::Mod),
-
- BinOp::BitXor => Ok(radium::Binop::BitXor),
- BinOp::BitAnd => Ok(radium::Binop::BitAnd),
- BinOp::BitOr => Ok(radium::Binop::BitOr),
- BinOp::Shl | BinOp::ShlUnchecked => Ok(radium::Binop::Shl),
- BinOp::Shr | BinOp::ShrUnchecked => Ok(radium::Binop::Shr),
-
- BinOp::Eq => Ok(radium::Binop::Eq),
- BinOp::Lt => Ok(radium::Binop::Lt),
- BinOp::Le => Ok(radium::Binop::Le),
- BinOp::Ne => Ok(radium::Binop::Ne),
- BinOp::Ge => Ok(radium::Binop::Ge),
- BinOp::Gt => Ok(radium::Binop::Gt),
-
- BinOp::Offset => {
- // we need to get the layout of the thing we're offsetting
- // try to get the type of e1.
- let e1_ty = self.get_type_of_operand(e1);
- let off_ty = TX::get_offset_ty(e1_ty)?;
- let st = self.ty_translator.translate_type_to_syn_type(off_ty)?;
- let ly = st.into();
- Ok(radium::Binop::PtrOffset(ly))
- },
- }
- }
-
- /// Translate checked binary operators.
- /// We need access to the operands, too, to handle the offset operator and get the right
- /// Caesium layout annotation.
- fn translate_checked_binop(op: BinOp) -> Result<radium::Binop, TranslationError<'tcx>> {
- match op {
- BinOp::Add => Ok(radium::Binop::CheckedAdd),
- BinOp::Sub => Ok(radium::Binop::CheckedSub),
- BinOp::Mul => Ok(radium::Binop::CheckedMul),
- BinOp::Shl => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support checked Shl".to_owned(),
- }),
- BinOp::Shr => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support checked Shr".to_owned(),
- }),
- _ => Err(TranslationError::UnknownError(
- "unexpected checked binop that is not Add, Sub, Mul, Shl, or Shr".to_owned(),
- )),
- }
- }
-
- /// Translate unary operators.
- fn translate_unop(op: UnOp, ty: Ty<'tcx>) -> Result<radium::Unop, TranslationError<'tcx>> {
- match op {
- UnOp::Not => match ty.kind() {
- ty::TyKind::Bool => Ok(radium::Unop::NotBool),
- ty::TyKind::Int(_) | ty::TyKind::Uint(_) => Ok(radium::Unop::NotInt),
- _ => Err(TranslationError::UnknownError(
- "application of UnOp::Not to non-{Int, Bool}".to_owned(),
- )),
- },
- UnOp::Neg => Ok(radium::Unop::Neg),
- }
- }
-
- /// Get the type to annotate a borrow with.
- fn get_type_annotation_for_borrow(
- &self,
- bk: BorrowKind,
- pl: &Place<'tcx>,
- ) -> Result<Option<radium::RustType>, TranslationError<'tcx>> {
- let BorrowKind::Mut { .. } = bk else {
- return Ok(None);
- };
-
- let ty = self.get_type_of_place(pl);
-
- // For borrows, we can safely ignore the downcast type -- we cannot borrow a particularly variant
- let translated_ty = self.ty_translator.translate_type(ty.ty)?;
- let annot_ty = radium::RustType::of_type(&translated_ty);
-
- Ok(Some(annot_ty))
- }
-
- /// Translates an Rvalue.
- fn translate_rvalue(
- &mut self,
- loc: Location,
- rval: &Rvalue<'tcx>,
- ) -> Result<radium::Expr, TranslationError<'tcx>> {
- match rval {
- Rvalue::Use(op) => {
- // converts an lvalue to an rvalue
- self.translate_operand(op, true)
- },
-
- Rvalue::Ref(region, bk, pl) => {
- let translated_pl = self.translate_place(pl)?;
- let translated_bk = TX::translate_borrow_kind(*bk)?;
- let ty_annot = self.get_type_annotation_for_borrow(*bk, pl)?;
-
- if let Some(loan) = self.info.get_optional_loan_at_location(loc) {
- let atomic_region = self.info.atomic_region_of_loan(loan);
- let lft = self.ty_translator.format_atomic_region(&atomic_region);
- Ok(radium::Expr::Borrow {
- lft,
- bk: translated_bk,
- ty: ty_annot,
- e: Box::new(translated_pl),
- })
- } else {
- info!("Didn't find loan at {:?}: {:?}; region {:?}", loc, rval, region);
- let region = regions::region_to_region_vid(*region);
- let lft = self.format_region(region);
-
- Ok(radium::Expr::Borrow {
- lft,
- bk: translated_bk,
- ty: ty_annot,
- e: Box::new(translated_pl),
- })
- }
- },
-
- Rvalue::AddressOf(mt, pl) => {
- let translated_pl = self.translate_place(pl)?;
- let translated_mt = TX::translate_mutability(*mt);
-
- Ok(radium::Expr::AddressOf {
- mt: translated_mt,
- e: Box::new(translated_pl),
- })
- },
-
- Rvalue::BinaryOp(op, operands) => {
- let e1 = &operands.as_ref().0;
- let e2 = &operands.as_ref().1;
-
- let e1_ty = self.get_type_of_operand(e1);
- let e2_ty = self.get_type_of_operand(e2);
- let e1_st = self.ty_translator.translate_type_to_syn_type(e1_ty)?;
- let e2_st = self.ty_translator.translate_type_to_syn_type(e2_ty)?;
-
- let translated_e1 = self.translate_operand(e1, true)?;
- let translated_e2 = self.translate_operand(e2, true)?;
- let translated_op = self.translate_binop(*op, &operands.as_ref().0, &operands.as_ref().1)?;
-
- Ok(radium::Expr::BinOp {
- o: translated_op,
- ot1: e1_st.into(),
- ot2: e2_st.into(),
- e1: Box::new(translated_e1),
- e2: Box::new(translated_e2),
- })
- },
-
- Rvalue::CheckedBinaryOp(op, operands) => {
- let e1 = &operands.as_ref().0;
- let e2 = &operands.as_ref().1;
-
- let e1_ty = self.get_type_of_operand(e1);
- let e2_ty = self.get_type_of_operand(e2);
- let e1_st = self.ty_translator.translate_type_to_syn_type(e1_ty)?;
- let e2_st = self.ty_translator.translate_type_to_syn_type(e2_ty)?;
-
- let translated_e1 = self.translate_operand(e1, true)?;
- let translated_e2 = self.translate_operand(e2, true)?;
- let translated_op = TX::translate_checked_binop(*op)?;
-
- Ok(radium::Expr::BinOp {
- o: translated_op,
- ot1: e1_st.into(),
- ot2: e2_st.into(),
- e1: Box::new(translated_e1),
- e2: Box::new(translated_e2),
- })
- },
-
- Rvalue::UnaryOp(op, operand) => {
- let translated_e1 = self.translate_operand(operand, true)?;
- let e1_ty = self.get_type_of_operand(operand);
- let e1_st = self.ty_translator.translate_type_to_syn_type(e1_ty)?;
- let translated_op = TX::translate_unop(*op, e1_ty)?;
-
- Ok(radium::Expr::UnOp {
- o: translated_op,
- ot: e1_st.into(),
- e: Box::new(translated_e1),
- })
- },
-
- Rvalue::NullaryOp(op, _ty) => {
- // TODO: SizeOf
- Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support nullary ops (AlignOf, Sizeof)"
- .to_owned(),
- })
- },
-
- Rvalue::Discriminant(pl) => {
- let ty = self.get_type_of_place(pl);
- let translated_pl = self.translate_place(pl)?;
- info!("getting discriminant of {:?} at type {:?}", pl, ty);
-
- let ty::TyKind::Adt(adt_def, args) = ty.ty.kind() else {
- return Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support discriminant accesses on non-enum types ({:?}, got {:?})",
- rval, ty.ty
- ),
- });
- };
-
- let enum_use = self.ty_translator.generate_enum_use(*adt_def, args.iter())?;
- let els = enum_use.generate_raw_syn_type_term();
-
- let discriminant_acc = radium::Expr::EnumDiscriminant {
- els: els.to_string(),
- e: Box::new(translated_pl),
- };
-
- // need to do a load from this place
- let it = ty.ty.discriminant_ty(self.env.tcx());
- let translated_it = self.ty_translator.translate_type(it)?;
-
- let radium::Type::Int(translated_it) = translated_it else {
- return Err(TranslationError::UnknownError(format!(
- "type of discriminant is not an integer type {:?}",
- it
- )));
- };
-
- let ot = radium::OpType::Int(translated_it);
-
- Ok(radium::Expr::Use {
- ot,
- e: Box::new(discriminant_acc),
- })
- },
-
- Rvalue::Aggregate(kind, op) => {
- // translate operands
- let mut translated_ops: Vec<radium::Expr> = Vec::new();
- let mut operand_types: Vec<Ty<'tcx>> = Vec::new();
-
- for o in op {
- let translated_o = self.translate_operand(o, true)?;
- let type_of_o = self.get_type_of_operand(o);
- translated_ops.push(translated_o);
- operand_types.push(type_of_o);
- }
-
- match *kind {
- box mir::AggregateKind::Tuple => {
- if operand_types.is_empty() {
- // translate to unit literal
- return Ok(radium::Expr::Literal(radium::Literal::ZST));
- }
-
- let struct_use =
- self.ty_translator.generate_tuple_use(operand_types.iter().copied())?;
- let sl = struct_use.generate_raw_syn_type_term();
- let initializers: Vec<_> =
- translated_ops.into_iter().enumerate().map(|(i, o)| (i.to_string(), o)).collect();
-
- Ok(radium::Expr::StructInitE {
- sls: coq::term::App::new_lhs(sl.to_string()),
- components: initializers,
- })
- },
-
- box mir::AggregateKind::Adt(did, variant, args, ..) => {
- // get the adt def
- let adt_def: ty::AdtDef<'tcx> = self.env.tcx().adt_def(did);
-
- if adt_def.is_struct() {
- let variant = adt_def.variant(variant);
- let struct_use = self.ty_translator.generate_struct_use(variant.def_id, args)?;
-
- let Some(struct_use) = struct_use else {
- // if not, it's replaced by unit
- return Ok(radium::Expr::Literal(radium::Literal::ZST));
- };
-
- let sl = struct_use.generate_raw_syn_type_term();
- let initializers: Vec<_> = translated_ops
- .into_iter()
- .zip(variant.fields.iter())
- .map(|(o, field)| (field.name.to_string(), o))
- .collect();
-
- return Ok(radium::Expr::StructInitE {
- sls: coq::term::App::new_lhs(sl.to_string()),
- components: initializers,
- });
- }
-
- if adt_def.is_enum() {
- let variant_def = adt_def.variant(variant);
-
- let struct_use =
- self.ty_translator.generate_enum_variant_use(variant_def.def_id, args)?;
- let sl = struct_use.generate_raw_syn_type_term();
-
- let initializers: Vec<_> = translated_ops
- .into_iter()
- .zip(variant_def.fields.iter())
- .map(|(o, field)| (field.name.to_string(), o))
- .collect();
-
- let variant_e = radium::Expr::StructInitE {
- sls: coq::term::App::new_lhs(sl.to_string()),
- components: initializers,
- };
-
- let enum_use = self.ty_translator.generate_enum_use(adt_def, args)?;
- let els = enum_use.generate_raw_syn_type_term();
-
- info!("generating enum annotation for type {:?}", enum_use);
- let ty = radium::RustType::of_type(&radium::Type::Literal(enum_use));
- let variant_name = variant_def.name.to_string();
-
- return Ok(radium::Expr::EnumInitE {
- els: coq::term::App::new_lhs(els.to_string()),
- variant: variant_name,
- ty,
- initializer: Box::new(variant_e),
- });
- }
-
- // TODO
- Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support aggregate rvalue for other ADTs (got: {:?})",
- rval
- ),
- })
- },
- box mir::AggregateKind::Closure(def, _args) => {
- trace!("Translating Closure aggregate value for {:?}", def);
-
- // We basically translate this to a tuple
- if operand_types.is_empty() {
- // translate to unit literal
- return Ok(radium::Expr::Literal(radium::Literal::ZST));
- }
-
- let struct_use =
- self.ty_translator.generate_tuple_use(operand_types.iter().copied())?;
- let sl = struct_use.generate_raw_syn_type_term();
-
- let initializers: Vec<_> =
- translated_ops.into_iter().enumerate().map(|(i, o)| (i.to_string(), o)).collect();
-
- Ok(radium::Expr::StructInitE {
- sls: coq::term::App::new_lhs(sl.to_string()),
- components: initializers,
- })
- },
-
- _ => {
- // TODO
- Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support this kind of aggregate rvalue (got: {:?})",
- rval
- ),
- })
- },
- }
- },
-
- Rvalue::Cast(kind, op, to_ty) => {
- let op_ty = self.get_type_of_operand(op);
- let op_st = self.ty_translator.translate_type_to_syn_type(op_ty)?;
- let op_ot = op_st.into();
-
- let translated_op = self.translate_operand(op, true)?;
-
- let target_st = self.ty_translator.translate_type_to_syn_type(*to_ty)?;
- let target_ot = target_st.into();
-
- match kind {
- mir::CastKind::PointerCoercion(x) => {
- match x {
- ty::adjustment::PointerCoercion::MutToConstPointer => {
- // this is a NOP in our model
- Ok(translated_op)
- },
-
- ty::adjustment::PointerCoercion::ArrayToPointer
- | ty::adjustment::PointerCoercion::ClosureFnPointer(_)
- | ty::adjustment::PointerCoercion::ReifyFnPointer
- | ty::adjustment::PointerCoercion::UnsafeFnPointer
- | ty::adjustment::PointerCoercion::Unsize => {
- Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support this kind of pointer coercion (got: {:?})",
- rval
- ),
- })
- },
- }
- },
-
- mir::CastKind::DynStar => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support dyn* cast".to_owned(),
- }),
-
- mir::CastKind::IntToInt => {
- // Cast integer to integer
- Ok(radium::Expr::UnOp {
- o: radium::Unop::Cast(target_ot),
- ot: op_ot,
- e: Box::new(translated_op),
- })
- },
-
- mir::CastKind::IntToFloat => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support int-to-float cast".to_owned(),
- }),
-
- mir::CastKind::FloatToInt => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support float-to-int cast".to_owned(),
- }),
-
- mir::CastKind::FloatToFloat => Err(TranslationError::UnsupportedFeature {
- description: "RefinedRust does currently not support float-to-float cast".to_owned(),
- }),
-
- mir::CastKind::PtrToPtr => {
- match (op_ty.kind(), to_ty.kind()) {
- (TyKind::RawPtr(_), TyKind::RawPtr(_)) => {
- // Casts between raw pointers are NOPs for us
- Ok(translated_op)
- },
-
- _ => {
- // TODO: any other cases we should handle?
- Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support ptr-to-ptr cast (got: {:?})",
- rval
- ),
- })
- },
- }
- },
-
- mir::CastKind::FnPtrToPtr => Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support fnptr-to-ptr cast (got: {:?})",
- rval
- ),
- }),
-
- mir::CastKind::Transmute => Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support transmute cast (got: {:?})",
- rval
- ),
- }),
-
- mir::CastKind::PointerExposeAddress => {
- // Cast pointer to integer
- Ok(radium::Expr::UnOp {
- o: radium::Unop::Cast(target_ot),
- ot: radium::OpType::Ptr,
- e: Box::new(translated_op),
- })
- },
-
- mir::CastKind::PointerFromExposedAddress => Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support this kind of cast (got: {:?})",
- rval
- ),
- }),
- }
- },
-
- Rvalue::CopyForDeref(_)
- | Rvalue::Len(..)
- | Rvalue::Repeat(..)
- | Rvalue::ThreadLocalRef(..)
- | Rvalue::ShallowInitBox(_, _) => Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support this kind of rvalue (got: {:?})",
- rval
- ),
- }),
- }
- }
-
- /// Make a trivial place accessing `local`.
- fn make_local_place(&self, local: Local) -> Place<'tcx> {
- Place {
- local,
- projection: self.env.tcx().mk_place_elems(&[]),
- }
- }
-
- /// Translate an operand.
- /// This will either generate an lvalue (in case of Move or Copy) or an rvalue (in most cases
- /// of Constant). How this is used depends on the context. (e.g., Use of an integer constant
- /// does not typecheck, and produces a stuck program).
- fn translate_operand(
- &mut self,
- op: &Operand<'tcx>,
- to_rvalue: bool,
- ) -> Result<radium::Expr, TranslationError<'tcx>> {
- match op {
- // In Caesium: typed_place needs deref (not use) for place accesses.
- // use is used top-level to convert an lvalue to an rvalue, which is why we use it here.
- Operand::Copy(place) | Operand::Move(place) => {
- // check if this goes to a temporary of a checked op
- let place_kind = if self.checked_op_temporaries.contains_key(&place.local) {
- assert!(place.projection.len() == 1);
-
- let ProjectionElem::Field(f, _0) = place.projection[0] else {
- unreachable!("invariant violation for access to checked op temporary");
- };
-
- if f.index() != 0 {
- // make this a constant false -- our semantics directly checks for overflows
- // and otherwise throws UB.
- return Ok(radium::Expr::Literal(radium::Literal::Bool(false)));
- }
-
- // access to the result of the op
- self.make_local_place(place.local)
- } else {
- *place
- };
-
- let translated_place = self.translate_place(&place_kind)?;
- let ty = self.get_type_of_place(place);
-
- let st = self.ty_translator.translate_type_to_syn_type(ty.ty)?;
-
- if to_rvalue {
- Ok(radium::Expr::Use {
- ot: st.into(),
- e: Box::new(translated_place),
- })
- } else {
- Ok(translated_place)
- }
- },
- Operand::Constant(constant) => {
- // TODO: possibly need different handling of the rvalue flag
- // when this also handles string literals etc.
- return self.translate_constant(constant.as_ref());
- },
- }
- }
-
- /// Resolve the trait requirements of a function call.
- /// The target of the call, [did], should have been resolved as much as possible,
- /// as the requirements of a call can be different depending on which impl we consider.
- fn resolve_trait_requirements_of_call(
- &self,
- did: DefId,
- params: ty::GenericArgsRef<'tcx>,
- ) -> Result<Vec<radium::TraitReqInst<'def, Ty<'tcx>>>, TranslationError<'tcx>> {
- let mut scope = self.ty_translator.scope.borrow_mut();
- let mut state = types::STInner::InFunction(&mut scope);
- self.trait_registry.resolve_trait_requirements_in_state(&mut state, did, params)
- }
-
- /// Translate the use of an `FnDef`, registering that the current function needs to link against
- /// a particular monomorphization of the used function.
- /// Is guaranteed to return a `radium::Expr::CallTarget` with the parameter instantiation of
- /// this function annotated.
- fn translate_fn_def_use(&mut self, ty: Ty<'tcx>) -> Result<radium::Expr, TranslationError<'tcx>> {
- let TyKind::FnDef(defid, params) = ty.kind() else {
- return Err(TranslationError::UnknownError("not a FnDef type".to_owned()));
- };
-
- let current_param_env: ty::ParamEnv<'tcx> = self.env.tcx().param_env(self.proc.get_id());
-
- // Check whether we are calling into a trait method.
- // This works since we did not resolve concrete instances, so this is always an abstract
- // reference to the trait.
- let calling_trait = self.env.tcx().trait_of_item(*defid);
-
- // Check whether we are calling a plain function or a trait method
- let Some(calling_trait) = calling_trait else {
- // resolve the trait requirements
- let trait_spec_terms = self.resolve_trait_requirements_of_call(*defid, params)?;
-
- // track that we are using this function and generate the Coq location name
- let (code_param_name, ty_hint, lft_hint) =
- self.register_use_procedure(*defid, vec![], params, trait_spec_terms)?;
-
- let ty_hint = ty_hint.into_iter().map(|x| radium::RustType::of_type(&x)).collect();
-
- return Ok(radium::Expr::CallTarget(code_param_name, ty_hint, lft_hint));
- };
-
- // Otherwise, we are calling a trait method
- // Resolve the trait instance using trait selection
- let Some((resolved_did, resolved_params, kind)) =
- resolution::resolve_assoc_item(self.env.tcx(), current_param_env, *defid, params)
- else {
- return Err(TranslationError::TraitResolution(format!("Could not resolve trait {:?}", defid)));
- };
-
- info!(
- "Resolved trait method {:?} as {:?} with substs {:?} and kind {:?}",
- defid, resolved_did, resolved_params, kind
- );
-
- match kind {
- resolution::TraitResolutionKind::UserDefined => {
- // We can statically resolve the particular trait instance,
- // but need to apply the spec to the instance's spec attributes
-
- // resolve the trait requirements
- let trait_spec_terms =
- self.resolve_trait_requirements_of_call(resolved_did, resolved_params)?;
-
- let (param_name, ty_hint, lft_hint) =
- self.register_use_procedure(resolved_did, vec![], resolved_params, trait_spec_terms)?;
- let ty_hint = ty_hint.into_iter().map(|x| radium::RustType::of_type(&x)).collect();
-
- Ok(radium::Expr::CallTarget(param_name, ty_hint, lft_hint))
- },
-
- resolution::TraitResolutionKind::Param => {
- // In this case, we have already applied it to the spec attribute
-
- // resolve the trait requirements
- let trait_spec_terms = self.resolve_trait_requirements_of_call(*defid, params)?;
-
- let (param_name, ty_hint, lft_hint) =
- self.register_use_trait_method(resolved_did, resolved_params, trait_spec_terms)?;
- let ty_hint = ty_hint.into_iter().map(|x| radium::RustType::of_type(&x)).collect();
-
- Ok(radium::Expr::CallTarget(param_name, ty_hint, lft_hint))
- },
-
- resolution::TraitResolutionKind::Closure => {
- // TODO: here, we should first generate an instance of the trait
- //let body = self.env.tcx().instance_mir(middle::ty::InstanceDef::Item(resolved_did));
- //let body = self.env.tcx().instance_mir(middle::ty::InstanceDef::FnPtrShim(*defid, ty));
- //info!("closure body: {:?}", body);
-
- //FunctionTranslator::dump_body(body);
-
- //let res_result = ty::Instance::resolve(self.env.tcx(), callee_param_env, *defid, params);
- //info!("Resolution {:?}", res_result);
-
- // the args are just the closure args. We can ignore them.
- let _clos_args = resolved_params.as_closure();
-
- // resolve the trait requirements
- let trait_spec_terms = self.resolve_trait_requirements_of_call(*defid, params)?;
-
- let (param_name, ty_hint, lft_hint) =
- self.register_use_procedure(resolved_did, vec![], ty::List::empty(), trait_spec_terms)?;
- let ty_hint = ty_hint.into_iter().map(|x| radium::RustType::of_type(&x)).collect();
-
- Ok(radium::Expr::CallTarget(param_name, ty_hint, lft_hint))
- },
- }
- }
-
- /// Translate a scalar at a specific type to a `radium::Expr`.
- // TODO: Use `TryFrom` instead
- fn translate_scalar(
- &mut self,
- sc: &Scalar,
- ty: Ty<'tcx>,
- ) -> Result<radium::Expr, TranslationError<'tcx>> {
- // TODO: Use `TryFrom` instead
- fn translate_literal<'tcx, T, U>(
- sc: Result<T, U>,
- fptr: fn(T) -> radium::Literal,
- ) -> Result<radium::Expr, TranslationError<'tcx>> {
- sc.map_or(Err(TranslationError::InvalidLayout), |lit| Ok(radium::Expr::Literal(fptr(lit))))
- }
-
- match ty.kind() {
- TyKind::Bool => translate_literal(sc.to_bool(), radium::Literal::Bool),
-
- TyKind::Int(it) => match it {
- ty::IntTy::I8 => translate_literal(sc.to_i8(), radium::Literal::I8),
- ty::IntTy::I16 => translate_literal(sc.to_i16(), radium::Literal::I16),
- ty::IntTy::I32 => translate_literal(sc.to_i32(), radium::Literal::I32),
- ty::IntTy::I128 => translate_literal(sc.to_i128(), radium::Literal::I128),
-
- // For Radium, the pointer size is 8 bytes
- ty::IntTy::I64 | ty::IntTy::Isize => translate_literal(sc.to_i64(), radium::Literal::I64),
- },
-
- TyKind::Uint(it) => match it {
- ty::UintTy::U8 => translate_literal(sc.to_u8(), radium::Literal::U8),
- ty::UintTy::U16 => translate_literal(sc.to_u16(), radium::Literal::U16),
- ty::UintTy::U32 => translate_literal(sc.to_u32(), radium::Literal::U32),
- ty::UintTy::U128 => translate_literal(sc.to_u128(), radium::Literal::U128),
-
- // For Radium, the pointer is 8 bytes
- ty::UintTy::U64 | ty::UintTy::Usize => translate_literal(sc.to_u64(), radium::Literal::U64),
- },
-
- TyKind::Char => translate_literal(sc.to_char(), radium::Literal::Char),
-
- TyKind::FnDef(_, _) => self.translate_fn_def_use(ty),
-
- TyKind::Tuple(tys) => {
- if tys.is_empty() {
- return Ok(radium::Expr::Literal(radium::Literal::ZST));
- }
-
- Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support compound construction of tuples using literals (got: {:?})",
- ty
- ),
- })
- },
-
- TyKind::Ref(_, _, _) => match sc {
- Scalar::Int(_) => unreachable!(),
-
- Scalar::Ptr(pointer, _) => {
- let glob_alloc = self.env.tcx().global_alloc(pointer.provenance);
- match glob_alloc {
- middle::mir::interpret::GlobalAlloc::Static(did) => {
- info!(
- "Found static GlobalAlloc {:?} for Ref scalar {:?} at type {:?}",
- did, sc, ty
- );
-
- let s = self.const_registry.get_static(did)?;
- self.collected_statics.insert(did);
- Ok(radium::Expr::Literal(radium::Literal::Loc(s.loc_name.clone())))
- },
- middle::mir::interpret::GlobalAlloc::Memory(alloc) => {
- // TODO: this is needed
- Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support GlobalAlloc {:?} for scalar {:?} at type {:?}",
- glob_alloc, sc, ty
- ),
- })
- },
- _ => Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support GlobalAlloc {:?} for scalar {:?} at type {:?}",
- glob_alloc, sc, ty
- ),
- }),
- }
- },
- },
-
- _ => Err(TranslationError::UnsupportedFeature {
- description: format!(
- "RefinedRust does currently not support layout for const value: (got: {:?})",
- ty
- ),
- }),
- }
- }
-
- /// Translate a constant value from const evaluation.
- fn translate_constant_value(
- &mut self,
- v: mir::interpret::ConstValue<'tcx>,
- ty: Ty<'tcx>,
- ) -> Result<radium::Expr, TranslationError<'tcx>> {
- match v {
- ConstValue::Scalar(sc) => self.translate_scalar(&sc, ty),
- ConstValue::ZeroSized => {
- // TODO are there more special cases we need to handle somehow?
- match ty.kind() {
- TyKind::FnDef(_, _) => {
- info!("Translating ZST val for function call target: {:?}", ty);
- self.translate_fn_def_use(ty)
- },
- _ => Ok(radium::Expr::Literal(radium::Literal::ZST)),
- }
- },
- _ => {
- // TODO: do we actually care about this case or is this just something that can
- // appear as part of CTFE/MIRI?
- Err(TranslationError::UnsupportedFeature {
- description: format!("Unsupported Constant: ConstValue; {:?}", v),
- })
- },
- }
- }
-
- /// Translate a Constant to a `radium::Expr`.
- fn translate_constant(
- &mut self,
- constant: &Constant<'tcx>,
- ) -> Result<radium::Expr, TranslationError<'tcx>> {
- match constant.literal {
- ConstantKind::Ty(v) => {
- let const_ty = v.ty();
-
- match v.kind() {
- ConstKind::Value(v) => {
- // this doesn't contain the necessary structure anymore. Need to reconstruct using the
- // type.
- match v.try_to_scalar() {
- Some(sc) => self.translate_scalar(&sc, const_ty),
- _ => Err(TranslationError::UnsupportedFeature {
- description: format!("const value not supported: {:?}", v),
- }),
- }
- },
- _ => Err(TranslationError::UnsupportedFeature {
- description: "Unsupported ConstKind".to_owned(),
- }),
- }
- },
- ConstantKind::Val(val, ty) => self.translate_constant_value(val, ty),
- ConstantKind::Unevaluated(c, ty) => {
- // call const evaluation
- let param_env: ty::ParamEnv<'tcx> = self.env.tcx().param_env(self.proc.get_id());
- match self.env.tcx().const_eval_resolve(param_env, c, None) {
- Ok(res) => self.translate_constant_value(res, ty),
- Err(e) => match e {
- ErrorHandled::Reported(_) => Err(TranslationError::UnsupportedFeature {
- description: "Cannot interpret constant".to_owned(),
- }),
- ErrorHandled::TooGeneric => Err(TranslationError::UnsupportedFeature {
- description: "Const use is too generic".to_owned(),
- }),
- },
- }
- },
- }
- }
-
- /// Translate a place to a Caesium lvalue.
- fn translate_place(&mut self, pl: &Place<'tcx>) -> Result<radium::Expr, TranslationError<'tcx>> {
- // Get the type of the underlying local. We will use this to
- // get the necessary layout information for dereferencing
- let mut cur_ty = self.get_type_of_local(pl.local).map(PlaceTy::from_ty)?;
-
- let local_name = self
- .variable_map
- .get(&pl.local)
- .ok_or_else(|| TranslationError::UnknownVar(format!("{:?}", pl.local)))?;
-
- let mut acc_expr = radium::Expr::Var(local_name.to_string());
-
- // iterate in evaluation order
- for it in pl.projection {
- match &it {
- ProjectionElem::Deref => {
- // use the type of the dereferencee
- let st = self.ty_translator.translate_type_to_syn_type(cur_ty.ty)?;
- acc_expr = radium::Expr::Deref {
- ot: st.into(),
- e: Box::new(acc_expr),
- };
- },
- ProjectionElem::Field(f, _) => {
- // `t` is the type of the field we are accessing!
- let lit = self.ty_translator.generate_structlike_use(cur_ty.ty, cur_ty.variant_index)?;
- // TODO: does not do the right thing for accesses to fields of zero-sized objects.
- let struct_sls = lit.map_or(radium::SynType::Unit, |x| x.generate_raw_syn_type_term());
- let name = self.ty_translator.translator.get_field_name_of(
- *f,
- cur_ty.ty,
- cur_ty.variant_index.map(abi::VariantIdx::as_usize),
- )?;
-
- acc_expr = radium::Expr::FieldOf {
- e: Box::new(acc_expr),
- name,
- sls: struct_sls.to_string(),
- };
- },
- ProjectionElem::Index(_v) => {
- //TODO
- return Err(TranslationError::UnsupportedFeature {
- description: "places: implement index access".to_owned(),
- });
- },
- ProjectionElem::ConstantIndex { .. } => {
- //TODO
- return Err(TranslationError::UnsupportedFeature {
- description: "places: implement const index access".to_owned(),
- });
- },
- ProjectionElem::Subslice { .. } => {
- return Err(TranslationError::UnsupportedFeature {
- description: "places: implement subslicing".to_owned(),
- });
- },
- ProjectionElem::Downcast(_, variant_idx) => {
- info!("Downcast of ty {:?} to {:?}", cur_ty, variant_idx);
- if let ty::TyKind::Adt(def, args) = cur_ty.ty.kind() {
- if def.is_enum() {
- let enum_use = self.ty_translator.generate_enum_use(*def, args.iter())?;
- let els = enum_use.generate_raw_syn_type_term();
-
- let variant_name = types::TX::get_variant_name_of(cur_ty.ty, *variant_idx)?;
-
- acc_expr = radium::Expr::EnumData {
- els: els.to_string(),
- variant: variant_name,
- e: Box::new(acc_expr),
- }
- } else {
- return Err(TranslationError::UnknownError(
- "places: ADT downcasting on non-enum type".to_owned(),
- ));
- }
- } else {
- return Err(TranslationError::UnknownError(
- "places: ADT downcasting on non-enum type".to_owned(),
- ));
- }
- },
- ProjectionElem::OpaqueCast(_) => {
- return Err(TranslationError::UnsupportedFeature {
- description: "places: implement opaque casts".to_owned(),
- });
- },
- };
- // update cur_ty
- cur_ty = cur_ty.projection_ty(self.env.tcx(), it);
- }
- info!("translating place {:?} to {:?}", pl, acc_expr);
- Ok(acc_expr)
- }
-
- /// Get the type of a local in a body.
- fn get_type_of_local(&self, local: Local) -> Result<Ty<'tcx>, TranslationError<'tcx>> {
- self.proc
- .get_mir()
- .local_decls
- .get(local)
- .map(|decl| decl.ty)
- .ok_or_else(|| TranslationError::UnknownVar(String::new()))
- }
-
- /// Get the type of a place expression.
- fn get_type_of_place(&self, pl: &Place<'tcx>) -> PlaceTy<'tcx> {
- pl.ty(&self.proc.get_mir().local_decls, self.env.tcx())
- }
-
- /// Get the type of a const.
- fn get_type_of_const(cst: &Constant<'tcx>) -> Ty<'tcx> {
- match cst.literal {
- ConstantKind::Ty(cst) => cst.ty(),
- ConstantKind::Val(_, ty) | ConstantKind::Unevaluated(_, ty) => ty,
- }
- }
-
- /// Get the type of an operand.
- fn get_type_of_operand(&self, op: &Operand<'tcx>) -> Ty<'tcx> {
- op.ty(&self.proc.get_mir().local_decls, self.env.tcx())
- }
-}
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 2ab43fcf7451fd268e46817b37cfdbde8cf68149..b704a46a28b7796eb81c62c272492cd06feb37b6 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -8,6 +8,7 @@
#![feature(box_patterns)]
#![feature(let_chains)]
#![feature(rustc_private)]
+
mod attrs;
mod base;
mod body;
diff --git a/rr_frontend/translation/src/regions/assignment.rs b/rr_frontend/translation/src/regions/assignment.rs
index 8676d47c17299dfc776182969971e605061fe232..f7583c34e2f424939256ff6e4780f4d935d20bb2 100644
--- a/rr_frontend/translation/src/regions/assignment.rs
+++ b/rr_frontend/translation/src/regions/assignment.rs
@@ -6,24 +6,19 @@
//! Provides functionality for generating lifetime annotations for assignments.
-use std::collections::{BTreeMap, HashMap, HashSet};
+use std::collections::HashSet;
-use derive_more::{Constructor, Debug};
use log::{info, warn};
-use rr_rustc_interface::hir::def_id::DefId;
use rr_rustc_interface::middle::mir::tcx::PlaceTy;
-use rr_rustc_interface::middle::mir::{BasicBlock, BorrowKind, Location, Rvalue};
+use rr_rustc_interface::middle::mir::{BorrowKind, Location, Rvalue};
use rr_rustc_interface::middle::ty;
-use rr_rustc_interface::middle::ty::{Ty, TyCtxt, TyKind, TypeFoldable};
-use ty::TypeSuperFoldable;
+use rr_rustc_interface::middle::ty::{Ty, TypeFoldable};
use crate::base::{self, Region};
use crate::environment::borrowck::facts;
use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::arg_folder::ty_instantiate;
+use crate::environment::Environment;
use crate::regions::inclusion_tracker::{self, InclusionTracker};
-use crate::regions::EarlyLateRegionMap;
use crate::{regions, types};
/// Generate inclusions for a strong update assignment.
diff --git a/rr_frontend/translation/src/regions/calls.rs b/rr_frontend/translation/src/regions/calls.rs
index c0fb2db5321c0a8738d7174ab3d30b5da8ce2267..8e3b93148993d1a3ad22d1f324b4035d31faf907 100644
--- a/rr_frontend/translation/src/regions/calls.rs
+++ b/rr_frontend/translation/src/regions/calls.rs
@@ -6,40 +6,35 @@
//! Provides functionality for generating lifetime annotations for calls.
-use std::collections::{BTreeMap, HashMap, HashSet};
+use std::collections::{HashMap, HashSet};
-use derive_more::{Constructor, Debug};
+use derive_more::Debug;
use log::{info, warn};
-use rr_rustc_interface::hir::def_id::DefId;
-use rr_rustc_interface::middle::mir::tcx::PlaceTy;
-use rr_rustc_interface::middle::mir::{BasicBlock, BorrowKind, Location, Rvalue};
+use rr_rustc_interface::middle::mir::Location;
use rr_rustc_interface::middle::ty;
-use rr_rustc_interface::middle::ty::{Ty, TyCtxt, TyKind, TypeFoldable, TypeFolder};
-use ty::TypeSuperFoldable;
+use rr_rustc_interface::middle::ty::TypeFolder;
-use crate::base::{self, Region};
use crate::environment::borrowck::facts;
use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::arg_folder::ty_instantiate;
-use crate::regions::inclusion_tracker::{self, InclusionTracker};
+use crate::environment::{polonius_info, Environment};
+use crate::regions::inclusion_tracker::InclusionTracker;
use crate::regions::EarlyLateRegionMap;
-use crate::{regions, types};
+use crate::{base, regions, types};
// solve the constraints for the new_regions
// we first identify what kinds of constraints these new regions are subject to
#[derive(Debug)]
pub enum CallRegionKind {
// this is just an intersection of local regions.
- Intersection(HashSet<Region>),
+ Intersection(HashSet<base::Region>),
// this is equal to a specific region
- EqR(Region),
+ EqR(base::Region),
}
pub struct CallRegions {
- pub early_regions: Vec<Region>,
- pub late_regions: Vec<Region>,
- pub classification: HashMap<Region, CallRegionKind>,
+ pub early_regions: Vec<base::Region>,
+ pub late_regions: Vec<base::Region>,
+ pub classification: HashMap<base::Region, CallRegionKind>,
}
// `substs` are the substitutions for the early-bound regions
@@ -108,7 +103,7 @@ pub fn compute_call_regions<'tcx>(
}
}
// first sort this to enable cycle resolution
- let mut new_regions_sorted: Vec<Region> = new_regions.iter().copied().collect();
+ let mut new_regions_sorted: Vec<base::Region> = new_regions.iter().copied().collect();
new_regions_sorted.sort();
// identify the late-bound regions
diff --git a/rr_frontend/translation/src/regions/composite.rs b/rr_frontend/translation/src/regions/composite.rs
index f473b8ab42b449393fabef293832f720bb2084c7..2865cc38f28adde37f50d1fedbe1e5643bf12304 100644
--- a/rr_frontend/translation/src/regions/composite.rs
+++ b/rr_frontend/translation/src/regions/composite.rs
@@ -6,25 +6,17 @@
//! Provides functionality for generating lifetime annotations for composite expressions.
-use std::collections::{BTreeMap, HashMap, HashSet};
+use std::collections::HashSet;
-use derive_more::{Constructor, Debug};
use log::{info, warn};
-use rr_rustc_interface::hir::def_id::DefId;
-use rr_rustc_interface::middle::mir::tcx::PlaceTy;
-use rr_rustc_interface::middle::mir::{BasicBlock, BorrowKind, Location, Rvalue};
+use rr_rustc_interface::middle::mir::Location;
use rr_rustc_interface::middle::ty;
-use rr_rustc_interface::middle::ty::{Ty, TyCtxt, TyKind, TypeFoldable, TypeFolder};
-use ty::TypeSuperFoldable;
+use rr_rustc_interface::middle::ty::{Ty, TypeFolder};
-use crate::base::{self, Region};
use crate::environment::borrowck::facts;
-use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::arg_folder::ty_instantiate;
-use crate::regions::inclusion_tracker::{self, InclusionTracker};
-use crate::regions::EarlyLateRegionMap;
-use crate::{regions, types};
+use crate::environment::Environment;
+use crate::regions::inclusion_tracker::InclusionTracker;
+use crate::types;
/// On creating a composite value (e.g. a struct or enum), the composite value gets its own
/// Polonius regions We need to map these regions properly to the respective lifetimes.
diff --git a/rr_frontend/translation/src/regions/init.rs b/rr_frontend/translation/src/regions/init.rs
index d329ff2b999801199f4c623f3e72dea4cfa044dc..571131f5274dc5d3b4da3695aeb6adc9edaa1e87 100644
--- a/rr_frontend/translation/src/regions/init.rs
+++ b/rr_frontend/translation/src/regions/init.rs
@@ -6,21 +6,18 @@
//! Provides functionality for generating initial lifetime constraints.
-use std::collections::{BTreeMap, HashMap, HashSet};
+use std::collections::{BTreeMap, HashMap};
-use derive_more::{Constructor, Debug};
use log::{info, warn};
use rr_rustc_interface::hir::def_id::DefId;
-use rr_rustc_interface::middle::mir::tcx::PlaceTy;
use rr_rustc_interface::middle::mir::{BasicBlock, Location};
use rr_rustc_interface::middle::ty;
-use rr_rustc_interface::middle::ty::{Ty, TyCtxt, TyKind, TypeFoldable};
-use ty::TypeSuperFoldable;
+use rr_rustc_interface::middle::ty::Ty;
-use crate::base::{self, Region};
+use crate::base;
use crate::environment::borrowck::facts;
use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
+use crate::environment::{polonius_info, Environment};
use crate::regions::arg_folder::ty_instantiate;
use crate::regions::inclusion_tracker::InclusionTracker;
use crate::regions::EarlyLateRegionMap;
diff --git a/rr_frontend/translation/src/regions/mod.rs b/rr_frontend/translation/src/regions/mod.rs
index efbc908d42b6039b9560668d7ae02d73a20c294c..3a6039d326cc15413ec3307a569ebfcbe58851bf 100644
--- a/rr_frontend/translation/src/regions/mod.rs
+++ b/rr_frontend/translation/src/regions/mod.rs
@@ -15,21 +15,15 @@ pub mod init;
use std::collections::{BTreeMap, HashMap, HashSet};
-use arg_folder::ty_instantiate;
use derive_more::{Constructor, Debug};
use log::{info, warn};
-use rr_rustc_interface::hir::def_id::DefId;
-use rr_rustc_interface::middle::mir::tcx::PlaceTy;
-use rr_rustc_interface::middle::mir::{BasicBlock, Location};
use rr_rustc_interface::middle::ty;
-use rr_rustc_interface::middle::ty::{Ty, TyCtxt, TyKind, TypeFoldable};
+use rr_rustc_interface::middle::ty::TyCtxt;
use ty::TypeSuperFoldable;
-use crate::base::{self, Region};
+use crate::base::Region;
use crate::environment::borrowck::facts;
-use crate::environment::polonius_info::PoloniusInfo;
-use crate::environment::{dump_borrowck_info, polonius_info, Environment};
-use crate::regions::inclusion_tracker::InclusionTracker;
+use crate::environment::polonius_info;
/// Collect all the regions appearing in a type.
/// Data structure that maps early and late region indices inside functions to Polonius regions.