diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-21 08:48:20 +0100 |
commit | 01e32a075023ce7b037d42d048b1904ba3d9a82b (patch) | |
tree | 2d01f3855234e6eb945b929e489232001c406592 /ia32 | |
parent | 093e0ea167fde39429bf4bd3fc693a232af0d093 (diff) | |
parent | 1fdca8371317e656cb08eaec3adb4596d6447e9b (diff) | |
download | compcert-kvx-01e32a075023ce7b037d42d048b1904ba3d9a82b.tar.gz compcert-kvx-01e32a075023ce7b037d42d048b1904ba3d9a82b.zip |
Merge branch 'master' into cleanup
Diffstat (limited to 'ia32')
-rw-r--r-- | ia32/Asmexpand.ml | 2 | ||||
-rw-r--r-- | ia32/Asmgen.v | 13 | ||||
-rw-r--r-- | ia32/Asmgenproof.v | 79 | ||||
-rw-r--r-- | ia32/PrintOp.ml | 7 |
4 files changed, 37 insertions, 64 deletions
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index 4f2bb937..5e5bbb3e 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -459,4 +459,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/ia32/Asmgen.v b/ia32/Asmgen.v index 91122898..fd0d5bc5 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -12,16 +12,9 @@ (** Translation from Mach to IA32 Asm. *) -Require Import Coqlib. -Require Import Errors. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Memdata. -Require Import Op. -Require Import Locations. -Require Import Mach. -Require Import Asm. +Require Import Coqlib Errors. +Require Import Integers Floats AST Memdata. +Require Import Op Locations Mach Asm. Open Local Scope string_scope. Open Local Scope error_monad_scope. diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 105347e7..28237237 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -12,56 +12,43 @@ (** Correctness proof for x86 generation: main proof. *) -Require Import Coqlib. -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 Mach. -Require Import Conventions. -Require Import Asm. -Require Import Asmgen. -Require Import Asmgenproof0. -Require Import Asmgenproof1. +Require Import Coqlib Errors. +Require Import Integers Floats AST Linking. +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 fb f tf, @@ -73,14 +60,6 @@ Proof. monadInv B. rewrite H0 in EQ; inv EQ; auto. Qed. -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - intros. unfold ge, tge. - apply Genv.find_var_info_transf_partial with transf_fundef. - exact TRANSF. -Qed. - (** * Properties of control flow *) Lemma transf_function_no_overflow: @@ -682,8 +661,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). @@ -866,8 +844,7 @@ Transparent destroyed_at_function_entry. 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. unfold loc_external_result. apply agree_set_other; auto. apply agree_set_mregs; auto. @@ -885,7 +862,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. @@ -893,7 +870,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. @@ -911,7 +888,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/ia32/PrintOp.ml b/ia32/PrintOp.ml index 1f7f4a65..2a80e3d4 100644 --- a/ia32/PrintOp.ml +++ b/ia32/PrintOp.ml @@ -67,8 +67,8 @@ let print_addressing 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) | Oindirectsymbol id, [] -> fprintf pp "&%s" (extern_atom id) | Ocast8signed, [r1] -> fprintf pp "int8signed(%a)" reg r1 | Ocast8unsigned, [r1] -> fprintf pp "int8unsigned(%a)" reg r1 @@ -119,6 +119,9 @@ let print_operation reg pp = function | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1 | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1 + | Onot, [r1] -> fprintf pp "not(%a)" reg r1 + | Omulhs, [r1;r2] -> fprintf pp "mulhs(%a,%a)" reg r1 reg r2 + | Omulhu, [r1;r2] -> fprintf pp "mulhu(%a,%a)" reg r1 reg r2 | Ocmp c, args -> print_condition reg pp (c, args) | _ -> fprintf pp "<bad operator>" |