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