Merge tag 'v3.4' into mppa_k1c

Conflicts:
	.gitignore

9 files changed, 202 insertions, 93 deletions

diff --git a/driver/Assembler.mli b/driver/Assembler.mli
index d8a4e32b..4f2e95ae 100644
--- a/driver/Assembler.mli
+++ b/driver/Assembler.mli
@@ -15,7 +15,7 @@ val assemble: string -> string -> unit
   (** From asm to object file *)
 
 val assembler_actions: (Commandline.pattern * Commandline.action) list
-  (** Commandline optins affecting the assembler *)
+  (** Commandline options affecting the assembler *)
 
 val assembler_help: string
   (** Commandline help description *)
diff --git a/driver/Commandline.ml b/driver/Commandline.ml
index f139212d..75ca1683 100644
--- a/driver/Commandline.ml
+++ b/driver/Commandline.ml
@@ -74,7 +74,7 @@ let parse_array spec argv first last =
         with Not_found -> find_action s inexact_cases in
       match optact with
       | None ->
-        let msg = sprintf "Unknown argument `%s'" s in
+        let msg = sprintf "unknown argument `%s'" s in
         raise (CmdError msg)
       | Some(Set r) ->
           r := true; parse (i+1)
@@ -86,7 +86,7 @@ let parse_array spec argv first last =
           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
+            let msg = sprintf "option `%s' expects an argument" s in
             raise (CmdError msg)
           end
       | Some(Integer fn) ->
@@ -95,19 +95,19 @@ let parse_array spec argv first last =
               try
                 int_of_string argv.(i+1)
               with Failure _ ->
-                let msg = sprintf "Argument to option `%s' must be an integer" s in
+                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
+            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
+            let msg = sprintf "option `%s' expects an argument" s in
             raise (CmdError msg)
           end
       | Some (Unit f) -> f (); parse (i+1)
@@ -131,7 +131,7 @@ let long_int_action key s =
   try
     int_of_string s
   with Failure _ ->
-    let msg =  sprintf "Argument to option `%s' must be an integer" key in
+    let msg =  sprintf "argument to option `%s' must be an integer" key in
     raise (CmdError msg)
 
 let longopt_int key f =
diff --git a/driver/Complements.v b/driver/Complements.v
index d1bea1b3..3660fff0 100644
--- a/driver/Complements.v
+++ b/driver/Complements.v
@@ -13,30 +13,20 @@
 (** Corollaries of the main semantic preservation theorem. *)
 
 Require Import Classical.
-Require Import Coqlib.
-Require Import AST.
-Require Import Integers.
-Require Import Values.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Behaviors.
-Require Import Csyntax.
-Require Import Csem.
-Require Import Cstrategy.
-Require Import Clight.
-Require Import Cminor.
-Require Import RTL.
-Require Import Asm.
+Require Import Coqlib Errors.
+Require Import AST Linking Events Smallstep Behaviors.
+Require Import Csyntax Csem Cstrategy Asm.
 Require Import Compiler.
