From 8dc2366431f9210ad70a789c389d9d19c6fc802f Mon Sep 17 00:00:00 2001 From: Pierre Goutagny Date: Thu, 17 Jun 2021 16:32:05 +0200 Subject: Use Tunnelinglibs in Tunnelingaux --- backend/Tunnelingaux.ml | 337 ++++++++++++------------------------------------ 1 file changed, 81 insertions(+), 256 deletions(-) (limited to 'backend') diff --git a/backend/Tunnelingaux.ml b/backend/Tunnelingaux.ml index 87e6d303..d4b88a5d 100644 --- a/backend/Tunnelingaux.ml +++ b/backend/Tunnelingaux.ml @@ -23,261 +23,86 @@ open Coqlib open LTL open Maps open Camlcoq - -let limit_tunneling = None (* for debugging: [Some x] limit the number of iterations *) -let debug_flag = ref false -let final_dump = false (* set to true to have a more verbose debugging *) - -let debug fmt = - if !debug_flag then Printf.eprintf fmt - else Printf.ifprintf stderr fmt - -exception BugOnPC of int - -(* type of labels in the cfg *) -type label = int * P.t - -(* instructions under analyzis *) -type simple_inst = (* a simplified view of LTL instructions *) - LBRANCH of node -| LCOND of node * node -| OTHER -and node = { - lab : label; - mutable inst: simple_inst; - mutable link: node; (* link in the union-find: itself for non "nop"-nodes, target of the "nop" otherwise *) - mutable dist: int; - mutable tag: int - } - -(* type of the (simplified) CFG *) -type cfg = { - nodes: (int, node) Hashtbl.t; - mutable rems: node list; (* remaining conditions that may become lbranch or not *) - mutable num_rems: int; - mutable iter_num: int (* number of iterations in elimination of conditions *) - } - -let lab_i (n: node): int = fst n.lab -let lab_p (n: node): P.t = snd n.lab - -let rec target c n = (* inspired from the "find" of union-find algorithm *) - match n.inst with - | LCOND(s1,s2) -> - if n.link != n - then update c n - else if n.tag < c.iter_num then ( - (* we try to change the condition ... *) - n.tag <- c.iter_num; (* ... but at most once by iteration *) - let ts1 = target c s1 in - let ts2 = target c s2 in - if ts1 == ts2 then (n.link <- ts1; ts1) else n - ) else n - | _ -> - if n.link != n - then update c n - else n -and update c n = - let t = target c n.link in - n.link <- t; t - -let get_node c p = - let li = P.to_int p in - try - Hashtbl.find c.nodes li - with - Not_found -> - let rec n = { lab = (li, p); inst = OTHER; link = n ; dist = 0; tag = 0 } in - Hashtbl.add c.nodes li n; - n - -let set_branch c p s = - let li = P.to_int p in - try - let n = Hashtbl.find c.nodes li in - n.inst <- LBRANCH s; - n.link <- target c s - with - Not_found -> - let n = { lab = (li,p); inst = LBRANCH s; link = target c s; dist = 0; tag = 0 } in - Hashtbl.add c.nodes li n - - -(* build [c.nodes] and accumulate in [acc] conditions at beginning of LTL basic-blocks *) -let build_simplified_cfg c acc pc bb = - match bb with - | Lbranch s :: _ -> - let ns = get_node c s in - set_branch c pc ns; - acc - | Lcond (_, _, s1, s2, _) :: _ -> - c.num_rems <- c.num_rems + 1; - let ns1 = get_node c s1 in - let ns2 = get_node c s2 in - let npc = get_node c pc in - npc.inst <- LCOND(ns1, ns2); - npc::acc - | _ -> acc - -(* try to change a condition into a branch -[acc] is the current accumulator of conditions to consider in the next iteration of repeat_change_cond -*) -let try_change_cond c acc pc = - match pc.inst with - | LCOND(s1,s2) -> - let ts1 = target c s1 in - let ts2 = target c s2 in - if ts1 == ts2 then ( - pc.link <- ts1; - c.num_rems <- c.num_rems - 1; +open Tunnelinglibs + +module LANG = struct + type code_unit = LTL.bblock + type funct = LTL.coq_function +end + +module OPT = struct + let langname = "LTL" + let limit_tunneling = None + let debug_flag = ref false + let final_dump = false +end + +module Partial = Tunnelinglibs.Tunneling(LANG)(OPT) + +module FUNS = struct + let build_simplified_cfg c acc pc bb = + match bb with + | Lbranch s :: _ -> + let ns = get_node c s in + set_branch c pc ns; acc - ) else - pc::acc - | _ -> raise (BugOnPC (lab_i pc)) (* LCOND expected *) - -(* repeat [try_change_cond] until no condition is changed into a branch *) -let rec repeat_change_cond c = - c.iter_num <- c.iter_num + 1; - debug "++ Tunneling.branch_target %d: remaining number of conds to consider = %d\n" (c.iter_num) (c.num_rems); - let old = c.num_rems in - c.rems <- List.fold_left (try_change_cond c) [] c.rems; - let curr = c.num_rems in - let continue = - match limit_tunneling with - | Some n -> curr < old && c.iter_num < n - | None -> curr < old - in - if continue - then repeat_change_cond c - - -(* compute the final distance of each nop nodes to its target *) -let undef_dist = -1 -let self_dist = undef_dist-1 -let rec dist n = - if n.dist = undef_dist - then ( - n.dist <- self_dist; (* protection against an unexpected loop in the data-structure *) - n.dist <- - (match n.inst with - | OTHER -> 0 - | LBRANCH p -> 1 + dist p - | LCOND (p1,p2) -> 1 + (max (dist p1) (dist p2))); - n.dist - ) else if n.dist=self_dist then raise (BugOnPC (lab_i n)) - else n.dist - -let final_export f c = - let count = ref 0 in - let filter_nops_init_dist _ n acc = - let tn = target c n in - if tn == n - then ( - n.dist <- 0; (* force [n] to be a base case in the recursion of [dist] *) - acc - ) else ( - n.dist <- undef_dist; (* force [dist] to compute the actual [n.dist] *) - count := !count+1; - n::acc - ) - in - let nops = Hashtbl.fold filter_nops_init_dist c.nodes [] in - let res = List.fold_left (fun acc n -> PTree.set (lab_p n) (lab_p n.link, Z.of_uint (dist n)) acc) PTree.empty nops in - debug "* Tunneling.branch_target: final number of eliminated nops = %d\n" !count; - res - -(*********************************************) -(*** START: printing and debugging functions *) - -let string_of_labeli nodes ipc = - try - let pc = Hashtbl.find nodes ipc in - if pc.link == pc - then Printf.sprintf "(Target@%d)" (dist pc) - else Printf.sprintf "(Nop %d @%d)" (lab_i pc.link) (dist pc) - with - Not_found -> "" - -let print_bblock c println (pc, bb) = - match bb with - | Lbranch s::_ -> (if println then debug "\n"); debug "%d:Lbranch %d %s\n" pc (P.to_int s) (string_of_labeli c.nodes pc); false - | Lcond (_, _, s1, s2, _)::_ -> (if println then debug "\n"); debug "%d:Lcond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (string_of_labeli c.nodes pc); false - | _ -> debug "%d " pc; true - - -let print_cfg f c = - let a = Array.of_list (PTree.fold (fun acc pc bb -> (P.to_int pc,bb)::acc) f.fn_code []) in - Array.fast_sort (fun (i1,_) (i2,_) -> i2 - i1) a; - let ep = P.to_int f.fn_entrypoint in - debug "entrypoint: %d %s\n" ep (string_of_labeli c.nodes ep); - let println = Array.fold_left (print_bblock c) false a in - (if println then debug "\n");debug "remaining cond:"; - List.iter (fun n -> debug "%d " (lab_i n)) c.rems; - debug "\n" - -(*************************************************************) -(* Copy-paste of the extracted code of the verifier *) -(* with [raise (BugOnPC (P.to_int pc))] instead of [Error.*] *) - -let get td pc = - match PTree.get pc td with - | Some p -> let (t0, d) = p in (t0, d) - | None -> (pc, Z.of_uint 0) - -let check_bblock td pc bb = - match PTree.get pc td with - | Some p -> - let (tpc, dpc) = p in - let dpc0 = dpc in - (match bb with - | [] -> - raise (BugOnPC (P.to_int pc)) - | i :: _ -> - (match i with - | Lbranch s -> - let (ts, ds) = get td s in - if peq tpc ts - then if zlt ds dpc0 - then () - else raise (BugOnPC (P.to_int pc)) - else raise (BugOnPC (P.to_int pc)) - | Lcond (_, _, s1, s2, _) -> - let (ts1, ds1) = get td s1 in - let (ts2, ds2) = get td s2 in - if peq tpc ts1 - then if peq tpc ts2 - then if zlt ds1 dpc0 - then if zlt ds2 dpc0 - then () - else raise (BugOnPC (P.to_int pc)) - else raise (BugOnPC (P.to_int pc)) - else raise (BugOnPC (P.to_int pc)) - else raise (BugOnPC (P.to_int pc)) - | _ -> - raise (BugOnPC (P.to_int pc)))) - | None -> () - -(** val check_code : coq_UF -> code -> unit res **) - -let check_code td c = - PTree.fold (fun _ pc bb -> check_bblock td pc bb) c (()) - -(*** END: copy-paste & debugging functions *******) + | Lcond (_, _, s1, s2, _) :: _ -> + c.num_rems <- c.num_rems + 1; + let ns1 = get_node c s1 in + let ns2 = get_node c s2 in + let npc = get_node c pc in + npc.inst <- COND(ns1, ns2); + npc::acc + | _ -> acc + + let print_code_unit c println (pc, bb) = + match bb with + | Lbranch s::_ -> (if println then Partial.debug "\n"); Partial.debug "%d:Lbranch %d %s\n" pc (P.to_int s) (string_of_labeli c.nodes pc); false + | Lcond (_, _, s1, s2, _)::_ -> (if println then Partial.debug "\n"); Partial.debug "%d:Lcond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (string_of_labeli c.nodes pc); false + | _ -> Partial.debug "%d " pc; true + + let fn_code f = f.fn_code + let fn_entrypoint f = f.fn_entrypoint + + + (*************************************************************) + (* Copy-paste of the extracted code of the verifier *) + (* with [raise (BugOnPC (P.to_int pc))] instead of [Error.*] *) + + let check_code_unit td pc bb = + match PTree.get pc td with + | Some p -> + let (tpc, dpc) = p in + let dpc0 = dpc in + (match bb with + | [] -> + raise (BugOnPC (P.to_int pc)) + | i :: _ -> + (match i with + | Lbranch s -> + let (ts, ds) = get td s in + if peq tpc ts + then if zlt ds dpc0 + then () + else raise (BugOnPC (P.to_int pc)) + else raise (BugOnPC (P.to_int pc)) + | Lcond (_, _, s1, s2, _) -> + let (ts1, ds1) = get td s1 in + let (ts2, ds2) = get td s2 in + if peq tpc ts1 + then if peq tpc ts2 + then if zlt ds1 dpc0 + then if zlt ds2 dpc0 + then () + else raise (BugOnPC (P.to_int pc)) + else raise (BugOnPC (P.to_int pc)) + else raise (BugOnPC (P.to_int pc)) + else raise (BugOnPC (P.to_int pc)) + | _ -> + raise (BugOnPC (P.to_int pc)))) + | None -> () +end + +module T = Partial.T(FUNS) +let branch_target = T.branch_target -let branch_target f = - debug "* Tunneling.branch_target: starting on a new function\n"; - if limit_tunneling <> None then debug "* WARNING: limit_tunneling <> None\n"; - let c = { nodes = Hashtbl.create 100; rems = []; num_rems = 0; iter_num = 0 } in - c.rems <- PTree.fold (build_simplified_cfg c) f.fn_code []; - repeat_change_cond c; - let res = final_export f c in - if !debug_flag then ( - try - check_code res f.fn_code; - if final_dump then print_cfg f c; - with e -> ( - print_cfg f c; - check_code res f.fn_code - ) - ); - res -- cgit