engine/check_reachability.ml

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