From deea958b06b6c2c907c266ec5e996cf62216b985 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 12 Nov 2021 15:40:05 +0100 Subject: [PATCH 1/2] Add explicit tail calls to Clight and to C#minor By popular demand. The tail call optimization pass performed later in CompCert will not turn a call into a tail call if the function has stack-allocated data, because this might change the semantics. Having an explicit Stailcall form in Clight makes it possible to force some calls in tail position to be tail calls, deallocating. deallocate stack-allocated data before the call. This is the same reason why we have an Stailcall form in Cminor already. --- cfrontend/Clight.v | 12 ++++++ cfrontend/Cminorgen.v | 4 ++ cfrontend/Cminorgenproof.v | 70 ++++++++++++++++++++++------------ cfrontend/Csharpminor.v | 10 +++++ cfrontend/Cshmgen.v | 11 ++++++ cfrontend/Cshmgenproof.v | 29 ++++++++++++++ cfrontend/PrintClight.ml | 4 ++ cfrontend/SimplLocals.v | 3 ++ cfrontend/SimplLocalsproof.v | 73 ++++++++++++++++++++++-------------- 9 files changed, 164 insertions(+), 52 deletions(-) diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index d15bc90ad4..16a73e12f8 100644 --- a/cfrontend/Clight.v +++ b/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' -> diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 1b031866e8..8f4d44e9b0 100644 --- a/cfrontend/Cminorgen.v +++ b/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) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index bc1c92ca7c..5f77a44efd 100644 --- a/cfrontend/Cminorgenproof.v +++ b/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,7 +1978,7 @@ 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]]]. @@ -1980,7 +1986,7 @@ Proof. 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. @@ -1988,7 +1994,7 @@ Proof. 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,15 +2152,14 @@ 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]]]. @@ -2145,13 +2167,13 @@ Opaque PTree.set. 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]]]]]. @@ -2159,7 +2181,7 @@ Opaque PTree.set. 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. diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 4393640ced..c4260882da 100644 --- a/cfrontend/Csharpminor.v +++ b/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' -> diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 9e80417667..5fb302abe2 100644 --- a/cfrontend/Cshmgen.v +++ b/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) diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index 9829388805..2c32ff3edc 100644 --- a/cfrontend/Cshmgenproof.v +++ b/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. diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index a9ecb342cd..a226bd2caa 100644 --- a/cfrontend/PrintClight.ml +++ b/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 "@[return %a@,(@[%a@]);@ /*tailcall*/@]" + expr (15, e1) + print_expr_list (true, el) | Sbuiltin(None, ef, tyargs, el) -> fprintf p "@[builtin %s@,(@[%a@]);@]" (name_of_external ef) diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index 0a164e2949..750658ac53 100644 --- a/cfrontend/SimplLocals.v +++ b/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 => diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index c133d8eab7..760b433bc0 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -1952,6 +1952,8 @@ Proof. monadInv TS; auto. (* call *) monadInv TS; auto. + (* tailcall *) + monadInv TS; auto. (* builtin *) monadInv TS; auto. (* seq *) @@ -2035,7 +2037,7 @@ Lemma step_simulation: Proof. induction 1; simpl; intros; inv MS; simpl in *; try (monadInv TRS). -(* assign *) +- (* assign *) generalize (is_liftable_var_charact (cenv_for f) a1); destruct (is_liftable_var (cenv_for f) a1) as [id|]; monadInv TRS. (* liftable *) intros [ty [P Q]]; subst a1; simpl in *. @@ -2043,7 +2045,7 @@ Proof. exploit sem_cast_inject; eauto. intros [tv [C D]]. exploit me_vars; eauto. instantiate (1 := id). intros MV. inv H. - (* local variable *) ++ (* local variable *) econstructor; split. eapply step_Sset_debug. eauto. rewrite typeof_simpl_expr. eauto. econstructor; eauto with compat. @@ -2052,9 +2054,9 @@ Proof. inv MV; try congruence. inv H2; try congruence. unfold Mem.storev in H3. eapply Mem.store_unmapped_inject; eauto. congruence. erewrite assign_loc_nextblock; eauto. - (* global variable *) ++ (* global variable *) inv MV; congruence. - (* not liftable *) ++ (* not liftable *) intros P. exploit eval_simpl_lvalue; eauto with compat. intros [tb [tofs [E F]]]. exploit eval_simpl_expr; eauto with compat. intros [tv2 [A B]]. @@ -2069,14 +2071,14 @@ Proof. erewrite assign_loc_nextblock; eauto. erewrite assign_loc_nextblock; eauto. -(* set temporary *) +- (* set temporary *) exploit eval_simpl_expr; eauto with compat. intros [tv [A B]]. econstructor; split. apply plus_one. econstructor. eauto. econstructor; eauto with compat. eapply match_envs_set_temp; eauto. -(* call *) +- (* call *) exploit eval_simpl_expr; eauto with compat. intros [tvf [A B]]. exploit eval_simpl_exprlist; eauto with compat. intros [CASTED [tvargs [C D]]]. exploit match_cont_find_funct; eauto. intros [tfd [P Q]]. @@ -2088,7 +2090,22 @@ Proof. econstructor; eauto. intros. econstructor; eauto. -(* builtin *) +- (* tailcall *) + exploit eval_simpl_expr; eauto with compat. intros [tvf [A B]]. + exploit eval_simpl_exprlist; eauto with compat. intros [CASTED [tvargs [C D]]]. + exploit match_cont_find_funct; eauto. intros [tfd [P Q]]. + exploit match_envs_free_blocks; eauto. intros [tm' [U V]]. + econstructor; split. + apply plus_one. eapply step_tailcall with (fd := tfd). + rewrite typeof_simpl_expr. eauto. + eauto. eauto. eauto. + erewrite type_of_fundef_preserved; eauto. + monadInv TRF; auto. + eauto. + econstructor; eauto. + intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto. + +- (* builtin *) exploit eval_simpl_exprlist; eauto with compat. intros [CASTED [tvargs [C D]]]. exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals; eauto with compat. intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]]. @@ -2102,53 +2119,53 @@ Proof. eapply Ple_trans; eauto. eapply external_call_nextblock; eauto. eapply Ple_trans; eauto. eapply external_call_nextblock; eauto. -(* sequence *) +- (* sequence *) econstructor; split. apply plus_one. econstructor. econstructor; eauto with compat. econstructor; eauto with compat. -(* skip sequence *) +- (* skip sequence *) inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto. -(* continue sequence *) +- (* continue sequence *) inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto. -(* break sequence *) +- (* break sequence *) inv MCONT. econstructor; split. apply plus_one. econstructor. econstructor; eauto. -(* ifthenelse *) +- (* ifthenelse *) exploit eval_simpl_expr; eauto with compat. intros [tv [A B]]. econstructor; split. apply plus_one. apply step_ifthenelse with (v1 := tv) (b := b). auto. rewrite typeof_simpl_expr. eapply bool_val_inject; eauto. destruct b; econstructor; eauto with compat. -(* loop *) +- (* loop *) econstructor; split. apply plus_one. econstructor. econstructor; eauto with compat. econstructor; eauto with compat. -(* skip-or-continue loop *) +- (* skip-or-continue loop *) inv MCONT. econstructor; split. apply plus_one. econstructor. destruct H; subst x; simpl in *; intuition congruence. econstructor; eauto with compat. econstructor; eauto with compat. -(* break loop1 *) +- (* break loop1 *) inv MCONT. econstructor; split. apply plus_one. eapply step_break_loop1. econstructor; eauto. -(* skip loop2 *) +- (* skip loop2 *) inv MCONT. econstructor; split. apply plus_one. eapply step_skip_loop2. econstructor; eauto with compat. simpl; rewrite H2; rewrite H4; auto. -(* break loop2 *) +- (* break loop2 *) inv MCONT. econstructor; split. apply plus_one. eapply step_break_loop2. econstructor; eauto. -(* return none *) +- (* return none *) exploit match_envs_free_blocks; eauto. intros [tm' [P Q]]. econstructor; split. apply plus_one. econstructor; eauto. econstructor; eauto. intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto. -(* return some *) +- (* return some *) exploit eval_simpl_expr; eauto with compat. intros [tv [A B]]. exploit sem_cast_inject; eauto. intros [tv' [C D]]. exploit match_envs_free_blocks; eauto. intros [tm' [P Q]]. @@ -2157,7 +2174,7 @@ Proof. econstructor; eauto. intros. eapply match_cont_call_cont. eapply match_cont_free_env; eauto. -(* skip call *) +- (* skip call *) exploit match_envs_free_blocks; eauto. intros [tm' [P Q]]. econstructor; split. apply plus_one. econstructor; eauto. eapply match_cont_is_call_cont; eauto. @@ -2165,7 +2182,7 @@ Proof. econstructor; eauto. intros. apply match_cont_change_cenv with (cenv_for f); auto. eapply match_cont_free_env; eauto. -(* switch *) +- (* switch *) exploit eval_simpl_expr; eauto with compat. intros [tv [A B]]. econstructor; split. apply plus_one. econstructor; eauto. rewrite typeof_simpl_expr. instantiate (1 := n). @@ -2178,20 +2195,20 @@ Proof. econstructor; eauto. rewrite addr_taken_seq_of_labeled_statement. apply compat_cenv_select_switch. eauto with compat. -(* skip-break switch *) +- (* skip-break switch *) inv MCONT. econstructor; split. apply plus_one. eapply step_skip_break_switch. destruct H; subst x; simpl in *; intuition congruence. econstructor; eauto with compat. -(* continue switch *) +- (* continue switch *) inv MCONT. econstructor; split. apply plus_one. eapply step_continue_switch. econstructor; eauto with compat. -(* label *) +- (* label *) econstructor; split. apply plus_one. econstructor. econstructor; eauto. -(* goto *) +- (* goto *) generalize TRF; intros TRF'. monadInv TRF'. exploit (simpl_find_label j (cenv_for f) m lo tlo lbl (fn_body f) (call_cont k) x (call_cont tk)). eauto. eapply match_cont_call_cont. eauto. @@ -2202,7 +2219,7 @@ Proof. rewrite find_label_add_debug_params. rewrite find_label_store_params. rewrite find_label_add_debug_vars. eexact A. econstructor; eauto. -(* internal function *) +- (* internal function *) monadInv TRFD. inv H. generalize EQ; intro EQ'; monadInv EQ'. assert (list_norepet (var_names (fn_params f ++ fn_vars f))). @@ -2248,7 +2265,7 @@ Proof. rewrite (bind_parameters_nextblock _ _ _ _ _ _ H2). extlia. rewrite T; extlia. -(* external function *) +- (* external function *) monadInv TRFD. inv FUNTY. exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals. eapply match_cont_globalenv. eexact (MCONT VSet.empty). @@ -2261,7 +2278,7 @@ Proof. eapply external_call_nextblock; eauto. eapply external_call_nextblock; eauto. -(* return *) +- (* return *) specialize (MCONT (cenv_for f)). inv MCONT. econstructor; split. apply plus_one. econstructor. From ad80cb74e7459c1b1405d9428fedf4914a5afece Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 18 Nov 2021 17:40:52 +0100 Subject: [PATCH 2/2] Update clightgen to handle tail calls --- export/Clightnorm.ml | 4 ++++ export/ExportClight.ml | 5 +++++ 2 files changed, 9 insertions(+) diff --git a/export/Clightnorm.ml b/export/Clightnorm.ml index 88d44c08a9..9a7a8872cf 100644 --- a/export/Clightnorm.ml +++ b/export/Clightnorm.ml @@ -118,6 +118,10 @@ let rec norm_stmt s = let (sl1, e') = norm_expr e in let (sl2, el') = norm_expr_list el in add_sequence (sl1 @ sl2) (Scall(optid, e', el')) + | Stailcall(e, el) -> + let (sl1, e') = norm_expr e in + let (sl2, el') = norm_expr_list el in + add_sequence (sl1 @ sl2) (Stailcall(e', el')) | Sbuiltin(optid, ef, tyl, el) -> let (sl, el') = norm_expr_list el in add_sequence sl (Sbuiltin(optid, ef, tyl, el')) diff --git a/export/ExportClight.ml b/export/ExportClight.ml index e3b00986a9..2d6f9b203d 100644 --- a/export/ExportClight.ml +++ b/export/ExportClight.ml @@ -95,6 +95,9 @@ let rec stmt p = function | Scall(optid, e1, el) -> fprintf p "@[(Scall %a@ %a@ %a)@]" (print_option ident) optid expr e1 (print_list expr) el + | Stailcall(e1, el) -> + fprintf p "@[(Stailcall@ %a@ %a)@]" + expr e1 (print_list expr) el | Sbuiltin(optid, ef, tyl, el) -> fprintf p "@[(Sbuiltin %a@ %a@ %a@ %a)@]" (print_option ident) optid @@ -197,6 +200,8 @@ let rec name_stmt = function | Sset(id, e2) -> name_temporary id; name_expr e2 | Scall(optid, e1, el) -> name_opt_temporary optid; name_expr e1; List.iter name_expr el + | Stailcall(e1, el) -> + name_expr e1; List.iter name_expr el | Sbuiltin(optid, ef, tyl, el) -> name_opt_temporary optid; List.iter name_expr el | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2