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