From e6348c97faee39754efd13b69a70c54851e2a789 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 18 Nov 2021 22:11:02 +0000 Subject: Add bourdoncle code --- src/bourdoncle/Bourdoncle.v | 9 ++ src/bourdoncle/BourdoncleAux.ml | 109 +++++++++++++++++++++ src/bourdoncle/README.md | 3 + src/bourdoncle/bourdoncleIterator.ml | 183 +++++++++++++++++++++++++++++++++++ 4 files changed, 304 insertions(+) create mode 100644 src/bourdoncle/Bourdoncle.v create mode 100644 src/bourdoncle/BourdoncleAux.ml create mode 100644 src/bourdoncle/README.md create mode 100644 src/bourdoncle/bourdoncleIterator.ml 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 -- cgit