engine/check_reachability.ml

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