Merge branch 'master' into cleanup

4 files changed, 38 insertions, 64 deletions

diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index e114ab28..79f06991 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -439,4 +439,4 @@ let expand_fundef id = function
       Errors.OK (External ef)
 
 let expand_program (p: Asm.program) : Asm.program Errors.res =
-  AST.transform_partial_ident_program expand_fundef p
+  AST.transform_partial_program2 expand_fundef (fun id v -> Errors.OK v) p
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 7a29e4a5..eb52d16e 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -12,76 +12,52 @@
 
 (** Correctness proof for ARM code generation: main proof. *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import Errors.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Op.
-Require Import Locations.
-Require Import Conventions.
-Require Import Mach.
-Require Import Compopts.
-Require Import Asm.
-Require Import Asmgen.
-Require Import Asmgenproof0.
-Require Import Asmgenproof1.
+Require Import Coqlib Errors.
+Require Import Integers Floats AST Linking Compopts.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Op Locations Mach Conventions Asm.
+Require Import Asmgen Asmgenproof0 Asmgenproof1.
+
+Definition match_prog (p: Mach.program) (tp: Asm.program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. eapply match_transform_partial_program; eauto.
+Qed.
 
 Section PRESERVATION.
 
 Variable prog: Mach.program.
 Variable tprog: Asm.program.
-Hypothesis TRANSF: transf_program prog = Errors.OK tprog.
-
+Hypothesis TRANSF: match_prog prog tprog.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
-  forall id, Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof.
-  intros. unfold ge, tge.
-  apply Genv.find_symbol_transf_partial with transf_fundef.
-  exact TRANSF.
-Qed.
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof (Genv.find_symbol_match TRANSF).
 
-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 senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSF).
 
 Lemma functions_translated:
   forall b f,
   Genv.find_funct_ptr ge b = Some f ->
-  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Errors.OK tf.
-Proof
-  (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF).
+  exists tf,
+  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
 Lemma functions_transl:
-  forall f b tf,
-  Genv.find_funct_ptr ge b = Some (Internal f) ->
+  forall fb f tf,
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
   transf_function f = OK tf ->
-  Genv.find_funct_ptr tge b = Some (Internal tf).
-Proof.
-  intros.
-  destruct (functions_translated _ _ H) as [tf' [A B]].
-  rewrite A. monadInv B. f_equal. congruence.
-Qed.
-
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+  Genv.find_funct_ptr tge fb = Some (Internal tf).
 Proof.
-  intros. unfold ge, tge.
-  apply Genv.find_var_info_transf_partial with transf_fundef.
-  exact TRANSF.
+  intros. exploit functions_translated; eauto. intros [tf' [A B]].
+  monadInv B. rewrite H0 in EQ; inv EQ; auto.
 Qed.
 
 (** * Properties of control flow *)
@@ -758,8 +734,7 @@ Opaque loadind.
   eapply find_instr_tail; eauto.
   erewrite <- sp_val by eauto.
   eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   eauto.
   econstructor; eauto.
   instantiate (2 := tf); instantiate (1 := x).
@@ -921,8 +896,7 @@ Opaque loadind.
   intros [res' [m2' [P [Q [R S]]]]].
   left; econstructor; split.
   apply plus_one. eapply exec_step_external; eauto.
-  eapply external_call_symbols_preserved'; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved'; eauto. apply senv_preserved.
   econstructor; eauto.
   apply agree_set_other; auto with asmgen.
   eapply agree_set_mregs; eauto.
@@ -940,7 +914,7 @@ Proof.
   intros. inversion H. unfold ge0 in *.
   econstructor; split.
   econstructor.
-  eapply Genv.init_mem_transf_partial; eauto.
+  eapply (Genv.init_mem_transf_partial TRANSF); eauto.
   replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero)
      with (Vptr fb Int.zero).
   econstructor; eauto.
@@ -948,7 +922,7 @@ Proof.
   apply Mem.extends_refl.
   split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto.
   unfold Genv.symbol_address.
-  rewrite (transform_partial_program_main _ _ TRANSF).
+  rewrite (match_program_main TRANSF).
   rewrite symbols_preserved.
   unfold ge; rewrite H1. auto.
 Qed.
@@ -967,7 +941,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 public_preserved.
+  apply senv_preserved.
   eexact transf_initial_states.
   eexact transf_final_states.
   exact step_simulation.
diff --git a/arm/PrintOp.ml b/arm/PrintOp.ml
index 886f6de3..71e1dfc3 100644
--- a/arm/PrintOp.ml
+++ b/arm/PrintOp.ml
@@ -66,8 +66,8 @@ let print_condition reg pp = function
 let print_operation reg pp = function
   | Omove, [r1] -> reg pp r1
   | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n)
-  | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n)
-  | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n)
+  | Ofloatconst n, [] -> fprintf pp "%.15F" (camlfloat_of_coqfloat n)
+  | Osingleconst n, [] -> fprintf pp "%.15Ff" (camlfloat_of_coqfloat32 n)
   | Oaddrsymbol(id, ofs), [] ->
       fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs)
   | Oaddrstack ofs, [] ->
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 87f1057c..bfe11555 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -593,7 +593,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Pflid(r1, f) ->
           let f = camlint64_of_coqint(Floats.Float.to_bits f) in
           if Opt.vfpv3 && is_immediate_float64 f then begin
-            fprintf oc "	vmov.f64 %a, #%F\n"
+            fprintf oc "	vmov.f64 %a, #%.15F\n"
               freg r1 (Int64.float_of_bits f); 1
               (* immediate floats have at most 4 bits of fraction, so they
                  should print exactly with OCaml's F decimal format. *)
@@ -645,7 +645,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
       | Pflis(r1, f) ->
           let f = camlint_of_coqint(Floats.Float32.to_bits f) in
           if Opt.vfpv3 && is_immediate_float32 f then begin
-            fprintf oc "	vmov.f32 %a, #%F\n"
+            fprintf oc "	vmov.f32 %a, #%.15F\n"
               freg_single r1 (Int32.float_of_bits f); 1
               (* immediate floats have at most 4 bits of fraction, so they
                  should print exactly with OCaml's F decimal format. *)