Ugly commit 26.08.

prusti-contracts/prusti-contracts-proc-macros/src/lib.rs

@@ -168,6 +168,12 @@ pub fn quantified_predicate(_tokens: TokenStream) -> TokenStream {
     TokenStream::new()
 }
 
+#[cfg(not(feature = "prusti"))]
+#[proc_macro]
+pub fn assume_allocation_never_fails(_tokens: TokenStream) -> TokenStream {
+    TokenStream::new()
+}
+
 #[cfg(not(feature = "prusti"))]
 #[proc_macro_attribute]
 pub fn refine_trait_spec(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
@@ -598,6 +604,12 @@ pub fn quantified_predicate(tokens: TokenStream) -> TokenStream {
     prusti_specs::quantified_predicate(tokens.into()).into()
 }
 
+#[cfg(feature = "prusti")]
+#[proc_macro]
+pub fn assume_allocation_never_fails(tokens: TokenStream) -> TokenStream {
+    prusti_specs::assume_allocation_never_fails(tokens.into()).into()
+}
+
 #[cfg(feature = "prusti")]
 #[proc_macro]
 pub fn closure(tokens: TokenStream) -> TokenStream {

prusti-contracts/prusti-contracts/src/lib.rs

@@ -85,6 +85,9 @@ pub use prusti_contracts_proc_macros::materialize_predicate;
 /// coming from the quantifier.
 pub use prusti_contracts_proc_macros::quantified_predicate;
 
+/// A macro that tells Prusti to assume that the allocation never fails.
+pub use prusti_contracts_proc_macros::assume_allocation_never_fails;
+
 /// A macro for writing refutations using prusti syntax
 pub use prusti_contracts_proc_macros::prusti_refute;
 
@@ -707,6 +710,12 @@ pub fn prusti_quantified_predicate<T>(_arg: T) {
     unreachable!();
 }
 
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_assume_allocation_never_fails() {
+    unreachable!();
+}
+
 #[doc(hidden)]
 #[trusted]
 pub fn prusti_resolve_range<T>(

prusti-contracts/prusti-specs/src/lib.rs

@@ -1807,6 +1807,19 @@ pub fn quantified_predicate(tokens: TokenStream) -> TokenStream {
     }
 }
 
+pub fn assume_allocation_never_fails(tokens: TokenStream) -> TokenStream {
+    if !tokens.is_empty() {
+        return syn::Error::new(
+            tokens.span(),
+            "`assume_allocation_never_fails` does not take any arguments",
+        )
+        .to_compile_error();
+    }
+    unsafe_spec_function_call(quote! {
+        prusti_assume_allocation_never_fails()
+    })
+}
+
 fn close_any_ref(tokens: TokenStream, function: TokenStream) -> TokenStream {
     parse_expressions!(tokens, syn::Token![,] => reference, witness);
     // let (reference, witness) = handle_result!(parse_two_expressions::<syn::Token![,]>(tokens));

prusti-utils/src/config.rs

@@ -153,6 +153,8 @@ lazy_static::lazy_static! {
         settings.set_default("use_snapshot_parameters_in_predicates", false).unwrap();
         settings.set_default("check_no_drops", false).unwrap();
         settings.set_default("enable_type_invariants", false).unwrap();
+        settings.set_default("allow_prusti_assume", false).unwrap();
+        settings.set_default("allow_assuming_allocation_never_fails", false).unwrap();
         settings.set_default("use_new_encoder", true).unwrap();
         settings.set_default("function_gas_amount", 2).unwrap();
         settings.set_default::<Option<u8>>("number_of_parallel_verifiers", None).unwrap();
@@ -1216,6 +1218,23 @@ pub fn check_no_drops() -> bool {
     read_setting("check_no_drops")
 }
 
+/// When enabled, allows using `prusti_assume` and `prusti_structural_assume`
+/// macros.
+///
+/// **Note:** This option is taken into account only when `unsafe_core_proof` is
+/// true.
+pub fn allow_prusti_assume() -> bool {
+    read_setting("allow_prusti_assume")
+}
+
+/// When enabled, allows using `assume_allocation_never_fails` macro.
+///
+/// **Note:** This option is taken into account only when `unsafe_core_proof` is
+/// true.
+pub fn allow_assuming_allocation_never_fails() -> bool {
+    read_setting("allow_assuming_allocation_never_fails")
+}
+
 /// When enabled, Prusti uses the new VIR encoder.
 ///
 /// This is a temporary configuration flag.

prusti-viper/src/encoder/errors/error_manager.rs

@@ -244,6 +244,8 @@ pub enum ErrorCtxt {
     CheckedBinaryOpPrecondition,
     /// Materializing a predicate for purification algorithm failed.
     MaterializePredicate,
+    /// An unexpected failure while assuming that the allocation cannot fail.
+    UnexpectedAssumeAllocationNeverFails,
     // /// Permission error when dereferencing a raw pointer.
     // EnsureOwnedPredicate,
 }

prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/common/mod.rs

@@ -1170,6 +1170,17 @@ pub(in super::super::super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v>:
             BuiltinFunc::BuildingFracRefPredicate => {
                 unreachable!("FracRef should have been already built.")
             }
+            BuiltinFunc::AllocationNeverFails => {
+                let return_type = self.type_to_snapshot(lowerer, &app.return_type)?;
+                let call = lowerer.create_domain_func_app(
+                    "AllocationNeverFails",
+                    "allocation_never_fails",
+                    Vec::new(),
+                    return_type,
+                    app.position,
+                )?;
+                self.ensure_bool_expression(lowerer, app.get_type(), call, expect_math_bool)
+            }
         }
     }
 

prusti-viper/src/encoder/mir/procedures/encoder/mod.rs

@@ -4406,6 +4406,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                         .set_statement_error_ctxt(stmt, span, error_ctxt, self.def_id)?;
 
                 if assumption.is_structural || self.check_mode.check_specifications() {
+                    assert!(config::allow_prusti_assume(), "TODO: A proper error message that `allow_prusti_assume` needs to be enabled.");
                     encoded_statements.push(stmt);
                 }
 
@@ -5520,6 +5521,27 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> {
                             encoded_statements.push(statement);
                             Ok(true)
                         }
+                        "prusti_contracts::prusti_assume_allocation_never_fails" => {
+                            assert!(
+                                config::allow_assuming_allocation_never_fails(),
+                                "TODO: A proper error message that allow_assuming_allocation_never_fails needs to be enabled."
+                            );
+                            let assume = vir_high::Statement::assume_no_pos(
+                                vir_high::Expression::builtin_func_app_no_pos(
+                                    vir_high::BuiltinFunc::AllocationNeverFails,
+                                    Vec::new(),
+                                    Vec::new(),
+                                    vir_high::Type::Bool,
+                                ),
+                            );
+                            let statement = self.set_statement_error(
+                                location,
+                                ErrorCtxt::UnexpectedAssumeAllocationNeverFails,
+                                assume,
+                            )?;
+                            encoded_statements.push(statement);
+                            Ok(true)
+                        }
                         function_name => unreachable!("function: {}", function_name),
                     }
                 } else {

prusti-viper/src/encoder/mir/pure/interpreter/interpreter_high.rs

@@ -1064,6 +1064,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> {
                 )?;
                 subst_with(expr)
             }
+            "prusti_contracts::allocation_never_fails" => {
+                builtin((AllocationNeverFails, vir_high::Type::Bool))
+            }
             _ => Ok(None),
         }
     }

vir/defs/high/ast/expression.rs

@@ -303,6 +303,8 @@ pub enum BuiltinFunc {
     BuildingUniqueRefPredicate,
     /// A function represents FracRef with its arguments not yet properly typed.
     BuildingFracRefPredicate,
+    /// A function that signales whether allocation can fail.
+    AllocationNeverFails,
 }
 
 #[display(fmt = "__builtin__{}({})", function, "display::cjoin(arguments)")]