Changeset 2722 for src/RTLabs


Ignore:
Timestamp:
Feb 23, 2013, 5:05:03 PM (7 years ago)
Author:
campbell
Message:

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_semantics.ma

    r2677 r2722  
    3030   state
    3131| Callstate :
    32    ∀  vf : val. (* fn pointer; only used for instrumentation, not the semantics *)
     32   ∀  id : ident. (* fn name; only used for instrumentation, not the semantics *)
    3333   ∀  fd : fundef internal_function.
    3434   ∀args : list val.
     
    110110      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr … ge b);
    111111      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    112       return 〈E0, Callstate (Vptr (mk_pointer b zero_offset)) fd vs dst (adv l f ?::fs) m〉
     112      return 〈E0, Callstate id fd vs dst (adv l f ?::fs) m〉
    113113  | St_call_ptr frs args dst l ⇒ λH.
    114114      ! fv ← reg_retrieve (locals f) frs;
    115       ! fd ← opt_to_res … (msg BadFunction) (find_funct … ge fv);
     115      ! 〈fd,id〉 ← opt_to_res … (msg BadFunction) (find_funct_id … ge fv);
    116116      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    117       return 〈E0, Callstate fv fd vs dst (adv l f ?::fs) m〉
     117      return 〈E0, Callstate id fd vs dst (adv l f ?::fs) m〉
    118118(*
    119119  | St_tailcall_id id args ⇒ λH.
     
    214214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
    215215  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
    216   OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) (None ?) (nil ?) m).
     216  OK ? (Callstate main f (nil ?) (None ?) (nil ?) m).
    217217
    218218definition RTLabs_fullexec : fullexec io_out io_in ≝
     
    268268  | #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 % %
    269269  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ???) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
    270   | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #b * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ???) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     270  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok * #fd #fid #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ? Efd) #b * #Ev' #Efn %2 [ % | @b | @Efn ]
    271271(*
    272272  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     
    308308  Σb:block. find_funct_ptr … ge b = Some ? fd.
    309309#ge *
    310 [ * #func #locals #next #nok #sp #dst #fs #m #tr #vf #fd #args #dst' #fs' #m'
     310[ * #func #locals #next #nok #sp #dst #fs #m #tr #fid #fd #args #dst' #fs' #m'
    311311  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
    312312  cases (next_instruction ?)
     
    314314  [ 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
    315315    [ %{v} @Efd
    316     | cases vf in Efd;
    317       [ 4: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
     316    | cases v in Efd;
     317      [ 4: * #b #off cases fd' #fd'' #fid' #Efd %{b} lapply (find_funct_id_drop ????? Efd) #Efd' whd in Efd':(??%?); cases (eq_offset ??) in Efd';
    318318           [ #E @E | #E normalize in E; destruct ]
    319319      | *: normalize #A try #B try #C destruct
Note: See TracChangeset for help on using the changeset viewer.