- Timestamp:
- Jul 19, 2012, 6:13:54 PM (9 years ago)
- Location:
- src
- Files:
-
- 3 added
- 9 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTL_paolo.ma
r2214 r2217 25 25 | ertl_frame_size: register → ertl_seq. 26 26 27 definition ertl_uns_params ≝ mk_unserialized_params 28 (mk_step_params 27 definition ERTL_uns ≝ mk_unserialized_params 29 28 (* acc_a_reg ≝ *) register 30 29 (* acc_b_reg ≝ *) register … … 42 41 (* ext_call ≝ *) void 43 42 (* ext_tailcall ≝ *) void 44 ) 45 (mk_local_params 46 (mk_funct_params 47 (* resultT ≝ *) unit 48 (* paramsT ≝ *) ℕ) 49 (* localsT ≝ *) register). 43 (* paramsT ≝ *) ℕ 44 (* localsT ≝ *) register. 50 45 51 definition ERTL ≝ mk_graph_params ertl_uns_params.46 definition ERTL ≝ mk_graph_params ERTL_uns. 52 47 definition ertl_program ≝ joint_program ERTL. 53 48 -
src/LIN/joint_LTL_LIN_paolo.ma
r2214 r2217 13 13 14 14 definition LTL_LIN : unserialized_params ≝ mk_unserialized_params 15 (mk_step_params16 15 (* acc_a_reg ≝ *) unit 17 16 (* acc_b_reg ≝ *) unit … … 29 28 (* ext_call ≝ *) void 30 29 (* ext_tailcall ≝ *) void 31 ) 32 (mk_local_params 33 (mk_funct_params 34 (* resultT ≝ *) unit 35 (* paramsT ≝ *) unit) 36 (* localsT ≝ *) void). 30 (* paramsT ≝ *) unit 31 (* localsT ≝ *) void. 37 32 38 33 interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)). -
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. -
src/RTLabs/RTLabsToRTL_paolo.ma
r2214 r2217 8 8 include alias "ASM/BitVector.ma". 9 9 include alias "arithmetics/nat.ma". 10 11 definition rtl_fresh_reg: 12 ∀globals.freshT RTL globals register ≝ 13 λglobals,def. 14 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 15 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉. 16 17 definition rtl_fresh_reg_no_local : 18 ∀globals.freshT RTL globals register ≝ 19 λglobals,def. 20 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 21 〈set_runiverse ?? def runiverse, r〉. 22 10 23 definition size_of_sig_type ≝ 11 24 λsig. … … 48 61 λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf). 49 62 50 definition m_fresh : ∀tag.state_monad (universe tag) (identifier tag) ≝51 λtag,univ.let pr ≝ fresh … univ in 〈\snd pr, \fst pr〉.52 53 let rec register_freshes (n: nat) on n :54 state_monad (universe RegisterTag) (Σl.|l| = n) ≝55 match n return λx.state_monad ? (Σl.|l| = x) with56 [ O ⇒ return «[ ],?»57 | S n' ⇒58 ! r ← m_fresh ?;59 ! res ← register_freshes n';60 return «r::res,?»61 ].[2: cases res -res #res #EQ <EQ] % qed.62 63 63 definition initialize_local_env_internal : 64 (universe RegisterTag × local_env) → (register×typ) → (universe RegisterTag × local_env) ≝ 65 λlenv_runiverse,r_sig. 66 let 〈runiverse,lenv〉 ≝ lenv_runiverse in 64 ∀globals. 65 ((joint_internal_function RTL globals) × local_env) → (register×typ) → 66 ((joint_internal_function RTL globals) × local_env) ≝ 67 λglobals,def_env,r_sig. 68 let 〈def,lenv〉 ≝ def_env in 67 69 let 〈r, sig〉 ≝ r_sig in 68 70 let size ≝ size_of_sig_type sig in 69 let 〈runiverse,rs〉 ≝ register_freshes size runiverse in 70 〈runiverse,add … lenv r rs〉. 71 72 definition initialize_local_env : 73 list (register×typ) → 74 state_monad (universe RegisterTag) local_env ≝ 75 λregisters,runiverse. 76 foldl … initialize_local_env_internal 〈runiverse,empty_map …〉 registers. 71 let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in 72 〈def,add … lenv r rs〉. 77 73 78 74 include alias "common/Identifiers.ma". … … 84 80 | cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ? 85 81 ].cases prf #A #B assumption qed. 82 83 definition initialize_local_env : 84 ∀globals. 85 list (register×typ) → 86 freshT RTL globals local_env ≝ 87 λglobals,registers,def. 88 foldl ?? (initialize_local_env_internal globals) 〈def,empty_map …〉 registers. 89 90 lemma initialize_local_env_in : ∀globals,l,def,r. 91 Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def). 92 #globals #l #U #r @(list_elim_left … l) 93 [ * 94 | * #tl #sig #hd #IH #G elim (Exists_append … G) -G 95 whd in match initialize_local_env; normalize nodelta 96 >foldl_step change with (initialize_local_env ???) in match (foldl ?????); 97 [ #H lapply (IH H) 98 | * [2: *] #EQ destruct(EQ) 99 ] 100 cases (initialize_local_env ???) 101 #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta 102 elim (repeat_fresh ??????) #U'' #rs 103 [ >mem_set_add @orb_Prop_r assumption 104 | @mem_set_add_id 105 ] 106 qed. 107 108 example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr. 109 // qed-. 110 example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr. 111 // qed-. 112 113 definition initialize_locals_params_ret : 114 ∀globals. 115 (* locals *) list (register×typ) → 116 (* params *) list (register×typ) → 117 (* return *) option (register×typ) → 118 freshT RTL globals local_env ≝ 119 λglobals,locals,params,ret,def. 120 let 〈def',lenv〉 as EQ ≝ 121 initialize_local_env globals 122 ((match ret with 123 [ Some r_sig ⇒ [r_sig] 124 | None ⇒ [ ] 125 ]) @ locals @ params) def in 126 let locals' ≝ map_list_local_env lenv locals ? in 127 let params' ≝ map_list_local_env lenv params ? in 128 let ret' ≝ match ret return λx.ret = x → ? with 129 [ Some r_sig ⇒ λprf.find_local_env (\fst r_sig) lenv ? 130 | None ⇒ λ_.[ ] 131 ] (refl …) in 132 let def'' ≝ 133 mk_joint_internal_function RTL globals 134 (joint_if_luniverse … def') (joint_if_runiverse … def') ret' 135 params' locals' (joint_if_stacksize … def') 136 (joint_if_code … def') (joint_if_entry … def') (joint_if_exit … def') in 137 〈def'', lenv〉. @hide_prf 138 [ >(proj2_rewrite ????? EQ) 139 @initialize_local_env_in >prf %1 % 140 |*: >(proj2_rewrite ????? EQ) 141 @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr))) 142 [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params)) 143 [ #a #H @Exists_append_r @Exists_append_r @H 144 | generalize in match params; 145 ] 146 | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) locals)) 147 [ #a #H @Exists_append_r @Exists_append_l @H 148 | generalize in match locals; 149 ] 150 ] 151 #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G} 152 ] 153 qed. 86 154 87 155 definition make_addr ≝ … … 834 902 qed. 835 903 836 lemma initialize_local_env_in : ∀l,runiverse,r.837 Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env l runiverse).838 #l #U #r @(list_elim_left … l)839 [ *840 | * #tl #sig #hd #IH #G elim (Exists_append … G) -G841 whd in match initialize_local_env; normalize nodelta842 >foldl_step change with (initialize_local_env ??) in match (foldl ?????);843 [ #H lapply (IH H)844 | * [2: *] #EQ destruct(EQ)845 ]846 cases (initialize_local_env ??)847 #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta848 elim (register_freshes ??) #U'' #rs849 [ >mem_set_add @orb_Prop_r assumption850 | @mem_set_add_id851 ]852 qed.853 854 definition proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.855 // qed.856 definition proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.857 // qed.858 859 860 904 (* XXX: we use a "hack" here to circumvent the proof obligations required to 861 905 create res, an empty internal_function record. we insert into our graph … … 865 909 λglobals: list ident. 866 910 λdef. 867 let runiverse ≝ f_reggen def in 868 let 〈runiverse',lenv〉 as pr_eq ≝ initialize_local_env 869 (match f_result def with [ None ⇒ [ ] | Some r_sig ⇒ [r_sig]] @ 870 f_params def @ f_locals def) runiverse in 871 let params' ≝ map_list_local_env lenv (f_params def) ? in 872 let locals' ≝ map_list_local_env lenv (f_locals def) ? in 873 let result' ≝ 874 match (f_result def) return λx.f_result def = x → ? with 875 [ None ⇒ λ_.[ ] 876 | Some r_typ ⇒ λEQ. 877 find_local_env (\fst r_typ) lenv ? 878 ] (refl …) 879 in 911 let runiverse' ≝ f_reggen def in 880 912 let luniverse' ≝ f_labgen def in 881 913 let stack_size' ≝ f_stacksize def in … … 887 919 let graph' ≝ add LabelTag ? graph' exit' 888 920 (RETURN …) in 921 let init ≝ 922 mk_joint_internal_function RTL globals luniverse' runiverse' [ ] [ ] 923 [ ] stack_size' graph' (pi1 … entry') (pi1 … exit') in 924 let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals 925 (f_locals def) (f_params def) (f_result def) init in 889 926 let f_trans ≝ λlbl,stmt,def. 890 927 let pr ≝ translate_statement … lenv stmt in 891 b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in 892 let res ≝ 893 mk_joint_internal_function RTL globals luniverse' runiverse' result' params' 894 locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in 895 foldi … f_trans (f_graph def) res. 896 897 [1,2: >graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add 898 | >(proj2_rewrite ????? pr_eq) 899 @initialize_local_env_in >EQ normalize nodelta %1 % 900 |*: >(proj2_rewrite ????? pr_eq) 901 @(All_mp ??? (λpr.initialize_local_env_in ?? (\fst pr))) 902 [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_locals def))) 903 [ #a #H @Exists_append_r @Exists_append_r @H 904 | generalize in match (f_locals def); 905 ] 906 | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_params def))) 907 [ #a #H @Exists_append_r @Exists_append_l @H 908 | generalize in match (f_params def); 909 ] 910 ] 911 #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G} 912 ] 928 b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in 929 foldi … f_trans (f_graph def) init'. 930 @hide_prf 931 >graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add 913 932 qed. 914 933 -
src/joint/Joint_paolo.ma
r2214 r2217 24 24 | | / 25 25 unserialized_params 26 | \ 27 | \ 28 | local_params 29 | | 30 step_params funct_params 31 32 step_params : types needed to define steps (stmts with a default fallthrough) 26 27 unserialized_params : things unrelated to serialization (i.e. graph or linear 28 form) 33 29 stmt_params : adds successor type needed to define statements 34 30 funct_params : types of result register and parameters of function 35 local_params : adds types of local registers36 31 params : adds type of code and related properties *) 37 32 … … 75 70 definition zero_byte : Byte ≝ bv_zero 8. 76 71 77 record step_params : Type[1] ≝72 record unserialized_params : Type[1] ≝ 78 73 { acc_a_reg: Type[0] (* registers that will eventually need to be A *) 79 74 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *) … … 95 90 ; ext_tailcall : Type[0] 96 91 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *) 92 ; paramsT : Type[0] 93 ; localsT: Type[0] 97 94 }. 98 95 99 inductive joint_seq (p: step_params) (globals: list ident): Type[0] ≝96 inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝ 100 97 | COMMENT: String → joint_seq p globals 101 98 | COST_LABEL: costlabel → joint_seq p globals … … 145 142 extension_branch on _s : ext_branch ? to joint_branch ?.*) 146 143 147 inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝144 inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝ 148 145 | step_seq : joint_seq p globals → joint_step p globals 149 146 | COND: acc_a_reg p → label → joint_step p globals. … … 170 167 ]. 171 168 172 definition step_forall_labels : ∀p : step_params.∀globals.169 definition step_forall_labels : ∀p.∀globals. 173 170 (label → Prop) → joint_step p globals → Prop ≝ 174 171 λp,g,P,inst. All … P (step_labels … inst). 175 172 176 173 definition step_classifier : 177 ∀p : step_params.∀globals.174 ∀p.∀globals. 178 175 joint_step p globals → status_class ≝ λp,g,s. 179 176 match s with … … 187 184 ]. 188 185 189 record funct_params : Type[1] ≝190 { resultT : Type[0]191 ; paramsT : Type[0]192 }.193 194 record local_params : Type[1] ≝195 { funct_pars :> funct_params196 ; localsT: Type[0]197 }.198 199 record unserialized_params : Type[1] ≝200 { u_inst_pars :> step_params201 ; u_local_pars :> local_params202 }.203 204 186 record stmt_params : Type[1] ≝ 205 187 { uns_pars :> unserialized_params … … 208 190 }. 209 191 210 inductive joint_fin_step (p: step_params): Type[0] ≝192 inductive joint_fin_step (p: unserialized_params): Type[0] ≝ 211 193 | GOTO: label → joint_fin_step p 212 194 | RETURN: joint_fin_step p … … 468 450 forall_statements_i … (statement_closed … code) code. 469 451 470 (* CSC: special case where localsT is a list of registers (RTL and ERTL) *)471 definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.472 (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).473 474 452 record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝ 475 453 { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) … … 478 456 following, right? *) 479 457 (* joint_if_sig: signature; -- dropped in front end *) 480 joint_if_result : resultTp;458 joint_if_result : call_dest p; 481 459 joint_if_params : paramsT p; 482 460 joint_if_locals : list (localsT p); (* use void where no locals are present *) -
src/joint/TranslateUtils_paolo.ma
r2214 r2217 1 1 include "joint/Joint_paolo.ma". 2 2 include "joint/blocks.ma". 3 include "utilities/hide.ma". 3 4 4 5 (* general type of functions generating fresh things *) 5 (* type T is the syntactic type of the generated things *) 6 (* (sig for RTLabs registers, unit in others ) *) 7 definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g). 8 9 definition rtl_ertl_fresh_reg: 10 ∀inst_pars,funct_pars,globals. 11 freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝ 12 λinst_pars,var_pars,globals,def. 13 let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in 14 〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉. 6 definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g). 15 7 16 8 include alias "basics/lists/list.ma". 17 let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n : 18 freshT globals (rtl_ertl_params inst_pars funct_pars) 19 (Σl : list register. |l| = n) ≝ 20 let ret_type ≝ (Σl : list register. |l| = n) in 21 match n return λx.x = n → freshT … ret_type with 22 [ O ⇒ λeq'.return (mk_Sig … [ ] ?) 23 | S n' ⇒ λeq'. 24 ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n'; 25 ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals; 26 return (mk_Sig … (reg :: regs') ?) 27 ](refl …). <eq' normalize [//] elim regs' #l #eql >eql // 28 qed. 9 let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ) 10 on n : 11 freshT pars globals (Σl : list A. |l| = n) ≝ 12 match n return λx.freshT … (Σl.|l| = x) with 13 [ O ⇒ return «[ ], ?» 14 | S n' ⇒ 15 ! regs' ← repeat_fresh … fresh n'; 16 ! reg ← fresh ; 17 return «reg::regs',?» 18 ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed. 29 19 30 20 definition fresh_label: … … 126 116 ∀globals: list ident. 127 117 (* fresh register creation *) 128 freshT g lobals g_pars (localsT … g_pars) →118 freshT g_pars globals (localsT … g_pars) → 129 119 ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) + 130 120 bind_seq_block g_pars globals (joint_fin_step g_pars). … … 147 137 ∀globals: list ident. 148 138 (* fresh register creation *) 149 freshT globals dst_g_pars (localsT dst_g_pars) →139 freshT dst_g_pars globals (localsT dst_g_pars) → 150 140 (* initialized function definition with empty graph *) 151 141 joint_internal_function dst_g_pars globals → -
src/joint/semantics_paolo.ma
r2214 r2217 86 86 λpars,globals,ge,p.function_of_block pars globals ge (pblock p). 87 87 88 inductive step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝88 inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝ 89 89 | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *) 90 90 | Init : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *) 91 91 | Proceed : ∀flows.step_flow p F flows. (* go to implicit successor *) 92 92 93 inductive fin_step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝93 inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝ 94 94 | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls) 95 95 | FTailInit : Z → F → call_args p → fin_step_flow p F Call … … 126 126 ; fetch_external_args: external_function → state st_pars → 127 127 res (list val) 128 ; set_result: list val → state st_pars → res (state st_pars)128 ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars) 129 129 ; call_args_for_main: call_args uns_pars 130 130 ; call_dest_for_main: call_dest uns_pars 131 131 132 132 (* from now on, parameters that use the type of functions *) 133 ; read_result: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (list beval)133 ; read_result: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (list beval) 134 134 (* change of pc must be left to *_flow execution *) 135 135 ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars → 136 136 state st_pars → IO io_out io_in (state st_pars) 137 137 ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars → 138 state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_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 139 ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars. 140 140 state st_pars → 141 141 IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars)) 142 ; pop_frame: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (state st_pars)142 ; pop_frame: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (state st_pars) 143 143 }. 144 144 … … 206 206 fixed once we fully implement external functions. *) 207 207 let vs ≝ [mk_val ? evres] in 208 ! st ← set_result … p' vs st : IO ???;208 ! st ← set_result … p' vs dest st : IO ???; 209 209 return 〈Proceed ???, st〉 210 210 ]. … … 326 326 327 327 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals. 328 genv p globals → cpointer → res (joint_statement p globals) ≝ 328 genv p globals → cpointer → 329 res ((joint_internal_function p globals) × (joint_statement p globals)) ≝ 329 330 λp,msp,globals,ge,ptr. 330 331 let pt ≝ point_of_pointer ? msp ptr in 331 332 ! fn ← fetch_function … ge ptr ; 332 opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt). 333 ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt); 334 return 〈fn, stmt〉. 333 335 334 336 definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. … … 517 519 518 520 definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals → 519 state p → ∀s : joint_fin_step p.521 (* result registers of current function *) call_dest p → state p → ∀s : joint_fin_step p. 520 522 IO io_out io_in (state p) ≝ 521 λglobals,p,ge, st,s.523 λglobals,p,ge,ret,st,s. 522 524 match s return λx.IO ??? with 523 525 [ tailcall c ⇒ 524 !〈flow,st'〉 ← eval_ext_tailcall … ge c st ;526 !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ; 525 527 return st' 526 528 | _ ⇒ return st … … 528 530 529 531 definition eval_fin_step_pc : 530 ∀globals.∀p:sem_params. genv p globals → state p →532 ∀globals.∀p:sem_params. genv p globals → call_dest p → state p → 531 533 ∀s:joint_fin_step p. 532 534 IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝ 533 λg,p,ge, st,s.535 λg,p,ge,ret,st,s. 534 536 match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with 535 537 [ tailcall c ⇒ 536 !〈flow,st'〉 ← eval_ext_tailcall … ge c st ;538 !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ; 537 539 return flow 538 540 | GOTO l ⇒ return FRedirect … l … … 577 579 | _ ⇒ 578 580 ! 〈st',ra〉 ← fetch_ra … st ; 579 ! st'' ← pop_frame … ge st; 581 ! fn ← fetch_function … ge curr ; 582 ! st'' ← pop_frame … ge (joint_if_result … fn) st'; 580 583 return mk_state_pc ? st'' ra 581 584 ]. … … 583 586 definition eval_statement : 584 587 ∀globals.∀p:sem_params.genv p globals → 585 state_pc p → joint_ statement p globals →588 state_pc p → joint_internal_function p globals → joint_statement p globals → 586 589 IO io_out io_in (state_pc p) ≝ 587 λglobals,p,ge,st, stmt.590 λglobals,p,ge,st,curr_fn,stmt. 588 591 match stmt with 589 592 [ sequential s nxt ⇒ … … 592 595 eval_step_flow … ge st' nxtptr flow 593 596 | final s ⇒ 594 ! st' ← eval_fin_step_no_pc … ge st s ; 595 ! flow ← eval_fin_step_pc … ge st 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 ; 596 600 eval_fin_step_flow … ge st' (pc … st) flow 597 601 ]. … … 600 604 state_pc p → IO io_out io_in (state_pc p) ≝ 601 605 λglobals,p,ge,st. 602 ! s← fetch_statement ? p … ge (pc … st) : IO ???;603 eval_statement … ge st s.606 ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???; 607 eval_statement … ge st fn s. 604 608 605 609 (* Paolo: what if in an intermediate language main finishes with an external … … 609 613 genv p globals → cpointer → state_pc p → option int ≝ 610 614 λglobals,p,ge,exit,st.res_to_opt ? ( 611 do s← fetch_statement ? p … ge (pc … st);615 do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st); 612 616 match s with 613 617 [ final s' ⇒ 614 618 match s' with 615 619 [ RETURN ⇒ 616 do 〈st ,ra〉 ← fetch_ra … st;620 do 〈st',ra〉 ← fetch_ra … st; 617 621 if eq_pointer ra exit then 618 do vals ← read_result … ge st;622 do vals ← read_result … ge (joint_if_result … fn) st' ; 619 623 Word_of_list_beval vals 620 624 else
Note: See TracChangeset
for help on using the changeset viewer.