From 540fbd2e6d63c1be0dd520499132c134f5b0f8b3 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 16 Apr 2020 23:18:26 +0200 Subject: moved to extra --- backend/LICMaux.ml | 25 +++++++++---------------- 1 file changed, 9 insertions(+), 16 deletions(-) (limited to 'backend/LICMaux.ml') diff --git a/backend/LICMaux.ml b/backend/LICMaux.ml index 3f7d61b1..96214054 100644 --- a/backend/LICMaux.ml +++ b/backend/LICMaux.ml @@ -1,31 +1,24 @@ open RTL;; open Camlcoq;; open Maps;; -open Integers;; type reg = P.t;; -module IntSet = Set.Make(struct type t=int let compare = (-) end);; - -let loop_headers (f : coq_function) = - PTree.fold (fun (already : IntSet.t) - (coq_pc : node) (instr : instruction) -> - let pc = P.to_int coq_pc in - List.fold_left (fun (already : IntSet.t) (coq_pc' : node) -> - let pc' = P.to_int coq_pc' in - if pc' >= pc - then IntSet.add pc' already - else already) already (successors_instr instr)) - f.fn_code IntSet.empty;; +let loop_headers (f : coq_function) : RTL.node list = + List.map fst (List.filter snd (PTree.elements (Duplicateaux.get_loop_headers f.fn_code f.fn_entrypoint)));; let print_loop_headers f = print_endline "Loop headers"; - IntSet.iter - (fun i -> Printf.printf "%d " i) + List.iter + (fun i -> Printf.printf "%d " (P.to_int i)) (loop_headers f); print_newline ();; let gen_injections (f : coq_function) (coq_max_pc : node) (coq_max_reg : reg): - (Inject.inj_instr list) PTree.t = + (Inject.inj_instr list) PTree.t = + let _ = print_loop_headers f in + PTree.empty;; +(* let max_reg = P.to_int coq_max_reg in PTree.set coq_max_pc [Inject.INJload(AST.Mint32, (Op.Aindexed (Ptrofs.of_int (Z.of_sint 0))), [P.of_int 1], P.of_int (max_reg+1))] PTree.empty;; + *) -- cgit