Add bourdoncle to build

8 files changed, 64 insertions, 28 deletions

diff --git a/Makefile b/Makefile
index 0749d1c..5577ba9 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ COQMAKE := $(COQBIN)coq_makefile
 
 COQDOCFLAGS := --no-lib-name -l
 
-VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls, src/$(d)/*.v)
+VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls bourdoncle, src/$(d)/*.v)
 
 PREFIX ?= .
 
diff --git a/src/Compiler.v b/src/Compiler.v
index e4ab607..b907629 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -67,7 +67,7 @@ Require vericert.hls.RTLBlockgen.
 Require vericert.hls.RTLPargen.
 Require vericert.hls.RTLParFUgen.
 Require vericert.hls.HTLPargen.
-Require vericert.hls.Pipeline.
+(*Require vericert.hls.Pipeline.*)
 Require vericert.hls.IfConversion.
 (*Require vericert.hls.PipelineOp.*)
 Require vericert.HLSOpts.
diff --git a/src/bourdoncle/BourdoncleAux.ml b/src/bourdoncle/BourdoncleAux.ml
index 3c7fd58..a35004e 100644
--- a/src/bourdoncle/BourdoncleAux.ml
+++ b/src/bourdoncle/BourdoncleAux.ml
@@ -4,7 +4,8 @@ open Camlcoq
 open BinNums
 open BinPos
 open Maps
-open RTL
+open RTLBlock
+open RTLBlockInstr
 open BourdoncleIterator
 module B = Bourdoncle
 
@@ -38,25 +39,23 @@ let bourdoncleListToString (l : B.bourdoncle list) : string =
 (* Dummy type to avoid redefining existing functions *)
 type instr = | Inop
 
+let rec get_exits = function
+  | RBgoto j -> [(int_of_positive j, Inop)]
+  | RBcall (_,_,_,dst,j) -> [(int_of_positive j, Inop)]
+  | RBtailcall _ -> []
+  | RBbuiltin (_,_,dst,j) -> [(int_of_positive j, Inop)]
+  | RBcond (c,args,j,k) -> [(int_of_positive j, Inop);(int_of_positive k, Inop)]
+  | RBjumptable (_,tbl) -> List.map (fun j -> (int_of_positive j, Inop)) tbl
+  | RBpred_cf (p, cf1, cf2) -> List.append (get_exits cf1) (get_exits cf2)
+  | RBreturn _ -> []
+
 let build_cfg f =
   let entry = int_of_positive f.fn_entrypoint in
   let max = PTree.fold (fun m n _ -> max m (int_of_positive n)) f.fn_code 0 in
   (* nodes are between 1 and max+1 *)
   let succ = Array.make (max+1) [] in
   let _ = PTree.fold (fun () n ins ->
-			succ.(int_of_positive n) <-
-        let inop : instr = Inop in
-			  match ins with
-			    | RTL.Inop j -> [(int_of_positive j, inop)]
-			    | RTL.Iop (op,args,dst,j) -> [(int_of_positive j, Inop)]
-			    | RTL.Iload (_,_,_,dst,j) -> [(int_of_positive j, Inop)]
-			    | RTL.Istore (_,_,_,_,j) -> [(int_of_positive j, Inop)]
-			    | RTL.Icall (_,_,_,dst,j) -> [(int_of_positive j, Inop)]
-			    | RTL.Itailcall _ -> []
-			    | RTL.Ibuiltin (_,_,dst,j) -> [(int_of_positive j, Inop)]
-			    | RTL.Icond (c,args,j,k) -> [(int_of_positive j, Inop);(int_of_positive k, Inop)]
-			    | RTL.Ijumptable (_,tbl) -> List.map (fun j -> (int_of_positive j, inop)) tbl
-			    | RTL.Ireturn _ -> []) f.fn_code () in
+			succ.(int_of_positive n) <- get_exits ins.bb_exit) f.fn_code () in
     { entry = entry; succ = succ }
 
 let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list =
@@ -66,7 +65,7 @@ let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list =
     | (L ((I h) :: l, _)) :: r -> B.L (positive_of_int h, build_bourdoncle' l) :: (build_bourdoncle' r)
     | _ -> failwith "Assertion error: invalid bourdoncle ist"
 
-let build_bourdoncle'' (f : coq_function) : B.bourdoncle =
+let build_bourdoncle'' (f : bb coq_function) : B.bourdoncle =
   let cfg = build_cfg f in
   match build_bourdoncle' (get_bourdoncle cfg) with
     | [] -> failwith "assertion error: empty bourdoncle"
@@ -103,7 +102,7 @@ let build_order (b : B.bourdoncle) : coq_N PMap.t =
   let bo = build_order' (linearize b) (succ_pos N0) in
   (succ_pos N0, bo)
 
-let build_bourdoncle (f : coq_function) : (B.bourdoncle * coq_N PMap.t) =
+let build_bourdoncle (f : bb coq_function) : (B.bourdoncle * coq_N PMap.t) =
   let b = build_bourdoncle'' f in
   let bo = build_order b in
   (b, bo)
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 9b82e1b..395ec47 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -24,9 +24,10 @@ From vericert Require
      RTLPar
      RTLBlockInstr
      HTLgen
-     Pipeline
+     (*Pipeline*)
      HLSOpts
      Predicate
+     Bourdoncle
 .
 
 From Coq Require DecidableClass.
@@ -182,10 +183,13 @@ Extract Inlined Constant Binary.B2R => "fun _ -> assert false".
 Extract Inlined Constant Binary.round_mode => "fun _ -> assert false".
 Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
 
-Extract Constant Pipeline.pipeline => "pipelining.pipeline".
+(*Extract Constant Pipeline.pipeline => "pipelining.pipeline".*)
 Extract Constant RTLBlockgen.partition => "Partition.partition".
 Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".
 
+(* Loop normalization *)
+Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle".
+
 (* Needed in Coq 8.4 to avoid problems with Function definitions. *)
 Set Extraction AccessOpaque.
 
@@ -195,9 +199,9 @@ Separate Extraction
          vericert.Compiler.transf_hls_temp
          RTLBlockgen.transl_program RTLBlockInstr.successors_instr
          HTLgen.tbl_to_case_expr
-         Pipeline.pipeline
          Predicate.sat_pred_simple
          Verilog.stmnt_to_list
+         Bourdoncle.bourdoncle
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index b397d43..4585770 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -26,6 +26,9 @@ Require Import vericert.common.Vericertlib.
 Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLBlock.
 Require Import vericert.hls.Predicate.
+Require Import vericert.bourdoncle.Bourdoncle.
+
+Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N).
 
 (*|
 =============
@@ -96,11 +99,34 @@ Definition find_all_backedges (c: code) : list node :=
 Definition has_backedge (entry: node) (be: list node) :=
   any (fun x => Pos.eqb entry x) be.
 
-Definition find_blocks_with_cond (c: code) : list (node * bblock) :=
+Fixpoint get_loops (b: bourdoncle): list node :=
+  match b with
+  | L h b' => h::(fold_right (fun a b => get_loops a ++ b) nil b')
+  | I h => nil
+  end.
+
+Definition is_loop (b: list node) (n: node) :=
+  any (fun x => Pos.eqb x n) b.
+
+Definition is_flat_cfi (n: cf_instr) :=
+  match n with
+  | RBcond _ _ _ _ => false
+  | RBjumptable _ _ => false
+  | RBpred_cf _ _ _ => false
+  | _ => true
+  end.
+
+Definition is_flat (c: code) (succ: node) :=
+  match c ! succ with
+  | Some bblock => is_flat_cfi bblock.(bb_exit)
+  | None => false
+  end.
+
+Definition find_blocks_with_cond ep (b: list node) (c: code) : list (node * bblock) :=
   let backedges := find_all_backedges c in
   List.filter (fun x => is_cond_cfi (snd x).(bb_exit) &&
-                        negb (has_backedge (fst x) backedges) &&
-                        all (fun x' => negb (has_backedge x' backedges))
+                        (negb (is_loop b (fst x)) || Pos.eqb (fst x) ep) &&
+                        all (fun x' => is_flat c x')
                             (successors_instr (snd x).(bb_exit))
               ) (PTree.elements c).
 
@@ -109,8 +135,10 @@ Definition if_convert_code (p: nat * code) (nb: node * bblock) :=
   (S (fst p), PTree.set (fst nb) nbb (snd p)).
 
 Definition transf_function (f: function) : function :=
+  let (b, _) := build_bourdoncle f in
+  let b' := get_loops b in
   let (_, c) := List.fold_left if_convert_code
-                               (find_blocks_with_cond f.(fn_code))
+                               (find_blocks_with_cond f.(fn_entrypoint) b' f.(fn_code))
                                (1%nat, f.(fn_code)) in
   mkfunction f.(fn_sig) f.(fn_params) f.(fn_stacksize) c f.(fn_entrypoint).
 
diff --git a/src/hls/Pipeline.v b/src/hls/Pipeline.v
index 7f1485a..67ab1f5 100644
--- a/src/hls/Pipeline.v
+++ b/src/hls/Pipeline.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import compcert.lib.Maps.
+(*Require Import compcert.lib.Maps.
 Require Import compcert.common.AST.
 Require Import compcert.backend.RTL.
 
@@ -26,3 +26,4 @@ Definition transf_fundef := transf_fundef pipeline.
 
 Definition transf_program : program -> program :=
   transform_program transf_fundef.
+*)
diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v
index 793b752..bb01ff9 100644
--- a/src/hls/PipelineOp.v
+++ b/src/hls/PipelineOp.v
@@ -79,7 +79,7 @@ Definition map_at_err {A: Type} (n: nat) (f: A -> A) (l: list A): option (list A
   then None
   else Some (map_at n f l).
 
-Definition replace_div' sdiv udiv (d: instr) :=
+(*Definition replace_div' sdiv udiv (d: instr) :=
   match d with
   | RBop op Odiv args dst => RBpiped op sdiv args
   | RBop op Odivu args dst => RBpiped op udiv args
@@ -190,3 +190,4 @@ Definition transf_fundef (fd: fundef) : fundef :=
 
 Definition transf_program (p: program) : program :=
   transform_program transf_fundef p.
+*)
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index e557d4b..1969cad 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -637,7 +637,10 @@ let add_cycle_constr maxf n dfg constr =
                       - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int maxf))) - 1),
                       encode_var n (fst v') 0)
     ) constr (DFG.fold_vertex (fun v l ->
-      List.append l (longest_path v |> constrained_paths |> List.map (function (v', w) -> (v, v', - w)))
+      List.append l (longest_path v (*|> (function l -> List.iter (function (a, x) ->
+          printf "c: %d %d\n" (fst a) x) l; l)*) |> constrained_paths (* |> (function l -> List.iter (function (a, x) ->
+          printf "%d %d\n" (fst a) x) l; l)*)
+                     |> List.map (function (v', w) -> (v, v', - w)))
     ) dfg [])
 
 type resource =