Simplify next instruction type determination

Author: Patrick-6

src/concurrency/genmc/helper.rs

@@ -1,14 +1,11 @@
 use rustc_abi::Size;
-use rustc_const_eval::interpret::{InterpCx, InterpResult, interp_ok};
-use rustc_middle::mir::{Terminator, TerminatorKind};
-use rustc_middle::ty::{self, ScalarInt, Ty};
+use rustc_const_eval::interpret::{InterpResult, interp_ok};
+use rustc_middle::ty::ScalarInt;
 use tracing::info;
 
 use super::GenmcScalar;
 use crate::alloc_addresses::EvalContextExt as _;
-use crate::{
-    BorTag, MiriInterpCx, MiriMachine, Pointer, Provenance, Scalar, ThreadId, throw_unsup_format,
-};
+use crate::{BorTag, MiriInterpCx, Pointer, Provenance, Scalar, throw_unsup_format};
 
 pub fn split_access(address: Size, size: Size) -> impl Iterator<Item = (u64, u64)> {
     /// Maximum size memory access in bytes that GenMC supports.
@@ -139,53 +136,3 @@ pub fn genmc_scalar_to_scalar<'tcx>(
     let (value_scalar_int, _got_truncated) = ScalarInt::truncate_from_uint(scalar.value, size);
     interp_ok(Scalar::Int(value_scalar_int))
 }
-
-pub fn is_terminator_atomic<'tcx>(
-    ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-    terminator: &Terminator<'tcx>,
-    thread_id: ThreadId,
-) -> InterpResult<'tcx, bool> {
-    match &terminator.kind {
-        // All atomics are modeled as function calls to intrinsic functions.
-        // The one exception is thread joining, but those are also calls.
-        TerminatorKind::Call { func, .. } | TerminatorKind::TailCall { func, .. } => {
-            let frame = ecx.machine.threads.get_thread_stack(thread_id).last().unwrap();
-            let func_ty = func.ty(&frame.body().local_decls, *ecx.tcx);
-            info!("GenMC: terminator is a call with operand: {func:?}, ty of operand: {func_ty:?}");
-
-            is_function_atomic(ecx, func_ty)
-        }
-        _ => interp_ok(false),
-    }
-}
-
-fn is_function_atomic<'tcx>(
-    ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-    func_ty: Ty<'tcx>,
-    // func: &Operand<'tcx>,
-) -> InterpResult<'tcx, bool> {
-    let callee_def_id = match func_ty.kind() {
-        ty::FnDef(def_id, _args) => def_id,
-        _ => return interp_ok(true), // we don't know the callee, might be an intrinsic or pthread_join
-    };
-    if ecx.tcx.is_foreign_item(*callee_def_id) {
-        // Some shims, like pthread_join, must be considered loads. So just consider them all loads,
-        // these calls are not *that* common.
-        return interp_ok(true);
-    }
-
-    let Some(intrinsic_def) = ecx.tcx.intrinsic(callee_def_id) else {
-        // TODO GENMC: Make this work for other platforms?
-        let item_name = ecx.tcx.item_name(*callee_def_id);
-        info!("GenMC:  function DefId: {callee_def_id:?}, item name: {item_name:?}");
-        if matches!(item_name.as_str(), "pthread_join" | "WaitForSingleObject") {
-            info!("GenMC:   found a 'join' terminator: '{}'", item_name.as_str(),);
-            return interp_ok(true);
-        }
-        return interp_ok(false);
-    };
-    let intrinsice_name = intrinsic_def.name.as_str();
-    info!("GenMC:   intrinsic name: '{intrinsice_name}'");
-    // TODO GENMC(ENHANCEMENT): make this more precise (only loads). How can we make this maintainable?
-    interp_ok(intrinsice_name.starts_with("atomic_"))
-}

src/concurrency/genmc/mod.rs

@@ -17,7 +17,7 @@ use self::helper::{
 };
 use self::mapping::{min_max_to_genmc_rmw_op, to_genmc_rmw_op};
 use self::thread_info_manager::ThreadInfoManager;
-use crate::concurrency::genmc::helper::{is_terminator_atomic, split_access};
+use crate::concurrency::genmc::helper::split_access;
 use crate::{
     AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriConfig,
     MiriMachine, MiriMemoryKind, Scalar, TerminationInfo, ThreadId, ThreadManager, VisitProvenance,
@@ -864,11 +864,8 @@ impl GenmcCtx {
                     return interp_ok(active_thread_id);
                 }
 
-                if is_terminator_atomic(ecx, basic_block.terminator(), active_thread_id)? {
-                    ActionKind::Load
-                } else {
-                    ActionKind::NonLoad
-                }
+                // FIXME(genmc): determine terminator kind.
+                ActionKind::Load
             };
 
         info!(