(*
-* 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 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
+ * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
+ * This file is part of Coccinelle.
+ *
+ * Coccinelle is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, according to version 2 of the License.
+ *
+ * Coccinelle is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * The authors reserve the right to distribute this or future versions of
+ * Coccinelle under other licenses.
+ *)
+
+
+(*
+ * Copyright 2005-2010, 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 *)
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
let mcode r (_,_,kind,metapos) =
match kind with
Ast.MINUS(_,_,_,_) -> true
- | Ast.PLUS -> failwith "not possible"
+ | 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 make_raw_match label guard code =
predmaker guard (Lib_engine.Match(code),CTL.Control) label
-
+
let rec seq_fvs quantified = function
[] -> []
| fv1::fvs ->
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 =
| _ -> true)
| _ -> true)
a in*)
- (Ast.rewrap s (Ast.Nest(sd,w,multi,a,aft)),[Ast.Other_dots stmt_dots])
+ (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
| 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.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)),[])
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 =
| _ -> true)
| _ -> true)
a in*)
- (Ast.rewrap s (Ast.Nest(sd,w,multi,bef,a)),[Ast.Other_dots stmt_dots])
+ (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.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])
+ 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)),[])
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
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
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
[inlooppred None;
recurse body Tail new_quantified new_mquantified
(Some (lv,used)) (Some (lv,used)) None guard] in
- let after_pred = fallpred None in
+ let after_pred = loopfallpred None in
let or_cases after_branch = ctl_or body after_branch in
let (header,wrapper) =
if !used
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 stmt_fvs = Ast.get_fvs stmt in
- let fvs = get_unquantified quantified stmt_fvs in
- let (new_fvs,body) =
+ let ender =
match (d,after) with
- (Ast.CONTEXT(pos,Ast.NOTHING),(Tail|End|VeryEnd)) ->
+ (Ast.PLUS _, _) -> failwith "not possible"
+ | (Ast.CONTEXT(pos,Ast.NOTHING),(Tail|End|VeryEnd)) ->
(* just match the root. don't care about label; always ok *)
- (fvs,function f -> f(make_raw_match None false ast))
- | (Ast.MINUS(pos,inst,adj,[]),(Tail|End|VeryEnd)) ->
- (* 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. *)
- let ender =
- 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) in
- (label_var::fvs,
- function f -> ctl_and CTL.NONSTRICT label_pred (f ender))
- | _ ->
- (* more safe but less efficient *)
+ 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,inst,adj,_) -> Ast.MINUS(pos,inst,adj,[])
- | 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
- let ender =
- ctl_and CTL.NONSTRICT (make_raw_match label false ast)
+ (* 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
- [first_metamatch;
- ctl_au CTL.NONSTRICT rest_nodes last_node]) in
- (label_var::fvs,
- function f -> ctl_and CTL.NONSTRICT label_pred (f ender)) in
- quantify guard new_fvs
+ [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
+ quantify guard (label_var::fvs)
(sequencibility body label_pred process_bef_aft seqible)
(* --------------------------------------------------------------------- *)
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_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
| Common.Right stop_early ->
CTL.Let(v,y,
ctl_or (CTL.Ref v)
- (stop_early n (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 =
CTL.Pred(Lib_engine.BindGood(plus_var),
CTL.Modif plus_var2)))
else x in
- let body =
+ let body =
CTL.Let(v,nest,
CTL.Or(is_plus (CTL.Ref v),
whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
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
plus_modifier
(dots_au is_strict ((after = Tail) or (after = VeryEnd))
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)
+ (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 (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 (fallpred label)
+ (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 *)
-
+
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
when !Flag.sgrep_mode2 ->
(* in sgrep mode, we can propagate the - *)
Some (Ast.MINUS(Ast.NoPos,inst1,adj1,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)))
+ | (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.AFTER(l,c))) ->
+ Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l,c)))
| _ -> None in
let ret = Ast.make_mcode "return" in
let edots =
(quantify guard b1fvs
(make_seq
[start_brace;
- 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
+ (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 *)
| 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
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 *)
(* 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
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)
(function 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,
Common.union_set mb1fvs
(Common.union_set mb2fvs
(Common.union_set mb3fvs minus_quantified)) in
+ 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) ->
(match Ast.unwrap body with
- Ast.Nest(stmt_dots,[],false,_,_) ->
+ 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 *)
(* function body is all minus, no whencode *)
match Ast.undots body with
[body] ->
- (match Ast.unwrap body with
+ (match Ast.unwrap body with
Ast.Dots
((_,i,(Ast.MINUS(_,_,_,[]) as d),_),[],_,_) ->
(match (Ast.unwrap lbrace,Ast.unwrap rbrace) with
(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
HCoop / bpt / coccinelle.git / blobdiff