@@ -11,13 +11,14 @@ use std::collections::HashSet;
11
11
12
12
use crate :: codegen_cprover_gotoc:: codegen:: PropertyClass ;
13
13
use crate :: codegen_cprover_gotoc:: GotocCtx ;
14
- use crate :: kani_middle ;
14
+ use crate :: unwrap_or_return_codegen_unimplemented_stmt ;
15
15
use cbmc:: goto_program:: { Expr , Location , Stmt , Symbol , Type } ;
16
16
use cbmc:: { InternString , InternedString } ;
17
17
use lazy_static:: lazy_static;
18
- use rustc_smir:: rustc_internal;
19
- use rustc_target:: abi:: call:: Conv ;
18
+ use stable_mir:: abi:: { CallConvention , PassMode } ;
20
19
use stable_mir:: mir:: mono:: Instance ;
20
+ use stable_mir:: mir:: Place ;
21
+ use stable_mir:: ty:: { RigidTy , TyKind } ;
21
22
use stable_mir:: CrateDef ;
22
23
use tracing:: { debug, trace} ;
23
24
@@ -48,14 +49,12 @@ impl<'tcx> GotocCtx<'tcx> {
48
49
/// handled later.
49
50
pub fn codegen_foreign_fn ( & mut self , instance : Instance ) -> & Symbol {
50
51
debug ! ( ?instance, "codegen_foreign_function" ) ;
51
- let instance_internal = rustc_internal:: internal ( instance) ;
52
52
let fn_name = self . symbol_name_stable ( instance) . intern ( ) ;
53
53
if self . symbol_table . contains ( fn_name) {
54
54
// Symbol has been added (either a built-in CBMC function or a Rust allocation function).
55
55
self . symbol_table . lookup ( fn_name) . unwrap ( )
56
56
} else if RUST_ALLOC_FNS . contains ( & fn_name)
57
- || ( self . is_cffi_enabled ( )
58
- && kani_middle:: fn_abi ( self . tcx , instance_internal) . conv == Conv :: C )
57
+ || ( self . is_cffi_enabled ( ) && instance. fn_abi ( ) . unwrap ( ) . conv == CallConvention :: C )
59
58
{
60
59
// Add a Rust alloc lib function as is declared by core.
61
60
// When C-FFI feature is enabled, we just trust the rust declaration.
@@ -84,6 +83,40 @@ impl<'tcx> GotocCtx<'tcx> {
84
83
}
85
84
}
86
85
86
+ /// Generate a function call to a foreign function by potentially casting arguments and return value, since
87
+ /// the external function definition may not match exactly its Rust declaration.
88
+ /// See <https://github.com/model-checking/kani/issues/1350#issuecomment-1192036619> for more details.
89
+ pub fn codegen_foreign_call (
90
+ & mut self ,
91
+ fn_expr : Expr ,
92
+ args : Vec < Expr > ,
93
+ ret_place : & Place ,
94
+ loc : Location ,
95
+ ) -> Stmt {
96
+ let expected_args = fn_expr
97
+ . typ ( )
98
+ . parameters ( )
99
+ . unwrap ( )
100
+ . iter ( )
101
+ . zip ( args)
102
+ . map ( |( param, arg) | arg. cast_to ( param. typ ( ) . clone ( ) ) )
103
+ . collect :: < Vec < _ > > ( ) ;
104
+ let call_expr = fn_expr. call ( expected_args) ;
105
+
106
+ let ret_kind = self . place_ty_stable ( ret_place) . kind ( ) ;
107
+ if ret_kind. is_unit ( ) || matches ! ( ret_kind, TyKind :: RigidTy ( RigidTy :: Never ) ) {
108
+ call_expr. as_stmt ( loc)
109
+ } else {
110
+ let ret_expr = unwrap_or_return_codegen_unimplemented_stmt ! (
111
+ self ,
112
+ self . codegen_place_stable( ret_place)
113
+ )
114
+ . goto_expr ;
115
+ let ret_type = ret_expr. typ ( ) . clone ( ) ;
116
+ ret_expr. assign ( call_expr. cast_to ( ret_type) , loc)
117
+ }
118
+ }
119
+
87
120
/// Checks whether C-FFI has been enabled or not.
88
121
/// When enabled, we blindly encode the function type as is.
89
122
fn is_cffi_enabled ( & self ) -> bool {
@@ -102,24 +135,24 @@ impl<'tcx> GotocCtx<'tcx> {
102
135
/// Generate type for the given foreign instance.
103
136
fn codegen_ffi_type ( & mut self , instance : Instance ) -> Type {
104
137
let fn_name = self . symbol_name_stable ( instance) ;
105
- let fn_abi = kani_middle :: fn_abi ( self . tcx , rustc_internal :: internal ( instance ) ) ;
138
+ let fn_abi = instance . fn_abi ( ) . unwrap ( ) ;
106
139
let loc = self . codegen_span_stable ( instance. def . span ( ) ) ;
107
140
let params = fn_abi
108
141
. args
109
142
. iter ( )
110
143
. enumerate ( )
111
- . filter ( |& ( _, arg) | ( ! arg. is_ignore ( ) ) )
144
+ . filter ( |& ( _, arg) | ( arg. mode != PassMode :: Ignore ) )
112
145
. map ( |( idx, arg) | {
113
146
let arg_name = format ! ( "{fn_name}::param_{idx}" ) ;
114
147
let base_name = format ! ( "param_{idx}" ) ;
115
- let arg_type = self . codegen_ty ( arg. layout . ty ) ;
148
+ let arg_type = self . codegen_ty_stable ( arg. ty ) ;
116
149
let sym = Symbol :: variable ( & arg_name, & base_name, arg_type. clone ( ) , loc)
117
150
. with_is_parameter ( true ) ;
118
151
self . symbol_table . insert ( sym) ;
119
152
arg_type. as_parameter ( Some ( arg_name. into ( ) ) , Some ( base_name. into ( ) ) )
120
153
} )
121
154
. collect ( ) ;
122
- let ret_type = self . codegen_ty ( fn_abi. ret . layout . ty ) ;
155
+ let ret_type = self . codegen_ty_stable ( fn_abi. ret . ty ) ;
123
156
124
157
if fn_abi. c_variadic {
125
158
Type :: variadic_code ( params, ret_type)
@@ -140,9 +173,9 @@ impl<'tcx> GotocCtx<'tcx> {
140
173
let entry = self . unsupported_constructs . entry ( "foreign function" . into ( ) ) . or_default ( ) ;
141
174
entry. push ( loc) ;
142
175
143
- let call_conv = kani_middle :: fn_abi ( self . tcx , rustc_internal :: internal ( instance ) ) . conv ;
176
+ let call_conv = instance . fn_abi ( ) . unwrap ( ) . conv ;
144
177
let msg = format ! ( "call to foreign \" {call_conv:?}\" function `{fn_name}`" ) ;
145
- let url = if call_conv == Conv :: C {
178
+ let url = if call_conv == CallConvention :: C {
146
179
"https://github.com/model-checking/kani/issues/2423"
147
180
} else {
148
181
"https://github.com/model-checking/kani/issues/new/choose"
0 commit comments