miri/concurrency/genmc/
dummy.rs

1#![allow(unused)]
2
3use rustc_abi::{Align, Size};
4use rustc_const_eval::interpret::{InterpCx, InterpResult};
5use rustc_middle::mir;
6
7use crate::{
8    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriConfig,
9    MiriMachine, Scalar, ThreadId, ThreadManager, VisitProvenance, VisitWith,
10};
11
12#[derive(Debug)]
13pub struct GenmcCtx {}
14
15#[derive(Debug, Default, Clone)]
16pub struct GenmcConfig {}
17
18impl GenmcCtx {
19    pub fn new(_miri_config: &MiriConfig, _genmc_config: &GenmcConfig) -> Self {
20        unreachable!()
21    }
22
23    pub fn get_stuck_execution_count(&self) -> usize {
24        unreachable!()
25    }
26
27    pub fn print_genmc_graph(&self) {
28        unreachable!()
29    }
30
31    pub fn is_exploration_done(&self) -> bool {
32        unreachable!()
33    }
34
35    /**** Memory access handling ****/
36
37    pub(crate) fn handle_execution_start(&self) {
38        unreachable!()
39    }
40
41    pub(crate) fn handle_execution_end<'tcx>(
42        &self,
43        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
44    ) -> Result<(), String> {
45        unreachable!()
46    }
47
48    pub(super) fn set_ongoing_action_data_race_free(&self, _enable: bool) {
49        unreachable!()
50    }
51
52    //* might fails if there's a race, load might also not read anything (returns None) */
53    pub(crate) fn atomic_load<'tcx>(
54        &self,
55        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
56        _address: Size,
57        _size: Size,
58        _ordering: AtomicReadOrd,
59        _old_val: Option<Scalar>,
60    ) -> InterpResult<'tcx, Scalar> {
61        unreachable!()
62    }
63
64    pub(crate) fn atomic_store<'tcx>(
65        &self,
66        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
67        _address: Size,
68        _size: Size,
69        _value: Scalar,
70        _ordering: AtomicWriteOrd,
71    ) -> InterpResult<'tcx, ()> {
72        unreachable!()
73    }
74
75    pub(crate) fn atomic_fence<'tcx>(
76        &self,
77        _machine: &MiriMachine<'tcx>,
78        _ordering: AtomicFenceOrd,
79    ) -> InterpResult<'tcx, ()> {
80        unreachable!()
81    }
82
83    pub(crate) fn atomic_rmw_op<'tcx>(
84        &self,
85        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
86        _address: Size,
87        _size: Size,
88        _ordering: AtomicRwOrd,
89        (rmw_op, not): (mir::BinOp, bool),
90        _rhs_scalar: Scalar,
91    ) -> InterpResult<'tcx, (Scalar, Scalar)> {
92        unreachable!()
93    }
94
95    pub(crate) fn atomic_min_max_op<'tcx>(
96        &self,
97        ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
98        address: Size,
99        size: Size,
100        ordering: AtomicRwOrd,
101        min: bool,
102        is_signed: bool,
103        rhs_scalar: Scalar,
104    ) -> InterpResult<'tcx, (Scalar, Scalar)> {
105        unreachable!()
106    }
107
108    pub(crate) fn atomic_exchange<'tcx>(
109        &self,
110        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
111        _address: Size,
112        _size: Size,
113        _rhs_scalar: Scalar,
114        _ordering: AtomicRwOrd,
115    ) -> InterpResult<'tcx, (Scalar, bool)> {
116        unreachable!()
117    }
118
119    pub(crate) fn atomic_compare_exchange<'tcx>(
120        &self,
121        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
122        _address: Size,
123        _size: Size,
124        _expected_old_value: Scalar,
125        _new_value: Scalar,
126        _success: AtomicRwOrd,
127        _fail: AtomicReadOrd,
128        _can_fail_spuriously: bool,
129    ) -> InterpResult<'tcx, (Scalar, bool)> {
130        unreachable!()
131    }
132
133    pub(crate) fn memory_load<'tcx>(
134        &self,
135        _machine: &MiriMachine<'tcx>,
136        _address: Size,
137        _size: Size,
138    ) -> InterpResult<'tcx, ()> {
139        unreachable!()
140    }
141
142    pub(crate) fn memory_store<'tcx>(
143        &self,
144        _machine: &MiriMachine<'tcx>,
145        _address: Size,
146        _size: Size,
147    ) -> InterpResult<'tcx, ()> {
148        unreachable!()
149    }
150
151    /**** Memory (de)allocation ****/
152
153    pub(crate) fn handle_alloc<'tcx>(
154        &self,
155        _machine: &MiriMachine<'tcx>,
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        _address: Size,
167        _size: Size,
168        _align: Align,
169        _kind: MemoryKind,
170    ) -> InterpResult<'tcx, ()> {
171        unreachable!()
172    }
173
174    /**** Thread management ****/
175
176    pub(crate) fn handle_thread_create<'tcx>(
177        &self,
178        _threads: &ThreadManager<'tcx>,
179        _new_thread_id: ThreadId,
180    ) -> InterpResult<'tcx, ()> {
181        unreachable!()
182    }
183
184    pub(crate) fn handle_thread_join<'tcx>(
185        &self,
186        _active_thread_id: ThreadId,
187        _child_thread_id: ThreadId,
188    ) -> InterpResult<'tcx, ()> {
189        unreachable!()
190    }
191
192    pub(crate) fn handle_thread_stack_empty(&self, _thread_id: ThreadId) {
193        unreachable!()
194    }
195
196    pub(crate) fn handle_thread_finish<'tcx>(
197        &self,
198        _threads: &ThreadManager<'tcx>,
199    ) -> InterpResult<'tcx, ()> {
200        unreachable!()
201    }
202
203    /**** Scheduling functionality ****/
204
205    pub(crate) fn schedule_thread<'tcx>(
206        &self,
207        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
208    ) -> InterpResult<'tcx, ThreadId> {
209        unreachable!()
210    }
211
212    /**** Blocking instructions ****/
213
214    pub(crate) fn handle_verifier_assume<'tcx>(
215        &self,
216        _machine: &MiriMachine<'tcx>,
217        _condition: bool,
218    ) -> InterpResult<'tcx, ()> {
219        unreachable!()
220    }
221}
222
223impl VisitProvenance for GenmcCtx {
224    fn visit_provenance(&self, _visit: &mut VisitWith<'_>) {
225        unreachable!()
226    }
227}
228
229impl GenmcConfig {
230    pub fn parse_arg(_genmc_config: &mut Option<GenmcConfig>, trimmed_arg: &str) {
231        unimplemented!(
232            "GenMC feature im Miri is disabled, cannot handle argument: \"-Zmiri-genmc{trimmed_arg}\""
233        );
234    }
235
236    pub fn should_print_graph(&self, _rep: usize) -> bool {
237        unreachable!()
238    }
239}
miri/concurrency/genmc/dummy.rs

miri/concurrency/genmc/
dummy.rs
