Changeset 2677 for src/Cminor


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.

Location:
src/Cminor
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/Cminor_abstract.ma

    r2601 r2677  
    2323λs. match s with
    2424[ State _ _ _ _ _ _ _ _ _ _ ⇒ cl_other
    25 | Callstate _ _ _ _ ⇒ cl_call
     25| Callstate _ _ _ _ _ ⇒ cl_call
    2626| Returnstate _ _ _ ⇒ cl_return
    2727| Finalstate _ ⇒ cl_other
  • src/Cminor/Cminor_semantics.ma

    r2645 r2677  
    6969            state
    7070| Callstate:
     71    ∀   vf: val. (* fn pointer; only used for instrumentation, not the semantics *)
    7172    ∀   fd: fundef internal_function.
    7273    ∀ args: list val.
     
    297298        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct … ge vf);
    298299        ! 〈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 ?;
    299         return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     300        return 〈tr ⧺ tr', Callstate vf fd vargs m (Scall dst f sp en ? fInv k ? st)〉
    300301(*
    301302    | St_tailcall ef args ⇒ λInv.
     
    327328        return 〈Echarge l, State f s' en fInv ? m sp k ? st〉
    328329    ] Inv)
    329 | Callstate fd args m st ⇒
     330| Callstate _ fd args m st ⇒
    330331    match fd with
    331332    [ Internal f ⇒ err_to_io ?? (trace × state) (
     
    424425  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
    425426  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
    426   OK ? (Callstate f (nil ?) m SStop).
     427  OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) m SStop).
    427428
    428429definition Cminor_fullexec : fullexec io_out io_in ≝
     
    438439  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
    439440  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
    440   OK ? (Callstate f (nil ?) m SStop).
     441  OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) m SStop).
    441442
    442443definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.