(*
-* 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.
-*)
+ * 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
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) ->
+ 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
V.rebuilder
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- mcode
donothing donothing stmtdotsfn donothing
donothing donothing donothing donothing donothing donothing donothing
donothing donothing donothing donothing donothing
let contains_modif =
let bind x y = x or y in
let option_default = false in
- let mcode r (_,_,kind,_) =
+ 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 recursor =
V.combiner bind option_default
mcode 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 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 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
+ | _ -> 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 rule_elem do_nothing do_nothing do_nothing do_nothing in
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
- mcode
donothing donothing donothing donothing
donothing donothing donothing donothing donothing donothing
donothing donothing stmt_count donothing donothing donothing in
(function
Ast.WhenNot w -> let (w,_) = get_before w [] in Ast.WhenNot w
| Ast.WhenAlways w -> let (w,_) = get_before_e w [] in Ast.WhenAlways w
- | Ast.WhenModifier(x) -> Ast.WhenModifier(x))
+ | Ast.WhenModifier(x) -> Ast.WhenModifier(x)
+ | Ast.WhenNotTrue w -> Ast.WhenNotTrue w
+ | Ast.WhenNotFalse w -> Ast.WhenNotFalse w)
wc
and get_before_e s a =
| Ast.Nest(stmt_dots,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
+ a in*)
(Ast.rewrap s (Ast.Nest(sd,w,multi,a,aft)),[Ast.Other_dots stmt_dots])
| Ast.Disj(stmt_dots_list) ->
let (dsl,dsla) =
(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)),[])
- | _ -> failwith "get_before_e: not supported"
+ (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"
let rec get_after sl a =
match Ast.unwrap sl with
(function
Ast.WhenNot w -> let (w,_) = get_after w a (*?*) in Ast.WhenNot w
| Ast.WhenAlways w -> let (w,_) = get_after_e w a in Ast.WhenAlways w
- | Ast.WhenModifier(x) -> Ast.WhenModifier(x))
+ | Ast.WhenModifier(x) -> Ast.WhenModifier(x)
+ | Ast.WhenNotTrue w -> Ast.WhenNotTrue w
+ | Ast.WhenNotFalse w -> Ast.WhenNotFalse w)
wc
and get_after_e s a =
| Ast.Nest(stmt_dots,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
+ a in*)
(Ast.rewrap s (Ast.Nest(sd,w,multi,bef,a)),[Ast.Other_dots stmt_dots])
| Ast.Disj(stmt_dots_list) ->
let (dsl,dsla) =
(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 =
x::_ ->
(match Ast.unwrap x with
Ast.Atomic(x) ->
- (match Ast.unwrap x with
- Ast.Return(_,_) | Ast.ReturnExpr(_,_,_) -> true
- | _ -> false)
+ let rec loop x =
+ match Ast.unwrap x with
+ Ast.Return(_,_) | Ast.ReturnExpr(_,_,_) -> true
+ | Ast.DisjRuleElem((_::_) as l) -> List.for_all loop l
+ | _ -> false in
+ loop x
| Ast.Disj(disjs) -> List.for_all ends_in_return disjs
| _ -> false)
| _ -> false)
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
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
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
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
+ [] -> (matcher(Ast.CONTEXT(pos,Ast.NOTHING)),CTL.True,matcher d)
+ | _ -> (matcher d,
+ matcher(Ast.MINUS(pos,inst,adj,[])),
+ ctl_and CTL.NONSTRICT
+ (ctl_not (make_raw_match label false ast))
+ (matcher(Ast.MINUS(pos,inst,adj,[])))) 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
make_match None false
(wrapcode
(Ast.Continue(Ast.make_mcode "continue",Ast.make_mcode ";"))) in
- let stop_early v =
- if !exists = Exists
- then CTL.False
+ let stop_early =
+ if quantifier = Exists
+ then Common.Left(CTL.False)
else if toend
- then CTL.Or(aftpred label,exitpred label)
+ then Common.Left(CTL.Or(aftpred label,exitpred label))
else if is_strict
- then aftpred label
+ then Common.Left(aftpred label)
else
- 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
- 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 preflabelpred
- (ctl_or (retpred None)
- (if !Flag_engine.only_return_is_error_exit
- then CTL.True
- else
- (ctl_or matchcontinue
- (ctl_and CTL.NONSTRICT
- (ctl_or matchgoto matchbreak)
- (ctl_ag s (ctl_not seq_after)))))))))) in
- let v = get_let_ctr() in
+ Common.Right
+ (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)
+ (ctl_and CTL.NONSTRICT vx preflabelpred))
+ (ctl_and CTL.NONSTRICT preflabelpred
+ (if !Flag_matcher.only_return_is_error_exit
+ then
+ (ctl_and CTL.NONSTRICT
+ (retpred None) (ctl_not seq_after))
+ else
+ (ctl_or
+ (ctl_and CTL.NONSTRICT
+ (ctl_or (retpred None) matchcontinue)
+ (ctl_not seq_after))
+ (ctl_and CTL.NONSTRICT
+ (ctl_or matchgoto matchbreak)
+ ((*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
- op s x (CTL.Let(v,y,ctl_or (CTL.Ref v) (stop_early (CTL.Ref v))))
+ let v = get_let_ctr() in
+ op s x
+ (match stop_early with
+ Common.Left x1 -> ctl_or y x1
+ | Common.Right stop_early ->
+ 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 wrapcode =
+ process_bef_aft statement_list statement guard quantified wrapcode =
let ctl_and_ns = ctl_and CTL.NONSTRICT in
(* proces bef_aft *)
let shortest l =
if check_quantifier Ast.WhenExists Ast.WhenForall
then Exists
else
- if check_quantifier Ast.WhenExists Ast.WhenForall
+ if check_quantifier Ast.WhenForall Ast.WhenExists
then Forall
else !exists in
(* the following is used when we find a goto, etc and consider accepting
(poswhen,ctl_or (statement_list whencodes) negwhen)
| Ast.WhenAlways stm ->
(ctl_and CTL.NONSTRICT (statement stm) poswhen,negwhen)
- | Ast.WhenModifier(_) -> (poswhen,negwhen))
- (CTL.True,bef_aft) (List.rev whencodes) in
+ | Ast.WhenModifier(_) -> (poswhen,negwhen)
+ | Ast.WhenNotTrue(e) ->
+ (poswhen,
+ ctl_or (whencond_true e label guard quantified) negwhen)
+ | Ast.WhenNotFalse(e) ->
+ (poswhen,
+ ctl_or (whencond_false e label guard quantified) negwhen))
+ (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))
+ 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
+ Ast.Exp e -> [e]
+ | Ast.DisjRuleElem(res) ->
+ List.fold_left Common.union_set [] (List.map get_whencond_exps res)
+ | _ -> failwith "not possible"
+
+and make_whencond_headers e e1 label guard quantified =
+ let fvs = Ast.get_fvs e in
+ let header_pred h =
+ quantify guard (get_unquantified quantified fvs)
+ (make_match label guard h) in
+ let if_header e1 =
+ header_pred
+ (Ast.rewrap e
+ (Ast.IfHeader
+ (Ast.make_mcode "if",
+ Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in
+ let while_header e1 =
+ header_pred
+ (Ast.rewrap e
+ (Ast.WhileHeader
+ (Ast.make_mcode "while",
+ Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in
+ let for_header e1 =
+ header_pred
+ (Ast.rewrap e
+ (Ast.ForHeader
+ (Ast.make_mcode "for",Ast.make_mcode "(",None,Ast.make_mcode ";",
+ Some e1,Ast.make_mcode ";",None,Ast.make_mcode ")"))) in
+ let if_headers =
+ List.fold_left ctl_or CTL.False (List.map if_header e1) in
+ let while_headers =
+ List.fold_left ctl_or CTL.False (List.map while_header e1) in
+ let for_headers =
+ List.fold_left ctl_or CTL.False (List.map for_header e1) in
+ (if_headers, while_headers, for_headers)
+
+and whencond_true e label guard quantified =
+ let e1 = get_whencond_exps e in
+ let (if_headers, while_headers, for_headers) =
+ make_whencond_headers e e1 label guard quantified in
+ ctl_or
+ (ctl_and CTL.NONSTRICT (truepred label) (ctl_back_ex if_headers))
+ (ctl_and CTL.NONSTRICT
+ (inlooppred label) (ctl_back_ex (ctl_or while_headers for_headers)))
+
+and whencond_false e label guard quantified =
+ let e1 = get_whencond_exps e in
+ let (if_headers, while_headers, for_headers) =
+ make_whencond_headers e e1 label guard quantified in
+ ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers))
+ (ctl_and CTL.NONSTRICT (loopfallpred label)
+ (ctl_or (ctl_back_ex if_headers)
+ (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers))))
+
(* --------------------------------------------------------------------- *)
(* the main translation loop *)
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)))
+ Some (Ast.MINUS(Ast.NoPos,inst1,adj1,l1@l2))
+ | (Ast.MINUS(_,_,_,l1),Ast.MINUS(_,_,_,l2)) ->
+ Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2,Ast.ONE)))
+ | (Ast.CONTEXT(_,Ast.BEFORE(l1,c1)),
+ Ast.CONTEXT(_,Ast.AFTER(l2,c2))) ->
+ (if not (c1 = c2) then failwith "bad + code");
+ Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2,c1)))
| (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 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 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
ctl_and
(quantify guard lbfvs (make_match lbrace))
(ctl_and paren_pred label_pred) in
+ let empty_rbrace =
+ match Ast.unwrap rbrace with
+ Ast.SeqEnd((data,info,_,pos)) ->
+ Ast.rewrap rbrace(Ast.SeqEnd(Ast.make_mcode data))
+ | _ -> failwith "unexpected close brace" in
let end_brace =
(* label is not needed; paren_pred is enough *)
- ctl_and
- (quantify guard rbfvs (real_make_match None guard rbrace))
- paren_pred in
+ quantify guard rbfvs
+ (ctl_au (make_match empty_rbrace)
+ (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
+ (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
if ends_in_return body
then
(* matching error handling code *)
a goto within the current braces. checking for a goto at every
point in the pattern seems expensive and not worthwhile. *)
let pattern2 =
- let empty_rbrace =
- match Ast.unwrap rbrace with
- Ast.SeqEnd((data,info,_,pos)) ->
- Ast.rewrap rbrace(Ast.SeqEnd(Ast.make_mcode data))
- | _ -> failwith "unexpected close brace" in
let body = preprocess_dots body in (* redo, to drop braces *)
make_seq
[gotopred label;
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 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 ->
(function x ->
statement x Tail new_quantified minus_quantified None
llabel slabel true)
- guard (function x -> Ast.set_fvs [] (Ast.rewrap stmt x)))
+ 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
None llabel slabel true true)
(function x ->
statement x Tail quantified minus_quantified None llabel slabel true)
- guard (function x -> Ast.set_fvs [] (Ast.rewrap stmt x))
+ 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,contains_modif rbrace) with
- ([],[body],false) ->
+ let optim1 =
+ match (Ast.undots body,
+ contains_modif rbrace or contains_pos rbrace) with
+ ([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,_,_) -> Some (Common.Right whencode)
- | _ -> None)
- | _ -> None in
- let body_code =
- match fn_nest with
- Some (Common.Left stmt_dots) ->
- (* special case for function header + body - header is unambiguous
+ Ast.Nest(stmt_dots,[],false,_,_) ->
+ (* 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
+ 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_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
+ (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) ->
+ (* 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.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.WhenModifier(Ast.WhenAny) -> CTL.True
- | Ast.WhenModifier(_) -> prev)
- CTL.True whencode) in
- ctl_au leftarg (make_match stripped_rbrace)]
- | None ->
+ (match d with
+ Ast.MINUS(_,_,_,_) -> None
+ | _ ->
+ Some (
+ 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_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 (make_match stripped_rbrace)]))
+ | _ -> 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(_,_,_,[]) as d),_),[],_,_) ->
+ (match (Ast.unwrap lbrace,Ast.unwrap rbrace) with
+ (Ast.SeqStart((_,_,Ast.MINUS(_,_,_,[]),_)),
+ Ast.SeqEnd((_,_,Ast.MINUS(_,_,_,[]),_)))
+ 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 (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
CTL.And(CTL.NONSTRICT,
CTL.AX(CTL.FORWARD,s,CTL.AU(CTL.FORWARD,s2,e2,e3)),
CTL.EX(CTL.FORWARD,CTL.EU(CTL.FORWARD,e4,e5))))
- | CTL.AX(dir,s,CTL.XX(phi)) -> CTL.EX(dir,CTL.XX(cleanup phi))
+ | CTL.AX(dir,s,CTL.XX(phi)) -> CTL.EX(dir,cleanup phi)
| CTL.EX(dir,CTL.XX((CTL.AU(_,s,_,_)) as phi)) ->
- CTL.AX(dir,s,CTL.XX(cleanup phi))
+ CTL.AX(dir,s,cleanup phi)
| CTL.XX(phi) -> failwith "bad XX"
| CTL.AX(dir,s,phi1) -> CTL.AX(dir,s,cleanup phi1)
| CTL.AG(dir,s,phi1) -> CTL.AG(dir,s,cleanup phi1)
(* --------------------------------------------------------------------- *)
(* 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
+ let quantified = Common.minus_set (Common.union_set ua fuas) pos in
quantify false quantified
(match Ast.unwrap t with
Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
(* --------------------------------------------------------------------- *)
(* 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.CocciRule (a,b,c,_) -> asttoctlz (a,b,c) used_after positions
+ 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]
let pp_cocci_predicate (pred,modif) =
Pretty_print_engine.pp_predicate pred
HCoop / bpt / coccinelle.git / blobdiff