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: [PATCH] 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
---
.depend | 9 ++-
backend/Allocation.v | 4 ++
backend/Allocproof.v | 6 ++
backend/Alloctyping.v | 2 +
backend/Bounds.v | 1 +
backend/CSE.v | 2 +
backend/CSEproof.v | 7 ++
backend/Constprop.v | 23 +++---
backend/Constpropproof.v | 12 ++++
backend/LTL.v | 9 +++
backend/LTLin.v | 8 +++
backend/LTLintyping.v | 5 ++
backend/LTLtyping.v | 6 ++
backend/Linear.v | 8 +++
backend/Linearize.v | 2 +
backend/Linearizeaux.ml | 2 +
backend/Linearizeproof.v | 12 ++++
backend/Linearizetyping.v | 1 +
backend/Lineartyping.v | 4 ++
backend/Mach.v | 1 +
backend/Machabstr.v | 7 ++
backend/Machabstr2concr.v | 5 ++
backend/Machconcr.v | 8 +++
backend/Machtyping.v | 5 ++
backend/RTL.v | 30 ++++----
backend/RTLgen.v | 17 +++++
backend/RTLgenaux.ml | 50 ++++++++++---
backend/RTLgenproof.v | 83 ++++++++++++++--------
backend/RTLgenspec.v | 75 +++++++++++++++-----
backend/RTLtyping.v | 14 ++++
backend/RTLtypingaux.ml | 2 +
backend/Reload.v | 3 +
backend/Reloadproof.v | 14 ++++
backend/Reloadtyping.v | 6 +-
backend/Stacking.v | 2 +
backend/Stackingproof.v | 9 +++
backend/Stackingtyping.v | 3 +
backend/Tailcallproof.v | 7 ++
backend/Tunneling.v | 2 +
backend/Tunnelingproof.v | 7 ++
backend/Tunnelingtyping.v | 4 +-
common/Switch.v | 143 ++++++++++++++++++++++++++++++++++----
lib/Coqlib.v | 74 ++++++++++++++++++++
lib/Integers.v | 25 +++++++
lib/Ordered.v | 41 ++++++++++-
powerpc/Asm.v | 50 +++++++++----
powerpc/Asmgen.v | 10 +--
powerpc/Asmgenproof.v | 67 ++++++++++++++----
powerpc/PrintAsm.ml | 25 +++++--
49 files changed, 767 insertions(+), 145 deletions(-)
diff --git a/.depend b/.depend
index 9edeabd67..a0539b0b7 100644
--- a/.depend
+++ b/.depend
@@ -5,18 +5,17 @@ lib/Integers.vo: lib/Integers.v lib/Coqlib.vo
lib/Iteration.vo: lib/Iteration.v lib/Coqlib.vo
lib/Lattice.vo: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo
lib/Maps.vo: lib/Maps.v lib/Coqlib.vo
-lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo
+lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo
lib/Parmov.vo: lib/Parmov.v lib/Coqlib.vo
lib/UnionFind.vo: lib/UnionFind.v lib/Coqlib.vo
common/AST.vo: common/AST.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo
-common/Determinism2.vo: common/Determinism2.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo
common/Determinism.vo: common/Determinism.v lib/Coqlib.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo
common/Errors.vo: common/Errors.v lib/Coqlib.vo
common/Events.vo: common/Events.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo
common/Globalenvs.vo: common/Globalenvs.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo
common/Mem.vo: common/Mem.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo
common/Smallstep.vo: common/Smallstep.v lib/Coqlib.vo common/AST.vo common/Events.vo common/Globalenvs.vo lib/Integers.vo
-common/Switch.vo: common/Switch.v lib/Coqlib.vo lib/Integers.vo
+common/Switch.vo: common/Switch.v lib/Coqlib.vo lib/Integers.vo lib/Ordered.vo
common/Values.vo: common/Values.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo
$(ARCH)/$(VARIANT)/Conventions.vo: $(ARCH)/$(VARIANT)/Conventions.v lib/Coqlib.vo common/AST.vo backend/Locations.vo
$(ARCH)/$(VARIANT)/Stacklayout.vo: $(ARCH)/$(VARIANT)/Stacklayout.v lib/Coqlib.vo backend/Bounds.vo
@@ -27,6 +26,7 @@ $(ARCH)/Asmgen.vo: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo c
$(ARCH)/Asm.vo: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/$(VARIANT)/Conventions.vo
$(ARCH)/ConstpropOpproof.vo: $(ARCH)/ConstpropOpproof.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo $(ARCH)/ConstpropOp.vo backend/Constprop.vo
$(ARCH)/ConstpropOp.vo: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo
+$(ARCH)/extractionMachdep.vo: $(ARCH)/extractionMachdep.v
$(ARCH)/Machregs.vo: $(ARCH)/Machregs.v lib/Coqlib.vo lib/Maps.vo common/AST.vo
$(ARCH)/Op.vo: $(ARCH)/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo
$(ARCH)/SelectOpproof.vo: $(ARCH)/SelectOpproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo $(ARCH)/Op.vo backend/CminorSel.vo $(ARCH)/SelectOp.vo
@@ -56,6 +56,7 @@ backend/LTLin.vo: backend/LTLin.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/In
backend/LTLtyping.vo: backend/LTLtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/RTL.vo backend/Locations.vo backend/LTL.vo $(ARCH)/$(VARIANT)/Conventions.vo
backend/LTL.vo: backend/LTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo
backend/Machabstr2concr.vo: backend/Machabstr2concr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/Machabstr.vo backend/Machconcr.vo $(ARCH)/Asmgenretaddr.vo
+backend/Machabstrblock.vo: backend/Machabstrblock.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Mem.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Mach.vo backend/Machabstr.vo $(ARCH)/$(VARIANT)/Stacklayout.vo
backend/Machabstr.vo: backend/Machabstr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Mem.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo
backend/Machconcr.vo: backend/Machconcr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo
backend/Machtyping.vo: backend/Machtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Mem.vo lib/Integers.vo common/Values.vo common/Events.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Conventions.vo backend/Mach.vo backend/Machabstr.vo
@@ -80,6 +81,8 @@ backend/Tailcall.vo: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo
backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo
backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo
backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo lib/UnionFind.vo common/AST.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/LTL.vo
+cfrontend/Cmedium.saved.vo: cfrontend/Cmedium.saved.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
+cfrontend/Cmedium.vo: cfrontend/Cmedium.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
cfrontend/Cminorgenproof.vo: cfrontend/Cminorgenproof.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csharpminor.vo $(ARCH)/Op.vo backend/Cminor.vo cfrontend/Cminorgen.vo common/Switch.vo
cfrontend/Cminorgen.vo: cfrontend/Cminorgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Mem.vo cfrontend/Csharpminor.vo $(ARCH)/Op.vo backend/Cminor.vo
cfrontend/Csem.vo: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Mem.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo
diff --git a/backend/Allocation.v b/backend/Allocation.v
index 7d843e579..b802f4ac7 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -103,6 +103,8 @@ Definition transfer
reg_list_live args (reg_sum_live ros Regset.empty)
| Icond cond args ifso ifnot =>
reg_list_live args after
+ | Ijumptable arg tbl =>
+ reg_live arg after
| Ireturn optarg =>
reg_option_live optarg Regset.empty
end
@@ -167,6 +169,8 @@ Definition transf_instr
Ltailcall sig (sum_left_map assign ros) (List.map assign args)
| Icond cond args ifso ifnot =>
Lcond cond (List.map assign args) ifso ifnot
+ | Ijumptable arg tbl =>
+ Ljumptable (assign arg) tbl
| Ireturn optarg =>
Lreturn (option_map assign optarg)
end.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index fc0a0f3c6..10eaa5b1a 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -683,6 +683,12 @@ Proof.
eapply exec_Lcond_false; eauto. TranslInstr.
MatchStates. eapply agree_reg_list_live. eauto.
+ (* Ijumptable *)
+ assert (rs#arg = ls (assign arg)). apply AG. apply Regset.add_1. auto.
+ econstructor; split.
+ eapply exec_Ljumptable; eauto. TranslInstr. congruence.
+ MatchStates. eapply list_nth_z_in; eauto. eapply agree_reg_live; eauto.
+
(* Ireturn *)
econstructor; split.
eapply exec_Lreturn; eauto. TranslInstr; eauto.
diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v
index aba966010..260297f2c 100644
--- a/backend/Alloctyping.v
+++ b/backend/Alloctyping.v
@@ -141,6 +141,8 @@ Proof.
rewrite transf_unroll; auto.
(* cond *)
WT.
+ (* jumptable *)
+ WT.
(* return *)
WT.
rewrite transf_unroll; simpl.
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 8c5f536da..15468c574 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -106,6 +106,7 @@ Definition regs_of_instr (i: instruction) : list mreg :=
| Llabel lbl => nil
| Lgoto lbl => nil
| Lcond cond args lbl => nil
+ | Ljumptable arg tbl => nil
| Lreturn => nil
end.
diff --git a/backend/CSE.v b/backend/CSE.v
index ff8d41aa4..98b7bbf58 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -350,6 +350,8 @@ Definition transfer (f: function) (pc: node) (before: numbering) :=
empty_numbering
| Icond cond args ifso ifnot =>
before
+ | Ijumptable arg tbl =>
+ before
| Ireturn optarg =>
before
end
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 14027bf09..7f9424647 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -916,6 +916,13 @@ Proof.
eapply analysis_correct_1; eauto. simpl; auto.
unfold transfer; rewrite H; auto.
+ (* Icond false *)
+ econstructor; split.
+ eapply exec_Ijumptable; eauto.
+ econstructor; eauto.
+ eapply analysis_correct_1; eauto. simpl. eapply list_nth_z_in; eauto.
+ unfold transfer; rewrite H; auto.
+
(* Ireturn *)
econstructor; split.
eapply exec_Ireturn; eauto.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index cccce9a3e..e1ab2e9c0 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.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index dadb192fe..fff9a60da 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -390,6 +390,18 @@ Proof.
simpl; auto.
unfold transfer; rewrite H; auto.
+ (* Ijumptable *)
+ exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split.
+ caseEq (intval (approx_reg (analyze f)!!pc) arg); intros.
+ exploit intval_correct; eauto. eexact MATCH. intro VRS.
+ eapply exec_Inop; eauto. TransfInstr. rewrite H2.
+ replace i with n by congruence. rewrite H1. auto.
+ eapply exec_Ijumptable; eauto. TransfInstr. rewrite H2. auto.
+ constructor; auto.
+ eapply analyze_correct_1; eauto.
+ simpl. eapply list_nth_z_in; eauto.
+ unfold transfer; rewrite H; auto.
+
(* Ireturn *)
exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split.
eapply exec_Ireturn; eauto. TransfInstr; auto.
diff --git a/backend/LTL.v b/backend/LTL.v
index 2505566fa..6a693361b 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -42,6 +42,7 @@ Inductive instruction: Type :=
| Lcall: signature -> loc + ident -> list loc -> loc -> node -> instruction
| Ltailcall: signature -> loc + ident -> list loc -> instruction
| Lcond: condition -> list loc -> node -> node -> instruction
+ | Ljumptable: loc -> list node -> instruction
| Lreturn: option loc -> instruction.
Definition code: Type := PTree.t instruction.
@@ -206,6 +207,13 @@ Inductive step: state -> trace -> state -> Prop :=
eval_condition cond (map rs args) = Some false ->
step (State s f sp pc rs m)
E0 (State s f sp ifnot rs m)
+ | exec_Ljumptable:
+ forall s f sp pc rs m arg tbl n pc',
+ (fn_code f)!pc = Some(Ljumptable arg tbl) ->
+ rs arg = Vint n ->
+ list_nth_z tbl (Int.signed n) = Some pc' ->
+ step (State s f sp pc rs m)
+ E0 (State s f sp pc' rs m)
| exec_Lreturn:
forall s f stk pc rs m or,
(fn_code f)!pc = Some(Lreturn or) ->
@@ -263,6 +271,7 @@ Definition successors_instr (i: instruction) : list node :=
| Lcall sig ros args res s => s :: nil
| Ltailcall sig ros args => nil
| Lcond cond args ifso ifnot => ifso :: ifnot :: nil
+ | Ljumptable arg tbl => tbl
| Lreturn optarg => nil
end.
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 10b7d8323..e3533388e 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -50,6 +50,7 @@ Inductive instruction: Type :=
| Llabel: label -> instruction
| Lgoto: label -> instruction
| Lcond: condition -> list loc -> label -> instruction
+ | Ljumptable: loc -> list label -> instruction
| Lreturn: option loc -> instruction.
Definition code: Type := list instruction.
@@ -204,6 +205,13 @@ Inductive step: state -> trace -> state -> Prop :=
eval_condition cond (map rs args) = Some false ->
step (State s f sp (Lcond cond args lbl :: b) rs m)
E0 (State s f sp b rs m)
+ | exec_Ljumptable:
+ forall s f sp arg tbl b rs m n lbl b',
+ rs arg = Vint n ->
+ list_nth_z tbl (Int.signed n) = Some lbl ->
+ find_label lbl f.(fn_code) = Some b' ->
+ step (State s f sp (Ljumptable arg tbl :: b) rs m)
+ E0 (State s f sp b' rs m)
| exec_Lreturn:
forall s f stk rs m or b,
step (State s f (Vptr stk Int.zero) (Lreturn or :: b) rs m)
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index 9f3f5896b..6013a17df 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -76,6 +76,11 @@ Inductive wt_instr : instruction -> Prop :=
List.map Loc.type args = type_of_condition cond ->
locs_acceptable args ->
wt_instr (Lcond cond args lbl)
+ | wt_Ljumptable:
+ forall arg tbl,
+ Loc.type arg = Tint ->
+ loc_acceptable arg ->
+ wt_instr (Ljumptable arg tbl)
| wt_Lreturn:
forall optres,
option_map Loc.type optres = funsig.(sig_res) ->
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 0461c9af5..e62f9287f 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -94,6 +94,12 @@ Inductive wt_instr : instruction -> Prop :=
locs_acceptable args ->
valid_successor s1 -> valid_successor s2 ->
wt_instr (Lcond cond args s1 s2)
+ | wt_Ljumptable:
+ forall arg tbl,
+ Loc.type arg = Tint ->
+ loc_acceptable arg ->
+ (forall lbl, In lbl tbl -> valid_successor lbl) ->
+ wt_instr (Ljumptable arg tbl)
| wt_Lreturn:
forall optres,
option_map Loc.type optres = funct.(fn_sig).(sig_res) ->
diff --git a/backend/Linear.v b/backend/Linear.v
index e025407a8..bf21cb7dc 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -46,6 +46,7 @@ Inductive instruction: Type :=
| Llabel: label -> instruction
| Lgoto: label -> instruction
| Lcond: condition -> list mreg -> label -> instruction
+ | Ljumptable: mreg -> list label -> instruction
| Lreturn: instruction.
Definition code: Type := list instruction.
@@ -293,6 +294,13 @@ Inductive step: state -> trace -> state -> Prop :=
eval_condition cond (reglist rs args) = Some false ->
step (State s f sp (Lcond cond args lbl :: b) rs m)
E0 (State s f sp b rs m)
+ | exec_Ljumptable:
+ forall s f sp arg tbl b rs m n lbl b',
+ rs (R arg) = Vint n ->
+ list_nth_z tbl (Int.signed n) = Some lbl ->
+ find_label lbl f.(fn_code) = Some b' ->
+ step (State s f sp (Ljumptable arg tbl :: b) rs m)
+ E0 (State s f sp b' rs m)
| exec_Lreturn:
forall s f stk b rs m,
step (State s f (Vptr stk Int.zero) (Lreturn :: b) rs m)
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 431fe1720..31d0318cc 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -190,6 +190,8 @@ Definition linearize_instr (b: LTL.instruction) (k: code) : code :=
Lcond (negate_condition cond) args s2 :: add_branch s1 k
else
Lcond cond args s1 :: add_branch s2 k
+ | LTL.Ljumptable arg tbl =>
+ Ljumptable arg tbl :: k
| LTL.Lreturn or =>
Lreturn or :: k
end.
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index b27386052..1f4e5fac5 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -96,6 +96,8 @@ let basic_blocks f joins =
| Ltailcall (sig0, ros, args) -> end_block blk minpc
| Lcond (cond, args, ifso, ifnot) ->
end_block blk minpc; start_block ifso; start_block ifnot
+ | Ljumptable(arg, tbl) ->
+ end_block blk minpc; List.iter start_block tbl
| Lreturn optarg -> end_block blk minpc
(* next_in_block: check if join point and either extend block
or start block *)
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index e35fb11be..c79908d67 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -639,6 +639,18 @@ Proof.
traceEq.
econstructor; eauto.
+ (* Ljumptable *)
+ destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
+ simpl in EQ. subst c.
+ assert (REACH': (reachable f)!!pc' = true).
+ eapply reachable_successors; eauto. simpl. eapply list_nth_z_in; eauto.
+ exploit find_label_lin_succ; eauto.
+ inv WTI. apply H6. eapply list_nth_z_in; eauto.
+ intros [c'' AT'].
+ econstructor; split.
+ apply plus_one. eapply exec_Ljumptable; eauto.
+ econstructor; eauto.
+
(* Lreturn *)
destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
simpl in EQ. subst c.
diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v
index 627c878f0..716b66f13 100644
--- a/backend/Linearizetyping.v
+++ b/backend/Linearizetyping.v
@@ -60,6 +60,7 @@ Proof.
apply wt_add_branch; auto.
constructor; auto. apply wt_add_branch; auto.
apply wt_add_instr. constructor; auto. auto.
+ apply wt_add_instr. constructor; auto. auto.
Qed.
Lemma wt_linearize_body:
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 33b570b91..ba4952bd5 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -95,6 +95,10 @@ Inductive wt_instr : instruction -> Prop :=
forall cond args lbl,
List.map mreg_type args = type_of_condition cond ->
wt_instr (Lcond cond args lbl)
+ | wt_Ljumptable:
+ forall arg tbl,
+ mreg_type arg = Tint ->
+ wt_instr (Ljumptable arg tbl)
| wt_Lreturn:
wt_instr (Lreturn).
diff --git a/backend/Mach.v b/backend/Mach.v
index 0bb24428c..f7e85c3ef 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -61,6 +61,7 @@ Inductive instruction: Type :=
| Mlabel: label -> instruction
| Mgoto: label -> instruction
| Mcond: condition -> list mreg -> label -> instruction
+ | Mjumptable: mreg -> list label -> instruction
| Mreturn: instruction.
Definition code := list instruction.
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index aa17cd44b..a2630a2b8 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -282,6 +282,13 @@ Inductive step: state -> trace -> state -> Prop :=
eval_condition cond rs##args = Some false ->
step (State s f sp (Mcond cond args lbl :: c) rs fr m)
E0 (State s f sp c rs fr m)
+ | exec_Mjumptable:
+ forall s f sp arg tbl c rs fr m n lbl c',
+ rs arg = Vint n ->
+ list_nth_z tbl (Int.signed n) = Some lbl ->
+ find_label lbl f.(fn_code) = Some c' ->
+ step (State s f sp (Mjumptable arg tbl :: c) rs fr m)
+ E0 (State s f sp c' rs fr m)
| exec_Mreturn:
forall s f stk soff c rs fr m,
step (State s f (Vptr stk soff) (Mreturn :: c) rs fr m)
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index 139eac75c..89529fd4b 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -842,6 +842,11 @@ Proof.
eapply exec_Mcond_false; eauto.
econstructor; eauto.
+ (* Mjumptable *)
+ econstructor; split.
+ eapply exec_Mjumptable; eauto.
+ econstructor; eauto.
+
(* Mreturn *)
assert (WTF: wt_function f) by (inv WTS; auto).
econstructor; split.
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index 876f558c8..84ae0a4fd 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -204,6 +204,14 @@ Inductive step: state -> trace -> state -> Prop :=
eval_condition cond rs##args = Some false ->
step (State s f sp (Mcond cond args lbl :: c) rs m)
E0 (State s f sp c rs m)
+ | exec_Mjumptable:
+ forall s fb f sp arg tbl c rs m n lbl c',
+ rs arg = Vint n ->
+ list_nth_z tbl (Int.signed n) = Some lbl ->
+ Genv.find_funct_ptr ge fb = Some (Internal f) ->
+ find_label lbl f.(fn_code) = Some c' ->
+ step (State s fb sp (Mjumptable arg tbl :: c) rs m)
+ E0 (State s fb sp c' rs m)
| exec_Mreturn:
forall s fb stk soff c rs m f,
Genv.find_funct_ptr ge fb = Some (Internal f) ->
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index ef59e6f06..fe086cb4f 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -79,6 +79,10 @@ Inductive wt_instr : instruction -> Prop :=
forall cond args lbl,
List.map mreg_type args = type_of_condition cond ->
wt_instr (Mcond cond args lbl)
+ | wt_Mjumptable:
+ forall arg tbl,
+ mreg_type arg = Tint ->
+ wt_instr (Mjumptable arg tbl)
| wt_Mreturn:
wt_instr Mreturn.
@@ -280,6 +284,7 @@ Proof.
apply is_tail_find_label with lbl; congruence.
apply is_tail_find_label with lbl; congruence.
+ apply is_tail_find_label with lbl; congruence.
econstructor; eauto.
diff --git a/backend/RTL.v b/backend/RTL.v
index 5de073ee5..b2ee80fc2 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -75,6 +75,10 @@ Inductive instruction: Type :=
[cond] over the values of registers [args]. If the condition
is true, it transitions to [ifso]. If the condition is false,
it transitions to [ifnot]. *)
+ | Ijumptable: reg -> list node -> instruction
+ (** [Ijumptable arg tbl] transitions to the node that is the [n]-th
+ element of the list [tbl], where [n] is the signed integer
+ value of register [arg]. *)
| Ireturn: option reg -> instruction.
(** [Ireturn] terminates the execution of the current function
(it has no successor). It returns the value of the given
@@ -252,6 +256,13 @@ Inductive step: state -> trace -> state -> Prop :=
eval_condition cond rs##args = Some false ->
step (State s c sp pc rs m)
E0 (State s c sp ifnot rs m)
+ | exec_Ijumptable:
+ forall s c sp pc rs m arg tbl n pc',
+ c!pc = Some(Ijumptable arg tbl) ->
+ rs#arg = Vint n ->
+ list_nth_z tbl (Int.signed n) = Some pc' ->
+ step (State s c sp pc rs m)
+ E0 (State s c sp pc' rs m)
| exec_Ireturn:
forall s c stk pc rs m or,
c!pc = Some(Ireturn or) ->
@@ -339,30 +350,13 @@ Definition successors_instr (i: instruction) : list node :=
| Icall sig ros args res s => s :: nil
| Itailcall sig ros args => nil
| Icond cond args ifso ifnot => ifso :: ifnot :: nil
+ | Ijumptable arg tbl => tbl
| Ireturn optarg => nil
end.
Definition successors (f: function) : PTree.t (list node) :=
PTree.map (fun pc i => successors_instr i) f.(fn_code).
-(*
-Definition successors (f: function) (pc: node) : list node :=
- match f.(fn_code)!pc with
- | None => nil
- | Some i =>
- match i with
- | Inop s => s :: nil
- | Iop op args res s => s :: nil
- | Iload chunk addr args dst s => s :: nil
- | Istore chunk addr args src s => s :: nil
- | Icall sig ros args res s => s :: nil
- | Itailcall sig ros args => nil
- | Icond cond args ifso ifnot => ifso :: ifnot :: nil
- | Ireturn optarg => nil
- end
- end.
-*)
-
(** Transformation of a RTL function instruction by instruction.
This applies a given transformation function to all instructions
of a function and constructs a transformed function from that. *)
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 39add9861..942dc50b6 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -474,6 +474,15 @@ Definition transl_exit (nexits: list node) (n: nat) : mon node :=
| Some ne => ret ne
end.
+Fixpoint transl_jumptable (nexits: list node) (tbl: list nat) : mon (list node) :=
+ match tbl with
+ | nil => ret nil
+ | t1 :: tl =>
+ do n1 <- transl_exit nexits t1;
+ do nl <- transl_jumptable nexits tl;
+ ret (n1 :: nl)
+ end.
+
Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
{struct t} : mon node :=
match t with
@@ -487,6 +496,14 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree)
do n2 <- transl_switch r nexits t2;
do n1 <- transl_switch r nexits t1;
add_instr (Icond (Ccompuimm Clt key) (r :: nil) n1 n2)
+ | CTjumptable ofs sz tbl t' =>
+ do rt <- new_reg;
+ do ttbl <- transl_jumptable nexits tbl;
+ do n1 <- add_instr (Ijumptable rt ttbl);
+ do n2 <- transl_switch r nexits t';
+ do n3 <- add_instr (Icond (Ccompuimm Clt sz) (rt :: nil) n1 n2);
+ let op := if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs) in
+ add_instr (Iop op (r :: nil) rt n3)
end.
(** Translation of statements. [transl_stmt map s nd nexits nret rret]
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index 4c1fc05c0..7e42c80d1 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -27,16 +27,16 @@ module IntOrd =
module IntSet = Set.Make(IntOrd)
let normalize_table tbl =
- let rec norm seen = function
- | [] -> []
+ let rec norm keys accu = function
+ | [] -> (accu, keys)
| Datatypes.Coq_pair(key, act) :: rem ->
- if IntSet.mem key seen
- then norm seen rem
- else (key, act) :: norm (IntSet.add key seen) rem
- in norm IntSet.empty tbl
+ if IntSet.mem key keys
+ then norm keys accu rem
+ else norm (IntSet.add key keys) ((key, act) :: accu) rem
+ in norm IntSet.empty [] tbl
-let compile_switch default table =
- let sw = Array.of_list (normalize_table table) in
+let compile_switch_as_tree default tbl =
+ let sw = Array.of_list tbl in
Array.stable_sort (fun (n1, _) (n2, _) -> IntOrd.compare n1 n2) sw;
let rec build lo hi minval maxval =
match hi - lo with
@@ -70,3 +70,37 @@ let compile_switch default table =
build lo mid minval (Integers.Int.sub pivot Integers.Int.one),
build mid hi pivot maxval)
in build 0 (Array.length sw) Integers.Int.zero Integers.Int.max_unsigned
+
+let uint64_of_coqint n = (* force unsigned interpretation *)
+ Int64.logand (Int64.of_int32 (camlint_of_coqint n)) 0xFFFF_FFFFL
+
+let compile_switch_as_jumptable default cases minkey maxkey =
+ let tblsize = 1 + Int64.to_int (Int64.sub maxkey minkey) in
+ assert (tblsize >= 0 && tblsize <= Sys.max_array_length);
+ let tbl = Array.make tblsize default in
+ List.iter
+ (fun (key, act) ->
+ let pos = Int64.to_int (Int64.sub (uint64_of_coqint key) minkey) in
+ tbl.(pos) <- act)
+ cases;
+ CTjumptable(coqint_of_camlint (Int64.to_int32 minkey),
+ coqint_of_camlint (Int32.of_int tblsize),
+ Array.to_list tbl,
+ CTaction default)
+
+let dense_enough (numcases: int) (minkey: int64) (maxkey: int64) =
+ let span = Int64.sub maxkey minkey in
+ assert (span >= 0L);
+ let tree_size = Int64.mul 4L (Int64.of_int numcases)
+ and table_size = Int64.add 8L span in
+ numcases >= 7 (* really small jump tables are less efficient *)
+ && span < Int64.of_int Sys.max_array_length
+ && table_size <= tree_size
+
+let compile_switch default table =
+ let (tbl, keys) = normalize_table table in
+ let minkey = uint64_of_coqint (IntSet.min_elt keys)
+ and maxkey = uint64_of_coqint (IntSet.max_elt keys) in
+ if dense_enough (List.length tbl) minkey maxkey
+ then compile_switch_as_jumptable default tbl minkey maxkey
+ else compile_switch_as_tree default tbl
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index df1ade9dd..d07bd0814 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -419,37 +419,65 @@ Qed.
(** Correctness of the translation of [switch] statements *)
Lemma transl_switch_correct:
- forall cs sp rs m i code r nexits t ns,
- tr_switch code r nexits t ns ->
+ forall cs sp e m code map r nexits t ns,
+ tr_switch code map r nexits t ns ->
+ forall rs i act,
rs#r = Vint i ->
- exists nd,
- star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs m) /\
- nth_error nexits (comptree_match i t) = Some nd.
+ map_wf map ->
+ match_env map e nil rs ->
+ comptree_match i t = Some act ->
+ exists nd, exists rs',
+ star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\
+ nth_error nexits act = Some nd /\
+ match_env map e nil rs'.
Proof.
- induction 1; intros; simpl.
- exists n. split. apply star_refl. auto.
-
- caseEq (Int.eq i key); intros.
- exists nfound; split.
+ induction 1; simpl; intros.
+(* action *)
+ inv H3. exists n; exists rs; intuition.
+ apply star_refl.
+(* ifeq *)
+ caseEq (Int.eq i key); intro EQ; rewrite EQ in H5.
+ inv H5. exists nfound; exists rs; intuition.
apply star_one. eapply exec_Icond_true; eauto.
- simpl. rewrite H2. congruence. auto.
- exploit IHtr_switch; eauto. intros [nd [EX MATCH]].
- exists nd; split.
+ simpl. rewrite H2. congruence.
+ exploit IHtr_switch; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
+ exists nd1; exists rs1; intuition.
eapply star_step. eapply exec_Icond_false; eauto.
simpl. rewrite H2. congruence. eexact EX. traceEq.
- auto.
-
- caseEq (Int.ltu i key); intros.
- exploit IHtr_switch1; eauto. intros [nd [EX MATCH]].
- exists nd; split.
+(* iflt *)
+ caseEq (Int.ltu i key); intro EQ; rewrite EQ in H5.
+ exploit IHtr_switch1; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
+ exists nd1; exists rs1; intuition.
eapply star_step. eapply exec_Icond_true; eauto.
simpl. rewrite H2. congruence. eexact EX. traceEq.
- auto.
- exploit IHtr_switch2; eauto. intros [nd [EX MATCH]].
- exists nd; split.
+ exploit IHtr_switch2; eauto. intros [nd1 [rs1 [EX [NTH ME]]]].
+ exists nd1; exists rs1; intuition.
eapply star_step. eapply exec_Icond_false; eauto.
simpl. rewrite H2. congruence. eexact EX. traceEq.
- auto.
+(* jumptable *)
+ set (rs1 := rs#rt <- (Vint(Int.sub i ofs))).
+ assert (ME1: match_env map e nil rs1).
+ unfold rs1. eauto with rtlg.
+ assert (EX1: step tge (State cs code sp n rs m) E0 (State cs code sp n1 rs1 m)).
+ eapply exec_Iop; eauto.
+ predSpec Int.eq Int.eq_spec ofs Int.zero; simpl.
+ rewrite H10. rewrite Int.sub_zero_l. congruence.
+ rewrite H6. rewrite <- Int.sub_add_opp. auto.
+ caseEq (Int.ltu (Int.sub i ofs) sz); intro EQ; rewrite EQ in H9.
+ exploit H5; eauto. intros [nd [A B]].
+ exists nd; exists rs1; intuition.
+ eapply star_step. eexact EX1.
+ eapply star_step. eapply exec_Icond_true; eauto.
+ simpl. unfold rs1. rewrite Regmap.gss. congruence.
+ apply star_one. eapply exec_Ijumptable; eauto. unfold rs1. apply Regmap.gss.
+ reflexivity. traceEq.
+ exploit (IHtr_switch rs1); eauto. unfold rs1. rewrite Regmap.gso; auto.
+ intros [nd [rs' [EX [NTH ME]]]].
+ exists nd; exists rs'; intuition.
+ eapply star_step. eexact EX1.
+ eapply star_step. eapply exec_Icond_false; eauto.
+ simpl. unfold rs1. rewrite Regmap.gss. congruence.
+ eexact EX. reflexivity. traceEq.
Qed.
(** ** Semantic preservation for the translation of expressions *)
@@ -530,8 +558,6 @@ Definition transl_condition_prop
/\ match_env map e le rs'
/\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r).
-
-
(** The correctness of the translation is a huge induction over
the Cminor evaluation derivation for the source program. To keep
the proof manageable, we put each case of the proof in a separate
@@ -1194,15 +1220,16 @@ Proof.
econstructor; eauto. econstructor; eauto.
(* switch *)
- inv TS.
+ inv TS.
+ exploit validate_switch_correct; eauto. intro CTM.
exploit transl_expr_correct; eauto.
intros [rs' [A [B [C D]]]].
exploit transl_switch_correct; eauto.
- intros [nd [E F]].
+ intros [nd [rs'' [E [F G]]]].
econstructor; split.
right; split. eapply star_trans. eexact A. eexact E. traceEq. Lt_state.
- econstructor; eauto.
- rewrite (validate_switch_correct _ _ _ H3 n). constructor. auto.
+ econstructor; eauto.
+ constructor. auto.
(* return none *)
inv TS.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index caf93c836..037eb3fb1 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -713,22 +713,36 @@ Definition tr_store_optvar (c: code) (map: mapping)
(** Auxiliary for the compilation of [switch] statements. *)
+Definition tr_jumptable (nexits: list node) (tbl: list nat) (ttbl: list node) : Prop :=
+ forall v act,
+ list_nth_z tbl v = Some act ->
+ exists n, list_nth_z ttbl v = Some n /\ nth_error nexits act = Some n.
+
Inductive tr_switch
- (c: code) (r: reg) (nexits: list node):
+ (c: code) (map: mapping) (r: reg) (nexits: list node):
comptree -> node -> Prop :=
| tr_switch_action: forall act n,
nth_error nexits act = Some n ->
- tr_switch c r nexits (CTaction act) n
+ tr_switch c map r nexits (CTaction act) n
| tr_switch_ifeq: forall key act t' n ncont nfound,
- tr_switch c r nexits t' ncont ->
+ tr_switch c map r nexits t' ncont ->
nth_error nexits act = Some nfound ->
c!n = Some(Icond (Ccompimm Ceq key) (r :: nil) nfound ncont) ->
- tr_switch c r nexits (CTifeq key act t') n
+ tr_switch c map r nexits (CTifeq key act t') n
| tr_switch_iflt: forall key t1 t2 n n1 n2,
- tr_switch c r nexits t1 n1 ->
- tr_switch c r nexits t2 n2 ->
+ tr_switch c map r nexits t1 n1 ->
+ tr_switch c map r nexits t2 n2 ->
c!n = Some(Icond (Ccompuimm Clt key) (r :: nil) n1 n2) ->
- tr_switch c r nexits (CTiflt key t1 t2) n.
+ tr_switch c map r nexits (CTiflt key t1 t2) n
+ | tr_switch_jumptable: forall ofs sz tbl t n n1 n2 n3 rt ttbl,
+ ~reg_in_map map rt -> rt <> r ->
+ c!n = Some(Iop (if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs))
+ (r ::nil) rt n1) ->
+ c!n1 = Some(Icond (Ccompuimm Clt sz) (rt :: nil) n2 n3) ->
+ c!n2 = Some(Ijumptable rt ttbl) ->
+ tr_switch c map r nexits t n3 ->
+ tr_jumptable nexits tbl ttbl ->
+ tr_switch c map r nexits (CTjumptable ofs sz tbl t) n.
(** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c],
starting at node [ns], contains instructions that perform the Cminor
@@ -786,7 +800,7 @@ Inductive tr_stmt (c: code) (map: mapping):
| tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t,
validate_switch default cases t = true ->
tr_expr c map nil a ns n r ->
- tr_switch c r nexits t n ->
+ tr_switch c map r nexits t n ->
tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret
| tr_Sreturn_none: forall nret nd nexits ngoto,
tr_stmt c map (Sreturn None) nret nd nexits ngoto nret None
@@ -1000,9 +1014,9 @@ Qed.
Lemma tr_switch_incr:
forall s1 s2, state_incr s1 s2 ->
- forall r nexits t ns,
- tr_switch s1.(st_code) r nexits t ns ->
- tr_switch s2.(st_code) r nexits t ns.
+ forall map r nexits t ns,
+ tr_switch s1.(st_code) map r nexits t ns ->
+ tr_switch s2.(st_code) map r nexits t ns.
Proof.
induction 2; econstructor; eauto with rtlg.
Qed.
@@ -1051,24 +1065,47 @@ Proof.
destruct (nth_error nexits n); intro; monadInv H. auto.
Qed.
+Lemma transl_jumptable_charact:
+ forall nexits tbl s nl s' incr,
+ transl_jumptable nexits tbl s = OK nl s' incr ->
+ tr_jumptable nexits tbl nl /\ s' = s.
+Proof.
+ induction tbl; intros.
+ monadInv H. split. red. simpl. intros. discriminate. auto.
+ monadInv H. exploit transl_exit_charact; eauto. intros [A B].
+ exploit IHtbl; eauto. intros [C D].
+ split. red. simpl. intros. destruct (zeq v 0). inv H. exists x; auto. auto.
+ congruence.
+Qed.
+
Lemma transl_switch_charact:
- forall r nexits t s ns s' incr,
+ forall map r nexits t s ns s' incr,
+ map_valid map s -> reg_valid r s ->
transl_switch r nexits t s = OK ns s' incr ->
- tr_switch s'.(st_code) r nexits t ns.
+ tr_switch s'.(st_code) map r nexits t ns.
Proof.
induction t; simpl; intros.
exploit transl_exit_charact; eauto. intros [A B].
econstructor; eauto.
- monadInv H.
+ monadInv H1.
exploit transl_exit_charact; eauto. intros [A B]. subst s1.
econstructor; eauto with rtlg.
apply tr_switch_incr with s0; eauto with rtlg.
- monadInv H.
+ monadInv H1.
econstructor; eauto with rtlg.
apply tr_switch_incr with s1; eauto with rtlg.
apply tr_switch_incr with s0; eauto with rtlg.
+
+ monadInv H1.
+ exploit transl_jumptable_charact; eauto. intros [A B]. subst s1.
+ econstructor. eauto with rtlg.
+ apply sym_not_equal. apply valid_fresh_different with s; eauto with rtlg.
+ eauto with rtlg. eauto with rtlg. eauto with rtlg.
+ apply tr_switch_incr with s3. eauto with rtlg.
+ eapply IHt with (s := s2); eauto with rtlg.
+ auto.
Qed.
Lemma transl_stmt_charact:
@@ -1091,8 +1128,9 @@ Proof.
apply tr_expr_incr with s3; eauto with rtlg.
eapply transl_expr_charact; eauto with rtlg.
(* Scall *)
- assert (state_incr s0 s3) by eauto with rtlg.
- assert (state_incr s3 s6) by eauto with rtlg.
+ assert (state_incr s0 s2) by eauto with rtlg.
+ assert (state_incr s2 s4) by eauto with rtlg.
+ assert (state_incr s4 s6) by eauto with rtlg.
econstructor; eauto with rtlg.
eapply transl_expr_charact; eauto with rtlg.
apply tr_exprlist_incr with s6. auto.
@@ -1101,7 +1139,6 @@ Proof.
apply regs_valid_cons; eauto with rtlg.
apply regs_valid_incr with s1; eauto with rtlg.
apply regs_valid_cons; eauto with rtlg.
- apply regs_valid_incr with s2; eauto with rtlg.
apply tr_store_optvar_incr with s4; eauto with rtlg.
eapply store_optvar_charact; eauto with rtlg.
(* Stailcall *)
@@ -1149,7 +1186,7 @@ Proof.
econstructor; eauto with rtlg.
eapply transl_expr_charact; eauto with rtlg.
apply tr_switch_incr with s1; auto with rtlg.
- eapply transl_switch_charact; eauto with rtlg.
+ eapply transl_switch_charact with (s := s0); eauto with rtlg.
monadInv TR.
(* Sreturn *)
destruct o; destruct rret; inv TR.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 2df9d5df8..86f0eaf10 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 *.
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index cc7edf491..406ca07a9 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -87,6 +87,8 @@ let type_instr retty (Coq_pair(pc, i)) =
end
| Icond(cond, args, _, _) ->
set_types args (type_of_condition cond)
+ | Ijumptable(arg, _) ->
+ set_type arg Tint
| Ireturn(optres) ->
begin match optres, retty with
| None, None -> ()
diff --git a/backend/Reload.v b/backend/Reload.v
index 621e75b57..5728a6283 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -242,6 +242,9 @@ Definition transf_instr
| LTLin.Lcond cond args lbl =>
let rargs := regs_for args in
add_reloads args rargs (Lcond cond rargs lbl :: k)
+ | LTLin.Ljumptable arg tbl =>
+ let rarg := reg_for arg in
+ add_reload arg rarg (Ljumptable rarg tbl :: k)
| LTLin.Lreturn None =>
Lreturn :: k
| LTLin.Lreturn (Some loc) =>
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index a7becc36c..21d5f3806 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -1257,6 +1257,20 @@ Proof.
econstructor; eauto with coqlib.
apply agree_exten with ls; auto.
+ (* Ljumptable *)
+ ExploitWT; inv WTI.
+ exploit add_reload_correct_2.
+ intros [ls2 [A [B [C D]]]].
+ left; econstructor; split.
+ eapply plus_right. eauto. eapply exec_Ljumptable; eauto.
+ assert (Val.lessdef (rs arg) (ls arg)). apply AG. auto.
+ rewrite H in H2. inv H2. congruence.
+ apply find_label_transf_function; eauto.
+ traceEq.
+ econstructor; eauto with coqlib.
+ apply agree_exten with ls; auto.
+ eapply LTLin.find_label_is_tail; eauto.
+
(* Lreturn *)
ExploitWT; inv WTI.
destruct or; simpl.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 375bbfde7..df0715ee7 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -35,7 +35,7 @@ Require Import Reloadproof.
Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove
wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall
- wt_Llabel wt_Lgoto wt_Lcond wt_Lreturn: reloadty.
+ wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty.
Remark wt_code_cons:
forall f i c, wt_instr f i -> wt_code f c -> wt_code f (i :: c).
@@ -295,6 +295,10 @@ Proof.
eauto with reloadty.
auto with reloadty.
+ assert (mreg_type (reg_for arg) = Loc.type arg).
+ eauto with reloadty.
+ auto with reloadty.
+
destruct optres; simpl in *; auto with reloadty.
apply wt_add_reload; auto with reloadty.
unfold loc_result. rewrite <- H1.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 182c32269..5d9cf3747 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -185,6 +185,8 @@ Definition transl_instr
Mgoto lbl :: k
| Lcond cond args lbl =>
Mcond cond args lbl :: k
+ | Ljumptable arg tbl =>
+ Mjumptable arg tbl :: k
| Lreturn =>
restore_callee_save fe
(Mreturn :: k)
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 5b6f2dc7b..ba4295895 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1510,6 +1510,15 @@ Proof.
rewrite <- (agree_eval_regs _ _ _ _ _ _ _ args AG) in H; auto.
econstructor; eauto with coqlib.
+ (* Ljumptable *)
+ econstructor; split.
+ apply plus_one; eapply exec_Mjumptable.
+ rewrite <- (agree_eval_reg _ _ _ _ _ _ _ arg AG) in H; eauto.
+ eauto.
+ apply transl_find_label; eauto.
+ econstructor; eauto.
+ eapply find_label_incl; eauto.
+
(* Lreturn *)
exploit restore_callee_save_correct; eauto.
intros [ls' [A [B C]]].
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index 1bafc35b1..8ba5caedb 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -185,6 +185,9 @@ Proof.
(* cond *)
apply wt_instrs_cons; auto.
constructor; auto.
+ (* jumptable *)
+ apply wt_instrs_cons; auto.
+ constructor; auto.
(* return *)
apply wt_restore_callee_save. apply wt_instrs_cons. constructor. auto.
Qed.
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 1423e1e01..8681d84ad 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -630,6 +630,13 @@ Proof.
apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto.
constructor; auto.
+(* jumptable *)
+ TransfInstr.
+ left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'); split.
+ eapply exec_Ijumptable; eauto.
+ generalize (RLD arg). rewrite H0. intro. inv H2. auto.
+ constructor; auto.
+
(* return *)
TransfInstr.
left. exists (Returnstate s' (regmap_optget or Vundef rs') (free m' stk)); split.
diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index ef55a1572..3ad8c4d05 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -106,6 +106,8 @@ Definition tunnel_instr (uf: U.t) (b: instruction) : instruction :=
Ltailcall sig ros args
| Lcond cond args s1 s2 =>
Lcond cond args (U.repr uf s1) (U.repr uf s2)
+ | Ljumptable arg tbl =>
+ Ljumptable arg (List.map (U.repr uf) tbl)
| Lreturn or =>
Lreturn or
end.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index eccb62dd4..92ec68cf7 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -315,6 +315,13 @@ Proof.
eapply exec_Lcond_false; eauto.
rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
econstructor; eauto.
+ (* jumptable *)
+ generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
+ left; econstructor; split.
+ eapply exec_Ljumptable.
+ rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
+ eauto. rewrite list_nth_z_map. change U.elt with node. rewrite H1. reflexivity.
+ econstructor; eauto.
(* return *)
generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A.
left; econstructor; split.
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v
index 91745dfbe..8990cb44a 100644
--- a/backend/Tunnelingtyping.v
+++ b/backend/Tunnelingtyping.v
@@ -74,7 +74,9 @@ Lemma wt_tunnel_instr:
wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr (record_gotos f) i).
Proof.
intros; inv H0; simpl; econstructor; eauto;
- eapply branch_target_valid; 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.
Qed.
Lemma wt_tunnel_function:
diff --git a/common/Switch.v b/common/Switch.v
index 179d4d2ee..ee8f6aa8f 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -13,12 +13,18 @@
(* *)
(* *********************************************************************)
-(** Multi-way branches (``[switch]'') and their compilation
- to 2-way comparison trees. *)
+(** Multi-way branches (``switch'' statements) and their compilation
+ to comparison trees. *)
Require Import EqNat.
+Require Import FMaps.
+Require FMapAVL.
Require Import Coqlib.
Require Import Integers.
+Require Import Ordered.
+
+Module IntMap := FMapAVL.Make(OrderedInt).
+Module IntMapF := FMapFacts.Facts(IntMap).
(** A multi-way branch is composed of a list of (key, action) pairs,
plus a default action. *)
@@ -33,22 +39,29 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: table)
if Int.eq n key then action else switch_target n dfl rem
end.
-(** Multi-way branches are translated to a 2-way comparison tree.
- Each node of the tree performs an equality test or a less-than
- test against one of the keys. *)
+(** Multi-way branches are translated to comparison trees.
+ Each node of the tree performs either
+- an equality against one of the keys;
+- or a "less than" test against one of the keys;
+- or a computed branch (jump table) against a range of key values. *)
Inductive comptree : Type :=
| CTaction: nat -> comptree
| CTifeq: int -> nat -> comptree -> comptree
- | CTiflt: int -> comptree -> comptree -> comptree.
+ | CTiflt: int -> comptree -> comptree -> comptree
+ | CTjumptable: int -> int -> list nat -> comptree -> comptree.
-Fixpoint comptree_match (n: int) (t: comptree) {struct t}: nat :=
+Fixpoint comptree_match (n: int) (t: comptree) {struct t}: option nat :=
match t with
- | CTaction act => act
+ | CTaction act => Some act
| CTifeq key act t' =>
- if Int.eq n key then act else comptree_match n t'
+ if Int.eq n key then Some act else comptree_match n t'
| CTiflt key t1 t2 =>
if Int.ltu n key then comptree_match n t1 else comptree_match n t2
+ | CTjumptable ofs sz tbl t' =>
+ if Int.ltu (Int.sub n ofs) sz
+ then list_nth_z tbl (Int.signed (Int.sub n ofs))
+ else comptree_match n t'
end.
(** The translation from a table to a comparison tree is performed
@@ -80,12 +93,32 @@ Fixpoint split_eq (pivot: int) (cases: table)
else (same, (key, act) :: others)
end.
+Fixpoint split_between (ofs sz: int) (cases: table)
+ {struct cases} : IntMap.t nat * table :=
+ match cases with
+ | nil => (IntMap.empty nat, nil)
+ | (key, act) :: rem =>
+ let (inside, outside) := split_between ofs sz rem in
+ if Int.ltu (Int.sub key ofs) sz
+ then (IntMap.add key act inside, outside)
+ else (inside, (key, act) :: outside)
+ end.
+
Definition refine_low_bound (v lo: Z) :=
if zeq v lo then lo + 1 else lo.
Definition refine_high_bound (v hi: Z) :=
if zeq v hi then hi - 1 else hi.
+Fixpoint validate_jumptable (cases: IntMap.t nat) (default: nat)
+ (tbl: list nat) (n: int) {struct tbl} : bool :=
+ match tbl with
+ | nil => true
+ | act :: rem =>
+ beq_nat act (match IntMap.find n cases with Some a => a | None => default end)
+ && validate_jumptable cases default rem (Int.add n Int.one)
+ end.
+
Fixpoint validate (default: nat) (cases: table) (t: comptree)
(lo hi: Z) {struct t} : bool :=
match t with
@@ -112,6 +145,15 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree)
validate default lcases t1 lo (Int.unsigned pivot - 1)
&& validate default rcases t2 (Int.unsigned pivot) hi
end
+ | CTjumptable ofs sz tbl t' =>
+ let tbl_len := list_length_z tbl in
+ match split_between ofs sz cases with
+ | (inside, outside) =>
+ zle (Int.unsigned sz) tbl_len
+ && zle tbl_len Int.max_signed
+ && validate_jumptable inside default tbl ofs
+ && validate default outside t' lo hi
+ end
end.
Definition validate_switch (default: nat) (cases: table) (t: comptree) :=
@@ -163,11 +205,78 @@ Proof.
auto.
Qed.
+Lemma split_between_prop:
+ forall v default ofs sz cases inside outside,
+ split_between ofs sz cases = (inside, outside) ->
+ switch_target v default cases =
+ (if Int.ltu (Int.sub v ofs) sz
+ then match IntMap.find v inside with Some a => a | None => default end
+ else switch_target v default outside).
+Proof.
+ induction cases; intros until outside; simpl.
+ intros. inv H. simpl. destruct (Int.ltu (Int.sub v ofs) sz); auto.
+ destruct a as [key act]. case_eq (split_between ofs sz cases). intros ins outs SEQ.
+ rewrite (IHcases _ _ SEQ).
+ case_eq (Int.ltu (Int.sub key ofs) sz); intros; inv H0; simpl.
+ rewrite IntMapF.add_o.
+ predSpec Int.eq Int.eq_spec v key.
+ subst v. rewrite H. rewrite dec_eq_true. auto.
+ rewrite dec_eq_false; auto.
+ case_eq (Int.ltu (Int.sub v ofs) sz); intros; auto.
+ predSpec Int.eq Int.eq_spec v key.
+ subst v. congruence.
+ auto.
+Qed.
+
+Lemma validate_jumptable_correct_rec:
+ forall cases default tbl base v,
+ validate_jumptable cases default tbl base = true ->
+ 0 <= Int.signed v < list_length_z tbl -> Int.signed v <= Int.max_signed ->
+ list_nth_z tbl (Int.signed v) =
+ Some(match IntMap.find (Int.add base v) cases with Some a => a | None => default end).
+Proof.
+ induction tbl; intros until v; simpl.
+ unfold list_length_z; simpl. intros. omegaContradiction.
+ rewrite list_length_z_cons. intros. destruct (andb_prop _ _ H). clear H.
+ generalize (beq_nat_eq _ _ (sym_equal H2)). clear H2. intro. subst a.
+ destruct (zeq (Int.signed v) 0).
+ rewrite Int.add_signed. rewrite e. rewrite Zplus_0_r. rewrite Int.repr_signed. auto.
+ assert (Int.signed (Int.sub v Int.one) = Int.signed v - 1).
+ rewrite Int.sub_signed. change (Int.signed Int.one) with 1.
+ apply Int.signed_repr. split. apply Zle_trans with 0.
+ vm_compute; congruence. omega. omega.
+ replace (Int.add base v) with (Int.add (Int.add base Int.one) (Int.sub v Int.one)).
+ rewrite <- IHtbl. rewrite H. auto. auto. rewrite H. omega.
+ rewrite H. omega.
+ rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite Int.add_assoc.
+ replace (Int.add Int.one (Int.neg Int.one)) with Int.zero.
+ rewrite Int.add_zero. apply Int.add_commut.
+ apply Int.mkint_eq. reflexivity.
+Qed.
+
+Lemma validate_jumptable_correct:
+ forall cases default tbl ofs v sz,
+ validate_jumptable cases default tbl ofs = true ->
+ Int.ltu (Int.sub v ofs) sz = true ->
+ Int.unsigned sz <= list_length_z tbl <= Int.max_signed ->
+ list_nth_z tbl (Int.signed (Int.sub v ofs)) =
+ Some(match IntMap.find v cases with Some a => a | None => default end).
+Proof.
+ intros.
+ exploit Int.ltu_range_test; eauto. omega. intros.
+ rewrite (validate_jumptable_correct_rec cases default tbl ofs).
+ rewrite Int.sub_add_opp. rewrite Int.add_permut. rewrite <- Int.sub_add_opp.
+ rewrite Int.sub_idem. rewrite Int.add_zero. auto.
+ auto.
+ omega.
+ omega.
+Qed.
+
Lemma validate_correct_rec:
forall default v t cases lo hi,
validate default cases t lo hi = true ->
lo <= Int.unsigned v <= hi ->
- switch_target v default cases = comptree_match v t.
+ comptree_match v t = Some (switch_target v default cases).
Proof.
induction t; simpl; intros until hi.
(* base case *)
@@ -187,7 +296,7 @@ Proof.
intros. destruct (andb_prop _ _ H). clear H.
rewrite (split_eq_prop v default _ _ _ _ EQ).
predSpec Int.eq Int.eq_spec v i.
- symmetry. apply beq_nat_eq; auto.
+ f_equal. apply beq_nat_eq; auto.
eapply IHt. eauto.
assert (Int.unsigned v <> Int.unsigned i).
rewrite <- (Int.repr_unsigned v) in H.
@@ -203,11 +312,21 @@ Proof.
unfold Int.ltu. destruct (zlt (Int.unsigned v) (Int.unsigned i)).
eapply IHt1. eauto. omega.
eapply IHt2. eauto. omega.
+ (* jumptable node *)
+ case_eq (split_between i i0 cases). intros ins outs EQ V RANGE.
+ destruct (andb_prop _ _ V). clear V.
+ destruct (andb_prop _ _ H). clear H.
+ destruct (andb_prop _ _ H1). clear H1.
+ rewrite (split_between_prop v _ _ _ _ _ _ EQ).
+ case_eq (Int.ltu (Int.sub v i) i0); intros.
+ eapply validate_jumptable_correct; eauto.
+ split; eapply proj_sumbool_true; eauto.
+ eapply IHt; eauto.
Qed.
Definition table_tree_agree
(default: nat) (cases: table) (t: comptree) : Prop :=
- forall v, switch_target v default cases = comptree_match v t.
+ forall v, comptree_match v t = Some(switch_target v default cases).
Theorem validate_switch_correct:
forall default t cases,
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 416afa9cb..7bc4f8bf5 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -612,6 +612,80 @@ Proof.
Qed.
Hint Resolve nth_error_nil: coqlib.
+(** Compute the length of a list, with result in [Z]. *)
+
+Fixpoint list_length_z_aux (A: Type) (l: list A) (acc: Z) {struct l}: Z :=
+ match l with
+ | nil => acc
+ | hd :: tl => list_length_z_aux tl (Zsucc acc)
+ end.
+
+Remark list_length_z_aux_shift:
+ forall (A: Type) (l: list A) n m,
+ list_length_z_aux l n = list_length_z_aux l m + (n - m).
+Proof.
+ induction l; intros; simpl.
+ omega.
+ replace (n - m) with (Zsucc n - Zsucc m) by omega. auto.
+Qed.
+
+Definition list_length_z (A: Type) (l: list A) : Z :=
+ list_length_z_aux l 0.
+
+Lemma list_length_z_cons:
+ forall (A: Type) (hd: A) (tl: list A),
+ list_length_z (hd :: tl) = list_length_z tl + 1.
+Proof.
+ intros. unfold list_length_z. simpl.
+ rewrite (list_length_z_aux_shift tl 1 0). omega.
+Qed.
+
+Lemma list_length_z_pos:
+ forall (A: Type) (l: list A),
+ list_length_z l >= 0.
+Proof.
+ induction l; simpl. unfold list_length_z; simpl. omega.
+ rewrite list_length_z_cons. omega.
+Qed.
+
+(** Extract the n-th element of a list, as [List.nth_error] does,
+ but the index [n] is of type [Z]. *)
+
+Fixpoint list_nth_z (A: Type) (l: list A) (n: Z) {struct l}: option A :=
+ match l with
+ | nil => None
+ | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Zpred n)
+ end.
+
+Lemma list_nth_z_in:
+ forall (A: Type) (l: list A) n x,
+ list_nth_z l n = Some x -> In x l.
+Proof.
+ induction l; simpl; intros.
+ congruence.
+ destruct (zeq n 0). left; congruence. right; eauto.
+Qed.
+
+Lemma list_nth_z_map:
+ forall (A B: Type) (f: A -> B) (l: list A) n,
+ list_nth_z (List.map f l) n = option_map f (list_nth_z l n).
+Proof.
+ induction l; simpl; intros.
+ auto.
+ destruct (zeq n 0). auto. eauto.
+Qed.
+
+Lemma list_nth_z_range:
+ forall (A: Type) (l: list A) n x,
+ list_nth_z l n = Some x -> 0 <= n < list_length_z l.
+Proof.
+ induction l; simpl; intros.
+ discriminate.
+ rewrite list_length_z_cons. destruct (zeq n 0).
+ generalize (list_length_z_pos l); omega.
+ exploit IHl; eauto. unfold Zpred. omega.
+Qed.
+
(** Properties of [List.incl] (list inclusion). *)
Lemma incl_cons_inv:
diff --git a/lib/Integers.v b/lib/Integers.v
index 1eb59c5c5..c54b6fe5d 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -657,6 +657,13 @@ Proof.
apply eqm_samerepr. unfold z'; red. exists 1. omega.
Qed.
+Theorem signed_eq_unsigned:
+ forall x, unsigned x <= max_signed -> signed x = unsigned x.
+Proof.
+ intros. unfold signed. destruct (zlt (unsigned x) half_modulus).
+ auto. unfold max_signed in H. omegaContradiction.
+Qed.
+
(** ** Properties of addition *)
Theorem add_unsigned: forall x y, add x y = repr (unsigned x + unsigned y).
@@ -786,6 +793,13 @@ Proof.
symmetry. apply sub_add_opp.
Qed.
+Theorem sub_signed:
+ forall x y, sub x y = repr (signed x - signed y).
+Proof.
+ intros. unfold sub. apply eqm_samerepr.
+ apply eqm_sub; apply eqm_sym; apply eqm_signed_unsigned.
+Qed.
+
(** ** Properties of multiplication *)
Theorem mul_commut: forall x y, mul x y = mul y x.
@@ -2565,4 +2579,15 @@ Proof.
omega.
Qed.
+Theorem ltu_range_test:
+ forall x y,
+ ltu x y = true -> unsigned y <= max_signed ->
+ 0 <= signed x < unsigned y.
+Proof.
+ intros.
+ unfold Int.ltu in H. destruct (zlt (unsigned x) (unsigned y)); try discriminate.
+ rewrite signed_eq_unsigned.
+ generalize (unsigned_range x). omega. omega.
+Qed.
+
End Int.
diff --git a/lib/Ordered.v b/lib/Ordered.v
index eddc37213..1c7c7f43f 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -11,11 +11,12 @@
(* *********************************************************************)
(** Constructions of ordered types, for use with the [FSet] functors
- for finite sets. *)
+ for finite sets and the [FMap] functors for finite maps. *)
Require Import FSets.
Require Import Coqlib.
Require Import Maps.
+Require Import Integers.
(** The ordered type of positive numbers *)
@@ -49,6 +50,44 @@ Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := peq.
End OrderedPositive.
+(** The ordered type of machine integers *)
+
+Module OrderedInt <: OrderedType.
+
+Definition t := int.
+Definition eq (x y: t) := x = y.
+Definition lt (x y: t) := Int.unsigned x < Int.unsigned y.
+
+Lemma eq_refl : forall x : t, eq x x.
+Proof (@refl_equal t).
+Lemma eq_sym : forall x y : t, eq x y -> eq y x.
+Proof (@sym_equal t).
+Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+Proof (@trans_equal t).
+Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+Proof.
+ unfold lt; intros. omega.
+Qed.
+Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+Proof.
+ unfold lt,eq; intros; red; intros. subst. omega.
+Qed.
+Lemma compare : forall x y : t, Compare lt eq x y.
+Proof.
+ intros. destruct (zlt (Int.unsigned x) (Int.unsigned y)).
+ apply LT. auto.
+ destruct (Int.eq_dec x y).
+ apply EQ. auto.
+ apply GT.
+ assert (Int.unsigned x <> Int.unsigned y).
+ red; intros. rewrite <- (Int.repr_unsigned x) in n. rewrite <- (Int.repr_unsigned y) in n. congruence.
+ red. omega.
+Qed.
+
+Definition eq_dec : forall x y, { eq x y } + { ~ eq x y } := Int.eq_dec.
+
+End OrderedInt.
+
(** Indexed types (those that inject into [positive]) are ordered. *)
Module OrderedIndexed(A: INDEXED_TYPE) <: OrderedType.
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 0e6032fe7..18dc93aba 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -115,6 +115,7 @@ Inductive instruction : Type :=
| Pbs: ident -> instruction (**r branch to symbol *)
| Pblr: instruction (**r branch to contents of register LR *)
| Pbt: crbit -> label -> instruction (**r branch if true *)
+ | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *)
| Pcmplw: ireg -> ireg -> instruction (**r unsigned integer comparison *)
| Pcmplwi: ireg -> constant -> instruction (**r same, with immediate argument *)
| Pcmpw: ireg -> ireg -> instruction (**r signed integer comparison *)
@@ -196,8 +197,8 @@ Inductive instruction : Type :=
Expands to a float load [lfd] from an address in the constant data section
initialized with the floating-point constant:
<<
- addis r2, 0, ha16(lbl)
- lfd rdst, lo16(lbl)(r2)
+ addis r12, 0, ha16(lbl)
+ lfd rdst, lo16(lbl)(r12)
.const_data
lbl: .double floatcst
.text
@@ -218,8 +219,8 @@ lbl: .double floatcst
constant [2^31], subtract [2^31] if bigger, then convert to a signed
integer as above, then add back [2^31] if needed. Expands to:
<<
- addis r2, 0, ha16(lbl1)
- lfd f13, lo16(lbl1)(r2)
+ addis r12, 0, ha16(lbl1)
+ lfd f13, lo16(lbl1)(r12)
fcmpu cr7, rsrc, f13
cror 30, 29, 30
beq cr7, lbl2
@@ -242,12 +243,12 @@ lbl1: .long 0x41e00000, 0x00000000 # 2^31 in double precision
arithmetic over a memory word, which our memory model and axiomatization
of floats cannot express. Expands to:
<<
- addis r2, 0, 0x4330
- stwu r2, -8(r1)
- addis r2, rsrc, 0x8000
- stw r2, 4(r1)
- addis r2, 0, ha16(lbl)
- lfd f13, lo16(lbl)(r2)
+ addis r12, 0, 0x4330
+ stwu r12, -8(r1)
+ addis r12, rsrc, 0x8000
+ stw r12, 4(r1)
+ addis r12, 0, ha16(lbl)
+ lfd f13, lo16(lbl)(r12)
lfd rdst, 0(r1)
addi r1, r1, 8
fsub rdst, rdst, f13
@@ -260,11 +261,11 @@ lbl: .long 0x43300000, 0x80000000
- [Piuctf]: convert an unsigned integer to a float. The expansion is close
to that [Pictf], and equally obscure.
<<
- addis r2, 0, 0x4330
- stwu r2, -8(r1)
+ addis r12, 0, 0x4330
+ stwu r12, -8(r1)
stw rsrc, 4(r1)
- addis r2, 0, ha16(lbl)
- lfd f13, lo16(lbl)(r2)
+ addis r12, 0, ha16(lbl)
+ lfd f13, lo16(lbl)(r12)
lfd rdst, 0(r1)
addi r1, r1, 8
fsub rdst, rdst, f13
@@ -294,6 +295,18 @@ lbl: .long 0x43300000, 0x00000000
>>
Again, our memory model cannot comprehend that this operation
frees (logically) the current stack frame.
+- [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
+ as follows:
+<<
+ rlwinm r12, reg, 2, 0, 29
+ addis r12, r12, ha16(lbl)
+ lwz r12, lo16(lbl)(r12)
+ mtctr r12
+ bctr r12
+ .const_data
+lbl: .long table[0], table[1], ...
+ .text
+>>
*)
Definition code := list instruction.
@@ -608,6 +621,15 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| Vint n => if Int.eq n Int.zero then OK (nextinstr rs) m else goto_label c lbl rs m
| _ => Error
end
+ | Pbtbl r tbl =>
+ match rs#r with
+ | Vint n =>
+ match list_nth_z tbl (Int.signed n) with
+ | None => Error
+ | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
+ end
+ | _ => Error
+ end
| Pcmplw r1 r2 =>
OK (nextinstr (compare_uint rs rs#r1 rs#r2)) m
| Pcmplwi r1 cst =>
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index aebb48346..4beabb1c8 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -502,6 +502,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
let p := crbit_for_cond cond in
transl_cond cond args
(if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k)
+ | Mjumptable arg tbl =>
+ Pbtbl (ireg_of arg) tbl :: k
| Mreturn =>
Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
Pmtlr GPR12 ::
@@ -523,17 +525,11 @@ Definition transl_function (f: Mach.function) :=
Pstw GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 ::
transl_code f f.(fn_code).
-Fixpoint code_size (c: code) : Z :=
- match c with
- | nil => 0
- | instr :: c' => code_size c' + 1
- end.
-
Open Local Scope string_scope.
Definition transf_function (f: Mach.function) : res Asm.code :=
let c := transl_function f in
- if zlt Int.max_unsigned (code_size c)
+ if zlt Int.max_unsigned (list_length_z c)
then Errors.Error (msg "code size exceeded")
else Errors.OK c.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 2710eddde..4e45c8eae 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -65,19 +65,19 @@ Proof.
intros.
destruct (functions_translated _ _ H) as [tf [A B]].
rewrite A. generalize B. unfold transf_fundef, transf_partial_fundef, transf_function.
- case (zlt Int.max_unsigned (code_size (transl_function f))); simpl; intro.
+ case (zlt Int.max_unsigned (list_length_z (transl_function f))); simpl; intro.
congruence. intro. inv B0. auto.
Qed.
Lemma functions_transl_no_overflow:
forall b f,
Genv.find_funct_ptr ge b = Some (Internal f) ->
- code_size (transl_function f) <= Int.max_unsigned.
+ list_length_z (transl_function f) <= Int.max_unsigned.
Proof.
intros.
destruct (functions_translated _ _ H) as [tf [A B]].
generalize B. unfold transf_fundef, transf_partial_fundef, transf_function.
- case (zlt Int.max_unsigned (code_size (transl_function f))); simpl; intro.
+ case (zlt Int.max_unsigned (list_length_z (transl_function f))); simpl; intro.
congruence. intro; omega.
Qed.
@@ -105,21 +105,23 @@ Proof.
eauto.
Qed.
+(*
Remark code_size_pos:
forall fn, code_size fn >= 0.
Proof.
induction fn; simpl; omega.
Qed.
+*)
Remark code_tail_bounds:
forall fn ofs i c,
- code_tail ofs fn (i :: c) -> 0 <= ofs < code_size fn.
+ code_tail ofs fn (i :: c) -> 0 <= ofs < list_length_z fn.
Proof.
assert (forall ofs fn c, code_tail ofs fn c ->
- forall i c', c = i :: c' -> 0 <= ofs < code_size fn).
+ forall i c', c = i :: c' -> 0 <= ofs < list_length_z fn).
induction 1; intros; simpl.
- rewrite H. simpl. generalize (code_size_pos c'). omega.
- generalize (IHcode_tail _ _ H0). omega.
+ rewrite H. rewrite list_length_z_cons. generalize (list_length_z_pos c'). omega.
+ rewrite list_length_z_cons. generalize (IHcode_tail _ _ H0). omega.
eauto.
Qed.
@@ -138,7 +140,7 @@ Qed.
Lemma code_tail_next_int:
forall fn ofs i c,
- code_size fn <= Int.max_unsigned ->
+ list_length_z fn <= Int.max_unsigned ->
code_tail (Int.unsigned ofs) fn (i :: c) ->
code_tail (Int.unsigned (Int.add ofs Int.one)) fn c.
Proof.
@@ -167,7 +169,7 @@ Inductive transl_code_at_pc: val -> block -> Mach.function -> Mach.code -> Prop
Lemma exec_straight_steps_1:
forall fn c rs m c' rs' m',
exec_straight tge fn c rs m c' rs' m' ->
- code_size fn <= Int.max_unsigned ->
+ list_length_z fn <= Int.max_unsigned ->
forall b ofs,
rs#PC = Vptr b ofs ->
Genv.find_funct_ptr tge b = Some (Internal fn) ->
@@ -191,7 +193,7 @@ Qed.
Lemma exec_straight_steps_2:
forall fn c rs m c' rs' m',
exec_straight tge fn c rs m c' rs' m' ->
- code_size fn <= Int.max_unsigned ->
+ list_length_z fn <= Int.max_unsigned ->
forall b ofs,
rs#PC = Vptr b ofs ->
Genv.find_funct_ptr tge b = Some (Internal fn) ->
@@ -284,7 +286,7 @@ Lemma label_pos_code_tail:
exists pos',
label_pos lbl pos c = Some pos'
/\ code_tail (pos' - pos) c c'
- /\ pos < pos' <= pos + code_size c.
+ /\ pos < pos' <= pos + list_length_z c.
Proof.
induction c.
simpl; intros. discriminate.
@@ -293,12 +295,12 @@ Proof.
intro EQ; injection EQ; intro; subst c'.
exists (pos + 1). split. auto. split.
replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor.
- generalize (code_size_pos c). omega.
+ rewrite list_length_z_cons. generalize (list_length_z_pos c). omega.
intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]].
exists pos'. split. auto. split.
replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega.
constructor. auto.
- omega.
+ rewrite list_length_z_cons. omega.
Qed.
(** The following lemmas show that the translation from Mach to PPC
@@ -863,7 +865,7 @@ Proof.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
intro WTI. inversion WTI.
inv AT.
- assert (NOOV: code_size (transl_function f) <= Int.max_unsigned).
+ assert (NOOV: list_length_z (transl_function f) <= Int.max_unsigned).
eapply functions_transl_no_overflow; eauto.
destruct ros; simpl in H; simpl transl_code in H7.
(* Indirect call *)
@@ -940,7 +942,7 @@ Proof.
generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
intro WTI. inversion WTI.
inversion AT. subst b f0 c0.
- assert (NOOV: code_size (transl_function f) <= Int.max_unsigned).
+ assert (NOOV: list_length_z (transl_function f) <= Int.max_unsigned).
eapply functions_transl_no_overflow; eauto.
destruct ros; simpl in H; simpl in H9.
(* Indirect call *)
@@ -1127,6 +1129,40 @@ Proof.
auto with ppcgen.
Qed.
+Lemma exec_Mjumptable_prop:
+ forall (s : list stackframe) (fb : block) (f : function) (sp : val)
+ (arg : mreg) (tbl : list Mach.label) (c : list Mach.instruction)
+ (rs : mreg -> val) (m : mem) (n : int) (lbl : Mach.label)
+ (c' : Mach.code),
+ rs arg = Vint n ->
+ list_nth_z tbl (Int.signed n) = Some lbl ->
+ Genv.find_funct_ptr ge fb = Some (Internal f) ->
+ Mach.find_label lbl (fn_code f) = Some c' ->
+ exec_instr_prop
+ (Machconcr.State s fb sp (Mjumptable arg tbl :: c) rs m) E0
+ (Machconcr.State s fb sp c' rs m).
+Proof.
+ intros; red; intros; inv MS.
+ assert (f0 = f) by congruence. subst f0.
+ generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))).
+ intro WTI. inv WTI.
+ pose (rs1 := rs0 # GPR12 <- Vundef # CTR <- Vundef).
+ inv AT. simpl in H6.
+ assert (rs1 PC = Vptr fb ofs). rewrite H3. reflexivity.
+ generalize (functions_transl _ _ H1); intro FN.
+ generalize (functions_transl_no_overflow _ _ H1); intro NOOV.
+ exploit find_label_goto_label; eauto. intros [rs2 [A [B C]]].
+ left; exists (State rs2 m); split.
+ apply plus_one. econstructor. symmetry; eauto. eauto.
+ eapply find_instr_tail. eauto.
+ simpl. rewrite (ireg_val _ _ _ _ AG H4) in H. rewrite H.
+ change label with Mach.label; rewrite H0. eexact A.
+ econstructor; eauto.
+ eapply Mach.find_label_incl; eauto.
+ apply agree_exten_2 with rs1; auto.
+ unfold rs1. repeat apply agree_set_other; auto with ppcgen.
+Qed.
+
Lemma exec_Mreturn_prop:
forall (s : list stackframe) (fb stk : block) (soff : int)
(c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function),
@@ -1292,6 +1328,7 @@ Proof
exec_Mgoto_prop
exec_Mcond_true_prop
exec_Mcond_false_prop
+ exec_Mjumptable_prop
exec_Mreturn_prop
exec_function_internal_prop
exec_function_external_prop
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 539d9894e..df1b06293 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -261,6 +261,17 @@ let print_instruction oc labels = function
fprintf oc " blr\n"
| Pbt(bit, lbl) ->
fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl)
+ | Pbtbl(r, tbl) ->
+ let lbl = new_label() in
+ fprintf oc " rlwinm %a, %a, 2, 0, 29\n" ireg GPR12 ireg r;
+ fprintf oc " addis %a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl;
+ fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12;
+ fprintf oc " mtctr %a\n" ireg GPR12;
+ fprintf oc " bctr\n";
+ fprintf oc "%a:" label lbl;
+ List.iter
+ (fun l -> fprintf oc " .long %a\n" label (transl_label l))
+ tbl
| Pcmplw(r1, r2) ->
fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2
| Pcmplwi(r1, c) ->
@@ -472,11 +483,15 @@ let print_instruction oc labels = function
if Labelset.mem lbl labels then
fprintf oc "%a:\n" label (transl_label lbl)
-let rec labels_of_code = function
- | [] -> Labelset.empty
+let rec labels_of_code accu = function
+ | [] ->
+ accu
| (Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)) :: c ->
- Labelset.add lbl (labels_of_code c)
- | _ :: c -> labels_of_code c
+ labels_of_code (Labelset.add lbl accu) c
+ | Pbtbl(_, tbl) :: c ->
+ labels_of_code (List.fold_right Labelset.add tbl accu) c
+ | _ :: c ->
+ labels_of_code accu c
let print_function oc name code =
Hashtbl.clear current_function_labels;
@@ -488,7 +503,7 @@ let print_function oc name code =
if not (Cil2Csyntax.atom_is_static name) then
fprintf oc " .globl %a\n" symbol name;
fprintf oc "%a:\n" symbol name;
- List.iter (print_instruction oc (labels_of_code code)) code
+ List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code
(* Generation of stub functions *)
--
GitLab