Moved assembler and linker into own files.

The function to call the assembler and the linker are now in own
files like the preprocessor.
Bug 19197

9 files changed, 210 insertions, 122 deletions

diff --git a/driver/Assembler.ml b/driver/Assembler.ml
new file mode 100644
index 00000000..52fb17d8
--- /dev/null
+++ b/driver/Assembler.ml
@@ -0,0 +1,47 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*      Bernhard Schommer, AbsInt Angewandte Informatik GmbH           *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Clflags
+open Commandline
+open Driveraux
+
+(* From asm to object file *)
+
+let assemble ifile ofile =
+  let cmd = List.concat [
+    Configuration.asm;
+    ["-o"; ofile];
+    List.rev !assembler_options;
+    [ifile]
+  ] in
+  let exc = command cmd in
+  if exc <> 0 then begin
+    safe_remove ofile;
+    command_error "assembler" exc;
+    exit 2
+  end
+
+let assembler_actions =
+ [ Prefix "-Wa,", Self (fun s -> if gnu_system then
+    assembler_options := s :: !assembler_options
+  else
+    assembler_options := List.rev_append (explode_comma_option s) !assembler_options);
+  Exact "-Xassembler", String (fun s -> if gnu_system then
+    assembler_options := s::"-Xassembler":: !assembler_options
+  else
+    assembler_options := s::!assembler_options );]
+
+let assembler_help =
+"Assembling options:\n\
+\  -Wa,<opt>      Pass option <opt> to the assembler\n\
+\  -Xassembler <opt> Pass <opt> as an option to the assembler\n"
diff --git a/driver/Assembler.mli b/driver/Assembler.mli
new file mode 100644
index 00000000..d8a4e32b
--- /dev/null
+++ b/driver/Assembler.mli
@@ -0,0 +1,21 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*      Bernhard Schommer, AbsInt Angewandte Informatik GmbH           *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+val assemble: string -> string -> unit
+  (** From asm to object file *)
+
+val assembler_actions: (Commandline.pattern * Commandline.action) list
+  (** Commandline optins affecting the assembler *)
+
+val assembler_help: string
+  (** Commandline help description *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 5a7bd929..3e327437 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -16,6 +16,8 @@ open Clflags
 open Timing
 open Driveraux
 open Frontend
+open Assembler
+open Linker
 
 let dump_options = ref false
 
@@ -108,40 +110,6 @@ let compile_cminor_file ifile ofile =
                  ifile msg;
          exit 2
 
-(* From asm to object file *)
-
-let assemble ifile ofile =
-  let cmd = List.concat [
-    Configuration.asm;
-    ["-o"; ofile];
-    List.rev !assembler_options;
-    [ifile]
-  ] in
-  let exc = command cmd in
-  if exc <> 0 then begin
-    safe_remove ofile;
-    command_error "assembler" exc;
-    exit 2
-  end
-
-(* Linking *)
-
-let linker exe_name files =
-  let cmd = List.concat [
-    Configuration.linker;
-    ["-o"; exe_name];
-    files;
-    (if Configuration.has_runtime_lib
-     then ["-L" ^ !stdlib_path; "-lcompcert"]
-     else [])
-  ] in
-  let exc = command cmd in
-  if exc <> 0 then begin
-    command_error "linker" exc;
-    exit 2
-  end
-
-
 (* Processing of a .c file *)
 
 let process_c_file sourcename =
@@ -271,22 +239,6 @@ let process_h_file sourcename =
     exit 2
   end
 
-(* Record actions to be performed after parsing the command line *)
-
-let actions : ((string -> string) * string) list ref = ref []
-
-let push_action fn arg =
-  actions := (fn, arg) :: !actions
-
-let push_linker_arg arg =
-  push_action (fun s -> s) arg
-
-let perform_actions () =
-  let rec perform = function
-  | [] -> []
-  | (fn, arg) :: rem -> let res = fn arg in res :: perform rem
-  in perform (List.rev !actions)
-
 let version_string =
   if Version.buildnr <> "" && Version.tag <> "" then
     sprintf "The CompCert C verified compiler, %s, Build: %s, Tag: %s\n" Version.version Version.buildnr Version.tag
@@ -314,30 +266,6 @@ let target_help = if Configuration.arch = "arm" then
 else
   ""
 
-let gnu_linker_help =
-"  -nostartfiles  Do not use the standard system startup files when\n\
-\                 linking\n\
-\  -nodefaultlibs Do not use the standard system libraries when\n\
-\                 linking\n\
-\  -nostdlib      Do not use the standard system startup files or\n\
-\                 libraries when linking\n"
-
-let linker_help =
-"Linking options:\n\
-\  -l<lib>        Link library <lib>\n\
-\  -L<dir>        Add <dir> to search path for libraries\n" ^
- (if gnu_system then gnu_linker_help else "") ^
-"  -s             Remove all symbol table and relocation information from the\n\
-\                 executable\n\
-\  -static        Prevent linking with the shared libraries\n\
-\  -T <file>      Use <file> as linker command file\n\
-\  -Wl,<opt>      Pass option <opt> to the linker\n\
-\  -WUl,<opt>     Pass option <opt> to the gcc or dcc used for linking\n\
-\  -Xlinker <opt> Pass <opt> as an option to the linker\n\
-\  -u <symb>      Pretend the symbol <symb> is undefined to force linking of\n\
-\                 library modules to define it.\n"
-
-
 let usage_string =
   version_string ^
   "Usage: ccomp [options] <source files>\n\
@@ -387,9 +315,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)\n\
 \  -falign-branch-targets <n>  Set alignment (in bytes) of branch targets\n\
 \  -falign-cond-branches <n>  Set alignment (in bytes) of conditional branches\n" ^
  target_help ^
-"Assembling options:\n\
-\  -Wa,<opt>      Pass option <opt> to the assembler\n\
-\  -Xassembler <opt> Pass <opt> as an option to the assembler\n" ^
+ assembler_help ^
  linker_help ^
 "Tracing options:\n\
 \  -dprepro       Save C file after preprocessing in <file>.i\n\
@@ -463,11 +389,11 @@ let cmdline_actions =
 (* Debugging options *)
   Exact "-g", Self (fun s -> option_g := true;
     option_gdwarf := 3);] @
