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

miri/concurrency/genmc/
dummy.rs