-Require Import Errors.
 
 (** * Preservation of whole-program behaviors *)
 
 (** From the simulation diagrams proved in file [Compiler]. it follows that
   whole-program observable behaviors are preserved in the following sense.
   First, every behavior of the generated assembly code is matched by
-  a behavior of the source C code. *)
+  a behavior of the source C code.  The behavior [beh] of the assembly
+  code is either identical to the behavior [beh'] of the source C code
+  or ``improves upon'' [beh']  by replacing a ``going wrong'' behavior
+  with a more defined behavior. *)
 
 Theorem transf_c_program_preservation:
   forall p tp beh,
@@ -48,8 +38,9 @@ Proof.
   apply transf_c_program_correct; auto.
 Qed.
 
-(** As a corollary, if the source C code cannot go wrong, the behavior of the
-  generated assembly code is one of the possible behaviors of the source C code. *)
+(** As a corollary, if the source C code cannot go wrong, i.e. is free of
+  undefined behaviors, the behavior of the generated assembly code is
+  one of the possible behaviors of the source C code. *)
 
 Theorem transf_c_program_is_refinement:
   forall p tp,
@@ -124,83 +115,190 @@ Qed.
 (** * Satisfaction of specifications *)
 
 (** The second additional results shows that if all executions
-  of the source C program satisfies a given specification
-  (a predicate on the observable behavior of the program),
+  of the source C program satisfies a given specification,
   then all executions of the produced Asm program satisfy
-  this specification as well.
-
-  We first show this result for specifications that are stable
-  under the [behavior_improves] relation. *)
-
-Section SPECS_PRESERVED.
-
-Variable spec: program_behavior -> Prop.
+  this specification as well.  *)
+
+(** The specifications we consider here are sets of observable
+  behaviors, representing the good behaviors a program is expected
+  to have.  A specification can be as simple as
+  ``the program does not go wrong'' or as precise as
+  ``the program prints a prime number then terminates with code 0''.
+  As usual in Coq, sets of behaviors are represented as predicates
+  [program_behavior -> Prop]. *)
+
+Definition specification := program_behavior -> Prop.
+
+(** A program satisfies a specification if all its observable behaviors
+  are in the specification. *)
+
+Definition c_program_satisfies_spec (p: Csyntax.program) (spec: specification): Prop :=
+  forall beh,  program_behaves (Csem.semantics p) beh -> spec beh.
+Definition asm_program_satisfies_spec (p: Asm.program) (spec: specification): Prop :=
+  forall beh,  program_behaves (Asm.semantics p) beh -> spec beh.
+  
+(** It is not always the case that if the source program satisfies a
+  specification, then the generated assembly code satisfies it as
+  well.  For example, if the specification is ``the program goes wrong
+  on an undefined behavior'', a C source that goes wrong satisfies
+  this specification but can be compiled into Asm code that does not
+  go wrong and therefore does not satisfy the specification.
+
+  For this reason, we restrict ourselves to safety-enforcing specifications:
+  specifications that exclude ``going wrong'' behaviors and are satisfied
+  only by programs that execute safely. *)
+
+Definition safety_enforcing_specification (spec: specification): Prop :=
+  forall beh, spec beh -> not_wrong beh.
 
-Hypothesis spec_stable:
-  forall beh1 beh2, behavior_improves beh1 beh2 -> spec beh1 -> spec beh2.
+(** As the main result of this section, we show that CompCert
+  compilation preserves safety-enforcing specifications: 
+  any such specification that is satisfied by the source C program is
+  always satisfied by the generated assembly code. *)
 
 Theorem transf_c_program_preserves_spec:
-  forall p tp,
+  forall p tp spec,
   transf_c_program p = OK tp ->
-  (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) ->
-  (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh).
+  safety_enforcing_specification spec ->
+  c_program_satisfies_spec p spec ->
+  asm_program_satisfies_spec tp spec.
 Proof.
-  intros.
-  exploit transf_c_program_preservation; eauto. intros [beh' [A B]].
-  apply spec_stable with beh'; auto.
+  intros p tp spec TRANSF SES CSAT; red; intros beh AEXEC.
+  exploit transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR).
+  apply CSAT in CEXEC. destruct IMPR as [EQ | [t [A B]]].
+- congruence.
+- subst beh'. apply SES in CEXEC. contradiction. 
 Qed.
 
