(*
- * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
+ * 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.
*
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)
| (Ast.Dots(_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
d0::s::d1::rest)
- | (Ast.Nest(_,_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest,
+ | (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
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
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
bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
| Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) 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 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
[] -> []
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 =
| _ -> 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
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")
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 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 (loopfallpred 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))))
(* --------------------------------------------------------------------- *)
let (lbfvs,b1fvs,b2fvs,rbfvs) =
match
seq_fvs quantified
- [Ast.get_fvs lbrace;
- Ast.get_fvs body;Ast.get_fvs rbrace]
+ [Ast.get_fvs lbrace;Ast.get_fvs body;Ast.get_fvs rbrace]
with
- [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] ->
- (lbfvs,b1fvs,b2fvs,rbfvs)
+ [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] -> (lbfvs,b1fvs,b2fvs,rbfvs)
| _ -> failwith "not possible" in
let (mlbfvs,mb1fvs,mb2fvs,mrbfvs) =
match
seq_fvs minus_quantified
- [Ast.get_mfvs lbrace;
- Ast.get_mfvs body;Ast.get_mfvs rbrace]
+ [Ast.get_mfvs lbrace;Ast.get_mfvs body;Ast.get_mfvs rbrace]
with
[(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] ->
(lbfvs,b1fvs,b2fvs,rbfvs)
(* 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_mquantified2 =
new_quantified2 new_mquantified2
(Some (lv,ref true))
llabel slabel false guard)))])) in
- if ends_in_return body
+ 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:
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)))
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 *)
(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
- [start_brace;
+ [ctl_and start_brace paren_pred;
match whencode with
[] -> CTL.True
| _ ->
CTL.True
| Ast.WhenModifier(_) -> prev)
CTL.True whencode) in
- ctl_au leftarg (make_match stripped_rbrace)]))
+ ctl_au leftarg
+ (ctl_and
+ (make_match stripped_rbrace)
+ paren_pred)]))
| _ -> None)
| _ -> None in
let optim2 =
HCoop / bpt / coccinelle.git / blobdiff