Merge branch 'master' into pure-makefiles

5 files changed, 117 insertions, 91 deletions

diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index eba710a1..57d7de4a 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -48,6 +48,14 @@ Proof.
   exact TRANSF. 
 Qed.
 
+Lemma public_preserved:
+  forall id, Genv.public_symbol tge id = Genv.public_symbol ge id.
+Proof.
+  intros. unfold ge, tge. 
+  apply Genv.public_symbol_transf_partial with transf_fundef.
+  exact TRANSF. 
+Qed.
+
 Lemma functions_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
@@ -672,7 +680,7 @@ Opaque loadind.
   eapply exec_step_builtin. eauto. eauto.
   eapply find_instr_tail; eauto.
   eapply external_call_symbols_preserved'; eauto.
-  exact symbols_preserved. exact varinfo_preserved.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   eauto.
   econstructor; eauto.
   instantiate (2 := tf); instantiate (1 := x).
@@ -699,7 +707,7 @@ Opaque loadind.
   eapply exec_step_annot. eauto. eauto.
   eapply find_instr_tail; eauto. eauto.
   eapply external_call_symbols_preserved'; eauto.
-  exact symbols_preserved. exact varinfo_preserved.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   eapply match_states_intro with (ep := false); eauto with coqlib.
   unfold nextinstr. rewrite Pregmap.gss. 
   rewrite <- H1; simpl. econstructor; eauto.
@@ -876,7 +884,7 @@ Transparent destroyed_at_function_entry.
   left; econstructor; split.
   apply plus_one. eapply exec_step_external; eauto. 
   eapply external_call_symbols_preserved'; eauto. 
-  exact symbols_preserved. exact varinfo_preserved.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   econstructor; eauto.
   unfold loc_external_result.
   apply agree_set_other; auto. apply agree_set_mregs; auto.
@@ -920,7 +928,7 @@ Theorem transf_program_correct:
   forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
   eapply forward_simulation_star with (measure := measure).
-  eexact symbols_preserved.
+  eexact public_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact step_simulation.
diff --git a/ia32/Op.v b/ia32/Op.v
index 14e4cbb1..846d094f 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -659,6 +659,23 @@ Proof.
   destruct c; simpl; try congruence. reflexivity. 
 Qed.
 
