Merge pull request creusot-rs#802 from xldenis/no-synthetics

Author: xldenis

creusot/src/translation/function.rs

@@ -75,8 +75,6 @@ pub struct BodyTranslator<'body, 'tcx> {
     assertions: IndexMap<DefId, Term<'tcx>>,
 
     borrows: Option<Rc<BorrowSet<'tcx>>>,
-
-    synthetic_locals: Vec<(Local, Ty<'tcx>)>,
 }
 
 impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
@@ -131,7 +129,6 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
             invariants,
             assertions,
             borrows,
-            synthetic_locals: Vec::new(),
         }
     }
 
@@ -190,8 +187,7 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
     }
 
     fn translate_vars(&mut self) -> Vec<(LocalIdent, Span, Ty<'tcx>)> {
-        let mut vars =
-            Vec::with_capacity(self.body.local_decls.len() + self.synthetic_locals.len());
+        let mut vars = Vec::with_capacity(self.body.local_decls.len());
 
         for (loc, decl) in self.body.local_decls.iter_enumerated() {
             if self.erased_locals.contains(loc) {
@@ -202,10 +198,6 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
             vars.push((ident, decl.source_info.span, decl.ty))
         }
 
-        for (loc, ty) in self.synthetic_locals.iter() {
-            vars.push((LocalIdent::anon(*loc), DUMMY_SP, *ty));
-        }
-
         vars
     }
 
@@ -291,13 +283,6 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
         id
     }
 
