(*
+ * 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.
| (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
Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l)
| Ast.CIRCLES(l) -> failwith "elimopt: not supported"
| Ast.STARS(l) -> failwith "elimopt: not supported") in
-
+
V.rebuilder
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
- donothing donothing stmtdotsfn donothing
+ donothing donothing stmtdotsfn donothing donothing
donothing donothing donothing donothing donothing donothing donothing
donothing donothing donothing donothing donothing
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
[] -> []
| fv1::fvs ->
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")
let fvs = get_unquantified quantified stmt_fvs in
quantify guard fvs (make_match None guard x) in
(* label used to be used here, but it is not use; label is only needed after
-and within dots
+and within dots
ctl_and CTL.NONSTRICT (label_pred_maker label) *)
(match List.map Ast.unwrap res with
[] -> failwith "unexpected empty disj"
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
quantify guard efvs (make_match header)
| _ -> process())
| _ -> process()
-
+
(* --------------------------------------------------------------------- *)
(* statement metavariables *)
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_and CTL.NONSTRICT
(ctl_ex
(make_seq guard
[to_end; make_seq_after guard last_metamatch after]))
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
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))))
(* --------------------------------------------------------------------- *)
(* the main translation loop *)
-
+
let rec statement_list stmt_list after quantified minus_quantified
label llabel slabel dots_before guard =
let isdots x =
| 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 *)
+ 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 =
(* 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