Ignore:
Timestamp:
Feb 19, 2013, 12:23:50 PM (7 years ago)
Author:
campbell
Message:

Retain the pointer for the function called in front-end call states
so that we can do sensible stack costs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_semantics.ma

    r2645 r2677  
    3030   state
    3131| Callstate :
     32   ∀  vf : val. (* fn pointer; only used for instrumentation, not the semantics *)
    3233   ∀  fd : fundef internal_function.
    3334   ∀args : list val.
     
    109110      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr … ge b);
    110111      ! 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〉
    112113  | St_call_ptr frs args dst l ⇒ λH.
    113114      ! fv ← reg_retrieve (locals f) frs;
    114115      ! fd ← opt_to_res … (msg BadFunction) (find_funct … ge fv);
    115116      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    116       return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     117      return 〈E0, Callstate fv fd vs dst (adv l f ?::fs) m〉
    117118(*
    118119  | St_tailcall_id id args ⇒ λH.
     
    153154      return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    154155  ] (f_closed (func f) (next f) s ?)
    155 | Callstate fd params dst fs m ⇒
     156| Callstate _ fd params dst fs m ⇒
    156157    match fd return λ_. IO ??? with
    157158    [ Internal fn ⇒
     
    213214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
    214215  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).
    216217
    217218definition RTLabs_fullexec : fullexec io_out io_in ≝
     
    232233inductive state_rel : genv → state → state → Prop ≝
    233234| 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) (Callstate fd 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)
    235236(*
    236237| 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')
    237238*)
    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')
    239240| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
    240241| 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)
     
    276277  | #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
    277278  ]
    278 | * #fn #args #retdst #stk #m #tr #s'
     279| #vf * #fn #args #retdst #stk #m #tr #s'
    279280  whd in ⊢ (??%? → ?);
    280281  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
     
    293294(* Show that, in principle at least, we can calculate which function we called
    294295   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 *)
     300lemma jmeq_hackT : ∀T:Type[0]. ∀x,y:T. ∀P:Type[0].
     301  (x ≃ y → P) →
     302  (x = y → P).
     303/2/
     304qed.
     305
     306definition 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〉 →
    299308  Σb:block. find_funct_ptr … ge b = Some ? fd.
    300309#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'
    302311  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
    303312  cases (next_instruction ?)
    304313  (* 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; destruct
     314  [ 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
    306315    [ %{v} @Efd
    307     | cases v in Efd;
     316    | cases vf in Efd;
    308317      [ 4: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
    309318           [ #E @E | #E normalize in E; destruct ]
     
    313322  (* and everything else cannot occur, but we need to work through the
    314323     definition to find the resulting state to demonstrate that. *)
    315   | #l #LP whd in ⊢ (??%? → ?); #E destruct
    316   | #c #l #LP whd in ⊢ (??%? → ?); #E destruct
    317   | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct
    318   | #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:(??%?); destruct
    319   | #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:(??%?); destruct
    320   | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
    321   | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
    322   | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct
     324  | #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
    323332(*  | #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':(??%?); destruct
    325   ]
    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'
    327336  whd in ⊢ (??%? → ?);
    328337  [ @bind_res_value #loc #Eloc cases (alloc m O ?(*?*)) #m' #b whd in ⊢ (??%? → ?);
    329     #E destruct
     338    @jmeq_hackT #E destruct
    330339  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
    331340  ]
    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:(??%?); destruct
    335   | 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'
    338347  normalize #E destruct
    339348] qed.
     
    344353#ge *
    345354[ #f #fs #m * #F cases (F ?) @refl
    346 | #a #b #c #d #e * #F cases (F ?) @refl
     355| #a #b #c #d #e #f * #F cases (F ?) @refl
    347356| #a #b #c #d * #F cases (F ?) @refl
    348357| #r #F % [2: @refl | skip ]
Note: See TracChangeset for help on using the changeset viewer.