-  if gnu_system then
+  (if gnu_system then
  [ Exact "-gdwarf-2", Self (fun s -> option_g:=true;
     option_gdwarf := 2);
   Exact "-gdwarf-3", Self (fun s -> option_g := true;
-    option_gdwarf := 3);] else [] @
+    option_gdwarf := 3);] else []) @
  [ Exact "-frename-static", Self (fun s -> option_rename_static:= true);
    Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin
      option_g := false
@@ -494,38 +420,11 @@ let cmdline_actions =
       Exact "-marm", Unset option_mthumb; ]
   else [] @
 (* Assembling options *)
- [ Prefix "-Wa,", Self (fun s -> if gnu_system then
-    assembler_options := s :: !assembler_options
-  else
-    assembler_options := List.rev_append (explode_comma_option s) !assembler_options);
-  Exact "-Xassembler", String (fun s -> if gnu_system then
-    assembler_options := s::"-Xassembler":: !assembler_options
-  else
-    assembler_options := s::!assembler_options );
+  assembler_actions @
 (* Linking options *)
-  Prefix "-l", Self push_linker_arg;
-  Prefix "-L", Self push_linker_arg; ] @
-  if gnu_system then
-    [ Exact "-nostartfiles", Self push_linker_arg;
-      Exact "-nodefaultlibs", Self push_linker_arg;
-      Exact "-nostdlib", Self push_linker_arg;]
-  else [] @
- [ Exact "-s", Self push_linker_arg;
-  Exact "-static", Self push_linker_arg;
-  Exact "-T", String (fun s -> if gnu_system then begin
-    push_linker_arg ("-T");
-    push_linker_arg(s)
-  end else
-    push_linker_arg ("-Wm"^s));
-  Exact "-Xlinker", String (fun s -> if Configuration.system = "diab" then
-    push_linker_arg ("-Wl,"^s)
-  else
-    push_linker_arg s);
-  Prefix "-Wl,", Self push_linker_arg;
-  Prefix "-WUl,", Self (fun s -> List.iter push_linker_arg (explode_comma_option s));
-  Exact "-u", Self push_linker_arg;
+  linker_actions @
 (* Tracing options *)
-  Exact "-dprepro", Set option_dprepro;
+ [ Exact "-dprepro", Set option_dprepro;
   Exact "-dparse", Set option_dparse;
   Exact "-dc", Set option_dcmedium;
   Exact "-dclight", Set option_dclight;
@@ -549,7 +448,7 @@ let cmdline_actions =
   Exact "-trace", Self (fun _ -> Interp.trace := 2);
   Exact "-random", Self (fun _ -> Interp.mode := Interp.Random);
   Exact "-all", Self (fun _ -> Interp.mode := Interp.All)
-  ]
+ ]
 (* -f options: come in -f and -fno- variants *)
 (* Language support options *)
   @ f_opt "longdouble" option_flongdouble
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index b5d155d4..3fe22fac 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -94,17 +94,26 @@ let print_error oc msg =
     List.iter print_one_error msg;
     output_char oc '\n'
 
