1 files changed, 66 insertions, 31 deletions

diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 613236f..94225fa 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -26,6 +26,7 @@ open AST
 open Kildall
 open Op
 open RTLBlockInstr
+open Predicate
 open RTLBlock
 open HTL
 open Verilog
@@ -87,14 +88,25 @@ end)(struct
   let default = 0
 end)
 
+module DFGSimp = Graph.Persistent.Graph.Concrete(struct
+    type t = int * instr
+    let compare = compare
+    let equal = (=)
+    let hash = Hashtbl.hash
+  end)
+
+let convert dfg =
+  DFG.fold_vertex (fun v g -> DFGSimp.add_vertex g v) dfg DFGSimp.empty
+  |> DFG.fold_edges (fun v1 v2 g -> DFGSimp.add_edge (DFGSimp.add_edge g v1 v2) v2 v1) dfg
+
 let reg r = sprintf "r%d" (P.to_int r)
-let print_pred r = sprintf "p%d" (Nat.to_int r)
+let print_pred r = sprintf "p%d" (P.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)
+  | RBsetpred (_, _, _, p) -> sprintf "setpred(%s)" (print_pred p)
   | RBop (_, op, args, d) ->
     (match op, args with
     | Omove, _ -> "mov"
@@ -203,6 +215,8 @@ module DFGDot = Graph.Graphviz.Dot(struct
     include DFG
   end)
 
+module DFGDfs = Graph.Traverse.Dfs(DFG)
+
 module IMap = Map.Make (struct
   type t = int
 
@@ -341,7 +355,7 @@ let rec find_all_next_dst_read i dst i' curr =
   | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr'
   | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr'
   | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr'
-  | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr'
+  | RBsetpred (_, _, rs, _) :: curr' -> check_dst rs curr'
 
 let drop i lst =
   let rec drop' i' lst' =
@@ -400,10 +414,11 @@ let accumulate_WAW_mem_deps instrs dfg curri =
 
 let rec in_predicate p p' =
   match p' with
-  | Pvar p'' -> Nat.to_int p = Nat.to_int p''
-  | Pnot p'' -> in_predicate p p''
+  | Plit p'' -> P.to_int p = P.to_int (snd p'')
   | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2
   | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2
+  | Ptrue -> false
+  | Pfalse -> false
 
 let get_predicate = function
   | RBop (p, _, _, _) -> p
@@ -413,7 +428,7 @@ let get_predicate = function
 
 let rec next_setpred p i = function
   | [] -> None
-  | RBsetpred (_, _, p') :: rst ->
+  | RBsetpred (_, _, _, p') :: rst ->
     if in_predicate p' p then
       Some i
     else
@@ -446,7 +461,7 @@ let accumulate_RAW_pred_deps instrs dfg curri =
 let accumulate_WAR_pred_deps instrs dfg curri =
   let i, curr = curri in
   match curr with
-  | RBsetpred (_, _, p) -> (
+  | RBsetpred (_, _, _, p) -> (
       match next_preduse p 0 (take i instrs |> List.rev) with
       | None -> dfg
       | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
@@ -455,8 +470,8 @@ let accumulate_WAR_pred_deps instrs dfg curri =
 let accumulate_WAW_pred_deps instrs dfg curri =
   let i, curr = curri in
   match curr with
-  | RBsetpred (_, _, p) -> (
-      match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with
+  | RBsetpred (_, _, _, p) -> (
+      match next_setpred (Plit (true, p)) 0 (take i instrs |> List.rev) with
       | None -> dfg
       | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) )
   | _ -> dfg
@@ -499,18 +514,18 @@ let assigned_vars vars = function
   | RBop (_, _, _, dst) -> dst :: vars
   | RBload (_, _, _, _, dst) -> dst :: vars
   | RBstore (_, _, _, _, _) -> vars
-  | RBsetpred (_, _, _) -> vars
+  | RBsetpred (_, _, _, _) -> vars
 
 let get_pred = function
   | RBnop -> None
   | RBop (op, _, _, _) -> op
   | RBload (op, _, _, _, _) -> op
   | RBstore (op, _, _, _, _) -> op
-  | RBsetpred (_, _, _) -> None
+  | RBsetpred (_, _, _, _) -> None
 
 let independant_pred p p' =
-  match sat_pred_temp (Nat.of_int 100000) (Pand (p, p')) with
-  | Some None -> true
+  match sat_pred_simple (Pand (p, p')) with
+  | None -> true
   | _ -> false
 
 let check_dependent op1 op2 =
@@ -720,22 +735,22 @@ let parse_soln (tree, bbtree) s =
      else (tree, bbtree))
 
 let solve_constraints constr =
-  let oc = open_out "lpsolve.txt" in
+  let (fn, oc) = Filename.open_temp_file "vericert_" "_lp_solve" in
   fprintf oc "%s\n" (print_lp constr);
   close_out oc;
 
-  Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt")
-  |> drop 3
-  |> List.fold_left parse_soln (IMap.empty, IMap.empty)
+  let res = Str.split (Str.regexp_string "\n") (read_process ("lp_solve " ^ fn))
+            |> drop 3
+            |> List.fold_left parse_soln (IMap.empty, IMap.empty)
+  in
+  Sys.remove fn; res
 
 let subgraph dfg l =
   let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in
   List.fold_left (fun g v ->
       List.fold_left (fun g' v' ->
           let edges = DFG.find_all_edges dfg v v' in
-          List.fold_left (fun g'' e ->
-              DFG.add_edge_e g'' e
-            ) g' edges
+          List.fold_left DFG.add_edge_e g' edges
         ) g l
     ) dfg' l
 
@@ -755,6 +770,21 @@ let combine_bb_schedule schedule s =
   let i, st = s in
   IMap.update st (update_schedule i) schedule
 
+(**let add_el dfg i l =
+  List.*)
+
+let check_in el =
+  List.exists (List.exists ((=) el))
+
+let all_dfs dfg =
+  let roots = DFG.fold_vertex (fun v li ->
+      if DFG.in_degree dfg v = 0 then v :: li else li
+    ) dfg [] in
+  let dfg' = DFG.fold_edges (fun v1 v2 g -> DFG.add_edge g v2 v1) dfg dfg in
+  List.fold_left (fun a el ->
+      if check_in el a then a else
+        (DFGDfs.fold_component (fun v l -> v :: l) [] dfg' el) :: a) [] roots
+
 let range s e =
   List.init (e - s) (fun i -> i)
   |> List.map (fun x -> x + s)
@@ -773,23 +803,29 @@ let transf_rtlpar c c' schedule =
       let i_sched_tree =
         List.fold_left combine_bb_schedule IMap.empty i_sched
       in
-      (*let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd
+      let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd
                  |> List.map (List.map (fun x -> (x, List.nth bb_body' x)))
-      in*)
-      let body2 = List.fold_left (fun x b ->
+      in
+      (*let body2 = List.fold_left (fun x b ->
           match IMap.find_opt b i_sched_tree with
           | Some i -> i :: x
           | None -> [] :: x
         ) [] (range (fst bb_st_e) (snd bb_st_e + 1))
         |> List.map (List.map (fun x -> (x, List.nth bb_body' x)))
         |> List.rev
-      in
+      in*)
       (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*)
       let final_body2 = List.map (fun x -> subgraph dfg x
-                                           |> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x [])
-                                           |> List.rev) body2
+                                           |> (fun x ->
+                                               all_dfs x
+                                               |> List.map (subgraph x)
+                                               |> List.map (fun y ->
+                                                   TopoDFG.fold (fun i l -> snd i :: l) y []
+                                                   |> List.rev))) body
+                                           (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x [])
+                                           |> List.rev) body2*)
       in
-      { bb_body = List.map (fun x -> [x]) final_body2;
+      { bb_body = final_body2;
         bb_exit = ctrl_flow
       }
   in
@@ -799,7 +835,7 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
   let debug = true in
   let transf_graph (_, dfg, _) = dfg in
   let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in
-  (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg (second o)) c' else PTree.empty in*)
+  (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg o) c' else PTree.empty in*)
   let cgraph = PTree.elements c'
                |> List.map (function (x, y) -> (P.to_int x, y))
                |> List.fold_left (gather_cfg_constraints c) G.empty
@@ -809,7 +845,7 @@ let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) =
   close_out graph;
   let schedule' = solve_constraints cgraph 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';*)
+  (**printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*)
   transf_rtlpar c c' schedule'
 
 let rec find_reachable_states c e =
@@ -831,7 +867,6 @@ let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function =
   { fn_sig = f.fn_sig;
     fn_params = f.fn_params;
     fn_stacksize = f.fn_stacksize;
-    fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable;
-    fn_funct_units = f.fn_funct_units;
+    fn_code = scheduled (*List.fold_left (add_to_tree scheduled) PTree.empty reachable*);
     fn_entrypoint = f.fn_entrypoint
   }