Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div

(unfinished)

10 files changed, 193 insertions, 69 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index fd5f0e68..c20758b3 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -26,13 +26,20 @@ let option_ffloatconstprop = ref 2
 let option_ftailcalls = ref true
 let option_fconstprop = ref true
 let option_fcse = ref true
+let option_fcse2 = ref true
 let option_fredundancy = ref true
+let option_fduplicate = ref (-1)
+let option_finvertcond = ref true
+let option_ftracelinearize = ref false
 let option_fpostpass = ref true
 let option_fpostpass_sched = ref "list"
+let option_fifconversion = ref true
+let option_Obranchless = 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
@@ -70,7 +77,10 @@ let use_standard_headers =  ref Configuration.has_standard_headers
 let option_fglobaladdrtmp = ref false
 let option_fglobaladdroffset = ref false
 let option_fxsaddr = ref true  
-let option_coalesce_mem = ref true  
-
 let option_div_i32 = ref "stsud"
 let option_div_i64 = ref "stsud" 
+let option_faddx = ref false  
+let option_fcoalesce_mem = ref true
+let option_fforward_moves = ref true
+let option_all_loads_nontrap = ref false
+let option_inline_auto_threshold = ref 0
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/Compiler.v b/driver/Compiler.v
index 6d398327..499feff2 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -38,10 +38,14 @@ Require RTLgen.
 Require Tailcall.
 Require Inlining.
 Require Renumber.
+Require Duplicate.
 Require Constprop.
 Require CSE.
+Require ForwardMoves.
+Require CSE2.
 Require Deadcode.
 Require Unusedglob.
+Require Allnontrap.
 Require Allocation.
 Require Tunneling.
 Require Linearize.
@@ -59,10 +63,14 @@ Require RTLgenproof.
 Require Tailcallproof.
 Require Inliningproof.
 Require Renumberproof.
+Require Duplicateproof.
 Require Constpropproof.
 Require CSEproof.
+Require ForwardMovesproof.
+Require CSE2proof.
 Require Deadcodeproof.
 Require Unusedglobproof.
+Require Allnontrapproof.
 Require Allocproof.
 Require Tunnelingproof.
 Require Linearizeproof.
@@ -126,16 +134,24 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ print (print_RTL 2)
    @@ time "Renumbering" Renumber.transf_program
    @@ print (print_RTL 3)
-   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
+  @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program)
    @@ print (print_RTL 4)
-   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
    @@ print (print_RTL 5)
-  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
+   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
    @@ print (print_RTL 6)
-  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
    @@ print (print_RTL 7)
-  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
    @@ print (print_RTL 8)
+   @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
+   @@ print (print_RTL 9)
+  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+   @@ print (print_RTL 10)
+   @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+   @@ print (print_RTL 11)
+  @@@ time "Unused globals" Unusedglob.transform_program
+   @@ print (print_RTL 12)
   @@@ time "Register allocation" Allocation.transf_program
    @@ print print_LTL
    @@ time "Branch tunneling" Tunneling.tunnel_program
@@ -144,7 +160,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
   @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program)
   @@@ time "Mach generation" Stacking.transf_program
    @@ print print_Mach
-  @@@ time "Asm generation" Asmgen.transf_program.
+  @@@ time "Total Mach->Asm generation" Asmgen.transf_program.
 
 Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
    OK p
@@ -238,10 +254,14 @@ Definition CompCert's_passes :=
   ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog)
   ::: mkpass Inliningproof.match_prog
   ::: mkpass Renumberproof.match_prog
+  ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog)
   ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog)
   ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog)
   ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog)
+  ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog)
+  ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog)
   ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
+  ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog)
   ::: mkpass Unusedglobproof.match_prog
   ::: mkpass Allocproof.match_prog
   ::: mkpass Tunnelingproof.match_prog
@@ -281,17 +301,21 @@ Proof.
   set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *.
   destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate.
   set (p9 := Renumber.transf_program p8) in *.
