Changeset 2529 for src/joint/Traces.ma
 Timestamp:
 Dec 4, 2012, 6:16:25 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Traces.ma
r2484 r2529 15 15 { prog_spars : sem_params 16 16 ; prog : joint_program prog_spars 17 ; stack_sizes : (Σi.is_internal_function_of_program … prog i) →ℕ17 ; stack_sizes : ident → option ℕ 18 18 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) 19 19 }. … … 78 78 let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in 79 79 let dummy_pc ≝ mk_program_counter «mk_block Code (1), refl …» one in 80 let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in 80 let spp : xpointer ≝ 81 «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)), 82 pi2 … spb» in 81 83 (* let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *) 82 84 let main ≝ prog_main … p in … … 86 88 ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ; 87 89 let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in 88 ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … gemain) ;89 match ? return λx.description_of_function … main = x → ? with90 [ Internal fn ⇒ λprf.91 let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in92 ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;93 let pc' ≝ eval_internal_call_pc … ge mainin90 ! bl ← block_of_call … ge st_pc0 (inl … main) ; 91 ! 〈i, fn〉 ← fetch_function … ge bl ; 92 match fn with 93 [ Internal ifn ⇒ 94 ! st' ← eval_internal_call_no_pc … ge i ifn (call_args_for_main … pars) st_pc0 ; 95 let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in 94 96 return mk_state_pc … st' pc' 95  External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *) 96 ] (refl …). 97 [ @(description_of_internal_function … prf) 98  cases spb normalize // 99 ] 100 qed. 97  External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *) 98 ]. 101 99 102 100 definition joint_classify_seq : … … 105 103 match stmt with 106 104 [ CALL f args dest ⇒ 107 match function_of_call ?? (ev_genv p) st f with 108 [ OK fn ⇒ 109 match description_of_function … fn with 105 match (! bl ← block_of_call … (ev_genv p) st f ; 106 fetch_function … (ev_genv p) bl) with 107 [ OK id_fn ⇒ 108 match \snd id_fn with 110 109 [ Internal _ ⇒ cl_call 111 110  External _ ⇒ cl_other … … 136 135 ∀p : evaluation_params.state_pc p → status_class ≝ 137 136 λp,st. 138 match fetch_statement ? p… (ev_genv p) (pc … st) with139 [ OK f_s ⇒140 match \snd f_s with137 match fetch_statement … (ev_genv p) (pc … st) with 138 [ OK i_f_s ⇒ 139 match \snd i_f_s with 141 140 [ sequential s _ ⇒ joint_classify_step p st s 142 141  final s ⇒ joint_classify_final p s … … 145 144 ]. 146 145 146 definition no_call : ∀p,g.joint_seq p g → Prop ≝ 147 λp,g,s.match s with 148 [ CALL _ _ _ ⇒ False 149  _ ⇒ True 150 ]. 151 152 definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝ 153 λp,g,s.match s with 154 [ COST_LABEL _ ⇒ False 155  _ ⇒ True 156 ]. 157 158 lemma no_call_advance : ∀p : evaluation_params. 159 ∀s,nxt.∀st : state_pc p. 160 no_call p (globals p) s → 161 eval_seq_advance p (globals p) (ev_genv p) s nxt st = return next … nxt st. 162 #p * // #f #args #dest #nxt #st * 163 qed. 164 165 lemma no_call_other : ∀p : evaluation_params.∀st,s. 166 no_call p (globals p) s → 167 joint_classify_seq … st s = cl_other. 168 #p #st * // #f #args #dest * 169 qed. 170 171 lemma cond_call_other : 172 ∀p,globals.∀P : joint_step p globals → Prop. 173 (∀a,lbltrue.P (COND … a lbltrue)) → 174 (∀f,args,dest.P (CALL … f args dest)) → 175 (∀s.no_call ?? s → P s) → 176 ∀s.P s. 177 #p #globals #P #H1 #H2 #H3 * // * /2 by / qed. 178 147 179 lemma joint_classify_call : ∀p : evaluation_params.∀st. 148 180 joint_classify p st = cl_call → 149 ∃ f,f',args,dest,next,fn,fd.150 fetch_statement ? p… (ev_genv p) (pc … st) =151 OK ? 〈 f, sequential … (CALL … f' args dest) next〉 ∧152 function_of_call … (ev_genv p) st f' = OK ? fn∧153 description_of_function … (ev_genv p) fn = Internal … fd.181 ∃i_f,f',args,dest,next,bl,i',fd'. 182 fetch_statement … (ev_genv p) (pc … st) = 183 OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧ 184 block_of_call … (ev_genv p) st f' = OK ? bl ∧ 185 fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉. 154 186 #p #st 155 187 whd in match joint_classify; normalize nodelta 156 inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta 157 [ * #f * [ * [ #lbl  #b #f #args ]] 158 [ * [ #a #lbl #next ] 159 [ * 160 [14: #f' #args #dest  #s  #lbl  #mv  #a  #a  #i #prf #dpl #dph  #op #a #b #a' #b' 161  #op #a #a'  #op #a #a' #arg  #a #dpl #dph  #dpl #dph #arg 162  #ext ] #next 163 [ whd in match joint_classify_step; whd in match joint_classify_seq; 164 normalize nodelta 165 inversion (function_of_call ?????) normalize nodelta 166 [ #fn 167 inversion (description_of_function ?? fn) #fd 168 #EQfd 169  #e 170 ] #EQfn 171 ] 188 inversion (fetch_statement … (ev_genv p) (pc … st)) normalize nodelta 189 [2: #e #_ #ABS destruct(ABS) ] 190 * #i_f * [2: * [ #lbl   #fl #f #args ] #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ] 191 @cond_call_other 192 [ #a #lbl #nxt #_ normalize in ⊢ (%→?); #ABS destruct(ABS) 193 3: #s #no_call #nxt #_ whd in match joint_classify_step; 194 normalize nodelta >(no_call_other … no_call) #ABS destruct(ABS) 195 ] 196 #f' #args #dest #nxt #fetch 197 whd in match joint_classify_step; whd in match joint_classify_seq; 198 normalize nodelta 199 inversion (block_of_call ?????) 200 [ #bl #block_of_c >m_return_bind 201 inversion (fetch_function ???) 202 [ * #i' * 203 [ #fd' #fetch' #_ 204 %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'} 205 % [ %{block_of_c} % ] 206 whd in match fetch_internal_function; normalize nodelta 207 >fetch' % 172 208 ] 173 209 ] 174  #e 175 ] #EQfetch 176 [*: #ABS normalize in ABS; destruct(ABS) ] 177 normalize nodelta #_ 178 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} 179 %{EQfd} %{EQfn} % 210 ] 211 #x #_ normalize in ⊢ (%→?); #ABS destruct(ABS) 180 212 qed. 181 213 … … 183 215 (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝ 184 216 λp,s1,s2. 185 match fetch_statement ? p… (ev_genv p) (pc … s1) with217 match fetch_statement … (ev_genv p) (pc … s1) with 186 218 [ OK x ⇒ 187 219 match \snd x with 188 220 [ sequential s next ⇒ 189 pc … s2 = succ_pc p p(pc … s1) next221 pc … s2 = succ_pc p (pc … s1) next 190 222  _ ⇒ False (* never happens *) 191 223 ] … … 225 257 I think handling of the function is easier *) 226 258 λp,st. 227 let dummy : ident ≝ an_identifier ? one in 228 match fetch_statement ? p… (ev_genv p) (pc … st) with259 let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *) 260 match fetch_statement … (ev_genv p) (pc … st) with 229 261 [ OK x ⇒ 230 262 match \snd x with … … 234 266 match s with 235 267 [ CALL f' args dest ⇒ 236 match function_of_call … (ev_genv p) st f' with 237 [ OK f ⇒ f 268 match 269 (! bl ← block_of_call … (ev_genv p) st f' ; 270 fetch_internal_function … (ev_genv p) bl) with 271 [ OK i_f ⇒ \fst i_f 238 272  _ ⇒ dummy 239 273 ] … … 279 313  _ ⇒ None ? 280 314 ]. 315 316 317 lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt. 318 no_cost_label p (globals p) s → 319 cost_label_of_stmt … (sequential … s nxt) = None ?. 320 #p * // #lbl #next * 321 qed. 281 322 282 323 definition joint_abstract_status : … … 293 334 (* as_label_of_pc ≝ *) 294 335 (λpc. 295 match fetch_statement ? p… (ev_genv p) pc with336 match fetch_statement … (ev_genv p) pc with 296 337 [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt) 297 338  _ ⇒ None ? … … 300 341 (* as_final ≝ *) (λs.is_final p (globals ?) (ev_genv p) (exit p) s ≠ None ?) 301 342 (* as_call_ident ≝ *) (joint_call_ident p). 343
Note: See TracChangeset
for help on using the changeset viewer.