miri/concurrency/genmc/
dummy.rs

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

miri/concurrency/genmc/
dummy.rs