+(** Global variables mentioned in an operation or addressing mode *)
+
+Definition globals_addressing (addr: addressing) : list ident :=
+  match addr with
+  | Aglobal s n => s :: nil
+  | Abased s n => s :: nil
+  | Abasedscaled sc s n => s :: nil
+  | _ => nil
+  end.
+
+Definition globals_operation (op: operation) : list ident :=
+  match op with
+  | Oindirectsymbol s => s :: nil
+  | Olea addr => globals_addressing addr
+  | _ => nil
+  end.
+
 (** * Invariance and compatibility properties. *)
 
 (** [eval_operation] and [eval_addressing] depend on a global environment
@@ -699,14 +716,11 @@ End GENV_TRANSF.
 
 Section EVAL_COMPAT.
 
-Variable F V: Type.
-Variable genv: Genv.t F V.
+Variable F1 F2 V1 V2: Type.
+Variable ge1: Genv.t F1 V1.
+Variable ge2: Genv.t F2 V2.
 Variable f: meminj.
 
-Hypothesis symbol_address_inj: 
-  forall id ofs,
-  val_inject f (Genv.symbol_address genv id ofs) (Genv.symbol_address genv id ofs).
-
 Variable m1: mem.
 Variable m2: mem.
 
@@ -781,29 +795,37 @@ Ltac TrivialExists :=
 
 Lemma eval_addressing_inj:
   forall addr sp1 vl1 sp2 vl2 v1,
+  (forall id ofs,
+      In id (globals_addressing addr) ->
+      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
   val_inject f sp1 sp2 ->
   val_list_inject f vl1 vl2 ->
-  eval_addressing genv sp1 addr vl1 = Some v1 ->
-  exists v2, eval_addressing genv sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
+  eval_addressing ge1 sp1 addr vl1 = Some v1 ->
+  exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ val_inject f v1 v2.
 Proof.
-  intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
+  intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists.
   apply Values.val_add_inject; auto.
   apply Values.val_add_inject; auto. apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto. inv H4; simpl; auto.
-  apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H2; simpl; auto.
-  apply Values.val_add_inject; auto.
-  apply Values.val_add_inject; auto. inv H4; simpl; auto.
+  apply Values.val_add_inject; auto. inv H5; simpl; auto.
+  apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. inv H3; simpl; auto.
+  apply H; simpl; auto.
+  apply Values.val_add_inject; auto. apply H; simpl; auto.
+  apply Values.val_add_inject; auto. apply H; simpl; auto. inv H5; simpl; auto.
   apply Values.val_add_inject; auto.
 Qed.
 
 Lemma eval_operation_inj:
   forall op sp1 vl1 sp2 vl2 v1,
+  (forall id ofs,
+      In id (globals_operation op) ->
+      val_inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
   val_inject f sp1 sp2 ->
   val_list_inject f vl1 vl2 ->
-  eval_operation genv sp1 op vl1 m1 = Some v1 ->
-  exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
+  eval_operation ge1 sp1 op vl1 m1 = Some v1 ->
+  exists v2, eval_operation ge2 sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
 Proof.
-  intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
+  intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
+  apply GL; simpl; auto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
@@ -951,13 +973,14 @@ Proof.
           eval_operation genv sp op vl2 m2 = Some v2
           /\ val_inject (fun b => Some(b, 0)) v1 v2).
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
-  intros. rewrite <- val_inject_lessdef; auto.
   apply valid_pointer_extends; auto.
   apply weak_valid_pointer_extends; auto.
   apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
-  rewrite <- val_inject_lessdef; auto.
-  eauto. auto. 
+  intros. apply val_inject_lessdef. auto. 
+  apply val_inject_lessdef; auto.
+  eauto. 
+  auto.
   destruct H2 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto. 
 Qed.
 
@@ -1026,7 +1049,7 @@ Proof.
   intros. 
   rewrite eval_shift_stack_addressing. simpl.
   eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto.
-  exact symbol_address_inject.
+  intros. apply symbol_address_inject.
 Qed.
 
 Lemma eval_operation_inject:
@@ -1041,11 +1064,11 @@ Proof.
   intros. 
   rewrite eval_shift_stack_operation. simpl.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
-  exact symbol_address_inject.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
+  intros. apply symbol_address_inject. 
 Qed.
 
 End EVAL_INJECT.
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 5c84af6b..649fd292 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -57,7 +57,7 @@ let preg oc = function
 
 
 (* System dependend printer functions *)
-module type SYSTEM=
+module type SYSTEM =
     sig
       val raw_symbol: out_channel -> string -> unit
       val symbol: out_channel -> P.t -> unit
@@ -69,6 +69,8 @@ module type SYSTEM=
       val print_fun_info: out_channel -> P.t -> unit
       val print_var_info: out_channel -> P.t -> unit
       val print_epilogue: out_channel -> unit
+      val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit
+      val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit
     end
 
 (* Printer functions for cygwin *)
@@ -86,8 +88,10 @@ module Cygwin_System =
         
     let name_of_section = function
       | Section_text -> ".text"
-      | Section_data _ | Section_small_data _ -> ".data"
-      | Section_const  | Section_small_const -> ".section	.rdata,\"dr\""
+      | Section_data i | Section_small_data i ->
+          if i then ".data" else "COMM"
+      | Section_const i | Section_small_const i ->
+          if i then ".section	.rdata,\"dr\"" else "COMM"
       | Section_string -> ".section	.rdata,\"dr\""
       | Section_literal -> ".section	.rdata,\"dr\""
       | Section_jumptable -> ".text"
@@ -108,6 +112,14 @@ module Cygwin_System =
     let print_var_info _ _ = ()
 
     let print_epilogue _ = ()
+
+    let print_comm_decl oc name sz al =
+      fprintf oc "	.comm	%a, %s, %d\n" symbol name (Z.to_string sz) al
+
+    let print_lcomm_decl oc name sz al =
+      fprintf oc "	.local	%a\n" symbol name;
+      print_comm_decl oc name sz al
+
   end:SYSTEM)
 
 (* Printer functions for ELF *)
@@ -125,8 +137,10 @@ module ELF_System =
 
     let name_of_section = function
       | Section_text -> ".text"
-      | Section_data i | Section_small_data i -> if i then ".data" else "COMM"
-      | Section_const | Section_small_const -> ".section	.rodata"
+      | Section_data i | Section_small_data i ->
+          if i then ".data" else "COMM"
+      | Section_const i | Section_small_const i ->
+          if i then ".section	.rodata" else "COMM"
       | Section_string -> ".section	.rodata"
       | Section_literal -> ".section	.rodata.cst8,\"aM\",@progbits,8"
       | Section_jumptable -> ".text"
@@ -151,6 +165,14 @@ module ELF_System =
       fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
 
     let print_epilogue _ = ()
+
+    let print_comm_decl oc name sz al =
+      fprintf oc "	.comm	%a, %s, %d\n" symbol name (Z.to_string sz) al
+
+    let print_lcomm_decl oc name sz al =
+      fprintf oc "	.local	%a\n" symbol name;
+      print_comm_decl oc name sz al
+
   end:SYSTEM)
 
 (* Printer functions for MacOS *)
