Cleanup

AeneasVerif · Sep 4, 2024 · 9bc0ccf · 9bc0ccf
1 parent 99d2cc1
commit 9bc0ccf
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 48 deletions.
diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
@@ -919,10 +919,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 Some(RawStatement::FakeRead(t_place))
             }
             StatementKind::PlaceMention(place) => {
-                // Simply accesses a place. Introduced for instance in place
-                // of `let _ = ...`. We desugar it to a fake read.
+                // Simply accesses a place, for use of the borrow checker. Introduced for instance
+                // in place of `let _ = ...`. We desugar it to a fake read.
                 let t_place = self.translate_place(span, place)?;
-
                 Some(RawStatement::FakeRead(t_place))
             }
             StatementKind::SetDiscriminant {
@@ -933,46 +932,31 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                 let variant_id = translate_variant_id(*variant_index);
                 Some(RawStatement::SetDiscriminant(t_place, variant_id))
             }
-            StatementKind::StorageLive(_) => {
-                // We ignore StorageLive
-                None
-            }
+            // We ignore StorageLive
+            StatementKind::StorageLive(_) => None,
             StatementKind::StorageDead(local) => {
                 let var_id = self.get_local(local).unwrap();
                 Some(RawStatement::StorageDead(var_id))
             }
-            StatementKind::Retag(_, _) => {
-                // This is for the stacked borrows
-                trace!("retag");
-                None
-            }
-            StatementKind::AscribeUserType(_, _) => {
-                trace!("AscribedUserType");
-                // We ignore those: they are just used by the type checker.
-                // Note that this instruction is used only in certain passes
-                // (it is not present in optimized MIR for instance).
-                None
-            }
-            StatementKind::Coverage(_) => {
-                error_or_panic!(self, span, "Unsupported statement kind: coverage");
-            }
-            StatementKind::Nop => {
-                // We ignore this statement
-                None
-            }
             StatementKind::Deinit(place) => {
                 let t_place = self.translate_place(span, place)?;
                 Some(RawStatement::Deinit(t_place))
             }
             StatementKind::Intrinsic(_) => {
                 error_or_panic!(self, span, "Unsupported statement kind: intrinsic");
             }
-            StatementKind::ConstEvalCounter => {
-                // See the doc: only used in the interpreter, to check that
-                // const code doesn't run for too long or even indefinitely.
-                // We consider it as a no-op.
-                None
-            }
+            // This is for the stacked borrows memory model.
+            StatementKind::Retag(_, _) => None,
+            // There are user-provided type annotations with no semantic effect (since we get a
+            // fully-typechecked MIR (TODO: this isn't quite true with opaque types, we should
+            // really use promoted MIR)).
+            StatementKind::AscribeUserType(_, _) => None,
+            // Used for coverage instrumentation.
+            StatementKind::Coverage(_) => None,
+            // Used in the interpreter to check that const code doesn't run for too long or even
+            // indefinitely.
+            StatementKind::ConstEvalCounter => None,
+            StatementKind::Nop => None,
         };
 
         // Add the span information

diff --git a/charon/src/transform/ullbc_to_llbc.rs b/charon/src/transform/ullbc_to_llbc.rs
@@ -1453,24 +1453,17 @@ fn opt_statement_to_nop_if_none(span: Span, opt_st: Option<tgt::Statement>) -> t
 
 fn translate_statement(st: &src::Statement) -> Option<tgt::Statement> {
     let src_span = st.span;
-    let st = match &st.content {
-        src::RawStatement::Assign(place, rvalue) => {
-            tgt::RawStatement::Assign(place.clone(), rvalue.clone())
-        }
-        src::RawStatement::FakeRead(place) => tgt::RawStatement::FakeRead(place.clone()),
+    let st = match st.content.clone() {
+        src::RawStatement::Assign(place, rvalue) => tgt::RawStatement::Assign(place, rvalue),
+        src::RawStatement::FakeRead(place) => tgt::RawStatement::FakeRead(place),
         src::RawStatement::SetDiscriminant(place, variant_id) => {
-            tgt::RawStatement::SetDiscriminant(place.clone(), *variant_id)
-        }
-        src::RawStatement::StorageDead(var_id) => {
-            // We translate a StorageDead as a drop
-            let place = Place::new(*var_id);
-            tgt::RawStatement::Drop(place)
-        }
-        src::RawStatement::Deinit(place) => {
-            // We translate a deinit as a drop
-            tgt::RawStatement::Drop(place.clone())
+            tgt::RawStatement::SetDiscriminant(place, variant_id)
         }
-        src::RawStatement::Error(s) => tgt::RawStatement::Error(s.clone()),
+        // We translate a StorageDead as a drop
+        src::RawStatement::StorageDead(var_id) => tgt::RawStatement::Drop(Place::new(var_id)),
+        // We translate a deinit as a drop
+        src::RawStatement::Deinit(place) => tgt::RawStatement::Drop(place),
+        src::RawStatement::Error(s) => tgt::RawStatement::Error(s),
     };
     Some(tgt::Statement::new(src_span, st))
 }