Add explicit tail calls to Clight and C#minor

cfrontend/Clight.v

@@ -98,6 +98,7 @@ Inductive statement : Type :=
   | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *)
   | Sset : ident -> expr -> statement   (**r assignment [tempvar = rvalue] *)
   | Scall: option ident -> expr -> list expr -> statement (**r function call *)
+  | Stailcall: expr -> list expr -> statement (**r function call in tail position *)
   | Sbuiltin: option ident -> external_function -> typelist -> list expr -> statement (**r builtin invocation *)
   | Ssequence : statement -> statement -> statement  (**r sequence *)
   | Sifthenelse : expr  -> statement -> statement -> statement (**r conditional *)
@@ -580,6 +581,17 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Scall optid a al) k e le m)
         E0 (Callstate fd vargs (Kcall optid f e le k) m)
 
+  | step_tailcall:   forall f a al k e le m tyargs tyres cconv vf vargs fd m',
+      classify_fun (typeof a) = fun_case_f tyargs tyres cconv ->
+      eval_expr e le m a vf ->
+      eval_exprlist e le m al tyargs vargs ->
+      Genv.find_funct ge vf = Some fd ->
+      type_of_fundef fd = Tfunction tyargs tyres cconv ->
+      fn_return f = tyres ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
+      step (State f (Stailcall a al) k e le m)
+        E0 (Callstate fd vargs (call_cont k) m')
+
   | step_builtin:   forall f optid ef tyargs al k e le m vargs t vres m',
       eval_exprlist e le m al tyargs vargs ->
       external_call ef ge vargs m t vres m' ->

cfrontend/Cminorgen.v

@@ -164,6 +164,10 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt)
       do te <- transl_expr cenv e;
       do tel <- transl_exprlist cenv el;
       OK (Scall optid sig te tel)
+  | Csharpminor.Stailcall sig e el =>
+      do te <- transl_expr cenv e;
+      do tel <- transl_exprlist cenv el;
+      OK (Stailcall sig te tel)
   | Csharpminor.Sbuiltin optid ef el =>
       do tel <- transl_exprlist cenv el;
       OK (Sbuiltin optid ef tel)

cfrontend/Cminorgenproof.v

@@ -1664,6 +1664,12 @@ Proof.
   econstructor; split. apply star_refl. split. exact I. econstructor; eauto.
 Qed.
 
+Lemma call_cont_is_call_cont:
+  forall k, Csharpminor.is_call_cont (Csharpminor.call_cont k).
+Proof.
+  induction k; simpl; auto.
+Qed.
+
 (** Properties of [switch] compilation *)
 
 Inductive lbl_stmt_tail: lbl_stmt -> nat -> lbl_stmt -> Prop :=
@@ -1951,7 +1957,7 @@ Lemma transl_step_correct:
 Proof.
   induction 1; intros T1 MSTATE; inv MSTATE.
 
-(* skip seq *)
+- (* skip seq *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -1963,7 +1969,7 @@ Proof.
   exploit IHMK; eauto. intros [T2 [A B]].
   exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq.
   auto.
-(* skip block *)
+- (* skip block *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -1972,23 +1978,23 @@ Proof.
   exploit IHMK; eauto. intros [T2 [A B]].
   exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq.
   auto.
-(* skip call *)
+- (* skip call *)
   monadInv TR. left.
   exploit match_is_call_cont; eauto. intros [tk' [A [B C]]].
   exploit match_callstack_freelist; eauto. intros [tm' [P [Q R]]].
   econstructor; split.
   eapply plus_right. eexact A. apply step_skip_call. auto. eauto. traceEq.
   econstructor; eauto.
 
-(* set *)
+- (* set *)
   monadInv TR.
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   left; econstructor; split.
   apply plus_one. econstructor; eauto.
   econstructor; eauto.
   eapply match_callstack_set_temp; eauto.
 
-(* store *)
+- (* store *)
   monadInv TR.
   exploit transl_expr_correct. eauto. eauto. eexact H. eauto.
   intros [tv1 [EVAL1 VINJ1]].
@@ -2005,7 +2011,7 @@ Proof.
   intros. eapply Mem.perm_store_2; eauto.
   intros. eapply Mem.perm_store_1; eauto.
 
-(* call *)
+- (* call *)
   simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]].
   monadInv TR.
   exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]].
@@ -2022,7 +2028,24 @@ Proof.
   eapply match_Kcall with (cenv' := cenv); eauto.
   red; auto.
 
-(* builtin *)
+- (* tailcall *)
+  simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]].
+  monadInv TR.
+  exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]].
+  assert (tvf = vf).
+    exploit match_callstack_match_globalenvs; eauto. intros [bnd MG].
+    eapply val_inject_function_pointer; eauto.
+  subst tvf.
+  exploit transl_exprlist_correct; eauto. intros [tvargs [EVAL2 VINJ2]].
+  exploit match_callstack_freelist; eauto. intros [tm' [P [Q R]]].
+  left; econstructor; split.
+  apply plus_one. eapply step_tailcall; eauto.
+  apply sig_preserved; eauto.
+  econstructor; eauto.
+  eapply match_call_cont; eauto.
+  apply call_cont_is_call_cont.
+
+- (* builtin *)
   monadInv TR.
   exploit transl_exprlist_correct; eauto.
   intros [tvargs [EVAL2 VINJ2]].
@@ -2048,37 +2071,37 @@ Opaque PTree.set.
   eapply match_callstack_set_temp; eauto.
   auto.
 
-(* seq *)
+- (* seq *)
   monadInv TR.
   left; econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
   econstructor; eauto.
-(* seq 2 *)
+- (* seq 2 *)
   right. split. auto. split. auto. econstructor; eauto.
 
-(* ifthenelse *)
+- (* ifthenelse *)
   monadInv TR.
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Ptrofs.zero) te tm); split.
   apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto.
   econstructor; eauto. destruct b; auto.
 
