Integration du front-end CIL developpe par Thomas Moniot

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

1 files changed, 134 insertions, 10 deletions

diff --git a/caml/Main2.ml b/caml/Main2.ml
index 41815758..713af82b 100644
--- a/caml/Main2.ml
+++ b/caml/Main2.ml
@@ -1,5 +1,105 @@
 open Printf
-open Datatypes
+
+(* 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 %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 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 "Unsupported C feature: %s\n" msg;
+        exit 2
+    | Failure msg ->
+        eprintf "Error in translation CIL -> Csyntax:\n%s\n" msg;
+        exit 2 in
+  (* Save Csyntax if requested *)
+  if !save_csyntax then begin
+    let oc = open_out (targetname ^ ".csyntax") 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
+    | Datatypes.Some x -> x
+    | Datatypes.None ->
+        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
@@ -9,10 +109,10 @@ let process_cminor_file sourcename =
     match Main.transf_cminor_program
             (CMtypecheck.type_program
               (CMparser.prog CMlexer.token lb)) with
-    | None ->
+    | Datatypes.None ->
         eprintf "Compiler failure\n";
         exit 2
-    | Some p ->
+    | Datatypes.Some p ->
         let oc = open_out targetname in
         PrintPPC.print_program oc p;
         close_out oc
@@ -29,12 +129,36 @@ let process_cminor_file sourcename =
                  sourcename msg;
          exit 2
 
-let process_file filename =
-  if Filename.check_suffix filename ".cm" then
-    process_cminor_file filename
-  else
-    raise (Arg.Bad ("unknown file type " ^ filename))
+(* 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 = "-dcsyntax" 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 _ =
-  Arg.parse [] process_file
-    "Usage: ccomp <options> <files>\nOptions are:"
+  parse_cmdline 1