Merge branch 'master' into dwarf

12 files changed, 489 insertions, 179 deletions

diff --git a/Changelog b/Changelog
index 4b102d78..87b2174f 100644
--- a/Changelog
+++ b/Changelog
@@ -1,7 +1,8 @@
 - In string and character literals, treat illegal escape sequences 
   (e.g. "\%" or "\0") as an error instead of a warning.
 - Upgraded Flocq to version 2.4.0.
-
+- cchecklink: added option "-files-from" to read .sdump file names
+    from a file or from standard input.	  
 
 Release 2.4, 2014-09-17
 =======================
diff --git a/backend/Tailcall.v b/backend/Tailcall.v
index 25da531c..db246fec 100644
--- a/backend/Tailcall.v
+++ b/backend/Tailcall.v
@@ -14,7 +14,6 @@
 
 Require Import Coqlib.
 Require Import Maps.
-Require Import Compopts.
 Require Import AST.
 Require Import Registers.
 Require Import Op.
@@ -100,7 +99,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) :=
   using a compilation option. *)
 
 Definition transf_function (f: function) : function :=
-  if zeq f.(fn_stacksize) 0 && eliminate_tailcalls tt
+  if zeq f.(fn_stacksize) 0
   then RTL.transf_function (transf_instr f) f
   else f.
 
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 1965b18e..cc4ff55e 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -13,7 +13,6 @@
 (** Recognition of tail calls: correctness proof *)
 
 Require Import Coqlib.
-Require Import Compopts.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
@@ -183,11 +182,10 @@ Lemma transf_instr_lookup:
   exists i',  (transf_function f).(fn_code)!pc = Some i' /\ transf_instr_spec f i i'.
 Proof.
   intros. unfold transf_function.
-  destruct (zeq (fn_stacksize f) 0). destruct (eliminate_tailcalls tt).
+  destruct (zeq (fn_stacksize f) 0).
   simpl. rewrite PTree.gmap. rewrite H. simpl. 
   exists (transf_instr f pc i); split. auto. apply transf_instr_charact; auto. 
   exists i; split. auto. constructor.
-  exists i; split. auto. constructor.
 Qed.
 
 (** * Semantic properties of the code transformation *)
@@ -263,14 +261,14 @@ Lemma sig_preserved:
   forall f, funsig (transf_fundef f) = funsig f.
 Proof.
   destruct f; auto. simpl. unfold transf_function. 
-  destruct (zeq (fn_stacksize f) 0 && eliminate_tailcalls tt); auto. 
+  destruct (zeq (fn_stacksize f) 0); auto. 
 Qed.
 
 Lemma stacksize_preserved:
   forall f, fn_stacksize (transf_function f) = fn_stacksize f.
 Proof.
   unfold transf_function. intros. 
-  destruct (zeq (fn_stacksize f) 0 && eliminate_tailcalls tt); auto.
+  destruct (zeq (fn_stacksize f) 0); auto.
 Qed.
 
 Lemma find_function_translated:
@@ -556,7 +554,7 @@ Proof.
   assert (fn_stacksize (transf_function f) = fn_stacksize f /\
           fn_entrypoint (transf_function f) = fn_entrypoint f /\
           fn_params (transf_function f) = fn_params f).
-    unfold transf_function. destruct (zeq (fn_stacksize f) 0 && eliminate_tailcalls tt); auto. 
+    unfold transf_function. destruct (zeq (fn_stacksize f) 0); auto. 
   destruct H0 as [EQ1 [EQ2 EQ3]]. 
   left. econstructor; split.
   simpl. eapply exec_function_internal; eauto. rewrite EQ1; eauto.
diff --git a/checklink/Validator.ml b/checklink/Validator.ml
index baf06fca..6969409a 100644
--- a/checklink/Validator.ml
+++ b/checklink/Validator.ml
@@ -22,6 +22,27 @@ let set_conf_file s =
   | Some _ -> raise (Arg.Bad "multiple configuration files given on command line")
   end
 
+let read_sdumps_from_channel ic =
+  try
+    while true do
+      let l = input_line ic in
+      if l <> "" then sdump_files := l :: !sdump_files
+    done
+  with End_of_file ->
+    ()
+
+let read_sdumps_from_file f =
+  if f = "-" then
+    read_sdumps_from_channel stdin
+  else begin
+    try
+      let ic = open_in f in
+      read_sdumps_from_channel ic;
+      close_in ic
+    with Sys_error msg ->
+      Printf.eprintf "Error reading file: %s\n" msg; exit 2
+  end
+
 let option_disassemble = ref false
 let disassemble_list = ref ([]: string list)
 let add_disassemble s =