-(* loop *)
+- (* loop *)
   monadInv TR.
   left; econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
   econstructor; eauto. simpl. rewrite EQ; auto.
 
-(* block *)
+- (* block *)
   monadInv TR.
   left; econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
   econstructor; eauto.
 
-(* exit seq *)
+- (* exit seq *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -2090,7 +2113,7 @@ Opaque PTree.set.
   exists T2; split; auto. eapply plus_left.
   simpl. constructor. apply plus_star; eauto. traceEq.
 
-(* exit block 0 *)
+- (* exit block 0 *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -2100,7 +2123,7 @@ Opaque PTree.set.
   exists T2; split; auto. simpl.
   eapply plus_left. constructor. apply plus_star; eauto. traceEq.
 
-(* exit block n+1 *)
+- (* exit block n+1 *)
   monadInv TR. left.
   dependent induction MK.
   econstructor; split.
@@ -2110,7 +2133,7 @@ Opaque PTree.set.
   exists T2; split; auto. simpl.
   eapply plus_left. constructor. apply plus_star; eauto. traceEq.
 
-(* switch *)
+- (* switch *)
   simpl in TR. destruct (switch_table cases O) as [tbl dfl] eqn:STBL. monadInv TR.
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   assert (SA: switch_argument islong tv n).
@@ -2129,37 +2152,36 @@ Opaque PTree.set.
   reflexivity. reflexivity. traceEq.
   auto.
 
-(* return none *)
+- (* return none *)
   monadInv TR. left.
   exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
   econstructor; split.
   apply plus_one. eapply step_return_0. eauto.
   econstructor; eauto. eapply match_call_cont; eauto.
-  simpl; auto.
 
-(* return some *)
+- (* return some *)
   monadInv TR. left.
   exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]].
   exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]].
   econstructor; split.
   apply plus_one. eapply step_return_1. eauto. eauto.
   econstructor; eauto. eapply match_call_cont; eauto.
 
-(* label *)
+- (* label *)
   monadInv TR.
   left; econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
 
-(* goto *)
+- (* goto *)
   monadInv TR.
   exploit transl_find_label_body; eauto.
   intros [ts' [tk' [xenv' [A [B C]]]]].
   left; econstructor; split.
   apply plus_one. apply step_goto. eexact A.
   econstructor; eauto.
 
-(* internal call *)
+- (* internal call *)
   monadInv TR. generalize EQ; clear EQ; unfold transl_function.
   caseEq (build_compilenv f). intros ce sz BC.
   destruct (zle sz Ptrofs.max_unsigned); try congruence.
@@ -2178,7 +2200,7 @@ Opaque PTree.set.
   econstructor. eexact TRBODY. eauto. eexact MINJ2. eexact MCS2.
   inv MK; simpl in ISCC; contradiction || econstructor; eauto.
 
-(* external call *)
+- (* external call *)
   monadInv TR.
   exploit match_callstack_match_globalenvs; eauto. intros [hi MG].
   exploit external_call_mem_inject; eauto.
@@ -2195,7 +2217,7 @@ Opaque PTree.set.
   eapply external_call_nextblock; eauto.
   eapply external_call_nextblock; eauto.
 
-(* return *)
+- (* return *)
   inv MK. simpl.
   left; econstructor; split.
   apply plus_one. econstructor; eauto.

cfrontend/Csharpminor.v

@@ -62,6 +62,7 @@ Inductive stmt : Type :=
   | Sset : ident -> expr -> stmt
   | Sstore : memory_chunk -> expr -> expr -> stmt
   | Scall : option ident -> signature -> expr -> list expr -> stmt
+  | Stailcall: signature -> expr -> list expr -> stmt
   | Sbuiltin : option ident -> external_function -> list expr -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: expr -> stmt -> stmt -> stmt
@@ -390,6 +391,15 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Scall optid sig a bl) k e le m)
         E0 (Callstate fd vargs (Kcall optid f e le k) m)
 
