From 438d541dbe5fe7d7fe6b7aacaa6e6ef070c2e237 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 16 Apr 2020 20:23:35 +0200 Subject: Move reserved_registers to CPragmas. The list of reserved_registers is never reset between the compilation of multiple files. Instead of storing them in IRC they are moved in the CPragmas file and reset in the a new reset function for Cpragmas whic is called per file. --- driver/Frontend.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'driver') diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 74791247..bb97e945 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 *) -- cgit From 4a676623badb718da4055b7f26ee05f5097f4e7b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 4 May 2020 11:11:27 +0200 Subject: Move Commandline to the lib/ directory The Commandline module is reusable in other projects, and its license (GPL) allows such reuse, so its natural place is in lib/ rather than in driver/ --- driver/Commandline.ml | 141 ------------------------------------------------- driver/Commandline.mli | 55 ------------------- 2 files changed, 196 deletions(-) delete mode 100644 driver/Commandline.ml delete mode 100644 driver/Commandline.mli (limited to 'driver') 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=] and calls [fn] with the integer argument -*) - -val argv: string array -(** [argv] contains the complete command line after @-file expandsion *) -- cgit From fdaa2a3e7269ab5fc6fade4ac56699ad21de1bda Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 1 Jul 2020 19:33:12 +0200 Subject: Add option to print version information in file --- driver/CommonOptions.ml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index c151ecf2..fc7bbb77 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -24,9 +24,24 @@ let version_string tool_name = let print_version_and_exit tool_name () = Printf.printf "%s" (version_string tool_name); exit 0 +let version_file_string tool_name = + if Version.buildnr <> "" && Version.tag <> "" then + Printf.sprintf "This is CompCert %s,\nVersion: %s,\nBuild: %s,\nTag: %s\n" tool_name Version.version Version.buildnr Version.tag + else + Printf.sprintf "The CompCert %s,\nversion %s\n" tool_name Version.version + +let print_version_file_and_exit tool_name file = + let oc = open_out_bin file in + output_string oc (version_file_string tool_name); + close_out_noerr oc; + exit 0 + 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); + Exact "-version-file", String (print_version_file_and_exit tool_name); + Exact "--version-file", String (print_version_file_and_exit tool_name); + ] (* Language support options *) @@ -76,6 +91,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 Print version inforation to and exit -target Generate code for the given target -conf Read configuration from file @ Read command line options from -- cgit From f8cfbc1bc22c06835e9ea7b0cab41a8f25b523ba Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 2 Jul 2020 14:52:34 +0200 Subject: Introduce additional "branch" build information. --- driver/CommonOptions.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index fc7bbb77..a2f249c1 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,8 @@ let print_version_and_exit tool_name () = let version_file_string tool_name = if Version.buildnr <> "" && Version.tag <> "" then - Printf.sprintf "This is CompCert %s,\nVersion: %s,\nBuild: %s,\nTag: %s\n" tool_name Version.version Version.buildnr Version.tag + Printf.sprintf "This is CompCert %s,\nVersion: %s,\nBuild: %s,\nTag: %s,\nBranch: %s\n" + tool_name Version.version Version.buildnr Version.tag Version.branch else Printf.sprintf "The CompCert %s,\nversion %s\n" tool_name Version.version -- cgit From ae7eeb880d35fb12b4620e5320a8f9677a72d159 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 2 Jul 2020 15:30:58 +0200 Subject: Remove no longer needed option enforce-buildnr --- driver/Driver.ml | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index be1252f9..66cfeaa7 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -238,12 +238,6 @@ Code generation options: (use -fno- to turn off -f) 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 @@ -279,10 +273,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; -- cgit From 1a01ad629109cdb60fddae3787e3a589d20e9790 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 7 Jul 2020 18:36:31 +0200 Subject: Use the same version string. The version string dumped in the file should be the same as the version string printed by `-version`. The option is also not printed by `-help` since it is for internal use only. --- driver/CommonOptions.ml | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) (limited to 'driver') diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index a2f249c1..e0e75e58 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -16,7 +16,7 @@ open Commandline (* The version string for [tool_name] *) let version_string tool_name = if Version.buildnr <> "" && Version.tag <> "" && Version.branch <> "" then - Printf.sprintf "The CompCert %s, Release: %s, Build: %s, Tag: %s, Branch %s\n" + Printf.sprintf "The CompCert %s\nVersion: %s\nBuild: %s\nTag: %s\nBranch: %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 @@ -25,16 +25,10 @@ let version_string tool_name = let print_version_and_exit tool_name () = Printf.printf "%s" (version_string tool_name); exit 0 -let version_file_string tool_name = - if Version.buildnr <> "" && Version.tag <> "" then - Printf.sprintf "This is CompCert %s,\nVersion: %s,\nBuild: %s,\nTag: %s,\nBranch: %s\n" - tool_name Version.version Version.buildnr Version.tag Version.branch - else - Printf.sprintf "The CompCert %s,\nversion %s\n" tool_name Version.version - +(* Print the version string to a file and exit the program *) let print_version_file_and_exit tool_name file = let oc = open_out_bin file in - output_string oc (version_file_string tool_name); + output_string oc (version_string tool_name); close_out_noerr oc; exit 0 @@ -93,7 +87,6 @@ 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 Print version inforation to and exit -target Generate code for the given target -conf Read configuration from file @ Read command line options from -- cgit From 430263226793599834da40a39b2f82565338bd70 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 8 Jul 2020 16:51:22 +0200 Subject: Revert "Use the same version string." This reverts commit 1a01ad629109cdb60fddae3787e3a589d20e9790. --- driver/CommonOptions.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'driver') diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index e0e75e58..a2f249c1 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -16,7 +16,7 @@ open Commandline (* The version string for [tool_name] *) let version_string tool_name = if Version.buildnr <> "" && Version.tag <> "" && Version.branch <> "" then - Printf.sprintf "The CompCert %s\nVersion: %s\nBuild: %s\nTag: %s\nBranch: %s\n" + 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 @@ -25,10 +25,16 @@ let version_string tool_name = let print_version_and_exit tool_name () = Printf.printf "%s" (version_string tool_name); exit 0 -(* Print the version string to a file and exit the program *) +let version_file_string tool_name = + if Version.buildnr <> "" && Version.tag <> "" then + Printf.sprintf "This is CompCert %s,\nVersion: %s,\nBuild: %s,\nTag: %s,\nBranch: %s\n" + tool_name Version.version Version.buildnr Version.tag Version.branch + else + Printf.sprintf "The CompCert %s,\nversion %s\n" tool_name Version.version + let print_version_file_and_exit tool_name file = let oc = open_out_bin file in - output_string oc (version_string tool_name); + output_string oc (version_file_string tool_name); close_out_noerr oc; exit 0 @@ -87,6 +93,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 Print version inforation to and exit -target Generate code for the given target -conf Read configuration from file @ Read command line options from -- cgit From a00de29bc143e758ed034018c3c528e873b9b3da Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 8 Jul 2020 17:58:51 +0200 Subject: Fix typo. --- driver/CommonOptions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index a2f249c1..839bad1b 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -16,7 +16,7 @@ open Commandline (* The version string for [tool_name] *) let version_string tool_name = if Version.buildnr <> "" && Version.tag <> "" && Version.branch <> "" then - Printf.sprintf "The CompCert %s, Release: %s, Build: %s, Tag: %s, Branch %s\n" + 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 -- cgit From 72be849e2a9bbe7e8a8438bf561c5a677a35c9e0 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 9 Jul 2020 10:55:44 +0200 Subject: No trailing commas for --version-file option. --- driver/CommonOptions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index 839bad1b..5993c68d 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -27,7 +27,7 @@ let print_version_and_exit tool_name () = let version_file_string tool_name = if Version.buildnr <> "" && Version.tag <> "" then - Printf.sprintf "This is CompCert %s,\nVersion: %s,\nBuild: %s,\nTag: %s,\nBranch: %s\n" + Printf.sprintf "This is CompCert %s\nVersion: %s\nBuild: %s\nTag: %s\nBranch: %s\n" tool_name Version.version Version.buildnr Version.tag Version.branch else Printf.sprintf "The CompCert %s,\nversion %s\n" tool_name Version.version -- cgit From 6903cff15e6a66982513f5fe1511ed70eb781cbd Mon Sep 17 00:00:00 2001 From: Christoph Cullmann Date: Thu, 30 Jul 2020 09:59:14 +0200 Subject: Add missing comment for print_version_file_and_exit --- driver/CommonOptions.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'driver') diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index 5993c68d..cbc04a44 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -32,6 +32,7 @@ let version_file_string tool_name = else Printf.sprintf "The CompCert %s,\nversion %s\n" tool_name Version.version +(* Print the version string to a file and exit the program *) let print_version_file_and_exit tool_name file = let oc = open_out_bin file in output_string oc (version_file_string tool_name); -- cgit From 600803caeeaeae889f0b3020423402bf542f022b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 12 Oct 2020 16:34:56 +0200 Subject: Remove -version-file option It is specific to AbsInt's commercial version of CompCert. --- driver/CommonOptions.ml | 21 ++------------------- 1 file changed, 2 insertions(+), 19 deletions(-) (limited to 'driver') diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml index cbc04a44..e8a6941c 100644 --- a/driver/CommonOptions.ml +++ b/driver/CommonOptions.ml @@ -25,26 +25,9 @@ let version_string tool_name = let print_version_and_exit tool_name () = Printf.printf "%s" (version_string tool_name); exit 0 -let version_file_string tool_name = - if Version.buildnr <> "" && Version.tag <> "" then - Printf.sprintf "This is CompCert %s\nVersion: %s\nBuild: %s\nTag: %s\nBranch: %s\n" - tool_name Version.version Version.buildnr Version.tag Version.branch - else - Printf.sprintf "The CompCert %s,\nversion %s\n" tool_name Version.version - -(* Print the version string to a file and exit the program *) -let print_version_file_and_exit tool_name file = - let oc = open_out_bin file in - output_string oc (version_file_string tool_name); - close_out_noerr oc; - exit 0 - 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-file", String (print_version_file_and_exit tool_name); - Exact "--version-file", String (print_version_file_and_exit tool_name); - ] + Exact "--version", Unit (print_version_and_exit tool_name) ] (* Language support options *) @@ -105,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 ] -- cgit From b1b853a2e9f7f2143fedd58772a702bc9c6a8ba1 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 30 Oct 2020 18:32:04 +0100 Subject: Add -main option to specify entrypoint function in interpreter mode (#374) When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function. This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option. The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0. --- driver/Clflags.ml | 1 + driver/Driver.ml | 4 +++- driver/Interp.ml | 55 +++++++++++++++++++++++++++++++++++++------------------ 3 files changed, 41 insertions(+), 19 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2db9399f..80883372 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -67,3 +67,4 @@ let option_small_const = ref (!option_small_data) let option_timings = ref false let stdlib_path = ref Configuration.stdlib_path let use_standard_headers = ref Configuration.has_standard_headers +let main_function_name = ref "main" diff --git a/driver/Driver.ml b/driver/Driver.ml index 66cfeaa7..043e43c1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -233,6 +233,7 @@ Code generation options: (use -fno- to turn off -f) -trace Have the interpreter produce a detailed trace of reductions -random Randomize execution order -all Simulate all possible execution orders + -main Start executing at function instead of main() |} let print_usage_and_exit () = @@ -355,7 +356,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 *) 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 *) -- cgit From b40aef6c55b837786cd749260e8e8d8a1d328034 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Dec 2020 17:52:51 +0100 Subject: Error when using -main without -interp Outside of -interp mode, -main has no (known) effect but could be confused for a linker option that sets the program's entrypoint, say. It's safer to reject the option. --- driver/Driver.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 043e43c1..2b34d538 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -412,6 +412,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 -- cgit