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

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";