+  | step_tailcall: forall f sig a bl k e le m vf vargs fd m',
+      eval_expr e le m a vf ->
+      eval_exprlist e le m bl vargs ->
+      Genv.find_funct ge vf = Some fd ->
+      funsig fd = sig ->
+      Mem.free_list m (blocks_of_env e) = Some m' ->
+      step (State f (Stailcall sig a bl) k e le m)
+        E0 (Callstate fd vargs (call_cont k) m')
+
   | step_builtin: forall f optid ef bl k e le m vargs t vres m',
       eval_exprlist e le m bl vargs ->
       external_call ef ge vargs m t vres m' ->

cfrontend/Cshmgen.v

@@ -687,6 +687,17 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
           OK (make_funcall x res sg tb tcl)
       | _ => Error(msg "Cshmgen.transl_stmt(call)")
       end
+  | Clight.Stailcall b cl =>
+      match classify_fun (typeof b) with
+      | fun_case_f args res cconv =>
+          do tb <- transl_expr ce b;
+          do tcl <- transl_arglist ce cl args;
+          let sg := {| sig_args := typlist_of_arglist cl args;
+                       sig_res  := rettype_of_type res;
+                       sig_cc   := cconv |} in
+          OK (Stailcall sg tb tcl)
+      | _ => Error(msg "Cshmgen.transl_stmt(tailcall)")
+      end
   | Clight.Sbuiltin x ef tyargs bl =>
       do tbl <- transl_arglist ce bl tyargs;
       OK(Sbuiltin x ef tbl)

cfrontend/Cshmgenproof.v

@@ -1572,6 +1572,9 @@ Proof.
   simpl in TR. destruct (classify_fun (typeof e)); monadInv TR.
   unfold make_funcall.
   destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto.
+- (* tailcall *)
+  simpl in TR. destruct (classify_fun (typeof e)); monadInv TR.
+  auto.
 - (* builtin *)
   auto.
 - (* seq *)
@@ -1651,6 +1654,12 @@ Proof.
   split; auto; eapply match_Kcall_normalize; eauto.
 Qed.
 
+Lemma call_cont_is_call_cont:
+  forall k, Clight.is_call_cont (Clight.call_cont k).
+Proof.
+  induction k; simpl; auto.
+Qed.
+
 (** The simulation proof *)
 
 Lemma transl_step:
@@ -1725,6 +1734,26 @@ Proof.
     intros. eapply make_normalization_correct; eauto. constructor; eauto.
     exact I.
 
+- (* tailcall *)
+  revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
+  intros targs tres cc CF TR. monadInv TR. inv MTR.
+  exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK').
+  rewrite H in CF. simpl in CF. inv CF.
+  set (sg := {| sig_args := typlist_of_arglist al targs;
+                sig_res := rettype_of_type (fn_return f);
+                sig_cc := cc |}) in *.
+  assert (SIG: funsig tfd = sg).
+  { unfold sg; erewrite typlist_of_arglist_eq by eauto.
+    eapply transl_fundef_sig1; eauto. rewrite H3; auto. }
+  econstructor; split.
+  apply plus_one. eapply step_tailcall; eauto.
+  eapply transl_expr_correct with (cunit := cu); eauto.
+  eapply transl_arglist_correct with (cunit := cu); eauto.
+  eapply match_env_free_blocks; eauto.
+  eapply match_callstate with (ce := prog_comp_env cu); eauto.
+  eapply match_cont_call_cont. eauto.
+  apply call_cont_is_call_cont.
+
 - (* builtin *)
   monadInv TR. inv MTR.
   econstructor; split.

cfrontend/PrintClight.ml

@@ -143,6 +143,10 @@ let rec print_stmt p s =
                 (temp_name id)
                 expr (15, e1)
                 print_expr_list (true, el)
+  | Stailcall(e1, el) ->
+      fprintf p "@[<hv 2>return %a@,(@[<hov 0>%a@]);@ /*tailcall*/@]"
+                expr (15, e1)
+                print_expr_list (true, el)
   | Sbuiltin(None, ef, tyargs, el) ->
       fprintf p "@[<hv 2>builtin %s@,(@[<hov 0>%a@]);@]"
                 (name_of_external ef)

cfrontend/SimplLocals.v

@@ -119,6 +119,8 @@ Fixpoint simpl_stmt (cenv: compilenv) (s: statement) : res statement :=
   | Scall optid a al =>
       do x <- check_opttemp cenv optid;
       OK (Scall optid (simpl_expr cenv a) (simpl_exprlist cenv al))
+  | Stailcall a al =>
+      OK (Stailcall (simpl_expr cenv a) (simpl_exprlist cenv al))
   | Sbuiltin optid ef tyargs al =>
       do x <- check_opttemp cenv optid;
       OK (Sbuiltin optid ef tyargs (simpl_exprlist cenv al))
@@ -208,6 +210,7 @@ Fixpoint addr_taken_stmt (s: statement) : VSet.t :=
   | Sassign a b => VSet.union (addr_taken_expr a) (addr_taken_expr b)
   | Sset id a => addr_taken_expr a
   | Scall optid a bl => VSet.union (addr_taken_expr a) (addr_taken_exprlist bl)
+  | Stailcall a bl => VSet.union (addr_taken_expr a) (addr_taken_exprlist bl)
   | Sbuiltin optid ef tyargs bl => addr_taken_exprlist bl
   | Ssequence s1 s2 => VSet.union (addr_taken_stmt s1) (addr_taken_stmt s2)
   | Sifthenelse a s1 s2 =>