From 341d1123c475e3fb73032e2f6c6a337c4e2c59c1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 16 Dec 2020 14:48:50 +0100 Subject: intermediatet commit before builtins --- aarch64/Asmblockgen.v | 15 +- aarch64/Asmblockgenproof.v | 1049 ++++++++++++++++++++++++- aarch64/Asmblockgenproof0.v | 387 +++++++++ aarch64/Asmblockgenproof1.v | 1834 +++++++++++++++++++++++++++++++++++++++++++ aarch64/Asmblockprops.v | 104 +-- 5 files changed, 3291 insertions(+), 98 deletions(-) create mode 100644 aarch64/Asmblockgenproof1.v (limited to 'aarch64') diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 96e7db4b..e260bd69 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -389,9 +389,9 @@ Definition arith_extended Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode := if Int.eq n Int.zero then Pmov rd r1 ::bi k - else if Int.eq n Int.one then +(* else if Int.eq n Int.one then Padd W (SOlsr (Int.repr 31)) X16 r1 r1 ::bi - Porr W (SOasr n) rd XZR X16 ::bi k + Porr W (SOasr n) rd XZR X16 ::bi k *) else Porr W (SOasr (Int.repr 31)) X16 XZR r1 ::bi Padd W (SOlsr (Int.sub Int.iwordsize n)) X16 r1 X16 ::bi @@ -400,9 +400,9 @@ Definition shrx32 (rd r1: ireg) (n: int) (k: bcode) : bcode := Definition shrx64 (rd r1: ireg) (n: int) (k: bcode) : bcode := if Int.eq n Int.zero then Pmov rd r1 ::bi k - else if Int.eq n Int.one then +(* else if Int.eq n Int.one then Padd X (SOlsr (Int.repr 63)) X16 r1 r1 ::bi - Porr X (SOasr n) rd XZR X16 ::bi k + Porr X (SOasr n) rd XZR X16 ::bi k *) else Porr X (SOasr (Int.repr 63)) X16 XZR r1 ::bi Padd X (SOlsr (Int.sub Int64.iwordsize' n)) X16 r1 X16 ::bi @@ -1141,8 +1141,11 @@ Definition transl_instr_basic (f: Machblock.function) (i: Machblock.basic_inst) OK (if ep then c else loadptr_bc XSP f.(fn_link_ofs) X29 c) | MBop op args res => transl_op op args res k - | MBload _ chunk addr args dst => - transl_load chunk addr args dst k + | MBload t chunk addr args dst => + match t with + | TRAP => transl_load chunk addr args dst k + | NOTRAP => Error(msg "Asmgenblock.transl_instr_basic: NOTRAP load not supported in aarch64.") + end | MBstore chunk addr args src => transl_store chunk addr args src k end. diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index 33acc110..55f50b7a 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -1,12 +1,24 @@ -(** Correctness proof for aarch64/Asmblock generation: main proof. -CURRENTLY A STUB ! -*) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import Coqlib Errors. Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock IterList. -Require Import Asmblockgen Asmblockgenproof0. +Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops. Module MB := Machblock. Module AB := Asmblock. @@ -44,13 +56,16 @@ Lemma functions_translated: Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. Proof (Genv.find_funct_ptr_transf_partial TRANSF). -Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), - Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs. - -(*Lemma functions_bound_max_pos: forall fb f, +Lemma functions_transl: + forall fb f tf, Genv.find_funct_ptr ge fb = Some (Internal f) -> - (max_pos next f) <= Ptrofs.max_unsigned. -Admitted.*) + transf_function f = OK tf -> + Genv.find_funct_ptr tge fb = Some (Internal tf). +Proof. + intros. exploit functions_translated; eauto. intros [tf' [A B]]. + monadInv B. unfold transf_function in H0. monadInv H0. + destruct zlt; try discriminate. rewrite EQ in EQ0. inv EQ0; inv EQ1; auto. +Qed. Lemma transf_function_no_overflow: forall f tf, @@ -60,6 +75,14 @@ Proof. omega. Qed. +Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), + Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs. + +(*Lemma functions_bound_max_pos: forall fb f, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + (max_pos next f) <= Ptrofs.max_unsigned. +Admitted.*) + (** * Proof of semantic preservation *) (** Semantic preservation is proved using a complex simulation diagram @@ -118,6 +141,183 @@ Inductive match_states: Machblock.state -> Asm.state -> Prop := match_states (Machblock.Returnstate s ms m) (Asm.State rs m'). +Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *) + +Lemma cons_bblocks_label: + forall hd bdy ex tbb tc, + cons_bblocks hd bdy ex = tbb::tc -> + header tbb = hd. +Proof. + intros until tc. intros CONSB. unfold cons_bblocks in CONSB. + destruct ex; try destruct bdy; try destruct c; try destruct i. + all: inv CONSB; simpl; auto. +Qed. + +Lemma cons_bblocks_label2: + forall hd bdy ex tbb1 tbb2, + cons_bblocks hd bdy ex = tbb1::tbb2::nil -> + header tbb2 = nil. +Proof. + intros until tbb2. intros CONSB. unfold cons_bblocks in CONSB. + destruct ex; try destruct bdy; try destruct c; try destruct i. + all: inv CONSB; simpl; auto. +Qed. + +Remark in_dec_transl: + forall lbl hd, + (if in_dec lbl hd then true else false) = (if MB.in_dec lbl hd then true else false). +Proof. + intros. destruct (in_dec lbl hd), (MB.in_dec lbl hd). all: tauto. +Qed. + +Lemma transl_is_label: + forall lbl bb tbb f ep tc, + transl_block f bb ep = OK (tbb::tc) -> + is_label lbl tbb = MB.is_label lbl bb. +Proof. + intros until tc. intros TLB. + destruct tbb as [thd tbdy tex]; simpl in *. + monadInv TLB. + unfold is_label. simpl. + apply cons_bblocks_label in H0. simpl in H0. subst. + rewrite in_dec_transl. auto. +Qed. + +Lemma transl_is_label_false2: + forall lbl bb f ep tbb1 tbb2, + transl_block f bb ep = OK (tbb1::tbb2::nil) -> + is_label lbl tbb2 = false. +Proof. + intros until tbb2. intros TLB. + destruct tbb2 as [thd tbdy tex]; simpl in *. + monadInv TLB. apply cons_bblocks_label2 in H0. simpl in H0. subst. + apply is_label_correct_false. simpl. auto. +Qed. + +(* +Lemma transl_is_label2: + forall f bb ep tbb1 tbb2 lbl, + transl_block f bb ep = OK (tbb1::tbb2::nil) -> + is_label lbl tbb1 = MB.is_label lbl bb + /\ is_label lbl tbb2 = false. +Proof. + intros. split. eapply transl_is_label; eauto. eapply transl_is_label_false2; eauto. +Qed. *) + +Lemma transl_block_nonil: + forall f c ep tc, + transl_block f c ep = OK tc -> + tc <> nil. +Proof. + intros. monadInv H. unfold cons_bblocks. + destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i. + all: discriminate. +Qed. + +Lemma transl_block_limit: forall f bb ep tbb1 tbb2 tbb3 tc, + ~transl_block f bb ep = OK (tbb1 :: tbb2 :: tbb3 :: tc). +Proof. + intros. intro. monadInv H. + unfold cons_bblocks in H0. + destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i. + all: discriminate. +Qed. + +Lemma find_label_transl_false: + forall x f lbl bb ep x', + transl_block f bb ep = OK x -> + MB.is_label lbl bb = false -> + find_label lbl (x++x') = find_label lbl x'. +Proof. + intros until x'. intros TLB MBis; simpl; auto. + destruct x as [|x0 x1]; simpl; auto. + destruct x1 as [|x1 x2]; simpl; auto. + - erewrite <- transl_is_label in MBis; eauto. rewrite MBis. auto. + - destruct x2 as [|x2 x3]; simpl; auto. + + erewrite <- transl_is_label in MBis; eauto. rewrite MBis. + erewrite transl_is_label_false2; eauto. + + apply transl_block_limit in TLB. destruct TLB. +Qed. + +Lemma transl_blocks_label: + forall lbl f c tc ep, + transl_blocks f c ep = OK tc -> + match MB.find_label lbl c with + | None => find_label lbl tc = None + | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_blocks f c' false = OK tc' + end. +Proof. + induction c; simpl; intros. + inv H. auto. + monadInv H. + destruct (MB.is_label lbl a) eqn:MBis. + - destruct x as [|tbb tc]. { apply transl_block_nonil in EQ. contradiction. } + simpl find_label. exploit transl_is_label; eauto. intros ABis. rewrite MBis in ABis. + rewrite ABis. + eexists. eexists. split; eauto. simpl transl_blocks. + assert (MB.header a <> nil). + { apply MB.is_label_correct_true in MBis. + destruct (MB.header a). contradiction. discriminate. } + destruct (MB.header a); try contradiction. + rewrite EQ. simpl. rewrite EQ1. simpl. auto. + - apply IHc in EQ1. destruct (MB.find_label lbl c). + + destruct EQ1 as (tc' & FIND & TLBS). exists tc'; eexists; auto. + erewrite find_label_transl_false; eauto. + + erewrite find_label_transl_false; eauto. +Qed. + +Lemma find_label_nil: + forall bb lbl c, + header bb = nil -> + find_label lbl (bb::c) = find_label lbl c. +Proof. + intros. destruct bb as [hd bdy ex]; simpl in *. subst. + assert (is_label lbl {| AB.header := nil; AB.body := bdy; AB.exit := ex; AB.correct := correct |} = false). + { erewrite <- is_label_correct_false. simpl. auto. } + rewrite H. auto. +Qed. + +Theorem transl_find_label: + forall lbl f tf, + transf_function f = OK tf -> + match MB.find_label lbl f.(MB.fn_code) with + | None => find_label lbl tf.(fn_blocks) = None + | Some c => exists tc, find_label lbl tf.(fn_blocks) = Some tc /\ transl_blocks f c false = OK tc + end. +Proof. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); inv EQ0. clear g. + monadInv EQ. unfold make_prologue. simpl fn_blocks. repeat (rewrite find_label_nil); simpl; auto. + eapply transl_blocks_label; eauto. +Qed. + +End TRANSL_LABEL. +(** A valid branch in a piece of Machblock code translates to a valid ``go to'' + transition in the generated Asmblock code. *) + +Lemma find_label_goto_label: + forall f tf lbl rs m c' b ofs, + Genv.find_funct_ptr ge b = Some (Internal f) -> + transf_function f = OK tf -> + rs PC = Vptr b ofs -> + MB.find_label lbl f.(MB.fn_code) = Some c' -> + exists tc', exists rs', + goto_label tf lbl rs m = Next rs' m + /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc' + /\ forall r, r <> PC -> rs'#r = rs#r. +Proof. + intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. + intros (tc & A & B). + exploit label_pos_code_tail; eauto. instantiate (1 := 0). + intros [pos' [P [Q R]]]. + exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))). + split. unfold goto_label. rewrite P. rewrite H1. auto. + split. rewrite Pregmap.gss. constructor; auto. + rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. + auto. omega. + generalize (transf_function_no_overflow _ _ H0). omega. + intros. apply Pregmap.gso; auto. +Qed. + (** Existence of return addresses *) Lemma return_address_exists: @@ -144,11 +344,6 @@ Ltac exploreInst := | [ H : bind _ _ = OK _ |- _ ] => monadInv H | [ H : Error _ = OK _ |- _ ] => inversion H end. - -Ltac desif := - repeat match goal with - | [ |- context[if ?f then _ else _ ] ] => destruct f - end. (** Some translation properties *) @@ -488,6 +683,688 @@ Proof. all: simpl; auto. Qed. +Lemma exec_straight_body: + forall c c' rs1 m1 rs2 m2, + exec_straight tge lk c rs1 m1 c' rs2 m2 -> + exists l, + c = l ++ c' + /\ exec_body lk tge l rs1 m1 = Next rs2 m2. +Proof. + induction c; try (intros; inv H; fail). + intros until m2. intros EXES. inv EXES. + - exists (a :: nil). repeat (split; simpl; auto). rewrite H6. auto. + - eapply IHc in H7; eauto. destruct H7 as (l' & Hc & EXECB). subst. + exists (a :: l'). repeat (split; simpl; auto). + rewrite H1. auto. +Qed. + +Lemma exec_straight_body2: + forall c rs1 m1 c' rs2 m2, + exec_straight tge lk c rs1 m1 c' rs2 m2 -> + exists body, + exec_body lk tge body rs1 m1 = Next rs2 m2 + /\ body ++ c' = c. +Proof. + intros until m2. induction 1. + - exists (i1::nil). split; auto. simpl. rewrite H. auto. + - destruct IHexec_straight as (bdy & EXEB & BTC). + exists (i:: bdy). split; simpl. + + rewrite H. auto. + + congruence. +Qed. + +Lemma exec_straight_opt_body2: + forall c rs1 m1 c' rs2 m2, + exec_straight_opt tge lk c rs1 m1 c' rs2 m2 -> + exists body, + exec_body lk tge body rs1 m1 = Next rs2 m2 + /\ body ++ c' = c. +Proof. + intros until m2. intros EXES. + inv EXES. + - exists nil. split; auto. + - eapply exec_straight_body2. auto. +Qed. + +Lemma PC_not_data_preg: forall r , + data_preg r = true -> + r <> PC. +Proof. + intros. destruct (PregEq.eq r PC); [ rewrite e in H; simpl in H; discriminate | auto ]. +Qed. + +Lemma X30_not_data_preg: forall r , + data_preg r = true -> + r <> X30. +Proof. + intros. destruct (PregEq.eq r X30); [ rewrite e in H; simpl in H; discriminate | auto ]. +Qed. + +Ltac Simpl := + rewrite Pregmap.gso; try apply PC_not_data_preg; try apply X30_not_data_preg. + +Ltac ArgsInv := + repeat (match goal with + | [ H: Error _ = OK _ |- _ ] => discriminate + | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args + | [ H: bind _ _ = OK _ |- _ ] => monadInv H + | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv + | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv + end); + subst; + repeat (match goal with + | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in * + | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in * + end). + +(* See (C) in the diagram. The proofs are mostly adapted from the previous Mach->Asm proofs, but are + unfortunately quite cumbersome. To reproduce them, it's best to have a Coq IDE with you and see by + yourself the steps *) +Theorem step_simu_control: + forall bb' fb fn s sp c ms' m' rs2 m2 t S'' rs1 m1 tbb tbdy2 tex cs2, + MB.body bb' = nil -> + (forall ef args res, MB.exit bb' <> Some (MBbuiltin ef args res)) -> + Genv.find_funct_ptr tge fb = Some (Internal fn) -> + pstate cs2 = (State rs2 m2) -> + pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex -> + cur cs2 = tbb -> + match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 -> + match_asmstate fb cs2 (State rs1 m1) -> + exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') t S'' -> + (exists rs3 m3 rs4 m4, + exec_body lk tge tbdy2 rs2 m2 = Next rs3 m3 + /\ exec_exit tge fn (Ptrofs.repr (size tbb)) rs3 m3 tex t rs4 m4 + /\ match_states S'' (State rs4 m4)). +Proof. Admitted. (* + intros until cs2. intros Hbody Hbuiltin FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP. + inv ESTEP. + - inv MCS. inv MAS. simpl in *. + inv Hpstate. + destruct ctl. + + (* MBcall *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + destruct s1 as [rf|fid]; simpl in H1. + * (* Indirect call *) + monadInv H1. monadInv EQ. + assert (ms' rf = Vptr f' Ptrofs.zero). + { unfold find_function_ptr in H12. destruct (ms' rf); try discriminate. + revert H12; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } + assert (rs2 x = Vptr f' Ptrofs.zero). + { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. } + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. + remember (Ptrofs.add _ _) as ofs'. + assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc). + { econstructor; eauto. } + assert (f1 = f) by congruence. subst f1. + exploit return_address_offset_correct; eauto. intros; subst ra. + + repeat eexists. + econstructor; eauto. econstructor. + econstructor; eauto. econstructor; eauto. + eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. + unfold incrPC; repeat Simpl; auto. + simpl. unfold incrPC; rewrite Pregmap.gso; auto; try discriminate. + rewrite !Pregmap.gss. rewrite PCeq. rewrite Heqofs'. simpl. auto. + + * (* Direct call *) + monadInv H1. + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. + remember (Ptrofs.add _ _) as ofs'. + assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc). + econstructor; eauto. + assert (f1 = f) by congruence. subst f1. + exploit return_address_offset_correct; eauto. intros; subst ra. + repeat eexists. + econstructor; eauto. econstructor. + econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. + unfold incrPC; repeat Simpl; auto. unfold Genv.symbol_address. rewrite symbols_preserved. simpl in H12. rewrite H12. auto. + unfold incrPC; simpl; rewrite Pregmap.gso; try discriminate. rewrite !Pregmap.gss. + subst. unfold Val.offset_ptr. rewrite PCeq. auto. + + (* MBtailcall *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + exploit Mem.loadv_extends. eauto. eexact H13. auto. simpl. intros [parent' [A B]]. + destruct s1 as [rf|fid]; simpl in H11. + * monadInv H1. monadInv EQ. + assert (ms' rf = Vptr f' Ptrofs.zero). + { destruct (ms' rf); try discriminate. revert H11. predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } + assert (rs2 x = Vptr f' Ptrofs.zero). + { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. } + + assert (f = f1) by congruence. subst f1. clear FIND1. clear H12. + exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). + exploit exec_straight_body; eauto. + intros (l & MKEPI & EXEB). + repeat eexists. rewrite app_nil_r in MKEPI. + rewrite <- MKEPI in EXEB. + eauto. econstructor. simpl. unfold incrPC. + rewrite !Pregmap.gso; try discriminate. eauto. + econstructor; eauto. + { apply agree_set_other. + - econstructor; auto with asmgen. + + apply V. + + intro r. destruct r; apply V; auto. + - eauto with asmgen. } + rewrite Pregmap.gss. rewrite Z; auto; try discriminate. + eapply ireg_of_not_X30''; eauto. + eapply ireg_of_not_X16''; eauto. + * monadInv H1. assert (f = f1) by congruence. subst f1. clear FIND1. clear H12. + exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). + exploit exec_straight_body; eauto. + intros (l & MKEPI & EXEB). + repeat eexists. inv EQ. rewrite app_nil_r in MKEPI. + rewrite <- MKEPI in EXEB. + eauto. inv EQ. econstructor. simpl. unfold incrPC. + eauto. + econstructor; eauto. + { apply agree_set_other. + - econstructor; auto with asmgen. + + apply V. + + intro r. destruct r; apply V; auto. + - eauto with asmgen. } + { rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H11. auto. } + + (* MBbuiltin (contradiction) *) + assert (MB.exit bb' <> Some (MBbuiltin e l b)) by (apply Hbuiltin). + rewrite <- H in H1. contradict H1; auto. + + (* MBgoto *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. assert (f1 = f) by congruence. subst f1. clear H9. + remember (incrPC (Ptrofs.repr (size tbb)) rs2) as rs2'. + exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND'. + assert (tf = fn) by congruence. subst tf. + exploit find_label_goto_label. + eauto. eauto. + instantiate (2 := rs2'). + { subst. unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. eauto. } + eauto. + intros (tc' & rs' & GOTO & AT2 & INV). + + eexists. eexists. repeat eexists. repeat split. + econstructor; eauto. + rewrite Heqrs2' in INV. unfold incrPC in INV. + rewrite Heqrs2' in GOTO; simpl; eauto. + econstructor; eauto. + eapply agree_exten; eauto with asmgen. + assert (forall r : preg, r <> PC -> rs' r = rs2 r). + { intros. rewrite Heqrs2' in INV. + rewrite INV; unfold incrPC; try rewrite Pregmap.gso; auto. } + eauto with asmgen. + congruence. + + (* MBcond *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + * (* MBcond true *) + assert (f0 = f) by congruence. subst f0. + exploit eval_condition_lessdef. + eapply preg_vals; eauto. + all: eauto. + intros EC. monadInv H1. + unfold transl_cond_branch in EQ. ArgsInv. + { unfold transl_cond_branch_default in EQ. monadInv EQ. unfold transl_cond in EQ0. + destruct c0; try discriminate. } + { destruct c0; ArgsInv; + try (unfold transl_cond_branch_default, transl_cond in EQ; try monadInv EQ; discriminate). + - destruct c0. + 3:{ unfold transl_cond_branch_default, transl_cond in EQ. monadInv EQ. monadInv EQ0. + repeat eexists. destruct is_arith_imm32. + - simpl. eauto. + - destruct is_arith_imm32; simpl; eauto. + + discriminate. + destruct c0; ArgsInv. unfold transl_cond_branch_default in EQ; try monadInv EQ; try unfold transl_cond in EQ0; + try discriminate. + { destruct c0; try discriminate. } + + + { monadInv EQ. unfold transl_cond in EQ0. destruct c0; try discriminate. } + { apply IHl. discriminate. + { destruct l, c0; simpl in *; try congruence. + destruct c0; simpl. simpl in EQ. monadInv EQ. + + exploit (transl_cbranch_correct); eauto. intros (rsX & mX & rsY & mY & A & B & C). + + exists rsX. exists mX. exists rsY. exists mY. split. eauto. eauto. + + assert (PCeq': rs2 PC = rs' PC). { admit. (* inv A; auto. erewrite <- exec_straight_pc. 2: eapply H. eauto. *) } + rewrite PCeq' in PCeq. + assert (f1 = f) by congruence. subst f1. + exploit find_label_goto_label. + 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs')). unfold incrPC. + rewrite Pregmap.gss. + unfold Val.offset_ptr. rewrite PCeq. eauto. + intros (tc' & rs3 & GOTOL & TLPC & Hrs3). + exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'. + assert (tf = fn) by congruence. subst tf. + + repeat eexists. + rewrite <- BTC. simpl. rewrite app_nil_r. eauto. + eapply (cfi_step tge fn (Ptrofs.repr (size tbb)) rs' m2 (Some x0) E0 _ _). rewrite <- BTC. simpl. econstructor. rewrite B. eauto. + + econstructor; eauto. + eapply agree_exten with rs2; eauto with asmgen. + { intros. destruct r; try destruct g; try discriminate. + all: rewrite Hrs3; try discriminate; unfold nextblock, incrPC; Simpl. } + intros. discriminate. + + * (* MBcond false *) + assert (f0 = f) by congruence. subst f0. + exploit eval_condition_lessdef. + eapply preg_vals; eauto. + all: eauto. + intros EC. + + exploit transl_cbranch_correct_false; eauto. intros (rs' & jmp & A & B & C). + exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC). + assert (PCeq': rs2 PC = rs' PC). { inv A; auto. erewrite <- exec_straight_pc. 2: eapply H. eauto. } + rewrite PCeq' in PCeq. + exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'. + assert (tf = fn) by congruence. subst tf. + + assert (NOOV: size_blocks fn.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. + + repeat eexists. + rewrite H6. rewrite <- BTC. rewrite extract_basics_to_code. simpl. rewrite app_nil_r. eauto. + rewrite H7. rewrite <- BTC. rewrite extract_ctl_basics_to_code. simpl extract_ctl. rewrite B. eauto. + + econstructor; eauto. + unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto. + eapply agree_exten with rs2; eauto with asmgen. + { intros. destruct r; try destruct g; try discriminate. + all: rewrite <- C; try discriminate; unfold nextblock, incrPC; Simpl. } + intros. discriminate. + + (* MBjumptable *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. + monadInv H1. + generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV. + assert (f1 = f) by congruence. subst f1. + exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef). + unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity. + exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn. + + intros [tc' [rs' [A [B C]]]]. + exploit ireg_val; eauto. rewrite H13. intros LD; inv LD. + + repeat eexists. + rewrite H6. simpl extract_basic. simpl. eauto. + rewrite H7. simpl extract_ctl. simpl. Simpl. rewrite <- H1. unfold Mach.label in H14. unfold label. rewrite H14. eapply A. + econstructor; eauto. + eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen. + { assert (destroyed_by_jumptable = R62 :: R63 :: nil) by auto. rewrite H2 in H0. simpl in H0. inv H0. + destruct (preg_eq r' GPR63). subst. contradiction. + destruct (preg_eq r' GPR62). subst. contradiction. + destruct r'; Simpl. } + discriminate. + + (* MBreturn *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). + exploit exec_straight_body; eauto. + simpl. eauto. + intros EXEB. + assert (f1 = f) by congruence. subst f1. + + repeat eexists. + rewrite H6. simpl extract_basic. eauto. + rewrite H7. simpl extract_ctl. simpl. reflexivity. + econstructor; eauto. + unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen. + + - inv MCS. inv MAS. simpl in *. subst. inv Hpstate. + destruct bb' as [hd' bdy' ex']; simpl in *. subst. + monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6. + simpl. repeat eexists. + econstructor. 4: instantiate (3 := false). all:eauto. + unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + assert (f = f0) by congruence. subst f0. econstructor; eauto. + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. eauto. + eapply agree_exten; eauto. intros. Simpl. + discriminate. +Qed.*) + +(* Handling the individual instructions of theorem (B) in the above diagram. A bit less cumbersome, but still tough *) +Theorem step_simu_basic: + forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy, + MB.header bb = nil -> MB.body bb = bi::(bdy) -> (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> + bb' = {| MB.header := nil; MB.body := bdy; MB.exit := MB.exit bb |} -> + basic_step ge s fb sp ms m bi ms' m' -> + pstate cs1 = (State rs1 m1) -> pbody1 cs1 = tbdy -> + match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 -> + (exists rs2 m2 l cs2 tbdy', + cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := tbdy'; pbody2 := pbody2 cs1; + pctl := pctl cs1; ep := it1_is_parent (ep cs1) bi; rem := rem cs1; cur := cur cs1 |} + /\ tbdy = l ++ tbdy' + /\ exec_body lk tge l rs1 m1 = Next rs2 m2 + /\ match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2). +Proof. + intros until bdy. intros Hheader Hbody Hnobuiltin (* Hnotempty *) Hbb' BSTEP Hpstate Hpbody1 MCS. inv MCS. + simpl in *. inv Hpstate. + rewrite Hbody in TBC. monadInv TBC. + inv BSTEP. + + - (* MBgetstack *) + simpl in EQ0. + unfold Mach.load_stack in H. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + exploit loadind_correct; eauto with asmgen. + intros (rs2 & EXECS & Hrs'1 & Hrs'2). + eapply exec_straight_body in EXECS. + destruct EXECS as (l & Hlbi & EXECB). + exists rs2, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. } + subst. simpl in Hheadereq. + + eapply match_codestate_intro; eauto. + eapply agree_set_mreg; eauto with asmgen. + intro Hep. simpl in Hep. discriminate. + - (* MBsetstack *) + simpl in EQ0. + unfold Mach.store_stack in H. + assert (Val.lessdef (ms src) (rs1 (preg_of src))). { eapply preg_val; eauto. } + exploit Mem.storev_extends; eauto. intros [m2' [A B]]. + exploit storeind_correct; eauto with asmgen. + rewrite (sp_val _ _ _ AG) in A. eauto. intros [rs' [P Q]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs', m2', l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + subst. + eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto. + eapply agree_undef_regs; eauto with asmgen. + simpl; intros. rewrite Q; auto with asmgen. rewrite Hheader in DXP. auto. + - (* MBgetparam *) + simpl in EQ0. + + assert (f0 = f) by congruence; subst f0. + unfold Mach.load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. auto. + intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. + exploit Mem.loadv_extends. eauto. eexact H1. auto. + intros [v' [C D]]. + + monadInv EQ0. rewrite Hheader. rewrite Hheader in DXP. + destruct ep0 eqn:EPeq. + + (* X29 contains parent *) + + exploit loadind_correct. eexact EQ1. + instantiate (2 := rs1). rewrite DXP; eauto. discriminate. + intros [rs2 [P [Q R]]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m1, l. eexists. + eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. } + subst. + eapply match_codestate_intro; eauto. + + eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. + simpl; intros. rewrite R; auto with asmgen. unfold preg_of. + apply preg_of_not_X29; auto. + + (* X29 does not contain parent *) + + rewrite chunk_of_Tptr in A. + exploit loadptr_correct. eexact A. discriminate. intros [rs2 [P [Q R]]]. + exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto. + discriminate. + intros [rs3 [S [T U]]]. + + exploit exec_straight_trans. + eapply P. + eapply S. + intros EXES. + + eapply exec_straight_body in EXES. + destruct EXES as (l & ll & EXECB). + exists rs3, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } + subst. + eapply match_codestate_intro; eauto. + eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. + instantiate (1 := rs2#X29 <- (rs3#X29)). intros. + rewrite Pregmap.gso; auto with asmgen. + congruence. + intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen. + simpl; intros. rewrite U; auto with asmgen. + apply preg_of_not_X29; auto. + - (* MBop *) + simpl in EQ0. rewrite Hheader in DXP. + + assert (eval_operation tge sp op (map ms args) m' = Some v). + rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. + exploit eval_operation_lessdef. + eapply preg_vals; eauto. + 2: eexact H0. + all: eauto. + intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + subst. + eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto. + apply agree_set_undef_mreg with rs1; auto. + apply Val.lessdef_trans with v'; auto. + simpl; intros. destruct (andb_prop _ _ H1); clear H1. + rewrite R; auto. apply preg_of_not_X29; auto. +Local Transparent destroyed_by_op. + destruct op; simpl; auto; try discriminate. + - (* MBload *) + simpl in EQ0. rewrite Hheader in DXP. + + assert (Op.eval_addressing tge sp addr (map ms args) = Some a). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit Mem.loadv_extends; eauto. intros [v' [C D]]. destruct trap; try discriminate. + exploit transl_load_correct; eauto. + intros [rs2 [P [Q R]]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } + subst. + eapply match_codestate_intro; eauto. + eapply agree_set_mreg; eauto with asmgen. + intro Hep. simpl in Hep. discriminate. + - (* MBload notrap1 *) + simpl in EQ0. unfold transl_load in EQ0. discriminate. + (*destruct addr; simpl in H; destruct chunk; monadInv EQ0. + all: + destruct args as [|h0 t0]; try discriminate; + destruct t0 as [|h1 t1]; try discriminate; + destruct t1 as [|h2 t2]; try discriminate.*) + + - (* MBload notrap2 *) + simpl in EQ0. unfold transl_load in EQ0. discriminate. + (*simpl in EQ0. rewrite Hheader in DXP. + + assert (Op.eval_addressing tge sp addr (map ms args) = Some a). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit transl_load_correct; eauto. + intros [rs2 [P [Q R]]]. + + destruct (Mem.loadv chunk m1 a') as [v' | ] eqn:Hload. + { + exploit transl_load_correct; eauto. + intros [rs2 [P [Q R]]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + eapply match_codestate_intro; eauto. + + eapply agree_set_undef_mreg; eauto. intros; auto with asmgen. + + simpl in *. discriminate. + } + { + exploit transl_load_correct_notrap2; eauto. + intros [rs2 [P [Q R]]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. +(* assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } + rewrite <- Hheadereq. *) subst. + eapply match_codestate_intro; eauto. + + eapply agree_set_undef_mreg; eauto. intros; auto with asmgen. + simpl in *. discriminate. + }*) + - (* MBstore *) + simpl in EQ0. rewrite Hheader in DXP. + + assert (Op.eval_addressing tge sp addr (map ms args) = Some a). + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + assert (Val.lessdef (ms src) (rs1 (preg_of src))). eapply preg_val; eauto. + exploit Mem.storev_extends; eauto. intros [m2' [C D]]. + exploit transl_store_correct; eauto. intros [rs2 [P Q]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m2', l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } + subst. + eapply match_codestate_intro; eauto. + eapply agree_undef_regs; eauto with asmgen. + intro Hep. simpl in Hep. discriminate. +Qed. + +Lemma exec_body_trans: + forall l l' rs0 m0 rs1 m1 rs2 m2, + exec_body lk tge l rs0 m0 = Next rs1 m1 -> + exec_body lk tge l' rs1 m1 = Next rs2 m2 -> + exec_body lk tge (l++l') rs0 m0 = Next rs2 m2. +Proof. + induction l. + - simpl. induction l'. intros. + + simpl in *. congruence. + + intros. inv H. auto. + - intros until m2. intros EXEB1 EXEB2. + inv EXEB1. destruct (exec_basic _) eqn:EBI; try discriminate. + simpl. rewrite EBI. eapply IHl; eauto. +Qed. + +Lemma exec_body_control: + forall b t rs1 m1 rs2 m2 rs3 m3 fn, + exec_body lk tge (body b) rs1 m1 = Next rs2 m2 -> + exec_exit tge fn (Ptrofs.repr (size b)) rs2 m2 (exit b) t rs3 m3 -> + exec_bblock lk tge fn b rs1 m1 t rs3 m3. +Proof. + intros until fn. intros EXEB EXECTL. + econstructor; eauto. +Qed. + +Inductive exec_header: codestate -> codestate -> Prop := + | exec_header_cons: forall cs1, + exec_header cs1 {| pstate := pstate cs1; pheader := nil; pbody1 := pbody1 cs1; pbody2 := pbody2 cs1; + pctl := pctl cs1; ep := (if pheader cs1 then ep cs1 else false); rem := rem cs1; + cur := cur cs1 |}. + +(* Theorem (A) in the diagram, the easiest of all *) +Theorem step_simu_header: + forall bb s fb sp c ms m rs1 m1 cs1, + pstate cs1 = (State rs1 m1) -> + match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 -> + (exists cs1', + exec_header cs1 cs1' + /\ match_codestate fb (MB.State s fb sp (mb_remove_header bb::c) ms m) cs1'). +Proof. + intros until cs1. intros Hpstate MCS. + eexists. split; eauto. + econstructor; eauto. + inv MCS. simpl in *. inv Hpstate. + econstructor; eauto. +Qed. + +(* Theorem (B) in the diagram, using step_simu_basic + induction on the Machblock body *) +Theorem step_simu_body: + forall bb s fb sp c ms m rs1 m1 ms' cs1 m', + MB.header bb = nil -> + (forall ef args res, MB.exit bb <> Some (MBbuiltin ef args res)) -> + body_step ge s fb sp (MB.body bb) ms m ms' m' -> + pstate cs1 = (State rs1 m1) -> + match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 -> + (exists rs2 m2 cs2 ep, + cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := nil; pbody2 := pbody2 cs1; + pctl := pctl cs1; ep := ep; rem := rem cs1; cur := cur cs1 |} + /\ exec_body lk tge (pbody1 cs1) rs1 m1 = Next rs2 m2 + /\ match_codestate fb (MB.State s fb sp ({| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |}::c) ms' m') cs2). +Proof. + intros bb. destruct bb as [hd bdy ex]; simpl; auto. induction bdy as [|bi bdy]. + - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS. + inv BSTEP. + exists rs1, m1, cs1, (ep cs1). + inv MCS. inv Hpstate. simpl in *. monadInv TBC. repeat (split; simpl; auto). + econstructor; eauto. + - intros until m'. intros Hheader Hnobuiltin BSTEP Hpstate MCS. inv BSTEP. + rename ms' into ms''. rename m' into m''. rename rs' into ms'. rename m'0 into m'. + exploit (step_simu_basic); eauto. simpl. eauto. simpl; auto. simpl; auto. + intros (rs2 & m2 & l & cs2 & tbdy' & Hcs2 & Happ & EXEB & MCS'). + simpl in *. + exploit IHbdy. auto. 2: eapply H6. 3: eapply MCS'. all: eauto. subst; eauto. simpl; auto. + intros (rs3 & m3 & cs3 & ep & Hcs3 & EXEB' & MCS''). + exists rs3, m3, cs3, ep. + repeat (split; simpl; auto). subst. simpl in *. auto. + rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto. +Qed. + (* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *) (* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *) Lemma step_simulation_bblock': @@ -543,8 +1420,7 @@ Proof. assert (exists rs1 m1, pstate cs1 = State rs1 m1). { inv MAS. simpl. eauto. } destruct H as (rs1 & m1 & Hpstate2). subst. assert (f = fb). { inv MCS. auto. } subst fb. - all: admit. - (*exploit step_simu_header. + exploit step_simu_header. 2: eapply MCS. all: eauto. intros (cs1' & EXEH & MCS2). @@ -561,15 +1437,11 @@ Proof. assert (exists tf, Genv.find_funct_ptr tge f = Some (Internal tf)). { exploit functions_translated; eauto. intros (tf & FIND' & TRANSF'). monadInv TRANSF'. eauto. } destruct H as (tf & FIND'). - assert (exists tex, pbody2 cs1 = extract_basic tex /\ pctl cs1 = extract_ctl tex). - { inv MAS. simpl in *. eauto. } - destruct H as (tex & Hpbody2 & Hpctl). inv EXEH. simpl in *. subst. exploit step_simu_control. 9: eapply MCS'. all: simpl. 10: eapply ESTEP. all: simpl; eauto. - rewrite Hpbody2. rewrite Hpctl. { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto. erewrite exec_body_pc; eauto. } intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS'). @@ -580,14 +1452,14 @@ Proof. eauto. intros EXEB2. exploit exec_body_control; eauto. - rewrite <- Hpbody2 in EXEB2. rewrite <- Hbody in EXEB2. eauto. - rewrite Hexit. rewrite Hpctl. eauto. - intros EXECB. inv EXECB. + rewrite <- Hbody in EXEB2. eauto. + rewrite Hexit. eauto. + intros EXECB. (* inv EXECB. *) exists (State rs4 m4). split; auto. eapply plus_one. rewrite Hpstate2. assert (exists ofs, rs1 PC = Vptr f ofs). { rewrite Hpstate2 in MAS. inv MAS. simpl in *. eauto. } - destruct H0 as (ofs & Hrs1pc). + destruct H as (ofs & Hrs1pc). eapply exec_step_internal; eauto. (* proving the initial find_bblock *) @@ -595,10 +1467,10 @@ Proof. assert (f1 = f0) by congruence. subst f0. rewrite PCeq in Hrs1pc. inv Hrs1pc. exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''. - inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ. + inv FIND''. monadInv TRANS''. unfold transf_function in TRANSF0. monadInv TRANSF0. + destruct (zlt _ _) in EQ1; try discriminate. rewrite EQ in EQ0. inv EQ0. inv EQ1. eapply find_bblock_tail; eauto. -Qed.*) -Admitted. +Qed. Theorem step_simulation_bblock: forall sf f sp bb ms m ms' m' S2 c, @@ -616,6 +1488,106 @@ Proof. - econstructor. Qed. +(* Definition split (c: MB.code) := + match c with + | nil => nil + | bb::c => {| MB.header := MB.header bb; MB.body := MB.body bb; MB.exit := None |} + :: {| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |} :: c + end. + +Lemma cons_ok_eq3 {A: Type} : + forall (x:A) y z x' y' z', + x = x' -> y = y' -> z = z' -> + OK (x::y::z) = OK (x'::y'::z'). +Proof. + intros. subst. auto. +Qed. + +Lemma transl_blocks_split_builtin: + forall bb c ep f ef args res, + MB.exit bb = Some (MBbuiltin ef args res) -> MB.body bb <> nil -> + transl_blocks f (split (bb::c)) ep = transl_blocks f (bb::c) ep. +Proof. + intros until res. intros Hexit Hbody. simpl split. + unfold transl_blocks. fold transl_blocks. unfold transl_block. + simpl. remember (transl_basic_code _ _ _) as tbc. remember (transl_exit _ _) as tbi. + remember (transl_blocks _ _ _) as tlbs. + destruct tbc; destruct tbi; destruct tlbs. + - unfold cons_bblocks; try destruct p; try simpl; rewrite app_nil_r. + destruct l; destruct o; destruct b; simpl. auto. + + auto. + all: unfold cons_bblocks; try destruct p; try simpl; auto. + - simpl. rewrite Hexit in Heqtbi. simpl in Heqtbi. monadInv Heqtbi. simpl. + unfold cons_bblocks. simpl. destruct l. + + exploit transl_basic_code_nonil; eauto. intro. destruct H. + + simpl. rewrite app_nil_r. simpl. apply cons_ok_eq3. all: try eapply bblock_equality. all: simpl; auto. +Qed. + +Lemma transl_code_at_pc_split_builtin: + forall rs f f0 bb c ep tf tc ef args res, + MB.body bb <> nil -> MB.exit bb = Some (MBbuiltin ef args res) -> + transl_code_at_pc ge (rs PC) f f0 (bb :: c) ep tf tc -> + transl_code_at_pc ge (rs PC) f f0 (split (bb :: c)) ep tf tc. +Proof. + intros until res. intros Hbody Hexit AT. inv AT. + econstructor; eauto. erewrite transl_blocks_split_builtin; eauto. +Qed. + + +Theorem match_states_split_builtin: + forall sf f sp bb c rs m ef args res S1, + MB.body bb <> nil -> MB.exit bb = Some (MBbuiltin ef args res) -> + match_states (Machblock.State sf f sp (bb :: c) rs m) S1 -> + match_states (Machblock.State sf f sp (split (bb::c)) rs m) S1. +Proof. + intros until S1. intros Hbody Hexit MS. + inv MS. + econstructor; eauto. + eapply transl_code_at_pc_split_builtin; eauto. +Qed. *) + +Theorem step_simulation_builtin: + forall ef args res bb sf f sp c ms m t S2, + MB.body bb = nil -> MB.exit bb = Some (MBbuiltin ef args res) -> + exit_step return_address_offset ge (MB.exit bb) (Machblock.State sf f sp (bb :: c) ms m) t S2 -> + forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' -> + exists S2' : state, plus (step lk) tge S1' t S2' /\ match_states S2 S2'. +Proof. + intros until S2. intros Hbody Hexit ESTEP S1' MS. + inv MS. inv AT. monadInv H2. monadInv EQ. + rewrite Hbody in EQ. monadInv EQ. + rewrite Hexit in EQ0. monadInv EQ0. + rewrite Hexit in ESTEP. inv ESTEP. inv H4. + + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H1); intro NOOV. + exploit builtin_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2' [A [B [C D]]]]]. + econstructor; split. apply plus_one. + simpl in H3. + eapply exec_step_internal. eauto. eauto. + eapply find_bblock_tail; eauto. + simpl. econstructor. eexists. simpl. split; eauto. + econstructor. + erewrite <- sp_val by eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + eauto. + econstructor; eauto. + instantiate (2 := tf); instantiate (1 := x0). + unfold incrPC. rewrite Pregmap.gss. + rewrite set_res_other. rewrite undef_regs_other_2. + rewrite <- H. simpl. econstructor; eauto. + eapply code_tail_next_int; eauto. + rewrite preg_notin_charact. intros. auto with asmgen. + auto with asmgen. + apply agree_nextblock. eapply agree_set_res; auto. + eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. + congruence. +Qed. + (* Measure to prove finite stuttering, see the other backends *) Definition measure (s: MB.state) : nat := match s with @@ -631,26 +1603,23 @@ Theorem step_simulation: forall S1' (MS: match_states S1 S1'), (exists S2', plus (step lk) tge S1' t S2' /\ match_states S2 S2') \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. -Proof. - induction 1; intros. +Proof. Admitted. +(* induction 1; intros. - (* bblock *) left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0. - all: admit. -all: admit. -Admitted. - (*all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; + all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto). + (* MBbuiltin *) destruct (MB.body bb) eqn:MBB. * inv H. eapply step_simulation_builtin; eauto. rewrite MBE. eauto. - * eapply match_states_split_builtin in MS; eauto. - 2: rewrite MBB; discriminate. - simpl split in MS. + * (* eapply match_states_split_builtin in MS; eauto. + 2: rewrite MBB; discriminate. *) + (* simpl split in MS. *) rewrite <- MBB in H. - remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb1. - assert (MB.body bb = MB.body bb1). { subst. simpl. auto. } - rewrite H1 in H. subst. +(* remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb1. *) +(* assert (MB.body bb = MB.body bb1). { subst. simpl. auto. } *) +(* rewrite H1 in H. subst. *) exploit step_simulation_bblock. eapply H. discriminate. simpl. constructor. diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index 69d6037c..4a35485e 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -6,6 +6,7 @@ (* Xavier Leroy INRIA Paris-Rocquencourt *) (* David Monniaux CNRS, VERIMAG *) (* Cyril Six Kalray *) +(* Léo Gourdin UGA, VERIMAG *) (* *) (* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) (* This file is distributed under the terms of the INRIA *) @@ -44,6 +45,52 @@ Module AB:=Asmblock. (** * Agreement between Mach registers and processor registers *) +Hint Extern 2 (_ <> _) => congruence: asmgen. + +Lemma ireg_of_eq: + forall r r', ireg_of r = OK r' -> preg_of r = IR r'. +Proof. + unfold ireg_of; intros. destruct (preg_of r) as [[[rr1|]|]|xsp|]; inv H; auto. +Qed. + +Lemma freg_of_eq: + forall r r', freg_of r = OK r' -> preg_of r = FR r'. +Proof. + unfold freg_of; intros. destruct (preg_of r) as [[fr|]|xsp|]; inv H; auto. +Qed. + +Lemma ireg_of_eq': + forall r r', ireg_of r = OK r' -> dreg_of r = IR r'. +Proof. + unfold ireg_of; intros. destruct r; simpl in *; inv H; auto. +Qed. + +Lemma freg_of_eq': + forall r r', freg_of r = OK r' -> dreg_of r = FR r'. +Proof. + unfold freg_of; intros. destruct r; simpl in *; inv H; auto. +Qed. + +Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop := + match rl with + | nil => True + | r1 :: nil => r <> preg_of r1 + | r1 :: rl => r <> preg_of r1 /\ preg_notin r rl + end. + +Remark preg_notin_charact: + forall r rl, + preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr). +Proof. + induction rl; simpl; intros. + tauto. + destruct rl. + simpl. split. intros. intuition congruence. auto. + rewrite IHrl. split. + intros [A B]. intros. destruct H. congruence. auto. + auto. +Qed. + Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree { agree_sp: rs#SP = sp; agree_sp_def: sp <> Vundef; @@ -67,6 +114,184 @@ Proof. intros. destruct H. auto. Qed. +Lemma preg_vals: + forall ms sp rs, agree ms sp rs -> + forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)). +Proof. + induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto. +Qed. + +Lemma preg_of_injective: + forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. +Proof. + destruct r1; destruct r2; simpl; intros; reflexivity || discriminate. +Qed. + +Lemma sp_val: + forall ms sp rs, agree ms sp rs -> sp = rs#SP. +Proof. + intros. destruct H; auto. +Qed. + +Lemma ireg_val: + forall ms sp rs r r', + agree ms sp rs -> + ireg_of r = OK r' -> + Val.lessdef (ms r) rs#r'. +Proof. + intros. rewrite <- (ireg_of_eq _ _ H0). eapply preg_val; eauto. +Qed. + +Lemma preg_of_not_X29: forall dst, + negb (mreg_eq dst R29) = true -> + DR (IR X29) <> preg_of dst. +Proof. + intros. destruct dst; try discriminate. +Qed. + +Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. + +(** Preservation of register agreement under various assignments. *) + +Lemma agree_set_mreg: + forall ms sp rs r v rs', + agree ms sp rs -> + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Mach.Regmap.set r v ms) sp rs'. +Proof. + intros. destruct H. split; auto. + rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP. + intros. unfold Mach.Regmap.set. destruct (Mach.RegEq.eq r0 r). congruence. + rewrite H1. auto. apply preg_of_data. + red; intros; elim n. eapply preg_of_injective; eauto. +Qed. + +Lemma agree_set_other: + forall ms sp rs r v, + agree ms sp rs -> + data_preg r = false -> + agree ms sp (rs#r <- v). +Proof. + intros. apply agree_exten with rs. auto. + intros. apply Pregmap.gso. congruence. +Qed. + +Lemma agree_nextblock: + forall ms sp rs b, + agree ms sp rs -> agree ms sp (incrPC (Ptrofs.repr (size b)) rs). +Proof. + intros. unfold incrPC. apply agree_set_other. auto. auto. +Qed. + +Lemma agree_set_res: + forall res ms sp rs v v', + agree ms sp rs -> + Val.lessdef v v' -> + agree (Mach.set_res res v ms) sp (set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v' rs). +Proof. + induction res; simpl; intros. +- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto. + intros. apply Pregmap.gso; auto. +- auto. +- apply IHres2. apply IHres1. auto. + apply Val.hiword_lessdef; auto. + apply Val.loword_lessdef; auto. +Qed. + +Lemma agree_undef_regs: + forall ms sp rl rs rs', + agree ms sp rs -> + (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') -> + agree (Mach.undef_regs rl ms) sp rs'. +Proof. + intros. destruct H. split; auto. + rewrite <- agree_sp0. apply H0; auto. + rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP. + intros. destruct (In_dec mreg_eq r rl). + rewrite Mach.undef_regs_same; auto. + rewrite Mach.undef_regs_other; auto. rewrite H0; auto. + apply preg_of_data. + rewrite preg_notin_charact. intros; red; intros. elim n. + exploit preg_of_injective; eauto. congruence. +Qed. + +Lemma agree_set_undef_mreg: + forall ms sp rs r v rl rs', + agree ms sp rs -> + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', data_preg r' = true -> r' <> preg_of r -> preg_notin r' rl -> rs'#r' = rs#r') -> + agree (Mach.Regmap.set r v (Mach.undef_regs rl ms)) sp rs'. +Proof. + intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto. + apply agree_undef_regs with rs; auto. + intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of r)). + congruence. auto. + intros. rewrite Pregmap.gso; auto. +Qed. + +Lemma agree_change_sp: + forall ms sp rs sp', + agree ms sp rs -> sp' <> Vundef -> + agree ms sp' (rs#SP <- sp'). +Proof. + intros. inv H. split; auto. + intros. rewrite Pregmap.gso; auto with asmgen. +Qed. + +Remark builtin_arg_match: + forall ge (rs: regset) sp m a v, + eval_builtin_arg ge (fun r => rs (dreg_of r)) sp m a v -> + eval_builtin_arg ge (fun r => rs (DR r)) sp m (map_builtin_arg dreg_of a) v. +Proof. + induction 1; simpl; eauto with barg. econstructor. +Qed. + +Lemma builtin_args_match: + forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> + forall al vl, eval_builtin_args ge ms sp m al vl -> + exists vl', eval_builtin_args ge (fun r => rs (DR r)) sp m' (map (map_builtin_arg dreg_of) al) vl' + /\ Val.lessdef_list vl vl'. +Proof. + induction 3; intros; simpl. + exists (@nil val); split; constructor. + exploit (@eval_builtin_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto. + intros; eapply preg_val; eauto. + intros (v1' & A & B). + destruct IHlist_forall2 as [vl' [C D]]. + exists (v1' :: vl'); split; constructor; auto. apply builtin_arg_match; auto. +Qed. + +Lemma set_res_other: + forall r res v rs, + data_preg r = false -> + set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v rs r = rs r. +Proof. + induction res; simpl; intros. +- apply Pregmap.gso. red; intros; subst r. rewrite dreg_of_data in H; discriminate. +- auto. +- rewrite IHres2, IHres1; auto. +Qed. + +Lemma undef_regs_other: + forall r rl rs, + (forall r', In r' rl -> r <> r') -> + undef_regs rl rs r = rs r. +Proof. + induction rl; simpl; intros. auto. + rewrite IHrl by auto. rewrite Pregmap.gso; auto. +Qed. + +Lemma undef_regs_other_2: + forall r rl rs, + preg_notin r rl -> + undef_regs (map preg_of rl) rs r = rs r. +Proof. + intros. apply undef_regs_other. intros. + exploit list_in_map_inv; eauto. intros [mr [A B]]. subst. + rewrite preg_notin_charact in H. auto. +Qed. + Inductive code_tail: Z -> bblocks -> bblocks -> Prop := | code_tail_0: forall c, code_tail 0 c c @@ -156,6 +381,45 @@ Proof. - rewrite Ptrofs.unsigned_repr; omega. Qed. +(** The [find_label] function returns the code tail starting at the + given label. A connection with [code_tail] is then established. *) + +Fixpoint find_label (lbl: label) (c: bblocks) {struct c} : option bblocks := + match c with + | nil => None + | bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl + end. + +(* inspired from Mach *) + +Lemma find_label_tail: + forall lbl c c', MB.find_label lbl c = Some c' -> is_tail c' c. +Proof. + induction c; simpl; intros. discriminate. + destruct (MB.is_label lbl a). inv H. auto with coqlib. eauto with coqlib. +Qed. + +Lemma label_pos_code_tail: + forall lbl c pos c', + find_label lbl c = Some c' -> + exists pos', + label_pos lbl pos c = Some pos' + /\ code_tail (pos' - pos) c c' + /\ pos <= pos' <= pos + size_blocks c. +Proof. + induction c. + simpl; intros. discriminate. + simpl; intros until c'. + case (is_label lbl a). + - intros. inv H. exists pos. split; auto. split. + replace (pos - pos) with 0 by omega. constructor. constructor; try omega. + generalize (size_blocks_pos c). generalize (size_positive a). omega. + - intros. generalize (IHc (pos+size a) c' H). intros [pos' [A [B C]]]. + exists pos'. split. auto. split. + replace (pos' - pos) with ((pos' - (pos + (size a))) + (size a)) by omega. + constructor. auto. generalize (size_positive a). omega. +Qed. + (** Predictor for return addresses in generated Asm code. The [return_address_offset] predicate defined here is used in the @@ -282,6 +546,129 @@ Proof. congruence. Qed. +Section STRAIGHTLINE. + +Variable ge: genv. +Variable lk: aarch64_linker. +Variable fn: function. + +(** Straight-line code is composed of processor instructions that execute + in sequence (no branches, no function calls and returns). + The following inductive predicate relates the machine states + before and after executing a straight-line sequence of instructions. + Instructions are taken from the first list instead of being fetched + from memory. *) + +Inductive exec_straight: list basic -> regset -> mem -> + list basic -> regset -> mem -> Prop := + | exec_straight_one: + forall i1 c rs1 m1 rs2 m2, + exec_basic lk ge i1 rs1 m1 = Next rs2 m2 -> + exec_straight (i1 :: c) rs1 m1 c rs2 m2 + | exec_straight_step: + forall i c rs1 m1 rs2 m2 c' rs3 m3, + exec_basic lk ge i rs1 m1 = Next rs2 m2 -> + exec_straight c rs2 m2 c' rs3 m3 -> + exec_straight (i :: c) rs1 m1 c' rs3 m3. + +Lemma exec_straight_trans: + forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, + exec_straight c1 rs1 m1 c2 rs2 m2 -> + exec_straight c2 rs2 m2 c3 rs3 m3 -> + exec_straight c1 rs1 m1 c3 rs3 m3. +Proof. + induction 1; intros. + apply exec_straight_step with rs2 m2; auto. + apply exec_straight_step with rs2 m2; auto. +Qed. + +Lemma exec_straight_two: + forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, + exec_basic lk ge i1 rs1 m1 = Next rs2 m2 -> + exec_basic lk ge i2 rs2 m2 = Next rs3 m3 -> + exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3. +Proof. + intros. apply exec_straight_step with rs2 m2; auto. + apply exec_straight_one; auto. +Qed. + +Lemma exec_straight_three: + forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4, + exec_basic lk ge i1 rs1 m1 = Next rs2 m2 -> + exec_basic lk ge i2 rs2 m2 = Next rs3 m3 -> + exec_basic lk ge i3 rs3 m3 = Next rs4 m4 -> + exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4. +Proof. + intros. apply exec_straight_step with rs2 m2; auto. + eapply exec_straight_two; eauto. +Qed. + +Inductive exec_straight_opt: list basic -> regset -> mem -> list basic -> regset -> mem -> Prop := + | exec_straight_opt_refl: forall c rs m, + exec_straight_opt c rs m c rs m + | exec_straight_opt_intro: forall c1 rs1 m1 c2 rs2 m2, + exec_straight c1 rs1 m1 c2 rs2 m2 -> + exec_straight_opt c1 rs1 m1 c2 rs2 m2. + +Remark exec_straight_opt_right: + forall c3 rs3 m3 c1 rs1 m1 c2 rs2 m2, + exec_straight_opt c1 rs1 m1 c2 rs2 m2 -> + exec_straight c2 rs2 m2 c3 rs3 m3 -> + exec_straight c1 rs1 m1 c3 rs3 m3. +Proof. + destruct 1; intros. auto. eapply exec_straight_trans; eauto. +Qed. + +Lemma exec_straight_opt_step: + forall i c rs1 m1 rs2 m2 c' rs3 m3, + exec_basic lk ge i rs1 m1 = Next rs2 m2 -> + exec_straight_opt c rs2 m2 c' rs3 m3 -> + exec_straight (i :: c) rs1 m1 c' rs3 m3. +Proof. + intros. inv H0. +- apply exec_straight_one; auto. +- eapply exec_straight_step; eauto. +Qed. + +Lemma exec_straight_opt_step_opt: + forall i c rs1 m1 rs2 m2 c' rs3 m3, + exec_basic lk ge i rs1 m1 = Next rs2 m2 -> + exec_straight_opt c rs2 m2 c' rs3 m3 -> + exec_straight_opt (i :: c) rs1 m1 c' rs3 m3. +Proof. + intros. apply exec_straight_opt_intro. eapply exec_straight_opt_step; eauto. +Qed. + +(** Linking exec_straight with exec_straight_blocks *) + +(* Lemma exec_straight_pc: + forall c c' rs1 m1 rs2 m2, + exec_straight c rs1 m1 c' rs2 m2 -> + rs2 PC = rs1 PC. +Proof. + induction c; intros; try (inv H; fail). + inv H. + - eapply exec_basic_instr_pc; eauto. + - rewrite (IHc c' rs3 m3 rs2 m2); auto. + erewrite exec_basic_instr_pc; eauto. +Qed. *) + +Lemma exec_body_pc: + forall ge l rs1 m1 rs2 m2, + exec_body lk ge l rs1 m1 = Next rs2 m2 -> + rs2 PC = rs1 PC. +Proof. + induction l. + - intros. inv H. auto. + - intros until m2. intro EXEB. + inv EXEB. destruct (exec_basic _ _ _ _ _) eqn:EBI; try discriminate. + eapply IHl in H0. rewrite H0. + destruct s. + erewrite exec_basic_instr_pc; eauto. +Qed. + +End STRAIGHTLINE. + (** * Properties of the Machblock call stack *) Section MATCH_STACK. diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v new file mode 100644 index 00000000..bc4302ca --- /dev/null +++ b/aarch64/Asmblockgenproof1.v @@ -0,0 +1,1834 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(** * Proof of correctness for individual instructions *) + +Require Import Coqlib Errors Maps Zbits. +Require Import AST Integers Floats Values Memory Globalenvs Linking. +Require Import Op Locations Machblock Conventions. +Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops. + +Module MB := Machblock. +Module AB := Asmblock. + +Section CONSTRUCTORS. + +Variable lk: aarch64_linker. +Variable ge: genv. +Variable fn: function. + +Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), + Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address ge id ofs. + +Ltac Simplif := + ((rewrite Pregmap.gss) + || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen. + +Ltac Simpl := repeat Simplif. + +Ltac ArgsInv := + repeat (match goal with + | [ H: Error _ = OK _ |- _ ] => discriminate + | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args + | [ H: bind _ _ = OK _ |- _ ] => monadInv H + | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv + | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv + end); + subst; + repeat (match goal with + | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in * + | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in * + end). + +Ltac SimplEval H := + match type of H with + | Some _ = None _ => discriminate + | Some _ = Some _ => inversion H; subst + | ?a = Some ?b => let A := fresh in assert (A: Val.maketotal a = b) by (rewrite H; reflexivity) +end. + +Ltac TranslOpSimpl := + econstructor; split; + [ apply exec_straight_one; reflexivity + | split; [ apply Val.lessdef_same; simpl; Simpl; fail | intros; simpl; Simpl; fail ] ]. + +Ltac TranslOpSimplN := + econstructor; split; + try apply exec_straight_one; try reflexivity; try split; try apply Val.lessdef_same; + Simpl; simpl; try destruct negb; Simpl; try intros; Simpl; simpl; try destruct negb; Simpl. + +Lemma preg_of_iregsp_not_PC: forall r, preg_of_iregsp r <> PC. +Proof. + destruct r; simpl; try discriminate. +Qed. +Hint Resolve preg_of_iregsp_not_PC: asmgen. + +Lemma preg_of_not_X16: forall r, preg_of r <> X16. +Proof. + destruct r; simpl; try discriminate. +Qed. + +Lemma preg_of_not_X30: forall r, preg_of r <> X30. +Proof. + destruct r; simpl; try discriminate. +Qed. + +Lemma ireg_of_not_X16: forall r x, ireg_of r = OK x -> x <> X16. +Proof. + unfold ireg_of; intros. destruct (preg_of r) eqn:E; inv H. + red; intros; subst x. elim (preg_of_not_X16 r); auto. + destruct d. destruct i. inv H1; auto. + all: discriminate. +Qed. + +Lemma ireg_of_not_X16': forall r x, ireg_of r = OK x -> IR x <> IR X16. +Proof. + intros. apply ireg_of_not_X16 in H. congruence. +Qed. + +Lemma ireg_of_not_X16'': forall r x, ireg_of r = OK x -> DR (IR x) <> DR (IR X16). +Proof. + intros. apply ireg_of_not_X16 in H. congruence. +Qed. + +Lemma ireg_of_not_X30: forall r x, ireg_of r = OK x -> x <> X30. +Proof. + unfold ireg_of; intros. destruct (preg_of r) eqn:E; inv H. + red; intros; subst x. elim (preg_of_not_X30 r); auto. + destruct d. destruct i. inv H1; auto. + all: discriminate. +Qed. + +Lemma ireg_of_not_X30': forall r x, ireg_of r = OK x -> IR x <> IR X30. +Proof. + intros. apply ireg_of_not_X30 in H. congruence. +Qed. + +Lemma ireg_of_not_X30'': forall r x, ireg_of r = OK x -> DR (IR x) <> DR (IR X30). +Proof. + intros. apply ireg_of_not_X30 in H. congruence. +Qed. + +Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16' ireg_of_not_X16'': asmgen. +Hint Resolve preg_of_not_X30 ireg_of_not_X30 ireg_of_not_X30' ireg_of_not_X30'': asmgen. + +Inductive wf_decomposition: list (Z * Z) -> Prop := + | wf_decomp_nil: + wf_decomposition nil + | wf_decomp_cons: forall m n p l, + n = Zzero_ext 16 m -> 0 <= p -> wf_decomposition l -> + wf_decomposition ((n, p) :: l). + +Lemma decompose_int_wf: + forall N n p, 0 <= p -> wf_decomposition (decompose_int N n p). +Proof. +Local Opaque Zzero_ext. + induction N as [ | N]; simpl; intros. +- constructor. +- set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0). ++ apply IHN. omega. ++ econstructor. reflexivity. omega. apply IHN; omega. +Qed. + +Fixpoint recompose_int (accu: Z) (l: list (Z * Z)) : Z := + match l with + | nil => accu + | (n, p) :: l => recompose_int (Zinsert accu n p 16) l + end. + +Lemma decompose_int_correct: + forall N n p accu, + 0 <= p -> + (forall i, p <= i -> Z.testbit accu i = false) -> + (forall i, 0 <= i < p + Z.of_nat N * 16 -> + Z.testbit (recompose_int accu (decompose_int N n p)) i = + if zlt i p then Z.testbit accu i else Z.testbit n i). +Proof. + induction N as [ | N]; intros until accu; intros PPOS ABOVE i RANGE. +- simpl. rewrite zlt_true; auto. xomega. +- rewrite inj_S in RANGE. simpl. + set (frag := Zzero_ext 16 (Z.shiftr n p)). + assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)). + { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega. + rewrite Z.shiftr_spec by omega. f_equal; omega. } + destruct (Z.eqb_spec frag 0). ++ rewrite IHN. +* destruct (zlt i p). rewrite zlt_true by omega. auto. + destruct (zlt i (p + 16)); auto. + rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto. +* omega. +* intros; apply ABOVE; omega. +* xomega. ++ simpl. rewrite IHN. +* destruct (zlt i (p + 16)). +** rewrite Zinsert_spec by omega. unfold proj_sumbool. + rewrite zlt_true by omega. + destruct (zlt i p). + rewrite zle_false by omega. auto. + rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega. +** rewrite Z.ldiff_spec, Z.shiftl_spec by omega. + change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega. + rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. +* omega. +* intros. rewrite Zinsert_spec by omega. unfold proj_sumbool. + rewrite zle_true by omega. rewrite zlt_false by omega. simpl. + apply ABOVE. omega. +* xomega. +Qed. + +Corollary decompose_int_eqmod: forall N n, + eqmod (two_power_nat (N * 16)%nat) (recompose_int 0 (decompose_int N n 0)) n. +Proof. + intros; apply eqmod_same_bits; intros. + rewrite decompose_int_correct. apply zlt_false; omega. + omega. intros; apply Z.testbit_0_l. xomega. +Qed. + +Corollary decompose_notint_eqmod: forall N n, + eqmod (two_power_nat (N * 16)%nat) + (Z.lnot (recompose_int 0 (decompose_int N (Z.lnot n) 0))) n. +Proof. + intros; apply eqmod_same_bits; intros. + rewrite Z.lnot_spec, decompose_int_correct. + rewrite zlt_false by omega. rewrite Z.lnot_spec by omega. apply negb_involutive. + omega. intros; apply Z.testbit_0_l. xomega. omega. +Qed. + +Lemma negate_decomposition_wf: + forall l, wf_decomposition l -> wf_decomposition (negate_decomposition l). +Proof. + induction 1; simpl; econstructor; auto. + instantiate (1 := (Z.lnot m)). + apply equal_same_bits; intros. + rewrite H. change 65535 with (two_p 16 - 1). + rewrite Z.lxor_spec, !Zzero_ext_spec, Z.lnot_spec, Ztestbit_two_p_m1 by omega. + destruct (zlt i 16). + apply xorb_true_r. + auto. +Qed. + +Lemma Zinsert_eqmod: + forall n x1 x2 y p l, 0 <= p -> 0 <= l -> + eqmod (two_power_nat n) x1 x2 -> + eqmod (two_power_nat n) (Zinsert x1 y p l) (Zinsert x2 y p l). +Proof. + intros. apply eqmod_same_bits; intros. rewrite ! Zinsert_spec by omega. + destruct (zle p i && zlt i (p + l)); auto. + apply same_bits_eqmod with n; auto. +Qed. + +Lemma Zinsert_0_l: + forall y p l, + 0 <= p -> 0 <= l -> + Z.shiftl (Zzero_ext l y) p = Zinsert 0 (Zzero_ext l y) p l. +Proof. + intros. apply equal_same_bits; intros. + rewrite Zinsert_spec by omega. unfold proj_sumbool. + destruct (zlt i p); [rewrite zle_false by omega|rewrite zle_true by omega]; simpl. +- rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto. +- rewrite Z.shiftl_spec by omega. + destruct (zlt i (p + l)); auto. + rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto. +Qed. + +Lemma recompose_int_negated: + forall l, wf_decomposition l -> + forall accu, recompose_int (Z.lnot accu) (negate_decomposition l) = Z.lnot (recompose_int accu l). +Proof. + induction 1; intros accu; simpl. +- auto. +- rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. + rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega. + unfold proj_sumbool. + destruct (zle p i); simpl; auto. + destruct (zlt i (p + 16)); simpl; auto. + change 65535 with (two_p 16 - 1). + rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega. + apply xorb_true_r. +Qed. + +Lemma exec_loadimm_k_w: + forall (rd: ireg) k m l, + wf_decomposition l -> + forall (rs: regset) accu, + rs#rd = Vint (Int.repr accu) -> + exists rs', + exec_straight_opt ge lk (loadimm_k W rd l k) rs m k rs' m + /\ rs'#rd = Vint (Int.repr (recompose_int accu l)) + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + induction 1; intros rs accu ACCU; simpl. +- exists rs; split. apply exec_straight_opt_refl. auto. +- destruct (IHwf_decomposition + ((rs#rd <- (insert_in_int rs#rd n p 16))) + (Zinsert accu n p 16)) + as (rs' & P & Q & R). + Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. + apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + exists rs'; split. + eapply exec_straight_opt_step_opt. simpl. eauto. auto. + split. exact Q. intros; Simpl. rewrite R by auto. Simpl. +Qed. + +Lemma exec_loadimm_z_w: + forall rd l k rs m, + wf_decomposition l -> + exists rs', + exec_straight ge lk (loadimm_z W rd l k) rs m k rs' m + /\ rs'#rd = Vint (Int.repr (recompose_int 0 l)) + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + unfold loadimm_z; destruct 1. +- econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. +- set (accu0 := Zinsert 0 n p 16). + set (rs1 := rs#rd <- (Vint (Int.repr accu0))). + destruct (exec_loadimm_k_w rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. + split. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. +Qed. + +Lemma exec_loadimm_n_w: + forall rd l k rs m, + wf_decomposition l -> + exists rs', + exec_straight ge lk (loadimm_n W rd l k) rs m k rs' m + /\ rs'#rd = Vint (Int.repr (Z.lnot (recompose_int 0 l))) + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + unfold loadimm_n; destruct 1. +- econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. +- set (accu0 := Z.lnot (Zinsert 0 n p 16)). + set (rs1 := rs#rd <- (Vint (Int.repr accu0))). + destruct (exec_loadimm_k_w rd k m (negate_decomposition l) + (negate_decomposition_wf l H1) + rs1 accu0) as (rs2 & P & Q & R). + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. + unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. + split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. +Qed. + +Lemma exec_loadimm32: + forall rd n k rs m, + exists rs', + exec_straight ge lk (loadimm32 rd n k) rs m k rs' m + /\ rs'#rd = Vint n + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + unfold loadimm32, loadimm; intros. + destruct (is_logical_imm32 n). +- econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite Int.repr_unsigned, Int.or_zero_l; auto. + intros; Simpl. +- set (dz := decompose_int 2%nat (Int.unsigned n) 0). + set (dn := decompose_int 2%nat (Z.lnot (Int.unsigned n)) 0). + assert (A: Int.repr (recompose_int 0 dz) = n). + { transitivity (Int.repr (Int.unsigned n)). + apply Int.eqm_samerepr. apply decompose_int_eqmod. + apply Int.repr_unsigned. } + assert (B: Int.repr (Z.lnot (recompose_int 0 dn)) = n). + { transitivity (Int.repr (Int.unsigned n)). + apply Int.eqm_samerepr. apply decompose_notint_eqmod. + apply Int.repr_unsigned. } + destruct Nat.leb. ++ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega. ++ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. +Qed. + +Lemma exec_loadimm_k_x: + forall (rd: ireg) k m l, + wf_decomposition l -> + forall (rs: regset) accu, + rs#rd = Vlong (Int64.repr accu) -> + exists rs', + exec_straight_opt ge lk (loadimm_k X rd l k) rs m k rs' m + /\ rs'#rd = Vlong (Int64.repr (recompose_int accu l)) + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + induction 1; intros rs accu ACCU; simpl. +- exists rs; split. apply exec_straight_opt_refl. auto. +- destruct (IHwf_decomposition + (rs#rd <- (insert_in_long rs#rd n p 16)) + (Zinsert accu n p 16)) + as (rs' & P & Q & R). + Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. + apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. + exists rs'; split. + eapply exec_straight_opt_step_opt. simpl; eauto. auto. + split. exact Q. intros; Simpl. rewrite R by auto. Simpl. +Qed. + +Lemma exec_loadimm_z_x: + forall rd l k rs m, + wf_decomposition l -> + exists rs', + exec_straight ge lk (loadimm_z X rd l k) rs m k rs' m + /\ rs'#rd = Vlong (Int64.repr (recompose_int 0 l)) + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + unfold loadimm_z; destruct 1. +- econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. +- set (accu0 := Zinsert 0 n p 16). + set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). + destruct (exec_loadimm_k_x rd k m l H1 rs1 accu0) as (rs2 & P & Q & R); auto. + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. + split. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. +Qed. + +Lemma exec_loadimm_n_x: + forall rd l k rs m, + wf_decomposition l -> + exists rs', + exec_straight ge lk (loadimm_n X rd l k) rs m k rs' m + /\ rs'#rd = Vlong (Int64.repr (Z.lnot (recompose_int 0 l))) + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + unfold loadimm_n; destruct 1. +- econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. + intros; Simpl. +- set (accu0 := Z.lnot (Zinsert 0 n p 16)). + set (rs1 := rs#rd <- (Vlong (Int64.repr accu0))). + destruct (exec_loadimm_k_x rd k m (negate_decomposition l) + (negate_decomposition_wf l H1) + rs1 accu0) as (rs2 & P & Q & R). + unfold rs1; Simpl. + exists rs2; split. + eapply exec_straight_opt_step; eauto. + simpl. unfold rs1. do 5 f_equal. + unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. + split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. + intros. rewrite R by auto. unfold rs1; Simpl. +Qed. + +Lemma exec_loadimm64: + forall rd n k rs m, + exists rs', + exec_straight ge lk (loadimm64 rd n k) rs m k rs' m + /\ rs'#rd = Vlong n + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + unfold loadimm64, loadimm; intros. + destruct (is_logical_imm64 n). +- econstructor; split. + apply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite Int64.repr_unsigned, Int64.or_zero_l; auto. + intros; Simpl. +- set (dz := decompose_int 4%nat (Int64.unsigned n) 0). + set (dn := decompose_int 4%nat (Z.lnot (Int64.unsigned n)) 0). + assert (A: Int64.repr (recompose_int 0 dz) = n). + { transitivity (Int64.repr (Int64.unsigned n)). + apply Int64.eqm_samerepr. apply decompose_int_eqmod. + apply Int64.repr_unsigned. } + assert (B: Int64.repr (Z.lnot (recompose_int 0 dn)) = n). + { transitivity (Int64.repr (Int64.unsigned n)). + apply Int64.eqm_samerepr. apply decompose_notint_eqmod. + apply Int64.repr_unsigned. } + destruct Nat.leb. ++ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega. ++ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. +Qed. + +(** Add immediate *) + +Lemma exec_addimm_aux_32: + forall (insn: Z -> arith_pp) (sem: val -> val -> val), + (forall rd r1 n rs m, + exec_basic lk ge (PArith (PArithPP (insn n) rd r1)) rs m = + Next (rs#rd <- (sem rs#r1 (Vint (Int.repr n)))) m) -> + (forall v n1 n2, sem (sem v (Vint n1)) (Vint n2) = sem v (Vint (Int.add n1 n2))) -> + forall rd r1 n k rs m, + exists rs', + exec_straight ge lk (addimm_aux insn rd r1 (Int.unsigned n) k) rs m k rs' m + /\ rs'#rd = sem rs#r1 (Vint n) + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + intros insn sem SEM ASSOC; intros. unfold addimm_aux. + set (nlo := Zzero_ext 12 (Int.unsigned n)). set (nhi := Int.unsigned n - nlo). + assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega). + rewrite <- (Int.repr_unsigned n). + destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)]. +- econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. +- econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. +- econstructor; split. eapply exec_straight_two. + apply SEM. apply SEM. simpl. Simpl. + split. Simpl. simpl. rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr. + rewrite E. auto with ints. + intros; Simpl. +Qed. + +Lemma exec_addimm32: + forall (rd r1: ireg) n k rs m, + r1 <> X16 -> + exists rs', + exec_straight ge lk (addimm32 rd r1 n k) rs m k rs' m + /\ rs'#rd = Val.add rs#r1 (Vint n) + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + intros. unfold addimm32. set (nn := Int.neg n). + destruct (Int.eq n (Int.zero_ext 24 n)); [| destruct (Int.eq nn (Int.zero_ext 24 nn))]. +- apply exec_addimm_aux_32 with (sem := Val.add). auto. intros; apply Val.add_assoc. +- rewrite <- Val.sub_opp_add. + apply exec_addimm_aux_32 with (sem := Val.sub). auto. + intros. rewrite ! Val.sub_add_opp, Val.add_assoc. rewrite Int.neg_add_distr. auto. +- destruct (Int.lt n Int.zero). ++ rewrite <- Val.sub_opp_add; fold nn. + edestruct (exec_loadimm32 X16 nn) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite B, C; eauto with asmgen. + intros; Simpl. ++ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. + split. Simpl. rewrite B, C; eauto with asmgen. + intros; Simpl. +Qed. + +Lemma exec_addimm_aux_64: + forall (insn: Z -> arith_pp) (sem: val -> val -> val), + (forall rd r1 n rs m, + exec_basic lk ge (PArith (PArithPP (insn n) rd r1)) rs m = + Next (rs#rd <- (sem rs#r1 (Vlong (Int64.repr n)))) m) -> + (forall v n1 n2, sem (sem v (Vlong n1)) (Vlong n2) = sem v (Vlong (Int64.add n1 n2))) -> + forall rd r1 n k rs m, + exists rs', + exec_straight ge lk (addimm_aux insn rd r1 (Int64.unsigned n) k) rs m k rs' m + /\ rs'#rd = sem rs#r1 (Vlong n) + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + intros insn sem SEM ASSOC; intros. unfold addimm_aux. + set (nlo := Zzero_ext 12 (Int64.unsigned n)). set (nhi := Int64.unsigned n - nlo). + assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; omega). + rewrite <- (Int64.repr_unsigned n). + destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)]. +- econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. +- econstructor; split. apply exec_straight_one. apply SEM. Simpl. + split. Simpl. do 3 f_equal; omega. + intros; Simpl. +- econstructor; split. eapply exec_straight_two. + apply SEM. apply SEM. Simpl. Simpl. + split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int64.eqm_samerepr. + rewrite E. auto with ints. + intros; Simpl. +Qed. + +Lemma exec_addimm64: + forall (rd r1: iregsp) n k rs m, + r1 <> X16 -> + exists rs', + exec_straight ge lk (addimm64 rd r1 n k) rs m k rs' m + /\ rs'#rd = Val.addl rs#r1 (Vlong n) + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + intros. + unfold addimm64. set (nn := Int64.neg n). + destruct (Int64.eq n (Int64.zero_ext 24 n)); [| destruct (Int64.eq nn (Int64.zero_ext 24 nn))]. +- apply exec_addimm_aux_64 with (sem := Val.addl). auto. intros; apply Val.addl_assoc. +- rewrite <- Val.subl_opp_addl. + apply exec_addimm_aux_64 with (sem := Val.subl). auto. + intros. rewrite ! Val.subl_addl_opp, Val.addl_assoc. rewrite Int64.neg_add_distr. auto. +- destruct (Int64.lt n Int64.zero). ++ rewrite <- Val.subl_opp_addl; fold nn. + edestruct (exec_loadimm64 X16 nn) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. + split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. + intros; Simpl. ++ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. Simpl. + split. Simpl. rewrite B, C; eauto with asmgen. simpl. rewrite Int64.shl'_zero. auto. + intros; Simpl. +Qed. + +(** Logical immediate *) + +Lemma exec_logicalimm32: + forall (insn1: Z -> arith_rr0) + (insn2: shift_op -> arith_rr0r) + (sem: val -> val -> val), + (forall rd r1 n rs m, + exec_basic lk ge (PArith (PArithRR0 (insn1 n) rd r1)) rs m = + Next (rs#rd <- (sem rs##r1 (Vint (Int.repr n)))) m) -> + (forall rd r1 r2 s rs m, + exec_basic lk ge (PArith (PArithRR0R (insn2 s) rd r1 r2)) rs m = + Next (rs#rd <- (sem rs##r1 (eval_shift_op_int rs#r2 s))) m) -> + forall rd r1 n k rs m, + r1 <> X16 -> + exists rs', + exec_straight ge lk (logicalimm32 insn1 insn2 rd r1 n k) rs m k rs' m + /\ rs'#rd = sem rs#r1 (Vint n) + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + intros until sem; intros SEM1 SEM2; intros. unfold logicalimm32. + destruct (is_logical_imm32 n). +- econstructor; split. + apply exec_straight_one. apply SEM1. + split. Simpl. rewrite Int.repr_unsigned; auto. intros; Simpl. +- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. apply SEM2. + split. Simpl. f_equal; auto. apply C; auto with asmgen. + intros; Simpl. +Qed. + +Lemma exec_logicalimm64: + forall (insn1: Z -> arith_rr0) + (insn2: shift_op -> arith_rr0r) + (sem: val -> val -> val), + (forall rd r1 n rs m, + exec_basic lk ge (PArith (PArithRR0 (insn1 n) rd r1)) rs m = + Next (rs#rd <- (sem rs###r1 (Vlong (Int64.repr n)))) m) -> + (forall rd r1 r2 s rs m, + exec_basic lk ge (PArith (PArithRR0R (insn2 s) rd r1 r2)) rs m = + Next (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s))) m) -> + forall rd r1 n k rs m, + r1 <> X16 -> + exists rs', + exec_straight ge lk (logicalimm64 insn1 insn2 rd r1 n k) rs m k rs' m + /\ rs'#rd = sem rs#r1 (Vlong n) + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + intros until sem; intros SEM1 SEM2; intros. unfold logicalimm64. + destruct (is_logical_imm64 n). +- econstructor; split. + apply exec_straight_one. apply SEM1. + split. Simpl. rewrite Int64.repr_unsigned. auto. intros; Simpl. +- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. apply SEM2. + split. Simpl. f_equal; auto. apply C; auto with asmgen. + intros; Simpl. +Qed. + +(** Load address of symbol *) + +Lemma exec_loadsymbol: forall rd s ofs k rs m, + rd <> X16 \/ Archi.pic_code tt = false -> + exists rs', + exec_straight ge lk (loadsymbol rd s ofs k) rs m k rs' m + /\ rs'#rd = Genv.symbol_address ge s ofs + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + unfold loadsymbol; intros. destruct (Archi.pic_code tt). +- predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero. ++ subst ofs. econstructor; split. + apply exec_straight_one. simpl; eauto. + split. Simpl. intros; Simpl. ++ exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence. + intros (rs1 & A & B & C). + econstructor; split. + econstructor. simpl; eauto. auto. eexact A. + split. simpl in B; rewrite B. Simpl. + rewrite <- Genv.shift_symbol_address_64 by auto. + rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto. + intros. rewrite C by auto. Simpl. +- econstructor; split. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. + intros; Simpl. +Qed. + +(** Shifted operands *) + +Remark transl_shift_not_none: + forall s a, transl_shift s a <> SOnone. +Proof. + destruct s; intros; simpl; congruence. +Qed. + +Remark or_zero_eval_shift_op_int: + forall v s, s <> SOnone -> Val.or (Vint Int.zero) (eval_shift_op_int v s) = eval_shift_op_int v s. +Proof. + intros; destruct s; try congruence; destruct v; auto; simpl; + destruct (Int.ltu n Int.iwordsize); auto; rewrite Int.or_zero_l; auto. +Qed. + +Remark or_zero_eval_shift_op_long: + forall v s, s <> SOnone -> Val.orl (Vlong Int64.zero) (eval_shift_op_long v s) = eval_shift_op_long v s. +Proof. + intros; destruct s; try congruence; destruct v; auto; simpl; + destruct (Int.ltu n Int64.iwordsize'); auto; rewrite Int64.or_zero_l; auto. +Qed. + +Remark add_zero_eval_shift_op_long: + forall v s, s <> SOnone -> Val.addl (Vlong Int64.zero) (eval_shift_op_long v s) = eval_shift_op_long v s. +Proof. + intros; destruct s; try congruence; destruct v; auto; simpl; + destruct (Int.ltu n Int64.iwordsize'); auto; rewrite Int64.add_zero_l; auto. +Qed. + +Lemma transl_eval_shift: forall s v (a: amount32), + eval_shift_op_int v (transl_shift s a) = eval_shift s v a. +Proof. + intros. destruct s; simpl; auto. +Qed. + +Lemma transl_eval_shift': forall s v (a: amount32), + Val.or (Vint Int.zero) (eval_shift_op_int v (transl_shift s a)) = eval_shift s v a. +Proof. + intros. rewrite or_zero_eval_shift_op_int by (apply transl_shift_not_none). + apply transl_eval_shift. +Qed. + +Lemma transl_eval_shiftl: forall s v (a: amount64), + eval_shift_op_long v (transl_shift s a) = eval_shiftl s v a. +Proof. + intros. destruct s; simpl; auto. +Qed. + +Lemma transl_eval_shiftl': forall s v (a: amount64), + Val.orl (Vlong Int64.zero) (eval_shift_op_long v (transl_shift s a)) = eval_shiftl s v a. +Proof. + intros. rewrite or_zero_eval_shift_op_long by (apply transl_shift_not_none). + apply transl_eval_shiftl. +Qed. + +Lemma transl_eval_shiftl'': forall s v (a: amount64), + Val.addl (Vlong Int64.zero) (eval_shift_op_long v (transl_shift s a)) = eval_shiftl s v a. +Proof. + intros. rewrite add_zero_eval_shift_op_long by (apply transl_shift_not_none). + apply transl_eval_shiftl. +Qed. + +(** Zero- and Sign- extensions *) + +Lemma exec_move_extended_base: forall rd r1 ex k rs m, + exists rs', + exec_straight ge lk (move_extended_base rd r1 ex k) rs m k rs' m + /\ rs' rd = match ex with Xsgn32 => Val.longofint rs#r1 | Xuns32 => Val.longofintu rs#r1 end + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + unfold move_extended_base; destruct ex; econstructor; + (split; [apply exec_straight_one; simpl; eauto | split; [Simpl|intros;Simpl]]). +Qed. + +Lemma exec_move_extended: forall rd r1 ex (a: amount64) k rs m, + exists rs', + exec_straight ge lk (move_extended rd r1 ex a k) rs m k rs' m + /\ rs' rd = Op.eval_extend ex rs#r1 a + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + unfold move_extended; intros. predSpec Int.eq Int.eq_spec a Int.zero. +- exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). + exists rs'; split. eexact A. split. unfold Op.eval_extend. rewrite H. rewrite B. + destruct ex, (rs r1); simpl; auto; rewrite Int64.shl'_zero; auto. + auto. +- Local Opaque Val.addl. + exploit (exec_move_extended_base rd r1 ex). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + change (SOlsl a) with (transl_shift Slsl a). rewrite transl_eval_shiftl''. eauto. auto. + split. Simpl. rewrite B. auto. + intros; Simpl. +Qed. + +Lemma exec_arith_extended: + forall (sem: val -> val -> val) + (insnX: extend_op -> arith_ppp) + (insnS: shift_op -> arith_rr0r), + (forall rd r1 r2 x rs m, + exec_basic lk ge (PArith (PArithPPP (insnX x) rd r1 r2)) rs m = + Next (rs#rd <- (sem rs#r1 (eval_extend rs#r2 x))) m) -> + (forall rd r1 r2 s rs m, + exec_basic lk ge (PArith (PArithRR0R (insnS s) rd r1 r2)) rs m = + Next (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s))) m) -> + forall (rd r1 r2: ireg) (ex: extension) (a: amount64) (k: bcode) rs m, + r1 <> X16 -> + exists rs', + exec_straight ge lk (arith_extended insnX insnS rd r1 r2 ex a k) rs m k rs' m + /\ rs'#rd = sem rs#r1 (Op.eval_extend ex rs#r2 a) + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + intros sem insnX insnS EX ES; intros. unfold arith_extended. destruct (Int.ltu a (Int.repr 5)). +- econstructor; split. + apply exec_straight_one. rewrite EX; eauto. auto. + split. Simpl. f_equal. destruct ex; auto. + intros; Simpl. +- exploit (exec_move_extended_base X16 r2 ex). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + rewrite ES. eauto. auto. + split. Simpl. unfold ir0. rewrite C by eauto with asmgen. f_equal. + rewrite B. destruct ex; auto. + intros; Simpl. +Qed. + +(** Extended right shift *) + +Lemma exec_shrx32: forall (rd r1: ireg) (n: int) k v (rs: regset) m, + Val.shrx rs#r1 (Vint n) = Some v -> + r1 <> X16 -> + exists rs', + exec_straight ge lk (shrx32 rd r1 n k) rs m k rs' m + /\ rs'#rd = v + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + unfold shrx32; intros. apply Val.shrx_shr_2 in H. + destruct (Int.eq n Int.zero) eqn:E0. +- econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. subst v; auto. intros; Simpl. +- econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + split. subst v; Simpl. intros; Simpl. +Qed. + +Lemma exec_shrx32_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, + Val.shrx rs#r1 (Vint n) = None -> + r1 <> X16 -> + exists rs', + exec_straight ge lk (shrx32 rd r1 n k) rs m k rs' m + /\ Val.lessdef (Val.maketotal None) (rs' x) + /\ forall r, data_preg r = true -> r <> rd -> preg_notin r (destroyed_by_op (Oshrximm n)) -> rs'#r = rs#r. +Proof. + unfold shrx32; intros. + destruct (Int.eq n Int.zero) eqn:E0. +- econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. auto. intros; Simpl. +- econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_int by congruence. eauto. + split. Simpl. intros; Simpl. +Qed. + +Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m, + Val.shrxl rs#r1 (Vint n) = Some v -> + r1 <> X16 -> + exists rs', + exec_straight ge lk (shrx64 rd r1 n k) rs m k rs' m + /\ rs'#rd = v + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + unfold shrx64; intros. apply Val.shrxl_shrl_2 in H. + destruct (Int.eq n Int.zero) eqn:E. +- econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. subst v; auto. intros; Simpl. +- econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + split. subst v; Simpl. intros; Simpl. +Qed. + +Lemma exec_shrx64_none: forall (rd r1: ireg) (n: int) k x (rs: regset) m, + Val.shrxl rs#r1 (Vint n) = None -> + r1 <> X16 -> + exists rs', + exec_straight ge lk (shrx64 rd r1 n k) rs m k rs' m + /\ Val.lessdef (Val.maketotal None) (rs' x) + /\ forall r, data_preg r = true -> r <> rd -> preg_notin r (destroyed_by_op (Oshrximm n)) -> rs'#r = rs#r. +Proof. + unfold shrx64; intros. + destruct (Int.eq n Int.zero) eqn:E. +- econstructor; split. apply exec_straight_one; simpl; eauto. + split. Simpl. auto. intros; Simpl. +- econstructor; split. eapply exec_straight_three. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + simpl; eauto. + unfold exec_basic, exec_arith_instr, arith_eval_rr0r. + rewrite or_zero_eval_shift_op_long by congruence. eauto. + split. Simpl. intros; Simpl. +Qed. + +Ltac TranslOpBase := + econstructor; split; + [ apply exec_straight_one; [simpl; eauto ] + | split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl; Simpl + | intros; Simpl; fail ] ]. + +(** Condition bits *) + +Lemma compare_int_spec: forall rs v1 v2, + let rs' := compare_int rs v1 v2 in + rs'#CN = (Val.negative (Val.sub v1 v2)) + /\ rs'#CZ = (Val_cmpu Ceq v1 v2) + /\ rs'#CC = (Val_cmpu Cge v1 v2) + /\ rs'#CV = (Val.sub_overflow v1 v2). +Proof. + intros; unfold rs'; auto. +Qed. + +Lemma eval_testcond_compare_sint: forall c v1 v2 b rs, + Val.cmp_bool c v1 v2 = Some b -> + eval_testcond (cond_for_signed_cmp c) (compare_int rs v1 v2) = Some b. +Proof. + intros. generalize (compare_int_spec rs v1 v2). + set (rs' := compare_int rs v1 v2). intros (B & C & D & E). + unfold eval_testcond; rewrite B, C, D, E. + destruct v1; try discriminate; destruct v2; try discriminate. + simpl in H; inv H. + unfold Val_cmpu; simpl. destruct c; simpl. +- destruct (Int.eq i i0); auto. +- destruct (Int.eq i i0); auto. +- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. +- rewrite Int.lt_sub_overflow, Int.not_lt. + destruct (Int.eq i i0), (Int.lt i i0); auto. +- rewrite Int.lt_sub_overflow, (Int.lt_not i). + destruct (Int.eq i i0), (Int.lt i i0); auto. +- rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. +Qed. + +Lemma eval_testcond_compare_uint: forall c v1 v2 b rs, + Val_cmpu_bool c v1 v2 = Some b -> + eval_testcond (cond_for_unsigned_cmp c) (compare_int rs v1 v2) = Some b. +Proof. + intros. generalize (compare_int_spec rs v1 v2). + set (rs' := compare_int rs v1 v2). intros (B & C & D & E). + unfold eval_testcond; rewrite B, C, D, E. + destruct v1; try discriminate; destruct v2; try discriminate. + simpl in H; inv H. + unfold Val_cmpu; simpl. destruct c; simpl. +- destruct (Int.eq i i0); auto. +- destruct (Int.eq i i0); auto. +- destruct (Int.ltu i i0); auto. +- rewrite (Int.not_ltu i). destruct (Int.eq i i0), (Int.ltu i i0); auto. +- rewrite (Int.ltu_not i). destruct (Int.eq i i0), (Int.ltu i i0); auto. +- destruct (Int.ltu i i0); auto. +Qed. + +Lemma compare_long_spec: forall rs v1 v2, + let rs' := compare_long rs v1 v2 in + rs'#CN = (Val.negativel (Val.subl v1 v2)) + /\ rs'#CZ = (Val_cmplu Ceq v1 v2) + /\ rs'#CC = (Val_cmplu Cge v1 v2) + /\ rs'#CV = (Val.subl_overflow v1 v2). +Proof. + intros; unfold rs'; auto. +Qed. + +Remark int64_sub_overflow: + forall x y, + Int.xor (Int.repr (Int64.unsigned (Int64.sub_overflow x y Int64.zero))) + (Int.repr (Int64.unsigned (Int64.negative (Int64.sub x y)))) = + (if Int64.lt x y then Int.one else Int.zero). +Proof. + intros. + transitivity (Int.repr (Int64.unsigned (if Int64.lt x y then Int64.one else Int64.zero))). + rewrite <- (Int64.lt_sub_overflow x y). + unfold Int64.sub_overflow, Int64.negative. + set (s := Int64.signed x - Int64.signed y - Int64.signed Int64.zero). + destruct (zle Int64.min_signed s && zle s Int64.max_signed); + destruct (Int64.lt (Int64.sub x y) Int64.zero); + auto. + destruct (Int64.lt x y); auto. +Qed. + +Lemma eval_testcond_compare_slong: forall c v1 v2 b rs, + Val.cmpl_bool c v1 v2 = Some b -> + eval_testcond (cond_for_signed_cmp c) (compare_long rs v1 v2) = Some b. +Proof. + intros. generalize (compare_long_spec rs v1 v2). + set (rs' := compare_long rs v1 v2). intros (B & C & D & E). + unfold eval_testcond; rewrite B, C, D, E. + destruct v1; try discriminate; destruct v2; try discriminate. + simpl in H; inv H. + unfold Val_cmplu; simpl. destruct c; simpl. +- destruct (Int64.eq i i0); auto. +- destruct (Int64.eq i i0); auto. +- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. +- rewrite int64_sub_overflow, Int64.not_lt. + destruct (Int64.eq i i0), (Int64.lt i i0); auto. +- rewrite int64_sub_overflow, (Int64.lt_not i). + destruct (Int64.eq i i0), (Int64.lt i i0); auto. +- rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. +Qed. + +Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs, + Val_cmplu_bool c v1 v2 = Some b -> + eval_testcond (cond_for_unsigned_cmp c) (compare_long rs v1 v2) = Some b. +Proof. + intros. generalize (compare_long_spec rs v1 v2). + set (rs' := compare_long rs v1 v2). intros (B & C & D & E). + unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu. + destruct v1; try discriminate; destruct v2; try discriminate; simpl in H. +- (* int-int *) + inv H. destruct c; simpl. ++ destruct (Int64.eq i i0); auto. ++ destruct (Int64.eq i i0); auto. ++ destruct (Int64.ltu i i0); auto. ++ rewrite (Int64.not_ltu i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. ++ rewrite (Int64.ltu_not i). destruct (Int64.eq i i0), (Int64.ltu i i0); auto. ++ destruct (Int64.ltu i i0); auto. +- (* int-ptr *) + simpl. + destruct (Archi.ptr64); simpl; try discriminate. + destruct (Int64.eq i Int64.zero); simpl; try discriminate. + destruct c; simpl in H; inv H; reflexivity. +- (* ptr-int *) + simpl. + destruct (Archi.ptr64); simpl; try discriminate. + destruct (Int64.eq i0 Int64.zero); try discriminate. + destruct c; simpl in H; inv H; reflexivity. +- (* ptr-ptr *) + simpl. + destruct (eq_block b0 b1). + destruct (Archi.ptr64); simpl; try discriminate. + inv H. + destruct c; simpl. +* destruct (Ptrofs.eq i i0); auto. +* destruct (Ptrofs.eq i i0); auto. +* destruct (Ptrofs.ltu i i0); auto. +* rewrite (Ptrofs.not_ltu i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. +* rewrite (Ptrofs.ltu_not i). destruct (Ptrofs.eq i i0), (Ptrofs.ltu i i0); auto. +* destruct (Ptrofs.ltu i i0); auto. +* destruct c; simpl in H; inv H; reflexivity. +Qed. + +Lemma compare_float_spec: forall rs f1 f2, + let rs' := compare_float rs (Vfloat f1) (Vfloat f2) in + rs'#CN = (Val.of_bool (Float.cmp Clt f1 f2)) + /\ rs'#CZ = (Val.of_bool (Float.cmp Ceq f1 f2)) + /\ rs'#CC = (Val.of_bool (negb (Float.cmp Clt f1 f2))) + /\ rs'#CV = (Val.of_bool (negb (Float.ordered f1 f2))). +Proof. + intros; auto. +Qed. + +Lemma eval_testcond_compare_float: forall c v1 v2 b rs, + Val.cmpf_bool c v1 v2 = Some b -> + eval_testcond (cond_for_float_cmp c) (compare_float rs v1 v2) = Some b. +Proof. + intros. destruct v1; try discriminate; destruct v2; simpl in H; inv H. + generalize (compare_float_spec rs f f0). + set (rs' := compare_float rs (Vfloat f) (Vfloat f0)). + intros (B & C & D & E). + unfold eval_testcond; rewrite B, C, D, E. +Local Transparent Float.cmp Float.ordered. + unfold Float.cmp, Float.ordered; + destruct c; destruct (Float.compare f f0) as [[]|]; reflexivity. +Qed. + +Lemma eval_testcond_compare_not_float: forall c v1 v2 b rs, + option_map negb (Val.cmpf_bool c v1 v2) = Some b -> + eval_testcond (cond_for_float_not_cmp c) (compare_float rs v1 v2) = Some b. +Proof. + intros. destruct v1; try discriminate; destruct v2; simpl in H; inv H. + generalize (compare_float_spec rs f f0). + set (rs' := compare_float rs (Vfloat f) (Vfloat f0)). + intros (B & C & D & E). + unfold eval_testcond; rewrite B, C, D, E. +Local Transparent Float.cmp Float.ordered. + unfold Float.cmp, Float.ordered; + destruct c; destruct (Float.compare f f0) as [[]|]; reflexivity. +Qed. + +Lemma compare_single_spec: forall rs f1 f2, + let rs' := compare_single rs (Vsingle f1) (Vsingle f2) in + rs'#CN = (Val.of_bool (Float32.cmp Clt f1 f2)) + /\ rs'#CZ = (Val.of_bool (Float32.cmp Ceq f1 f2)) + /\ rs'#CC = (Val.of_bool (negb (Float32.cmp Clt f1 f2))) + /\ rs'#CV = (Val.of_bool (negb (Float32.ordered f1 f2))). +Proof. + intros; auto. +Qed. + +Lemma eval_testcond_compare_single: forall c v1 v2 b rs, + Val.cmpfs_bool c v1 v2 = Some b -> + eval_testcond (cond_for_float_cmp c) (compare_single rs v1 v2) = Some b. +Proof. + intros. destruct v1; try discriminate; destruct v2; simpl in H; inv H. + generalize (compare_single_spec rs f f0). + set (rs' := compare_single rs (Vsingle f) (Vsingle f0)). + intros (B & C & D & E). + unfold eval_testcond; rewrite B, C, D, E. +Local Transparent Float32.cmp Float32.ordered. + unfold Float32.cmp, Float32.ordered; + destruct c; destruct (Float32.compare f f0) as [[]|]; reflexivity. +Qed. + +Lemma eval_testcond_compare_not_single: forall c v1 v2 b rs, + option_map negb (Val.cmpfs_bool c v1 v2) = Some b -> + eval_testcond (cond_for_float_not_cmp c) (compare_single rs v1 v2) = Some b. +Proof. + intros. destruct v1; try discriminate; destruct v2; simpl in H; inv H. + generalize (compare_single_spec rs f f0). + set (rs' := compare_single rs (Vsingle f) (Vsingle f0)). + intros (B & C & D & E). + unfold eval_testcond; rewrite B, C, D, E. +Local Transparent Float32.cmp Float32.ordered. + unfold Float32.cmp, Float32.ordered; + destruct c; destruct (Float32.compare f f0) as [[]|]; reflexivity. +Qed. + +Remark compare_float_inv: forall rs v1 v2 r, + match r with CR _ => False | _ => True end -> + (compare_float rs v1 v2)#r = rs#r. +Proof. + intros; unfold compare_float. + destruct r; try contradiction; destruct v1; auto; destruct v2; auto. +Qed. + +Remark compare_single_inv: forall rs v1 v2 r, + match r with CR _ => False | _ => True end -> + (compare_single rs v1 v2)#r = rs#r. +Proof. + intros; unfold compare_single. + destruct r; try contradiction; destruct v1; auto; destruct v2; auto. +Qed. + +Lemma transl_cbranch_correct: + forall cond args lbl k c m ms b sp rs m' bdy t ofs, + transl_cond_branch cond args lbl k = OK (bdy, c) -> + eval_condition cond (List.map ms args) m = Some b -> + agree ms sp rs -> + Mem.extends m m' -> + exists rs' m' rs'' m'', + exec_body lk ge bdy rs m = Next rs' m' + /\ exec_exit ge fn ofs rs' m' (Some c) t rs'' m'' + /\ forall r, data_preg r = true -> rs'#r = rs#r. +Proof. +Admitted. + +(* Lemma transl_cbranch_correct_true: + forall cond args lbl k c m ms sp rs m' bdy, + transl_cond_branch cond args lbl k = OK (bdy, c) -> + eval_condition cond (List.map ms args) m = Some true -> + agree ms sp rs -> + Mem.extends m m' -> + exists rs', exists insn, + exec_straight_opt ge lk bdy rs m' k rs' m' + /\ exec_cfi ge fn insn (nextinstr rs') m' = goto_label fn lbl (nextinstr rs') m' + /\ forall r, data_preg r = true -> rs'#r = rs#r. +Proof. + intros. eapply transl_cbranch_correct_1 with (b := true); eauto. +Qed. *) + +Lemma transl_cond_correct: + forall cond args k c rs m, + transl_cond cond args k = OK c -> + exists rs', + exec_straight ge lk c rs m k rs' m + /\ (forall b, + eval_condition cond (map rs (map preg_of args)) m = Some b -> + eval_testcond (cond_for_cond cond) rs' = Some b) + /\ forall r, data_preg r = true -> rs'#r = rs#r. +Proof. + intros until m; intros TR. destruct cond; simpl in TR; ArgsInv. +- (* Ccomp *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. +- (* Ccompu *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. +- (* Ccompimm *) + destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. ++ econstructor; split. + apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. + split; intros. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply eval_testcond_compare_sint; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. +- (* Ccompuimm *) + destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. ++ econstructor; split. + apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto. + split; intros. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply eval_testcond_compare_uint; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. +- (* Ccompshift *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_sint; auto. + destruct r; reflexivity || discriminate. +- (* Ccompushift *) + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite transl_eval_shift. apply eval_testcond_compare_uint; auto. + destruct r; reflexivity || discriminate. +- (* Cmaskzero *) + destruct (is_logical_imm32 n). ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply (eval_testcond_compare_sint Ceq); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. +- (* Cmasknotzero *) + destruct (is_logical_imm32 n). ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply (eval_testcond_compare_sint Cne); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. +- (* Ccompl *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. +- (* Ccomplu *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. +- (* Ccomplimm *) + destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. ++ econstructor; split. + apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. + split; intros. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. auto. + split; intros. apply eval_testcond_compare_slong; auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. +- (* Ccompluimm *) + destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. ++ econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. ++ econstructor; split. + apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. + split; intros. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. + simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. +- (* Ccomplshift *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_slong; auto. + destruct r; reflexivity || discriminate. +- (* Ccomplushift *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. + erewrite Val_cmplu_bool_correct; eauto. + destruct r; reflexivity || discriminate. +- (* Cmasklzero *) + destruct (is_logical_imm64 n). ++ econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply (eval_testcond_compare_slong Ceq); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. +- (* Cmasknotzero *) + destruct (is_logical_imm64 n). ++ econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto. + destruct r; reflexivity || discriminate. ++ exploit (exec_loadimm64 X16 n). intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. + apply exec_straight_one. simpl. rewrite B, C by eauto with asmgen. eauto. + split; intros. apply (eval_testcond_compare_slong Cne); auto. + transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. +- (* Ccompf *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Cnotcompf *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Ccompfzero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Cnotcompfzero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_float; auto. + destruct r; discriminate || rewrite compare_float_inv; auto. +- (* Ccompfs *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +- (* Cnotcompfs *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +- (* Ccompfszero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +- (* Cnotcompfszero *) + econstructor; split. apply exec_straight_one. simpl; eauto. + split; intros. apply eval_testcond_compare_not_single; auto. + destruct r; discriminate || rewrite compare_single_inv; auto. +Qed. + +Lemma transl_op_correct: + forall op args res k (rs: regset) m v c, + transl_op op args res k = OK c -> + eval_operation ge (rs#SP) op (map rs (map preg_of args)) m = Some v -> + exists rs', + exec_straight ge lk c rs m k rs' m + /\ Val.lessdef v rs'#(preg_of res) + /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. +Proof. + (* assert (SAME: forall v1 v2, v1 = v2 -> Val.lessdef v2 v1). { intros; subst; auto. } *) +Local Opaque Int.eq Int64.eq Val.add Val.addl Int.zwordsize Int64.zwordsize. + intros until c; intros TR EV. + unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl; + try (rewrite <- transl_eval_shift; TranslOpSimpl). +- (* move *) + destruct (preg_of res), (preg_of m0); try destruct d; try destruct d0; inv TR; TranslOpSimpl. +- (* intconst *) + exploit exec_loadimm32. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. +- (* longconst *) + exploit exec_loadimm64. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. intros; auto with asmgen. +- (* floatconst *) + destruct (Float.eq_dec n Float.zero). ++ subst n. TranslOpSimpl. ++ TranslOpSimplN. +- (* singleconst *) + destruct (Float32.eq_dec n Float32.zero). ++ subst n. TranslOpSimpl. ++ TranslOpSimplN. +- (* loadsymbol *) + exploit (exec_loadsymbol x id ofs). eauto with asmgen. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. +- (* addrstack *) + exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)); try discriminate. simpl; eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. replace (DR XSP) with (SP) in B by auto. rewrite B. +Local Transparent Val.addl. + destruct (rs SP); simpl; auto. rewrite Ptrofs.of_int64_to_int64 by auto. auto. + auto. +- (* shift *) + rewrite <- transl_eval_shift'. TranslOpSimpl. +- (* addimm *) + exploit (exec_addimm32 x x0 n). eauto with asmgen. intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. +- (* mul *) + TranslOpBase. +Local Transparent Val.add. + destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int.add_zero_l; auto. +- (* andimm *) + exploit (exec_logicalimm32 (Pandimm W) (Pand W)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. +- (* orimm *) + exploit (exec_logicalimm32 (Porrimm W) (Porr W)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. +- (* xorimm *) + exploit (exec_logicalimm32 (Peorimm W) (Peor W)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. +- (* not *) + TranslOpBase. + destruct (rs x0); auto. simpl. rewrite Int.or_zero_l; auto. +- (* notshift *) + TranslOpBase. + destruct (eval_shift s (rs x0) a); auto. simpl. rewrite Int.or_zero_l; auto. +- (* shrx *) + assert (Val.maketotal (Val.shrx (rs x0) (Vint n)) = Val.maketotal (Val.shrx (rs x0) (Vint n))) by eauto. + destruct (Val.shrx) eqn:E. + + exploit (exec_shrx32 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + econstructor; split. eexact A. split. rewrite B; auto. auto. + + exploit (exec_shrx32_none x x0 n); eauto with asmgen. +- (* zero-ext *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. +- (* sign-ext *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int.shl_zero. auto. +- (* shlzext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int.shl_zero_ext_min; auto using a32_range. +- (* shlsext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int.shl_sign_ext_min; auto using a32_range. +- (* zextshr *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.zero_ext_shru_min; auto using a32_range. +- (* sextshr *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a32_range; simpl. rewrite <- Int.sign_ext_shr_min; auto using a32_range. +- (* shiftl *) + rewrite <- transl_eval_shiftl'. TranslOpSimpl. +- (* extend *) + exploit (exec_move_extended x0 x1 x a k). intros (rs' & A & B & C). + econstructor; split. eexact A. + split. rewrite B; auto. eauto with asmgen. +- (* addlshift *) + TranslOpBase. +- (* addext *) + exploit (exec_arith_extended Val.addl Paddext (Padd X)). + auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). + econstructor; split. eexact A. split. rewrite B; auto. auto. +- (* addlimm *) + exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto. +- (* neglshift *) + TranslOpBase. +- (* sublshift *) + TranslOpBase. +- (* subext *) + exploit (exec_arith_extended Val.subl Psubext (Psub X)). + auto. auto. instantiate (1 := x1). eauto with asmgen. intros (rs' & A & B & C). + econstructor; split. eexact A. split. rewrite B; auto. auto. +- (* mull *) + TranslOpBase. + destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto. +- (* andlshift *) + TranslOpBase. +- (* andlimm *) + exploit (exec_logicalimm64 (Pandimm X) (Pand X)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. +- (* orlshift *) + TranslOpBase. +- (* orlimm *) + exploit (exec_logicalimm64 (Porrimm X) (Porr X)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. +- (* orlshift *) + TranslOpBase. +- (* xorlimm *) + exploit (exec_logicalimm64 (Peorimm X) (Peor X)). + intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + exists rs'; split. eexact A. split. rewrite B; auto. auto. +- (* notl *) + TranslOpBase. + destruct (rs x0); auto. simpl. rewrite Int64.or_zero_l; auto. +- (* notlshift *) + TranslOpBase. + destruct (eval_shiftl s (rs x0) a); auto. simpl. rewrite Int64.or_zero_l; auto. +- (* biclshift *) + TranslOpBase. +- (* ornlshift *) + TranslOpBase. +- (* eqvlshift *) + TranslOpBase. +- (* shrx *) + assert (Val.maketotal (Val.shrxl (rs x0) (Vint n)) = Val.maketotal (Val.shrxl (rs x0) (Vint n))) by eauto. + destruct (Val.shrxl) eqn:E. + + exploit (exec_shrx64 x x0 n); eauto with asmgen. intros (rs' & A & B & C). + econstructor; split. eexact A. split. rewrite B; auto. auto. + + exploit (exec_shrx64_none x x0 n); eauto with asmgen. +- (* zero-ext-l *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. +- (* sign-ext-l *) + TranslOpBase. + destruct (rs x0); auto; simpl. rewrite Int64.shl'_zero. auto. +- (* shllzext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_zero_ext_min; auto using a64_range. +- (* shllsext *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite <- Int64.shl'_sign_ext_min; auto using a64_range. +- (* zextshrl *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.zero_ext_shru'_min; auto using a64_range. +- (* sextshrl *) + TranslOpBase. + destruct (rs x0); simpl; auto. rewrite ! a64_range; simpl. rewrite <- Int64.sign_ext_shr'_min; auto using a64_range. +- (* condition *) + exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. + split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. + rewrite (B b) by auto. auto. + auto. + intros; Simpl. +- (* select *) + destruct (preg_of res) as [[ir|fr]|cr|] eqn:RES; monadInv TR. + + (* integer *) + generalize (ireg_of_eq _ _ EQ) (ireg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. + exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. + split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. + rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. + rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. + auto. + intros; Simpl. + + (* FP *) + generalize (freg_of_eq _ _ EQ) (freg_of_eq _ _ EQ1); intros E1 E2; rewrite E1, E2. + exploit (transl_cond_correct cond args); eauto. intros (rs' & A & B & C). + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. + split. Simpl. destruct (eval_condition cond (map rs (map preg_of args)) m) as [b|]; simpl in *. + rewrite (B b) by auto. rewrite !C. apply Val.lessdef_normalize. + rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. + auto. + intros; Simpl. +Qed. + +(** Translation of addressing modes, loads, stores *) + +Lemma transl_addressing_correct: + forall sz addr args (insn: Asm.addressing -> basic) k (rs: regset) m c b o, + transl_addressing sz addr args insn k = OK c -> + Op.eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some (Vptr b o) -> + exists ad rs', + exec_straight_opt ge lk c rs m (insn ad :: k) rs' m + /\ eval_addressing lk ad rs' = Vptr b o + /\ forall r, data_preg r = true -> rs' r = rs r. +Proof. + intros until o; intros TR EV. + unfold transl_addressing in TR; destruct addr; ArgsInv; SimplEval EV. +- (* Aindexed *) + destruct (offset_representable sz ofs); inv EQ0. ++ econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. ++ exploit (exec_loadimm64 X16 ofs). intros (rs' & A & B & C). + econstructor; exists rs'; split. apply exec_straight_opt_intro; eexact A. + split. simpl. rewrite B, C by eauto with asmgen. auto. + eauto with asmgen. +- (* Aindexed2 *) + econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. +- (* Aindexed2shift *) + destruct (Int.eq a Int.zero) eqn:E; [|destruct (Int.eq (Int.shl Int.one a) (Int.repr sz))]; inv EQ2. ++ apply Int.same_if_eq in E. rewrite E. + econstructor; econstructor; split. apply exec_straight_opt_refl. + split; auto. simpl. + rewrite Val.addl_commut in H0. destruct (rs x0); try discriminate. + unfold Val.shll. rewrite Int64.shl'_zero. auto. ++ econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. ++ econstructor; econstructor; split. + apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. + split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto. + intros; Simpl. +- (* Aindexed2ext *) + destruct (Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz)); inv EQ2. ++ econstructor; econstructor; split. apply exec_straight_opt_refl. + split; auto. destruct x; auto. ++ exploit (exec_arith_extended Val.addl Paddext (Padd X)); auto. + instantiate (1 := x0). eauto with asmgen. + intros (rs' & A & B & C). + econstructor; exists rs'; split. + apply exec_straight_opt_intro. eexact A. + split. simpl. rewrite B. rewrite Val.addl_assoc. f_equal. + unfold Op.eval_extend; destruct x, (rs x1); simpl; auto; rewrite ! a64_range; + simpl; rewrite Int64.add_zero; auto. + intros. apply C; eauto with asmgen. +- (* Aglobal *) + destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR. ++ econstructor; econstructor; split. + apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. + split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence. + intros; Simpl. ++ exploit (exec_loadsymbol X16 id ofs). auto. intros (rs' & A & B & C). + econstructor; exists rs'; split. + apply exec_straight_opt_intro. eexact A. + split. simpl. + rewrite B. rewrite <- Genv.shift_symbol_address_64, Ptrofs.add_zero by auto. + simpl in EV. congruence. + auto with asmgen. +- (* Ainstrack *) + assert (E: Val.addl (rs SP) (Vlong (Ptrofs.to_int64 ofs)) = Vptr b o). + { simpl in EV. inv EV. destruct (rs SP); simpl in H1; inv H1. simpl. + rewrite Ptrofs.of_int64_to_int64 by auto. auto. } + destruct (offset_representable sz (Ptrofs.to_int64 ofs)); inv TR. ++ econstructor; econstructor; split. apply exec_straight_opt_refl. + auto. ++ exploit (exec_loadimm64 X16 (Ptrofs.to_int64 ofs)). intros (rs' & A & B & C). + econstructor; exists rs'; split. + apply exec_straight_opt_intro. eexact A. + split. simpl. rewrite B, C by eauto with asmgen. auto. + auto with asmgen. +Qed. + +Lemma transl_load_correct: + forall chunk addr args dst k c (rs: regset) m vaddr v, + transl_load chunk addr args dst k = OK c -> + Op.eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some vaddr -> + Mem.loadv chunk m vaddr = Some v -> + exists rs', + exec_straight ge lk c rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, data_preg r = true -> r <> preg_of dst -> rs' r = rs r. +Proof. + intros. destruct vaddr; try discriminate. + assert (A: exists sz insn, + transl_addressing sz addr args insn k = OK c + /\ (forall ad rs', exec_basic lk ge (insn ad) rs' m = + exec_load_rd_a lk chunk (fun v => v) ad (dreg_of dst) rs' m)). + { + destruct chunk; monadInv H; + try rewrite (ireg_of_eq' _ _ EQ); try rewrite (freg_of_eq' _ _ EQ); + do 2 econstructor; (split; [eassumption|auto]). + } + destruct A as (sz & insn & B & C). + exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R). + assert (X: exec_load_rd_a lk chunk (fun v => v) ad (dreg_of dst) rs' m = + Next (rs'#(preg_of dst) <- v) m). + { unfold exec_load_rd_a. rewrite Q, H1. auto. } + econstructor; split. + eapply exec_straight_opt_right. eexact P. + apply exec_straight_one. rewrite C, X; eauto. Simpl. + split. auto. intros; Simpl. +Qed. + +Lemma transl_store_correct: + forall chunk addr args src k c (rs: regset) m vaddr m', + transl_store chunk addr args src k = OK c -> + Op.eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some vaddr -> + Mem.storev chunk m vaddr rs#(preg_of src) = Some m' -> + exists rs', + exec_straight ge lk c rs m k rs' m' + /\ forall r, data_preg r = true -> rs' r = rs r. +Proof. + intros. destruct vaddr; try discriminate. + set (chunk' := match chunk with Mint8signed => Mint8unsigned + | Mint16signed => Mint16unsigned + | _ => chunk end). + assert (A: exists sz insn, + transl_addressing sz addr args insn k = OK c + /\ (forall ad rs', exec_basic lk ge (insn ad) rs' m = + exec_store_rs_a lk chunk' ad rs'#(preg_of src) rs' m)). + { + unfold chunk'; destruct chunk; monadInv H; + try rewrite (ireg_of_eq _ _ EQ); try rewrite (freg_of_eq _ _ EQ); + do 2 econstructor; (split; [eassumption|auto]). + } + destruct A as (sz & insn & B & C). + exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R). + assert (X: Mem.storev chunk' m (Vptr b i) rs#(preg_of src) = Some m'). + { rewrite <- H1. unfold chunk'. destruct chunk; auto; simpl; symmetry. + apply Mem.store_signed_unsigned_8. + apply Mem.store_signed_unsigned_16. } + assert (Y: exec_store_rs_a lk chunk' ad rs'#(preg_of src) rs' m = + Next rs' m'). + { unfold exec_store_rs_a. rewrite Q, R, X by auto with asmgen. auto. } + econstructor; split. + eapply exec_straight_opt_right. eexact P. + apply exec_straight_one. rewrite C, Y; eauto. + intros; Simpl. rewrite R; auto. +Qed. + +(** Memory accesses *) + +Lemma indexed_memory_access_correct: forall insn sz (base: iregsp) ofs k (rs: regset) m b i, + preg_of_iregsp base <> X16 -> + Val.offset_ptr rs#base ofs = Vptr b i -> + exists ad rs', + exec_straight_opt ge lk (indexed_memory_access_bc insn sz base ofs k) rs m (insn ad :: k) rs' m + /\ eval_addressing lk ad rs' = Vptr b i + /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r. +Proof. + unfold indexed_memory_access_bc; intros. + assert (Val.addl rs#base (Vlong (Ptrofs.to_int64 ofs)) = Vptr b i). + { destruct (rs base); try discriminate. simpl in *. rewrite Ptrofs.of_int64_to_int64 by auto. auto. } + destruct offset_representable. +- econstructor; econstructor; split. apply exec_straight_opt_refl. auto. +- exploit (exec_loadimm64 X16); eauto. intros (rs' & A & B & C). + econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A. + split. simpl. rewrite B, C; eauto; try discriminate. + unfold preg_of_iregsp in H. destruct base; auto. auto. +Qed. + +Lemma loadptr_correct: forall (base: iregsp) ofs dst k m v (rs: regset), + Mem.loadv Mint64 m (Val.offset_ptr rs#base ofs) = Some v -> + preg_of_iregsp base <> IR X16 -> + exists rs', + exec_straight ge lk (loadptr_bc base ofs dst k) rs m k rs' m + /\ rs'#dst = v + /\ forall r, r <> PC -> r <> X16 -> r <> dst -> rs' r = rs r. +Proof. + intros. + destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. + exploit indexed_memory_access_correct; eauto. intros (ad & rs' & A & B & C). + econstructor; split. + eapply exec_straight_opt_right. eexact A. + apply exec_straight_one. simpl. unfold exec_load_rd_a. rewrite B, H. eauto. + split. Simpl. intros; Simpl. +Qed. + +Lemma loadind_correct: + forall (base: iregsp) ofs ty dst k c (rs: regset) m v, + loadind base ofs ty dst k = OK c -> + Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v -> + preg_of_iregsp base <> IR X16 -> + exists rs', + exec_straight ge lk c rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. +Proof. + intros. + destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. + assert (X: exists sz (insn: addressing -> ld_instruction), + c = indexed_memory_access_bc insn sz base ofs k + /\ (forall ad rs', exec_basic lk ge (insn ad) rs' m = + exec_load_rd_a lk (chunk_of_type ty) (fun v => v) ad (dreg_of dst) rs' m)). + { + unfold loadind in H; destruct ty; destruct (dst); inv H; + do 2 econstructor; split; eauto. + } + destruct X as (sz & insn & EQ & SEM). subst c. + exploit indexed_memory_access_correct; eauto. intros (ad & rs' & A & B & C). + econstructor; split. + eapply exec_straight_opt_right. eexact A. + apply exec_straight_one. rewrite SEM. unfold exec_load. + unfold exec_load_rd_a. rewrite B, H0. eauto. Simpl. + split. auto. intros; Simpl. +Qed. + +Lemma storeind_correct: forall (base: iregsp) ofs ty src k c (rs: regset) m m', + storeind src base ofs ty k = OK c -> + Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) rs#(preg_of src) = Some m' -> + preg_of_iregsp base <> IR X16 -> + exists rs', + exec_straight ge lk c rs m k rs' m' + /\ forall r, data_preg r = true -> rs' r = rs r. +Proof. + intros. + destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. + assert (X: exists sz (insn: addressing -> st_instruction), + c = indexed_memory_access_bc insn sz base ofs k + /\ (forall ad rs', exec_basic lk ge (insn ad) rs' m = + exec_store_rs_a lk (chunk_of_type ty) ad rs'#(preg_of src) rs' m)). + { + unfold storeind in H; destruct ty; destruct (preg_of src) as [[ir|fr]|cr|]; inv H; do 2 econstructor; split; eauto. + } + destruct X as (sz & insn & EQ & SEM). subst c. + exploit indexed_memory_access_correct; eauto. intros (ad & rs' & A & B & C). + econstructor; split. + eapply exec_straight_opt_right. eexact A. + apply exec_straight_one. rewrite SEM. + unfold exec_store. unfold exec_store_rs_a. + rewrite B, C, H0 by eauto with asmgen. eauto. + intros; Simpl. unfold data_preg in H2. destruct r as [[[ir|]|fr]|cr|]. + all: rewrite C; auto; try discriminate; + destruct ir; try discriminate. +Qed. + +Lemma make_epilogue_correct: + forall ge0 f m stk soff cs m' ms rs tm, + Mach.load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) -> + Mach.load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra cs) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + agree ms (Vptr stk soff) rs -> + Mem.extends m tm -> + match_stack ge0 cs -> + exists rs', exists tm', + exec_straight ge lk (make_epilogue f) rs tm nil rs' tm' + /\ agree ms (parent_sp cs) rs' + /\ Mem.extends m' tm' + /\ rs'#RA = parent_ra cs + /\ rs'#SP = parent_sp cs + /\ (forall r, r <> PC -> r <> SP -> r <> X30 -> r <> X16 -> rs'#r = rs#r). +Proof. + assert (Archi.ptr64 = true) as SF; auto. + intros until tm; intros LP LRA FREE AG MEXT MCS. + exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP'). + exploit Mem.loadv_extends. eauto. eexact LRA. auto. simpl. intros (ra' & LRA' & LDRA'). + exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'. + exploit lessdef_parent_ra; eauto. intros EQ; subst ra'; clear LDRA'. + exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT'). + unfold make_epilogue. + rewrite chunk_of_Tptr in *. unfold Mptr in *. rewrite SF in *. + + exploit (loadptr_correct XSP (fn_retaddr_ofs f)). + instantiate (2 := rs). simpl. + replace (rs XSP) with (rs SP) by auto. + rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. simpl; discriminate. + + intros (rs1 & A1 & B1 & C1). + econstructor; econstructor; split. + eapply exec_straight_trans. eexact A1. apply exec_straight_one. simpl. + simpl; rewrite (C1 SP) by auto with asmgen. rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. + rewrite FREE'. eauto. + split. apply agree_set_other; auto. + apply agree_change_sp with (Vptr stk soff). + apply agree_exten with rs; auto. intros; apply C1; auto with asmgen. + eapply parent_sp_def; eauto. + split. auto. + split. Simpl. + split. Simpl. + intros. Simpl. +Qed. + +End CONSTRUCTORS. \ No newline at end of file diff --git a/aarch64/Asmblockprops.v b/aarch64/Asmblockprops.v index d1015ea9..cef95aad 100644 --- a/aarch64/Asmblockprops.v +++ b/aarch64/Asmblockprops.v @@ -39,7 +39,13 @@ Lemma preg_of_data: Proof. intros. destruct r; reflexivity. Qed. -Hint Resolve preg_of_data: asmgen. + +Lemma dreg_of_data: + forall r, data_preg (dreg_of r) = true. +Proof. + intros. destruct r; reflexivity. +Qed. +Hint Resolve preg_of_data dreg_of_data: asmgen. Lemma data_diff: forall r r', @@ -55,6 +61,12 @@ Proof. intros. apply data_diff; auto with asmgen. Qed. +Lemma preg_of_not_SP: + forall r, preg_of r <> SP. +Proof. + intros. unfold preg_of; destruct r; simpl; try discriminate. +Qed. + (* Lemma preg_of_not_SP: forall r, preg_of r <> SP. @@ -81,73 +93,61 @@ Lemma nextblock_inv1: forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r. Proof. intros. apply nextblock_inv. red; intro; subst; discriminate. -Qed. +Qed.*) + +Ltac desif := + repeat match goal with + | [ |- context[ if ?f then _ else _ ] ] => destruct f + end. + +Ltac decomp := + repeat match goal with + | [ |- context[ match (?rs ?r) with | _ => _ end ] ] => destruct (rs r) + end. Ltac Simplif := - ((rewrite nextblock_inv by eauto with asmgen) - || (rewrite nextblock_inv1 by eauto with asmgen) + ((desif) + || (try unfold compare_long) + || (try unfold compare_int) + || (try unfold compare_float) + || (try unfold compare_single) + || decomp || (rewrite Pregmap.gss) - || (rewrite nextblock_pc) || (rewrite Pregmap.gso by eauto with asmgen) ); auto with asmgen. Ltac Simpl := repeat Simplif. +Section EPC. + +Variable lk: aarch64_linker. + (* For Asmblockgenproof0 *) Theorem exec_basic_instr_pc: forall ge b rs1 m1 rs2 m2, - exec_basic_instr ge b rs1 m1 = Next rs2 m2 -> + exec_basic lk ge b rs1 m1 = Next rs2 m2 -> rs2 PC = rs1 PC. Proof. - intros. destruct b; try destruct i; try destruct i. - all: try (inv H; Simpl). - 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. - - 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. - - { (* PLoadQRRO *) - unfold parexec_load_q_offset in H1. - destruct (gpreg_q_expand _) as [r0 r1] in H1. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. } - { (* PLoadORRO *) - unfold parexec_load_o_offset in H1. - destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. } - 1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail. - 1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. - 1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. - - { (* PStoreQRRO *) - unfold parexec_store_q_offset in H1. - destruct (gpreg_q_expand _) as [r0 r1] in H1. - unfold eval_offset in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - inv H1. Simpl. reflexivity. } - { (* PStoreORRO *) - unfold parexec_store_o_offset in H1. - destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. - unfold eval_offset in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - inv H1. Simpl. reflexivity. } - - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. - destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. - - destruct rs; try discriminate. inv H1. Simpl. - - destruct rd; try discriminate. inv H1; Simpl. - - reflexivity. + intros. destruct b; try destruct i; try destruct i; try destruct ld; try destruct ld; + try destruct st; try destruct st; try destruct a. + all: try (inv H; simpl in *; auto; Simpl). + all: try (try unfold exec_load_rd_a in H1; try destruct (Mem.loadv _ _ _); inv H1; Simpl). + all: try (try unfold exec_load_double in H0; destruct (Mem.loadv _ _ _); simpl in *; + try destruct (Mem.loadv _ _ _); simpl in *; inv H0; Simpl). + all: try (try unfold exec_store_rs_a in H0; try destruct (Mem.storev _ _ _); inv H0; auto; Simpl). + all: try (try unfold exec_store_double in H1; destruct (Mem.storev _ _ _); simpl in *; + try destruct (Mem.storev _ _ _); simpl in *; inv H1; auto; Simpl). + - (* alloc *) + destruct (Mem.alloc _ _ _); destruct (Mem.store _ _ _); inv H1; auto; Simpl. + - (* free *) + destruct (rs1 SP); try discriminate; destruct (Mem.free _ _ _ _); inv H1; Simpl. Qed. +End EPC. + +(* + (* For PostpassSchedulingproof *) Lemma regset_double_set: -- cgit