@@ -207,9 +207,40 @@ impl<'hir> LoweringContext<'_, 'hir> {
207207 sig : FnSig { decl, header, span : fn_sig_span } ,
208208 generics,
209209 body,
210+ contract,
210211 ..
211212 } ) => {
212213 self . with_new_scopes ( * fn_sig_span, |this| {
214+ assert ! ( this. contract. is_none( ) ) ;
215+ if let Some ( contract) = contract {
216+ let requires = contract. requires . clone ( ) ;
217+ let ensures = contract. ensures . clone ( ) ;
218+ let ensures = ensures. map ( |ens| {
219+ // FIXME: this needs to be a fresh (or illegal) identifier to prevent
220+ // accidental capture of a parameter or global variable.
221+ let checker_ident: Ident =
222+ Ident :: from_str_and_span ( "__ensures_checker" , ens. span ) ;
223+ let ( checker_pat, checker_hir_id) = this. pat_ident_binding_mode_mut (
224+ ens. span ,
225+ checker_ident,
226+ hir:: BindingMode :: NONE ,
227+ ) ;
228+
229+ crate :: FnContractLoweringEnsures {
230+ expr : ens,
231+ fresh_ident : ( checker_ident, checker_pat, checker_hir_id) ,
232+ }
233+ } ) ;
234+
235+ // Note: `with_new_scopes` will reinstall the outer
236+ // item's contract (if any) after its callback finishes.
237+ this. contract . replace ( crate :: FnContractLoweringInfo {
238+ span,
239+ requires,
240+ ensures,
241+ } ) ;
242+ }
243+
213244 // Note: we don't need to change the return type from `T` to
214245 // `impl Future<Output = T>` here because lower_body
215246 // only cares about the input argument patterns in the function
@@ -1054,10 +1085,64 @@ impl<'hir> LoweringContext<'_, 'hir> {
10541085 body : impl FnOnce ( & mut Self ) -> hir:: Expr < ' hir > ,
10551086 ) -> hir:: BodyId {
10561087 self . lower_body ( |this| {
1057- (
1058- this. arena . alloc_from_iter ( decl. inputs . iter ( ) . map ( |x| this. lower_param ( x) ) ) ,
1059- body ( this) ,
1060- )
1088+ let params =
1089+ this. arena . alloc_from_iter ( decl. inputs . iter ( ) . map ( |x| this. lower_param ( x) ) ) ;
1090+ let result = body ( this) ;
1091+
1092+ let opt_contract = this. contract . take ( ) ;
1093+
1094+ // { body }
1095+ // ==>
1096+ // { contract_requires(PRECOND); { body } }
1097+ let Some ( contract) = opt_contract else { return ( params, result) } ;
1098+ let result_ref = this. arena . alloc ( result) ;
1099+ let lit_unit = |this : & mut LoweringContext < ' _ , ' hir > | {
1100+ this. expr ( contract. span , hir:: ExprKind :: Tup ( & [ ] ) )
1101+ } ;
1102+
1103+ let precond: hir:: Stmt < ' hir > = if let Some ( req) = contract. requires {
1104+ let lowered_req = this. lower_expr_mut ( & req) ;
1105+ let precond = this. expr_call_lang_item_fn_mut (
1106+ req. span ,
1107+ hir:: LangItem :: ContractCheckRequires ,
1108+ & * arena_vec ! [ this; lowered_req] ,
1109+ ) ;
1110+ this. stmt_expr ( req. span , precond)
1111+ } else {
1112+ let u = lit_unit ( this) ;
1113+ this. stmt_expr ( contract. span , u)
1114+ } ;
1115+
1116+ let ( postcond_checker, result) = if let Some ( ens) = contract. ensures {
1117+ let crate :: FnContractLoweringEnsures { expr : ens, fresh_ident } = ens;
1118+ let lowered_ens: hir:: Expr < ' hir > = this. lower_expr_mut ( & ens) ;
1119+ let postcond_checker = this. expr_call_lang_item_fn (
1120+ ens. span ,
1121+ hir:: LangItem :: ContractBuildCheckEnsures ,
1122+ & * arena_vec ! [ this; lowered_ens] ,
1123+ ) ;
1124+ let checker_binding_pat = fresh_ident. 1 ;
1125+ (
1126+ this. stmt_let_pat (
1127+ None ,
1128+ ens. span ,
1129+ Some ( postcond_checker) ,
1130+ this. arena . alloc ( checker_binding_pat) ,
1131+ hir:: LocalSource :: Contract ,
1132+ ) ,
1133+ this. inject_ensures_check ( result_ref, ens. span , fresh_ident. 0 , fresh_ident. 2 ) ,
1134+ )
1135+ } else {
1136+ let u = lit_unit ( this) ;
1137+ ( this. stmt_expr ( contract. span , u) , & * result_ref)
1138+ } ;
1139+
1140+ let block = this. block_all (
1141+ contract. span ,
1142+ arena_vec ! [ this; precond, postcond_checker] ,
1143+ Some ( result) ,
1144+ ) ;
1145+ ( params, this. expr_block ( block) )
10611146 } )
10621147 }
10631148
0 commit comments