diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-22 11:25:08 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-22 11:25:08 +0200 |
commit | ac7b7bd5e911d21439615263e5fd9d132c0e7fba (patch) | |
tree | 8fb2c1fe7d43f980116e1eb3a4c4fe7de579cc68 | |
parent | dff562c47c47fcac90c116782c92b692f2bb9bf9 (diff) | |
parent | a05f92785ffa93e4001d2a2e9a630351593fabc2 (diff) | |
download | compcert-kvx-ac7b7bd5e911d21439615263e5fd9d132c0e7fba.tar.gz compcert-kvx-ac7b7bd5e911d21439615263e5fd9d132c0e7fba.zip |
Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
-rw-r--r-- | Makefile | 1 | ||||
-rw-r--r-- | aarch64/Machregs.v | 2 | ||||
-rw-r--r-- | aarch64/TargetPrinter.ml | 4 | ||||
-rw-r--r-- | backend/Duplicateaux.ml | 355 | ||||
-rw-r--r-- | backend/LICMaux.ml | 32 | ||||
-rw-r--r-- | backend/Linearizeaux.ml | 442 | ||||
-rw-r--r-- | common/DebugPrint.ml | 28 | ||||
-rwxr-xr-x | configure | 1 | ||||
-rw-r--r-- | cparser/Machine.ml | 12 | ||||
-rw-r--r-- | cparser/Machine.mli | 3 | ||||
-rw-r--r-- | doc/index-kvx.html | 2 | ||||
-rw-r--r-- | driver/Configuration.ml | 1 | ||||
-rw-r--r-- | driver/Configuration.mli | 3 | ||||
-rw-r--r-- | driver/Frontend.ml | 5 | ||||
-rw-r--r-- | scheduling/RTLpathLivegenaux.ml | 30 | ||||
-rw-r--r-- | test/monniaux/profiling/compcert_profiling.dat | bin | 0 -> 96 bytes | |||
-rwxr-xr-x | test/monniaux/profiling/test_profiling | bin | 0 -> 14144 bytes | |||
-rw-r--r-- | test/monniaux/profiling/test_profiling.c | 15 |
18 files changed, 370 insertions, 566 deletions
@@ -297,6 +297,7 @@ compcert.ini: Makefile.config echo "linker_options=$(CLINKER_OPTIONS)";\ echo "arch=$(ARCH)"; \ echo "model=$(MODEL)"; \ + echo "os=$(OS)"; \ echo "abi=$(ABI)"; \ echo "endianness=$(ENDIANNESS)"; \ echo "system=$(SYSTEM)"; \ diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index 3d27f48f..bfe23e83 100644 --- a/aarch64/Machregs.v +++ b/aarch64/Machregs.v @@ -158,7 +158,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => R15 :: R17 :: R29 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob - | EF_profiling _ _ => R15 :: R17 :: nil + | EF_profiling _ _ => R15 :: R17 :: R29 :: nil | _ => nil end. diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 9ec1d563..53959152 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -231,8 +231,8 @@ module Target (*: TARGET*) = fprintf oc "%s:\n" lbl; fprintf oc " ldaxr x17, [x15]\n"; fprintf oc " add x17, x17, 1\n"; - fprintf oc " stlxr w17, x17, [x15]\n"; - fprintf oc " cbnz w17, %s\n" lbl; + fprintf oc " stlxr w29, x17, [x15]\n"; + fprintf oc " cbnz w29, %s\n" lbl; fprintf oc "%s end profiling %a %d\n" comment Profilingaux.pp_id id kind;; diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index b3635527..d55da64a 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -24,6 +24,76 @@ open Maps open Camlcoq open DebugPrint +let stats_oc = ref None + +let set_stats_oc () = + try + let name = Sys.getenv "COMPCERT_PREDICT_STATS" in + let oc = open_out_gen [Open_append; Open_creat; Open_text] 0o666 name in + stats_oc := Some oc + with Not_found -> () + +(* number of total CBs *) +let stats_nb_total = ref 0 +(* we predicted the same thing as the profiling *) +let stats_nb_correct_predicts = ref 0 +(* we predicted something (say Some true), but the profiling predicted the opposite (say Some false) *) +let stats_nb_mispredicts = ref 0 +(* we did not predict anything (None) even though the profiling did predict something *) +let stats_nb_missed_opportunities = ref 0 +(* we predicted something (say Some true) but the profiling preferred not to predict anything (None) *) +let stats_nb_overpredict = ref 0 + +(* heuristic specific counters *) +let wrong_opcode = ref 0 +let wrong_return = ref 0 +let wrong_loop2 = ref 0 +let wrong_loop = ref 0 +let wrong_call = ref 0 + +let right_opcode = ref 0 +let right_return = ref 0 +let right_loop2 = ref 0 +let right_loop = ref 0 +let right_call = ref 0 + +let reset_stats () = begin + stats_nb_total := 0; + stats_nb_correct_predicts := 0; + stats_nb_mispredicts := 0; + stats_nb_missed_opportunities := 0; + stats_nb_overpredict := 0; + wrong_opcode := 0; + wrong_return := 0; + wrong_loop2 := 0; + wrong_loop := 0; + wrong_call := 0; + right_opcode := 0; + right_return := 0; + right_loop2 := 0; + right_loop := 0; + right_call := 0; +end + +let incr theref = theref := !theref + 1 + +let has_some o = match o with Some _ -> true | None -> false + +let stats_oc_recording () = has_some !stats_oc + +let write_stats_oc () = + match !stats_oc with + | None -> () + | Some oc -> begin + Printf.fprintf oc "%d %d %d %d %d %d %d %d %d %d %d %d %d %d %d\n" !stats_nb_total + !stats_nb_correct_predicts !stats_nb_mispredicts !stats_nb_missed_opportunities + !stats_nb_overpredict + !wrong_opcode !wrong_return !wrong_loop2 !wrong_loop !wrong_call + !right_opcode !right_return !right_loop2 !right_loop !right_call + ; + close_out oc + end + let get_loop_headers = LICMaux.get_loop_headers let get_some = LICMaux.get_some let rtl_successors = LICMaux.rtl_successors @@ -270,120 +340,66 @@ let get_inner_loops f code is_loop_header = ) (PTree.elements loopmap) end +let get_loop_bodies code entrypoint = + let predecessors = get_predecessors_rtl code in + (* Algorithm from Muchnik, Compiler Design & Implementation, Figure 7.21 page 192 *) + let natural_loop n m = + debug "Natural Loop from %d to %d\n" (P.to_int n) (P.to_int m); + let in_body = ref (PTree.map (fun n b -> false) code) in + let body = ref [] in + let add_to_body n = begin + in_body := PTree.set n true !in_body; + body := n :: !body + end + in let rec process_node p = + debug " Processing node %d\n" (P.to_int p); + List.iter (fun pred -> + debug " Looking at predecessor of %d: %d\n" (P.to_int p) (P.to_int pred); + let is_in_body = get_some @@ PTree.get pred !in_body in + if (not @@ is_in_body) then begin + debug " --> adding to body\n"; + add_to_body pred; + process_node pred + end + ) (get_some @@ PTree.get p predecessors) + in begin + add_to_body m; + add_to_body n; + (if (m != n) then process_node m); + !body + end + in let option_natural_loop n = function + | None -> None + | Some m -> Some (natural_loop n m) + in PTree.map option_natural_loop (LICMaux.get_loop_backedges code entrypoint) -(* Returns a PTree of either None or Some b where b determines the node following the loop, for a cb instruction *) -(* It uses the fact that loops in CompCert are done by a branch (backedge) instruction followed by a cb *) +(* Returns a PTree of either None or Some b where b determines the node in the loop body, for a cb instruction *) let get_loop_info f is_loop_header bfs_order code = - debug "GET LOOP INFO\n"; - debug "==================================\n"; let loop_info = ref (PTree.map (fun n i -> None) code) in - let mark_path n lbody = - let cb_info = ref PTree.empty in - let visited = ref (PTree.map (fun n i -> false) code) in - (* Returns true if there is a path from src to dest (not involving jumptables) *) - (* Mark nodes as visited along the way *) - let explore src dest = - debug "Trying to dive a path from %d to %d\n" (P.to_int src) (P.to_int dest); - (* Memoizing the results to avoid exponential blow-up *) - let memory = ref PTree.empty in - let rec explore_rec src = - debug "explore_rec %d vs %d... " (P.to_int src) (P.to_int dest); - if (P.to_int src) == (P.to_int dest) then (debug "FOUND\n"; true) - else if (get_some @@ PTree.get src !visited) then (debug "VISITED... :( \n"; false) - (* if we went out of the innermost loop *) - else if (not @@ List.mem src lbody) then (debug "Out of innermost...\n"; false) - else begin - let inst = get_some @@ PTree.get src code in - visited := PTree.set src true !visited; - match rtl_successors inst with - | [] -> false - | [s] -> explore_wrap s - | [s1; s2] -> let snapshot_visited = ref !visited in begin - debug "\t\tSplit at %d: either %d or %d\n" (P.to_int src) (P.to_int s1) (P.to_int s2); - (* Remembering that we tried the ifso node *) - cb_info := PTree.set src true !cb_info; - match explore_wrap s1 with - | true -> ( - visited := !snapshot_visited; - match explore_wrap s2 with - | true -> begin - (* Both paths lead to a loop: we cannot predict the CB - * (but the explore still succeeds) *) - cb_info := PTree.remove src !cb_info; - true - end - | false -> true (* nothing to do, the explore succeeded *) - ) - | false -> begin - cb_info := PTree.set src false !cb_info; - match explore_wrap s2 with - | true -> true - | false -> (cb_info := PTree.remove src !cb_info; false) - end - end - | _ -> false + let mark_body body = + List.iter (fun n -> + match get_some @@ PTree.get n code with + | Icond (_, _, ifso, ifnot, _) -> begin + match PTree.get n !loop_info with + | None -> () + | Some _ -> + let b1 = List.mem ifso body in + let b2 = List.mem ifnot body in + if (b1 && b2) then () + else if (b1 || b2) then begin + if b1 then loop_info := PTree.set n (Some true) !loop_info + else if b2 then loop_info := PTree.set n (Some false) !loop_info + end end - and explore_wrap src = begin - match PTree.get src !memory with - | Some b -> b - | None -> - let result = explore_rec src in - (memory := PTree.set src result !memory; result) - end in explore_wrap src - (* Goes forward until a CB is encountered - * Returns None if no CB was found, or Some the_cb_node - * Marks nodes as visited along the way *) - in let rec advance_to_cb src = - if (get_some @@ PTree.get src !visited) then None - else begin - visited := PTree.set src true !visited; - match get_some @@ PTree.get src code with - | Inop s | Iop (_, _, _, s) | Iload (_,_,_,_,_,s) | Istore (_,_,_,_,s) | Icall (_,_,_,_,s) - | Ibuiltin (_,_,_,s) -> advance_to_cb s - | Icond _ -> Some src - | Ijumptable _ | Itailcall _ | Ireturn _ -> None - end - in begin - debug "Attempting to find natural loop from HEAD %d..\n" (P.to_int n); - match advance_to_cb n with - | None -> (debug "\tNo CB found\n") - | Some s -> ( debug "\tFound a CB! %d\n" (P.to_int s); - match get_some @@ PTree.get s !loop_info with - | None | Some _ -> begin - match get_some @@ PTree.get s code with - | Icond (_, _, n1, n2, _) -> ( - let b1 = explore n1 n in - let b2 = explore n2 n in - if (b1 && b2) then - debug "\tBoth paths lead back to the head: NONE\n" - else if (b1 || b2) then begin - if b1 then begin - debug "\tTrue path leads to the head: TRUE\n"; - loop_info := PTree.set s (Some true) !loop_info; - end else if b2 then begin - debug "\tFalse path leads to the head: FALSE\n"; - loop_info := PTree.set s (Some false) !loop_info - end; - debug "\tSetting other CBs encountered..\n"; - List.iter (fun (cb, dir) -> - debug "\t\t%d is %B\n" (P.to_int cb) dir; - loop_info := PTree.set cb (Some dir) !loop_info - ) (PTree.elements !cb_info) - end else - debug "\tNo path leads back to the head: NONE\n" - ) - | _ -> failwith "\tNot an Icond\n" - end - (* | Some _ -> ( debug "already loop info there\n" ) FIXME - we don't know yet whether a branch to a loop head is a backedge or not *) - ) - end - in let iloops = get_inner_loops f code is_loop_header in - begin - List.iter (fun il -> mark_path il.head il.body) iloops; - (* List.iter mark_path @@ List.filter (fun n -> get_some @@ PTree.get n is_loop_header) bfs_order; *) - debug "==================================\n"; - !loop_info - end + | _ -> () + ) body + in let bodymap = get_loop_bodies code f.fn_entrypoint in + List.iter (fun (_,obody) -> + match obody with + | None -> () + | Some body -> mark_body body + ) (PTree.elements bodymap); + !loop_info (* Remark - compared to the original Branch Prediction for Free paper, we don't use the store heuristic *) let get_directions f code entrypoint = begin @@ -397,28 +413,59 @@ let get_directions f code entrypoint = begin (* debug "\n"; *) List.iter (fun n -> match (get_some @@ PTree.get n code) with - | Icond (cond, lr, ifso, ifnot, pred) -> - (match pred with Some _ -> debug "RTL node %d already has prediction information\n" (P.to_int n) - | None -> - (* debug "Analyzing %d.." (P.to_int n); *) - let heuristics = [ do_opcode_heuristic; - do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic; - (* do_store_heuristic *) ] in - let preferred = ref None in - begin - debug "Deciding condition for RTL node %d\n" (P.to_int n); - List.iter (fun do_heur -> - match !preferred with - | None -> preferred := do_heur code cond ifso ifnot is_loop_header - | Some _ -> () - ) heuristics; - directions := PTree.set n !preferred !directions; - (match !preferred with | Some false -> debug "\tFALLTHROUGH\n" - | Some true -> debug "\tBRANCH\n" - | None -> debug "\tUNSURE\n"); - debug "---------------------------------------\n" - end - ) + | Icond (cond, lr, ifso, ifnot, pred) -> begin + if stats_oc_recording () || not @@ has_some pred then + (* debug "Analyzing %d.." (P.to_int n); *) + let heuristics = [ do_opcode_heuristic; + do_return_heuristic; do_loop2_heuristic loop_info n; do_loop_heuristic; do_call_heuristic; + (* do_store_heuristic *) ] in + let preferred = ref None in + let current_heuristic = ref 0 in + begin + debug "Deciding condition for RTL node %d\n" (P.to_int n); + List.iter (fun do_heur -> + match !preferred with + | None -> begin + preferred := do_heur code cond ifso ifnot is_loop_header; + if stats_oc_recording () then begin + (* Getting stats about mispredictions from each heuristic *) + (match !preferred, pred with + | Some false, Some true + | Some true, Some false + (* | Some _, None *) (* Uncomment for overpredicts *) + -> begin + match !current_heuristic with + | 0 -> incr wrong_opcode + | 1 -> incr wrong_return + | 2 -> incr wrong_loop2 + | 3 -> incr wrong_loop + | 4 -> incr wrong_call + | _ -> failwith "Shouldn't happen" + end + | Some false, Some false + | Some true, Some true -> begin + match !current_heuristic with + | 0 -> incr right_opcode + | 1 -> incr right_return + | 2 -> incr right_loop2 + | 3 -> incr right_loop + | 4 -> incr right_call + | _ -> failwith "Shouldn't happen" + end + | _ -> () + ); + incr current_heuristic + end + end + | Some _ -> () + ) heuristics; + directions := PTree.set n !preferred !directions; + (match !preferred with | Some false -> debug "\tFALLTHROUGH\n" + | Some true -> debug "\tBRANCH\n" + | None -> debug "\tUNSURE\n"); + debug "---------------------------------------\n" + end + end | _ -> () ) bfs_order; !directions @@ -426,11 +473,28 @@ let get_directions f code entrypoint = begin end let update_direction direction = function -| Icond (cond, lr, n, n', pred) -> +| Icond (cond, lr, n, n', pred) -> begin + (* Counting stats from profiling *) + if stats_oc_recording () then begin + incr stats_nb_total; + match pred, direction with + | None, None -> incr stats_nb_correct_predicts + | None, Some _ -> incr stats_nb_overpredict + | Some _, None -> incr stats_nb_missed_opportunities + | Some false, Some false -> incr stats_nb_correct_predicts + | Some false, Some true -> incr stats_nb_mispredicts + | Some true, Some false -> incr stats_nb_mispredicts + | Some true, Some true -> incr stats_nb_correct_predicts + end; + (* only update if there is no prior existing branch prediction *) (match pred with | None -> Icond (cond, lr, n, n', direction) - | Some _ -> Icond (cond, lr, n, n', pred) ) + | Some _ -> begin + Icond (cond, lr, n, n', pred) + end + ) + end | i -> i (* Uses branch prediction to write prediction annotations in Icond *) @@ -1026,15 +1090,20 @@ let static_predict f = let entrypoint = f.fn_entrypoint in let code = f.fn_code in let revmap = make_identity_ptree code in - let code = - if !Clflags.option_fpredict then - update_directions f code entrypoint - else code in - let code = - if !Clflags.option_fpredict then - invert_iconds code - else code in - ((code, entrypoint), revmap) + begin + reset_stats (); + set_stats_oc (); + let code = + if !Clflags.option_fpredict then + update_directions f code entrypoint + else code in + write_stats_oc (); + let code = + if !Clflags.option_fpredict then + invert_iconds code + else code in + ((code, entrypoint), revmap) + end let unroll_single f = let entrypoint = f.fn_entrypoint in diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 1f6b8817..b88dbc2d 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -41,24 +41,25 @@ let rtl_successors = function * * If we come accross an edge to a Processed node, it's a loop! *) -let get_loop_headers code entrypoint = begin - debug "get_loop_headers\n"; +let get_loop_backedges code entrypoint = begin + debug "get_loop_backedges\n"; let visited = ref (PTree.map (fun n i -> Unvisited) code) - and is_loop_header = ref (PTree.map (fun n i -> false) code) - in let rec dfs_visit code = function + and loop_backedge = ref (PTree.map (fun n i -> None) code) + in let rec dfs_visit code origin = function | [] -> () | node :: ln -> debug "ENTERING node %d, REM are %a\n" (P.to_int node) print_intlist ln; match (get_some @@ PTree.get node !visited) with | Visited -> begin debug "\tNode %d is already Visited, skipping\n" (P.to_int node); - dfs_visit code ln + dfs_visit code origin ln end | Processed -> begin debug "Node %d is a loop header\n" (P.to_int node); - is_loop_header := PTree.set node true !is_loop_header; + debug "The backedge is from %d\n" (P.to_int @@ get_some origin); + loop_backedge := PTree.set node origin !loop_backedge; visited := PTree.set node Visited !visited; - dfs_visit code ln + dfs_visit code origin ln end | Unvisited -> begin visited := PTree.set node Processed !visited; @@ -67,19 +68,26 @@ let get_loop_headers code entrypoint = begin | None -> failwith "No such node" | Some i -> let next_visits = rtl_successors i in begin debug "About to visit: %a\n" print_intlist next_visits; - dfs_visit code next_visits + dfs_visit code (Some node) next_visits end); debug "Node %d is Visited!\n" (P.to_int node); visited := PTree.set node Visited !visited; - dfs_visit code ln + dfs_visit code origin ln end in begin - dfs_visit code [entrypoint]; - debug "LOOP HEADERS: %a\n" print_ptree_bool !is_loop_header; - !is_loop_header + dfs_visit code None [entrypoint]; + debug "LOOP BACKEDGES: %a\n" print_ptree_opint !loop_backedge; + !loop_backedge end end +let get_loop_headers code entrypoint = + let backedges = get_loop_backedges code entrypoint in + PTree.map (fun _ ob -> + match ob with + | None -> false + | Some _ -> true + ) backedges module Dominator = struct diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 3f1a8b6e..5914f6a3 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -126,400 +126,64 @@ let enumerate_aux_flat f reach = * This is a slight alteration to the above heuristic, ensuring that any * superblock will be contiguous in memory, while still following the original * heuristic + * + * Slight change: instead of taking the minimum pc of the superblock, we just take + * the pc of the first block. + * (experimentally this leads to slightly better performance..) *) -let get_some = function -| None -> failwith "Did not get some" -| Some thing -> thing - -exception EmptyList - -let rec last_element = function - | [] -> raise EmptyList - | e :: [] -> e - | e' :: e :: l -> last_element (e::l) - -let print_plist l = - let rec f = function - | [] -> () - | n :: l -> Printf.printf "%d, " (P.to_int n); f l - in begin - if !debug_flag then begin - Printf.printf "["; - f l; - Printf.printf "]" - end - end - -(* adapted from the above join_points function, but with PTree *) -let get_join_points code entry = - let reached = ref (PTree.map (fun n i -> false) code) in - let reached_twice = ref (PTree.map (fun n i -> false) code) in - let rec traverse pc = - if get_some @@ PTree.get pc !reached then begin - if not (get_some @@ PTree.get pc !reached_twice) then - reached_twice := PTree.set pc true !reached_twice - end else begin - reached := PTree.set pc true !reached; - traverse_succs (successors_block @@ get_some @@ PTree.get pc code) - end - and traverse_succs = function - | [] -> () - | [pc] -> traverse pc - | pc :: l -> traverse pc; traverse_succs l - in traverse entry; !reached_twice - -let forward_sequences code entry = - let visited = ref (PTree.map (fun n i -> false) code) in - let join_points = get_join_points code entry in - (* returns the list of traversed nodes, and a list of nodes to start traversing next *) - let rec traverse_fallthrough code node = - (* debug "Traversing %d..\n" (P.to_int node); *) - if not (get_some @@ PTree.get node !visited) then begin - visited := PTree.set node true !visited; - match PTree.get node code with - | None -> failwith "No such node" - | Some bb -> - let ln, rem = match (last_element bb) with - | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _ - | Lbuiltin _ -> assert false - | Ltailcall _ | Lreturn -> begin (* debug "STOP tailcall/return\n"; *) ([], []) end - | Lbranch n -> - if get_some @@ PTree.get n join_points then ([], [n]) - else let ln, rem = traverse_fallthrough code n in (ln, rem) - | Lcond (_, _, ifso, ifnot, info) -> (match info with - | None -> begin (* debug "STOP Lcond None\n"; *) ([], [ifso; ifnot]) end - | Some false -> - if get_some @@ PTree.get ifnot join_points then ([], [ifso; ifnot]) - else let ln, rem = traverse_fallthrough code ifnot in (ln, [ifso] @ rem) - | Some true -> - if get_some @@ PTree.get ifso join_points then ([], [ifso; ifnot]) - else let ln, rem = traverse_fallthrough code ifso in (ln, [ifnot] @ rem) - ) - | Ljumptable(_, ln) -> begin (* debug "STOP Ljumptable\n"; *) ([], ln) end - in ([node] @ ln, rem) - end - else ([], []) - in let rec f code = function - | [] -> [] - | node :: ln -> - let fs, rem_from_node = traverse_fallthrough code node - in [fs] @ ((f code rem_from_node) @ (f code ln)) - in (f code [entry]) - -(** Unused code -module PInt = struct - type t = P.t - let compare x y = compare (P.to_int x) (P.to_int y) -end - -module PSet = Set.Make(PInt) - -module LPInt = struct - type t = P.t list - let rec compare x y = - match x with - | [] -> ( match y with - | [] -> 0 - | _ -> 1 ) - | e :: l -> match y with - | [] -> -1 - | e' :: l' -> - let e_cmp = PInt.compare e e' in - if e_cmp == 0 then compare l l' else e_cmp -end - -module LPSet = Set.Make(LPInt) - -let iter_lpset f s = Seq.iter f (LPSet.to_seq s) - -let first_of = function - | [] -> None - | e :: l -> Some e - -let rec last_of = function - | [] -> None - | e :: l -> (match l with [] -> Some e | e :: l -> last_of l) - -let can_be_merged code s s' = - let last_s = get_some @@ last_of s in - let first_s' = get_some @@ first_of s' in - match get_some @@ PTree.get last_s code with - | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _ - | Lbuiltin _ | Ltailcall _ | Lreturn -> false - | Lbranch n -> n == first_s' - | Lcond (_, _, ifso, ifnot, info) -> (match info with - | None -> false - | Some false -> ifnot == first_s' - | Some true -> failwith "Inconsistency detected - ifnot is not the preferred branch") - | Ljumptable (_, ln) -> - match ln with - | [] -> false - | n :: ln -> n == first_s' - -let merge s s' = Some s - -let try_merge code (fs: (BinNums.positive list) list) = - let seqs = ref (LPSet.of_list fs) in - let oldLength = ref (LPSet.cardinal !seqs) in - let continue = ref true in - let found = ref false in - while !continue do - begin - found := false; - iter_lpset (fun s -> - if !found then () - else iter_lpset (fun s' -> - if (!found || s == s') then () - else if (can_be_merged code s s') then - begin - seqs := LPSet.remove s !seqs; - seqs := LPSet.remove s' !seqs; - seqs := LPSet.add (get_some (merge s s')) !seqs; - found := true; - end - else () - ) !seqs - ) !seqs; - if !oldLength == LPSet.cardinal !seqs then - continue := false - else - oldLength := LPSet.cardinal !seqs - end - done; - !seqs -*) - -(** Code adapted from Duplicateaux.get_loop_headers - * - * Getting loop branches with a DFS visit : - * Each node is either Unvisited, Visited, or Processed - * pre-order: node becomes Processed - * post-order: node becomes Visited - * - * If we come accross an edge to a Processed node, it's a loop! - *) -type pos = BinNums.positive - -module PP = struct - type t = pos * pos - let compare a b = - let ax, ay = a in - let bx, by = b in - let dx = compare ax bx in - if (dx == 0) then compare ay by - else dx -end - -module PPMap = Map.Make(PP) - -type vstate = Unvisited | Processed | Visited - -let get_loop_edges code entry = - let visited = ref (PTree.map (fun n i -> Unvisited) code) in - let is_loop_edge = ref PPMap.empty - in let rec dfs_visit code from = function - | [] -> () - | node :: ln -> - match (get_some @@ PTree.get node !visited) with - | Visited -> () - | Processed -> begin - let from_node = get_some from in - is_loop_edge := PPMap.add (from_node, node) true !is_loop_edge; - visited := PTree.set node Visited !visited - end - | Unvisited -> begin - visited := PTree.set node Processed !visited; - let bb = get_some @@ PTree.get node code in - let next_visits = (match (last_element bb) with - | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _ - | Lbuiltin _ -> assert false - | Ltailcall _ | Lreturn -> [] - | Lbranch n -> [n] - | Lcond (_, _, ifso, ifnot, _) -> [ifso; ifnot] - | Ljumptable(_, ln) -> ln - ) in dfs_visit code (Some node) next_visits; - visited := PTree.set node Visited !visited; - dfs_visit code from ln - end - in begin - dfs_visit code None [entry]; - !is_loop_edge - end - -let ppmap_is_true pp ppmap = PPMap.mem pp ppmap && PPMap.find pp ppmap - -module Int = struct - type t = int - let compare x y = compare x y -end - -module ISet = Set.Make(Int) - -let print_iset s = begin - if !debug_flag then begin - Printf.printf "{"; - ISet.iter (fun e -> Printf.printf "%d, " e) s; - Printf.printf "}" - end -end - -let print_depmap dm = begin - if !debug_flag then begin - Printf.printf "[|"; - Array.iter (fun s -> print_iset s; Printf.printf ", ") dm; - Printf.printf "|]\n" - end -end - -let construct_depmap code entry fs = - let is_loop_edge = get_loop_edges code entry in - let visited = ref (PTree.map (fun n i -> false) code) in - let depmap = Array.map (fun e -> ISet.empty) fs in - let find_index_of_node n = - let index = ref 0 in - begin - Array.iteri (fun i s -> - match List.find_opt (fun e -> e == n) s with - | Some _ -> index := i - | None -> () - ) fs; - !index - end - in let check_and_update_depmap from target = - (* debug "From %d to %d\n" (P.to_int from) (P.to_int target); *) - if not (ppmap_is_true (from, target) is_loop_edge) then - let in_index_fs = find_index_of_node from in - let out_index_fs = find_index_of_node target in - if out_index_fs != in_index_fs then - depmap.(out_index_fs) <- ISet.add in_index_fs depmap.(out_index_fs) - else () - else () - in let rec dfs_visit code = function - | [] -> () - | node :: ln -> - begin - match (get_some @@ PTree.get node !visited) with - | true -> () - | false -> begin - visited := PTree.set node true !visited; - let bb = get_some @@ PTree.get node code in - let next_visits = - match (last_element bb) with - | Ltailcall _ | Lreturn -> [] - | Lbranch n -> (check_and_update_depmap node n; [n]) - | Lcond (_, _, ifso, ifnot, _) -> begin - check_and_update_depmap node ifso; - check_and_update_depmap node ifnot; - [ifso; ifnot] - end - | Ljumptable(_, ln) -> begin - List.iter (fun n -> check_and_update_depmap node n) ln; - ln - end - (* end of bblocks should not be another value than one of the above *) - | _ -> failwith "last_element gave an invalid output" - in dfs_visit code next_visits - end; - dfs_visit code ln - end - in begin - dfs_visit code [entry]; - depmap - end - -let print_sequence s = - if !debug_flag then begin - Printf.printf "["; - List.iter (fun n -> Printf.printf "%d, " (P.to_int n)) s; - Printf.printf "]\n" - end - -let print_ssequence ofs = - if !debug_flag then begin - Printf.printf "["; - List.iter (fun s -> print_sequence s) ofs; - Printf.printf "]\n" - end - -let order_sequences code entry fs = - let fs_a = Array.of_list fs in - let depmap = construct_depmap code entry fs_a in - let fs_evaluated = Array.map (fun e -> false) fs_a in - let ordered_fs = ref [] in - let evaluate s_id = - begin - assert (not fs_evaluated.(s_id)); - ordered_fs := fs_a.(s_id) :: !ordered_fs; - fs_evaluated.(s_id) <- true; - (* debug "++++++\n"; - debug "Scheduling %d\n" s_id; - debug "Initial depmap: "; print_depmap depmap; *) - Array.iteri (fun i deps -> - depmap.(i) <- ISet.remove s_id deps - ) depmap; - (* debug "Final depmap: "; print_depmap depmap; *) +let super_blocks f joins = + let blocks = ref [] in + let visited = ref IntSet.empty in + (* start_block: + pc is the function entry point + or a join point + or the successor of a conditional test *) + let rec start_block pc = + let npc = P.to_int pc in + if not (IntSet.mem npc !visited) then begin + visited := IntSet.add npc !visited; + in_block [] npc pc end - in let choose_best_of candidates = - let current_best_id = ref None in - let current_best_score = ref None in - begin - List.iter (fun id -> - match !current_best_id with - | None -> begin - current_best_id := Some id; - match fs_a.(id) with - | [] -> current_best_score := None - | n::l -> current_best_score := Some (P.to_int n) - end - | Some b -> begin - match fs_a.(id) with - | [] -> () - | n::l -> let nscore = P.to_int n in - match !current_best_score with - | None -> (current_best_id := Some id; current_best_score := Some nscore) - | Some bs -> if nscore > bs then (current_best_id := Some id; current_best_score := Some nscore) + (* in_block: add pc to block and check successors *) + and in_block blk minpc pc = + let blk = pc :: blk in + match PTree.get pc f.fn_code with + | None -> assert false + | Some b -> + let rec do_instr_list = function + | [] -> assert false + | Lbranch s :: _ -> next_in_block blk minpc s + | Ltailcall (sig0, ros) :: _ -> end_block blk minpc + | Lcond (cond, args, ifso, ifnot, pred) :: _ -> begin + match pred with + | None -> (end_block blk minpc; start_block ifso; start_block ifnot) + | Some true -> (next_in_block blk minpc ifso; start_block ifnot) + | Some false -> (next_in_block blk minpc ifnot; start_block ifso) end - ) candidates; - !current_best_id - end - in let select_next () = - let candidates = ref [] in - begin - Array.iteri (fun i deps -> - begin - (* debug "Deps of %d: " i; print_iset deps; debug "\n"; *) - (* FIXME - if we keep it that way (no dependency check), remove all the unneeded stuff *) - if ((* deps == ISet.empty && *) not fs_evaluated.(i)) then - candidates := i :: !candidates - end - ) depmap; - if not (List.length !candidates > 0) then begin - Array.iteri (fun i deps -> - if (not fs_evaluated.(i)) then candidates := i :: !candidates - ) depmap; - end; - get_some (choose_best_of !candidates) - end - in begin - debug "-------------------------------\n"; - debug "depmap: "; print_depmap depmap; - debug "forward sequences identified: "; print_ssequence fs; - while List.length !ordered_fs != List.length fs do - let next_id = select_next () in - evaluate next_id - done; - debug "forward sequences ordered: "; print_ssequence (List.rev (!ordered_fs)); - List.rev (!ordered_fs) - end + | Ljumptable(arg, tbl) :: _ -> + end_block blk minpc; List.iter start_block tbl + | Lreturn :: _ -> end_block blk minpc + | instr :: b' -> do_instr_list b' in + do_instr_list b + (* next_in_block: check if join point and either extend block + or start block *) + and next_in_block blk minpc pc = + let npc = P.to_int pc in + if IntSet.mem npc joins + then (end_block blk minpc; start_block pc) + else in_block blk minpc pc + (* end_block: record block that we just discovered *) + and end_block blk minpc = + blocks := (minpc, List.rev blk) :: !blocks + in + start_block f.fn_entrypoint; !blocks + +(* Build the enumeration *) -let enumerate_aux_trace f reach = - let code = f.fn_code in - let entry = f.fn_entrypoint in - let fs = forward_sequences code entry in - let ofs = order_sequences code entry fs in - List.flatten ofs +let enumerate_aux_sb f reach = + flatten_blocks (super_blocks f (join_points f)) let enumerate_aux f reach = - if !Clflags.option_ftracelinearize then enumerate_aux_trace f reach + if !Clflags.option_ftracelinearize then enumerate_aux_sb f reach else enumerate_aux_flat f reach diff --git a/common/DebugPrint.ml b/common/DebugPrint.ml index 5078f727..6f8449ee 100644 --- a/common/DebugPrint.ml +++ b/common/DebugPrint.ml @@ -20,6 +20,20 @@ let print_ptree_bool oc pt = end else () +let print_ptree_opint oc pt = + if !debug_flag then + let elements = PTree.elements pt in + begin + Printf.fprintf oc "["; + List.iter (fun (n, op) -> + match op with + | None -> () + | Some p -> Printf.fprintf oc "%d -> %d, " (P.to_int n) (P.to_int p) + ) elements; + Printf.fprintf oc "]\n" + end + else () + let print_intlist oc l = let rec f oc = function | [] -> () @@ -30,6 +44,20 @@ let print_intlist oc l = end end +let print_ptree_oplist oc pt = + if !debug_flag then + let elements = PTree.elements pt in + begin + Printf.fprintf oc "["; + List.iter (fun (n, ol) -> + match ol with + | None -> () + | Some l -> Printf.fprintf oc "%d -> %a,\n" (P.to_int n) print_intlist l + ) elements; + Printf.fprintf oc "]\n" + end + else () + (* Adapted from backend/PrintRTL.ml: print_function *) let print_code code = let open PrintRTL in let open Printf in if (!debug_flag) then begin @@ -710,6 +710,7 @@ HAS_STANDARD_HEADERS=$has_standard_headers INSTALL_COQDEV=$install_coqdev LIBMATH=$libmath MODEL=$model +OS=${os:-unspecified} SYSTEM=$system RESPONSEFILE=$responsefile LIBRARY_FLOCQ=$library_Flocq diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 73b71ea0..4f5a93d2 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -242,7 +242,7 @@ let rv64 = struct_passing_style = SP_ref_callee; (* Wrong *) struct_return_style = SR_ref } (* to check *) -let kvx = +let kvxbase = { name = "kvx"; char_signed = true; wchar_signed = true; @@ -275,7 +275,15 @@ let kvx = supports_unaligned_accesses = true; struct_passing_style = SP_value32_ref_callee; struct_return_style = SR_int1to4; - has_non_trapping_loads = true; + has_non_trapping_loads = false; +} + +let kvxcos = + { kvxbase with has_non_trapping_loads = false; +} + +let kvxmbr = + { kvxbase with has_non_trapping_loads = true; } let aarch64 = diff --git a/cparser/Machine.mli b/cparser/Machine.mli index 54436758..07b55832 100644 --- a/cparser/Machine.mli +++ b/cparser/Machine.mli @@ -88,7 +88,8 @@ val arm_littleendian : t val arm_bigendian : t val rv32 : t val rv64 : t -val kvx : t +val kvxmbr : t +val kvxcos : t val aarch64 : t val gcc_extensions : t -> t diff --git a/doc/index-kvx.html b/doc/index-kvx.html index 6d56cbdb..62afb423 100644 --- a/doc/index-kvx.html +++ b/doc/index-kvx.html @@ -278,7 +278,7 @@ This IR is generic over the processor, even if currently, only used for KVX. </TD> <TD>RTL to RTL</TD> <TD><A HREF="html/compcert.backend.Duplicate.html">Duplicate</A> (generic checker)</TD> - <TD><A HREF="html/compcert.scheduling.Duplicateproof.html">Duplicateproof</A> (generic proof)<BR> + <TD><A HREF="html/compcert.backend.Duplicateproof.html">Duplicateproof</A> (generic proof)<BR> <a href="html/compcert.backend.Duplicatepasses.html">Duplicatepasses</a> (several passes from several oracles)</TD> </TR> <TR valign="top" style="color:#000000"> diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 1d40214a..ecc2aba6 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -126,6 +126,7 @@ let arch = | "powerpc"|"arm"|"x86"|"riscV"|"kvx"|"aarch64" as a -> a | v -> bad_config "arch" [v] let model = get_config_string "model" +let os = get_config_string "os" let abi = get_config_string "abi" let is_big_endian = match get_config_string "endianness" with diff --git a/driver/Configuration.mli b/driver/Configuration.mli index a71da72d..75e547ff 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -19,6 +19,9 @@ val model: string val abi: string (** ABI to use *) +val os: string + (** ABI to use *) + val is_big_endian: bool (** Endianness to use *) diff --git a/driver/Frontend.ml b/driver/Frontend.ml index c99da945..c8890046 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -117,7 +117,10 @@ let init () = | "riscV" -> if Configuration.model = "64" then Machine.rv64 else Machine.rv32 - | "kvx" -> Machine.kvx + | "kvx" -> if Configuration.os = "cos" then Machine.kvxcos + else if Configuration.os = "mbr" then Machine.kvxmbr + else (Printf.eprintf "Configuration OS = %s\n" Configuration.os; + failwith "Wrong OS configuration for KVX") | "aarch64" -> Machine.aarch64 | _ -> assert false end; diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml index 9b93bc32..2a20a15d 100644 --- a/scheduling/RTLpathLivegenaux.ml +++ b/scheduling/RTLpathLivegenaux.ml @@ -82,13 +82,15 @@ let get_path_map code entry join_points = let visited = ref (PTree.map (fun n i -> false) code) in let path_map = ref PTree.empty in let rec dig_path e = - let psize = ref (-1) in - let path_successors = ref [] in - let rec dig_path_rec n : (path_info * node list) option = - if not (get_some @@ PTree.get n !visited) then + if (get_some @@ PTree.get e !visited) then + () + else begin + visited := PTree.set e true !visited; + let psize = ref (-1) in + let path_successors = ref [] in + let rec dig_path_rec n : (path_info * node list) option = let inst = get_some @@ PTree.get n code in begin - visited := PTree.set n true !visited; psize := !psize + 1; let successor = match predicted_successor inst with | None -> None @@ -102,15 +104,15 @@ let get_path_map code entry join_points = input_regs = Regset.empty; pre_output_regs = Regset.empty; output_regs = Regset.empty }, !path_successors @ successors_inst inst) end - else None - in match dig_path_rec e with - | None -> () - | Some ret -> - let (path_info, succs) = ret in - begin - path_map := PTree.set e path_info !path_map; - List.iter dig_path succs - end + in match dig_path_rec e with + | None -> () + | Some ret -> + let (path_info, succs) = ret in + begin + path_map := PTree.set e path_info !path_map; + List.iter dig_path succs + end + end in begin dig_path entry; !path_map diff --git a/test/monniaux/profiling/compcert_profiling.dat b/test/monniaux/profiling/compcert_profiling.dat Binary files differnew file mode 100644 index 00000000..fa57a995 --- /dev/null +++ b/test/monniaux/profiling/compcert_profiling.dat diff --git a/test/monniaux/profiling/test_profiling b/test/monniaux/profiling/test_profiling Binary files differnew file mode 100755 index 00000000..b530aae2 --- /dev/null +++ b/test/monniaux/profiling/test_profiling diff --git a/test/monniaux/profiling/test_profiling.c b/test/monniaux/profiling/test_profiling.c new file mode 100644 index 00000000..013b1d68 --- /dev/null +++ b/test/monniaux/profiling/test_profiling.c @@ -0,0 +1,15 @@ +#include <stdlib.h> +#include <stdio.h> + +int main(int argc, char **argv) { + if (argc < 2) return 1; + int i = atoi(argv[1]); + if (i > 0) { + printf("positive\n"); + } else if (i==0) { + printf("zero\n"); + } else { + printf("negative\n"); + } + return 0; +} |