Merge pull request creusot-rs#803 from xldenis/better-local-names

better local names

Author: xldenis

creusot/src/backend/constant.rs

@@ -4,7 +4,7 @@ use why3::declaration::{Decl, LetDecl, LetKind, Module, ValDecl};
 
 use crate::{
     ctx::TranslatedItem,
-    translation::{constant::from_ty_const, function::closure_generic_decls},
+    translation::{constant::from_ty_const, fmir::LocalDecls, function::closure_generic_decls},
     util::{self, module_name},
 };
 
@@ -29,7 +29,7 @@ impl<'tcx> Why3Generator<'tcx> {
         let span = self.def_span(def_id);
         let res = from_ty_const(&mut self.ctx, constant, param_env, span);
         let mut names = CloneMap::new(self.tcx, def_id, CloneLevel::Body);
-        let res = res.to_why(self, &mut names, None);
+        let res = res.to_why(self, &mut names, &LocalDecls::new());
         let sig = signature_of(self, &mut names, def_id);
         let mut decls: Vec<_> = closure_generic_decls(self.tcx, def_id).collect();
         let (clones, summary) = names.to_clones(self);

creusot/src/backend/interface.rs

@@ -35,8 +35,8 @@ pub(crate) fn interface_for<'tcx>(
             if subst.as_closure().kind() == ClosureKind::FnMut {
                 sig.contract.ensures.push(
                     Exp::pure_var("unnest".into())
-                        .app_to(Exp::Current(Box::new(Exp::pure_var("_1'".into()))))
-                        .app_to(Exp::Final(Box::new(Exp::pure_var("_1'".into())))),
+                        .app_to(Exp::Current(Box::new(Exp::pure_var("_1".into()))))
+                        .app_to(Exp::Final(Box::new(Exp::pure_var("_1".into())))),
                 )
             }
         }

creusot/src/backend/place.rs

