Remove __VERIFIER_assume

Author: Patrick-6

src/concurrency/genmc/dummy.rs

@@ -241,6 +241,17 @@ impl GenmcCtx {
     ) -> InterpResult<'tcx> {
         unreachable!()
     }
+
+    /**** Blocking instructions ****/
+
+    #[allow(unused)]
+    pub(crate) fn handle_verifier_assume<'tcx>(
+        &self,
+        _machine: &MiriMachine<'tcx>,
+        _condition: bool,
+    ) -> InterpResult<'tcx, ()> {
+        unreachable!()
+    }
 }
 
 /// Other functionality not directly related to event handling
@@ -261,12 +272,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
     fn genmc_schedule_thread(&mut self) -> InterpResult<'tcx, ThreadId> {
         unreachable!()
     }
-
-    /**** Blocking instructions ****/
-
-    fn handle_genmc_verifier_assume(&mut self, _condition: &OpTy<'tcx>) -> InterpResult<'tcx> {
-        unreachable!()
-    }
 }
 
 impl VisitProvenance for GenmcCtx {

src/concurrency/genmc/mod.rs

@@ -696,6 +696,17 @@ impl GenmcCtx {
         }
         interp_ok(())
     }
+
+    /**** Blocking instructions ****/
+
+    #[allow(unused)]
+    pub(crate) fn handle_verifier_assume<'tcx>(
+        &self,
+        machine: &MiriMachine<'tcx>,
+        condition: bool,
+    ) -> InterpResult<'tcx, ()> {
+        if condition { interp_ok(()) } else { self.handle_user_block(machine) }
+    }
 }
 
 impl GenmcCtx {
@@ -923,17 +934,8 @@ impl GenmcCtx {
 
     /**** Blocking functionality ****/
 
-    fn handle_user_block<'tcx>(&self, machine: &MiriMachine<'tcx>) -> InterpResult<'tcx> {
-        let thread_infos = self.thread_infos.borrow();
-        let curr_thread = machine.threads.active_thread();
-        let genmc_curr_thread = thread_infos.get_info(curr_thread).genmc_tid;
-        info!("GenMC: handle_user_block, blocking thread {curr_thread:?} ({genmc_curr_thread:?})");
-
-        let mut mc = self.handle.borrow_mut();
-        let pinned_mc = mc.as_mut();
-        pinned_mc.handleUserBlock(genmc_curr_thread.0);
-
-        interp_ok(())
+    fn handle_user_block<'tcx>(&self, _machine: &MiriMachine<'tcx>) -> InterpResult<'tcx> {
+        todo!()
     }
 }
 
@@ -1122,40 +1124,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             return interp_ok(next_thread_id);
         }
     }
-
-    /**** Blocking instructions ****/
-
-    /// Handle an `assume` statement. This will tell GenMC to block the current thread if the `condition` is false.
-    /// Returns `true` if the current thread should be blocked in Miri too.
-    fn handle_genmc_verifier_assume(&mut self, condition: &OpTy<'tcx>) -> InterpResult<'tcx> {
-        let this = self.eval_context_mut();
-        let condition_bool = this.read_scalar(condition)?.to_bool()?;
-        info!("GenMC: handle_genmc_verifier_assume, condition: {condition:?} = {condition_bool}");
-        if condition_bool {
-            return interp_ok(());
-        }
-        let genmc_ctx = this.machine.data_race.as_genmc_ref().unwrap();
-        genmc_ctx.handle_user_block(&this.machine)?;
-        let condition = condition.clone();
-        this.block_thread(
-            BlockReason::GenmcAssume,
-            None,
-            callback!(
-                @capture<'tcx> {
-                    condition: OpTy<'tcx>,
-                }
-                |this, unblock: UnblockKind| {
-                    assert_eq!(unblock, UnblockKind::Ready);
-
-                    let condition = this.run_for_validation_ref(|this| this.read_scalar(&condition))?.to_bool()?;
-                    assert!(condition);
-
-                    interp_ok(())
-                }
-            ),
-        );
-        interp_ok(())
-    }
 }
 
 impl VisitProvenance for GenmcCtx {

src/shims/foreign_items.rs

@@ -17,7 +17,6 @@ use rustc_target::callconv::FnAbi;
 use self::helpers::{ToHost, ToSoft};
 use super::alloc::EvalContextExt as _;
 use super::backtrace::EvalContextExt as _;
-use crate::concurrency::GenmcEvalContextExt as _;
 use crate::*;
 
 /// Type of dynamic symbols (for `dlsym` et al)
@@ -440,22 +439,6 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
                 }
             }
 
-            /*** \/ GENMC VERIFIER CALLS \/ ****/
-            "miri_genmc_verifier_assume" => {
-                let [condition] =
-                    this.check_shim_sig_lenient(abi, CanonAbi::Rust, link_name, args)?;
-                if this.machine.data_race.as_genmc_ref().is_some() {
-                    this.handle_genmc_verifier_assume(condition)?;
-                } else {
-                    tracing::warn!(
-                        "GenMC: function `miri_genmc_verifier_assume` used, but GenMC mode is not active, skip ..."
-                    );
-                }
-            }
-
-            // TODO GENMC: add other genmc functions
-
-            /*** /\ GENMC VERIFIER CALLS /\ ****/
             // Aborting the process.
             "exit" => {
                 let [code] = this.check_shim_sig_lenient(abi, CanonAbi::C, link_name, args)?;

tests/genmc/pass/litmus/assume-ctrl/assume-ctrl.rs

@@ -147,7 +147,4 @@ extern "Rust" {
     /// "symbolic" alignment checks. Will fail if the pointer is not actually aligned or `align` is
     /// not a power of two. Has no effect when alignment checks are concrete (which is the default).
     pub fn miri_promise_symbolic_alignment(ptr: *const (), align: usize);
-
-    /// Blocks the current execution if the argument is false
-    pub fn miri_genmc_verifier_assume(condition: bool);
 }