powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).

Added -dmach option and corresponding printer for Mach code.
CleanupLabelsproof.v: fixed for ARM
Driver.ml: -E sends output to stdout; support for .s and .S source files.
cparser/Elab.ml: spurious comment deleted.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 46 insertions, 11 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index b34b10a..c47d0f3 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -31,6 +31,7 @@ let option_dcastopt = ref false
 let option_dconstprop = ref false
 let option_dcse = ref false
 let option_dalloc = ref false
+let option_dmach = ref false
 let option_dasm = ref false
 let option_E = ref false
 let option_S = ref false
diff --git a/driver/Compiler.v b/driver/Compiler.v
index bde6308..d8810a4 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -92,6 +92,7 @@ Parameter print_RTL_castopt: RTL.fundef -> unit.
 Parameter print_RTL_constprop: RTL.fundef -> unit.
 Parameter print_RTL_cse: RTL.fundef -> unit.
 Parameter print_LTLin: LTLin.fundef -> unit.
+Parameter print_Mach: Mach.fundef -> unit.
 
 Open Local Scope string_scope.
 
@@ -113,7 +114,7 @@ Notation "a @@ b" :=
    (apply_total _ _ a b) (at level 50, left associativity).
 
 Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
-  match printer prog with tt => prog end.
+  let unused := printer prog in prog.
 
 (** We define three translation functions for whole programs: one
   starting with a C program, one with a Cminor program, one with an
@@ -149,6 +150,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef :=
    @@ print print_LTLin
    @@ Reload.transf_fundef
   @@@ Stacking.transf_fundef
+   @@ print print_Mach
   @@@ Asmgen.transf_fundef.
 
 (* Here is the translation of a CminorSel function to an Asm function. *)
@@ -316,7 +318,7 @@ Proof.
              Reloadtyping.program_typing_preserved
              Stackingtyping.program_typing_preserved; intros.
 
-  eapply Asmgenproof.transf_program_correct; eauto 6.
+  eapply Asmgenproof.transf_program_correct; eauto 8.
   eapply Stackingproof.transf_program_correct; eauto 6.
   eapply Reloadproof.transf_program_correct; eauto.
   eapply CleanupLabelsproof.transf_program_correct; eauto.
@@ -341,7 +343,6 @@ Proof.
   eapply transf_rtl_program_correct; eauto.
   eapply RTLgenproof.transf_program_correct; eauto.
   eapply Selectionproof.transf_program_correct; eauto.
-  rewrite print_identity. auto.
 Qed.
 
 Theorem transf_c_program_correct:
diff --git a/driver/Driver.ml b/driver/Driver.ml
index ee48ffc..87b1569 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -46,16 +46,18 @@ let print_error oc msg =
 (* From C to preprocessed C *)
 
 let preprocess ifile ofile =
+  let output =
+    if ofile = "-" then "" else sprintf "> %s" ofile in
   let cmd =
-    sprintf "%s -D__COMPCERT__ %s %s %s > %s"
+    sprintf "%s -D__COMPCERT__ %s %s %s %s"
       Configuration.prepro
       (if Configuration.need_stdlib_wrapper
        then sprintf "-I%s" !stdlib_path
        else "")
       (quote_options !prepro_options)
-      ifile ofile in
+      ifile output in
   if command cmd <> 0 then begin
-    safe_remove ofile;
+    if ofile <> "-" then safe_remove ofile;
     eprintf "Error during preprocessing.\n";
     exit 2
   end
@@ -103,6 +105,7 @@ let compile_c_file sourcename ifile ofile =
   set_dest PrintRTL.destination_constprop option_dconstprop ".constprop.rtl";
   set_dest PrintRTL.destination_cse option_dcse ".cse.rtl";
   set_dest PrintLTLin.destination option_dalloc ".alloc.ltl";
+  set_dest PrintMach.destination option_dmach ".mach";
   (* Convert to Asm *)
   let asm =
     match Compiler.transf_c_program csyntax with
@@ -152,7 +155,6 @@ let assemble ifile ofile =
     sprintf "%s -o %s %s"
       Configuration.asm ofile ifile in
   let retcode = command cmd in
-  if not !option_dasm then safe_remove ifile;
   if retcode <> 0 then begin
     safe_remove ofile;
     eprintf "Error during assembling.\n";
@@ -177,7 +179,7 @@ let linker exe_name files =
 let process_c_file sourcename =
   let prefixname = Filename.chop_suffix sourcename ".c" in
   if !option_E then begin
-    preprocess sourcename (prefixname ^ ".i")
+    preprocess sourcename "-"
   end else begin
     let preproname = Filename.temp_file "compcert" ".i" in
     preprocess sourcename preproname;
@@ -189,7 +191,8 @@ let process_c_file sourcename =
         then prefixname ^ ".s"
         else Filename.temp_file "compcert" ".s" in
       compile_c_file sourcename preproname asmname;
-      assemble asmname (prefixname ^ ".o")
+      assemble asmname (prefixname ^ ".o");
+      if not !option_dasm then safe_remove asmname
     end
   end;
   prefixname ^ ".o"
@@ -206,7 +209,27 @@ let process_cminor_file sourcename =
       then prefixname ^ ".s"
       else Filename.temp_file "compcert" ".s" in
     compile_cminor_file sourcename asmname;
-    assemble asmname (prefixname ^ ".o")
+    assemble asmname (prefixname ^ ".o");
+    if not !option_dasm then safe_remove asmname
+  end;
+  prefixname ^ ".o"
+
+(* Processing of .S and .s files *)
+
+let process_s_file sourcename =
+  let prefixname = Filename.chop_suffix sourcename ".s" in
+  assemble sourcename (prefixname ^ ".o");
+  prefixname ^ ".o"
+
+let process_S_file sourcename =
+  let prefixname = Filename.chop_suffix sourcename ".s" in
+  if !option_E then begin
+    preprocess sourcename "-"
+  end else begin
+    let preproname = Filename.temp_file "compcert" ".s" in
+    preprocess sourcename preproname;
+    assemble preproname (prefixname ^ ".o");
+    safe_remove preproname
   end;
   prefixname ^ ".o"
 
@@ -217,10 +240,12 @@ let usage_string =
 Recognized source files:
   .c             C source file
   .cm            Cminor source file
+  .s             Assembly file
+  .S             Assembly file, to be run through the preprocessor
   .o             Object file
   .a             Library file
 Processing options:
-  -E             Preprocess only, save result in <file>.i
+  -E             Preprocess only, send result to standard output
   -S             Compile to assembler only, save result in <file>.s
   -c             Compile to object file only (no linking), result in <file>.o
 Preprocessing options:
@@ -248,6 +273,7 @@ Tracing options:
   -dconstprop    Save RTL after constant propagation in <file>.constprop.rtl
   -dcse          Save RTL after CSE optimization in <file>.cse.rtl
   -dalloc        Save LTL after register allocation in <file>.alloc.ltl
+  -dmach         Save generated Mach code in <file>.mach
   -dasm          Save generated assembly in <file>.s
 Linking options:
   -l<lib>        Link library <lib>
@@ -332,6 +358,7 @@ let cmdline_actions =
   "-dconstprop$", Set option_dconstprop;
   "-dcse$", Set option_dcse;
   "-dalloc$", Set option_dalloc;
+  "-dmach$", Set option_dmach;
   "-dasm$", Set option_dasm;
   "-E$", Set option_E;
   "-S$", Set option_S;
@@ -343,6 +370,12 @@ let cmdline_actions =
   ".*\\.cm$", Self (fun s ->
       let objfile = process_cminor_file s in
       linker_options := objfile :: !linker_options);
+  ".*\\.s$", Self (fun s ->
+      let objfile = process_s_file s in
+      linker_options := objfile :: !linker_options);
+  ".*\\.S$", Self (fun s ->
+      let objfile = process_S_file s in
+      linker_options := objfile :: !linker_options);
   ".*\\.[oa]$", Self (fun s ->
       linker_options := s :: !linker_options);
   "-fsmall-data$", Integer(fun n -> option_small_data := n);