-    fn fresh_local(&mut self, ty: Ty<'tcx>) -> Local {
-        let id = self.body.local_decls.len() + self.synthetic_locals.len();
-        let local = Local::from_usize(id);
-        self.synthetic_locals.push((local, ty));
-        local
-    }
-
     fn resolve_locals(&mut self, mut locals: BitSet<Local>) {
         locals.subtract(&self.erased_locals.to_hybrid());
 

creusot/src/translation/function/statement.rs

@@ -200,10 +200,8 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             let lhs_ty = place.ty(self.body, self.tcx).ty;
             if !place.is_indirect() && need_resolve_before.contains(place.local)
                 && let Some((id, subst)) = super::resolve_predicate_of(self.ctx, self.param_env(), lhs_ty) {
-                let tmp_local: Place = self.fresh_local(lhs_ty).into();
-                self.emit_assignment(&tmp_local, RValue::Expr(rval));
                 self.emit_statement(fmir::Statement::Resolve(id, subst, *place));
-                self.emit_assignment(place, RValue::Expr(Expr::Place(tmp_local)));
+                self.emit_assignment(place, RValue::Expr(rval));
             } else {
                 self.emit_assignment(place, RValue::Expr(rval));
             }

creusot/tests/should_succeed/all_zero.mlcfg

@@ -182,7 +182,6 @@ module AllZero_AllZero
   var _14 : ();
   var _15 : ();
   var _16 : ();
-  var _17 : borrowed (AllZero_List_Type.t_list);
   {
     l_1 <- l;
     goto BB0
@@ -219,10 +218,9 @@ module AllZero_AllZero
     assume { Resolve1.resolve value_11 };
     _13 <- borrow_mut ( * next_12);
     next_12 <- { next_12 with current = ( ^ _13) };
-    _17 <- _13;
-    _13 <- any borrowed (AllZero_List_Type.t_list);
     assume { Resolve0.resolve loop_l_6 };
-    loop_l_6 <- _17;
+    loop_l_6 <- _13;
+    _13 <- any borrowed (AllZero_List_Type.t_list);
     _9 <- ();
     assume { Resolve2.resolve next_12 };
     goto BB2

creusot/tests/should_succeed/all_zero/why3session.xml

@@ -7,7 +7,7 @@
 <path name=".."/><path name="all_zero.mlcfg"/>
 <theory name="AllZero_AllZero" proved="true">
  <goal name="all_zero&#39;vc" expl="VC for all_zero" proved="true">
- <proof prover="1"><result status="valid" time="0.06" steps="775"/></proof>
+ <proof prover="1"><result status="valid" time="0.06" steps="774"/></proof>
  </goal>
 </theory>
 </file>

creusot/tests/should_succeed/all_zero/why3shapes.gz

@@ -1470,7 +1470,6 @@ module Hashmap_Impl5_Add
   var _55 : Hashmap_List_Type.t_list (k, v);
   var _56 : Hashmap_List_Type.t_list (k, v);
   var _57 : ();
-  var _59 : borrowed (Hashmap_List_Type.t_list (k, v));
   {
     self_1 <- self;
     key_2 <- key;
@@ -1584,10 +1583,9 @@ module Hashmap_Impl5_Add
     tl_37 <- { tl_37 with current = ( ^ _47) };
     _46 <- borrow_mut ( * _47);
     _47 <- { _47 with current = ( ^ _46) };
-    _59 <- _46;
-    _46 <- any borrowed (Hashmap_List_Type.t_list (k, v));
     assume { Resolve1.resolve l_17 };
-    l_17 <- _59;
+    l_17 <- _46;
+    _46 <- any borrowed (Hashmap_List_Type.t_list (k, v));
     assume { Resolve1.resolve _47 };
     _32 <- ();
     assume { Resolve8.resolve tl_37 };

creusot/tests/should_succeed/hashmap.mlcfg

@@ -61,22 +61,22 @@
   <proof prover="6"><result status="valid" time="0.03" steps="142"/></proof>
   </goal>
   <goal name="add&#39;vc.13" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.56" steps="20655"/></proof>
+  <proof prover="6"><result status="valid" time="0.56" steps="20638"/></proof>
   </goal>
   <goal name="add&#39;vc.14" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.40" steps="14823"/></proof>
+  <proof prover="6"><result status="valid" time="0.40" steps="14808"/></proof>
   </goal>
   <goal name="add&#39;vc.15" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.22" steps="9199"/></proof>
+  <proof prover="6"><result status="valid" time="0.22" steps="9188"/></proof>
   </goal>
   <goal name="add&#39;vc.16" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.48" steps="17390"/></proof>
+  <proof prover="6"><result status="valid" time="0.48" steps="17371"/></proof>
   </goal>
   <goal name="add&#39;vc.17" expl="loop invariant preservation" proved="true">
-  <proof prover="6"><result status="valid" time="0.07" steps="426"/></proof>
+  <proof prover="6"><result status="valid" time="0.07" steps="424"/></proof>
   </goal>
   <goal name="add&#39;vc.18" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.22" steps="42104"/></proof>
+  <proof prover="0"><result status="valid" time="0.22" steps="42085"/></proof>
   </goal>
   <goal name="add&#39;vc.19" expl="assertion" proved="true">
   <transf name="inline_goal" proved="true" >

creusot/tests/should_succeed/hashmap/why3session.xml

@@ -212,7 +212,6 @@ module ListIndexMut_IndexMut
   var _28 : ();
   var _29 : ();
   var _30 : borrowed uint32;
-  var _31 : borrowed (ListIndexMut_List_Type.t_list);
   {
     param_l_1 <- param_l;
     param_ix_2 <- param_ix;
@@ -266,10 +265,9 @@ module ListIndexMut_IndexMut
     l_11 <- { l_11 with current = (let ListIndexMut_List_Type.C_List a b =  * l_11 in ListIndexMut_List_Type.C_List a (let ListIndexMut_Option_Type.C_Some a = ListIndexMut_List_Type.list_1 ( * l_11) in ListIndexMut_Option_Type.C_Some ( ^ n_24))) };
     _25 <- borrow_mut ( * n_24);
     n_24 <- { n_24 with current = ( ^ _25) };
-    _31 <- _25;
-    _25 <- any borrowed (ListIndexMut_List_Type.t_list);
     assume { Resolve0.resolve l_11 };
-    l_11 <- _31;
+    l_11 <- _25;
+    _25 <- any borrowed (ListIndexMut_List_Type.t_list);
     _22 <- ();
     assume { Resolve1.resolve n_24 };
     ix_12 <- ([#"../list_index_mut.rs" 63 8 63 15] ix_12 - ([#"../list_index_mut.rs" 63 14 63 15] (1 : usize)));