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 /backend | |
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 'backend')
-rw-r--r-- | backend/LTLintyping.v | 2 | ||||
-rw-r--r-- | backend/LTLtyping.v | 2 | ||||
-rw-r--r-- | backend/Lineartyping.v | 2 | ||||
-rw-r--r-- | backend/Machtyping.v | 1 | ||||
-rw-r--r-- | backend/RTLtyping.v | 6 | ||||
-rw-r--r-- | backend/Tunnelingtyping.v | 3 |
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: |