Commit 13b0e8f1 authored by David Monniaux's avatar David Monniaux
Browse files

Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work

parents 749fa737 0a6082e1
...@@ -203,8 +203,7 @@ Fixpoint verify_mapping_mn_rec dupmap f f' lm := ...@@ -203,8 +203,7 @@ Fixpoint verify_mapping_mn_rec dupmap f f' lm :=
match lm with match lm with
| nil => OK tt | nil => OK tt
| m :: lm => do u <- verify_mapping_mn dupmap f f' m; | m :: lm => do u <- verify_mapping_mn dupmap f f' m;
do u2 <- verify_mapping_mn_rec dupmap f f' lm; verify_mapping_mn_rec dupmap f f' lm
OK tt
end. end.
Definition verify_mapping_match_nodes dupmap (f f': function): res unit := Definition verify_mapping_match_nodes dupmap (f f': function): res unit :=
......
...@@ -22,9 +22,8 @@ ...@@ -22,9 +22,8 @@
open RTL open RTL
open Maps open Maps
open Camlcoq open Camlcoq
open DebugPrint
let debug_flag = LICMaux.debug_flag
let debug = LICMaux.debug
let get_loop_headers = LICMaux.get_loop_headers let get_loop_headers = LICMaux.get_loop_headers
let get_some = LICMaux.get_some let get_some = LICMaux.get_some
let rtl_successors = LICMaux.rtl_successors let rtl_successors = LICMaux.rtl_successors
...@@ -87,8 +86,6 @@ end ...@@ -87,8 +86,6 @@ end
module PSet = Set.Make(PInt) module PSet = Set.Make(PInt)
let print_intlist = LICMaux.print_intlist
let print_intset s = let print_intset s =
let seq = PSet.to_seq s let seq = PSet.to_seq s
in begin in begin
...@@ -101,18 +98,6 @@ let print_intset s = ...@@ -101,18 +98,6 @@ let print_intset s =
end end
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 (* Looks ahead (until a branch) to see if a node further down verifies
* the given predicate *) * the given predicate *)
let rec look_ahead_gen (successors: RTL.instruction -> P.t list) code node is_loop_header predicate = let rec look_ahead_gen (successors: RTL.instruction -> P.t list) code node is_loop_header predicate =
...@@ -215,16 +200,6 @@ type innerLoop = { ...@@ -215,16 +200,6 @@ type innerLoop = {
let print_pset = LICMaux.pp_pset 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 let rtl_successors_pref = function
| Itailcall _ | Ireturn _ -> [] | Itailcall _ | Ireturn _ -> []
| Icall(_,_,_,_,n) | Ibuiltin(_,_,_,n) | Inop n | Iop (_,_,_,n) | Icall(_,_,_,_,n) | Ibuiltin(_,_,_,n) | Inop n | Iop (_,_,_,n)
...@@ -458,21 +433,21 @@ let update_direction direction = function ...@@ -458,21 +433,21 @@ let update_direction direction = function
| Some _ -> Icond (cond, lr, n, n', pred) ) | Some _ -> Icond (cond, lr, n, n', pred) )
| i -> i | 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 *) (* Uses branch prediction to write prediction annotations in Icond *)
let update_directions f code entrypoint = begin let update_directions f code entrypoint = begin
debug "Update_directions\n"; debug "Update_directions\n";
let directions = get_directions f code entrypoint let directions = get_directions f code entrypoint in
in begin let code' = ref code in
begin
debug "Get Directions done, now proceeding to update all direction information..\n";
(* debug "Ifso directions: "; (* debug "Ifso directions: ";
ptree_printbool directions; ptree_printbool directions;
debug "\n"; *) 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
end end
...@@ -554,8 +529,6 @@ let print_traces oc traces = ...@@ -554,8 +529,6 @@ let print_traces oc traces =
Printf.fprintf oc "Traces: {%a}\n" f traces Printf.fprintf oc "Traces: {%a}\n" f traces
end end
let print_code code = LICMaux.print_code code
(* Dumb (but linear) trace selection *) (* Dumb (but linear) trace selection *)
let select_traces_linear code entrypoint = let select_traces_linear code entrypoint =
let is_visited = ref (PTree.map (fun n i -> false) code) in let is_visited = ref (PTree.map (fun n i -> false) code) in
...@@ -770,14 +743,6 @@ let invert_iconds code = ...@@ -770,14 +743,6 @@ let invert_iconds code =
* cyclic dependencies between LICMaux and Duplicateaux * 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 = let print_inner_loop iloop =
debug "{preds: %a, body: %a, head: %d, finals: %a, sb_final: %a}\n" debug "{preds: %a, body: %a, head: %d, finals: %a, sb_final: %a}\n"
print_intlist iloop.preds print_intlist iloop.preds
...@@ -794,8 +759,6 @@ let rec print_inner_loops = function ...@@ -794,8 +759,6 @@ let rec print_inner_loops = function
print_inner_loops iloops print_inner_loops iloops
end end
let print_pint oc i = if !debug_flag then Printf.fprintf oc "%d" (P.to_int i) else ()
let cb_exit_node = function let cb_exit_node = function
| Icond (_,_,n1,n2,p) -> begin match p with | Icond (_,_,n1,n2,p) -> begin match p with
| Some true -> Some n2 | Some true -> Some n2
......
...@@ -111,7 +111,7 @@ Proof. ...@@ -111,7 +111,7 @@ Proof.
- monadInv H0. inversion H. - monadInv H0. inversion H.
- inversion H. - inversion H.
+ subst. monadInv H0. destruct x. assumption. + subst. monadInv H0. destruct x. assumption.
+ monadInv H0. destruct x0. eapply IHlb; assumption. + monadInv H0. destruct x. eapply IHlb; assumption.
Qed. Qed.
Lemma verify_is_copy_correct: Lemma verify_is_copy_correct:
......
...@@ -16,16 +16,11 @@ open Maps;; ...@@ -16,16 +16,11 @@ open Maps;;
open Kildall;; open Kildall;;
open HashedSet;; open HashedSet;;
open Inject;; open Inject;;
open DebugPrint;;
type reg = P.t;; type reg = P.t;;
(** get_loop_headers moved from Duplicateaux.ml to LICMaux.ml to prevent cycle dependencies *) (** 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 type vstate = Unvisited | Processed | Visited
let get_some = function let get_some = function
...@@ -39,42 +34,6 @@ let rtl_successors = function ...@@ -39,42 +34,6 @@ let rtl_successors = function
| Icond (_,_,n1,n2,_) -> [n1; n2] | Icond (_,_,n1,n2,_) -> [n1; n2]
| Ijumptable (_,ln) -> ln | 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 : (** Getting loop branches with a DFS visit :
* Each node is either Unvisited, Visited, or Processed * Each node is either Unvisited, Visited, or Processed
* pre-order: node becomes 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 = { ...@@ -61,6 +61,7 @@ type t = {
supports_unaligned_accesses: bool; supports_unaligned_accesses: bool;
struct_passing_style: struct_passing_style; struct_passing_style: struct_passing_style;
struct_return_style : struct_return_style; struct_return_style : struct_return_style;
has_non_trapping_loads : bool;
} }
let ilp32ll64 = { let ilp32ll64 = {
...@@ -96,6 +97,7 @@ let ilp32ll64 = { ...@@ -96,6 +97,7 @@ let ilp32ll64 = {
supports_unaligned_accesses = false; supports_unaligned_accesses = false;
struct_passing_style = SP_ref_callee; struct_passing_style = SP_ref_callee;
struct_return_style = SR_ref; struct_return_style = SR_ref;
has_non_trapping_loads = false;
} }
let i32lpll64 = { let i32lpll64 = {
...@@ -131,6 +133,7 @@ let i32lpll64 = { ...@@ -131,6 +133,7 @@ let i32lpll64 = {
supports_unaligned_accesses = false; supports_unaligned_accesses = false;
struct_passing_style = SP_ref_callee; struct_passing_style = SP_ref_callee;
struct_return_style = SR_ref; struct_return_style = SR_ref;
has_non_trapping_loads = false;
} }
let il32pll64 = { let il32pll64 = {
...@@ -166,6 +169,7 @@ let il32pll64 = { ...@@ -166,6 +169,7 @@ let il32pll64 = {
supports_unaligned_accesses = false; supports_unaligned_accesses = false;
struct_passing_style = SP_ref_callee; struct_passing_style = SP_ref_callee;
struct_return_style = SR_ref; struct_return_style = SR_ref;
has_non_trapping_loads = false;
} }
(* Canned configurations for some ABIs *) (* Canned configurations for some ABIs *)
...@@ -270,7 +274,9 @@ let kvx = ...@@ -270,7 +274,9 @@ let kvx =
bitfields_msb_first = false; (* TO CHECK *) bitfields_msb_first = false; (* TO CHECK *)
supports_unaligned_accesses = true; supports_unaligned_accesses = true;
struct_passing_style = SP_value32_ref_callee; struct_passing_style = SP_value32_ref_callee;
struct_return_style = SR_int1to4 } struct_return_style = SR_int1to4;
has_non_trapping_loads = true;
}
let aarch64 = let aarch64 =
{ i32lpll64 with name = "aarch64"; { i32lpll64 with name = "aarch64";
...@@ -323,6 +329,7 @@ let undef = { ...@@ -323,6 +329,7 @@ let undef = {
supports_unaligned_accesses = false; supports_unaligned_accesses = false;
struct_passing_style = SP_ref_callee; struct_passing_style = SP_ref_callee;
struct_return_style = SR_ref; struct_return_style = SR_ref;
has_non_trapping_loads = false;
} }
(* The current configuration. Must be initialized before use. *) (* The current configuration. Must be initialized before use. *)
......
...@@ -60,6 +60,7 @@ type t = { ...@@ -60,6 +60,7 @@ type t = {
supports_unaligned_accesses: bool; supports_unaligned_accesses: bool;
struct_passing_style: struct_passing_style; struct_passing_style: struct_passing_style;
struct_return_style: struct_return_style; struct_return_style: struct_return_style;
has_non_trapping_loads: bool;
} }
(* The current configuration *) (* The current configuration *)
......
...@@ -6,13 +6,7 @@ open Camlcoq ...@@ -6,13 +6,7 @@ open Camlcoq
open Datatypes open Datatypes
open Kildall open Kildall
open Lattice open Lattice
open DebugPrint
let debug_flag = ref false
let dprintf fmt = let open Printf in
match !debug_flag with
| true -> printf fmt
| false -> ifprintf stdout fmt
let get_some = function let get_some = function
| None -> failwith "Got None instead of Some _" | None -> failwith "Got None instead of Some _"
...@@ -122,22 +116,6 @@ let get_path_map code entry join_points = ...@@ -122,22 +116,6 @@ let get_path_map code entry join_points =
!path_map !path_map
end 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 let transfer f pc after = let open Liveness in
match PTree.get pc f.fn_code with match PTree.get pc f.fn_code with
| Some i -> | Some i ->
...@@ -257,7 +235,7 @@ let set_pathmap_liveness f pm = ...@@ -257,7 +235,7 @@ let set_pathmap_liveness f pm =
let new_pm = ref PTree.empty in let new_pm = ref PTree.empty in
let code = f.fn_code in let code = f.fn_code in
begin begin
dprintf "Liveness: "; print_ptree_regset liveness; dprintf "\n"; debug "Liveness: "; print_ptree_regset liveness; debug "\n";
List.iter (fun (n, pi) -> List.iter (fun (n, pi) ->
let inputs = get_some @@ PTree.get n liveness in let inputs = get_some @@ PTree.get n liveness in
let outputs = get_outputs liveness code n pi in let outputs = get_outputs liveness code n pi in
...@@ -267,31 +245,23 @@ let set_pathmap_liveness f pm = ...@@ -267,31 +245,23 @@ let set_pathmap_liveness f pm =
!new_pm !new_pm
end 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 let print_path_info pi = begin
dprintf "(psize=%d; " (Camlcoq.Nat.to_int pi.psize); debug "(psize=%d; " (Camlcoq.Nat.to_int pi.psize);
dprintf "input_regs="; debug "input_regs=";
print_regset pi.input_regs; print_regset pi.input_regs;
dprintf "; output_regs="; debug "; output_regs=";
print_regset pi.output_regs; print_regset pi.output_regs;
dprintf ")" debug ")"
end end
let print_path_map path_map = begin let print_path_map path_map = begin
dprintf "["; debug "[";
List.iter (fun (n,pi) -> List.iter (fun (n,pi) ->
dprintf "\n\t"; debug "\n\t";
dprintf "%d: " (P.to_int n); debug "%d: " (P.to_int n);
print_path_info pi print_path_info pi
) (PTree.elements path_map); ) (PTree.elements path_map);
dprintf "]" debug "]"
end end
let build_path_map f = let build_path_map f =
...@@ -300,10 +270,10 @@ let build_path_map f = ...@@ -300,10 +270,10 @@ let build_path_map f =
let join_points = get_join_points code entry in let join_points = get_join_points code entry in
let path_map = set_pathmap_liveness f @@ get_path_map code entry join_points in let path_map = set_pathmap_liveness f @@ get_path_map code entry join_points in
begin begin
dprintf "Join points: "; debug "Join points: ";
print_true_nodes join_points; print_true_nodes join_points;
dprintf "\nPath map: "; debug "\nPath map: ";
print_path_map path_map; print_path_map path_map;
dprintf "\n"; debug "\n";
path_map path_map
end end
...@@ -4,6 +4,10 @@ open Maps ...@@ -4,6 +4,10 @@ open Maps
open RTLpathLivegenaux open RTLpathLivegenaux
open Registers open Registers
open Camlcoq open Camlcoq
open Machine
open DebugPrint
let config = Machine.config
type superblock = { type superblock = {
instructions: P.t array; (* pointers to code instructions *) instructions: P.t array; (* pointers to code instructions *)
...@@ -15,54 +19,26 @@ type superblock = {