From 410a5db3d48e84f2157c2c4f4bc29056c0e174b9 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 24 Jun 2016 13:57:27 +0200 Subject: 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 --- driver/Assembler.ml | 47 ++++++++++++++++++++ driver/Assembler.mli | 21 +++++++++ driver/Driver.ml | 119 ++++----------------------------------------------- driver/Driveraux.ml | 25 +++++++---- driver/Driveraux.mli | 13 +++++- driver/Frontend.ml | 4 +- driver/Frontend.mli | 1 + driver/Linker.ml | 81 +++++++++++++++++++++++++++++++++++ driver/Linker.mli | 21 +++++++++ 9 files changed, 210 insertions(+), 122 deletions(-) create mode 100644 driver/Assembler.ml create mode 100644 driver/Assembler.mli create mode 100644 driver/Linker.ml create mode 100644 driver/Linker.mli 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, Pass option to the assembler\n\ +\ -Xassembler Pass 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 Link library \n\ -\ -L Add 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 Use as linker command file\n\ -\ -Wl, Pass option to the linker\n\ -\ -WUl, Pass option to the gcc or dcc used for linking\n\ -\ -Xlinker Pass as an option to the linker\n\ -\ -u Pretend the symbol is undefined to force linking of\n\ -\ library modules to define it.\n" - - let usage_string = version_string ^ "Usage: ccomp [options] \n\ @@ -387,9 +315,7 @@ Code generation options: (use -fno- to turn off -f)\n\ \ -falign-branch-targets Set alignment (in bytes) of branch targets\n\ \ -falign-cond-branches Set alignment (in bytes) of conditional branches\n" ^ target_help ^ -"Assembling options:\n\ -\ -Wa, Pass option to the assembler\n\ -\ -Xassembler Pass as an option to the assembler\n" ^ + assembler_help ^ linker_help ^ "Tracing options:\n\ \ -dprepro Save C file after preprocessing in .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 Undefine preprocessor symbol\n\ \ -Wp, Pass option to the preprocessor\n\ \ -Xpreprocessor Pass option 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 Link library \n\ +\ -L Add 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 Use as linker command file\n\ +\ -Wl, Pass option to the linker\n\ +\ -WUl, Pass option to the gcc or dcc used for linking\n\ +\ -Xlinker Pass as an option to the linker\n\ +\ -u Pretend the symbol 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 *) -- cgit