Changeset 2677 for src/RTLabs/RTLabs_semantics.ma
 Timestamp:
 Feb 19, 2013, 12:23:50 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabs_semantics.ma
r2645 r2677 30 30 state 31 31  Callstate : 32 ∀ vf : val. (* fn pointer; only used for instrumentation, not the semantics *) 32 33 ∀ fd : fundef internal_function. 33 34 ∀args : list val. … … 109 110 ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr … ge b); 110 111 ! vs ← m_list_map … (reg_retrieve (locals f)) args; 111 return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉112 return 〈E0, Callstate (Vptr (mk_pointer b zero_offset)) fd vs dst (adv l f ?::fs) m〉 112 113  St_call_ptr frs args dst l ⇒ λH. 113 114 ! fv ← reg_retrieve (locals f) frs; 114 115 ! fd ← opt_to_res … (msg BadFunction) (find_funct … ge fv); 115 116 ! vs ← m_list_map … (reg_retrieve (locals f)) args; 116 return 〈E0, Callstate f d vs dst (adv l f ?::fs) m〉117 return 〈E0, Callstate fv fd vs dst (adv l f ?::fs) m〉 117 118 (* 118 119  St_tailcall_id id args ⇒ λH. … … 153 154 return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉 154 155 ] (f_closed (func f) (next f) s ?) 155  Callstate fd params dst fs m ⇒156  Callstate _ fd params dst fs m ⇒ 156 157 match fd return λ_. IO ??? with 157 158 [ Internal fn ⇒ … … 213 214 do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main); 214 215 do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b); 215 OK ? (Callstate f (nil ?) (None ?) (nil ?) m).216 OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) (None ?) (nil ?) m). 216 217 217 218 definition RTLabs_fullexec : fullexec io_out io_in ≝ … … 232 233 inductive state_rel : genv → state → state → Prop ≝ 233 234  normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m') 234  to_call : ∀ge,f,fs,m, fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ? ge b = Some ? fd → state_rel ge (State f fs m) (Callstatefd args dst (f'::fs) m)235  to_call : ∀ge,f,fs,m,vf,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate vf fd args dst (f'::fs) m) 235 236 (* 236 237  tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m') 237 238 *) 238  from_call : ∀ge, fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate(Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m')239  from_call : ∀ge,vf,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate vf (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m') 239 240  to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m') 240 241  from_ret : ∀ge,f,fs,rtv,dst,f',m. next f = next f' → frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m) … … 276 277  #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %4 277 278 ] 278  * #fn #args #retdst #stk #m #tr #s'279  #vf * #fn #args #retdst #stk #m #tr #s' 279 280 whd in ⊢ (??%? → ?); 280 281 [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?); … … 293 294 (* Show that, in principle at least, we can calculate which function we called 294 295 on a transition. The proof is a functional inversion similar to eval_preserves, 295 above. *) 296 297 definition func_block_of_exec : ∀ge,s,t,fd,args,dst,fs,m. 298 eval_statement ge s = Value ??? 〈t,Callstate fd args dst fs m〉 → 296 above. Note: this was originally done before the value was added to 297 Callstate. *) 298 299 (* Hack due to lack of discriminator for large inductive types *) 300 lemma jmeq_hackT : ∀T:Type[0]. ∀x,y:T. ∀P:Type[0]. 301 (x ≃ y → P) → 302 (x = y → P). 303 /2/ 304 qed. 305 306 definition func_block_of_exec : ∀ge,s,t,vf,fd,args,dst,fs,m. 307 eval_statement ge s = Value ??? 〈t,Callstate vf fd args dst fs m〉 → 299 308 Σb:block. find_funct_ptr … ge b = Some ? fd. 300 309 #ge * 301 [ * #func #locals #next #nok #sp #dst #fs #m #tr # fd #args #dst' #fs' #m'310 [ * #func #locals #next #nok #sp #dst #fs #m #tr #vf #fd #args #dst' #fs' #m' 302 311 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 303 312 cases (next_instruction ?) 304 313 (* Function call cases. *) 305 [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs #E normalize in E; destruct314 [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs @jmeq_hackT #E normalize in E; destruct 306 315 [ %{v} @Efd 307  cases v in Efd;316  cases vf in Efd; 308 317 [ 4: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd; 309 318 [ #E @E  #E normalize in E; destruct ] … … 313 322 (* and everything else cannot occur, but we need to work through the 314 323 definition to find the resulting state to demonstrate that. *) 315  #l #LP whd in ⊢ (??%? → ?); #E destruct316  #c #l #LP whd in ⊢ (??%? → ?); #E destruct317  #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct318  #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct319  #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct320  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct321  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct322  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct324  #l #LP whd in ⊢ (??%? → ?); @jmeq_hackT #E destruct 325  #c #l #LP whd in ⊢ (??%? → ?); @jmeq_hackT #E destruct 326  #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc @jmeq_hackT #E whd in E:(??%??); destruct 327  #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct 328  #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct 329  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct 330  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct 331  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb @jmeq_hackT #E whd in E:(??%??); destruct 323 332 (*  #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct  #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct  #l' #e #E whd in E:(??%?); destruct ]  *: [1,3: #vl] #E whd in E:(??%?); destruct ]*) 324  #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct325 ] 326  * #fn #args #retdst #stk #m #tr#fd' #args' #dst' #fs' #m'333  #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); @jmeq_hackT #E' whd in E':(??%??); destruct 334 ] 335  #vf * #fn #args #retdst #stk #m #tr #vf' #fd' #args' #dst' #fs' #m' 327 336 whd in ⊢ (??%? → ?); 328 337 [ @bind_res_value #loc #Eloc cases (alloc m O ?(*?*)) #m' #b whd in ⊢ (??%? → ?); 329 #E destruct338 @jmeq_hackT #E destruct 330 339  @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct 331 340 ] 332  #v #r * [2: #f #fs ] #m #tr # fd' #args' #dst' #fs' #m'333 whd in ⊢ (??%? → ?); 334 [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct335  cases v [ normalize #E destruct  * [ 2: * #r normalize #E destruct  *: normalize #a try #b destruct ] ]336 ] 337  #r #tr # fd' #args' #dst' #fs' #m'341  #v #r * [2: #f #fs ] #m #tr #vf' #fd' #args' #dst' #fs' #m' 342 whd in ⊢ (??%? → ?); 343 [ @bind_res_value #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct 344  cases v [ normalize #E destruct  * [ 2: * #r normalize @jmeq_hackT #E destruct  *: normalize #a try #b destruct ] ] 345 ] 346  #r #tr #vf' #fd' #args' #dst' #fs' #m' 338 347 normalize #E destruct 339 348 ] qed. … … 344 353 #ge * 345 354 [ #f #fs #m * #F cases (F ?) @refl 346  #a #b #c #d #e * #F cases (F ?) @refl355  #a #b #c #d #e #f * #F cases (F ?) @refl 347 356  #a #b #c #d * #F cases (F ?) @refl 348 357  #r #F % [2: @refl  skip ]
Note: See TracChangeset
for help on using the changeset viewer.