diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 14:58:33 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 14:58:33 +0000 |
commit | 8ccc7f2f597aff2c8590c4e62552fb53406ad0f8 (patch) | |
tree | a553844ce1b6960ae5240f65593c085be733e3b2 /powerpc | |
parent | 74487f079dd56663f97f9731cea328931857495c (diff) | |
download | compcert-8ccc7f2f597aff2c8590c4e62552fb53406ad0f8.tar.gz compcert-8ccc7f2f597aff2c8590c4e62552fb53406ad0f8.zip |
More realistic treatment of jump tables: show the absence of overflow when accessing the table
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1172 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-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 |
4 files changed, 51 insertions, 22 deletions
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"; |