diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asm.v | 10 | ||||
| -rw-r--r-- | powerpc/Asmgen.v | 39 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 144 | ||||
| -rw-r--r-- | powerpc/ConstpropOp.vp | 1 | ||||
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 2 | ||||
| -rw-r--r-- | powerpc/Op.v | 16 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | powerpc/PrintOp.ml | 2 | ||||
| -rw-r--r-- | powerpc/SelectOp.vp | 22 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v | 49 | ||||
| -rw-r--r-- | powerpc/Unusedglob1.ml | 2 | ||||
| -rw-r--r-- | powerpc/extractionMachdep.v | 1 |
13 files changed, 238 insertions, 58 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index e6e9d76..1441929 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -101,7 +101,9 @@ Inductive constant: Type := | Cint: int -> constant | Csymbol_low: ident -> int -> constant | Csymbol_high: ident -> int -> constant - | Csymbol_sda: ident -> int -> constant. + | Csymbol_sda: ident -> int -> constant + | Csymbol_rel_low: ident -> int -> constant + | Csymbol_rel_high: ident -> int -> constant. (** A note on constants: while immediate operands to PowerPC instructions must be representable in 16 bits (with @@ -422,6 +424,8 @@ Axiom small_data_area_addressing: symbol_is_small_data id ofs = true -> small_data_area_offset ge id ofs = symbol_offset id ofs. +Parameter symbol_is_rel_data: ident -> int -> bool. + (** Armed with the [low_half] and [high_half] functions, we can define the evaluation of a symbolic constant. Note that for [const_high], integer constants @@ -436,6 +440,8 @@ Definition const_low (c: constant) := | Csymbol_low id ofs => low_half (symbol_offset id ofs) | Csymbol_high id ofs => Vundef | Csymbol_sda id ofs => small_data_area_offset ge id ofs + | Csymbol_rel_low id ofs => low_half (symbol_offset id ofs) + | Csymbol_rel_high id ofs => Vundef end. Definition const_high (c: constant) := @@ -444,6 +450,8 @@ Definition const_high (c: constant) := | Csymbol_low id ofs => Vundef | Csymbol_high id ofs => high_half (symbol_offset id ofs) | Csymbol_sda id ofs => Vundef + | Csymbol_rel_low id ofs => Vundef + | Csymbol_rel_high id ofs => high_half (symbol_offset id ofs) end. (** The semantics is purely small-step and defined as a function diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index cc9a51c..b3f0722 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -322,6 +322,11 @@ Definition transl_cond_op (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) +Definition csymbol_high (s: ident) (ofs: int) (rel: bool) := + if rel then Csymbol_rel_high s ofs else Csymbol_high s ofs. +Definition csymbol_low (s: ident) (ofs: int) (rel: bool) := + if rel then Csymbol_rel_low s ofs else Csymbol_low s ofs. + Definition transl_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with @@ -340,8 +345,9 @@ Definition transl_op OK (if symbol_is_small_data s ofs then Paddi r GPR0 (Csymbol_sda s ofs) :: k else - Paddis r GPR0 (Csymbol_high s ofs) :: - Paddi r r (Csymbol_low s ofs) :: k) + let rel := symbol_is_rel_data s ofs in + Paddis r GPR0 (csymbol_high s ofs rel) :: + Paddi r r (csymbol_low s ofs rel) :: k) | Oaddrstack n, nil => do r <- ireg_of res; OK (addimm r GPR1 n k) | Ocast8signed, a1 :: nil => @@ -353,6 +359,18 @@ Definition transl_op OK (Padd r r1 r2 :: k) | Oaddimm n, a1 :: nil => do r1 <- ireg_of a1; do r <- ireg_of res; OK (addimm r r1 n k) + | Oaddsymbol s ofs, a1 :: nil => + do r1 <- ireg_of a1; do r <- ireg_of res; + OK (if symbol_is_small_data s ofs then + Paddi GPR0 GPR0 (Csymbol_sda s ofs) :: + Padd r r1 GPR0 :: k + else if symbol_is_rel_data s ofs then + Paddis GPR0 GPR0 (Csymbol_rel_high s ofs) :: + Padd r r1 GPR0 :: + Paddi r r (Csymbol_rel_low s ofs) :: k + else + Paddis r r1 (Csymbol_high s ofs) :: + Paddi r r (Csymbol_low s ofs) :: k) | Osub, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; OK (Psubfc r r2 r1 :: k) @@ -499,12 +517,21 @@ Definition transl_memory_access OK (if symbol_is_small_data symb ofs then mk1 (Csymbol_sda symb ofs) GPR0 :: k else - Paddis temp GPR0 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k) + let rel := symbol_is_rel_data symb ofs in + Paddis temp GPR0 (csymbol_high symb ofs rel) :: + mk1 (csymbol_low symb ofs rel) temp :: k) | Abased symb ofs, a1 :: nil => do r1 <- ireg_of a1; - OK (Paddis temp r1 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) temp :: k) + OK (if symbol_is_small_data symb ofs then + Paddi GPR0 GPR0 (Csymbol_sda symb ofs) :: + mk2 r1 GPR0 :: k + else if symbol_is_rel_data symb ofs then + Paddis GPR0 GPR0 (Csymbol_rel_high symb ofs) :: + Padd temp r1 GPR0 :: + mk1 (Csymbol_rel_low symb ofs) temp :: k + else + Paddis temp r1 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) temp :: k) | Ainstack ofs, nil => OK (if Int.eq (high_s ofs) Int.zero then mk1 (Cint ofs) GPR1 :: k diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 869fab3..990d35d 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -243,6 +243,8 @@ Opaque Int.eq. unfold transl_op; intros; destruct op; TailNoLabel. destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. destruct (symbol_is_small_data i i0); TailNoLabel. + destruct (symbol_is_small_data i i0); TailNoLabel. + destruct (symbol_is_rel_data i i0); TailNoLabel. destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. eapply transl_cond_op_label; eauto. @@ -259,6 +261,8 @@ Proof. unfold transl_memory_access; intros; destruct addr; TailNoLabel. destruct (Int.eq (high_s i) Int.zero); TailNoLabel. destruct (symbol_is_small_data i i0); TailNoLabel. + destruct (symbol_is_small_data i i0); TailNoLabel. + destruct (symbol_is_rel_data i i0); TailNoLabel. destruct (Int.eq (high_s i) Int.zero); TailNoLabel. Qed. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index cd961c9..d9b6cf3 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -103,6 +103,42 @@ Proof. rewrite Int.sub_idem. apply Int.add_zero. Qed. +Lemma add_zero_symbol_offset: + forall ge id ofs, + Val.add Vzero (symbol_offset ge id ofs) = symbol_offset ge id ofs. +Proof. + unfold symbol_offset; intros. destruct (Genv.find_symbol ge id); auto. + simpl. rewrite Int.add_zero; auto. +Qed. + +Lemma csymbol_high_low: + forall ge id ofs, + Val.add (high_half (symbol_offset ge id ofs)) (low_half (symbol_offset ge id ofs)) + = symbol_offset ge id ofs. +Proof. + intros. rewrite Val.add_commut. apply low_high_half. +Qed. + +Lemma csymbol_high_low_2: + forall ge id ofs rel, + Val.add (const_high ge (csymbol_high id ofs rel)) + (const_low ge (csymbol_low id ofs rel)) = symbol_offset ge id ofs. +Proof. + intros. destruct rel; apply csymbol_high_low. +Qed. + +(* +Lemma csymbol_sda_eq: + forall ge id ofs, + symbol_is_small_data id ofs = true -> + Val.add Vzero (const_low ge (Csymbol_sda id ofs)) = symbol_offset ge id ofs. +Proof. + intros. unfold const_low. rewrite small_data_area_addressing by auto. + unfold symbol_offset. + destruct (Genv.find_symbol ge id); simpl; auto. rewrite Int.add_zero; auto. +Qed. +*) + (** Useful properties of the GPR0 registers. *) Lemma gpr_or_zero_not_zero: @@ -827,17 +863,14 @@ Opaque Int.eq. set (v' := symbol_offset ge i i0). destruct (symbol_is_small_data i i0) eqn:SD. (* small data *) +Opaque Val.add. econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. Simpl. rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. - destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero; auto. + split. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_offset. intros; Simpl. (* not small data *) -Opaque Val.add. econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. Simpl. rewrite gpr_or_zero_zero. - rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. - rewrite (Val.add_commut Vzero). rewrite high_half_zero. - rewrite Val.add_commut. rewrite low_high_half. auto. + split. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. + rewrite Val.add_assoc. rewrite csymbol_high_low_2. apply add_zero_symbol_offset. intros; Simpl. (* Oaddrstack *) destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. @@ -845,6 +878,26 @@ Opaque Val.add. (* Oaddimm *) destruct (addimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. exists rs'; auto with asmgen. + (* Oaddsymbol *) + destruct (symbol_is_small_data i i0) eqn:SD. + (* small data *) + econstructor; split. eapply exec_straight_two; simpl; reflexivity. + split. Simpl. rewrite (Val.add_commut (rs x)). f_equal. + rewrite small_data_area_addressing by auto. apply add_zero_symbol_offset. + intros; Simpl. + destruct (symbol_is_rel_data i i0). + (* relative data *) + econstructor; split. eapply exec_straight_three; simpl; reflexivity. + split. Simpl. rewrite gpr_or_zero_zero. rewrite gpr_or_zero_not_zero by (eauto with asmgen). + Simpl. rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). f_equal. + rewrite Val.add_assoc. rewrite csymbol_high_low. apply add_zero_symbol_offset. + intros; Simpl. + (* absolute data *) + econstructor; split. eapply exec_straight_two; simpl; reflexivity. + split. Simpl. rewrite ! gpr_or_zero_not_zero by (eauto with asmgen). Simpl. + rewrite Val.add_assoc. rewrite (Val.add_commut (rs x)). f_equal. + apply csymbol_high_low. + intros; Simpl. (* Osubimm *) case (Int.eq (high_s i) Int.zero). TranslOpSimpl. @@ -935,12 +988,12 @@ Lemma transl_memory_access_correct: temp <> GPR0 -> (forall cst (r1: ireg) (rs1: regset) k, Val.add (gpr_or_zero rs1 r1) (const_low ge cst) = a -> - (forall r, r <> PC -> r <> temp -> rs1 r = rs r) -> + (forall r, r <> PC -> r <> temp -> r <> GPR0 -> rs1 r = rs r) -> exists rs', exec_straight ge fn (mk1 cst r1 :: k) rs1 m k rs' m' /\ P rs') -> (forall (r1 r2: ireg) (rs1: regset) k, Val.add rs1#r1 rs1#r2 = a -> - (forall r, r <> PC -> r <> temp -> rs1 r = rs r) -> + (forall r, r <> PC -> r <> temp -> r <> GPR0 -> rs1 r = rs r) -> exists rs', exec_straight ge fn (mk2 r1 r2 :: k) rs1 m k rs' m' /\ P rs') -> exists rs', @@ -969,34 +1022,61 @@ Transparent Val.add. (* Aglobal *) destruct (symbol_is_small_data i i0) eqn:SISD; inv TR. (* Aglobal from small data *) - apply MK1. simpl. rewrite small_data_area_addressing; auto. - unfold symbol_address, symbol_offset. - destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero. auto. + apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. + apply add_zero_symbol_offset. auto. (* Aglobal general case *) - set (rs1 := nextinstr (rs#temp <- (const_high ge (Csymbol_high i i0)))). - exploit (MK1 (Csymbol_low i i0) temp rs1 k). + set (rel := symbol_is_rel_data i i0). + set (rs1 := nextinstr (rs#temp <- (const_high ge (csymbol_high i i0 rel)))). + exploit (MK1 (csymbol_low i i0 rel) temp rs1 k). simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. - unfold rs1. Simpl. - unfold const_high, const_low. - rewrite Val.add_commut. rewrite low_high_half. auto. + unfold rs1. Simpl. apply csymbol_high_low_2. intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. unfold exec_instr. rewrite gpr_or_zero_zero. - rewrite Val.add_commut. unfold const_high. - rewrite high_half_zero. - reflexivity. reflexivity. + rewrite Val.add_commut. unfold const_high, csymbol_high. + destruct rel; rewrite high_half_zero; reflexivity. + reflexivity. assumption. assumption. (* Abased *) + destruct (symbol_is_small_data i i0) eqn:SISD. + (* Abased from small data *) + set (rs1 := nextinstr (rs#GPR0 <- (symbol_offset ge i i0))). + exploit (MK2 x GPR0 rs1 k). + unfold rs1; Simpl. apply Val.add_commut. + intros. unfold rs1; Simpl. + intros [rs' [EX' AG']]. + exists rs'; split. apply exec_straight_step with rs1 m. + unfold exec_instr. rewrite gpr_or_zero_zero. f_equal. unfold rs1. f_equal. f_equal. + unfold const_low. rewrite small_data_area_addressing; auto. + apply add_zero_symbol_offset. + reflexivity. + assumption. assumption. + destruct (symbol_is_rel_data i i0). + (* Abased relative *) + set (rs1 := nextinstr (rs#GPR0 <- (const_high ge (Csymbol_rel_high i i0)))). + set (rs2 := nextinstr (rs1#temp <- (Val.add (rs x) (const_high ge (Csymbol_rel_high i i0))))). + exploit (MK1 (Csymbol_rel_low i i0) temp rs2 k). + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. + unfold rs2. Simpl. rewrite Val.add_assoc. simpl. rewrite csymbol_high_low. + apply Val.add_commut. + intros. unfold rs2; Simpl. unfold rs1; Simpl. + intros [rs' [EX' AG']]. + exists rs'. split. apply exec_straight_step with rs1 m. + unfold exec_instr. rewrite gpr_or_zero_zero. + rewrite (Val.add_commut Vzero). unfold const_high. rewrite high_half_zero. auto. + reflexivity. + apply exec_straight_step with rs2 m. + simpl. unfold rs2, rs1. Simpl. + reflexivity. + assumption. assumption. + (* Abased absolute *) set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (const_high ge (Csymbol_high i i0))))). exploit (MK1 (Csymbol_low i i0) temp rs1 k). simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. unfold rs1. Simpl. - rewrite Val.add_assoc. - unfold const_high, const_low. - symmetry. rewrite Val.add_commut. f_equal. f_equal. - rewrite Val.add_commut. rewrite low_high_half. auto. + rewrite Val.add_assoc. simpl. rewrite csymbol_high_low. apply Val.add_commut. intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. @@ -1028,7 +1108,7 @@ Lemma transl_load_correct: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v - /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs' r = rs r. + /\ forall r, r <> PC -> r <> GPR12 -> r <> GPR0 -> r <> preg_of dst -> rs' r = rs r. Proof. intros. assert (BASE: forall mk1 mk2 k' chunk' v', @@ -1043,7 +1123,7 @@ Proof. exists rs', exec_straight ge fn c rs m k' rs' m /\ rs'#(preg_of dst) = v' - /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs' r = rs r). + /\ forall r, r <> PC -> r <> GPR12 -> r <> GPR0 -> r <> preg_of dst -> rs' r = rs r). { intros. eapply transl_memory_access_correct; eauto. congruence. intros. econstructor; split. apply exec_straight_one. @@ -1095,7 +1175,7 @@ Lemma transl_store_correct: Mem.storev chunk m a (rs (preg_of src)) = Some m' -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, r <> PC -> preg_notin r (destroyed_by_store chunk addr) -> rs' r = rs r. + /\ forall r, r <> PC -> r <> GPR0 -> preg_notin r (destroyed_by_store chunk addr) -> rs' r = rs r. Proof. Local Transparent destroyed_by_store. intros. @@ -1119,15 +1199,15 @@ Local Transparent destroyed_by_store. store2 chunk' (preg_of src) r1 r2 rs1 m) -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, r <> PC -> r <> GPR11 /\ r <> GPR12 -> rs' r = rs r). + /\ forall r, r <> PC -> r <> GPR0 -> r <> GPR11 /\ r <> GPR12 -> rs' r = rs r). { intros. eapply transl_memory_access_correct; eauto. intros. econstructor; split. apply exec_straight_one. rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. - intros; Simpl. apply H7; auto. destruct TEMP0; destruct H9; congruence. + intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. intros. econstructor; split. apply exec_straight_one. rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. - intros; Simpl. apply H7; auto. destruct TEMP0; destruct H9; congruence. + intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. } destruct chunk; monadInv H. - (* Mint8signed *) @@ -1150,10 +1230,10 @@ Local Transparent destroyed_by_store. intros. econstructor; split. apply exec_straight_one. simpl. unfold store1. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. Local Transparent destroyed_by_store. - simpl; intros. destruct H4 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. + simpl; intros. destruct H5 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. intros. econstructor; split. apply exec_straight_one. simpl. unfold store2. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. - simpl; intros. destruct H4 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. + simpl; intros. destruct H5 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. - (* Mfloat64 *) apply Mem.storev_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. - (* Mfloat64al32 *) diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index b755b5e..9bee4db 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -89,6 +89,7 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) := | Oaddimm n, I n1 :: nil => I (Int.add n1 n) | Oaddimm n, G s1 n1 :: nil => G s1 (Int.add n1 n) | Oaddimm n, S n1 :: nil => S (Int.add n1 n) + | Oaddsymbol s ofs, I n :: nil => G s (Int.add ofs n) | Osub, I n1 :: I n2 :: nil => I(Int.sub n1 n2) | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2) | Osub, S n1 :: I n2 :: nil => S (Int.sub n1 n2) diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index b7fad69..2aba9c2 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -138,6 +138,8 @@ Proof. rewrite Val.add_assoc; auto. + rewrite shift_symbol_address; auto. + unfold symbol_address. destruct (Genv.find_symbol ge s1); auto. rewrite Val.sub_add_opp. rewrite Val.add_assoc. simpl. rewrite Int.sub_add_opp. auto. diff --git a/powerpc/Op.v b/powerpc/Op.v index 085a098..dbc474e 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -61,6 +61,7 @@ Inductive operation : Type := | Ocast16signed: operation (**r [rd] is 16-bit sign extension of [r1] *) | Oadd: operation (**r [rd = r1 + r2] *) | Oaddimm: int -> operation (**r [rd = r1 + n] *) + | Oaddsymbol: ident -> int -> operation (**r [rd = addr(id + ofs) + r1] *) | Osub: operation (**r [rd = r1 - r2] *) | Osubimm: int -> operation (**r [rd = n - r1] *) | Omul: operation (**r [rd = r1 * r2] *) @@ -183,6 +184,7 @@ Definition eval_operation | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1) | Oadd, v1::v2::nil => Some (Val.add v1 v2) | Oaddimm n, v1::nil => Some (Val.add v1 (Vint n)) + | Oaddsymbol s ofs, v1::nil => Some (Val.add (symbol_address genv s ofs) v1) | Osub, v1::v2::nil => Some (Val.sub v1 v2) | Osubimm n, v1::nil => Some (Val.sub (Vint n) v1) | Omul, v1::v2::nil => Some (Val.mul v1 v2) @@ -276,6 +278,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ocast16signed => (Tint :: nil, Tint) | Oadd => (Tint :: Tint :: nil, Tint) | Oaddimm _ => (Tint :: nil, Tint) + | Oaddsymbol _ _ => (Tint :: nil, Tint) | Osub => (Tint :: Tint :: nil, Tint) | Osubimm _ => (Tint :: nil, Tint) | Omul => (Tint :: Tint :: nil, Tint) @@ -353,6 +356,7 @@ Proof with (try exact I). destruct v0... destruct v0; destruct v1... destruct v0... + unfold symbol_address. destruct (Genv.find_symbol genv i)... destruct v0... destruct v0; destruct v1... simpl. destruct (eq_block b b0)... destruct v0... destruct v0; destruct v1... @@ -650,19 +654,24 @@ Variable ge2: Genv.t F2 V2. Hypothesis agree_on_symbols: forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s. +Remark symbol_address_preserved: + forall s ofs, symbol_address ge2 s ofs = symbol_address ge1 s ofs. +Proof. + unfold symbol_address; intros. rewrite agree_on_symbols; auto. +Qed. + Lemma eval_operation_preserved: forall sp op vl m, eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m. Proof. - intros. destruct op; simpl; auto. - destruct vl; auto. decEq. unfold symbol_address. rewrite agree_on_symbols. auto. + intros. destruct op; simpl; auto; rewrite symbol_address_preserved; auto. Qed. Lemma eval_addressing_preserved: forall sp addr vl, eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl. Proof. - intros. destruct addr; simpl; auto; unfold symbol_address; rewrite agree_on_symbols; auto. + intros. destruct addr; simpl; auto; rewrite symbol_address_preserved; auto. Qed. End GENV_TRANSF. @@ -760,6 +769,7 @@ Proof. inv H4; simpl; auto. apply Values.val_add_inject; auto. apply Values.val_add_inject; auto. + apply Values.val_add_inject; auto. inv H4; inv H2; simpl; auto. econstructor; eauto. rewrite Int.sub_add_l. auto. destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 08438df..e720b6f 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -100,6 +100,10 @@ let constant oc cst = | Diab -> fprintf oc "(%a)@sdarx" symbol_offset (s, camlint_of_coqint n) end + | Csymbol_rel_low(s, n) -> + fprintf oc "(%a)@sdax@l" symbol_offset (s, camlint_of_coqint n) + | Csymbol_rel_high(s, n) -> + fprintf oc "(%a)@sdarx@ha" symbol_offset (s, camlint_of_coqint n) let num_crbit = function | CRbit_0 -> 0 diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index eda41d1..664280f 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -57,6 +57,8 @@ let print_operation reg pp = function | Ocast16signed, [r1] -> fprintf pp "int16signed(%a)" reg r1 | Oadd, [r1;r2] -> fprintf pp "%a + %a" reg r1 reg r2 | Oaddimm n, [r1] -> fprintf pp "%a + %ld" reg r1 (camlint_of_coqint n) + | Oaddsymbol(id, ofs), [r1] -> + fprintf pp "\"%s\" + %ld + %a" (extern_atom id) (camlint_of_coqint ofs) reg r1 | Osub, [r1;r2] -> fprintf pp "%a - %a" reg r1 reg r2 | Osubimm n, [r1] -> fprintf pp "%ld - %a" (camlint_of_coqint n) reg r1 | Omul, [r1;r2] -> fprintf pp "%a * %a" reg r1 reg r2 diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index b0e7c4d..bdb94bd 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -79,25 +79,41 @@ Nondetfunction addimm (n: int) (e: expr) := | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) + | Eop (Oaddsymbol s m) (t ::: Enil) => Eop (Oaddsymbol s (Int.add n m)) (t ::: Enil) | _ => Eop (Oaddimm n) (e ::: Enil) end. +Nondetfunction addsymbol (s: ident) (ofs: int) (e: expr) := + match e with + | Eop (Ointconst n) Enil => Eop (Oaddrsymbol s (Int.add ofs n)) Enil + | Eop (Oaddimm n) (t ::: Enil) => Eop (Oaddsymbol s (Int.add ofs n)) (t ::: Enil) + | _ => Eop (Oaddsymbol s ofs) (e ::: Enil) + end. + Nondetfunction add (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 | t1, Eop (Ointconst n2) Enil => addimm n2 t1 + | Eop (Oaddrsymbol s ofs) Enil, t2 => + addsymbol s ofs t2 + | t1, Eop (Oaddrsymbol s ofs) Enil => + addsymbol s ofs t1 | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) | Eop (Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | Eop (Oaddrsymbol s n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => - Eop Oadd (Eop (Oaddrsymbol s (Int.add n1 n2)) Enil ::: t2 ::: Enil) | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => Eop Oadd (Eop (Oaddrstack (Int.add n1 n2)) Enil ::: t2 ::: Enil) + | Eop (Oaddsymbol s ofs) (t1:::Enil), Eop (Oaddimm n) (t2:::Enil) => + addsymbol s (Int.add ofs n) (Eop Oadd (t1:::t2:::Enil)) + | Eop (Oaddsymbol s ofs) (t1:::Enil), t2 => + addsymbol s ofs (Eop Oadd (t1:::t2:::Enil)) | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) + | t1, Eop (Oaddsymbol s ofs) (t2:::Enil) => + addsymbol s ofs (Eop Oadd (t1:::t2:::Enil)) | _, _ => Eop Oadd (e1:::e2:::Enil) end. @@ -435,7 +451,7 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) := match e with | Eop (Oaddrsymbol s n) Enil => (Aglobal s n, Enil) | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) - | Eop Oadd (Eop (Oaddrsymbol s n) Enil ::: e2 ::: Enil) => (Abased s n, e2:::Enil) + | Eop (Oaddsymbol s n) (e1:::Enil) => (Abased s n, e1:::Enil) | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil) | Eop Oadd (e1:::e2:::Enil) => if can_use_Aindexed2 chunk diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index c0601eb..0cfa707 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -152,6 +152,13 @@ Proof. TrivialExists. Qed. +Remark symbol_address_shift: + forall s ofs n, + symbol_address ge s (Int.add ofs n) = Val.add (symbol_address ge s ofs) (Vint n). +Proof. + unfold symbol_address; intros. destruct (Genv.find_symbol ge s); auto. +Qed. + Theorem eval_addimm: forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)). Proof. @@ -164,34 +171,50 @@ Proof. unfold symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto. rewrite Val.add_assoc. rewrite Int.add_commut. auto. subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto. + subst. rewrite Int.add_commut. rewrite symbol_address_shift. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut. Qed. +Theorem eval_addsymbol: + forall s ofs, unary_constructor_sound (addsymbol s ofs) (Val.add (symbol_address ge s ofs)). +Proof. + red; unfold addsymbol; intros until x. + case (addsymbol_match a); intros; InvEval; simpl; TrivialExists; simpl. + rewrite symbol_address_shift. auto. + rewrite symbol_address_shift. subst x. rewrite Val.add_assoc. f_equal. f_equal. + apply Val.add_commut. +Qed. + Theorem eval_add: binary_constructor_sound add Val.add. Proof. red; intros until y. unfold add; case (add_match a b); intros; InvEval. - rewrite Val.add_commut. apply eval_addimm; auto. - apply eval_addimm; auto. - subst. +- rewrite Val.add_commut. apply eval_addimm; auto. +- apply eval_addimm; auto. +- apply eval_addsymbol; auto. +- rewrite Val.add_commut. apply eval_addsymbol; auto. +- subst. replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2))) with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))). apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. decEq. apply Val.add_permut. - subst. +- subst. replace (Val.add (Val.add v1 (Vint n1)) y) with (Val.add (Val.add v1 y) (Vint n1)). apply eval_addimm. EvalOp. repeat rewrite Val.add_assoc. decEq. apply Val.add_commut. - subst. TrivialExists. - econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. - simpl. rewrite (Val.add_commut v1). rewrite <- Val.add_assoc. decEq; decEq. - unfold symbol_address. destruct (Genv.find_symbol ge s); auto. - subst. TrivialExists. - econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. +- subst. TrivialExists. + econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. simpl. repeat rewrite Val.add_assoc. decEq; decEq. rewrite Val.add_commut. rewrite Val.add_permut. auto. - subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. - TrivialExists. +- replace (Val.add x y) with + (Val.add (symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)). + apply eval_addsymbol; auto. EvalOp. + subst. rewrite symbol_address_shift. rewrite ! Val.add_assoc. f_equal. + rewrite Val.add_permut. f_equal. apply Val.add_commut. +- subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp. +- subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. +- subst. rewrite Val.add_permut. apply eval_addsymbol. EvalOp. +- TrivialExists. Qed. Theorem eval_sub: binary_constructor_sound sub Val.sub. @@ -834,7 +857,7 @@ Proof. intros until v. unfold addressing; case (addressing_match a); intros; InvEval. exists (@nil val). split. eauto with evalexpr. simpl. auto. exists (@nil val). split. eauto with evalexpr. simpl. auto. - exists (v0 :: nil). split. eauto with evalexpr. simpl. congruence. + exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence. exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence. destruct (can_use_Aindexed2 chunk). exists (v1 :: v0 :: nil). split. eauto with evalexpr. simpl. congruence. diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml index c16cd2f..fabac33 100644 --- a/powerpc/Unusedglob1.ml +++ b/powerpc/Unusedglob1.ml @@ -21,6 +21,8 @@ let referenced_constant = function | Csymbol_low(s, ofs) -> [s] | Csymbol_high(s, ofs) -> [s] | Csymbol_sda(s, ofs) -> [s] + | Csymbol_rel_low(s, ofs) -> [s] + | Csymbol_rel_high(s, ofs) -> [s] let referenced_builtin ef = match ef with diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index bc0184e..352d3b5 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -17,6 +17,7 @@ Extract Constant Asm.low_half => "fun _ -> assert false". Extract Constant Asm.high_half => "fun _ -> assert false". Extract Constant Asm.symbol_is_small_data => "C2C.atom_is_small_data". Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false". +Extract Constant Asm.symbol_is_rel_data => "C2C.atom_is_rel_data". (* Suppression of stupidly big equality functions *) Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y". |