aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-02-15 18:24:14 +0000
committerYann Herklotz <git@yannherklotz.com>2021-02-15 18:24:14 +0000
commitd3bf6d2115eb4c5ac59ff9be554cc7e086c612f8 (patch)
treeb7e0843bc45444b7d15b14c3a090fc6b53238cd3
parent12298c0d621ddf090d5e7e980266c44248ae7014 (diff)
downloadvericert-kvx-d3bf6d2115eb4c5ac59ff9be554cc7e086c612f8.tar.gz
vericert-kvx-d3bf6d2115eb4c5ac59ff9be554cc7e086c612f8.zip
Add data and control dependencies to reworked graph
-rw-r--r--src/hls/Schedule.ml279
1 files changed, 236 insertions, 43 deletions
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 47d5989..5c83e7f 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -35,8 +35,22 @@ open HTLMonadExtra
module SS = Set.Make(P)
+type svtype =
+ | BBType of int
+ | VarType of int * int
+
+type sv = {
+ sv_type: svtype;
+ sv_num: int;
+}
+
+let print_sv v =
+ match v with
+ | { sv_type = BBType bbi; sv_num = n } -> sprintf "bb%dn%d" bbi n
+ | { sv_type = VarType (bbi, i); sv_num = n } -> sprintf "var%dn%d_%d" bbi i n
+
module G = Graph.Persistent.Digraph.ConcreteLabeled(struct
- type t = int * int
+ type t = sv
let compare = compare
let equal = (=)
let hash = Hashtbl.hash
@@ -48,8 +62,20 @@ end)(struct
let default = 0
end)
+module GDot = Graph.Graphviz.Dot(struct
+ let graph_attributes _ = []
+ let default_vertex_attributes _ = []
+ let vertex_name = print_sv
+ let vertex_attributes _ = []
+ let get_subgraph _ = None
+ let default_edge_attributes _ = []
+ let edge_attributes _ = []
+
+ include G
+ end)
+
module DFG = Graph.Persistent.Digraph.ConcreteLabeled(struct
- type t = int
+ type t = int * instr
let compare = compare
let equal = (=)
let hash = Hashtbl.hash
@@ -61,10 +87,114 @@ end)(struct
let default = 0
end)
+let reg r = sprintf "r%d" (P.to_int r)
+let print_pred r = sprintf "p%d" (Nat.to_int r)
+
+let print_instr = function
+ | RBnop -> ""
+ | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r)
+ | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r)
+ | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p)
+ | RBop (_, op, args, d) ->
+ (match op, args with
+ | Omove, _ -> "mov"
+ | Ointconst n, _ -> sprintf "%s=%ld" (reg d) (camlint_of_coqint n)
+ | Olongconst n, _ -> sprintf "%s=%LdL" (reg d) (camlint64_of_coqint n)
+ | Ofloatconst n, _ -> sprintf "%s=%.15F" (reg d) (camlfloat_of_coqfloat n)
+ | Osingleconst n, _ -> sprintf "%s=%.15Ff" (reg d) (camlfloat_of_coqfloat32 n)
+ | Oindirectsymbol id, _ -> sprintf "%s=&%s" (reg d) (extern_atom id)
+ | Ocast8signed, [r1] -> sprintf "%s=int8signed(%s)" (reg d) (reg r1)
+ | Ocast8unsigned, [r1] -> sprintf "%s=int8unsigned(%s)" (reg d) (reg r1)
+ | Ocast16signed, [r1] -> sprintf "%s=int16signed(%s)" (reg d) (reg r1)
+ | Ocast16unsigned, [r1] -> sprintf "%s=int16unsigned(%s)" (reg d) (reg r1)
+ | Oneg, [r1] -> sprintf "%s=-%s" (reg d) (reg r1)
+ | Osub, [r1;r2] -> sprintf "%s=%s-%s" (reg d) (reg r1) (reg r2)
+ | Omul, [r1;r2] -> sprintf "%s=%s*%s" (reg d) (reg r1) (reg r2)
+ | Omulimm n, [r1] -> sprintf "%s=%s*%ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Omulhs, [r1;r2] -> sprintf "%s=mulhs(%s,%s)" (reg d) (reg r1) (reg r2)
+ | Omulhu, [r1;r2] -> sprintf "%s=mulhu(%s,%s)" (reg d) (reg r1) (reg r2)
+ | Odiv, [r1;r2] -> sprintf "%s=%s /s %s" (reg d) (reg r1) (reg r2)
+ | Odivu, [r1;r2] -> sprintf "%s=%s /u %s" (reg d) (reg r1) (reg r2)
+ | Omod, [r1;r2] -> sprintf "%s=%s %%s %s" (reg d) (reg r1) (reg r2)
+ | Omodu, [r1;r2] -> sprintf "%s=%s %%u %s" (reg d) (reg r1) (reg r2)
+ | Oand, [r1;r2] -> sprintf "%s=%s & %s" (reg d) (reg r1) (reg r2)
+ | Oandimm n, [r1] -> sprintf "%s=%s & %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oor, [r1;r2] -> sprintf "%s=%s | %s" (reg d) (reg r1) (reg r2)
+ | Oorimm n, [r1] -> sprintf "%s=%s | %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oxor, [r1;r2] -> sprintf "%s=%s ^ %s" (reg d) (reg r1) (reg r2)
+ | Oxorimm n, [r1] -> sprintf "%s=%s ^ %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Onot, [r1] -> sprintf "%s=not(%s)" (reg d) (reg r1)
+ | Oshl, [r1;r2] -> sprintf "%s=%s << %s" (reg d) (reg r1) (reg r2)
+ | Oshlimm n, [r1] -> sprintf "%s=%s << %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oshr, [r1;r2] -> sprintf "%s=%s >>s %s" (reg d) (reg r1) (reg r2)
+ | Oshrimm n, [r1] -> sprintf "%s=%s >>s %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oshrximm n, [r1] -> sprintf "%s=%s >>x %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oshru, [r1;r2] -> sprintf "%s=%s >>u %s" (reg d) (reg r1) (reg r2)
+ | Oshruimm n, [r1] -> sprintf "%s=%s >>u %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Ororimm n, [r1] -> sprintf "%s=%s ror %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oshldimm n, [r1;r2] -> sprintf "%s=(%s, %s) << %ld" (reg d) (reg r1) (reg r2) (camlint_of_coqint n)
+ | Olea addr, args -> sprintf "%s=addr" (reg d)
+ | Omakelong, [r1;r2] -> sprintf "%s=makelong(%s,%s)" (reg d) (reg r1) (reg r2)
+ | Olowlong, [r1] -> sprintf "%s=lowlong(%s)" (reg d) (reg r1)
+ | Ohighlong, [r1] -> sprintf "%s=highlong(%s)" (reg d) (reg r1)
+ | Ocast32signed, [r1] -> sprintf "%s=long32signed(%s)" (reg d) (reg r1)
+ | Ocast32unsigned, [r1] -> sprintf "%s=long32unsigned(%s)" (reg d) (reg r1)
+ | Onegl, [r1] -> sprintf "%s=-l %s" (reg d) (reg r1)
+ | Osubl, [r1;r2] -> sprintf "%s=%s -l %s" (reg d) (reg r1) (reg r2)
+ | Omull, [r1;r2] -> sprintf "%s=%s *l %s" (reg d) (reg r1) (reg r2)
+ | Omullimm n, [r1] -> sprintf "%s=%s *l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+ | Omullhs, [r1;r2] -> sprintf "%s=mullhs(%s,%s)" (reg d) (reg r1) (reg r2)
+ | Omullhu, [r1;r2] -> sprintf "%s=mullhu(%s,%s)" (reg d) (reg r1) (reg r2)
+ | Odivl, [r1;r2] -> sprintf "%s=%s /ls %s" (reg d) (reg r1) (reg r2)
+ | Odivlu, [r1;r2] -> sprintf "%s=%s /lu %s" (reg d) (reg r1) (reg r2)
+ | Omodl, [r1;r2] -> sprintf "%s=%s %%ls %s" (reg d) (reg r1) (reg r2)
+ | Omodlu, [r1;r2] -> sprintf "%s=%s %%lu %s" (reg d) (reg r1) (reg r2)
+ | Oandl, [r1;r2] -> sprintf "%s=%s &l %s" (reg d) (reg r1) (reg r2)
+ | Oandlimm n, [r1] -> sprintf "%s=%s &l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+ | Oorl, [r1;r2] -> sprintf "%s=%s |l %s" (reg d) (reg r1) (reg r2)
+ | Oorlimm n, [r1] -> sprintf "%s=%s |l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+ | Oxorl, [r1;r2] -> sprintf "%s=%s ^l %s" (reg d) (reg r1) (reg r2)
+ | Oxorlimm n, [r1] -> sprintf "%s=%s ^l %Ld" (reg d) (reg r1) (camlint64_of_coqint n)
+ | Onotl, [r1] -> sprintf "%s=notl(%s)" (reg d) (reg r1)
+ | Oshll, [r1;r2] -> sprintf "%s=%s <<l %s" (reg d) (reg r1) (reg r2)
+ | Oshllimm n, [r1] -> sprintf "%s=%s <<l %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oshrl, [r1;r2] -> sprintf "%s=%s >>ls %s" (reg d) (reg r1) (reg r2)
+ | Oshrlimm n, [r1] -> sprintf "%s=%s >>ls %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oshrxlimm n, [r1] -> sprintf "%s=%s >>lx %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oshrlu, [r1;r2] -> sprintf "%s=%s >>lu %s" (reg d) (reg r1) (reg r2)
+ | Oshrluimm n, [r1] -> sprintf "%s=%s >>lu %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Ororlimm n, [r1] -> sprintf "%s=%s rorl %ld" (reg d) (reg r1) (camlint_of_coqint n)
+ | Oleal addr, args -> sprintf "%s=addr" (reg d)
+ | Onegf, [r1] -> sprintf "%s=negf(%s)" (reg d) (reg r1)
+ | Oabsf, [r1] -> sprintf "%s=absf(%s)" (reg d) (reg r1)
+ | Oaddf, [r1;r2] -> sprintf "%s=%s +f %s" (reg d) (reg r1) (reg r2)
+ | Osubf, [r1;r2] -> sprintf "%s=%s -f %s" (reg d) (reg r1) (reg r2)
+ | Omulf, [r1;r2] -> sprintf "%s=%s *f %s" (reg d) (reg r1) (reg r2)
+ | Odivf, [r1;r2] -> sprintf "%s=%s /f %s" (reg d) (reg r1) (reg r2)
+ | Onegfs, [r1] -> sprintf "%s=negfs(%s)" (reg d) (reg r1)
+ | Oabsfs, [r1] -> sprintf "%s=absfs(%s)" (reg d) (reg r1)
+ | Oaddfs, [r1;r2] -> sprintf "%s=%s +fs %s" (reg d) (reg r1) (reg r2)
+ | Osubfs, [r1;r2] -> sprintf "%s=%s -fs %s" (reg d) (reg r1) (reg r2)
+ | Omulfs, [r1;r2] -> sprintf "%s=%s *fs %s" (reg d) (reg r1) (reg r2)
+ | Odivfs, [r1;r2] -> sprintf "%s=%s /fs %s" (reg d) (reg r1) (reg r2)
+ | Osingleoffloat, [r1] -> sprintf "%s=singleoffloat(%s)" (reg d) (reg r1)
+ | Ofloatofsingle, [r1] -> sprintf "%s=floatofsingle(%s)" (reg d) (reg r1)
+ | Ointoffloat, [r1] -> sprintf "%s=intoffloat(%s)" (reg d) (reg r1)
+ | Ofloatofint, [r1] -> sprintf "%s=floatofint(%s)" (reg d) (reg r1)
+ | Ointofsingle, [r1] -> sprintf "%s=intofsingle(%s)" (reg d) (reg r1)
+ | Osingleofint, [r1] -> sprintf "%s=singleofint(%s)" (reg d) (reg r1)
+ | Olongoffloat, [r1] -> sprintf "%s=longoffloat(%s)" (reg d) (reg r1)
+ | Ofloatoflong, [r1] -> sprintf "%s=floatoflong(%s)" (reg d) (reg r1)
+ | Olongofsingle, [r1] -> sprintf "%s=longofsingle(%s)" (reg d) (reg r1)
+ | Osingleoflong, [r1] -> sprintf "%s=singleoflong(%s)" (reg d) (reg r1)
+ | Ocmp c, args -> sprintf "%s=cmp" (reg d)
+ | Osel (c, ty), r1::r2::args -> sprintf "%s=sel" (reg d)
+ | _, _ -> sprintf "N/a")
+
module DFGDot = Graph.Graphviz.Dot(struct
let graph_attributes _ = []
let default_vertex_attributes _ = []
- let vertex_name = string_of_int
+ let vertex_name = function (i, instr) -> sprintf "\"%d:%s\"" i (print_instr instr)
let vertex_attributes _ = []
let get_subgraph _ = None
let default_edge_attributes _ = []
@@ -79,6 +209,8 @@ module IMap = Map.Make (struct
let compare = compare
end)
+let gen_vertex instrs i = (i, List.nth instrs i)
+
(** The DFG type defines a list of instructions with their data dependencies as [edges], which are
the pairs of integers that represent the index of the instruction in the [nodes]. The edges
always point from left to right. *)
@@ -113,28 +245,29 @@ let read_process command =
Buffer.contents buffer
(** Add a dependency if it uses a register that was written to previously. *)
-let add_dep i tree dfg curr =
+let add_dep map i tree dfg curr =
match PTree.get curr tree with
| None -> dfg
- | Some ip -> printf "%d -> %d\n" ip i; DFG.add_edge dfg ip i
+ | Some ip ->
+ DFG.add_edge dfg (List.nth map ip) (List.nth map i)
(** This function calculates the dependencies of each instruction. The nodes correspond to previous
registers that were allocated and show which instruction caused it.
This function only gathers the RAW constraints, and will therefore only be active for operations
that modify registers, which is this case only affects loads and operations. *)
-let accumulate_RAW_deps dfg curr =
+let accumulate_RAW_deps map dfg curr =
let i, dst_map, graph = dfg in
let acc_dep_instruction rs dst =
( i + 1,
PTree.set dst i dst_map,
- List.fold_left (add_dep i dst_map) graph rs
+ List.fold_left (add_dep map i dst_map) graph rs
)
in
let acc_dep_instruction_nodst rs =
( i + 1,
dst_map,
- List.fold_left (add_dep i dst_map) graph rs)
+ List.fold_left (add_dep map i dst_map) graph rs)
in
match curr with
| RBop (op, _, rs, dst) -> acc_dep_instruction rs dst
@@ -201,7 +334,7 @@ let accumulate_RAW_mem_deps instrs dfg curri =
| RBload (_, _, _, _, _) -> (
match next_store 0 (take i instrs |> List.rev) with
| None -> dfg
- | Some d -> DFG.add_edge dfg (i - d - 1) i )
+ | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
| _ -> dfg
let accumulate_WAR_mem_deps instrs dfg curri =
@@ -210,7 +343,7 @@ let accumulate_WAR_mem_deps instrs dfg curri =
| RBstore (_, _, _, _, _) -> (
match next_load 0 (take i instrs |> List.rev) with
| None -> dfg
- | Some d -> DFG.add_edge dfg (i - d - 1) i )
+ | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
| _ -> dfg
let accumulate_WAW_mem_deps instrs dfg curri =
@@ -219,7 +352,7 @@ let accumulate_WAW_mem_deps instrs dfg curri =
| RBstore (_, _, _, _, _) -> (
match next_store 0 (take i instrs |> List.rev) with
| None -> dfg
- | Some d -> DFG.add_edge dfg (i - d - 1) i )
+ | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
| _ -> dfg
(** Predicate dependencies. *)
@@ -266,7 +399,7 @@ let accumulate_RAW_pred_deps instrs dfg curri =
| Some p -> (
match next_setpred p 0 (take i instrs |> List.rev) with
| None -> dfg
- | Some d -> DFG.add_edge dfg (i - d - 1) i )
+ | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
| _ -> dfg
let accumulate_WAR_pred_deps instrs dfg curri =
@@ -275,7 +408,7 @@ let accumulate_WAR_pred_deps instrs dfg curri =
| RBsetpred (_, _, p) -> (
match next_preduse p 0 (take i instrs |> List.rev) with
| None -> dfg
- | Some d -> DFG.add_edge dfg (i - d - 1) i )
+ | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
| _ -> dfg
let accumulate_WAW_pred_deps instrs dfg curri =
@@ -284,7 +417,7 @@ let accumulate_WAW_pred_deps instrs dfg curri =
| RBsetpred (_, _, p) -> (
match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with
| None -> dfg
- | Some d -> DFG.add_edge dfg (i - d - 1) i )
+ | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
| _ -> dfg
(** This function calculates the WAW dependencies, which happen when two writes are ordered one
@@ -294,7 +427,7 @@ let accumulate_WAW_deps instrs dfg curri =
let i, curr = curri in
let dst_dep dst =
match find_next_dst_write i dst (i + 1) (drop (i + 1) instrs) with
- | Some (a, b) -> DFG.add_edge dfg a b
+ | Some (a, b) -> DFG.add_edge dfg (gen_vertex instrs a) (gen_vertex instrs b)
| _ -> dfg
in
match curr with
@@ -303,7 +436,7 @@ let accumulate_WAW_deps instrs dfg curri =
| RBstore (_, _, _, _, _) -> (
match next_store (i + 1) (drop (i + 1) instrs) with
| None -> dfg
- | Some i' -> DFG.add_edge dfg i i' )
+ | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') )
| _ -> dfg
let accumulate_WAR_deps instrs dfg curri =
@@ -313,7 +446,7 @@ let accumulate_WAR_deps instrs dfg curri =
|> List.map (function (d, d') -> (i - d' - 1, d))
in
List.fold_left (fun g ->
- function (d, d') -> DFG.add_edge g d d') dfg dep_list
+ function (d, d') -> DFG.add_edge g (gen_vertex instrs d) (gen_vertex instrs d')) dfg dep_list
in
match curr with
| RBop (_, _, _, dst) -> dst_dep dst
@@ -344,13 +477,13 @@ let check_dependent op1 op2 =
| Some p, Some p' -> not (independant_pred p p')
| _, _ -> true
-let remove_unnecessary_deps graph instrs =
- let is_dependent i1 i2 g =
- let instr1 = List.nth instrs i1 in
- let instr2 = List.nth instrs i2 in
+let remove_unnecessary_deps graph =
+ let is_dependent v1 v2 g =
+ let (_, instr1) = v1 in
+ let (_, instr2) = v2 in
if check_dependent (get_pred instr1) (get_pred instr2)
then g
- else DFG.remove_edge g i1 i2
+ else DFG.remove_edge g v1 v2
in
DFG.fold_edges is_dependent graph graph
@@ -358,28 +491,26 @@ let remove_unnecessary_deps graph instrs =
before the sink of the basic block. After that, there should be constraints for data
dependencies between nodes. *)
let gather_bb_constraints debug bb =
- let _, _, dfg =
- List.fold_left accumulate_RAW_deps
- (0, PTree.empty, DFG.empty)
+ let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in
+ let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in
+ let _, _, dfg' =
+ List.fold_left (accumulate_RAW_deps ibody)
+ (0, PTree.empty, dfg)
bb.bb_body
in
- let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in
- if debug then printf "DFG : %a\n" print_dfg dfg else ();
- let dfg1 = List.fold_left (accumulate_WAW_deps bb.bb_body) dfg ibody in
- if debug then printf "DFG': %a\n" print_dfg dfg1 else ();
- let dfg2 = List.fold_left (accumulate_WAR_deps bb.bb_body) dfg1 ibody in
- if debug then printf "DFG'': %a\n" print_dfg dfg2 else ();
- let dfg3 = List.fold_left (accumulate_RAW_mem_deps bb.bb_body) dfg2 ibody in
- if debug then printf "DFG''': %a\n" print_dfg dfg3 else ();
- let dfg4 = List.fold_left (accumulate_WAR_mem_deps bb.bb_body) dfg3 ibody in
- if debug then printf "DFG'''': %a\n" print_dfg dfg4 else ();
- let dfg5 = List.fold_left (accumulate_WAW_mem_deps bb.bb_body) dfg4 ibody in
- let dfg6 = List.fold_left (accumulate_RAW_pred_deps bb.bb_body) dfg5 ibody in
- let dfg7 = List.fold_left (accumulate_WAR_pred_deps bb.bb_body) dfg6 ibody in
- let dfg8 = List.fold_left (accumulate_WAW_pred_deps bb.bb_body) dfg7 ibody in
- let dfg9 = remove_unnecessary_deps dfg8 bb.bb_body in
- if debug then printf "DFG''''': %a\n" print_dfg dfg9 else ();
- (List.length bb.bb_body, dfg9, successors_instr bb.bb_exit)
+ let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg'
+ [ accumulate_WAW_deps;
+ accumulate_WAR_deps;
+ accumulate_RAW_mem_deps;
+ accumulate_WAR_mem_deps;
+ accumulate_WAW_mem_deps;
+ accumulate_RAW_pred_deps;
+ accumulate_WAR_pred_deps;
+ accumulate_WAW_pred_deps
+ ]
+ in
+ let dfg''' = remove_unnecessary_deps dfg'' in
+ (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit)
let gen_bb_name s i = sprintf "bb%d%s" (P.to_int i) s
@@ -424,7 +555,7 @@ let gather_cfg_constraints (completed, (bvars, constraints, types)) c curr =
^ String.concat ""
(List.map (print_src_order curr)
(List.init num_iters (fun x -> x)))
- ^ DFG.fold_edges (fun e1 e2 s -> s ^ print_data_dep_order curr (e1, e2)) dfg ""
+ ^ DFG.fold_edges (fun e1 e2 s -> s ^ print_data_dep_order curr (fst e1, fst e2)) dfg ""
in
let types' =
types
@@ -443,11 +574,63 @@ let gather_cfg_constraints (completed, (bvars, constraints, types)) c curr =
in
(curr :: completed, (bvars', constraints', types'))
+let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i }
+let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i }
+
+let add_super_nodes n dfg =
+ DFG.fold_vertex (function v1 -> fun g ->
+ (if DFG.in_degree dfg v1 = 0
+ then G.add_edge_e g (encode_bb n 0, 0, encode_var n (fst v1) 0)
+ else g) |>
+ (fun g' ->
+ if DFG.out_degree dfg v1 = 0
+ then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1)
+ else g')) dfg
+
+let add_data_dependencies n =
+ DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g ->
+ G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0)
+ )
+
+let add_ctrl_deps n succs constr =
+ List.fold_left (fun g n' ->
+ G.add_edge_e g (encode_bb n 1, -1, encode_bb n' 0)
+ ) constr succs
+
+let gather_cfg_constraints_g c constr curr =
+ let (n, dfg) = curr in
+ match PTree.get (P.of_int n) c with
+ | None -> assert false
+ | Some { bb_body = body; bb_exit = ctrl } ->
+ add_super_nodes n dfg constr |>
+ add_data_dependencies n dfg |>
+ add_ctrl_deps n (successors_instr ctrl
+ |> List.map P.to_int
+ |> List.filter (fun n' -> n' < n))
+
let rec intersperse s = function
| [] -> []
| [ a ] -> [ a ]
| x :: xs -> x :: s :: intersperse s xs
+let print_objective constr =
+ let vars = G.fold_vertex (fun v1 l ->
+ match v1 with
+ | { sv_type = VarType _; sv_num = 0 } -> print_sv v1 :: l
+ | _ -> l
+ ) constr []
+ in
+ "min: " ^ String.concat "" (intersperse " + " vars) ^ ";\n"
+
+let print_lp constr =
+ print_objective constr ^
+ (G.fold_edges_e (function (e1, w, e2) -> fun s ->
+ s ^ sprintf "%s - %s <= %d;\n" (print_sv e1) (print_sv e2) w
+ ) constr "" |>
+ G.fold_vertex (fun v1 s ->
+ s ^ sprintf "int %s;\n" (print_sv v1)
+ ) constr)
+
let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ]
let parse_soln tree s =
@@ -545,6 +728,16 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
List.fold_left (fun compl ->
gather_cfg_constraints compl c') ([], ([], "", ""))
in
+ let transf_graph (p, (_, dfg, _)) = (P.to_int p, dfg) in
+ let cgraph = List.map transf_graph (PTree.elements c') |>
+ List.fold_left (gather_cfg_constraints_g c) G.empty
+ in
+ let graph = open_out "constr_graph.dot" in
+ fprintf graph "%a\n" GDot.output_graph cgraph;
+ close_out graph;
+ let lp_file = open_out "lp_solve2.txt" in
+ fprintf lp_file "%s\n" (print_lp cgraph);
+ close_out lp_file;
let schedule' = solve_constraints vars constraints types in
(*IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*)
(*printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)