@@ -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