-End SPECS_PRESERVED.
+(** Safety-enforcing specifications are not the only good properties
+  of source programs that are preserved by compilation.  Another example
+  of a property that is preserved is the ``initial trace'' property:
+  all executions of the program start by producing an expected trace
+  of I/O actions, representing the good behavior expected from the program.
+  After that, the program may terminate, or continue running, or go wrong
+  on an undefined behavior.  What matters is that the program produced
+  the expected trace at the beginning of its execution.  This is a typical
+  liveness property, and it is preserved by compilation. *)
+
+Definition c_program_has_initial_trace (p: Csyntax.program) (t: trace): Prop :=
+  forall beh, program_behaves (Csem.semantics p) beh -> behavior_prefix t beh.
+Definition asm_program_has_initial_trace (p: Asm.program) (t: trace): Prop :=
+  forall beh, program_behaves (Asm.semantics p) beh -> behavior_prefix t beh.
+
+Theorem transf_c_program_preserves_initial_trace:
+  forall p tp t,
+  transf_c_program p = OK tp ->
+  c_program_has_initial_trace p t ->
+  asm_program_has_initial_trace tp t.
+Proof.
+  intros p tp t TRANSF CTRACE; red; intros beh AEXEC.
+  exploit transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR).
+  apply CTRACE in CEXEC. destruct IMPR as [EQ | [t' [A B]]].
+- congruence.
+- destruct CEXEC as (beh1' & EQ').
+  destruct B as (beh1 & EQ).
+  subst beh'. destruct beh1'; simpl in A; inv A. 
+  exists (behavior_app t0 beh1). apply behavior_app_assoc.
+Qed.
 
-(** As a corollary, we obtain preservation of safety specifications:
-  specifications that exclude "going wrong" behaviors. *)
+(** * Extension to separate compilation *)
 
-Section SAFETY_PRESERVED.
+(** The results above were given in terms of whole-program compilation.
+    They also extend to separate compilation followed by linking. *)
 
-Variable spec: program_behavior -> Prop.
+Section SEPARATE_COMPILATION.
 
-Hypothesis spec_safety:
-  forall beh, spec beh -> not_wrong beh.
+(** The source: a list of C compilation units *)
+Variable c_units: nlist Csyntax.program.
 
-Theorem transf_c_program_preserves_safety_spec:
-  forall p tp,
-  transf_c_program p = OK tp ->
-  (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) ->
-  (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh).
+(** The compiled code: a list of Asm compilation units, obtained by separate compilation *)
+Variable asm_units: nlist Asm.program.
+Hypothesis separate_compilation_succeeds: 
+  nlist_forall2 (fun cu tcu => transf_c_program cu = OK tcu) c_units asm_units.
+
+(** We assume that the source C compilation units can be linked together
+    to obtain a monolithic C program [c_program]. *)
+Variable c_program: Csyntax.program.
+Hypothesis source_linking: link_list c_units = Some c_program.
+
+(** Then, linking the Asm units obtained by separate compilation succeeds. *)
+Lemma compiled_linking_succeeds:
+  { asm_program | link_list asm_units = Some asm_program }.
 Proof.
-  intros. eapply transf_c_program_preserves_spec; eauto.
-  intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]].
-  subst beh1. elim (spec_safety _ H3).
+  destruct (link_list asm_units) eqn:E. 
+- exists p; auto.
+- exfalso. 
+  exploit separate_transf_c_program_correct; eauto. intros (a & P & Q).
+  congruence.
 Qed.
 
-End SAFETY_PRESERVED.
+(** Let asm_program be the result of linking the Asm units. *)
+Let asm_program: Asm.program := proj1_sig compiled_linking_succeeds.
+Let compiled_linking: link_list asm_units = Some asm_program := proj2_sig compiled_linking_succeeds.
+
+(** Then, [asm_program] preserves the semantics and the specifications of
+  [c_program], in the following sense.
+  First, every behavior of [asm_program] improves upon one of the possible
+  behaviors of [c_program]. *)
 
-(** We also have preservation of liveness specifications:
-  specifications that assert the existence of a prefix of the observable
-  trace satisfying some conditions. *)
+Theorem separate_transf_c_program_preservation:
+  forall beh,
+  program_behaves (Asm.semantics asm_program) beh ->
+  exists beh', program_behaves (Csem.semantics c_program) beh' /\ behavior_improves beh' beh.
+Proof.
+  intros. exploit separate_transf_c_program_correct; eauto. intros (a & P & Q).
+  assert (a = asm_program) by congruence. subst a. 
+  eapply backward_simulation_behavior_improves; eauto.
+Qed.
 
-Section LIVENESS_PRESERVED.
+(** As a corollary, if [c_program] is free of undefined behaviors, 
+  the behavior of [asm_program] is one of the possible behaviors of [c_program]. *)
 
