summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Asm.v10
-rw-r--r--powerpc/Asmgen.v39
-rw-r--r--powerpc/Asmgenproof.v4
-rw-r--r--powerpc/Asmgenproof1.v144
-rw-r--r--powerpc/ConstpropOp.vp1
-rw-r--r--powerpc/ConstpropOpproof.v2
-rw-r--r--powerpc/Op.v16
-rw-r--r--powerpc/PrintAsm.ml4
-rw-r--r--powerpc/PrintOp.ml2
-rw-r--r--powerpc/SelectOp.vp22
-rw-r--r--powerpc/SelectOpproof.v49
-rw-r--r--powerpc/Unusedglob1.ml2
-rw-r--r--powerpc/extractionMachdep.v1
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".