- Timestamp:
- Mar 26, 2013, 2:01:15 PM (7 years ago)
- Location:
- src
- Files:
-
- 9 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTL.ma
r2946 r2952 140 140 res in 141 141 let res ≝ add_graph … l2 142 (sequential … (CALL ERTL ? (inl … (prog_main … p)) 4it) l3)142 (sequential … (CALL ERTL ? (inl … (prog_main … p)) 0 it) l3) 143 143 res in 144 144 let res ≝ add_graph … l3 -
src/ERTLptr/ERTLptr.ma
r2946 r2952 68 68 res in 69 69 let res ≝ add_graph … l2 70 (sequential … (CALL ERTLptr ? (inl … (prog_main … p)) 4it) l3)70 (sequential … (CALL ERTLptr ? (inl … (prog_main … p)) 0 it) l3) 71 71 res in 72 72 let res ≝ add_graph … l3 -
src/LIN/LIN.ma
r2946 r2952 34 34 let code ≝ 35 35 [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ; 36 〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 4it) it〉 ;36 〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ; 37 37 〈Some ? l3, GOTO ? l3〉 ] in 38 38 mk_joint_internal_function LIN (prog_var_names … p) -
src/LTL/LTL.ma
r2946 r2952 49 49 res in 50 50 let res ≝ add_graph … l2 51 (sequential … (CALL LTL ? (inl … (prog_main … p)) 4it) l3)51 (sequential … (CALL LTL ? (inl … (prog_main … p)) 0 it) l3) 52 52 res in 53 53 let res ≝ add_graph … l3 -
src/RTL/RTL.ma
r2946 r2952 113 113 res in 114 114 let res ≝ add_graph … l2 115 (sequential … (CALL RTL ? (inl … (prog_main … p)) (map … (Reg ?) rs) rs)l3)115 (sequential … (CALL RTL ? (inl … (prog_main … p)) [ ] l3) 116 116 res in 117 117 let res ≝ add_graph … l3 -
src/joint/Traces.ma
r2946 r2952 2 2 include "common/StructuredTraces.ma". 3 3 4 record evaluation_params : Type[1] ≝ 5 { globals: list ident 6 ; sparams:> sem_params 7 ; ev_genv: genv sparams globals 8 (* ; io_env : state sparams → ∀o:io_out.res (io_in o) *) 9 }. 4 record evaluation_params (p : sem_params) : Type[0] ≝ 5 { globals : list ident 6 ; ev_genv :> genv p globals 7 }. 10 8 11 9 record prog_params : Type[1] ≝ 12 { prog_spars : sem_params10 { prog_spars :> sem_params 13 11 ; prog : joint_program prog_spars 14 12 ; stack_sizes : ident → option ℕ … … 16 14 }. 17 15 18 lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l. 19 #A #B #f #P #l elim l -l [*] 20 #hd #tl #IH * 21 [ #Phd %1{Phd} 22 | #Ptl %2{(IH Ptl)} 23 ] 24 qed. 25 26 lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x. 27 #A #P #l elim l -l [*] #hd #tl #IH * 28 [ #Phd %{hd} %{Phd} %1 % 29 | #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1} 30 ] 31 qed. 32 33 lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l. 34 #A #P #l elim l -l [ #x *] #hd #tl #IH #x * 35 [ #EQ >EQ #H %1{H} 36 | #Intl #Px %2{(IH … Intl Px)} 37 ] 38 qed. 39 40 lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l. 41 #A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed. 42 43 lemma lookup_remove_elim : ∀tag,A.∀P : option A → Prop. 44 ∀m,i,j. 45 (i = j → P (None ?)) → 46 (i ≠ j → P (lookup tag A m i)) → 47 P (lookup tag A (remove tag A m j) i). 48 #tag #A #P #m #i #j #H1 #H2 49 @(eq_identifier_elim … i j) #H destruct 50 [ >lookup_remove_hit @H1 % | >lookup_remove_miss try @H2 assumption ] 51 qed. 52 53 definition make_global : prog_params → evaluation_params 54 ≝ 55 λpars. 56 let p ≝ prog pars in 57 let spars ≝ prog_spars pars in 58 let genv ≝ joint_globalenv spars p in 59 let get_pc_lbl ≝ λid,lbl. 60 ! bl ← block_of_funct_id … spars genv id ; 61 pc_of_label … genv bl lbl in 62 mk_evaluation_params 63 (prog_var_names … p) 64 spars 65 (mk_genv_gen ?? genv ? (stack_sizes pars) get_pc_lbl) 66 (* (prog_io pars) *). 67 #s #H 68 elim (find_symbol_exists … (λx.x) … p s ?) 69 [ #bl #EQ % 70 whd in match genv; whd in match find_symbol; whd in match drop_fn; normalize nodelta 71 @lookup_add_elim #H 72 [2: @lookup_remove_elim [ #EQ >EQ in H; * #ABS cases (ABS ?) % ] 73 #_ change with (find_symbol ? (globalenv … (λx.x) p) s = ? → ?) >EQ ] 74 #ABS destruct(ABS) ] 75 @Exists_append_r 76 @(Exists_mp … H) // 77 qed. 78 79 coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params 80 ≝ make_global on _p : prog_params to evaluation_params. 16 definition joint_make_global : ∀p : prog_params.evaluation_params (prog_spars p) ≝ 17 λp.mk_evaluation_params ? 18 (prog_var_names … (prog p)) 19 (joint_globalenv p (prog p) (stack_sizes p)). 20 21 coercion joint_make_global : ∀p : prog_params.evaluation_params (prog_spars p) ≝ 22 joint_make_global on p : prog_params to evaluation_params ?. 81 23 82 24 definition make_initial_state : 83 25 ∀pars: prog_params.state_pc pars ≝ 84 26 λpars.let p ≝ prog pars in 85 let sem_globals : evaluation_params ≝ pars in 86 let ge ≝ ev_genv sem_globals in 27 let ge ≝ ev_genv pars in 87 28 (* this is going to change shortly: globals will not reside in globalenv anymore *) 88 29 let m0 ≝ \snd (globalenv_allocmem … (λx.x) p) in … … 97 38 (* let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *) 98 39 let main ≝ prog_main … p in 99 let st ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m globals_size in 100 mk_state_pc ? (set_sp … spp st) init_pc (null_pc one). 40 let st ≝ mk_state pars 41 (* frames ≝ *)(Some ? (empty_framesT …)) 42 (* internal_stack ≝ *) empty_is 43 (* carry ≝ *)(BBbit false) 44 (* regs ≝ *)(empty_regsT … spp) 45 (* mem ≝ *)m 46 (* stack_usage ≝ *)globals_size in 47 mk_state_pc ? 48 (* state_no_pc ≝ *)(set_sp … spp st) 49 (* pc ≝ *)init_pc 50 (* last_pop ≝ *)(null_pc one). 51 @hide_prf 101 52 cases m0 in H; #m1 #m2 #m3 #H 102 53 whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥ … … 105 56 106 57 definition joint_classify_step : 107 ∀p : evaluation_params.joint_step p (globals … p)→ status_class ≝108 λp, stmt.58 ∀p,globals.joint_step p globals → status_class ≝ 59 λp,g,stmt. 109 60 match stmt with 110 61 [ CALL f args dest ⇒ cl_call … … 114 65 115 66 definition joint_classify_final : 116 ∀p : evaluation_params.joint_fin_step p → status_class ≝67 ∀p.joint_fin_step p → status_class ≝ 117 68 λp,stmt. 118 69 match stmt with … … 123 74 124 75 definition joint_classify : 125 ∀p : evaluation_params.state_pc p → status_class ≝126 λp, st.127 match fetch_statement … (ev_genv p) (pc … st) with76 ∀p.∀pars : evaluation_params p.state_pc p → status_class ≝ 77 λp,pars,st. 78 match fetch_statement … (ev_genv … pars) (pc … st) with 128 79 [ OK i_fn_s ⇒ 129 80 match \snd i_fn_s with 130 [ sequential s _ ⇒ joint_classify_step ps131 | final s ⇒ joint_classify_final ps81 [ sequential s _ ⇒ joint_classify_step … s 82 | final s ⇒ joint_classify_final … s 132 83 | FCOND _ _ _ _ ⇒ cl_jump 133 84 ] … … 135 86 ]. 136 87 137 lemma joint_classify_call : ∀p : evaluation_params.∀st.138 joint_classify p st = cl_call →88 lemma joint_classify_call : ∀p,pars,st. 89 joint_classify p pars st = cl_call → 139 90 ∃i_f,f',args,dest,next. 140 fetch_statement … (ev_genv p) (pc … st) =91 fetch_statement … (ev_genv … pars) (pc … st) = 141 92 OK ? 〈i_f, sequential … (CALL … f' args dest) next〉. 142 #p # st93 #p #pars #st 143 94 whd in match joint_classify; normalize nodelta 144 inversion (fetch_statement … (ev_genv p) (pc … st))95 inversion (fetch_statement ????) 145 96 [2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] 146 97 * #i_f * … … 153 104 qed. 154 105 155 definition joint_after_ret : ∀p :evaluation_params.156 (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝157 λp, s1,s2.158 match fetch_statement … (ev_genv p) (pc … s1) with106 definition joint_after_ret : ∀p : sem_params.∀pars. 107 (Σs : state_pc p.joint_classify p pars s = cl_call) → state_pc p → Prop ≝ 108 λp,pars,s1,s2. 109 match fetch_statement … (ev_genv … pars) (pc … s1) with 159 110 [ OK x ⇒ 160 111 match \snd x with … … 167 118 ]. 168 119 169 definition joint_call_ident : ∀p :evaluation_params.120 definition joint_call_ident : ∀p : sem_params.∀pars. 170 121 state_pc p → ident ≝ 171 122 (* this is a definition without a dummy ident : … … 193 144 (* with a dummy ident (which is never used as seen above in the commented script) 194 145 I think handling of the function is easier *) 195 λp, st.146 λp,pars,st. 196 147 let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *) 197 match fetch_statement … (ev_genv p) (pc … st) with148 match fetch_statement … (ev_genv … pars) (pc … st) with 198 149 [ OK x ⇒ 199 150 match \snd x with … … 202 153 [ CALL f' args dest ⇒ 203 154 match 204 (! bl ← block_of_call … (ev_genv p) f' st;205 fetch_internal_function … (ev_genv p) bl) with155 (! bl ← block_of_call … (ev_genv … pars) f' st; 156 fetch_internal_function … (ev_genv … pars) bl) with 206 157 [ OK i_f ⇒ \fst i_f 207 158 | _ ⇒ dummy … … 214 165 ]. 215 166 216 definition joint_tailcall_ident : ∀p: evaluation_params.167 definition joint_tailcall_ident : ∀p:sem_params.∀pars. 217 168 state_pc p → ident ≝ 218 λp, st.169 λp,pars,st. 219 170 let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *) 220 match fetch_statement … (ev_genv p) (pc … st) with171 match fetch_statement … (ev_genv … pars) (pc … st) with 221 172 [ OK x ⇒ 222 173 match \snd x with … … 225 176 [ TAILCALL _ f' args ⇒ 226 177 match 227 (! bl ← block_of_call … (ev_genv p) f' st;228 fetch_internal_function … (ev_genv p) bl) with178 (! bl ← block_of_call … (ev_genv … pars) f' st; 179 fetch_internal_function … (ev_genv … pars) bl) with 229 180 [ OK i_f ⇒ \fst i_f 230 181 | _ ⇒ dummy … … 256 207 257 208 definition cost_label_of_stmt : 258 ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝259 λp, s.match s with209 ∀p : sem_params.∀pars.joint_statement p (globals p pars) → option costlabel ≝ 210 λp,pars,s.match s with 260 211 [ sequential s _ ⇒ 261 212 match s with … … 267 218 268 219 definition joint_label_of_pc ≝ 269 λp : evaluation_params.220 λp,pars. 270 221 (λpc. 271 match fetch_statement … (ev_genv p ) pc with222 match fetch_statement … (ev_genv p pars) pc with 272 223 [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt) 273 224 | _ ⇒ None ? … … 278 229 mk_program_counter «mk_block (-1), refl …» (p1 one). 279 230 280 definition joint_final: ∀p: sem_params.∀globals. 281 genv p globals → state_pc p → option int ≝ 282 λp,globals,ge,st. 231 definition joint_final: ∀p: sem_params.∀pars. 232 state_pc p → option int ≝ 233 λp,pars,st. 234 let ge ≝ ev_genv p pars in 283 235 if eq_program_counter (pc … st) exit_pc' then 284 236 let ret ≝ call_dest_for_main ?? p in … … 294 246 (* as_status ≝ *) (state_pc p) 295 247 (* as_execute ≝ *) 296 (λs1,s2.eval_state … (ev_genv p) s1 = return s2)248 (λs1,s2.eval_state … (ev_genv … p) s1 = return s2) 297 249 (* (* as_init ≝ *) (make_initial_state p) *) 298 250 (* as_pc ≝ *) pcDeq 299 251 (* as_pc_of ≝ *) (pc …) 300 (* as_classify ≝ *) (joint_classify p)301 (* as_label_of_pc ≝ *) (joint_label_of_pc p)302 (* as_after_return ≝ *) (joint_after_ret p)303 (* as_result ≝ *) (joint_final p (globals ?) (ev_genv p))304 (* as_call_ident ≝ *) (λst.joint_call_ident p st)305 (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident p st).252 (* as_classify ≝ *) (joint_classify … p) 253 (* as_label_of_pc ≝ *) (joint_label_of_pc … p) 254 (* as_after_return ≝ *) (joint_after_ret … p) 255 (* as_result ≝ *) (joint_final … p) 256 (* as_call_ident ≝ *) (λst.joint_call_ident … p st) 257 (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident … p st). 306 258 307 259 (* alternative definition with integrated prog_params constructor *) -
src/joint/joint_fullexec.ma
r2946 r2952 2 2 include "common/Measurable.ma". 3 3 4 (* fullexec and co. *)5 record joint_global (p : sem_params) : Type[0] ≝6 { jglobals : list ident7 ; jgenv :> genv p jglobals8 }.9 10 definition eval_params_of_global : ∀p.joint_global p → evaluation_params ≝11 λp,gl.mk_evaluation_params (jglobals … gl) p gl.12 13 coercion eval_params_of_global : ∀p.∀gl : joint_global p.evaluation_params ≝14 eval_params_of_global on _gl : joint_global ? to evaluation_params.15 16 definition make_joint_global : ∀p : sem_params.17 (joint_program p × (ident → option ℕ)) →18 joint_global p ≝19 λpars, p_stack.20 let p ≝ \fst p_stack in21 let stack_sizes ≝ \snd p_stack in22 let ev_pars : evaluation_params ≝ mk_prog_params pars p stack_sizes in23 mk_joint_global pars24 (globals … ev_pars)25 (ev_genv … ev_pars).26 27 4 definition joint_exec: sem_params → trans_system io_out io_in ≝ 28 λG.mk_trans_system ?? ( joint_globalG) (λ_. state_pc G)29 (λenv.joint_final G (jglobals … env)env)5 λG.mk_trans_system ?? (evaluation_params G) (λ_. state_pc G) 6 (λenv.joint_final … env) 30 7 (λenv.λst.! st' ← eval_state … env st ; 31 let charge ≝ match joint_label_of_pc env (pc … st) with8 let charge ≝ match joint_label_of_pc … env (pc … st) with 32 9 [ Some c ⇒ Echarge c | None ⇒ E0 ] in 33 10 return 〈charge, st'〉). … … 37 14 λG.mk_fullexec ?? (joint_program G × (ident → option ℕ)) 38 15 (joint_exec G) 39 ( make_joint_global G)16 (λpr.joint_make_global (mk_prog_params G (\fst pr) (\snd pr))) 40 17 (λp_stacks. 41 18 return make_initial_state (mk_prog_params G (\fst p_stacks) (\snd p_stacks))). … … 44 21 preclassified_system ≝ 45 22 λG.mk_preclassified_system (joint_fullexec G) 46 (λenv.λst.¬is_none … (joint_label_of_pc (eval_params_of_global … env)(pc … st)))47 (λenv.joint_classify (eval_params_of_global … env))48 (λenv.λs.λ_.joint_call_ident (eval_params_of_global … env)s).23 (λenv.λst.¬is_none … (joint_label_of_pc … env (pc … st))) 24 (λenv.joint_classify … env) 25 (λenv.λs.λ_.joint_call_ident … env s). -
src/joint/joint_semantics.ma
r2946 r2952 17 17 ; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ? 18 18 ; stack_sizes : ident → option ℕ 19 ; get_pc_from_label : ident (* current function *) → label → res program_counter19 ; premain : F globals 20 20 }. 21 21 … … 119 119 *) 120 120 121 definition pre_main_id : ident ≝ an_identifier … one. 122 121 123 (* this can replace graph_fetch function and lin_fetch_function *) 122 124 definition fetch_function: 123 ∀F .124 ∀ge : genv_ t F.125 ∀F,globals. 126 ∀ge : genv_gen F globals. 125 127 (Σb.block_region b = Code) → 126 res (ident×F) ≝ 127 λF,ge,bl. 128 opt_to_res … [MSG BadFunction] 129 (! id ← symbol_for_block … ge bl ; 130 ! fd ← find_funct_ptr … ge bl ; 131 return 〈id, fd〉). 128 res (ident×(fundef (F globals))) ≝ 129 λF,g,ge,bl. 130 if eqZb (block_id bl) (-1) then 131 return 〈pre_main_id, Internal ? (premain … ge)〉 132 else 133 opt_to_res … [MSG BadFunction] 134 (! id ← symbol_for_block … ge bl ; 135 ! fd ← find_funct_ptr … ge bl ; 136 return 〈id, fd〉). 132 137 133 138 definition fetch_internal_function : 134 ∀F .135 ∀ge : genv_ t (fundef F).139 ∀F,globals. 140 ∀ge : genv_gen F globals. 136 141 (Σb.block_region b = Code) → 137 res (ident× F) ≝138 λF,g e,bl.142 res (ident×(F globals)) ≝ 143 λF,g,ge,bl. 139 144 ! 〈id, fd〉 ← fetch_function … ge bl ; 140 145 match fd with … … 143 148 ]. 144 149 145 lemma fetch_internal_function_no_minus_one :150 (* lemma fetch_internal_function_minus_one : 146 151 ∀F,V,i,p,bl. 147 152 block_id (pi1 … bl) = -1 → … … 154 159 cases (symbol_for_block ???) normalize // 155 160 qed. 161 *) 156 162 157 163 inductive call_kind : Type[0] ≝ … … 317 323 318 324 definition fetch_statement: ∀p : sem_params.∀globals. 319 ∀ge : genv _t (joint_function p globals). program_counter →325 ∀ge : genv p globals. program_counter → 320 326 res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝ 321 327 λp,globals,ge,ptr. … … 326 332 327 333 definition pc_of_label : ∀p : sem_params.∀globals. 328 genv _t (joint_function p globals)→ (Σb.block_region b = Code) → label → res program_counter ≝334 genv p globals → (Σb.block_region b = Code) → label → res program_counter ≝ 329 335 λp,globals,ge,bl,lbl. 330 336 ! 〈i, fn〉 ← fetch_internal_function … ge bl ; … … 378 384 379 385 definition goto: ∀p : sem_params.∀globals. 380 genv _t (joint_function p globals)→ label → state_pc p → res (state_pc p) ≝386 genv p globals → label → state_pc p → res (state_pc p) ≝ 381 387 λp,globals,ge,l,st. 382 388 ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ; … … 393 399 set_pc … newpc st. 394 400 395 definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) → 401 definition next_of_call_pc : ∀p : sem_params.∀globals. 402 genv p globals → 396 403 program_counter → res (succ p) ≝ 397 404 λp,globals,ge,pc. … … 488 495 ! bl ← find_symbol … ge id; 489 496 code_block_of_block bl). 490 497 498 definition get_pc_from_label : 499 ∀p : sem_params.∀globals. 500 genv p globals → 501 ident (* current function *) → label → res program_counter ≝ 502 λp,g,ge,id,lbl. 503 ! bl ← block_of_funct_id … p ge id ; 504 pc_of_label … ge bl lbl. 505 491 506 definition block_of_call ≝ λp : sem_params. 492 507 λglobals.λge: genv_t (joint_function p globals).λf.λst : state p. -
src/joint/semanticsUtils.ma
r2946 r2952 136 136 on _pars : sem_lin_params to sem_params. 137 137 138 (* watch out, implementation dependent: 139 an_identifier SymbolTag one must be unused (used for premain) 140 *) 141 definition pre_main_id : ident ≝ an_identifier … one. 142 138 (* TODO move elsewhere *) 143 139 lemma lookup_opt_pm_set_elim : ∀A.∀P : option A → Prop.∀p,q,o,m. 144 140 (p = q → P o) → … … 162 158 qed. 163 159 164 (* we just manually overwrite genv_t tables with the pre_main.165 the RTLabs → RTL pass will need to ensure no pre_main_id is actually present *)166 definition joint_globalenv :167 ∀pars : sem_params.joint_program pars → genv_t ? ≝168 λpars,prog.169 let genv ≝ drop_fn … pre_main_id (globalenv … (λx.x) prog) in170 mk_genv_t ?171 (insert … one (Internal … (pre_main_generator … pars prog)) (functions … genv))172 (nextfunction … genv)173 (add … (symbols … genv) pre_main_id (mk_block (-1)))174 ?.175 @hide_prf176 whd in match insert; normalize nodelta #b177 @lookup_opt_pm_set_elim #H destruct178 [ #_ %{pre_main_id} @lookup_add_hit ]179 #G cases (functions_inv … G) #id #EQ %{id}180 @lookup_add_elim #EQid destruct [2: assumption ]181 @⊥ whd in match drop_fn in EQ; normalize nodelta in EQ;182 >lookup_remove_hit in EQ; #ABS destruct183 qed.184 185 160 lemma fetch_statement_eq : ∀p:sem_params.∀g. 186 ∀ge : genv _t (joint_function p g).∀ptr : program_counter.161 ∀ge : genv p g.∀ptr : program_counter. 187 162 ∀i,fn,s. 188 163 fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 → … … 196 171 197 172 lemma fetch_statement_inv : ∀p:sem_params.∀g. 198 ∀ge : genv _t (joint_function p g).∀ptr : program_counter.173 ∀ge : genv p g.∀ptr : program_counter. 199 174 ∀i,fn,s. 200 175 fetch_statement … ge ptr = OK … 〈i, fn, s〉 → … … 204 179 #p #g #ge #ptr #i #fn #s #H 205 180 elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H 206 elim (bind_inversion ????? H) #s' * #H181 elim (bind_inversion ????? H) #s' * -H #H 207 182 lapply (opt_eq_from_res ???? H) -H #EQ2 208 183 whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2} … … 421 396 include alias "common/Pointers.ma". 422 397 423 lemma fetch_function_transf : 424 ∀A,B,V,init.∀prog_in : program A V. 425 ∀trans : ∀vars.A vars → B vars. 426 let prog_out ≝ transform_program … prog_in trans in 398 (* TODO move *) 399 lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l. 400 #A #P #Q #l #H elim l -l [2: #hd #tl #IH] * #G whd /3 by or_introl, or_intror/ qed. 401 402 definition joint_globalenv : 403 ∀p : sem_params.∀pr:joint_program p. 404 (ident → option ℕ) → genv p (prog_var_names … pr) ≝ 405 λp,prog,stacksizes. 406 let genv ≝ globalenv … (λx.x) prog in 407 mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog). 408 #s #H 409 elim (find_symbol_exists ?? (λx.x) … prog s ?) 410 [ #bl #EQ >EQ % #ABS destruct ] 411 @Exists_append_r 412 @(Exists_mp … H) // 413 qed. 414 415 lemma opt_to_res_bind : ∀X,Y,m,f,e.opt_to_res Y e (! x ← m ; f x) = 416 ! x ← opt_to_res X e m ; opt_to_res Y e (f x). 417 #X #Y * [2: #x] #f #e % qed. 418 419 lemma fetch_function_transf: 420 ∀src,dst : sem_params.∀prog_in : joint_program src. 421 ∀stacksizes. 422 ∀trans : ∀vars.joint_function src vars → joint_function dst vars. 423 let prog_out ≝ 424 mk_joint_program dst 425 (transform_program … prog_in trans) (init_cost_label … prog_in) in 427 426 ∀bl. 428 fetch_function … (globalenv … init prog_out) bl = 429 ! 〈i, f〉 ← fetch_function … (globalenv … init prog_in) bl ; 430 return 〈i, trans … f〉. 431 #A #B #V #init #prog_in #trans #bl 432 whd in match fetch_function; normalize nodelta 433 >(symbol_for_block_transf A B V init prog_in trans) 434 cases (symbol_for_block ???) [ % ] #id >m_return_bind >m_return_bind 427 fetch_function … (joint_globalenv … prog_out stacksizes) bl = 428 if eqZb (block_id bl) (-1) then 429 return 〈pre_main_id, Internal ? (pre_main_generator … dst prog_out)〉 430 else 431 ! 〈id, f〉 ← fetch_function … (joint_globalenv … prog_in stacksizes) bl ; 432 return 〈id, trans … f〉. 433 #src #dst #p #sizes #tf whd 434 lapply (transform_program_match … tf p) 435 #MATCH 436 whd in match fetch_function; 437 whd in match joint_globalenv; normalize nodelta 438 #bl @eqZb_elim #Hbl normalize nodelta [ % ] 439 >symbol_for_block_transf 440 >opt_to_res_bind >opt_to_res_bind in ⊢ (???%); >m_bind_bind 441 @m_bind_ext_eq #id 435 442 whd in match find_funct_ptr; normalize nodelta 436 whd in match (block_region (pi1 ?? bl)); 437 cases (block_id (pi1 ?? bl)) [2,3: #p] normalize nodelta try % 438 >(functions_transf A B V init prog_in trans p) 439 cases (lookup_opt ???) // 443 cases bl -bl ** [2,3: #p] normalize nodelta #_ try % 444 lapply (functions_match … (globalenv_match … MATCH) p) try @(λx.x) 445 [#v #w * //] 446 lapply (sym_eq ????) 447 whd in match prog_var_names; normalize nodelta 448 #E >(K ?? E) -E normalize nodelta 449 cases (lookup_opt ???) [2: #x ] normalize nodelta 450 cases (lookup_opt ???) [2,4: #y ] normalize nodelta 451 * % 440 452 qed. 441 453 442 454 lemma fetch_internal_function_transf : 443 ∀A,B,V,init.∀prog_in : program (λvars.fundef (A vars)) V. 444 ∀trans : ∀vars.A vars → B vars. 445 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in 455 ∀src,dst : sem_params.∀prog_in : joint_program src. 456 ∀stacksizes. 457 ∀trans : ∀vars.joint_closed_internal_function src vars → joint_closed_internal_function dst vars. 458 let prog_out ≝ 459 mk_joint_program dst 460 (transform_program … prog_in (λvars.transf_fundef … (trans vars))) (init_cost_label … prog_in) in 446 461 ∀bl. 447 fetch_internal_function … (globalenv … init prog_out) bl = 448 ! 〈i, f〉 ← fetch_internal_function … (globalenv … init prog_in) bl ; 449 return 〈i, trans … f〉. 450 #A #B #V #init #prog #trans #bl 451 whd in match fetch_internal_function; normalize nodelta 452 >(fetch_function_transf … prog) 453 cases (fetch_function ???) 454 [ * #id * #f % | #e % ] 462 fetch_internal_function … (joint_globalenv … prog_out stacksizes) bl = 463 if eqZb (block_id bl) (-1) then 464 return 〈pre_main_id, pre_main_generator … dst prog_out〉 465 else 466 ! 〈i, f〉 ← fetch_internal_function … (joint_globalenv … prog_in stacksizes) bl ; 467 return 〈i, trans … f〉. 468 #src #dst #p #sizes #tf whd 469 #bl whd in match fetch_internal_function; normalize nodelta 470 >(fetch_function_transf … p) 471 @eqZb_elim #Hbl [%] normalize nodelta >m_bind_bind >m_bind_bind 472 @m_bind_ext_eq * #id * #f % 455 473 qed. 456 474 … … 485 503 definition b_graph_transform_program_props ≝ 486 504 λsrc,dst : sem_graph_params. 505 λstacksizes. 487 506 λdata,prog_in. 488 507 λinit_regs : block → list register. … … 490 509 λf_regs : block → label → list register. 491 510 let prog_out ≝ b_graph_transform_program src dst data prog_in in 492 let src_genv ≝ joint_globalenv src prog_in in493 let dst_genv ≝ joint_globalenv dst prog_out in511 let src_genv ≝ joint_globalenv src prog_in stacksizes in 512 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 494 513 ∀bl,def_in. 495 514 block_id … bl ≠ -1 → … … 503 522 lemma make_b_graph_transform_program_props : 504 523 ∀src,dst:sem_graph_params. 524 ∀stacksizes. 505 525 ∀data : ∀globals.joint_closed_internal_function src globals → 506 526 bound_b_graph_translate_data src dst globals. 507 527 ∀prog_in : joint_program src. 508 528 let prog_out ≝ b_graph_transform_program … data prog_in in 509 let src_genv ≝ joint_globalenv src prog_in in510 let dst_genv ≝ joint_globalenv dst prog_out in529 let src_genv ≝ joint_globalenv src prog_in stacksizes in 530 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 511 531 ∃init_regs : block → list register. 512 532 ∃f_lbls : block → label → list label. 513 533 ∃f_regs : block → label → list register. 514 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs.534 b_graph_transform_program_props src dst stacksizes data prog_in init_regs f_lbls f_regs. 515 535 cases daemon (* TOREDO 516 536 #src #dst #data #prog_in … … 612 632 qed. 613 633 634 lemma if_elim' : ∀A : Type[0].∀P : A → Prop.∀b : bool.∀c1,c2 : A. 635 (b → P c1) → (¬(bool_to_Prop b) → P c2) → P (if b then c1 else c2). 636 #A #P * /3 by Prop_notb/ qed. 637 614 638 lemma b_graph_transform_program_fetch_internal_function : 615 639 ∀src,dst:sem_graph_params. 640 ∀stacksizes. 616 641 ∀data : ∀globals.joint_closed_internal_function src globals → 617 642 bound_b_graph_translate_data src dst globals. … … 620 645 ∀f_lbls : block → label → list label. 621 646 ∀f_regs : block → label → list register. 622 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →647 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs → 623 648 let prog_out ≝ b_graph_transform_program … data prog_in in 624 let src_genv ≝ joint_globalenv src prog_in in625 let dst_genv ≝ joint_globalenv dst prog_out in649 let src_genv ≝ joint_globalenv src prog_in stacksizes in 650 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 626 651 ∀bl : Σbl.block_region … bl = Code.∀id,def_in. 627 652 block_id … bl ≠ -1 → … … 632 657 b_graph_translate_props src dst ? init_data 633 658 def_in def_out (f_lbls bl) (f_regs bl). 634 #src #dst # data #prog_in659 #src #dst #stacksizes #data #prog_in 635 660 #init_regs #f_lbls #f_regs #props 636 661 #bl #id #def_in #NEQ 637 662 #H @('bind_inversion H) * #id' * #def_in' -H 638 normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct 639 @('bind_inversion (opt_eq_from_res … H)) -H #id' #EQ1 640 #H @('bind_inversion H) -H #def_in' #H 641 whd in ⊢ (??%%→?); #EQ destruct 663 normalize nodelta [2: #_ whd in ⊢ (??%%→?); #ABS destruct ] 664 whd in match fetch_function; normalize nodelta 665 >(eqZb_false … NEQ) normalize nodelta 666 #H @('bind_inversion (opt_eq_from_res … H)) -H #id'' #EQ1 667 #H @('bind_inversion H) -H #def_in'' #H 668 whd in ⊢ (??%%→??%%→?); #EQ2 #EQ3 destruct 642 669 cases (props … NEQ H) 643 670 #loc_data * #def_out ** #H1 #H2 #H3 … … 646 673 whd in match fetch_internal_function; 647 674 whd in match fetch_function; normalize nodelta 648 cases daemon (* TOREDO 675 >(eqZb_false … NEQ) normalize nodelta 649 676 >symbol_for_block_transf >EQ1 >m_return_bind 650 >H1 % *)677 >H1 % 651 678 qed. 652 679 653 680 lemma b_graph_transform_program_fetch_statement : 654 ∀src,dst:sem_graph_params. 681 ∀src,dst:sem_graph_params.∀stacksizes. 655 682 ∀data : ∀globals.joint_closed_internal_function src globals → 656 683 bound_b_graph_translate_data src dst globals. … … 659 686 ∀f_lbls : block → label → list label. 660 687 ∀f_regs : block → label → list register. 661 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →688 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs → 662 689 let prog_out ≝ b_graph_transform_program … data prog_in in 663 let src_genv ≝ joint_globalenv src prog_in in664 let dst_genv ≝ joint_globalenv dst prog_out in690 let src_genv ≝ joint_globalenv src prog_in stacksizes in 691 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 665 692 ∀pc,id,def_in,s. 666 693 block_id … (pc_block … pc) ≠ -1 → … … 686 713 | FCOND abs _ _ _ ⇒ Ⓧabs 687 714 ]. 688 #src #dst # data #prog_in715 #src #dst #stacksizes #data #prog_in 689 716 #init_regs #f_lbls #f_regs #props 690 717 #pc #id #def_in #s #NEQ … … 701 728 702 729 lemma b_graph_transform_program_fetch_statement_plus : 703 ∀src,dst:sem_graph_params. 730 ∀src,dst:sem_graph_params.∀stacksizes. 704 731 ∀data : ∀globals.joint_closed_internal_function src globals → 705 732 bound_b_graph_translate_data src dst globals. … … 708 735 ∀f_lbls : block → label → list label. 709 736 ∀f_regs : block → label → list register. 710 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →737 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs → 711 738 let prog_out ≝ b_graph_transform_program … data prog_in in 712 let src_genv ≝ joint_globalenv src prog_in in713 let dst_genv ≝ joint_globalenv dst prog_out in739 let src_genv ≝ joint_globalenv src prog_in stacksizes in 740 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in 714 741 ∀pc,id,def_in,s. 715 742 block_id … (pc_block … pc) ≠ -1 → … … 744 771 | FCOND abs _ _ _ ⇒ Ⓧabs 745 772 ]. 746 #src #dst # data #prog_in773 #src #dst #stacksizes #data #prog_in 747 774 #init_regs #f_lbls #f_regs #props 748 775 #pc #id #def_in #s #NEQ
Note: See TracChangeset
for help on using the changeset viewer.