diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 01:05:32 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 01:05:32 +0100 |
| commit | 0a44da6a7037d9eb270386eeef4f929177c4ec0d (patch) | |
| tree | ac08c768bbdedda7d791972ee0e2c4db1fb5ac14 /src/bourdoncle | |
| parent | 27714f85233e52978caebd67b550bde51e693d48 (diff) | |
| download | vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.tar.gz vericert-0a44da6a7037d9eb270386eeef4f929177c4ec0d.zip | |
Rewrite a lot fixing scheduling of Gible
Diffstat (limited to 'src/bourdoncle')
| -rw-r--r-- | src/bourdoncle/BourdoncleAux.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/bourdoncle/BourdoncleAux.ml b/src/bourdoncle/BourdoncleAux.ml index a35004e..1ea4de6 100644 --- a/src/bourdoncle/BourdoncleAux.ml +++ b/src/bourdoncle/BourdoncleAux.ml @@ -4,8 +4,9 @@ open Camlcoq open BinNums open BinPos open Maps -open RTLBlock -open RTLBlockInstr +open Gible +open GibleSeq +open GibleSeq open BourdoncleIterator module B = Bourdoncle @@ -46,7 +47,6 @@ let rec get_exits = function | 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 = @@ -55,7 +55,8 @@ let build_cfg f = (* 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) <- get_exits ins.bb_exit) f.fn_code () in + succ.(int_of_positive n) <- List.map (fun j -> (int_of_positive j, Inop)) + (all_successors ins)) f.fn_code () in { entry = entry; succ = succ } let rec build_bourdoncle' (bl : bourdoncle list) : B.bourdoncle list = @@ -65,7 +66,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 : bb coq_function) : B.bourdoncle = +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" @@ -102,7 +103,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 : bb coq_function) : (B.bourdoncle * coq_N PMap.t) = +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) |