Merge pull request #312 from Nadrieril/stealing

charon/src/bin/charon-driver/translate/get_mir.rs

@@ -40,16 +40,20 @@ pub fn get_mir_for_def_id_and_level(
         match level {
             MirLevel::Built => {
                 let body = tcx.mir_built(local_def_id);
-                // We clone to be sure there are no problems with locked values
-                body.borrow().clone()
+                if !body.is_stolen() {
+                    return Some(body.borrow().clone());
+                }
             }
             MirLevel::Promoted => {
                 let (body, _) = tcx.mir_promoted(local_def_id);
-                // We clone to be sure there are no problems with locked values
-                body.borrow().clone()
+                if !body.is_stolen() {
+                    return Some(body.borrow().clone());
+                }
             }
-            MirLevel::Optimized => tcx.optimized_mir(def_id).clone(),
+            MirLevel::Optimized => {}
         }
+        // Use the optimized MIR if it was requested or if the requested body was stolen.
+        tcx.optimized_mir(def_id).clone()
     } else {
         // There are only two MIRs we can fetch for non-local bodies: CTFE mir for globals and
         // const fns, and optimized MIR for inlinable functions. The rest don't have MIR in the

charon/tests/ui/stealing.out

@@ -0,0 +1,22 @@
+# Final LLBC before serialization:
+
+global test_crate::SLICE  {
+    let @0: Array<(), 4 : usize>; // return
+    let @1: (); // anonymous local
+
+    @1 := ()
+    @0 := @ArrayRepeat<'_, (), 4 : usize>(move (@1))
+    drop @1
+    return
+}
+
+fn test_crate::four() -> usize
+{
+    let @0: usize; // return
+
+    @0 := const (4 : usize)
+    return
+}
+
+
+

charon/tests/ui/stealing.rs

@@ -0,0 +1,7 @@
+// Translating this needs the evaluatable MIR of `fn four()`, which steals its `mir_built` body.
+// There's no simple ordering of the translation of items that can avoid all stealing.
+static SLICE: [(); four()] = [(); 4];
+
+const fn four() -> usize {
+    2 + 2
+}