-let gnu_option s =
-  if Configuration.system <> "diab" then
-    true
-  else begin
-    eprintf "ccomp: warning: option %s only supported for gcc backend\n" s;
-    false
-  end
-
+let gnu_system = Configuration.system <> "diab"
 
 (* Command-line parsing *)
 let explode_comma_option s =
   match Str.split (Str.regexp ",") s with
   | [] -> assert false
   | _ :: tl -> tl
+
+(* Record actions to be performed after parsing the command line *)
+
+let actions : ((string -> string) * string) list ref = ref []
+
+let push_action fn arg =
+  actions := (fn, arg) :: !actions
+
+let push_linker_arg arg =
+  push_action (fun s -> s) arg
+
+let perform_actions () =
+  let rec perform = function
+  | [] -> []
+  | (fn, arg) :: rem -> let res = fn arg in res :: perform rem
+  in perform (List.rev !actions)
diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli
index 1cb219a1..60efcc80 100644
--- a/driver/Driveraux.mli
+++ b/driver/Driveraux.mli
@@ -36,8 +36,17 @@ val ensure_inputfile_exists: string -> unit
 val print_error:out_channel -> Errors.errcode list -> unit
    (** Printing of error messages *)
 
-val gnu_option: string -> bool
-   (** Set the options for gnu systems *)
+val gnu_system: bool
+   (** Are the target tools gnu tools? *)
 
 val explode_comma_option: string -> string list
    (** Split option at commas *)
+
+val push_action: (string -> string) -> string -> unit
+  (** Add an action to be performed after parsing the command line *)
+
+val push_linker_arg: string -> unit
+  (** Add a linker arguments *)
+
+val perform_actions: unit -> string list
+  (** Perform actions *)
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 00387a05..043d4e5a 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -125,7 +125,7 @@ let prepro_actions = [
   Exact "-Xpreprocessor", String (fun s ->
     prepro_options := s :: !prepro_options);
   Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options);]
-  @ (if Configuration.system <> "diab" then gnu_prepro_actions else [])
+  @ (if gnu_system then gnu_prepro_actions else [])
 
 let gnu_prepro_help =
 "\  -M            Ouput a rule suitable for make describing the\n\
@@ -161,4 +161,4 @@ let prepro_help = "Preprocessing options:\n\
 \  -U<symb>       Undefine preprocessor symbol\n\
 \  -Wp,<opt>      Pass option <opt> to the preprocessor\n\
 \  -Xpreprocessor <opt> Pass option <opt> to the preprocessor\n"
