Add bourdoncle code

4 files changed, 304 insertions, 0 deletions

diff --git a/src/bourdoncle/Bourdoncle.v b/src/bourdoncle/Bourdoncle.v
new file mode 100644
index 0000000..9d470b7
--- /dev/null
+++ b/src/bourdoncle/Bourdoncle.v
@@ -0,0 +1,9 @@
+(** Type of a Bourdoncle component. *)
+
+Require Import List.
+Require Import BinPos.
+Notation node := positive.
+
+Inductive bourdoncle :=
+| I : node -> bourdoncle
+| L : node -> list bourdoncle -> bourdoncle.
diff --git a/src/bourdoncle/BourdoncleAux.ml b/src/bourdoncle/BourdoncleAux.ml
new file mode 100644
index 0000000..3c7fd58
--- /dev/null
+++ b/src/bourdoncle/BourdoncleAux.ml
@@ -0,0 +1,109 @@
+(* Note: this file is used by SliceToString, so it must not include it *)
+
+open Camlcoq
+open BinNums
+open BinPos
+open Maps
+open RTL
+open BourdoncleIterator
+module B = Bourdoncle
+
+type node = P.t
+
+let int_of_positive p =
+  let i = P.to_int p in
+    i - 1
+
+let positive_of_int n = P.of_int (n+1)
+
+(* Functions copied from SliceToString to avoid mutual inclusion *)
+let nodeToString (p : P.t) : string =
+  Int.to_string (P.to_int p)
+let rec cleanListToString' (aToString: 'a -> string) (l : 'a list) =
+  match l with
+  | [] -> ""
+  | e :: r -> " " ^ (aToString e) ^ (cleanListToString' aToString r)
+let cleanListToString (aToString: 'a -> string) (l : 'a list) =
+  match l with
+  | [] -> "[]"
+  | [e] -> "(" ^ (aToString e) ^ ")"
+  | e :: r -> "(" ^ (aToString e) ^ (cleanListToString' aToString r) ^ ")"
+let rec bourdoncleToString (b : B.bourdoncle) : string =
+  match b with
+    | B.I n -> (nodeToString n)
+    | B.L (h, lb) -> cleanListToString bourdoncleToString ((B.I h) :: lb)
+let bourdoncleListToString (l : B.bourdoncle list) : string =
+  cleanListToString bourdoncleToString l
+
+(* Dummy type to avoid redefining existing functions *)
+type instr = | Inop
+
+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
+    { entry = entry; succ = succ }
+
+let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list =
+  match bl with
+    | [] -> []
+    | (I i) :: r -> B.I (positive_of_int i) :: (build_bourdoncle' r)
+    | (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 cfg = build_cfg f in
+  match build_bourdoncle' (get_bourdoncle cfg) with
+    | [] -> failwith "assertion error: empty bourdoncle"
+    | l ->
+      begin
+        match l with
+          | B.I h :: r -> B.L (h, r)
+          | B.L (_, _) :: _ ->
+            begin
+              Printf.printf "ASSERTION ERROR: invalid program structure (too many bourdoncles)\n";
+              Printf.printf "Head should be an element, but it is a list\n";
+              Printf.printf "Failed at: %s\n" (bourdoncleListToString l);
+              failwith "assertion error"
+            end
+          | _ -> failwith "assertion error : ???"
+      end
+
+(* Auxiliary function for build_order *)
+let rec linearize (b : B.bourdoncle) : node list =
+  match b with
+    | B.I n -> [n]
+    | B.L (h, l) -> List.fold_left (fun l0 b' -> l0 @ (linearize b')) [h] l
+
+let succ_pos = function
+  | N0 -> Npos Coq_xH
+  | Npos p -> Npos (Pos.succ p)
+
+let rec build_order' (l : node list) (count : coq_N) : coq_N PTree.t =
+  match l with
+    | [] -> PTree.empty
+    | n :: r -> PTree.set n count (build_order' r (succ_pos count))
+
+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 b = build_bourdoncle'' f in
+  let bo = build_order b in
+  (b, bo)
diff --git a/src/bourdoncle/README.md b/src/bourdoncle/README.md
new file mode 100644
index 0000000..e1d02b9
--- /dev/null
+++ b/src/bourdoncle/README.md
@@ -0,0 +1,3 @@
+# Bourdoncle implementation
+
+This code was taken from WCET analysis in CompCert, which can be found [here](http://www.irisa.fr/celtique/ext/loopbound/).
diff --git a/src/bourdoncle/bourdoncleIterator.ml b/src/bourdoncle/bourdoncleIterator.ml
new file mode 100644
index 0000000..3cf0c78
--- /dev/null
+++ b/src/bourdoncle/bourdoncleIterator.ml
@@ -0,0 +1,183 @@
+type ('ab, 'instr) adom = {
+  order: 'ab -> 'ab -> bool;
+  join: 'ab -> 'ab -> 'ab;
+  widen: 'ab -> 'ab -> 'ab;
+  top: unit -> 'ab;
+  bot: unit -> 'ab;
+  transfer: 'instr -> 'ab -> 'ab;
+  to_string: 'ab -> string
+}
+
+type 'instr cfg = {
+  entry: int;
+  succ: (int * 'instr) list array;
+}
+
+(* Utilities *)
+let rec print_list_sep_rec sep pp = function
+  | [] -> ""
+  | x::q -> sep^(pp x)^(print_list_sep_rec sep pp q)
+
+let rec print_list_sep_list_rec sep pp = function
+  | [] -> []
+  | x::q -> (sep^(pp x))::(print_list_sep_list_rec sep pp q)
+
+let print_list_sep sep pp = function
+  | [] -> ""
+  | x::q -> (pp x)^(print_list_sep_rec sep pp q)
+
+let dot_cfg cfg filename =
+  let f = open_out filename in
+    Printf.fprintf f "digraph {\n";
+    Array.iteri
+      (fun i l ->
+	 List.iter (fun (j,_) -> Printf.fprintf f "  n%d -> n%d\n" i j) l)
+      cfg.succ;
+    Printf.fprintf f "}\n";
+    close_out f
+
+
+(* Bourdoncle *)
+type bourdoncle = L of (bourdoncle list) * Ptset.t | I of int
+
+let rec string_of_bourdoncle_list l =
+    print_list_sep  " " string_of_bourdoncle l
+and string_of_bourdoncle = function
+  | L (l,_) -> "("^(string_of_bourdoncle_list l)^")"
+  | I i -> string_of_int i
+
+(* For efficiency we pre-compute the set of nodes in a cfc *)
+let add_component =
+  List.fold_left
+    (fun s b ->
+       match b with
+	 | I i -> Ptset.add i s
+	 | L (_,s') -> Ptset.union s s')
+    Ptset.empty
+
+(* Bourdoncle strategy computation  *)
+let get_bourdoncle cfg =
+  let date = ref 0 in
+  let debut = Array.map (fun _ -> 0) cfg.succ in
+  let stack = Stack.create () in
+  let rec component i =
+    let partition = ref [] in
+      List.iter
+	(fun (j,_) ->
+	   if debut.(j)=0 then ignore (visite j partition))
+	cfg.succ.(i);
+      (I i) :: !partition
+  and visite i partition =
+    incr date;
+    debut.(i) <- !date;
+    let min = ref !date in
+    let loop = ref false in
+      Stack.push i stack;
+      List.iter
+	(fun (j,_) ->
+	   let m = if debut.(j)=0 then visite j partition else debut.(j) in
+	     if m <= !min then
+	       begin
+		 min := m;
+		 loop := true
+	       end)
+	cfg.succ.(i);
+      if !min=debut.(i) then
+	begin
+	  debut.(i) <- max_int;
+	  let k = ref (Stack.pop stack) in
+	    if !loop then begin
+	      while (!k<>i) do
+		debut.(!k) <- 0;
+		k := Stack.pop stack;
+	      done;
+	      let c = component i in
+		partition := (L (c,add_component c)) :: !partition
+	    end
+	    else partition := (I i) :: !partition
+	end;
+      !min
+  in
+  let partition = ref [] in
+    (* only one entry in the cfg *)
+    ignore (visite cfg.entry partition);
+    Array.iteri (fun i d -> if d=0 then cfg.succ.(i) <- []) debut;
+    !partition
+
+(* predecessors *)
+let get_pred cfg =
+  let pred = Array.make (Array.length cfg.succ) [] in
+    Array.iteri
+      (fun i succs ->
+	 List.iter
+	   (fun (j,ins) ->
+	      pred.(j) <- (i,ins) :: pred.(j))
+	   succs
+      )
+      cfg.succ;
+    pred
+
+let check_fixpoint adom cfg res =
+  if not (adom.order (adom.top ()) res.(cfg.entry)) then
+    failwith "res.(ENTRY) should be top !\n";
+  Array.iteri
+      (fun i succs ->
+	 List.iter
+	 (fun (j,op) ->
+	    if not (adom.order (adom.transfer op res.(i)) res.(j)) then
+	      begin
+		dot_cfg cfg "debug_bourdoncle.dot";
+		failwith (Printf.sprintf "res.(%d) should be lower than res.(%d) !\n" i j)
+	      end)
+	   succs)
+    cfg.succ
+
+let option_down_iterations = ref 1
+
+let rec f_list f acc = function
+    [] -> acc
+  | x::q -> f_list f (f acc x) q
+
+let run_with_bourdoncle adom b cfg =
+  let preds = get_pred cfg in
+  let res = Array.init (Array.length preds) (fun _ -> adom.bot ()) in
+  let join_list = f_list adom.join in
+  let _ = res.(cfg.entry) <- adom.top () in
+    let upd j =
+      if j <> cfg.entry then
+	res.(j) <-
+	  join_list (adom.bot ())
+	  (List.map (fun (i,op) -> adom.transfer op res.(i)) preds.(j)) in
+    let upd_except_cfc j cfc =
+      if j <> cfg.entry then
+	res.(j) <- join_list res.(j)
+	  (List.map (fun (i,op) -> adom.transfer op res.(i))
+	     (List.filter (fun (i,op) -> not (Ptset.mem i cfc)) preds.(j)))
+    in
+    let nb_down = !option_down_iterations in
+    let rec iter_component down = function
+      | L (I head::rest,cfc) ->
+	  let rec aux down = function
+	      [] ->
+		let old_ab = res.(head) in
+		let _ = upd head in
+		let new_ab = res.(head) in
+		  if down >= nb_down || (new_ab = old_ab) then ()
+		  else if not (adom.order new_ab old_ab) then
+		    begin
+		      res.(head) <- adom.widen old_ab new_ab;
+		      aux (-1) rest
+		    end
+		  else (upd head; aux (down+1) rest)
+	    | b::q -> iter_component down b; aux down q in
+	    upd_except_cfc head cfc;
+	    aux down rest
+      | I i -> upd i
+      | _ -> assert false in
+      List.iter (iter_component (-1)) b;
+      check_fixpoint adom cfg res;
+      res
+
+let run adom cfg =
+  let b = get_bourdoncle cfg in
+    run_with_bourdoncle adom b cfg