- Timestamp:
- Jul 19, 2012, 6:13:54 PM (9 years ago)
- Location:
- src/RTL
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTLToERTL_paolo.ma
r2214 r2217 6 6 7 7 include alias "basics/lists/list.ma". 8 9 definition ertl_fresh_reg: 10 ∀globals.freshT ERTL globals register ≝ 11 λglobals,def. 12 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 13 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉. 8 14 9 15 definition save_hdws : … … 101 107 definition allocate_regs : 102 108 ∀globals,rs.rs_set rs → 103 state_monad (joint_internal_function ERTL globals)(list (register×Register)) ≝109 freshT ERTL globals (list (register×Register)) ≝ 104 110 λglobals,rs,saved,def. 105 111 let allocate_regs_internal ≝ 106 112 λr: Register. 107 113 λdef_sregs. 108 let 〈def, r'〉 ≝ rtl_ertl_fresh_reg … (\fst def_sregs) in114 let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in 109 115 〈def, 〈r', r〉::\snd def_sregs〉 in 110 116 rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉. … … 118 124 let end_lbl ≝ joint_if_exit … def in 119 125 state_run … def ( 120 ! sral ← rtl_ertl_fresh_reg … ;121 ! srah ← rtl_ertl_fresh_reg … ;126 ! sral ← ertl_fresh_reg … ; 127 ! srah ← ertl_fresh_reg … ; 122 128 ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ; 123 ! prologue' ← bcompile … ( rtl_ertl_fresh_reg …) (prologue … params sral srah sregs) ;129 ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ; 124 130 let epilogue' ≝ epilogue … ret_regs sral srah sregs in 125 131 ! def' ← state_get … ; … … 258 264 graph' entry' exit' in 259 265 let def'' ≝ b_graph_translate … 260 ( rtl_ertl_fresh_reg …)266 (ertl_fresh_reg …) 261 267 def' 262 268 (translate_step globals) -
src/RTL/RTL_paolo.ma
r2214 r2217 12 12 13 13 definition RTL_uns ≝ mk_unserialized_params 14 (mk_step_params15 14 (* acc_a_reg ≝ *) register 16 15 (* acc_b_reg ≝ *) register … … 28 27 (* ext_call ≝ *) rtl_call 29 28 (* ext_tailcall ≝ *) rtl_tailcall 30 ) 31 (mk_local_params 32 (mk_funct_params 33 (* resultT ≝ *) (list register) 34 (* paramsT ≝ *) (list register)) 35 (* localsT ≝ *) register). 29 (* paramsT ≝ *) (list register) 30 (* localsT ≝ *) register. 36 31 37 32 definition RTL ≝ mk_graph_params RTL_uns. … … 98 93 99 94 definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params 100 (mk_step_params101 95 (* acc_a_reg ≝ *) register 102 96 (* acc_b_reg ≝ *) register … … 114 108 (* ext_call ≝ *) rtl_call 115 109 (* ext_tailcall ≝ *) void 116 ) 117 (mk_local_params 118 (mk_funct_params 119 (* resultT ≝ *) (list register) 120 (* paramsT ≝ *) (list register)) 121 (* localsT ≝ *) register)). 110 (* paramsT ≝ *) (list register) 111 (* localsT ≝ *) register). 122 112 123 113 definition rtl_ntc_program ≝ joint_program RTL_ntc. -
src/RTL/semantics_paolo.ma
r1999 r2217 6 6 record frame: Type[0] ≝ 7 7 { fr_ret_regs: list register 8 ; fr_pc: address9 ; fr_sp: pointer8 ; fr_pc: cpointer 9 ; fr_sp: xpointer 10 10 ; fr_carry: beval 11 11 ; fr_regs: register_env beval 12 12 }. 13 13 14 definition rtl_sem_state_params: sem_state_params ≝14 definition RTL_state : sem_state_params ≝ 15 15 mk_sem_state_params 16 16 (list frame) … … 19 19 (λ_.empty_map …). 20 20 21 definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : rtl_argument.21 definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument. 22 22 match a with 23 23 [ Reg r ⇒ reg_retrieve env r 24 | Imm b ⇒ return (BVByte b)24 | Imm b ⇒ return b 25 25 ]. 26 26 … … 30 30 31 31 definition rtl_fetch_ra: 32 state rtl_sem_state_params → res ((state rtl_sem_state_params) × address) ≝32 state RTL_state → res ((state RTL_state) × cpointer) ≝ 33 33 λst. 34 34 match st_frms ? st with … … 36 36 | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ]. 37 37 38 definition rtl_init_locals : 39 list register → register_env beval → register_env beval ≝ 40 λlocals,env. 41 foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals. 42 38 definition rtl_init_local : 39 register → register_env beval → register_env beval ≝ 40 λlocal,env.add … env local BVundef. 43 41 44 42 definition rtl_setup_call: 45 nat → list register → list rtl_argument → state rtl_sem_state_params → res (state rtl_sem_state_params) ≝43 nat → list register → list psd_argument → state RTL_state → res (state RTL_state) ≝ 46 44 λstacksize,formal_arg_regs,actual_arg_regs,st. 47 45 let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in … … 53 51 (OK … (empty_map …)) formal_arg_regs actual_arg_regs ; 54 52 OK … 55 (set_regs rtl_sem_state_paramsnew_regs53 (set_regs RTL_state new_regs 56 54 (set_m … mem 57 (set_sp … (mk_pointer XData b ? (mk_offset 0)) st))).55 (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))). 58 56 cases b * #r #off #E >E % 59 57 qed. 60 58 61 definition rtl_save_frame ≝ λl.λretregs.λst : state rtl_sem_state_params.59 definition rtl_save_frame ≝ λl.λretregs.λst : state RTL_state. 62 60 let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in 63 set_frms rtl_sem_state_params frame st.61 OK … (set_frms RTL_state frame st). 64 62 65 63 (*CSC: XXXX, for external functions only*) 66 axiom rtl_fetch_external_args: external_function → state rtl_sem_state_params → res (list val). 67 axiom rtl_set_result: list val → state rtl_sem_state_params → res (state rtl_sem_state_params). 68 69 definition rtl_msu_params : 70 more_sem_unserialized_params rtl_uns_params ≝ 71 mk_more_sem_unserialized_params rtl_uns_params rtl_sem_state_params 72 reg_store reg_retrieve rtl_arg_retrieve 73 reg_store reg_retrieve rtl_arg_retrieve 74 reg_store reg_retrieve rtl_arg_retrieve 75 reg_store reg_retrieve rtl_arg_retrieve 76 rtl_arg_retrieve 77 (λenv,p. let 〈dest,src〉 ≝ p in 78 ! v ← rtl_arg_retrieve env src ; 79 reg_store dest v env) 80 rtl_fetch_ra 81 rtl_init_locals 82 rtl_save_frame 83 rtl_setup_call 84 rtl_fetch_external_args 85 rtl_set_result 86 [ ] [ ] (*dummy*). 87 88 (* alias *) 89 definition rtl_reg_store : register→beval→state rtl_sem_state_params→ 90 res (state rtl_sem_state_params) ≝ acca_store ? rtl_msu_params. 91 definition rtl_reg_retrieve : state rtl_sem_state_params→register→res beval ≝ 92 acca_retrieve ? rtl_msu_params. 64 axiom rtl_fetch_external_args: external_function → state RTL_state → res (list val). 65 axiom rtl_set_result: list val → list register → state RTL_state → res (state RTL_state). 66 67 definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st. 68 definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st). 93 69 94 70 definition rtl_read_result : 95 ∀globals. genv globals rtl_params → state rtl_sem_state_params → res (list beval) ≝ 96 λglobals,ge,st. 97 ! p ← code_pointer_of_address (pc … st) ; 98 ! fn ← fetch_function … ge p ; 99 m_mmap … (rtl_reg_retrieve st) (joint_if_result … fn). 71 ∀globals.genv RTL globals → list register → state RTL_state → res (list beval) ≝ 72 λglobals,ge,rets,st. 73 m_list_map … (rtl_reg_retrieve st) rets. 100 74 101 75 (*CSC: we could use a dependent type here: the list of return values should have … … 103 77 saves the OutOfBounds exception *) 104 78 definition rtl_pop_frame: 105 ∀globals. genv globals rtl_params → state rtl_sem_state_params→106 res (state rtl_sem_state_params) ≝107 λglobals,ge, st.108 do ret_vals ← rtl_read_result … ge st ;79 ∀globals. genv RTL globals → list register → state RTL_state → 80 res (state RTL_state) ≝ 81 λglobals,ge,ret,st. 82 do ret_vals ← rtl_read_result … ge ret st ; 109 83 match st_frms ? st with 110 84 [ nil ⇒ Error ? [MSG EmptyStack] … … 117 91 (OK … st) (fr_ret_regs hd) ; 118 92 OK … 119 (set_frms rtl_sem_state_paramstl120 (set_regs rtl_sem_state_params(fr_regs hd)93 (set_frms RTL_state tl 94 (set_regs RTL_state (fr_regs hd) 121 95 (set_sp … (fr_sp hd) 122 96 (set_carry … (fr_carry hd) 123 97 (set_m … (free … (m … st) (pblock (sp … st))) st)))))]. 124 98 125 126 99 (* This code is quite similar to eval_call_block: can we factorize it out? *) 127 definition eval_tail_call_block: 128 ∀globals.genv globals rtl_params → state rtl_sem_state_params → 129 block → call_args rtl_uns_params → IO io_out io_in (trace×(state rtl_sem_state_params)) ≝ 130 λglobals,ge,st,b,args. 131 ! 〈next, tr, st〉 ← eval_call_block_preamble ? rtl_params rtl_msu_params ge st b args (None ?) ; 132 match next with 133 [ None ⇒ (* Paolo: external tailcall, copied from evaluation of return, is it right? *) 134 ! 〈st,ra〉 ← fetch_ra … st ; 135 ! st ← rtl_pop_frame … ge st; 136 return 〈tr,st〉 137 | Some lbl ⇒ 138 return 〈tr,st〉 139 ]. 140 141 definition block_of_register_pair: register → register → state rtl_sem_state_params → res block ≝ 100 definition eval_tailcall_block: 101 ∀globals.genv RTL globals → state RTL_state → 102 block → call_args RTL → 103 (* this is where the result of the current function should be stored *) 104 call_dest RTL → 105 IO io_out io_in 106 ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×(state RTL_state)) ≝ 107 λglobals,ge,st,b,args,ret. 108 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 109 match fd with 110 [ Internal fd ⇒ 111 return 〈FTailInit ?? (block_id b) fd args, st〉 112 | External fn ⇒ 113 ! params ← rtl_fetch_external_args … fn st : IO ???; 114 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; 115 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 116 (* CSC: XXX bug here; I think I should split it into Byte-long 117 components; instead I am making a singleton out of it. To be 118 fixed once we fully implement external functions. *) 119 let vs ≝ [mk_val ? evres] in 120 ! st ← rtl_set_result … vs ret st : IO ???; 121 return 〈FEnd2 ??, st〉 122 ]. 123 124 definition block_of_register_pair: register → register → state RTL_state → res block ≝ 142 125 λr1,r2,st. 143 126 do v1 ← rtl_reg_retrieve st r1 ; … … 146 129 OK … (pblock ptr). 147 130 148 definition rtl_exec_extended:149 ∀globals. genv globals rtl_params →150 rtl_ instruction_extension → state rtl_sem_state_params → address→151 IO io_out io_in ( (option (label)) × trace × (state rtl_sem_state_params)) ≝152 λglobals,ge,stm,st ,next_addr.131 definition eval_rtl_seq: 132 ∀globals. genv RTL globals → 133 rtl_seq → state RTL_state → 134 IO io_out io_in (state RTL_state) ≝ 135 λglobals,ge,stm,st. 153 136 match stm with 154 [ rtl_st _ext_stack_address dreg1 dreg2 ⇒137 [ rtl_stack_address dreg1 dreg2 ⇒ 155 138 let sp ≝ sp ? st in 156 139 ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ; 157 140 ! st ← rtl_reg_store dreg1 dpl st ; 158 ! st ← rtl_reg_store dreg2 dph st ; 159 return 〈None label,E0, st〉 160 | rtl_st_ext_call_ptr r1 r2 args dest ⇒ 161 ! b ← block_of_register_pair r1 r2 st : IO ???; 162 eval_call_block_preamble ? rtl_params rtl_msu_params 163 ge st b args (Some ? 〈dest,next_addr〉) ]. 164 165 definition rtl_exec_fin_extended: 166 ∀globals. genv globals rtl_params → 167 rtl_statement_extension → state rtl_sem_state_params → 168 IO io_out io_in (trace × (state rtl_sem_state_params)) ≝ 169 λglobals,ge,stm,st. 141 rtl_reg_store dreg2 dph st 142 ]. 143 144 definition eval_rtl_call: 145 ∀globals. genv RTL globals → 146 rtl_call → state RTL_state → 147 IO io_out io_in ((step_flow RTL ? Call)×(state RTL_state)) ≝ 148 λglobals,ge,stm,st. 149 match stm with 150 [ rtl_call_ptr r1 r2 args dest ⇒ 151 ! b ← block_of_register_pair r1 r2 st : IO ???; 152 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 153 match fd with 154 [ Internal fd ⇒ 155 return 〈Init ?? (block_id b) fd args dest, st〉 156 | External fn ⇒ 157 ! params ← rtl_fetch_external_args … fn st : IO ???; 158 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; 159 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 160 (* CSC: XXX bug here; I think I should split it into Byte-long 161 components; instead I am making a singleton out of it. To be 162 fixed once we fully implement external functions. *) 163 let vs ≝ [mk_val ? evres] in 164 ! st ← rtl_set_result … vs dest st : IO ???; 165 return 〈Proceed ???, st〉 166 ] 167 ]. 168 169 definition eval_rtl_tailcall: 170 ∀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. 170 174 match stm with 171 [ rtl_ st_ext_tailcall_id id args ⇒175 [ rtl_tailcall_id id args ⇒ 172 176 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???; 173 eval_tail _call_block … ge st b args174 | rtl_ st_ext_tailcall_ptr r1 r2 args ⇒177 eval_tailcall_block … ge st b args ret 178 | rtl_tailcall_ptr r1 r2 args ⇒ 175 179 ! b ← block_of_register_pair r1 r2 st : IO ???; 176 eval_tail _call_block … ge st b args180 eval_tailcall_block … ge st b args ret 177 181 ]. 178 182 179 definition rtl_msg_params : more_sem_genv_params rtl_params ≝ 180 mk_more_sem_genv_params rtl_params rtl_msu_params 183 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 [ ] [ ] 181 201 rtl_read_result 182 rtl_exec_extended 183 rtl_exec_fin_extended 184 rtl_pop_frame. 185 186 187 188 definition rtl_sem_params : sem_params ≝ make_sem_graph_params … rtl_msg_params. 189 190 definition rtl_fullexec ≝ joint_fullexec … rtl_sem_params. 202 eval_rtl_seq 203 eval_rtl_tailcall 204 eval_rtl_call.
Note: See TracChangeset
for help on using the changeset viewer.