Changeset 2952 for src/joint/Traces.ma
 Timestamp:
 Mar 26, 2013, 2:01:15 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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 *)
Note: See TracChangeset
for help on using the changeset viewer.