From a3f1744823d6dbeaf400812de86263fb615bbbba Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 17 May 2013 11:37:39 +0000 Subject: Add option -fno-tailcalls to turn off tailcall elimination (causes problem with some static analysis tools). */PrintAsm.ml: don't cfa_adjust at Pfreeframe, as more code from the function can appear after (in case of tailcalls). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2256 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/PrintAsm.ml | 4 +--- backend/Tailcall.v | 7 +++++-- backend/Tailcallproof.v | 10 ++++++---- driver/Clflags.ml | 1 + driver/Driver.ml | 2 ++ extraction/extraction.v | 5 +++++ ia32/PrintAsm.ml | 3 +-- powerpc/PrintAsm.ml | 3 +-- 8 files changed, 22 insertions(+), 13 deletions(-) diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index a506bed..cb3ce4d 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -648,9 +648,7 @@ let print_instruction oc = function | Pfreeframe(sz, ofs) -> if Asmgen.is_immed_arith sz then fprintf oc " add sp, sp, #%a\n" coqint sz - else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; - cfi_adjust oc (Int32.neg (camlint_of_coqint sz)); - 1 + else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1 | Plabel lbl -> fprintf oc "%a:\n" print_label lbl; 0 | Ploadsymbol(r1, id, ofs) -> diff --git a/backend/Tailcall.v b/backend/Tailcall.v index 917ec83..26beb34 100644 --- a/backend/Tailcall.v +++ b/backend/Tailcall.v @@ -95,10 +95,13 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) := end. (** A function is transformed only if its stack block is empty, - as explained above. *) + as explained above. Moreover, we can turn tail calls off + using a compilation option. *) + +Parameter eliminate_tailcalls: unit -> bool. Definition transf_function (f: function) : function := - if zeq f.(fn_stacksize) 0 + if zeq f.(fn_stacksize) 0 && eliminate_tailcalls tt then RTL.transf_function (transf_instr f) f else f. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 02a6ca9..77725cf 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -181,10 +181,12 @@ Lemma transf_instr_lookup: f.(fn_code)!pc = Some i -> exists i', (transf_function f).(fn_code)!pc = Some i' /\ transf_instr_spec f i i'. Proof. - intros. unfold transf_function. destruct (zeq (fn_stacksize f) 0). + intros. unfold transf_function. + destruct (zeq (fn_stacksize f) 0). destruct (eliminate_tailcalls tt). simpl. rewrite PTree.gmap. rewrite H. simpl. exists (transf_instr f pc i); split. auto. apply transf_instr_charact; auto. exists i; split. auto. constructor. + exists i; split. auto. constructor. Qed. (** * Semantic properties of the code transformation *) @@ -260,14 +262,14 @@ Lemma sig_preserved: forall f, funsig (transf_fundef f) = funsig f. Proof. destruct f; auto. simpl. unfold transf_function. - destruct (zeq (fn_stacksize f) 0); auto. + destruct (zeq (fn_stacksize f) 0 && eliminate_tailcalls tt); auto. Qed. Lemma stacksize_preserved: forall f, fn_stacksize (transf_function f) = fn_stacksize f. Proof. unfold transf_function. intros. - destruct (zeq (fn_stacksize f) 0); auto. + destruct (zeq (fn_stacksize f) 0 && eliminate_tailcalls tt); auto. Qed. Lemma find_function_translated: @@ -553,7 +555,7 @@ Proof. assert (fn_stacksize (transf_function f) = fn_stacksize f /\ fn_entrypoint (transf_function f) = fn_entrypoint f /\ fn_params (transf_function f) = fn_params f). - unfold transf_function. destruct (zeq (fn_stacksize f) 0); auto. + unfold transf_function. destruct (zeq (fn_stacksize f) 0 && eliminate_tailcalls tt); auto. destruct H0 as [EQ1 [EQ2 EQ3]]. left. econstructor; split. simpl. eapply exec_function_internal; eauto. rewrite EQ1; eauto. diff --git a/driver/Clflags.ml b/driver/Clflags.ml index d70467a..88983d1 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -22,6 +22,7 @@ let option_fvararg_calls = ref true let option_fpacked_structs = ref false let option_fsse = ref true let option_ffloatconstprop = ref 2 +let option_ftailcalls = ref true let option_falignfunctions = ref (None: int option) let option_falignbranchtargets = ref 0 let option_faligncondbranchs = ref 0 diff --git a/driver/Driver.ml b/driver/Driver.ml index 3d981f0..0e54ad9 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -392,6 +392,7 @@ Code generation options: (use -fno- to turn off -f) : -fsmall-const Set maximal size for allocation in small constant area -ffloat-const-prop Control constant propagation of floats (=0: none, =1: limited, =2: full; default is full) + -ftailcalls Optimize function calls in tail position [on] -falign-functions Set alignment (in bytes) of function entry points -falign-branch-targets Set alignment (in bytes) of branch targets -falign-cond-branches Set alignment (in bytes) of conditional branches @@ -500,6 +501,7 @@ let cmdline_actions = "-fnone$", Self (fun _ -> List.iter (fun r -> r := false) language_support_options); ] + @ f_opt "tailcalls" option_ftailcalls @ f_opt "longdouble" option_flongdouble @ f_opt "struct-return" option_fstruct_return @ f_opt "bitfields" option_fbitfields diff --git a/extraction/extraction.v b/extraction/extraction.v index df155f1..6bc0234 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -19,6 +19,7 @@ Require RTLgen. Require Inlining. Require ConstpropOp. Require Constprop. +Require Tailcall. Require Allocation. Require Compiler. @@ -73,6 +74,10 @@ Extract Constant ConstpropOp.propagate_float_constants => Extract Constant Constprop.generate_float_constants => "fun _ -> !Clflags.option_ffloatconstprop >= 2". +(* Tailcall *) +Extract Constant Tailcall.eliminate_tailcalls => + "fun _ -> !Clflags.option_ftailcalls". + (* Allocation *) Extract Constant Allocation.regalloc => "Regalloc.regalloc". diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 12f6691..5ee4d01 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -716,8 +716,7 @@ let print_instruction oc = function fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link | Pfreeframe(sz, ofs_ra, ofs_link) -> let sz = sp_adjustment sz in - fprintf oc " addl $%ld, %%esp\n" sz; - cfi_adjust oc (Int32.neg sz) + fprintf oc " addl $%ld, %%esp\n" sz | Pbuiltin(ef, args, res) -> begin match ef with | EF_builtin(name, sg) -> diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index dd0ec1f..12dd78c 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -715,8 +715,7 @@ let print_instruction oc tbl pc fallthrough = function if sz < 0x8000l then fprintf oc " addi %a, %a, %ld\n" ireg GPR1 ireg GPR1 sz else - fprintf oc " lwz %a, %ld(%a)\n" ireg GPR1 ofs ireg GPR1; - cfi_adjust oc (Int32.neg sz) + fprintf oc " lwz %a, %ld(%a)\n" ireg GPR1 ofs ireg GPR1 | Pfabs(r1, r2) -> fprintf oc " fabs %a, %a\n" freg r1 freg r2 | Pfadd(r1, r2, r3) -> -- cgit v1.2.3