engine/check_reachability.ml

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