-(*
-* 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 <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
| Lib_engine.Paren _, _ -> []
| Lib_engine.Label s, _ ->
let labels = F.extract_labels node in
- [(nodei, (p,[(s --> (Lib_engine.LabelVal labels))]))]
+ [(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 labels))]))])
+ [(nodei,
+ (p,[(s -->
+ (Lib_engine.LabelVal (Lib_engine.Absolute 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))]))
- )
+ [(nodei,
+ (p,[(s --> (Lib_engine.LabelVal (Lib_engine.Prefix labels)))]))]
| Lib_engine.Match (re), _unwrapnode ->
let substs =
| 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.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, _ -> []
(* 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
+ 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
+ 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);
Pretty_print_engine.pp_predicate x
end
+(* prefix has to be nonempty *)
+let prefix l1 l2 =
+ let rec loop = function
+ ([],_) -> true
+ | (_,[]) -> false
+ | (x::xs,y::ys) when x = y -> loop (xs,ys)
+ | _ -> false in
+ loop(l1,l2)
+
+let compatible_labels l1 l2 =
+ match (l1,l2) with
+ (Lib_engine.Absolute(l1),Lib_engine.Absolute(l2)) -> l1 =*= l2
+ | (Lib_engine.Absolute(l1),Lib_engine.Prefix(l2)) -> prefix l1 l2
+ | (Lib_engine.Prefix(l1),Lib_engine.Absolute(l2)) -> prefix l2 l1
+ | (Lib_engine.Prefix(l1),Lib_engine.Prefix(l2)) ->
+ not (l1 = []) && not (l2 = []) &&
+ List.hd l1 =*= List.hd l2 (* labels are never empty *)
+
+let merge_labels l1 l2 =
+ match (l1,l2) with
+ (* known to be compatible *)
+ (Lib_engine.Absolute(_),Lib_engine.Absolute(_)) -> l1
+ | (Lib_engine.Absolute(_),Lib_engine.Prefix(_)) -> l1
+ | (Lib_engine.Prefix(_),Lib_engine.Absolute(_)) -> l2
+ | (Lib_engine.Prefix(l1),Lib_engine.Prefix(l2)) ->
+ let rec max_prefix = function
+ (x::xs,y::ys) when x = y -> x::(max_prefix(xs,ys))
+ | (l1,l2) -> [] in
+ Lib_engine.Prefix(max_prefix(l1,l2))
+
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_mvar x x' = x =*= x'
let eq_val v v' =
(* v = v' *)
match (v,v') with
| (Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal a),
Lib_engine.NormalMetaVal(Ast_c.MetaTypeVal b)) ->
C_vs_c.eq_type a b
- | _ -> v = v'
+ | (Lib_engine.LabelVal(l1),Lib_engine.LabelVal(l2)) ->
+ compatible_labels l1 l2
+ | _ -> v =*= v'
let merge_val v v' = (* values guaranteed to be compatible *)
(* v *)
match (v,v') with
| (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))
+ | (Lib_engine.LabelVal(l1),Lib_engine.LabelVal(l2)) ->
+ Lib_engine.LabelVal(merge_labels l1 l2)
| _ -> v
let print_mvar (_,s) = Format.print_string s
let (satbis_to_trans_info:
- (nodei * Lib_engine.metavars_binding2 * Lib_engine.predicate) list ->
- (nodei * Lib_engine.metavars_binding * Ast_cocci.rule_elem) list) =
+ (int list *
+ (nodei * Lib_engine.metavars_binding2 * Lib_engine.predicate)) list ->
+ (int 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
+ xs +> List.fold_left (fun prev (index,(nodei, binding2, pred)) ->
+ match pred with
+ | Lib_engine.Match (rule_elem) ->
+ if !Flag.track_iso_usage then show_isos rule_elem;
+ (index,
+ (nodei, metavars_binding2_to_binding binding2, rule_elem))
+ ::prev
(* see BindGood in asttotctl2 *)
- | Lib_engine.BindGood (_) -> prev
- | _ -> raise Impossible
- ) []
+ | 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 (same,others) = List.partition (function (x1,_) -> x =*= x1) rest in
let ls =
List.concat
(List.map
(x,Ast_c.MetaPosValList new_ls) :: coalesce_positions others
| x::rest -> x :: coalesce_positions rest
+let strip env =
+ List.map
+ (function (v,vl) ->
+ let vl =
+ match vl with
+ Ast_c.MetaExprVal a ->
+ Ast_c.MetaExprVal(Lib_parsing_c.al_inh_expr a)
+ | Ast_c.MetaExprListVal a ->
+ Ast_c.MetaExprListVal(Lib_parsing_c.al_inh_arguments a)
+ | Ast_c.MetaStmtVal a ->
+ Ast_c.MetaStmtVal(Lib_parsing_c.al_inh_statement a)
+ | Ast_c.MetaInitVal a ->
+ Ast_c.MetaInitVal(Lib_parsing_c.al_inh_init a)
+ | x -> (*don't contain binding info*) x in
+ (v,vl))
+ env
+
+let rec nub ls =
+ match ls with
+ [] -> []
+ | (x::xs) when (List.mem x xs) -> nub xs
+ | (x::xs) -> x::(nub xs)
+
(*****************************************************************************)
(* Call ctl engine *)
(*****************************************************************************)
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 *
- Lib_engine.metavars_binding list)) =
+ (Lib_engine.numbered_transformation_info * bool *
+ Lib_engine.metavars_binding * 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)
+ WRAPPED_ENGINE.satbis (flow, label, states) ctl
+ (used_after, binding2)
in
if not (!Flag_parsing_cocci.sgrep_mode || !Flag.sgrep_mode2 ||
!Flag_matcher.allow_inconsistent_paths)
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
+ let newbindings = List.map strip newbindings in
+ let newbindings = nub newbindings in
(trans_info, returned_any_states, binding, newbindings)
let mysat a b c =
HCoop / bpt / coccinelle.git / blobdiff