Changeset 2473 for src/joint/Traces.ma
 Timestamp:
 Nov 16, 2012, 6:59:24 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Traces.ma
r2470 r2473 11 11 12 12 13 (* move elsewhere *)14 definition is_internal_function_of_program :15 ∀A,B.program (λvars.fundef (A vars)) B → ident → Prop ≝16 λA,B,prog,i.∃ifd.In … (prog_funct ?? prog) 〈i, Internal ? ifd〉.17 18 lemma opt_elim : ∀A.∀m : option A.∀P : option A → Prop.19 (m = None ? → P (None ?)) →20 (∀x.m = Some ? x → P (Some ? x)) → P m.21 #A * [2: #x] #P #H1 #H222 [ @H2  @H1 ] % qed.23 24 axiom find_funct_ptr_symbol_inversion:25 ∀F,V,init. ∀p: program F V.26 ∀id: ident. ∀b: block. ∀f: F ?.27 find_symbol ? (globalenv ?? init p) id = Some ? b →28 find_funct_ptr ? (globalenv ?? init p) b = Some ? f →29 In … (prog_funct ?? p) 〈id, f〉.30 31 lemma is_internal_function_of_program_ok :32 ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i.33 is_internal_function ?? (globalenv ?? init prog) i →34 is_internal_function_of_program ?? prog i.35 #A #B #init #prog #i whd in ⊢ (%→%); * #ifn36 @(opt_elim … (find_symbol … i)) [#_ #ABS normalize in ABS; destruct(ABS) ]37 #bl #EQbl >m_return_bind #EQfind %{ifn}38 @(find_funct_ptr_symbol_inversion … EQbl EQfind)39 qed.40 13 41 14 record prog_params : Type[1] ≝ … … 45 18 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) 46 19 }. 20 21 lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l. 22 #A #B #f #P #l elim l l [*] 23 #hd #tl #IH * 24 [ #Phd %1{Phd} 25  #Ptl %2{(IH Ptl)} 26 ] 27 qed. 28 29 lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x. 30 #A #P #l elim l l [*] #hd #tl #IH * 31 [ #Phd %{hd} %{Phd} %1 % 32  #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1} 33 ] 34 qed. 35 36 lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l. 37 #A #P #l elim l l [ #x *] #hd #tl #IH #x * 38 [ #EQ >EQ #H %1{H} 39  #Intl #Px %2{(IH … Intl Px)} 40 ] 41 qed. 47 42 48 43 definition make_global : prog_params → evaluation_params … … 60 55 (* (prog_io pars) *). 61 56 [ @(is_internal_function_of_program_ok … (pi2 … i)) 62  (* TODO or TOBEFOUND *) 63 cases daemon 57  #s #H 58 lapply (map_Exists … H) H #H 59 elim (Exists_In … H) H ** #id #r #v * #id_in #EQ destruct(EQ) 60 elim (find_symbol_exists ??????? id_in) 61 [ #bl #EQ >EQ % #ABS destruct(ABS)] 64 62 ] 65 63 qed. … … 90 88 match ? return λx.description_of_function … main = x → ? with 91 89 [ Internal fn ⇒ λprf. 92 let main : Σi : ident.is_internal_function ??? ?≝ «main, ?» in90 let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in 93 91 ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ; 94 92 let pc' ≝ eval_internal_call_pc … ge main in … … 157 155 [ #fn normalize nodelta 158 156 lapply (refl … (description_of_function … (ev_genv p) fn)) 159 elim (description_of_function ?? ??) in ⊢ (???%→%); #fd157 elim (description_of_function ?? fn) in ⊢ (???%→%); #fd 160 158 #EQfd 161 159  #e … … 171 169 qed. 172 170 171 definition joint_after_ret : ∀p:evaluation_params. 172 (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝ 173 λp,s1,s2. 174 match fetch_statement ? p … (ev_genv p) (pc … s1) with 175 [ OK x ⇒ 176 match \snd x with 177 [ sequential s next ⇒ 178 pc … s2 = succ_pc p p (pc … s1) next 179  _ ⇒ False (* never happens *) 180 ] 181  _ ⇒ False (* never happens *) 182 ]. 183 173 184 definition joint_call_ident : ∀p:evaluation_params. 174 185 (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝ 186 (* this is a definition without a dummy ident : 175 187 λp,st. 176 188 match ? … … 198 210 lapply ABS ABS 199 211 >EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS) 200 qed. 212 qed. *) 213 (* with a dummy ident (which is never used as seen above in the commented script) 214 I think handling of the function is easier *) 215 λp,st. 216 let dummy : ident ≝ an_identifier ? one in 217 match fetch_statement ? p … (ev_genv p) (pc … st) with 218 [ OK x ⇒ 219 match \snd x with 220 [ sequential s next ⇒ 221 match s with 222 [ step_seq s ⇒ 223 match s with 224 [ CALL f' args dest ⇒ 225 match function_of_call … (ev_genv p) st f' with 226 [ OK f ⇒ f 227  _ ⇒ dummy 228 ] 229  _ ⇒ dummy 230 ] 231  _ ⇒ dummy 232 ] 233  _ ⇒ dummy 234 ] 235  _ ⇒ dummy 236 ]. 201 237 202 238 definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?. … … 250 286  _ ⇒ None ? 251 287 ]) 252 (* as_after_return ≝ *) 253 (λs1,s2. 254 (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *) 255 ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧ 256 succ_pc p p (pc … s1) nxt = pc … s2) 288 (* as_after_return ≝ *) (joint_after_ret p) 257 289 (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?) 258 290 (* as_call_ident ≝ *) (joint_call_ident p).
Note: See TracChangeset
for help on using the changeset viewer.