Fail in case of missing resolve data for mutable borrows (#1690)

Author: Lysxia

creusot/src/analysis.rs

@@ -54,7 +54,7 @@ type BorrowId = usize;
 
 /// Information computed by this analysis.
 #[derive(TyEncodable, TyDecodable, Clone, Debug)]
-pub struct BodyData<'tcx> {
+pub struct BorrowData<'tcx> {
     /// Resolves before each statement and terminator
     ///
     /// For `Call` terminators, they are split in a `Call` statement and a `Goto` terminator,
@@ -72,9 +72,9 @@ pub struct BodyData<'tcx> {
     two_phase_activated: HashMap<Orphan<Location>, Vec<(Place<'tcx>, Place<'tcx>, BorrowKind)>>,
 }
 
-impl<'tcx> BodyData<'tcx> {
+impl<'tcx> BorrowData<'tcx> {
     pub fn new() -> Self {
-        BodyData {
+        BorrowData {
             resolved_at: HashMap::new(),
             resolved_between_blocks: HashMap::new(),
             two_phase_created: HashSet::new(),
@@ -262,7 +262,7 @@ pub struct Analysis<'a, 'tcx> {
     not_final_places: ResultsCursor<'a, 'tcx, NotFinalPlaces<'tcx>>,
     /// `&mut` because we also rename assertions here
     body_specs: &'a mut BodySpecs<'tcx>,
-    data: BodyData<'tcx>,
+    data: BorrowData<'tcx>,
 }
 
 impl<'a, 'tcx> HasTyCtxt<'tcx> for Analysis<'a, 'tcx> {
@@ -305,7 +305,7 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
             not_final_places: NotFinalPlaces::new(tcx, &body.body)
                 .iterate_to_fixpoint(tcx, &body.body, None)
                 .into_results_cursor(&body.body),
-            data: BodyData::new(),
+            data: BorrowData::new(),
             body_specs,
         }
     }
@@ -852,7 +852,10 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
 /// Analysis to run from crates that don't have access to creusot-contracts.
 // TODO: this will be used very soon
 #[allow(dead_code)]
-pub(crate) fn run_without_specs<'a, 'tcx>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> BodyData<'tcx> {
+pub(crate) fn run_without_specs<'a, 'tcx>(
+    tcx: TyCtxt<'tcx>,
+    def_id: LocalDefId,
+) -> BorrowData<'tcx> {
     let body = callbacks::get_body(tcx, def_id);
     let mut body_specs = BodySpecs::empty();
     let corenamer = HashMap::new();
@@ -869,7 +872,7 @@ pub(crate) fn run_with_specs<'a, 'tcx>(
     ctx: &TranslationCtx<'tcx>,
     body: &'a BodyWithBorrowckFacts<'tcx>,
     body_specs: &mut BodySpecs<'tcx>,
-) -> BodyData<'tcx> {
+) -> BorrowData<'tcx> {
     let tcx = ctx.tcx;
     let corenamer = &ctx.corenamer.borrow();
     // We take `locals` from `body_specs` and put it back later

creusot/src/translation/function.rs

@@ -2,7 +2,7 @@ mod statement;
 mod terminator;
 
 use crate::{
-    analysis::{self, BodyData, BodySpecs},
+    analysis::{self, BodySpecs, BorrowData},
     backend::ty_inv::is_tyinv_trivial,
     ctx::*,
     gather_spec_closures::LoopSpecKind,
@@ -35,7 +35,7 @@ struct BodyTranslator<'a, 'tcx> {
     body_id: BodyId,
 
     body: &'a Body<'tcx>,
-    body_data: BodyData<'tcx>,
+    borrow_data: Option<BorrowData<'tcx>>,
     typing_env: TypingEnv<'tcx>,
 
     /// Current block being generated
@@ -94,26 +94,26 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
         body_id: BodyId,
         f: F,
     ) -> R {
-        let (body, body_specs, body_data) = match body_id.def_id.as_local() {
+        let (body, body_specs, borrow_data) = match body_id.def_id.as_local() {
             Some(def_id) => {
                 let body_with_facts = ctx.body_with_facts(def_id);
                 let body = match body_id.promoted {
                     None => &body_with_facts.body,
                     Some(promoted) => body_with_facts.promoted.get(promoted).unwrap(),
                 };
                 let mut body_specs = analysis::BodySpecs::from_body(ctx, body);
-                let body_data = match body_id.promoted {
-                    None => analysis::run_with_specs(ctx, &body_with_facts, &mut body_specs),
-                    Some(_) => BodyData::new(),
+                let borrow_data = match body_id.promoted {
+                    None => Some(analysis::run_with_specs(ctx, &body_with_facts, &mut body_specs)),
+                    Some(_) => None,
                 };
-                (body, body_specs, body_data)
+                (body, body_specs, borrow_data)
             }
             None => {
                 assert!(body_id.promoted.is_none());
                 let body = ctx.tcx.mir_for_ctfe(body_id.def_id);
                 let body_specs = analysis::BodySpecs::from_body(ctx, &body);
-                let body_data = BodyData::new();
-                (body, body_specs, body_data)
+                let borrow_data = None;
+                (body, body_specs, borrow_data)
             }
         };
         let typing_env = ctx.typing_env(body_id.def_id);
@@ -129,7 +129,7 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
         f(BodyTranslator {
             body,
             body_id,
-            body_data,
+            borrow_data,
             typing_env,
             locals,
             vars,
@@ -213,7 +213,10 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
     }
 
     fn resolve_at(&mut self, loc: Location, span: Span) {
-        for place in self.body_data.remove_resolved_places_at(loc) {
+        let Some(borrow_data) = &mut self.borrow_data else {
+            return;
+        };
+        for place in borrow_data.remove_resolved_places_at(loc) {
             self.emit_resolve(place, span);
         }
     }

creusot/src/translation/function/promoted.rs

@@ -9,12 +9,13 @@ use crate::{
         pearlite::Term,
     },
 };
+use rustc_ast::Mutability;
 use rustc_middle::{
     mir::{
         BorrowKind::*, CastKind, Location, Operand::*, Place, Rvalue, SourceInfo, Statement,
         StatementKind,
     },
-    ty::{Ty, TyKind, UintTy, adjustment::PointerCoercion},
+    ty::{ConstKind, Ty, TyKind, UintTy, adjustment::PointerCoercion},
 };
 use rustc_span::Span;
 
@@ -77,11 +78,18 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                     }
                     RValue::Operand(Operand::Copy(self.translate_place(pl, span)))
                 }
+                // Special case to support const-promoted `&mut []`
+                Mut { .. } if self.borrow_data.is_none() && is_mut_ref_empty(&ty) => {
+                    self.emit_borrow(place, pl, fmir::BorrowKind::Mut, span);
+                    // No need to resolve: the length of the final value is set to 0 by the type invariant
+                    return;
+                }
                 Mut { .. } => {
-                    if self.erased_locals.contains(pl.local) || self.is_two_phase(loc) {
+                    let Some(borrow_data) = &self.borrow_data else { self.error_no_borrow_data() };
+                    if self.erased_locals.contains(pl.local) || borrow_data.is_two_phase_at(loc) {
                         return;
                     }
-                    let is_final = self.is_final_at(loc);
+                    let is_final = borrow_data.is_final_at(loc);
                     self.emit_borrow(place, pl, is_final, span);
                     return;
                 }
@@ -205,17 +213,40 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
         }
     }
 
-    fn is_two_phase(&self, loc: Location) -> bool {
-        self.body_data.is_two_phase_at(loc)
-    }
-
     pub(super) fn activate_two_phase(&mut self, loc: Location, span: Span) {
-        for (lhs, rhs, is_final) in self.body_data.remove_two_phase_activated_at(loc) {
+        let Some(borrow_data) = &mut self.borrow_data else {
+            return;
+        };
+        for (lhs, rhs, is_final) in borrow_data.remove_two_phase_activated_at(loc) {
             self.emit_borrow(lhs, rhs, is_final, span)
         }
     }
 
-    fn is_final_at(&self, loc: Location) -> fmir::BorrowKind {
-        self.body_data.is_final_at(loc)
+    /// Fail if mutable borrows are used and no borrow data is available.
+    fn error_no_borrow_data(&self) -> ! {
+        self.crash_and_error(
+            self.body.span,
+            format!(
+                "can't translate {}: no data to resolve mutable borrows",
+                self.tcx().def_path_str(self.body_id.def_id)
+            ),
+        );
     }
 }
+
+/// Check whether `ty` is of the form `&mut [T; 0]`
+fn is_mut_ref_empty<'tcx>(ty: &Ty<'tcx>) -> bool {
+    let TyKind::Ref(_, ty, Mutability::Mut) = ty.kind() else {
+        return false;
+    };
+    let TyKind::Array(_, len) = ty.kind() else {
+        return false;
+    };
+    let ConstKind::Value(value) = len.kind() else {
+        return false;
+    };
+    let Some(scalar) = value.valtree.try_to_scalar_int() else {
+        return false;
+    };
+    scalar.is_null()
+}

creusot/src/translation/function/statement.rs

@@ -184,7 +184,9 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             | TailCall { .. } => unreachable!("{:?}", terminator.kind),
         };
         // Insert blocks of resolve statements and retarget the terminator to those blocks.
-        if let Some(mut resolved) = self.body_data.remove_resolved_between_blocks(loc.block) {
+        if let Some(borrow_data) = &mut self.borrow_data
+            && let Some(mut resolved) = borrow_data.remove_resolved_between_blocks(loc.block)
+        {
             let mut retarget = HashMap::new();
             for target in term.targets_mut() {
                 match resolved.remove(target) {