diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-06 22:33:46 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-06 22:33:46 +0200 |
commit | e64b9464fb6662bf63ac255eca94d17d572c9d81 (patch) | |
tree | 517819d4f4e29fbd3a68d6431dd471baf0d427b0 | |
parent | 8e03466a1a2e7bbc9057ac76ee18deda990dc884 (diff) | |
download | compcert-kvx-e64b9464fb6662bf63ac255eca94d17d572c9d81.tar.gz compcert-kvx-e64b9464fb6662bf63ac255eca94d17d572c9d81.zip |
ONE "admitted" and things compile
-rw-r--r-- | backend/Allocation.v | 28 | ||||
-rw-r--r-- | backend/Allocproof.v | 37 | ||||
-rw-r--r-- | backend/Inliningaux.ml | 2 | ||||
-rw-r--r-- | backend/PrintLTL.ml | 7 | ||||
-rw-r--r-- | backend/PrintMach.ml | 5 | ||||
-rw-r--r-- | backend/PrintRTL.ml | 7 | ||||
-rw-r--r-- | backend/PrintXTL.ml | 7 | ||||
-rw-r--r-- | backend/Regalloc.ml | 26 | ||||
-rw-r--r-- | backend/Splitting.ml | 4 | ||||
-rw-r--r-- | backend/XTL.ml | 4 | ||||
-rw-r--r-- | backend/XTL.mli | 2 | ||||
-rw-r--r-- | common/PrintAST.ml | 4 |
12 files changed, 87 insertions, 46 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index c1fbf90d..6e4fcc82 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -63,14 +63,14 @@ Inductive block_shape: Type := (mv2: moves) (s: node) | BSloaddead (chunk: memory_chunk) (addr: addressing) (args: list reg) (dst: reg) (mv: moves) (s: node) - | BSload2 (trap : trapping_mode) (addr1 addr2: addressing) (args: list reg) (dst: reg) + | BSload2 (addr1 addr2: addressing) (args: list reg) (dst: reg) (mv1: moves) (args1': list mreg) (dst1': mreg) (mv2: moves) (args2': list mreg) (dst2': mreg) (mv3: moves) (s: node) - | BSload2_1 (trap : trapping_mode) (addr: addressing) (args: list reg) (dst: reg) + | BSload2_1 (addr: addressing) (args: list reg) (dst: reg) (mv1: moves) (args': list mreg) (dst': mreg) (mv2: moves) (s: node) - | BSload2_2 (trap : trapping_mode) (addr addr': addressing) (args: list reg) (dst: reg) + | BSload2_2 (addr addr': addressing) (args: list reg) (dst: reg) (mv1: moves) (args': list mreg) (dst': mreg) (mv2: moves) (s: node) | BSstore (chunk: memory_chunk) (addr: addressing) (args: list reg) (src: reg) @@ -232,24 +232,26 @@ Definition pair_instr_block | Lload trap' chunk' addr' args' dst' :: b2 => assertion (trapping_mode_eq trap' trap); if chunk_eq chunk Mint64 && Archi.splitlong then + (* TODO: do not support non trapping split loads *) + assertion (trapping_mode_eq trap TRAP); assertion (chunk_eq chunk' Mint32); let (mv2, b3) := extract_moves nil b2 in match b3 with | Lload trap'' chunk'' addr'' args'' dst'' :: b4 => - assertion (trapping_mode_eq trap'' trap); + assertion (trapping_mode_eq trap'' TRAP); let (mv3, b5) := extract_moves nil b4 in assertion (chunk_eq chunk'' Mint32); assertion (eq_addressing addr addr'); assertion (option_eq eq_addressing (offset_addressing addr 4) (Some addr'')); assertion (check_succ s b5); - Some(BSload2 trap addr addr'' args dst mv1 args' dst' mv2 args'' dst'' mv3 s) + Some(BSload2 addr addr'' args dst mv1 args' dst' mv2 args'' dst'' mv3 s) | _ => assertion (check_succ s b3); if (eq_addressing addr addr') then - Some(BSload2_1 trap addr args dst mv1 args' dst' mv2 s) + Some(BSload2_1 addr args dst mv1 args' dst' mv2 s) else (assertion (option_eq eq_addressing (offset_addressing addr 4) (Some addr')); - Some(BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s)) + Some(BSload2_2 addr addr' args dst mv1 args' dst' mv2 s)) end else ( let (mv2, b3) := extract_moves nil b2 in @@ -1029,7 +1031,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv) do e1 <- track_moves env mv2 e; do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1; track_moves env mv1 e2 - | BSload2 trap addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => + | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => do e1 <- track_moves env mv3 e; let e2 := remove_equation (Eq kind_second_word dst (R dst2')) e1 in assertion (loc_unconstrained (R dst2') e2); @@ -1042,14 +1044,14 @@ Definition transfer_aux (f: RTL.function) (env: regenv) assertion (reg_unconstrained dst e5); do e6 <- add_equations args args1' e5; track_moves env mv1 e6 - | BSload2_1 trap addr args dst mv1 args' dst' mv2 s => + | BSload2_1 addr args dst mv1 args' dst' mv2 s => do e1 <- track_moves env mv2 e; let e2 := remove_equation (Eq kind_first_word dst (R dst')) e1 in assertion (reg_loc_unconstrained dst (R dst') e2); assertion (can_undef (destroyed_by_load Mint32 addr) e2); do e3 <- add_equations args args' e2; track_moves env mv1 e3 - | BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s => + | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s => do e1 <- track_moves env mv2 e; let e2 := remove_equation (Eq kind_second_word dst (R dst')) e1 in assertion (reg_loc_unconstrained dst (R dst') e2); @@ -1266,9 +1268,9 @@ Definition successors_block_shape (bsh: block_shape) : list node := | BSop op args res mv1 args' res' mv2 s => s :: nil | BSopdead op args res mv s => s :: nil | BSload trap chunk addr args dst mv1 args' dst' mv2 s => s :: nil - | BSload2 trap addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => s :: nil - | BSload2_1 trap addr args dst mv1 args' dst' mv2 s => s :: nil - | BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s => s :: nil + | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => s :: nil + | BSload2_1 addr args dst mv1 args' dst' mv2 s => s :: nil + | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s => s :: nil | BSloaddead chunk addr args dst mv s => s :: nil | BSstore chunk addr args src mv1 args' src' s => s :: nil | BSstore2 addr addr' args src mv1 args1' src1' mv2 args2' src2' s => s :: nil diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 44dda4ac..ab6f87b0 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2229,7 +2229,7 @@ Proof. econstructor; eauto. eapply wt_exec_Iload; eauto. -- (* BSload notrap1 *) +- (* load notrap1 *) generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). intro WTRS'. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. @@ -2247,7 +2247,7 @@ Proof. exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. econstructor; eauto. -(* BSload notrap dead? *) +(* load notrap1 dead *) - exploit exec_moves; eauto. intros [ls1 [X Y]]. econstructor; split. eapply plus_left. econstructor; eauto. @@ -2259,7 +2259,38 @@ Proof. econstructor; eauto. eapply wt_exec_Iload_notrap; eauto. +(* load regular notrap2 *) +- (* exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. + + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. eapply exec_Lload_notrap2 with (a := a'). rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + + generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). intro WTRS'. + *) + + admit. +- (* load notrap2 dead *) + exploit exec_moves; eauto. intros [ls1 [X Y]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_right. eexact X. econstructor; eauto. + eauto. traceEq. + exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. + eapply reg_unconstrained_satisf; eauto. + intros [enext [U V]]. + econstructor; eauto. + eapply wt_exec_Iload_notrap; eauto. + (* store *) - exploit exec_moves; eauto. intros [ls1 [X Y]]. exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD. @@ -2511,7 +2542,7 @@ Proof. eapply plus_left. constructor. eexact A. traceEq. econstructor; eauto. apply wt_regset_assign; auto. rewrite WTRES0; auto. -Qed. +Admitted. Lemma initial_states_simulation: forall st1, RTL.initial_state prog st1 -> diff --git a/backend/Inliningaux.ml b/backend/Inliningaux.ml index 842e0c93..609b2637 100644 --- a/backend/Inliningaux.ml +++ b/backend/Inliningaux.ml @@ -57,7 +57,7 @@ let used_in_globvar io gv = let fun_inline_analysis id io fn = let inst io nid = function | Iop (op, args, dest, succ) -> used_id io (globals_operation op) - | Iload (chunk, addr, args, dest, succ) + | Iload (_, chunk, addr, args, dest, succ) | Istore (chunk, addr, args, dest, succ) -> used_id io (globals_addressing addr) | Ibuiltin (ef, args, dest, succ) -> used_id io (globals_of_builtin_args args) | Icall (_, Coq_inr cid, _, _, _) diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index 1c449e74..b309a9f2 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -61,9 +61,10 @@ let print_succ pp s dfl = let print_instruction pp succ = function | Lop(op, args, res) -> fprintf pp "%a = %a" mreg res (print_operation mreg) (op, args) - | Lload(chunk, addr, args, dst) -> - fprintf pp "%a = %s[%a]" - mreg dst (name_of_chunk chunk) (print_addressing mreg) (addr, args) + | Lload(trap,chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]%a" + mreg dst (name_of_chunk chunk) (print_addressing mreg) (addr, args) + print_trapping_mode trap | Lgetstack(sl, ofs, ty, dst) -> fprintf pp "%a = %a" mreg dst slot (sl, ofs, ty) | Lsetstack(src, sl, ofs, ty) -> diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index 517f3037..70e65832 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -48,10 +48,11 @@ let print_instruction pp i = | Mop(op, args, res) -> fprintf pp "\t%a = %a\n" reg res (PrintOp.print_operation reg) (op, args) - | Mload(chunk, addr, args, dst) -> - fprintf pp "\t%a = %s[%a]\n" + | Mload(trap, chunk, addr, args, dst) -> + fprintf pp "\t%a = %s[%a]%a\n" reg dst (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) + print_trapping_mode trap | Mstore(chunk, addr, args, src) -> fprintf pp "\t%s[%a] = %a\n" (name_of_chunk chunk) diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 841540b6..c25773e5 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -50,10 +50,11 @@ let print_instruction pp (pc, i) = fprintf pp "%a = %a\n" reg res (PrintOp.print_operation reg) (op, args); print_succ pp s (pc - 1) - | Iload(chunk, addr, args, dst, s) -> - fprintf pp "%a = %s[%a]\n" + | Iload(trap, chunk, addr, args, dst, s) -> + fprintf pp "%a = %s[%a]%a\n" reg dst (name_of_chunk chunk) - (PrintOp.print_addressing reg) (addr, args); + (PrintOp.print_addressing reg) (addr, args) + print_trapping_mode trap; print_succ pp s (pc - 1) | Istore(chunk, addr, args, src, s) -> fprintf pp "%s[%a] = %a\n" diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index 6432682a..1c7655fb 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -86,9 +86,10 @@ let print_instruction pp succ = function fprintf pp "(%a) = (%a) using %a, %a" vars dsts vars srcs var t1 var t2 | Xop(op, args, res) -> fprintf pp "%a = %a" var res (print_operation var) (op, args) - | Xload(chunk, addr, args, dst) -> - fprintf pp "%a = %s[%a]" - var dst (name_of_chunk chunk) (print_addressing var) (addr, args) + | Xload(trap, chunk, addr, args, dst) -> + fprintf pp "%a = %s[%a]%a" + var dst (name_of_chunk chunk) (print_addressing var) (addr, args) + print_trapping_mode trap | Xstore(chunk, addr, args, src) -> fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing var) (addr, args) var src diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 7db8a866..f2658b04 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -249,18 +249,18 @@ let block_of_RTL_instr funsig tyenv = function else let t = new_temp (tyenv res) in (t :: args2', t) in movelist args1 args3 (Xop(op, args3, res3) :: move res3 res1 [Xbranch s]) - | RTL.Iload(chunk, addr, args, dst, s) -> + | RTL.Iload(trap, chunk, addr, args, dst, s) -> if Archi.splitlong && chunk = Mint64 then begin match offset_addressing addr (coqint_of_camlint 4l) with | None -> assert false | Some addr' -> - [Xload(Mint32, addr, vregs tyenv args, + [Xload(trap, Mint32, addr, vregs tyenv args, V((if Archi.big_endian then dst else twin_reg dst), Tint)); - Xload(Mint32, addr', vregs tyenv args, + Xload(trap, Mint32, addr', vregs tyenv args, V((if Archi.big_endian then twin_reg dst else dst), Tint)); Xbranch s] end else - [Xload(chunk, addr, vregs tyenv args, vreg tyenv dst); Xbranch s] + [Xload(trap, chunk, addr, vregs tyenv args, vreg tyenv dst); Xbranch s] | RTL.Istore(chunk, addr, args, src, s) -> if Archi.splitlong && chunk = Mint64 then begin match offset_addressing addr (coqint_of_camlint 4l) with @@ -364,7 +364,7 @@ let live_before instr after = if VSet.mem res after then vset_addlist args (VSet.remove res after) else after - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> if VSet.mem dst after then vset_addlist args (VSet.remove dst after) else after @@ -459,7 +459,7 @@ let dce_instr instr after k = if VSet.mem res after then instr :: k else k - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> if VSet.mem dst after then instr :: k else k @@ -550,7 +550,7 @@ let spill_costs f = (* temps must not be spilled *) | Xop(op, args, res) -> charge_list 10 1 args; charge 10 1 res - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> charge_list 10 1 args; charge 10 1 dst | Xstore(chunk, addr, args, src) -> charge_list 10 1 args; charge 10 1 src @@ -677,7 +677,7 @@ let add_interfs_instr g instr live = (vset_addlist (res :: argl) (VSet.remove res live)) end; add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op) - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> add_interfs_def g dst live; add_interfs_destroyed g (VSet.remove dst live) (destroyed_by_load chunk addr) @@ -782,7 +782,7 @@ let tospill_instr alloc instr ts = ts | Xop(op, args, res) -> addlist_tospill alloc args (add_tospill alloc res ts) - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> addlist_tospill alloc args (add_tospill alloc dst ts) | Xstore(chunk, addr, args, src) -> addlist_tospill alloc args (add_tospill alloc src ts) @@ -964,10 +964,10 @@ let spill_instr tospill eqs instr = add res tmp (kill tmp (kill res eqs2))) end end - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> let (args', c1, eqs1) = reload_vars tospill eqs args in let (dst', c2, eqs2) = save_var tospill eqs1 dst in - (c1 @ Xload(chunk, addr, args', dst') :: c2, eqs2) + (c1 @ Xload(trap, chunk, addr, args', dst') :: c2, eqs2) | Xstore(chunk, addr, args, src) -> let (args', c1, eqs1) = reload_vars tospill eqs args in let (src', c2, eqs2) = reload_var tospill eqs1 src in @@ -1115,8 +1115,8 @@ let transl_instr alloc instr k = LTL.Lop(Omove, [rarg1], rres) :: LTL.Lop(op, rres :: rargl, rres) :: k end - | Xload(chunk, addr, args, dst) -> - LTL.Lload(chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k + | Xload(trap, chunk, addr, args, dst) -> + LTL.Lload(trap, chunk, addr, mregs_of alloc args, mreg_of alloc dst) :: k | Xstore(chunk, addr, args, src) -> LTL.Lstore(chunk, addr, mregs_of alloc args, mreg_of alloc src) :: k | Xcall(sg, vos, args, res) -> diff --git a/backend/Splitting.ml b/backend/Splitting.ml index 40f09c3d..78eb66a5 100644 --- a/backend/Splitting.ml +++ b/backend/Splitting.ml @@ -151,8 +151,8 @@ let ren_instr f maps pc i = | Inop s -> Inop s | Iop(op, args, res, s) -> Iop(op, ren_regs before args, ren_reg after res, s) - | Iload(chunk, addr, args, dst, s) -> - Iload(chunk, addr, ren_regs before args, ren_reg after dst, s) + | Iload(trap, chunk, addr, args, dst, s) -> + Iload(trap, chunk, addr, ren_regs before args, ren_reg after dst, s) | Istore(chunk, addr, args, src, s) -> Istore(chunk, addr, ren_regs before args, ren_reg before src, s) | Icall(sg, ros, args, res, s) -> diff --git a/backend/XTL.ml b/backend/XTL.ml index f10efeed..c496fafb 100644 --- a/backend/XTL.ml +++ b/backend/XTL.ml @@ -30,7 +30,7 @@ type instruction = | Xspill of var * var | Xparmove of var list * var list * var * var | Xop of operation * var list * var - | Xload of memory_chunk * addressing * var list * var + | Xload of trapping_mode * memory_chunk * addressing * var list * var | Xstore of memory_chunk * addressing * var list * var | Xcall of signature * (var, ident) sum * var list * var list | Xtailcall of signature * (var, ident) sum * var list @@ -159,7 +159,7 @@ let type_instr = function let (targs, tres) = type_of_operation op in set_vars_type args targs; set_var_type res tres - | Xload(chunk, addr, args, dst) -> + | Xload(trap, chunk, addr, args, dst) -> set_vars_type args (type_of_addressing addr); set_var_type dst (type_of_chunk chunk) | Xstore(chunk, addr, args, src) -> diff --git a/backend/XTL.mli b/backend/XTL.mli index 54988d4b..b4b77fab 100644 --- a/backend/XTL.mli +++ b/backend/XTL.mli @@ -31,7 +31,7 @@ type instruction = | Xspill of var * var | Xparmove of var list * var list * var * var | Xop of operation * var list * var - | Xload of memory_chunk * addressing * var list * var + | Xload of trapping_mode * memory_chunk * addressing * var list * var | Xstore of memory_chunk * addressing * var list * var | Xcall of signature * (var, ident) sum * var list * var list | Xtailcall of signature * (var, ident) sum * var list diff --git a/common/PrintAST.ml b/common/PrintAST.ml index e477957a..baddb722 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -90,3 +90,7 @@ let rec print_builtin_res px oc = function fprintf oc "splitlong(%a, %a)" (print_builtin_res px) hi (print_builtin_res px) lo +let print_trapping_mode oc = function + | TRAP -> () + | NOTRAP -> output_string oc " [notrap]" + |