From 8ccc7f2f597aff2c8590c4e62552fb53406ad0f8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Nov 2009 14:58:33 +0000 Subject: 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 --- powerpc/Asmgenproof.v | 52 ++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 39 insertions(+), 13 deletions(-) (limited to 'powerpc/Asmgenproof.v') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 4e45c8e..a2fc610 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: -- cgit v1.2.3