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 --- backend/RTLtyping.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'backend/RTLtyping.v') diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 86f0eaf..d8e2f21 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. -- cgit v1.2.3