1
1
use rustc_middle:: throw_unsup_format;
2
2
use tracing:: debug;
3
3
4
+ use crate :: concurrency:: genmc:: MAX_ACCESS_SIZE ;
4
5
use crate :: concurrency:: thread:: EvalContextExt as _;
5
6
use crate :: {
6
7
BlockReason , InterpResult , MachineCallback , MiriInterpCx , OpTy , Scalar , UnblockKind ,
@@ -9,62 +10,56 @@ use crate::{
9
10
10
11
// Handling of code intercepted by Miri in GenMC mode, such as assume statement or `std::sync::Mutex`.
11
12
12
- impl < ' tcx > EvalContextExt < ' tcx > for crate :: MiriInterpCx < ' tcx > { }
13
- pub trait EvalContextExt < ' tcx > : crate :: MiriInterpCxExt < ' tcx > {
14
- /// Given a `ty::Instance<'tcx>`, do any required special handling.
15
- /// Returns true if this `instance` should be skipped (i.e., no MIR should be executed for it).
16
- fn genmc_intercept_function (
17
- & mut self ,
18
- instance : rustc_middle:: ty:: Instance < ' tcx > ,
19
- args : & [ rustc_const_eval:: interpret:: FnArg < ' tcx , crate :: Provenance > ] ,
20
- dest : & crate :: PlaceTy < ' tcx > ,
21
- ) -> InterpResult < ' tcx , bool > {
22
- let this = self . eval_context_mut ( ) ;
23
- let genmc_ctx = this
24
- . machine
25
- . data_race
26
- . as_genmc_ref ( )
27
- . expect ( "This function should only be called in GenMC mode." ) ;
28
-
29
- let get_mutex_call_infos = || {
30
- assert_eq ! ( args. len( ) , 1 ) ;
31
- let arg = this. copy_fn_arg ( & args[ 0 ] ) ;
32
- let addr = this. read_target_usize ( & arg) ?;
33
- // FIXME(genmc): assert that we have at least 1 byte.
34
- // FIXME(genmc): maybe use actual size of mutex here?.
35
-
36
- let genmc_curr_thread = genmc_ctx. active_thread_genmc_tid ( & this. machine ) ;
37
- interp_ok ( ( genmc_curr_thread, addr, 1 ) )
38
- } ;
13
+ #[ derive( Clone , Copy ) ]
14
+ struct MutexMethodArgs {
15
+ address : u64 ,
16
+ size : u64 ,
17
+ }
39
18
40
- use rustc_span:: sym;
41
- interp_ok ( if this. tcx . is_diagnostic_item ( sym:: sys_mutex_lock, instance. def_id ( ) ) {
42
- debug ! ( "GenMC: handling Mutex::lock()" ) ;
43
- let ( genmc_curr_thread, addr, size) = get_mutex_call_infos ( ) ?;
19
+ impl < ' tcx > EvalContextExtPriv < ' tcx > for crate :: MiriInterpCx < ' tcx > { }
20
+ trait EvalContextExtPriv < ' tcx > : crate :: MiriInterpCxExt < ' tcx > {
21
+ fn parse_mutex_method_args (
22
+ & self ,
23
+ args : & [ rustc_const_eval:: interpret:: FnArg < ' tcx , crate :: Provenance > ] ,
24
+ ) -> InterpResult < ' tcx , MutexMethodArgs > {
25
+ assert_eq ! ( args. len( ) , 1 , "Mutex lock/unlock/try_lock should take exactly 1 argument." ) ;
26
+ let this = self . eval_context_ref ( ) ;
27
+ let arg = this. copy_fn_arg ( & args[ 0 ] ) ;
28
+ // FIXME(genmc): use actual size of the pointee of `arg`.
29
+ let size = 1 ;
30
+ // GenMC does not support large accesses, we limit the size to the maximum access size.
31
+ interp_ok ( MutexMethodArgs {
32
+ address : this. read_target_usize ( & arg) ?,
33
+ size : size. min ( MAX_ACCESS_SIZE ) ,
34
+ } )
35
+ }
44
36
45
- let result = genmc_ctx. handle . borrow_mut ( ) . pin_mut ( ) . handle_mutex_lock (
46
- genmc_curr_thread,
47
- addr,
48
- size,
49
- ) ;
50
- if let Some ( error) = result. error . as_ref ( ) {
51
- // FIXME(genmc): improve error handling.
52
- throw_ub_format ! ( "{}" , error. to_string_lossy( ) ) ;
53
- }
54
- if result. is_lock_acquired {
55
- debug ! ( "GenMC: handling Mutex::lock: success: lock acquired." ) ;
56
- return interp_ok ( true ) ;
57
- }
58
- debug ! ( "GenMC: handling Mutex::lock failed, blocking thread" ) ;
59
- // NOTE: We don't write anything back to Miri's memory, the Mutex state is handled only by GenMC.
37
+ fn intercept_mutex_lock ( & mut self , args : MutexMethodArgs ) -> InterpResult < ' tcx > {
38
+ debug ! ( "GenMC: handling Mutex::lock()" ) ;
39
+ let MutexMethodArgs { address, size } = args;
40
+ let this = self . eval_context_mut ( ) ;
41
+ let genmc_ctx = this. machine . data_race . as_genmc_ref ( ) . unwrap ( ) ;
42
+ let genmc_tid = genmc_ctx. active_thread_genmc_tid ( & this. machine ) ;
43
+ let result =
44
+ genmc_ctx. handle . borrow_mut ( ) . pin_mut ( ) . handle_mutex_lock ( genmc_tid, address, size) ;
45
+ if let Some ( error) = result. error . as_ref ( ) {
46
+ // FIXME(genmc): improve error handling.
47
+ throw_ub_format ! ( "{}" , error. to_string_lossy( ) ) ;
48
+ }
49
+ if result. is_lock_acquired {
50
+ debug ! ( "GenMC: handling Mutex::lock: success: lock acquired." ) ;
51
+ return interp_ok ( ( ) ) ;
52
+ }
53
+ debug ! ( "GenMC: handling Mutex::lock failed, blocking thread" ) ;
54
+ // NOTE: We don't write anything back to Miri's memory, the Mutex state is handled only by GenMC.
60
55
61
- this. block_thread (
56
+ this. block_thread (
62
57
crate :: BlockReason :: Genmc ,
63
58
None ,
64
59
crate :: callback!(
65
60
@capture<' tcx> {
66
- genmc_curr_thread : i32 ,
67
- addr : u64 ,
61
+ genmc_tid : i32 ,
62
+ address : u64 ,
68
63
size: u64 ,
69
64
}
70
65
|this, unblock: crate :: UnblockKind | {
@@ -74,7 +69,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
74
69
let result = genmc_ctx. handle
75
70
. borrow_mut( )
76
71
. pin_mut( )
77
- . handle_mutex_lock( genmc_curr_thread , addr , size) ;
72
+ . handle_mutex_lock( genmc_tid , address , size) ;
78
73
if let Some ( error) = result. error. as_ref( ) {
79
74
// FIXME(genmc): improve error handling.
80
75
throw_ub_format!( "{}" , error. to_string_lossy( ) ) ;
@@ -88,40 +83,78 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
88
83
}
89
84
) ,
90
85
) ;
91
- // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC.
86
+ // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC.
87
+ interp_ok ( ( ) )
88
+ }
89
+
90
+ fn intercept_mutex_try_lock (
91
+ & mut self ,
92
+ args : MutexMethodArgs ,
93
+ dest : & crate :: PlaceTy < ' tcx > ,
94
+ ) -> InterpResult < ' tcx > {
95
+ debug ! ( "GenMC: handling Mutex::try_lock()" ) ;
96
+ let this = self . eval_context_mut ( ) ;
97
+ let genmc_ctx = this. machine . data_race . as_genmc_ref ( ) . unwrap ( ) ;
98
+ let result = genmc_ctx. handle . borrow_mut ( ) . pin_mut ( ) . handle_mutex_try_lock (
99
+ genmc_ctx. active_thread_genmc_tid ( & this. machine ) ,
100
+ args. address ,
101
+ args. size ,
102
+ ) ;
103
+ if let Some ( error) = result. error . as_ref ( ) {
104
+ // FIXME(genmc): improve error handling.
105
+ throw_ub_format ! ( "{}" , error. to_string_lossy( ) ) ;
106
+ }
107
+ debug ! ( "GenMC: Mutex::try_lock(): is_lock_acquired: {}" , result. is_lock_acquired) ;
108
+ // Write the return value of try_lock, i.e., whether we acquired the mutex.
109
+ this. write_scalar ( Scalar :: from_bool ( result. is_lock_acquired ) , dest) ?;
110
+ // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC.
111
+ interp_ok ( ( ) )
112
+ }
113
+
114
+ fn intercept_mutex_unlock ( & self , args : MutexMethodArgs ) -> InterpResult < ' tcx > {
115
+ debug ! ( "GenMC: handling Mutex::unlock()" ) ;
116
+ let this = self . eval_context_ref ( ) ;
117
+ let genmc_ctx = this. machine . data_race . as_genmc_ref ( ) . unwrap ( ) ;
118
+ let result = genmc_ctx. handle . borrow_mut ( ) . pin_mut ( ) . handle_mutex_unlock (
119
+ genmc_ctx. active_thread_genmc_tid ( & this. machine ) ,
120
+ args. address ,
121
+ args. size ,
122
+ ) ;
123
+ if let Some ( error) = result. error . as_ref ( ) {
124
+ // FIXME(genmc): improve error handling.
125
+ throw_ub_format ! ( "{}" , error. to_string_lossy( ) ) ;
126
+ }
127
+ // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC.}
128
+ interp_ok ( ( ) )
129
+ }
130
+ }
131
+
132
+ impl < ' tcx > EvalContextExt < ' tcx > for crate :: MiriInterpCx < ' tcx > { }
133
+ pub trait EvalContextExt < ' tcx > : crate :: MiriInterpCxExt < ' tcx > {
134
+ /// Given a `ty::Instance<'tcx>`, do any required special handling.
135
+ /// Returns true if this `instance` should be skipped (i.e., no MIR should be executed for it).
136
+ fn genmc_intercept_function (
137
+ & mut self ,
138
+ instance : rustc_middle:: ty:: Instance < ' tcx > ,
139
+ args : & [ rustc_const_eval:: interpret:: FnArg < ' tcx , crate :: Provenance > ] ,
140
+ dest : & crate :: PlaceTy < ' tcx > ,
141
+ ) -> InterpResult < ' tcx , bool > {
142
+ let this = self . eval_context_mut ( ) ;
143
+ assert ! (
144
+ this. machine. data_race. as_genmc_ref( ) . is_some( ) ,
145
+ "This function should only be called in GenMC mode."
146
+ ) ;
147
+
148
+ // NOTE: When adding new intercepted functions here, they must also be added to `fn get_function_kind` in `concurrency/genmc/scheduling.rs`.
149
+ use rustc_span:: sym;
150
+ interp_ok ( if this. tcx . is_diagnostic_item ( sym:: sys_mutex_lock, instance. def_id ( ) ) {
151
+ this. intercept_mutex_lock ( this. parse_mutex_method_args ( args) ?) ?;
92
152
true
93
153
} else if this. tcx . is_diagnostic_item ( sym:: sys_mutex_try_lock, instance. def_id ( ) ) {
94
- debug ! ( "GenMC: handling Mutex::try_lock()" ) ;
95
- let ( genmc_curr_thread, addr, size) = get_mutex_call_infos ( ) ?;
96
-
97
- let result = genmc_ctx. handle . borrow_mut ( ) . pin_mut ( ) . handle_mutex_try_lock (
98
- genmc_curr_thread,
99
- addr,
100
- size,
101
- ) ;
102
- if let Some ( error) = result. error . as_ref ( ) {
103
- // FIXME(genmc): improve error handling.
104
- throw_ub_format ! ( "{}" , error. to_string_lossy( ) ) ;
105
- }
106
- debug ! ( "GenMC: Mutex::try_lock(): is_lock_acquired: {}" , result. is_lock_acquired) ;
107
- // Write the return value of the intercepted function.
108
- // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC.
109
- this. write_scalar ( Scalar :: from_bool ( result. is_lock_acquired ) , dest) ?;
154
+ this. intercept_mutex_try_lock ( this. parse_mutex_method_args ( args) ?, dest) ?;
110
155
true
111
156
} else if this. tcx . is_diagnostic_item ( sym:: sys_mutex_unlock, instance. def_id ( ) ) {
112
- debug ! ( "GenMC: handling Mutex::unlock()" ) ;
113
- let ( genmc_curr_thread, addr, size) = get_mutex_call_infos ( ) ?;
114
-
115
- let result = genmc_ctx. handle . borrow_mut ( ) . pin_mut ( ) . handle_mutex_unlock (
116
- genmc_curr_thread,
117
- addr,
118
- size,
119
- ) ;
120
- if let Some ( error) = result. error . as_ref ( ) {
121
- // FIXME(genmc): improve error handling.
122
- throw_ub_format ! ( "{}" , error. to_string_lossy( ) ) ;
123
- }
124
- // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC.
157
+ this. intercept_mutex_unlock ( this. parse_mutex_method_args ( args) ?) ?;
125
158
true
126
159
} else {
127
160
// Nothing to intercept.
0 commit comments