-  set (p10 := total_if optim_constprop Constprop.transf_program p9) in *.
-  set (p11 := total_if optim_constprop Renumber.transf_program p10) in *.
-  destruct (partial_if optim_CSE CSE.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate.
-  destruct (partial_if optim_redundancy Deadcode.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
-  destruct (Unusedglob.transform_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate.
-  destruct (Allocation.transf_program p14) as [p15|e] eqn:P15; simpl in T; try discriminate.
-  set (p16 := Tunneling.tunnel_program p15) in *.
-  destruct (Linearize.transf_program p16) as [p17|e] eqn:P17; simpl in T; try discriminate.
-  set (p18 := CleanupLabels.transf_program p17) in *.
-  destruct (partial_if debug Debugvar.transf_program p18) as [p19|e] eqn:P19; simpl in T; try discriminate.
-  destruct (Stacking.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate.
+  destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate.
+  set (p11 := total_if optim_constprop Constprop.transf_program p10) in *.
+  set (p12 := total_if optim_constprop Renumber.transf_program p11) in *.
+  destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
+  set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *.
+  set (p13ter := total_if optim_forward_moves ForwardMoves.transf_program p13bis) in *.
+  destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate.
+  set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *.
+  destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate.
+  destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate.
+  set (p17 := Tunneling.tunnel_program p16) in *.
+  destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate.
+  set (p19 := CleanupLabels.transf_program p18) in *.
+  destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; simpl in T; try discriminate.
+  destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; simpl in T; try discriminate.
   unfold match_prog; simpl.
   exists p1; split. apply SimplExprproof.transf_program_match; auto.
   exists p2; split. apply SimplLocalsproof.match_transf_program; auto.
@@ -302,17 +326,21 @@ Proof.
   exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match.
   exists p8; split. apply Inliningproof.transf_program_match; auto.
   exists p9; split. apply Renumberproof.transf_program_match; auto.
-  exists p10; split. apply total_if_match. apply Constpropproof.transf_program_match.
-  exists p11; split. apply total_if_match. apply Renumberproof.transf_program_match.
-  exists p12; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
-  exists p13; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
-  exists p14; split. apply Unusedglobproof.transf_program_match; auto.
-  exists p15; split. apply Allocproof.transf_program_match; auto.
-  exists p16; split. apply Tunnelingproof.transf_program_match.
-  exists p17; split. apply Linearizeproof.transf_program_match; auto.
-  exists p18; split. apply CleanupLabelsproof.transf_program_match; auto.
-  exists p19; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match.
-  exists p20; split. apply Stackingproof.transf_program_match; auto.
+  exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto.
+  exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match.
+  exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match.
+  exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match.
+  exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match.
+  exists p13ter; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match.
+  exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
+  exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match.
+  exists p15; split. apply Unusedglobproof.transf_program_match; auto.
+  exists p16; split. apply Allocproof.transf_program_match; auto.
+  exists p17; split. apply Tunnelingproof.transf_program_match.
+  exists p18; split. apply Linearizeproof.transf_program_match; auto.
+  exists p19; split. apply CleanupLabelsproof.transf_program_match; auto.
+  exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match.
+  exists p21; split. apply Stackingproof.transf_program_match; auto.
   exists tp; split. apply Asmgenproof.transf_program_match; auto.
   reflexivity.
 Qed.
@@ -364,7 +392,7 @@ Ltac DestructM :=
       destruct H as (p & M & MM); clear H
   end.
   repeat DestructM. subst tp.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p21)).
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -384,14 +412,22 @@ Ltac DestructM :=
     eapply Inliningproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct.
+  eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct.
   eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct.
   eapply compose_forward_simulations.
+  eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct.
+  eapply compose_forward_simulations.
+  eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
     eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
+    eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct.
+  eapply compose_forward_simulations.
     eapply Unusedglobproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply Allocproof.transf_program_correct; eassumption.
diff --git a/driver/Compopts.v b/driver/Compopts.v
index f7de596c..848657e5 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -27,6 +27,9 @@ Parameter generate_float_constants: unit -> bool.
 (** For value analysis.  Currently always false. *)
 Parameter va_strict: unit -> bool.
 
+(** Flag -fduplicate. Branch prediction annotation + tail duplication *)
+Parameter optim_duplicate: unit -> bool.
+
 (** Flag -ftailcalls.  For tail call optimization. *)
 Parameter optim_tailcalls: unit -> bool.
 
@@ -36,6 +39,9 @@ Parameter optim_constprop: unit -> bool.
 (** Flag -fcse.  For common subexpression elimination. *)
 Parameter optim_CSE: unit -> bool.
 
+(** Flag -fcse2.  For DMonniaux's common subexpression elimination. *)
+Parameter optim_CSE2: unit -> bool.
+
 (** Flag -fredundancy.  For dead code elimination. *)
 Parameter optim_redundancy: unit -> bool.
 
@@ -43,19 +49,32 @@ Parameter optim_redundancy: unit -> bool.
 Parameter optim_postpass: unit -> bool.
 
 (** FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false) *)
-Parameter optim_fglobaladdrtmp: unit -> bool.
+Parameter optim_globaladdrtmp: unit -> bool.
 
 (** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses  (default false) *)
-Parameter optim_fglobaladdroffset: unit -> bool.
+Parameter optim_globaladdroffset: unit -> bool.
 
 (** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *)
-Parameter optim_fxsaddr: unit -> bool.
+Parameter optim_xsaddr: unit -> bool.
 
 (** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *)
 Parameter optim_coalesce_mem: unit -> bool.
 
+(** FIXME TEMPORARY Flag -faddx. Fuse (default false) *)
+Parameter optim_addx: unit -> bool.
+
 (** Flag -fthumb.  For the ARM back-end. *)
 Parameter thumb: unit -> bool.
 
 (** Flag -g.  For insertion of debugging information. *)
 Parameter debug: unit -> bool.
+
+(** Flag -fall-loads-nontrap. Turn user loads into non trapping. *)
+Parameter all_loads_nontrap: unit -> bool.
+
+(** Flag -fforward-moves. Forward moves after CSE. *)
+Parameter optim_forward_moves: unit -> bool.
+
+(* TODO is there a more appropriate place? *)
+Require Import Coqlib.
+Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index eae3aaab..08084720 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
 
@@ -123,7 +123,7 @@ let get_bool_config key =
 
 let arch =
   match get_config_string "arch" with
-  | "powerpc"|"arm"|"x86"|"riscV"|"mppa_k1c" as a -> a
+  | "powerpc"|"arm"|"x86"|"riscV"|"mppa_k1c"|"aarch64" as a -> a
   | v -> bad_config "arch" [v]
 let model = get_config_string "model"
 let abi = get_config_string "abi"
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 314cf31c..ba48f29a 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -185,20 +185,36 @@ Processing options:
 {|Optimization options: (use -fno-<opt> to turn off -f<opt>)
   -O             Optimize the compiled code [on by default]
   -O0            Do not optimize the compiled code
-  -O1 -O2 -O3    Synonymous for -O
+  -O1            Perform all optimization passes except scheduling
+  -O2 -O3        Synonymous for -O
   -Os            Optimize for code size in preference to code speed
+  -Obranchless   Optimize to generate fewer conditional branches; try to produce
+                 branch-free instruction sequences as much as possible
+  -finline-auto-threshold n   Inline functions under size n
   -ftailcalls    Optimize function calls in tail position [on]
   -fconst-prop   Perform global constant propagation  [on]
   -ffloat-const-prop <n>  Control constant propagation of floats
                    (<n>=0: none, <n>=1: limited, <n>=2: full; default is full)
   -fcse          Perform common subexpression elimination [on]
+  -fcse2         Perform inter-loop common subexpression elimination [on]
   -fredundancy   Perform redundancy elimination [on]
   -fpostpass     Perform postpass scheduling (only for K1 architecture) [on]
   -fpostpass= <optim> Perform postpass scheduling with the specified optimization [list]
                    (<optim>=list: list scheduling, <optim>=ilp: ILP, <optim>=greedy: just packing bundles)
+  -fduplicate <nb_nodes> Perform tail duplication to form superblocks on predicted traces
+    nb_nodes control the heuristic deciding to duplicate or not
+    A value of -1 desactivates the entire pass (including branch prediction)
+    A value of 0 desactivates the duplication (but activates the branch prediction)
+    FIXME : this is desactivated by default for now
+    -finvertcond    Invert conditions based on predicted paths (to prefer fallthrough).
+                    Requires -fduplicate to be also activated [on]
+    -ftracelinearize Linearizes based on the traces identified by duplicate phase
+                    It is heavily recommended to activate -finvertcond with this pass [off]
+  -fforward-moves   Forward moves after CSE
   -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]
 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 +222,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 +269,10 @@ 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_fcse2;
+    option_fpostpass;
+    option_fredundancy; option_finline; option_finline_functions_called_once;
 ]
 
 let set_all opts () = List.iter (fun r -> r := true) opts
@@ -265,14 +285,18 @@ 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 f_opt_str name ref strref default =
+  let f_opt_str name ref strref =
     [Exact("-f" ^ name ^ "="), String 
-      (fun s -> (strref := (if s == "" then default else s)); ref := true)
+      (fun s -> (strref := (if s == "" then "list" else s)); ref := true)
      ] in
   let f_str name strref default =
     [Exact("-f" ^ name ^ "="), String 
       (fun s -> (strref := (if s == "" then default else s)))
      ] 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,14 +327,18 @@ let cmdline_actions =
  [
   Exact "-O0", Unit (unset_all optimization_options);
   Exact "-O", Unit (set_all optimization_options);
+  _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false);
   _Regexp "-O[123]$", Unit (set_all optimization_options);
   Exact "-Os", Set option_Osize;
+  Exact "-Obranchless", Set option_Obranchless;
+  Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n);
   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 "-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
