aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
Diffstat (limited to 'driver')
-rw-r--r--driver/Commandline.ml9
-rw-r--r--driver/Commandline.mli2
-rw-r--r--driver/Configuration.ml5
-rw-r--r--driver/Configuration.mli3
-rw-r--r--driver/Driver.ml78
-rw-r--r--driver/Driveraux.ml16
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
generated by cgit (git 2.34.1) at 2024-07-01 13:58:32 +0000