engine/check_reachability.ml

   1 (*
   2  * Copyright 2012, INRIA
   3  * Julia Lawall, Gilles Muller
   4  * Copyright 2010-2011, INRIA, University of Copenhagen
   5  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
   6  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
   7  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
   8  * This file is part of Coccinelle.
   9  *
  10  * Coccinelle is free software: you can redistribute it and/or modify
  11  * it under the terms of the GNU General Public License as published by
  12  * the Free Software Foundation, according to version 2 of the License.
  13  *
  14  * Coccinelle is distributed in the hope that it will be useful,
  15  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  16  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  17  * GNU General Public License for more details.
  18  *
  19  * You should have received a copy of the GNU General Public License
  20  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  21  *
  22  * The authors reserve the right to distribute this or future versions of
  23  * Coccinelle under other licenses.
  24  *)
  25
  26
  27 # 0 "./check_reachability.ml"
  28 (* ---------------------------------------------------------------- *)
  29 (* code to check for ambiguities *)
  30
  31 (* Idea: for each node that is said to be modified in any witness tree, we
  32   check that all backward paths end up at the root of some witness tree
  33   that says that the node should be modified.  We then give a warning, if
  34   the node itself appears more than once in such a path, because then there
  35   could be some instances that are modified and some that are not.  An
  36   example is as follows:
  37
  38   f(); ... g(); ... - h();
  39
  40   with C code: f(); while(E) { h(); g(); } g(); h();
  41
  42   Then the h() in the while loop matches both the first ... and the - h();
  43
  44   Concretely, if a node 47 is in the witness tree rooted at 1 and the
  45   witness tree rooted at 2, then we give an error if 47 is not in the set
  46   of nodes satisfying AF[1v2] and give a warning if 47 is in the set of
  47   nodes satisfying EXEF(47 & EXEF(1v2)). (Note that the root of a witness
  48   tree here is the node causing the pattern to match; there might not be
  49   any witnesses associated with this node.)
  50
  51   Another try on the exists formula:
  52   !(1v2) & EXE[!(1v2) U 47]
  53   The first !(1v2) is to discard immediately cases where the beginning and
  54   end of the path are the same.  Afterwards, it would only seem necessary to
  55   serach up to the next occurrence of 47 (leaf), ensuring that there are not
  56   1s or 2s (starting points) along the way.  Then the second 47 would be in
  57   the path, but possible not transformed.
  58  *)
  59
  60 module G = Ograph_extended
  61 module CTL = Ast_ctl
  62
  63 (* Step 1: for each tree, make a mapping from the modified nodes to the root
  64 of the tree *)
  65
  66 let modified = (Hashtbl.create(25) : (G.nodei, G.nodei list ref) Hashtbl.t)
  67
  68 let build_modified (n,_,wits) =
  69   let rec loop = function
  70       CTL.Wit(st,[CTL.Subst(x,Wrapper_ctl.PredVal(CTL.Modif(v)))],anno,wit) ->
  71         let cell =
  72           try Hashtbl.find modified st
  73           with Not_found ->
  74             let cell = ref [] in Hashtbl.add modified st cell; cell in
  75         cell := n :: !cell;
  76         List.iter loop wit
  77     |   CTL.Wit(st,_,anno,wit) -> List.iter loop wit
  78     |   CTL.NegWit(wit) -> () in
  79   List.iter loop wits
  80
  81 (* Step 2: For each node in the hash table, create the error and warning
  82    formulas *)
  83
  84 type 'a nodes = Node of 'a | After
  85
  86 let create_formulas _ =
  87   Hashtbl.fold
  88     (function node ->
  89       function roots ->
  90         function acc ->
  91           (*let exef f =
  92             wrap
  93               (Ast_ctl.EX
  94                  (Ast_ctl.BACKWARD,wrap(Ast_ctl.EF(Ast_ctl.BACKWARD,f)))) in*)
  95           let match_node = Ast_ctl.Pred(Node(node)) in
  96           let match_roots =
  97             List.map (function n -> Ast_ctl.Pred(Node(n)))
  98               (List.sort compare !roots) in
  99           let or_roots =
 100             List.fold_left
 101               (function prev -> function cur -> Ast_ctl.Or(prev,cur))
 102               (List.hd match_roots) (List.tl match_roots) in
 103           (* no point to search if no path, and the presence of after
 104              in the AF formula can make things slow *)
 105           if List.mem node !roots
 106           then acc
 107           else
 108             (node,
 109              Ast_ctl.AF(Ast_ctl.BACKWARD,Ast_ctl.NONSTRICT,
 110                         Ast_ctl.Or(or_roots,Ast_ctl.Pred(After))),
 111              Ast_ctl.And
 112                (Ast_ctl.NONSTRICT,
 113                 Ast_ctl.Not(or_roots),
 114                 Ast_ctl.EX
 115                   (Ast_ctl.BACKWARD,
 116                    Ast_ctl.EU(Ast_ctl.BACKWARD,or_roots,match_node))))
 117            (*exef
 118               (wrap(Ast_ctl.And(Ast_ctl.NONSTRICT,match_node,exef(roots))))*)
 119           :: acc)
 120     modified []
 121
 122 (* Step 3: check the formula on the control-flow graph *)
 123
 124 module PRED =
 125   struct
 126     type t = Ograph_extended.nodei nodes
 127     let print_predicate = function
 128         After -> Format.print_string "after"
 129       | Node x -> Format.print_string (string_of_int x)
 130   end
 131
 132 module ENV =
 133   struct
 134     type value = unit
 135     type mvar = unit
 136     let eq_mvar x x'   = failwith "should not be invoked"
 137     let eq_val v v'    = failwith "should not be invoked"
 138     let merge_val v v' = failwith "should not be invoked"
 139
 140     let print_mvar s   = failwith "should not be invoked"
 141     let print_value x  = failwith "should not be invoked"
 142   end
 143
 144
 145 module CFG =
 146   struct
 147     type node = Ograph_extended.nodei
 148     type cfg =
 149         (Control_flow_c.node, Control_flow_c.edge)
 150           Ograph_extended.ograph_mutable
 151     let predecessors cfg n = List.map fst ((cfg#predecessors n)#tolist)
 152     let successors   cfg n = List.map fst ((cfg#successors n)#tolist)
 153     let extract_is_loop cfg n =
 154       Control_flow_c.extract_is_loop (cfg#nodes#find n)
 155     let print_node i = Format.print_string (string_of_int i)
 156     let size cfg = cfg#nodes#length
 157     let print_graph cfg label border_nodes fill_nodes filename = ()
 158   end
 159
 160 module ENGINE = Ctl_engine.CTL_ENGINE (ENV) (CFG) (PRED)
 161
 162 let test_formula state formula cfg =
 163     let label = function
 164         Node pred -> [(pred,[],[])]
 165       | After ->
 166           List.concat
 167             (List.map
 168                (fun (nodei, node) ->
 169                  match Control_flow_c.unwrap node with
 170                    Control_flow_c.AfterNode -> [(nodei,[],[])]
 171                  | _ -> [])
 172                cfg#nodes#tolist) in
 173     let verbose = !Flag_ctl.verbose_ctl_engine in
 174     let pm = !Flag_ctl.partial_match in
 175 (*     let gt = !Flag_ctl.graphical_trace in *)
 176     Flag_ctl.verbose_ctl_engine := false;
 177     Flag_ctl.partial_match := false;
 178     Flag_ctl.checking_reachability := true;
 179 (*     Flag_ctl.graphical_trace := ""; *)
 180     let res =
 181       ENGINE.sat (cfg,label,List.map fst cfg#nodes#tolist)
 182         (CTL.And(CTL.NONSTRICT,CTL.Pred(Node(state)),formula))
 183         [[Node(state)]] in
 184     Flag_ctl.verbose_ctl_engine := verbose;
 185     Flag_ctl.partial_match := pm;
 186     Flag_ctl.checking_reachability := false;
 187 (*     Flag_ctl.graphical_trace := gt; *)
 188     match res with [] -> false | _ -> true
 189
 190 (* ---------------------------------------------------------------- *)
 191 (* Entry point *)
 192
 193 (* The argument is a list of triples with a node name, an empty environment
 194 and a witness tree *)
 195
 196 type witness =
 197     (Ograph_extended.nodei, unit,
 198      (Ograph_extended.nodei, unit, unit) Ast_ctl.generic_ctl list)
 199       Ast_ctl.generic_witnesstree
 200
 201 type ('a,'b,'c,'d,'e) triples =
 202     (Ograph_extended.nodei * 'a *
 203      (Ograph_extended.nodei,
 204       ('b, ('c, 'd) Wrapper_ctl.wrapped_binding) CTL.generic_subst list, 'e)
 205      CTL.generic_witnesstree list) list
 206
 207 let check_reachability rulename triples cfg =
 208   Hashtbl.clear modified;
 209   List.iter build_modified triples;
 210   let formulas = create_formulas() in
 211   List.iter
 212     (function (node,af_formula,ef_formula) ->
 213       if test_formula node af_formula cfg
 214       then
 215         if test_formula node ef_formula cfg
 216         then
 217           let n = cfg#nodes#find node in
 218           Printf.printf
 219             "warning: %s, node %d: %s in %s may be inconsistently modified\n"
 220             rulename node (snd n) !Flag.current_element
 221         else ()
 222       else
 223         let n = cfg#nodes#find node in
 224         failwith
 225           (Printf.sprintf
 226              "%s: node %d: %s in %s reachable by inconsistent control-flow paths"
 227              rulename node (snd n) !Flag.current_element))
 228     formulas