Continue on Partitioning algorithm

3 files changed, 66 insertions, 14 deletions

diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index e6ee512..9755125 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -20,7 +20,8 @@ From vericert Require
      Verilog
      Value
      Compiler
-     RTLBlockgen.
+     RTLBlockgen
+     RTLBlock.
 
 From Coq Require DecidableClass.
 
@@ -174,7 +175,7 @@ Set Extraction AccessOpaque.
 Cd "src/extraction".
 Separate Extraction
          Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls
-         RTLBlockgen.transl_program
+         RTLBlockgen.transl_program RTLBlock.successors_instr
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index 9241abe..105dcdd 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -34,25 +34,66 @@ let find_backedge i n =
   List.filter (fun s -> P.lt n s) succ
 
 let find_backedges c =
+  PTree.fold (fun l n i -> List.append (find_backedge i n) l) c []
 
 let prepend_instr i = function
   | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e}
 
-let rec bblock_from_RTL (c : RTL.code) i =
+let translate_inst = function
+  | RTL.Inop _ -> Some RBnop
+  | RTL.Iop (op, ls, dst, _) -> Some (RBop (op, ls, dst))
+  | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (m, addr, ls, dst))
+  | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (m, addr, ls, src))
+  | _ -> None
+
+let translate_cfi = function
+  | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n))
+  | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls))
+  | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n))
+  | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2))
+  | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls))
+  | 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
-  match i, succ with
-  | RTL.Inop _, Some i::[] -> begin
-      match bblock_from_RTL c i with
-      | Errors.OK bb -> Errors.OK (prepend_instr RBnop bb)
+  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)
       | Errors.Error msg -> Errors.Error msg
     end
-  | RTL.Iop (op, rs, dst, _), Some i::[] -> begin
-      match bblock_from_RTL c i with
-      | Errors.OK bb
-    end
+  | (_, Some i'), _ ->
+    Errors.OK {bb_body = []; bb_exit = Some i'}
+  | _, _ -> Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong."))
+
+let rec traverselist f l =
+  match l with
+  | [] -> Errors.OK []
+  | x::xs ->
+    match f x with
+    | Errors.Error msg -> Errors.Error msg
+    | Errors.OK x' ->
+      match traverselist f xs with
+      | Errors.Error msg -> Errors.Error msg
+      | Errors.OK xs' ->
+        Errors.OK (x'::xs')
+
+let rec translate_all start c =
+  match PTree.get start c with
+  | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all."))
+  | Some i ->
+    match next_bblock_from_RTL c i with
+    | Errors.Error msg -> Errors.Error msg
+    | 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 ->
 
 (* 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;
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 7169d4a..2aaa010 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -35,13 +35,13 @@ Inductive instruction : Type :=
 Definition bblock_body : Type := list instruction.
 
 Inductive control_flow_inst : Type :=
-| RBcall : signature -> ident -> list reg -> reg -> node -> control_flow_inst
-| RBtailcall : signature -> ident -> list reg -> control_flow_inst
+| RBcall : signature -> reg + ident -> list reg -> reg -> node -> control_flow_inst
+| RBtailcall : signature -> reg + ident -> list reg -> control_flow_inst
 | RBbuiltin : external_function -> list (builtin_arg reg) ->
               builtin_res reg -> node -> control_flow_inst
 | RBcond : condition -> list reg -> node -> node -> control_flow_inst
 | RBjumptable : reg -> list node -> control_flow_inst
-| RBredurn : option reg -> control_flow_inst.
+| RBreturn : option reg -> control_flow_inst.
 
 Record bblock : Type := mk_bblock {
     bb_body: bblock_body;
@@ -67,3 +67,13 @@ Definition funsig (fd: fundef) :=
   | Internal f => fn_sig f
   | External ef => ef_sig ef
   end.
+
+Definition successors_instr (i : control_flow_inst) : list node :=
+  match i with
+  | RBcall sig ros args res s => s :: nil
+  | RBtailcall sig ros args => nil
+  | RBbuiltin ef args res s => s :: nil
+  | RBcond cond args ifso ifnot => ifso :: ifnot :: nil
+  | RBjumptable arg tbl => tbl
+  | RBreturn optarg => nil
+  end.