From 5a542d158d3bde832e38b65ad5347299fbe7ee32 Mon Sep 17 00:00:00 2001 From: Pierre Goutagny Date: Thu, 17 Jun 2021 15:58:29 +0200 Subject: Simplify tunneling factorisation The recursive module definitions required unnecessarily long expicit signatures for little added legibility. --- backend/RTLTunnelingaux.ml | 65 +++++++++++++++++----------------------------- 1 file changed, 24 insertions(+), 41 deletions(-) (limited to 'backend/RTLTunnelingaux.ml') diff --git a/backend/RTLTunnelingaux.ml b/backend/RTLTunnelingaux.ml index 5fe327d4..9333e357 100644 --- a/backend/RTLTunnelingaux.ml +++ b/backend/RTLTunnelingaux.ml @@ -26,8 +26,6 @@ open Maps open Camlcoq open Tunnelinglibs -let nopcounter = ref 0 - module LANG = struct type code_unit = RTL.instruction type funct = RTL.coq_function @@ -40,60 +38,44 @@ module OPT = struct let final_dump = false end -module rec T: sig - val get_node: cfg -> positive -> node - val set_branch: cfg -> positive -> node -> unit - val debug: ('a, out_channel, unit) format -> 'a - val string_of_labeli: ('a, node) Hashtbl.t -> 'a -> string - exception BugOnPC of int - val branch_target: RTL.coq_function -> (positive * Z.t) PTree.t - -end = Tunnelinglibs.Tunneling(LANG)(OPT)(FUNS) - -and FUNS: sig - val build_simplified_cfg: cfg -> node list -> positive -> LANG.code_unit -> node list - - val print_code_unit: cfg -> bool -> int * LANG.code_unit -> bool +module Partial = Tunnelinglibs.Tunneling(LANG)(OPT) - val fn_code: LANG.funct -> LANG.code_unit PTree.t - val fn_entrypoint: LANG.funct -> positive - - val check_code_unit: (positive * integer) PTree.t -> positive -> LANG.code_unit -> unit -end = struct +module FUNS = struct let build_simplified_cfg c acc pc i = match i with | Inop s -> - let ns = T.get_node c s in - T.set_branch c pc ns; + let ns = get_node c s in + set_branch c pc ns; incr nopcounter; acc | Icond (_, _, s1, s2, _) -> c.num_rems <- c.num_rems + 1; - let ns1 = T.get_node c s1 in - let ns2 = T.get_node c s2 in - let npc = T.get_node c pc in + 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, i) = match i with - | Inop s -> (if println then T.debug "\n"); T.debug "%d:Inop %d %s\n" pc (P.to_int s) (T.string_of_labeli c.nodes pc); false - | Icond (_, _, s1, s2, _) -> (if println then T.debug "\n"); T.debug "%d:Icond (%d,%d) %s\n" pc (P.to_int s1) (P.to_int s2) (T.string_of_labeli c.nodes pc); false - | _ -> T.debug "%d " pc; true + | Inop s -> (if println then Partial.debug "\n"); + Partial.debug "%d:Inop %d %s\n" pc (P.to_int s) (string_of_labeli c.nodes pc); + false + | Icond (_, _, s1, s2, _) -> (if println then Partial.debug "\n"); + Partial.debug "%d:Icond (%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 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_code_unit td pc i = match PTree.get pc td with | Some p -> @@ -105,8 +87,8 @@ end = struct if peq tpc ts then if zlt ds dpc0 then () - else raise (T.BugOnPC (P.to_int pc)) - else raise (T.BugOnPC (P.to_int pc)) + else raise (BugOnPC (P.to_int pc)) + else raise (BugOnPC (P.to_int pc)) | Icond (_, _, s1, s2, _) -> let (ts1, ds1) = get td s1 in let (ts2, ds2) = get td s2 in @@ -115,15 +97,16 @@ end = struct then if zlt ds1 dpc0 then if zlt ds2 dpc0 then () - else raise (T.BugOnPC (P.to_int pc)) - else raise (T.BugOnPC (P.to_int pc)) - else raise (T.BugOnPC (P.to_int pc)) - else raise (T.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)) + else raise (BugOnPC (P.to_int pc)) | _ -> - raise (T.BugOnPC (P.to_int pc)) end + raise (BugOnPC (P.to_int pc)) end | None -> () end +module T = Partial.T(FUNS) let branch_target = T.branch_target -- cgit