| 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 | * |
| 25 | * Wrapping for FUNCTORS and MODULES |
| 26 | * |
| 27 | * |
| 28 | * $Id: wrapper_ctl.ml,v 1.67 2007/11/20 12:57:25 julia Exp $ |
| 29 | * |
| 30 | * **********************************************************************) |
| 31 | |
| 32 | type info = int |
| 33 | |
| 34 | type ('pred, 'mvar) wrapped_ctl = |
| 35 | ('pred * 'mvar Ast_ctl.modif, 'mvar, info) Ast_ctl.generic_ctl |
| 36 | |
| 37 | type ('value, 'pred) wrapped_binding = |
| 38 | | ClassicVal of 'value |
| 39 | | PredVal of 'pred Ast_ctl.modif |
| 40 | |
| 41 | type ('pred,'state,'mvar,'value) labelfunc = |
| 42 | 'pred -> |
| 43 | ('state * ('pred * ('mvar, 'value) Ast_ctl.generic_substitution)) list |
| 44 | |
| 45 | (* pad: what is 'wit ? *) |
| 46 | type ('pred,'state,'mvar,'value,'wit) wrapped_labelfunc = |
| 47 | ('pred * 'mvar Ast_ctl.modif) -> |
| 48 | ('state * |
| 49 | ('mvar,('value,'pred) wrapped_binding) Ast_ctl.generic_substitution * |
| 50 | 'wit |
| 51 | ) list |
| 52 | |
| 53 | (* ********************************************************************** *) |
| 54 | (* Module type: CTL_ENGINE_BIS (wrapper for CTL_ENGINE) *) |
| 55 | (* ********************************************************************** *) |
| 56 | |
| 57 | (* This module must convert the labelling function passed as parameter, by |
| 58 | using convert_label. Then create a SUBST2 module handling the |
| 59 | wrapped_binding. Then it can instantiates the generic CTL_ENGINE |
| 60 | module. Call sat. And then process the witness tree to remove all that |
| 61 | is not revelevant for the transformation phase. |
| 62 | *) |
| 63 | |
| 64 | module CTL_ENGINE_BIS = |
| 65 | functor (SUB : Ctl_engine.SUBST) -> |
| 66 | functor (G : Ctl_engine.GRAPH) -> |
| 67 | functor(P : Ctl_engine.PREDICATE) -> |
| 68 | struct |
| 69 | |
| 70 | exception TODO_CTL of string (* implementation still not quite done so... *) |
| 71 | exception NEVER_CTL of string (* Some things should never happen *) |
| 72 | |
| 73 | module A = Ast_ctl |
| 74 | |
| 75 | type predicate = P.t |
| 76 | module WRAPPER_ENV = |
| 77 | struct |
| 78 | type mvar = SUB.mvar |
| 79 | type value = (SUB.value,predicate) wrapped_binding |
| 80 | let eq_mvar = SUB.eq_mvar |
| 81 | let eq_val wv1 wv2 = |
| 82 | match (wv1,wv2) with |
| 83 | | (ClassicVal(v1),ClassicVal(v2)) -> SUB.eq_val v1 v2 |
| 84 | | (PredVal(v1),PredVal(v2)) -> v1 = v2 (* FIX ME: ok? *) |
| 85 | | _ -> false |
| 86 | let merge_val wv1 wv2 = |
| 87 | match (wv1,wv2) with |
| 88 | | (ClassicVal(v1),ClassicVal(v2)) -> ClassicVal(SUB.merge_val v1 v2) |
| 89 | | _ -> wv1 (* FIX ME: ok? *) |
| 90 | |
| 91 | |
| 92 | let print_mvar x = SUB.print_mvar x |
| 93 | let print_value x = |
| 94 | match x with |
| 95 | ClassicVal v -> SUB.print_value v |
| 96 | | PredVal(A.Modif v) -> P.print_predicate v |
| 97 | | PredVal(A.UnModif v) -> P.print_predicate v |
| 98 | | PredVal(A.Control) -> Format.print_string "no value" |
| 99 | end |
| 100 | |
| 101 | module WRAPPER_PRED = |
| 102 | struct |
| 103 | type t = P.t * SUB.mvar Ast_ctl.modif |
| 104 | let print_predicate (pred, modif) = |
| 105 | begin |
| 106 | P.print_predicate pred; |
| 107 | (match modif with |
| 108 | Ast_ctl.Modif x | Ast_ctl.UnModif x -> |
| 109 | Format.print_string " with <modifTODO>" |
| 110 | | Ast_ctl.Control -> ()) |
| 111 | end |
| 112 | end |
| 113 | |
| 114 | (* Instantiate a wrapped version of CTL_ENGINE *) |
| 115 | module WRAPPER_ENGINE = |
| 116 | Ctl_engine.CTL_ENGINE (WRAPPER_ENV) (G) (WRAPPER_PRED) |
| 117 | |
| 118 | (* Wrap a label function *) |
| 119 | let (wrap_label: ('pred,'state,'mvar,'value) labelfunc -> |
| 120 | ('pred,'state,'mvar,'value,'wit) wrapped_labelfunc) = |
| 121 | fun oldlabelfunc -> |
| 122 | fun (p, predvar) -> |
| 123 | |
| 124 | let penv p' = |
| 125 | match predvar with |
| 126 | | A.Modif(x) -> [A.Subst(x,PredVal(A.Modif(p')))] |
| 127 | | A.UnModif(x) -> [A.Subst(x,PredVal(A.UnModif(p')))] |
| 128 | | A.Control -> [] in |
| 129 | |
| 130 | let conv_sub sub = |
| 131 | match sub with |
| 132 | | A.Subst(x,v) -> A.Subst(x,ClassicVal(v)) |
| 133 | | A.NegSubst(x,v) -> A.NegSubst(x,ClassicVal(v)) in |
| 134 | |
| 135 | let conv_trip (s,(p',env)) = |
| 136 | (s,penv p' @ (List.map conv_sub env),[](*pad: ?*)) |
| 137 | in |
| 138 | List.map conv_trip (oldlabelfunc p) |
| 139 | |
| 140 | (* ---------------------------------------------------------------- *) |
| 141 | |
| 142 | (* FIX ME: what about negative witnesses and negative substitutions *) |
| 143 | let unwrap_wits modifonly wits = |
| 144 | let mkth th = |
| 145 | Common.map_filter |
| 146 | (function A.Subst(x,ClassicVal(v)) -> Some (x,v) | _ -> None) |
| 147 | th in |
| 148 | let rec loop neg acc = function |
| 149 | A.Wit(st,[A.Subst(x,PredVal(A.Modif(v)))],anno,wit) -> |
| 150 | (match wit with |
| 151 | [] -> [(st,acc,v)] |
| 152 | | _ -> raise (NEVER_CTL "predvar tree should have no children")) |
| 153 | | A.Wit(st,[A.Subst(x,PredVal(A.UnModif(v)))],anno,wit) |
| 154 | when not modifonly or !Flag.track_iso_usage -> |
| 155 | (match wit with |
| 156 | [] -> [(st,acc,v)] |
| 157 | | _ -> raise (NEVER_CTL "predvar tree should have no children")) |
| 158 | | A.Wit(st,th,anno,wit) -> |
| 159 | List.concat (List.map (loop neg ((mkth th) @ acc)) wit) |
| 160 | | A.NegWit(_) -> [] (* why not failure? *) in |
| 161 | List.concat (List.map (function wit -> loop false [] wit) wits) |
| 162 | ;; |
| 163 | |
| 164 | (* |
| 165 | (* a match can return many trees, but within each tree, there has to be |
| 166 | at most one value for each variable that is in the used_after list *) |
| 167 | let collect_used_after used_after envs = |
| 168 | let print_var var = SUB.print_mvar var; Format.print_flush() in |
| 169 | List.concat |
| 170 | (List.map |
| 171 | (function used_after_var -> |
| 172 | let vl = |
| 173 | List.fold_left |
| 174 | (function rest -> |
| 175 | function env -> |
| 176 | try |
| 177 | let vl = List.assoc used_after_var env in |
| 178 | match rest with |
| 179 | None -> Some vl |
| 180 | | Some old_vl when SUB.eq_val vl old_vl -> rest |
| 181 | | Some old_vl -> print_var used_after_var; |
| 182 | Format.print_newline(); |
| 183 | SUB.print_value old_vl; |
| 184 | Format.print_newline(); |
| 185 | SUB.print_value vl; |
| 186 | Format.print_newline(); |
| 187 | failwith "incompatible values" |
| 188 | with Not_found -> rest) |
| 189 | None envs in |
| 190 | match vl with |
| 191 | None -> [] |
| 192 | | Some vl -> [(used_after_var, vl)]) |
| 193 | used_after) |
| 194 | *) |
| 195 | |
| 196 | (* a match can return many trees, but within each tree, there has to be |
| 197 | at most one value for each variable that is in the used_after list *) |
| 198 | (* actually, this should always be the case, because these variables |
| 199 | should be quantified at the top level. so the more complicated |
| 200 | definition above should not be needed. *) |
| 201 | let collect_used_after used_after envs = |
| 202 | List.concat |
| 203 | (List.map |
| 204 | (function used_after_var -> |
| 205 | let vl = |
| 206 | List.fold_left |
| 207 | (function rest -> |
| 208 | function env -> |
| 209 | try |
| 210 | let vl = List.assoc used_after_var env in |
| 211 | if List.exists (function x -> SUB.eq_val x vl) rest |
| 212 | then rest |
| 213 | else vl::rest |
| 214 | with Not_found -> rest) |
| 215 | [] envs in |
| 216 | List.map (function x -> (used_after_var, x)) vl) |
| 217 | used_after) |
| 218 | |
| 219 | (* ----------------------------------------------------- *) |
| 220 | |
| 221 | (* The wrapper for sat from the CTL_ENGINE *) |
| 222 | let satbis_noclean (grp,lab,states) (phi,reqopt) : |
| 223 | ('pred,'anno) WRAPPER_ENGINE.triples = |
| 224 | WRAPPER_ENGINE.sat (grp,wrap_label lab,states) phi reqopt |
| 225 | |
| 226 | (* Returns the "cleaned up" result from satbis_noclean *) |
| 227 | let (satbis : |
| 228 | G.cfg * |
| 229 | (predicate,G.node,SUB.mvar,SUB.value) labelfunc * |
| 230 | G.node list -> |
| 231 | ((predicate,SUB.mvar) wrapped_ctl * |
| 232 | (WRAPPER_PRED.t list list)) -> |
| 233 | (WRAPPER_ENV.mvar list * (SUB.mvar * SUB.value) list) -> |
| 234 | ((WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples * |
| 235 | ((G.node * (SUB.mvar * SUB.value) list * predicate) |
| 236 | list list * |
| 237 | bool * |
| 238 | (WRAPPER_ENV.mvar * SUB.value) list list))) = |
| 239 | fun m phi (used_after, binding) -> |
| 240 | let noclean = satbis_noclean m phi in |
| 241 | let witness_trees = List.map (fun (_,_,w) -> w) noclean in |
| 242 | let res = List.map (unwrap_wits true) witness_trees in |
| 243 | let new_bindings = |
| 244 | List.map |
| 245 | (function bindings_per_witness_tree -> |
| 246 | (List.map (function (_,env,_) -> env) bindings_per_witness_tree)) |
| 247 | (List.map (unwrap_wits false) witness_trees) in |
| 248 | (noclean, |
| 249 | (res,not(noclean = []), |
| 250 | (* throw in the old binding. By construction it doesn't conflict |
| 251 | with any of the new things, and it is useful if there are no new |
| 252 | things. *) |
| 253 | (List.map (collect_used_after used_after) new_bindings))) |
| 254 | |
| 255 | let print_bench _ = WRAPPER_ENGINE.print_bench() |
| 256 | |
| 257 | (* END OF MODULE: CTL_ENGINE_BIS *) |
| 258 | end |