| 1 | (* |
| 2 | * Copyright 2005-2008, Ecole des Mines de Nantes, University of Copenhagen |
| 3 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller |
| 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 | end |
| 148 | |
| 149 | module ENGINE = Ctl_engine.CTL_ENGINE (ENV) (CFG) (PRED) |
| 150 | |
| 151 | let test_formula state formula cfg = |
| 152 | let label = function |
| 153 | Node pred -> [(pred,[],[])] |
| 154 | | After -> |
| 155 | List.concat |
| 156 | (List.map |
| 157 | (fun (nodei, node) -> |
| 158 | match Control_flow_c.unwrap node with |
| 159 | Control_flow_c.AfterNode -> [(nodei,[],[])] |
| 160 | | _ -> []) |
| 161 | cfg#nodes#tolist) in |
| 162 | let verbose = !Flag_ctl.verbose_ctl_engine in |
| 163 | let pm = !Flag_ctl.partial_match in |
| 164 | Flag_ctl.verbose_ctl_engine := false; |
| 165 | Flag_ctl.partial_match := false; |
| 166 | let res = |
| 167 | ENGINE.sat (cfg,label,List.map fst cfg#nodes#tolist) |
| 168 | (CTL.And(CTL.NONSTRICT,CTL.Pred(Node(state)),formula)) |
| 169 | [[Node(state)]] in |
| 170 | Flag_ctl.verbose_ctl_engine := verbose; |
| 171 | Flag_ctl.partial_match := pm; |
| 172 | match res with [] -> false | _ -> true |
| 173 | |
| 174 | (* ---------------------------------------------------------------- *) |
| 175 | (* Entry point *) |
| 176 | |
| 177 | (* The argument is a list of triples with a node name, an empty environment |
| 178 | and a witness tree *) |
| 179 | |
| 180 | type witness = |
| 181 | (Ograph_extended.nodei, unit, |
| 182 | (Ograph_extended.nodei, unit, unit) Ast_ctl.generic_ctl list) |
| 183 | Ast_ctl.generic_witnesstree |
| 184 | |
| 185 | type ('a,'b,'c,'d,'e) triples = |
| 186 | (Ograph_extended.nodei * 'a * |
| 187 | (Ograph_extended.nodei, |
| 188 | ('b, ('c, 'd) Wrapper_ctl.wrapped_binding) CTL.generic_subst list, 'e) |
| 189 | CTL.generic_witnesstree list) list |
| 190 | |
| 191 | let check_reachability triples cfg = |
| 192 | Hashtbl.clear modified; |
| 193 | List.iter build_modified triples; |
| 194 | let formulas = create_formulas() in |
| 195 | List.iter |
| 196 | (function (node,af_formula,ef_formula) -> |
| 197 | if test_formula node af_formula cfg |
| 198 | then |
| 199 | if test_formula node ef_formula cfg |
| 200 | then |
| 201 | Printf.printf "warning: node %d may be inconsistently modified\n" |
| 202 | node |
| 203 | else () |
| 204 | else |
| 205 | failwith |
| 206 | (Printf.sprintf |
| 207 | "node %d reachable by inconsistent control-flow paths" node)) |
| 208 | formulas |