diff options
49 files changed, 767 insertions, 145 deletions
@@ -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 7d843e5..b802f4a 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 fc0a0f3..10eaa5b 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 aba9660..260297f 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 8c5f536..15468c5 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 ff8d41a..98b7bbf 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 14027bf..7f94246 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 cccce9a..e1ab2e9 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 dadb192..fff9a60 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 2505566..6a69336 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 10b7d83..e353338 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 9f3f589..6013a17 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 0461c9a..e62f928 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 e025407..bf21cb7 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 431fe17..31d0318 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 b273860..1f4e5fa 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 e35fb11..c79908d 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 627c878..716b66f 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 33b570b..ba4952b 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 0bb2442..f7e85c3 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 aa17cd4..a2630a2 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 139eac7..89529fd 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 876f558..84ae0a4 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 ef59e6f..fe086cb 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 5de073e..b2ee80f 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 39add98..942dc50 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 4c1fc05..7e42c80 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 df1ade9..d07bd08 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 caf93c8..037eb3f 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 2df9d5d..86f0eaf 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -112,6 +112,11 @@ Inductive wt_instr : instruction -> Prop := valid_successor s1 -> valid_successor s2 -> wt_instr (Icond cond args s1 s2) + | wt_Ijumptable: + forall arg tbl, + env arg = Tint -> + (forall s, In s tbl -> valid_successor s) -> + wt_instr (Ijumptable arg tbl) | wt_Ireturn: forall optres, option_map env optres = funct.(fn_sig).(sig_res) -> @@ -224,6 +229,9 @@ Definition check_instr (i: instruction) : bool := check_regs args (type_of_condition cond) && check_successor s1 && check_successor s2 + | Ijumptable arg tbl => + check_reg arg Tint + && List.forallb check_successor tbl | Ireturn optres => match optres, funct.(fn_sig).(sig_res) with | None, None => true @@ -326,6 +334,10 @@ Proof. constructor. apply check_regs_correct; auto. apply check_successor_correct; auto. apply check_successor_correct; auto. + (* jumptable *) + constructor. apply check_reg_correct; auto. + rewrite List.forallb_forall in H0. intros. apply check_successor_correct; auto. + intros. (* return *) constructor. destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate. @@ -538,6 +550,8 @@ Proof. (* Icond *) econstructor; eauto. econstructor; eauto. + (* Ijumptable *) + econstructor; eauto. (* Ireturn *) econstructor; eauto. destruct or; simpl in *. diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index cc7edf4..406ca07 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 621e75b..5728a62 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 a7becc3..21d5f38 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 375bbfd..df0715e 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 182c322..5d9cf37 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 5b6f2dc..ba42958 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 1bafc35..8ba5cae 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 1423e1e..8681d84 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 ef55a15..3ad8c4d 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 eccb62d..92ec68c 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 91745df..8990cb4 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 179d4d2..ee8f6aa 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 416afa9..7bc4f8b 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 1eb59c5..c54b6fe 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 eddc372..1c7c7f4 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 0e6032f..18dc93a 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 aebb483..4beabb1 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 2710edd..4e45c8e 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 539d989..df1b062 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 *) |