From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asm.v | 26 +-- arm/Asmgen.v | 102 ++++++----- arm/Asmgenproof.v | 161 +++++++++------- arm/Asmgenproof1.v | 473 +++++++++++++++++++++++++++++++----------------- arm/Asmgenretaddr.v | 32 +++- arm/ConstpropOpproof.v | 111 ++++++------ arm/Op.v | 322 ++++++++++++++++++++++---------- arm/PrintAsm.ml | 31 ++-- arm/SelectOp.v | 2 +- arm/SelectOpproof.v | 85 ++++----- arm/linux/Stacklayout.v | 88 +++++++-- 11 files changed, 913 insertions(+), 520 deletions(-) (limited to 'arm') diff --git a/arm/Asm.v b/arm/Asm.v index 7ea1a8a3..051b7e47 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -165,8 +165,8 @@ Inductive instruction : Type := | Psufd: freg -> freg -> freg -> instruction (**r float subtraction *) (* Pseudo-instructions *) - | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *) - | Pfreeframe: Z -> Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) + | Pallocframe: Z -> int -> instruction (**r allocate new stack frame *) + | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) @@ -186,20 +186,20 @@ lbl: .word symbol >> Initialized data in the constant data section are not modeled here, which is why we use a pseudo-instruction for this purpose. -- [Pallocframe lo hi pos]: in the formal semantics, this pseudo-instruction - allocates a memory block with bounds [lo] and [hi], stores the value +- [Pallocframe sz pos]: in the formal semantics, this pseudo-instruction + allocates a memory block with bounds [0] and [sz], stores the value of the stack pointer at offset [pos] in this block, and sets the stack pointer to the address of the bottom of this block. In the printed ASM assembly code, this allocation is: << mov r12, sp - sub sp, sp, #(hi - lo) + sub sp, sp, #sz str r12, [sp, #pos] >> This cannot be expressed in our memory model, which does not reflect the fact that stack frames are adjacent and allocated/freed following a stack discipline. -- [Pfreeframe pos]: in the formal semantics, this pseudo-instruction +- [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction reads the word at [pos] of the block pointed by the stack pointer, frees this block, and sets the stack pointer to the value read. In the printed ASM assembly code, this freeing @@ -494,20 +494,20 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Psufd r1 r2 r3 => OK (nextinstr (rs#r1 <- (Val.subf rs#r2 rs#r3))) m (* Pseudo-instructions *) - | Pallocframe lo hi pos => - let (m1, stk) := Mem.alloc m lo hi in - let sp := (Vptr stk (Int.repr lo)) in + | Pallocframe sz pos => + let (m1, stk) := Mem.alloc m 0 sz in + let sp := (Vptr stk Int.zero) in match Mem.storev Mint32 m1 (Val.add sp (Vint pos)) rs#IR13 with | None => Error - | Some m2 => OK (nextinstr (rs#IR13 <- sp)) m2 + | Some m2 => OK (nextinstr (rs #IR12 <- (rs#IR13) #IR13 <- sp)) m2 end - | Pfreeframe lo hi pos => + | Pfreeframe sz pos => match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with | None => Error | Some v => match rs#IR13 with | Vptr stk ofs => - match Mem.free m stk lo hi with + match Mem.free m stk 0 sz with | None => Error | Some m' => OK (nextinstr (rs#IR13 <- v)) m' end @@ -521,7 +521,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pbtbl r tbl => match rs#r with | Vint n => - let pos := Int.signed n in + let pos := Int.unsigned n in if zeq (Zmod pos 4) 0 then match list_nth_z tbl (pos / 4) with | None => Error diff --git a/arm/Asmgen.v b/arm/Asmgen.v index b3412fbf..a1f8d960 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -36,7 +36,7 @@ Require Import Asm. Fixpoint is_immed_arith_aux (n: nat) (x msk: int) {struct n}: bool := match n with - | O => false + | Datatypes.O => false | Datatypes.S n' => Int.eq (Int.and x (Int.not msk)) Int.zero || is_immed_arith_aux n' x (Int.ror msk (Int.repr 2)) @@ -55,46 +55,65 @@ Definition is_immed_mem_float (x: int) : bool := Int.eq (Int.and x (Int.repr 3)) Int.zero && Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x. +(** Decomposition of a 32-bit integer into a list of immediate arguments, + whose sum or "or" or "xor" equals the integer. *) + +Fixpoint decompose_int_rec (N: nat) (n p: int) : list int := + match N with + | Datatypes.O => + if Int.eq_dec n Int.zero then nil else n :: nil + | Datatypes.S M => + if Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then + decompose_int_rec M n (Int.add p (Int.repr 2)) + else + let m := Int.shl (Int.repr 255) p in + Int.and n m :: + decompose_int_rec M (Int.and n (Int.not m)) (Int.add p (Int.repr 2)) + end. + +Definition decompose_int (n: int) : list int := + match decompose_int_rec 12%nat n Int.zero with + | nil => Int.zero :: nil + | l => l + end. + +Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code) := + match l with + | nil => + op1 (SOimm Int.zero) :: k (**r should never happen *) + | i :: l' => + op1 (SOimm i) :: map (fun i => op2 (SOimm i)) l' ++ k + end. + (** Smart constructors for integer immediate arguments. *) Definition loadimm (r: ireg) (n: int) (k: code) := - if is_immed_arith n then - Pmov r (SOimm n) :: k - else if is_immed_arith (Int.not n) then - Pmvn r (SOimm (Int.not n)) :: k - else (* could be much improved! *) - Pmov r (SOimm (Int.and n (Int.repr 255))) :: - Porr r r (SOimm (Int.and n (Int.repr 65280))) :: - Porr r r (SOimm (Int.and n (Int.repr 16711680))) :: - Porr r r (SOimm (Int.and n (Int.repr 4278190080))) :: - k. + let d1 := decompose_int n in + let d2 := decompose_int (Int.not n) in + if le_dec (List.length d1) (List.length d2) + then iterate_op (Pmov r) (Porr r r) d1 k + else iterate_op (Pmvn r) (Pbic r r) d2 k. Definition addimm (r1 r2: ireg) (n: int) (k: code) := - if is_immed_arith n then - Padd r1 r2 (SOimm n) :: k - else if is_immed_arith (Int.neg n) then - Psub r1 r2 (SOimm (Int.neg n)) :: k - else - Padd r1 r2 (SOimm (Int.and n (Int.repr 255))) :: - Padd r1 r1 (SOimm (Int.and n (Int.repr 65280))) :: - Padd r1 r1 (SOimm (Int.and n (Int.repr 16711680))) :: - Padd r1 r1 (SOimm (Int.and n (Int.repr 4278190080))) :: - k. + let d1 := decompose_int n in + let d2 := decompose_int (Int.neg n) in + if le_dec (List.length d1) (List.length d2) + then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k + else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k. Definition andimm (r1 r2: ireg) (n: int) (k: code) := - if is_immed_arith n then - Pand r1 r2 (SOimm n) :: k - else if is_immed_arith (Int.not n) then - Pbic r1 r2 (SOimm (Int.not n)) :: k - else - loadimm IR14 n (Pand r1 r2 (SOreg IR14) :: k). + if is_immed_arith n + then Pand r1 r2 (SOimm n) :: k + else iterate_op (Pbic r1 r2) (Pbic r1 r1) (decompose_int (Int.not n)) k. -Definition makeimm (instr: ireg -> ireg -> shift_op -> instruction) - (r1 r2: ireg) (n: int) (k: code) := - if is_immed_arith n then - instr r1 r2 (SOimm n) :: k - else - loadimm IR14 n (instr r1 r2 (SOreg IR14) :: k). +Definition rsubimm (r1 r2: ireg) (n: int) (k: code) := + iterate_op (Prsb r1 r2) (Padd r1 r1) (decompose_int n) k. + +Definition orimm (r1 r2: ireg) (n: int) (k: code) := + iterate_op (Porr r1 r2) (Porr r1 r1) (decompose_int n) k. + +Definition xorimm (r1 r2: ireg) (n: int) (k: code) := + iterate_op (Peor r1 r2) (Peor r1 r1) (decompose_int n) k. (** Translation of a shift immediate operation (type [Op.shift]) *) @@ -235,7 +254,7 @@ Definition transl_op | Orsubshift s, a1 :: a2 :: nil => Prsb (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k | Orsubimm n, a1 :: nil => - makeimm Prsb (ireg_of r) (ireg_of a1) n k + rsubimm (ireg_of r) (ireg_of a1) n k | Omul, a1 :: a2 :: nil => if ireg_eq (ireg_of r) (ireg_of a1) || ireg_eq (ireg_of r) (ireg_of a2) @@ -256,13 +275,13 @@ Definition transl_op | Oorshift s, a1 :: a2 :: nil => Porr (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k | Oorimm n, a1 :: nil => - makeimm Porr (ireg_of r) (ireg_of a1) n k + orimm (ireg_of r) (ireg_of a1) n k | Oxor, a1 :: a2 :: nil => Peor (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k | Oxorshift s, a1 :: a2 :: nil => Peor (ireg_of r) (ireg_of a1) (transl_shift s (ireg_of a2)) :: k | Oxorimm n, a1 :: nil => - makeimm Peor (ireg_of r) (ireg_of a1) n k + xorimm (ireg_of r) (ireg_of a1) n k | Obic, a1 :: a2 :: nil => Pbic (ireg_of r) (ireg_of a1) (SOreg (ireg_of a2)) :: k | Obicshift s, a1 :: a2 :: nil => @@ -469,12 +488,10 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pblsymb symb :: k | Mtailcall sig (inl r) => loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) - :: Pbreg (ireg_of r) :: k) + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg (ireg_of r) :: k) | Mtailcall sig (inr symb) => loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) - :: Pbsymb symb :: k) + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb :: k) | Mbuiltin ef args res => Pbuiltin ef (map preg_of args) (preg_of res) :: k | Mlabel lbl => @@ -488,8 +505,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pbtbl IR14 tbl :: k | Mreturn => loadind_int IR13 f.(fn_retaddr_ofs) IR14 - (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) - :: Pbreg IR14 :: k) + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: k) end. Definition transl_code (f: Mach.function) (il: list Mach.instruction) := @@ -501,7 +517,7 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) := around, leading to incorrect executions. *) Definition transl_function (f: Mach.function) := - Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: + Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: Pstr IR14 IR13 (SAimm f.(fn_retaddr_ofs)) :: transl_code f f.(fn_code). diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index d3e082f0..0a429cca 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -330,12 +330,26 @@ Section TRANSL_LABEL. Variable lbl: label. +Remark iterate_op_label: + forall op1 op2 l k, + (forall so, is_label lbl (op1 so) = false) -> + (forall so, is_label lbl (op2 so) = false) -> + find_label lbl (iterate_op op1 op2 l k) = find_label lbl k. +Proof. + intros. unfold iterate_op. + destruct l as [ | hd tl]. + simpl. rewrite H. auto. + simpl. rewrite H. + induction tl; simpl. auto. rewrite H0; auto. +Qed. +Hint Resolve iterate_op_label: labels. + Remark loadimm_label: forall r n k, find_label lbl (loadimm r n k) = find_label lbl k. Proof. - intros. unfold loadimm. - destruct (is_immed_arith n). reflexivity. - destruct (is_immed_arith (Int.not n)); reflexivity. + intros. unfold loadimm. + destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n)))); + auto with labels. Qed. Hint Rewrite loadimm_label: labels. @@ -343,9 +357,8 @@ Remark addimm_label: forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k. Proof. intros; unfold addimm. - destruct (is_immed_arith n). reflexivity. - destruct (is_immed_arith (Int.neg n)). reflexivity. - autorewrite with labels. reflexivity. + destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n)))); + auto with labels. Qed. Hint Rewrite addimm_label: labels. @@ -353,31 +366,30 @@ Remark andimm_label: forall r1 r2 n k, find_label lbl (andimm r1 r2 n k) = find_label lbl k. Proof. intros; unfold andimm. - destruct (is_immed_arith n). reflexivity. - destruct (is_immed_arith (Int.not n)). reflexivity. - autorewrite with labels. reflexivity. + destruct (is_immed_arith n). reflexivity. auto with labels. Qed. Hint Rewrite andimm_label: labels. -Remark makeimm_Prsb_label: - forall r1 r2 n k, find_label lbl (makeimm Prsb r1 r2 n k) = find_label lbl k. +Remark rsubimm_label: + forall r1 r2 n k, find_label lbl (rsubimm r1 r2 n k) = find_label lbl k. Proof. - intros; unfold makeimm. - destruct (is_immed_arith n). reflexivity. autorewrite with labels; auto. + intros; unfold rsubimm. auto with labels. Qed. -Remark makeimm_Porr_label: - forall r1 r2 n k, find_label lbl (makeimm Porr r1 r2 n k) = find_label lbl k. +Hint Rewrite rsubimm_label: labels. + +Remark orimm_label: + forall r1 r2 n k, find_label lbl (orimm r1 r2 n k) = find_label lbl k. Proof. - intros; unfold makeimm. - destruct (is_immed_arith n). reflexivity. autorewrite with labels; auto. + intros; unfold orimm. auto with labels. Qed. -Remark makeimm_Peor_label: - forall r1 r2 n k, find_label lbl (makeimm Peor r1 r2 n k) = find_label lbl k. +Hint Rewrite orimm_label: labels. + +Remark xorimm_label: + forall r1 r2 n k, find_label lbl (xorimm r1 r2 n k) = find_label lbl k. Proof. - intros; unfold makeimm. - destruct (is_immed_arith n). reflexivity. autorewrite with labels; auto. + intros; unfold xorimm. auto with labels. Qed. -Hint Rewrite makeimm_Prsb_label makeimm_Porr_label makeimm_Peor_label: labels. +Hint Rewrite xorimm_label: labels. Remark loadind_int_label: forall base ofs dst k, find_label lbl (loadind_int base ofs dst k) = find_label lbl k. @@ -692,7 +704,7 @@ Proof. rewrite (sp_val _ _ _ AG) in A. exploit loadind_correct. eexact A. reflexivity. intros [rs2 [EX [RES OTH]]]. - left; eapply exec_straight_steps; eauto with coqlib. + left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. exists m'; split; auto. simpl. exists rs2; split. eauto. apply agree_set_mreg with rs; auto. congruence. auto with ppcgen. @@ -715,19 +727,19 @@ Proof. rewrite (sp_val _ _ _ AG) in B. exploit storeind_correct. eexact B. reflexivity. congruence. intros [rs2 [EX OTH]]. - left; eapply exec_straight_steps; eauto with coqlib. + left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. exists m2; split; auto. - exists rs2; split; eauto. + simpl. exists rs2; split. eauto. apply agree_exten with rs; auto with ppcgen. Qed. Lemma exec_Mgetparam_prop: - forall (s : list stackframe) (fb : block) (f: Mach.function) (sp parent : val) + forall (s : list stackframe) (fb : block) (f: Mach.function) (sp : val) (ofs : int) (ty : typ) (dst : mreg) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (v : val), Genv.find_funct_ptr ge fb = Some (Internal f) -> - load_stack m sp Tint f.(fn_link_ofs) = Some parent -> - load_stack m parent ty ofs = Some v -> + load_stack m sp Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (parent_sp s) ty ofs = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mgetparam ofs ty dst :: c) ms m) E0 (Machconcr.State s fb sp c (Regmap.set dst v (Regmap.set IT1 Vundef ms)) m). Proof. @@ -738,18 +750,18 @@ Proof. unfold load_stack in *. exploit Mem.loadv_extends. eauto. eexact H0. eauto. intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. - assert (parent' = parent). inv B. auto. simpl in H1; discriminate. subst parent'. + assert (parent' = parent_sp s). inv B. auto. rewrite <- H3 in H1; discriminate. subst parent'. exploit Mem.loadv_extends. eauto. eexact H1. eauto. intros [v' [C D]]. exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_link_ofs) IR14 - rs m' parent (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))). + rs m' (parent_sp s) (loadind IR14 ofs (mreg_type dst) dst (transl_code f c))). auto. intros [rs1 [EX1 [RES1 OTH1]]]. exploit (loadind_correct tge (transl_function f) IR14 ofs (mreg_type dst) dst (transl_code f c) rs1 m' v'). rewrite RES1. auto. auto. intros [rs2 [EX2 [RES2 OTH2]]]. - left. eapply exec_straight_steps; eauto with coqlib. + left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. exists m'; split; auto. exists rs2; split; simpl. eapply exec_straight_trans; eauto. @@ -762,20 +774,20 @@ Lemma exec_Mop_prop: forall (s : list stackframe) (fb : block) (sp : val) (op : operation) (args : list mreg) (res : mreg) (c : list Mach.instruction) (ms : mreg -> val) (m : mem) (v : val), - eval_operation ge sp op ms ## args = Some v -> + eval_operation ge sp op ms ## args m = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0 (Machconcr.State s fb sp c (Regmap.set res v (undef_op op ms)) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. - exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. intros [v' [A B]]. - assert (C: eval_operation tge sp op rs ## (preg_of ## args) = Some v'). + assert (C: eval_operation tge sp op rs ## (preg_of ## args) m' = Some v'). rewrite <- A. apply eval_operation_preserved. exact symbols_preserved. rewrite (sp_val _ _ _ AG) in C. exploit transl_op_correct; eauto. intros [rs' [P [Q R]]]. - left; eapply exec_straight_steps; eauto with coqlib. + left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. exists m'; split; auto. exists rs'; split. simpl. eexact P. assert (agree (Regmap.set res v ms) sp rs'). @@ -809,7 +821,8 @@ Proof. eauto; intros; reflexivity. Qed. -Lemma storev_8_signed_unsigned: forall m a v, Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_8. Qed. Lemma storev_16_signed_unsigned: forall m a v, Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_16. Qed. +Lemma storev_8_signed_unsigned: forall m a v, Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. Proof. intros. unfold Mem.storev. + destruct a; auto. apply Mem.store_signed_unsigned_8. Qed. Lemma storev_16_signed_unsigned: forall m a v, Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. Proof. intros. unfold Mem.storev. destruct a; auto. apply Mem.store_signed_unsigned_16. Qed. Lemma exec_Mstore_prop: forall (s : list stackframe) (fb : block) (sp : val) @@ -826,7 +839,7 @@ Proof. intro WTI; inv WTI. assert (eval_addressing tge sp addr ms##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. - left; eapply exec_straight_steps; eauto with coqlib. + left; eapply exec_straight_steps. auto. eauto. auto. eauto with coqlib. eauto. eauto. destruct chunk; simpl; simpl in H6; try (rewrite storev_8_signed_unsigned in H0); try (rewrite storev_16_signed_unsigned in H0); @@ -896,8 +909,19 @@ Proof. intros. rewrite Pregmap.gso; auto with ppcgen. Qed. - -Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m', find_function_ptr ge ros ms = Some f' -> Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 (Callstate s f' ms m'). Proof. +Lemma exec_Mtailcall_prop: + forall (s : list stackframe) (fb stk : block) (soff : int) + (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) + (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m', + find_function_ptr ge ros ms = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + exec_instr_prop + (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 + (Callstate s f' ms m'). +Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). @@ -906,7 +930,7 @@ Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff match ros with inl r => Pbreg (ireg_of r) | inr symb => Pbsymb symb end). assert (TR: transl_code f (Mtailcall sig ros :: c) = loadind_int IR13 (fn_retaddr_ofs f) IR14 - (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)). + (Pfreeframe f.(fn_stacksize) (fn_link_ofs f) :: call_instr :: transl_code f c)). unfold call_instr; destruct ros; auto. unfold load_stack in *. exploit Mem.loadv_extends. eauto. eexact H1. auto. @@ -918,7 +942,7 @@ Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. destruct (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14 rs m'0 (parent_ra s) - (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c)) + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: call_instr :: transl_code f c)) as [rs1 [EXEC1 [RES1 OTH1]]]. rewrite <- (sp_val ms (Vptr stk soff) rs); auto. set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))). @@ -1021,7 +1045,7 @@ Lemma exec_Mcond_true_prop: (cond : condition) (args : list mreg) (lbl : Mach.label) (c : list Mach.instruction) (ms : mreg -> val) (m : mem) (c' : Mach.code), - eval_condition cond ms ## args = Some true -> + eval_condition cond ms ## args m = Some true -> Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 @@ -1030,7 +1054,8 @@ Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inv WTI. - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. + intros A. exploit transl_cond_correct. eauto. eauto. intros [rs2 [EX [RES OTH]]]. inv AT. simpl in H5. @@ -1057,14 +1082,15 @@ Lemma exec_Mcond_false_prop: forall (s : list stackframe) (fb : block) (sp : val) (cond : condition) (args : list mreg) (lbl : Mach.label) (c : list Mach.instruction) (ms : mreg -> val) (m : mem), - eval_condition cond ms ## args = Some false -> + eval_condition cond ms ## args m = Some false -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 (Machconcr.State s fb sp c (undef_temps ms) m). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inv WTI. - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. intros A. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. + intros A. exploit transl_cond_correct. eauto. eauto. intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. @@ -1081,7 +1107,7 @@ Lemma exec_Mjumptable_prop: (ms : mreg -> val) (m : mem) (n : int) (lbl : Mach.label) (c' : Mach.code), ms arg = Vint n -> - list_nth_z tbl (Int.signed n) = Some lbl -> + list_nth_z tbl (Int.unsigned n) = Some lbl -> Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop @@ -1093,11 +1119,10 @@ Proof. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inv WTI. exploit list_nth_z_range; eauto. intro RANGE. - assert (SHIFT: Int.signed (Int.shl n (Int.repr 2)) = Int.signed n * 4). + assert (SHIFT: Int.unsigned (Int.shl n (Int.repr 2)) = Int.unsigned n * 4). rewrite Int.shl_mul. - rewrite Int.mul_signed. - apply Int.signed_repr. - split. apply Zle_trans with 0. vm_compute; congruence. omega. + unfold Int.mul. + apply Int.unsigned_repr. omega. inv AT. simpl in H7. set (k1 := Pbtbl IR14 tbl :: transl_code f c). @@ -1122,9 +1147,8 @@ Proof. eapply find_instr_tail. unfold k1 in CT1. eauto. unfold exec_instr. change (rs1 IR14) with (Vint (Int.shl n (Int.repr 2))). -Opaque Zmod. Opaque Zdiv. - simpl. rewrite SHIFT. rewrite Z_mod_mult. rewrite zeq_true. - rewrite Z_div_mult. + lazy iota beta. rewrite SHIFT. + rewrite Z_mod_mult. rewrite zeq_true. rewrite Z_div_mult. change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq. econstructor; eauto. eapply Mach.find_label_incl; eauto. @@ -1133,7 +1157,16 @@ Opaque Zmod. Opaque Zdiv. apply agree_undef_temps; auto. Qed. -Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m', Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 (Returnstate s ms m'). Proof. +Lemma exec_Mreturn_prop: + forall (s : list stackframe) (fb stk : block) (soff : int) + (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 + (Returnstate s ms m'). +Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. unfold load_stack in *. @@ -1147,13 +1180,13 @@ Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : exploit (loadind_int_correct tge (transl_function f) IR13 f.(fn_retaddr_ofs) IR14 rs m'0 (parent_ra s) - (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)). + (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbreg IR14 :: transl_code f c)). rewrite <- (sp_val ms (Vptr stk soff) rs); auto. intros [rs1 [EXEC1 [RES1 OTH1]]]. set (rs2 := nextinstr (rs1#IR13 <- (parent_sp s))). assert (EXEC2: exec_straight tge (transl_function f) (loadind_int IR13 (fn_retaddr_ofs f) IR14 - (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c)) + (Pfreeframe f.(fn_stacksize) (fn_link_ofs f) :: Pbreg IR14 :: transl_code f c)) rs m'0 (Pbreg IR14 :: transl_code f c) rs2 m2'). eapply exec_straight_trans. eexact EXEC1. apply exec_straight_one. simpl. rewrite OTH1; try congruence. @@ -1188,12 +1221,12 @@ Lemma exec_function_internal_prop: forall (s : list stackframe) (fb : block) (ms : Mach.regset) (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block), Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mem.alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) -> - let sp := Vptr stk (Int.repr (- fn_framesize f)) in + Mem.alloc m 0 (fn_stacksize f) = (m1, stk) -> + let sp := Vptr stk Int.zero in store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 -> store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> exec_instr_prop (Machconcr.Callstate s fb ms m) E0 - (Machconcr.State s fb sp (fn_code f) ms m3). + (Machconcr.State s fb sp (fn_code f) (undef_temps ms) m3). Proof. intros; red; intros; inv MS. assert (WTF: wt_function f). @@ -1201,7 +1234,7 @@ Proof. inversion TY; auto. exploit functions_transl; eauto. intro TFIND. generalize (functions_transl_no_overflow _ _ H); intro NOOV. - set (rs2 := nextinstr (rs#IR13 <- sp)). + set (rs2 := nextinstr (rs#IR12 <- (rs#IR13) #IR13 <- sp)). set (rs3 := nextinstr rs2). exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. intros [m1' [A B]]. @@ -1218,7 +1251,7 @@ Proof. unfold transl_function at 2. apply exec_straight_two with rs2 m2'. unfold exec_instr. rewrite A. fold sp. - rewrite <- (sp_val ms (parent_sp s) rs); auto. rewrite C. auto. + rewrite (sp_val ms (parent_sp s) rs) in C; auto. rewrite C. auto. unfold exec_instr. unfold eval_shift_addr. unfold exec_store. change (rs2 IR13) with sp. change (rs2 IR14) with (rs IR14). rewrite ATLR. rewrite E. auto. @@ -1231,10 +1264,12 @@ Proof. eapply code_tail_next_int; auto. change (Int.unsigned Int.zero) with 0. unfold transl_function. constructor. - assert (AG3: agree ms sp rs3). + assert (AG3: agree (undef_temps ms) sp rs3). unfold rs3. apply agree_nextinstr. unfold rs2. apply agree_nextinstr. - apply agree_change_sp with (parent_sp s); auto. + apply agree_change_sp with (parent_sp s). + apply agree_exten_temps with rs; auto. + intros. apply Pregmap.gso; auto with ppcgen. unfold sp. congruence. left; exists (State rs3 m3'); split. (* execution *) diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index c10c9dfc..fb49cb7a 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -441,6 +441,169 @@ Qed. (** * Correctness of ARM constructor functions *) +(** Decomposition of an integer constant *) + +Lemma decompose_int_rec_or: + forall N n p x, List.fold_left Int.or (decompose_int_rec N n p) x = Int.or x n. +Proof. + induction N; intros; simpl. + destruct (Int.eq_dec n Int.zero); simpl. + subst n. rewrite Int.or_zero. auto. + auto. + destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero). + auto. + simpl. rewrite IHN. rewrite Int.or_assoc. decEq. rewrite <- Int.and_or_distrib. + rewrite Int.or_not_self. apply Int.and_mone. +Qed. + +Lemma decompose_int_rec_xor: + forall N n p x, List.fold_left Int.xor (decompose_int_rec N n p) x = Int.xor x n. +Proof. + induction N; intros; simpl. + destruct (Int.eq_dec n Int.zero); simpl. + subst n. rewrite Int.xor_zero. auto. + auto. + destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero). + auto. + simpl. rewrite IHN. rewrite Int.xor_assoc. decEq. rewrite <- Int.and_xor_distrib. + rewrite Int.xor_not_self. apply Int.and_mone. +Qed. + +Lemma decompose_int_rec_add: + forall N n p x, List.fold_left Int.add (decompose_int_rec N n p) x = Int.add x n. +Proof. + induction N; intros; simpl. + destruct (Int.eq_dec n Int.zero); simpl. + subst n. rewrite Int.add_zero. auto. + auto. + destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero). + auto. + simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. + rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self. +Qed. + +Remark decompose_int_rec_nil: + forall N n p, decompose_int_rec N n p = nil -> n = Int.zero. +Proof. + intros. generalize (decompose_int_rec_or N n p Int.zero). rewrite H. simpl. + rewrite Int.or_commut; rewrite Int.or_zero; auto. +Qed. + +Lemma decompose_int_general: + forall (f: val -> int -> val) (g: int -> int -> int), + (forall v1 n2 n3, f (f v1 n2) n3 = f v1 (g n2 n3)) -> + (forall n1 n2 n3, g (g n1 n2) n3 = g n1 (g n2 n3)) -> + (forall n, g Int.zero n = n) -> + (forall N n p x, List.fold_left g (decompose_int_rec N n p) x = g x n) -> + forall n v, + List.fold_left f (decompose_int n) v = f v n. +Proof. + intros f g DISTR ASSOC ZERO DECOMP. + assert (A: forall l x y, g x (fold_left g l y) = fold_left g l (g x y)). + induction l; intros; simpl. auto. rewrite IHl. decEq. rewrite ASSOC; auto. + assert (B: forall l v n, fold_left f l (f v n) = f v (fold_left g l n)). + induction l; intros; simpl. + auto. + rewrite IHl. rewrite DISTR. decEq. decEq. auto. + intros. unfold decompose_int. + destruct (decompose_int_rec 12 n Int.zero) as []_eqn. + simpl. exploit decompose_int_rec_nil; eauto. congruence. + simpl. rewrite B. decEq. + generalize (DECOMP 12%nat n Int.zero Int.zero). + rewrite Heql. simpl. repeat rewrite ZERO. auto. +Qed. + +Lemma decompose_int_or: + forall n v, + List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) v = Val.or v (Vint n). +Proof. + intros. apply decompose_int_general with (f := fun v n => Val.or v (Vint n)) (g := Int.or). + intros. rewrite Val.or_assoc. auto. + apply Int.or_assoc. + intros. rewrite Int.or_commut. apply Int.or_zero. + apply decompose_int_rec_or. +Qed. + +Lemma decompose_int_bic: + forall n v, + List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int n) v = Val.and v (Vint (Int.not n)). +Proof. + intros. apply decompose_int_general with (f := fun v n => Val.and v (Vint (Int.not n))) (g := Int.or). + intros. rewrite Val.and_assoc. simpl. decEq. decEq. rewrite Int.not_or_and_not. auto. + apply Int.or_assoc. + intros. rewrite Int.or_commut. apply Int.or_zero. + apply decompose_int_rec_or. +Qed. + +Lemma decompose_int_xor: + forall n v, + List.fold_left (fun v i => Val.xor v (Vint i)) (decompose_int n) v = Val.xor v (Vint n). +Proof. + intros. apply decompose_int_general with (f := fun v n => Val.xor v (Vint n)) (g := Int.xor). + intros. rewrite Val.xor_assoc. auto. + apply Int.xor_assoc. + intros. rewrite Int.xor_commut. apply Int.xor_zero. + apply decompose_int_rec_xor. +Qed. + +Lemma decompose_int_add: + forall n v, + List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) v = Val.add v (Vint n). +Proof. + intros. apply decompose_int_general with (f := fun v n => Val.add v (Vint n)) (g := Int.add). + intros. rewrite Val.add_assoc. auto. + apply Int.add_assoc. + intros. rewrite Int.add_commut. apply Int.add_zero. + apply decompose_int_rec_add. +Qed. + +Lemma decompose_int_sub: + forall n v, + List.fold_left (fun v i => Val.sub v (Vint i)) (decompose_int n) v = Val.sub v (Vint n). +Proof. + intros. apply decompose_int_general with (f := fun v n => Val.sub v (Vint n)) (g := Int.add). + intros. repeat rewrite Val.sub_add_opp. rewrite Val.add_assoc. decEq. simpl. decEq. + rewrite Int.neg_add_distr; auto. + apply Int.add_assoc. + intros. rewrite Int.add_commut. apply Int.add_zero. + apply decompose_int_rec_add. +Qed. + +Lemma iterate_op_correct: + forall op1 op2 (f: val -> int -> val) (rs: regset) (r: ireg) m v0 n k, + (forall (rs:regset) n, + exec_instr ge fn (op2 (SOimm n)) rs m = + OK (nextinstr (rs#r <- (f (rs#r) n))) m) -> + (forall n, + exec_instr ge fn (op1 (SOimm n)) rs m = + OK (nextinstr (rs#r <- (f v0 n))) m) -> + exists rs', + exec_straight (iterate_op op1 op2 (decompose_int n) k) rs m k rs' m + /\ rs'#r = List.fold_left f (decompose_int n) v0 + /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'. +Proof. + intros until k; intros SEM2 SEM1. + unfold iterate_op. + destruct (decompose_int n) as [ | i tl] _eqn. + unfold decompose_int in Heql. destruct (decompose_int_rec 12%nat n Int.zero); congruence. + revert k. pattern tl. apply List.rev_ind. + (* base case *) + intros; simpl. econstructor. + split. apply exec_straight_one. rewrite SEM1. reflexivity. reflexivity. + split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. auto. + intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen. + (* inductive case *) + intros. + rewrite List.map_app. simpl. rewrite app_ass. simpl. + destruct (H (op2 (SOimm x) :: k)) as [rs' [A [B C]]]. + econstructor. + split. eapply exec_straight_trans. eexact A. apply exec_straight_one. + rewrite SEM2. reflexivity. reflexivity. + split. rewrite fold_left_app; simpl. rewrite nextinstr_inv; auto with ppcgen. + rewrite Pregmap.gss. rewrite B. auto. + intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen. +Qed. + (** Loading a constant. *) Lemma loadimm_correct: @@ -451,46 +614,19 @@ Lemma loadimm_correct: /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'. Proof. intros. unfold loadimm. - case (is_immed_arith n). - (* single move *) - exists (nextinstr (rs#r <- (Vint n))). - split. apply exec_straight_one. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. - apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - case (is_immed_arith (Int.not n)). - (* single move-complement *) - exists (nextinstr (rs#r <- (Vint n))). - split. apply exec_straight_one. - simpl. change (Int.xor (Int.not n) Int.mone) with (Int.not (Int.not n)). - rewrite Int.not_involutive. auto. - reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. - apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - (* mov - or - or - or *) - set (n1 := Int.and n (Int.repr 255)). - set (n2 := Int.and n (Int.repr 65280)). - set (n3 := Int.and n (Int.repr 16711680)). - set (n4 := Int.and n (Int.repr 4278190080)). - set (rs1 := nextinstr (rs#r <- (Vint n1))). - set (rs2 := nextinstr (rs1#r <- (Val.or rs1#r (Vint n2)))). - set (rs3 := nextinstr (rs2#r <- (Val.or rs2#r (Vint n3)))). - set (rs4 := nextinstr (rs3#r <- (Val.or rs3#r (Vint n4)))). - exists rs4. - split. apply exec_straight_four with rs1 m rs2 m rs3 m; auto. - split. unfold rs4. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold rs3. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - repeat rewrite Val.or_assoc. simpl. decEq. - unfold n4, n3, n2, n1. repeat rewrite <- Int.and_or_distrib. - change (Int.and n Int.mone = n). apply Int.and_mone. - intros. - unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs3. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n)))). + (* mov - orr* *) + replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero). + apply iterate_op_correct. + auto. + intros; simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto. + rewrite decompose_int_or. simpl. rewrite Int.or_commut; rewrite Int.or_zero; auto. + (* mvn - bic* *) + replace (Vint n) with (List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int (Int.not n)) (Vint Int.mone)). + apply iterate_op_correct. + auto. + intros. simpl. rewrite Int.and_commut; rewrite Int.and_mone; auto. + rewrite decompose_int_bic. simpl. rewrite Int.not_involutive. rewrite Int.and_commut. rewrite Int.and_mone; auto. Qed. (** Add integer immediate. *) @@ -503,46 +639,21 @@ Lemma addimm_correct: /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. intros. unfold addimm. - (* addi *) - case (is_immed_arith n). - exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))). - split. apply exec_straight_one; auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - (* subi *) - case (is_immed_arith (Int.neg n)). - exists (nextinstr (rs#r1 <- (Val.sub rs#r2 (Vint (Int.neg n))))). - split. apply exec_straight_one; auto. - split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - apply Val.sub_opp_add. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - (* general *) - set (n1 := Int.and n (Int.repr 255)). - set (n2 := Int.and n (Int.repr 65280)). - set (n3 := Int.and n (Int.repr 16711680)). - set (n4 := Int.and n (Int.repr 4278190080)). - set (rs1 := nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n1)))). - set (rs2 := nextinstr (rs1#r1 <- (Val.add rs1#r1 (Vint n2)))). - set (rs3 := nextinstr (rs2#r1 <- (Val.add rs2#r1 (Vint n3)))). - set (rs4 := nextinstr (rs3#r1 <- (Val.add rs3#r1 (Vint n4)))). - exists rs4. - split. apply exec_straight_four with rs1 m rs2 m rs3 m; auto. - simpl. - split. unfold rs4. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold rs3. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - repeat rewrite Val.add_assoc. simpl. decEq. decEq. - unfold n4, n3, n2, n1. repeat rewrite Int.add_and. - change (Int.and n Int.mone = n). apply Int.and_mone. - vm_compute; auto. - vm_compute; auto. - vm_compute; auto. - intros. - unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs3. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n)))). + (* add - add* *) + replace (Val.add (rs r2) (Vint n)) + with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)). + apply iterate_op_correct. + auto. + auto. + apply decompose_int_add. + (* sub - sub* *) + replace (Val.add (rs r2) (Vint n)) + with (List.fold_left (fun v i => Val.sub v (Vint i)) (decompose_int (Int.neg n)) (rs r2)). + apply iterate_op_correct. + auto. + auto. + rewrite decompose_int_sub. apply Val.sub_opp_add. Qed. (* And integer immediate *) @@ -553,7 +664,7 @@ Lemma andimm_correct: exists rs', exec_straight (andimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = Val.and rs#r2 (Vint n) - /\ forall r': preg, r' <> r1 -> r' <> IR14 -> r' <> PC -> rs'#r' = rs#r'. + /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. intros. unfold andimm. (* andi *) @@ -562,57 +673,72 @@ Proof. split. apply exec_straight_one; auto. split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - (* bici *) - case (is_immed_arith (Int.not n)). - exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))). - split. apply exec_straight_one; auto. simpl. - change (Int.xor (Int.not n) Int.mone) with (Int.not (Int.not n)). - rewrite Int.not_involutive. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - (* general *) - exploit loadimm_correct. intros [rs' [A [B C]]]. - exists (nextinstr (rs'#r1 <- (Val.and rs#r2 (Vint n)))). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. rewrite B. rewrite C; auto with ppcgen. + (* bic - bic* *) + replace (Val.and (rs r2) (Vint n)) + with (List.fold_left (fun v i => Val.and v (Vint (Int.not i))) (decompose_int (Int.not n)) (rs r2)). + apply iterate_op_correct. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + auto. + rewrite decompose_int_bic. rewrite Int.not_involutive. auto. Qed. -(** Other integer immediate *) +(** Reverse sub immediate *) -Lemma makeimm_correct: - forall (instr: ireg -> ireg -> shift_op -> instruction) - (sem: val -> val -> val) - r1 (r2: ireg) n k (rs : regset) m, - (forall c r1 r2 so rs m, - exec_instr ge c (instr r1 r2 so) rs m - = OK (nextinstr rs#r1 <- (sem rs#r2 (eval_shift_op so rs))) m) -> - r2 <> IR14 -> +Lemma rsubimm_correct: + forall r1 r2 n k rs m, exists rs', - exec_straight (makeimm instr r1 r2 n k) rs m k rs' m - /\ rs'#r1 = sem rs#r2 (Vint n) - /\ forall r': preg, r' <> r1 -> r' <> PC -> r' <> IR14 -> rs'#r' = rs#r'. + exec_straight (rsubimm r1 r2 n k) rs m k rs' m + /\ rs'#r1 = Val.sub (Vint n) rs#r2 + /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. - intros. unfold makeimm. - case (is_immed_arith n). - (* one immed instr *) - exists (nextinstr (rs#r1 <- (sem rs#r2 (Vint n)))). - split. apply exec_straight_one. - change (Vint n) with (eval_shift_op (SOimm n) rs). auto. - auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - (* general case *) - exploit loadimm_correct. intros [rs' [A [B C]]]. - exists (nextinstr (rs'#r1 <- (sem rs#r2 (Vint n)))). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - rewrite <- B. rewrite <- (C r2). - change (rs' IR14) with (eval_shift_op (SOreg IR14) rs'). auto. - congruence. auto with ppcgen. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto with ppcgen. + intros. unfold rsubimm. + (* rsb - add* *) + replace (Val.sub (Vint n) (rs r2)) + with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (Val.neg (rs r2))). + apply iterate_op_correct. + auto. + intros. simpl. destruct (rs r2); auto. simpl. rewrite Int.sub_add_opp. + rewrite Int.add_commut; auto. + rewrite decompose_int_add. + destruct (rs r2); simpl; auto. rewrite Int.sub_add_opp. rewrite Int.add_commut; auto. +Qed. + +(** Or immediate *) + +Lemma orimm_correct: + forall r1 r2 n k rs m, + exists rs', + exec_straight (orimm r1 r2 n k) rs m k rs' m + /\ rs'#r1 = Val.or rs#r2 (Vint n) + /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. +Proof. + intros. unfold orimm. + (* ori - ori* *) + replace (Val.or (rs r2) (Vint n)) + with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) (rs r2)). + apply iterate_op_correct. + auto. + auto. + apply decompose_int_or. +Qed. + +(** Xor immediate *) + +Lemma xorimm_correct: + forall r1 r2 n k rs m, + exists rs', + exec_straight (xorimm r1 r2 n k) rs m k rs' m + /\ rs'#r1 = Val.xor rs#r2 (Vint n) + /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. +Proof. + intros. unfold xorimm. + (* xori - xori* *) + replace (Val.xor (rs r2) (Vint n)) + with (List.fold_left (fun v i => Val.xor v (Vint i)) (decompose_int n) (rs r2)). + apply iterate_op_correct. + auto. + auto. + apply decompose_int_xor. Qed. (** Indexed memory loads. *) @@ -636,8 +762,7 @@ Proof. split. eapply exec_straight_trans. eauto. apply exec_straight_one. simpl. unfold exec_load. rewrite B. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. - rewrite H. auto. - auto. + rewrite H. auto. auto. split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. Qed. @@ -659,7 +784,8 @@ Proof. exploit addimm_correct. eauto. intros [rs' [A [B C]]]. exists (nextinstr (rs'#dst <- v)). split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_load. rewrite B. rewrite Val.add_assoc. simpl. + simpl. unfold exec_load. rewrite B. + rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. auto. split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. @@ -700,8 +826,8 @@ Proof. exploit addimm_correct. eauto. intros [rs' [A [B C]]]. exists (nextinstr rs'). split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_store. rewrite B. rewrite C. - rewrite Val.add_assoc. simpl. rewrite Int.add_zero. + simpl. unfold exec_store. rewrite B. + rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. congruence. auto with ppcgen. auto. intros. rewrite nextinstr_inv; auto. @@ -723,10 +849,11 @@ Proof. exploit addimm_correct. eauto. intros [rs' [A [B C]]]. exists (nextinstr rs'). split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_store. rewrite B. rewrite C. - rewrite Val.add_assoc. simpl. rewrite Int.add_zero. + simpl. unfold exec_store. rewrite B. + rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. - congruence. congruence. auto with ppcgen. auto. + congruence. congruence. + auto with ppcgen. intros. rewrite nextinstr_inv; auto. Qed. @@ -827,13 +954,14 @@ Ltac TypeInv := TypeInv1; simpl in *; unfold preg_of in *; TypeInv2. Lemma transl_cond_correct: forall cond args k rs m b, map mreg_type args = type_of_condition cond -> - eval_condition cond (map rs (map preg_of args)) = Some b -> + eval_condition cond (map rs (map preg_of args)) m = Some b -> exists rs', exec_straight (transl_cond cond args k) rs m k rs' m /\ rs'#(CR (crbit_for_cond cond)) = Val.of_bool b /\ forall r, important_preg r = true -> rs'#r = rs r. Proof. - intros until b; intros TY EV. rewrite <- (eval_condition_weaken _ _ EV). clear EV. + intros until b; intros TY EV. + rewrite <- (eval_condition_weaken _ _ _ EV). clear EV. destruct cond; simpl in TY; TypeInv. (* Ccomp *) generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))). @@ -917,11 +1045,11 @@ Qed. Ltac Simpl := match goal with - | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen] - | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto - | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto - | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen] - | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen] + | [ |- context[nextinstr _ _] ] => rewrite nextinstr_inv; [auto | auto with ppcgen] + | [ |- context[Pregmap.get ?x (Pregmap.set ?x _ _)] ] => rewrite Pregmap.gss; auto + | [ |- context[Pregmap.set ?x _ _ ?x] ] => rewrite Pregmap.gss; auto + | [ |- context[Pregmap.get _ (Pregmap.set _ _ _)] ] => rewrite Pregmap.gso; [auto | auto with ppcgen] + | [ |- context[Pregmap.set _ _ _ _] ] => rewrite Pregmap.gso; [auto | auto with ppcgen] end. Ltac TranslOpSimpl := @@ -932,13 +1060,13 @@ Ltac TranslOpSimpl := Lemma transl_op_correct: forall op args res k (rs: regset) m v, wt_instr (Mop op args res) -> - eval_operation ge rs#IR13 op (map rs (map preg_of args)) = Some v -> + eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v -> exists rs', exec_straight (transl_op op args res k) rs m k rs' m /\ rs'#(preg_of res) = v /\ forall r, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r. Proof. - intros. rewrite <- (eval_operation_weaken _ _ _ _ H0). inv H. + intros. rewrite <- (eval_operation_weaken _ _ _ _ _ H0). inv H. (* Omove *) simpl. exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))). @@ -952,7 +1080,7 @@ Proof. congruence. (* Ointconst *) generalize (loadimm_correct (ireg_of res) i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. auto. split. auto. intros. auto with ppcgen. + exists rs'. split. auto. split. rewrite B; auto. intros. auto with ppcgen. (* Oaddrstack *) generalize (addimm_correct (ireg_of res) IR13 i k rs m). intros [rs' [EX [RES OTH]]]. @@ -960,41 +1088,43 @@ Proof. (* Ocast8signed *) econstructor; split. eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity. + split. Simpl. Simpl. Simpl. Simpl. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. + reflexivity. compute; auto. intros. repeat Simpl. (* Ocast8unsigned *) econstructor; split. - eapply exec_straight_one. simpl; eauto. auto. - split. Simpl. Simpl. - destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_and. reflexivity. + eapply exec_straight_one. simpl; eauto. auto. + split. Simpl. Simpl. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_and. auto. compute; auto. - intros. repeat Simpl. + intros. repeat Simpl. (* Ocast16signed *) econstructor; split. eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity. + split. Simpl. Simpl. Simpl. Simpl. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.sign_ext_shr_shl. auto. compute; auto. intros. repeat Simpl. (* Ocast16unsigned *) econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. Simpl. Simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_shru_shl. reflexivity. + eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. Simpl. Simpl. Simpl. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.zero_ext_shru_shl; auto. compute; auto. - intros. repeat Simpl. + intros. repeat Simpl. (* Oaddimm *) generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m). intros [rs' [A [B C]]]. exists rs'. split. auto. split. auto. auto with ppcgen. (* Orsbimm *) - exploit (makeimm_correct Prsb (fun v1 v2 => Val.sub v2 v1) (ireg_of res) (ireg_of m0)); - auto with ppcgen. + generalize (rsubimm_correct (ireg_of res) (ireg_of m0) i k rs m). intros [rs' [A [B C]]]. exists rs'. - split. eauto. split. rewrite B. auto. auto with ppcgen. + split. eauto. split. rewrite B. + destruct (rs (ireg_of m0)); auto. + auto with ppcgen. (* Omul *) destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)). econstructor; split. @@ -1006,17 +1136,15 @@ Proof. generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m (ireg_of_not_IR14 m0)). intros [rs' [A [B C]]]. - exists rs'. split. auto. split. auto. auto with ppcgen. + exists rs'; auto with ppcgen. (* Oorimm *) - exploit (makeimm_correct Porr Val.or (ireg_of res) (ireg_of m0)); - auto with ppcgen. + generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. eauto. split. auto. auto with ppcgen. + exists rs'; auto with ppcgen. (* Oxorimm *) - exploit (makeimm_correct Peor Val.xor (ireg_of res) (ireg_of m0)); - auto with ppcgen. + generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. eauto. split. auto. auto with ppcgen. + exists rs'; auto with ppcgen. (* Oshrximm *) assert (exists n, rs (ireg_of m0) = Vint n /\ Int.ltu i (Int.repr 31) = true). destruct (rs (ireg_of m0)); try discriminate. @@ -1050,8 +1178,11 @@ Proof. auto. unfold rs3. case islt; auto. auto. split. unfold rs4. repeat Simpl. rewrite ARG1. simpl. rewrite LTU'. rewrite Int.shrx_shr. fold islt. unfold rs3. rewrite nextinstr_inv; auto with ppcgen. - destruct islt. rewrite RES2. change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))). - rewrite ARG1. simpl. rewrite LTU'. auto. + destruct islt. + rewrite RES2. + change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))). + rewrite ARG1. + simpl. rewrite LTU'. auto. rewrite Pregmap.gss. simpl. rewrite LTU'. auto. assumption. intros. unfold rs4; repeat Simpl. unfold rs3; repeat Simpl. @@ -1059,10 +1190,10 @@ Proof. rewrite OTH2; auto with ppcgen. (* Ocmp *) fold preg_of in *. - assert (exists b, eval_condition c rs ## (preg_of ## args) = Some b /\ v = Val.of_bool b). - fold preg_of in H0. destruct (eval_condition c rs ## (preg_of ## args)). + assert (exists b, eval_condition c rs ## (preg_of ## args) m = Some b /\ v = Val.of_bool b). + fold preg_of in H0. destruct (eval_condition c rs ## (preg_of ## args) m). exists b; split; auto. destruct b; inv H0; auto. congruence. - clear H0. destruct H as [b [EVC VBO]]. rewrite (eval_condition_weaken _ _ EVC). + clear H0. destruct H as [b [EVC VBO]]. rewrite (eval_condition_weaken _ _ _ EVC). destruct (transl_cond_correct c args (Pmov (ireg_of res) (SOimm Int.zero) :: Pmovc (crbit_for_cond c) (ireg_of res) (SOimm Int.one) :: k) diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v index 359aaf27..97250a6e 100644 --- a/arm/Asmgenretaddr.v +++ b/arm/Asmgenretaddr.v @@ -102,6 +102,16 @@ Ltac IsTail := | _ => idtac end. +Lemma iterate_op_tail: + forall op1 op2 l k, is_tail k (iterate_op op1 op2 l k). +Proof. + intros. unfold iterate_op. + destruct l. + auto with coqlib. + constructor. revert l; induction l; simpl; auto with coqlib. +Qed. +Hint Resolve iterate_op_tail: ppcretaddr. + Lemma loadimm_tail: forall r n k, is_tail k (loadimm r n k). Proof. unfold loadimm; intros; IsTail. Qed. @@ -117,10 +127,20 @@ Lemma andimm_tail: Proof. unfold andimm; intros; IsTail. Qed. Hint Resolve andimm_tail: ppcretaddr. -Lemma makeimm_tail: - forall f r1 r2 n k, is_tail k (makeimm f r1 r2 n k). -Proof. unfold makeimm; intros; IsTail. Qed. -Hint Resolve makeimm_tail: ppcretaddr. +Lemma rsubimm_tail: + forall r1 r2 n k, is_tail k (rsubimm r1 r2 n k). +Proof. unfold rsubimm; intros; IsTail. Qed. +Hint Resolve rsubimm_tail: ppcretaddr. + +Lemma orimm_tail: + forall r1 r2 n k, is_tail k (orimm r1 r2 n k). +Proof. unfold orimm; intros; IsTail. Qed. +Hint Resolve orimm_tail: ppcretaddr. + +Lemma xorimm_tail: + forall r1 r2 n k, is_tail k (xorimm r1 r2 n k). +Proof. unfold xorimm; intros; IsTail. Qed. +Hint Resolve xorimm_tail: ppcretaddr. Lemma transl_cond_tail: forall cond args k, is_tail k (transl_cond cond args k). @@ -189,11 +209,11 @@ Proof. Qed. Lemma return_address_exists: - forall f c, is_tail c f.(fn_code) -> + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) -> exists ra, return_address_offset f c ra. Proof. intros. assert (is_tail (transl_code f c) (transl_function f)). - unfold transl_function. IsTail. apply transl_code_tail; auto. + unfold transl_function. IsTail. apply transl_code_tail; eauto with coqlib. destruct (is_tail_code_tail _ _ H0) as [ofs A]. exists (Int.repr ofs). constructor. auto. Qed. diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 3f98b881..25758cc8 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -88,10 +88,10 @@ Ltac InvVLMA := approximations returned by [eval_static_operation]. *) Lemma eval_static_condition_correct: - forall cond al vl b, + forall cond al vl m b, val_list_match_approx al vl -> eval_static_condition cond al = Some b -> - eval_condition cond vl = Some b. + eval_condition cond vl m = Some b. Proof. intros until b. unfold eval_static_condition. @@ -100,9 +100,9 @@ Proof. Qed. Lemma eval_static_operation_correct: - forall op sp al vl v, + forall op sp al vl m v, val_list_match_approx al vl -> - eval_operation ge sp op vl = Some v -> + eval_operation ge sp op vl m = Some v -> val_match_approx (eval_static_operation op al) v. Proof. intros until v. @@ -144,7 +144,7 @@ Proof. inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto. caseEq (eval_static_condition c vl0). - intros. generalize (eval_static_condition_correct _ _ _ _ H H1). + intros. generalize (eval_static_condition_correct _ _ _ m _ H H1). intro. rewrite H2 in H0. destruct b; injection H0; intro; subst v; simpl; auto. intros; simpl; auto. @@ -168,6 +168,7 @@ Section STRENGTH_REDUCTION. Variable app: reg -> approx. Variable sp: val. Variable rs: regset. +Variable m: mem. Hypothesis MATCH: forall r, val_match_approx (app r) rs#r. Lemma intval_correct: @@ -183,7 +184,7 @@ Qed. Lemma cond_strength_reduction_correct: forall cond args, let (cond', args') := cond_strength_reduction app cond args in - eval_condition cond' rs##args' = eval_condition cond rs##args. + eval_condition cond' rs##args' m = eval_condition cond rs##args m. Proof. intros. unfold cond_strength_reduction. case (cond_strength_reduction_match cond args); intros. @@ -191,7 +192,6 @@ Proof. caseEq (intval app r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmp. auto. - destruct c; reflexivity. caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. @@ -199,6 +199,7 @@ Proof. caseEq (intval app r1); intros. simpl. rewrite (intval_correct _ _ H). destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto. + destruct c; reflexivity. caseEq (intval app r2); intros. simpl. rewrite (intval_correct _ _ H0). auto. auto. @@ -217,8 +218,8 @@ Qed. Lemma make_addimm_correct: forall n r v, let (op, args) := make_addimm n r in - eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_addimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -230,8 +231,8 @@ Qed. Lemma make_shlimm_correct: forall n r v, let (op, args) := make_shlimm n r in - eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shlimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -244,8 +245,8 @@ Qed. Lemma make_shrimm_correct: forall n r v, let (op, args) := make_shrimm n r in - eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shrimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -258,8 +259,8 @@ Qed. Lemma make_shruimm_correct: forall n r v, let (op, args) := make_shruimm n r in - eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_shruimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -273,8 +274,8 @@ Lemma make_mulimm_correct: forall n r r' v, rs#r' = Vint n -> let (op, args) := make_mulimm n r r' in - eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_mulimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -282,8 +283,8 @@ Proof. generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros. subst n. simpl in H2. simpl. FuncInv. rewrite Int.mul_one in H1. congruence. caseEq (Int.is_power2 n); intros. - replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil)) - with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)). + replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil) m) + with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil) m). apply make_shlimm_correct. simpl. generalize (Int.is_power2_range _ _ H2). change (Z_of_nat Int.wordsize) with 32. intro. rewrite H3. @@ -294,8 +295,8 @@ Qed. Lemma make_andimm_correct: forall n r v, let (op, args) := make_andimm n r in - eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_andimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -308,8 +309,8 @@ Qed. Lemma make_orimm_correct: forall n r v, let (op, args) := make_orimm n r in - eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_orimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -322,8 +323,8 @@ Qed. Lemma make_xorimm_correct: forall n r v, let (op, args) := make_xorimm n r in - eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v -> - eval_operation ge sp op rs##args = Some v. + eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v -> + eval_operation ge sp op rs##args m = Some v. Proof. intros; unfold make_xorimm. generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros. @@ -336,16 +337,16 @@ Qed. Lemma op_strength_reduction_correct: forall op args v, let (op', args') := op_strength_reduction app op args in - eval_operation ge sp op rs##args = Some v -> - eval_operation ge sp op' rs##args' = Some v. + eval_operation ge sp op rs##args m = Some v -> + eval_operation ge sp op' rs##args' m = Some v. Proof. intros; unfold op_strength_reduction; case (op_strength_reduction_match op args); intros; simpl List.map. (* Oadd *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil) m). apply make_addimm_correct. simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto. caseEq (intval app r2); intros. @@ -354,8 +355,8 @@ Proof. (* Oaddshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil)). + replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil) m). apply make_addimm_correct. simpl. destruct rs#r1; auto. assumption. @@ -365,16 +366,16 @@ Proof. simpl in *. destruct rs#r2; auto. caseEq (intval app r2); intros. rewrite (intval_correct _ _ H0). - replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)). + replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil) m). apply make_addimm_correct. simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. assumption. (* Osubshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil)). + replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil) m). apply make_addimm_correct. simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto. assumption. @@ -386,8 +387,8 @@ Proof. (* Omul *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil) m). apply make_mulimm_correct. apply intval_correct; auto. simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto. caseEq (intval app r2); intros. @@ -398,8 +399,8 @@ Proof. caseEq (intval app r2); intros. caseEq (Int.is_power2 i); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)). + replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil) m). apply make_shruimm_correct. simpl. destruct rs#r1; auto. change 32 with (Z_of_nat Int.wordsize). @@ -412,8 +413,8 @@ Proof. (* Oand *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil) m). apply make_andimm_correct. simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto. caseEq (intval app r2); intros. @@ -422,15 +423,15 @@ Proof. (* Oandshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil)). + replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil) m). apply make_andimm_correct. reflexivity. assumption. (* Oor *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil) m). apply make_orimm_correct. simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto. caseEq (intval app r2); intros. @@ -439,15 +440,15 @@ Proof. (* Oorshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil)). + replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil) m). apply make_orimm_correct. reflexivity. assumption. (* Oxor *) caseEq (intval app r1); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil)) - with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)). + replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil) m) + with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil) m). apply make_xorimm_correct. simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto. caseEq (intval app r2); intros. @@ -456,22 +457,22 @@ Proof. (* Oxorshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil)). + replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil) m). apply make_xorimm_correct. reflexivity. assumption. (* Obic *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil)). + replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil) m). apply make_andimm_correct. reflexivity. assumption. (* Obicshift *) caseEq (intval app r2); intros. rewrite (intval_correct _ _ H). - replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil)) - with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil)). + replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil) m) + with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil) m). apply make_andimm_correct. reflexivity. assumption. (* Oshl *) diff --git a/arm/Op.v b/arm/Op.v index 0a3504e9..bb688ce4 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -32,6 +32,7 @@ Require Import Floats. Require Import Values. Require Import Memory. Require Import Globalenvs. +Require Import Events. Set Implicit Arguments. @@ -175,33 +176,36 @@ Definition eval_shift (s: shift) (n: int) : int := | Sror x => Int.ror n (s_amount x) end. -Definition eval_condition (cond: condition) (vl: list val): +Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with | Ccomp c, Vint n1 :: Vint n2 :: nil => Some (Int.cmp c n1 n2) - | Ccomp c, Vptr b1 n1 :: Vptr b2 n2 :: nil => - if eq_block b1 b2 - then Some (Int.cmp c n1 n2) - else eval_compare_mismatch c - | Ccomp c, Vptr b1 n1 :: Vint n2 :: nil => - eval_compare_null c n2 - | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil => - eval_compare_null c n1 | Ccompu c, Vint n1 :: Vint n2 :: nil => Some (Int.cmpu c n1 n2) + | Ccompu c, Vptr b1 n1 :: Vptr b2 n2 :: nil => + if Mem.valid_pointer m b1 (Int.unsigned n1) + && Mem.valid_pointer m b2 (Int.unsigned n2) then + if eq_block b1 b2 + then Some (Int.cmpu c n1 n2) + else eval_compare_mismatch c + else None + | Ccompu c, Vptr b1 n1 :: Vint n2 :: nil => + eval_compare_null c n2 + | Ccompu c, Vint n1 :: Vptr b2 n2 :: nil => + eval_compare_null c n1 | Ccompshift c s, Vint n1 :: Vint n2 :: nil => Some (Int.cmp c n1 (eval_shift s n2)) - | Ccompshift c s, Vptr b1 n1 :: Vint n2 :: nil => - eval_compare_null c (eval_shift s n2) | Ccompushift c s, Vint n1 :: Vint n2 :: nil => Some (Int.cmpu c n1 (eval_shift s n2)) + | Ccompushift c s, Vptr b1 n1 :: Vint n2 :: nil => + eval_compare_null c (eval_shift s n2) | Ccompimm c n, Vint n1 :: nil => Some (Int.cmp c n1 n) - | Ccompimm c n, Vptr b1 n1 :: nil => - eval_compare_null c n | Ccompuimm c n, Vint n1 :: nil => Some (Int.cmpu c n1 n) + | Ccompuimm c n, Vptr b1 n1 :: nil => + eval_compare_null c n | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil => Some (Float.cmp c f1 f2) | Cnotcompf c, Vfloat f1 :: Vfloat f2 :: nil => @@ -218,7 +222,7 @@ Definition offset_sp (sp: val) (delta: int) : option val := Definition eval_operation (F V: Type) (genv: Genv.t F V) (sp: val) - (op: operation) (vl: list val): option val := + (op: operation) (vl: list val) (m: mem): option val := match op, vl with | Omove, v1::nil => Some v1 | Ointconst n, nil => Some (Vint n) @@ -285,7 +289,7 @@ Definition eval_operation | Ointoffloat, Vfloat f1 :: nil => option_map Vint (Float.intoffloat f1) | Ofloatofint, Vint n1 :: nil => Some (Vfloat (Float.floatofint n1)) | Ocmp c, _ => - match eval_condition c vl with + match eval_condition c vl m with | None => None | Some false => Some Vfalse | Some true => Some Vtrue @@ -346,24 +350,26 @@ Proof. Qed. Lemma eval_negate_condition: - forall (cond: condition) (vl: list val) (b: bool), - eval_condition cond vl = Some b -> - eval_condition (negate_condition cond) vl = Some (negb b). + forall (cond: condition) (vl: list val) (b: bool) (m: mem), + eval_condition cond vl m = Some b -> + eval_condition (negate_condition cond) vl m = Some (negb b). Proof. intros. destruct cond; simpl in H; FuncInv; try subst b; simpl. rewrite Int.negate_cmp. auto. + rewrite Int.negate_cmpu. auto. apply eval_negate_compare_null; auto. apply eval_negate_compare_null; auto. - destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence. + destruct (Mem.valid_pointer m b0 (Int.unsigned i) && + Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate. + destruct (eq_block b0 b1). rewrite Int.negate_cmpu. congruence. destruct c; simpl in H; inv H; auto. - rewrite Int.negate_cmpu. auto. rewrite Int.negate_cmp. auto. - apply eval_negate_compare_null; auto. rewrite Int.negate_cmpu. auto. - rewrite Int.negate_cmp. auto. apply eval_negate_compare_null; auto. + rewrite Int.negate_cmp. auto. rewrite Int.negate_cmpu. auto. + apply eval_negate_compare_null; auto. auto. rewrite negb_elim. auto. Qed. @@ -382,8 +388,8 @@ Hypothesis agree_on_symbols: forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s. Lemma eval_operation_preserved: - forall sp op vl, - eval_operation ge2 sp op vl = eval_operation ge1 sp op vl. + forall sp op vl m, + eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m. Proof. intros. unfold eval_operation; destruct op; try rewrite agree_on_symbols; @@ -518,9 +524,9 @@ Variable A V: Type. Variable genv: Genv.t A V. Lemma type_of_operation_sound: - forall op vl sp v, + forall op vl sp v m, op <> Omove -> - eval_operation genv sp op vl = Some v -> + eval_operation genv sp op vl m = Some v -> Val.has_type v (snd (type_of_operation op)). Proof. intros. @@ -684,22 +690,24 @@ Proof. Qed. Lemma eval_condition_weaken: - forall c vl b, - eval_condition c vl = Some b -> + forall c vl b m, + eval_condition c vl m = Some b -> eval_condition_total c vl = Val.of_bool b. Proof. intros. unfold eval_condition in H; destruct c; FuncInv; try subst b; try reflexivity; simpl; try (apply eval_compare_null_weaken; auto). + destruct (Mem.valid_pointer m b0 (Int.unsigned i) && + Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate. unfold eq_block in H. destruct (zeq b0 b1); try congruence. apply eval_compare_mismatch_weaken; auto. symmetry. apply Val.notbool_negb_1. Qed. Lemma eval_operation_weaken: - forall sp op vl v, - eval_operation genv sp op vl = Some v -> + forall sp op vl v m, + eval_operation genv sp op vl m = Some v -> eval_operation_total sp op vl = v. Proof. intros. @@ -721,7 +729,7 @@ Proof. assert (Int.unsigned (Int.repr 31) < Int.unsigned Int.iwordsize). vm_compute; auto. omega. discriminate. destruct (Float.intoffloat f); simpl in H; inv H. auto. - caseEq (eval_condition c vl); intros; rewrite H0 in H. + caseEq (eval_condition c vl m); intros; rewrite H0 in H. replace v with (Val.of_bool b). eapply eval_condition_weaken; eauto. destruct b; simpl; congruence. @@ -783,12 +791,20 @@ Ltac InvLessdef := end. Lemma eval_condition_lessdef: - forall cond vl1 vl2 b, + forall cond vl1 vl2 b m1 m2, Val.lessdef_list vl1 vl2 -> - eval_condition cond vl1 = Some b -> - eval_condition cond vl2 = Some b. + Mem.extends m1 m2 -> + eval_condition cond vl1 m1 = Some b -> + eval_condition cond vl2 m2 = Some b. Proof. intros. destruct cond; simpl in *; FuncInv; InvLessdef; auto. + destruct (Mem.valid_pointer m1 b0 (Int.unsigned i) && + Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate. + destruct (andb_prop _ _ Heqb2) as [A B]. + assert (forall b ofs, Mem.valid_pointer m1 b ofs = true -> Mem.valid_pointer m2 b ofs = true). + intros until ofs. repeat rewrite Mem.valid_pointer_nonempty_perm. + apply Mem.perm_extends; auto. + rewrite (H _ _ A). rewrite (H _ _ B). auto. Qed. Ltac TrivialExists := @@ -799,34 +815,36 @@ Ltac TrivialExists := end. Lemma eval_operation_lessdef: - forall sp op vl1 vl2 v1, + forall sp op vl1 vl2 v1 m1 m2, Val.lessdef_list vl1 vl2 -> - eval_operation genv sp op vl1 = Some v1 -> - exists v2, eval_operation genv sp op vl2 = Some v2 /\ Val.lessdef v1 v2. + Mem.extends m1 m2 -> + eval_operation genv sp op vl1 m1 = Some v1 -> + exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2. Proof. intros. destruct op; simpl in *; FuncInv; InvLessdef; TrivialExists. exists v2; auto. - destruct (Genv.find_symbol genv i); inv H0. TrivialExists. + destruct (Genv.find_symbol genv i); inv H1. TrivialExists. exists v1; auto. exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto. exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto. exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto. exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto. - destruct (eq_block b b0); inv H0. TrivialExists. - destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. - destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i0 Int.iwordsize); inv H0; TrivialExists. - destruct (Int.ltu i Int.iwordsize); inv H0; TrivialExists. + destruct (eq_block b b0); inv H1. TrivialExists. + destruct (Int.eq i0 Int.zero); inv H1; TrivialExists. + destruct (Int.eq i0 Int.zero); inv H1; TrivialExists. destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialExists. - destruct (Int.ltu i (Int.repr 31)); inv H0; TrivialExists. + destruct (Int.ltu i Int.iwordsize); inv H1; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H2; TrivialExists. + destruct (Int.ltu i0 Int.iwordsize); inv H2; TrivialExists. + destruct (Int.ltu i (Int.repr 31)); inv H1; TrivialExists. exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. - destruct (Float.intoffloat f); simpl in *; inv H0. TrivialExists. - caseEq (eval_condition c vl1); intros. rewrite H1 in H0. - rewrite (eval_condition_lessdef c H H1). - destruct b; inv H0; TrivialExists. - rewrite H1 in H0. discriminate. + destruct (Float.intoffloat f); simpl in *; inv H1. TrivialExists. + exists v1; split; auto. + destruct (eval_condition c vl1 m1) as [] _eqn. + rewrite (eval_condition_lessdef c H H0 Heqo). + auto. + discriminate. Qed. Lemma eval_addressing_lessdef: @@ -841,6 +859,154 @@ Qed. End EVAL_LESSDEF. +(** Shifting stack-relative references. This is used in [Stacking]. *) + +Definition shift_stack_addressing (delta: int) (addr: addressing) := + match addr with + | Ainstack ofs => Ainstack (Int.add delta ofs) + | _ => addr + end. + +Definition shift_stack_operation (delta: int) (op: operation) := + match op with + | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) + | _ => op + end. + +Lemma type_shift_stack_addressing: + forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr. +Proof. + intros. destruct addr; auto. +Qed. + +Lemma type_shift_stack_operation: + forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. +Proof. + intros. destruct op; auto. +Qed. + +(** Compatibility of the evaluation functions with memory injections. *) + +Section EVAL_INJECT. + +Variable F V: Type. +Variable genv: Genv.t F V. +Variable f: meminj. +Hypothesis globals: meminj_preserves_globals genv f. +Variable sp1: block. +Variable sp2: block. +Variable delta: Z. +Hypothesis sp_inj: f sp1 = Some(sp2, delta). + +Ltac InvInject := + match goal with + | [ H: val_inject _ (Vint _) _ |- _ ] => + inv H; InvInject + | [ H: val_inject _ (Vfloat _) _ |- _ ] => + inv H; InvInject + | [ H: val_inject _ (Vptr _ _) _ |- _ ] => + inv H; InvInject + | [ H: val_list_inject _ nil _ |- _ ] => + inv H; InvInject + | [ H: val_list_inject _ (_ :: _) _ |- _ ] => + inv H; InvInject + | _ => idtac + end. + +Lemma eval_condition_inject: + forall cond vl1 vl2 b m1 m2, + val_list_inject f vl1 vl2 -> + Mem.inject f m1 m2 -> + eval_condition cond vl1 m1 = Some b -> + eval_condition cond vl2 m2 = Some b. +Proof. + intros. destruct cond; simpl in *; FuncInv; InvInject; auto. + destruct (Mem.valid_pointer m1 b0 (Int.unsigned i)) as [] _eqn; try discriminate. + destruct (Mem.valid_pointer m1 b1 (Int.unsigned i0)) as [] _eqn; try discriminate. + simpl in H1. + exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb0. econstructor; eauto. + intros V1. rewrite V1. + exploit Mem.valid_pointer_inject_val. eauto. eexact Heqb2. econstructor; eauto. + intros V2. rewrite V2. + simpl. + destruct (eq_block b0 b1); inv H1. + rewrite H3 in H5; inv H5. rewrite dec_eq_true. + decEq. apply Int.translate_cmpu. + eapply Mem.valid_pointer_inject_no_overflow; eauto. + eapply Mem.valid_pointer_inject_no_overflow; eauto. + exploit Mem.different_pointers_inject; eauto. intros P. + destruct (eq_block b3 b4); auto. + destruct P. contradiction. + destruct c; unfold eval_compare_mismatch in *; inv H2. + unfold Int.cmpu. rewrite Int.eq_false; auto. congruence. + unfold Int.cmpu. rewrite Int.eq_false; auto. congruence. +Qed. + +Ltac TrivialExists2 := + match goal with + | [ |- exists v2, Some ?v1 = Some v2 /\ val_inject _ _ v2 ] => + exists v1; split; [auto | econstructor; eauto] + | _ => idtac + end. + +Lemma eval_addressing_inject: + forall addr vl1 vl2 v1, + val_list_inject f vl1 vl2 -> + eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> + exists v2, + eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 + /\ val_inject f v1 v2. +Proof. + assert (UNUSED: meminj_preserves_globals genv f). exact globals. + intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists2. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. auto. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. +Qed. + +Lemma eval_operation_inject: + forall op vl1 vl2 v1 m1 m2, + val_list_inject f vl1 vl2 -> + Mem.inject f m1 m2 -> + eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> + exists v2, + eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 + /\ val_inject f v1 v2. +Proof. + intros. destruct op; simpl in *; FuncInv; InvInject; TrivialExists2. + exists v'; auto. + destruct (Genv.find_symbol genv i) as [] _eqn; inv H1. + TrivialExists2. eapply (proj1 globals); eauto. rewrite Int.add_zero; auto. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + exists (Val.sign_ext 8 v'); split; auto. inv H4; simpl; auto. + exists (Val.zero_ext 8 v'); split; auto. inv H4; simpl; auto. + exists (Val.sign_ext 16 v'); split; auto. inv H4; simpl; auto. + exists (Val.zero_ext 16 v'); split; auto. inv H4; simpl; auto. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + rewrite Int.sub_add_l. auto. + destruct (eq_block b b0); inv H1. rewrite H3 in H5; inv H5. rewrite dec_eq_true. + rewrite Int.sub_shifted. TrivialExists2. + rewrite Int.sub_add_l. auto. + destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2. + destruct (Int.eq i0 Int.zero); inv H1. TrivialExists2. + destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2. + destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2. + destruct (Int.ltu i0 Int.iwordsize); inv H1. TrivialExists2. + destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists2. + exists (Val.singleoffloat v'); split; auto. inv H4; simpl; auto. + destruct (Float.intoffloat f0); simpl in *; inv H1. TrivialExists2. + destruct (eval_condition c vl1 m1) as [] _eqn; try discriminate. + exploit eval_condition_inject; eauto. intros EQ; rewrite EQ. + destruct b; inv H1; TrivialExists2. +Qed. + +End EVAL_INJECT. + (** Recognition of integers that are valid shift amounts. *) Definition is_shift_amount_aux (n: int) : @@ -891,10 +1057,10 @@ Definition op_for_binary_addressing (addr: addressing) : operation := end. Lemma eval_op_for_binary_addressing: - forall (F V: Type) (ge: Genv.t F V) sp addr args v, + forall (F V: Type) (ge: Genv.t F V) sp addr args v m, (length args >= 2)%nat -> eval_addressing ge sp addr args = Some v -> - eval_operation ge sp (op_for_binary_addressing addr) args = Some v. + eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. Proof. intros. unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; simpl. @@ -926,54 +1092,22 @@ Definition is_trivial_op (op: operation) : bool := | _ => false end. -(** Shifting stack-relative references. This is used in [Stacking]. *) -Definition shift_stack_addressing (delta: int) (addr: addressing) := - match addr with - | Ainstack ofs => Ainstack (Int.add delta ofs) - | _ => addr - end. +(** Operations that depend on the memory state. *) -Definition shift_stack_operation (delta: int) (op: operation) := +Definition op_depends_on_memory (op: operation) : bool := match op with - | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) - | _ => op + | Ocmp (Ccompu _) => true + | _ => false end. -Lemma shift_stack_eval_addressing: - forall (F V: Type) (ge: Genv.t F V) sp addr args delta, - eval_addressing ge (Val.sub sp (Vint delta)) (shift_stack_addressing delta addr) args = - eval_addressing ge sp addr args. +Lemma op_depends_on_memory_correct: + forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, + op_depends_on_memory op = false -> + eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros. destruct addr; simpl; auto. - destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. - decEq. decEq. rewrite <- Int.add_assoc. decEq. - rewrite Int.sub_add_opp. rewrite Int.add_assoc. - rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. - rewrite Int.sub_idem. apply Int.add_zero. + intros until m2. destruct op; simpl; try congruence. + destruct c; simpl; congruence. Qed. -Lemma shift_stack_eval_operation: - forall (F V: Type) (ge: Genv.t F V) sp op args delta, - eval_operation ge (Val.sub sp (Vint delta)) (shift_stack_operation delta op) args = - eval_operation ge sp op args. -Proof. - intros. destruct op; simpl; auto. - destruct args; auto. unfold offset_sp. destruct sp; simpl; auto. - decEq. decEq. rewrite <- Int.add_assoc. decEq. - rewrite Int.sub_add_opp. rewrite Int.add_assoc. - rewrite (Int.add_commut (Int.neg delta)). rewrite <- Int.sub_add_opp. - rewrite Int.sub_idem. apply Int.add_zero. -Qed. -Lemma type_shift_stack_addressing: - forall delta addr, type_of_addressing (shift_stack_addressing delta addr) = type_of_addressing addr. -Proof. - intros. destruct addr; auto. -Qed. - -Lemma type_shift_stack_operation: - forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. -Proof. - intros. destruct op; auto. -Qed. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 4f470cef..883ee724 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -453,30 +453,21 @@ let print_instruction oc labels = function | Psufd(r1, r2, r3) -> fprintf oc " sufd %a, %a, %a\n" freg r1 freg r2 freg r3; 1 (* Pseudo-instructions *) - | Pallocframe(lo, hi, ofs) -> - let lo = camlint_of_coqint lo - and hi = camlint_of_coqint hi - and ofs = camlint_of_coqint ofs in - let sz = Int32.sub hi lo in - (* Keep stack 4-aligned *) - let sz4 = Int32.logand (Int32.add sz 3l) 0xFFFF_FFFCl in - (* FIXME: consider a store multiple? *) - (* R12 = first int temporary is unused at this point, - but this should be reflected in the proof *) + | Pallocframe(sz, ofs) -> fprintf oc " mov r12, sp\n"; let ninstr = ref 0 in List.iter - (fun mask -> - let b = Int32.logand sz4 mask in - if b <> 0l then begin - fprintf oc " sub sp, sp, #%ld\n" b; - incr ninstr - end) - [0xFF000000l; 0x00FF0000l; 0x0000FF00l; 0x000000FFl]; - fprintf oc " str r12, [sp, #%ld]\n" ofs; + (fun n -> + fprintf oc " sub sp, sp, #%a\n" coqint n; + incr ninstr) + (Asmgen.decompose_int sz); + fprintf oc " str r12, [sp, #%a]\n" coqint ofs; 2 + !ninstr - | Pfreeframe(lo, hi, ofs) -> - fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1 + | Pfreeframe(sz, ofs) -> + if Asmgen.is_immed_arith sz + then fprintf oc " add sp, sp, #%a\n" coqint sz + else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; + 1 | Plabel lbl -> if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl; 0 diff --git a/arm/SelectOp.v b/arm/SelectOp.v index df2413a6..44528c61 100644 --- a/arm/SelectOp.v +++ b/arm/SelectOp.v @@ -146,7 +146,7 @@ Definition notint (e: expr) := (** ** Boolean negation *) Definition notbool_base (e: expr) := - Eop (Ocmp (Ccompimm Ceq Int.zero)) (e ::: Enil). + Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil). Fixpoint notbool (e: expr) {struct e} : expr := match e with diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index cdb21cbe..7602b119 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -64,13 +64,13 @@ Ltac InvEval1 := Ltac InvEval2 := match goal with - | [ H: (eval_operation _ _ _ nil = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] => simpl in H; inv H - | [ H: (eval_operation _ _ _ (_ :: nil) = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv - | [ H: (eval_operation _ _ _ (_ :: _ :: nil) = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv - | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) = Some _) |- _ ] => + | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] => simpl in H; FuncInv | _ => idtac @@ -162,12 +162,12 @@ Proof. eapply eval_notbool_base; eauto. inv H. eapply eval_Eop; eauto. - simpl. assert (eval_condition c vl = Some b). + simpl. assert (eval_condition c vl m = Some b). generalize H6. simpl. case (eval_condition c vl); intros. destruct b0; inv H1; inversion H0; auto; congruence. congruence. - rewrite (Op.eval_negate_condition _ _ H). + rewrite (Op.eval_negate_condition _ _ _ H). destruct b; reflexivity. inv H. eapply eval_Econdition; eauto. @@ -524,9 +524,9 @@ Qed. Lemma eval_mod_aux: forall divop semdivop, - (forall sp x y, + (forall sp x y m, y <> Int.zero -> - eval_operation ge sp divop (Vint x :: Vint y :: nil) = + eval_operation ge sp divop (Vint x :: Vint y :: nil) m = Some (Vint (semdivop x y))) -> forall le a b x y, eval_expr ge sp e m le a (Vint x) -> @@ -757,7 +757,7 @@ Theorem eval_singleoffloat: eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). Proof. TrivialOp singleoffloat. Qed. -Theorem eval_comp_int: +Theorem eval_comp: forall le c a x b y, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vint y) -> @@ -767,11 +767,26 @@ Proof. unfold comp; case (comp_match a b); intros; InvEval. EvalOp. simpl. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity. EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. - EvalOp. simpl. rewrite Int.swap_cmp. rewrite H. destruct (Int.cmp c x y); reflexivity. + EvalOp. simpl. rewrite H. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity. EvalOp. simpl. rewrite H0. destruct (Int.cmp c x y); reflexivity. EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. Qed. +Theorem eval_compu_int: + forall le c a x b y, + eval_expr ge sp e m le a (Vint x) -> + eval_expr ge sp e m le b (Vint y) -> + eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). +Proof. + intros until y. + unfold compu; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. rewrite Int.swap_cmpu. rewrite H. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. rewrite H0. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. +Qed. + Remark eval_compare_null_trans: forall c x v, (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> @@ -786,15 +801,15 @@ Proof. destruct c; try discriminate; auto. Qed. -Theorem eval_comp_ptr_int: +Theorem eval_compu_ptr_int: forall le c a x1 x2 b y v, eval_expr ge sp e m le a (Vptr x1 x2) -> eval_expr ge sp e m le b (Vint y) -> (if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - eval_expr ge sp e m le (comp c a b) v. + eval_expr ge sp e m le (compu c a b) v. Proof. intros until v. - unfold comp; case (comp_match a b); intros; InvEval. + unfold compu; case (comp_match a b); intros; InvEval. EvalOp. simpl. apply eval_compare_null_trans; auto. EvalOp. simpl. rewrite H0. apply eval_compare_null_trans; auto. EvalOp. simpl. apply eval_compare_null_trans; auto. @@ -814,61 +829,49 @@ Proof. destruct c; simpl; try discriminate; auto. Qed. -Theorem eval_comp_int_ptr: +Theorem eval_compu_int_ptr: forall le c a x b y1 y2 v, eval_expr ge sp e m le a (Vint x) -> eval_expr ge sp e m le b (Vptr y1 y2) -> (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - eval_expr ge sp e m le (comp c a b) v. + eval_expr ge sp e m le (compu c a b) v. Proof. intros until v. - unfold comp; case (comp_match a b); intros; InvEval. + unfold compu; case (comp_match a b); intros; InvEval. EvalOp. simpl. apply eval_swap_compare_null_trans; auto. EvalOp. simpl. rewrite H. apply eval_swap_compare_null_trans; auto. EvalOp. simpl. apply eval_compare_null_trans; auto. Qed. -Theorem eval_comp_ptr_ptr: +Theorem eval_compu_ptr_ptr: forall le c a x1 x2 b y1 y2, eval_expr ge sp e m le a (Vptr x1 x2) -> eval_expr ge sp e m le b (Vptr y1 y2) -> + Mem.valid_pointer m x1 (Int.unsigned x2) + && Mem.valid_pointer m y1 (Int.unsigned y2) = true -> x1 = y1 -> - eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)). + eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x2 y2)). Proof. intros until y2. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. subst y1. rewrite dec_eq_true. - destruct (Int.cmp c x2 y2); reflexivity. + unfold compu; case (comp_match a b); intros; InvEval. + EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. + destruct (Int.cmpu c x2 y2); reflexivity. Qed. -Theorem eval_comp_ptr_ptr_2: +Theorem eval_compu_ptr_ptr_2: forall le c a x1 x2 b y1 y2 v, eval_expr ge sp e m le a (Vptr x1 x2) -> eval_expr ge sp e m le b (Vptr y1 y2) -> + Mem.valid_pointer m x1 (Int.unsigned x2) + && Mem.valid_pointer m y1 (Int.unsigned y2) = true -> x1 <> y1 -> Cminor.eval_compare_mismatch c = Some v -> - eval_expr ge sp e m le (comp c a b) v. + eval_expr ge sp e m le (compu c a b) v. Proof. intros until y2. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite dec_eq_false; auto. - destruct c; simpl in H2; inv H2; auto. -Qed. - - -Theorem eval_compu: - forall le c a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). -Proof. - intros until y. unfold compu; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. rewrite H. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. rewrite H0. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. + EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto. + destruct c; simpl in H3; inv H3; auto. Qed. Theorem eval_compf: diff --git a/arm/linux/Stacklayout.v b/arm/linux/Stacklayout.v index b374bfd9..4521114f 100644 --- a/arm/linux/Stacklayout.v +++ b/arm/linux/Stacklayout.v @@ -28,12 +28,6 @@ Require Import Bounds. - Pointer to activation record of the caller. - Space for the stack-allocated data declared in Cminor. -To facilitate some of the proofs, the Cminor stack-allocated data -starts at offset 0; the preceding areas in the activation record -therefore have negative offsets. This part (with negative offsets) -is called the ``frame'', by opposition with the ``Cminor stack data'' -which is the part with positive offsets. - The [frame_env] compilation environment records the positions of the boundaries between areas in the frame part. *) @@ -49,7 +43,8 @@ Record frame_env : Type := mk_frame_env { fe_num_int_callee_save: Z; fe_ofs_float_local: Z; fe_ofs_float_callee_save: Z; - fe_num_float_callee_save: Z + fe_num_float_callee_save: Z; + fe_stack_data: Z }. (** Computation of the frame environment from the bounds of the current @@ -63,17 +58,84 @@ Definition make_env (b: bounds) := let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *) let ora := ofcs + 8 * b.(bound_float_callee_save) in (* retaddr *) let olink := ora + 4 in (* back link *) - let sz := olink + 4 in (* total frame size *) + let ostkdata := olink + 4 in (* stack data *) + let sz := align (ostkdata + b.(bound_stack_data)) 8 in mk_frame_env sz olink ora oil oics b.(bound_int_callee_save) - ofl ofcs b.(bound_float_callee_save). + ofl ofcs b.(bound_float_callee_save) + ostkdata. +(** Separation property *) -Remark align_float_part: +Remark frame_env_separated: forall b, - 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <= - align (4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8. + let fe := make_env b in + 0 <= fe_ofs_arg + /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_int_local) + /\ fe.(fe_ofs_int_local) + 4 * b.(bound_int_local) <= fe.(fe_ofs_int_callee_save) + /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_local) + /\ fe.(fe_ofs_float_local) + 8 * b.(bound_float_local) <= fe.(fe_ofs_float_callee_save) + /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_ofs_retaddr) + /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_ofs_link) + /\ fe.(fe_ofs_link) + 4 <= fe.(fe_stack_data) + /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size). Proof. - intros. apply align_le. omega. + intros. + generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)). + generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 8 (refl_equal _)). + unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, + fe_ofs_int_local, fe_ofs_int_callee_save, + fe_num_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + fe_stack_data, fe_ofs_arg. + intros. + generalize (bound_int_local_pos b); intro; + generalize (bound_float_local_pos b); intro; + generalize (bound_int_callee_save_pos b); intro; + generalize (bound_float_callee_save_pos b); intro; + generalize (bound_outgoing_pos b); intro; + generalize (bound_stack_data_pos b); intro. + omega. Qed. +(** Alignment property *) + +Remark frame_env_aligned: + forall b, + let fe := make_env b in + (4 | fe.(fe_ofs_link)) + /\ (4 | fe.(fe_ofs_int_local)) + /\ (4 | fe.(fe_ofs_int_callee_save)) + /\ (8 | fe.(fe_ofs_float_local)) + /\ (8 | fe.(fe_ofs_float_callee_save)) + /\ (4 | fe.(fe_ofs_retaddr)) + /\ (4 | fe.(fe_stack_data)) + /\ (8 | fe.(fe_size)). +Proof. + intros. + unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, + fe_ofs_int_local, fe_ofs_int_callee_save, + fe_num_int_callee_save, + fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + fe_stack_data. + set (x1 := 4 * bound_outgoing b). + assert (4 | x1). unfold x1; exists (bound_outgoing b); ring. + set (x2 := x1 + 4 * bound_int_local b). + assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring. + set (x3 := x2 + 4 * bound_int_callee_save b). + set (x4 := align x3 8). + assert (8 | x4). unfold x4. apply align_divides. omega. + set (x5 := x4 + 8 * bound_float_local b). + assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring. + set (x6 := x5 + 8 * bound_float_callee_save b). + assert (4 | x6). + apply Zdivides_trans with 8. exists 2; auto. + unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. + set (x7 := x6 + 4). + assert (4 | x7). unfold x7; apply Zdivide_plus_r; auto. exists 1; auto. + set (x8 := x7 + 4). + assert (4 | x8). unfold x8; apply Zdivide_plus_r; auto. exists 1; auto. + set (x9 := align (x8 + bound_stack_data b) 8). + assert (8 | x9). unfold x9; apply align_divides. omega. + tauto. +Qed. -- cgit