-  ^ (if Configuration.system <> "diab" then gnu_prepro_help else "")
+  ^ (if gnu_system then gnu_prepro_help else "")
diff --git a/driver/Frontend.mli b/driver/Frontend.mli
index 689f382f..d0514d01 100644
--- a/driver/Frontend.mli
+++ b/driver/Frontend.mli
@@ -21,3 +21,4 @@ val prepro_actions: (Commandline.pattern * Commandline.action) list
   (** Commandline optins affecting the frontend *)
 
 val prepro_help: string
+  (** Commandline help description *)
diff --git a/driver/Linker.ml b/driver/Linker.ml
new file mode 100644
index 00000000..501a2ae3
--- /dev/null
+++ b/driver/Linker.ml
@@ -0,0 +1,81 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*      Bernhard Schommer, AbsInt Angewandte Informatik GmbH           *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Clflags
+open Commandline
+open Driveraux
+
+
+(* Linking *)
+
+let linker exe_name files =
+  let cmd = List.concat [
+    Configuration.linker;
+    ["-o"; exe_name];
+    files;
+    (if Configuration.has_runtime_lib
+     then ["-L" ^ !stdlib_path; "-lcompcert"]
+     else [])
+  ] in
+  let exc = command cmd in
+  if exc <> 0 then begin
+    command_error "linker" exc;
+    exit 2
+  end
+
+
+let gnu_linker_help =
+"  -nostartfiles  Do not use the standard system startup files when\n\
+\                 linking\n\
+\  -nodefaultlibs Do not use the standard system libraries when\n\
+\                 linking\n\
+\  -nostdlib      Do not use the standard system startup files or\n\
+\                 libraries when linking\n"
+
+let linker_help =
+"Linking options:\n\
+\  -l<lib>        Link library <lib>\n\
+\  -L<dir>        Add <dir> to search path for libraries\n" ^
+ (if gnu_system then gnu_linker_help else "") ^
+"  -s             Remove all symbol table and relocation information from the\n\
+\                 executable\n\
+\  -static        Prevent linking with the shared libraries\n\
+\  -T <file>      Use <file> as linker command file\n\
+\  -Wl,<opt>      Pass option <opt> to the linker\n\
+\  -WUl,<opt>     Pass option <opt> to the gcc or dcc used for linking\n\
+\  -Xlinker <opt> Pass <opt> as an option to the linker\n\
+\  -u <symb>      Pretend the symbol <symb> is undefined to force linking of\n\
+\                 library modules to define it.\n"
+
+let linker_actions =
+  [ Prefix "-l", Self push_linker_arg;
+    Prefix "-L", Self push_linker_arg; ] @
+  if gnu_system then
+    [ Exact "-nostartfiles", Self push_linker_arg;
+      Exact "-nodefaultlibs", Self push_linker_arg;
+      Exact "-nostdlib", Self push_linker_arg;]
+  else [] @
+    [ Exact "-s", Self push_linker_arg;
+      Exact "-static", Self push_linker_arg;
+      Exact "-T", String (fun s -> if gnu_system then begin
+        push_linker_arg ("-T");
+        push_linker_arg(s)
+      end else
+        push_linker_arg ("-Wm"^s));
+      Exact "-Xlinker", String (fun s -> if Configuration.system = "diab" then
+        push_linker_arg ("-Wl,"^s)
+      else
+        push_linker_arg s);
+      Prefix "-Wl,", Self push_linker_arg;
+      Prefix "-WUl,", Self (fun s -> List.iter push_linker_arg (explode_comma_option s));
+      Exact "-u", Self push_linker_arg;]
diff --git a/driver/Linker.mli b/driver/Linker.mli
new file mode 100644
index 00000000..3b92da05
--- /dev/null
+++ b/driver/Linker.mli
@@ -0,0 +1,21 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*      Bernhard Schommer, AbsInt Angewandte Informatik GmbH           *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+val linker: string -> string list -> unit
+  (** Link files into executbale *)
+
+val linker_actions: (Commandline.pattern * Commandline.action) list
+  (** Commandline optins affecting the assembler *)
+
+val linker_help: string
+  (** Commandline help description *)