(*
-* 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.
-*)
+ * 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.
+ *)
(* for MINUS and CONTEXT, pos is always None in this file *)
(* true = don't see all matched nodes, only modified ones *)
let onlyModif = ref true(*false*)
-type ex = Exists | Forall | ReverseForall
+type ex = Exists | Forall
let exists = ref Forall
module Ast = Ast_cocci
let warning s = Printf.fprintf stderr "warning: %s\n" s
type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif
-type formula =
- (cocci_predicate,Ast.meta_name, Wrapper_ctl.info) Ast_ctl.generic_ctl
+type formula = Lib_engine.ctlcocci
+type top_formula = NONDECL of Lib_engine.ctlcocci | CODE of Lib_engine.ctlcocci
let union = Common.union_set
let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1
let ctl_seqor x y =
match (x,y) with
- (CTL.True,_) | (_,CTL.True) -> CTL.True
+ (* drop x or true case because x might have side effects *)
+ (CTL.True,_) (* | (_,CTL.True) *) -> CTL.True
| (CTL.False,a) | (a,CTL.False) -> a
| _ -> CTL.SeqOr(x,y)
match !exists with
Exists -> CTL.EX(CTL.FORWARD,x)
| Forall -> CTL.AX(CTL.FORWARD,s,x)
- | ReverseForall -> failwith "not supported"
let ctl_ax_absolute s = function
CTL.True -> CTL.True
match (x,!exists) with
(CTL.True,Exists) -> CTL.EF(CTL.FORWARD,y)
| (CTL.True,Forall) -> CTL.AF(CTL.FORWARD,s,y)
- | (CTL.True,ReverseForall) -> failwith "not supported"
| (_,Exists) -> CTL.EU(CTL.FORWARD,x,y)
| (_,Forall) -> CTL.AU(CTL.FORWARD,s,x,y)
- | (_,ReverseForall) -> failwith "not supported"
let ctl_anti_au s x y = (* only for ..., where the quantifier is changed *)
CTL.XX
(match (x,!exists) with
(CTL.True,Exists) -> CTL.AF(CTL.FORWARD,s,y)
| (CTL.True,Forall) -> CTL.EF(CTL.FORWARD,y)
- | (CTL.True,ReverseForall) -> failwith "not supported"
| (_,Exists) -> CTL.AU(CTL.FORWARD,s,x,y)
- | (_,Forall) -> CTL.EU(CTL.FORWARD,x,y)
- | (_,ReverseForall) -> failwith "not supported")
+ | (_,Forall) -> CTL.EU(CTL.FORWARD,x,y))
let ctl_uncheck = function
CTL.True -> CTL.True
used := true;
CTL.Pred(Lib_engine.BCLabel(label_var),CTL.Control)
-let predmaker guard pred label =
- ctl_and (guard_to_strict guard) (CTL.Pred pred) (label_pred_maker label)
+(* label used to be used here, but it is not used; label is only needed after
+and within dots *)
+let predmaker guard pred label = CTL.Pred pred
let aftpred = predmaker false (Lib_engine.After, CTL.Control)
let retpred = predmaker false (Lib_engine.Return, CTL.Control)
let truepred = predmaker false (Lib_engine.TrueBranch, CTL.Control)
let falsepred = predmaker false (Lib_engine.FalseBranch, CTL.Control)
let fallpred = predmaker false (Lib_engine.FallThrough, CTL.Control)
+let loopfallpred = predmaker false (Lib_engine.LoopFallThrough, CTL.Control)
-let aftret label_var f = ctl_or (aftpred label_var) (exitpred label_var)
+(*let aftret label_var =
+ ctl_or (aftpred label_var)
+ (ctl_or (loopfallpred label_var) (exitpred label_var))*)
let letctr = ref 0
let get_let_ctr _ =
| (Ast.Dots(_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
d0::s::d1::rest)
- | (Ast.Nest(_,_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
- d0::s::d1::rest) ->
+ | (Ast.Nest(_,_,_,_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)
+ ::urest,
+ d0::s::d1::rest) -> (* why no case for nest as u? *)
let l = Ast.get_line stm in
let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in
let new_rest2 = dots_list urest rest in
Ast.inherited = inh_both;
Ast.saved_witness = saved_both}]
- | ([Ast.Nest(_,_,_,_,_);Ast.OptStm(stm)],[d1;_]) ->
+ | ([Ast.Nest(_,_,_,_,_,_,_);Ast.OptStm(stm)],[d1;_]) ->
let l = Ast.get_line stm in
let rw = Ast.rewrap stm in
let rwd = Ast.rewrap stm in
Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l)
| Ast.CIRCLES(l) -> failwith "elimopt: not supported"
| Ast.STARS(l) -> failwith "elimopt: not supported") in
-
+
V.rebuilder
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- donothing donothing stmtdotsfn donothing
+ donothing donothing stmtdotsfn donothing donothing
donothing donothing donothing donothing donothing donothing donothing
donothing donothing donothing donothing donothing
let option_default = false in
let mcode r (_,_,kind,metapos) =
match kind with
- Ast.MINUS(_,_) -> true
- | Ast.PLUS -> failwith "not possible"
+ Ast.MINUS(_,_,_,_) -> true
+ | Ast.PLUS _ -> failwith "not possible"
| Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
let do_nothing r k e = k e in
let rule_elem r k re =
let res = k re in
match Ast.unwrap re with
Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
- bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
- | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
+ bind (mcode r ((),(),bef,[])) res
+ | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res
+ | _ -> res in
+ let init r k i =
+ let res = k i in
+ match Ast.unwrap i with
+ Ast.StrInitList(allminus,_,_,_,_) -> allminus or res
| _ -> res in
let recursor =
V.combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- do_nothing do_nothing do_nothing do_nothing
- do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
+ do_nothing do_nothing do_nothing do_nothing do_nothing
+ do_nothing do_nothing do_nothing do_nothing init do_nothing
do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
recursor.V.combiner_rule_elem
let contains_pos =
let bind x y = x or y in
let option_default = false in
- let mcode r (_,_,kind,metapos) =
- match metapos with
- Ast.MetaPos(_,_,_,_,_) -> true
- | Ast.NoMetaPos -> false in
+ let mcode r (_,_,kind,metapos) = not (metapos = []) in
let do_nothing r k e = k e in
let rule_elem r k re =
let res = k re in
match Ast.unwrap re with
Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
- bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
- | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
+ bind (mcode r ((),(),bef,[])) res
+ | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res
| _ -> res in
let recursor =
V.combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- do_nothing do_nothing do_nothing do_nothing
+ do_nothing do_nothing do_nothing do_nothing do_nothing
do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
recursor.V.combiner_rule_elem
| _ -> CTL.Exists(true,v,predmaker guard (matcher,CTL.UnModif v) label))
let make_raw_match label guard code =
- predmaker guard (Lib_engine.Match(code),CTL.Control) label
-
+ match intersect !used_after (Ast.get_fvs code) with
+ [] -> predmaker guard (Lib_engine.Match(code),CTL.Control) label
+ | _ ->
+ let v = fresh_var() in
+ CTL.Exists(true,v,predmaker guard (Lib_engine.Match(code),CTL.UnModif v)
+ label)
+
let rec seq_fvs quantified = function
[] -> []
| fv1::fvs ->
let option_default = 0 in
let stmt_count r k s =
match Ast.unwrap s with
- Ast.Seq(_,_,_,_) | Ast.FunDecl(_,_,_,_,_) -> (k s) + 1
+ Ast.Seq(_,_,_) | Ast.FunDecl(_,_,_,_) -> (k s) + 1
| _ -> k s in
let donothing r k e = k e in
let mcode r x = 0 in
let recursor = V.combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- donothing donothing donothing donothing
+ donothing donothing donothing donothing donothing
donothing donothing donothing donothing donothing donothing
donothing donothing stmt_count donothing donothing donothing in
let res = string_of_int (recursor.V.combiner_statement s) in
match Ast.unwrap s with
Ast.Dots(d,w,_,aft) ->
(Ast.rewrap s (Ast.Dots(d,get_before_whencode w,a,aft)),a)
- | Ast.Nest(stmt_dots,w,multi,_,aft) ->
+ | Ast.Nest(starter,stmt_dots,ender,w,multi,_,aft) ->
let w = get_before_whencode w in
let (sd,_) = get_before stmt_dots a in
- let a =
+ (*let a =
+ got rid of this, don't want to let nests overshoot
List.filter
(function
Ast.Other a ->
Unify_ast.MAYBE -> false
| _ -> true)
| _ -> true)
- a in
- (Ast.rewrap s (Ast.Nest(sd,w,multi,a,aft)),[Ast.Other_dots stmt_dots])
+ a in*)
+ (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,a,aft)),
+ [Ast.Other_dots stmt_dots])
| Ast.Disj(stmt_dots_list) ->
let (dsl,dsla) =
List.split (List.map (function e -> get_before e a) stmt_dots_list) in
(match Ast.unwrap ast with
Ast.MetaStmt(_,_,_,_) -> (s,[])
| _ -> (s,[Ast.Other s]))
- | Ast.Seq(lbrace,decls,body,rbrace) ->
+ | Ast.Seq(lbrace,body,rbrace) ->
let index = count_nested_braces s in
- let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in
- let (bd,_) = get_before body dea in
- (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
- [Ast.WParen(rbrace,index)])
+ let (bd,_) = get_before body [Ast.WParen(lbrace,index)] in
+ (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)),[Ast.WParen(rbrace,index)])
| Ast.Define(header,body) ->
let (body,_) = get_before body [] in
(Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s])
| Ast.Iterator(header,body,aft) ->
let (bd,_) = get_before_e body [] in
(Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
- | Ast.Switch(header,lb,cases,rb) ->
+ | Ast.Switch(header,lb,decls,cases,rb) ->
+ let index = count_nested_braces s in
+ let (de,dea) = get_before decls [Ast.WParen(lb,index)] in
let cases =
List.map
(function case_line ->
Ast.rewrap case_line (Ast.CaseLine(header,body))
| Ast.OptCase(case_line) -> failwith "not supported")
cases in
- (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
- | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
- let (de,dea) = get_before decls [] in
- let (bd,_) = get_before body dea in
- (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
+ (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)),
+ [Ast.WParen(rb,index)])
+ | Ast.FunDecl(header,lbrace,body,rbrace) ->
+ let (bd,_) = get_before body [] in
+ (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[])
| _ ->
Pretty_print_cocci.statement "" s; Format.print_newline();
failwith "get_before_e: not supported"
match Ast.unwrap s with
Ast.Dots(d,w,bef,_) ->
(Ast.rewrap s (Ast.Dots(d,get_after_whencode a w,bef,a)),a)
- | Ast.Nest(stmt_dots,w,multi,bef,_) ->
+ | Ast.Nest(starter,stmt_dots,ender,w,multi,bef,_) ->
let w = get_after_whencode a w in
let (sd,_) = get_after stmt_dots a in
- let a =
+ (*let a =
+ got rid of this. don't want to let nests overshoot
List.filter
(function
Ast.Other a ->
Unify_ast.MAYBE -> false
| _ -> true)
| _ -> true)
- a in
- (Ast.rewrap s (Ast.Nest(sd,w,multi,bef,a)),[Ast.Other_dots stmt_dots])
+ a in*)
+ (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,bef,a)),
+ [Ast.Other_dots stmt_dots])
| Ast.Disj(stmt_dots_list) ->
let (dsl,dsla) =
List.split (List.map (function e -> get_after e a) stmt_dots_list) in
(function
Ast.Other x ->
(match Ast.unwrap x with
- Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
+ Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) ->
failwith
"dots/nest not allowed before and after stmt metavar"
| _ -> ())
(match Ast.undots x with
x::_ ->
(match Ast.unwrap x with
- Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_) ->
+ Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) ->
failwith
("dots/nest not allowed before and after stmt "^
"metavar")
(Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots a,i)))),[])
| Ast.MetaStmt(_,_,_,_) -> (s,[])
| _ -> (s,[Ast.Other s]))
- | Ast.Seq(lbrace,decls,body,rbrace) ->
+ | Ast.Seq(lbrace,body,rbrace) ->
let index = count_nested_braces s in
- let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in
- let (de,_) = get_after decls bda in
- (Ast.rewrap s (Ast.Seq(lbrace,de,bd,rbrace)),
+ let (bd,_) = get_after body [Ast.WParen(rbrace,index)] in
+ (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)),
[Ast.WParen(lbrace,index)])
| Ast.Define(header,body) ->
let (body,_) = get_after body a in
| Ast.Iterator(header,body,aft) ->
let (bd,_) = get_after_e body a in
(Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])
- | Ast.Switch(header,lb,cases,rb) ->
+ | Ast.Switch(header,lb,decls,cases,rb) ->
+ let index = count_nested_braces s in
let cases =
List.map
(function case_line ->
match Ast.unwrap case_line with
Ast.CaseLine(header,body) ->
- let (body,_) = get_after body [] in
+ let (body,_) = get_after body [Ast.WParen(rb,index)] in
Ast.rewrap case_line (Ast.CaseLine(header,body))
| Ast.OptCase(case_line) -> failwith "not supported")
cases in
- (Ast.rewrap s (Ast.Switch(header,lb,cases,rb)),[Ast.Other s])
- | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
- let (bd,bda) = get_after body [] in
- let (de,_) = get_after decls bda in
- (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,bd,rbrace)),[])
+ let (de,_) = get_after decls [] in
+ (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)),[Ast.WParen(lb,index)])
+ | Ast.FunDecl(header,lbrace,body,rbrace) ->
+ let (bd,_) = get_after body [] in
+ (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[])
| _ -> failwith "get_after_e: not supported"
let preprocess_dots sl =
let rec suffixes = function
[] -> []
| x::xs -> xs::(suffixes xs) in
- let prefixes = List.rev (suffixes (List.rev guard_matches)) in
+ let prefixes =
+ (* normally, we check that an expression does not match something
+ earlier in the disjunction (calculated as prefixes). But for large
+ disjunctions, this can result in a very big CTL formula. So we
+ give the user the option to say he doesn't want this feature, if that is
+ the case. *)
+ if !Flag_matcher.no_safe_expressions
+ then List.map (function _ -> []) matches
+ else List.rev (suffixes (List.rev guard_matches)) in
let info = (* not null *)
List.map2
(function matcher ->
let stmt_fvs = Ast.get_fvs x in
let fvs = get_unquantified quantified stmt_fvs in
quantify guard fvs (make_match None guard x) in
- ctl_and CTL.NONSTRICT (label_pred_maker label)
+(* label used to be used here, but it is not use; label is only needed after
+and within dots
+ ctl_and CTL.NONSTRICT (label_pred_maker label) *)
(match List.map Ast.unwrap res with
[] -> failwith "unexpected empty disj"
| Ast.Exp(e)::rest -> exptymatch res make_match make_guard_match
if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false)
all
then failwith "unexpected exp or ty";
- List.fold_left ctl_seqor CTL.False
- (List.rev (List.map make_match res)))
+ List.fold_left ctl_seqor CTL.False (List.map make_match res))
(* code might be a DisjRuleElem, in which case we break it apart
code doesn't contain an Exp or Ty
Ast.DisjRuleElem(res) ->
let make_match = make_match None guard in
let orop = if guard then ctl_or else ctl_seqor in
- ctl_and CTL.NONSTRICT (label_pred_maker label)
+(* label used to be used here, but it is not use; label is only needed after
+and within dots
+ ctl_and CTL.NONSTRICT (label_pred_maker label) *)
(List.fold_left orop CTL.False (List.map make_match res))
| _ -> make_match label guard code
if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
& EX After
*)
- (* free variables *)
+ (* free variables *)
let (efvs,bfvs) =
match seq_fvs quantified
[Ast.get_fvs ifheader;Ast.get_fvs branch;afvs] with
let lv = get_label_ctr() in
let used = ref false in
let true_branch =
+ (* no point to put a label on truepred etc; it is local to this construct
+ so it must have the same label *)
make_seq guard
- [truepred label; recurse branch Tail new_quantified new_mquantified
+ [truepred None; recurse branch Tail new_quantified new_mquantified
(Some (lv,used)) llabel slabel guard] in
- let after_pred = aftpred label in
+ let after_pred = aftpred None in
let or_cases after_branch =
- ctl_or true_branch (ctl_or (fallpred label) after_branch) in
+ ctl_or true_branch (ctl_or (fallpred None) after_branch) in
let (if_header,wrapper) =
if !used
then
| _ -> failwith "not possible" in
let (e2fvs,b2fvs,s2fvs) =
(* fvs on else? *)
- match seq_fvs quantified
- [Ast.get_fvs ifheader;Ast.get_fvs branch2;afvs] with
+ (* just combine with the else branch. no point to have separate
+ quantifier, since there is only one possible control-flow path *)
+ let else_fvs = Common.union_set (Ast.get_fvs els) (Ast.get_fvs branch2) in
+ match seq_fvs quantified [Ast.get_fvs ifheader;else_fvs;afvs] with
[(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
- (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
+ (e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
| _ -> failwith "not possible" in
let bothfvs = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in
let exponlyfvs = intersect e1fvs e2fvs in
| _ -> failwith "not possible" in
let (me2fvs,mb2fvs,ms2fvs) =
(* fvs on else? *)
- match seq_fvs minus_quantified
- [Ast.get_mfvs ifheader;Ast.get_mfvs branch2;[]] with
+ (* just combine with the else branch. no point to have separate
+ quantifier, since there is only one possible control-flow path *)
+ let else_mfvs =
+ Common.union_set (Ast.get_mfvs els) (Ast.get_mfvs branch2) in
+ match seq_fvs minus_quantified [Ast.get_mfvs ifheader;else_mfvs;[]] with
[(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
(e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
| _ -> failwith "not possible" in
let used = ref false in
let true_branch =
make_seq guard
- [truepred label; recurse branch1 Tail new_quantified new_mquantified
+ [truepred None; recurse branch1 Tail new_quantified new_mquantified
(Some (lv,used)) llabel slabel guard] in
let false_branch =
make_seq guard
- [falsepred label; make_match els;
+ [falsepred None;
+ quantify guard
+ (Common.minus_set (Ast.get_fvs els) new_quantified)
+ (header_match None guard els);
recurse branch2 Tail new_quantified new_mquantified
(Some (lv,used)) llabel slabel guard] in
- let after_pred = aftpred label in
+ let after_pred = aftpred None in
let or_cases after_branch =
ctl_or true_branch (ctl_or false_branch after_branch) in
let s = guard_to_strict guard in
else (if_header,function x -> x) in
wrapper
(end_control_structure bothfvs if_header or_cases after_pred
- (Some(ctl_and s (ctl_ex (falsepred label)) (ctl_ex after_pred)))
- (Some(ctl_ex (falsepred label)))
+ (Some(ctl_and s (ctl_ex (falsepred None)) (ctl_ex after_pred)))
+ (Some(ctl_ex (falsepred None)))
aft after label guard)
let forwhile header body ((afvs,_,_,_) as aft) after
quantified minus_quantified label recurse make_match guard =
let process _ =
(* the translation in this case is similar to that of an if with no else *)
- (* free variables *)
+ (* free variables *)
let (efvs,bfvs) =
match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body;afvs] with
[(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs)
| _ -> failwith "not possible" in
let new_quantified = Common.union_set bfvs quantified in
- (* minus free variables *)
+ (* minus free variables *)
let (mefvs,mbfvs) =
match seq_fvs minus_quantified
[Ast.get_mfvs header;Ast.get_mfvs body;[]] with
let used = ref false in
let body =
make_seq guard
- [inlooppred label;
+ [inlooppred None;
recurse body Tail new_quantified new_mquantified
(Some (lv,used)) (Some (lv,used)) None guard] in
- let after_pred = fallpred label in
+ let after_pred = loopfallpred None in
let or_cases after_branch = ctl_or body after_branch in
let (header,wrapper) =
if !used
(Ast.Atomic(re),(_,_,_,Ast.CONTEXT(_,Ast.NOTHING))) ->
(match Ast.unwrap re with
Ast.MetaStmt((_,_,Ast.CONTEXT(_,Ast.NOTHING),_),
- Type_cocci.Unitary,_,false) ->
+ Type_cocci.Unitary,_,false)
+ when after = Tail or after = End or after = VeryEnd ->
let (efvs) =
match seq_fvs quantified [Ast.get_fvs header] with
[(efvs,_)] -> efvs
quantify guard efvs (make_match header)
| _ -> process())
| _ -> process()
-
+
(* --------------------------------------------------------------------- *)
(* statement metavariables *)
let label_var = (*fresh_label_var*) string2var "_lab" in
let label_pred =
CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in
- let prelabel_pred =
- CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
+ (*let prelabel_pred =
+ CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*)
let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
let full_metamatch = matcher d in
let first_metamatch =
matcher
(match d with
- Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_)) ->
- Ast.CONTEXT(pos,Ast.BEFORE(bef))
+ Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_,c)) ->
+ Ast.CONTEXT(pos,Ast.BEFORE(bef,c))
| Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
- | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
+ | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
+(*
let middle_metamatch =
matcher
(match d with
Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
- | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
+ | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
+*)
let last_metamatch =
matcher
(match d with
- Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft)) ->
- Ast.CONTEXT(pos,Ast.AFTER(aft))
+ Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft,c)) ->
+ Ast.CONTEXT(pos,Ast.AFTER(aft,c))
| Ast.CONTEXT(_,_) -> d
- | Ast.MINUS(_,_) | Ast.PLUS -> failwith "not possible") in
+ | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in
+(*
let rest_nodes =
- ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
+ ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in
+*)
+
+ let to_end = ctl_or (aftpred None) (loopfallpred None) in
let left_or = (* the whole statement is one node *)
+ make_seq_after guard
+ (ctl_and CTL.NONSTRICT (ctl_not (ctl_ex to_end)) full_metamatch) after in
+ let right_or = (* the statement covers multiple nodes *)
+ ctl_and CTL.NONSTRICT
+ (ctl_ex
+ (make_seq guard
+ [to_end; make_seq_after guard last_metamatch after]))
+ first_metamatch in
+
+(*
+ let left_or =
make_seq guard
[full_metamatch; and_after guard (ctl_not prelabel_pred) after] in
- let right_or = (* the statement covers multiple nodes *)
+ let right_or =
make_seq guard
[first_metamatch;
ctl_au CTL.NONSTRICT
[ctl_and CTL.NONSTRICT last_metamatch label_pred;
and_after guard
(ctl_not prelabel_pred) after])] in
+*)
+
let body f =
ctl_and CTL.NONSTRICT label_pred
(f (ctl_and CTL.NONSTRICT
let prelabel_pred =
CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
- let pure_d =
- (* don't have to put anything before the beginning, so don't have to
- distinguish the first node. so don't have to bother about paths,
- just use the label. label ensures that found nodes match up with
- what they should because it is in the lhs of the andany. *)
- match d with
- Ast.MINUS(pos,[]) -> true
- | Ast.CONTEXT(pos,Ast.NOTHING) -> true
- | _ -> false in
let ender =
- match (pure_d,after) with
- (true,Tail) | (true,End) | (true,VeryEnd) ->
- (* the label sharing makes it safe to use AndAny *)
- CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
- ctl_and CTL.NONSTRICT label_pred
- (make_raw_match label false ast),
- ctl_and CTL.NONSTRICT (matcher d) prelabel_pred)
- | _ ->
- (* more safe but less efficient *)
+ match (d,after) with
+ (Ast.PLUS _, _) -> failwith "not possible"
+ | (Ast.CONTEXT(pos,Ast.NOTHING),(Tail|End|VeryEnd)) ->
+ (* just match the root. don't care about label; always ok *)
+ make_raw_match None false ast
+ | (Ast.CONTEXT(pos,Ast.BEFORE(_,_)),(Tail|End|VeryEnd)) ->
+ ctl_and CTL.NONSTRICT
+ (make_raw_match None false ast) (* statement *)
+ (matcher d) (* transformation *)
+ | (Ast.CONTEXT(pos,(Ast.NOTHING|Ast.BEFORE(_,_))),(After a | Guard a)) ->
+ (* This case and the MINUS one couldprobably be merged, if
+ HackForStmt were to notice when its arguments are trivial *)
let first_metamatch = matcher d in
- let rest_metamatch =
- matcher
- (match d with
- Ast.MINUS(pos,_) -> Ast.MINUS(pos,[])
- | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING)
- | Ast.PLUS -> failwith "not possible") in
- let rest_nodes = ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred in
- let last_node = and_after guard (ctl_not prelabel_pred) after in
- (ctl_and CTL.NONSTRICT (make_raw_match label false ast)
- (make_seq guard
- [first_metamatch;
- ctl_au CTL.NONSTRICT rest_nodes last_node])) in
+ (* try to follow after link *)
+ let to_end = ctl_or (aftpred None) (loopfallpred None) in
+ let is_compound =
+ ctl_ex(make_seq guard [to_end; CTL.True; a]) in
+ let not_compound =
+ make_seq_after guard (ctl_not (ctl_ex to_end)) after in
+ ctl_and CTL.NONSTRICT (make_raw_match label false ast)
+ (ctl_and CTL.NONSTRICT
+ first_metamatch (ctl_or is_compound not_compound))
+ | (Ast.CONTEXT(pos,(Ast.AFTER _|Ast.BEFOREAFTER _)),_) ->
+ failwith "not possible"
+ | (Ast.MINUS(pos,inst,adj,l),after) ->
+ let (first_metamatch,last_metamatch,rest_metamatch) =
+ match l with
+ Ast.NOREPLACEMENT ->
+ (matcher(Ast.CONTEXT(pos,Ast.NOTHING)),CTL.True,matcher d)
+ | _ -> (matcher d,
+ matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)),
+ ctl_and CTL.NONSTRICT
+ (ctl_not (make_raw_match label false ast))
+ (matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)))) in
+ (* try to follow after link *)
+ let to_end = ctl_or (aftpred None) (loopfallpred None) in
+ let is_compound =
+ ctl_ex
+ (make_seq guard
+ [to_end; make_seq_after guard last_metamatch after]) in
+ let not_compound =
+ make_seq_after guard (ctl_not (ctl_ex to_end)) after in
+ ctl_and CTL.NONSTRICT
+ (ctl_and CTL.NONSTRICT (make_raw_match label false ast)
+ (ctl_and CTL.NONSTRICT
+ first_metamatch (ctl_or is_compound not_compound)))
+ (* don't have to put anything before the beginning, so don't have to
+ distinguish the first node. so don't have to bother about paths,
+ just use the label. label ensures that found nodes match up with
+ what they should because it is in the lhs of the andany. *)
+ (CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
+ ctl_and CTL.NONSTRICT label_pred
+ (make_raw_match label false ast),
+ ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred))
+ in
let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in
let stmt_fvs = Ast.get_fvs stmt in
let fvs = get_unquantified quantified stmt_fvs in
(* --------------------------------------------------------------------- *)
(* dots and nests *)
-let dots_au is_strict toend label s wrapcode x seq_after y quantifier =
+let dots_au is_strict toend label s wrapcode n x seq_after y quantifier =
let matchgoto = gotopred None in
let matchbreak =
make_match None false
then Common.Left(aftpred label)
else
Common.Right
- (function v ->
+ (function vx -> function v ->
+ (* vx is the contents of the nest, if any. we can only stop early
+ if we find neither the ending code nor the nest contents in
+ the if branch. not sure if this is a good idea. *)
let lv = get_label_ctr() in
let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
let preflabelpred = label_pred_maker (Some (lv,ref true)) in
+ (*let is_paren =
+ (* Rather a special case. But if the code afterwards is just
+ a } then there is no point checking after a goto that it does
+ not appear. *)
+ (* this optimization doesn't work. probably depends on whether
+ the destination of the break/goto is local or more global than
+ the dots *)
+ match seq_after with
+ CTL.And(_,e1,e2) ->
+ let is_paren = function
+ CTL.Pred(Lib_engine.Paren _,_) -> true
+ | _ -> false in
+ is_paren e1 or is_paren e2
+ | _ -> false in *)
ctl_or (aftpred label)
(quantify false [lv]
(ctl_and CTL.NONSTRICT
(ctl_and CTL.NONSTRICT (truepred label) labelpred)
(ctl_au CTL.NONSTRICT
- (ctl_and CTL.NONSTRICT (ctl_not v) preflabelpred)
+ (ctl_and CTL.NONSTRICT (ctl_not v)
+ (ctl_and CTL.NONSTRICT vx preflabelpred))
(ctl_and CTL.NONSTRICT preflabelpred
(if !Flag_matcher.only_return_is_error_exit
then
(ctl_not seq_after))
(ctl_and CTL.NONSTRICT
(ctl_or matchgoto matchbreak)
- (ctl_ag s (ctl_not seq_after)))))))))) in
+ ((*if is_paren
+ (* an optim that failed see defn is_paren
+ and tests/makes_a_loop *)
+ then CTL.True
+ else*)
+ (ctl_ag s
+ (ctl_not seq_after))))))))))) in
let op = if quantifier = !exists then ctl_au else ctl_anti_au in
let v = get_let_ctr() in
op s x
(match stop_early with
- Common.Left x -> ctl_or y x
+ Common.Left x1 -> ctl_or y x1
| Common.Right stop_early ->
- CTL.Let(v,y,ctl_or (CTL.Ref v) (stop_early (CTL.Ref v))))
+ CTL.Let(v,y,
+ ctl_or (CTL.Ref v)
+ (ctl_and CTL.NONSTRICT (label_pred_maker label)
+ (stop_early n (CTL.Ref v)))))
let rec dots_and_nests plus nest whencodes bef aft dotcode after label
process_bef_aft statement_list statement guard quantified wrapcode =
| Ast.WhenNotFalse(e) ->
(poswhen,
ctl_or (whencond_false e label guard quantified) negwhen))
- (CTL.True,bef_aft) (List.rev whencodes) in
+ (CTL.True,CTL.False(*bef_aft*)) (List.rev whencodes) in
+ (*bef_aft modifies arg so that inside of a nest can't cause the next
+ to overshoot its boundaries, eg a() <...f()...> b() where f is
+ a metavariable and the whole thing matches code in a loop;
+ don't want f to match eg b(), allowing to go around the loop again*)
let poswhen = ctl_and_ns arg poswhen in
let negwhen =
(* if !exists
on the "true" in between code *)
let plus_var = if plus then get_label_ctr() else string2var "" in
let plus_var2 = if plus then get_label_ctr() else string2var "" in
- let ornest =
+ let (ornest,just_nest) =
+ (* just_nest is used when considering whether to stop early, to continue
+ to collect nest information in the if branch *)
match (nest,guard && not plus) with
- (None,_) | (_,true) -> whencodes CTL.True
+ (None,_) | (_,true) -> (whencodes CTL.True,CTL.True)
| (Some nest,false) ->
let v = get_let_ctr() in
let is_plus x =
CTL.Pred(Lib_engine.BindGood(plus_var),
CTL.Modif plus_var2)))
else x in
- CTL.Let(v,nest,
- CTL.Or(is_plus (CTL.Ref v),
- whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
+ let body =
+ CTL.Let(v,nest,
+ CTL.Or(is_plus (CTL.Ref v),
+ whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
+ (body,body) in
let plus_modifier x =
if plus
then
let ender =
match after with
- After f -> f
- | Guard f -> ctl_uncheck f
+ (* label within dots is taken care of elsewhere. the next two lines
+ put the label on the code following dots *)
+ After f -> ctl_and (guard_to_strict guard) f labelled
+ | Guard f ->
+ (* actually, label should be None based on the only use of Guard... *)
+ assert (label = None);
+ ctl_and CTL.NONSTRICT (ctl_uncheck f) labelled
| VeryEnd ->
let exit = endpred label in
let errorexit = exitpred label in
else exit (* end at the real end of the function *) *) in
plus_modifier
(dots_au is_strict ((after = Tail) or (after = VeryEnd))
- label (guard_to_strict guard) wrapcode
- (ctl_and_ns dotcode (ctl_and_ns ornest labelled))
- aft ender quantifier)
+ label (guard_to_strict guard) wrapcode just_nest
+ (ctl_and_ns dotcode
+ (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest) labelled))
+ aft ender quantifier)
and get_whencond_exps e =
match Ast.unwrap e with
let e1 = get_whencond_exps e in
let (if_headers, while_headers, for_headers) =
make_whencond_headers e e1 label guard quantified in
+ (* if with else *)
ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers))
- (ctl_and CTL.NONSTRICT (fallpred label)
- (ctl_or (ctl_back_ex if_headers)
+ (* if without else *)
+ (ctl_or (ctl_and CTL.NONSTRICT (fallpred label) (ctl_back_ex if_headers))
+ (* failure of loop test *)
+ (ctl_and CTL.NONSTRICT (loopfallpred label)
(ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
(* --------------------------------------------------------------------- *)
(* the main translation loop *)
-
+
let rec statement_list stmt_list after quantified minus_quantified
label llabel slabel dots_before guard =
let isdots x =
this makes more matching for things like when (...) S, but perhaps
that matching is not so costly anyway *)
(*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*)
- | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_)) as d),_),
+ | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_,_)) as d),_),
keep,seqible,_)
- | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_)) as d),_),
+ | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_,_)) as d),_),
keep,seqible,_)->
svar_context_with_add_after stmt s label quantified d ast seqible
after
is absent *)
let new_mc =
match (retmc,semmc) with
- (Ast.MINUS(_,l1),Ast.MINUS(_,l2)) when !Flag.sgrep_mode2 ->
+ (Ast.MINUS(_,inst1,adj1,l1),Ast.MINUS(_,_,_,l2))
+ when !Flag.sgrep_mode2 ->
(* in sgrep mode, we can propagate the - *)
- Some (Ast.MINUS(Ast.NoPos,l1@l2))
- | (Ast.MINUS(_,l1),Ast.MINUS(_,l2))
- | (Ast.CONTEXT(_,Ast.BEFORE(l1)),
- Ast.CONTEXT(_,Ast.AFTER(l2))) ->
- Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2)))
+ let new_info =
+ match (l1,l2) with
+ (Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) ->
+ Ast.NOREPLACEMENT
+ | _ ->
+ failwith "no replacements allowed in sgrep mode" in
+ Some (Ast.MINUS(Ast.NoPos,inst1,adj1,new_info))
+ | (Ast.MINUS(_,_,_,l1),Ast.MINUS(_,_,_,l2)) ->
+ let change =
+ match (l1,l2) with
+ (Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) ->
+ Ast.NOTHING
+ | (Ast.NOREPLACEMENT,Ast.REPLACEMENT(l,ct))
+ | (Ast.REPLACEMENT(l,ct),Ast.NOREPLACEMENT) ->
+ Ast.BEFORE(l,ct)
+ | (Ast.REPLACEMENT(l1,ct1),Ast.REPLACEMENT(l2,ct2)) ->
+ Ast.BEFORE(l1@l2,Ast.lub_count ct1 ct2) in
+ Some (Ast.CONTEXT(Ast.NoPos,change))
+ | (Ast.CONTEXT(_,Ast.BEFORE(l1,c1)),
+ Ast.CONTEXT(_,Ast.AFTER(l2,c2))) ->
+ Some
+ (Ast.CONTEXT(Ast.NoPos,
+ Ast.BEFORE(l1@l2,Ast.lub_count c1 c2)))
| (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING))
| (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) ->
Some retmc
- | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.AFTER(l))) ->
- Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l)))
+ | (Ast.CONTEXT(_,Ast.NOTHING),
+ Ast.CONTEXT(_,Ast.AFTER(l,c))) ->
+ Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l,c)))
| _ -> None in
let ret = Ast.make_mcode "return" in
let edots =
quantified minus_quantified label llabel slabel guard in
dots_done := true;
make_seq_after term after)
- | Ast.Seq(lbrace,decls,body,rbrace) ->
- let (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs) =
+ | Ast.Seq(lbrace,body,rbrace) ->
+ let (lbfvs,b1fvs,b2fvs,rbfvs) =
match
seq_fvs quantified
- [Ast.get_fvs lbrace;Ast.get_fvs decls;
- Ast.get_fvs body;Ast.get_fvs rbrace]
+ [Ast.get_fvs lbrace;Ast.get_fvs body;Ast.get_fvs rbrace]
with
- [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
- (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
+ [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] -> (lbfvs,b1fvs,b2fvs,rbfvs)
| _ -> failwith "not possible" in
- let (mlbfvs,mb1fvs,mb2fvs,mb3fvs,mrbfvs) =
+ let (mlbfvs,mb1fvs,mb2fvs,mrbfvs) =
match
seq_fvs minus_quantified
- [Ast.get_mfvs lbrace;Ast.get_mfvs decls;
- Ast.get_mfvs body;Ast.get_mfvs rbrace]
+ [Ast.get_mfvs lbrace;Ast.get_mfvs body;Ast.get_mfvs rbrace]
with
- [(lbfvs,b1fvs);(_,b2fvs);(_,b3fvs);(rbfvs,_)] ->
- (lbfvs,b1fvs,b2fvs,b3fvs,rbfvs)
+ [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] ->
+ (lbfvs,b1fvs,b2fvs,rbfvs)
| _ -> failwith "not possible" in
let pv = count_nested_braces stmt in
let lv = get_label_ctr() in
(* label is not needed; paren_pred is enough *)
quantify guard rbfvs
(ctl_au (make_match empty_rbrace)
- (ctl_and
- (real_make_match None guard rbrace)
- paren_pred)) in
+ (ctl_and (real_make_match None guard rbrace) paren_pred)) in
let new_quantified2 =
Common.union_set b1fvs (Common.union_set b2fvs quantified) in
- let new_quantified3 = Common.union_set b3fvs new_quantified2 in
let new_mquantified2 =
Common.union_set mb1fvs (Common.union_set mb2fvs minus_quantified) in
- let new_mquantified3 = Common.union_set mb3fvs new_mquantified2 in
let pattern_as_given =
let new_quantified2 = Common.union_set [pv] new_quantified2 in
- let new_quantified3 = Common.union_set [pv] new_quantified3 in
quantify true [pv;lv]
(quantify guard b1fvs
(make_seq
[start_brace;
- quantify guard b2fvs
- (statement_list decls
- (After
- (quantify guard b3fvs
- (statement_list body
- (After (make_seq_after end_brace after))
- new_quantified3 new_mquantified3
- (Some (lv,ref true)) (* label mostly useful *)
- llabel slabel true guard)))
- new_quantified2 new_mquantified2
- (Some (lv,ref true)) llabel slabel false guard)])) in
- if ends_in_return body
+ (ctl_or
+ (if !exists = Exists then CTL.False else (aftpred label))
+ (quantify guard b2fvs
+ (statement_list body
+ (After (make_seq_after end_brace after))
+ new_quantified2 new_mquantified2
+ (Some (lv,ref true))
+ llabel slabel false guard)))])) in
+ let empty_body =
+ match Ast.undots body with
+ [body] ->
+ (match Ast.unwrap body with
+ Ast.Dots
+ ((_,i,Ast.CONTEXT(_,Ast.NOTHING),_),[],_,_) ->
+ (match Ast.unwrap rbrace with
+ Ast.SeqEnd((_,_,Ast.CONTEXT(_,Ast.NOTHING),_))
+ when not (contains_pos rbrace) -> true
+ | _ -> false)
+ | _ -> false)
+ | _ -> false in
+ if empty_body && after = Tail
+ (* for just a match of an if branch of the form { ... }, just
+ match the first brace *)
+ then quantify guard lbfvs (make_match lbrace)
+ else if ends_in_return body
then
(* matching error handling code *)
(* Cases:
ctl_au
(make_match empty_rbrace)
(ctl_ax (* skip the destination label *)
- (quantify guard b3fvs
+ (quantify guard b2fvs
(statement_list body End
- new_quantified3 new_mquantified3 None llabel slabel
+ new_quantified2 new_mquantified2 None llabel slabel
true guard)))] in
let pattern3 =
let new_quantified2 = Common.union_set [pv] new_quantified2 in
- let new_quantified3 = Common.union_set [pv] new_quantified3 in
quantify true [pv;lv]
(quantify guard b1fvs
(make_seq
(* want AF even for sgrep *)
(CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace))))
(quantify guard b2fvs
- (statement_list decls
- (After
- (quantify guard b3fvs
- (statement_list body Tail
- (*After
- (make_seq_after
- nopv_end_brace after)*)
- new_quantified3 new_mquantified3
- None llabel slabel true guard)))
+ (statement_list body Tail
new_quantified2 new_mquantified2
- (Some (lv,ref true))
+ None(*no label because past the goto*)
llabel slabel false guard))])) in
- ctl_or pattern_as_given
- (match Ast.unwrap decls with
- Ast.DOTS([]) -> ctl_or pattern2 pattern3
- | Ast.DOTS(l) -> pattern3
- | _ -> failwith "circles and stars not supported")
+ ctl_or pattern_as_given (ctl_or pattern2 pattern3)
else pattern_as_given
| Ast.IfThen(ifheader,branch,aft) ->
ifthen ifheader branch aft after quantified minus_quantified
label llabel slabel statement make_match guard
-
+
| Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
ifthenelse ifheader branch1 els branch2 aft after quantified
minus_quantified label llabel slabel statement make_match guard
label statement make_match guard
| Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *)
- ctl_and
- (label_pred_maker label)
+ (*ctl_and seems pointless, disjuncts see label too
+ (label_pred_maker label)*)
(List.fold_left ctl_seqor CTL.False
(List.map
(function sl ->
llabel slabel true guard)
stmt_dots_list))
- | Ast.Nest(stmt_dots,whencode,multi,bef,aft) ->
+ | Ast.Nest(starter,stmt_dots,ender,whencode,multi,bef,aft) ->
(* label in recursive call is None because label check is already
- wrapped around the corresponding code *)
+ wrapped around the corresponding code. not good enough, want to stay
+ in a specific region, dots and nests will keep going *)
let bfvs =
match seq_fvs quantified [Ast.get_wcfvs whencode;Ast.get_fvs stmt_dots]
(* no minus version because when code doesn't contain any minus code *)
let new_quantified = Common.union_set bfvs quantified in
+ let dot_code =
+ match Ast.get_mcodekind starter with (*ender must have the same mcode*)
+ Ast.MINUS(_,_,_,_) as d ->
+ (* no need for the fresh metavar, but ... is a bit weird as a
+ variable name *)
+ Some(make_match (make_meta_rule_elem d ([],[],[])))
+ | _ -> None in
+
quantify guard bfvs
(let dots_pattern =
statement_list stmt_dots (a2n after) new_quantified minus_quantified
- None llabel slabel true guard in
+ label(*None*) llabel slabel true guard in
dots_and_nests multi
- (Some dots_pattern) whencode bef aft None after label
+ (Some dots_pattern) whencode bef aft dot_code after label
(process_bef_aft new_quantified minus_quantified
- None llabel slabel true)
+ label(*None*) llabel slabel true)
(function x ->
- statement_list x Tail new_quantified minus_quantified None
+ statement_list x Tail new_quantified minus_quantified label(*None*)
llabel slabel true true)
(function x ->
- statement x Tail new_quantified minus_quantified None
+ statement x Tail new_quantified minus_quantified label(*None*)
llabel slabel true)
guard quantified
(function x -> Ast.set_fvs [] (Ast.rewrap stmt x)))
| Ast.Dots((_,i,d,_),whencodes,bef,aft) ->
let dot_code =
match d with
- Ast.MINUS(_,_) ->
- (* no need for the fresh metavar, but ... is a bit wierd as a
+ Ast.MINUS(_,_,_,_) ->
+ (* no need for the fresh metavar, but ... is a bit weird as a
variable name *)
Some(make_match (make_meta_rule_elem d ([],[],[])))
| _ -> None in
guard quantified
(function x -> Ast.set_fvs [] (Ast.rewrap stmt x))
- | Ast.Switch(header,lb,cases,rb) ->
+ | Ast.Switch(header,lb,decls,cases,rb) ->
let rec intersect_all = function
[] -> []
| [x] -> x
| x::xs -> intersect x (intersect_all xs) in
+ let rec intersect_all2 = function (* pairwise *)
+ [] -> []
+ | x::xs ->
+ let front =
+ List.filter
+ (function elem -> List.exists (List.mem elem) xs)
+ x in
+ Common.union_set front (intersect_all2 xs) in
let rec union_all l = List.fold_left union [] l in
(* start normal variables *)
let header_fvs = Ast.get_fvs header in
let lb_fvs = Ast.get_fvs lb in
+ let decl_fvs = union_all (List.map Ast.get_fvs (Ast.undots decls)) in
let case_fvs = List.map Ast.get_fvs cases in
let rb_fvs = Ast.get_fvs rb in
let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
rbfvs::all_rbfvs)
| _ -> failwith "not possible")
- ([],[],[],[],[],[],[]) case_fvs in
+ ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in
let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs,
all_casefvs,all_b3fvs,all_rbfvs) =
(List.rev all_efvs,List.rev all_b1fvs,List.rev all_lbfvs,
(* let rbonlyfvs = intersect_all all_rbfvs in*)
let b1fvs = union_all all_b1fvs in
let new1_quantified = union b1fvs quantified in
- let b2fvs = union (union_all all_b1fvs) (intersect_all all_casefvs) in
+ let b2fvs =
+ union (union_all all_b2fvs) (intersect_all2 all_casefvs) in
let new2_quantified = union b2fvs new1_quantified in
(* let b3fvs = union_all all_b3fvs in*)
(* ------------------- start minus free variables *)
let header_mfvs = Ast.get_mfvs header in
let lb_mfvs = Ast.get_mfvs lb in
+ let decl_mfvs = union_all (List.map Ast.get_mfvs (Ast.undots decls)) in
let case_mfvs = List.map Ast.get_mfvs cases in
let rb_mfvs = Ast.get_mfvs rb in
let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs,
rbfvs::all_rbfvs)
| _ -> failwith "not possible")
- ([],[],[],[],[],[],[]) case_mfvs in
+ ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in
let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs,
all_mcasefvs,all_mb3fvs,all_mrbfvs) =
(List.rev all_mefvs,List.rev all_mb1fvs,List.rev all_mlbfvs,
(* let rbonlyfvs = intersect_all all_rbfvs in*)
let mb1fvs = union_all all_mb1fvs in
let new1_mquantified = union mb1fvs quantified in
- let mb2fvs = union (union_all all_mb1fvs) (intersect_all all_mcasefvs) in
+ let mb2fvs =
+ union (union_all all_mb2fvs) (intersect_all2 all_mcasefvs) in
let new2_mquantified = union mb2fvs new1_mquantified in
(* let b3fvs = union_all all_b3fvs in*)
(* ------------------- end collection of free variables *)
quantify guard e1fvs (real_make_match label true header)
| Ast.OptCase(case_line) -> failwith "not supported")
cases in
- let no_header =
- ctl_not (List.fold_left ctl_or_fl CTL.False case_headers) in
let lv = get_label_ctr() in
let used = ref false in
+ let (decls_exists_code,decls_all_code) =
+ (*don't really understand this*)
+ if (Ast.undots decls) = []
+ then (CTL.True,CTL.False)
+ else
+ let res =
+ statement_list decls Tail
+ new2_quantified new2_mquantified (Some (lv,used)) llabel None
+ false(*?*) guard in
+ (res,res) in
+ let no_header =
+ ctl_not
+ (List.fold_left ctl_or_fl CTL.False
+ (List.map ctl_uncheck
+ (decls_all_code::case_headers))) in
let case_code =
List.map
(function case_line ->
let new3_mquantified = union mb1fvs new2_mquantified in
let body =
statement_list body Tail
- new3_quantified new3_mquantified label llabel
- (Some (lv,used)) true(*?*) guard in
+ new3_quantified new3_mquantified (Some (lv,used)) llabel
+ (Some (lv,used)) false(*?*) guard in
quantify guard b1fvs (make_seq [case_header; body])
| Ast.OptCase(case_line) -> failwith "not supported")
cases in
(make_seq
[ctl_and lb
(List.fold_left ctl_and CTL.True
- (List.map ctl_ex case_headers));
- List.fold_left ctl_or_fl no_header case_code])))
+ (List.map ctl_ex
+ (decls_exists_code :: case_headers)));
+ List.fold_left ctl_or_fl no_header
+ (decls_all_code :: case_code)])))
after_branch in
let aft =
(rb_fvs,Ast.get_fresh rb,Ast.get_inherited rb,
wrapper
(end_control_structure b1fvs switch_header body
after_pred (Some(ctl_ex after_pred)) None aft after label guard)
- | Ast.FunDecl(header,lbrace,decls,body,rbrace) ->
- let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs) =
+ | Ast.FunDecl(header,lbrace,body,rbrace) ->
+ let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs) =
match
seq_fvs quantified
- [Ast.get_fvs header;Ast.get_fvs lbrace;Ast.get_fvs decls;
+ [Ast.get_fvs header;Ast.get_fvs lbrace;
Ast.get_fvs body;Ast.get_fvs rbrace]
with
- [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
- (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
+ [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] ->
+ (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs)
| _ -> failwith "not possible" in
- let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mb4fvs,mrbfvs) =
+ let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mrbfvs) =
match
seq_fvs quantified
- [Ast.get_mfvs header;Ast.get_mfvs lbrace;Ast.get_mfvs decls;
+ [Ast.get_mfvs header;Ast.get_mfvs lbrace;
Ast.get_mfvs body;Ast.get_mfvs rbrace]
with
- [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(_,b4fvs);(rbfvs,_)] ->
- (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,b4fvs,rbfvs)
+ [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] ->
+ (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs)
| _ -> failwith "not possible" in
let function_header = quantify guard hfvs (make_match header) in
let start_brace = quantify guard lbfvs (make_match lbrace) in
let new_quantified3 =
Common.union_set b1fvs
(Common.union_set b2fvs (Common.union_set b3fvs quantified)) in
- let new_quantified4 = Common.union_set b4fvs new_quantified3 in
let new_mquantified3 =
Common.union_set mb1fvs
(Common.union_set mb2fvs
(Common.union_set mb3fvs minus_quantified)) in
- let new_mquantified4 = Common.union_set mb4fvs new_mquantified3 in
- let fn_nest =
- match (Ast.undots decls,Ast.undots body,
+ let not_minus = function Ast.MINUS(_,_,_,_) -> false | _ -> true in
+ let optim1 =
+ match (Ast.undots body,
contains_modif rbrace or contains_pos rbrace) with
- ([],[body],false) ->
+ ([body],false) ->
(match Ast.unwrap body with
- Ast.Nest(stmt_dots,[],multi,_,_) ->
- if multi
- then None (* not sure how to optimize this case *)
- else Some (Common.Left stmt_dots)
- | Ast.Dots(_,whencode,_,_) when
+ Ast.Nest(starter,stmt_dots,ender,[],false,_,_)
+ (* perhaps could optimize for minus case too... TODO *)
+ when not_minus (Ast.get_mcodekind starter)
+ ->
+ (* special case for function header + body - header is unambiguous
+ and unique, so we can just look for the nested body anywhere
+ else in the CFG *)
+ Some
+ (CTL.AndAny
+ (CTL.FORWARD,guard_to_strict guard,start_brace,
+ statement_list stmt_dots
+ (* discards match on right brace, but don't need it *)
+ (Guard (make_seq_after end_brace after))
+ new_quantified3 new_mquantified3
+ None llabel slabel true guard))
+ | Ast.Dots((_,i,d,_),whencode,_,_) when
(List.for_all
(* flow sensitive, so not optimizable *)
(function Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
false
| _ -> true) whencode) ->
- Some (Common.Right whencode)
+ (* try to be more efficient for the case where the body is just
+ ... Perhaps this is too much of a special case, but useful
+ for dropping a parameter and checking that it is never used. *)
+ (match d with
+ Ast.MINUS(_,_,_,_) -> None
+ | _ ->
+ let pv =
+ (* no nested braces, because only dots *)
+ string2var ("p1") in
+ let paren_pred =
+ CTL.Pred(Lib_engine.Paren pv,CTL.Control) in
+ Some (
+ make_seq
+ [ctl_and start_brace paren_pred;
+ match whencode with
+ [] -> CTL.True
+ | _ ->
+ let leftarg =
+ ctl_and
+ (ctl_not
+ (List.fold_left
+ (function prev ->
+ function
+ Ast.WhenAlways(s) -> prev
+ | Ast.WhenNot(sl) ->
+ let x =
+ statement_list sl Tail
+ new_quantified3
+ new_mquantified3
+ label llabel slabel
+ true true in
+ ctl_or prev x
+ | Ast.WhenNotTrue(_)
+ | Ast.WhenNotFalse(_) ->
+ failwith "unexpected"
+ | Ast.WhenModifier
+ (Ast.WhenAny) -> CTL.False
+ | Ast.WhenModifier(_) -> prev)
+ CTL.False whencode))
+ (List.fold_left
+ (function prev ->
+ function
+ Ast.WhenAlways(s) ->
+ let x =
+ statement s Tail
+ new_quantified3
+ new_mquantified3
+ label llabel slabel true in
+ ctl_and prev x
+ | Ast.WhenNot(sl) -> prev
+ | Ast.WhenNotTrue(_)
+ | Ast.WhenNotFalse(_) ->
+ failwith "unexpected"
+ | Ast.WhenModifier(Ast.WhenAny) ->
+ CTL.True
+ | Ast.WhenModifier(_) -> prev)
+ CTL.True whencode) in
+ ctl_au leftarg
+ (ctl_and
+ (make_match stripped_rbrace)
+ paren_pred)]))
+ | _ -> None)
+ | _ -> None in
+ let optim2 =
+ (* function body is all minus, no whencode *)
+ match Ast.undots body with
+ [body] ->
+ (match Ast.unwrap body with
+ Ast.Dots
+ ((_,i,(Ast.MINUS(_,_,_,Ast.NOREPLACEMENT) as d),_),[],_,_) ->
+ (match (Ast.unwrap lbrace,Ast.unwrap rbrace) with
+ (Ast.SeqStart((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_)),
+ Ast.SeqEnd((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_)))
+ when not (contains_pos rbrace) ->
+ Some
+ (* andany drops everything to the end, including close
+ braces - not just function body, could check
+ label to keep braces *)
+ (ctl_and start_brace
+ (ctl_ax
+ (CTL.AndAny
+ (CTL.FORWARD,guard_to_strict guard,CTL.True,
+ make_match
+ (make_meta_rule_elem d ([],[],[]))))))
+ | _ -> None)
| _ -> None)
| _ -> None in
let body_code =
- match fn_nest with
- Some (Common.Left stmt_dots) ->
- (* special case for function header + body - header is unambiguous
- and unique, so we can just look for the nested body anywhere
- else in the CFG *)
- CTL.AndAny
- (CTL.FORWARD,guard_to_strict guard,start_brace,
- statement_list stmt_dots
- (* discards match on right brace, but don't need it *)
- (Guard (make_seq_after end_brace after))
- new_quantified4 new_mquantified4
- None llabel slabel true guard)
- | Some (Common.Right whencode) ->
- (* try to be more efficient for the case where the body is just
- ... Perhaps this is too much of a special case, but useful
- for dropping a parameter and checking that it is never used. *)
- make_seq
- [start_brace;
- match whencode with
- [] -> CTL.True
- | _ ->
- let leftarg =
- ctl_and
- (ctl_not
- (List.fold_left
- (function prev ->
- function
- Ast.WhenAlways(s) -> prev
- | Ast.WhenNot(sl) ->
- let x =
- statement_list sl Tail
- new_quantified4 new_mquantified4
- label llabel slabel true true in
- ctl_or prev x
- | Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
- failwith "unexpected"
- | Ast.WhenModifier(Ast.WhenAny) -> CTL.False
- | Ast.WhenModifier(_) -> prev)
- CTL.False whencode))
- (List.fold_left
- (function prev ->
- function
- Ast.WhenAlways(s) ->
- let x =
- statement s Tail
- new_quantified4 new_mquantified4
- label llabel slabel true in
- ctl_and prev x
- | Ast.WhenNot(sl) -> prev
- | Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
- failwith "unexpected"
- | Ast.WhenModifier(Ast.WhenAny) -> CTL.True
- | Ast.WhenModifier(_) -> prev)
- CTL.True whencode) in
- ctl_au leftarg (make_match stripped_rbrace)]
- | None ->
+ match (optim1,optim2) with
+ (Some o1,_) -> o1
+ | (_,Some o2) -> o2
+ | _ ->
make_seq
[start_brace;
quantify guard b3fvs
- (statement_list decls
- (After
- (quantify guard b4fvs
- (statement_list body
- (After (make_seq_after end_brace after))
- new_quantified4 new_mquantified4
- None llabel slabel true guard)))
+ (statement_list body
+ (After (make_seq_after end_brace after))
new_quantified3 new_mquantified3 None llabel slabel
false guard)] in
quantify guard b1fvs
(v,ctl_or
(ctl_back_ex (ctl_or (truepred label) (inlooppred label)))
(ctl_back_ex (ctl_back_ex (falsepred label))),
- ctl_or case1 case2)
+ ctl_or case1 case2)
| Ast.NoDots -> term
(* un_process_bef_aft is because we don't want to do transformation in this
(* --------------------------------------------------------------------- *)
(* Function declaration *)
-let top_level name (ua,pos) t =
+(* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
+
+let top_level name ((ua,pos),fua) (fuas,t) =
let ua = List.filter (function (nm,_) -> nm = name) ua in
used_after := ua;
saved := Ast.get_saved t;
- let quantified = Common.minus_set ua pos in
- quantify false quantified
- (match Ast.unwrap t with
+ let quantified = Common.minus_set (Common.union_set ua fuas) pos in
+ let (wrap,formula) =
+ match Ast.unwrap t with
Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
- | Ast.DECL(stmt) ->
+ | Ast.NONDECL(stmt) ->
let unopt = elim_opt.V.rebuilder_statement stmt in
let unopt = preprocess_dots_e unopt in
- cleanup(statement unopt VeryEnd quantified [] None None None false)
+ let formula =
+ cleanup(statement unopt VeryEnd quantified [] None None None false) in
+ ((function x -> NONDECL x), formula)
| Ast.CODE(stmt_dots) ->
let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in
let unopt = preprocess_dots unopt in
let res =
statement_list unopt VeryEnd quantified [] None None None
false false in
- cleanup
- (if starts_with_dots
- then
+ let formula =
+ cleanup
+ (if starts_with_dots
+ then
(* EX because there is a loop on enter/top *)
- ctl_and CTL.NONSTRICT (toppred None) (ctl_ex res)
- else if starts_with_brace
- then
- ctl_and CTL.NONSTRICT
- (ctl_not(CTL.EX(CTL.BACKWARD,(funpred None)))) res
- else res)
- | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords")
+ ctl_and CTL.NONSTRICT (toppred None) (ctl_ex res)
+ else if starts_with_brace
+ then
+ ctl_and CTL.NONSTRICT
+ (ctl_not(CTL.EX(CTL.BACKWARD,(funpred None)))) res
+ else res) in
+ ((function x -> CODE x), formula)
+ | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords" in
+ wrap (quantify false quantified formula)
(* --------------------------------------------------------------------- *)
(* Entry points *)
-let asttoctlz (name,(_,_,exists_flag),l) used_after positions =
+let asttoctlz (name,(_,_,exists_flag),l)
+ (used_after,fresh_used_after,fresh_used_after_seeds) positions =
letctr := 0;
labelctr := 0;
(match exists_flag with
Ast.Exists -> exists := Exists
| Ast.Forall -> exists := Forall
- | Ast.ReverseForall -> exists := ReverseForall
| Ast.Undetermined ->
exists := if !Flag.sgrep_mode2 then Exists else Forall);
(function (t,_) ->
match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
(List.combine l (List.combine used_after positions))) in
- let res = List.map2 (top_level name) used_after l in
+ let res =
+ List.map2 (top_level name)
+ (List.combine used_after fresh_used_after)
+ (List.combine fresh_used_after_seeds l) in
exists := Forall;
res
let asttoctl r used_after positions =
match r with
- Ast.ScriptRule _ -> []
+ Ast.ScriptRule _ | Ast.InitialScriptRule _ | Ast.FinalScriptRule _ -> []
| Ast.CocciRule (a,b,c,_,Ast_cocci.Normal) ->
asttoctlz (a,b,c) used_after positions
- | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CTL.True]
+ | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CODE CTL.True]
let pp_cocci_predicate (pred,modif) =
Pretty_print_engine.pp_predicate pred
HCoop / bpt / coccinelle.git / blobdiff