@@ -161,15 +183,17 @@ module MacOS_System =
      fprintf oc "_%s" s
 
     let symbol oc symb =
-      fprintf oc "%s" (extern_atom symb)
+      fprintf oc "_%s" (extern_atom symb)
 
     let label oc lbl =
       fprintf oc "L%d" lbl
 
     let name_of_section = function
       | Section_text -> ".text"
-      | Section_data _ | Section_small_data _ -> ".data"
-      | Section_const  | Section_small_const -> ".const"
+      | Section_data i | Section_small_data i ->
+          if i then ".data" else "COMM"
+      | Section_const i  | Section_small_const i ->
+          if i then ".const" else "COMM"
       | Section_string -> ".const"
       | Section_literal -> ".literal8"
       | Section_jumptable -> ".const"
@@ -206,7 +230,16 @@ module MacOS_System =
           fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s;
           fprintf oc "	.indirect_symbol %a\n" raw_symbol s;
           fprintf oc "	.long	0\n")
-        !indirect_symbols
+        !indirect_symbols;
+      indirect_symbols := StringSet.empty
+
+    let print_comm_decl oc name sz al =
+      fprintf oc "	.comm	%a, %s, %d\n"
+                 symbol name (Z.to_string sz) (log2 al)
+
+    let print_lcomm_decl oc name sz al =
+      fprintf oc "	.lcomm	%a, %s, %d\n"
+                 symbol name (Z.to_string sz) (log2 al)
 
   end:SYSTEM)
 
@@ -638,7 +671,6 @@ let print_builtin_inline oc name args res =
 let float64_literals : (int * int64) list ref = ref []
 let float32_literals : (int * int32) list ref = ref []
 let jumptables : (int * label list) list ref = ref []
-let indirect_symbols : StringSet.t ref = ref StringSet.empty
 
 (* Reminder on AT&T syntax: op source, dest *)
 
@@ -996,12 +1028,9 @@ let print_var oc name v =
       end else begin
         let sz =
           match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
