Changeset 2677 for src/Cminor

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:

• Cminor_abstract.ma (modified) (1 diff)
• Cminor_semantics.ma (modified) (5 diffs)

src/Cminor/Cminor_abstract.ma

@@ -23 +23 @@
 λs. match s with
 [ State _ _ _ _ _ _ _ _ _ _ ⇒ cl_other
-| Callstate _ _ _ _ ⇒ cl_call
+| Callstate _ _ _ _ _ ⇒ cl_call
 | Returnstate _ _ _ ⇒ cl_return
 | Finalstate _ ⇒ cl_other

src/Cminor/Cminor_semantics.ma

@@ -69 +69 @@
             state
 | Callstate:
+    ∀   vf: val. (* fn pointer; only used for instrumentation, not the semantics *)
     ∀   fd: fundef internal_function.
     ∀ args: list val.
@@ -297 +298 @@
         ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct … ge vf);
         ! 〈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 ?;
-        return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
+        return 〈tr ⧺ tr', Callstate vf fd vargs m (Scall dst f sp en ? fInv k ? st)〉
 (*
     | St_tailcall ef args ⇒ λInv.
@@ -327 +328 @@
         return 〈Echarge l, State f s' en fInv ? m sp k ? st〉
     ] Inv)
-| Callstate fd args m st ⇒
+| Callstate _ fd args m st ⇒
     match fd with
     [ Internal f ⇒ err_to_io ?? (trace × state) (
@@ -424 +425 @@
   do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
-  OK ? (Callstate f (nil ?) m SStop).
+  OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) m SStop).
 
 definition Cminor_fullexec : fullexec io_out io_in ≝
@@ -438 +439 @@
   do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
   do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
-  OK ? (Callstate f (nil ?) m SStop).
+  OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) m SStop).
 
 definition Cminor_noinit_fullexec : fullexec io_out io_in ≝