Changeset 2233
- Timestamp:
- Jul 23, 2012, 4:51:51 PM (7 years ago)
- Location:
- src
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/semantics_paolo.ma
r2208 r2233 1 include "joint/ SemanticUtils.ma".2 include "ERTL/ERTL .ma". (* CSC: syntax.ma in RTLabs *)1 include "joint/semanticsUtils_paolo.ma". 2 include "ERTL/ERTL_paolo.ma". (* CSC: syntax.ma in RTLabs *) 3 3 include alias "common/Identifiers.ma". 4 4 5 record ertl_psd_env : Type[0] ≝ 6 { psd_regs : register_env beval 7 (* this tells what pseudo-registers should have their value corrected by spilled_no *) 8 ; need_spilled_no : identifier_set RegisterTag 9 }. 10 11 definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env). 12 definition add_need_spilled_no ≝ 13 λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r). 14 definition rm_need_spilled_no ≝ 15 λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖ {(r)}). 16 17 definition ertl_reg_env ≝ ertl_psd_env × hw_register_env. 18 5 19 definition ps_reg_store ≝ 6 λr,v.λlocal_env:(register_env beval) × hw_register_env. 7 do res ← reg_store r v (\fst local_env) ; 8 OK … 〈res, \snd local_env〉. 20 λr,v.λlocal_env : ertl_reg_env. 21 do res ← reg_store r v (psd_regs (\fst local_env)) ; 22 let psd_env ≝ set_psd_regs res (\fst local_env) in 23 OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉. 9 24 10 25 definition ps_reg_retrieve ≝ 11 λlocal_env: (register_env beval) × hw_register_env. reg_retrieve … (\fst local_env).26 λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)). 12 27 13 28 definition hw_reg_store ≝ 14 λr,v.λlocal_env: (register_env beval) × hw_register_env.29 λr,v.λlocal_env:ertl_reg_env. 15 30 OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉. 16 31 17 32 definition hw_reg_retrieve ≝ 18 λlocal_env: (register_env beval) × hw_register_env.λreg.33 λlocal_env:ertl_reg_env.λreg. 19 34 OK … (hwreg_retrieve … (\snd local_env) reg). 20 35 21 definition ertl_more_sem_params: more_sem_params ertl_params_ := 22 mk_more_sem_params ertl_params_ 23 (list (register_env beval)) [] ((register_env beval) × hw_register_env) 24 (λsp.〈empty_map …,init_hw_register_env sp〉) 0 it 25 ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve 26 ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve 27 (λlocals,dest_src. 28 do v ← 29 match \snd dest_src with 30 [ pseudo reg ⇒ ps_reg_retrieve locals reg 31 | hardware reg ⇒ hw_reg_retrieve locals reg] ; 32 match \fst dest_src with 33 [ pseudo reg ⇒ ps_reg_store reg v locals 34 | hardware reg ⇒ hw_reg_store reg v locals]). 35 definition ertl_sem_params: sem_params ≝ mk_sem_params … ertl_more_sem_params. 36 definition ps_arg_retrieve ≝ 37 λlocal_env,a. 38 match a with 39 [ Reg r ⇒ ps_reg_retrieve local_env r 40 | Imm b ⇒ return b 41 ]. 36 42 37 definition ertl_init_locals : 38 list register → 39 (register_env beval) × hw_register_env → (register_env beval) × hw_register_env ≝ 40 λlocals,lenv. 41 〈foldl … (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals, \snd lenv〉. 43 definition ERTL_state : sem_state_params ≝ 44 mk_sem_state_params 45 (* framesT ≝ *) (list ertl_psd_env) 46 (* empty_framesT ≝ *) [ ] 47 (* regsT ≝ *) ertl_reg_env 48 (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉). 42 49 43 (*CSC: could we use here a dependent type to avoid the Error case? *) 44 axiom EmptyStack: String. 45 definition ertl_pop_frame: 46 ∀globals. genv … (ertl_params globals) → state … ertl_sem_params → res (state … ertl_sem_params) ≝ 47 λglobals,ge,st. 48 let frms ≝ st_frms ? st in 49 match frms with 50 [ nil ⇒ Error ? [MSG EmptyStack] 51 | cons hd tl ⇒ 52 OK … (set_frms ertl_sem_params tl (set_regs ertl_sem_params 〈hd, \snd (regs … st)〉 st)) ]. 50 (* we ignore need_spilled_no as we never move framesize based values around in the 51 translation *) 52 definition ertl_eval_move ≝ λenv,pr. 53 ! v ← 54 match \snd pr with 55 [ Reg src ⇒ 56 match src with 57 [ PSD r ⇒ ps_reg_retrieve env r 58 | HDW r ⇒ hw_reg_retrieve env r 59 ] 60 | Imm bv ⇒ return bv ] ; 61 match \fst pr with 62 [ PSD r ⇒ ps_reg_store r v env 63 | HDW r ⇒ hw_reg_store r v env 64 ]. 65 66 definition ertl_allocate_local ≝ 67 λreg.λlenv : ertl_reg_env. 68 〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉. 53 69 54 70 definition ertl_save_frame: 55 address → nat → nat → nat → unit → state … ertl_sem_params → res (state … ertl_sem_params) ≝56 λ l.λ_.λ_.λ_.λ_.λst.57 do st ← save_ra … st l;71 cpointer → unit → state … ERTL_state → res (state … ERTL_state) ≝ 72 λpc.λ_.λst. 73 do st ← save_ra … st pc ; 58 74 OK … 59 (set_frms ertl_sem_params (\fst (regs … st) :: (st_frms … st)) 60 (set_regs ertl_sem_params 〈empty_map …,\snd (regs … st)〉 st)). 61 62 definition ertl_result_regs: 63 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res (list register) ≝ 64 λglobals,ge,st. 65 do fn ← graph_fetch_function … globals ge st ; 66 OK … (joint_if_result … fn). 75 (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st)) 76 (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)). 67 77 68 78 (*CSC: XXXX, for external functions only*) 69 axiom ertl_fetch_external_args: external_function → state ertl_sem_params → res (list val). 70 axiom ertl_set_result: list val → state ertl_sem_params → res (state ertl_sem_params). 79 axiom ertl_fetch_external_args: external_function → state ERTL_state → res (list val). 80 axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state). 81 (* I think there should be a list beval in place of list val here 82 λvals.λ_.λst. 83 (* set all RegisterRets to 0 *) 84 let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in 85 let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in 86 let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?. 87 let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in 88 return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*) 71 89 72 definition framesize: 73 ∀globals. genv … (ertl_params globals) → state ertl_sem_params → res nat ≝ 74 λglobals,ge,st. 75 do f ← graph_fetch_function … ge st ; 76 OK ? (joint_if_stacksize globals … f). 90 definition xdata_pointer_of_address: address → res xpointer ≝ 91 λp.let 〈v1,v2〉 ≝ p in 92 ! p ← pointer_of_bevals [v1;v2] ; 93 match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with 94 [ XData ⇒ λE.OK ? (mk_Sig … p E) 95 | _ ⇒ λ_.Error … [MSG BadPointer] 96 ] (refl …). 77 97 78 definition get_hwsp : state ertl_sem_params → address ≝ 98 definition address_of_xdata_pointer: xpointer → address ≝ 99 λp.list_to_pair … (bevals_of_pointer p) ?. % qed. 100 101 definition get_hwsp : ERTL_state → res xpointer ≝ 79 102 λst. 80 103 let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in 81 104 let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in 82 〈spl,sph〉.105 xdata_pointer_of_address 〈spl,sph〉. 83 106 84 definition set_hwsp : address → state ertl_sem_params → state ertl_sem_params≝107 definition set_hwsp : xpointer → ERTL_state → ERTL_state ≝ 85 108 λsp,st. 86 let 〈spl,sph〉 ≝ sp in109 let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in 87 110 let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in 88 111 let hwregs ≝ hwreg_store RegisterSPH sph hwregs in 89 set_regs ertl_sem_params〈\fst (regs … st),hwregs〉 st.112 set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st. 90 113 91 definition ertl_more_sem_params1: ∀globals. more_sem_params1 … (ertl_params globals) ≝ 92 λglobals. 93 mk_more_sem_params1 … ertl_more_sem_params graph_succ_p (graph_pointer_of_label …) 94 (graph_fetch_statement …) (load_ra …) (ertl_result_regs …) 95 ertl_init_locals ertl_save_frame (ertl_pop_frame …) 96 ertl_fetch_external_args ertl_set_result. 97 definition ertl_sem_params1: ∀globals. sem_params1 globals ≝ 98 λglobals. mk_sem_params1 … (ertl_more_sem_params1 globals). 114 definition eval_ertl_seq: 115 ∀globals. genv ERTL globals → 116 ertl_seq → joint_internal_function ERTL globals → ERTL_state → 117 IO io_out io_in ERTL_state ≝ 118 λglobals,ge,stm,curr_fn,st. 119 let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in 120 match stm with 121 [ ertl_new_frame ⇒ 122 ! sp ← get_hwsp st ; 123 let newsp ≝ shift_pointer … sp framesize in 124 return set_hwsp newsp st 125 | ertl_del_frame ⇒ 126 ! sp ← get_hwsp st ; 127 let newsp ≝ shift_pointer … sp framesize in 128 return set_hwsp newsp st 129 | ertl_frame_size dst ⇒ 130 let env ≝ regs … st in 131 ! env' ← ps_reg_store dst (BVByte framesize) env ; 132 let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in 133 return set_regs ERTL_state env'' st 134 ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 99 135 100 definition ertl_exec_extended: 101 ∀globals. genv globals (ertl_params globals) → 102 ertl_statement_extension → label → state ertl_sem_params → 103 IO io_out io_in (trace × (state ertl_sem_params)) ≝ 104 λglobals,ge,stm,l,st. 105 match stm with 106 [ ertl_st_ext_new_frame ⇒ 107 ! v ← framesize globals … ge st; 108 let sp ≝ get_hwsp st in 109 ! newsp ← addr_sub sp v; 110 let st ≝ set_hwsp newsp st in 111 ! st ← next … (ertl_sem_params1 globals) l st ; 112 return 〈E0,st〉 113 | ertl_st_ext_del_frame ⇒ 114 ! v ← framesize … ge st; 115 let sp ≝ get_hwsp st in 116 ! newsp ← addr_add sp v; 117 let st ≝ set_hwsp newsp st in 118 ! st ← next … (ertl_sem_params1 …) l st ; 119 return 〈E0,st〉 120 | ertl_st_ext_frame_size dst ⇒ 121 ! v ← framesize … ge st; 122 ! st ← greg_store ertl_sem_params dst (BVByte (bitvector_of_nat … v)) st; 123 ! st ← next … (ertl_sem_params1 …) l st ; 124 return 〈E0, st〉 125 ]. 136 definition ertl_post_op2 ≝ 137 λop,dst,arg1,arg2,st. 138 let local_env ≝ regs ERTL_state st in 139 let f ≝ λarg,st.match arg with 140 [ Reg r ⇒ 141 if r ∈ need_spilled_no (\fst local_env) then 142 set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st 143 else 144 st 145 | _ ⇒ st 146 ] in 147 match op with 148 [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *) 149 | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *) 150 | Sub ⇒ f arg1 st 151 | _ ⇒ st]. 152 126 153 127 definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝ 128 λglobals. mk_more_sem_params2 … (ertl_more_sem_params1 …) (ertl_exec_extended …). 129 130 definition ertl_fullexec: fullexec io_out io_in ≝ 131 joint_fullexec … (λp. ertl_more_sem_params2 (prog_var_names … p)). 154 definition ERTL_semantics ≝ 155 make_sem_graph_params ERTL 156 (mk_more_sem_unserialized_params ?? 157 (* st_pars ≝ *) ERTL_state 158 (* acca_store_ ≝ *) ps_reg_store 159 (* acca_retrieve_ ≝ *) ps_reg_retrieve 160 (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve 161 (* accb_store_ ≝ *) ps_reg_store 162 (* accb_retrieve_ ≝ *) ps_reg_retrieve 163 (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve 164 (* dpl_store_ ≝ *) ps_reg_store 165 (* dpl_retrieve_ ≝ *) ps_reg_retrieve 166 (* dpl_arg_retrieve_ ≝ *) ps_arg_retrieve 167 (* dph_store_ ≝ *) ps_reg_store 168 (* dph_retrieve_ ≝ *) ps_reg_retrieve 169 (* dph_arg_retrieve_ ≝ *) ps_arg_retrieve 170 (* snd_arg_retrieve_ ≝ *) ps_arg_retrieve 171 (* pair_reg_move_ ≝ *) ertl_eval_move 172 (* fetch_ra ≝ *) (load_ra …) 173 (* allocate_local ≝ *) ertl_allocate_local 174 (* save_frame ≝ *) ertl_save_frame 175 (* setup_call ≝ *) (λ_.λ_.λ_.λst.return st) 176 (* fetch_external_args≝ *) ertl_fetch_external_args 177 (* set_result ≝ *) ertl_set_result 178 (* call_args_for_main ≝ *) 0 179 (* call_dest_for_main ≝ *) it 180 (* read_result ≝ *) (λ_.λ_.λ_. 181 λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets) 182 (* eval_ext_seq ≝ *) eval_ertl_seq 183 (* eval_ext_tailcall ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) 184 (* eval_ext_call ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) 185 (* pop_frame ≝ *) (λ_.λ_.λ_.λst.return st) 186 (* post_op2 ≝ *) (λ_.λ_.ertl_post_op2)). -
src/LIN/joint_LTL_LIN_semantics_paolo.ma
r2217 r2233 63 63 (* read_result ≝ *) (λ_.λ_.λ_. 64 64 λst.return map … (hwreg_retrieve (regs … st)) RegisterRets) 65 (* eval_ext_seq ≝ *) (λ_.λ_. eval_ltl_lin_seq)65 (* eval_ext_seq ≝ *) (λ_.λ_.λs.λ_.eval_ltl_lin_seq s) 66 66 (* eval_ext_tailcall ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) 67 67 (* eval_ext_call ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) 68 (* pop_frame ≝ *) (λ_.λ_.λ_.λst.return st). 68 (* pop_frame ≝ *) (λ_.λ_.λ_.λst.return st) 69 (* post_op2 ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st). -
src/RTL/semantics_paolo.ma
r2217 r2233 30 30 31 31 definition rtl_fetch_ra: 32 state RTL_state → res ((state RTL_state)× cpointer) ≝32 RTL_state → res (RTL_state × cpointer) ≝ 33 33 λst. 34 34 match st_frms ? st with … … 41 41 42 42 definition rtl_setup_call: 43 nat → list register → list psd_argument → state RTL_state → res (state RTL_state)≝43 nat → list register → list psd_argument → RTL_state → res RTL_state ≝ 44 44 λstacksize,formal_arg_regs,actual_arg_regs,st. 45 45 let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in … … 57 57 qed. 58 58 59 definition rtl_save_frame ≝ λl.λretregs.λst : stateRTL_state.59 definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state. 60 60 let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in 61 61 OK … (set_frms RTL_state frame st). 62 62 63 63 (*CSC: XXXX, for external functions only*) 64 axiom rtl_fetch_external_args: external_function → stateRTL_state → res (list val).65 axiom rtl_set_result: list val → list register → state RTL_state → res (state RTL_state).64 axiom rtl_fetch_external_args: external_function → RTL_state → res (list val). 65 axiom rtl_set_result: list val → list register → RTL_state → res RTL_state. 66 66 67 67 definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st. … … 69 69 70 70 definition rtl_read_result : 71 ∀globals.genv RTL globals → list register → stateRTL_state → res (list beval) ≝71 ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝ 72 72 λglobals,ge,rets,st. 73 73 m_list_map … (rtl_reg_retrieve st) rets. … … 77 77 saves the OutOfBounds exception *) 78 78 definition rtl_pop_frame: 79 ∀globals. genv RTL globals → list register → state RTL_state → 80 res (state RTL_state) ≝ 81 λglobals,ge,ret,st. 79 ∀globals. genv RTL globals → joint_internal_function RTL globals → RTL_state → 80 res RTL_state ≝ 81 λglobals,ge,curr_fn,st. 82 let ret ≝ joint_if_result … curr_fn in 82 83 do ret_vals ← rtl_read_result … ge ret st ; 83 84 match st_frms ? st with … … 99 100 (* This code is quite similar to eval_call_block: can we factorize it out? *) 100 101 definition eval_tailcall_block: 101 ∀globals.genv RTL globals → stateRTL_state →102 ∀globals.genv RTL globals → RTL_state → 102 103 block → call_args RTL → 103 104 (* this is where the result of the current function should be stored *) 104 105 call_dest RTL → 105 106 IO io_out io_in 106 ((fin_step_flow RTL (joint_internal_function RTL globals) Call)× (state RTL_state)) ≝107 ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝ 107 108 λglobals,ge,st,b,args,ret. 108 109 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); … … 122 123 ]. 123 124 124 definition block_of_register_pair: register → register → stateRTL_state → res block ≝125 definition block_of_register_pair: register → register → RTL_state → res block ≝ 125 126 λr1,r2,st. 126 127 do v1 ← rtl_reg_retrieve st r1 ; … … 131 132 definition eval_rtl_seq: 132 133 ∀globals. genv RTL globals → 133 rtl_seq → stateRTL_state →134 IO io_out io_in (state RTL_state)≝135 λglobals,ge,stm, st.134 rtl_seq → joint_internal_function RTL globals → RTL_state → 135 IO io_out io_in RTL_state ≝ 136 λglobals,ge,stm,curr_fn,st. 136 137 match stm with 137 138 [ rtl_stack_address dreg1 dreg2 ⇒ … … 144 145 definition eval_rtl_call: 145 146 ∀globals. genv RTL globals → 146 rtl_call → stateRTL_state →147 IO io_out io_in ((step_flow RTL ? Call)× (state RTL_state)) ≝147 rtl_call → RTL_state → 148 IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝ 148 149 λglobals,ge,stm,st. 149 150 match stm with … … 169 170 definition eval_rtl_tailcall: 170 171 ∀globals. genv RTL globals → 171 rtl_tailcall → call_dest RTL → state RTL_state → 172 IO io_out io_in ((fin_step_flow RTL ? Call)×(state RTL_state)) ≝ 173 λglobals,ge,stm,ret,st. 172 rtl_tailcall → joint_internal_function RTL globals → RTL_state → 173 IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝ 174 λglobals,ge,stm,curr_fn,st. 175 let ret ≝ joint_if_result … curr_fn in 174 176 match stm with 175 177 [ rtl_tailcall_id id args ⇒ … … 182 184 183 185 definition RTL_semantics ≝ 184 mk_more_sem_unserialized_params RTL (joint_internal_function RTL) 185 RTL_state 186 reg_store reg_retrieve rtl_arg_retrieve 187 reg_store reg_retrieve rtl_arg_retrieve 188 reg_store reg_retrieve rtl_arg_retrieve 189 reg_store reg_retrieve rtl_arg_retrieve 190 rtl_arg_retrieve 191 (λenv,p. let 〈dest,src〉 ≝ p in 192 ! v ← rtl_arg_retrieve env src ; 193 reg_store dest v env) 194 rtl_fetch_ra 195 rtl_init_local 196 rtl_save_frame 197 rtl_setup_call 198 rtl_fetch_external_args 199 rtl_set_result 200 [ ] [ ] 201 rtl_read_result 202 eval_rtl_seq 203 eval_rtl_tailcall 204 eval_rtl_call. 186 make_sem_graph_params RTL 187 (mk_more_sem_unserialized_params ?? 188 RTL_state 189 reg_store reg_retrieve rtl_arg_retrieve 190 reg_store reg_retrieve rtl_arg_retrieve 191 reg_store reg_retrieve rtl_arg_retrieve 192 reg_store reg_retrieve rtl_arg_retrieve 193 rtl_arg_retrieve 194 (λenv,p. let 〈dest,src〉 ≝ p in 195 ! v ← rtl_arg_retrieve env src ; 196 reg_store dest v env) 197 rtl_fetch_ra 198 rtl_init_local 199 rtl_save_frame 200 rtl_setup_call 201 rtl_fetch_external_args 202 rtl_set_result 203 [ ] [ ] 204 rtl_read_result 205 eval_rtl_seq 206 eval_rtl_tailcall 207 eval_rtl_call 208 rtl_pop_frame 209 (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)). -
src/joint/semantics_paolo.ma
r2217 r2233 33 33 ; m: bemem 34 34 }. 35 36 coercion sem_state_params_to_state nocomposites: 37 ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0]. 35 38 36 39 record state_pc (semp : sem_state_params) : Type[0] ≝ … … 134 137 (* change of pc must be left to *_flow execution *) 135 138 ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars → 136 state st_pars → IO io_out io_in (state st_pars)139 F globals → state st_pars → IO io_out io_in (state st_pars) 137 140 ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars → 138 call_dest uns_pars → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))139 ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars.140 state st_pars →141 F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars)) 142 ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → 143 ext_call uns_pars → state st_pars → 141 144 IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars)) 142 ; pop_frame: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (state st_pars) 145 ; pop_frame: ∀globals.genv_t (fundef (F globals)) → F globals → state st_pars → res (state st_pars) 146 (* do something more in some op2 calculations (e.g. mark a register for correction 147 with spilled_no in ERTL) *) 148 ; post_op2 : ∀globals.genv_t (fundef (F globals)) → 149 Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars → 150 state st_pars → state st_pars 143 151 }. 144 152 … … 407 415 408 416 definition eval_seq_no_pc : 409 ∀ globals.∀p:sem_params. genv p globals → state p→410 ∀s:joint_seq p globals.417 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → 418 state p → ∀s:joint_seq p globals. 411 419 IO io_out io_in (state p) ≝ 412 λ globals,p,ge,st,seq.420 λp,globals,ge,curr_fn,st,seq. 413 421 match seq return λx.IO ??? with 414 422 [ extension_seq c ⇒ 415 eval_ext_seq … ge c st423 eval_ext_seq … ge c curr_fn st 416 424 | LOAD dst addrl addrh ⇒ 417 425 ! vaddrh ← dph_arg_retrieve … st addrh ; … … 447 455 let carry ≝ beval_of_bool carry in 448 456 ! st' ← acca_store … dacc_a v' st; 449 return set_carry … carry st'457 return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st') 450 458 | CLEAR_CARRY ⇒ 451 459 return set_carry … BVfalse st … … 484 492 485 493 definition eval_seq_pc : 486 ∀ globals.∀p:sem_params. genv p globals → state p →494 ∀p:sem_params.∀globals. genv p globals → state p → 487 495 ∀s:joint_seq p globals. 488 496 IO io_out io_in (step_flow p ? (step_flows … s)) ≝ 489 λ g,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with497 λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with 490 498 [ CALL_ID id args dest ⇒ 491 499 ! b ← opt_to_res \ldots [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???; … … 499 507 500 508 definition eval_step : 501 ∀globals.∀p:sem_params. genv p globals → state p → 509 ∀p:sem_params.∀globals. genv p globals → 510 joint_internal_function p globals → state p → 502 511 ∀s:joint_step p globals. 503 512 IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝ 504 λ globals,p,ge,st,s.513 λp,globals,ge,curr_fn,st,s. 505 514 match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with 506 515 [ step_seq s ⇒ 507 516 ! flow ← eval_seq_pc ?? ge st s ; 508 ! st' ← eval_seq_no_pc ?? ge st s ;517 ! st' ← eval_seq_no_pc ?? ge curr_fn st s ; 509 518 return 〈flow,st'〉 510 519 | COND src ltrue ⇒ … … 518 527 %1 % qed. 519 528 520 definition eval_fin_step_no_pc : ∀ globals: list ident.∀p:sem_params. genv p globals →521 (* result registers of current function *) call_dest p→ state p → ∀s : joint_fin_step p.529 definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals → 530 (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p. 522 531 IO io_out io_in (state p) ≝ 523 λ globals,p,ge,ret,st,s.532 λp,globals,ge,curr_fn,st,s. 524 533 match s return λx.IO ??? with 525 534 [ tailcall c ⇒ 526 !〈flow,st'〉 ← eval_ext_tailcall … ge c retst ;535 !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ; 527 536 return st' 528 537 | _ ⇒ return st … … 530 539 531 540 definition eval_fin_step_pc : 532 ∀ globals.∀p:sem_params. genv p globals → call_dest p→ state p →541 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p → 533 542 ∀s:joint_fin_step p. 534 543 IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝ 535 λ g,p,ge,ret,st,s.544 λp,g,ge,curr_fn,st,s. 536 545 match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with 537 546 [ tailcall c ⇒ 538 !〈flow,st'〉 ← eval_ext_tailcall … ge c retst ;547 !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ; 539 548 return flow 540 549 | GOTO l ⇒ return FRedirect … l … … 542 551 ]. %1 % qed. 543 552 544 definition do_call : ∀ globals: list ident.∀p:sem_params. genv p globals →553 definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals → 545 554 state p → Z → joint_internal_function p globals → call_args p → 546 555 res (state_pc p) ≝ 547 λ globals,p,ge,st,id,fn,args.556 λp,globals,ge,st,id,fn,args. 548 557 ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn) 549 558 args st ; … … 557 566 (* The pointer provided is the one to the *next* instruction. *) 558 567 definition eval_step_flow : 559 ∀ globals.∀p:sem_params.∀flows.genv p globals →568 ∀p:sem_params.∀globals.∀flows.genv p globals → 560 569 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝ 561 λ globals,p,flows,ge,st,nxt,cmd.570 λp,globals,flows,ge,st,nxt,cmd. 562 571 match cmd with 563 572 [ Redirect _ l ⇒ … … 570 579 ]. 571 580 572 definition eval_fin_step_flow : ∀ globals: list ident.∀p:sem_params.∀flows. genv p globals →581 definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals → 573 582 state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝ 574 λ globals,p,lbls,ge,st,curr,cmd.583 λp,globals,lbls,ge,st,curr,cmd. 575 584 match cmd with 576 585 [ FRedirect _ l ⇒ goto … ge l st curr … … 580 589 ! 〈st',ra〉 ← fetch_ra … st ; 581 590 ! fn ← fetch_function … ge curr ; 582 ! st'' ← pop_frame … ge (joint_if_result … fn)st';591 ! st'' ← pop_frame … ge fn st'; 583 592 return mk_state_pc ? st'' ra 584 593 ]. … … 591 600 match stmt with 592 601 [ sequential s nxt ⇒ 593 ! 〈flow,st'〉 ← eval_step … ge st s ;602 ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ; 594 603 ! nxtptr ← succ_pc ? p (pc … st) nxt ; 595 604 eval_step_flow … ge st' nxtptr flow 596 605 | final s ⇒ 597 let ret ≝ joint_if_result … curr_fn in 598 ! st' ← eval_fin_step_no_pc … ge ret st s ; 599 ! flow ← eval_fin_step_pc … ge ret st s ; 606 ! st' ← eval_fin_step_no_pc … ge curr_fn st s ; 607 ! flow ← eval_fin_step_pc … ge curr_fn st s ; 600 608 eval_fin_step_flow … ge st' (pc … st) flow 601 609 ].
Note: See TracChangeset
for help on using the changeset viewer.