From 74487f079dd56663f97f9731cea328931857495c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 10 Nov 2009 12:50:57 +0000
Subject: Added support for jump tables in back end.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/RTLtyping.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'backend/RTLtyping.v')

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 2df9d5d..86f0eaf 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -112,6 +112,11 @@ Inductive wt_instr : instruction -> Prop :=
       valid_successor s1 ->
       valid_successor s2 ->
       wt_instr (Icond cond args s1 s2)
+  | wt_Ijumptable:
+      forall arg tbl,
+      env arg = Tint ->
+      (forall s, In s tbl -> valid_successor s) ->
+      wt_instr (Ijumptable arg tbl)
   | wt_Ireturn: 
       forall optres,
       option_map env optres = funct.(fn_sig).(sig_res) ->
@@ -224,6 +229,9 @@ Definition check_instr (i: instruction) : bool :=
       check_regs args (type_of_condition cond)
       && check_successor s1
       && check_successor s2
+  | Ijumptable arg tbl =>
+      check_reg arg Tint
+      && List.forallb check_successor tbl
   | Ireturn optres =>
       match optres, funct.(fn_sig).(sig_res) with
       | None, None => true
@@ -326,6 +334,10 @@ Proof.
   constructor. apply check_regs_correct; auto.
   apply check_successor_correct; auto.
   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. 
   (* return *)
   constructor. 
   destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate.
@@ -538,6 +550,8 @@ Proof.
   (* Icond *)
   econstructor; eauto.
   econstructor; eauto.
+  (* Ijumptable *)
+  econstructor; eauto.
   (* Ireturn *)
   econstructor; eauto. 
   destruct or; simpl in *.
-- 
cgit v1.2.3