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

6 files changed, 13 insertions, 3 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: