Stailcall

1 files changed, 21 insertions, 5 deletions

diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v
index 481c43da..b5c3b26f 100644
--- a/mppa_k1c/lib/RTLpathSE_theory.v
+++ b/mppa_k1c/lib/RTLpathSE_theory.v
@@ -856,8 +856,8 @@ Inductive sfval :=
   | Snone
   | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:node)
     (* NB: [res] the return register is hard-wired ! Is it restrictive ? *)
-(*
   | Stailcall: signature -> sval + ident -> list_sval -> sfval
+(*
   | Sbuiltin: external_function -> list (builtin_arg sval) -> builtin_res sval -> sfval
   | Sjumptable: sval -> list node -> sfval
 *)
@@ -879,14 +879,22 @@ Inductive sfmatch (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: sistate) stac
       seval_list_sval ge sp lsv rs0 m0 = Some args ->
       sfmatch pge ge sp st stack f rs0 m0 (Scall sig svos lsv res pc) rs m
         E0 (Callstate (Stackframe res f sp pc rs :: stack) fd args m)
-(* TODO:
-  | exec_Itailcall stk pc rs m sig ros args fd m':
+  | exec_Stailcall stk rs m sig svos args fd m' lsv:
+      sfind_function pge ge sp svos rs0 m0 = Some fd ->
+      funsig fd = sig ->
+      Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
+      seval_list_sval ge sp lsv rs0 m0 = Some args ->
+      sfmatch pge ge sp st stack f rs0 m0 (Stailcall sig svos lsv) rs m
+        E0 (Callstate stack fd args m')
+(* 
+
       (fn_code f)!pc = Some(Itailcall sig ros args) ->
       find_function pge ros rs = Some fd ->
       funsig fd = sig ->
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->
       path_last_step ge pge stack f (Vptr stk Ptrofs.zero) pc rs m
-        E0 (Callstate stack fd rs##args m')
+        E0 (Callstate stack fd rs##args m') *)
+(* TODO:
   | exec_Ibuiltin sp pc rs m ef args res pc' vargs t vres m':
       (fn_code f)!pc = Some(Ibuiltin ef args res pc') ->
       eval_builtin_args ge (fun r => rs#r) sp m args vargs ->
@@ -929,6 +937,10 @@ Definition sfstep (i: instruction) (prev: sistate_local): sfval :=
     let svos := sum_left_map prev.(si_sreg) ros in
     let sargs := list_sval_inj (List.map prev.(si_sreg) args) in
     Scall sig svos sargs res pc
+  | Itailcall sig ros args =>
+    let svos := sum_left_map prev.(si_sreg) ros in
+    let sargs := list_sval_inj (List.map prev.(si_sreg) args) in
+    Stailcall sig svos sargs
   | Ireturn or => 
     let sor := SOME r <- or IN Some (prev.(si_sreg) r) in
     Sreturn sor
@@ -949,7 +961,11 @@ Proof.
     - destruct ros; simpl in * |- *; auto.
       rewrite REG; auto.
     - erewrite seval_list_sval_inj; simpl; auto.
-  + (* Itaillcall *) admit.
+  + (* Itailcall *) intros. eapply exec_Stailcall; auto.
+    - destruct ros; simpl in * |- *; auto.
+      rewrite REG; auto.
+    - eauto.
+    - erewrite seval_list_sval_inj; simpl; auto.
   + (* Ibuiltin *) admit.
   + (* Ijumptable *) admit.
   + (* Ireturn *) intros; eapply exec_Sreturn; simpl; eauto.