@@ -3,7 +3,7 @@ use std::sync::Arc;
3
3
4
4
use genmc_sys:: {
5
5
ActionKind , GENMC_GLOBAL_ADDRESSES_MASK , GenmcScalar , GenmcThreadId , MemOrdering ,
6
- MiriGenMCShim , RMWBinOp , StoreEventType , createGenmcHandle,
6
+ MiriGenMCShim , RMWBinOp , StoreEventType , UniquePtr , createGenmcHandle,
7
7
} ;
8
8
use rustc_abi:: { Align , Size } ;
9
9
use rustc_const_eval:: interpret:: { AllocId , InterpCx , InterpResult , interp_ok} ;
@@ -45,7 +45,7 @@ struct ExitStatus {
45
45
}
46
46
47
47
pub struct GenmcCtx {
48
- handle : RefCell < NonNullUniquePtr < MiriGenMCShim > > ,
48
+ handle : RefCell < UniquePtr < MiriGenMCShim > > ,
49
49
50
50
// TODO GENMC (PERFORMANCE): could use one RefCell for all internals instead of multiple
51
51
thread_infos : RefCell < ThreadInfoManager > ,
@@ -66,14 +66,9 @@ impl GenmcCtx {
66
66
/// Create a new `GenmcCtx` from a given config.
67
67
pub fn new ( miri_config : & MiriConfig ) -> Self {
68
68
let genmc_config = miri_config. genmc_config . as_ref ( ) . unwrap ( ) ;
69
- info ! ( "GenMC: Creating new GenMC Context" ) ;
70
-
71
- let handle = createGenmcHandle ( & genmc_config. params ) ;
72
- let non_null_handle = NonNullUniquePtr :: new ( handle) . expect ( "GenMC should not return null" ) ;
73
- let non_null_handle = RefCell :: new ( non_null_handle) ;
74
-
69
+ let handle = RefCell :: new ( createGenmcHandle ( & genmc_config. params ) ) ;
75
70
Self {
76
- handle : non_null_handle ,
71
+ handle,
77
72
thread_infos : Default :: default ( ) ,
78
73
allow_data_races : Cell :: new ( false ) ,
79
74
global_allocations : Default :: default ( ) ,
@@ -83,20 +78,20 @@ impl GenmcCtx {
83
78
84
79
pub fn get_blocked_execution_count ( & self ) -> u64 {
85
80
let mc = self . handle . borrow ( ) ;
86
- mc. as_ref ( ) . getBlockedExecutionCount ( )
81
+ mc. as_ref ( ) . unwrap ( ) . getBlockedExecutionCount ( )
87
82
}
88
83
89
84
pub fn get_explored_execution_count ( & self ) -> u64 {
90
85
let mc = self . handle . borrow ( ) ;
91
- mc. as_ref ( ) . getExploredExecutionCount ( )
86
+ mc. as_ref ( ) . unwrap ( ) . getExploredExecutionCount ( )
92
87
}
93
88
94
89
/// This function determines if we should continue exploring executions or if we are done.
95
90
///
96
91
/// In GenMC mode, the input program should be repeatedly executed until this function returns `true` or an error is found.
97
92
pub fn is_exploration_done ( & self ) -> bool {
98
93
let mut mc = self . handle . borrow_mut ( ) ;
99
- mc. as_mut ( ) . isExplorationDone ( )
94
+ mc. as_mut ( ) . unwrap ( ) . isExplorationDone ( )
100
95
}
101
96
102
97
pub fn get_exit_status ( & self ) -> Option < ( i32 , bool ) > {
@@ -121,7 +116,7 @@ impl GenmcCtx {
121
116
self . exit_status . set ( None ) ;
122
117
123
118
let mut mc = self . handle . borrow_mut ( ) ;
124
- mc. as_mut ( ) . handleExecutionStart ( ) ;
119
+ mc. as_mut ( ) . unwrap ( ) . handleExecutionStart ( ) ;
125
120
}
126
121
127
122
/// Inform GenMC that the program's execution has ended.
@@ -133,7 +128,7 @@ impl GenmcCtx {
133
128
_ecx : & InterpCx < ' tcx , MiriMachine < ' tcx > > ,
134
129
) -> Result < ( ) , String > {
135
130
let mut mc = self . handle . borrow_mut ( ) ;
136
- let result = mc. as_mut ( ) . handleExecutionEnd ( ) ;
131
+ let result = mc. as_mut ( ) . unwrap ( ) . handleExecutionEnd ( ) ;
137
132
if let Some ( msg) = result. as_ref ( ) {
138
133
let msg = msg. to_string_lossy ( ) . to_string ( ) ;
139
134
info ! ( "GenMC: execution ended with error \" {msg}\" " ) ;
@@ -345,7 +340,7 @@ impl GenmcCtx {
345
340
let genmc_old_value = scalar_to_genmc_scalar ( ecx, old_value) ?;
346
341
347
342
let mut mc = self . handle . borrow_mut ( ) ;
348
- let pinned_mc = mc. as_mut ( ) ;
343
+ let pinned_mc = mc. as_mut ( ) . unwrap ( ) ;
349
344
let cas_result = pinned_mc. handleCompareExchange (
350
345
genmc_tid. 0 ,
351
346
genmc_address,
@@ -498,7 +493,7 @@ impl GenmcCtx {
498
493
let alignment = alignment. bytes ( ) ;
499
494
500
495
let mut mc = self . handle . borrow_mut ( ) ;
501
- let pinned_mc = mc. as_mut ( ) ;
496
+ let pinned_mc = mc. as_mut ( ) . unwrap ( ) ;
502
497
let chosen_address = pinned_mc. handleMalloc ( genmc_tid. 0 , genmc_size, alignment) ;
503
498
504
499
assert_ne ! ( chosen_address, 0 , "GenMC malloc returned nullptr." ) ;
@@ -542,7 +537,7 @@ impl GenmcCtx {
542
537
let genmc_size = size. bytes ( ) . max ( 1 ) ;
543
538
544
539
let mut mc = self . handle . borrow_mut ( ) ;
545
- let pinned_mc = mc. as_mut ( ) ;
540
+ let pinned_mc = mc. as_mut ( ) . unwrap ( ) ;
546
541
pinned_mc. handleFree ( genmc_tid. 0 , genmc_address, genmc_size) ;
547
542
548
543
// TODO GENMC (ERROR HANDLING): can this ever fail?
@@ -566,7 +561,7 @@ impl GenmcCtx {
566
561
let genmc_new_tid = thread_infos. add_thread ( new_thread_id) ;
567
562
568
563
let mut mc = self . handle . borrow_mut ( ) ;
569
- mc. as_mut ( ) . handleThreadCreate ( genmc_new_tid. 0 , genmc_parent_tid. 0 ) ;
564
+ mc. as_mut ( ) . unwrap ( ) . handleThreadCreate ( genmc_new_tid. 0 , genmc_parent_tid. 0 ) ;
570
565
571
566
interp_ok ( ( ) )
572
567
}
@@ -583,7 +578,7 @@ impl GenmcCtx {
583
578
let genmc_child_tid = thread_infos. get_info ( child_thread_id) . genmc_tid ;
584
579
585
580
let mut mc = self . handle . borrow_mut ( ) ;
586
- mc. as_mut ( ) . handleThreadJoin ( genmc_curr_tid. 0 , genmc_child_tid. 0 ) ;
581
+ mc. as_mut ( ) . unwrap ( ) . handleThreadJoin ( genmc_curr_tid. 0 , genmc_child_tid. 0 ) ;
587
582
588
583
interp_ok ( ( ) )
589
584
}
@@ -603,7 +598,7 @@ impl GenmcCtx {
603
598
) ;
604
599
605
600
let mut mc = self . handle . borrow_mut ( ) ;
606
- let pinned_mc = mc. as_mut ( ) ;
601
+ let pinned_mc = mc. as_mut ( ) . unwrap ( ) ;
607
602
pinned_mc. handleThreadFinish ( genmc_tid. 0 , ret_val) ;
608
603
}
609
604
@@ -666,7 +661,7 @@ impl GenmcCtx {
666
661
let genmc_size = size. bytes ( ) ;
667
662
668
663
let mut mc = self . handle . borrow_mut ( ) ;
669
- let pinned_mc = mc. as_mut ( ) ;
664
+ let pinned_mc = mc. as_mut ( ) . unwrap ( ) ;
670
665
let load_result = pinned_mc. handleLoad (
671
666
genmc_tid. 0 ,
672
667
genmc_address,
@@ -719,7 +714,7 @@ impl GenmcCtx {
719
714
) ;
720
715
721
716
let mut mc = self . handle . borrow_mut ( ) ;
722
- let pinned_mc = mc. as_mut ( ) ;
717
+ let pinned_mc = mc. as_mut ( ) . unwrap ( ) ;
723
718
let store_result = pinned_mc. handleStore (
724
719
genmc_tid. 0 ,
725
720
genmc_address,
@@ -838,7 +833,7 @@ impl GenmcCtx {
838
833
let curr_thread_info = thread_infos. get_info ( active_thread_id) ;
839
834
840
835
let mut mc = self . handle . borrow_mut ( ) ;
841
- let pinned_mc = mc. as_mut ( ) ;
836
+ let pinned_mc = mc. as_mut ( ) . unwrap ( ) ;
842
837
let result =
843
838
pinned_mc. scheduleNext ( curr_thread_info. genmc_tid . 0 , curr_thread_next_instr_kind) ;
844
839
if result >= 0 {
0 commit comments