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/Constprop.v | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

(limited to 'backend/Constprop.v')

diff --git a/backend/Constprop.v b/backend/Constprop.v
index cccce9a3..e1ab2e9c 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -121,26 +121,14 @@ Definition transfer (f: function) (pc: node) (before: D.t) :=
   | None => before
   | Some i =>
       match i with
-      | Inop s =>
-          before
       | Iop op args res s =>
           let a := eval_static_operation op (approx_regs before args) in
           D.set res a before
       | Iload chunk addr args dst s =>
           D.set dst Unknown before
-      | Istore chunk addr args src s =>
-          before
       | Icall sig ros args res s =>
           D.set res Unknown before
-      | Itailcall sig ros args =>
-          before
-(*
-      | Ialloc arg res s =>
-          D.set res Unknown before
-*)
-      | Icond cond args ifso ifnot =>
-          before
-      | Ireturn optarg =>
+      | _ =>
           before
       end
   end.
@@ -212,6 +200,15 @@ Definition transf_instr (app: D.t) (instr: instruction) :=
           let (cond', args') := cond_strength_reduction (approx_reg app) cond args in
           Icond cond' args' s1 s2
       end
+  | Ijumptable arg tbl =>
+      match intval (approx_reg app) arg with
+      | Some n =>
+          match list_nth_z tbl (Int.signed n) with
+          | Some s => Inop s
+          | None => instr
+          end
+      | None => instr
+      end
   | _ =>
       instr
   end.
-- 
cgit