diff options
| -rw-r--r-- | aarch64/Asmblock.v | 3 | ||||
| -rw-r--r-- | aarch64/Asmblockdeps.v | 2 | ||||
| -rw-r--r-- | aarch64/Asmblockgenproof0.v | 988 | ||||
| -rw-r--r-- | aarch64/Asmblockgenproof1.v | 2141 | ||||
| -rw-r--r-- | aarch64/PostpassScheduling.v | 423 | ||||
| -rw-r--r-- | aarch64/PostpassSchedulingOracle.ml | 6 | ||||
| -rw-r--r-- | aarch64/PostpassSchedulingproof.v | 429 | ||||
| -rwxr-xr-x | configure | 2 |
8 files changed, 109 insertions, 3885 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index da45324b..7f94a087 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -336,12 +336,13 @@ Inductive basic : Type := *) . +(* Not used in Coq, declared in ocaml directly in PostpassSchedulingOracle.ml Inductive instruction : Type := | PBasic (i: basic) | PControl (i: control). Coercion PBasic: basic >-> instruction. -Coercion PControl: control >-> instruction. +Coercion PControl: control >-> instruction. *) (** * Definition of a bblock diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 9b8b8d49..4a40ed43 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -23,7 +23,7 @@ Require Import AST. Require Import Asm Asmblock. -Require Import Asmblockgenproof0 Asmblockprops. +Require Import Asmblockprops. Require Import Values. Require Import Globalenvs. Require Import Memory. diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v deleted file mode 100644 index 172e770d..00000000 --- a/aarch64/Asmblockgenproof0.v +++ /dev/null @@ -1,988 +0,0 @@ -(* *************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* Xavier Leroy INRIA Paris-Rocquencourt *) -(* David Monniaux CNRS, VERIMAG *) -(* Cyril Six Kalray *) -(* *) -(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) -(* This file is distributed under the terms of the INRIA *) -(* Non-Commercial License Agreement. *) -(* *) -(* *************************************************************) - -(** * "block" version of Asmgenproof0 - - This module is largely adapted from Asmgenproof0.v of the other backends - It needs to stand apart because of the block structure, and the distinction control/basic that there isn't in the other backends - It has similar definitions than Asmgenproof0, but adapted to this new structure *) - -Require Import Coqlib. -Require Intv. -Require Import AST. -Require Import Errors. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Locations. -Require Import Machblock. -Require Import Asmblock. -Require Import Asmblockgen. -Require Import Conventions1. -Require Import Axioms. -Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *) -Require Import Asmblockprops. - -Module MB:=Machblock. -Module AB:=Asmblock. - -(* -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); inv H; auto. -Qed. - -Lemma freg_of_eq: - forall r r', freg_of r = OK r' -> preg_of r = IR r'. -Proof. - unfold freg_of; intros. destruct (preg_of r); inv H; 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 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. - -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. - -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. - -(** * Agreement between Mach registers and processor registers *) - -Record agree (ms: Mach.regset) (sp: val) (rs: AB.regset) : Prop := mkagree { - agree_sp: rs#SP = sp; - agree_sp_def: sp <> Vundef; - agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r)) -}. - -Lemma preg_val: - forall ms sp rs r, agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r). -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 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 freg_val: - forall ms sp rs r r', - agree ms sp rs -> - freg_of r = OK r' -> - Val.lessdef (ms r) (rs#r'). -Proof. - intros. rewrite <- (freg_of_eq _ _ H0). eapply preg_val; eauto. -Qed. - -Lemma agree_exten: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, data_preg r = true -> rs'#r = rs#r) -> - agree ms sp rs'. -Proof. - intros. destruct H. split; auto. - rewrite H0; auto. auto. - intros. rewrite H0; auto. apply preg_of_data. -Qed. - -(** 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. - -Corollary agree_set_mreg_parallel: - forall ms sp rs r v v', - agree ms sp rs -> - Val.lessdef v v' -> - agree (Mach.Regmap.set r v ms) sp (Pregmap.set (preg_of r) v' rs). -Proof. - intros. eapply agree_set_mreg; eauto. rewrite Pregmap.gss; auto. intros; apply Pregmap.gso; auto. -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 (nextblock b rs). -Proof. - intros. unfold nextblock. apply agree_set_other. auto. auto. -Qed. - -Lemma agree_set_pair: - forall sp p v v' ms rs, - agree ms sp rs -> - Val.lessdef v v' -> - agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs). -Proof. - intros. destruct p; simpl. -- apply agree_set_mreg_parallel; auto. -- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto. - apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto. -Qed. - -Lemma agree_undef_nondata_regs: - forall ms sp rl rs, - agree ms sp rs -> - (forall r, In r rl -> data_preg r = false) -> - agree ms sp (undef_regs rl rs). -Proof. - induction rl; simpl; intros. auto. - apply IHrl. apply agree_exten with rs; auto. - intros. apply Pregmap.gso. red; intros; subst. - assert (data_preg a = false) by auto. congruence. - intros. apply H0; 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_undef_caller_save_regs: - forall ms sp rs, - agree ms sp rs -> - agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs). -Proof. - intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split. -- unfold proj_sumbool; rewrite dec_eq_true. auto. -- auto. -- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). - destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. -+ apply list_in_map_inv in i. destruct i as (mr & A & B). - assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. - apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. -+ destruct (is_callee_save r) eqn:CS; auto. - elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. -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. - -(** Connection between Mach and Asm calling conventions for external - functions. *) - -Lemma extcall_arg_match: - forall ms sp rs m m' l v, - agree ms sp rs -> - Mem.extends m m' -> - Mach.extcall_arg ms m sp l v -> - exists v', AB.extcall_arg rs m' l v' /\ Val.lessdef v v'. -Proof. - intros. inv H1. - exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto. - unfold Mach.load_stack in H2. - exploit Mem.loadv_extends; eauto. intros [v' [A B]]. - rewrite (sp_val _ _ _ H) in A. - exists v'; split; auto. - econstructor. eauto. assumption. -Qed. - -Lemma extcall_arg_pair_match: - forall ms sp rs m m' p v, - agree ms sp rs -> - Mem.extends m m' -> - Mach.extcall_arg_pair ms m sp p v -> - exists v', AB.extcall_arg_pair rs m' p v' /\ Val.lessdef v v'. -Proof. - intros. inv H1. -- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto. -- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1). - exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2). - exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. -Qed. - - -Lemma extcall_args_match: - forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> - forall ll vl, - list_forall2 (Mach.extcall_arg_pair ms m sp) ll vl -> - exists vl', list_forall2 (AB.extcall_arg_pair rs m') ll vl' /\ Val.lessdef_list vl vl'. -Proof. - induction 3; intros. - exists (@nil val); split. constructor. constructor. - exploit extcall_arg_pair_match; eauto. intros [v1' [A B]]. - destruct IHlist_forall2 as [vl' [C D]]. - exists (v1' :: vl'); split; constructor; auto. -Qed. - -Lemma extcall_arguments_match: - forall ms m m' sp rs sg args, - agree ms sp rs -> Mem.extends m m' -> - Mach.extcall_arguments ms m sp sg args -> - exists args', AB.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'. -Proof. - unfold Mach.extcall_arguments, AB.extcall_arguments; intros. - eapply extcall_args_match; eauto. -Qed. - -Remark builtin_arg_match: - forall ge (rs: regset) sp m a v, - eval_builtin_arg ge (fun r => rs (preg_of r)) sp m a v -> - eval_builtin_arg ge rs sp m (map_builtin_arg preg_of a) v. -Proof. - induction 1; simpl; eauto with barg. -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 rs sp m' (map (map_builtin_arg preg_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 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 (AB.set_res (map_builtin_res preg_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 set_res_other: - forall r res v rs, - data_preg r = false -> - set_res (map_builtin_res preg_of res) v rs r = rs r. -Proof. - induction res; simpl; intros. -- apply Pregmap.gso. red; intros; subst r. rewrite preg_of_data in H; discriminate. -- auto. -- rewrite IHres2, IHres1; auto. -Qed. - -(* 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. -*) -(* inspired from Asmgenproof0 *) - -(* ... skip ... *) - -(** The ``code tail'' of an instruction list [c] is the list of instructions - starting at PC [pos]. *) - -Inductive code_tail: Z -> bblocks -> bblocks -> Prop := - | code_tail_0: forall c, - code_tail 0 c c - | code_tail_S: forall pos bi c1 c2, - code_tail pos c1 c2 -> - code_tail (pos + (size bi)) (bi :: c1) c2. - -(* -Lemma code_tail_pos: - forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0. -Proof. - induction 1. omega. - Admitted. -(* TODO How to import this module? generalize (bblock_size_pos bi); intros; omega. -Qed. *) - -Lemma find_bblock_tail: - forall c1 bi c2 pos, - code_tail pos c1 (bi :: c2) -> - find_bblock pos c1 = Some bi. -Proof. - induction c1; simpl; intros. - inversion H. - destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega. - destruct (zeq pos 0). subst pos. - inv H. auto. - Admitted. -(* TODO same as above generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega. - inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega. - eauto. -Qed. - *) - -Local Hint Resolve code_tail_0 code_tail_S: core. - -Lemma code_tail_next: - forall fn ofs c0, - code_tail ofs fn c0 -> - forall bi c1, c0 = bi :: c1 -> code_tail (ofs + (size bi)) fn c1. -Proof. - induction 1; intros. - - subst; eauto. - - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto. - omega. -Qed. - -Lemma size_blocks_pos c: 0 <= size_blocks c. -Proof. - induction c as [| a l ]; simpl; try omega. - generalize (size_positive a); omega. -Qed. - -Remark code_tail_positive: - forall fn ofs c, - code_tail ofs fn c -> 0 <= ofs. -Proof. - induction 1; intros; simpl. - - omega. - - generalize (size_positive bi). omega. -Qed. - -Remark code_tail_size: - forall fn ofs c, - code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c. -Proof. - induction 1; intros; simpl; try omega. -Qed. - -Remark code_tail_bounds fn ofs c: - code_tail ofs fn c -> 0 <= ofs <= size_blocks fn. -Proof. - intro H; - exploit code_tail_size; eauto. - generalize (code_tail_positive _ _ _ H), (size_blocks_pos c). - omega. -Qed. - -Local Hint Resolve code_tail_next: core. - -Lemma code_tail_next_int: - forall fn ofs bi c, - size_blocks fn <= Ptrofs.max_unsigned -> - code_tail (Ptrofs.unsigned ofs) fn (bi :: c) -> - code_tail (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bi)))) fn c. -Proof. - intros. - exploit code_tail_size; eauto. - simpl; generalize (code_tail_positive _ _ _ H0), (size_positive bi), (size_blocks_pos c). - intros. - rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr. - - rewrite Ptrofs.unsigned_repr; eauto. - omega. - - rewrite Ptrofs.unsigned_repr; omega. -Qed. - -(** Predictor for return addresses in generated Asm code. - - The [return_address_offset] predicate defined here is used in the - semantics for Mach to determine the return addresses that are - stored in activation records. *) - -(** Consider a Mach function [f] and a sequence [c] of Mach instructions - representing the Mach code that remains to be executed after a - function call returns. The predicate [return_address_offset f c ofs] - holds if [ofs] is the integer offset of the PPC instruction - following the call in the Asm code obtained by translating the - code of [f]. Graphically: -<< - Mach function f |--------- Mcall ---------| - Mach code c | |--------| - | \ \ - | \ \ - | \ \ - Asm code | |--------| - Asm function |------------- Pcall ---------| - - <-------- ofs -------> ->> -*) - -Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : Prop := - forall tf tc, - transf_function f = OK tf -> - transl_blocks f c false = OK tc -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc. - -Lemma transl_blocks_tail: - forall f c1 c2, is_tail c1 c2 -> - forall tc2 ep2, transl_blocks f c2 ep2 = OK tc2 -> - exists tc1, exists ep1, transl_blocks f c1 ep1 = OK tc1 /\ is_tail tc1 tc2. -Proof. - induction 1; simpl; intros. - exists tc2; exists ep2; split; auto with coqlib. - monadInv H0. exploit IHis_tail; eauto. intros (tc1 & ep1 & A & B). - exists tc1; exists ep1; split. auto. - eapply is_tail_trans with x0; eauto with coqlib. -Qed. - -Lemma is_tail_code_tail: - forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1. -Proof. - induction 1; eauto. - destruct IHis_tail; eauto. -Qed. - -Section RETADDR_EXISTS. - -Hypothesis transf_function_inv: - forall f tf, transf_function f = OK tf -> - exists tc ep, transl_blocks f (Machblock.fn_code f) ep = OK tc /\ is_tail tc (fn_blocks tf). - -Hypothesis transf_function_len: - forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned. - - -Lemma return_address_exists: - forall b f c, is_tail (b :: c) f.(MB.fn_code) -> - exists ra, return_address_offset f c ra. -Proof. - intros. destruct (transf_function f) as [tf|] eqn:TF. - + exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1). - exploit transl_blocks_tail; eauto. intros (tc2 & ep2 & TR2 & TL2). - monadInv TR2. - assert (TL3: is_tail x0 (fn_blocks tf)). - { apply is_tail_trans with tc1; auto. - apply is_tail_trans with (x++x0); auto. eapply is_tail_app. - } - exploit is_tail_code_tail. eexact TL3. intros [ofs CT]. - exists (Ptrofs.repr ofs). red; intros. - rewrite Ptrofs.unsigned_repr. congruence. - exploit code_tail_bounds; eauto. - intros; apply transf_function_len in TF. omega. - + exists Ptrofs.zero; red; intros. congruence. -Qed. - -End RETADDR_EXISTS. - -(** [transl_code_at_pc pc fb f c ep tf tc] holds if the code pointer [pc] points - within the Asmblock code generated by translating Machblock function [f], - and [tc] is the tail of the generated code at the position corresponding - to the code pointer [pc]. *) - -Inductive transl_code_at_pc (ge: MB.genv): - val -> block -> MB.function -> MB.code -> bool -> AB.function -> AB.bblocks -> Prop := - transl_code_at_pc_intro: - forall b ofs f c ep tf tc, - Genv.find_funct_ptr ge b = Some(Internal f) -> - transf_function f = Errors.OK tf -> - transl_blocks f c ep = OK tc -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc -> - transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc. - -Remark code_tail_no_bigger: - forall pos c1 c2, code_tail pos c1 c2 -> (length c2 <= length c1)%nat. -Proof. - induction 1; simpl; omega. -Qed. - -Remark code_tail_unique: - forall fn c pos pos', - code_tail pos fn c -> code_tail pos' fn c -> pos = pos'. -Proof. - induction fn; intros until pos'; intros ITA CT; inv ITA; inv CT; auto. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - generalize (code_tail_no_bigger _ _ _ H3); simpl; intro; omega. - f_equal. eauto. -Qed. - -Lemma return_address_offset_correct: - forall ge b ofs fb f c tf tc ofs', - transl_code_at_pc ge (Vptr b ofs) fb f c false tf tc -> - return_address_offset f c ofs' -> - ofs' = ofs. -Proof. - intros. inv H. red in H0. - exploit code_tail_unique. eexact H12. eapply H0; eauto. intro. - rewrite <- (Ptrofs.repr_unsigned ofs). - rewrite <- (Ptrofs.repr_unsigned ofs'). - congruence. -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. - -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. - -(** Helper lemmas to reason about -- the "code is tail of" property -- correct translation of labels. *) - -Definition tail_nolabel (k c: bblocks) : Prop := - is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k. - -Lemma tail_nolabel_refl: - forall c, tail_nolabel c c. -Proof. - intros; split. apply is_tail_refl. auto. -Qed. - -Lemma tail_nolabel_trans: - forall c1 c2 c3, tail_nolabel c2 c3 -> tail_nolabel c1 c2 -> tail_nolabel c1 c3. -Proof. - intros. destruct H; destruct H0; split. - eapply is_tail_trans; eauto. - intros. rewrite H1; auto. -Qed. - -Definition nolabel (b: bblock) := - match (header b) with nil => True | _ => False end. - -Hint Extern 1 (nolabel _) => exact I : labels. - -Lemma tail_nolabel_cons: - forall b c k, - nolabel b -> tail_nolabel k c -> tail_nolabel k (b :: c). -Proof. - intros. destruct H0. split. - constructor; auto. - intros. simpl. rewrite <- H1. destruct b as [hd bdy ex]; simpl in *. - destruct hd as [|l hd]; simpl in *. - - assert (is_label lbl {| AB.header := nil; AB.body := bdy; AB.exit := ex; AB.correct := correct |} = false). - { apply is_label_correct_false. simpl header. apply in_nil. } - rewrite H2. auto. - - contradiction. -Qed. - -Hint Resolve tail_nolabel_refl: labels. - -Ltac TailNoLabel := - eauto with labels; - match goal with - | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [auto; exact I | TailNoLabel] - | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: assertion_failed = OK _ |- _ ] => discriminate - | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabel - | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabel - | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabel - | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabel - | _ => idtac - end. - -Remark tail_nolabel_find_label: - forall lbl k c, tail_nolabel k c -> find_label lbl c = find_label lbl k. -Proof. - intros. destruct H. auto. -Qed. - -Remark tail_nolabel_is_tail: - forall k c, tail_nolabel k c -> is_tail k c. -Proof. - intros. destruct H. auto. -Qed. - -Lemma exec_body_pc: - forall ge l rs1 m1 rs2 m2, - exec_body 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_instr _ _ _ _) eqn:EBI; try discriminate. - eapply IHl in H0. rewrite H0. - erewrite exec_basic_instr_pc; eauto. -Qed. - -Section STRAIGHTLINE. - -Variable ge: genv. -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 instruction -> regset -> mem -> - list instruction -> regset -> mem -> Prop := - | exec_straight_one: - forall i1 c rs1 m1 rs2 m2, - exec_basic_instr ge i1 rs1 m1 = Next rs2 m2 -> - exec_straight ((PBasic i1) ::g c) rs1 m1 c rs2 m2 - | exec_straight_step: - forall i c rs1 m1 rs2 m2 c' rs3 m3, - exec_basic_instr ge i rs1 m1 = Next rs2 m2 -> - exec_straight c rs2 m2 c' rs3 m3 -> - exec_straight ((PBasic i) :: c) rs1 m1 c' rs3 m3. - -Inductive exec_control_rel: option control -> bblock -> regset -> mem -> - regset -> mem -> Prop := - | exec_control_rel_intro: - forall rs1 m1 b rs1' ctl rs2 m2, - rs1' = nextblock b rs1 -> - exec_control ge fn ctl rs1' m1 = Next rs2 m2 -> - exec_control_rel ctl b rs1 m1 rs2 m2. - -Inductive exec_bblock_rel: bblock -> regset -> mem -> regset -> mem -> Prop := - | exec_bblock_rel_intro: - forall rs1 m1 b rs2 m2, - exec_bblock ge fn b rs1 m1 = Next rs2 m2 -> - exec_bblock_rel b rs1 m1 rs2 m2. - -Lemma exec_straight_body: - forall c l rs1 m1 rs2 m2, - exec_straight c rs1 m1 nil rs2 m2 -> - code_to_basics c = Some l -> - exec_body ge l rs1 m1 = Next rs2 m2. -Proof. - induction c as [|i c]. - - intros until m2. intros EXES CTB. inv EXES. - - intros until m2. intros EXES CTB. inv EXES. - + inv CTB. simpl. rewrite H6. auto. - + inv CTB. destruct (code_to_basics c); try discriminate. inv H0. eapply IHc in H7; eauto. - rewrite <- H7. simpl. rewrite H1. auto. -Qed. - -Lemma exec_straight_body2: - forall c rs1 m1 c' rs2 m2, - exec_straight c rs1 m1 c' rs2 m2 -> - exists body, - exec_body ge body rs1 m1 = Next rs2 m2 - /\ (basics_to_code body) ++g 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_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_instr ge i1 rs1 m1 = Next rs2 m2 -> - exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 -> - exec_straight (i1 ::g i2 ::g 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_instr ge i1 rs1 m1 = Next rs2 m2 -> - exec_basic_instr ge i2 rs2 m2 = Next rs3 m3 -> - exec_basic_instr ge i3 rs3 m3 = Next rs4 m4 -> - exec_straight (i1 ::g i2 ::g i3 ::g c) rs1 m1 c rs4 m4. -Proof. - intros. apply exec_straight_step with rs2 m2; auto. - eapply exec_straight_two; eauto. -Qed. - -(** Like exec_straight predicate, but on blocks *) - -Inductive exec_straight_blocks: bblocks -> regset -> mem -> - bblocks -> regset -> mem -> Prop := - | exec_straight_blocks_one: - forall b1 c rs1 m1 rs2 m2, - exec_bblock ge fn b1 rs1 m1 = Next rs2 m2 -> - rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b1)) -> - exec_straight_blocks (b1 :: c) rs1 m1 c rs2 m2 - | exec_straight_blocks_step: - forall b c rs1 m1 rs2 m2 c' rs3 m3, - exec_bblock ge fn b rs1 m1 = Next rs2 m2 -> - rs2#PC = Val.offset_ptr rs1#PC (Ptrofs.repr (size b)) -> - exec_straight_blocks c rs2 m2 c' rs3 m3 -> - exec_straight_blocks (b :: c) rs1 m1 c' rs3 m3. - -Lemma exec_straight_blocks_trans: - forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, - exec_straight_blocks c1 rs1 m1 c2 rs2 m2 -> - exec_straight_blocks c2 rs2 m2 c3 rs3 m3 -> - exec_straight_blocks c1 rs1 m1 c3 rs3 m3. -Proof. - induction 1; intros. - apply exec_straight_blocks_step with rs2 m2; auto. - apply exec_straight_blocks_step with rs2 m2; auto. -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 regset_same_assign (rs: regset) r: - rs # r <- (rs r) = rs. -Proof. - apply functional_extensionality. intros x. destruct (preg_eq x r); subst; Simpl. -Qed. - -Lemma exec_straight_through_singleinst: - forall a b rs1 m1 rs2 m2 rs2' m2' lb, - bblock_single_inst (PBasic a) = b -> - exec_straight (a ::g nil) rs1 m1 nil rs2 m2 -> - nextblock b rs2 = rs2' -> m2 = m2' -> - exec_straight_blocks (b::lb) rs1 m1 lb rs2' m2'. -Proof. - intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. - simpl. rewrite regset_same_assign. auto. - simpl; auto. unfold nextblock, incrPC; simpl. Simpl. erewrite exec_straight_pc; eauto. -Qed. - -(** The following lemmas show that straight-line executions - (predicate [exec_straight_blocks]) correspond to correct Asm executions. *) - -Lemma exec_straight_steps_1: - forall c rs m c' rs' m', - exec_straight_blocks c rs m c' rs' m' -> - size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned -> - forall b ofs, - rs#PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal fn) -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c -> - plus step ge (State rs m) E0 (State rs' m'). -Proof. - induction 1; intros. - apply plus_one. - econstructor; eauto. - eapply find_bblock_tail. eauto. - eapply plus_left'. - econstructor; eauto. - eapply find_bblock_tail. eauto. - apply IHexec_straight_blocks with b0 (Ptrofs.add ofs (Ptrofs.repr (size b))). - auto. rewrite H0. rewrite H3. reflexivity. - auto. - apply code_tail_next_int; auto. - traceEq. -Qed. - -Lemma exec_straight_steps_2: - forall c rs m c' rs' m', - exec_straight_blocks c rs m c' rs' m' -> - size_blocks (fn_blocks fn) <= Ptrofs.max_unsigned -> - forall b ofs, - rs#PC = Vptr b ofs -> - Genv.find_funct_ptr ge b = Some (Internal fn) -> - code_tail (Ptrofs.unsigned ofs) (fn_blocks fn) c -> - exists ofs', - rs'#PC = Vptr b ofs' - /\ code_tail (Ptrofs.unsigned ofs') (fn_blocks fn) c'. -Proof. - induction 1; intros. - exists (Ptrofs.add ofs (Ptrofs.repr (size b1))). split. - rewrite H0. rewrite H2. auto. - apply code_tail_next_int; auto. - apply IHexec_straight_blocks with (Ptrofs.add ofs (Ptrofs.repr (size b))). - auto. rewrite H0. rewrite H3. reflexivity. auto. - apply code_tail_next_int; auto. -Qed. - -End STRAIGHTLINE. - -(** * Properties of the Machblock call stack *) - -Section MATCH_STACK. - -Variable ge: MB.genv. - -Inductive match_stack: list MB.stackframe -> Prop := - | match_stack_nil: - match_stack nil - | match_stack_cons: forall fb sp ra c s f tf tc, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - transl_code_at_pc ge ra fb f c false tf tc -> - sp <> Vundef -> - match_stack s -> - match_stack (Stackframe fb sp ra c :: s). - -Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. -Proof. - induction 1; simpl. - unfold Vnullptr; destruct Archi.ptr64; congruence. - auto. -Qed. - -Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. -Proof. - induction 1; simpl. - unfold Vnullptr; destruct Archi.ptr64; congruence. - inv H0. congruence. -Qed. - -Lemma lessdef_parent_sp: - forall s v, - match_stack s -> Val.lessdef (parent_sp s) v -> v = parent_sp s. -Proof. - intros. inv H0. auto. exploit parent_sp_def; eauto. tauto. -Qed. - -Lemma lessdef_parent_ra: - forall s v, - match_stack s -> Val.lessdef (parent_ra s) v -> v = parent_ra s. -Proof. - intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. -Qed. - -End MATCH_STACK.*) diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v deleted file mode 100644 index b42309bc..00000000 --- a/aarch64/Asmblockgenproof1.v +++ /dev/null @@ -1,2141 +0,0 @@ -(* ORIGINAL aarch64/Asmgenproof1 file that needs to be adapted - -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, Collège de France and INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Correctness proof for AArch64 code generation: auxiliary results. *) - -Require Import Recdef Coqlib Zwf Zbits. -Require Import Maps Errors AST Integers Floats Values Memory Globalenvs. -Require Import Op Locations Mach Asm Conventions. -Require Import Asmgen. -Require Import Asmgenproof0. - -Local Transparent Archi.ptr64. - -(** Properties of registers *) - -Lemma preg_of_not_RA: - forall r, (preg_of r) <> RA. -Proof. - destruct r; discriminate. -Qed. - -Lemma RA_not_written: - forall (rs : regset) dst v, - rs # (preg_of dst) <- v RA = rs RA. -Proof. - intros. - apply Pregmap.gso. - intro. - symmetry in H. - exact (preg_of_not_RA dst H). -Qed. - -Hint Resolve RA_not_written : asmgen. - -Lemma RA_not_written2: - forall (rs : regset) dst v i, - preg_of dst = i -> - rs # i <- v RA = rs RA. -Proof. - intros. - subst i. - apply RA_not_written. -Qed. - -Hint Resolve RA_not_written2 : asmgen. - -Lemma RA_not_written3: - forall (rs : regset) dst v i, - ireg_of dst = OK i -> - rs # i <- v RA = rs RA. -Proof. - intros. - unfold ireg_of in H. - destruct preg_of eqn:PREG; try discriminate. - replace i0 with i in * by congruence. - eapply RA_not_written2; eassumption. -Qed. - -Hint Resolve RA_not_written3 : asmgen. - -Lemma preg_of_iregsp_not_PC: forall r, preg_of_iregsp r <> PC. -Proof. - destruct r; simpl; congruence. -Qed. -Hint Resolve preg_of_iregsp_not_PC: asmgen. - -Lemma preg_of_not_X16: forall r, preg_of r <> X16. -Proof. - destruct r; simpl; congruence. -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. -Qed. - -Lemma ireg_of_not_RA: forall r x, ireg_of r = OK x -> x <> RA. -Proof. - unfold ireg_of; intros. destruct (preg_of r) eqn:E; inv H. - red; intros; subst x. elim (preg_of_not_RA r); auto. -Qed. - -Lemma ireg_of_not_RA': forall r x, ireg_of r = OK x -> RA <> x. -Proof. - intros. intro. - apply (ireg_of_not_RA r x); auto. -Qed. - -Lemma ireg_of_not_RA'': forall r x, ireg_of r = OK x -> IR RA <> IR x. -Proof. - intros. intro. - apply (ireg_of_not_RA' r x); auto. congruence. -Qed. - -Hint Resolve ireg_of_not_RA ireg_of_not_RA' ireg_of_not_RA'' : asmgen. - -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. - -Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen. - -(** Useful simplification tactic *) - - -Ltac Simplif := - ((rewrite nextinstr_inv by eauto with asmgen) - || (rewrite nextinstr_inv1 by eauto with asmgen) - || (rewrite Pregmap.gss) - || (rewrite nextinstr_pc) - || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen. - -Ltac Simpl := repeat Simplif. - -(** * Correctness of ARM constructor functions *) - -Section CONSTRUCTORS. - -Variable ge: genv. -Variable fn: function. - -(** Decomposition of integer literals *) - -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 -> - rd <> RA -> - forall (rs: regset) accu, - rs#rd = Vint (Int.repr accu) -> - exists rs', - exec_straight_opt ge fn (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) - /\ rs' # RA = rs # RA. -Proof. - induction 1; intros RD_NOT_RA rs accu ACCU; simpl. -- exists rs; split. apply exec_straight_opt_refl. auto. -- destruct (IHwf_decomposition RD_NOT_RA - (nextinstr (rs#rd <- (insert_in_int rs#rd n p 16))) - (Zinsert accu n p 16)) - as (rs' & P & Q & R & S). - 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. exact P. - split. exact Q. - split. - { intros; Simpl. - rewrite R by auto. Simpl. } - { rewrite S. Simpl. } -Qed. - -Lemma exec_loadimm_z_w: - forall rd l k rs m, - wf_decomposition l -> - rd <> RA -> - exists rs', - exec_straight ge fn (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; intro RD_NOT_RA. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Zinsert 0 n p 16). - set (rs1 := nextinstr (rs#rd <- (Vint (Int.repr accu0)))). - destruct (exec_loadimm_k_w rd k m l H1 RD_NOT_RA rs1 accu0) as (rs2 & P & Q & R & S); 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. - reflexivity. - 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 -> - rd <> RA -> - exists rs', - exec_straight ge fn (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; intro RD_NOT_RA. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Z.lnot (Zinsert 0 n p 16)). - set (rs1 := nextinstr (rs#rd <- (Vint (Int.repr accu0)))). - destruct (exec_loadimm_k_w rd k m (negate_decomposition l) - (negate_decomposition_wf l H1) - RD_NOT_RA rs1 accu0) - as (rs2 & P & Q & R & S). - 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. - reflexivity. - 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 - (RD_NOT_RA : rd <> RA), - exists rs', - exec_straight ge fn (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. trivial. -+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. trivial. -Qed. - -Lemma exec_loadimm_k_x: - forall (rd: ireg) k m l, - wf_decomposition l -> - rd <> RA -> - forall (rs: regset) accu, - rs#rd = Vlong (Int64.repr accu) -> - exists rs', - exec_straight_opt ge fn (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 RD_NOT_RA rs accu ACCU; simpl. -- exists rs; split. apply exec_straight_opt_refl. auto. -- destruct (IHwf_decomposition RD_NOT_RA - (nextinstr (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. exact P. - 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 -> - rd <> RA -> - exists rs', - exec_straight ge fn (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; intro RD_NOT_RA. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Zinsert 0 n p 16). - set (rs1 := nextinstr (rs#rd <- (Vlong (Int64.repr accu0)))). - destruct (exec_loadimm_k_x rd k m l H1 RD_NOT_RA 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. - reflexivity. - 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 -> - rd <> RA -> - exists rs', - exec_straight ge fn (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; intro RD_NOT_RA. -- econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - split. Simpl. - intros; Simpl. -- set (accu0 := Z.lnot (Zinsert 0 n p 16)). - set (rs1 := nextinstr (rs#rd <- (Vlong (Int64.repr accu0)))). - destruct (exec_loadimm_k_x rd k m (negate_decomposition l) - (negate_decomposition_wf l H1) - RD_NOT_RA 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. - reflexivity. - 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, - rd <> RA -> - exists rs', - exec_straight ge fn (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 until m; intro RD_NOT_RA. - 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. trivial. -+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. trivial. -Qed. - -(** Add immediate *) - -Lemma exec_addimm_aux_32: - forall (insn: iregsp -> iregsp -> Z -> instruction) (sem: val -> val -> val), - (forall rd r1 n rs m, - exec_instr ge fn (insn rd r1 n) rs m = - Next (nextinstr (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, - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs' # RA = rs # RA. -Proof. - intros insn sem SEM ASSOC; intros until m; intro RD_NOT_RA. 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. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - split; intros; Simpl. -- econstructor; split. eapply exec_straight_two. - apply SEM. apply SEM. Simpl. Simpl. - split. Simpl. rewrite ASSOC. do 2 f_equal. apply Int.eqm_samerepr. - rewrite E. auto with ints. - split; intros; Simpl. -Qed. - -Lemma exec_addimm32: - forall rd r1 n k rs m, - r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs' # RA = rs # RA. -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). congruence. - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite B, C; eauto with asmgen. - split; intros; Simpl. -+ edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). congruence. - econstructor; split. - eapply exec_straight_trans. eexact A. eapply exec_straight_one. simpl; eauto. auto. - split. Simpl. rewrite B, C; eauto with asmgen. - split; intros; Simpl. -Qed. - -Lemma exec_addimm_aux_64: - forall (insn: iregsp -> iregsp -> Z -> instruction) (sem: val -> val -> val), - (forall rd r1 n rs m, - exec_instr ge fn (insn rd r1 n) rs m = - Next (nextinstr (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, - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs' # RA = rs # RA. -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. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. - split; 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. - split; intros; Simpl. -Qed. - -Lemma exec_addimm64: - forall rd r1 n k rs m, - preg_of_iregsp r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs' # RA = rs # RA. -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). congruence. - 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. - split; intros; Simpl. -+ edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). congruence. - 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. - split; intros; Simpl. -Qed. - -(** Logical immediate *) - -Lemma exec_logicalimm32: - forall (insn1: ireg -> ireg0 -> Z -> instruction) - (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction) - (sem: val -> val -> val), - (forall rd r1 n rs m, - exec_instr ge fn (insn1 rd r1 n) rs m = - Next (nextinstr (rs#rd <- (sem rs##r1 (Vint (Int.repr n))))) m) -> - (forall rd r1 r2 s rs m, - exec_instr ge fn (insn2 rd r1 r2 s) rs m = - Next (nextinstr (rs#rd <- (sem rs##r1 (eval_shift_op_int rs#r2 s)))) m) -> - forall rd r1 n k rs m, - r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs' # RA = rs # RA. -Proof. - intros until sem; intros SEM1 SEM2; intros. unfold logicalimm32. - destruct (is_logical_imm32 n). -- econstructor; split. - apply exec_straight_one. apply SEM1. reflexivity. - split. Simpl. rewrite Int.repr_unsigned; auto. - split; intros; Simpl. -- edestruct (exec_loadimm32 X16 n) as (rs1 & A & B & C). congruence. - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. apply SEM2. reflexivity. - split. Simpl. f_equal; auto. apply C; auto with asmgen. - split; intros; Simpl. -Qed. - -Lemma exec_logicalimm64: - forall (insn1: ireg -> ireg0 -> Z -> instruction) - (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction) - (sem: val -> val -> val), - (forall rd r1 n rs m, - exec_instr ge fn (insn1 rd r1 n) rs m = - Next (nextinstr (rs#rd <- (sem rs###r1 (Vlong (Int64.repr n))))) m) -> - (forall rd r1 r2 s rs m, - exec_instr ge fn (insn2 rd r1 r2 s) rs m = - Next (nextinstr (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s)))) m) -> - forall rd r1 n k rs m, - r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs' # RA = rs # RA. -Proof. - intros until sem; intros SEM1 SEM2; intros. unfold logicalimm64. - destruct (is_logical_imm64 n). -- econstructor; split. - apply exec_straight_one. apply SEM1. reflexivity. - split. Simpl. rewrite Int64.repr_unsigned. auto. - split; intros; Simpl. -- edestruct (exec_loadimm64 X16 n) as (rs1 & A & B & C). congruence. - econstructor; split. - eapply exec_straight_trans. eexact A. - apply exec_straight_one. apply SEM2. reflexivity. - split. Simpl. f_equal; auto. apply C; auto with asmgen. - split; intros; Simpl. -Qed. - -(** Load address of symbol *) - -Lemma exec_loadsymbol: forall rd s ofs k rs m, - rd <> X16 \/ Archi.pic_code tt = false -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs'#RA = rs#RA. -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 | reflexivity]. - split. Simpl. split; intros; Simpl. - -+ exploit exec_addimm64. instantiate (1 := rd). simpl. destruct H; congruence. - instantiate (1 := rd). assumption. - intros (rs1 & A & B & C & D). - 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. - split; intros. rewrite C by auto; Simpl. - rewrite D. Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. Simpl. rewrite symbol_high_low; auto. - split; 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 fn (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|auto] | split; [Simpl|intros;Simpl]]). -Qed. - -Lemma exec_move_extended: forall rd r1 ex (a: amount64) k rs m, - exists rs', - exec_straight ge fn (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_instr. 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: iregsp -> iregsp -> ireg -> extend_op -> instruction) - (insnS: ireg -> ireg0 -> ireg -> shift_op -> instruction), - (forall rd r1 r2 x rs m, - exec_instr ge fn (insnX rd r1 r2 x) rs m = - Next (nextinstr (rs#rd <- (sem rs#r1 (eval_extend rs#r2 x)))) m) -> - (forall rd r1 r2 s rs m, - exec_instr ge fn (insnS rd r1 r2 s) rs m = - Next (nextinstr (rs#rd <- (sem rs###r1 (eval_shift_op_long rs#r2 s)))) m) -> - forall (rd r1 r2: ireg) (ex: extension) (a: amount64) (k: code) rs m, - r1 <> X16 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs' # RA = rs # RA. -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. - split; 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 ir0x. rewrite C by eauto with asmgen. f_equal. - rewrite B. destruct ex; auto. - split; 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 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs' # RA = rs # RA. -Proof. - unfold shrx32; intros. apply Val.shrx_shr_3 in H. - destruct (Int.eq n Int.zero) eqn:E. -- econstructor; split. apply exec_straight_one; [simpl;eauto|auto]. - split. Simpl. subst v; auto. - split; intros; Simpl. -- generalize (Int.eq_spec n Int.one). - destruct (Int.eq n Int.one); intro ONE. - * subst n. - econstructor; split. eapply exec_straight_two. - all: simpl; auto. - split. - ** subst v; Simpl. - destruct (Val.add _ _); simpl; trivial. - change (Int.ltu Int.one Int.iwordsize) with true; simpl. - rewrite Int.or_zero_l. - reflexivity. - ** split; intros; Simpl. - * econstructor; split. eapply exec_straight_three. - unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. - simpl; eauto. - unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto. - auto. auto. auto. - split. subst v; Simpl. - split; 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 -> - (IR RA) <> (preg_of_iregsp (RR1 rd)) -> - exists rs', - exec_straight ge fn (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) - /\ rs' # RA = rs # RA. -Proof. - unfold shrx64; intros. apply Val.shrxl_shrl_3 in H. - destruct (Int.eq n Int.zero) eqn:E. -- econstructor; split. apply exec_straight_one; [simpl;eauto|auto]. - split. Simpl. subst v; auto. - split; intros; Simpl. -- generalize (Int.eq_spec n Int.one). - destruct (Int.eq n Int.one); intro ONE. - * subst n. - econstructor; split. eapply exec_straight_two. - all: simpl; auto. - split. - ** subst v; Simpl. - destruct (Val.addl _ _); simpl; trivial. - change (Int.ltu Int.one Int64.iwordsize') with true; simpl. - rewrite Int64.or_zero_l. - reflexivity. - ** split; intros; Simpl. - * econstructor; split. eapply exec_straight_three. - unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. - simpl; eauto. - unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto. - auto. auto. auto. - split. subst v; Simpl. - split; intros; Simpl. -Qed. - -(** Condition bits *) - -Lemma compare_int_spec: forall rs v1 v2 m, - let rs' := compare_int rs v1 v2 m in - rs'#CN = (Val.negative (Val.sub v1 v2)) - /\ rs'#CZ = (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2) - /\ rs'#CC = (Val.cmpu (Mem.valid_pointer m) 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 m, - Val.cmp_bool c v1 v2 = Some b -> - eval_testcond (cond_for_signed_cmp c) (compare_int rs v1 v2 m) = Some b. -Proof. - intros. generalize (compare_int_spec rs v1 v2 m). - set (rs' := compare_int rs v1 v2 m). 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 m, - Val.cmpu_bool (Mem.valid_pointer m) c v1 v2 = Some b -> - eval_testcond (cond_for_unsigned_cmp c) (compare_int rs v1 v2 m) = Some b. -Proof. - intros. generalize (compare_int_spec rs v1 v2 m). - set (rs' := compare_int rs v1 v2 m). 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 m, - let rs' := compare_long rs v1 v2 m in - rs'#CN = (Val.negativel (Val.subl v1 v2)) - /\ rs'#CZ = (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Ceq v1 v2)) - /\ rs'#CC = (Val.maketotal (Val.cmplu (Mem.valid_pointer m) 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 m, - Val.cmpl_bool c v1 v2 = Some b -> - eval_testcond (cond_for_signed_cmp c) (compare_long rs v1 v2 m) = Some b. -Proof. - intros. generalize (compare_long_spec rs v1 v2 m). - set (rs' := compare_long rs v1 v2 m). 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 m, - Val.cmplu_bool (Mem.valid_pointer m) c v1 v2 = Some b -> - eval_testcond (cond_for_unsigned_cmp c) (compare_long rs v1 v2 m) = Some b. -Proof. - intros. generalize (compare_long_spec rs v1 v2 m). - set (rs' := compare_long rs v1 v2 m). 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 (Int64.eq i Int64.zero && - (Mem.valid_pointer m b0 (Ptrofs.unsigned i0) - || Mem.valid_pointer m b0 (Ptrofs.unsigned i0 - 1))); try discriminate. - destruct c; simpl in H; inv H; reflexivity. -- (* ptr-int *) - simpl. - destruct (Int64.eq i0 Int64.zero && - (Mem.valid_pointer m b0 (Ptrofs.unsigned i) - || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); try discriminate. - destruct c; simpl in H; inv H; reflexivity. -- (* ptr-ptr *) - simpl. - destruct (eq_block b0 b1). -+ destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) - || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1)) && - (Mem.valid_pointer m b1 (Ptrofs.unsigned i0) - || Mem.valid_pointer m b1 (Ptrofs.unsigned i0 - 1))); - 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 (Mem.valid_pointer m b0 (Ptrofs.unsigned i) && - Mem.valid_pointer m b1 (Ptrofs.unsigned i0)); try discriminate. - 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 -> - (nextinstr (compare_float rs v1 v2))#r = (nextinstr 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 -> - (nextinstr (compare_single rs v1 v2))#r = (nextinstr rs)#r. -Proof. - intros; unfold compare_single. - destruct r; try contradiction; destruct v1; auto; destruct v2; auto. -Qed. - -(** Translation of conditionals *) - -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). - -Lemma compare_int_RA: - forall rs a b m, - compare_int rs a b m X30 = rs X30. -Proof. - unfold compare_int. - intros. - repeat rewrite Pregmap.gso by congruence. - trivial. -Qed. - -Hint Resolve compare_int_RA : asmgen. - -Lemma compare_long_RA: - forall rs a b m, - compare_long rs a b m X30 = rs X30. -Proof. - unfold compare_long. - intros. - repeat rewrite Pregmap.gso by congruence. - trivial. -Qed. - -Hint Resolve compare_long_RA : asmgen. - -Lemma compare_float_RA: - forall rs a b, - compare_float rs a b X30 = rs X30. -Proof. - unfold compare_float. - intros. - destruct a; destruct b. - all: repeat rewrite Pregmap.gso by congruence; trivial. -Qed. - -Hint Resolve compare_float_RA : asmgen. - - -Lemma compare_single_RA: - forall rs a b, - compare_single rs a b X30 = rs X30. -Proof. - unfold compare_single. - intros. - destruct a; destruct b. - all: repeat rewrite Pregmap.gso by congruence; trivial. -Qed. - -Hint Resolve compare_single_RA : asmgen. - - -Lemma transl_cond_correct: - forall cond args k c rs m, - transl_cond cond args k = OK c -> - exists rs', - exec_straight ge fn 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) - /\ rs' # RA = rs # RA. -Proof. - intros until m; intros TR. destruct cond; simpl in TR; ArgsInv. -- (* Ccomp *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -- (* Ccompu *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat 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. - repeat 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. - repeat split; intros. apply eval_testcond_compare_sint; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). congruence. 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. - repeat split; intros. apply eval_testcond_compare_sint; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. - auto with asmgen. - Simpl. rewrite compare_int_RA. - apply C; congruence. -- (* Ccompuimm *) - destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat 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. - repeat split; intros. apply eval_testcond_compare_uint; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). congruence. 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. - repeat split; intros. apply eval_testcond_compare_uint; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_int_RA. - apply C; congruence. -- (* Ccompshift *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat 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. - repeat 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. - repeat split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Ceq); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm32 X16 n). congruence. 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. - repeat split; intros. apply (eval_testcond_compare_sint Ceq); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_int_RA. - apply C; congruence. - -- (* Cmasknotzero *) - destruct (is_logical_imm32 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite Int.repr_unsigned. apply (eval_testcond_compare_sint Cne); auto. - destruct r; reflexivity || discriminate. - -+ exploit (exec_loadimm32 X16 n). congruence. 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. - repeat split; intros. apply (eval_testcond_compare_sint Cne); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_int_RA. - apply C; congruence. - -- (* Ccompl *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -- (* Ccomplu *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. apply eval_testcond_compare_ulong; auto. - 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. - repeat 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. auto. - repeat split; intros. apply eval_testcond_compare_slong; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). congruence. 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. - repeat split; intros. apply eval_testcond_compare_slong; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_long_RA. - apply C; congruence. - -- (* Ccompluimm *) - destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. - destruct r; reflexivity || discriminate. -+ econstructor; split. - apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. auto. - repeat split; intros. apply eval_testcond_compare_ulong; auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). congruence. 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. - repeat split; intros. apply eval_testcond_compare_ulong; auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_long_RA. - apply C; congruence. - -- (* Ccomplshift *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat 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. auto. - repeat split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. - destruct r; reflexivity || discriminate. -- (* Cmasklzero *) - destruct (is_logical_imm64 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Ceq); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). congruence. 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. - repeat split; intros. apply (eval_testcond_compare_slong Ceq); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_long_RA. - apply C; congruence. - -- (* Cmasknotzero *) - destruct (is_logical_imm64 n). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - repeat split; intros. rewrite Int64.repr_unsigned. apply (eval_testcond_compare_slong Cne); auto. - destruct r; reflexivity || discriminate. -+ exploit (exec_loadimm64 X16 n). congruence. 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. - repeat split; intros. apply (eval_testcond_compare_slong Cne); auto. - transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - Simpl. rewrite compare_long_RA. - apply C; congruence. - -- (* Ccompf *) - econstructor; split. apply exec_straight_one. simpl; eauto. - rewrite compare_float_inv; auto. - repeat split; intros. apply eval_testcond_compare_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. - Simpl. -- (* Cnotcompf *) - econstructor; split. apply exec_straight_one. simpl; eauto. - rewrite compare_float_inv; auto. - repeat split; intros. apply eval_testcond_compare_not_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. - Simpl. -- (* Ccompfzero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - rewrite compare_float_inv; auto. - repeat split; intros. apply eval_testcond_compare_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. - Simpl. -- (* Cnotcompfzero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - rewrite compare_float_inv; auto. - repeat split; intros. apply eval_testcond_compare_not_float; auto. - destruct r; discriminate || rewrite compare_float_inv; auto. - Simpl. -- (* Ccompfs *) - econstructor; split. apply exec_straight_one. simpl; eauto. - rewrite compare_single_inv; auto. - repeat split; intros. apply eval_testcond_compare_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. - Simpl. -- (* Cnotcompfs *) - econstructor; split. apply exec_straight_one. simpl; eauto. - rewrite compare_single_inv; auto. - repeat split; intros. apply eval_testcond_compare_not_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. - Simpl. -- (* Ccompfszero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - rewrite compare_single_inv; auto. - repeat split; intros. apply eval_testcond_compare_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. - Simpl. -- (* Cnotcompfszero *) - econstructor; split. apply exec_straight_one. simpl; eauto. - rewrite compare_single_inv; auto. - repeat split; intros. apply eval_testcond_compare_not_single; auto. - destruct r; discriminate || rewrite compare_single_inv; auto. - Simpl. -Qed. - -(** Translation of conditional branches *) - -Lemma transl_cond_branch_correct: - forall cond args lbl k c rs m b, - transl_cond_branch cond args lbl k = OK c -> - eval_condition cond (map rs (map preg_of args)) m = Some b -> - exists rs' insn, - exec_straight_opt ge fn c rs m (insn :: k) rs' m - /\ exec_instr ge fn insn rs' m = - (if b then goto_label fn lbl rs' m else Next (nextinstr rs') m) - /\ (forall r, data_preg r = true -> rs'#r = rs#r) - /\ rs' # RA = rs # RA. -Proof. - intros until b; intros TR EV. - assert (DFL: - transl_cond_branch_default cond args lbl k = OK c -> - exists rs' insn, - exec_straight_opt ge fn c rs m (insn :: k) rs' m - /\ exec_instr ge fn insn rs' m = - (if b then goto_label fn lbl rs' m else Next (nextinstr rs') m) - /\ (forall r, data_preg r = true -> rs'#r = rs#r) - /\ rs' # RA = rs # RA ). - { - unfold transl_cond_branch_default; intros. - exploit transl_cond_correct; eauto. intros (rs' & A & B & C & D). - exists rs', (Pbc (cond_for_cond cond) lbl); split. - apply exec_straight_opt_intro. eexact A. - repeat split; auto. simpl. rewrite (B b) by auto. auto. - } -Local Opaque transl_cond transl_cond_branch_default. - destruct args as [ | a1 args]; simpl in TR; auto. - destruct args as [ | a2 args]; simpl in TR; auto. - destruct cond; simpl in TR; auto. -- (* Ccompimm *) - destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; - apply Int.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccompimm Cne 0 *) - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. destruct (rs x); simpl in EV; inv EV. simpl. auto. -+ (* Ccompimm Ceq 0 *) - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. destruct (rs x); simpl in EV; inv EV. simpl. destruct (Int.eq i Int.zero); auto. -- (* Ccompuimm *) - destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; - apply Int.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccompuimm Cne 0 *) - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. rewrite EV. auto. -+ (* Ccompuimm Ceq 0 *) - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV. destruct b; auto. -- (* Cmaskzero *) - destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. - erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. - rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto. -- (* Cmasknotzero *) - destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv. - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. - erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto. - rewrite EV. auto. -- (* Ccomplimm *) - destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; - apply Int64.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccomplimm Cne 0 *) - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. destruct (rs x); simpl in EV; inv EV. simpl. auto. -+ (* Ccomplimm Ceq 0 *) - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. destruct (rs x); simpl in EV; inv EV. simpl. destruct (Int64.eq i Int64.zero); auto. -- (* Ccompluimm *) - destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; - apply Int64.same_if_eq in N0; subst n; ArgsInv. -+ (* Ccompluimm Cne 0 *) - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. rewrite EV. auto. -+ (* Ccompluimm Ceq 0 *) - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cne), EV. destruct b; auto. -- (* Cmasklzero *) - destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. - erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. - rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto. -- (* Cmasklnotzero *) - destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv. - do 2 econstructor; split. - apply exec_straight_opt_refl. - split; auto. simpl. - erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto. - rewrite EV. auto. -Qed. - -(** Translation of arithmetic operations *) - -Ltac SimplEval H := - match type of H with - | Some _ = None _ => discriminate - | Some _ = Some _ => inv H - | ?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; [simpl; eauto | reflexivity] - | split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl; - apply Val.lessdef_same; Simpl; fail - | split; [ intros; Simpl; fail - | intros; Simpl; eauto with asmgen; fail] ]]. - -Ltac TranslOpBase := - econstructor; split; - [ apply exec_straight_one; [simpl; eauto | reflexivity] - | split; [ rewrite ? transl_eval_shift, ? transl_eval_shiftl; Simpl - | split; [ intros; Simpl; fail - | intros; Simpl; eapply RA_not_written2; eauto] ]]. - -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 fn 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) - /\ rs' RA = rs RA. -Proof. -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. -- (* move *) - destruct (preg_of res) eqn:RR; try discriminate; destruct (preg_of m0) eqn:R1; inv TR. - all: TranslOpSimpl. -- (* intconst *) - exploit exec_loadimm32. apply (ireg_of_not_RA res); eassumption. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. - split. intros; auto with asmgen. - apply C. congruence. - eapply ireg_of_not_RA''; eauto. -- (* longconst *) - exploit exec_loadimm64. apply (ireg_of_not_RA res); eassumption. - intros (rs' & A & B & C). - exists rs'; split. eexact A. split. rewrite B; auto. - split. intros; auto with asmgen. - apply C. congruence. - eapply ireg_of_not_RA''; eauto. -- (* floatconst *) - destruct (Float.eq_dec n Float.zero). -+ subst n. TranslOpSimpl. -+ TranslOpSimpl. -- (* singleconst *) - destruct (Float32.eq_dec n Float32.zero). -+ subst n. TranslOpSimpl. -+ TranslOpSimpl. -- (* loadsymbol *) - exploit (exec_loadsymbol x id ofs). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. rewrite B; auto. - split; auto. -- (* addrstack *) - exploit (exec_addimm64 x XSP (Ptrofs.to_int64 ofs)). simpl; eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. simpl in B; 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. eapply ireg_of_not_RA''; eassumption. - intros (rs' & A & B & C & D). - 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. apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. rewrite B; auto. - split; auto. -- (* orimm *) - exploit (exec_logicalimm32 (Porrimm W) (Porr W)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. rewrite B; auto. - split; auto. -- (* xorimm *) - exploit (exec_logicalimm32 (Peorimm W) (Peor W)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - 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 *) - exploit (exec_shrx32 x x0 n); eauto with asmgen. apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - econstructor; split. eexact A. split. rewrite B; auto. - split; auto. -- (* 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. - split; eauto with asmgen. -- (* addext *) - exploit (exec_arith_extended Val.addl Paddext (Padd X)). - auto. auto. instantiate (1 := x1). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - econstructor; split. eexact A. split. rewrite B; auto. - split; auto. -- (* addlimm *) - exploit (exec_addimm64 x x0 n). simpl. generalize (ireg_of_not_X16 _ _ EQ1). congruence. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. simpl in B; rewrite B; auto. auto. -- (* subext *) - exploit (exec_arith_extended Val.subl Psubext (Psub X)). - auto. auto. instantiate (1 := x1). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - econstructor; split. eexact A. split. rewrite B; auto. - split; auto. -- (* mull *) - TranslOpBase. - destruct (rs x0); auto; destruct (rs x1); auto. simpl. rewrite Int64.add_zero_l; auto. -- (* andlimm *) - exploit (exec_logicalimm64 (Pandimm X) (Pand X)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* orlimm *) - exploit (exec_logicalimm64 (Porrimm X) (Porr X)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - exists rs'; split. eexact A. split. rewrite B; auto. auto. -- (* xorlimm *) - exploit (exec_logicalimm64 (Peorimm X) (Peor X)). - intros; reflexivity. intros; reflexivity. instantiate (1 := x0). eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. - intros (rs' & A & B & C & D). - 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. -- (* shrx *) - exploit (exec_shrx64 x x0 n); eauto with asmgen. - apply (ireg_of_not_RA'' res); eassumption. intros (rs' & A & B & C & D ). - econstructor; split. eexact A. split. rewrite B; auto. auto. -- (* 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 & D). - 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. - split; intros; Simpl. -- (* select *) - destruct (preg_of res) 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 & D). - 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. rewrite !C. apply Val.lessdef_normalize. - rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. - auto. - split; intros; Simpl. - rewrite <- D. - eapply RA_not_written2; eassumption. - + (* 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 & D). - 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. rewrite !C. apply Val.lessdef_normalize. - rewrite <- E2; auto with asmgen. rewrite <- E1; auto with asmgen. - auto. - split; intros; Simpl. -Qed. - -(** Translation of addressing modes, loads, stores *) - -Lemma transl_addressing_correct: - forall sz addr args (insn: Asm.addressing -> instruction) 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 fn c rs m (insn ad :: k) rs' m - /\ Asm.eval_addressing ge ad rs' = Vptr b o - /\ (forall r, data_preg r = true -> rs' r = rs r) - /\ rs' # RA = rs # RA. -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). congruence. 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. - split; 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. auto. - split. simpl. Simpl. rewrite H0. simpl. rewrite Ptrofs.add_zero. auto. - split; 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. - instantiate (1 := X16). simpl. congruence. - intros (rs' & A & B & C & D). - 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. - split; intros. - apply C; eauto with asmgen. - trivial. -- (* 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. auto. - split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence. - split; intros; Simpl. -+ exploit (exec_loadsymbol X16 id ofs). auto. - simpl. congruence. - intros (rs' & A & B & C & D). - 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. - split; 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)). - simpl. congruence. - 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 TRAP 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 fn 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) - /\ rs' # RA = rs # RA. -Proof. - intros. destruct vaddr; try discriminate. - assert (A: exists sz insn, - transl_addressing sz addr args insn k = OK c - /\ (forall ad rs', exec_instr ge fn (insn ad) rs' m = - exec_load ge chunk (fun v => v) ad (preg_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 & S). - assert (X: exec_load ge chunk (fun v => v) ad (preg_of dst) rs' m = - Next (nextinstr (rs'#(preg_of dst) <- v)) m). - { unfold exec_load. rewrite Q, H1. auto. } - econstructor; split. - eapply exec_straight_opt_right. eexact P. - apply exec_straight_one. rewrite C, X; eauto. Simpl. - split. Simpl. - split; intros; Simpl. - rewrite <- S. - apply RA_not_written. -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 fn c rs m k rs' m' - /\ (forall r, data_preg r = true -> rs' r = rs r) - /\ rs' # RA = rs # RA. -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_instr ge fn (insn ad) rs' m = - exec_store ge 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 & S). - 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 ge chunk' ad rs'#(preg_of src) rs' m = - Next (nextinstr rs') m'). - { unfold exec_store. 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. Simpl. - split; intros; Simpl. -Qed. - -(** Translation of indexed memory accesses *) - -Lemma indexed_memory_access_correct: forall insn sz (base: iregsp) ofs k (rs: regset) m b i, - preg_of_iregsp base <> IR X16 -> - Val.offset_ptr rs#base ofs = Vptr b i -> - exists ad rs', - exec_straight_opt ge fn (indexed_memory_access insn sz base ofs k) rs m (insn ad :: k) rs' m - /\ Asm.eval_addressing ge ad rs' = Vptr b i - /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r. -Proof. - unfold indexed_memory_access; 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. - simpl. congruence. - intros (rs' & A & B & C). - econstructor; econstructor; split. apply exec_straight_opt_intro; eexact A. - split. simpl. rewrite B, C by eauto with asmgen. 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 fn (loadptr 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. rewrite B, H. eauto. auto. - split. Simpl. - intros; Simpl. -Qed. - -Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset), - Mem.storev Mint64 m (Val.offset_ptr rs#base ofs) rs#src = Some m' -> - preg_of_iregsp base <> IR X16 -> - src <> X16 -> - exists rs', - exec_straight ge fn (storeptr src base ofs k) rs m k rs' m' - /\ (forall r, r <> PC -> r <> X16 -> rs' r = rs r) - /\ rs' RA = rs RA. -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_store. rewrite B, C, H by eauto with asmgen. eauto. auto. - split; 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 fn 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) - /\ rs' RA = rs RA. -Proof. - intros. - destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. - assert (X: exists sz insn, - c = indexed_memory_access insn sz base ofs k - /\ (forall ad rs', exec_instr ge fn (insn ad) rs' m = - exec_load ge (chunk_of_type ty) (fun v => v) ad (preg_of dst) rs' m)). - { - unfold loadind in H; destruct ty; destruct (preg_of dst); inv H; do 2 econstructor; 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. rewrite B, H0. eauto. Simpl. - split. Simpl. - split. intros; Simpl. - Simpl. rewrite RA_not_written. - apply C; congruence. -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 fn c rs m k rs' m' - /\ (forall r, data_preg r = true -> rs' r = rs r) - /\ rs' RA = rs RA. -Proof. - intros. - destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate. - assert (X: exists sz insn, - c = indexed_memory_access insn sz base ofs k - /\ (forall ad rs', exec_instr ge fn (insn ad) rs' m = - exec_store ge (chunk_of_type ty) ad rs'#(preg_of src) rs' m)). - { - unfold storeind in H; destruct ty; destruct (preg_of src); inv H; do 2 econstructor; 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. rewrite B, C, H0 by eauto with asmgen. eauto. - Simpl. - split. intros; Simpl. - Simpl. -Qed. - -Lemma make_epilogue_correct: - forall ge0 f m stk soff cs m' ms rs k tm, - (is_leaf_function f = true -> rs # (IR RA) = parent_ra cs) -> - load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp cs) -> - ((* FIXME is_leaf_function f = false -> *) 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 fn (make_epilogue f k) rs tm k 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 <> RA -> r <> X16 -> rs'#r = rs#r). -Proof. - intros until tm; intros LEAF_RA LP LRA FREE AG MEXT MCS. - - (* FIXME - Cannot be used at this point - destruct (is_leaf_function f) eqn:IS_LEAF. - { - exploit Mem.loadv_extends. eauto. eexact LP. auto. simpl. intros (parent' & LP' & LDP'). - exploit lessdef_parent_sp; eauto. intros EQ; subst parent'; clear LDP'. - exploit Mem.free_parallel_extends; eauto. intros (tm' & FREE' & MEXT'). - unfold make_epilogue. - rewrite IS_LEAF. - - econstructor; econstructor; split. - apply exec_straight_one. simpl. - rewrite <- (sp_val _ _ _ AG). simpl; rewrite LP'. - rewrite FREE'. eauto. auto. - split. apply agree_nextinstr. apply agree_set_other; auto. - apply agree_change_sp with (Vptr stk soff). - apply agree_exten with rs; auto. - eapply parent_sp_def; eauto. - split. auto. - split. Simpl. - split. Simpl. - intros. Simpl. - } - lapply LRA. 2: reflexivity. - clear LRA. intro LRA. *) - 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. - (* FIXME rewrite IS_LEAF. *) - exploit (loadptr_correct XSP (fn_retaddr_ofs f)). - instantiate (2 := rs). simpl. rewrite <- (sp_val _ _ _ AG). simpl. eexact LRA'. simpl; congruence. - 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. auto. - split. apply agree_nextinstr. 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/PostpassScheduling.v b/aarch64/PostpassScheduling.v index fa7e2776..74c2438e 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.v @@ -17,9 +17,8 @@ Require Import Coqlib Errors AST Integers. Require Import Asmblock Axioms Memory Globalenvs. -Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops. +Require Import Asmblockdeps Asmblockprops. Require Import IterList. -(*Require Peephole.*) Local Open Scope error_monad_scope. @@ -33,188 +32,6 @@ Section verify_schedule. Variable lk: aarch64_linker. -(* -(** * Concat all bundles into one big basic block *) - -(* Lemmas necessary for defining concat_all *) -Lemma app_nonil {A: Type} (l l': list A) : l <> nil -> l ++ l' <> nil. -Proof. - intros. destruct l; simpl. - - contradiction. - - discriminate. -Qed. - -Lemma app_nonil2 {A: Type} : forall (l l': list A), l' <> nil -> l ++ l' <> nil. -Proof. - destruct l. - - intros. simpl; auto. - - intros. rewrite <- app_comm_cons. discriminate. -Qed. - -Definition check_size bb := - if zlt Ptrofs.max_unsigned (size bb) - then Error (msg "PostpassSchedulingproof.check_size") - else OK tt. - -Program Definition concat2 (bb bb': bblock) : res bblock := - do ch <- check_size bb; - do ch' <- check_size bb'; - match (exit bb) with - | None => - match (header bb') with - | nil => - match (exit bb') with - | Some (PExpand (Pbuiltin _ _ _)) => Error (msg "PostpassSchedulingproof.concat2: builtin not alone") - | _ => OK {| header := header bb; body := body bb ++ body bb'; exit := exit bb' |} - end - | _ => Error (msg "PostpassSchedulingproof.concat2") - end - | _ => Error (msg "PostpassSchedulingproof.concat2") - end. -Next Obligation. - apply wf_bblock_refl. constructor. - - destruct bb' as [hd' bdy' ex' WF']. destruct bb as [hd bdy ex WF]. simpl in *. - apply wf_bblock_refl in WF'. apply wf_bblock_refl in WF. - inversion_clear WF'. inversion_clear WF. clear H1 H3. - inversion H2; inversion H0. - + left. apply app_nonil. auto. - + right. auto. - + left. apply app_nonil2. auto. - + right. auto. - - unfold builtin_alone. intros. rewrite H0 in H. - assert (Some (PExpand (Pbuiltin ef args res)) <> Some (PExpand (Pbuiltin ef args res))). - apply (H ef args res). contradict H1. auto. -Defined. - -Lemma concat2_zlt_size: - forall a b bb, - concat2 a b = OK bb -> - size a <= Ptrofs.max_unsigned - /\ size b <= Ptrofs.max_unsigned. -Proof. - intros. monadInv H. - split. - - unfold check_size in EQ. destruct (zlt Ptrofs.max_unsigned (size a)); monadInv EQ. omega. - - unfold check_size in EQ1. destruct (zlt Ptrofs.max_unsigned (size b)); monadInv EQ1. omega. -Qed. - -Lemma concat2_noexit: - forall a b bb, - concat2 a b = OK bb -> - exit a = None. -Proof. - intros. destruct a as [hd bdy ex WF]; simpl in *. - destruct ex as [e|]; simpl in *; auto. - unfold concat2 in H. simpl in H. monadInv H. -Qed. - -Lemma concat2_decomp: - forall a b bb, - concat2 a b = OK bb -> - body bb = body a ++ body b - /\ exit bb = exit b. -Proof. - intros. exploit concat2_noexit; eauto. intros. - destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bd ex WF]; simpl in *. - subst exa. - unfold concat2 in H; simpl in H. - destruct hdb. - - destruct exb. - + destruct c. - * destruct i; monadInv H; split; auto. - * monadInv H. split; auto. - + monadInv H. split; auto. - - monadInv H. -Qed. - -Lemma concat2_size: - forall a b bb, concat2 a b = OK bb -> size bb = size a + size b. -Proof. - intros. unfold concat2 in H. - destruct a as [hda bda exa WFa]; destruct b as [hdb bdb exb WFb]; destruct bb as [hd bdy ex WF]; simpl in *. - destruct exa; monadInv H. destruct hdb; try (monadInv EQ2). destruct exb; try (monadInv EQ2). - - destruct c. - + destruct i; monadInv EQ2; - unfold size; simpl; rewrite app_length; rewrite Nat.add_0_r; rewrite <- Nat2Z.inj_add; rewrite Nat.add_assoc; reflexivity. - + monadInv EQ2. unfold size; simpl. rewrite app_length. rewrite Nat.add_0_r. rewrite <- Nat2Z.inj_add. rewrite Nat.add_assoc. reflexivity. - - unfold size; simpl. rewrite app_length. repeat (rewrite Nat.add_0_r). rewrite <- Nat2Z.inj_add. reflexivity. -Qed. - -Lemma concat2_header: - forall bb bb' tbb, - concat2 bb bb' = OK tbb -> header bb = header tbb. -Proof. - intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *. - unfold concat2 in H. simpl in H. monadInv H. - destruct ex; try discriminate. destruct hd'; try discriminate. destruct ex'. - - destruct c. - + destruct i; try discriminate; congruence. - + congruence. - - congruence. -Qed. - -Lemma concat2_no_header_in_middle: - forall bb bb' tbb, - concat2 bb bb' = OK tbb -> - header bb' = nil. -Proof. - intros. destruct bb as [hd bdy ex COR]; destruct bb' as [hd' bdy' ex' COR']; destruct tbb as [thd tbdy tex tCOR]; simpl in *. - unfold concat2 in H. simpl in H. monadInv H. - destruct ex; try discriminate. destruct hd'; try discriminate. reflexivity. -Qed. - - - -Fixpoint concat_all (lbb: list bblock) : res bblock := - match lbb with - | nil => Error (msg "PostpassSchedulingproof.concatenate: empty list") - | bb::nil => OK bb - | bb::lbb => - do bb' <- concat_all lbb; - concat2 bb bb' - end. - -Lemma concat_all_size : - forall lbb a bb bb', - concat_all (a :: lbb) = OK bb -> - concat_all lbb = OK bb' -> - size bb = size a + size bb'. -Proof. - intros. unfold concat_all in H. fold concat_all in H. - destruct lbb; try discriminate. - monadInv H. rewrite H0 in EQ. inv EQ. - apply concat2_size. assumption. -Qed. - -Lemma concat_all_header: - forall lbb bb tbb, - concat_all (bb::lbb) = OK tbb -> header bb = header tbb. -Proof. - destruct lbb. - - intros. simpl in H. congruence. - - intros. simpl in H. destruct lbb. - + inv H. eapply concat2_header; eassumption. - + monadInv H. eapply concat2_header; eassumption. -Qed. - -Lemma concat_all_no_header_in_middle: - forall lbb tbb, - concat_all lbb = OK tbb -> - Forall (fun b => header b = nil) (tail lbb). -Proof. - induction lbb; intros; try constructor. - simpl. simpl in H. destruct lbb. - - constructor. - - monadInv H. simpl tl in IHlbb. constructor. - + apply concat2_no_header_in_middle in EQ0. apply concat_all_header in EQ. congruence. - + apply IHlbb in EQ. assumption. -Qed. - -Inductive is_concat : bblock -> list bblock -> Prop := - | mk_is_concat: forall tbb lbb, concat_all lbb = OK tbb -> is_concat tbb lbb. -*) -(** * Remainder of the verified scheduler *) - Definition verify_schedule (bb bb' : bblock) : res unit := match bblock_simub bb bb' with | true => OK tt @@ -230,105 +47,6 @@ Proof. apply Z.eqb_eq. assumption. Qed. -(* Lemma verify_schedule_no_header: - forall bb bb', - verify_schedule (no_header bb) bb' = verify_schedule bb bb'. -Proof. - intros. unfold verify_schedule. unfold bblock_simub. unfold pure_bblock_simu_test, bblock_simu_test. rewrite trans_block_noheader_inv. - reflexivity. -Qed. *) - - -(*Lemma stick_header_verify_schedule:*) - (*forall hd bb' hbb' bb,*) - (*stick_header hd bb' = hbb' ->*) - (*verify_schedule bb bb' = verify_schedule bb hbb'.*) -(*Proof.*) - (*intros. unfold verify_schedule. unfold bblock_simub, pure_bblock_simu_test, bblock_simu_test.*) - (*rewrite <- H. rewrite trans_block_header_inv. reflexivity.*) -(*Qed.*) - -(*Lemma check_size_stick_header:*) - (*forall bb hd,*) - (*check_size bb = check_size (stick_header hd bb).*) -(*Proof.*) - (*intros. unfold check_size. rewrite stick_header_size. reflexivity.*) -(*Qed.*) - -(*Lemma stick_header_concat2:*) - (*forall bb bb' hd tbb,*) - (*concat2 bb bb' = OK tbb ->*) - (*concat2 (stick_header hd bb) bb' = OK (stick_header hd tbb).*) -(*Proof.*) - (*intros. monadInv H. erewrite check_size_stick_header in EQ.*) - (*unfold concat2. rewrite EQ. rewrite EQ1. simpl.*) - (*destruct bb as [hdr bdy ex COR]; destruct bb' as [hdr' bdy' ex' COR']; simpl in *.*) - (*destruct ex; try discriminate. destruct hdr'; try discriminate. destruct ex'.*) - (*- destruct c.*) - (*+ destruct i; try discriminate; inv EQ2; unfold stick_header; simpl; reflexivity.*) - (*+ inv EQ2. unfold stick_header; simpl. reflexivity.*) - (*- inv EQ2. unfold stick_header; simpl. reflexivity.*) -(*Qed.*) - -(*Lemma stick_header_concat_all:*) - (*forall bb c tbb hd,*) - (*concat_all (bb :: c) = OK tbb ->*) - (*concat_all (stick_header hd bb :: c) = OK (stick_header hd tbb).*) -(*Proof.*) - (*intros. simpl in *. destruct c; try congruence.*) - (*monadInv H. rewrite EQ. simpl.*) - (*apply stick_header_concat2. assumption.*) -(*Qed.*) - -(*Lemma stick_header_code_no_header:*) - (*forall bb c,*) - (*stick_header_code (header bb) (no_header bb :: c) = OK (bb :: c).*) -(*Proof.*) - (*intros. unfold stick_header_code. simpl. rewrite stick_header_no_header. reflexivity.*) -(*Qed.*) - -(*Lemma hd_tl_size:*) - (*forall lbb bb, hd_error lbb = Some bb -> size_blocks lbb = size bb + size_blocks (tl lbb).*) -(*Proof.*) - (*destruct lbb.*) - (*- intros. simpl in H. discriminate.*) - (*- intros. simpl in H. inv H. simpl. reflexivity.*) -(*Qed.*) - -(*Lemma stick_header_code_size:*) - (*forall h lbb lbb', stick_header_code h lbb = OK lbb' -> size_blocks lbb = size_blocks lbb'.*) -(*Proof.*) - (*intros. unfold stick_header_code in H. destruct (hd_error lbb) eqn:HD; try discriminate.*) - (*inv H. simpl. rewrite stick_header_size. erewrite hd_tl_size; eauto.*) -(*Qed.*) - -(*Lemma stick_header_code_no_header_in_middle:*) - (*forall c h lbb,*) - (*stick_header_code h c = OK lbb ->*) - (*Forall (fun b => header b = nil) (tl c) ->*) - (*Forall (fun b => header b = nil) (tl lbb).*) -(*Proof.*) - (*destruct c; intros.*) - (*- unfold stick_header_code in H. simpl in H. discriminate.*) - (*- unfold stick_header_code in H. simpl in H. inv H. simpl in H0.*) - (*simpl. assumption.*) -(*Qed.*) - -(*Lemma stick_header_code_concat_all:*) - (*forall hd lbb hlbb tbb,*) - (*stick_header_code hd lbb = OK hlbb ->*) - (*concat_all lbb = OK tbb ->*) - (*exists htbb,*) - (*concat_all hlbb = OK htbb*) - (*/\ stick_header hd tbb = htbb.*) -(*Proof.*) - (*intros. exists (stick_header hd tbb). split; auto.*) - (*destruct lbb.*) - (*- unfold stick_header_code in H. simpl in H. discriminate.*) - (*- unfold stick_header_code in H. simpl in H. inv H.*) - (*apply stick_header_concat_all. assumption.*) -(*Qed.*) - Program Definition make_bblock_from_basics lb := match lb with | nil => Error (msg "PostpassScheduling.make_bblock_from_basics") @@ -341,79 +59,22 @@ Program Definition schedule_to_bblock (lb: list basic) (oc: option control) : re | Some c => OK {| header := nil; body := lb; exit := Some c |} end. Next Obligation. - unfold Is_true, AB.non_empty_bblockb. - unfold AB.non_empty_exit. rewrite orb_true_r. reflexivity. + unfold Is_true, non_empty_bblockb. + unfold non_empty_exit. rewrite orb_true_r. reflexivity. Qed. Definition do_schedule (bb: bblock) : res bblock := if (Z.eqb (size bb) 1) then OK (bb) - else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end. (* TODO Something here *) - -(* TODO to remove ? *) -(*Definition verify_par_bblock (bb: bblock) : res unit :=*) - (*if (bblock_para_check bb) then OK tt else Error (msg "PostpassScheduling.verify_par_bblock").*) -(*Fixpoint verify_par (lbb: list bblock) :=*) - (*match lbb with*) - (*| nil => OK tt*) - (*| bb :: lbb => do res <- verify_par_bblock bb; verify_par lbb*) - (*end.*) + else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end. Definition verified_schedule (bb : bblock) : res bblock := let nhbb := no_header bb in - (* TODO remove? let bb'' := Peephole.optimize_bblock bb' in *) do nhbb' <- do_schedule nhbb; - (*do tbb <- concat_all lbb;*) let bb' := stick_header (header bb) nhbb' in do sizecheck <- verify_size bb bb'; - do schedcheck <- verify_schedule bb bb'; (* TODO Keep this one *) + do schedcheck <- verify_schedule bb bb'; OK (bb'). -(* Definition verified_schedule_nob (bb : bblock) : res (list bblock) := - let nhbb := no_header bb in - do bb' <- do_schedule nhbb; - do sizecheck <- verify_size nhbb bb'; - do schedcheck <- verify_schedule nhbb bb'; - do res <- stick_header_code (header bb) bb'; - OK res. *) - -(*Lemma verified_schedule_nob_size:*) - (*forall bb lbb, verified_schedule_nob bb = OK lbb -> size bb = size_blocks lbb.*) -(*Proof.*) - (*intros. monadInv H. erewrite <- stick_header_code_size; eauto.*) - (*apply verify_size_size.*) - (*destruct x1; try discriminate. assumption.*) -(*Qed.*) - -(*Lemma verified_schedule_nob_no_header_in_middle:*) - (*forall lbb bb,*) - (*verified_schedule_nob bb = OK lbb ->*) - (*Forall (fun b => header b = nil) (tail lbb).*) -(*Proof.*) - (*intros. monadInv H. eapply stick_header_code_no_header_in_middle; eauto.*) - (*eapply concat_all_no_header_in_middle. eassumption.*) -(*Qed.*) - -(*Lemma verified_schedule_nob_header:*) - (*forall bb tbb lbb,*) - (*verified_schedule_nob bb = OK (tbb :: lbb) ->*) - (*header bb = header tbb*) - (*/\ Forall (fun b => header b = nil) lbb.*) -(*Proof.*) - (*intros. split.*) - (*- monadInv H. unfold stick_header_code in EQ3. destruct (hd_error _); try discriminate. inv EQ3.*) - (*simpl. reflexivity.*) - (*- apply verified_schedule_nob_no_header_in_middle in H. assumption.*) -(*Qed.*) - - -(* Definition verified_schedule (bb : bblock) : res (list bblock) := - verified_schedule_nob bb. *) -(* TODO Remove? - match exit bb with - | Some (PExpand (Pbuiltin ef args res)) => OK (bb::nil) (* Special case for ensuring the lemma verified_schedule_builtin_idem *) - | _ => verified_schedule_nob bb - end.*) - Lemma verified_schedule_size: forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'. Proof. @@ -439,83 +100,17 @@ Proof. rewrite ESIZE. reflexivity. Qed. -(*Lemma verified_schedule_no_header_in_middle:*) - (*forall lbb bb,*) - (*verified_schedule bb = OK lbb ->*) - (*Forall (fun b => header b = nil) (tail lbb).*) -(*Proof.*) - (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) - (*all: try (eapply verified_schedule_nob_no_header_in_middle; eauto; fail).*) - (*inv H. simpl. auto.*) -(*Qed.*) - -(*Lemma verified_schedule_header:*) - (*forall bb tbb lbb,*) - (*verified_schedule bb = OK (tbb :: lbb) ->*) - (*header bb = header tbb*) - (*/\ Forall (fun b => header b = nil) lbb.*) -(*Proof.*) - (*intros. unfold verified_schedule in H. destruct (exit bb). destruct c. destruct i.*) - (*all: try (eapply verified_schedule_nob_header; eauto; fail).*) - (*inv H. split; simpl; auto.*) -(*Qed.*) - - -(*Lemma verified_schedule_nob_correct:*) - (*forall ge f bb lbb,*) - (*verified_schedule_nob bb = OK lbb ->*) - (*exists tbb,*) - (*is_concat tbb lbb*) - (*/\ bblock_simu ge f bb tbb.*) -(*Proof.*) - (*intros. monadInv H.*) - (*exploit stick_header_code_concat_all; eauto.*) - (*intros (tbb & CONC & STH).*) - (*exists tbb. split; auto. constructor; auto.*) - (*rewrite verify_schedule_no_header in EQ2. erewrite stick_header_verify_schedule in EQ2; eauto.*) - (*eapply bblock_simub_correct; eauto. unfold verify_schedule in EQ2.*) - (*destruct (bblock_simub _ _); auto; try discriminate.*) -(*Qed.*) - Theorem verified_schedule_correct: forall ge f bb bb', verified_schedule bb = OK bb' -> bblock_simu lk ge f bb bb'. Proof. -(* intros. - assert (size bb = size bb'). { apply verified_schedule_size. auto. } - unfold verified_schedule in H. monadInv H. + intros. + monadInv H. eapply bblock_simub_correct. - unfold do_schedule in EQ. unfold verify_schedule in EQ0. - - destruct (bblock_simub _ _) in *; try discriminate. - destruct schedule. - simpl. unfold bblock_simub. - - eapply bblock_simub_correct. - destruct (bblock_simub); try discriminate. - - destruct schedule. - unfold bblock_simu, exec_bblock. destruct (exit bb). destruct c. destruct i. - - - intros rs m rs' m' t (rs1 & m1 & EBDY & EXT). - - eexists; eexists; split. - simpl. unfold exec_body. - - all: try (eapply verified_schedule_nob_correct; eauto; fail). - inv H. eexists; eexists; split; simpl; auto. constructor; auto. simpl; auto. constructor; auto. -Qed. *) -Admitted. -(*Lemma verified_schedule_builtin_idem:*) - (*forall bb ef args res lbb,*) - (*exit bb = Some (PExpand (Pbuiltin ef args res)) ->*) - (*verified_schedule bb = OK lbb ->*) - (*lbb = bb :: nil.*) -(*Proof.*) - (*intros. unfold verified_schedule in H0. rewrite H in H0. inv H0. reflexivity.*) -(*Qed.*) + destruct (bblock_simub _ _) in *; try discriminate; auto. +Qed. End verify_schedule. diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml index 463d65b5..9263babc 100644 --- a/aarch64/PostpassSchedulingOracle.ml +++ b/aarch64/PostpassSchedulingOracle.ml @@ -23,6 +23,8 @@ let debug = false * Extracting infos from Asm instructions *) +type instruction = PBasic of basic | PControl of control + type location = Reg of Asm.preg | Mem | IREG0_XZR type ab_inst_rec = { @@ -40,7 +42,9 @@ let arith_p_real = function | Padrp (_, _) -> Adrp | Pmovz (_, _, _) -> Movz | Pmovn (_, _, _) -> Movn - | Pfmovimms _ -> Fmov (* XXX We could also use load, but Fmov may be more convenient for tuning *) + | Pfmovimms _ -> + Fmov + (* XXX We could also use load, but Fmov may be more convenient for tuning *) | Pfmovimmd _ -> Fmov let arith_pp_real = function diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index 22daede9..c32579a2 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -5,6 +5,7 @@ (* Sylvain Boulmé Grenoble-INP, VERIMAG *) (* 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 *) @@ -16,7 +17,7 @@ Require Import Coqlib Errors. Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Machblock Conventions Asmblock. -Require Import Asmblockgenproof0 Asmblockprops. +Require Import Asmblockprops. Require Import PostpassScheduling. Require Import Asmblockgenproof. Require Import Axioms. @@ -32,103 +33,6 @@ Proof. intros. eapply match_transform_partial_program; eauto. Qed. -(* -Lemma regset_double_set_id: - forall r (rs: regset) v1 v2, - (rs # r <- v1 # r <- v2) = (rs # r <- v2). -Proof. - intros. apply functional_extensionality. intros. destruct (preg_eq r x). - - subst r. repeat (rewrite Pregmap.gss; auto). - - repeat (rewrite Pregmap.gso); auto. -Qed. - -Lemma exec_body_pc_var: - forall l ge rs m rs' m' v, - exec_body ge l rs m = Next rs' m' -> - exec_body ge l (rs # PC <- v) m = Next (rs' # PC <- v) m'. -Proof. - induction l. - - intros. simpl. simpl in H. inv H. auto. - - intros. simpl in *. - destruct (exec_basic_instr ge a rs m) eqn:EXEBI; try discriminate. - erewrite exec_basic_instr_pc_var; eauto. -Qed. - -Lemma pc_set_add: - forall rs v r x y, - 0 <= x <= Ptrofs.max_unsigned -> - 0 <= y <= Ptrofs.max_unsigned -> - rs # r <- (Val.offset_ptr v (Ptrofs.repr (x + y))) = rs # r <- (Val.offset_ptr (rs # r <- (Val.offset_ptr v (Ptrofs.repr x)) r) (Ptrofs.repr y)). -Proof. - intros. apply functional_extensionality. intros r0. destruct (preg_eq r r0). - - subst. repeat (rewrite Pregmap.gss); auto. - destruct v; simpl; auto. - rewrite Ptrofs.add_assoc. - enough (Ptrofs.repr (x + y) = Ptrofs.add (Ptrofs.repr x) (Ptrofs.repr y)) as ->; auto. - unfold Ptrofs.add. - enough (x + y = Ptrofs.unsigned (Ptrofs.repr x) + Ptrofs.unsigned (Ptrofs.repr y)) as ->; auto. - repeat (rewrite Ptrofs.unsigned_repr); auto. - - repeat (rewrite Pregmap.gso; auto). -Qed. - -Lemma concat2_straight: - forall a b bb rs m rs'' m'' f ge, - concat2 a b = OK bb -> - exec_bblock ge f bb rs m = Next rs'' m'' -> - exists rs' m', - exec_bblock ge f a rs m = Next rs' m' - /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a)) - /\ exec_bblock ge f b rs' m' = Next rs'' m''. -Proof. - intros until ge. intros CONC2 EXEB. - exploit concat2_zlt_size; eauto. intros (LTA & LTB). - exploit concat2_noexit; eauto. intros EXA. - exploit concat2_decomp; eauto. intros. inv H. - unfold exec_bblock in EXEB. destruct (exec_body ge (body bb) rs m) eqn:EXEB'; try discriminate. - rewrite H0 in EXEB'. apply exec_body_app in EXEB'. destruct EXEB' as (rs1 & m1 & EXEB1 & EXEB2). - eexists; eexists. split. - unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto. - split. - exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto. - unfold exec_bblock. unfold nextblock, incrPC. rewrite regset_same_assign. erewrite exec_body_pc_var; eauto. - rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id. - assert (size bb = size a + size b). - { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r. - repeat (rewrite Nat2Z.inj_add). omega. } - clear EXA H0 H1. rewrite H in EXEB. - assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. } - rewrite H0. rewrite <- pc_set_add; auto. - exploit size_positive. instantiate (1 := a). intro. omega. - exploit size_positive. instantiate (1 := b). intro. omega. -Qed. - -Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) : - forall a bb rs m lbb rs'' m'', - lbb <> nil -> - concat_all (a :: lbb) = OK bb -> - exec_bblock ge f bb rs m = Next rs'' m'' -> - exists bb' rs' m', - concat_all lbb = OK bb' - /\ exec_bblock ge f a rs m = Next rs' m' - /\ rs' PC = Val.offset_ptr (rs PC) (Ptrofs.repr (size a)) - /\ exec_bblock ge f bb' rs' m' = Next rs'' m''. -Proof. - intros until m''. intros Hnonil CONC EXEB. - simpl in CONC. - destruct lbb as [|b lbb]; try contradiction. clear Hnonil. - monadInv CONC. exploit concat2_straight; eauto. intros (rs' & m' & EXEB1 & PCeq & EXEB2). - exists x. repeat econstructor. all: eauto. -Qed. - -Lemma ptrofs_add_repr : - forall a b, - Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr a) (Ptrofs.repr b)) = Ptrofs.unsigned (Ptrofs.repr (a + b)). -Proof. - intros a b. - rewrite Ptrofs.add_unsigned. repeat (rewrite Ptrofs.unsigned_repr_eq). - rewrite <- Zplus_mod. auto. -Qed. -*) Section PRESERVATION_ASMBLOCK. Variables prog tprog: program. @@ -136,15 +40,7 @@ Variable lk: aarch64_linker. Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. -(* -Lemma transf_function_no_overflow: - forall f tf, - transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned. -Proof. - intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. - omega. -Qed. -*) + Lemma symbols_preserved: forall id, Genv.find_symbol tge id = Genv.find_symbol ge id. @@ -153,31 +49,14 @@ Proof (Genv.find_symbol_match TRANSL). Lemma senv_preserved: Senv.equiv ge tge. Proof (Genv.senv_match TRANSL). -(* -Lemma functions_translated: - forall v f, - Genv.find_funct ge v = Some f -> - exists tf, - Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial TRANSL). -*) + Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. Proof (Genv.find_funct_ptr_transf_partial TRANSL). -(* -Lemma functions_transl: - forall fb f tf, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - transf_function f = OK tf -> - Genv.find_funct_ptr tge fb = Some (Internal tf). -Proof. - intros. exploit function_ptr_translated; eauto. - intros (tf' & A & B). monadInv B. rewrite H0 in EQ. inv EQ. auto. -Qed. -*) + Inductive match_states: state -> state -> Prop := | match_states_intro: forall s1 s2, s1 = s2 -> match_states s1 s2. @@ -212,48 +91,6 @@ Proof. intros. inv H0. inv H. econstructor; eauto. Qed. -(* Lemma tail_find_bblock: - forall lbb pos bb, - find_bblock pos lbb = Some bb -> - exists c, code_tail pos lbb (bb::c). -Proof. - induction lbb. - - intros. simpl in H. inv H. - - intros. simpl in H. - destruct (zlt pos 0); try (inv H; fail). - destruct (zeq pos 0). - + inv H. exists lbb. constructor; auto. - + apply IHlbb in H. destruct H as (c & TAIL). exists c. - enough (pos = pos - size a + size a) as ->. - apply code_tail_S; auto. - omega. -Qed. *) - -(* Lemma code_tail_head_app: - forall l pos c1 c2, - code_tail pos c1 c2 -> - code_tail (pos + size_blocks l) (l++c1) c2. -Proof. - induction l. - - intros. simpl. rewrite Z.add_0_r. auto. - - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption. -Qed. *) - -(* Lemma transf_blocks_verified: - forall c tc pos bb c', - transf_blocks c = OK tc -> - code_tail pos c (bb::c') -> - exists lbb, - verified_schedule bb = OK lbb. -Proof. - induction c; intros. - - simpl in H. inv H. inv H0. - - inv H0. - + monadInv H. exists x0; eauto. - + unfold transf_blocks in H. fold transf_blocks in H. monadInv H. - exploit IHc; eauto. -Qed. *) - Lemma transf_find_bblock: forall ofs f bb tf, find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb -> @@ -269,97 +106,43 @@ Proof. induction (fn_blocks f). - intros. simpl in *. discriminate. - intros. simpl in *. - monadInv EQ0. simpl. - destruct (zlt z 0); try discriminate. - destruct (zeq z 0). - + inv H. eauto. - + monadInv EQ0. - exploit IHb; eauto. - intros (tbb & SCH & FIND). - eexists; split; eauto. - inv FIND. - unfold verify_size in EQ0. - destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate. - rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE. - reflexivity. -Qed. - -Lemma transf_exec_bblock: - forall f tf bb ofs t rs m rs' m', - find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb -> - transf_function f = OK tf -> - exec_bblock lk ge f bb rs m t rs' m' -> - exists tbb, - exec_bblock lk tge tf tbb rs m t rs' m' - /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb. + monadInv EQ0. simpl. + destruct (zlt z 0); try discriminate. + destruct (zeq z 0). + + inv H. eauto. + + monadInv EQ0. + exploit IHb; eauto. + intros (tbb & SCH & FIND). + eexists; split; eauto. + inv FIND. + unfold verify_size in EQ0. + destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate. + rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE. + reflexivity. +Qed. + +Lemma stick_header_neutral: forall a, + a = (stick_header (header a) (no_header a)). Proof. - intros. inv H1. - monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x0))); try (inv EQ0; fail). inv EQ0. - monadInv EQ. simpl in *. - generalize (Ptrofs.unsigned ofs) H x0 g EQ0; clear ofs H x0 g EQ0. - induction (fn_blocks f). - - intros. simpl in *. discriminate. - - intros. simpl in *. - monadInv EQ0. simpl. - destruct (zlt z 0); try discriminate. - destruct (zeq z 0). - + inv H. -Admitted. + intros. + unfold stick_header. unfold Asmblock.stick_header_obligation_1. simpl. destruct a. + simpl. reflexivity. +Qed. Lemma symbol_address_preserved: forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs. Proof. intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity. Qed. -(* -Lemma head_tail {A: Type}: - forall (l: list A) hd, hd::l = hd :: (tail (hd::l)). -Proof. - intros. simpl. auto. -Qed. - -Lemma verified_schedule_not_empty: - forall bb lbb, - verified_schedule bb = OK lbb -> lbb <> nil. -Proof. - intros. apply verified_schedule_size in H. - pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g. - destruct lbb; simpl in *; discriminate. -Qed. - -Lemma header_nil_label_pos_none: - forall lbb l p, - Forall (fun b => header b = nil) lbb -> label_pos l p lbb = None. -Proof. - induction lbb. - - intros. simpl. auto. - - intros. inv H. simpl. unfold is_label. rewrite H2. destruct (in_dec l nil). { inv i. } - auto. -Qed. Lemma verified_schedule_label: - forall bb tbb lbb l, - verified_schedule bb = OK (tbb :: lbb) -> - is_label l bb = is_label l tbb - /\ label_pos l 0 lbb = None. -Proof. - intros. exploit verified_schedule_header; eauto. - intros (HdrEq & HdrNil). - split. - - unfold is_label. rewrite HdrEq. reflexivity. - - apply header_nil_label_pos_none. assumption. -Qed. - -Lemma label_pos_app_none: - forall c c' l p p', - label_pos l p c = None -> - label_pos l (p' + size_blocks c) c' = label_pos l p' (c ++ c'). + forall bb tbb l, + verified_schedule bb = OK (tbb) -> + is_label l bb = is_label l tbb. Proof. - induction c. - - intros. simpl in *. rewrite Z.add_0_r. reflexivity. - - intros. simpl in *. destruct (is_label _ _) eqn:ISLABEL. - + discriminate. - + eapply IHc in H. rewrite Z.add_assoc. eauto. + intros. + unfold is_label. + monadInv H. simpl. auto. Qed. Remark label_pos_pvar_none_add: @@ -422,20 +205,18 @@ Proof. eapply label_pos_pvar_add; eauto. Qed. -Lemma label_pos_head_app: - forall c bb lbb l tc p, - verified_schedule bb = OK lbb -> +Lemma label_pos_head_cons: + forall c bb tbb l tc p, + verified_schedule bb = OK tbb -> label_pos l p c = label_pos l p tc -> - label_pos l p (bb :: c) = label_pos l p (lbb ++ tc). + label_pos l p (bb :: c) = label_pos l p (tbb :: tc). Proof. - intros. simpl. destruct lbb as [|tbb lbb]. - - apply verified_schedule_not_empty in H. contradiction. - - simpl. exploit verified_schedule_label; eauto. intros (ISLBL & LBLPOS). - rewrite ISLBL. - destruct (is_label l tbb) eqn:ISLBL'; simpl; auto. - eapply label_pos_pvar in H0. erewrite H0. - erewrite verified_schedule_size; eauto. simpl size_blocks. rewrite Z.add_assoc. - erewrite label_pos_app_none; eauto. + intros. simpl. + exploit verified_schedule_label; eauto. intros ISLBL. + rewrite ISLBL. + destruct (is_label l tbb) eqn:ISLBL'; simpl; auto. + eapply label_pos_pvar in H0. erewrite H0. + erewrite verified_schedule_size; eauto. Qed. Lemma label_pos_preserved: @@ -444,8 +225,8 @@ Lemma label_pos_preserved: Proof. induction c. - intros. simpl in *. inv H. reflexivity. - - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ. - eapply label_pos_head_app; eauto. + - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. + eapply IHc in EQ. eapply label_pos_head_cons; eauto. Qed. Lemma label_pos_preserved_blocks: @@ -458,38 +239,6 @@ Proof. monadInv EQ0. simpl. eapply label_pos_preserved; eauto. Qed. -Lemma transf_exec_exit: - forall f sz cfi t rs m rs' m', - (exec_cfi ge f cfi (incrPC sz rs) m = Next rs' m') -> - exec_exit ge f sz rs m (Some (PCtlFlow cfi)) t rs' m'. -Proof. - intros. - destruct t. - - constructor; auto. - - congruence. - destruct ex; try destruct c; simpl. - - generalize cfi_step. intros. apply H0. - - monadInv H. monadInv EQ. - destruct (zlt Ptrofs.max_unsigned _); try discriminate. - monadInv EQ0. simpl. - assert (ge = Genv.globalenv prog). auto. - assert (tge = Genv.globalenv tprog). auto. - pose symbol_address_preserved. - - - exists rs; exists m. apply cfi_step. inv H. - destruct cfi; simpl; eauto. - assert (ge = Genv.globalenv prog); auto; - assert (tge = Genv.globalenv tprog); auto; - pose symbol_address_preserved; simpl. - - - constructor. - unfold exec_exit. - exploreInst; simpl; auto; try congruence; - unfold par_goto_label; unfold par_eval_branch; unfold par_goto_label; erewrite label_pos_preserved_blocks; eauto. -Qed. -*) Lemma transf_exec_basic: forall i rs m, exec_basic lk ge i rs m = exec_basic lk tge i rs m. Proof. @@ -507,55 +256,59 @@ Proof. destruct (exec_basic _ _ _); auto. Qed. -(* Lemma transf_exec_bblock: - forall f tf bb b ofs t rs m rs' m', - rs PC = Vptr b ofs -> +Lemma transf_exec_cfi: forall f tf cfi rs m, transf_function f = OK tf -> - exec_bblock lk ge f bb rs m t rs' m' -> exec_bblock lk tge tf bb rs m t rs' m'. -Proof. - intros. monadInv H. monadInv EQ. pose symbol_address_preserved. - simpl in *. - destruct (zlt Ptrofs.max_unsigned (size_blocks x0)); try discriminate. - monadInv EQ0. unfold transf_blocks in *. destruct f. simpl in *. - generalize H0 EQ1; clear H0 EQ1. - induction (fn_blocks). - - intros. monadInv EQ1. auto. admit. - - intros. apply IHb. -Qed. *) -(* -Lemma transf_step_simu: - forall f b bb ofs c rs m t rs' m' rs1 m1, - Genv.find_funct_ptr tge b = Some (Internal tf) -> - (* size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned -> *) - rs PC = Vptr b ofs -> - exec_body lk ge (body bi) rs m = Next rs1 m1 -> - exec_exit ge f (Ptrofs.repr (size bb)) rs1 m1 (exit bb) t rs' m' -> - plus (step lk) tge (State rs m) t (State rs' m'). -Proof. - induction bb'. - - intros until m'. simpl. intros. discriminate. - - intros until m'. intros GFIND SIZE PCeq TAIL CONC EXEB. - destruct lbb. - + simpl in *. clear IHlbb. inv CONC. eapply plus_one. econstructor; eauto. eapply find_bblock_tail; eauto. - + exploit concat_all_exec_bblock; eauto; try discriminate. - intros (tbb0 & rs0 & m0 & CONC0 & EXEB0 & PCeq' & EXEB1). - eapply plus_left. - econstructor. - 3: eapply find_bblock_tail. rewrite <- app_comm_cons in TAIL. 3: eauto. - all: eauto. - eapply plus_star. eapply IHlbb; eauto. rewrite PCeq in PCeq'. simpl in PCeq'. all: eauto. - eapply code_tail_next_int; eauto. -Qed. -*) + exec_cfi ge f cfi rs m = exec_cfi tge tf cfi rs m. +Proof. + intros. destruct cfi; simpl; auto; + assert (ge = Genv.globalenv prog); auto; + assert (tge = Genv.globalenv tprog); auto; + pose symbol_address_preserved. + all: try unfold eval_branch; try unfold eval_neg_branch; try unfold goto_label; + try erewrite label_pos_preserved_blocks; try rewrite e; eauto. + destruct (rs # X16 <- Vundef r1); auto. + destruct (list_nth_z tbl (Int.unsigned i)); auto. + erewrite label_pos_preserved_blocks; eauto. +Qed. + +Lemma transf_exec_exit: + forall f tf sz ex t rs m rs' m', + transf_function f = OK tf -> + exec_exit ge f sz rs m ex t rs' m' -> + exec_exit tge tf sz rs m ex t rs' m'. +Proof. + intros. induction H0. + - econstructor. + - econstructor. erewrite <- transf_exec_cfi; eauto. + - econstructor; eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. +Qed. + +Lemma transf_exec_bblock: + forall f tf bb t rs m rs' m', + transf_function f = OK tf -> + exec_bblock lk ge f bb rs m t rs' m' -> + exec_bblock lk tge tf bb rs m t rs' m'. +Proof. + intros. + destruct H0 as [rs1[m1[BDY EXIT]]]. + unfold exec_bblock. + eexists; eexists; split. + rewrite <- transf_exec_body; eauto. + eapply transf_exec_exit; eauto. +Qed. + Theorem transf_step_correct: forall s1 t s2, step lk ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), (exists s2', step lk tge s1' t s2' /\ match_states s2 s2'). Proof. induction 1; intros; inv MS. - - inversion H2. - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. - exploit transf_exec_bblock; eauto. intros (lbb & EBB & FIND). + - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. + exploit transf_find_bblock; eauto. intros (tbb & VES & FIND). + exploit verified_schedule_correct; eauto. intros EBB. + eapply transf_exec_bblock in EBB; eauto. exists (State rs' m'). split; try (econstructor; eauto). - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF. @@ -576,9 +329,9 @@ Qed. End PRESERVATION_ASMBLOCK. +(* Require Import Asm. -(* Lemma verified_par_checks_alls_bundles lb x: forall bundle, verify_par lb = OK x -> List.In bundle lb -> verify_par_bblock bundle = OK tt. @@ -845,7 +845,7 @@ if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling cat >> Makefile.config <<EOF ARCHDIRS=$arch kvx/lib kvx/abstractbb kvx/abstractbb/Impure BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v\\ - Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asm.v Asmblockprops.v\\ + Asmblock.v Asmblockgen.v Asmblockgenproof.v Asm.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v\\ AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\ |