@@ -31,12 +52,15 @@ let add_disassemble s =
 let options = [
   (* Main options *)
   "-exe", Arg.String set_elf_file,
-  "<filename> Specify the ELF executable file to analyze";
+    "<filename> Specify the ELF executable file to analyze";
   "-conf", Arg.String set_conf_file,
-  "<filename> Specify a configuration file";
+    "<filename> Specify a configuration file";
+  "-files-from", Arg.String read_sdumps_from_file,
+    "<filename> Read names of .sdump files from the given file\n\
+       \t(or from standard input if <filename> is '-')";
   (* Parsing behavior *)
   "-relaxed", Arg.Set ELF_parsers.relaxed,
-  "Allows the following behaviors in the ELF parser:
+  "Allows the following behaviors in the ELF parser:\n\
 \t* Use of a fallback heuristic to resolve symbols bootstrapped at load time";
   (* Printing behavior *)
   "-no-exhaustive", Arg.Clear Check.exhaustivity,
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index c6217ba1..ead27b36 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -24,6 +24,9 @@ let option_fpacked_structs = ref false
 let option_ffpu = ref true
 let option_ffloatconstprop = ref 2
 let option_ftailcalls = ref true
+let option_fconstprop = ref true
+let option_fcse = ref true
+let option_fredundancy = ref true
 let option_falignfunctions = ref (None: int option)
 let option_falignbranchtargets = ref 0
 let option_faligncondbranchs = ref 0
diff --git a/driver/Commandline.ml b/driver/Commandline.ml
new file mode 100644
index 00000000..bc095af6
--- /dev/null
+++ b/driver/Commandline.ml
@@ -0,0 +1,105 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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)
+
+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 usage 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 ->
+          if s <> "-help" && s <> "--help" 
+          then eprintf "Unknown argument `%s'\n" s
+          else printf "%s" usage;
+          exit 2
+      | 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
+            eprintf "Option `%s' expects an argument\n" s; exit 2
+          end
+      | Some(Integer fn) ->
+          if i + 1 <= last then begin
+            let n =
+              try
+                int_of_string argv.(i+1)
+              with Failure _ ->
+                eprintf "Argument to option `%s' must be an integer\n" s;
+                exit 2
+            in
+            fn n; parse (i+2)
+          end else begin
+            eprintf "Option `%s' expects an argument\n" s; exit 2
+          end
+    end
+  in parse first
+
+let parse_cmdline spec usage =
+  parse_array spec usage Sys.argv 1 (Array.length Sys.argv - 1)
diff --git a/driver/Commandline.mli b/driver/Commandline.mli
new file mode 100644
index 00000000..7a18905f
--- /dev/null
+++ b/driver/Commandline.mli
@@ -0,0 +1,41 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 *)
+
+val parse_cmdline:
+  (pattern * action) list -> string (* usage string *) -> unit
+
+(* Note on precedence: [Exact] patterns are tried first, then the other
+   patterns are tried in the order in which they appear in the list. *)
diff --git a/driver/Compiler.v b/driver/Compiler.v
index ae54f487..fb813c7c 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -71,6 +71,8 @@ Require Linearizeproof.
 Require CleanupLabelsproof.
 Require Stackingproof.
 Require Asmgenproof.
+(** Command-line flags. *)
+Require Import Compopts.
 
 (** Pretty-printers (defined in Caml). *)
 Parameter print_Clight: Clight.program -> unit.
@@ -103,6 +105,14 @@ Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
 
 Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
 
+Definition total_if {A: Type}
+          (flag: unit -> bool) (f: A -> A) (prog: A) : A :=
+  if flag tt then f prog else prog.
+
+Definition partial_if {A: Type}
+          (flag: unit -> bool) (f: A -> res A) (prog: A) : res A :=
+  if flag tt then f prog else OK prog.
+
 (** We define three translation functions for whole programs: one
   starting with a C program, one with a Cminor program, one with an
   RTL program.  The three translations produce Asm programs ready for
@@ -111,24 +121,24 @@ Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
 Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    OK f
    @@ print (print_RTL 0)
-   @@ time "Tail calls" Tailcall.transf_program
+   @@ total_if Compopts.optim_tailcalls (time "Tail calls" Tailcall.transf_program)
    @@ print (print_RTL 1)
   @@@ time "Inlining" Inlining.transf_program
    @@ print (print_RTL 2)
    @@ time "Renumbering" Renumber.transf_program
    @@ print (print_RTL 3)
-   @@ time "Constant propagation" Constprop.transf_program
+   @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
    @@ print (print_RTL 4)
-   @@ time "Renumbering" Renumber.transf_program
+   @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
    @@ print (print_RTL 5)
-  @@@ time "CSE" CSE.transf_program
+  @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
    @@ print (print_RTL 6)
-  @@@ time "Dead code" Deadcode.transf_program
+  @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 7)
   @@@ time "Register allocation" Allocation.transf_program
    @@ print print_LTL
    @@ time "Branch tunneling" Tunneling.tunnel_program
