miri/concurrency/genmc/
dummy.rs

1use rustc_abi::{Align, Size};
2use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult};
3
4pub use self::intercept::EvalContextExt as GenmcEvalContextExt;
5pub use self::run::run_genmc_mode;
6use crate::eval::ExitType;
7use crate::{
8    AtomicFenceOrd, AtomicReadOrd, AtomicRmwOp, AtomicRwOrd, AtomicWriteOrd, MemoryKind,
9    MiriMachine, OpTy, Scalar, ThreadId, ThreadManager, VisitProvenance, VisitWith,
10};
11
12#[derive(Debug)]
13pub struct GenmcCtx {}
14
15#[derive(Debug, Default, Clone)]
16pub struct GenmcConfig {}
17
18mod run {
19    use std::num::NonZeroI32;
20    use std::rc::Rc;
21
22    use rustc_middle::ty::TyCtxt;
23
24    use crate::{GenmcCtx, MiriConfig};
25
26    pub fn run_genmc_mode<'tcx>(
27        _tcx: TyCtxt<'tcx>,
28        _config: &MiriConfig,
29        _eval_entry: impl Fn(Rc<GenmcCtx>) -> Result<(), NonZeroI32>,
30    ) -> Result<(), NonZeroI32> {
31        unreachable!();
32    }
33}
34
35mod intercept {
36    use super::*;
37
38    impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
39    pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
40        fn genmc_intercept_function(
41            &mut self,
42            _instance: rustc_middle::ty::Instance<'tcx>,
43            _args: &[rustc_const_eval::interpret::FnArg<'tcx, crate::Provenance>],
44            _dest: &crate::PlaceTy<'tcx>,
45        ) -> InterpResult<'tcx, bool> {
46            unreachable!()
47        }
48
49        fn handle_genmc_verifier_assume(&mut self, _condition: &OpTy<'tcx>) -> InterpResult<'tcx> {
50            unreachable!();
51        }
52    }
53}
54
55impl GenmcCtx {
56    // We don't provide the `new` function in the dummy module.
57
58    pub(crate) fn schedule_thread<'tcx>(
59        &self,
60        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
61    ) -> InterpResult<'tcx, Option<ThreadId>> {
62        unreachable!()
63    }
64
65    /**** Memory access handling ****/
66
67    pub(super) fn set_ongoing_action_data_race_free(&self, _enable: bool) {
68        unreachable!()
69    }
70
71    //* might fails if there's a race, load might also not read anything (returns None) */
72    pub(crate) fn atomic_load<'tcx>(
73        &self,
74        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
75        _address: Size,
76        _size: Size,
77        _ordering: AtomicReadOrd,
78        _old_val: Option<Scalar>,
79    ) -> InterpResult<'tcx, Scalar> {
80        unreachable!()
81    }
82
83    pub(crate) fn atomic_store<'tcx>(
84        &self,
85        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
86        _address: Size,
87        _size: Size,
88        _value: Scalar,
89        _old_value: Option<Scalar>,
90        _ordering: AtomicWriteOrd,
91    ) -> InterpResult<'tcx, bool> {
92        unreachable!()
93    }
94
95    pub(crate) fn atomic_fence<'tcx>(
96        &self,
97        _machine: &MiriMachine<'tcx>,
98        _ordering: AtomicFenceOrd,
99    ) -> InterpResult<'tcx> {
100        unreachable!()
101    }
102
103    pub(crate) fn atomic_rmw<'tcx>(
104        &self,
105        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
106        _address: Size,
107        _size: Size,
108        _atomic_op: AtomicRmwOp,
109        _is_signed: bool,
110        _ordering: AtomicRwOrd,
111        _rhs_scalar: Scalar,
112        _old_value: Scalar,
113    ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
114        unreachable!()
115    }
116
117    pub(crate) fn atomic_compare_exchange<'tcx>(
118        &self,
119        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
120        _address: Size,
121        _size: Size,
122        _expected_old_value: Scalar,
123        _new_value: Scalar,
124        _success: AtomicRwOrd,
125        _fail: AtomicReadOrd,
126        _can_fail_spuriously: bool,
127        _old_value: Scalar,
128    ) -> InterpResult<'tcx, (Scalar, Option<Scalar>, bool)> {
129        unreachable!()
130    }
131
132    pub(crate) fn memory_load<'tcx>(
133        &self,
134        _machine: &MiriMachine<'tcx>,
135        _address: Size,
136        _size: Size,
137    ) -> InterpResult<'tcx> {
138        unreachable!()
139    }
140
141    pub(crate) fn memory_store<'tcx>(
142        &self,
143        _machine: &MiriMachine<'tcx>,
144        _address: Size,
145        _size: Size,
146    ) -> InterpResult<'tcx> {
147        unreachable!()
148    }
149
150    /**** Memory (de)allocation ****/
151
152    pub(crate) fn handle_alloc<'tcx>(
153        &self,
154        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
155        _alloc_id: AllocId,
156        _size: Size,
157        _alignment: Align,
158        _memory_kind: MemoryKind,
159    ) -> InterpResult<'tcx, u64> {
160        unreachable!()
161    }
162
163    pub(crate) fn handle_dealloc<'tcx>(
164        &self,
165        _machine: &MiriMachine<'tcx>,
166        _alloc_id: AllocId,
167        _address: Size,
168        _kind: MemoryKind,
169    ) -> InterpResult<'tcx> {
170        unreachable!()
171    }
172
173    /**** Thread management ****/
174
175    pub(crate) fn handle_thread_create<'tcx>(
176        &self,
177        _threads: &ThreadManager<'tcx>,
178        _start_routine: crate::Pointer,
179        _func_arg: &crate::ImmTy<'tcx>,
180        _new_thread_id: ThreadId,
181    ) -> InterpResult<'tcx> {
182        unreachable!()
183    }
184
185    pub(crate) fn handle_thread_join<'tcx>(
186        &self,
187        _active_thread_id: ThreadId,
188        _child_thread_id: ThreadId,
189    ) -> InterpResult<'tcx> {
190        unreachable!()
191    }
192
193    pub(crate) fn handle_thread_finish<'tcx>(&self, _threads: &ThreadManager<'tcx>) {
194        unreachable!()
195    }
196
197    pub(crate) fn handle_exit<'tcx>(
198        &self,
199        _thread: ThreadId,
200        _exit_code: i32,
201        _exit_type: ExitType,
202    ) -> InterpResult<'tcx> {
203        unreachable!()
204    }
205}
206
207impl VisitProvenance for GenmcCtx {
208    fn visit_provenance(&self, _visit: &mut VisitWith<'_>) {
209        unreachable!()
210    }
211}
212
213impl GenmcConfig {
214    pub fn parse_arg(
215        _genmc_config: &mut Option<GenmcConfig>,
216        _trimmed_arg: &str,
217    ) -> Result<(), String> {
218        if cfg!(feature = "genmc") {
219            Err(format!("GenMC is disabled in this build of Miri"))
220        } else {
221            Err(format!("GenMC is not supported on this target"))
222        }
223    }
224
225    pub fn validate(_miri_config: &mut crate::MiriConfig) -> Result<(), &'static str> {
226        Ok(())
227    }
228}
miri/concurrency/genmc/dummy.rs

miri/concurrency/genmc/
dummy.rs
