diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-07 17:43:45 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-07 17:43:45 +0100 |
commit | 13b0e8f162f751a9bdbe9952ebe1f22eb77d0f87 (patch) | |
tree | a6837d6e7908865d420d1c209ec0b69321ab5ca0 | |
parent | 749fa737e57bb37539ee742f0df552fec8d3e4ef (diff) | |
parent | 0a6082e151cea873b4f7bf946a9e96450d785c2c (diff) | |
download | compcert-kvx-13b0e8f162f751a9bdbe9952ebe1f22eb77d0f87.tar.gz compcert-kvx-13b0e8f162f751a9bdbe9952ebe1f22eb77d0f87.zip |
Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
-rw-r--r-- | backend/Duplicate.v | 3 | ||||
-rw-r--r-- | backend/Duplicateaux.ml | 57 | ||||
-rw-r--r-- | backend/Duplicateproof.v | 2 | ||||
-rw-r--r-- | backend/LICMaux.ml | 43 | ||||
-rw-r--r-- | common/DebugPrint.ml | 118 | ||||
-rw-r--r-- | cparser/Machine.ml | 9 | ||||
-rw-r--r-- | cparser/Machine.mli | 1 | ||||
-rw-r--r-- | scheduling/RTLpathLivegenaux.ml | 56 | ||||
-rw-r--r-- | scheduling/RTLpathScheduleraux.ml | 215 | ||||
-rw-r--r-- | test/monniaux/yarpgen/Makefile | 14 |
10 files changed, 256 insertions, 262 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 7dea752b..40db4e45 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -203,8 +203,7 @@ Fixpoint verify_mapping_mn_rec dupmap f f' lm := match lm with | nil => OK tt | m :: lm => do u <- verify_mapping_mn dupmap f f' m; - do u2 <- verify_mapping_mn_rec dupmap f f' lm; - OK tt + verify_mapping_mn_rec dupmap f f' lm end. Definition verify_mapping_match_nodes dupmap (f f': function): res unit := diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 861df3cd..b3635527 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -22,9 +22,8 @@ open RTL open Maps open Camlcoq +open DebugPrint -let debug_flag = LICMaux.debug_flag -let debug = LICMaux.debug let get_loop_headers = LICMaux.get_loop_headers let get_some = LICMaux.get_some let rtl_successors = LICMaux.rtl_successors @@ -87,8 +86,6 @@ end module PSet = Set.Make(PInt) -let print_intlist = LICMaux.print_intlist - let print_intset s = let seq = PSet.to_seq s in begin @@ -101,18 +98,6 @@ let print_intset s = end end -let ptree_printbool pt = - let elements = PTree.elements pt - in begin - if !debug_flag then begin - Printf.printf "["; - List.iter (fun (n, b) -> - if b then Printf.printf "%d, " (P.to_int n) else () - ) elements; - Printf.printf "]" - end - end - (* Looks ahead (until a branch) to see if a node further down verifies * the given predicate *) let rec look_ahead_gen (successors: RTL.instruction -> P.t list) code node is_loop_header predicate = @@ -215,16 +200,6 @@ type innerLoop = { let print_pset = LICMaux.pp_pset -let print_ptree printer pt = - let elements = PTree.elements pt in - begin - debug "[\n"; - List.iter (fun (n, elt) -> - debug "\t%d: %a\n" (P.to_int n) printer elt - ) elements; - debug "]\n" - end - let rtl_successors_pref = function | Itailcall _ | Ireturn _ -> [] | Icall(_,_,_,_,n) | Ibuiltin(_,_,_,n) | Inop n | Iop (_,_,_,n) @@ -458,21 +433,21 @@ let update_direction direction = function | Some _ -> Icond (cond, lr, n, n', pred) ) | i -> i -let rec update_direction_rec directions = function -| [] -> PTree.empty -| m::lm -> let (n, i) = m - in let direction = get_some @@ PTree.get n directions - in PTree.set n (update_direction direction i) (update_direction_rec directions lm) - (* Uses branch prediction to write prediction annotations in Icond *) let update_directions f code entrypoint = begin debug "Update_directions\n"; - let directions = get_directions f code entrypoint - in begin + let directions = get_directions f code entrypoint in + let code' = ref code in + begin + debug "Get Directions done, now proceeding to update all direction information..\n"; (* debug "Ifso directions: "; ptree_printbool directions; debug "\n"; *) - update_direction_rec directions (PTree.elements code) + List.iter (fun (n, i) -> + let direction = get_some @@ PTree.get n directions in + code' := PTree.set n (update_direction direction i) !code' + ) (PTree.elements code); + !code' end end @@ -554,8 +529,6 @@ let print_traces oc traces = Printf.fprintf oc "Traces: {%a}\n" f traces end -let print_code code = LICMaux.print_code code - (* Dumb (but linear) trace selection *) let select_traces_linear code entrypoint = let is_visited = ref (PTree.map (fun n i -> false) code) in @@ -770,14 +743,6 @@ let invert_iconds code = * cyclic dependencies between LICMaux and Duplicateaux *) - - -let print_option_pint oc o = - if !debug_flag then - match o with - | None -> Printf.fprintf oc "None" - | Some n -> Printf.fprintf oc "Some %d" (P.to_int n) - let print_inner_loop iloop = debug "{preds: %a, body: %a, head: %d, finals: %a, sb_final: %a}\n" print_intlist iloop.preds @@ -794,8 +759,6 @@ let rec print_inner_loops = function print_inner_loops iloops end -let print_pint oc i = if !debug_flag then Printf.fprintf oc "%d" (P.to_int i) else () - let cb_exit_node = function | Icond (_,_,n1,n2,p) -> begin match p with | Some true -> Some n2 diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 2480ccf0..cc24104f 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -111,7 +111,7 @@ Proof. - monadInv H0. inversion H. - inversion H. + subst. monadInv H0. destruct x. assumption. - + monadInv H0. destruct x0. eapply IHlb; assumption. + + monadInv H0. destruct x. eapply IHlb; assumption. Qed. Lemma verify_is_copy_correct: diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index df98077b..1f6b8817 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -16,16 +16,11 @@ open Maps;; open Kildall;; open HashedSet;; open Inject;; +open DebugPrint;; type reg = P.t;; (** get_loop_headers moved from Duplicateaux.ml to LICMaux.ml to prevent cycle dependencies *) -let debug_flag = ref false - -let debug fmt = - if !debug_flag then (flush stderr; Printf.eprintf fmt) - else Printf.ifprintf stderr fmt - type vstate = Unvisited | Processed | Visited let get_some = function @@ -39,42 +34,6 @@ let rtl_successors = function | Icond (_,_,n1,n2,_) -> [n1; n2] | Ijumptable (_,ln) -> ln -let print_ptree_bool oc pt = - if !debug_flag then - let elements = PTree.elements pt in - begin - Printf.fprintf oc "["; - List.iter (fun (n, b) -> - if b then Printf.fprintf oc "%d, " (P.to_int n) - ) elements; - Printf.fprintf oc "]\n" - end - else () - -let print_intlist oc l = - let rec f oc = function - | [] -> () - | n::ln -> (Printf.fprintf oc "%d %a" (P.to_int n) f ln) - in begin - if !debug_flag then begin - Printf.fprintf oc "[%a]" f l - end - end - -(* Adapted from backend/PrintRTL.ml: print_function *) -let print_code code = let open PrintRTL in let open Printf in - if (!debug_flag) then begin - fprintf stdout "{\n"; - let instrs = - List.sort - (fun (pc1, _) (pc2, _) -> compare pc2 pc1) - (List.rev_map - (fun (pc, i) -> (P.to_int pc, i)) - (PTree.elements code)) in - List.iter (print_instruction stdout) instrs; - fprintf stdout "}" - end - (** Getting loop branches with a DFS visit : * Each node is either Unvisited, Visited, or Processed * pre-order: node becomes Processed diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml new file mode 100644 index 00000000..64efe727 --- /dev/null +++ b/common/DebugPrint.ml @@ -0,0 +1,118 @@ +open Maps +open Camlcoq +open Registers + +let debug_flag = ref false + +let debug fmt = + if !debug_flag then (flush stderr; Printf.eprintf fmt) + else Printf.ifprintf stderr fmt + +let print_ptree_bool oc pt = + if !debug_flag then + let elements = PTree.elements pt in + begin + Printf.fprintf oc "["; + List.iter (fun (n, b) -> + if b then Printf.fprintf oc "%d, " (P.to_int n) + ) elements; + Printf.fprintf oc "]\n" + end + else () + +let print_intlist oc l = + let rec f oc = function + | [] -> () + | n::ln -> (Printf.fprintf oc "%d %a" (P.to_int n) f ln) + in begin + if !debug_flag then begin + Printf.fprintf oc "[%a]" f l + end + end + +(* Adapted from backend/PrintRTL.ml: print_function *) +let print_code code = let open PrintRTL in let open Printf in + if (!debug_flag) then begin + fprintf stdout "{\n"; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements code)) in + List.iter (print_instruction stdout) instrs; + fprintf stdout "}" + end + +let ptree_printbool pt = + let elements = PTree.elements pt + in begin + if !debug_flag then begin + Printf.printf "["; + List.iter (fun (n, b) -> + if b then Printf.printf "%d, " (P.to_int n) else () + ) elements; + Printf.printf "]" + end + end + +let print_ptree printer pt = + let elements = PTree.elements pt in + begin + debug "[\n"; + List.iter (fun (n, elt) -> + debug "\t%d: %a\n" (P.to_int n) printer elt + ) elements; + debug "]\n" + end + +let print_option_pint oc o = + if !debug_flag then + match o with + | None -> Printf.fprintf oc "None" + | Some n -> Printf.fprintf oc "Some %d" (P.to_int n) + +let print_pint oc i = if !debug_flag then Printf.fprintf oc "%d" (P.to_int i) else () + +let print_regset rs = begin + debug "["; + List.iter (fun n -> debug "%d " (P.to_int n)) (Regset.elements rs); + debug "]" +end + +let print_ptree_regset pt = begin + debug "["; + List.iter (fun (n, rs) -> + debug "\n\t"; + debug "%d: " (P.to_int n); + print_regset rs + ) (PTree.elements pt); + debug "]" +end + +let print_true_nodes booltree = begin + debug "["; + List.iter (fun (n,b) -> + if b then debug "%d " (P.to_int n) + ) (PTree.elements booltree); + debug "]"; +end + + +let print_instructions insts code = + let get_some = function + | None -> failwith "Did not get some" + | Some thing -> thing + in if (!debug_flag) then begin + debug "[ "; + List.iter ( + fun n -> (PrintRTL.print_instruction stdout (P.to_int n, get_some @@ PTree.get n code)) + ) insts; debug "]" + end + +let print_arrayp arr = begin + debug "[| "; + Array.iter (fun n -> debug "%d, " (P.to_int n)) arr; + debug "|]" +end + diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 97ca9223..73b71ea0 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -61,6 +61,7 @@ type t = { supports_unaligned_accesses: bool; struct_passing_style: struct_passing_style; struct_return_style : struct_return_style; + has_non_trapping_loads : bool; } let ilp32ll64 = { @@ -96,6 +97,7 @@ let ilp32ll64 = { supports_unaligned_accesses = false; struct_passing_style = SP_ref_callee; struct_return_style = SR_ref; + has_non_trapping_loads = false; } let i32lpll64 = { @@ -131,6 +133,7 @@ let i32lpll64 = { supports_unaligned_accesses = false; struct_passing_style = SP_ref_callee; struct_return_style = SR_ref; + has_non_trapping_loads = false; } let il32pll64 = { @@ -166,6 +169,7 @@ let il32pll64 = { supports_unaligned_accesses = false; struct_passing_style = SP_ref_callee; struct_return_style = SR_ref; + has_non_trapping_loads = false; } (* Canned configurations for some ABIs *) @@ -270,7 +274,9 @@ let kvx = bitfields_msb_first = false; (* TO CHECK *) supports_unaligned_accesses = true; struct_passing_style = SP_value32_ref_callee; - struct_return_style = SR_int1to4 } + struct_return_style = SR_int1to4; + has_non_trapping_loads = true; +} let aarch64 = { i32lpll64 with name = "aarch64"; @@ -323,6 +329,7 @@ let undef = { supports_unaligned_accesses = false; struct_passing_style = SP_ref_callee; struct_return_style = SR_ref; + has_non_trapping_loads = false; } (* The current configuration. Must be initialized before use. *) diff --git a/cparser/Machine.mli b/cparser/Machine.mli index 0e1e22d1..54436758 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -60,6 +60,7 @@ type t = { supports_unaligned_accesses: bool; struct_passing_style: struct_passing_style; struct_return_style: struct_return_style; + has_non_trapping_loads: bool; } (* The current configuration *) diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml index dd971db8..ab921954 100644 --- a/scheduling/RTLpathLivegenaux.ml +++ b/scheduling/RTLpathLivegenaux.ml @@ -6,13 +6,7 @@ open Camlcoq open Datatypes open Kildall open Lattice - -let debug_flag = ref false - -let dprintf fmt = let open Printf in - match !debug_flag with - | true -> printf fmt - | false -> ifprintf stdout fmt +open DebugPrint let get_some = function | None -> failwith "Got None instead of Some _" @@ -122,22 +116,6 @@ let get_path_map code entry join_points = !path_map end -let print_regset rs = begin - dprintf "["; - List.iter (fun n -> dprintf "%d " (P.to_int n)) (Regset.elements rs); - dprintf "]" -end - -let print_ptree_regset pt = begin - dprintf "["; - List.iter (fun (n, rs) -> - dprintf "\n\t"; - dprintf "%d: " (P.to_int n); - print_regset rs - ) (PTree.elements pt); - dprintf "]" -end - let transfer f pc after = let open Liveness in match PTree.get pc f.fn_code with | Some i -> @@ -257,7 +235,7 @@ let set_pathmap_liveness f pm = let new_pm = ref PTree.empty in let code = f.fn_code in begin - dprintf "Liveness: "; print_ptree_regset liveness; dprintf "\n"; + debug "Liveness: "; print_ptree_regset liveness; debug "\n"; List.iter (fun (n, pi) -> let inputs = get_some @@ PTree.get n liveness in let outputs = get_outputs liveness code n pi in @@ -267,31 +245,23 @@ let set_pathmap_liveness f pm = !new_pm end -let print_true_nodes booltree = begin - dprintf "["; - List.iter (fun (n,b) -> - if b then dprintf "%d " (P.to_int n) - ) (PTree.elements booltree); - dprintf "]"; -end - let print_path_info pi = begin - dprintf "(psize=%d; " (Camlcoq.Nat.to_int pi.psize); - dprintf "input_regs="; + debug "(psize=%d; " (Camlcoq.Nat.to_int pi.psize); + debug "input_regs="; print_regset pi.input_regs; - dprintf "; output_regs="; + debug "; output_regs="; print_regset pi.output_regs; - dprintf ")" + debug ")" end let print_path_map path_map = begin - dprintf "["; + debug "["; List.iter (fun (n,pi) -> - dprintf "\n\t"; - dprintf "%d: " (P.to_int n); + debug "\n\t"; + debug "%d: " (P.to_int n); print_path_info pi ) (PTree.elements path_map); - dprintf "]" + debug "]" end let build_path_map f = @@ -300,10 +270,10 @@ let build_path_map f = let join_points = get_join_points code entry in let path_map = set_pathmap_liveness f @@ get_path_map code entry join_points in begin - dprintf "Join points: "; + debug "Join points: "; print_true_nodes join_points; - dprintf "\nPath map: "; + debug "\nPath map: "; print_path_map path_map; - dprintf "\n"; + debug "\n"; path_map end diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml index 66910bdf..a294d0b5 100644 --- a/scheduling/RTLpathScheduleraux.ml +++ b/scheduling/RTLpathScheduleraux.ml @@ -4,6 +4,10 @@ open Maps open RTLpathLivegenaux open Registers open Camlcoq +open Machine +open DebugPrint + +let config = Machine.config type superblock = { instructions: P.t array; (* pointers to code instructions *) @@ -15,54 +19,26 @@ type superblock = { typing: RTLtyping.regenv } -let print_instructions insts code = - if (!debug_flag) then begin - dprintf "[ "; - List.iter ( - fun n -> (PrintRTL.print_instruction stdout (P.to_int n, get_some @@ PTree.get n code)) - ) insts; dprintf "]" - end - let print_superblock sb code = let insts = sb.instructions in let li = sb.liveins in let outs = sb.output_regs in begin - dprintf "{ instructions = "; print_instructions (Array.to_list insts) code; dprintf "\n"; - dprintf " liveins = "; print_ptree_regset li; dprintf "\n"; - dprintf " output_regs = "; print_regset outs; dprintf "}" + debug "{ instructions = "; print_instructions (Array.to_list insts) code; debug "\n"; + debug " liveins = "; print_ptree_regset li; debug "\n"; + debug " output_regs = "; print_regset outs; debug "}" end let print_superblocks lsb code = let rec f = function | [] -> () - | sb :: lsb -> (print_superblock sb code; dprintf ",\n"; f lsb) + | sb :: lsb -> (print_superblock sb code; debug ",\n"; f lsb) in begin - dprintf "[\n"; + debug "[\n"; f lsb; - dprintf "]" + debug "]" end -(* Adapted from backend/PrintRTL.ml: print_function *) -let print_code code = let open PrintRTL in let open Printf in - if (!debug_flag) then begin - fprintf stdout "{\n"; - let instrs = - List.sort - (fun (pc1, _) (pc2, _) -> compare pc2 pc1) - (List.rev_map - (fun (pc, i) -> (P.to_int pc, i)) - (PTree.elements code)) in - List.iter (print_instruction stdout) instrs; - fprintf stdout "}" - end - -let print_arrayp arr = begin - dprintf "[| "; - Array.iter (fun n -> dprintf "%d, " (P.to_int n)) arr; - dprintf "|]" -end - let get_superblocks code entry pm typing = let visited = ref (PTree.map (fun n i -> false) code) in let rec get_superblocks_rec pc = @@ -100,7 +76,7 @@ let get_superblocks code entry pm typing = end in let lsb = get_superblocks_rec entry in begin (* debug_flag := true; *) - dprintf "Superblocks identified:"; print_superblocks lsb code; dprintf "\n"; + debug "Superblocks identified:"; print_superblocks lsb code; debug "\n"; (* debug_flag := false; *) lsb end @@ -219,11 +195,45 @@ let sinst_to_rinst = function ) | Send i -> i +let is_a_cb = function Icond _ -> true | _ -> false +let is_a_load = function Iload _ -> true | _ -> false + +let find_array arr n = + let index = ref None in + begin + Array.iteri (fun i n' -> + if n = n' then + match !index with + | Some _ -> failwith "More than one element present" + | None -> index := Some i + ) arr; + !index + end + +let rec hashedset_from_list = function + | [] -> HashedSet.PSet.empty + | n::ln -> HashedSet.PSet.add n (hashedset_from_list ln) + +let hashedset_map f hs = hashedset_from_list @@ List.map f @@ HashedSet.PSet.elements hs + let apply_schedule code sb new_order = let tc = ref code in let old_order = sb.instructions in - begin + let count_cbs order code = + let current_cbs = ref HashedSet.PSet.empty in + let cbs_above = ref PTree.empty in + Array.iter (fun n -> + let inst = get_some @@ PTree.get n code in + if is_a_cb inst then current_cbs := HashedSet.PSet.add n !current_cbs + else if is_a_load inst then cbs_above := PTree.set n !current_cbs !cbs_above + ) order; + !cbs_above + in let fmap n = + let index = get_some @@ find_array new_order n in + old_order.(index) + in begin check_order code old_order new_order; + (* First pass - modify the positions, nothing else *) Array.iteri (fun i n' -> let inst' = get_some @@ PTree.get n' code in let iend = Array.length old_order - 1 in @@ -246,103 +256,56 @@ let apply_schedule code sb new_order = @@ rinst_to_sinst inst' in tc := PTree.set (Array.get old_order i) new_inst !tc ) new_order; + (* Second pass - turn the loads back into trapping when it was not needed *) + (* 1) We remember which CBs are "above" a given load *) + let cbs_above = count_cbs old_order code in + (* 2) We do the same for new_order *) + let cbs_above' = count_cbs (Array.map fmap new_order) !tc in + (* 3) We examine each load, turn it back into trapping if cbs_above is included in cbs_above' *) + Array.iter (fun n -> + let n' = fmap n in + let inst' = get_some @@ PTree.get n' !tc in + match inst' with + | Iload (t,a,b,c,d,s) -> + let pset = hashedset_map fmap @@ get_some @@ PTree.get n cbs_above in + let pset' = get_some @@ PTree.get n' cbs_above' in + if HashedSet.PSet.is_subset pset pset' then tc := PTree.set n' (Iload (AST.TRAP,a,b,c,d,s)) !tc + else assert !config.has_non_trapping_loads + | _ -> () + ) old_order; !tc end - (* -let main_successors = function -| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> [n] -| Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> [n] -| Icond (_,_,n1,n2,p) -> ( - match p with - | Some true -> [n1; n2] - | Some false -> [n2; n1] - | None -> [n1; n2] ) -| Ijumptable _ | Itailcall _ | Ireturn _ -> [] - -let change_predicted_successor i s = match i with - | Itailcall _ | Ireturn _ -> failwith "Wrong instruction (5) - Tailcalls and returns should not be moved in the middle of a superblock" - | Ijumptable _ -> failwith "Wrong instruction (6) - Jumptables should not be moved in the middle of a superblock" - | Inop n -> Inop s - | Iop (a,b,c,n) -> Iop (a,b,c,s) - | Iload (a,b,c,d,e,n) -> Iload (a,b,c,d,e,s) - | Istore (a,b,c,d,n) -> Istore (a,b,c,d,s) - | Icall (a,b,c,d,n) -> Icall (a,b,c,d,s) - | Ibuiltin (a,b,c,n) -> Ibuiltin (a,b,c,s) - | Icond (a,b,n1,n2,p) -> ( - match p with - | Some true -> Icond (a,b,s,n2,p) - | Some false -> Icond (a,b,n1,s,p) - | None -> failwith "Predicted a successor for an Icond with p=None - unpredicted CB should not be moved in the middle of the superblock" - ) - -let rec change_successors i = function - | [] -> ( - match i with - | Itailcall _ | Ireturn _ -> i - | _ -> failwith "Wrong instruction (1)") - | [s] -> ( - match i with - | Inop n -> Inop s - | Iop (a,b,c,n) -> Iop (a,b,c,s) - | Iload (a,b,c,d,e,n) -> Iload (a,b,c,d,e,s) - | Istore (a,b,c,d,n) -> Istore (a,b,c,d,s) - | Icall (a,b,c,d,n) -> Icall (a,b,c,d,s) - | Ibuiltin (a,b,c,n) -> Ibuiltin (a,b,c,s) - | Ijumptable (a,[n]) -> Ijumptable (a,[s]) - | Icond (a,b,n1,n2,p) -> ( - match p with - | Some true -> Icond (a,b,s,n2,p) - | Some false -> Icond (a,b,n1,s,p) - | None -> failwith "Icond Wrong instruction (2) ; should not happen?" - ) - | _ -> failwith "Wrong instruction (2)") - | [s1; s2] -> ( - match i with - | Icond (a,b,n1,n2,p) -> Icond (a,b,s1,s2,p) - | Ijumptable (a, [n1; n2]) -> Ijumptable (a, [s1; s2]) - | _ -> change_successors i [s1]) - | ls -> ( - match i with - | Ijumptable (a, ln) -> begin - assert ((List.length ln) == (List.length ls)); - Ijumptable (a, ls) - end - | _ -> failwith "Wrong instruction (4)") - - -let apply_schedule code sb new_order = - let tc = ref code in - let old_order = sb.instructions in - let last_node = Array.get old_order (Array.length old_order - 1) in - let last_successors = main_successors - @@ get_some @@ PTree.get last_node code in - begin - check_order code old_order new_order; - Array.iteri (fun i n' -> - let inst' = get_some @@ PTree.get n' code in - let new_inst = - if (i == (Array.length old_order - 1)) then - change_successors inst' last_successors - else - change_predicted_successor inst' (Array.get old_order (i+1)) - in tc := PTree.set (Array.get old_order i) new_inst !tc - ) new_order; - !tc +let turn_all_loads_nontrap sb code = + if not !config.has_non_trapping_loads then code + else begin + let code' = ref code in + Array.iter (fun n -> + let inst = get_some @@ PTree.get n code in + match inst with + | Iload (t,a,b,c,d,s) -> code' := PTree.set n (Iload (AST.NOTRAP,a,b,c,d,s)) !code' + | _ -> () + ) sb.instructions; + !code' end -*) let rec do_schedule code = function | [] -> code | sb :: lsb -> - let schedule = schedule_superblock sb code in - let new_code = apply_schedule code sb schedule in + (* Trick: instead of turning loads into non trap as needed.. + * First, we turn them all into non-trap. + * Then, we turn back those who didn't need to be turned, into TRAP again + * This is because the scheduler (rightfully) refuses to schedule ahead of a branch + * operations that might trap *) + let code' = turn_all_loads_nontrap sb code in + let schedule = schedule_superblock sb code' in + let new_code = apply_schedule code' sb schedule in begin (* debug_flag := true; *) - dprintf "Old Code: "; print_code code; - dprintf "\nSchedule to apply: "; print_arrayp schedule; - dprintf "\nNew Code: "; print_code new_code; - dprintf "\n"; + debug "Old Code: "; print_code code; + debug "\nSchedule to apply: "; print_arrayp schedule; + debug "\nNew Code: "; print_code new_code; + debug "\n"; (* debug_flag := false; *) do_schedule new_code lsb end @@ -358,10 +321,10 @@ let scheduler f = let lsb = get_superblocks code entry pm typing in begin (* debug_flag := true; *) - dprintf "Pathmap:\n"; dprintf "\n"; + debug "Pathmap:\n"; debug "\n"; print_path_map pm; - dprintf "Superblocks:\n"; - print_superblocks lsb code; dprintf "\n"; + debug "Superblocks:\n"; + print_superblocks lsb code; debug "\n"; (* debug_flag := false; *) let tc = do_schedule code lsb in (((tc, entry), pm), id_ptree) diff --git a/test/monniaux/yarpgen/Makefile b/test/monniaux/yarpgen/Makefile index 24dd19c3..f9efd5a0 100644 --- a/test/monniaux/yarpgen/Makefile +++ b/test/monniaux/yarpgen/Makefile @@ -39,6 +39,20 @@ TESTS_GCC_TARGET_OUT=$(shell seq --format $(PREFIX)/example.gcc.target.out 1 $(M TESTS_GCC_HOST_OUT=$(shell seq --format $(PREFIX)/example.gcc.host.out 1 $(MAX)) TESTS_CMP=$(shell seq --format $(PREFIX)/example.target.cmp 1 $(MAX)) # $(shell seq --format $(PREFIX)/example.host_target.cmp 1 $(MAX)) +# FIXME - test000089 fails in CI in arm and armhf because of memory consumption during register allocation being too high +# Removing it from the pool +BADID:=89 +TESTS_C:=$(filter-out $(shell seq --format $(PREFIX)/func.c $(BADID) $(BADID)),$(TESTS_C)) +TESTS_C:=$(filter-out $(shell seq --format $(PREFIX)/driver.c $(BADID) $(BADID)),$(TESTS_C)) +TESTS_C:=$(filter-out $(shell seq --format $(PREFIX)/init.c $(BADID) $(BADID)),$(TESTS_C)) +TESTS_C:=$(filter-out $(shell seq --format $(PREFIX)/hash.c $(BADID) $(BADID)),$(TESTS_C)) +TESTS_C:=$(filter-out $(shell seq --format $(PREFIX)/check.c $(BADID) $(BADID)),$(TESTS_C)) +TESTS_C:=$(filter-out $(shell seq --format $(PREFIX)/init.h $(BADID) $(BADID)),$(TESTS_C)) +TESTS_CMP:=$(filter-out $(shell seq --format $(PREFIX)/example.target.cmp $(BADID) $(BADID)),$(TESTS_CMP)) +TESTS_GCC_HOST_OUT:=$(filter-out $(shell seq --format $(PREFIX)/example.gcc.host.out $(BADID) $(BADID)),$(TESTS_GCC_HOST_OUT)) +TESTS_CCOMP_TARGET_OUT:=$(filter-out $(shell seq --format $(PREFIX)/example.ccomp.target.out $(BADID) $(BADID)),$(TESTS_CCOMP_TARGET_OUT)) +TESTS_GCC_TARGET_OUT:=$(filter-out $(shell seq --format $(PREFIX)/example.gcc.target.out $(BADID) $(BADID)),$(TESTS_GCC_TARGET_OUT)) + all: $(TESTS_CCOMP_TARGET_OUT) $(TESTS_GCC_TARGET_OUT) $(TESTS_CCOMP_TARGET_S) $(TESTS_GCC_TARGET_S) $(TESTS_CMP) $(TESTS_C) tests_c: $(TESTS_C) |