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

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-<opt> to turn off -f<opt>) :
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
   -ffloat-const-prop <n>  Control constant propagation of floats
                    (<n>=0: none, <n>=1: limited, <n>=2: full; default is full)
+  -ftailcalls    Optimize function calls in tail position [on]
   -falign-functions <n>  Set alignment (in bytes) of function entry points
   -falign-branch-targets <n>  Set alignment (in bytes) of branch targets
   -falign-cond-branches <n>  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) ->