plugins/cfg/stackify.ml

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 open Why3
  13 open Cfg_ast
  14 open Ptree
  15
  16 (* Todo use labeled graph *)
  17 module G = Graph.Imperative.Digraph.Concrete (struct
  18   type t = label
  19
  20   let equal a b = a.id_str = b.id_str
  21   let compare a b = String.compare a.id_str b.id_str
  22   let hash a = Hashtbl.hash a.id_str
  23 end)
  24
  25 module Dom = Graph.Dominator.Make (G)
  26 module Topo = Graph.WeakTopological.Make (G)
  27
  28 let rec targets (t : cfg_term) : label list =
  29   match t.cfg_term_desc with
  30   | CFGgoto l -> [ l ]
  31   | CFGswitch (_, brs) -> List.fold_left (fun acc (_, a) -> targets a @ acc) [] brs
  32   | CFGreturn _ -> []
  33   | CFGabsurd -> []
  34
  35 type labeled_block = label * block
  36 type usage = Multi | One
  37
  38 type exp_tree =
  39   | Scope of label * usage * exp_tree * exp_tree
  40   | Loop of (loop_clause * ident option * Ptree.term * int option ref) list * exp_tree
  41   | Block of labeled_block
  42
  43 let rec _print_exp_structure' exp =
  44   match exp with
  45   | Scope (lbl, _, tgt, exp) ->
  46       Format.printf "Scope( %s = " lbl.id_str;
  47       _print_exp_structure' tgt;
  48       Format.printf " in ";
  49       _print_exp_structure' exp;
  50       Format.printf ")"
  51   | Loop (_, exp) ->
  52       Format.printf "Loop[  ";
  53       _print_exp_structure' exp;
  54       Format.printf "]"
  55   | Block (l, _) -> Format.printf "Block(%s)" l.id_str
  56
  57 let graph_from_blocks (bl : (label * block) list) : G.t =
  58   let g = G.create () in
  59   List.iter
  60     (fun (source, (_, t)) ->
  61       let target_label = targets t in
  62       G.add_vertex g source;
  63       List.iter (fun target -> G.add_edge g source target) target_label)
  64     bl;
  65   g
  66
  67 exception NotReducible of (string * string)
  68 exception NotConnected of G.V.t list
  69
  70 let () =
  71   Exn_printer.register (fun fmt exn ->
  72       match exn with
  73       | NotReducible (n1, n2) ->
  74           Format.fprintf fmt "CFG is not a reducible graph. The nodes %s %s belong to a cycle with multiple entries" n1
  75             n2
  76       | NotConnected s ->
  77           Format.fprintf fmt
  78             "CFG is not a connected graph. The following nodes are not reachable from the start block: ";
  79           List.iter (fun el -> Format.printf "%s" el.id_str) s
  80       | _ -> raise exn)
  81
  82 module Sint = Extset.Make (struct
  83   type t = label
  84
  85   let compare a b = String.compare a.id_str b.id_str
  86 end)
  87
  88 let _graph_is_reducible (g : G.t) (dom : G.V.t -> G.V.t -> bool) (entry : label) =
  89   let visited = ref Sint.empty in
  90   let to_visit = Stack.create () in
  91   Stack.push entry to_visit;
  92
  93   while not (Stack.is_empty to_visit) do
  94     let node = Stack.pop to_visit in
  95     visited := Sint.add node !visited;
  96
  97     G.iter_succ
  98       (fun succ ->
  99         if not (Sint.mem succ !visited) then Stack.push succ to_visit
 100         else if (* back-edge *)
 101                 not (dom succ node) then raise (NotReducible (succ.id_str, node.id_str)))
 102       g node
 103   done;
 104   (* graph is connected *)
 105   let unreached = G.fold_vertex (fun v u -> if not (Sint.mem v !visited) then Sint.add v u else u) g Sint.empty in
 106   if not (Sint.is_empty unreached) then raise (NotConnected (Sint.elements unreached));
 107   ()
 108
 109 let rec entry e = match e with Block b -> b | Loop (_, h) -> entry h | Scope (_, _, _, h) -> entry h
 110 (* unused | _ -> assert false *)
 111
 112 let mk_scope label usage tgt body = Scope (label, usage, tgt, body)
 113
 114 let rec treeify_from_components pred dom (prev : exp_tree option) blocks (wto : label Graph.WeakTopological.t) :
 115     exp_tree =
 116   Option.get
 117     (Graph.WeakTopological.fold_left
 118        (fun prev c ->
 119          let e = treeify_component pred dom blocks c in
 120          let lbl = fst (entry e) in
 121          let forward_preds = List.filter (fun pred -> not (dom lbl pred)) (pred lbl) in
 122          let usage = if List.length forward_preds > 1 then Multi else One in
 123          match prev with Some prev -> Some (mk_scope lbl usage e prev) | None -> Some e)
 124        prev wto)
 125
 126 and treeify_component pred dom blocks (wto : label Graph.WeakTopological.element) : exp_tree =
 127   let open Graph.WeakTopological in
 128   match wto with
 129   | Vertex b -> Block (List.find (fun (l, _) -> l.id_str = b.id_str) blocks)
 130   | Component (v, b) ->
 131       let rec split_invariants = function
 132         | { cfg_instr_desc = CFGinvariant is } :: xs ->
 133             let invs, stmts = split_invariants xs in
 134             (is @ invs, stmts)
 135         | [] -> ([], [])
 136         | a -> ([], a)
 137       in
 138       let l, (s, t) = List.find (fun (l, _) -> l.id_str = v.id_str) blocks in
 139       let invariants, stmts = split_invariants s in
 140
 141       Loop (invariants, treeify_from_components pred dom (Some (Block (l, (stmts, t)))) blocks b)
 142
 143 and treeify pred dom cs = treeify_from_components pred dom None cs
 144
 145 let stackify (bl : labeled_block list) (entry : label) : exp_tree =
 146   let g = graph_from_blocks bl in
 147   let idom = Dom.compute_idom g entry in
 148   let dom = Dom.idom_to_dom idom in
 149
 150   (* graph_is_reducible g dom entry; *)
 151   let comps = Topo.recursive_scc g entry in
 152   let t = treeify (G.pred g) dom bl comps in
 153   t