X-Git-Url: http://git.hcoop.net/bpt/coccinelle.git/blobdiff_plain/1be43e1299fc61538d62349ca012514b28f8734f:/engine/.%23ctlcocci_integration.ml.1.111..485bce717a659e363d3bb74bf2ff76f1cd3b0ff7:/engine/static/git-favicon.png diff --git a/engine/.#ctlcocci_integration.ml.1.111 b/engine/.#ctlcocci_integration.ml.1.111 deleted file mode 100644 index 5f736aa..0000000 --- a/engine/.#ctlcocci_integration.ml.1.111 +++ /dev/null @@ -1,422 +0,0 @@ -(* -* Copyright 2005-2008, 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 . -* -* 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_engine.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_engine.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 = - Pattern3.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. - * Indeed, à la fin de la branche then (et else), on devrait aller directement - * au suivant du endif, sinon si ecrit if(1) { foo(); }; bar(); - * sans '...' entre le if et bar(), alors ca matchera pas car le CTL - * generera un AX bar() qui il tombera d'abord sur le [endif] :( - * Mais chiant de changer l'algo de generation, marche pas tres bien avec - * ma facon de faire recursive et compositionnel. - * => faire une fonction qui applique des fixes autour de ce control flow, - * comme ca passe un bon flow a rene, mais garde un flow a moi pour pouvoir - * facilement generate back the ast. - * alt: faire un wrapper autourde mon graphe pour lui passer dans le module CFG - * une fonction qui passe a travers les Fake, mais bof. - * - * update: also make loop the deadcode nodes, the one that have - * no predecessor. - *) -let (fix_flow_ctl2: F.cflow -> F.cflow) = fun flow -> - let g = ref flow in - - let topi = F.first_node !g in - !g#add_arc ((topi, topi), F.Direct); - - (* for the #define CFG who have no Exit but have at least a EndNode *) - (try - let endi = F.find_node (fun x -> x = F.EndNode) !g in - !g#add_arc ((endi, endi), F.Direct); - with Not_found -> () - ); - - (* for the regular functions *) - (try - let exitnodei = F.find_node (fun x -> x = F.Exit) !g in - let errornodei = F.find_node (fun x -> x = F.ErrorExit) !g in - - !g#add_arc ((exitnodei, exitnodei), F.Direct); - - if null ((!g#successors errornodei)#tolist) && - null ((!g#predecessors errornodei)#tolist) - then !g#del_node errornodei - else !g#add_arc ((errornodei, errornodei), F.Direct); - with Not_found -> () - ); - - let fake_nodes = !g#nodes#tolist +> List.filter (fun (nodei, node) -> - match F.unwrap node with - | F.CaseNode _ - | F.Enter - (*| F.Fake*) (* [endif], [endswitch], ... *) - -> true - | _ -> false - ) in - - fake_nodes +> List.iter (fun (nodei, node) -> F.remove_one_node nodei !g); - - (* even when have deadcode, julia want loop over those nodes *) - !g#nodes#tolist +> List.iter (fun (nodei, node) -> - if (!g#predecessors nodei)#null - then begin - let fakei = !g#add_node (F.mk_node F.Fake [] [] "DEADCODELOOP") in - !g#add_arc ((fakei, nodei), F.Direct); - !g#add_arc ((fakei, fakei), F.Direct); - end - ); - - !g#nodes#tolist +> List.iter (fun (nodei, node) -> - assert (List.length ((!g#successors nodei)#tolist) >= 1); - (* no: && List.length ((!g#predecessors nodei)#tolist) >= 1 - because the enter node at least have no predecessors *) - ); - - !g -let fix_flow_ctl a = - Common.profile_code "fix_flow" (fun () -> fix_flow_ctl2 a) - - - - - -(*****************************************************************************) -(* subtil: the label must operate on newflow, not (old) cflow - * update: now I supposed that we give me a fixed_flow - *) -let model_for_ctl dropped_isos cflow binding = - let newflow = cflow (* old: fix_flow_ctl (control_flow_for_ctl cflow) *) in - let labels = labels_for_ctl dropped_isos (newflow#nodes#tolist) binding in - let states = List.map fst newflow#nodes#tolist in - newflow, labels, states - - -(*****************************************************************************) - -module PRED = - struct - type t = Lib_engine.predicate - let print_predicate x = - Pretty_print_cocci.print_plus_flag := false; - Pretty_print_cocci.print_minus_flag := false; - Pretty_print_engine.pp_predicate x - end - -module ENV = - struct - type value = Lib_engine.metavar_binding_kind2 - type mvar = Ast_cocci.meta_name - let eq_mvar x x' = x = x' - let eq_val v v' = - (* v = v' *) - match (v,v') with - (Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1)), - Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))) -> - ((min1 <= min2) && (max1 >= max2)) or - ((min2 <= min1) && (max2 >= max1)) - | (Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal a), - Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal b)) -> - C_vs_c.eq_type a b - | _ -> v = v' - let merge_val v v' = (* values guaranteed to be compatible *) - (* v *) - match (v,v') with - (Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1)), - Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2))) -> - if (min1 <= min2) && (max1 >= max2) - then Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min1,max1)) - else - if (min2 <= min1) && (max2 >= max1) - then Lib_engine.NormalMetaVal(Ast_c.MetaPosVal(min2,max2)) - else failwith "incompatible positions give to merge" - | (Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal a), - Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal b)) -> - Lib_engine.NormalMetaVal (Ast_c.MetaTypeVal (C_vs_c.merge_type a b)) - - | _ -> v - let print_mvar (_,s) = Format.print_string s - let print_value x = Pretty_print_engine.pp_binding_kind2 x - end - -module CFG = - struct - type node = int - type cfg = (F.node, F.edge) Ograph_extended.ograph_mutable - let predecessors cfg n = List.map fst ((cfg#predecessors n)#tolist) - let successors cfg n = List.map fst ((cfg#successors n)#tolist) - let extract_is_loop cfg n = - Control_flow_c.extract_is_loop (cfg#nodes#find n) - let print_node i = Format.print_string (i_to_s i) - let size cfg = cfg#nodes#length - end - - -module WRAPPED_ENGINE = Wrapper_ctl.CTL_ENGINE_BIS (ENV) (CFG) (PRED) - -let print_bench _ = WRAPPED_ENGINE.print_bench() - -type pred = Lib_engine.predicate * Ast_cocci.meta_name Ast_ctl.modif - -(*****************************************************************************) -let metavars_binding2_to_binding binding2 = - binding2 +> Common.map_filter (fun (s, kind2) -> - match kind2 with - | Lib_engine.NormalMetaVal kind -> Some (s, kind) - (* I thought it was Impossible to have this when called from - satbis_to_trans_info but it does not seems so *) - | Lib_engine.ParenVal _ -> None - | Lib_engine.LabelVal _ -> None - | Lib_engine.BadVal -> None (* should not occur *) - | Lib_engine.GoodVal -> None (* should not occur *) - ) - -let metavars_binding_to_binding2 binding = - binding +> List.map (fun (s, kind) -> s, Lib_engine.NormalMetaVal kind) - - -let (satbis_to_trans_info: - (nodei * Lib_engine.metavars_binding2 * Lib_engine.predicate) list -> - (nodei * Lib_engine.metavars_binding * Ast_cocci.rule_elem) list) = - fun xs -> - xs +> List.fold_left (fun prev (nodei, binding2, pred) -> - match pred with - | Lib_engine.Match (rule_elem) -> - if !Flag.track_iso_usage then show_isos rule_elem; - (nodei, metavars_binding2_to_binding binding2, rule_elem) - ::prev - (* see BindGood in asttotctl2 *) - | Lib_engine.BindGood (_) -> prev - | _ -> raise Impossible - ) [] - -(*****************************************************************************) - -let rec coalesce_positions = function - [] -> [] - | (x,Ast_c.MetaPosValList l)::rest -> - let (same,others) = List.partition (function (x1,_) -> x = x1) rest in - let ls = - List.concat - (List.map - (function - (_,Ast_c.MetaPosValList l) -> l - | _ -> failwith "unexpected non-position") - same) in - let new_ls = List.sort compare (l@ls) in - (x,Ast_c.MetaPosValList new_ls) :: coalesce_positions others - | x::rest -> x :: coalesce_positions rest - -(*****************************************************************************) -(* Call ctl engine *) -(*****************************************************************************) -let (mysat2: - Lib_engine.model -> - (Lib_engine.ctlcocci * (pred list list)) -> - (Lib_engine.mvar list*Lib_engine.metavars_binding) -> - (Lib_engine.transformation_info * bool * Lib_engine.metavars_binding list)) = - fun (flow, label, states) ctl (used_after, binding) -> - let binding2 = metavars_binding_to_binding2 binding in - let (triples,(trans_info2, returned_any_states, used_after_envs)) = - WRAPPED_ENGINE.satbis (flow, label, states) ctl (used_after, binding2) - in - if not (!Flag_parsing_cocci.sgrep_mode || !Flag.sgrep_mode2 || - !Flag_engine.allow_inconsistent_paths) - then Check_reachability.check_reachability triples flow; - let (trans_info2,used_after_fresh_envs) = - Postprocess_transinfo.process used_after binding2 trans_info2 in - let used_after_envs = - Common.uniq(List.map2 (@) used_after_fresh_envs used_after_envs) in - let trans_info = satbis_to_trans_info trans_info2 in - let newbindings = List.map metavars_binding2_to_binding used_after_envs in - let newbindings = List.map coalesce_positions newbindings in - (trans_info, returned_any_states, newbindings) - -let mysat a b c = - Common.profile_code "mysat" (fun () -> mysat2 a b c)