From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgenproof1.v | 1507 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1507 insertions(+) create mode 100644 arm/Asmgenproof1.v (limited to 'arm/Asmgenproof1.v') diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v new file mode 100644 index 00000000..32fedf31 --- /dev/null +++ b/arm/Asmgenproof1.v @@ -0,0 +1,1507 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness proof for ARM code generation: auxiliary results. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. +Require Import Op. +Require Import Locations. +Require Import Mach. +Require Import Machconcr. +Require Import Machtyping. +Require Import Asm. +Require Import Asmgen. +Require Conventions. + +(** * Correspondence between Mach registers and PPC registers *) + +Hint Extern 2 (_ <> _) => discriminate: ppcgen. + +(** Mapping from Mach registers to PPC registers. *) + +Lemma preg_of_injective: + forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. +Proof. + destruct r1; destruct r2; simpl; intros; reflexivity || discriminate. +Qed. + +(** Characterization of PPC registers that correspond to Mach registers. *) + +Definition is_data_reg (r: preg) : Prop := + match r with + | IR IR14 => False + | CR _ => False + | PC => False + | _ => True + end. + +Lemma ireg_of_is_data_reg: + forall (r: mreg), is_data_reg (ireg_of r). +Proof. + destruct r; exact I. +Qed. + +Lemma freg_of_is_data_reg: + forall (r: mreg), is_data_reg (ireg_of r). +Proof. + destruct r; exact I. +Qed. + +Lemma preg_of_is_data_reg: + forall (r: mreg), is_data_reg (preg_of r). +Proof. + destruct r; exact I. +Qed. + +Lemma ireg_of_not_IR13: + forall r, ireg_of r <> IR13. +Proof. + intro. case r; discriminate. +Qed. +Lemma ireg_of_not_IR14: + forall r, ireg_of r <> IR14. +Proof. + intro. case r; discriminate. +Qed. + +Hint Resolve ireg_of_not_IR13 ireg_of_not_IR14: ppcgen. + +Lemma preg_of_not: + forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2. +Proof. + intros; red; intro. subst r2. elim H. apply preg_of_is_data_reg. +Qed. +Hint Resolve preg_of_not: ppcgen. + +Lemma preg_of_not_IR13: + forall r, preg_of r <> IR13. +Proof. + intro. case r; discriminate. +Qed. +Hint Resolve preg_of_not_IR13: ppcgen. + +(** Agreement between Mach register sets and PPC register sets. *) + +Definition agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) := + rs#IR13 = sp /\ forall r: mreg, ms r = rs#(preg_of r). + +Lemma preg_val: + forall ms sp rs r, + agree ms sp rs -> ms r = rs#(preg_of r). +Proof. + intros. elim H. auto. +Qed. + +Lemma ireg_val: + forall ms sp rs r, + agree ms sp rs -> + mreg_type r = Tint -> + ms r = rs#(ireg_of r). +Proof. + intros. elim H; intros. + generalize (H2 r). unfold preg_of. rewrite H0. auto. +Qed. + +Lemma freg_val: + forall ms sp rs r, + agree ms sp rs -> + mreg_type r = Tfloat -> + ms r = rs#(freg_of r). +Proof. + intros. elim H; intros. + generalize (H2 r). unfold preg_of. rewrite H0. auto. +Qed. + +Lemma sp_val: + forall ms sp rs, + agree ms sp rs -> + sp = rs#IR13. +Proof. + intros. elim H; auto. +Qed. + +Lemma agree_exten_1: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, is_data_reg r -> rs'#r = rs#r) -> + agree ms sp rs'. +Proof. + unfold agree; intros. elim H; intros. + split. rewrite H0. auto. exact I. + intros. rewrite H0. auto. apply preg_of_is_data_reg. +Qed. + +Lemma agree_exten_2: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r) -> + agree ms sp rs'. +Proof. + intros. eapply agree_exten_1; eauto. + intros. apply H0; red; intro; subst r; elim H1. +Qed. + +(** Preservation of register agreement under various assignments. *) + +Lemma agree_set_mreg: + forall ms sp rs r v, + agree ms sp rs -> + agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v). +Proof. + unfold agree; intros. elim H; intros; clear H. + split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_IR13. + intros. unfold Regmap.set. case (RegEq.eq r0 r); intro. + subst r0. rewrite Pregmap.gss. auto. + rewrite Pregmap.gso. auto. red; intro. + elim n. apply preg_of_injective; auto. +Qed. +Hint Resolve agree_set_mreg: ppcgen. + +Lemma agree_set_mireg: + forall ms sp rs r v, + agree ms sp (rs#(preg_of r) <- v) -> + mreg_type r = Tint -> + agree ms sp (rs#(ireg_of r) <- v). +Proof. + intros. unfold preg_of in H. rewrite H0 in H. auto. +Qed. +Hint Resolve agree_set_mireg: ppcgen. + +Lemma agree_set_mfreg: + forall ms sp rs r v, + agree ms sp (rs#(preg_of r) <- v) -> + mreg_type r = Tfloat -> + agree ms sp (rs#(freg_of r) <- v). +Proof. + intros. unfold preg_of in H. rewrite H0 in H. auto. +Qed. +Hint Resolve agree_set_mfreg: ppcgen. + +Lemma agree_set_other: + forall ms sp rs r v, + agree ms sp rs -> + ~(is_data_reg r) -> + agree ms sp (rs#r <- v). +Proof. + intros. apply agree_exten_1 with rs. + auto. intros. apply Pregmap.gso. red; intro; subst r0; contradiction. +Qed. +Hint Resolve agree_set_other: ppcgen. + +Lemma agree_nextinstr: + forall ms sp rs, + agree ms sp rs -> agree ms sp (nextinstr rs). +Proof. + intros. unfold nextinstr. apply agree_set_other. auto. auto. +Qed. +Hint Resolve agree_nextinstr: ppcgen. + +Lemma agree_set_mireg_twice: + forall ms sp rs r v v', + agree ms sp rs -> + mreg_type r = Tint -> + agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v). +Proof. + intros. replace (IR (ireg_of r)) with (preg_of r). elim H; intros. + split. repeat (rewrite Pregmap.gso; auto with ppcgen). + intros. case (mreg_eq r r0); intro. + subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto. + assert (preg_of r <> preg_of r0). + red; intro. elim n. apply preg_of_injective. auto. + rewrite Regmap.gso; auto. + repeat (rewrite Pregmap.gso; auto). + unfold preg_of. rewrite H0. auto. +Qed. +Hint Resolve agree_set_mireg_twice: ppcgen. + +Lemma agree_set_twice_mireg: + forall ms sp rs r v v', + agree (Regmap.set r v' ms) sp rs -> + mreg_type r = Tint -> + agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v). +Proof. + intros. elim H; intros. + split. rewrite Pregmap.gso. auto. + generalize (ireg_of_not_IR13 r); congruence. + intros. generalize (H2 r0). + case (mreg_eq r0 r); intro. + subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0. + rewrite Pregmap.gss. auto. + repeat rewrite Regmap.gso; auto. + rewrite Pregmap.gso. auto. + replace (IR (ireg_of r)) with (preg_of r). + red; intros. elim n. apply preg_of_injective; auto. + unfold preg_of. rewrite H0. auto. +Qed. +Hint Resolve agree_set_twice_mireg: ppcgen. + +Lemma agree_set_commut: + forall ms sp rs r1 r2 v1 v2, + r1 <> r2 -> + agree ms sp ((rs#r2 <- v2)#r1 <- v1) -> + agree ms sp ((rs#r1 <- v1)#r2 <- v2). +Proof. + intros. apply agree_exten_1 with ((rs#r2 <- v2)#r1 <- v1). auto. + intros. + case (preg_eq r r1); intro. + subst r1. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. + auto. auto. + case (preg_eq r r2); intro. + subst r2. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. + auto. auto. + repeat (rewrite Pregmap.gso; auto). +Qed. +Hint Resolve agree_set_commut: ppcgen. + +Lemma agree_nextinstr_commut: + forall ms sp rs r v, + agree ms sp (rs#r <- v) -> + r <> PC -> + agree ms sp ((nextinstr rs)#r <- v). +Proof. + intros. unfold nextinstr. apply agree_set_commut. auto. + apply agree_set_other. auto. auto. +Qed. +Hint Resolve agree_nextinstr_commut: ppcgen. + +Lemma agree_set_mireg_exten: + forall ms sp rs r v (rs': regset), + agree ms sp rs -> + mreg_type r = Tint -> + rs'#(ireg_of r) = v -> + (forall r', r' <> PC -> r' <> ireg_of r -> r' <> IR14 -> rs'#r' = rs#r') -> + agree (Regmap.set r v ms) sp rs'. +Proof. + intros. apply agree_exten_2 with (rs#(ireg_of r) <- v). + auto with ppcgen. + intros. unfold Pregmap.set. case (PregEq.eq r0 (ireg_of r)); intro. + subst r0. auto. apply H2; auto. +Qed. + +(** Useful properties of the PC and GPR0 registers. *) + +Lemma nextinstr_inv: + forall r rs, r <> PC -> (nextinstr rs)#r = rs#r. +Proof. + intros. unfold nextinstr. apply Pregmap.gso. auto. +Qed. +Hint Resolve nextinstr_inv: ppcgen. + +Lemma nextinstr_set_preg: + forall rs m v, + (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone. +Proof. + intros. unfold nextinstr. rewrite Pregmap.gss. + rewrite Pregmap.gso. auto. apply sym_not_eq. auto with ppcgen. +Qed. +Hint Resolve nextinstr_set_preg: ppcgen. + +(** Connection between Mach and Asm calling conventions for external + functions. *) + +Lemma extcall_arg_match: + forall ms sp rs m l v, + agree ms sp rs -> + Machconcr.extcall_arg ms m sp l v -> + Asm.extcall_arg rs m l v. +Proof. + intros. inv H0. + rewrite (preg_val _ _ _ r H). constructor. + rewrite (sp_val _ _ _ H) in H1. + destruct ty; unfold load_stack in H1. + econstructor. reflexivity. assumption. + econstructor. reflexivity. assumption. +Qed. + +Lemma extcall_args_match: + forall ms sp rs m, agree ms sp rs -> + forall ll vl, + Machconcr.extcall_args ms m sp ll vl -> + Asm.extcall_args rs m ll vl. +Proof. + induction 2; constructor; auto. eapply extcall_arg_match; eauto. +Qed. + +Lemma extcall_arguments_match: + forall ms m sp rs sg args, + agree ms sp rs -> + Machconcr.extcall_arguments ms m sp sg args -> + Asm.extcall_arguments rs m sg args. +Proof. + unfold Machconcr.extcall_arguments, Asm.extcall_arguments; intros. + eapply extcall_args_match; eauto. +Qed. + +(** * Execution of straight-line code *) + +Section STRAIGHTLINE. + +Variable ge: genv. +Variable fn: code. + +(** Straight-line code is composed of PPC instructions that execute + in sequence (no branches, no function calls and returns). + The following inductive predicate relates the machine states + before and after executing a straight-line sequence of instructions. + Instructions are taken from the first list instead of being fetched + from memory. *) + +Inductive exec_straight: code -> regset -> mem -> + code -> regset -> mem -> Prop := + | exec_straight_one: + forall i1 c rs1 m1 rs2 m2, + exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> + rs2#PC = Val.add rs1#PC Vone -> + exec_straight (i1 :: c) rs1 m1 c rs2 m2 + | exec_straight_step: + forall i c rs1 m1 rs2 m2 c' rs3 m3, + exec_instr ge fn i rs1 m1 = OK rs2 m2 -> + rs2#PC = Val.add rs1#PC Vone -> + exec_straight c rs2 m2 c' rs3 m3 -> + exec_straight (i :: c) rs1 m1 c' rs3 m3. + +Lemma exec_straight_trans: + forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, + exec_straight c1 rs1 m1 c2 rs2 m2 -> + exec_straight c2 rs2 m2 c3 rs3 m3 -> + exec_straight c1 rs1 m1 c3 rs3 m3. +Proof. + induction 1; intros. + apply exec_straight_step with rs2 m2; auto. + apply exec_straight_step with rs2 m2; auto. +Qed. + +Lemma exec_straight_two: + forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, + exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> + exec_instr ge fn i2 rs2 m2 = OK rs3 m3 -> + rs2#PC = Val.add rs1#PC Vone -> + rs3#PC = Val.add rs2#PC Vone -> + exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3. +Proof. + intros. apply exec_straight_step with rs2 m2; auto. + apply exec_straight_one; auto. +Qed. + +Lemma exec_straight_three: + forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4, + exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> + exec_instr ge fn i2 rs2 m2 = OK rs3 m3 -> + exec_instr ge fn i3 rs3 m3 = OK rs4 m4 -> + rs2#PC = Val.add rs1#PC Vone -> + rs3#PC = Val.add rs2#PC Vone -> + rs4#PC = Val.add rs3#PC Vone -> + exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4. +Proof. + intros. apply exec_straight_step with rs2 m2; auto. + eapply exec_straight_two; eauto. +Qed. + +Lemma exec_straight_four: + forall i1 i2 i3 i4 c rs1 m1 rs2 m2 rs3 m3 rs4 m4 rs5 m5, + exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> + exec_instr ge fn i2 rs2 m2 = OK rs3 m3 -> + exec_instr ge fn i3 rs3 m3 = OK rs4 m4 -> + exec_instr ge fn i4 rs4 m4 = OK rs5 m5 -> + rs2#PC = Val.add rs1#PC Vone -> + rs3#PC = Val.add rs2#PC Vone -> + rs4#PC = Val.add rs3#PC Vone -> + rs5#PC = Val.add rs4#PC Vone -> + exec_straight (i1 :: i2 :: i3 :: i4 :: c) rs1 m1 c rs5 m5. +Proof. + intros. apply exec_straight_step with rs2 m2; auto. + eapply exec_straight_three; eauto. +Qed. + +(** * Correctness of ARM constructor functions *) + +(** Properties of comparisons. *) +(* +Lemma compare_float_spec: + forall rs v1 v2, + let rs1 := nextinstr (compare_float rs v1 v2) in + rs1#CR0_0 = Val.cmpf Clt v1 v2 + /\ rs1#CR0_1 = Val.cmpf Cgt v1 v2 + /\ rs1#CR0_2 = Val.cmpf Ceq v1 v2 + /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> + r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. +Proof. + intros. unfold rs1. + split. reflexivity. + split. reflexivity. + split. reflexivity. + intros. rewrite nextinstr_inv; auto. + unfold compare_float. repeat (rewrite Pregmap.gso; auto). +Qed. + +Lemma compare_sint_spec: + forall rs v1 v2, + let rs1 := nextinstr (compare_sint rs v1 v2) in + rs1#CR0_0 = Val.cmp Clt v1 v2 + /\ rs1#CR0_1 = Val.cmp Cgt v1 v2 + /\ rs1#CR0_2 = Val.cmp Ceq v1 v2 + /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> + r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. +Proof. + intros. unfold rs1. + split. reflexivity. + split. reflexivity. + split. reflexivity. + intros. rewrite nextinstr_inv; auto. + unfold compare_sint. repeat (rewrite Pregmap.gso; auto). +Qed. + +Lemma compare_uint_spec: + forall rs v1 v2, + let rs1 := nextinstr (compare_uint rs v1 v2) in + rs1#CR0_0 = Val.cmpu Clt v1 v2 + /\ rs1#CR0_1 = Val.cmpu Cgt v1 v2 + /\ rs1#CR0_2 = Val.cmpu Ceq v1 v2 + /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> + r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. +Proof. + intros. unfold rs1. + split. reflexivity. + split. reflexivity. + split. reflexivity. + intros. rewrite nextinstr_inv; auto. + unfold compare_uint. repeat (rewrite Pregmap.gso; auto). +Qed. +*) + +(** Loading a constant. *) + +Lemma loadimm_correct: + forall r n k rs m, + exists rs', + exec_straight (loadimm r n k) rs m k rs' m + /\ rs'#r = Vint n + /\ 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. +Qed. + +(** Add integer immediate. *) + +Lemma addimm_correct: + forall r1 r2 n k rs m, + exists rs', + exec_straight (addimm r1 r2 n k) rs m k rs' m + /\ rs'#r1 = Val.add rs#r2 (Vint n) + /\ 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. +Qed. + +(* And integer immediate *) + +Lemma andimm_correct: + forall r1 r2 n k rs m, + r2 <> IR14 -> + 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'. +Proof. + intros. unfold andimm. + (* andi *) + case (is_immed_arith n). + exists (nextinstr (rs#r1 <- (Val.and 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. + (* 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. congruence. + auto. + split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. + intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. +Qed. + +(** Other integer 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 -> + 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'. +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. +Qed. + +(** Indexed memory loads. *) + +Lemma loadind_int_correct: + forall (base: ireg) ofs dst (rs: regset) m v k, + Mem.loadv Mint32 m (Val.add rs#base (Vint ofs)) = Some v -> + exists rs', + exec_straight (loadind_int base ofs dst k) rs m k rs' m + /\ rs'#dst = v + /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. +Proof. + intros; unfold loadind_int. destruct (is_immed_mem_word ofs). + exists (nextinstr (rs#dst <- v)). + split. apply exec_straight_one. simpl. + unfold exec_load. rewrite H. auto. auto. + split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. + intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + exploit addimm_correct. 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. 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. +Qed. + +Lemma loadind_float_correct: + forall (base: ireg) ofs dst (rs: regset) m v k, + Mem.loadv Mfloat64 m (Val.add rs#base (Vint ofs)) = Some v -> + exists rs', + exec_straight (loadind_float base ofs dst k) rs m k rs' m + /\ rs'#dst = v + /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. +Proof. + intros; unfold loadind_float. destruct (is_immed_mem_float ofs). + exists (nextinstr (rs#dst <- v)). + split. apply exec_straight_one. simpl. + unfold exec_load. rewrite H. auto. auto. + split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. + intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + 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. + 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. +Qed. + +Lemma loadind_correct: + forall (base: ireg) ofs ty dst k (rs: regset) m v, + Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v -> + mreg_type dst = ty -> + exists rs', + exec_straight (loadind base ofs ty dst k) rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, r <> PC -> r <> IR14 -> r <> preg_of dst -> rs'#r = rs#r. +Proof. + intros. unfold loadind. + assert (preg_of dst <> PC). + unfold preg_of. case (mreg_type dst); discriminate. + unfold preg_of. rewrite H0. destruct ty. + apply loadind_int_correct; auto. + apply loadind_float_correct; auto. +Qed. + +(** Indexed memory stores. *) + +Lemma storeind_int_correct: + forall (base: ireg) ofs (src: ireg) (rs: regset) m m' k, + Mem.storev Mint32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' -> + src <> IR14 -> + exists rs', + exec_straight (storeind_int src base ofs k) rs m k rs' m' + /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. +Proof. + intros; unfold storeind_int. destruct (is_immed_mem_word ofs). + exists (nextinstr rs). + split. apply exec_straight_one. simpl. + unfold exec_store. rewrite H. auto. auto. + intros. rewrite nextinstr_inv; auto. + 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. + rewrite H. auto. + congruence. auto with ppcgen. auto. + intros. rewrite nextinstr_inv; auto. +Qed. + +Lemma storeind_float_correct: + forall (base: ireg) ofs (src: freg) (rs: regset) m m' k, + Mem.storev Mfloat64 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' -> + base <> IR14 -> + exists rs', + exec_straight (storeind_float src base ofs k) rs m k rs' m' + /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. +Proof. + intros; unfold storeind_float. destruct (is_immed_mem_float ofs). + exists (nextinstr rs). + split. apply exec_straight_one. simpl. + unfold exec_store. rewrite H. auto. auto. + intros. rewrite nextinstr_inv; auto. + 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. + rewrite H. auto. + congruence. congruence. auto with ppcgen. auto. + intros. rewrite nextinstr_inv; auto. +Qed. + +Lemma storeind_correct: + forall (base: ireg) ofs ty src k (rs: regset) m m', + Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' -> + mreg_type src = ty -> + base <> IR14 -> + exists rs', + exec_straight (storeind src base ofs ty k) rs m k rs' m' + /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. +Proof. + intros. unfold storeind. unfold preg_of in H. rewrite H0 in H. destruct ty. + apply storeind_int_correct. auto. auto. auto with ppcgen. + apply storeind_float_correct. auto. auto. +Qed. + +(** Translation of shift immediates *) + +Lemma transl_shift_correct: + forall s (r: ireg) (rs: regset), + eval_shift_op (transl_shift s r) rs = eval_shift_total s (rs#r). +Proof. + intros. destruct s; simpl; + unfold eval_shift_total, eval_shift, Val.shl, Val.shr, Val.shru, Val.ror; + rewrite (s_amount_ltu s); auto. +Qed. + +Lemma transl_shift_addr_correct: + forall s (r: ireg) (rs: regset), + eval_shift_addr (transl_shift_addr s r) rs = eval_shift_total s (rs#r). +Proof. + intros. destruct s; simpl; + unfold eval_shift_total, eval_shift, Val.shl, Val.shr, Val.shru, Val.ror; + rewrite (s_amount_ltu s); auto. +Qed. + +(** Translation of conditions *) + +Ltac TypeInv := + match goal with + | H: (List.map ?f ?x = nil) |- _ => + destruct x; [clear H | simpl in H; discriminate] + | H: (List.map ?f ?x = ?hd :: ?tl) |- _ => + destruct x; simpl in H; + [ discriminate | + injection H; clear H; let T := fresh "T" in ( + intros H T; TypeInv) ] + | _ => idtac + end. + +(** Translation of conditions. *) + +Lemma compare_int_spec: + forall rs v1 v2, + let rs1 := nextinstr (compare_int rs v1 v2) in + rs1#CReq = (Val.cmp Ceq v1 v2) + /\ rs1#CRne = (Val.cmp Cne v1 v2) + /\ rs1#CRhs = (Val.cmpu Cge v1 v2) + /\ rs1#CRlo = (Val.cmpu Clt v1 v2) + /\ rs1#CRhi = (Val.cmpu Cgt v1 v2) + /\ rs1#CRls = (Val.cmpu Cle v1 v2) + /\ rs1#CRge = (Val.cmp Cge v1 v2) + /\ rs1#CRlt = (Val.cmp Clt v1 v2) + /\ rs1#CRgt = (Val.cmp Cgt v1 v2) + /\ rs1#CRle = (Val.cmp Cle v1 v2) + /\ forall r', is_data_reg r' -> rs1#r' = rs#r'. +Proof. + intros. unfold rs1. intuition; try reflexivity. + rewrite nextinstr_inv; [unfold compare_int; repeat rewrite Pregmap.gso; auto | idtac]; + red; intro; subst r'; elim H. +Qed. + +Lemma compare_float_spec: + forall rs v1 v2, + let rs' := nextinstr (compare_float rs v1 v2) in + rs'#CReq = (Val.cmpf Ceq v1 v2) + /\ rs'#CRne = (Val.cmpf Cne v1 v2) + /\ rs'#CRmi = (Val.cmpf Clt v1 v2) + /\ rs'#CRpl = (Val.notbool (Val.cmpf Clt v1 v2)) + /\ rs'#CRhi = (Val.notbool (Val.cmpf Cle v1 v2)) + /\ rs'#CRls = (Val.cmpf Cle v1 v2) + /\ rs'#CRge = (Val.cmpf Cge v1 v2) + /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2)) + /\ rs'#CRgt = (Val.cmpf Cgt v1 v2) + /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2)) + /\ forall r', is_data_reg r' -> rs'#r' = rs#r'. +Proof. + intros. unfold rs'. intuition; try reflexivity. + rewrite nextinstr_inv; [unfold compare_float; repeat rewrite Pregmap.gso; auto | idtac]; + red; intro; subst r'; elim H. +Qed. + +Lemma transl_cond_correct: + forall cond args k ms sp rs m b, + map mreg_type args = type_of_condition cond -> + agree ms sp rs -> + eval_condition cond (map ms 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 + /\ agree ms sp rs'. +Proof. + intros. + rewrite <- (eval_condition_weaken _ _ _ H1). clear H1. + destruct cond; simpl in H; TypeInv; simpl. + (* Ccomp *) + generalize (compare_int_spec rs ms#m0 ms#m1). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_int rs ms#m0 ms#m1)). + split. apply exec_straight_one. simpl. + repeat rewrite <- (ireg_val ms sp rs); trivial. + reflexivity. + split. + case c; simpl; auto. + apply agree_exten_1 with rs; auto. + (* Ccompu *) + generalize (compare_int_spec rs ms#m0 ms#m1). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_int rs ms#m0 ms#m1)). + split. apply exec_straight_one. simpl. + repeat rewrite <- (ireg_val ms sp rs); trivial. + reflexivity. + split. + case c; simpl; auto. + apply agree_exten_1 with rs; auto. + (* Ccompshift *) + generalize (compare_int_spec rs ms#m0 (eval_shift_total s ms#m1)). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_int rs ms#m0 (eval_shift_total s ms#m1))). + split. apply exec_straight_one. simpl. + rewrite transl_shift_correct. + repeat rewrite <- (ireg_val ms sp rs); trivial. + reflexivity. + split. + case c; simpl; auto. + apply agree_exten_1 with rs; auto. + (* Ccompushift *) + generalize (compare_int_spec rs ms#m0 (eval_shift_total s ms#m1)). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_int rs ms#m0 (eval_shift_total s ms#m1))). + split. apply exec_straight_one. simpl. + rewrite transl_shift_correct. + repeat rewrite <- (ireg_val ms sp rs); trivial. + reflexivity. + split. + case c; simpl; auto. + apply agree_exten_1 with rs; auto. + (* Ccompimm *) + destruct (is_immed_arith i). + generalize (compare_int_spec rs ms#m0 (Vint i)). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_int rs ms#m0 (Vint i))). + split. apply exec_straight_one. simpl. + rewrite <- (ireg_val ms sp rs); trivial. auto. + split. + case c; simpl; auto. + apply agree_exten_1 with rs; auto. + exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. + assert (AG: agree ms sp rs'). apply agree_exten_2 with rs; auto. + generalize (compare_int_spec rs' ms#m0 (Vint i)). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_int rs' ms#m0 (Vint i))). + split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. + rewrite Q. rewrite <- (ireg_val ms sp rs'); trivial. auto. + split. + case c; simpl; auto. + apply agree_exten_1 with rs'; auto. + (* Ccompuimm *) + destruct (is_immed_arith i). + generalize (compare_int_spec rs ms#m0 (Vint i)). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_int rs ms#m0 (Vint i))). + split. apply exec_straight_one. simpl. + rewrite <- (ireg_val ms sp rs); trivial. auto. + split. + case c; simpl; auto. + apply agree_exten_1 with rs; auto. + exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. + assert (AG: agree ms sp rs'). apply agree_exten_2 with rs; auto. + generalize (compare_int_spec rs' ms#m0 (Vint i)). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_int rs' ms#m0 (Vint i))). + split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. + rewrite Q. rewrite <- (ireg_val ms sp rs'); trivial. auto. + split. + case c; simpl; auto. + apply agree_exten_1 with rs'; auto. + (* Ccompf *) + generalize (compare_float_spec rs ms#m0 ms#m1). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_float rs ms#m0 ms#m1)). + split. apply exec_straight_one. simpl. + repeat rewrite <- (freg_val ms sp rs); trivial. auto. + split. + case c; simpl; auto. + apply agree_exten_1 with rs; auto. + (* Cnotcompf *) + generalize (compare_float_spec rs ms#m0 ms#m1). + intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + exists (nextinstr (compare_float rs ms#m0 ms#m1)). + split. apply exec_straight_one. simpl. + repeat rewrite <- (freg_val ms sp rs); trivial. auto. + split. + case c; simpl; auto. + rewrite Val.negate_cmpf_ne. auto. + rewrite Val.negate_cmpf_eq. auto. + apply agree_exten_1 with rs; auto. +Qed. + +(** Translation of arithmetic operations. *) + +Ltac TranslOpSimpl := + match goal with + | |- exists rs' : regset, + exec_straight ?c ?rs ?m ?k rs' ?m /\ + agree (Regmap.set ?res ?v ?ms) ?sp rs' => + (exists (nextinstr (rs#(ireg_of res) <- v)); + split; + [ apply exec_straight_one; + [ repeat (rewrite (ireg_val ms sp rs); auto); + simpl; try rewrite transl_shift_correct; reflexivity + | reflexivity ] + | auto with ppcgen ]) + || + (exists (nextinstr (rs#(freg_of res) <- v)); + split; + [ apply exec_straight_one; + [ repeat (rewrite (freg_val ms sp rs); auto); reflexivity + | reflexivity ] + | auto with ppcgen ]) + end. + +Lemma transl_op_correct: + forall op args res k ms sp rs m v, + wt_instr (Mop op args res) -> + agree ms sp rs -> + eval_operation ge sp op (map ms args) m = Some v -> + exists rs', + exec_straight (transl_op op args res k) rs m k rs' m + /\ agree (Regmap.set res v ms) sp rs'. +Proof. + intros. rewrite <- (eval_operation_weaken _ _ _ _ _ H1). (*clear H1; clear v.*) + inversion H. + (* Omove *) + simpl. exists (nextinstr (rs#(preg_of res) <- (ms r1))). + split. caseEq (mreg_type r1); intro. + apply exec_straight_one. simpl. rewrite (ireg_val ms sp rs); auto. + simpl. unfold preg_of. rewrite <- H3. rewrite H6. reflexivity. + auto with ppcgen. + apply exec_straight_one. simpl. rewrite (freg_val ms sp rs); auto. + simpl. unfold preg_of. rewrite <- H3. rewrite H6. reflexivity. + auto with ppcgen. + auto with ppcgen. + (* Other instructions *) + clear H2 H3 H5. + destruct op; simpl in H6; injection H6; clear H6; intros; + TypeInv; simpl; try (TranslOpSimpl). + (* Omove again *) + congruence. + (* Ointconst *) + generalize (loadimm_correct (ireg_of res) i k rs m). + intros [rs' [A [B C]]]. + exists rs'. split. auto. + apply agree_set_mireg_exten with rs; auto. +(* + (* Ofloatconst *) + exists (nextinstr (rs#(freg_of res) <- (Vfloat f))). + split. apply exec_straight_one. reflexivity. reflexivity. + auto with ppcgen. + (* Oaddrsymbol *) + change (find_symbol_offset ge i i0) with (symbol_offset ge i i0). + set (v := symbol_offset ge i i0). + pose (rs1 := nextinstr (rs#GPR2 <- (high_half v))). + exists (nextinstr (rs1#(ireg_of res) <- v)). + split. apply exec_straight_two with rs1 m. + unfold exec_instr. rewrite gpr_or_zero_zero. + unfold const_high. rewrite Val.add_commut. + rewrite high_half_zero. reflexivity. + simpl. rewrite gpr_or_zero_not_zero. 2: congruence. + unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. + rewrite Pregmap.gss. + fold v. rewrite Val.add_commut. unfold v. rewrite low_high_half. + reflexivity. reflexivity. reflexivity. + unfold rs1. apply agree_nextinstr. apply agree_set_mireg; auto. + apply agree_set_mreg. apply agree_nextinstr. + apply agree_set_other. auto. simpl. tauto. +*) + (* Oaddrstack *) + generalize (addimm_correct (ireg_of res) IR13 i k rs m). + intros [rs' [EX [RES OTH]]]. + exists rs'. split. auto. + apply agree_set_mireg_exten with rs; auto. + rewrite (sp_val ms sp rs). auto. auto. + (* Ocast8signed *) + set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 24))))). + set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 24))))). + exists rs2. split. + apply exec_straight_two with rs1 m; auto. + simpl. rewrite <- (ireg_val ms sp rs); auto. + unfold rs2. + replace (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 24))) with (Val.sign_ext 8 (ms m0)). + apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. + apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. + unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + destruct (ms m0); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity. + vm_compute; auto. + (* Ocast8unsigned *) + exists (nextinstr (rs#(ireg_of res) <- (Val.and (ms m0) (Vint (Int.repr 255))))). + split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity. + replace (Val.zero_ext 8 (ms m0)) + with (Val.and (ms m0) (Vint (Int.repr 255))). + auto with ppcgen. + destruct (ms m0); simpl; auto. rewrite Int.zero_ext_and. reflexivity. + vm_compute; auto. + (* Ocast16signed *) + set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 16))))). + set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 16))))). + exists rs2. split. + apply exec_straight_two with rs1 m; auto. + simpl. rewrite <- (ireg_val ms sp rs); auto. + unfold rs2. + replace (Val.shr (rs1 (ireg_of res)) (Vint (Int.repr 16))) with (Val.sign_ext 16 (ms m0)). + apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. + apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. + unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + destruct (ms m0); simpl; auto. rewrite Int.sign_ext_shr_shl. reflexivity. + vm_compute; auto. + (* Ocast16unsigned *) + set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shl (ms m0) (Vint (Int.repr 16))))). + set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.shru (rs1 (ireg_of res)) (Vint (Int.repr 16))))). + exists rs2. split. + apply exec_straight_two with rs1 m; auto. + simpl. rewrite <- (ireg_val ms sp rs); auto. + unfold rs2. + replace (Val.shru (rs1 (ireg_of res)) (Vint (Int.repr 16))) with (Val.zero_ext 16 (ms m0)). + apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. + apply agree_set_mireg_twice; auto with ppcgen. auto with ppcgen. + unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + destruct (ms m0); simpl; auto. rewrite Int.zero_ext_shru_shl. reflexivity. + vm_compute; auto. + (* Oaddimm *) + generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m). + intros [rs' [A [B C]]]. + exists rs'. split. auto. + apply agree_set_mireg_exten with rs; auto. + rewrite (ireg_val ms sp rs); auto. + (* Orsbimm *) + exploit (makeimm_correct Prsb (fun v1 v2 => Val.sub v2 v1) (ireg_of res) (ireg_of m0)); + auto with ppcgen. + intros [rs' [A [B C]]]. + exists rs'. + split. eauto. + apply agree_set_mireg_exten with rs; auto. rewrite B. + rewrite <- (ireg_val ms sp rs); auto. + (* Omul *) + destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)). + set (rs1 := nextinstr (rs#IR14 <- (Val.mul (ms m0) (ms m1)))). + set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#IR14))). + exists rs2; split. + apply exec_straight_two with rs1 m; auto. + simpl. repeat rewrite <- (ireg_val ms sp rs); auto. + unfold rs2. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. + apply agree_nextinstr. apply agree_nextinstr_commut. + apply agree_set_mireg; auto. apply agree_set_mreg. apply agree_set_other. auto. + simpl; auto. auto with ppcgen. discriminate. + TranslOpSimpl. + (* Oandimm *) + 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. + apply agree_set_mireg_exten with rs; auto. + rewrite (ireg_val ms sp rs); auto. + (* Oorimm *) + exploit (makeimm_correct Porr Val.or (ireg_of res) (ireg_of m0)); + auto with ppcgen. + intros [rs' [A [B C]]]. + exists rs'. + split. eauto. + apply agree_set_mireg_exten with rs; auto. rewrite B. + rewrite <- (ireg_val ms sp rs); auto. + (* Oxorimm *) + exploit (makeimm_correct Peor Val.xor (ireg_of res) (ireg_of m0)); + auto with ppcgen. + intros [rs' [A [B C]]]. + exists rs'. + split. eauto. + apply agree_set_mireg_exten with rs; auto. rewrite B. + rewrite <- (ireg_val ms sp rs); auto. + (* Oshrximm *) + assert (exists n, ms m0 = Vint n /\ Int.ltu i (Int.repr 31) = true). + simpl in H1. destruct (ms m0); try discriminate. + exists i0; split; auto. destruct (Int.ltu i (Int.repr 31)); discriminate || auto. + destruct H3 as [n [ARG1 LTU]]. + assert (LTU': Int.ltu i (Int.repr 32) = true). + exploit Int.ltu_inv. eexact LTU. intro. + unfold Int.ltu. apply zlt_true. + assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto. + omega. + assert (RSm0: rs (ireg_of m0) = Vint n). + rewrite <- ARG1. symmetry. eapply ireg_val; eauto. + set (islt := Int.lt n Int.zero). + set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero))). + assert (OTH1: forall r', is_data_reg r' -> rs1#r' = rs#r'). + generalize (compare_int_spec rs (Vint n) (Vint Int.zero)). + fold rs1. intros [A B]. intuition. + exploit (addimm_correct IR14 (ireg_of m0) (Int.sub (Int.shl Int.one i) Int.one)). + intros [rs2 [EXEC2 [RES2 OTH2]]]. + set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))). + set (rs4 := nextinstr (rs3#(ireg_of res) <- (Val.shr rs3#IR14 (Vint i)))). + exists rs4; split. + apply exec_straight_step with rs1 m. + simpl. rewrite RSm0. auto. auto. + eapply exec_straight_trans. eexact EXEC2. + apply exec_straight_two with rs3 m. + simpl. rewrite OTH2. change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)). + unfold Val.cmp. change (Int.cmp Cge n Int.zero) with (negb islt). + rewrite OTH2. rewrite OTH1. rewrite RSm0. + unfold rs3. case islt; reflexivity. + apply ireg_of_is_data_reg. decEq; auto with ppcgen. auto with ppcgen. congruence. congruence. + simpl. auto. + auto. unfold rs3. case islt; auto. auto. + (* agreement *) + assert (RES4: rs4#(ireg_of res) = Vint(Int.shrx n i)). + unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gss. + rewrite Int.shrx_shr. fold islt. unfold rs3. + repeat rewrite nextinstr_inv; auto. + case islt. rewrite RES2. rewrite OTH1. rewrite RSm0. + simpl. rewrite LTU'. auto. + apply ireg_of_is_data_reg. + rewrite Pregmap.gss. simpl. rewrite LTU'. auto. congruence. + exact LTU. auto with ppcgen. + assert (OTH4: forall r, is_data_reg r -> r <> ireg_of res -> rs4#r = rs#r). + intros. + assert (r <> PC). red; intro; subst r; elim H3. + assert (r <> IR14). red; intro; subst r; elim H3. + unfold rs4. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + unfold rs3. rewrite nextinstr_inv; auto. + transitivity (rs2 r). + case islt. auto. apply Pregmap.gso; auto. + rewrite OTH2; auto. + apply agree_exten_1 with (rs#(ireg_of res) <- (Val.shrx (ms m0) (Vint i))). + auto with ppcgen. + intros. unfold Pregmap.set. destruct (PregEq.eq r (ireg_of res)). + subst r. rewrite ARG1. simpl. rewrite LTU'. auto. + auto. + (* Ointoffloat *) + exists (nextinstr (rs#(ireg_of res) <- (Val.intoffloat (ms m0)))). + split. apply exec_straight_one. + repeat (rewrite (freg_val ms sp rs); auto). + reflexivity. auto with ppcgen. + (* Ointuoffloat *) + exists (nextinstr (rs#(ireg_of res) <- (Val.intuoffloat (ms m0)))). + split. apply exec_straight_one. + repeat (rewrite (freg_val ms sp rs); auto). + reflexivity. auto with ppcgen. + (* Ofloatofint *) + exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)))). + split. apply exec_straight_one. + repeat (rewrite (ireg_val ms sp rs); auto). + reflexivity. auto 10 with ppcgen. + (* Ofloatofintu *) + exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)))). + split. apply exec_straight_one. + repeat (rewrite (ireg_val ms sp rs); auto). + reflexivity. auto 10 with ppcgen. + (* Ocmp *) + assert (exists b, eval_condition c ms##args m = Some b /\ v = Val.of_bool b). + simpl in H1. destruct (eval_condition c ms##args m). + destruct b; inv H1. exists true; auto. exists false; auto. + discriminate. + destruct H5 as [b [EVC EQ]]. + exploit transl_cond_correct; eauto. intros [rs' [A [B C]]]. + rewrite (eval_condition_weaken _ _ _ EVC). + set (rs1 := nextinstr (rs'#(ireg_of res) <- (Vint Int.zero))). + set (rs2 := nextinstr (if b then (rs1#(ireg_of res) <- Vtrue) else rs1)). + exists rs2; split. + eapply exec_straight_trans. eauto. + apply exec_straight_two with rs1 m; auto. + simpl. replace (rs1 (crbit_for_cond c)) with (Val.of_bool b). + unfold rs2. destruct b; auto. + unfold rs2. destruct b; auto. + apply agree_set_mireg_exten with rs'; auto. + unfold rs2. rewrite nextinstr_inv; auto with ppcgen. + destruct b. apply Pregmap.gss. + unfold rs1. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. + intros. unfold rs2. rewrite nextinstr_inv; auto. + transitivity (rs1 r'). destruct b; auto. rewrite Pregmap.gso; auto. + unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. +Qed. + +Remark val_add_add_zero: + forall v1 v2, Val.add v1 v2 = Val.add (Val.add v1 v2) (Vint Int.zero). +Proof. + intros. destruct v1; destruct v2; simpl; auto; rewrite Int.add_zero; auto. +Qed. + +Lemma transl_load_store_correct: + forall (mk_instr_imm: ireg -> int -> instruction) + (mk_instr_gen: option (ireg -> shift_addr -> instruction)) + (is_immed: int -> bool) + addr args k ms sp rs m ms' m', + (forall (r1: ireg) (rs1: regset) n k, + eval_addressing_total sp addr (map ms args) = Val.add rs1#r1 (Vint n) -> + agree ms sp rs1 -> + exists rs', + exec_straight (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\ + agree ms' sp rs') -> + match mk_instr_gen with + | None => True + | Some mk => + (forall (r1: ireg) (sa: shift_addr) (rs1: regset) k, + eval_addressing_total sp addr (map ms args) = Val.add rs1#r1 (eval_shift_addr sa rs1) -> + agree ms sp rs1 -> + exists rs', + exec_straight (mk r1 sa :: k) rs1 m k rs' m' /\ + agree ms' sp rs') + end -> + agree ms sp rs -> + map mreg_type args = type_of_addressing addr -> + exists rs', + exec_straight (transl_load_store mk_instr_imm mk_instr_gen is_immed addr args k) rs m + k rs' m' + /\ agree ms' sp rs'. +Proof. + intros. destruct addr; simpl in H2; TypeInv; simpl. + (* Aindexed *) + case (is_immed i). + (* Aindexed, small displacement *) + apply H; eauto. simpl. rewrite (ireg_val ms sp rs); auto. + (* Aindexed, large displacement *) + exploit (addimm_correct IR14 (ireg_of t)); eauto with ppcgen. + intros [rs' [A [B C]]]. + exploit (H IR14 rs' Int.zero); eauto. + simpl. rewrite (ireg_val ms sp rs); auto. rewrite B. + rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity. + apply agree_exten_2 with rs; auto. + intros [rs'' [D E]]. + exists rs''; split. + eapply exec_straight_trans. eexact A. eexact D. auto. + (* Aindexed2 *) + destruct mk_instr_gen as [mk | ]. + (* binary form available *) + apply H0; auto. simpl. repeat rewrite (ireg_val ms sp rs); auto. + (* binary form not available *) + set (rs' := nextinstr (rs#IR14 <- (Val.add (ms t) (ms t0)))). + exploit (H IR14 rs' Int.zero); eauto. + simpl. repeat rewrite (ireg_val ms sp rs); auto. + unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + repeat rewrite (ireg_val ms sp rs); auto. apply val_add_add_zero. + unfold rs'; auto with ppcgen. + intros [rs'' [A B]]. + exists rs''; split. + eapply exec_straight_step with (rs2 := rs'); eauto. + simpl. repeat rewrite <- (ireg_val ms sp rs); auto. + auto. + (* Aindexed2shift *) + destruct mk_instr_gen as [mk | ]. + (* binary form available *) + apply H0; auto. simpl. repeat rewrite (ireg_val ms sp rs); auto. + rewrite transl_shift_addr_correct. auto. + (* binary form not available *) + set (rs' := nextinstr (rs#IR14 <- (Val.add (ms t) (eval_shift_total s (ms t0))))). + exploit (H IR14 rs' Int.zero); eauto. + simpl. repeat rewrite (ireg_val ms sp rs); auto. + unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. + repeat rewrite (ireg_val ms sp rs); auto. apply val_add_add_zero. + unfold rs'; auto with ppcgen. + intros [rs'' [A B]]. + exists rs''; split. + eapply exec_straight_step with (rs2 := rs'); eauto. + simpl. rewrite transl_shift_correct. + repeat rewrite <- (ireg_val ms sp rs); auto. + auto. + (* Ainstack *) + destruct (is_immed i). + (* Ainstack, short displacement *) + apply H. simpl. rewrite (sp_val ms sp rs); auto. auto. + (* Ainstack, large displacement *) + exploit (addimm_correct IR14 IR13); eauto with ppcgen. + intros [rs' [A [B C]]]. + exploit (H IR14 rs' Int.zero); eauto. + simpl. rewrite (sp_val ms sp rs); auto. rewrite B. + rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity. + apply agree_exten_2 with rs; auto. + intros [rs'' [D E]]. + exists rs''; split. + eapply exec_straight_trans. eexact A. eexact D. auto. +Qed. + +Lemma transl_load_int_correct: + forall (mk_instr: ireg -> ireg -> shift_addr -> instruction) + (is_immed: int -> bool) + (rd: mreg) addr args k ms sp rs m chunk a v, + (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset), + exec_instr ge c (mk_instr r1 r2 sa) rs1 m = + exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) -> + agree ms sp rs -> + map mreg_type args = type_of_addressing addr -> + mreg_type rd = Tint -> + eval_addressing ge sp addr (map ms args) = Some a -> + Mem.loadv chunk m a = Some v -> + exists rs', + exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m + k rs' m + /\ agree (Regmap.set rd v ms) sp rs'. +Proof. + intros. unfold transl_load_store_int. + exploit eval_addressing_weaken. eauto. intros. + apply transl_load_store_correct with ms; auto. + intros. exists (nextinstr (rs1#(ireg_of rd) <- v)); split. + apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. + unfold exec_load. rewrite H4. auto. auto. + auto with ppcgen. + intros. exists (nextinstr (rs1#(ireg_of rd) <- v)); split. + apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. + unfold exec_load. rewrite H4. auto. auto. + auto with ppcgen. +Qed. + +Lemma transl_load_float_correct: + forall (mk_instr: freg -> ireg -> int -> instruction) + (is_immed: int -> bool) + (rd: mreg) addr args k ms sp rs m chunk a v, + (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset), + exec_instr ge c (mk_instr r1 r2 n) rs1 m = + exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) -> + agree ms sp rs -> + map mreg_type args = type_of_addressing addr -> + mreg_type rd = Tfloat -> + eval_addressing ge sp addr (map ms args) = Some a -> + Mem.loadv chunk m a = Some v -> + exists rs', + exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m + k rs' m + /\ agree (Regmap.set rd v ms) sp rs'. +Proof. + intros. unfold transl_load_store_float. + exploit eval_addressing_weaken. eauto. intros. + apply transl_load_store_correct with ms; auto. + intros. exists (nextinstr (rs1#(freg_of rd) <- v)); split. + apply exec_straight_one. rewrite H. rewrite <- H6. rewrite H5. + unfold exec_load. rewrite H4. auto. auto. + auto with ppcgen. +Qed. + +Lemma transl_store_int_correct: + forall (mk_instr: ireg -> ireg -> shift_addr -> instruction) + (is_immed: int -> bool) + (rd: mreg) addr args k ms sp rs m chunk a m', + (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset), + exec_instr ge c (mk_instr r1 r2 sa) rs1 m = + exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) -> + agree ms sp rs -> + map mreg_type args = type_of_addressing addr -> + mreg_type rd = Tint -> + eval_addressing ge sp addr (map ms args) = Some a -> + Mem.storev chunk m a (ms rd) = Some m' -> + exists rs', + exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m + k rs' m' + /\ agree ms sp rs'. +Proof. + intros. unfold transl_load_store_int. + exploit eval_addressing_weaken. eauto. intros. + apply transl_load_store_correct with ms; auto. + intros. exists (nextinstr rs1); split. + apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. + unfold exec_store. rewrite <- (ireg_val ms sp rs1); auto. + rewrite H4. auto. auto. + auto with ppcgen. + intros. exists (nextinstr rs1); split. + apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. + unfold exec_store. rewrite <- (ireg_val ms sp rs1); auto. + rewrite H4. auto. auto. + auto with ppcgen. +Qed. + +Lemma transl_store_float_correct: + forall (mk_instr: freg -> ireg -> int -> instruction) + (is_immed: int -> bool) + (rd: mreg) addr args k ms sp rs m chunk a m', + (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset), + exec_instr ge c (mk_instr r1 r2 n) rs1 m = + exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) -> + agree ms sp rs -> + map mreg_type args = type_of_addressing addr -> + mreg_type rd = Tfloat -> + eval_addressing ge sp addr (map ms args) = Some a -> + Mem.storev chunk m a (ms rd) = Some m' -> + exists rs', + exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m + k rs' m' + /\ agree ms sp rs'. +Proof. + intros. unfold transl_load_store_float. + exploit eval_addressing_weaken. eauto. intros. + apply transl_load_store_correct with ms; auto. + intros. exists (nextinstr rs1); split. + apply exec_straight_one. rewrite H. simpl. rewrite <- H6. rewrite H5. + unfold exec_store. rewrite <- (freg_val ms sp rs1); auto. + rewrite H4. auto. auto. + auto with ppcgen. +Qed. + +(** Translation of allocations *) + +Lemma transl_alloc_correct: + forall ms sp rs sz m m' blk k, + agree ms sp rs -> + ms Conventions.loc_alloc_argument = Vint sz -> + Mem.alloc m 0 (Int.signed sz) = (m', blk) -> + let ms' := Regmap.set Conventions.loc_alloc_result (Vptr blk Int.zero) ms in + exists rs', + exec_straight (Pallocblock :: k) rs m k rs' m' + /\ agree ms' sp rs'. +Proof. + intros. + pose (rs' := nextinstr (rs#IR0 <- (Vptr blk Int.zero) #IR14 <- (Val.add rs#PC Vone))). + exists rs'; split. + apply exec_straight_one. unfold exec_instr. + generalize (preg_val _ _ _ Conventions.loc_alloc_argument H). + unfold preg_of; intro. simpl in H2. rewrite <- H2. rewrite H0. + rewrite H1. reflexivity. + reflexivity. + unfold ms', rs'. apply agree_nextinstr. apply agree_set_other. + change (IR IR0) with (preg_of Conventions.loc_alloc_result). + apply agree_set_mreg. auto. + simpl. tauto. +Qed. + +End STRAIGHTLINE. + -- cgit