diff options
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Commandline.ml | 9 | ||||
-rw-r--r-- | driver/Commandline.mli | 2 | ||||
-rw-r--r-- | driver/Configuration.ml | 5 | ||||
-rw-r--r-- | driver/Configuration.mli | 3 | ||||
-rw-r--r-- | driver/Driver.ml | 78 | ||||
-rw-r--r-- | driver/Driveraux.ml | 16 |
6 files changed, 71 insertions, 42 deletions
diff --git a/driver/Commandline.ml b/driver/Commandline.ml index d125736a..c0dd6257 100644 --- a/driver/Commandline.ml +++ b/driver/Commandline.ml @@ -32,6 +32,8 @@ type action = | Self of (string -> unit) | String of (string -> unit) | Integer of (int -> unit) + | Ignore + | Unit of (unit -> unit) let match_pattern text = function | Exact s -> @@ -96,6 +98,13 @@ let parse_array spec argv first last = end else begin eprintf "Option `%s' expects an argument\n" s; exit 2 end + | Some (Ignore) -> + if i + 1 <= last then begin + parse (i+2) + end else begin + eprintf "Option `%s' expects an argument\n" s; exit 2 + end + | Some (Unit f) -> f (); parse (i+1) end in parse first diff --git a/driver/Commandline.mli b/driver/Commandline.mli index 79786678..197d0b04 100644 --- a/driver/Commandline.mli +++ b/driver/Commandline.mli @@ -33,6 +33,8 @@ type action = | Self of (string -> unit) (** call the function with the matched string *) | String of (string -> unit) (** read next arg as a string, call function *) | Integer of (int -> unit) (** read next arg as an int, call function *) + | Ignore (** ignore the next arg *) + | Unit of (unit -> unit) (** call the function with unit as argument *) val parse_cmdline: (pattern * action) list -> unit diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 0a2b3eec..87e29e0f 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -121,6 +121,11 @@ let arch = | v -> bad_config "arch" [v] let model = get_config_string "model" let abi = get_config_string "abi" +let is_big_endian = + match get_config_string "endianness" with + | "big" -> true + | "little" -> false + | v -> bad_config "endianness" [v] let system = get_config_string "system" let has_runtime_lib = match get_config_string "has_runtime_lib" with diff --git a/driver/Configuration.mli b/driver/Configuration.mli index 7087c3c2..197e8ad2 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -19,6 +19,9 @@ val model: string val abi: string (** ABI to use *) +val is_big_endian: bool + (** Endianness to use *) + val system: string (** Flavor of operating system that runs CompCert *) diff --git a/driver/Driver.ml b/driver/Driver.ml index eccd233c..b89d93c1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -23,6 +23,7 @@ let dump_options = ref false (* Optional sdump suffix *) let sdump_suffix = ref ".json" +let sdump_folder = ref "" (* Dump Asm code in asm format for the validator *) @@ -59,8 +60,11 @@ let compile_c_ast sourcename csyntax ofile = eprintf "%s: %a" sourcename print_error msg; exit 2 in (* Dump Asm in binary and JSON format *) - if !option_sdump then - dump_jasm asm sourcename (output_filename sourcename ".c" !sdump_suffix); + if !option_sdump then begin + let sf = output_filename sourcename ".c" !sdump_suffix in + let csf = Filename.concat !sdump_folder sf in + dump_jasm asm sourcename csf + end; (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm; @@ -341,18 +345,19 @@ General options:\n\ \ -v Print external commands before invoking them\n\ \ -timings Show the time spent in various compiler passes\n\ \ -version Print the version string and exit\n\ -\ @<file> Read command line options from <file>\n\ -Interpreter mode:\n\ +\ @<file> Read command line options from <file>\n" ^ + Cerrors.warning_help ^ +"Interpreter mode:\n\ \ -interp Execute given .c files using the reference interpreter\n\ \ -quiet Suppress diagnostic messages for the interpreter\n\ \ -trace Have the interpreter produce a detailed trace of reductions\n\ \ -random Randomize execution order\n\ \ -all Simulate all possible execution orders\n" -let print_usage_and_exit _ = +let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let print_version_and_exit _ = +let print_version_and_exit () = printf "%s" version_string; exit 0 let language_support_options = [ @@ -365,8 +370,8 @@ let optimization_options = [ option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy ] -let set_all opts = List.iter (fun r -> r := true) opts -let unset_all opts = List.iter (fun r -> r := false) opts +let set_all opts () = List.iter (fun r -> r := true) opts +let unset_all opts () = List.iter (fun r -> r := false) opts let num_source_files = ref 0 @@ -375,13 +380,16 @@ let num_input_files = ref 0 let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in + let dwarf_version version () = + option_g:=true; + option_gdwarf := version in [ (* Getting help *) - Exact "-help", Self print_usage_and_exit; - Exact "--help", Self print_usage_and_exit; + Exact "-help", Unit print_usage_and_exit; + Exact "--help", Unit print_usage_and_exit; (* Getting version info *) - Exact "-version", Self print_version_and_exit; - Exact "--version", Self print_version_and_exit; + Exact "-version", Unit print_version_and_exit; + Exact "--version", Unit print_version_and_exit; (* Processing options *) Exact "-c", Set option_c; Exact "-E", Set option_E; @@ -392,17 +400,15 @@ let cmdline_actions = (* Preprocessing options *) @ prepro_actions @ (* Language support options -- more below *) - [ Exact "-fall", Self (fun _ -> set_all language_support_options); - Exact "-fnone", Self (fun _ -> unset_all language_support_options); + [ Exact "-fall", Unit (set_all language_support_options); + Exact "-fnone", Unit (unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true; - option_gdwarf := 3);] @ + Exact "-g", Unit (dwarf_version 3);] @ (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 []) @ - [ Exact "-frename-static", Self (fun s -> option_rename_static:= true); + [ Exact "-gdwarf-2", Unit (dwarf_version 2); + Exact "-gdwarf-3", Unit (dwarf_version 3);] + else []) @ + [ Exact "-frename-static", Set option_rename_static; Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin option_g := false end else begin @@ -410,9 +416,9 @@ let cmdline_actions = option_gdepth := if n > 3 then 3 else n end); (* Code generation options -- more below *) - Exact "-O0", Self (fun _ -> unset_all optimization_options); - Exact "-O", Self (fun _ -> set_all optimization_options); - _Regexp "-O[123]$", Self (fun _ -> set_all optimization_options); + Exact "-O0", Unit (unset_all optimization_options); + Exact "-O", Unit (set_all optimization_options); + _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); @@ -421,8 +427,8 @@ let cmdline_actions = Exact "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n); Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); (* Target processor options *) - Exact "-conf", String (fun _ -> ()); (* Ignore option since it is already handled *) - Exact "-target", String (fun _ -> ());] @ (* Ignore option since it is already handled *) + Exact "-conf", Ignore; (* Ignore option since it is already handled *) + Exact "-target", Ignore;] @ (* Ignore option since it is already handled *) (if Configuration.arch = "arm" then [ Exact "-mthumb", Set option_mthumb; Exact "-marm", Unset option_mthumb; ] @@ -455,18 +461,20 @@ let cmdline_actions = dump_options:=true); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); + Exact "-sdump-folder", String (fun s -> sdump_folder := s); Exact "-doptions", Set dump_options; (* General options *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); - Exact "-timings", Set option_timings; - Exact "-Werror", Set Cerrors.warn_error; + Exact "-timings", Set option_timings;] @ +(* Diagnostic options *) + Cerrors.warning_options @ (* Interpreter mode *) - Exact "-interp", Set option_interp; - Exact "-quiet", Self (fun _ -> Interp.trace := 0); - Exact "-trace", Self (fun _ -> Interp.trace := 2); - Exact "-random", Self (fun _ -> Interp.mode := Interp.Random); - Exact "-all", Self (fun _ -> Interp.mode := Interp.All) + [ Exact "-interp", Set option_interp; + Exact "-quiet", Unit (fun () -> Interp.trace := 0); + Exact "-trace", Unit (fun () -> Interp.trace := 2); + Exact "-random", Unit (fun () -> Interp.mode := Interp.Random); + Exact "-all", Unit (fun () -> Interp.mode := Interp.All) ] (* -f options: come in -f and -fno- variants *) (* Language support options *) @@ -525,7 +533,9 @@ let _ = | "powerpc" -> if Configuration.system = "linux" then Machine.ppc_32_bigendian else Machine.ppc_32_diab_bigendian - | "arm" -> Machine.arm_littleendian + | "arm" -> if Configuration.is_big_endian + then Machine.arm_bigendian + else Machine.arm_littleendian | "ia32" -> if Configuration.abi = "macosx" then Machine.x86_32_macosx else Machine.x86_32 diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index 33cd9215..d25301d2 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -28,14 +28,6 @@ let rec waitpid_no_intr pid = with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid let command stdout args = - if !option_v then begin - eprintf "+ %s" (String.concat " " args); - begin match stdout with - | None -> () - | Some f -> eprintf " > %s" f - end; - prerr_endline "" - end; let argv = Array.of_list args in assert (Array.length argv > 0); try @@ -59,6 +51,14 @@ let command stdout args = -1 let command ?stdout args = + if !option_v then begin + eprintf "+ %s" (String.concat " " args); + begin match stdout with + | None -> () + | Some f -> eprintf " > %s" f + end; + prerr_endline "" + end; let resp = Sys.win32 && Configuration.response_file_style <> Configuration.Unsupported in if resp && List.fold_left (fun len arg -> len + String.length arg + 1) 0 args > 7000 then let quote,prefix = match Configuration.response_file_style with |