Release coccinelle-0.2.4

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

(*
 * Copyright 2010, INRIA, University of Copenhagen
 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
 * 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.
 *)


(*
 * Copyright 2010, INRIA, University of Copenhagen
 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
 * 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 (Lib_engine.Absolute 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 (Lib_engine.Absolute labels)))]))])
      | Lib_engine.PrefixLabel s, _ ->
          let labels = F.extract_labels node in
          [(nodei,
	    (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Prefix labels)))]))]

      | 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.LoopFallThrough, F.LoopFallThroughNode -> [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.LoopFallThrough, _ -> []
      | 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.