Release coccinelle-0.1.8

[bpt/coccinelle.git] / engine / ctlcocci_integration.ml

(*
* Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
* Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
* This file is part of Coccinelle.
* 
* Coccinelle is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, according to version 2 of the License.
* 
* Coccinelle is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
* GNU General Public License for more details.
* 
* You should have received a copy of the GNU General Public License
* along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
* 
* The authors reserve the right to distribute this or future versions of
* Coccinelle under other licenses.
*)


open Common

open Ograph_extended

module F = Control_flow_c

(*****************************************************************************)
(* Debugging functions *)
(*****************************************************************************)
let show_or_not_predicate pred = 
  if !Flag_matcher.debug_engine then begin 
    indent_do (fun () -> 
      adjust_pp_with_indent_and_header "labeling: pred = " (fun () -> 
        Pretty_print_engine.pp_predicate pred;
      );
    )
  end

let show_or_not_nodes nodes =
  if !Flag_matcher.debug_engine  then begin 
    indent_do (fun () -> 
      adjust_pp_with_indent_and_header "labeling: result = " (fun () -> 
        Common.pp_do_in_box (fun () -> 
          pp "{";
          Common.print_between 
            (fun () -> pp ";"; Format.print_cut())
            (fun (nodei, (_predTODO, subst)) -> 
              Format.print_int nodei;
              Common.pp_do_in_box (fun () -> 
                Pretty_print_engine.pp_binding2_ctlsubst subst
              )
            ) nodes;
          pp "}";
        );
      )
    )
  end

let show_isos rule_elem =
  match Ast_cocci.get_isos rule_elem with
    [] -> ()
  | isos ->
      let line = Ast_cocci.get_line rule_elem in
      Printf.printf "rule elem: ";
      Pretty_print_cocci.rule_elem "" rule_elem;
      Format.print_newline();
      List.iter
	(function (nm,x) ->
	  Printf.printf "    iso: %s(%d): " nm line;
	  Pretty_print_cocci.pp_print_anything x;
	  Format.print_newline())
	isos

(*****************************************************************************)
(* Labeling function *)
(*****************************************************************************)
let (-->) x v = Ast_ctl.Subst (x,v);;

(* Take list of predicate and for each predicate returns where in the
 * control flow it matches, and the set of subsitutions for this match. 
 *)
let (labels_for_ctl: string list (* dropped isos *) ->
 (nodei * F.node) list -> Lib_engine.metavars_binding -> 
 Lib_engine.label_ctlcocci) =
  fun dropped_isos nodes binding ->

   (fun p -> 
     show_or_not_predicate p;

     let nodes' = nodes +> List.map (fun (nodei, node) -> 
      (* todo? put part of this code in pattern ? *)
      (match p, F.unwrap node with
      | Lib_engine.Paren s,  (F.SeqStart (_, bracelevel, _)) -> 
	  let make_var x = ("",i_to_s x) in
          [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))]
      | Lib_engine.Paren s,  (F.SeqEnd (bracelevel, _)) -> 
	  let make_var x = ("",i_to_s x) in
          [(nodei, (p,[(s --> (Lib_engine.ParenVal (make_var bracelevel)))]))]
      | Lib_engine.Paren _, _ -> []
      | Lib_engine.Label s, _ -> 
          let labels = F.extract_labels node in
          [(nodei, (p,[(s --> (Lib_engine.LabelVal labels))]))]
      | Lib_engine.BCLabel s, _ -> 
	  (match F.extract_bclabels node with
	    [] -> [] (* null for all nodes that are not break or continue *)
	  | labels ->
              [(nodei, (p,[(s --> (Lib_engine.LabelVal labels))]))])
      | Lib_engine.PrefixLabel s, _ -> 
          let labels = F.extract_labels node in
          let prefixes = Common.inits labels +> Common.tail in
          prefixes +> List.map (fun prefixlabels -> 
            (nodei, (p,[(s --> (Lib_engine.LabelVal prefixlabels))]))
          )

      | Lib_engine.Match (re), _unwrapnode -> 
          let substs = 
            Pattern_c.match_re_node dropped_isos re node binding
            +> List.map (fun (re', subst) -> 
              Lib_engine.Match (re'), subst
            )
          in
          substs +> List.map (fun (p', subst) -> 
            (nodei, 
              (p', 
                subst +> List.map (fun (s, meta) -> 
                  s --> Lib_engine.NormalMetaVal meta
                ))))

      | Lib_engine.InLoop,      F.InLoopNode ->  [nodei, (p,[])]
      | Lib_engine.TrueBranch , F.TrueNode ->  [nodei, (p,[])]
      | Lib_engine.FalseBranch, F.FalseNode -> [nodei, (p,[])]
      | Lib_engine.After,       F.AfterNode -> [nodei, (p,[])]
      | Lib_engine.FallThrough, F.FallThroughNode -> [nodei,(p,[])]
      | Lib_engine.FunHeader,   F.FunHeader _ -> [nodei, (p,[])]
      | Lib_engine.Top,         F.TopNode ->   [nodei, (p,[])]
      | Lib_engine.Exit,        F.Exit ->      [nodei, (p,[])]
      | Lib_engine.ErrorExit,   F.ErrorExit -> [nodei, (p,[])]
      |	Lib_engine.Goto,        F.Goto(_,_,_) -> [nodei, (p,[])]

      | Lib_engine.InLoop , _ -> []
      | Lib_engine.TrueBranch , _ -> []
      | Lib_engine.FalseBranch, _ -> []
      | Lib_engine.After, _ -> []
      | Lib_engine.FallThrough, _ -> []
      | Lib_engine.FunHeader, _  -> []
      | Lib_engine.Top, _  -> []
      | Lib_engine.Exit, _  -> []
      | Lib_engine.ErrorExit, _  -> []
      | Lib_engine.Goto, _  -> []

      |	Lib_engine.BindGood s, _ -> [(nodei, (p,[(s --> Lib_engine.GoodVal)]))]
      |	Lib_engine.BindBad s, _ ->  [(nodei, (p,[(s --> Lib_engine.BadVal)]))]
      |	Lib_engine.FakeBrace, _ ->
	  if F.extract_is_fake node then [nodei, (p,[])] else []

      | Lib_engine.Return, node -> 
          (match node with
            (* todo? should match the Exit code ? 
             * todo: one day try also to match the special function
             * such as panic(); 
             *)
          | F.Return _ ->  [nodei, (p,[])]
          | F.ReturnExpr _ -> [nodei, (p,[])]
          | _ -> []
          )
      )
     ) +> List.concat
     in

     show_or_not_nodes nodes';
     nodes'
   ) 

(*****************************************************************************)
(* Some fix flow, for CTL, for unparse *)
(*****************************************************************************)
(* could erase info on nodes, and edge, because they are not used by rene *)
let (control_flow_for_ctl: F.cflow -> ('a, 'b) ograph_mutable) = 
 fun cflow -> cflow



(* Just make the final node of the control flow loop over itself. 
 * It seems that one hypothesis of the SAT algorithm is that each node as at
 * least a successor.
 * 
 * update: do same for errorexit node.
 * 
 * update: also erase the fake nodes (and adjust the edges accordingly), 
 * so that AX in CTL can now work.