(*
-* Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
-* Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
-* This file is part of Coccinelle.
-*
-* Coccinelle is free software: you can redistribute it and/or modify
-* it under the terms of the GNU General Public License as published by
-* the Free Software Foundation, according to version 2 of the License.
-*
-* Coccinelle is distributed in the hope that it will be useful,
-* but WITHOUT ANY WARRANTY; without even the implied warranty of
-* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-* GNU General Public License for more details.
-*
-* You should have received a copy of the GNU General Public License
-* along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
-*
-* The authors reserve the right to distribute this or future versions of
-* Coccinelle under other licenses.
-*)
+ * Copyright 2010, INRIA, University of Copenhagen
+ * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
+ * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
+ * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
+ * This file is part of Coccinelle.
+ *
+ * Coccinelle is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, according to version 2 of the License.
+ *
+ * Coccinelle is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
+ *
+ * The authors reserve the right to distribute this or future versions of
+ * Coccinelle under other licenses.
+ *)
(* Arities matter for the minus slice, but not for the plus slice. *)
else starter @ ender in
(lst,
{endinfo with Ast0.tline_start = startinfo.Ast0.tline_start}) in
- let attach_bef bef beforeinfo = function
+ let attach_bef bef beforeinfo befit = function
(true,mcl) ->
List.iter
(function
mreplacements := concat bef beforeinfo mrepl tokeninfo
| Ast0.CONTEXT(mbefaft) ->
(match !mbefaft with
- (Ast.BEFORE(mbef),mbeforeinfo,a) ->
+ (Ast.BEFORE(mbef,it),mbeforeinfo,a) ->
let (newbef,newinfo) =
concat bef beforeinfo mbef mbeforeinfo in
- mbefaft := (Ast.BEFORE(newbef),newinfo,a)
- | (Ast.AFTER(maft),_,a) ->
+ let it = Ast.lub_count befit it in
+ mbefaft := (Ast.BEFORE(newbef,it),newinfo,a)
+ | (Ast.AFTER(maft,it),_,a) ->
+ let it = Ast.lub_count befit it in
mbefaft :=
- (Ast.BEFOREAFTER(bef,maft),beforeinfo,a)
- | (Ast.BEFOREAFTER(mbef,maft),mbeforeinfo,a) ->
+ (Ast.BEFOREAFTER(bef,maft,it),beforeinfo,a)
+ | (Ast.BEFOREAFTER(mbef,maft,it),mbeforeinfo,a) ->
let (newbef,newinfo) =
concat bef beforeinfo mbef mbeforeinfo in
+ let it = Ast.lub_count befit it in
mbefaft :=
- (Ast.BEFOREAFTER(newbef,maft),newinfo,a)
+ (Ast.BEFOREAFTER(newbef,maft,it),newinfo,a)
| (Ast.NOTHING,_,a) ->
- mbefaft := (Ast.BEFORE(bef),beforeinfo,a))
+ mbefaft :=
+ (Ast.BEFORE(bef,befit),beforeinfo,a))
| _ -> failwith "unexpected annotation")
mcl
| _ ->
+ Printf.printf "before %s\n" (Dumper.dump bef);
failwith
- "context tree should not have bad code on both sides" in
- let attach_aft aft afterinfo = function
+ "context tree should not have bad code before" in
+ let attach_aft aft afterinfo aftit = function
(true,mcl) ->
List.iter
(function
mreplacements := concat mrepl tokeninfo aft afterinfo
| Ast0.CONTEXT(mbefaft) ->
(match !mbefaft with
- (Ast.BEFORE(mbef),b,_) ->
+ (Ast.BEFORE(mbef,it),b,_) ->
+ let it = Ast.lub_count aftit it in
mbefaft :=
- (Ast.BEFOREAFTER(mbef,aft),b,afterinfo)
- | (Ast.AFTER(maft),b,mafterinfo) ->
+ (Ast.BEFOREAFTER(mbef,aft,it),b,afterinfo)
+ | (Ast.AFTER(maft,it),b,mafterinfo) ->
let (newaft,newinfo) =
concat maft mafterinfo aft afterinfo in
- mbefaft := (Ast.AFTER(newaft),b,newinfo)
- | (Ast.BEFOREAFTER(mbef,maft),b,mafterinfo) ->
+ let it = Ast.lub_count aftit it in
+ mbefaft := (Ast.AFTER(newaft,it),b,newinfo)
+ | (Ast.BEFOREAFTER(mbef,maft,it),b,mafterinfo) ->
let (newaft,newinfo) =
concat maft mafterinfo aft afterinfo in
+ let it = Ast.lub_count aftit it in
mbefaft :=
- (Ast.BEFOREAFTER(mbef,newaft),b,newinfo)
+ (Ast.BEFOREAFTER(mbef,newaft,it),b,newinfo)
| (Ast.NOTHING,b,_) ->
- mbefaft := (Ast.AFTER(aft),b,afterinfo))
+ mbefaft := (Ast.AFTER(aft,aftit),b,afterinfo))
| _ -> failwith "unexpected annotation")
mcl
| _ ->
failwith
- "context tree should not have bad code on both sides" in
+ "context tree should not have bad code after" in
(match !befaft with
- (Ast.BEFORE(bef),beforeinfo,_) ->
- attach_bef bef beforeinfo
+ (Ast.BEFORE(bef,it),beforeinfo,_) ->
+ attach_bef bef beforeinfo it
(einfo.Ast0.attachable_start,einfo.Ast0.mcode_start)
- | (Ast.AFTER(aft),_,afterinfo) ->
- attach_aft aft afterinfo
+ | (Ast.AFTER(aft,it),_,afterinfo) ->
+ attach_aft aft afterinfo it
(einfo.Ast0.attachable_end,einfo.Ast0.mcode_end)
- | (Ast.BEFOREAFTER(bef,aft),beforeinfo,afterinfo) ->
- attach_bef bef beforeinfo
+ | (Ast.BEFOREAFTER(bef,aft,it),beforeinfo,afterinfo) ->
+ attach_bef bef beforeinfo it
(einfo.Ast0.attachable_start,einfo.Ast0.mcode_start);
- attach_aft aft afterinfo
+ attach_aft aft afterinfo it
(einfo.Ast0.attachable_end,einfo.Ast0.mcode_end)
| (Ast.NOTHING,_,_) -> ())
- | Ast0.PLUS -> () in
+ | Ast0.PLUS _ -> () in
V0.flat_combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
mcode mcode
let donothing r k e = k e in
let bind x y = x && y in
let option_default = true in
- let mcode (_,_,_,mc,_) =
+ let mcode (_,_,_,mc,_,_) =
match mc with
Ast0.MINUS(r) -> let (plusses,_) = !r in plusses = []
| _ -> false in
List.for_all r.VT0.combiner_rec_statement_dots statement_dots_list
| _ -> k e in
+ let case_line r k e =
+ match Ast0.unwrap e with
+ Ast0.DisjCase(starter,case_lines,mids,ender) ->
+ List.for_all r.VT0.combiner_rec_case_line case_lines
+ | _ -> k e in
+
V0.flat_combiner bind option_default
mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
mcode mcode
donothing donothing donothing donothing donothing donothing
donothing expression typeC donothing donothing declaration
- statement donothing donothing
+ statement case_line donothing
(* --------------------------------------------------------------------- *)
(* --------------------------------------------------------------------- *)
{ Ast.line = info.Ast0.pos_info.Ast0.line_start;
Ast.column = info.Ast0.pos_info.Ast0.column;
Ast.strbef = strings_to_s info.Ast0.strings_before;
- Ast.straft = strings_to_s info.Ast0.strings_after; }
+ Ast.straft = strings_to_s info.Ast0.strings_after;}
-let convert_mcodekind = function
+let convert_mcodekind adj = function
Ast0.MINUS(replacements) ->
let (replacements,_) = !replacements in
- Ast.MINUS(Ast.NoPos,replacements)
- | Ast0.PLUS -> Ast.PLUS
+ Ast.MINUS(Ast.NoPos,[],adj,replacements)
+ | Ast0.PLUS count -> Ast.PLUS count
| Ast0.CONTEXT(befaft) ->
let (befaft,_,_) = !befaft in Ast.CONTEXT(Ast.NoPos,befaft)
| Ast0.MIXED(_) -> failwith "not possible for mcode"
-let pos_mcode(term,_,info,mcodekind,pos) =
+let pos_mcode(term,_,info,mcodekind,pos,adj) =
(* avoids a recursion problem *)
- (term,convert_info info,convert_mcodekind mcodekind,Ast.NoMetaPos)
+ (term,convert_info info,convert_mcodekind adj mcodekind,Ast.NoMetaPos)
-let mcode(term,_,info,mcodekind,pos) =
+let mcode (term,_,info,mcodekind,pos,adj) =
let pos =
match !pos with
Ast0.MetaPos(pos,constraints,per) ->
Ast.MetaPos(pos_mcode pos,constraints,per,unitary,false)
| _ -> Ast.NoMetaPos in
- (term,convert_info info,convert_mcodekind mcodekind,pos)
+ (term,convert_info info,convert_mcodekind adj mcodekind,pos)
(* --------------------------------------------------------------------- *)
(* Dots *)
and ident i =
rewrap i (do_isos (Ast0.get_iso i))
(match Ast0.unwrap i with
- Ast0.Id(name) -> Ast.Id(mcode name)
- | Ast0.MetaId(name,constraints,_) ->
- let constraints = List.map ident constraints in
- Ast.MetaId(mcode name,constraints,unitary,false)
- | Ast0.MetaFunc(name,constraints,_) ->
- let constraints = List.map ident constraints in
- Ast.MetaFunc(mcode name,constraints,unitary,false)
- | Ast0.MetaLocalFunc(name,constraints,_) ->
- let constraints = List.map ident constraints in
- Ast.MetaLocalFunc(mcode name,constraints,unitary,false)
- | Ast0.OptIdent(id) -> Ast.OptIdent(ident id)
- | Ast0.UniqueIdent(id) -> Ast.UniqueIdent(ident id))
+ Ast0.Id(name) -> Ast.Id(mcode name)
+ | Ast0.MetaId(name,constraints,_) ->
+ Ast.MetaId(mcode name,constraints,unitary,false)
+ | Ast0.MetaFunc(name,constraints,_) ->
+ Ast.MetaFunc(mcode name,constraints,unitary,false)
+ | Ast0.MetaLocalFunc(name,constraints,_) ->
+ Ast.MetaLocalFunc(mcode name,constraints,unitary,false)
+ | Ast0.OptIdent(id) -> Ast.OptIdent(ident id)
+ | Ast0.UniqueIdent(id) -> Ast.UniqueIdent(ident id))
(* --------------------------------------------------------------------- *)
(* Expression *)
| Ast0.SizeOfType(szf,lp,ty,rp) ->
Ast.SizeOfType(mcode szf, mcode lp,typeC ty,mcode rp)
| Ast0.TypeExp(ty) -> Ast.TypeExp(typeC ty)
- | Ast0.MetaErr(name,constraints,_) ->
- let constraints = List.map expression constraints in
- Ast.MetaErr(mcode name,constraints,unitary,false)
- | Ast0.MetaExpr(name,constraints,ty,form,_) ->
- let constraints = List.map expression constraints in
- Ast.MetaExpr(mcode name,constraints,unitary,ty,form,false)
+ | Ast0.MetaErr(name,cstrts,_) ->
+ Ast.MetaErr(mcode name,constraints cstrts,unitary,false)
+ | Ast0.MetaExpr(name,cstrts,ty,form,_) ->
+ Ast.MetaExpr(mcode name,constraints cstrts,unitary,ty,form,false)
| Ast0.MetaExprList(name,Some lenname,_) ->
Ast.MetaExprList(mcode name,Some (mcode lenname,unitary,false),
unitary,false)
| Ast0.MetaExprList(name,None,_) ->
Ast.MetaExprList(mcode name,None,unitary,false)
| Ast0.EComma(cm) -> Ast.EComma(mcode cm)
- | Ast0.DisjExpr(_,exps,_,_) -> Ast.DisjExpr(List.map expression exps)
- | Ast0.NestExpr(_,exp_dots,_,whencode,multi) ->
+ | Ast0.DisjExpr(_,exps,_,_) ->
+ Ast.DisjExpr(List.map expression exps)
+ | Ast0.NestExpr(starter,exp_dots,ender,whencode,multi) ->
+ let starter = mcode starter in
let whencode = get_option expression whencode in
- Ast.NestExpr(dots expression exp_dots,whencode,multi)
+ let ender = mcode ender in
+ Ast.NestExpr(starter,dots expression exp_dots,ender,whencode,multi)
| Ast0.Edots(dots,whencode) ->
let dots = mcode dots in
let whencode = get_option expression whencode in
and expression_dots ed = dots expression ed
+and constraints c =
+ match c with
+ Ast0.NoConstraint -> Ast.NoConstraint
+ | Ast0.NotIdCstrt idctrt -> Ast.NotIdCstrt idctrt
+ | Ast0.NotExpCstrt exps -> Ast.NotExpCstrt (List.map expression exps)
+ | Ast0.SubExpCstrt ids -> Ast.SubExpCstrt ids
+
(* --------------------------------------------------------------------- *)
(* Types *)
(* Initialiser *)
and strip_idots initlist =
+ let isminus mc =
+ match Ast0.get_mcode_mcodekind mc with
+ Ast0.MINUS _ -> true
+ | _ -> false in
match Ast0.unwrap initlist with
Ast0.DOTS(x) ->
- let (whencode,init) =
+ let (whencode,init,dotinfo) =
List.fold_left
- (function (prevwhen,previnit) ->
+ (function (prevwhen,previnit,dotinfo) ->
function cur ->
match Ast0.unwrap cur with
Ast0.Idots(dots,Some whencode) ->
- (whencode :: prevwhen, previnit)
- | Ast0.Idots(dots,None) -> (prevwhen,previnit)
- | _ -> (prevwhen, cur :: previnit))
- ([],[]) x in
- (List.rev whencode, List.rev init)
+ (whencode :: prevwhen, previnit,
+ (isminus dots)::dotinfo)
+ | Ast0.Idots(dots,None) ->
+ (prevwhen, previnit, (isminus dots)::dotinfo)
+ | _ -> (prevwhen, cur :: previnit, dotinfo))
+ ([],[],[]) x in
+ let allminus =
+ if List.for_all (function x -> not x) dotinfo
+ then false (* false if no dots *)
+ else
+ if List.for_all (function x -> x) dotinfo
+ then true
+ else failwith "inconsistent annotations on initialiser list dots" in
+ (List.rev whencode, List.rev init, allminus)
| Ast0.CIRCLES(x) | Ast0.STARS(x) -> failwith "not possible for an initlist"
and initialiser i =
Ast0.MetaInit(name,_) -> Ast.MetaInit(mcode name,unitary,false)
| Ast0.InitExpr(exp) -> Ast.InitExpr(expression exp)
| Ast0.InitList(lb,initlist,rb) ->
- let (whencode,initlist) = strip_idots initlist in
- Ast.InitList(mcode lb,List.map initialiser initlist,mcode rb,
+ let (whencode,initlist,allminus) = strip_idots initlist in
+ Ast.InitList(allminus,mcode lb,List.map initialiser initlist,mcode rb,
List.map initialiser whencode)
| Ast0.InitGccExt(designators,eq,ini) ->
Ast.InitGccExt(List.map designator designators,mcode eq,
(match Ast0.unwrap s with
Ast0.Decl((_,bef),decl) ->
Ast.Atomic(rewrap_rule_elem s
- (Ast.Decl(convert_mcodekind bef,
+ (Ast.Decl(convert_mcodekind (-1) bef,
check_allminus.VT0.combiner_rec_statement s,
declaration decl)))
| Ast0.Seq(lbrace,body,rbrace) ->
let lbrace = mcode lbrace in
- let (decls,body) = separate_decls seqible body in
+ let body = dots (statement seqible) body in
let rbrace = mcode rbrace in
Ast.Seq(iso_tokenwrap lbrace s (Ast.SeqStart(lbrace))
(do_isos (Ast0.get_iso s)),
- decls,body,
+ body,
tokenwrap rbrace s (Ast.SeqEnd(rbrace)))
| Ast0.ExprStatement(exp,sem) ->
Ast.Atomic(rewrap_rule_elem s
(rewrap_rule_elem s
(Ast.IfHeader(mcode iff,mcode lp,expression exp,mcode rp)),
statement Ast.NotSequencible branch,
- ([],[],[],convert_mcodekind aft))
+ ([],[],[],convert_mcodekind (-1) aft))
| Ast0.IfThenElse(iff,lp,exp,rp,branch1,els,branch2,(_,aft)) ->
let els = mcode els in
Ast.IfThenElse
statement Ast.NotSequencible branch1,
tokenwrap els s (Ast.Else(els)),
statement Ast.NotSequencible branch2,
- ([],[],[],convert_mcodekind aft))
+ ([],[],[],convert_mcodekind (-1) aft))
| Ast0.While(wh,lp,exp,rp,body,(_,aft)) ->
Ast.While(rewrap_rule_elem s
(Ast.WhileHeader
(mcode wh,mcode lp,expression exp,mcode rp)),
statement Ast.NotSequencible body,
- ([],[],[],convert_mcodekind aft))
+ ([],[],[],convert_mcodekind (-1) aft))
| Ast0.Do(d,body,wh,lp,exp,rp,sem) ->
let wh = mcode wh in
Ast.Do(rewrap_rule_elem s (Ast.DoHeader(mcode d)),
let body = statement Ast.NotSequencible body in
Ast.For(rewrap_rule_elem s
(Ast.ForHeader(fr,lp,exp1,sem1,exp2,sem2,exp3,rp)),
- body,([],[],[],convert_mcodekind aft))
+ body,([],[],[],convert_mcodekind (-1) aft))
| Ast0.Iterator(nm,lp,args,rp,body,(_,aft)) ->
Ast.Iterator(rewrap_rule_elem s
(Ast.IteratorHeader
dots expression args,
mcode rp)),
statement Ast.NotSequencible body,
- ([],[],[],convert_mcodekind aft))
- | Ast0.Switch(switch,lp,exp,rp,lb,cases,rb) ->
+ ([],[],[],convert_mcodekind (-1) aft))
+ | Ast0.Switch(switch,lp,exp,rp,lb,decls,cases,rb) ->
let switch = mcode switch in
let lp = mcode lp in
let exp = expression exp in
let rp = mcode rp in
let lb = mcode lb in
+ let decls = dots (statement seqible) decls in
let cases = List.map case_line (Ast0.undots cases) in
let rb = mcode rb in
Ast.Switch(rewrap_rule_elem s (Ast.SwitchHeader(switch,lp,exp,rp)),
tokenwrap lb s (Ast.SeqStart(lb)),
- cases,
+ decls,cases,
tokenwrap rb s (Ast.SeqEnd(rb)))
| Ast0.Break(br,sem) ->
Ast.Atomic(rewrap_rule_elem s (Ast.Break(mcode br,mcode sem)))
| Ast0.Disj(_,rule_elem_dots_list,_,_) ->
Ast.Disj(List.map (function x -> statement_dots seqible x)
rule_elem_dots_list)
- | Ast0.Nest(_,rule_elem_dots,_,whn,multi) ->
+ | Ast0.Nest(starter,rule_elem_dots,ender,whn,multi) ->
Ast.Nest
- (statement_dots Ast.Sequencible rule_elem_dots,
+ (mcode starter,statement_dots Ast.Sequencible rule_elem_dots,
+ mcode ender,
List.map
(whencode (statement_dots Ast.Sequencible)
(statement Ast.NotSequencible))
let params = parameter_list params in
let rp = mcode rp in
let lbrace = mcode lbrace in
- let (decls,body) = separate_decls seqible body in
+ let body = dots (statement seqible) body in
let rbrace = mcode rbrace in
let allminus = check_allminus.VT0.combiner_rec_statement s in
Ast.FunDecl(rewrap_rule_elem s
- (Ast.FunHeader(convert_mcodekind bef,
+ (Ast.FunHeader(convert_mcodekind (-1) bef,
allminus,fi,name,lp,params,rp)),
tokenwrap lbrace s (Ast.SeqStart(lbrace)),
- decls,body,
+ body,
tokenwrap rbrace s (Ast.SeqEnd(rbrace)))
| Ast0.Include(inc,str) ->
Ast.Atomic(rewrap_rule_elem s (Ast.Include(mcode inc,mcode str)))
| Ast0.CIRCLES(x) -> Ast.CIRCLES(process_list seqible isos x)
| Ast0.STARS(x) -> Ast.STARS(process_list seqible isos x))
+ (* the following is no longer used.
+ the goal was to let one put a statement at the very beginning of a function
+ pattern and have it skip over the declarations in the C code.
+ that feature was removed a long time ago, however, in favor of
+ ... when != S, which also causes whatever comes after it to match the
+ first real statement.
+ the separation of declarations from the rest of the body means that the
+ quantifier of any variable shared between them comes out too high, posing
+ problems when there is ... decl ... stmt, as the quantifier of any shared
+ variable will be around the whole thing, making variables not free enough
+ in the first ..., and thus not implementing the expected shortest path
+ condition. example: f() { ... int A; ... foo(A); }.
+ the quantifier for A should start just before int A, not at the top of the
+ function.
and separate_decls seqible d =
let rec collect_decls = function
[] -> ([],[])
match Ast0.unwrap d with
Ast0.DOTS(x) -> process x d (function x -> Ast.DOTS x)
| Ast0.CIRCLES(x) -> process x d (function x -> Ast.CIRCLES x)
- | Ast0.STARS(x) -> process x d (function x -> Ast.STARS x) in
+ | Ast0.STARS(x) -> process x d (function x -> Ast.STARS x) *) in
statement Ast.Sequencible s
let colon = mcode colon in
let code = dots statement code in
Ast.CaseLine(rewrap c no_isos (Ast.Case(case,exp,colon)),code)
+ | Ast0.DisjCase(_,case_lines,_,_) ->
+ failwith "not supported"
+ (*Ast.CaseLine(Ast.DisjRuleElem(List.map case_line case_lines))*)
+
| Ast0.OptCase(case) -> Ast.OptCase(case_line case))
and statement_dots l = dots statement l
HCoop / bpt / coccinelle.git / blobdiff