1- use rustc_middle:: throw_unsup_format;
1+ use rustc_middle:: { throw_unsup_format, ty } ;
22use tracing:: debug;
33
4- use crate :: concurrency:: genmc:: MAX_ACCESS_SIZE ;
54use crate :: concurrency:: thread:: EvalContextExt as _;
6- use crate :: {
7- BlockReason , InterpResult , MachineCallback , MiriInterpCx , OpTy , Scalar , UnblockKind ,
8- VisitProvenance , VisitWith , callback, interp_ok, throw_ub_format,
9- } ;
5+ use crate :: * ;
106
117// Handling of code intercepted by Miri in GenMC mode, such as assume statement or `std::sync::Mutex`.
128
13- #[ derive( Clone , Copy ) ]
14- struct MutexMethodArgs {
15- address : u64 ,
16- size : u64 ,
17- }
18-
199impl < ' tcx > EvalContextExtPriv < ' tcx > for crate :: MiriInterpCx < ' tcx > { }
2010trait EvalContextExtPriv < ' tcx > : crate :: MiriInterpCxExt < ' tcx > {
21- fn parse_mutex_method_args (
11+ /// Small helper to get the arguments of an intercepted function call.
12+ fn get_fn_args < const N : usize > (
2213 & 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." ) ;
14+ instance : ty :: Instance < ' tcx > ,
15+ args : & [ FnArg < ' tcx > ] ,
16+ ) -> InterpResult < ' tcx , [ OpTy < ' tcx > ; N ] > {
2617 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- } )
18+ let args = this. copy_fn_args ( args) ; // FIXME: Should `InPlace` arguments be reset to uninit?
19+ if let Ok ( ops) = args. try_into ( ) {
20+ return interp_ok ( ops) ;
21+ }
22+ panic ! ( "{} is a diagnostic item expected to have {} arguments" , instance, N ) ;
3523 }
3624
37- fn intercept_mutex_lock ( & mut self , args : MutexMethodArgs ) -> InterpResult < ' tcx > {
25+ fn intercept_mutex_lock ( & mut self , mutex : MPlaceTy < ' tcx > ) -> InterpResult < ' tcx > {
3826 debug ! ( "GenMC: handling Mutex::lock()" ) ;
39- let MutexMethodArgs { address, size } = args;
4027 let this = self . eval_context_mut ( ) ;
4128 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) ;
29+
30+ let result = genmc_ctx. handle . borrow_mut ( ) . pin_mut ( ) . handle_mutex_lock (
31+ genmc_ctx. active_thread_genmc_tid ( & this. machine ) ,
32+ mutex. ptr ( ) . addr ( ) . bytes ( ) ,
33+ mutex. layout . size . bytes ( ) ,
34+ ) ;
4535 if let Some ( error) = result. error . as_ref ( ) {
4636 // FIXME(genmc): improve error handling.
4737 throw_ub_format ! ( "{}" , error. to_string_lossy( ) ) ;
@@ -58,9 +48,7 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
5848 None ,
5949 crate :: callback!(
6050 @capture<' tcx> {
61- genmc_tid: i32 ,
62- address: u64 ,
63- size: u64 ,
51+ mutex: MPlaceTy <' tcx>,
6452 }
6553 |this, unblock: crate :: UnblockKind | {
6654 debug!( "GenMC: handling Mutex::lock: unblocking callback called." ) ;
@@ -69,7 +57,11 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
6957 let result = genmc_ctx. handle
7058 . borrow_mut( )
7159 . pin_mut( )
72- . handle_mutex_lock( genmc_tid, address, size) ;
60+ . handle_mutex_lock(
61+ genmc_ctx. active_thread_genmc_tid( & this. machine) ,
62+ mutex. ptr( ) . addr( ) . bytes( ) ,
63+ mutex. layout. size. bytes( ) ,
64+ ) ;
7365 if let Some ( error) = result. error. as_ref( ) {
7466 // FIXME(genmc): improve error handling.
7567 throw_ub_format!( "{}" , error. to_string_lossy( ) ) ;
@@ -89,16 +81,16 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
8981
9082 fn intercept_mutex_try_lock (
9183 & mut self ,
92- args : MutexMethodArgs ,
84+ mutex : MPlaceTy < ' tcx > ,
9385 dest : & crate :: PlaceTy < ' tcx > ,
9486 ) -> InterpResult < ' tcx > {
9587 debug ! ( "GenMC: handling Mutex::try_lock()" ) ;
9688 let this = self . eval_context_mut ( ) ;
9789 let genmc_ctx = this. machine . data_race . as_genmc_ref ( ) . unwrap ( ) ;
9890 let result = genmc_ctx. handle . borrow_mut ( ) . pin_mut ( ) . handle_mutex_try_lock (
9991 genmc_ctx. active_thread_genmc_tid ( & this. machine ) ,
100- args . address ,
101- args . size ,
92+ mutex . ptr ( ) . addr ( ) . bytes ( ) ,
93+ mutex . layout . size . bytes ( ) ,
10294 ) ;
10395 if let Some ( error) = result. error . as_ref ( ) {
10496 // FIXME(genmc): improve error handling.
@@ -111,14 +103,14 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
111103 interp_ok ( ( ) )
112104 }
113105
114- fn intercept_mutex_unlock ( & self , args : MutexMethodArgs ) -> InterpResult < ' tcx > {
106+ fn intercept_mutex_unlock ( & self , mutex : MPlaceTy < ' tcx > ) -> InterpResult < ' tcx > {
115107 debug ! ( "GenMC: handling Mutex::unlock()" ) ;
116108 let this = self . eval_context_ref ( ) ;
117109 let genmc_ctx = this. machine . data_race . as_genmc_ref ( ) . unwrap ( ) ;
118110 let result = genmc_ctx. handle . borrow_mut ( ) . pin_mut ( ) . handle_mutex_unlock (
119111 genmc_ctx. active_thread_genmc_tid ( & this. machine ) ,
120- args . address ,
121- args . size ,
112+ mutex . ptr ( ) . addr ( ) . bytes ( ) ,
113+ mutex . layout . size . bytes ( ) ,
122114 ) ;
123115 if let Some ( error) = result. error . as_ref ( ) {
124116 // FIXME(genmc): improve error handling.
@@ -147,19 +139,23 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
147139
148140 // NOTE: When adding new intercepted functions here, they must also be added to `fn get_function_kind` in `concurrency/genmc/scheduling.rs`.
149141 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) ?) ?;
152- true
142+ if this. tcx . is_diagnostic_item ( sym:: sys_mutex_lock, instance. def_id ( ) ) {
143+ let [ mutex] = this. get_fn_args ( instance, args) ?;
144+ let mutex = this. deref_pointer ( & mutex) ?;
145+ this. intercept_mutex_lock ( mutex) ?;
153146 } else if this. tcx . is_diagnostic_item ( sym:: sys_mutex_try_lock, instance. def_id ( ) ) {
154- this. intercept_mutex_try_lock ( this. parse_mutex_method_args ( args) ?, dest) ?;
155- true
147+ let [ mutex] = this. get_fn_args ( instance, args) ?;
148+ let mutex = this. deref_pointer ( & mutex) ?;
149+ this. intercept_mutex_try_lock ( mutex, dest) ?;
156150 } else if this. tcx . is_diagnostic_item ( sym:: sys_mutex_unlock, instance. def_id ( ) ) {
157- this. intercept_mutex_unlock ( this. parse_mutex_method_args ( args) ?) ?;
158- true
151+ let [ mutex] = this. get_fn_args ( instance, args) ?;
152+ let mutex = this. deref_pointer ( & mutex) ?;
153+ this. intercept_mutex_unlock ( mutex) ?;
159154 } else {
160155 // Nothing to intercept.
161- false
162- } )
156+ return interp_ok ( false ) ;
157+ }
158+ interp_ok ( true )
163159 }
164160
165161 /// Handle an `assume` statement. This will tell GenMC to block the current thread if the `condition` is false.
0 commit comments