Changeset 2286 for src/RTL/semantics.ma
- Timestamp:
- Aug 2, 2012, 3:18:11 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/semantics.ma
r2176 r2286 6 6 record frame: Type[0] ≝ 7 7 { fr_ret_regs: list register 8 ; fr_pc: address9 ; fr_sp: pointer10 ; fr_carry: be val8 ; fr_pc: cpointer 9 ; fr_sp: xpointer 10 ; fr_carry: bebit 11 11 ; fr_regs: register_env beval 12 12 }. 13 13 14 definition rtl_more_sem_params: more_sem_params rtl_params_ := 15 mk_more_sem_params rtl_params_ 16 (list frame) [] (register_env beval) (λ_.empty_map …) [] [](*dummy*) 17 reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve 18 reg_store reg_retrieve reg_store reg_retrieve 19 (λlocals,dest_src. 20 do v ← reg_retrieve locals (\snd dest_src) ; 21 reg_store (\fst dest_src) v locals). 22 definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params. 23 24 definition rtl_init_locals : 25 list register → register_env beval → register_env beval ≝ 26 λlocals,env. 27 foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals. 14 definition RTL_state : sem_state_params ≝ 15 mk_sem_state_params 16 (list frame) 17 [ ] 18 (register_env beval) 19 (λ_.empty_map …). 20 21 definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument. 22 match a with 23 [ Reg r ⇒ reg_retrieve env r 24 | Imm b ⇒ return b 25 ]. 28 26 29 27 (*CSC: could we use here a dependent type to avoid the Error case? *) … … 32 30 33 31 definition rtl_fetch_ra: 34 state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝32 RTL_state → res (RTL_state × cpointer) ≝ 35 33 λst. 36 34 match st_frms ? st with … … 38 36 | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ]. 39 37 40 definition rtl_result_regs: 41 ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝ 42 λglobals,ge,st. 43 do fn ← graph_fetch_function … globals ge st ; 44 OK … (joint_if_result … fn). 45 46 (*CSC: we could use a dependent type here: the list of return values should have 47 the same length of the list of return registers that store the values. This 48 saves the OutOfBounds exception *) 49 definition rtl_pop_frame: 50 ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝ 51 λglobals,ge,st. 52 do ret_regs ← rtl_result_regs … ge st ; 53 do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ; 54 match st_frms ? st with 55 [ nil ⇒ Error ? [MSG EmptyStack] 56 | cons hd tl ⇒ 57 do st ← 58 mfold_left_i ?? 59 (λi.λst.λreg. 60 do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ; 61 greg_store rtl_sem_params reg v st) 62 (OK … st) (fr_ret_regs hd) ; 63 OK … 64 (set_frms rtl_sem_params tl 65 (set_regs rtl_sem_params (fr_regs hd) 66 (set_sp … (fr_sp hd) 67 (set_carry … (fr_carry hd) 68 (set_m … (free … (m … st) (pblock (sp … st))) st)))))]. 69 70 definition rtl_call_function: 71 nat → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝ 38 definition rtl_init_local : 39 register → register_env beval → register_env beval ≝ 40 λlocal,env.add … env local BVundef. 41 42 definition rtl_setup_call: 43 nat → list register → list psd_argument → RTL_state → res RTL_state ≝ 72 44 λstacksize,formal_arg_regs,actual_arg_regs,st. 73 45 let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in … … 75 47 mfold_left2 … 76 48 (λlenv,dest,src. 77 do v ← greg_retrieve … stsrc ;49 do v ← rtl_arg_retrieve … (regs ? st) src ; 78 50 OK … (add … lenv dest v)) 79 51 (OK … (empty_map …)) formal_arg_regs actual_arg_regs ; 80 52 OK … 81 (set_regs rtl_sem_paramsnew_regs53 (set_regs RTL_state new_regs 82 54 (set_m … mem 83 (set_sp … (mk_pointer b (mk_offset 0)) st))). 84 (*cases b * #r #off #E >E % 85 qed.*) 86 87 definition rtl_save_frame: 88 address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝ 89 λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st. 90 let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st) in 91 let st ≝ set_frms rtl_sem_params frame st in 92 rtl_call_function stacksize formal_arg_regs actual_arg_regs st. 55 (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))). 56 cases b * #r #off #E >E % 57 qed. 58 59 definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state. 60 let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in 61 OK … (set_frms RTL_state frame st). 93 62 94 63 (*CSC: XXXX, for external functions only*) 95 axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val). 96 axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params). 97 98 definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝ 99 λglobals. 100 mk_more_sem_params1 … rtl_more_sem_params graph_succ_p (graph_pointer_of_label …) 101 (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …) 102 rtl_init_locals rtl_save_frame (rtl_pop_frame …) 103 rtl_fetch_external_args rtl_set_result. 104 definition rtl_sem_params1: ∀globals. sem_params1 … globals ≝ 105 λglobals. mk_sem_params1 … (rtl_more_sem_params1 globals). 106 107 definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝ 108 λr1,r2,st. 109 do v1 ← greg_retrieve rtl_sem_params st r1 ; 110 do v2 ← greg_retrieve rtl_sem_params st r2 ; 111 do ptr ← pointer_of_address 〈v1,v2〉 ; 112 OK … (pblock ptr). 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 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). 69 70 definition rtl_read_result : 71 ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝ 72 λglobals,ge,rets,st. 73 m_list_map … (rtl_reg_retrieve st) rets. 74 75 (*CSC: we could use a dependent type here: the list of return values should have 76 the same length of the list of return registers that store the values. This 77 saves the OutOfBounds exception *) 78 definition rtl_pop_frame: 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 83 do ret_vals ← rtl_read_result … ge ret st ; 84 match st_frms ? st with 85 [ nil ⇒ Error ? [MSG EmptyStack] 86 | cons hd tl ⇒ 87 do st ← 88 mfold_left_i … 89 (λi.λst.λreg. 90 do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ; 91 rtl_reg_store reg v st) 92 (OK … st) (fr_ret_regs hd) ; 93 OK … 94 (set_frms RTL_state tl 95 (set_regs RTL_state (fr_regs hd) 96 (set_sp … (fr_sp hd) 97 (set_carry … (fr_carry hd) 98 (set_m … (free … (m … st) (pblock (sp … st))) st)))))]. 113 99 114 100 (* This code is quite similar to eval_call_block: can we factorize it out? *) 115 definition eval_tail_call_block: 116 ∀globals.genv … (rtl_params globals) → state rtl_sem_params → 117 block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝ 118 λglobals,ge,st,b,args. 119 ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr … ge b); 101 definition eval_tailcall_block: 102 ∀globals.genv RTL globals → RTL_state → 103 block → call_args RTL → 104 (* this is where the result of the current function should be stored *) 105 call_dest RTL → 106 IO io_out io_in 107 ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝ 108 λglobals,ge,st,b,args,ret. 109 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 120 110 match fd with 121 [ Internal fn ⇒ 122 let st ≝ set_m … (free … (m … st) (pblock (sp … st))) st in 123 ! st ← rtl_call_function (joint_if_stacksize … fn) (joint_if_params … fn) args st ; 124 let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in 125 let l' ≝ joint_if_entry … fn in 126 ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ; 127 return 〈 E0, st〉 128 | External fn ⇒ ?(* 129 ! params ← fetch_external_args … fn st; 130 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)); 111 [ Internal fd ⇒ 112 return 〈FTailInit ?? (block_id b) fd args, st〉 113 | External fn ⇒ 114 ! params ← rtl_fetch_external_args … fn st : IO ???; 115 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; 131 116 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 132 117 (* CSC: XXX bug here; I think I should split it into Byte-long 133 118 components; instead I am making a singleton out of it. To be 134 119 fixed once we fully implement external functions. *) 135 let vs ≝ [mk_val ? evres] in 136 ! st ← set_result … vs st; 137 let st ≝ set_pc … ra st in 138 ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 *) 139 ]. 140 cases daemon (*CSC: XXX tailcall to external function not implemented yet; 141 it needs alls other functions on external calls *) 142 qed. 143 144 definition rtl_exec_extended: 145 ∀globals. genv globals (rtl_params globals) → 146 rtl_statement_extension → label → state rtl_sem_params → 147 IO io_out io_in (trace × (state rtl_sem_params)) ≝ 148 λglobals,ge,stm,l,st. 120 let vs ≝ [mk_val ? evres] in 121 ! st ← rtl_set_result … vs ret st : IO ???; 122 return 〈FEnd2 ??, st〉 123 ]. 124 125 definition block_of_register_pair: register → register → RTL_state → res block ≝ 126 λr1,r2,st. 127 do v1 ← rtl_reg_retrieve st r1 ; 128 do v2 ← rtl_reg_retrieve st r2 ; 129 do ptr ← pointer_of_address 〈v1,v2〉 ; 130 OK … (pblock ptr). 131 132 definition eval_rtl_seq: 133 ∀globals. genv RTL globals → 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. 149 137 match stm with 150 [ rtl_st _ext_stack_address dreg1 dreg2 ⇒138 [ rtl_stack_address dreg1 dreg2 ⇒ 151 139 let sp ≝ sp ? st in 152 140 ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ; 153 ! st ← greg_store rtl_sem_params dreg1 dpl st ; 154 ! st ← greg_store rtl_sem_params dreg2 dph st ; 155 ! st ← next … (rtl_sem_params1 globals) l st ; 156 return 〈E0, st〉 157 | rtl_st_ext_call_ptr r1 r2 args dest ⇒ 158 ! b ← block_of_register_pair r1 r2 st : IO ??? ; 159 ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) : IO ??? ; 160 eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals)) 161 ge st b args dest ra 162 | rtl_st_ext_tailcall_id id args ⇒ 141 ! st ← rtl_reg_store dreg1 dpl st ; 142 rtl_reg_store dreg2 dph st 143 ]. 144 145 definition eval_rtl_call: 146 ∀globals. genv RTL globals → 147 rtl_call → RTL_state → 148 IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝ 149 λglobals,ge,stm,st. 150 match stm with 151 [ rtl_call_ptr r1 r2 args dest ⇒ 152 ! b ← block_of_register_pair r1 r2 st : IO ???; 153 ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?); 154 match fd with 155 [ Internal fd ⇒ 156 return 〈Init ?? (block_id b) fd args dest, st〉 157 | External fn ⇒ 158 ! params ← rtl_fetch_external_args … fn st : IO ???; 159 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; 160 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); 161 (* CSC: XXX bug here; I think I should split it into Byte-long 162 components; instead I am making a singleton out of it. To be 163 fixed once we fully implement external functions. *) 164 let vs ≝ [mk_val ? evres] in 165 ! st ← rtl_set_result … vs dest st : IO ???; 166 return 〈Proceed ???, st〉 167 ] 168 ]. 169 170 definition eval_rtl_tailcall: 171 ∀globals. genv RTL globals → 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 176 match stm with 177 [ rtl_tailcall_id id args ⇒ 163 178 ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???; 164 eval_tail _call_block … ge st b args165 | rtl_ st_ext_tailcall_ptr r1 r2 args ⇒179 eval_tailcall_block … ge st b args ret 180 | rtl_tailcall_ptr r1 r2 args ⇒ 166 181 ! b ← block_of_register_pair r1 r2 st : IO ???; 167 eval_tail _call_block … ge st b args182 eval_tailcall_block … ge st b args ret 168 183 ]. 169 184 170 definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝ 171 λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …). 172 173 definition rtl_fullexec ≝ 174 joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)). 185 definition RTL_semantics ≝ 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)).
Note: See TracChangeset
for help on using the changeset viewer.