Changeset 2457 for src/joint/semantics.ma
 Timestamp:
 Nov 13, 2012, 11:30:23 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semantics.ma
r2443 r2457 11 11 only the head is kept (or Undef if the list is empty) ??? *) 12 12 13 definition is_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)). 14 λi : ident.∃fd. 15 ! bl ← find_symbol … ge i ; 16 find_funct_ptr … ge bl = Some ? fd. 17 18 definition description_of_function : ∀F,globals,ge.(Σi.is_function F globals ge i) → 19 fundef (F globals) ≝ 20 λF,globals,ge,i. 21 match ! bl ← find_symbol … ge i ; 22 find_funct_ptr … ge bl 23 return λx.(∃fd.x = ?) → ? 24 with 25 [ Some fd ⇒ λ_.fd 26  None ⇒ λprf.⊥ 27 ] (pi2 … i). 28 cases prf #fd #ABS destruct 29 qed. 30 31 definition is_internal_function ≝ λF.λglobals : list ident.λge : genv_t (fundef (F globals)). 32 λi : ident.∃fd. 33 ! bl ← find_symbol … ge i ; 34 find_funct_ptr … ge bl = Some ? (Internal ? fd). 35 36 lemma description_of_internal_function : ∀F,globals,ge,i,fn. 37 description_of_function F globals ge i = Internal ? fn → is_internal_function … ge i. 38 #F #globals #ge * #i * #fd #EQ 39 #fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ 40 %{EQ} 41 qed. 42 43 lemma internal_function_is_function : ∀F,globals,ge,i. 44 is_internal_function F globals ge i → is_function … ge i. 45 #F #globals #ge #i * #fn #prf %{prf} qed. 46 47 definition if_of_function : ∀F,globals,ge.(Σi.is_internal_function F globals ge i) → 48 F globals ≝ 49 λF,globals,ge,i. 50 match ! bl ← find_symbol … ge i ; 51 find_funct_ptr … ge bl 52 return λx.(∃fn.x = ?) → ? 53 with 54 [ Some fd ⇒ 55 match fd return λx.(∃fn.Some ? x = ?) → ? with 56 [ Internal fn ⇒ λ_.fn 57  External _ ⇒ λprf.⊥ 58 ] 59  None ⇒ λprf.⊥ 60 ] (pi2 … i). 61 cases prf #fn #ABS destruct 62 qed. 63 13 64 (* Paolo: I'll put in this record the property about genv we need *) 14 65 record genv_gen (F : list ident → Type[0]) (globals : list ident) : Type[0] ≝ 15 66 { ge :> genv_t (fundef (F globals)) 16 67 ; find_symbol_exists : ∀id.In ? globals id → find_symbol … ge id ≠ None ? 68 ; stack_sizes : (Σi.is_internal_function F globals ge i) → ℕ 17 69 }. 18 70 … … 102 154 axiom BadProgramCounter : String. 103 155 104 definition function_of_block : 105 ∀pars : params. 106 ∀globals. 107 genv pars globals → 108 block → 109 res (joint_closed_internal_function pars globals) ≝ 110 λpars,globals,ge,b. 111 do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; 112 match def with 113 [ Internal def' ⇒ OK … def' 114  External _ ⇒ Error … [MSG BadProgramCounter]]. 115 116 (* this can replace graph_fetch function and lin_fetch_function *) 117 definition fetch_function: 118 ∀pars : params. 119 ∀globals. 120 genv pars globals → 121 cpointer → 122 res (joint_closed_internal_function pars globals) ≝ 123 λpars,globals,ge,p.function_of_block pars globals ge (pblock p). 124 156 (* 125 157 inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝ 126 158  Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for gotolike flow alteration *) … … 133 165  FEnd1 : fin_step_flow p F (Labels [ ]) (* end flow *) 134 166  FEnd2 : fin_step_flow p F Call. (* end flow *) 167 *) 168 169 definition funct_of_ident : ∀F,globals,ge. 170 ident → option (Σi.is_function F globals ge i) 171 ≝ λF,globals,ge,i. 172 match ? 173 return λx.! bl ← find_symbol … ge i ; 174 find_funct_ptr … ge bl = x → ? 175 with 176 [ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf» 177  None ⇒ λ_.None ? 178 ] (refl …). 179 180 lemma match_opt_prf_elim : ∀A,B : Type[0].∀m : option A. 181 ∀Q : option A → Prop. 182 ∀c1 : ∀a.Q (Some ? a) → B. 183 ∀c2 : Q (None ?) → B. 184 ∀P : B → Prop. 185 (∀a,prf.P (c1 a prf)) → 186 (∀prf.P (c2 prf)) → 187 ∀prf : Q m. 188 P (match m return λx.Q x → ? with 189 [ Some a ⇒ λprf.c1 a prf 190  None ⇒ λprf.c2 prf 191 ] prf). 192 #A #B * [2: #a ] #Q #c1 #c2 #P #H1 #H2 #prf 193 normalize [@H1  @H2] 194 qed. 195 196 lemma symbol_of_function_block_ok : 197 ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf). 198 #F #ge #b #FFP 199 whd in ⊢ (???(??%)); 200 @match_opt_prf_elim [//] #H @⊥ 201 (* cut and paste from global env *) 202 whd in H:(??%?); 203 cases b in FFP H ⊢ %; * * b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP  *: * #H cases (H (refl ??)) ] 204 cases (functions_inv … ge b FFP) 205 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b))) 206 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b))) 207 cases (find ????) 208 [ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ *  * #H' cases (H' (refl ??)) ] 209  * #id' #b' #_ normalize #_ #E destruct 210 ] qed. 211 212 definition funct_of_block : ∀F,globals,ge. 213 block → option (Σi.is_function F globals ge i) ≝ 214 λF,globals,ge,bl. 215 match find_funct_ptr … ge bl 216 return λx.find_funct_ptr … ge bl = x → ? with 217 [ Some fd ⇒ λprf.return mk_Sig 218 ident (λi.is_function F globals ge i) 219 (symbol_of_function_block … ge bl ?) 220 (ex_intro … fd ?) 221  None ⇒ λ_.None ? 222 ] (refl …). 223 [ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf 224  >prf % #ABS destruct(ABS) 225 ] 226 qed. 227 228 definition int_funct_of_block : ∀F,globals,ge. 229 block → option (Σi.is_internal_function F globals ge i) ≝ 230 λF,globals,ge,bl. 231 ! f ← funct_of_block … ge bl ; 232 match ? 233 return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i) 234 with 235 [ Internal fn ⇒ λprf.return «pi1 … f, ?» 236  External fn ⇒ λ_.None ? 237 ] (refl …). 238 @(description_of_internal_function … prf) 239 qed. 240 241 definition funct_of_bevals : ∀F,globals,ge. 242 beval → beval → option (Σi.is_function F globals ge i) ≝ 243 λF,globals,ge,dpl,dph. 244 ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ; 245 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ 246 match ptype ptr with [ Code ⇒ true  _ ⇒ false] then 247 funct_of_block … (pblock ptr) 248 else None ?. 249 250 definition block_of_funct_ident ≝ λF,globals,ge. 251 λi : Σi.is_function F globals ge i. 252 match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with 253 [ Some bl ⇒ λ_.bl 254  None ⇒ λprf.⊥ 255 ] (pi2 … i). 256 cases prf #fd normalize #ABS destruct(ABS) 257 qed. 258 259 axiom ProgramCounterOutOfCode : String. 260 axiom PointNotFound : String. 261 axiom LabelNotFound : String. 262 axiom MissingSymbol : String. 263 axiom FailedLoad : String. 264 axiom BadFunction : String. 265 axiom SuccessorNotProvided : String. 266 axiom BadPointer : String. 267 268 (* this can replace graph_fetch function and lin_fetch_function *) 269 definition fetch_function: 270 ∀pars : params. 271 ∀globals. 272 ∀ge : genv pars globals. 273 cpointer → 274 res (Σi.is_internal_function … ge i) ≝ 275 λpars,globals,ge,p. 276 opt_to_res … [MSG BadFunction; MSG BadPointer] 277 (int_funct_of_block … ge (pblock p)). 135 278 136 279 record sem_unserialized_params … … 138 281 (F : list ident → Type[0]) : Type[1] ≝ 139 282 { st_pars :> sem_state_params 283 140 284 ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars) 141 285 ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval … … 161 305 ; setup_call : nat → paramsT … uns_pars → call_args uns_pars → 162 306 state st_pars → res (state st_pars) 163 ; fetch_external_args: external_function → state st_pars → 307 ; fetch_external_args: external_function → state st_pars → call_args … uns_pars → 164 308 res (list val) 165 309 ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars) … … 170 314 ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval) 171 315 (* change of pc must be left to *_flow execution *) 172 ; eval_ext_seq: ∀globals.genv_gen F globals → ext_seq uns_pars → 173 F globals → state st_pars → IO io_out io_in (state st_pars) 174 ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars → 175 F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars)) 176 ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars → 177 state st_pars → IO io_out io_in ident 178 ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars) 179 (* do something more in some op2 calculations (e.g. mark a register for correction 180 with spilled_no in ERTL) *) 181 ; post_op2 : ∀globals.genv_gen F globals → 182 Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars → 183 state st_pars → state st_pars 316 ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars → 317 (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in (state st_pars) 318 ; pop_frame: ∀globals.∀ge : genv_gen F globals. 319 (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars) 184 320 }. 185 321 … … 220 356 return set_regs ? r st. 221 357 222 axiom BadPointer : String.223 224 (* this is preamble to all calls (including tail ones). The optional argument in225 input tells the function whether it has to save the frame for internal226 calls.227 the first element of the triple is the entry point of the function if228 it is an internal one, or false in case of an external one.229 The actual update of the pc is left to later, as it depends on230 serialization and on whether the call is a tail one. *)231 definition eval_call_block:232 ∀p,F.∀p':sem_unserialized_params p F.∀globals.233 genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →234 IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝235 λp,F,p',globals,ge,st,b,args,dest.236 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);237 match fd with238 [ Internal fd ⇒239 return 〈Init ?? (block_id b) fd args dest, st〉240  External fn ⇒241 ! params ← fetch_external_args … p' fn st : IO ???;242 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;243 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));244 (* CSC: XXX bug here; I think I should split it into Bytelong245 components; instead I am making a singleton out of it. To be246 fixed once we fully implement external functions. *)247 let vs ≝ [mk_val ? evres] in248 ! st ← set_result … p' vs dest st : IO ???;249 return 〈Proceed ???, st〉250 ].251 252 358 axiom FailedStore: String. 253 359 … … 355 461 qed. 356 462 357 axiom ProgramCounterOutOfCode : String.358 axiom PointNotFound : String.359 axiom LabelNotFound : String.360 361 463 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals. 362 genv p globals →cpointer →363 res (( joint_closed_internal_function p globals) × (joint_statement p globals)) ≝464 ∀ge:genv p globals. cpointer → 465 res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝ 364 466 λp,msp,globals,ge,ptr. 467 let bl ≝ pblock ptr in 468 ! f ← opt_to_res … [MSG BadFunction; MSG BadPointer] 469 (int_funct_of_block … ge bl) ; 470 let fn ≝ if_of_function … f in 365 471 let pt ≝ point_of_pointer ? msp ptr in 366 ! fn ← fetch_function … ge ptr ;367 472 ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt); 368 return 〈f n, stmt〉.369 473 return 〈f, stmt〉. 474 370 475 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. 371 476 genv p globals → cpointer → label → res cpointer ≝ 372 477 λp,msp,globals,ge,ptr,lbl. 373 ! fn ← fetch_function … ge ptr ; 478 ! f ← fetch_function … ge ptr ; 479 let fn ≝ if_of_function … ge f in 374 480 ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl] 375 481 (point_of_label … (joint_if_code … fn) lbl) ; … … 435 541 return mk_state_pc … st newpc. 436 542 437 axiom MissingSymbol : String. 438 axiom FailedLoad : String. 439 axiom BadFunction : String. 440 axiom SuccessorNotProvided : String. 441 442 definition block_of_call ≝ λp:sem_params.λglobals. 543 544 definition function_of_call ≝ λp:sem_params.λglobals. 443 545 λge: genv p globals.λst : state p.λf. 444 546 match f with 445 547 [ inl id ⇒ 446 opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol… ge id)548 opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id) 447 549  inr addr ⇒ 448 550 ! addr_l ← dpl_arg_retrieve … st (\fst addr) ; 449 551 ! addr_h ← dph_arg_retrieve … st (\snd addr) ; 450 ! ptr ← pointer_of_bevals [addr_l ; addr_h] ; 451 if eq_bv … (bv_zero …) (offv (poff … ptr)) then 452 return pblock ptr 453 else Error … [MSG BadFunction] 552 opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h) 454 553 ]. 455 554 555 (* Paolo: why external calls do not need args?? *) 556 definition eval_external_call ≝ 557 λp,F.λp' : sem_unserialized_params p F.λfn,args,dest,st. 558 ! params ← fetch_external_args … p' fn st args : IO ???; 559 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; 560 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 561 (* CSC: XXX bug here; I think I should split it into Bytelong 562 components; instead I am making a singleton out of it. To be 563 fixed once we fully implement external functions. *) 564 let vs ≝ [mk_val ? evres] in 565 set_result … p' vs dest st. 566 567 lemma block_of_funct_ident_is_code : ∀F,globals,ge,i. 568 block_region (block_of_funct_ident F globals ge i) = Code. 569 #F #globals #ge * #i * #fd 570 whd in ⊢ (?→??(?%)?); 571 cases (find_symbol ???) 572 [ #ABS normalize in ABS; destruct(ABS) ] 573 #bl normalize nodelta >m_return_bind 574 whd in ⊢ (??%?→?); cases (block_region bl) 575 [ #ABS normalize in ABS; destruct(ABS) ] 576 #_ % 577 qed. 578 579 definition eval_internal_call_pc ≝ 580 λp : sem_params.λglobals : list ident.λge : genv p globals.λi. 581 let fn ≝ if_of_function … ge i in 582 let l' ≝ joint_if_entry ?? fn in 583 let pointer_in_fn ≝ mk_pointer (block_of_funct_ident … ge (pi1 … i)) (mk_offset (bv_zero …)) in 584 pointer_of_point ? p … pointer_in_fn l'. 585 [ @block_of_funct_ident_is_code 586  cases i /2 by internal_function_is_function/ 587 ] 588 qed. 589 590 definition eval_internal_call_no_pc ≝ 591 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st. 592 let fn ≝ if_of_function … ge i in 593 let stack_size ≝ stack_sizes … ge i in 594 ! st' ← setup_call … stack_size (joint_if_params … fn) args st ; 595 let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in 596 return set_regs p regs st. 597 456 598 definition eval_seq_no_pc : 457 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals→458 state p → ∀s:joint_seq p globals.599 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) → 600 state p → cpointer → joint_seq p globals → 459 601 IO io_out io_in (state p) ≝ 460 λp,globals,ge,curr_fn,st, seq.602 λp,globals,ge,curr_fn,st,next,seq. 461 603 match seq return λx.IO ??? with 462 604 [ extension_seq c ⇒ … … 489 631 ! 〈v',carry〉 ← be_op2 (carry … st) op v1 v2 ; 490 632 ! st' ← acca_store … dacc_a v' st; 491 return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')633 return set_carry … carry st' 492 634  CLEAR_CARRY ⇒ 493 635 return set_carry … (BBbit false) st … … 509 651 pair_reg_move … st dst_src 510 652  CALL f args dest ⇒ 511 ! b ← block_of_call … ge st f : IO ???; 512 ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ; 513 return st' 653 ! fn ← function_of_call … ge st f : IO ???; 654 match description_of_function … fn return λx.description_of_function … fn = x → ? with 655 [ Internal fd ⇒ λprf. 656 ! st' ← save_frame … next dest st ; 657 eval_internal_call_no_pc … ge «fn, ?» args st' (* only pc changes *) 658  External fd ⇒ λ_.eval_external_call … fd args dest st 659 ] (refl …) 514 660  _ ⇒ return st 515 661 ]. 516 662 [ @find_symbol_exists 517 663 lapply prf 518 664 elim globals [*] 519 665 #hd #tl #IH * [@eq_identifier_elim #H * >H %1 % ] 520 666 #G %2 @IH @G 521 qed. 522 523 definition eval_seq_pc : 524 ∀p:sem_params.∀globals. genv p globals → state p → 525 ∀s:joint_seq p globals. 526 IO io_out io_in (step_flow p ? (step_flows … s)) ≝ 527 λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with 667  @(description_of_internal_function … prf) 668 ] 669 qed. 670 671 definition eval_seq_pc : 672 ∀p:sem_params.∀globals.∀ge:genv p globals. 673 state p → cpointer → joint_seq p globals → 674 res cpointer ≝ 675 λp,globals,ge,st,next,s. 676 match s with 528 677 [ CALL f args dest ⇒ 529 ! b ← block_of_call … ge st f : IO ???; 530 ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ; 531 return flow 532  _ ⇒ return Proceed ??? 678 ! fn ← function_of_call … ge st f; 679 match ? return λx.description_of_function … fn = x → ? with 680 [ Internal _ ⇒ λprf.eval_internal_call_pc … ge «fn, ?» 681  External _ ⇒ λ_.return next 682 ] (refl …) 683  _ ⇒ return next 533 684 ]. 534 535 definition eval_step : 536 ∀p:sem_params.∀globals. genv p globals → 537 joint_closed_internal_function p globals → state p → 538 ∀s:joint_step p globals. 539 IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝ 540 λp,globals,ge,curr_fn,st,s. 541 match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with 542 [ step_seq s ⇒ 543 ! flow ← eval_seq_pc ?? ge st s ; 544 ! st' ← eval_seq_no_pc ?? ge curr_fn st s ; 545 return 〈flow,st'〉 546  COND src ltrue ⇒ 547 ! v ← acca_retrieve … st src; 548 ! b ← bool_of_beval v; 549 if b then 550 return 〈Redirect ??? ltrue, st〉 551 else 552 return 〈Proceed ???, st〉 685 @(description_of_internal_function … prf) 686 qed. 687 688 definition eval_statement : 689 ∀p:sem_params.∀globals.∀ge:genv p globals. 690 (Σi.is_internal_function … ge i) → state_pc p → 691 ∀s:joint_statement p globals. 692 IO io_out io_in (state_pc p) ≝ 693 λp,g,ge,curr_fn,st,s. 694 match s with 695 [ sequential s next ⇒ 696 ! next_ptr ← succ_pc ? p (pc … st) next : IO ??? ; 697 match s return λ_.IO ??? with 698 [ step_seq s ⇒ 699 ! st' ← eval_seq_no_pc … ge curr_fn st next_ptr s ; 700 ! pc' ← eval_seq_pc … ge st next_ptr s ; 701 return mk_state_pc … st' pc' 702  COND a l ⇒ 703 ! v ← acca_retrieve … st a ; 704 ! b ← bool_of_beval … v ; 705 ! pc' ← 706 if b then 707 pointer_of_label ? p … ge (pc … st) l 708 else 709 succ_pc ? p (pc … st) next ; 710 return mk_state_pc … st pc' 711 ] 712  final s ⇒ 713 match s with 714 [ GOTO l ⇒ 715 ! pc' ← pointer_of_label ? p ? ge (pc … st) l ; 716 return mk_state_pc … st pc' 717  RETURN ⇒ 718 ! st' ← pop_frame … curr_fn st ; 719 ! 〈pc', st''〉 ← fetch_ra … p st' ; 720 return mk_state_pc … st'' pc' 721  TAILCALL _ f args ⇒ 722 ! fn ← function_of_call … ge st f : IO ???; 723 match ? return λx.description_of_function … fn = x → ? with 724 [ Internal _ ⇒ λprf. 725 ! pc' ← eval_internal_call_pc … ge «fn, ?» ; 726 return mk_state_pc … st pc' 727  External fd ⇒ λ_. 728 let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in 729 ! st' ← eval_external_call ??? fd args curr_dest st ; 730 ! st'' ← pop_frame … curr_fn st ; 731 ! 〈pc', st'''〉 ← fetch_ra … p st'' ; 732 return mk_state_pc … st''' pc' 733 ] (refl …) 734 ] 553 735 ]. 554 %1 % qed. 555 556 definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals → 557 (* current function *) joint_closed_internal_function p globals → state p → ∀s : joint_fin_step p. 558 IO io_out io_in (state p) ≝ 559 λp,globals,ge,curr_fn,st,s. 560 match s return λx.IO ??? with 561 [ tailcall c ⇒ 562 !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ; 563 return st' 564  _ ⇒ return st 565 ]. 566 567 definition eval_fin_step_pc : 568 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → state p → 569 ∀s:joint_fin_step p. 570 IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝ 571 λp,g,ge,curr_fn,st,s. 572 match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with 573 [ tailcall c ⇒ 574 !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ; 575 return flow 576  GOTO l ⇒ return FRedirect … l 577  RETURN ⇒ return FEnd1 ?? 578 ]. %1 % qed. 579 580 definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals → 581 state p → Z → joint_closed_internal_function p globals → call_args p → 582 res (state_pc p) ≝ 583 λp,globals,ge,st,id,fn,args. 584 ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn) 585 args st ; 586 let regs ≝ foldr ?? (allocate_local … p) (regs … st) (joint_if_locals … fn) in 587 let l' ≝ joint_if_entry … fn in 588 let st' ≝ set_regs p regs st in 589 let pointer_in_fn ≝ mk_pointer (mk_block Code id) (mk_offset (bv_zero …)) in 590 ! pc ← pointer_of_point ? p … pointer_in_fn l' ; 591 return mk_state_pc ? st' pc. % qed. 592 593 (* The pointer provided is the one to the *next* instruction. *) 594 definition eval_step_flow : 595 ∀p:sem_params.∀globals.∀flows.genv p globals → 596 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝ 597 λp,globals,flows,ge,st,nxt,cmd. 598 match cmd with 599 [ Redirect _ l ⇒ 600 goto … ge l st nxt 601  Init id fn args dest ⇒ 602 ! st' ← save_frame … nxt dest st ; 603 do_call ?? ge st' id fn args 604  Proceed _ ⇒ 605 return mk_state_pc ? st nxt 606 ]. 607 608 definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals → 609 state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝ 610 λp,globals,lbls,ge,st,curr,cmd. 611 match cmd with 612 [ FRedirect _ l ⇒ goto … ge l st curr 613  FTailInit id fn args ⇒ 614 do_call … ge st id fn args 615  _ ⇒ 616 ! 〈ra, st'〉 ← fetch_ra … st ; 617 ! fn ← fetch_function … ge curr ; 618 ! st'' ← pop_frame … ge fn st'; 619 return mk_state_pc ? st'' ra 620 ]. 621 622 definition eval_statement : 623 ∀globals.∀p:sem_params.genv p globals → 624 state_pc p → joint_closed_internal_function p globals → joint_statement p globals → 625 IO io_out io_in (state_pc p) ≝ 626 λglobals,p,ge,st,curr_fn,stmt. 627 match stmt with 628 [ sequential s nxt ⇒ 629 ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ; 630 ! nxtptr ← succ_pc ? p (pc … st) nxt ; 631 eval_step_flow … ge st' nxtptr flow 632  final s ⇒ 633 ! st' ← eval_fin_step_no_pc … ge curr_fn st s ; 634 ! flow ← eval_fin_step_pc … ge curr_fn st s ; 635 eval_fin_step_flow … ge st' (pc … st) flow 636 ]. 736 @(description_of_internal_function … prf) 737 qed. 637 738 638 739 definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals → … … 640 741 λglobals,p,ge,st. 641 742 ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???; 642 eval_statement … ge st fns.743 eval_statement … ge fn st s. 643 744 644 745 (* Paolo: what if in an intermediate language main finishes with an external … … 648 749 genv p globals → cpointer → state_pc p → option int ≝ 649 750 λglobals,p,ge,exit,st.res_to_opt ? ( 650 do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st); 751 do 〈f,s〉 ← fetch_statement ? p … ge (pc … st); 752 let fn ≝ if_of_function … f in 651 753 match s with 652 754 [ final s' ⇒
Note: See TracChangeset
for help on using the changeset viewer.