-Variable spec: trace -> Prop.
+Theorem separate_transf_c_program_is_refinement:
+  (forall beh, program_behaves (Csem.semantics c_program) beh -> not_wrong beh) ->
+  (forall beh, program_behaves (Asm.semantics asm_program) beh -> program_behaves (Csem.semantics c_program) beh).
+Proof.
+  intros. exploit separate_transf_c_program_preservation; eauto. intros (beh' & P & Q).
+  assert (not_wrong beh') by auto.
+  inv Q.
+- auto.
+- destruct H2 as (t & U & V). subst beh'. elim H1. 
+Qed.
 
-Definition liveness_spec_satisfied (b: program_behavior) : Prop :=
-  exists t, behavior_prefix t b /\ spec t.
+(** We now show that if all executions of [c_program] satisfy a specification,
+  then all executions of [asm_program] also satisfy the specification, provided
+  the specification is of the safety-enforcing kind. *)
 
-Theorem transf_c_program_preserves_liveness_spec:
-  forall p tp,
-  transf_c_program p = OK tp ->
-  (forall beh, program_behaves (Csem.semantics p) beh -> liveness_spec_satisfied beh) ->
-  (forall beh, program_behaves (Asm.semantics tp) beh -> liveness_spec_satisfied beh).
+Theorem separate_transf_c_program_preserves_spec:
+  forall spec,
+  safety_enforcing_specification spec ->
+  c_program_satisfies_spec c_program spec ->
+  asm_program_satisfies_spec asm_program spec.
 Proof.
-  intros. eapply transf_c_program_preserves_spec; eauto.
-  intros. destruct H3 as [t1 [A B]]. destruct H2.
-  subst. exists t1; auto.
-  destruct H2 as [t [C D]]. subst.
-  destruct A as [b1 E]. destruct D as [b2 F].
-  destruct b1; simpl in E; inv E.
-  exists t1; split; auto.
-  exists (behavior_app t0 b2); apply behavior_app_assoc.
+  intros spec SES CSAT; red; intros beh AEXEC.
+  exploit separate_transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR).
+  apply CSAT in CEXEC. destruct IMPR as [EQ | [t [A B]]].
+- congruence.
+- subst beh'. apply SES in CEXEC. contradiction. 
 Qed.
 
-End LIVENESS_PRESERVED.
+(** As another corollary of [separate_transf_c_program_preservation],
+  if all executions of [c_program] have a trace [t] as initial trace,
+  so do all executions of [asm_program]. *)
+
+Theorem separate_transf_c_program_preserves_initial_trace:
+  forall t,
+  c_program_has_initial_trace c_program t ->
+  asm_program_has_initial_trace asm_program t.
+Proof.
+  intros t CTRACE; red; intros beh AEXEC.
+  exploit separate_transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR).
+  apply CTRACE in CEXEC. destruct IMPR as [EQ | [t' [A B]]].
+- congruence.
+- destruct CEXEC as (beh1' & EQ').
+  destruct B as (beh1 & EQ).
+  subst beh'. destruct beh1'; simpl in A; inv A. 
+  exists (behavior_app t0 beh1). apply behavior_app_assoc.
+Qed.
 
+End SEPARATE_COMPILATION.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 0ad820ea..8ab8557c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -404,7 +404,7 @@ let _ =
     parse_cmdline cmdline_actions;
     DebugInit.init (); (* Initialize the debug functions *)
     if nolink () && !option_o <> None && !num_source_files >= 2 then
-      fatal_error no_loc "Ambiguous '-o' option (multiple source files)";
+      fatal_error no_loc "ambiguous '-o' option (multiple source files)";
     if !num_input_files = 0 then
       fatal_error no_loc "no input file";
     let linker_args = time "Total compilation time" perform_actions () in
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml
index ccc3d00d..5b2d792e 100644
--- a/driver/Driveraux.ml
+++ b/driver/Driveraux.ml
@@ -47,7 +47,7 @@ let command stdout args =
     match status with
     | Unix.WEXITED rc -> rc
     | Unix.WSIGNALED n | Unix.WSTOPPED n ->
-        error no_loc "Command '%s' killed on a signal." argv.(0); -1
+        error no_loc "command '%s' killed on a signal." argv.(0); -1
   with Unix.Unix_error(err, fn, param) ->
     error no_loc "executing '%s': %s: %s %s"
             argv.(0) fn (Unix.error_message err) param;
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index db84a9f9..b29bb7f3 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -17,6 +17,15 @@ open Driveraux
 
 (* Common frontend functions between clightgen and ccomp *)
 
+let predefined_macros =
+  [
+    "-D__COMPCERT__";
+    "-U__STDC_IEC_559_COMPLEX__";
+    "-D__STDC_NO_ATOMICS__";
+    "-D__STDC_NO_COMPLEX__";
+    "-D__STDC_NO_THREADS__";
+    "-D__STDC_NO_VLA__"
+  ]
 
 (* From C to preprocessed C *)
 
@@ -26,7 +35,7 @@ let preprocess ifile ofile =
     if ofile = "-" then None else Some ofile in
   let cmd = List.concat [
     Configuration.prepro;
-    ["-D__COMPCERT__"];
+    predefined_macros;
     (if !Clflags.use_standard_headers
      then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ]
      else []);
@@ -64,10 +73,12 @@ let parse_c_file sourcename ifile =
 let init () =
   Machine.config:=
     begin match Configuration.arch with
-    | "powerpc" -> if Configuration.gnu_toolchain
-                   then if Configuration.abi = "linux"
-                   then Machine.ppc_32_linux_bigendian
-                   else Machine.ppc_32_bigendian
+    | "powerpc" -> if Configuration.model = "e5500" || Configuration.model = "ppc64"
+                   then if Configuration.abi = "linux" then Machine.ppc_32_r64_linux_bigendian
+                   else if Configuration.gnu_toolchain then Machine.ppc_32_r64_bigendian
+                   else Machine.ppc_32_r64_diab_bigendian
+                   else if Configuration.abi = "linux" then Machine.ppc_32_linux_bigendian
+                   else if Configuration.gnu_toolchain then Machine.ppc_32_bigendian
                    else Machine.ppc_32_diab_bigendian
     | "arm"     -> if Configuration.is_big_endian
                    then Machine.arm_bigendian
@@ -116,7 +127,7 @@ let gnu_prepro_actions = [
   Exact "-imacros", String (gnu_prepro_opt_key "-imacros");
   Exact "-idirafter", String (gnu_prepro_opt_key "-idirafter");
   Exact "-isystem", String (gnu_prepro_opt_key "-isystem");
-  Exact "-iquote", String (gnu_prepro_opt_key "-iquore");
+  Exact "-iquote", String (gnu_prepro_opt_key "-iquote");
   Exact "-P", Self gnu_prepro_opt;
   Exact "-C", Self gnu_prepro_opt;
   Exact "-CC", Self gnu_prepro_opt;]
diff --git a/driver/Frontend.mli b/driver/Frontend.mli
index 39f0e612..a18c2704 100644
--- a/driver/Frontend.mli
+++ b/driver/Frontend.mli
@@ -18,7 +18,7 @@ val parse_c_file: string -> string -> Csyntax.coq_function Ctypes.program
   (** From preprocessed C to Csyntax *)
 
 val prepro_actions: (Commandline.pattern * Commandline.action) list
-  (** Commandline optins affecting the frontend *)
+  (** Commandline options affecting the frontend *)
 
 val prepro_help: string
   (** Commandline help description *)
diff --git a/driver/Linker.ml b/driver/Linker.ml
index 6e6ad6b4..d6e1d384 100644
--- a/driver/Linker.ml
+++ b/driver/Linker.ml
@@ -86,4 +86,4 @@ let linker_actions =
       push_linker_arg s);
     Prefix "-Wl,", Self push_linker_arg;
     Prefix "-WUl,", Self (fun s -> List.iter push_linker_arg (explode_comma_option s));
-    Exact "-u", Self push_linker_arg;]
+    Exact "-u", String (fun s -> push_linker_arg "-u"; push_linker_arg s);]
diff --git a/driver/Linker.mli b/driver/Linker.mli
index 3b92da05..dd034543 100644
--- a/driver/Linker.mli
+++ b/driver/Linker.mli
@@ -12,10 +12,10 @@
 (* *********************************************************************)
 
 val linker: string -> string list -> unit
-  (** Link files into executbale *)
+  (** Link files into executable *)
 
 val linker_actions: (Commandline.pattern * Commandline.action) list
-  (** Commandline optins affecting the assembler *)
+  (** Commandline options affecting the assembler *)
 
 val linker_help: string
   (** Commandline help description *)