@@ -22,25 +22,27 @@ impl<'tcx> Translator<'tcx> {
22
22
let function_name = self . tcx . def_path_str ( function_def_id) ;
23
23
24
24
match function_call {
25
- FunctionCall :: ForeignWithSyncPrimitive => {
26
- self . call_foreign_function_with_sync_primitive (
25
+ FunctionCall :: CondVarNew => {
26
+ self . call_condvar_new ( & function_name, args, destination, & function_call_places) ;
27
+ }
28
+ FunctionCall :: CondVarNotifyOne => {
29
+ self . call_condvar_notify_one (
27
30
& function_name,
28
31
args,
29
32
destination,
30
33
& function_call_places,
31
34
) ;
32
35
}
33
- FunctionCall :: CondVarNew => {
34
- self . call_condvar_new ( & function_name, destination, & function_call_places) ;
35
- }
36
- FunctionCall :: CondVarNotifyOne => {
37
- self . call_condvar_notify_one ( & function_name, args, & function_call_places) ;
38
- }
39
36
FunctionCall :: CondVarWait => {
40
37
self . call_condvar_wait ( args, destination, & function_call_places) ;
41
38
}
42
39
FunctionCall :: Foreign => {
43
- self . call_foreign_function ( & function_name, & function_call_places) ;
40
+ self . call_foreign_function (
41
+ & function_name,
42
+ args,
43
+ destination,
44
+ & function_call_places,
45
+ ) ;
44
46
}
45
47
FunctionCall :: MirFunction => {
46
48
let ( start_place, end_place, _) = function_call_places;
@@ -52,10 +54,10 @@ impl<'tcx> Translator<'tcx> {
52
54
self . call_mutex_lock ( & function_name, args, destination, & function_call_places) ;
53
55
}
54
56
FunctionCall :: MutexNew => {
55
- self . call_mutex_new ( & function_name, destination, & function_call_places) ;
57
+ self . call_mutex_new ( & function_name, args , destination, & function_call_places) ;
56
58
}
57
59
FunctionCall :: ThreadJoin => {
58
- self . call_thread_join ( & function_name, args, & function_call_places) ;
60
+ self . call_thread_join ( & function_name, args, destination , & function_call_places) ;
59
61
}
60
62
FunctionCall :: ThreadSpawn => {
61
63
self . call_thread_spawn ( & function_name, args, destination, & function_call_places) ;
@@ -72,34 +74,25 @@ impl<'tcx> Translator<'tcx> {
72
74
/// A separate counter is incremented every time that
73
75
/// the function is called to generate a unique label.
74
76
///
77
+ /// Performs a check to keep track of synchronization primitives.
78
+ /// In case the first argument is a mutex, lock guard, join handle or condition variable,
79
+ /// it links the first argument of the function to its return value.
80
+ ///
75
81
/// Returns the transition that represents the function call.
76
82
fn call_foreign_function (
77
83
& mut self ,
78
84
function_name : & str ,
85
+ args : & [ rustc_middle:: mir:: Operand < ' tcx > ] ,
86
+ destination : rustc_middle:: mir:: Place < ' tcx > ,
79
87
function_call_places : & FunctionPlaces ,
80
88
) -> TransitionRef {
81
89
let index = self . function_counter . get_count ( function_name) ;
82
90
self . function_counter . increment ( function_name) ;
83
- call_foreign_function (
91
+ let function_transition = call_foreign_function (
84
92
function_call_places,
85
93
& foreign_call_transition_labels ( function_name, index) ,
86
94
& mut self . net ,
87
- )
88
- }
89
-
90
- /// Handler for the case `FunctionCall::ForeignWithSyncPrimitive`.
91
- /// It is an extension of `call_foreign_function` that performs a check
92
- /// to keep track of synchronization primitives.
93
- /// The goal is to link the first argument of the function to its return value
94
- /// in case the first argument is a mutex, lock guard, join handle or condition variable.
95
- fn call_foreign_function_with_sync_primitive (
96
- & mut self ,
97
- function_name : & str ,
98
- args : & [ rustc_middle:: mir:: Operand < ' tcx > ] ,
99
- destination : rustc_middle:: mir:: Place < ' tcx > ,
100
- function_call_places : & FunctionPlaces ,
101
- ) {
102
- self . call_foreign_function ( function_name, function_call_places) ;
95
+ ) ;
103
96
104
97
let current_function = self . call_stack . peek_mut ( ) ;
105
98
link_return_value_if_sync_variable (
@@ -109,16 +102,19 @@ impl<'tcx> Translator<'tcx> {
109
102
current_function. def_id ,
110
103
self . tcx ,
111
104
) ;
105
+
106
+ function_transition
112
107
}
113
108
114
109
/// Handler for the case `FunctionCall::CondvarNew`.
115
110
fn call_condvar_new (
116
111
& mut self ,
117
112
function_name : & str ,
113
+ args : & [ rustc_middle:: mir:: Operand < ' tcx > ] ,
118
114
destination : rustc_middle:: mir:: Place < ' tcx > ,
119
115
function_call_places : & FunctionPlaces ,
120
116
) {
121
- self . call_foreign_function ( function_name, function_call_places) ;
117
+ self . call_foreign_function ( function_name, args , destination , function_call_places) ;
122
118
123
119
let current_function = self . call_stack . peek_mut ( ) ;
124
120
self . condvar_manager . translate_side_effects_new (
@@ -133,9 +129,11 @@ impl<'tcx> Translator<'tcx> {
133
129
& mut self ,
134
130
function_name : & str ,
135
131
args : & [ rustc_middle:: mir:: Operand < ' tcx > ] ,
132
+ destination : rustc_middle:: mir:: Place < ' tcx > ,
136
133
function_call_places : & FunctionPlaces ,
137
134
) {
138
- let notify_one_transition = self . call_foreign_function ( function_name, function_call_places) ;
135
+ let notify_one_transition =
136
+ self . call_foreign_function ( function_name, args, destination, function_call_places) ;
139
137
140
138
let current_function = self . call_stack . peek_mut ( ) ;
141
139
self . condvar_manager . translate_side_effects_notify_one (
@@ -177,7 +175,7 @@ impl<'tcx> Translator<'tcx> {
177
175
function_call_places : & FunctionPlaces ,
178
176
) {
179
177
let transition_function_call =
180
- self . call_foreign_function ( function_name, function_call_places) ;
178
+ self . call_foreign_function ( function_name, args , destination , function_call_places) ;
181
179
182
180
let current_function = self . call_stack . peek_mut ( ) ;
183
181
self . mutex_manager . translate_side_effects_lock (
@@ -193,10 +191,11 @@ impl<'tcx> Translator<'tcx> {
193
191
fn call_mutex_new (
194
192
& mut self ,
195
193
function_name : & str ,
194
+ args : & [ rustc_middle:: mir:: Operand < ' tcx > ] ,
196
195
destination : rustc_middle:: mir:: Place < ' tcx > ,
197
196
function_call_places : & FunctionPlaces ,
198
197
) {
199
- self . call_foreign_function ( function_name, function_call_places) ;
198
+ self . call_foreign_function ( function_name, args , destination , function_call_places) ;
200
199
201
200
let current_function = self . call_stack . peek_mut ( ) ;
202
201
self . mutex_manager . translate_side_effects_new (
@@ -211,10 +210,11 @@ impl<'tcx> Translator<'tcx> {
211
210
& mut self ,
212
211
function_name : & str ,
213
212
args : & [ rustc_middle:: mir:: Operand < ' tcx > ] ,
213
+ destination : rustc_middle:: mir:: Place < ' tcx > ,
214
214
function_call_places : & FunctionPlaces ,
215
215
) {
216
216
let transition_function_call =
217
- self . call_foreign_function ( function_name, function_call_places) ;
217
+ self . call_foreign_function ( function_name, args , destination , function_call_places) ;
218
218
219
219
let current_function = self . call_stack . peek ( ) ;
220
220
self . thread_manager . translate_side_effects_join (
@@ -233,7 +233,7 @@ impl<'tcx> Translator<'tcx> {
233
233
function_call_places : & FunctionPlaces ,
234
234
) {
235
235
let transition_function_call =
236
- self . call_foreign_function ( function_name, function_call_places) ;
236
+ self . call_foreign_function ( function_name, args , destination , function_call_places) ;
237
237
238
238
let current_function = self . call_stack . peek_mut ( ) ;
239
239
self . thread_manager . translate_side_effects_spawn (
0 commit comments