Changeset 2722 for src/Clight


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/Clight
Files:
7 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
Note: See TracChangeset for help on using the changeset viewer.