- Timestamp:
- Mar 15, 2013, 11:32:51 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/joint_semantics.ma
r2876 r2878 59 59 ; carry: bebit 60 60 ; regs: regsT semp 61 ; stack_usage : ℕ62 61 ; m: bemem 63 62 }. … … 80 79 81 80 definition set_m: ∀p. bemem → state p → state p ≝ 82 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) 83 (stack_usage … st) m. 81 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m. 84 82 85 83 definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝ 86 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs 87 (stack_usage … st) (m … st). 84 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st). 88 85 89 86 definition set_sp: ∀p. ? → state p → state p ≝ 90 87 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in 91 mk_state p (st_frms … st) (istack … st) (carry … st) regs' ( stack_usage … st) (m … st).88 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st). 92 89 93 90 definition set_carry: ∀p. bebit → state p → state p ≝ 94 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) 95 (stack_usage … st) (m … st). 91 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st). 96 92 97 93 definition set_istack: ∀p. internal_stack → state p → state p ≝ 98 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) 99 (stack_usage … st) (m … st). 94 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st). 100 95 101 96 definition set_pc: ∀p. ? → state_pc p → state_pc p ≝ … … 109 104 110 105 definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝ 111 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) 112 (stack_usage … st) (m … st). 106 λp,frms,st. mk_state … (Some ? (frms)) (istack … st) (carry … st) (regs … st) (m … st). 113 107 114 108 (* … … 519 513 set_result … p vs dest st. 520 514 521 definition increment_stack_usage : ∀p.ℕ → state p → state p ≝522 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)523 (stack_usage … st + n) (m … st).524 525 definition decrement_stack_usage : ∀p.ℕ → state p → state p ≝526 λp,n,st.mk_state p (st_frms … st) (istack … st) (carry … st) (regs … st)527 (stack_usage … st - n) (m … st).528 529 515 definition eval_internal_call ≝ 530 516 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args. 531 517 λst : state p. 532 518 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ; 533 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ; 534 return increment_stack_usage … stack_size st'. 519 setup_call … stack_size (joint_if_params … globals fn) args st. 535 520 536 521 definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ]. … … 571 556 λst : state p. 572 557 ! st' ← pop_frame … ge curr_id curr_ret st ; 573 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_id] (stack_sizes … ge curr_id) ;574 let st'' ≝ decrement_stack_usage … stack_size (\fst st') in575 558 ! nxt ← next_of_call_pc … ge (\snd … st') ; 576 559 return 577 next … nxt (set_last_pop … (\snd … st') 〈st'', \snd st'〉) (* now address pushed on stack are calling ones! *).560 next … nxt (set_last_pop … (\snd … st') st') (* now address pushed on stack are calling ones! *). 578 561 579 562 definition eval_tailcall ≝ … … 585 568 match fd with 586 569 [ Internal ifd ⇒ 587 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … curr_f] (stack_sizes … ge curr_f) ; 588 let st' ≝ decrement_stack_usage … stack_size st in 589 ! st'' ← eval_internal_call p globals ge i ifd args st' ; 570 ! st' ← eval_internal_call p globals ge i ifd args st ; 590 571 let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in 591 return mk_state_pc … st' 'pc (last_pop … st)572 return mk_state_pc … st' pc (last_pop … st) 592 573 | External efd ⇒ 593 574 ! st' ← eval_external_call … efd args curr_ret st ;
Note: See TracChangeset
for help on using the changeset viewer.