miri/concurrency/genmc/
dummy.rs

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

miri/concurrency/genmc/
dummy.rs
