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