Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles

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

2 files changed, 345 insertions, 166 deletions

diff --git a/caml/Driver.ml b/caml/Driver.ml
new file mode 100644
index 00000000..fcd7a57b
--- /dev/null
+++ b/caml/Driver.ml
@@ -0,0 +1,345 @@
+open Printf
+
+(* Location of the standard library *)
+
+let stdlib_path = ref(
+  try
+    Sys.getenv "COMPCERT_LIBRARY"
+  with Not_found ->
+    Configuration.stdlib_path)
+
+(* Command-line flags *)
+
+let prepro_options = ref ([]: string list)
+let linker_options = ref ([]: string list)
+let exe_name = ref "a.out"
+let option_flonglong = ref false
+let option_dclight = ref false
+let option_dasm = ref false
+let option_E = ref false
+let option_S = ref false
+let option_c = ref false
+let option_v = ref false
+
+let command cmd =
+  if !option_v then begin
+    prerr_string "+ "; prerr_string cmd; prerr_endline ""
+  end;
+  Sys.command cmd
+
+let quote_options opts =
+  String.concat " " (List.rev_map Filename.quote opts)
+
+let safe_remove file =
+  try Sys.remove file with Sys_error _ -> ()
+
+(* Printing of error messages *)
+
+let print_error oc msg =
+  let print_one_error = function
+  | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
+  | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
+  in Camlcoq.coqlist_iter print_one_error msg
+
+(* For the CIL -> Csyntax translator:
+
+  * The meaning of some type specifiers may depend on compiler options:
+      the size of an int or the default signedness of char, for instance.
+
+  * Those type conversions may be parameterized thanks to a functor.
+
+  * Remark: [None] means that the type specifier is not supported
+      (that is, an Unsupported exception will be raised if that type
+      specifier is encountered in the program).
+*)
+
+module TypeSpecifierTranslator = struct
+  
+  open Cil
+  open Csyntax
+    
+  (** Convert a Cil.ikind into an (intsize * signedness) option *)
+  let convertIkind = function
+    | IChar      -> Some (I8, Unsigned)
+    | ISChar     -> Some (I8, Signed)
+    | IUChar     -> Some (I8, Unsigned)
+    | IInt       -> Some (I32, Signed)
+    | IUInt      -> Some (I32, Unsigned)
+    | IShort     -> Some (I16, Signed)
+    | IUShort    -> Some (I16, Unsigned)
+    | ILong      -> Some (I32, Signed)
+    | IULong     -> Some (I32, Unsigned)
+    | ILongLong  -> if !option_flonglong then Some (I32, Signed) else None
+    | IULongLong -> if !option_flonglong then Some (I32, Unsigned) else None
+	
+  (** Convert a Cil.fkind into an floatsize option *)
+  let convertFkind = function
+    | FFloat      -> Some F32
+    | FDouble     -> Some F64
+    | FLongDouble -> if !option_flonglong then Some F64 else None
+	
+end
+
+module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator)
+
+(* From C to preprocessed C *)
+
+let preprocess ifile ofile =
+  let cmd =
+    sprintf "gcc -arch ppc -D__COMPCERT__ -I%s %s -E %s > %s"
+      !stdlib_path
+      (quote_options !prepro_options)
+      ifile ofile in
+  if command cmd <> 0 then begin
+    safe_remove ofile;
+    eprintf "Error during preprocessing.\n";
+    exit 2
+  end
+
+(* From preprocessed C to asm *)
+
+let compile_c_file sourcename ifile ofile =
+  (* Parsing and production of a CIL.file *)
+  let cil =
+    try
+      Frontc.parse ifile ()
+    with
+    | Frontc.ParseError msg ->
+        eprintf "Error during parsing: %s\n" msg;
+        exit 2
+    | Errormsg.Error ->
+        exit 2 in
+  (* Remove preprocessed file (always a temp file) *)
+  safe_remove ifile;
+  (* Restore original source file name *)
+  cil.Cil.fileName <- sourcename;
+  (* Cleanup in the CIL.file *)
+  Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil;
+  (* Conversion to Csyntax *)
+  let csyntax =
+    try
+      Cil2CsyntaxTranslator.convertFile cil
+    with
+    | Cil2CsyntaxTranslator.Unsupported msg ->
+        eprintf "%s\n" msg;
+        exit 2
+    | Cil2CsyntaxTranslator.Internal_error msg ->
+        eprintf "%s\nPlease report it.\n" msg;
+        exit 2 in
+  (* Save Csyntax if requested *)
+  if !option_dclight then begin
+    let targetname = Filename.chop_suffix sourcename ".c" in
+    let oc = open_out (targetname ^ ".light.c") in
+    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
+    close_out oc
+  end;
+  (* Convert to PPC *)
+  let ppc =
+    match Main.transf_c_program csyntax with
+    | Errors.OK x -> x
+    | Errors.Error msg ->
+        print_error stderr msg;
+        exit 2 in
+  (* Save PPC asm *)
+  let oc = open_out ofile in
+  PrintPPC.print_program oc ppc;
+  close_out oc
+
+(* From Cminor to asm *)
+
+let compile_cminor_file ifile ofile =
+  let ic = open_in ifile in
+  let lb = Lexing.from_channel ic in
+  try
+    match Main.transf_cminor_program
+            (CMtypecheck.type_program
+              (CMparser.prog CMlexer.token lb)) with
+    | Errors.Error msg ->
+        print_error stderr msg;
+        exit 2
+    | Errors.OK p ->
+        let oc = open_out ofile in
+        PrintPPC.print_program oc p;
+        close_out oc
+  with Parsing.Parse_error ->
+         eprintf "File %s, character %d: Syntax error\n"
+                 ifile (Lexing.lexeme_start lb);
+         exit 2
+     | CMlexer.Error msg ->  
+         eprintf "File %s, character %d: %s\n"
+                 ifile (Lexing.lexeme_start lb) msg;
+         exit 2
+     | CMtypecheck.Error msg ->
+         eprintf "File %s, type-checking error:\n%s"
+                 ifile msg;
+         exit 2
+
+(* From asm to object file *)
+
+let assemble ifile ofile =
+  let cmd =
+    sprintf "gcc -arch ppc -c -o %s %s"
+      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";
+    exit 2
+  end
+
+(* Linking *)
+
+let linker exe_name files =
+  let cmd =
+    sprintf "gcc -arch ppc -o %s %s -L%s -lcompcert"
+      (Filename.quote exe_name)
+      (quote_options files)
+      !stdlib_path in
+  if command cmd <> 0 then exit 2
+
+(* Processing of a .c file *)
+
+let process_c_file sourcename =
+  let prefixname = Filename.chop_suffix sourcename ".c" in
+  if !option_E then begin
+    preprocess sourcename (prefixname ^ ".i")
+  end else begin
+    let preproname = Filename.temp_file "compcert" ".i" in
+    preprocess sourcename preproname;
+    if !option_S then begin
+      compile_c_file sourcename preproname (prefixname ^ ".s")
+    end else begin
+      let asmname =
+        if !option_dasm
+        then prefixname ^ ".s"
+        else Filename.temp_file "compcert" ".s" in
+      compile_c_file sourcename preproname asmname;
+      assemble asmname (prefixname ^ ".o")
+    end
+  end;
+  prefixname ^ ".o"
+
+(* Processing of a .cm file *)
+
+let process_cminor_file sourcename =
+  let prefixname = Filename.chop_suffix sourcename ".cm" in
+  if !option_S then begin
+    compile_cminor_file sourcename (prefixname ^ ".s")
+  end else begin
+    let asmname =
+      if !option_dasm
+      then prefixname ^ ".s"
+      else Filename.temp_file "compcert" ".s" in
+    compile_cminor_file sourcename asmname;
+    assemble asmname (prefixname ^ ".o")
+  end;
+  prefixname ^ ".o"
+
+(* Command-line parsing *)
+
+let starts_with s1 s2 =
+  String.length s1 >= String.length s2 &&
+  String.sub s1 0 (String.length s2) = s2
+
+let usage_string =
+"ccomp [options] <source files>
+Recognized source files:
+  .c             C source file
+  .cm            Cminor source file
+  .o             Object file
+  .a             Library file
+Processing options:
+  -E             Preprocess only, save result in <file>.i
+  -S             Compile to assembler only, save result in <file>.s
+  -c             Compile to object file only (no linking), result in <file>.o
+Preprocessing options:
+  -I<dir>        Add <dir> to search path for #include files
+  -D<symb>=<val> Define preprocessor symbol
+  -U<symb>       Undefine preprocessor symbol
+Compilation options:
+  -flonglong     Treat 'long long' as 'long' and 'long double' as 'double'
+  -dclight       Save generated Clight in <file>.light.c
+  -dasm          Save generated assembly in <file>.s
+Linking options:
+  -l<lib>        Link library <lib>
+  -L<dir>        Add <dir> to search path for libraries
+  -o <file>      Generate executable in <file> (default: a.out)
+General options:
+  -stdlib <dir>  Set the path of the Compcert run-time library
+  -v             Print external commands before invoking them
+"
+
+let rec parse_cmdline i =
+  if i < Array.length Sys.argv then begin
+    let s = Sys.argv.(i) in
+    if starts_with s "-I" || starts_with s "-D" || starts_with s "-U"
+    then begin
+      prepro_options := s :: !prepro_options;
+      parse_cmdline (i + 1)
+    end else 
+    if starts_with s "-l" || starts_with s "-L" then begin
+      linker_options := s :: !linker_options;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-o" && i + 1 < Array.length Sys.argv then begin
+      exe_name := Sys.argv.(i + 1);
+      parse_cmdline (i + 2)
+    end else
+    if s = "-stdlib" && i + 1 < Array.length Sys.argv then begin
+      stdlib_path := Sys.argv.(i + 1);
+      parse_cmdline (i + 2)
+    end else
+    if s = "-flonglong" then begin
+      option_flonglong := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-dclight" then begin
+      option_dclight := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-dasm" then begin
+      option_dasm := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-E" then begin
+      option_E := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-S" then begin
+      option_S := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-c" then begin
+      option_c := true;
+      parse_cmdline (i + 1)
+    end else
+    if s = "-v" then begin
+      option_v := true;
+      parse_cmdline (i + 1)
+    end else
+    if Filename.check_suffix s ".c" then begin
+      let objfile = process_c_file s in
+      linker_options := objfile :: !linker_options;
+      parse_cmdline (i + 1)
+    end else
+    if Filename.check_suffix s ".cm" then begin
+      let objfile = process_cminor_file s in
+      linker_options := objfile :: !linker_options;
+      parse_cmdline (i + 1)
+    end else
+    if Filename.check_suffix s ".o" || Filename.check_suffix s ".a" then begin
+      linker_options := s :: !linker_options;
+      parse_cmdline (i + 1)
+    end else begin
+      eprintf "Unknown argument `%s'\n" s;
+      eprintf "Usage: %s" usage_string;
+      exit 2
+    end
+  end
+
+let _ =
+  parse_cmdline 1;
+  if not (!option_c || !option_S || !option_E) then begin
+    linker !exe_name !linker_options
+  end
diff --git a/caml/Main2.ml b/caml/Main2.ml
deleted file mode 100644
index e3399fb9..00000000
--- a/caml/Main2.ml
+++ /dev/null
@@ -1,166 +0,0 @@
-open Printf
-
-(* For the CIL -> Csyntax translator:
-
-  * The meaning of some type specifiers may depend on compiler options:
-      the size of an int or the default signedness of char, for instance.
-
-  * Those type conversions may be parameterized thanks to a functor.
-
-  * Remark: [None] means that the type specifier is not supported
-      (that is, an Unsupported exception will be raised if that type
-      specifier is encountered in the program).
-*)
-
-module TypeSpecifierTranslator = struct
-  
-  open Cil
-  open Csyntax
-    
-  (** Convert a Cil.ikind into an (intsize * signedness) option *)
-  let convertIkind = function
-    | IChar      -> Some (I8, Unsigned)
-    | ISChar     -> Some (I8, Signed)
-    | IUChar     -> Some (I8, Unsigned)
-    | IInt       -> Some (I32, Signed)
-    | IUInt      -> Some (I32, Unsigned)
-    | IShort     -> Some (I16, Signed)
-    | IUShort    -> Some (I16, Unsigned)
-    | ILong      -> Some (I32, Signed)
-    | IULong     -> Some (I32, Unsigned)
-    | ILongLong  -> (***Some (I32, Signed)***) None
-    | IULongLong -> (***Some (I32, Unsigned)***) None
-	
-  (** Convert a Cil.fkind into an floatsize option *)
-  let convertFkind = function
-    | FFloat      -> Some F32
-    | FDouble     -> Some F64
-    | FLongDouble -> (***Some F64***) None
-	
-end
-
-module Cil2CsyntaxTranslator = Cil2Csyntax.Make(TypeSpecifierTranslator)
-
-let prepro_options = ref []
-let save_csyntax = ref false
-
-let preprocess file =
-  let temp = Filename.temp_file "compcert" ".i" in
-  let cmd =
-    sprintf "gcc -arch ppc %s -D__COMPCERT__ -E %s > %s"
-      (String.concat " " (List.rev !prepro_options))
-      file
-      temp in
-  if Sys.command cmd = 0
-  then temp
-  else (eprintf "Error during preprocessing.\n"; exit 2)
-
-let process_c_file sourcename =
-  let targetname = Filename.chop_suffix sourcename ".c" in
-  (* Preprocessing with cpp *)
-  let preproname = preprocess sourcename in
-  (* Parsing and production of a CIL.file *)
-  let cil =
-    try
-      Frontc.parse preproname ()
-    with
-    | Frontc.ParseError msg ->
-        eprintf "Error during parsing: %s\n" msg;
-        exit 2
-    | Errormsg.Error ->
-        exit 2 in
-  Sys.remove preproname;
-  (* Restore source file name before preprocessing *)
-  cil.Cil.fileName <- sourcename;
-  (* Cleanup in the CIL.file *)
-  Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil;
-  (* Conversion to Csyntax *)
-  let csyntax =
-    try
-      Cil2CsyntaxTranslator.convertFile cil
-    with
-    | Cil2CsyntaxTranslator.Unsupported msg ->
-        eprintf "%s\n" msg;
-        exit 2
-    | Cil2CsyntaxTranslator.Internal_error msg ->
-        eprintf "%s\nPlease report it.\n" msg;
-        exit 2 in
-  (* Save Csyntax if requested *)
-  if !save_csyntax then begin
-    let oc = open_out (targetname ^ ".light.c") in
-    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
-    close_out oc
-  end;
-  (* Convert to PPC *)
-  let ppc =
-    match Main.transf_c_program csyntax with
-    | Errors.OK x -> x
-    | Errors.Error msg ->
-        eprintf "Error in translation Csyntax -> PPC\n";
-        exit 2 in
-  (* Save PPC asm *)
-  let oc = open_out (targetname ^ ".s") in
-  PrintPPC.print_program oc ppc;
-  close_out oc
-
-let process_cminor_file sourcename =
-  let targetname = Filename.chop_suffix sourcename ".cm" ^ ".s" in
-  let ic = open_in sourcename in
-  let lb = Lexing.from_channel ic in
-  try
-    match Main.transf_cminor_program
-            (CMtypecheck.type_program
-              (CMparser.prog CMlexer.token lb)) with
-    | Errors.Error msg ->
-        eprintf "Compiler failure\n";
-        exit 2
-    | Errors.OK p ->
-        let oc = open_out targetname in
-        PrintPPC.print_program oc p;
-        close_out oc
-  with Parsing.Parse_error ->
-         eprintf "File %s, character %d: Syntax error\n"
-                 sourcename (Lexing.lexeme_start lb);
-         exit 2
-     | CMlexer.Error msg ->  
-         eprintf "File %s, character %d: %s\n"
-                 sourcename (Lexing.lexeme_start lb) msg;
-         exit 2
-     | CMtypecheck.Error msg ->
-         eprintf "File %s, type-checking error:\n%s"
-                 sourcename msg;
-         exit 2
-
-(* Command-line parsing *)
-
-let starts_with s1 s2 =
-  String.length s1 >= String.length s2 &&
-  String.sub s1 0 (String.length s2) = s2
-
-let rec parse_cmdline i =
-  if i < Array.length Sys.argv then begin
-    let s = Sys.argv.(i) in
-    if s = "-dump-c" then begin
-      save_csyntax := true;
-      parse_cmdline (i + 1)
-    end else
-    if starts_with s "-I" || starts_with s "-D" || starts_with s "-U"
-    then begin
-      prepro_options := s :: !prepro_options;
-      parse_cmdline (i + 1)
-    end else 
-    if Filename.check_suffix s ".cm" then begin
-      process_cminor_file s;
-      parse_cmdline (i + 1)
-    end else
-    if Filename.check_suffix s ".c" then begin
-      process_c_file s;
-      parse_cmdline (i + 1)
-    end else begin
-      eprintf "Unknown argument `%s'\n" s;
-      exit 2
-    end
-  end
-
-let _ =
-  parse_cmdline 1