diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-12-17 10:22:15 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-12-17 10:22:15 +0100 |
commit | 471a8363c185e073fdfb8aefeb863b215870285d (patch) | |
tree | 511160c38944b6bea7c64359ca0e890d8c5c7bbf /driver | |
parent | a71ed69400fbd8f6533a32c117e7063f6b083049 (diff) | |
parent | a644da350c329d302150310a0995ccf1f72937e5 (diff) | |
download | compcert-kvx-471a8363c185e073fdfb8aefeb863b215870285d.tar.gz compcert-kvx-471a8363c185e073fdfb8aefeb863b215870285d.zip |
Merge branch 'kvx-work' into aarch64-peephole
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Clflags.ml | 1 | ||||
-rw-r--r-- | driver/Commandline.ml | 141 | ||||
-rw-r--r-- | driver/Commandline.mli | 55 | ||||
-rw-r--r-- | driver/CommonOptions.ml | 10 | ||||
-rw-r--r-- | driver/Driver.ml | 17 | ||||
-rw-r--r-- | driver/Frontend.ml | 1 | ||||
-rw-r--r-- | driver/Interp.ml | 55 |
7 files changed, 51 insertions, 229 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index b8b5ab05..60d532db 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -111,3 +111,4 @@ let option_inline_auto_threshold = ref 0 let option_profile_arcs = ref false let option_fbranch_probabilities = ref true let option_debug_compcert = ref 0 +let main_function_name = ref "main" diff --git a/driver/Commandline.ml b/driver/Commandline.ml deleted file mode 100644 index 672ed834..00000000 --- a/driver/Commandline.ml +++ /dev/null @@ -1,141 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Parsing of command-line flags and arguments *) - -open Printf - -type pattern = - | Exact of string - | Prefix of string - | Suffix of string - | Regexp of Str.regexp - -let _Regexp re = Regexp (Str.regexp re) - -type action = - | Set of bool ref - | Unset of bool ref - | Self of (string -> unit) - | String of (string -> unit) - | Integer of (int -> unit) - | Ignore - | Unit of (unit -> unit) - -exception CmdError of string - -let match_pattern text = function - | Exact s -> - text = s - | Prefix pref -> - let lpref = String.length pref and ltext = String.length text in - lpref < ltext && String.sub text 0 lpref = pref - (* strict prefix: no match if pref = text. See below. *) - | Suffix suff -> - let lsuff = String.length suff and ltext = String.length text in - lsuff < ltext && String.sub text (ltext - lsuff) lsuff = suff - (* strict suffix: no match if suff = text, so that e.g. ".c" - causes an error rather than being treated as a C source file. *) - | Regexp re -> - Str.string_match re text 0 - -let rec find_action text = function - | [] -> None - | (pat, act) :: rem -> - if match_pattern text pat then Some act else find_action text rem - -let parse_array spec argv first last = - (* Split the spec into Exact patterns (in a hashtable) and other patterns *) - let exact_cases = (Hashtbl.create 29 : (string, action) Hashtbl.t) in - let rec split_spec = function - | [] -> [] - | (Exact s, act) :: rem -> Hashtbl.add exact_cases s act; split_spec rem - | (pat, act) :: rem -> (pat, act) :: split_spec rem in - let inexact_cases = split_spec spec in - (* Parse the vector of arguments *) - let rec parse i = - if i <= last then begin - let s = argv.(i) in - let optact = - try Some (Hashtbl.find exact_cases s) - with Not_found -> find_action s inexact_cases in - match optact with - | None -> - let msg = sprintf "unknown argument `%s'" s in - raise (CmdError msg) - | Some(Set r) -> - r := true; parse (i+1) - | Some(Unset r) -> - r := false; parse (i+1) - | Some(Self fn) -> - fn s; parse (i+1) - | Some(String fn) -> - if i + 1 <= last then begin - fn argv.(i+1); parse (i+2) - end else begin - let msg = sprintf "option `%s' expects an argument" s in - raise (CmdError msg) - end - | Some(Integer fn) -> - if i + 1 <= last then begin - let n = - try - int_of_string argv.(i+1) - with Failure _ -> - let msg = sprintf "argument to option `%s' must be an integer" s in - raise (CmdError msg) - in - fn n; parse (i+2) - end else begin - let msg = sprintf "option `%s' expects an argument" s in - raise (CmdError msg) - end - | Some (Ignore) -> - if i + 1 <= last then begin - parse (i+2) - end else begin - let msg = sprintf "option `%s' expects an argument" s in - raise (CmdError msg) - end - | Some (Unit f) -> f (); parse (i+1) - end - in parse first - -let argv = - try - Responsefile.expandargv Sys.argv - with Responsefile.Error msg | Sys_error msg -> - eprintf "Error while processing the command line: %s\n" msg; - exit 2 - -let parse_cmdline spec = - parse_array spec argv 1 (Array.length argv - 1) - -let long_int_action key s = - let ls = String.length s - and lkey = String.length key in - assert (ls > lkey); - let s = String.sub s (lkey + 1) (ls - lkey - 1) in - try - int_of_string s - with Failure _ -> - let msg = sprintf "argument to option `%s' must be an integer" key in - raise (CmdError msg) - -let longopt_int key f = - let act s = - let n = long_int_action key s in - f n in - Prefix (key ^ "="),Self act diff --git a/driver/Commandline.mli b/driver/Commandline.mli deleted file mode 100644 index 8bb6f18f..00000000 --- a/driver/Commandline.mli +++ /dev/null @@ -1,55 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(* Parsing of command-line flags and arguments *) - -(* A command-line specification is a list of pairs (pattern, action). - Command-line words are matched against the patterns, and the - corresponding actions are invoked. *) - -type pattern = - | Exact of string (** exactly this string *) - | Prefix of string (** any string starting with this prefix *) - | Suffix of string (** any string ending with this suffix *) - | Regexp of Str.regexp (** any string matching this anchored regexp *) - -val _Regexp: string -> pattern (** text of an [Str] regexp *) - -type action = - | Set of bool ref (** set the given ref to true *) - | Unset of bool ref (** set the given ref to false *) - | 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 *) -(* Note on precedence: [Exact] patterns are tried first, then the other - patterns are tried in the order in which they appear in the list. *) - -exception CmdError of string -(** Raise by [parse_cmdline] when an error occurred *) - -val parse_cmdline: (pattern * action) list -> unit -(** [parse_cmdline actions] parses the command line (after @-file expansion) - and performs all [actions]. Raises [CmdError] if an error occurred. -*) - -val longopt_int: string -> (int -> unit) -> pattern * action -(** [longopt_int key fn] generates a pattern and an action for - options of the form [key=<n>] and calls [fn] with the integer argument -*) - -val argv: string array -(** [argv] contains the complete command line after @-file expandsion *) diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index c151ecf2..e8a6941c 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -15,8 +15,9 @@ open Commandline (* The version string for [tool_name] *) let version_string tool_name = - if Version.buildnr <> "" && Version.tag <> "" then - Printf.sprintf "The CompCert %s, Release: %s, Build: %s, Tag: %s\n" tool_name Version.version Version.buildnr Version.tag + if Version.buildnr <> "" && Version.tag <> "" && Version.branch <> "" then + Printf.sprintf "The CompCert %s, Release: %s, Build: %s, Tag: %s, Branch: %s\n" + tool_name Version.version Version.buildnr Version.tag Version.branch else Printf.sprintf "The CompCert %s, version %s\n" tool_name Version.version @@ -26,7 +27,7 @@ let print_version_and_exit tool_name () = let version_options tool_name = [ Exact "-version", Unit (print_version_and_exit tool_name); - Exact "--version", Unit (print_version_and_exit tool_name);] + Exact "--version", Unit (print_version_and_exit tool_name) ] (* Language support options *) @@ -76,6 +77,7 @@ let general_help = -v Print external commands before invoking them -timings Show the time spent in various compiler passes -version Print the version string and exit + -version-file <file> Print version inforation to <file> and exit -target <value> Generate code for the given target -conf <file> Read configuration from file @<file> Read command line options from <file> @@ -86,4 +88,4 @@ let general_options = Exact "-target", Ignore;(* Ignore option since it is already handled *) Exact "-v", Set option_v; Exact "-stdlib", String(fun s -> stdlib_path := s); - Exact "-timings", Set option_timings;] + Exact "-timings", Set option_timings ] diff --git a/driver/Driver.ml b/driver/Driver.ml index 8ceb3a25..089cd423 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -263,17 +263,12 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -trace Have the interpreter produce a detailed trace of reductions -random Randomize execution order -all Simulate all possible execution orders + -main <name> Start executing at function <name> instead of main() |} let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let enforce_buildnr nr = - let build = int_of_string Version.buildnr in - if nr != build then - fatal_error no_loc "Mismatching builds: This is CompCert build %d, but QSK requires build %d.\n\ -Please use matching builds of QSK and CompCert." build nr - let dump_mnemonics destfile = let oc = open_out_bin destfile in let pp = Format.formatter_of_out_channel oc in @@ -320,10 +315,7 @@ let cmdline_actions = @ version_options tool_name @ (* Enforcing CompCert build numbers for QSKs and mnemonics dump *) (if Version.buildnr <> "" then - [ Exact "-qsk-enforce-build", Integer enforce_buildnr; - Exact "--qsk-enforce-build", Integer enforce_buildnr; - Exact "-dump-mnemonics", String dump_mnemonics; - ] + [Exact "-dump-mnemonics", String dump_mnemonics;] else []) @ (* Processing options *) [ Exact "-c", Set option_c; @@ -409,7 +401,8 @@ let cmdline_actions = 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) + Exact "-all", Unit (fun () -> Interp.mode := Interp.All); + Exact "-main", String (fun s -> main_function_name := s) ] (* Optimization options *) (* -f options: come in -f and -fno- variants *) @@ -497,6 +490,8 @@ let _ = fatal_error no_loc "ambiguous '-o' option (multiple source files)"; if !num_input_files = 0 then fatal_error no_loc "no input file"; + if not !option_interp && !main_function_name <> "main" then + fatal_error no_loc "option '-main' requires option '-interp'"; let linker_args = time "Total compilation time" perform_actions () in if not (nolink ()) && linker_args <> [] then begin linker (output_filename_default "a.out") linker_args diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 5db0040f..c99da945 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -75,6 +75,7 @@ let preprocess ifile ofile = let parse_c_file sourcename ifile = Debug.init_compile_unit sourcename; Sections.initialize(); + CPragmas.reset(); (* Simplification options *) let simplifs = "b" (* blocks: mandatory *) diff --git a/driver/Interp.ml b/driver/Interp.ml index d4286779..6c83e819 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -587,41 +587,60 @@ let world_program prog = (* Massaging the program to get a suitable "main" function *) -let change_main_function p old_main old_main_ty = - let old_main = Evalof(Evar(old_main, old_main_ty), old_main_ty) in +let change_main_function p new_main_fn = + let new_main_id = intern_string "%main%" in + { p with + Ctypes.prog_main = new_main_id; + Ctypes.prog_defs = + (new_main_id, Gfun(Internal new_main_fn)) :: p.Ctypes.prog_defs } + +let call_main3_function main_id main_ty = + let main_var = Evalof(Evar(main_id, main_ty), main_ty) in let arg1 = Eval(Vint(coqint_of_camlint 0l), type_int32s) in let arg2 = arg1 in let body = - Sreturn(Some(Ecall(old_main, Econs(arg1, Econs(arg2, Enil)), type_int32s))) in - let new_main_fn = - { fn_return = type_int32s; fn_callconv = cc_default; - fn_params = []; fn_vars = []; fn_body = body } in - let new_main_id = intern_string "___main" in - { prog_main = new_main_id; - Ctypes.prog_defs = (new_main_id, Gfun(Ctypes.Internal new_main_fn)) :: p.Ctypes.prog_defs; - Ctypes.prog_public = p.Ctypes.prog_public; - prog_types = p.prog_types; - prog_comp_env = p.prog_comp_env } + Sreturn(Some(Ecall(main_var, Econs(arg1, Econs(arg2, Enil)), type_int32s))) + in + { fn_return = type_int32s; fn_callconv = cc_default; + fn_params = []; fn_vars = []; fn_body = body } + +let call_other_main_function main_id main_ty main_ty_res = + let main_var = Evalof(Evar(main_id, main_ty), main_ty) in + let body = + Ssequence(Sdo(Ecall(main_var, Enil, main_ty_res)), + Sreturn(Some(Eval(Vint(coqint_of_camlint 0l), type_int32s)))) in + { fn_return = type_int32s; fn_callconv = cc_default; + fn_params = []; fn_vars = []; fn_body = body } let rec find_main_function name = function | [] -> None - | (id, Gfun fd) :: gdl -> if id = name then Some fd else find_main_function name gdl - | (id, Gvar v) :: gdl -> find_main_function name gdl + | (id, Gfun fd) :: gdl -> + if id = name then Some fd else find_main_function name gdl + | (id, Gvar v) :: gdl -> + find_main_function name gdl let fixup_main p = match find_main_function p.Ctypes.prog_main p.Ctypes.prog_defs with | None -> - fprintf err_formatter "ERROR: no main() function@."; + fprintf err_formatter "ERROR: no entry function %s()@." + (extern_atom p.Ctypes.prog_main); None | Some main_fd -> match type_of_fundef main_fd with | Tfunction(Tnil, Ctypes.Tint(I32, Signed, _), _) -> Some p - | Tfunction(Tcons(Ctypes.Tint _, Tcons(Tpointer(Tpointer(Ctypes.Tint(I8,_,_),_),_), Tnil)), + | Tfunction(Tcons(Ctypes.Tint _, + Tcons(Tpointer(Tpointer(Ctypes.Tint(I8,_,_),_),_), Tnil)), Ctypes.Tint _, _) as ty -> - Some (change_main_function p p.Ctypes.prog_main ty) + Some (change_main_function p + (call_main3_function p.Ctypes.prog_main ty)) + | Tfunction(Tnil, ty_res, _) as ty -> + Some (change_main_function p + (call_other_main_function p.Ctypes.prog_main ty ty_res)) | _ -> - fprintf err_formatter "ERROR: wrong type for main() function@."; + fprintf err_formatter + "ERROR: wrong type for entry function %s()@." + (extern_atom p.Ctypes.prog_main); None (* Execution of a whole program *) |