Changeset 2677 for src/Clight/Csem.ma


Ignore:
Timestamp:
Feb 19, 2013, 12:23:50 PM (8 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/Clight/Csem.ma

    r2608 r2677  
    933933      ∀m: mem.  state
    934934  | Callstate:
     935      ∀fb: val. (* function pointer; used by stack instrumentation, but not the semantics *)
    935936      ∀fd: clight_fundef.
    936937      ∀args: list val.
     
    10301031      type_of_fundef fd = fun_typeof a →
    10311032      step ge (State f (Scall (None ?) a al) k e m)
    1032            (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m)
     1033           (tr1⧺tr2) (Callstate vf fd vargs (Kcall (None ?) f e k) m)
    10331034
    10341035  | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
     
    10391040      type_of_fundef fd = fun_typeof a →
    10401041      step ge (State f (Scall (Some ? lhs) a al) k e m)
    1041            (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
     1042           (tr1⧺tr2⧺tr3) (Callstate vf fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)
    10421043
    10431044  | step_seq:  ∀f,s1,s2,k,e,m.
     
    11651166           E0 (State f s' k' e m)
    11661167
    1167   | step_internal_function: ∀f,vargs,k,m,e,m1,m2.
     1168  | step_internal_function: ∀vf,f,vargs,k,m,e,m1,m2.
    11681169      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 →
    11691170      bind_parameters e m1 (fn_params f) vargs m2 →
    1170       step ge (Callstate (CL_Internal f) vargs k m)
     1171      step ge (Callstate vf (CL_Internal f) vargs k m)
    11711172           E0 (State f (fn_body f) k e m2)
    11721173
    1173   | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.
     1174  | step_external_function: ∀vf,id,targs,tres,vargs,k,m,vres,t.
    11741175      event_match (external_function id targs tres) vargs t vres →
    1175       step ge (Callstate (CL_External id targs tres) vargs k m)
     1176      step ge (Callstate vf (CL_External id targs tres) vargs k m)
    11761177            t (Returnstate vres k m)
    11771178
     
    12101211      find_symbol … ge (prog_main ?? p) = Some ? b →
    12111212      find_funct_ptr … ge b = Some ? f →
    1212       initial_state p (Callstate f (nil ?) Kstop m0).
     1213      initial_state p (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) Kstop m0).
    12131214
    12141215(* * A final state is a [Returnstate] with an empty continuation. *)
Note: See TracChangeset for help on using the changeset viewer.