Changeset 2722 for src


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.

Location:
src
Files:
12 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r2677 r2722  
    358358    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
    359359    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
    360     ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct … ge vf);
     360    ! 〈fd,id〉 ← opt_to_io … (msg BadFunctionValue) (find_funct_id … ge vf);
    361361    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
    362362(* requires associativity of IOMonad, so rearrange it below
     
    370370*)
    371371    match lhs with
    372          [ None ⇒ ret ? 〈tr2⧺tr3, Callstate vf fd vargs (Kcall (None ?) f e k) m〉
     372         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate id fd vargs (Kcall (None ?) f e k) m〉
    373373         | Some lhs' ⇒
    374374           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs' : IO ???;
    375            ret ? 〈tr1⧺tr2⧺tr3, Callstate vf fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
     375           ret ? 〈tr1⧺tr2⧺tr3, Callstate id fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
    376376         ]
    377377  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
     
    521521  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
    522522  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
    523   OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) Kstop m0).
     523  OK ? (Callstate (prog_main ?? p) f (nil ?) Kstop m0).
    524524
    525525let rec is_final (s:state) : option int ≝
  • src/Clight/CexecComplete.ma

    r2677 r2722  
    362362    change with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v) in H3:(??%?);
    363363    >H3 @refl
    364 | #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
     364| #f #e #eargs #k #ef #m #vf #vargs #f' #fid #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
    365365    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    366366    >(yields_eq ??? (exprlist_complete … H2)) whd in ⊢ (??%?);
     
    368368    >H4 elim (assert_type_eq_true (fun_typeof e)); #pty #ety >ety
    369369    @refl
    370 | #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
     370| #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #fid #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
    371371    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
    372372    >(yields_eq ??? (exprlist_complete … H3)) whd in ⊢ (??%?);
  • src/Clight/CexecSound.ma

    r2677 r2722  
    385385    @res_bindIO2_OK #vf #tr1 #Hvf0 lapply (exec_expr_sound' … Hvf0); #Hvf
    386386    @res_bindIO2_OK #vargs #tr2 #Hvargs0 lapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs
    387     @opt_bindIO_OK #fd #efd
     387    @opt_bindIO_OK * #fd #fid #efd
    388388    @bindIO_OK #ety
    389389    cases lex; whd;
  • src/Clight/Csem.ma

    r2677 r2722  
    933933      ∀m: mem.  state
    934934  | Callstate:
    935       ∀fb: val. (* function pointer; used by stack instrumentation, but not the semantics *)
     935      ∀id: ident. (* function name; used by stack instrumentation, but not the semantics *)
    936936      ∀fd: clight_fundef.
    937937      ∀args: list val.
     
    10251025           (tr1⧺tr2) (State f Sskip k e m')
    10261026
    1027   | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2.
     1027  | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd,id,tr1,tr2.
    10281028      eval_expr ge e m a vf tr1 →
    10291029      eval_exprlist ge e m al vargs tr2 →
    1030       find_funct … ge vf = Some ? fd
     1030      find_funct_id … ge vf = Some ? 〈fd,id〉
    10311031      type_of_fundef fd = fun_typeof a →
    10321032      step ge (State f (Scall (None ?) a al) k e m)
    1033            (tr1⧺tr2) (Callstate vf fd vargs (Kcall (None ?) f e k) m)
    1034 
    1035   | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
     1033           (tr1⧺tr2) (Callstate id fd vargs (Kcall (None ?) f e k) m)
     1034
     1035  | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,id,tr1,tr2,tr3.
    10361036      eval_lvalue ge e m lhs loc ofs tr1 →
    10371037      eval_expr ge e m a vf tr2 →
    10381038      eval_exprlist ge e m al vargs tr3 →
    1039       find_funct … ge vf = Some ? fd
     1039      find_funct_id … ge vf = Some ? 〈fd,id〉
    10401040      type_of_fundef fd = fun_typeof a →
    10411041      step ge (State f (Scall (Some ? lhs) a al) k e m)
    1042            (tr1⧺tr2⧺tr3) (Callstate vf fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
     1042           (tr1⧺tr2⧺tr3) (Callstate id fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
    10431043
    10441044  | step_seq:  ∀f,s1,s2,k,e,m.
     
    11661166           E0 (State f s' k' e m)
    11671167
    1168   | step_internal_function: ∀vf,f,vargs,k,m,e,m1,m2.
     1168  | step_internal_function: ∀id,f,vargs,k,m,e,m1,m2.
    11691169      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 →
    11701170      bind_parameters e m1 (fn_params f) vargs m2 →
    1171       step ge (Callstate vf (CL_Internal f) vargs k m)
     1171      step ge (Callstate id (CL_Internal f) vargs k m)
    11721172           E0 (State f (fn_body f) k e m2)
    11731173
    1174   | step_external_function: ∀vf,id,targs,tres,vargs,k,m,vres,t.
     1174  | step_external_function: ∀fid,id,targs,tres,vargs,k,m,vres,t.
    11751175      event_match (external_function id targs tres) vargs t vres →
    1176       step ge (Callstate vf (CL_External id targs tres) vargs k m)
     1176      step ge (Callstate fid (CL_External id targs tres) vargs k m)
    11771177            t (Returnstate vres k m)
    11781178
     
    12111211      find_symbol … ge (prog_main ?? p) = Some ? b →
    12121212      find_funct_ptr … ge b = Some ? f →
    1213       initial_state p (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) Kstop m0).
     1213      initial_state p (Callstate (prog_main ?? p) f (nil ?) Kstop m0).
    12141214
    12151215(* * A final state is a [Returnstate] with an empty continuation. *)
  • src/Clight/SimplifyCasts.ma

    r2677 r2722  
    18931893  rg_find_symbol: ∀s.
    18941894    find_symbol ? ge s = find_symbol ? ge' s;
    1895   rg_find_funct: ∀v,f.
    1896     find_funct ? ge v = Some ? f
    1897     find_funct ? ge' v = Some ? (t f);
     1895  rg_find_funct: ∀v,f,id.
     1896    find_funct_id ? ge v = Some ? 〈f,id〉
     1897    find_funct_id ? ge' v = Some ? 〈t f,id〉;
    18981898  rg_find_funct_ptr: ∀b,f.
    18991899    find_funct_ptr ? ge b = Some ? f →
     
    25622562                             whd in match (bindIO ??????) in ⊢ (% → %);
    25632563                             elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a))
    2564                              cases (find_funct clight_fundef ge (\fst a));
     2564                             cases (find_funct_id clight_fundef ge (\fst a));
    25652565                             [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
    2566                              | 2: #clfd -Hsim #Hsim lapply (Hsim clfd (refl ? (Some ? clfd))) #Heq >Heq
     2566                             | 2: * #clfd #fid -Hsim #Hsim lapply (Hsim clfd fid (refl ??)) #Heq >Heq
    25672567                                  whd in match (bindIO ??????) in ⊢ (% → %);
    25682568                                  >simplify_type_of_fundef_eq >(simplify_fun_typeof_eq ge en m)
     
    25722572                                       [ 1: whd in match (bindIO ??????) in ⊢ (% → %);
    25732573                                            #Eq destruct (Eq)
    2574                                             %{(Callstate (\fst a) (simplify_fundef clfd) (\fst  l)
     2574                                            %{(Callstate fid (simplify_fundef clfd) (\fst  l)
    25752575                                                         (Kcall (None (block×offset×type)) (simplify_function f) en k') m)}
    25762576                                            @conj
     
    25852585                                                      whd in match (bindIO ??????) in ⊢ (% → %);
    25862586                                                      #Heq destruct (Heq)
    2587                                                       %{(Callstate (\fst a) (simplify_fundef clfd) (\fst  l)
     2587                                                      %{(Callstate fid (simplify_fundef clfd) (\fst  l)
    25882588                                                                   (Kcall (Some (block×offset×type) 〈\fst  x,typeof (simplify_e fptr)〉)
    25892589                                                                   (simplify_function f) en k') m)}
  • src/Clight/labelSimulation.ma

    r2682 r2722  
    8787 ]
    8888| #v #ty #b #o #tr #EX #u %{tr} % [
    89     whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;
     89    whd in EX:(??%?) ⊢ (??%?); cases (lookup SymbolTag ?? v) in EX ⊢ %;
    9090    [ whd in ⊢ (??%? → ??%?); >(rgg_find_symbol … RG) //
    9191    | #b // ]
     
    407407qed.
    408408
    409 lemma opt_find_funct : ∀ge,ge',m,vf,fd.
     409lemma opt_find_funct : ∀ge,ge',m,vf,fd,id.
    410410  related_globals_gen … label_fundef ge ge' →
    411   opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd
    412   ∃u. opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (\fst (label_fundef u fd)).
    413 #ge #ge' #m #vf #fd #RG
    414 lapply (rgg_find_funct … RG … vf fd)
    415 cases (find_funct … vf)
     411  opt_to_io io_out io_in … m (find_funct_id … ge vf) = Value … 〈fd,id〉
     412  ∃u. opt_to_io io_out io_in … m (find_funct_id … ge' vf) = Value … 〈\fst (label_fundef u fd), id〉.
     413#ge #ge' #m #vf #fd #id #RG
     414lapply (rgg_find_funct_id … RG … vf fd)
     415cases (find_funct_id … vf)
    416416[ #_ #E normalize in E; destruct
    417 | #fd' #H #E normalize in E; destruct cases (H (refl ??)) #u #FF %{u} >FF //
     417| * #fd' #id' #H #E normalize in E; destruct cases (H ? (refl ??)) #u #FF %{u} >FF //
    418418] qed.
    419419
     
    768768    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    769769    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
    770     cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
     770    cases (bindIO_inversion ??????? EX) -EX * #fd #fid * #EX3 #EX
    771771    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
    772772    whd in EX:(??%%);
     
    910910    cases v1 in EX1 EX;
    911911    [ 2: #sz #i #EX1 #EX
    912     | *: normalize #A #B try #C destruct
     912    | *: [ 3: #x ] #A whd in ⊢ (??%% → ?); #B destruct
    913913    ]
    914914    whd in EX:(??%%); cases ty in EX1 EX ⊢ %; normalize nodelta #sz' try #sg try #EX1 try #EX destruct
  • src/Clight/switchRemoval.ma

    r2706 r2722  
    19231923  rg_find_symbol: ∀s.
    19241924    find_symbol ? ge s = find_symbol ? ge' s;
    1925   rg_find_funct: ∀v,f.
    1926     find_funct ? ge v = Some ? f
    1927     find_funct ? ge' v = Some ? (t f);
     1925  rg_find_funct_id: ∀v,f,id.
     1926    find_funct_id ? ge v = Some ? 〈f,id〉
     1927    find_funct_id ? ge' v = Some ? 〈t f,id〉;
    19281928  rg_find_funct_ptr: ∀b,f.
    19291929    find_funct_ptr ? ge b = Some ? f →
     
    29132913       cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func
    29142914       cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args
    2915        cases (bindIO_inversion ??????? Hexec_args) #called_fundef * #Heq_fundef #Hexec_typeeq
     2915       cases (bindIO_inversion ??????? Hexec_args) * #called_fundef #fid * #Heq_fundef #Hexec_typeeq
    29162916       cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret
    29172917       >(Hsim_expr … Heq_func) whd in match (m_bind ?????);
    29182918       >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args)
    29192919       whd in ⊢ (??%?);
    2920        >(rg_find_funct … Hrelated … (opt_to_io_Value … Heq_fundef))
     2920       >(rg_find_funct_id … Hrelated … (opt_to_io_Value … Heq_fundef))
    29212921       whd in ⊢ (??%?); <fundef_type_simplify >Heq_assert
    29222922       whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret
  • src/Cminor/Cminor_semantics.ma

    r2677 r2722  
    6969            state
    7070| Callstate:
    71     ∀   vf: val. (* fn pointer; only used for instrumentation, not the semantics *)
     71    ∀   id: ident. (* fn name; only used for instrumentation, not the semantics *)
    7272    ∀   fd: fundef internal_function.
    7373    ∀ args: list val.
     
    296296    | St_call dst ef args ⇒ λInv.
    297297        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    298         ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct … ge vf);
     298        ! 〈fd,id〉 ← opt_to_res … (msg BadFunctionValue) (find_funct_id … ge vf);
    299299        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    300         return 〈tr ⧺ tr', Callstate vf fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     300        return 〈tr ⧺ tr', Callstate id fd vargs m (Scall dst f sp en ? fInv k ? st)〉
    301301(*
    302302    | St_tailcall ef args ⇒ λInv.
     
    425425  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
    426426  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
    427   OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) m SStop).
     427  OK ? (Callstate (prog_main ?? p) f (nil ?) m SStop).
    428428
    429429definition Cminor_fullexec : fullexec io_out io_in ≝
     
    439439  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
    440440  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
    441   OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) m SStop).
     441  OK ? (Callstate (prog_main ?? p) f (nil ?) m SStop).
    442442
    443443definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
  • 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
  • src/common/Globalenvs.ma

    r2645 r2722  
    425425qed.
    426426
     427
    427428lemma symbol_of_block_rev : ∀F,genv,b,id.
    428429  symbol_for_block F genv b = Some ? id →
     
    439440  | #_ *
    440441  ]
     442] qed.
     443
     444lemma symbol_of_block_rev' : ∀F,genv,b.
     445  symbol_for_block F genv b = None ? →
     446  find_funct_ptr F genv b = None ?.
     447#F #genv * * [ // | // ] #b #H
     448whd in ⊢ (??%?);
     449lapply (functions_inv ? genv b)
     450cases (lookup_opt F b ?) //
     451#f #H' cases (H' ?)
     452[ #id #E whd in H:(??%?);
     453  lapply (find_none ?? (symbols … genv) (λid,b'. eq_block (mk_block (neg b)) b') id (mk_block (neg b)))
     454  cases (find ????) in H ⊢ %;
     455  [ normalize #_ #H lapply (H (refl ??) E) >eqb_n_n *
     456  | * #id' #b' normalize #E destruct
     457  ]
     458| % #E destruct
    441459] qed.
    442460
     
    459477| * #id' #b' #_ normalize #_ #E destruct
    460478] qed.
     479
     480lemma symbol_of_function_block_ok : ∀F,ge,b,FFP,id.
     481  symbol_of_function_block F ge b FFP = id →
     482  symbol_for_block F ge b = Some ? id.
     483#F #ge #b #FFP #id whd in ⊢ (??%? → ?);
     484generalize in match (refl ? (symbol_for_block F ge b));
     485lapply (symbol_of_block_rev' F ge b)
     486cases (symbol_for_block F ge b) in ⊢ (% → ???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
     487[ #H @⊥ >(H (refl ??)) in FFP; * /2/
     488| #id' #_ #E normalize in ⊢ (% → ?); #E' destruct @E
     489] qed.
     490
     491definition symbol_of_function_block' : ∀F,ge,b,f. find_funct_ptr F ge b = Some ? f → ident ≝
     492λF,ge,b,f,FFP. symbol_of_function_block F ge b ?.
     493>FFP % #E destruct
     494qed.
     495
     496definition find_funct_ptr_id : ∀F:Type[0]. genv_t F → block → option (F × ident) ≝
     497λF:Type[0].λge:genv_t F.λb:block.
     498match find_funct_ptr F ge b return λx:option F. ? = x → option (F × ident) with
     499[ None ⇒ λ_. None ?
     500| Some f ⇒ λFFP. Some ? 〈f,symbol_of_function_block' F ge b f FFP〉
     501] (refl ??).
     502
     503lemma find_funct_ptr_id_drop : ∀F,ge,b,f,id.
     504  find_funct_ptr_id F ge b = Some ? 〈f,id〉 →
     505  find_funct_ptr F ge b = Some ? f.
     506#F #ge #b #f #id whd in ⊢ (??%? → ?);
     507generalize in match (refl ??);
     508cases (find_funct_ptr F ge b) in ⊢ (???% → ??(match % with [_⇒?|_⇒?] ?)? → %);
     509[ #X #E normalize in E; destruct
     510| #f' #ID #E whd in E:(??%?); destruct %
     511] qed.
     512
     513coercion ffpi_drop :
     514  ∀F,ge,b,f,id.
     515  ∀FFP:find_funct_ptr_id F ge b = Some ? 〈f,id〉.
     516  find_funct_ptr F ge b = Some ? f ≝ find_funct_ptr_id_drop
     517  on _FFP:eq (option ?) ?? to eq (option ?) ??.
     518
     519lemma find_funct_ptr_id_inv : ∀F,ge,b,f,id.
     520  find_funct_ptr_id F ge b = Some ? 〈f,id〉 →
     521  find_funct_ptr F ge b = Some ? f ∧
     522  symbol_for_block F ge b = Some ? id.
     523#F #ge #b #f #id whd in ⊢ (??%? → ?);
     524generalize in match (refl ??);
     525cases (find_funct_ptr F ge b) in ⊢ (???% → ??(match % with [_⇒?|_⇒?] ?)? → %);
     526[ #X #E normalize in E; destruct
     527| #f' #FFP #E whd in E:(??%?); %
     528  [ destruct %
     529  | @(symbol_of_function_block_ok F ge b ? id)
     530    [ >FFP % #E' destruct
     531    | destruct %
     532    ]
     533  ]
     534] qed.
     535
     536lemma make_find_funct_ptr_id : ∀F,ge,b,f,id.
     537  find_funct_ptr F ge b = Some ? f →
     538  symbol_for_block F ge b = Some ? id →
     539  find_funct_ptr_id F ge b = Some ? 〈f,id〉.
     540#F #ge #b #f #id #FFP #SYM
     541whd in ⊢ (??%?); generalize in match (refl ??);
     542>FFP in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?);
     543#FFP' whd in ⊢ (??%?);
     544@eq_f @eq_f
     545whd in ⊢ (??%?);
     546generalize in match (refl ? (symbol_for_block F ge b));
     547>SYM in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?);
     548#SYM' whd in ⊢ (??%?); %
     549qed.
     550
     551definition symbol_of_function_val : ∀F,ge,v. find_funct F ge v ≠ None ? → ident ≝
     552λF,ge,v.
     553match v return λv. find_funct F ge v ≠ None ? → ident with
     554[ Vptr p ⇒ λH. symbol_of_function_block F ge (pblock p) ?
     555| _ ⇒ λH. ⊥
     556].
     557try (cases H #H' cases (H' (refl ??)))
     558lapply H
     559whd in match (find_funct ???);
     560@eq_offset_elim
     561[ #_ #H' @H'
     562| #X * #H' cases (H' (refl ??))
     563] qed.
     564
     565definition symbol_of_function_val' : ∀F,ge,v,f. find_funct F ge v = Some ? f → ident ≝
     566λF,ge,v,f,FF. symbol_of_function_val F ge v ?.
     567>FF % #E destruct
     568qed.
     569
     570definition find_funct_id : ∀F:Type[0]. genv_t F → val → option (F × ident) ≝
     571λF:Type[0].λge:genv_t F.λv:val.
     572match find_funct F ge v return λx:option F. ? = x → option (F × ident) with
     573[ None ⇒ λ_. None ?
     574| Some f ⇒ λFF. Some ? 〈f,symbol_of_function_val' F ge v f FF〉
     575] (refl ??).
     576
     577lemma find_funct_id_drop : ∀F,ge,v,f,id.
     578  find_funct_id F ge v = Some ? 〈f,id〉 →
     579  find_funct F ge v = Some ? f.
     580#F #ge #v #f #id whd in ⊢ (??%? → ?);
     581generalize in match (refl ??);
     582cases (find_funct F ge v) in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)? → ?);
     583[ #X #E normalize in E; destruct
     584| #f' #ID #E whd in E:(??%?); destruct assumption
     585] qed.
     586
     587coercion ffi_drop :
     588  ∀F,ge,v,f,id.
     589  ∀FF:find_funct_id F ge v = Some ? 〈f,id〉.
     590  find_funct F ge v = Some ? f ≝ find_funct_id_drop
     591  on _FF:eq (option ?) ?? to eq (option ?) ??.
     592
     593lemma find_funct_id_ptr : ∀F,ge,v,f,id.
     594  find_funct_id F ge v = Some ? 〈f,id〉 →
     595  ∃b. v = Vptr (mk_pointer b zero_offset) ∧
     596  find_funct_ptr_id F ge b = Some ? 〈f,id〉.
     597#F #ge #v #f #id whd in ⊢ (??%? → ?);
     598generalize in match (refl ??);
     599cases (find_funct F ge v) in ⊢ (???% → ??(match % with [_⇒?|_⇒?] ?)? → %);
     600[ #X #E normalize in E; destruct
     601| #f' #FF #E whd in E:(??%?);
     602  cases (find_funct_find_funct_ptr ???? FF) #b * #E1 #FFP %{b} %{E1}
     603  whd in ⊢ (??%?);
     604  generalize in match (refl ??);
     605  >FFP in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?);
     606  #FFP' whd in ⊢ (??%?); <E
     607  @eq_f @eq_f >E1 in FF E ⊢ %; #FF #E %
     608] qed.
     609
     610lemma find_funct_ptr_id_conv : ∀F,ge,b,f,id.
     611  find_funct_ptr_id F ge b = Some ? 〈f,id〉 →
     612  find_funct_id F ge (Vptr (mk_pointer b zero_offset)) = Some ? 〈f,id〉.
     613#F #ge * * [2,3:#b] #f #id
     614whd in ⊢ (??%? → ??%?); #E destruct
     615@E
     616qed.
    461617
    462618(*
     
    9431099qed.
    9441100
     1101lemma symbols_match:
     1102    ∀M:matching.
     1103    ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
     1104    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
     1105    match_program … M p p' →
     1106    symbols ? (globalenv … initW p') = symbols ? (globalenv … initV p).
     1107* #A #B #V #W #match_fun #match_var #initV #initW #initsize
     1108* #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain
     1109whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     1110whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
     1111change with (add_globals ?????) in match (foldl ?????);
     1112change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
     1113@sym_eq
     1114@(proj1 … (add_globals_match … Mvars))
     1115[ @(matching_fns_get_same_blocks … Mfns)
     1116  #f #g @match_funct_entry_id
     1117| * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
     1118] qed.
     1119
    9451120lemma
    9461121  find_symbol_match:
     
    9511126    ∀s: ident.
    9521127    find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s.
    953 * #A #B #V #W #match_fun #match_var #initV #initW #initsize
    954 * #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s
    955 whd in ⊢ (??%%);
    956 @sym_eq
    957 @(eq_f ??(λx. lookup SymbolTag block x s))
    958 whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
    959 whd in match (globalenv ????); whd in match (globalenv_allocmem ????);
    960 change with (add_globals ?????) in match (foldl ?????);
    961 change with (add_globals ?????) in match (foldl ? (ident×region×V) ???);
    962 @(proj1 … (add_globals_match … Mvars))
    963 [ @(matching_fns_get_same_blocks … Mfns)
    964   #f #g @match_funct_entry_id
    965 | * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % | @(initsize … MVE) ]
    966 ] qed.
     1128#M #initV #initW #initsize #p1 #p2 #MATCH #s
     1129whd in ⊢ (??%%); >(symbols_match M … initsize … MATCH) %
     1130qed.
    9671131 
    9681132lemma
     
    11181282  rg_find_symbol: ∀s.
    11191283    find_symbol … ge s = find_symbol … ge' s;
     1284  rg_symbol_for : ∀b.
     1285    symbol_for_block … ge b = symbol_for_block … ge' b;
    11201286  rg_find_funct: ∀v,f.
    11211287    find_funct … ge v = Some ? f →
     
    11261292}.
    11271293
     1294lemma rg_find_funct_id : ∀A,B,t,ge,ge'. ∀RG:related_globals A B t ge ge'. ∀v,f,id.
     1295  find_funct_id … ge v = Some ? 〈f,id〉 →
     1296  find_funct_id … ge' v = Some ? 〈t f,id〉.
     1297#A #B #t #ge #ge' #RG #v #f #id #FFI
     1298cases (find_funct_id_ptr ????? FFI)
     1299#b * #E1 #FFPI
     1300cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
     1301lapply (rg_find_funct_ptr … RG … FFP) #FFP'
     1302>(rg_symbol_for … RG b) in SYM; #SYM'
     1303lapply (make_find_funct_ptr_id … FFP' SYM')
     1304>E1 @find_funct_ptr_id_conv
     1305qed.
     1306
     1307lemma rg_find_funct_ptr_id : ∀A,B,t,ge,ge'. ∀RG:related_globals A B t ge ge'. ∀b,f,id.
     1308  find_funct_ptr_id … ge b = Some ? 〈f,id〉 →
     1309  find_funct_ptr_id … ge' b = Some ? 〈t f,id〉.
     1310#A #B #t #ge #ge' #RG #b #f #id #FFPI
     1311cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
     1312lapply (rg_find_funct_ptr … RG … FFP) #FFP'
     1313>(rg_symbol_for … RG b) in SYM; #SYM'
     1314@(make_find_funct_ptr_id … FFP' SYM')
     1315qed.
     1316
     1317
     1318
    11281319theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs.
    11291320  related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)).
    11301321#A #B #V #iV #p #tf %
    11311322[ #s @sym_eq @(find_symbol_transf A B V iV tf p)
     1323| #b whd in ⊢ (??%%); >(symbols_match … (transform_program_match … tf ?))
     1324  [ % | #v #w * #id #r #v1 #v2 #E destruct % | skip ]
    11321325| @(find_funct_transf A B V iV tf p)
    11331326| @(find_funct_ptr_transf A B V iV p tf)
     
    11371330  rgg_find_symbol: ∀s.
    11381331    find_symbol … ge s = find_symbol … ge' s;
     1332  rgg_symbol_for : ∀b.
     1333    symbol_for_block … ge b = symbol_for_block … ge' b;
    11391334  rgg_find_funct_ptr: ∀b,f.
    11401335    find_funct_ptr … ge b = Some ? f →
     
    11451340}.
    11461341
     1342lemma rgg_find_funct_id : ∀tag,A,B,t,ge,ge'. ∀RG:related_globals_gen tag A B t ge ge'. ∀v,f,id.
     1343  find_funct_id … ge v = Some ? 〈f,id〉 →
     1344  ∃g. find_funct_id … ge' v = Some ? 〈\fst (t g f),id〉.
     1345#tag #A #B #t #ge #ge' #RG #v #f #id #FFI
     1346cases (find_funct_id_ptr ????? FFI)
     1347#b * #E1 #FFPI
     1348cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
     1349cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g}
     1350>(rgg_symbol_for … RG b) in SYM; #SYM'
     1351lapply (make_find_funct_ptr_id … FFP' SYM')
     1352>E1 @find_funct_ptr_id_conv
     1353qed.
     1354
     1355lemma rgg_find_funct_ptr_id : ∀tag,A,B,t,ge,ge'. ∀RG:related_globals_gen tag A B t ge ge'. ∀b,f,id.
     1356  find_funct_ptr_id … ge b = Some ? 〈f,id〉 →
     1357  ∃g. find_funct_ptr_id … ge' b = Some ? 〈\fst (t g f),id〉.
     1358#tag #A #B #t #ge #ge' #RG #b #f #id #FFPI
     1359cases (find_funct_ptr_id_inv ????? FFPI) #FFP #SYM
     1360cases (rgg_find_funct_ptr … RG … FFP) #g #FFP' %{g}
     1361>(rgg_symbol_for … RG b) in SYM; #SYM'
     1362@(make_find_funct_ptr_id … FFP' SYM')
     1363qed.
     1364
    11471365include "utilities/extra_bool.ma".
    11481366
     
    11521370[ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p))
    11531371  #v #w * //
     1372| #b whd in ⊢ (??%%); >(symbols_match … (transform_program_gen_match … tf p))
     1373  [ % | #v #w * #id #r #v1 #v2 #E destruct % | skip ]
    11541374| #b #f #FFP
    11551375  cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
  • src/common/Measurable.ma

    r2685 r2722  
    394394 *)
    395395
    396 definition observables : ∀FE:fullexec io_out io_in. program … FE → nat → nat → option ((list trace) × (list trace)) ≝
    397 λFE,p,m,n.
    398   let trace ≝ exec_inf … FE p in
    399   match split_trace … trace m with
    400   [ Some x ⇒
    401     let 〈prefix,suffix〉 ≝ x in
    402     match split_trace … suffix n with
    403     [ Some y ⇒
    404       let interesting ≝ \fst y in
    405       Some ? 〈map … (fst ??) prefix, map … (fst ??) interesting〉
    406     | _ ⇒ None ?
    407     ]
    408   | _ ⇒ None ?
    409   ].
    410 
    411 definition state_at : ∀FE:fullexec io_out io_in. ∀p:program … FE. nat → option (state … FE (make_global … p)) ≝
    412 λFE,p,m.
    413   let trace ≝ exec_inf … FE p in
    414   match split_trace … trace m with
    415   [ Some x ⇒
    416     match \snd x with
    417     [ e_step _ s _ ⇒ Some ? s
    418     | e_stop _ _ s ⇒ Some ? s
    419     | _ ⇒ None ?
    420     ]
    421   | _ ⇒ None ?
    422   ].
     396definition observables : ∀C:preclassified_system. program ?? C → nat → nat → res ((list intensional_event) × (list intensional_event)) ≝
     397λC,p,m,n.
     398  let g ≝ make_global … (pcs_exec … C) p in
     399  let C' ≝ pcs_to_cs C g in
     400  ! s0 ← make_initial_state … p;
     401  ! 〈prefix,s1〉 ← exec_steps m ?? (cs_exec … C') g s0;
     402  ! 〈interesting,s2〉 ← exec_steps m ?? (cs_exec … C') g s1;
     403  let 〈cs,prefix'〉 ≝ intensional_trace_of_trace C' [ ] prefix in
     404  return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
     405
  • src/correctness.ma

    r2677 r2722  
    4747definition stack_cost_T ≝ ident → nat.
    4848
    49 (* Again, in principle we can use the fact that the state must be a call and
    50    also show some relevant invariants about call states, but we go with the
    51    easier option of returning zero elsewhere. *)
    52 definition Clight_stack_cost :
    53   stack_cost_T →
     49definition Clight_stack_ident :
    5450  cl_genv →
    5551  ∀s:Clight_state.
    5652  match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
    57   nat ≝
    58 λcost,ge,s,H.
    59 match s with
    60 [ Callstate v _ _ _ _ ⇒
    61   match v with [ Vptr p ⇒ match symbol_for_block … ge (pblock p) with [ Some id ⇒ cost id | _ ⇒ 0 ] | _ ⇒ 0 ]
    62 | _ ⇒ 0
     53  ident ≝
     54λge,s.
     55match s return λs. match Clight_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with
     56[ Callstate id _ _ _ _ ⇒ λ_. id
     57| _ ⇒ λH.⊥
    6358].
     59@H
     60qed.
    6461
    6562definition Clight_pcs : preclassified_system ≝
     
    6865  (λ_.Clight_labelled)
    6966  (λ_.Clight_classify)
    70   Clight_stack_cost.
     67  Clight_stack_ident.
    7168
    7269(* From measurable on Clight, we will end up with an RTLabs flat trace where
     
    8077 *)
    8178
    82 axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
     79axiom observables_8051 : object_code → nat → nat → res ((list intensional_event) × (list intensional_event)).
    8380
    8481definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
     
    132129  ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound →
    133130  ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
    134   ∃n1,n2. observables clight_fullexec labelled m1 m2 = observables_8051 object_code n1 n2 ∧
     131  ∃n1,n2. observables Clight_pcs labelled m1 m2 = observables_8051 object_code n1 n2 ∧
    135132          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    136133
Note: See TracChangeset for help on using the changeset viewer.