-        if C2C.atom_is_static name then
-          fprintf oc "	.local	%a\n" symbol name;
-        fprintf oc "	.comm	%a, %s, %d\n"
-          symbol name
-          (Z.to_string sz)
-          align
+        if C2C.atom_is_static name
+        then Target.print_lcomm_decl oc name sz align
+        else Target.print_comm_decl oc name sz align
       end
 
 let print_globdef oc (name, gdef) =
@@ -1032,7 +1061,8 @@ let print_program oc p =
   Hashtbl.clear Printer.filename_num;
   List.iter (Printer.print_globdef oc) p.prog_defs;
   if !Printer.need_masks then begin
-    Printer.section oc Section_const;  (* not Section_literal because not 8-bytes *)
+    Printer.section oc (Section_const true);
+                        (* not Section_literal because not 8-bytes *)
     Target.print_align oc 16;
     fprintf oc "%a:	.quad   0x8000000000000000, 0\n"
                Target.raw_symbol "__negd_mask";
@@ -1042,4 +1072,6 @@ let print_program oc p =
                Target.raw_symbol "__negs_mask";
     fprintf oc "%a:	.long   0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n"
                Target.raw_symbol "__abss_mask"
-  end
+  end;
+  Target.print_epilogue oc
+
diff --git a/ia32/Unusedglob1.ml b/ia32/Unusedglob1.ml
deleted file mode 100644
index eb0298bb..00000000
--- a/ia32/Unusedglob1.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Identifiers referenced from an IA32 Asm instruction *)
-
-open Datatypes
-open AST
-open Asm
-
-let referenced_addr (Addrmode(base, ofs, const)) =
-  match const with
-  | Coq_inl n -> []
-  | Coq_inr(s, ofs) -> [s]
-
-let referenced_builtin ef =
-  match ef with
-  | EF_vload_global(chunk, id, ofs) -> [id]
-  | EF_vstore_global(chunk, id, ofs) -> [id]
-  | _ -> []
-
-let referenced_instr = function
-  | Pmov_rm (_, a) | Pmov_mr (a, _)
-  | Pmov_rm_a (_, a) | Pmov_mr_a (a, _)
-  | Pmovsd_fm (_, a) | Pmovsd_mf(a, _)
-  | Pmovss_fm (_, a) | Pmovss_mf(a, _)
-  | Pfldl_m a | Pflds_m a | Pfstpl_m a | Pfstps_m a
-  | Pmovb_mr (a, _) | Pmovw_mr (a, _)
-  | Pmovzb_rm (_, a) | Pmovsb_rm (_, a)
-  | Pmovzw_rm (_, a) | Pmovsw_rm (_, a)
-  | Plea (_, a) -> referenced_addr a
-  | Pjmp_s(s, _) -> [s]
-  | Pcall_s(s, _) -> [s]
-  | Pbuiltin(ef, args, res) -> referenced_builtin ef
-  | _ -> []
-
-let code_of_function f = f.fn_code
-
diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v
index 874c2be3..53013337 100644
--- a/ia32/ValueAOp.v
+++ b/ia32/ValueAOp.v
@@ -58,7 +58,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ointconst n, nil => I n
   | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop
   | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop
-  | Oindirectsymbol id, nil => Ptr (Gl id Int.zero)
+  | Oindirectsymbol id, nil => Ifptr (Gl id Int.zero)
   | Ocast8signed, v1 :: nil => sign_ext 8 v1
   | Ocast8unsigned, v1 :: nil => zero_ext 8 v1
   | Ocast16signed, v1 :: nil => sign_ext 16 v1
@@ -145,7 +145,16 @@ Proof.
   intros; apply symbol_address_sound; apply GENV.
 Qed.
 
-Hint Resolve symbol_address_sound: va.
+Lemma symbol_address_sound_2:
+  forall id ofs,
+  vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)).
+Proof.
+  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F. 
+  constructor. constructor. apply GENV; auto.
+  constructor.
+Qed.
+
+Hint Resolve symbol_address_sound symbol_address_sound_2: va.
 
 Ltac InvHyps :=
   match goal with