@@ -1,9 +1,9 @@
 use crate::{
-    ctx::{BodyId, CloneMap, TranslationCtx},
-    translation::LocalIdent,
+    ctx::CloneMap,
+    translation::fmir::{self, LocalDecls},
 };
 use rustc_middle::{
-    mir::{tcx::PlaceTy, HasLocalDecls, Local, Place, PlaceRef},
+    mir::{tcx::PlaceTy, Local, Place, PlaceRef},
     ty::TyKind,
 };
 use why3::{
@@ -21,36 +21,18 @@ use why3::{
 use super::Why3Generator;
 
 impl<'tcx> Why3Generator<'tcx> {
-    pub(crate) fn place_ty(&mut self, body_id: BodyId, pl: PlaceRef<'tcx>) -> PlaceTy<'tcx> {
-        let local_ty = self.body(body_id).local_decls()[pl.local].ty;
+    pub(crate) fn place_ty(
+        &mut self,
+        locals: &fmir::LocalDecls<'tcx>,
+        pl: PlaceRef<'tcx>,
+    ) -> PlaceTy<'tcx> {
+        let local_ty = locals[&pl.local].2;
         pl.projection.iter().fold(PlaceTy::from_ty(local_ty), |place_ty, &elem| {
             place_ty.projection_ty(self.tcx, elem)
         })
     }
 }
 
-impl<'tcx> TranslationCtx<'tcx> {
-    pub(crate) fn translate_local(&mut self, body_id: BodyId, loc: Local) -> LocalIdent {
-        let body = self.body(body_id);
-
-        use rustc_middle::mir::VarDebugInfoContents::Place;
-        let debug_info: Vec<_> = body
-            .var_debug_info
-            .iter()
-            .filter(|var_info| match var_info.value {
-                Place(p) => p.as_local().map(|l| l == loc).unwrap_or(false),
-                _ => false,
-            })
-            .collect();
-
-        assert!(debug_info.len() <= 1, "expected at most one debug entry for local {:?}", loc);
-        match debug_info.get(0) {
-            Some(info) => LocalIdent::dbg(loc, *info),
-            None => LocalIdent::anon(loc),
-        }
-    }
-}
-
 /// Correctly translate an assignment from one place to another. The challenge here is correctly
 /// construction the expression that assigns deep inside a structure.
 /// (_1 as Some) = P      ---> let _1 = P ??
@@ -65,7 +47,7 @@ impl<'tcx> TranslationCtx<'tcx> {
 pub(crate) fn create_assign_inner<'tcx>(
     ctx: &mut Why3Generator<'tcx>,
     names: &mut CloneMap<'tcx>,
-    body_id: BodyId,
+    locals: &LocalDecls<'tcx>,
     lhs: &Place<'tcx>,
     rhs: Exp,
 ) -> mlcfg::Statement {
@@ -84,7 +66,7 @@ pub(crate) fn create_assign_inner<'tcx>(
     for (proj, elem) in lhs.iter_projections().rev() {
         // twisted stuff
         stump = &stump[0..stump.len() - 1];
-        let place_ty = ctx.place_ty(body_id, proj);
+        let place_ty = ctx.place_ty(locals, proj);
 
         match elem {
             Deref => {
@@ -94,7 +76,7 @@ pub(crate) fn create_assign_inner<'tcx>(
                 if mutability == Mut {
                     inner = RecUp {
                         record: Box::new(translate_rplace_inner(
-                            ctx, names, body_id, lhs.local, stump,
+                            ctx, names, locals, lhs.local, stump,
                         )),
                         label: "current".into(),
                         val: Box::new(inner),
@@ -119,9 +101,7 @@ pub(crate) fn create_assign_inner<'tcx>(
                     let ctor = names.constructor(variant.def_id, subst);
                     inner = Let {
                         pattern: ConsP(ctor.clone(), field_pats),
-                        arg: Box::new(translate_rplace_inner(
-                            ctx, names, body_id, lhs.local, stump,
-                        )),
+                        arg: Box::new(translate_rplace_inner(ctx, names, locals, lhs.local, stump)),
                         body: Box::new(Constructor { ctor, args: varexps }),
                     }
                 }
@@ -139,9 +119,7 @@ pub(crate) fn create_assign_inner<'tcx>(
 
                     inner = Let {
                         pattern: TupleP(field_pats),
-                        arg: Box::new(translate_rplace_inner(
-                            ctx, names, body_id, lhs.local, stump,
-                        )),
+                        arg: Box::new(translate_rplace_inner(ctx, names, locals, lhs.local, stump)),
                         body: Box::new(Tuple(varexps)),
                     }
                 }
@@ -160,9 +138,7 @@ pub(crate) fn create_assign_inner<'tcx>(
 
                     inner = Let {
                         pattern: ConsP(cons.clone(), field_pats),
-                        arg: Box::new(translate_rplace_inner(
-                            ctx, names, body_id, lhs.local, stump,
-                        )),
+                        arg: Box::new(translate_rplace_inner(ctx, names, locals, lhs.local, stump)),
                         body: Box::new(Exp::Constructor { ctor: cons, args: varexps }),
                     }
                 }
@@ -171,12 +147,12 @@ pub(crate) fn create_assign_inner<'tcx>(
             Downcast(_, _) => {}
             Index(ix) => {
                 let set = Exp::impure_qvar(QName::from_string("Slice.set").unwrap());
-                let ix_exp = Exp::impure_var(ctx.translate_local(body_id, ix).ident());
+                let ix_exp = Exp::impure_var(locals[&ix].0.ident());
 
                 inner = Call(
                     Box::new(set),
                     vec![
-                        translate_rplace_inner(ctx, names, body_id, lhs.local, stump),
+                        translate_rplace_inner(ctx, names, locals, lhs.local, stump),
                         ix_exp,
                         inner,
                     ],
@@ -188,7 +164,10 @@ pub(crate) fn create_assign_inner<'tcx>(
         }
     }
 
-    let ident = ctx.translate_local(body_id, lhs.local);
+    if locals.get(&lhs.local).is_none() {
+        eprintln!("{lhs:?} {locals:?}");
+    }
+    let ident = locals[&lhs.local].0.clone();
     Assign { lhs: ident.ident(), rhs: inner }
 }
 
@@ -198,17 +177,20 @@ pub(crate) fn create_assign_inner<'tcx>(
 pub(crate) fn translate_rplace_inner<'tcx>(
     ctx: &mut Why3Generator<'tcx>,
     names: &mut CloneMap<'tcx>,
-    body_id: BodyId,
+    locals: &LocalDecls<'tcx>,
     loc: Local,
     proj: &[rustc_middle::mir::PlaceElem<'tcx>],
 ) -> Exp {
-    let mut inner = Exp::impure_var(ctx.translate_local(body_id, loc).ident());
+    if locals.get(&loc).is_none() {
+        eprintln!("{locals:?} {loc:?}")
+    };
+    let mut inner = Exp::impure_var(locals[&loc].0.ident());
     if proj.is_empty() {
         return inner;
     }
 
     use rustc_middle::mir::ProjectionElem::*;
-    let mut place_ty = ctx.place_ty(body_id, Place::from(loc).as_ref());
+    let mut place_ty = ctx.place_ty(locals, Place::from(loc).as_ref());
 
     for elem in proj {
         match elem {
@@ -250,7 +232,7 @@ pub(crate) fn translate_rplace_inner<'tcx>(
             Downcast(_, _) => {}
             Index(ix) => {
                 // TODO: Use [_] syntax
-                let ix_exp = Exp::impure_var(ctx.translate_local(body_id, *ix).ident());
+                let ix_exp = Exp::impure_var(locals[ix].0.ident());
                 inner = Call(
                     Box::new(Exp::impure_qvar(QName::from_string("Slice.get").unwrap())),
                     vec![inner, ix_exp],