aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/LTLintyping.v2
-rw-r--r--backend/LTLtyping.v2
-rw-r--r--backend/Lineartyping.v2
-rw-r--r--backend/Machtyping.v1
-rw-r--r--backend/RTLtyping.v6
-rw-r--r--backend/Tunnelingtyping.v3
-rw-r--r--lib/Coqlib.v7
-rw-r--r--lib/Integers.v7
-rw-r--r--powerpc/Asm.v15
-rw-r--r--powerpc/Asmgen.v3
-rw-r--r--powerpc/Asmgenproof.v52
-rw-r--r--powerpc/PrintAsm.ml3
12 files changed, 78 insertions, 25 deletions
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 6013a17d..10058907 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -15,6 +15,7 @@
Require Import Coqlib.
Require Import Maps.
Require Import AST.
+Require Import Integers.
Require Import Op.
Require Import RTL.
Require Import Locations.
@@ -80,6 +81,7 @@ Inductive wt_instr : instruction -> Prop :=
forall arg tbl,
Loc.type arg = Tint ->
loc_acceptable arg ->
+ list_length_z tbl * 4 <= Int.max_signed ->
wt_instr (Ljumptable arg tbl)
| wt_Lreturn:
forall optres,
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index e62f9287..9a2322c7 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -15,6 +15,7 @@
Require Import Coqlib.
Require Import Maps.
Require Import AST.
+Require Import Integers.
Require Import Op.
Require Import RTL.
Require Import Locations.
@@ -99,6 +100,7 @@ Inductive wt_instr : instruction -> Prop :=
Loc.type arg = Tint ->
loc_acceptable arg ->
(forall lbl, In lbl tbl -> valid_successor lbl) ->
+ list_length_z tbl * 4 <= Int.max_signed ->
wt_instr (Ljumptable arg tbl)
| wt_Lreturn:
forall optres,
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index ba4952bd..1fe77378 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -15,6 +15,7 @@
Require Import Coqlib.
Require Import Maps.
Require Import AST.
+Require Import Integers.
Require Import Op.
Require Import RTL.
Require Import Locations.
@@ -98,6 +99,7 @@ Inductive wt_instr : instruction -> Prop :=
| wt_Ljumptable:
forall arg tbl,
mreg_type arg = Tint ->
+ list_length_z tbl * 4 <= Int.max_signed ->
wt_instr (Ljumptable arg tbl)
| wt_Lreturn:
wt_instr (Lreturn).
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index fe086cb4..8b40001a 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -82,6 +82,7 @@ Inductive wt_instr : instruction -> Prop :=
| wt_Mjumptable:
forall arg tbl,
mreg_type arg = Tint ->
+ list_length_z tbl * 4 <= Int.max_signed ->
wt_instr (Mjumptable arg tbl)
| wt_Mreturn:
wt_instr Mreturn.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 86f0eaf1..d8e2f212 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -116,6 +116,7 @@ Inductive wt_instr : instruction -> Prop :=
forall arg tbl,
env arg = Tint ->
(forall s, In s tbl -> valid_successor s) ->
+ list_length_z tbl * 4 <= Int.max_signed ->
wt_instr (Ijumptable arg tbl)
| wt_Ireturn:
forall optres,
@@ -232,6 +233,7 @@ Definition check_instr (i: instruction) : bool :=
| Ijumptable arg tbl =>
check_reg arg Tint
&& List.forallb check_successor tbl
+ && zle (list_length_z tbl * 4) Int.max_signed
| Ireturn optres =>
match optres, funct.(fn_sig).(sig_res) with
| None, None => true
@@ -336,8 +338,8 @@ Proof.
apply check_successor_correct; auto.
(* jumptable *)
constructor. apply check_reg_correct; auto.
- rewrite List.forallb_forall in H0. intros. apply check_successor_correct; auto.
- intros.
+ rewrite List.forallb_forall in H1. intros. apply check_successor_correct; auto.
+ eapply proj_sumbool_true. eauto.
(* return *)
constructor.
destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate.
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v
index 8990cb44..834e8e18 100644
--- a/backend/Tunnelingtyping.v
+++ b/backend/Tunnelingtyping.v
@@ -76,7 +76,8 @@ Proof.
intros; inv H0; simpl; econstructor; eauto;
try (eapply branch_target_valid; eauto).
intros. exploit list_in_map_inv; eauto. intros [x [A B]]. subst lbl.
- eapply branch_target_valid; eauto.
+ eapply branch_target_valid; eauto.
+ rewrite list_length_z_map. auto.
Qed.
Lemma wt_tunnel_function:
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 7bc4f8bf..02fa7bab 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -648,6 +648,13 @@ Proof.
rewrite list_length_z_cons. omega.
Qed.
+Lemma list_length_z_map:
+ forall (A B: Type) (f: A -> B) (l: list A),
+ list_length_z (map f l) = list_length_z l.
+Proof.
+ induction l. reflexivity. simpl. repeat rewrite list_length_z_cons. congruence.
+Qed.
+
(** Extract the n-th element of a list, as [List.nth_error] does,
but the index [n] is of type [Z]. *)
diff --git a/lib/Integers.v b/lib/Integers.v
index c54b6fe5..625973a0 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -871,6 +871,13 @@ Proof.
apply neg_mul_distr_l.
Qed.
+Theorem mul_signed:
+ forall x y, mul x y = repr (signed x * signed y).
+Proof.
+ intros; unfold mul. apply eqm_samerepr.
+ apply eqm_mult; apply eqm_sym; apply eqm_signed_unsigned.
+Qed.
+
(** ** Properties of binary decompositions *)
Lemma Z_shift_add_bin_decomp:
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 18dc93ab..1582b414 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -298,8 +298,7 @@ lbl: .long 0x43300000, 0x00000000
- [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
as follows:
<<
- rlwinm r12, reg, 2, 0, 29
- addis r12, r12, ha16(lbl)
+ addis r12, reg, ha16(lbl)
lwz r12, lo16(lbl)(r12)
mtctr r12
bctr r12
@@ -307,6 +306,7 @@ lbl: .long 0x43300000, 0x00000000
lbl: .long table[0], table[1], ...
.text
>>
+ Note that [reg] contains 4 times the index of the desired table entry.
*)
Definition code := list instruction.
@@ -624,10 +624,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| Pbtbl r tbl =>
match rs#r with
| Vint n =>
- match list_nth_z tbl (Int.signed n) with
- | None => Error
- | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
- end
+ let pos := Int.signed n in
+ if zeq (Zmod pos 4) 0 then
+ match list_nth_z tbl (pos / 4) with
+ | None => Error
+ | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
+ end
+ else Error
| _ => Error
end
| Pcmplw r1 r2 =>
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 4beabb1c..2c65ca4d 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -503,7 +503,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
transl_cond cond args
(if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k)
| Mjumptable arg tbl =>
- Pbtbl (ireg_of arg) tbl :: k
+ Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) ::
+ Pbtbl GPR12 tbl :: k
| Mreturn =>
Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
Pmtlr GPR12 ::
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 4e45c8ea..a2fc6108 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -1146,21 +1146,47 @@ Proof.
assert (f0 = f) by congruence. subst f0.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
intro WTI. inv WTI.
- pose (rs1 := rs0 # GPR12 <- Vundef # CTR <- Vundef).
- inv AT. simpl in H6.
- assert (rs1 PC = Vptr fb ofs). rewrite H3. reflexivity.
- generalize (functions_transl _ _ H1); intro FN.
- generalize (functions_transl_no_overflow _ _ H1); intro NOOV.
- exploit find_label_goto_label; eauto. intros [rs2 [A [B C]]].
- left; exists (State rs2 m); split.
- apply plus_one. econstructor. symmetry; eauto. eauto.
- eapply find_instr_tail. eauto.
- simpl. rewrite (ireg_val _ _ _ _ AG H4) in H. rewrite H.
- change label with Mach.label; rewrite H0. eexact A.
+ exploit list_nth_z_range; eauto. intro RANGE.
+ assert (SHIFT: Int.signed (Int.rolm n (Int.repr 2) (Int.repr (-4))) = Int.signed n * 4).
+ replace (Int.repr (-4)) with (Int.shl Int.mone (Int.repr 2)).
+ rewrite <- Int.shl_rolm. rewrite Int.shl_mul.
+ rewrite Int.mul_signed.
+ apply Int.signed_repr.
+ split. apply Zle_trans with 0. vm_compute; congruence. omega.
+ omega.
+ vm_compute. reflexivity.
+ vm_compute. apply Int.mkint_eq. auto.
+ inv AT. simpl in H7.
+ set (k1 := Pbtbl GPR12 tbl :: transl_code f c).
+ set (rs1 := nextinstr (rs0 # GPR12 <- (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))))).
+ generalize (functions_transl _ _ H4); intro FN.
+ generalize (functions_transl_no_overflow _ _ H4); intro NOOV.
+ assert (exec_straight tge (transl_function f)
+ (Prlwinm GPR12 (ireg_of arg) (Int.repr 2) (Int.repr (-4)) :: k1) rs0 m
+ k1 rs1 m).
+ apply exec_straight_one.
+ simpl. rewrite <- (ireg_val _ _ _ _ AG H5). rewrite H. reflexivity. reflexivity.
+ exploit exec_straight_steps_2; eauto.
+ intros [ofs' [PC1 CT1]].
+ set (rs2 := rs1 # GPR12 <- Vundef # CTR <- Vundef).
+ assert (PC2: rs2 PC = Vptr fb ofs'). rewrite <- PC1. reflexivity.
+ generalize (find_label_goto_label f lbl rs2 m _ _ _ FIND PC2 H2).
+ intros [rs3 [GOTO [AT3 INV3]]].
+ left; exists (State rs3 m); split.
+ eapply plus_right'.
+ eapply exec_straight_steps_1; eauto.
+ econstructor; eauto.
+ eapply find_instr_tail. unfold k1 in CT1. eauto.
+ unfold exec_instr.
+ change (rs1 GPR12) with (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))).
+Opaque Zmod. Opaque Zdiv.
+ simpl. rewrite SHIFT. rewrite Z_mod_mult. rewrite zeq_true.
+ rewrite Z_div_mult.
+ change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq.
econstructor; eauto.
eapply Mach.find_label_incl; eauto.
- apply agree_exten_2 with rs1; auto.
- unfold rs1. repeat apply agree_set_other; auto with ppcgen.
+ apply agree_exten_2 with rs2; auto.
+ unfold rs2, rs1. repeat apply agree_set_other; auto with ppcgen.
Qed.
Lemma exec_Mreturn_prop:
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index df1b0629..d9c65314 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -263,8 +263,7 @@ let print_instruction oc labels = function
fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl)
| Pbtbl(r, tbl) ->
let lbl = new_label() in
- fprintf oc " rlwinm %a, %a, 2, 0, 29\n" ireg GPR12 ireg r;
- fprintf oc " addis %a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl;
+ fprintf oc " addis %a, %a, %a\n" ireg GPR12 ireg r label_high lbl;
fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12;
fprintf oc " mtctr %a\n" ireg GPR12;
fprintf oc " bctr\n";
generated by cgit (git 2.34.1) at 2024-06-02 21:12:36 +0000