-  @@@ Linearize.transf_program
+  @@@ time "CFG linearization" Linearize.transf_program
    @@ time "Label cleanup" CleanupLabels.transf_program
   @@@ time "Mach generation" Stacking.transf_program
    @@ print print_Mach
@@ -175,6 +185,33 @@ Proof.
   intros. destruct x; simpl. rewrite print_identity. auto. auto. 
 Qed.
 
+Remark forward_simulation_identity:
+  forall sem, forward_simulation sem sem.
+Proof.
+  intros. apply forward_simulation_step with (fun s1 s2 => s2 = s1); intros.
+- auto.
+- exists s1; auto.
+- subst s2; auto.
+- subst s2. exists s1'; auto. 
+Qed. 
+
+Lemma total_if_simulation:
+  forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> A) (prog: A),
+  (forall p, forward_simulation (sem p) (sem (f p))) ->
+  forward_simulation (sem prog) (sem (total_if flag f prog)).
+Proof.
+  intros. unfold total_if. destruct (flag tt). auto. apply forward_simulation_identity.
+Qed.
+
+Lemma partial_if_simulation:
+  forall (A: Type) (sem: A -> semantics) (flag: unit -> bool) (f: A -> res A) (prog tprog: A),
+  partial_if flag f prog = OK tprog ->
+  (forall p tp, f p = OK tp -> forward_simulation (sem p) (sem tp)) ->
+  forward_simulation (sem prog) (sem tprog).
+Proof.
+  intros. unfold partial_if in *. destruct (flag tt). eauto. inv H. apply forward_simulation_identity.
+Qed.
+
 (** * Semantic preservation *)
 
 (** We prove that the [transf_program] translations preserve semantics
@@ -200,31 +237,44 @@ Proof.
   unfold transf_rtl_program, time in H.
   repeat rewrite compose_print_identity in H.
   simpl in H.
-  set (p1 := Tailcall.transf_program p) in *.
+  set (p1 := total_if optim_tailcalls Tailcall.transf_program p) in *.
   destruct (Inlining.transf_program p1) as [p11|] eqn:?; simpl in H; try discriminate.
   set (p12 := Renumber.transf_program p11) in *.
-  set (p2 := Constprop.transf_program p12) in *.
-  set (p21 := Renumber.transf_program p2) in *.
-  destruct (CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate.
-  destruct (Deadcode.transf_program p3) as [p31|] eqn:?; simpl in H; try discriminate.
+  set (p2 := total_if optim_constprop Constprop.transf_program p12) in *.
+  set (p21 := total_if optim_constprop Renumber.transf_program p2) in *.
+  destruct (partial_if optim_CSE CSE.transf_program p21) as [p3|] eqn:?; simpl in H; try discriminate.
+  destruct (partial_if optim_redundancy Deadcode.transf_program p3) as [p31|] eqn:?; simpl in H; try discriminate.
   destruct (Allocation.transf_program p31) as [p4|] eqn:?; simpl in H; try discriminate.
   set (p5 := Tunneling.tunnel_program p4) in *.
   destruct (Linearize.transf_program p5) as [p6|] eqn:?; simpl in H; try discriminate.
   set (p7 := CleanupLabels.transf_program p6) in *.
   destruct (Stacking.transf_program p7) as [p8|] eqn:?; simpl in H; try discriminate.
-  eapply compose_forward_simulation. apply Tailcallproof.transf_program_correct. 
-  eapply compose_forward_simulation. apply Inliningproof.transf_program_correct. eassumption.
-  eapply compose_forward_simulation. apply Renumberproof.transf_program_correct. 
-  eapply compose_forward_simulation. apply Constpropproof.transf_program_correct. 
-  eapply compose_forward_simulation. apply Renumberproof.transf_program_correct. 
-  eapply compose_forward_simulation. apply CSEproof.transf_program_correct. eassumption.
-  eapply compose_forward_simulation. apply Deadcodeproof.transf_program_correct. eassumption.
-  eapply compose_forward_simulation. apply Allocproof.transf_program_correct. eassumption.
-  eapply compose_forward_simulation. apply Tunnelingproof.transf_program_correct.
-  eapply compose_forward_simulation. apply Linearizeproof.transf_program_correct. eassumption. 
-  eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. 
-  eapply compose_forward_simulation. apply Stackingproof.transf_program_correct.
-    eexact Asmgenproof.return_address_exists. eassumption.
+  apply compose_forward_simulation with (RTL.semantics p1).
+    apply total_if_simulation. apply Tailcallproof.transf_program_correct. 
+  apply compose_forward_simulation with (RTL.semantics p11).
+    apply Inliningproof.transf_program_correct; auto.
+  apply compose_forward_simulation with (RTL.semantics p12).
+    apply Renumberproof.transf_program_correct. 
+  apply compose_forward_simulation with (RTL.semantics p2).
+    apply total_if_simulation. apply Constpropproof.transf_program_correct.
+  apply compose_forward_simulation with (RTL.semantics p21).
+    apply total_if_simulation. apply Renumberproof.transf_program_correct. 
+  apply compose_forward_simulation with (RTL.semantics p3).
+    eapply partial_if_simulation; eauto.  apply CSEproof.transf_program_correct.
+  apply compose_forward_simulation with (RTL.semantics p31).
+    eapply partial_if_simulation; eauto. apply Deadcodeproof.transf_program_correct.
+  apply compose_forward_simulation with (LTL.semantics p4).
+    apply Allocproof.transf_program_correct; auto.
+  apply compose_forward_simulation with (LTL.semantics p5).
+    apply Tunnelingproof.transf_program_correct.
+  apply compose_forward_simulation with (Linear.semantics p6).
+    apply Linearizeproof.transf_program_correct; auto.
+  apply compose_forward_simulation with (Linear.semantics p7).
+    apply CleanupLabelsproof.transf_program_correct. 
+  apply compose_forward_simulation with (Mach.semantics Asmgenproof0.return_address_offset p8).
+    apply Stackingproof.transf_program_correct.
+    exact Asmgenproof.return_address_exists.
+    auto.
   apply Asmgenproof.transf_program_correct; eauto.
   split. auto. 
   apply forward_to_backward_simulation. auto. 
diff --git a/driver/Compopts.v b/driver/Compopts.v
index 01109f52..d0c6686e 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -28,7 +28,16 @@ Parameter generate_float_constants: unit -> bool.
 Parameter va_strict: unit -> bool.
 
 (** Flag -ftailcalls.  For tail call optimization. *)
-Parameter eliminate_tailcalls: unit -> bool.
+Parameter optim_tailcalls: unit -> bool.
+
+(** Flag -fconstprop.  For constant propagation. *)
+Parameter optim_constprop: unit -> bool.
+
+(** Flag -fcse.  For common subexpression elimination. *)
+Parameter optim_CSE: unit -> bool.
+
+(** Flag -fredundancy.  For dead code elimination. *)
+Parameter optim_redundancy: unit -> bool.
 
 (** Flag -fthumb.  For the ARM back-end. *)
 Parameter thumb: unit -> bool.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 18005302..76509f41 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -11,6 +11,7 @@
 (* *********************************************************************)
 
 open Printf
+open Commandline
 open Camlcoq
 open Clflags
 open Timing
@@ -89,7 +90,6 @@ let parse_c_file sourcename ifile =
   (* Simplification options *)
   let simplifs =
     "b" (* blocks: mandatory *)
-(*  ^ (if !option_flonglong then "l" else "") *)
   ^ (if !option_fstruct_return then "s" else "")
   ^ (if !option_fbitfields then "f" else "")
   ^ (if !option_fpacked_structs then "p" else "")
@@ -170,6 +170,14 @@ let compile_c_file sourcename ifile ofile =
 (* From Cminor to asm *)
 
 let compile_cminor_file ifile ofile =
+  (* Prepare to dump RTL, Mach, etc, if requested *)
+  let set_dest dst opt ext =
+    dst := if !opt then Some (output_filename ifile ".cm" ext)
+                   else None in
+  set_dest PrintRTL.destination option_drtl ".rtl";
+  set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
+  set_dest PrintLTL.destination option_dltl ".ltl";
+  set_dest PrintMach.destination option_dmach ".mach";
   Sections.initialize();
   let ic = open_in ifile in
   let lb = Lexing.from_channel ic in
@@ -292,7 +300,7 @@ let process_cminor_file sourcename =
       then output_filename sourcename ".cm" ".s"
       else Filename.temp_file "compcert" ".s" in
     compile_cminor_file sourcename asmname;
-    let objname = output_filename ~final: !option_c sourcename ".c" ".o" in
+    let objname = output_filename ~final: !option_c sourcename ".cm" ".o" in
     assemble asmname objname;
     if not !option_dasm then safe_remove asmname;
     objname
@@ -318,6 +326,17 @@ let process_S_file sourcename =
     objname
   end
 
+(* Processing of .h files *)
+
+let process_h_file sourcename =
+  if !option_E then begin
+    preprocess sourcename (output_filename_default "-");
+    ""
+  end else begin
+    eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename;
+    exit 2
+  end    
+
 (* Record actions to be performed after parsing the command line *)
 
 let actions : ((string -> string) * string) list ref = ref []
@@ -341,57 +360,6 @@ let explode_comma_option s =
   | [] -> assert false
   | hd :: tl -> tl
 
-type action =
-  | Set of bool ref
-  | Unset of bool ref
-  | Self of (string -> unit)
-  | String of (string -> unit)
-  | Integer of (int -> unit)
-
-let rec find_action s = function
-  | [] -> None
-  | (re, act) :: rem ->
-      if Str.string_match re s 0 then Some act else find_action s rem
-
-let parse_cmdline spec usage =
-  let acts = List.map (fun (pat, act) -> (Str.regexp pat, act)) spec in
-  let rec parse i =
-    if i < Array.length Sys.argv then begin
-      let s = Sys.argv.(i) in
-      match find_action s acts with
-      | None ->
-          if s <> "-help" && s <> "--help" 
-          then eprintf "Unknown argument `%s'\n" s
-          else printf "%s" usage;
-          exit 2
-      | 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 < Array.length Sys.argv then begin
-            fn Sys.argv.(i+1); parse (i+2)
-          end else begin
-            eprintf "Option `%s' expects an argument\n" s; exit 2
-          end
-      | Some(Integer fn) ->
-          if i + 1 < Array.length Sys.argv then begin
-            let n =
-              try
-                int_of_string Sys.argv.(i+1)
-              with Failure _ ->
-                eprintf "Argument to option `%s' must be an integer\n" s;
-                exit 2
-            in
-            fn n; parse (i+2)
-          end else begin
-            eprintf "Option `%s' expects an argument\n" s; exit 2
-          end
-    end
-  in parse 1
-
 let usage_string =
 "The CompCert C verified compiler, version " ^ Configuration.version ^ "
 Usage: ccomp [options] <source files>
@@ -425,15 +393,21 @@ Language support options (use -fno-<opt> to turn off -f<opt>) :
   -fnone         Turn off all language support options above
 Debugging options:
   -g             Generate debugging information
-Code generation options: (use -fno-<opt> to turn off -f<opt>) :
-  -O             Optimize for speed [on by default]
-  -Os            Optimize for code size
+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
+  -Os            Optimize for code size in preference to code speed
+  -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]
+  -fredundancy   Perform redundancy elimination [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
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
-  -ffloat-const-prop <n>  Control constant propagation of floats
-                   (<n>=0: none, <n>=1: limited, <n>=2: full; default is full)
-  -ftailcalls    Optimize function calls in tail position [on]
   -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
@@ -474,79 +448,102 @@ let language_support_options = [
   option_fpacked_structs; option_finline_asm
 ]
 
+let optimization_options = [
+  option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy
+]
+
+let set_all opts = List.iter (fun r -> r := true) opts
+let unset_all opts = List.iter (fun r -> r := false) opts
+
 let num_source_files = ref 0
 
 let cmdline_actions =
   let f_opt name ref =
-    ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in
+    [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
   [
-  "-I$", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
-  "-D$", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
-  "-U$", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
-  "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options);
-  "-[lL].", Self(fun s -> push_linker_arg s);
-  "-o$", String(fun s -> option_o := Some s);
-  "-E$", Set option_E;
-  "-S$", Set option_S;
-  "-c$", Set option_c;
-  "-v$", Set option_v;
-  "-g$", Self (fun s -> option_g := true; push_linker_arg s);
-  "-stdlib$", String(fun s -> stdlib_path := s);
-  "-dparse$", Set option_dparse;
-  "-dc$", Set option_dcmedium;
-  "-dclight$", Set option_dclight;
-  "-dcminor", Set option_dcminor;
-  "-drtl$", Set option_drtl;
-  "-dltl$", Set option_dltl;
-  "-dalloctrace$", Set option_dalloctrace;
-  "-dmach$", Set option_dmach;
-  "-dasm$", Set option_dasm;
-  "-sdump$", Set option_sdump;
-  "-interp$", Set option_interp;
-  "-quiet$", Self (fun _ -> Interp.trace := 0);
-  "-trace$", Self (fun _ -> Interp.trace := 2);
-  "-random$", Self (fun _ -> Interp.mode := Interp.Random);
-  "-all$", Self (fun _ -> Interp.mode := Interp.All);
-  ".*\\.c$", Self (fun s ->
-      push_action process_c_file s;
-      incr num_source_files);
-  ".*\\.[ip]$", Self (fun s ->
-      push_action process_i_file s;
-      incr num_source_files);
-  ".*\\.cm$", Self (fun s ->
-      push_action process_cminor_file s;
-      incr num_source_files);
-  ".*\\.s$", Self (fun s ->
-      push_action process_s_file s;
-      incr num_source_files);
-  ".*\\.S$", Self (fun s ->
-      push_action process_S_file s;
-      incr num_source_files);
-  ".*\\.[oa]$", Self (fun s ->
-      push_linker_arg s);
-  "-Wp,", Self (fun s ->
-      prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
-  "-Wa,", Self (fun s ->
-      assembler_options := s :: !assembler_options);
-  "-Wl,", Self (fun s ->
-      push_linker_arg s);
-  "-Os$", Set option_Osize;
-  "-O$", Unset option_Osize;
-  "-timings$", Set option_timings;
-  "-mthumb$", Set option_mthumb;
-  "-marm$", Unset option_mthumb;
-  "-fsmall-data$", Integer(fun n -> option_small_data := n);
-  "-fsmall-const$", Integer(fun n -> option_small_const := n);
-  "-ffloat-const-prop$", Integer(fun n -> option_ffloatconstprop := n);
-  "-falign-functions$", Integer(fun n -> option_falignfunctions := Some n);
-  "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n);
-  "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n);
-  "-fall$", Self (fun _ ->
-              List.iter (fun r -> r := true) language_support_options);
-  "-fnone$", Self (fun _ ->
-              List.iter (fun r -> r := false) language_support_options);
+(* File arguments *)
+  Suffix ".c", Self (fun s ->
+      push_action process_c_file s; incr num_source_files);
+  Suffix ".i", Self (fun s ->
+      push_action process_i_file s; incr num_source_files);
+  Suffix ".p", Self (fun s ->
+      push_action process_i_file s; incr num_source_files);
+  Suffix ".cm", Self (fun s ->
+      push_action process_cminor_file s; incr num_source_files);
+  Suffix ".s", Self (fun s ->
+      push_action process_s_file s; incr num_source_files);
+  Suffix ".S", Self (fun s ->
+      push_action process_S_file s; incr num_source_files);
+  Suffix ".o", Self push_linker_arg;
+  Suffix ".a", Self push_linker_arg;
+  (* GCC compatibility: .o.ext files are also object files *)
+  _Regexp ".*\\.o\\.", Self push_linker_arg;
+  (* GCC compatibility: .h files can be preprocessed with -E *)
+  Suffix ".h", Self (fun s ->
+      push_action process_h_file s; incr num_source_files);
+(* Processing options *)
+  Exact "-c", Set option_c;
+  Exact "-E", Set option_E;
+  Exact "-S", Set option_S;
+  Exact "-o", String(fun s -> option_o := Some s);
+(* Preprocessing options *)
+  Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
+  Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options);
+  Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
+  Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options);
+  Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
+  Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options);
+  Prefix "-Wp,", Self (fun s ->
+    prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
+(* Language support options -- more below *)
+  Exact "-fall", Self (fun _ -> set_all language_support_options);
+  Exact "-fnone", Self (fun _ -> unset_all language_support_options);
+(* Debugging options *)
+  Exact "-g", Self (fun s -> option_g := true; push_linker_arg s);
+(* Code generation options -- more below *)
+  Exact "-O0", Self (fun _ -> unset_all optimization_options);
+  Exact "-O", Self (fun _ -> set_all optimization_options);
+  _Regexp "-O[123]$", Self (fun _ -> set_all optimization_options);
+  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);
+(* Target processor options *)
+  Exact "-mthumb", Set option_mthumb;
+  Exact "-marm", Unset option_mthumb;
+(* Assembling options *)
+  Prefix "-Wa,", Self (fun s -> assembler_options := s :: !assembler_options);
+(* Linking options *)
+  Prefix "-l", Self push_linker_arg;
+  Prefix "-L", Self push_linker_arg;
+  Prefix "-Wl,", Self push_linker_arg;
+(* Tracing options *)
+  Exact "-dparse", Set option_dparse;
+  Exact "-dc", Set option_dcmedium;
+  Exact "-dclight", Set option_dclight;
+  Exact "-dcminor", Set option_dcminor;
+  Exact "-drtl", Set option_drtl;
+  Exact "-dltl", Set option_dltl;
+  Exact "-dalloctrace", Set option_dalloctrace;
+  Exact "-dmach", Set option_dmach;
+  Exact "-dasm", Set option_dasm;
+  Exact "-sdump", Set option_sdump;
+(* General options *) 
+  Exact "-v", Set option_v;
+  Exact "-stdlib", String(fun s -> stdlib_path := s);
+  Exact "-timings", Set option_timings;
+(* Interpreter mode *)
+  Exact "-interp", Set option_interp;
+  Exact "-quiet", Self (fun _ -> Interp.trace := 0);
+  Exact "-trace", Self (fun _ -> Interp.trace := 2);
+  Exact "-random", Self (fun _ -> Interp.mode := Interp.Random);
+  Exact "-all", Self (fun _ -> Interp.mode := Interp.All)
   ]
-  @ f_opt "tailcalls" option_ftailcalls
+(* -f options: come in -f and -fno- variants *)
+(* Language support options *)
   @ f_opt "longdouble" option_flongdouble
   @ f_opt "struct-return" option_fstruct_return
   @ f_opt "bitfields" option_fbitfields
@@ -554,6 +551,12 @@ let cmdline_actions =
   @ f_opt "unprototyped" option_funprototyped
   @ f_opt "packed-structs" option_fpacked_structs
   @ f_opt "inline-asm" option_finline_asm
+(* Optimization options *)
+  @ f_opt "tailcalls" option_ftailcalls
+  @ f_opt "const-prop" option_fconstprop
+  @ f_opt "cse" option_fcse
+  @ f_opt "redundancy" option_fredundancy
+(* Code generation options *)
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
 
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 5b71a150..ee496ffa 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -92,8 +92,14 @@ Extract Constant Compopts.propagate_float_constants =>
   "fun _ -> !Clflags.option_ffloatconstprop >= 1".
 Extract Constant Compopts.generate_float_constants =>
   "fun _ -> !Clflags.option_ffloatconstprop >= 2".
-Extract Constant Compopts.eliminate_tailcalls =>
+Extract Constant Compopts.optim_tailcalls =>
   "fun _ -> !Clflags.option_ftailcalls".
+Extract Constant Compopts.optim_constprop =>
+  "fun _ -> !Clflags.option_fconstprop".
+Extract Constant Compopts.optim_CSE =>
+  "fun _ -> !Clflags.option_fcse".
+Extract Constant Compopts.optim_redundancy =>
+  "fun _ -> !Clflags.option_fredundancy".
 Extract Constant Compopts.thumb =>
   "fun _ -> !Clflags.option_mthumb".
 
diff --git a/lib/Floats.v b/lib/Floats.v
index e867cba8..f86632b9 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -92,28 +92,99 @@ Proof.
   destruct x as [[]|]; simpl; intros; discriminate.
 Qed.
 
-(** Function used to parse floats *)
+Section FP_PARSING.
 
-Program Definition build_from_parsed
-  (prec:Z) (emax:Z) (prec_gt_0 : Prec_gt_0 prec) (Hmax:prec < emax)
-  (base:positive) (intPart:positive) (expPart:Z) :=
-  match expPart return _ with
+Variables prec emax: Z.
+Context (prec_gt_0 : Prec_gt_0 prec).
+Hypothesis Hmax : (prec < emax)%Z.
+
+(** Function used to convert literals into FP numbers during parsing.
+   [intPart] is the mantissa
+   [expPart] is the exponent
+   [base] is the base for the exponent (usually 10 or 16).
+   The result is [intPart * base^expPart] rounded to the nearest FP number,
+   ties to even. *)
+
+Definition build_from_parsed (base:positive) (intPart:positive) (expPart:Z) : binary_float prec emax :=
+  match expPart with
     | Z0 =>
       binary_normalize prec emax prec_gt_0 Hmax mode_NE (Zpos intPart) Z0 false
     | Zpos p =>
       binary_normalize prec emax prec_gt_0 Hmax mode_NE ((Zpos intPart) * Zpower_pos (Zpos base) p) Z0 false
     | Zneg p =>
-      let exp := Zpower_pos (Zpos base) p in
-      match exp return 0 < exp -> _ with
-        | Zneg _ | Z0 => _
-        | Zpos p =>
-          fun _ =>
-          FF2B prec emax _ (proj1 (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE false intPart Z0 false p Z0))
-      end _
+      FF2B prec emax _ (proj1 (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE
+                                  false intPart Z0 false (Pos.pow base p) Z0))
   end.
-Next Obligation.
-  apply Zpower_pos_gt_0. reflexivity.
-Qed.
+
+Let emin := (3 - emax - prec)%Z.
+Let fexp := FLT_exp emin prec.
+
+Theorem build_from_parsed_correct:
+  forall base m e (BASE: 2 <= Zpos base),
+  let base_r := {| radix_val := Zpos base; radix_prop := Zle_imp_le_bool _ _ BASE |} in
+  let r := round radix2 fexp (round_mode mode_NE) (Z2R (Zpos m) * bpow base_r e) in
+  if Rlt_bool (Rabs r) (bpow radix2 emax) then
+     B2R _ _ (build_from_parsed base m e) = r
+  /\ is_finite _ _ (build_from_parsed base m e) = true
+  /\ Bsign _ _ (build_from_parsed base m e) = false
+  else
+    B2FF _ _ (build_from_parsed base m e) = F754_infinity false.
+Proof.
+  intros. 
+  assert (A: forall x, @F2R radix2 {| Fnum := x; Fexp := 0 |} = Z2R x).
+  { intros. unfold F2R, Fnum; simpl. ring. }
+  unfold build_from_parsed, r; destruct e. 
+- change (bpow base_r 0) with (1%R). rewrite Rmult_1_r.  
+  generalize (binary_normalize_correct _ _ _ Hmax mode_NE (Zpos m) 0 false).
+  fold emin; fold fexp. rewrite ! A.
+  destruct (Rlt_bool (Rabs (round radix2 fexp (round_mode mode_NE) (Z2R (Z.pos m))))
+                     (bpow radix2 emax)).
+  + intros (P & Q & R). split. auto. split. auto. rewrite R. rewrite Rcompare_Gt; auto. 
+    apply (Z2R_lt 0). compute; auto.
+  + intros P; rewrite P. unfold binary_overflow.
+    replace (Rlt_bool (Z2R (Z.pos m)) 0%R) with false. auto. 
+    rewrite Rlt_bool_false; auto. apply (Z2R_le 0). xomega.
+- generalize (binary_normalize_correct _ _ _ Hmax mode_NE (Zpos m * Z.pow_pos (Zpos base) p) 0 false).
+  fold emin; fold fexp. rewrite ! A.
+  assert (B: Z2R (Z.pos m * Z.pow_pos (Z.pos base) p) = (Z2R (Z.pos m) * bpow base_r (Z.pos p))%R).
+  { unfold bpow. apply Z2R_mult. }
+  rewrite B. 
+  destruct (Rlt_bool
+     (Rabs
+        (round radix2 fexp (round_mode mode_NE)
+           (Z2R (Z.pos m) * bpow base_r (Z.pos p)))) (bpow radix2 emax)).
+  + intros (P & Q & R). split. auto. split. auto. rewrite R. rewrite Rcompare_Gt; auto. 
+    apply Rmult_lt_0_compat. apply (Z2R_lt 0). xomega. apply bpow_gt_0. 
+  + intros P. rewrite P. unfold binary_overflow. 
+    replace (Rlt_bool (Z2R (Z.pos m) * bpow base_r (Z.pos p)) 0) with false.
+    auto.
+    rewrite Rlt_bool_false; auto. apply Rlt_le. apply Rmult_lt_0_compat. apply (Z2R_lt 0). xomega. apply bpow_gt_0. 
+- generalize (Bdiv_correct_aux prec emax prec_gt_0 Hmax mode_NE false m 0 false (base ^ p) 0).
+  set (f := 
+      match Fdiv_core_binary prec (Z.pos m) 0 (Z.pos (base ^ p)) 0 with
+      | (0, _, _) => F754_nan false 1
+      | (Z.pos mz0, ez, lz) =>
+          binary_round_aux prec emax mode_NE (xorb false false) mz0 ez lz
+      | (Z.neg _, _, _) => F754_nan false 1
+      end).
+  fold emin; fold fexp. rewrite ! A. unfold cond_Zopp. 
+  assert (B: (Z2R (Z.pos m) / Z2R (Z.pos (base ^ p)) =
+              Z2R (Z.pos m) * bpow base_r (Z.neg p))%R).
+  { change (Z.neg p) with (- (Z.pos p)). rewrite bpow_opp. unfold Rdiv. f_equal. f_equal. 
+    unfold bpow. f_equal. simpl. apply Pos2Z.inj_pow_pos. }
+  rewrite ! B. 
+  destruct (Rlt_bool
+     (Rabs
+        (round radix2 fexp (round_mode mode_NE)
+           (Z2R (Z.pos m) * bpow base_r (Z.neg p)))) (bpow radix2 emax)).
+  + intros (P & Q & R & S).
+    split. rewrite B2R_FF2B. exact Q. 
+    split. rewrite is_finite_FF2B. auto.
+    rewrite Bsign_FF2B. auto. 
+  + intros (P & Q). rewrite B2FF_FF2B. auto.
+Qed.
+
+End FP_PARSING.
 
 Local Notation __ := (refl_equal Datatypes.Lt).