diff options
-rw-r--r-- | backend/LTLintyping.v | 2 | ||||
-rw-r--r-- | backend/LTLtyping.v | 2 | ||||
-rw-r--r-- | backend/Lineartyping.v | 2 | ||||
-rw-r--r-- | backend/Machtyping.v | 1 | ||||
-rw-r--r-- | backend/RTLtyping.v | 6 | ||||
-rw-r--r-- | backend/Tunnelingtyping.v | 3 | ||||
-rw-r--r-- | lib/Coqlib.v | 7 | ||||
-rw-r--r-- | lib/Integers.v | 7 | ||||
-rw-r--r-- | powerpc/Asm.v | 15 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 3 | ||||
-rw-r--r-- | powerpc/Asmgenproof.v | 52 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 3 |
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"; |