diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_smt.ml | 35 | ||||
| -rw-r--r-- | src/jib/jib_ssa.ml | 118 | ||||
| -rw-r--r-- | src/jib/jib_ssa.mli | 13 |
3 files changed, 112 insertions, 54 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 350f50d9..de5feca1 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1343,6 +1343,19 @@ let rmw_modify smt = function end | _ -> assert false +let smt_terminator ctx = + let open Jib_ssa in + function + | T_end id -> + add_event ctx Return (Var (zencode_name id)); + [] + + | T_match_failure -> + add_pathcond_event ctx Match; + [] + + | T_undefined _ | T_goto _ | T_jump _ | T_label _ | T_none -> [] + (* For a basic block (contained in a control-flow node / cfnode), we turn the instructions into a sequence of define-const and declare-const expressions. Because we are working with a SSA graph, @@ -1421,21 +1434,11 @@ let smt_instr ctx = end; [declare_const ctx id ctyp] - | I_aux (I_end id, _) -> - add_event ctx Return (Var (zencode_name id)); - [] - | I_aux (I_clear _, _) -> [] - | I_aux (I_match_failure, _) -> - add_pathcond_event ctx Match; - [] - - | I_aux (I_undefined ctyp, _) -> [] - - (* I_jump and I_goto will only appear as terminators for basic blocks. *) - | I_aux ((I_jump _ | I_goto _), _) -> [] - + (* Should only appear as terminators for basic blocks. *) + | I_aux ((I_jump _ | I_goto _ | I_end _ | I_match_failure | I_undefined _), (_, l)) -> + Reporting.unreachable l __POS__ "SMT: Instruction should only appear as block terminator" | instr -> failwith ("Cannot translate: " ^ Pretty_print_sail.to_string (pp_instr instr)) @@ -1451,9 +1454,11 @@ let smt_cfnode all_cdefs ctx ssanodes = | _ -> declare_const ctx id ctyp in smt_reg_decs @ List.map smt_start (NameMap.bindings inits) - | CF_block instrs -> + | CF_block (instrs, terminator) -> let ctx = { ctx with pathcond = get_pathcond ctx ssanodes } in - List.concat (List.map (smt_instr ctx) instrs) + let smt_instrs = List.map (smt_instr ctx) instrs in + let smt_term = smt_terminator ctx terminator in + List.concat (smt_instrs @ [smt_term]) (* We can ignore any non basic-block/start control-flow nodes *) | _ -> [] diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml index a4a77f9d..dfacf90a 100644 --- a/src/jib/jib_ssa.ml +++ b/src/jib/jib_ssa.ml @@ -53,6 +53,7 @@ open Jib open Jib_util module IntSet = Set.Make(struct type t = int let compare = compare end) +module IntMap = Map.Make(struct type t = int let compare = compare end) (**************************************************************************) (* 1. Mutable graph type *) @@ -60,12 +61,16 @@ module IntSet = Set.Make(struct type t = int let compare = compare end) type 'a array_graph = { mutable next : int; - mutable nodes : ('a * IntSet.t * IntSet.t) option array + mutable nodes : ('a * IntSet.t * IntSet.t) option array; + mutable next_cond : int; + mutable conds : cval IntMap.t } let make ~initial_size () = { next = 0; - nodes = Array.make initial_size None + nodes = Array.make initial_size None; + next_cond = 1; + conds = IntMap.empty } let get_vertex graph n = graph.nodes.(n) @@ -77,6 +82,12 @@ let iter_graph f graph = | None -> () done +let add_cond cval graph = + let n = graph.next_cond in + graph.conds <- IntMap.add n cval graph.conds; + graph.next_cond <- n + 1; + n + (** Add a vertex to a graph, returning the node index *) let add_vertex data graph = let n = graph.next in @@ -187,12 +198,32 @@ let prune visited graph = (* 2. Mutable control flow graph *) (**************************************************************************) +type terminator = + | T_undefined of ctyp + | T_match_failure + | T_end of name + | T_goto of string + | T_jump of int * string + | T_label of string + | T_none + type cf_node = | CF_label of string - | CF_block of instr list - | CF_guard of cval + | CF_block of instr list * terminator + | CF_guard of int | CF_start of ctyp NameMap.t +let to_terminator graph = function + | I_label label -> T_label label + | I_goto label -> T_goto label + | I_jump (cval, label) -> + let n = add_cond cval graph in + T_jump (n, label) + | I_end name -> T_end name + | I_match_failure -> T_match_failure + | I_undefined ctyp -> T_undefined ctyp + | _ -> assert false + (* For now we only generate CFGs for flat lists of instructions *) let control_flow_graph instrs = let module StringMap = Map.Make(String) in @@ -209,46 +240,42 @@ let control_flow_graph instrs = let cf_split (I_aux (aux, _)) = match aux with - | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end _ | I_match_failure | I_undefined _ -> true + | I_label _ | I_goto _ | I_jump _ | I_end _ | I_match_failure | I_undefined _ -> true | _ -> false in let rec cfg preds instrs = let before, after = instr_split_at cf_split instrs in - let last = match after with - | I_aux (I_label _, _) :: _ -> [] - | instr :: _ -> [instr] - | _ -> [] + let terminator, after = match after with + | I_aux (instr, _) :: after -> to_terminator graph instr, after + | [] -> T_none, [] in - let preds = match before @ last with - | [] -> preds - | instrs -> - let n = add_vertex ([], CF_block instrs) graph in + let preds = match before, terminator with + | [], (T_none | T_label _) -> preds + | instrs, _ -> + let n = add_vertex ([], CF_block (instrs, terminator)) graph in List.iter (fun p -> add_edge p n graph) preds; [n] in - match after with - | I_aux ((I_end _ | I_match_failure | I_undefined _), _) :: after -> + match terminator with + | T_end _ | T_match_failure | T_undefined _ -> cfg [] after - | I_aux (I_goto label, _) :: after -> + | T_goto label -> List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds; cfg [] after - | I_aux (I_jump (cval, label), _) :: after -> - let t = add_vertex ([], CF_guard cval) graph in - let f = add_vertex ([], CF_guard (V_call (Bnot, [cval]))) graph in + | T_jump (cond, label) -> + let t = add_vertex ([], CF_guard cond) graph in + let f = add_vertex ([], CF_guard (- cond)) graph in List.iter (fun p -> add_edge p t graph; add_edge p f graph) preds; add_edge t (StringMap.find label !labels) graph; cfg [f] after - | I_aux (I_label label, _) :: after -> + | T_label label -> cfg (StringMap.find label !labels :: preds) after - | I_aux (_, (_, l)) :: after -> - Reporting.unreachable l __POS__ "Could not add instruction to control-flow graph" - - | [] -> preds + | T_none -> preds in let start = add_vertex ([], CF_start NameMap.empty) graph in @@ -422,7 +449,7 @@ let place_phi_functions graph df = let orig_A n = match graph.nodes.(n) with - | Some ((_, CF_block instrs), _, _) -> + | Some ((_, CF_block (instrs, _)), _, _) -> let vars = List.fold_left NameCTSet.union NameCTSet.empty (List.map instr_typed_writes instrs) in let vars = NameCTSet.diff vars (all_decls instrs) in all_vars := NameCTSet.union vars !all_vars; @@ -542,21 +569,32 @@ let rename_variables graph root children = counts := NameMap.add id i !counts; push_stack id i; I_init (ctyp, ssa_name i id, cval) - | I_jump (cval, label) -> - I_jump (fold_cval cval, label) - | I_end id -> - let i = top_stack id in - I_end (ssa_name i id) | instr -> instr in I_aux (aux, annot) in + let ssa_terminator = function + | T_jump (cond, label) -> + begin match IntMap.find_opt cond graph.conds with + | Some cval -> + graph.conds <- IntMap.add cond (fold_cval cval) graph.conds; + T_jump (cond, label) + | None -> assert false + end + | T_end id -> + let i = top_stack id in + T_end (ssa_name i id) + | terminator -> terminator + in + let ssa_cfnode = function | CF_start inits -> CF_start inits - | CF_block instrs -> CF_block (List.map ssa_instr instrs) + | CF_block (instrs, terminator) -> + let instrs = List.map ssa_instr instrs in + CF_block (instrs, ssa_terminator terminator) | CF_label label -> CF_label label - | CF_guard cval -> CF_guard (fold_cval cval) + | CF_guard cond -> CF_guard cond in let ssa_ssanode = function @@ -612,13 +650,19 @@ let rename_variables graph root children = let place_pi_functions graph start idom children = let get_guard = function - | CF_guard guard -> [guard] + | CF_guard cond -> + begin match IntMap.find_opt (abs cond) graph.conds with + | Some guard when cond > 0 -> [guard] + | Some guard -> [V_call (Bnot, [guard])] + | None -> assert false + end | _ -> [] in let get_pi_contents ssanodes = List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes) in + (* let rec between_dom p n = if n = p then [] @@ -634,13 +678,13 @@ let place_pi_functions graph start idom children = | _, pred -> pred end | None -> assert false - in + in *) let rec go n = begin match graph.nodes.(n) with | Some ((ssa, cfnode), preds, succs) -> let p = idom.(n) in - let bd = between_dom p n in + let bd = [] (* between_dom p n *) in if p <> -1 then begin match graph.nodes.(p) with | Some ((dom_ssa, _), _, _) -> @@ -699,9 +743,9 @@ let string_of_phis = function let string_of_node = function | (phis, CF_label label) -> string_of_phis phis ^ label - | (phis, CF_block instrs) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs + | (phis, CF_block (instrs, terminator)) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs | (phis, CF_start inits) -> string_of_phis phis ^ "START" - | (phis, CF_guard cval) -> string_of_phis phis ^ (String.escaped (Pretty_print_sail.to_string (pp_cval cval))) + | (phis, CF_guard cval) -> string_of_phis phis ^ string_of_int cval let vertex_color = function | (_, CF_start _) -> "peachpuff" diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli index 759e1ccb..72cf1a1e 100644 --- a/src/jib/jib_ssa.mli +++ b/src/jib/jib_ssa.mli @@ -77,10 +77,19 @@ exception Not_a_DAG of int val topsort : 'a array_graph -> int list +type terminator = + | T_undefined of Jib.ctyp + | T_match_failure + | T_end of Jib.name + | T_goto of string + | T_jump of int * string + | T_label of string + | T_none + type cf_node = | CF_label of string - | CF_block of Jib.instr list - | CF_guard of Jib.cval + | CF_block of Jib.instr list * terminator + | CF_guard of int | CF_start of Jib.ctyp NameMap.t val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) array_graph |