From 74487f079dd56663f97f9731cea328931857495c Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Nov 2009 12:50:57 +0000 Subject: Added support for jump tables in back end. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/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 ++- 40 files changed, 380 insertions(+), 88 deletions(-) (limited to 'backend') diff --git a/backend/Allocation.v b/backend/Allocation.v index 7d843e57..b802f4ac 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 fc0a0f3c..10eaa5b1 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 aba96601..260297f2 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 8c5f536d..15468c57 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 ff8d41aa..98b7bbf5 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 14027bf0..7f942464 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 cccce9a3..e1ab2e9c 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -121,26 +121,14 @@ Definition transfer (f: function) (pc: node) (before: D.t) := | None => before | Some i => match i with - | Inop s => - before | Iop op args res s => let a := eval_static_operation op (approx_regs before args) in D.set res a before | Iload chunk addr args dst s => D.set dst Unknown before - | Istore chunk addr args src s => - before | Icall sig ros args res s => D.set res Unknown before - | Itailcall sig ros args => - before -(* - | Ialloc arg res s => - D.set res Unknown before -*) - | Icond cond args ifso ifnot => - before - | Ireturn optarg => + | _ => before end end. @@ -212,6 +200,15 @@ Definition transf_instr (app: D.t) (instr: instruction) := let (cond', args') := cond_strength_reduction (approx_reg app) cond args in Icond cond' args' s1 s2 end + | Ijumptable arg tbl => + match intval (approx_reg app) arg with + | Some n => + match list_nth_z tbl (Int.signed n) with + | Some s => Inop s + | None => instr + end + | None => instr + end | _ => instr end. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index dadb192f..fff9a60d 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 2505566f..6a693361 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 10b7d832..e3533388 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 9f3f5896..6013a17d 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 0461c9af..e62f9287 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 e025407a..bf21cb7d 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 431fe172..31d0318c 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 b2738605..1f4e5fac 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 e35fb11b..c79908d6 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 627c878f..716b66f1 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 33b570b9..ba4952bd 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 0bb24428..f7e85c3e 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 aa17cd44..a2630a2b 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 139eac75..89529fd4 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 876f558c..84ae0a4f 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 ef59e6f0..fe086cb4 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 5de073ee..b2ee80fc 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 39add986..942dc50b 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 4c1fc05c..7e42c80d 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 df1ade9d..d07bd081 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 caf93c83..037eb3fb 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 2df9d5df..86f0eaf1 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 cc7edf49..406ca07a 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 621e75b5..5728a628 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 a7becc36..21d5f380 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 375bbfde..df0715ee 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 182c3226..5d9cf374 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 5b6f2dc7..ba429589 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 1bafc35b..8ba5caed 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 1423e1e0..8681d84a 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 ef55a157..3ad8c4d0 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 eccb62dd..92ec68cf 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 91745dfb..8990cb44 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: -- cgit