Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into mppa-if-conversion

7 files changed, 62 insertions, 25 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 651d644e..00bbc4d5 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -29,10 +29,13 @@ let option_fcse = ref true
 let option_fredundancy = ref true
 let option_fpostpass = ref true
 let option_fpostpass_sched = ref "list"
+let option_fifconversion = ref true
+let option_ffavor_branchless = ref false
 let option_falignfunctions = ref (None: int option)
 let option_falignbranchtargets = ref 0
 let option_faligncondbranchs = ref 0
 let option_finline_asm = ref false
+let option_fcommon = ref true
 let option_mthumb = ref (Configuration.model = "armv7m")
 let option_Osize = ref false
 let option_finline = ref true
diff --git a/driver/Commandline.ml b/driver/Commandline.ml
index 75ca1683..672ed834 100644
--- a/driver/Commandline.ml
+++ b/driver/Commandline.ml
@@ -16,7 +16,6 @@
 (* Parsing of command-line flags and arguments *)
 
 open Printf
-open Responsefile
 
 type pattern =
   | Exact of string
@@ -114,14 +113,15 @@ let parse_array spec argv first last =
     end
   in parse first
 
-let argv : string array ref = ref [||]
+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 =
-  try
-    argv := expandargv Sys.argv;
-    parse_array spec !argv 1 (Array.length !argv - 1)
-  with Responsefile.Error s ->
-    raise (CmdError s)
+  parse_array spec argv 1 (Array.length argv - 1)
 
 let long_int_action key s =
   let ls = String.length s
diff --git a/driver/Commandline.mli b/driver/Commandline.mli
index e1b917f2..8bb6f18f 100644
--- a/driver/Commandline.mli
+++ b/driver/Commandline.mli
@@ -39,11 +39,11 @@ type action =
    patterns are tried in the order in which they appear in the list. *)
 
 exception CmdError of string
-(** Raise by [parse_cmdline] when an error occured *)
+(** Raise by [parse_cmdline] when an error occurred *)
 
 val parse_cmdline: (pattern * action) list -> unit
-(** [parse_cmdline actions] parses the commandline and performs all [actions].
-    Raises [CmdError] if an error occurred.
+(** [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
@@ -51,5 +51,5 @@ val longopt_int: string -> (int -> unit) -> pattern * action
     options of the form [key=<n>] and calls [fn] with the integer argument
 *)
 
-val argv: string array ref
+val argv: string array
 (** [argv] contains the complete command line after @-file expandsion *)
diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml
index 58dd4007..c151ecf2 100644
--- a/driver/CommonOptions.ml
+++ b/driver/CommonOptions.ml
@@ -14,9 +14,9 @@ open Clflags
 open Commandline
 
 (* The version string for [tool_name] *)
-let version_string tool_name=
+let version_string tool_name =
   if Version.buildnr <> "" && Version.tag <> "" then
-    Printf.sprintf "The CompCert %s, %s, Build: %s, Tag: %s\n" tool_name Version.version Version.buildnr Version.tag
+    Printf.sprintf "The CompCert %s, Release: %s, Build: %s, Tag: %s\n" tool_name Version.version Version.buildnr Version.tag
   else
     Printf.sprintf "The CompCert %s, version %s\n" tool_name Version.version
 
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index eae3aaab..dcd0d60b 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -13,11 +13,11 @@
 open Printf
 
 let search_argv key =
-  let len = Array.length Sys.argv in
+  let len = Array.length Commandline.argv in
   let res: string option ref = ref None in
   for i = 1 to len - 2 do
-    if Sys.argv.(i) = key then
-      res := Some Sys.argv.(i + 1);
+    if Commandline.argv.(i) = key then
+      res := Some Commandline.argv.(i + 1);
   done;
   !res
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 74e7ae77..404271cd 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -199,6 +199,9 @@ Processing options:
   -finline       Perform inlining of functions [on]
   -finline-functions-called-once Integrate functions only required by their
                  single caller [on]
+  -fif-conversion Perform if-conversion (generation of conditional moves) [on]
+  -ffavor-branchless Favor the generation of branch-free instruction sequences,
+                     even when possibly more costly than the default   [off]
 Code generation options: (use -fno-<opt> to turn off -f<opt>)
   -ffpu          Use FP registers for some integer operations [on]
   -fsmall-data <n>  Set maximal size <n> for allocation in small data area
@@ -206,6 +209,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>)
   -falign-functions <n>  Set alignment (in bytes) of function entry points
   -falign-branch-targets <n>  Set alignment (in bytes) of branch targets
   -falign-cond-branches <n>  Set alignment (in bytes) of conditional branches
+  -fcommon       Put uninitialized globals in the common section [on].
 |} ^
  target_help ^
  toolchain_help ^
