Ghost macro inline (#1367)

creusot-contracts-proc/src/invariant.rs

@@ -100,7 +100,7 @@ fn filter_invariants(
     parse_push_invariant(&mut invariants, tag, invariant)?;
 
     let attrs = attrs.extract_if(0.., |attr| {
-        attr.path().get_ident().map_or(false, |i| i == "invariant" || i == "variant")
+        attr.path().get_ident().is_some_and(|i| i == "invariant" || i == "variant")
     });
     for attr in attrs {
         let i = if attr.path().get_ident().map(|i| i == "invariant").unwrap_or(false) {

creusot-contracts-proc/src/lib.rs

@@ -440,12 +440,10 @@ pub fn ghost(body: TS1) -> TS1 {
     let body = proc_macro2::TokenStream::from(ghost::ghost_preprocess(body));
     TS1::from(quote! {
         {
-            ::creusot_contracts::__stubs::ghost_from_fn({
-                #[creusot::ghost]
-                #[::creusot_contracts::pure]
-                || ::creusot_contracts::ghost::GhostBox::new({ #body })
-            },
-            ())
+            #[creusot::ghost_block]
+            {
+                ::creusot_contracts::ghost::GhostBox::new({ #body })
+            }
         }
     })
 }

creusot-contracts/src/stubs.rs

@@ -71,13 +71,6 @@ pub fn snapshot_from_fn<T: ?Sized, F: Fn() -> crate::Snapshot<T>>(_: F) -> crate
     panic!()
 }
 
-#[crate::pure]
-#[creusot::no_translate]
-#[rustc_diagnostic_item = "ghost_from_fn"]
-pub fn ghost_from_fn<T, F: FnOnce() -> T>(f: F, _arg: ()) -> T {
-    f()
-}
-
 #[logic]
 #[trusted]
 #[creusot::no_translate]

creusot/src/backend/optimization.rs

@@ -111,7 +111,7 @@ impl<'a, 'tcx> LocalUsage<'a, 'tcx> {
 
     fn visit_rvalue(&mut self, r: &RValue<'tcx>) {
         match r {
-            RValue::Ghost(t) => self.visit_term(t),
+            RValue::Snapshot(t) => self.visit_term(t),
             RValue::Borrow(_, p, _) | RValue::Ptr(p) => {
                 self.read_place(p);
                 self.read_place(p)
@@ -250,7 +250,7 @@ impl<'tcx> SimplePropagator<'tcx> {
                       self.prop.insert(l.local, op);
                       self.dead.insert(l.local);
                     }
-                Statement::Assignment(_, RValue::Ghost(_), _) => {
+                Statement::Assignment(_, RValue::Snapshot(_), _) => {
                     out_stmts.push(s)
                 }
                 Statement::Assignment(ref l, ref r, _) if self.should_erase(l.local) && r.is_pure() => {
@@ -293,7 +293,7 @@ impl<'tcx> SimplePropagator<'tcx> {
 
     fn visit_rvalue(&mut self, r: &mut RValue<'tcx>) {
         match r {
-            RValue::Ghost(t) => self.visit_term(t),
+            RValue::Snapshot(t) => self.visit_term(t),
             RValue::Ptr(p) | RValue::Borrow(_, p, _) => {
                 assert!(self.prop.get(&p.local).is_none(), "Trying to propagate borrowed variable")
             }

creusot/src/backend/optimization/invariants.rs

@@ -83,7 +83,7 @@ pub fn infer_proph_invariants<'tcx>(ctx: &TranslationCtx<'tcx>, body: &mut fmir:
                 }
                 prev_block.stmts.push(Statement::Assignment(
                     Place { local, projection: Vec::new() },
-                    RValue::Ghost(Term::call_no_normalize(
+                    RValue::Snapshot(Term::call_no_normalize(
                         tcx,
                         snap_new,
                         subst,

creusot/src/backend/program.rs

@@ -13,7 +13,6 @@ use crate::{
         wto::{weak_topological_order, Component},
         NameSupply, Namer, Why3Generator,
     },
-    contracts_items::is_ghost_closure,
     ctx::{BodyId, Dependencies},
     fmir::{self, Body, BorrowKind, Operand, TrivialInv},
     naming::ident_of,
@@ -192,9 +191,7 @@ pub fn to_why<'tcx, N: Namer<'tcx>>(
         // a closure with no contract
         || inferred_closure_spec
         // a promoted item
-        || body_id.promoted.is_some()
-        // a ghost closure
-        || is_ghost_closure(ctx.tcx, body_id.def_id());
+        || body_id.promoted.is_some();
 
     let ensures = sig.contract.ensures.into_iter().map(Condition::labelled_exp);
 
@@ -590,7 +587,7 @@ impl<'tcx> RValue<'tcx> {
 
                 Exp::var("_res")
             }
-            RValue::Ghost(t) => lower_pure(lower.ctx, lower.names, &t),
+            RValue::Snapshot(t) => lower_pure(lower.ctx, lower.names, &t),
             RValue::Borrow(_, _, _) => unreachable!(), // Handled in Statement::to_why
             RValue::UnaryOp(UnOp::PtrMetadata, op) => {
                 match op.ty(lower.ctx.tcx, lower.locals).kind() {

creusot/src/contracts_items/attributes.rs

@@ -45,7 +45,6 @@ attribute_functions! {
     [creusot::before_loop]                   => is_before_loop
     [creusot::spec::assert]                  => is_assertion
     [creusot::spec::snapshot]                => is_snapshot_closure
-    [creusot::ghost]                         => is_ghost_closure
     [creusot::decl::logic]                   => is_logic
     [creusot::decl::logic::prophetic]        => is_prophetic
     [creusot::decl::predicate]               => is_predicate

creusot/src/contracts_items/diagnostic_items.rs

@@ -78,8 +78,6 @@ contracts_items! {
         is_snapshot_deref               get_snapshot_deref
     fn GhostBox::new                     ["ghost_box_new"]
         is_ghost_new                    get_ghost_new
-    fn GhostBox::from_fn                 ["ghost_from_fn"]
-        is_ghost_from_fn                get_ghost_from_fn
     fn GhostBox::into_inner              ["ghost_box_into_inner"]
         is_ghost_into_inner             get_ghost_into_inner
     fn GhostBox::inner_logic             ["ghost_box_inner_logic"]

creusot/src/lib.rs

@@ -16,6 +16,7 @@ extern crate rustc_driver;
 extern crate rustc_errors;
 extern crate rustc_fluent_macro;
 extern crate rustc_hir;
+extern crate rustc_hir_typeck;
 extern crate rustc_index;
 extern crate rustc_infer;
 extern crate rustc_interface;
@@ -59,7 +60,6 @@ mod translation;
 use translation::*;
 mod util;
 mod validate;
-mod validate_terminates;
 mod very_stable_hash;
 
 rustc_fluent_macro::fluent_messages! { "../messages.ftl" }

creusot/src/lints.rs

@@ -9,5 +9,6 @@ pub fn register_lints(_sess: &Session, store: &mut LintStore) {
         experimental_types::EXPERIMENTAL,
         contractless_external_function::CONTRACTLESS_EXTERNAL_FUNCTION,
     ]);
+    store.register_late_pass(move |_| Box::new(crate::validate::GhostValidate {}));
     store.register_late_pass(move |_| Box::new(experimental_types::Experimental {}));
 }

creusot/src/translation.rs

@@ -19,9 +19,9 @@ use crate::{
     options::Output,
     translated_item::FileModule,
     validate::{
-        validate_impls, validate_opacity, validate_purity, validate_traits, validate_trusted,
+        validate_impls, validate_opacity, validate_purity, validate_terminates, validate_traits,
+        validate_trusted,
     },
-    validate_terminates::validate_terminates,
 };
 use ctx::TranslationCtx;
 use rustc_hir::{def::DefKind, def_id::DefId};

creusot/src/translation/fmir.rs

@@ -104,7 +104,7 @@ pub enum TrivialInv {
 
 #[derive(Clone, Debug)]
 pub enum RValue<'tcx> {
-    Ghost(Term<'tcx>),
+    Snapshot(Term<'tcx>),
     Borrow(BorrowKind, Place<'tcx>, TrivialInv),
     Operand(Operand<'tcx>),
     BinOp(BinOp, Operand<'tcx>, Operand<'tcx>),
@@ -118,7 +118,7 @@ pub enum RValue<'tcx> {
     Ptr(Place<'tcx>),
 }
 
-impl<'tcx> RValue<'tcx> {
+impl RValue<'_> {
     /// Returns false if the expression generates verification conditions
     pub fn is_pure(&self) -> bool {
         match self {
@@ -165,7 +165,7 @@ impl<'tcx> RValue<'tcx> {
             RValue::Len(_) => true,
             RValue::Array(_) => true,
             RValue::Repeat(_, _) => true,
-            RValue::Ghost(_) => true,
+            RValue::Snapshot(_) => true,
             RValue::Borrow(_, _, _) => true,
             RValue::Ptr(_) => true,
         }
@@ -415,7 +415,7 @@ pub(crate) fn super_visit_terminator<'tcx, V: FmirVisitor<'tcx>>(
 
 pub(crate) fn super_visit_rvalue<'tcx, V: FmirVisitor<'tcx>>(visitor: &mut V, rval: &RValue<'tcx>) {
     match rval {
-        RValue::Ghost(term) => {
+        RValue::Snapshot(term) => {
             visitor.visit_term(term);
         }
         RValue::Borrow(_, place, _) => {

creusot/src/translation/function.rs

@@ -3,8 +3,8 @@ use crate::{
     backend::ty_inv::is_tyinv_trivial,
     constant::from_mir_constant,
     contracts_items::{
-        get_fn_mut_impl_unnest, get_resolve_function, get_resolve_method, is_ghost_closure,
-        is_snapshot_closure, is_spec,
+        get_fn_mut_impl_unnest, get_resolve_function, get_resolve_method, is_snapshot_closure,
+        is_spec,
     },
     ctx::*,
     extended_location::ExtendedLocation,
@@ -90,8 +90,6 @@ struct BodyTranslator<'a, 'tcx> {
     assertions: IndexMap<DefId, Term<'tcx>>,
     /// Map of the `snapshot!` blocks to their translated version.
     snapshots: IndexMap<DefId, Term<'tcx>>,
-    /// Indicate that the current function is a `ghost!` closure.
-    is_ghost_closure: bool,
 
     borrows: Option<&'a BorrowSet<'tcx>>,
 
@@ -178,7 +176,6 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
             invariant_assertions: invariants.assertions,
             assertions,
             snapshots,
-            is_ghost_closure: is_ghost_closure(tcx, body_id.def_id()),
             borrows,
         })
     }
@@ -342,8 +339,8 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
         );
     }
 
-    fn emit_ghost_assign(&mut self, lhs: Place<'tcx>, rhs: Term<'tcx>, span: Span) {
-        self.emit_assignment(&lhs, fmir::RValue::Ghost(rhs), span)
+    fn emit_snapshot_assign(&mut self, lhs: Place<'tcx>, rhs: Term<'tcx>, span: Span) {
+        self.emit_assignment(&lhs, fmir::RValue::Snapshot(rhs), span)
     }
 
     fn emit_assignment(&mut self, lhs: &Place<'tcx>, rhs: RValue<'tcx>, span: Span) {
@@ -360,7 +357,7 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
     ) {
         // The assignement may, in theory, modify a variable that needs to be resolved.
         // Hence we resolve before the assignment.
-        self.resolve_places(need, &resolved);
+        self.resolve_places(need, resolved);
 
         // We resolve the destination place, if necessary
         match self.move_data().rev_lookup.find(destination.as_ref()) {