diff --git a/.depend b/.depend
index 9edeabd676c081e2e26b202f9ddbd19d74cffc4c..a0539b0b7fa9f692d937f050c244dc7c4b54f93c 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 7d843e5790cdfc5245b5da04c5ebaf813437c84f..b802f4ac7623b7ff5180a5f4098f3f2517909440 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 fc0a0f3c6e7dc0add73f4533df71daa9067274a5..10eaa5b1af8011c3658b0b4b97d3e7d117588d45 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 aba966010eb6ea6e5c236ab0f478f2e9a65472f5..260297f2c267c2842f0acee24d9b03b2f0010737 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 8c5f536daa7a61ca438751fb53a3ecf8b0741b75..15468c574b282e80f587a0e1f77a618cc41c8e26 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 ff8d41aa48be3d701cda321ac493fba00ef045c5..98b7bbf58e4e719f0ec3ea4e0a8e515b0ca3b5ad 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 14027bf09bb3fa28319710e08e5efdd7c7571cc2..7f942464769e45057accd627b8298ce0fb17028d 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 cccce9a3e10b263867801727fbea5b0911a49ef2..e1ab2e9c09328eb8027b9d4bfe1d024cbb3b1981 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 dadb192fe517cd15a44da644f28799ef3faf2592..fff9a60dae52447ee0f676d216fa15f64eb3637a 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 2505566fa628e158a557e6d4e419dffda9b8d427..6a693361ba5515463a2062a225e2da71eb9f61b8 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 10b7d83231362b6366ac65acdc9fa492c7f623bf..e3533388e814a2ef26d57b5f545b27fa771d2657 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 9f3f5896b5ed9d3196d163dbe6d078dac3993e82..6013a17df67247c1c9ccb8716af5126049131f09 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 0461c9af59737e6607237f1b966b46b8307b9551..e62f9287fa129c085bb55ff92998cf82ce36ad5f 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 e025407a8e27c4eeb36620dba37b302dcba45be6..bf21cb7dc5aa39691525324caaaaabb9c1cffd8c 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 431fe1720c2345edcb61bd0d0cb292acebe1a4d3..31d0318ccf8bbe00cbbff3083e050546985dcb9a 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 b27386052cc6b9133642a574b58d6fcc380cd657..1f4e5fac5c0733ba45e32b9251f0c407eab615a7 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 e35fb11be9dd433c3bfc30485a527b37751904dd..c79908d6799fb1f2a6ca592ea49fd99ba75d441b 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 627c878f08d33b68686a48ba74974f62c0507a9d..716b66f13f1ac2090022a48c971bc6b1c95d72a1 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 33b570b91746f67bb1e3dab79b9bc922140b822e..ba4952bd5a41be59bb384fc9b495a182be5c2768 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 0bb24428c22e2db209478cb030e895f0a7df67c3..f7e85c3eff5445c3f2ad7a6323d43081bc1b1176 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 aa17cd44b182721931bba2b7287772a53f297be9..a2630a2b84c4f770cbaf23f365756c229de1b0cd 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 139eac75c663268ffb9004f09bdc86b7037e29fb..89529fd4b62386ffb25572a6ddc6847222a71b00 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 876f558c8a05a494b6ce8c0cdfef62ed12a64be8..84ae0a4fd816bfa063fbd206dbb95c21d9c3b00e 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 ef59e6f06ea5190435a02b45095d424f3353b717..fe086cb4f3e7aae61663b95a303ec11dfe4a6353 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 5de073ee5b28fe247aba6678c305599b9b4b724c..b2ee80fc281ba40a05cf1994162e253fae6f683e 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 39add9861e1b6ad841b5d0f069574f1c59896f99..942dc50b60c49b34cb38896ad0b269520dc6cbd6 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 4c1fc05c0a4c6e70b2498587b04619fc0325ad90..7e42c80d1646b8c234a01dc8764732c0a49daca2 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 df1ade9ddf56792f29059462c855518d54693c52..d07bd0814d025662a3f6276a3e68b83ead12de0e 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 caf93c8362a35968aa669ca00f5186fbe101f2c1..037eb3fb14148c08fd4ee7ba3c9d08e3f257e8be 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 2df9d5df80390cd733579d2a0afe2a9b07baa7b5..86f0eaf10925533e01ec4d634dc0d8598d6bca64 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 cc7edf4917bfd82fdd15120c93cb1dee331297af..406ca07a9594dd4e8d6179db561ad7b3fe6eaeab 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 621e75b57acba17b946a108c22eb53a1e9a23413..5728a628315c9fe5b4ef4e8802e01d52699ca750 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 a7becc36cceb7d13cbbc9363457c3bc63fdabe4c..21d5f3806b45b40fe05c375e69981e667d668113 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 375bbfde7c6c84836697bc178fc7199a957dd22e..df0715ee79033cf2368d74bd941e47902ca6b6a0 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 182c322697f866ae3338a42e697c6a737b5e545c..5d9cf37472593ce3e23d90cc07f9f47d77551e92 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 5b6f2dc7ba5f0ce08a143b972ff1cf5cc72f79ad..ba42958959d3adc5874ef66e67d9bb0649d4d782 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 1bafc35b1056b091cfdc8190b9b778d943e4cb5b..8ba5caedba7ca592eaf7f7406c6f40030d02a060 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 1423e1e0171c663cf54026232d9b00ed13b4fffc..8681d84ada4644d28e3bc2f79c48881ea0f8017f 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 ef55a1572ee2291dd991d69ae2b390d822628c76..3ad8c4d05392f16e510d8742d497827b3a71b508 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 eccb62dd406d6d947a0ac72efc2330c83e43cdd8..92ec68cf74a8b1426400f0aa8c76f5d37840fe0d 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 91745dfbeda253565b18e73b4eddf5e1c35c2423..8990cb44a3b35cbc15d4e14b277384a30f585119 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 179d4d2ee675539c1c1482efb306ef10b018b0f6..ee8f6aa8f95b0e076e63d74f2d2d0599ec6d899b 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 416afa9cbea6f55a37ae7cc1cd2de389fa9a13ed..7bc4f8bf5f5306aa6ef9b73f00d3370261c3ad5f 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 1eb59c5c583d60f6ac6bdc0577f40951a811342c..c54b6fe5dc8a3f92f15e47ac88e9977d17f001c2 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 eddc372130c09b4003ac30ae20fceb2c191e2f89..1c7c7f43fea7c0752d01368e439402a84e68b029 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 0e6032fe7c09dceeac92356b583f46ff35c0db0e..18dc93aba87b41b112919108f45f255b62513e3a 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 aebb48346f20e0236a6537d51f9a7957fc8086eb..4beabb1c8d75d4b3eee3783b3af8412785718915 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 2710eddde6e957f83bff95c67ec045810c3295cf..4e45c8eae9cf59cbb649fc41d3ce08c03bacf699 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 539d9894e5f97cd6233166d8cc51ccddf1589ccf..df1b062935e50a8aea3536c3861017221e909e64 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 *)