@@ -252,7 +256,8 @@ let dump_mnemonics destfile =
   exit 0
 
 let optimization_options = [
-  option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy; option_fpostpass; option_finline_functions_called_once;
+  option_ftailcalls; option_fifconversion; option_fconstprop; option_fcse;
+  option_fpostpass; option_fredundancy; option_finline_functions_called_once;
 ]
 
 let set_all opts () = List.iter (fun r -> r := true) opts
@@ -269,6 +274,10 @@ let cmdline_actions =
     [Exact("-f" ^ name ^ "="), String 
       (fun s -> (strref := (if s == "" then "list" else s)); ref := true)
      ] in
+  let check_align n =
+    if n <= 0 || ((n land (n - 1)) <> 0) then
+      error no_loc "requested alignment %d is not a power of 2" n
+    in
   [
 (* Getting help *)
   Exact "-help", Unit print_usage_and_exit;
@@ -303,10 +312,12 @@ let cmdline_actions =
   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);
-  Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n);
-  Exact "-falign-functions", Integer(fun n -> option_falignfunctions := Some n);
-  Exact "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n);
-  Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n);] @
+  Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); 
+  Exact "-ffavor-branchless", Set option_ffavor_branchless;
+  Exact "-falign-functions", Integer(fun n -> check_align n; option_falignfunctions := Some n);
+  Exact "-falign-branch-targets", Integer(fun n -> check_align n; option_falignbranchtargets := n);
+  Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);] @
+      f_opt "common" option_fcommon @
 (* Target processor options *)
   (if Configuration.arch = "arm" then
     if Configuration.model = "armv6" then
@@ -365,6 +376,7 @@ let cmdline_actions =
 (* Optimization options *)
 (* -f options: come in -f and -fno- variants *)
   @ f_opt "tailcalls" option_ftailcalls
+  @ f_opt "if-conversion" option_fifconversion
   @ f_opt "const-prop" option_fconstprop
   @ f_opt "cse" option_fcse
   @ f_opt "redundancy" option_fredundancy
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index b29bb7f3..d7162865 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -11,21 +11,43 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+open Printf
 open Clflags
 open Commandline
 open Driveraux
 
 (* Common frontend functions between clightgen and ccomp *)
 
+(* Split the version number into major.minor *)
+
+let re_version = Str.regexp {|\([0-9]+\)\.\([0-9]+\)|}
+
+let (v_major, v_minor) =
+  let get n = int_of_string (Str.matched_group n Version.version) in
+  assert (Str.string_match re_version Version.version 0);
+  (get 1, get 2)
+
+let v_number =
+  assert (v_minor < 100);
+  100 * v_major + v_minor
+
+(* Predefined macros: version numbers, C11 features *)
+
 let predefined_macros =
-  [
+  let macros = [  
     "-D__COMPCERT__";
+    sprintf "-D__COMPCERT_MAJOR__=%d" v_major;    
+    sprintf "-D__COMPCERT_MINOR__=%d" v_minor;    
+    sprintf "-D__COMPCERT_VERSION__=%d" v_number;    
     "-U__STDC_IEC_559_COMPLEX__";
     "-D__STDC_NO_ATOMICS__";
     "-D__STDC_NO_COMPLEX__";
     "-D__STDC_NO_THREADS__";
     "-D__STDC_NO_VLA__"
-  ]
+  ] in
+  if Version.buildnr = ""
+  then macros
+  else sprintf "-D__COMPCERT_BUILDNR__=%s" Version.buildnr :: macros
 
 (* From C to preprocessed C *)
 
@@ -110,7 +132,7 @@ let gnu_prepro_opt_key key s =
 let gnu_prepro_opt s =
   prepro_options := s::!prepro_options
 
-(* Add gnu preprocessor option s and the implict -E *)
+(* Add gnu preprocessor option s and the implicit -E *)
 let gnu_prepro_opt_e s =
   prepro_options := s :: !prepro_options;
   option_E := true
@@ -150,7 +172,7 @@ let prepro_actions = [
   @ (if Configuration.gnu_toolchain then gnu_prepro_actions else [])
 
 let gnu_prepro_help =
-{|  -M            Ouput a rule suitable for make describing the
+{|  -M            Output a rule suitable for make describing the
                  dependencies of the main source file
   -MM            Like -M but do not mention system header files
   -MF <file>     Specifies file <file> as output file for -M or -MM