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