Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8

7 files changed, 49 insertions, 229 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index d1e7dd7f..989a7096 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -104,3 +104,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 d93578b6..07edf2d1 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -259,17 +259,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
@@ -316,10 +311,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;
@@ -405,7 +397,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/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 *)