diff options
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Asmexpand.ml | 2 | ||||
-rw-r--r-- | arm/Asmgenproof.v | 92 | ||||
-rw-r--r-- | arm/PrintOp.ml | 4 | ||||
-rw-r--r-- | arm/TargetPrinter.ml | 4 |
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. *) |