Merge pull request #892 from xldenis/borroed-ghost

Forbid the use of borrowed variables in ghost code
creusot-rs · Oct 21, 2023 · 385d5ff · 385d5ff
2 parents d7d19d8 + 45b690f
commit 385d5ff
Show file tree

Hide file tree

Showing 19 changed files with 768 additions and 635 deletions.
diff --git a/creusot/src/resolve.rs b/creusot/src/resolve.rs
@@ -160,6 +160,11 @@ impl<'body, 'tcx> EagerResolver<'body, 'tcx> {
         self.dead_locals()
     }
 
+    pub fn frozen_locals_before(&mut self, loc: Location) -> BitSet<Local> {
+        ExtendedLocation::Start(loc).seek_to(&mut self.borrows);
+        self.frozen_locals()
+    }
+
     pub fn resolved_locals_between_blocks(
         &mut self,
         from: BasicBlock,

diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs
@@ -24,7 +24,7 @@ use rustc_hir::def_id::DefId;
 use rustc_index::bit_set::BitSet;
 
 use rustc_middle::{
-    mir::{self, traversal::reverse_postorder, BasicBlock, Body, Local, Operand, Place},
+    mir::{self, traversal::reverse_postorder, BasicBlock, Body, Local, Location, Operand, Place},
     ty::{
         subst::{GenericArg, SubstsRef},
         ClosureKind::*,
@@ -167,6 +167,7 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
                     &self.locals,
                     *self.body.source_info(bb.start_location()),
                 ));
+                self.check_ghost_term(&body, bb.start_location());
                 match kind {
                     LoopSpecKind::Variant => self.emit_statement(fmir::Statement::Variant(body)),
                     LoopSpecKind::Invariant => {
@@ -334,6 +335,19 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
             .collect();
         fmir::Place { local: self.locals[&_pl.local], projection }
     }
+
+    fn check_ghost_term(&mut self, term: &Term<'tcx>, location: Location) {
+        if let Some(resolver) = &mut self.resolver {
+            let frozen = resolver.frozen_locals_before(location);
+            let free_vars = term.free_vars();
+            for f in frozen.iter() {
+                if free_vars.contains(&self.locals[&f]) {
+                    let msg = format!("Use of borrowed variable {}", self.locals[&f]);
+                    self.ctx.crash_and_error(term.span, &msg);
+                }
+            }
+        }
+    }
 }
 
 fn translate_vars<'tcx>(

diff --git a/creusot/src/translation/function/statement.rs b/creusot/src/translation/function/statement.rs
@@ -130,6 +130,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                                 .remove(def_id)
                                 .expect("Could not find body of assertion");
                             assertion.subst(&inv_subst(&self.body, &self.locals, si));
+                            self.check_ghost_term(&assertion, loc);
                             self.emit_statement(fmir::Statement::Assertion {
                                 cond: assertion,
                                 msg: "assertion".to_owned(),

diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs
@@ -77,6 +77,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                     let TyKind::Closure(def_id, _) = ty.kind() else { panic!() };
                     let mut assertion = self.assertions.remove(def_id).unwrap();
                     assertion.subst(&inv_subst(self.body, &self.locals, terminator.source_info));
+                    self.check_ghost_term(&assertion, location);
                     self.emit_ghost_assign(*destination, assertion);
                     self.emit_terminator(Terminator::Goto(target.unwrap()));
                     return;

diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs
@@ -1355,4 +1355,87 @@ impl<'tcx> Term<'tcx> {
             TermKind::Assert { cond } => cond.subst_with_inner(bound, inv_subst),
         }
     }
+
+    pub(crate) fn free_vars(&self) -> HashSet<Symbol> {
+        let mut free = HashSet::new();
+        self.free_vars_inner(&HashSet::new(), &mut free);
+        free
+    }
+
+    fn free_vars_inner(&self, bound: &HashSet<Symbol>, free: &mut HashSet<Symbol>) {
+        match &self.kind {
+            TermKind::Var(v) => {
+                if !bound.contains(v) {
+                    free.insert(*v);
+                }
+            }
+            TermKind::Lit(_) => {}
+            TermKind::Item(_, _) => {}
+            TermKind::Binary { lhs, rhs, .. } => {
+                lhs.free_vars_inner(bound, free);
+                rhs.free_vars_inner(bound, free)
+            }
+            TermKind::Unary { arg, .. } => arg.free_vars_inner(bound, free),
+            TermKind::Forall { binder, body } => {
+                let mut bound = bound.clone();
+                bound.insert(binder.0);
+
+                body.free_vars_inner(&bound, free);
+            }
+            TermKind::Exists { binder, body } => {
+                let mut bound = bound.clone();
+                bound.insert(binder.0);
+
+                body.free_vars_inner(&bound, free);
+            }
+            TermKind::Call { fun, args, .. } => {
+                fun.free_vars_inner(bound, free);
+                for arg in args {
+                    arg.free_vars_inner(bound, free);
+                }
+            }
+            TermKind::Constructor { fields, .. } => {
+                for field in fields {
+                    field.free_vars_inner(bound, free);
+                }
+            }
+            TermKind::Tuple { fields } => {
+                for field in fields {
+                    field.free_vars_inner(bound, free);
+                }
+            }
+            TermKind::Cur { term } => term.free_vars_inner(bound, free),
+            TermKind::Fin { term } => term.free_vars_inner(bound, free),
+            TermKind::Impl { lhs, rhs } => {
+                lhs.free_vars_inner(bound, free);
+                rhs.free_vars_inner(bound, free)
+            }
+            TermKind::Match { scrutinee, arms } => {
+                scrutinee.free_vars_inner(bound, free);
+                let mut bound = bound.clone();
+
+                for (pat, arm) in arms {
+                    pat.binds(&mut bound);
+                    arm.free_vars_inner(&bound, free);
+                }
+            }
+            TermKind::Let { pattern, arg, body } => {
+                arg.free_vars_inner(bound, free);
+                let mut bound = bound.clone();
+                pattern.binds(&mut bound);
+                body.free_vars_inner(&bound, free);
+            }
+            TermKind::Projection { lhs, .. } => lhs.free_vars_inner(bound, free),
+            TermKind::Old { term } => term.free_vars_inner(bound, free),
+            TermKind::Closure { body } => {
+                body.free_vars_inner(&bound, free);
+            }
+            TermKind::Absurd => {}
+            TermKind::Reborrow { cur, fin } => {
+                cur.free_vars_inner(bound, free);
+                fin.free_vars_inner(bound, free)
+            }
+            TermKind::Assert { cond } => cond.free_vars_inner(bound, free),
+        }
+    }
 }
diff --git a/creusot/tests/should_fail/bug/borrowed_ghost.rs b/creusot/tests/should_fail/bug/borrowed_ghost.rs
@@ -0,0 +1,10 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+pub fn use_borrowed() {
+    let mut x = gh! { true };
+    let r = &mut x; // x = ?, r = (gh true, x)
+    *r = gh! { !x.inner() }; // r = (gh (not (inner x)), x)
+                             // resolve r: x = gh (not (inner x))
+    proof_assert! { x.inner() == !x.inner() } // UNSOUND!
+}
diff --git a/creusot/tests/should_fail/bug/borrowed_ghost.stderr b/creusot/tests/should_fail/bug/borrowed_ghost.stderr
@@ -0,0 +1,10 @@
+error[creusot]: Use of borrowed variable x
+ --> borrowed_ghost.rs:7:10
+  |
+7 |     *r = gh! { !x.inner() }; // r = (gh (not (inner x)), x)
+  |          ^^^^^^^^^^^^^^^^^^
+  |
+  = note: this error originates in the macro `gh` (in Nightly builds, run with -Z macro-backtrace for more info)
+
+error: aborting due to previous error
+