Commit 2d086fdf authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

Merge branch 'kvx-work' into aarch64-peephole

parents 10da6dfa 13b0e8f1
......@@ -58,7 +58,8 @@ Definition transf_instr (fmap : PMap.t RB.t)
match instr with
| Iop op args dst s =>
let args' := subst_args fmap pc args in
match (if is_trivial_op op then None else find_op_in_fmap fmap pc op args') with
match (if (negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op)
then None else find_op_in_fmap fmap pc op args') with
| None => Iop op args' dst s
| Some src => Iop Omove (src::nil) dst s
end
......
......@@ -463,12 +463,12 @@ Proof.
destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SOp op)
(subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
* destruct (if is_trivial_op op
* destruct (if (negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op)
then None
else
rhs_find pc (SOp op)
(subst_args (fst (preanalysis tenv f)) pc args) t) eqn:FIND.
** destruct (is_trivial_op op). discriminate.
** destruct ((negb (Compopts.optim_CSE3_trivial_ops tt)) && (is_trivial_op op)). discriminate.
apply exec_Iop with (op := Omove) (args := r :: nil).
TR_AT.
subst instr'.
......
......@@ -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 :=
......
......@@ -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
......
......@@ -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:
......
......@@ -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
......
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
......@@ -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. *)
......
......@@ -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 *)
......
......@@ -253,6 +253,23 @@ This IR is generic over the processor, even if currently, only used for KVX.
<TD><A HREF="html/compcert.backend.Unusedglobproof.html">Unusedglobproof</A></TD>
</TR>
<TR valign="top" style="color:#000000">
<TD colspan="4"><b>Passes introduced for profiling (for later use in trace selection)</b></TD>
</TR>
<TR valign="top" style="color:#000000">
<TD>Insert profiling annotations (for recording experiments -- see PROFILE.md).
</TD>
<TD>RTL to RTL</TD>
<TD><A HREF="html/compcert.backend.Profiling.html">Profiling</A></TD>
<TD><A HREF="html/compcert.backend.Profilingproof.html">Profilingproof</A></TD>
</TR>
<TR valign="top" style="color:#000000">
<TD>Update ICond nodes (from recorded experiments -- see PROFILE.md).
</TD>
<TD>RTL to RTL</TD>
<TD><A HREF="html/compcert.backend.ProfilingExploit.html">ProfilingExploit</A></TD>
<TD><A HREF="html/compcert.backend.ProfilingExploitproof.html">ProfilingExploitproof</A></TD>
</TR>
<TR valign="top" style="color:#000000">
<TD colspan="4"><b>Passes introduced for superblock prepass scheduling</b></TD>
</TR>
......@@ -372,12 +389,13 @@ This IR is generic over the processor, even if currently, only used for KVX.
</TR>
</TABLE>
<font color=gray>
<H3>All together</H3>
<H3>All together (there are many more RTL passes than on vanilla CompCert: their order is specified in Compiler)</H3>
<UL>
</font>
<LI> <A HREF="html/compcert.driver.Compiler.html">Compiler</A>: composing the passes together;
whole-compiler semantic preservation theorems.
<font color=gray>
<LI> <A HREF="html/compcert.driver.Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
</UL>
......
......@@ -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
......@@ -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 =