@@ -369,19 +397,27 @@ 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 "cse2" option_fcse2
   @ f_opt "redundancy" option_fredundancy
   @ f_opt "postpass" option_fpostpass
-  @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched "list"
+  @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ]
+  @ f_opt "invertcond" option_finvertcond
+  @ f_opt "tracelinearize" option_ftracelinearize
+  @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched
   @ f_opt "inline" option_finline
   @ f_opt "inline-functions-called-once" option_finline_functions_called_once
   @ f_opt "globaladdrtmp" option_fglobaladdrtmp
   @ f_opt "globaladdroffset" option_fglobaladdroffset
   @ f_opt "xsaddr" option_fxsaddr
-  @ f_opt "coalesce-mem" option_coalesce_mem
   @ f_str "div-i32" option_div_i32 "stsud"
   @ f_str "div-i64" option_div_i64 "stsud"
+  @ f_opt "addx" option_faddx
+  @ f_opt "coalesce-mem" option_fcoalesce_mem
+  @ f_opt "all-loads-nontrap" option_all_loads_nontrap
+  @ f_opt "forward-moves" option_fforward_moves
 (* Code generation options *)
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index b29bb7f3..b9db0d23 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 *)
 
@@ -95,9 +117,10 @@ let init () =
                    then Machine.rv64
                    else Machine.rv32
     | "mppa_k1c" -> Machine.mppa_k1c
+    | "aarch64" -> Machine.aarch64
     | _         -> assert false
   end;
-  Builtins.set C2C.builtins;
+  Env.set_builtins C2C.builtins;
   Cutil.declare_attributes C2C.attributes;
   CPragmas.initialize()
 
@@ -110,7 +133,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 +173,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
diff --git a/driver/Interp.ml b/driver/Interp.ml
index 6760e76c..d4286779 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -15,12 +15,12 @@
 open Format
 open Camlcoq
 open AST
-open Integers
+open! Integers
 open Values
 open Memory
 open Globalenvs
 open Events
-open Ctypes
+open! Ctypes
 open Csyntax
 open Csem
 
@@ -145,7 +145,7 @@ let print_state p (prog, ge, s) =
 let compare_mem m1 m2 =
   (* assumes nextblocks were already compared equal *)
   (* should permissions be taken into account? *)
-  Pervasives.compare m1.Mem.mem_contents m2.Mem.mem_contents
+  compare m1.Mem.mem_contents m2.Mem.mem_contents
 
 (* Comparing continuations *)