From 2b5f5cb0bb6d8dbf302ab6d84c27eda30252912d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:23:18 +0100 Subject: Add support for EF_runtime externals Also: in Events, use Senv.equiv to state invariance wrt changes of global envs. --- ia32/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ia32') diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index 7ca31902..61beeb00 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -460,4 +460,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 -- cgit From e4723d142aa7b1229cdf5989340342d7c5ce870c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:31:26 +0100 Subject: Update the back-end proofs to the new linking framework. --- ia32/Asmgen.v | 13 +++------ ia32/Asmgenproof.v | 79 +++++++++++++++++++----------------------------------- 2 files changed, 31 insertions(+), 61 deletions(-) (limited to 'ia32') 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. -- cgit