Add working partitioning algorithm

4 files changed, 175 insertions, 42 deletions

diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index 105dcdd..1c25cdc 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -1,4 +1,4 @@
-(*
+ (*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
  *
@@ -29,12 +29,15 @@ open RTLBlock
 
 (* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass
    [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *)
-let find_backedge i n =
+let find_edge i n =
   let succ = RTL.successors_instr i in
-  List.filter (fun s -> P.lt n s) succ
+  let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in
+  (begin match filt with [] -> [] | _ -> [n] end, filt)
 
-let find_backedges c =
-  PTree.fold (fun l n i -> List.append (find_backedge i n) l) c []
+let find_edges c =
+  PTree.fold (fun l n i ->
+      let f = find_edge i n in
+      (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], [])
 
 let prepend_instr i = function
   | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e}
@@ -55,47 +58,63 @@ let translate_cfi = function
   | RTL.Ireturn r -> Some (RBreturn r)
   | _ -> None
 
-let rec next_bblock_from_RTL (c : RTL.code) i =
-  let succ = List.map (fun i -> PTree.get i c) (RTL.successors_instr i) in
+let rec next_bblock_from_RTL is_start e (c : RTL.code) s i =
+  let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in
   let trans_inst = (translate_inst i, translate_cfi i) in
   match trans_inst, succ with
-  | (Some i', _), Some i::[] -> begin
-      match next_bblock_from_RTL c i with
-      | Errors.OK bb -> Errors.OK (prepend_instr i' bb)
+  | (None, Some i'), _ ->
+    Errors.OK {bb_body = []; bb_exit = Some i'}
+  | (Some i', None), (s', Some i_n)::[] ->
+    if List.exists (fun x -> x = s) (fst e) then
+      Errors.OK { bb_body = [i']; bb_exit = Some (RBgoto s') }
+    else if List.exists (fun x -> x = s) (snd e) && not is_start then begin
+      Errors.OK { bb_body = []; bb_exit = Some (RBgoto s) }
+    end else begin
+      match next_bblock_from_RTL false e c s' i_n with
+      | Errors.OK bb ->
+        Errors.OK (prepend_instr i' bb)
       | Errors.Error msg -> Errors.Error msg
     end
-  | (_, Some i'), _ ->
-    Errors.OK {bb_body = []; bb_exit = Some i'}
-  | _, _ -> Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong."))
+  | _, _ ->
+    Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong."))
 
-let rec traverselist f l =
+let rec traverseacc f l c =
   match l with
-  | [] -> Errors.OK []
+  | [] -> Errors.OK c
   | x::xs ->
-    match f x with
+    match f x c with
     | Errors.Error msg -> Errors.Error msg
     | Errors.OK x' ->
-      match traverselist f xs with
+      match traverseacc f xs x' with
       | Errors.Error msg -> Errors.Error msg
-      | Errors.OK xs' ->
-        Errors.OK (x'::xs')
+      | Errors.OK xs' -> Errors.OK xs'
 
-let rec translate_all start c =
-  match PTree.get start c with
+let rec translate_all edge c s c_bb =
+  match PTree.get s c with
   | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all."))
   | Some i ->
-    match next_bblock_from_RTL c i with
+    match next_bblock_from_RTL true edge c s i with
     | Errors.Error msg -> Errors.Error msg
+    | Errors.OK {bb_exit = None; _} ->
+      Errors.Error (Errors.msg (coqstring_of_camlstring "Error in translate all"))
     | Errors.OK {bb_body = bb; bb_exit = Some e} ->
       let succ = successors_instr e in
-      match traverselist (fun s -> translate_all s c) succ with
-      | Errors.OK l ->
+      match traverseacc (translate_all edge c) succ c_bb with
+      | Errors.Error msg -> Errors.Error msg
+      | Errors.OK c' ->
+        Errors.OK (PTree.set s {bb_body = bb; bb_exit = Some e} c')
 
 (* Partition a function and transform it into RTLBlock. *)
 let function_from_RTL f =
-  let ba = find_backedges f.RTL.fn_code in
-  { fn_sig = f.RTL.fn_entrypoint;
-    fn_stacksize = f.RTL.fn_stacksize;
-    fn_entrypoint = f.RTL.fn_entrypoint;
-    fn_code = f.RTL.fn_code
-  }
+  let e = find_edges f.RTL.fn_code in
+  match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint PTree.empty with
+  | Errors.Error msg -> Errors.Error msg
+  | Errors.OK c ->
+    Errors.OK { fn_sig = f.RTL.fn_sig;
+                fn_stacksize = f.RTL.fn_stacksize;
+                fn_params = f.RTL.fn_params;
+                fn_entrypoint = f.RTL.fn_entrypoint;
+                fn_code = c
+              }
+
+let partition = function_from_RTL
diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml
index e69de29..45bd253 100644
--- a/src/hls/PrintRTLBlock.ml
+++ b/src/hls/PrintRTLBlock.ml
@@ -0,0 +1,119 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Pretty-printers for RTL code *)
+
+open Printf
+open Camlcoq
+open Datatypes
+open Maps
+open AST
+open RTLBlock
+open PrintAST
+
+(* Printing of RTL code *)
+
+let reg pp r =
+  fprintf pp "x%d" (P.to_int r)
+
+let rec regs pp = function
+  | [] -> ()
+  | [r] -> reg pp r
+  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
+
+let ros pp = function
+  | Coq_inl r -> reg pp r
+  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
+
+let print_bblock_body pp i =
+  fprintf pp "\t\t";
+  match i with
+  | RBnop -> fprintf pp "nop\n"
+  | RBop(op, ls, dst) ->
+     fprintf pp "%a = %a\n"
+       reg dst (PrintOp.print_operation reg) (op, ls)
+  | RBload(chunk, addr, args, dst) ->
+     fprintf pp "%a = %s[%a]\n"
+       reg dst (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+  | RBstore(chunk, addr, args, src) ->
+     fprintf pp "%s[%a] = %a\n"
+       (name_of_chunk chunk)
+       (PrintOp.print_addressing reg) (addr, args)
+       reg src
+
+let print_bblock_exit pp i =
+  fprintf pp "\t\t";
+  match i with
+  | Some(RBcall(_, fn, args, res, _)) ->
+      fprintf pp "%a = %a(%a)\n"
+        reg res ros fn regs args;
+  | Some(RBtailcall(_, fn, args)) ->
+      fprintf pp "tailcall %a(%a)\n"
+        ros fn regs args
+  | Some(RBbuiltin(ef, args, res, _)) ->
+      fprintf pp "%a = %s(%a)\n"
+        (print_builtin_res reg) res
+        (name_of_external ef)
+        (print_builtin_args reg) args
+  | Some(RBcond(cond, args, s1, s2)) ->
+      fprintf pp "if (%a) goto %d else goto %d\n"
+        (PrintOp.print_condition reg) (cond, args)
+        (P.to_int s1) (P.to_int s2)
+  | Some(RBjumptable(arg, tbl)) ->
+      let tbl = Array.of_list tbl in
+      fprintf pp "jumptable (%a)\n" reg arg;
+      for i = 0 to Array.length tbl - 1 do
+        fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i))
+      done
+  | Some(RBreturn None) ->
+      fprintf pp "return\n"
+  | Some(RBreturn (Some arg)) ->
+      fprintf pp "return %a\n" reg arg
+  | Some(RBgoto n) ->
+     fprintf pp "goto %d\n" (P.to_int n)
+  | None -> fprintf pp "\n"
+
+let print_bblock pp (pc, i) =
+  fprintf pp "%5d:{\n" pc;
+  List.iter (print_bblock_body pp) i.bb_body;
+  print_bblock_exit pp i.bb_exit;
+  fprintf pp "\t}\n\n"
+
+let print_function pp id f =
+  fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
+  let instrs =
+    List.sort
+      (fun (pc1, _) (pc2, _) -> compare pc2 pc1)
+      (List.rev_map
+        (fun (pc, i) -> (P.to_int pc, i))
+        (PTree.elements f.fn_code)) in
+  List.iter (print_bblock pp) instrs;
+  fprintf pp "}\n\n"
+
+let print_globdef pp (id, gd) =
+  match gd with
+  | Gfun(Internal f) -> print_function pp id f
+  | _ -> ()
+
+let print_program pp (prog: program) =
+  List.iter (print_globdef pp) prog.prog_defs
+
+let destination : string option ref = ref None
+
+let print_if prog =
+  match !destination with
+  | None -> ()
+  | Some f ->
+     let oc = open_out f in
+     print_program oc prog;
+     close_out oc
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 2aaa010..a1c3f25 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -41,7 +41,8 @@ Inductive control_flow_inst : Type :=
               builtin_res reg -> node -> control_flow_inst
 | RBcond : condition -> list reg -> node -> node -> control_flow_inst
 | RBjumptable : reg -> list node -> control_flow_inst
-| RBreturn : option reg -> control_flow_inst.
+| RBreturn : option reg -> control_flow_inst
+| RBgoto : node -> control_flow_inst.
 
 Record bblock : Type := mk_bblock {
     bb_body: bblock_body;
@@ -76,4 +77,5 @@ Definition successors_instr (i : control_flow_inst) : list node :=
   | RBcond cond args ifso ifnot => ifso :: ifnot :: nil
   | RBjumptable arg tbl => tbl
   | RBreturn optarg => nil
+  | RBgoto n => n :: nil
   end.
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index 05f9a32..6b3e9c3 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -24,16 +24,9 @@ From compcert Require Import
 From vericert Require Import
      RTLBlock.
 
-Parameter partition : RTL.code -> code.
+Parameter partition : RTL.function -> Errors.res function.
 
-Definition transl_function (f : RTL.function) : function :=
-  mkfunction f.(RTL.fn_sig)
-             f.(RTL.fn_params)
-             f.(RTL.fn_stacksize)
-             (partition f.(RTL.fn_code))
-             f.(RTL.fn_entrypoint).
+Definition transl_fundef := transf_partial_fundef partition.
 
-Definition transl_fundef := transf_fundef transl_function.
-
-Definition transl_program : RTL.program -> program :=
-  transform_program transl_fundef.
+Definition transl_program : RTL.program -> Errors.res program :=
+  transform_partial_program transl_fundef.