parsing_cocci/unify_ast.ml

   1 (*
   2  * Copyright 2010, INRIA, University of Copenhagen
   3  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
   4  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
   5  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
   6  * This file is part of Coccinelle.
   7  *
   8  * Coccinelle is free software: you can redistribute it and/or modify
   9  * it under the terms of the GNU General Public License as published by
  10  * the Free Software Foundation, according to version 2 of the License.
  11  *
  12  * Coccinelle is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  19  *
  20  * The authors reserve the right to distribute this or future versions of
  21  * Coccinelle under other licenses.
  22  *)
  23
  24
  25 (* --------------------------------------------------------------------- *)
  26 (* Given two patterns, A and B, determine whether B can match any matched
  27 subterms of A.  For simplicity, this doesn't maintain an environment; it
  28 just assume metavariables match.  Thus the result is either NO or MAYBE. *)
  29
  30 module Ast = Ast_cocci
  31 module V = Visitor_ast
  32
  33 (* --------------------------------------------------------------------- *)
  34
  35 type res = NO | MAYBE
  36
  37 let return b = if b then MAYBE else NO
  38
  39 let unify_mcode (x,_,_,_) (y,_,_,_) = x = y
  40
  41 let ret_unify_mcode a b = return (unify_mcode a b)
  42
  43 let unify_option f t1 t2 =
  44   match (t1,t2) with
  45     (Some t1, Some t2) -> f t1 t2
  46   | (None, None) -> return true
  47   | _ -> return false
  48
  49 let unify_true_option f t1 t2 =
  50   match (t1,t2) with
  51     (Some t1, Some t2) -> f t1 t2
  52   | (None, None) -> return true
  53   | _ -> return true
  54
  55 let bool_unify_option f t1 t2 =
  56   match (t1,t2) with
  57     (Some t1, Some t2) -> f t1 t2
  58   | (None, None) -> true
  59   | _ -> false
  60
  61 let conjunct_bindings b1 b2 =
  62   match b1 with NO -> b1 | MAYBE -> b2
  63
  64 let disjunct_bindings b1 b2 =
  65   match b1 with MAYBE -> b1 | NO -> b2
  66
  67 let disjunct_all_bindings = List.fold_left disjunct_bindings NO
  68
  69 (* --------------------------------------------------------------------- *)
  70
  71 (* compute the common prefix.  if in at least one case, this ends with the
  72 end of the pattern or a ..., then return true. *)
  73
  74 let unify_lists fn dfn la lb =
  75   let rec loop = function
  76       ([],_) | (_,[]) -> return true
  77     | (cura::resta,curb::restb) ->
  78         (match fn cura curb with
  79           MAYBE -> loop (resta,restb)
  80         | NO -> if dfn cura or dfn curb then MAYBE else NO) in
  81   loop (la,lb)
  82
  83 let unify_dots fn dfn d1 d2 =
  84   match (Ast.unwrap d1,Ast.unwrap d2) with
  85     (Ast.DOTS(l1),Ast.DOTS(l2))
  86   | (Ast.CIRCLES(l1),Ast.CIRCLES(l2))
  87   | (Ast.STARS(l1),Ast.STARS(l2)) -> unify_lists fn dfn l1 l2
  88   | _ -> return false
  89
  90 let edots e =
  91   match Ast.unwrap e with
  92     Ast.Edots(_,_) | Ast.Ecircles(_,_) | Ast.Estars(_,_) -> true
  93   | _ -> false
  94
  95 let ddots e =
  96   match Ast.unwrap e with
  97     Ast.Ddots(_,_) -> true
  98   | _ -> false
  99
 100 let pdots p =
 101   match Ast.unwrap p with
 102     Ast.Pdots(_) | Ast.Pcircles(_) -> true
 103   | _ -> false
 104
 105 let dpdots e =
 106   match Ast.unwrap e with
 107     Ast.DPdots(_) | Ast.DPcircles(_) -> true
 108   | _ -> false
 109
 110 let sdots s =
 111   match Ast.unwrap s with
 112     Ast.Dots(_,_,_,_) | Ast.Circles(_,_,_,_) | Ast.Stars(_,_,_,_) -> true
 113   | _ -> false
 114
 115 let idots e =
 116   match Ast.unwrap e with
 117     Ast.Idots(_,_) -> true
 118   | _ -> false
 119
 120 (* --------------------------------------------------------------------- *)
 121 (* Identifier *)
 122
 123 and unify_ident i1 i2 =
 124   match (Ast.unwrap i1,Ast.unwrap i2) with
 125     (Ast.Id(i1),Ast.Id(i2)) -> return (unify_mcode i1 i2)
 126
 127   | (Ast.MetaId(_,_,_,_),_)
 128   | (Ast.MetaFunc(_,_,_,_),_)
 129   | (Ast.MetaLocalFunc(_,_,_,_),_)
 130   | (_,Ast.MetaId(_,_,_,_))
 131   | (_,Ast.MetaFunc(_,_,_,_))
 132   | (_,Ast.MetaLocalFunc(_,_,_,_)) -> return true
 133
 134   | (Ast.OptIdent(_),_)
 135   | (Ast.UniqueIdent(_),_)
 136   | (_,Ast.OptIdent(_))
 137   | (_,Ast.UniqueIdent(_)) -> failwith "unsupported ident"
 138
 139 (* --------------------------------------------------------------------- *)
 140 (* Expression *)
 141
 142 let rec unify_expression e1 e2 =
 143   match (Ast.unwrap e1,Ast.unwrap e2) with
 144     (Ast.Ident(i1),Ast.Ident(i2)) -> unify_ident i1 i2
 145   | (Ast.Constant(c1),Ast.Constant(c2))-> return (unify_mcode c1 c2)
 146   | (Ast.FunCall(f1,lp1,args1,rp1),Ast.FunCall(f2,lp2,args2,rp2)) ->
 147       conjunct_bindings
 148         (unify_expression f1 f2)
 149         (unify_dots unify_expression edots args1 args2)
 150   | (Ast.Assignment(l1,op1,r1,_),Ast.Assignment(l2,op2,r2,_)) ->
 151       if unify_mcode op1 op2
 152       then conjunct_bindings (unify_expression l1 l2) (unify_expression r1 r2)
 153       else return false
 154   | (Ast.CondExpr(tst1,q1,thn1,c1,els1),Ast.CondExpr(tst2,q2,thn2,c2,els2)) ->
 155       conjunct_bindings (unify_expression tst1 tst2)
 156         (conjunct_bindings (unify_option unify_expression thn1 thn2)
 157            (unify_expression els1 els2))
 158   | (Ast.Postfix(e1,op1),Ast.Postfix(e2,op2)) ->
 159       if unify_mcode op1 op2 then unify_expression e1 e2 else return false
 160   | (Ast.Infix(e1,op1),Ast.Infix(e2,op2)) ->
 161       if unify_mcode op1 op2 then unify_expression e1 e2 else return false
 162   | (Ast.Unary(e1,op1),Ast.Unary(e2,op2)) ->
 163       if unify_mcode op1 op2 then unify_expression e1 e2 else return false
 164   | (Ast.Binary(l1,op1,r1),Ast.Binary(l2,op2,r2)) ->
 165       if unify_mcode op1 op2
 166       then conjunct_bindings (unify_expression l1 l2) (unify_expression r1 r2)
 167       else return false
 168   | (Ast.ArrayAccess(ar1,lb1,e1,rb1),Ast.ArrayAccess(ar2,lb2,e2,rb2)) ->
 169       conjunct_bindings (unify_expression ar1 ar2) (unify_expression e1 e2)
 170   | (Ast.RecordAccess(e1,d1,fld1),Ast.RecordAccess(e2,d2,fld2)) ->
 171       conjunct_bindings (unify_expression e1 e2) (unify_ident fld1 fld2)
 172   | (Ast.RecordPtAccess(e1,pt1,fld1),Ast.RecordPtAccess(e2,pt2,fld2)) ->
 173       conjunct_bindings (unify_expression e1 e2) (unify_ident fld1 fld2)
 174   | (Ast.Cast(lp1,ty1,rp1,e1),Ast.Cast(lp2,ty2,rp2,e2)) ->
 175       conjunct_bindings (unify_fullType ty1 ty2) (unify_expression e1 e2)
 176   | (Ast.SizeOfExpr(szf1,e1),Ast.SizeOfExpr(szf2,e2)) ->
 177       unify_expression e1 e2
 178   | (Ast.SizeOfType(szf1,lp1,ty1,rp1),Ast.SizeOfType(szf2,lp2,ty2,rp2)) ->
 179       unify_fullType ty1 ty2
 180   | (Ast.TypeExp(ty1),Ast.TypeExp(ty2)) -> unify_fullType ty1 ty2
 181   | (Ast.Paren(lp1,e1,rp1),Ast.Paren(lp2,e2,rp2)) ->
 182       unify_expression e1 e2
 183
 184   | (Ast.MetaErr(_,_,_,_),_)
 185   | (Ast.MetaExpr(_,_,_,_,_,_),_)
 186   | (Ast.MetaExprList(_,_,_,_),_)
 187   | (_,Ast.MetaErr(_,_,_,_))
 188   | (_,Ast.MetaExpr(_,_,_,_,_,_))
 189   | (_,Ast.MetaExprList(_,_,_,_)) -> return true
 190
 191   | (Ast.EComma(cm1),Ast.EComma(cm2)) -> return true
 192
 193   | (Ast.DisjExpr(e1),_) ->
 194       disjunct_all_bindings (List.map (function x -> unify_expression x e2) e1)
 195   | (_,Ast.DisjExpr(e2)) ->
 196       disjunct_all_bindings (List.map (function x -> unify_expression e1 x) e2)
 197   | (Ast.NestExpr(_,e1,_,_,_),Ast.NestExpr(_,e2,_,_,_)) ->
 198       unify_dots unify_expression edots e1 e2
 199
 200   (* dots can match against anything.  return true to be safe. *)
 201   | (Ast.Edots(_,_),_) | (_,Ast.Edots(_,_))
 202   | (Ast.Ecircles(_,_),_) | (_,Ast.Ecircles(_,_))
 203   | (Ast.Estars(_,_),_) | (_,Ast.Estars(_,_)) -> return true
 204
 205   | (Ast.OptExp(_),_)
 206   | (Ast.UniqueExp(_),_)
 207   | (_,Ast.OptExp(_))
 208   | (_,Ast.UniqueExp(_)) -> failwith "unsupported expression"
 209   | _ -> return false
 210
 211 (* --------------------------------------------------------------------- *)
 212 (* Types *)
 213
 214 and unify_fullType ft1 ft2 =
 215   match (Ast.unwrap ft1,Ast.unwrap ft2) with
 216     (Ast.Type(cv1,ty1),Ast.Type(cv2,ty2)) ->
 217       if bool_unify_option unify_mcode cv1 cv2
 218       then unify_typeC ty1 ty2
 219       else return false
 220   | (Ast.DisjType(ft1),_) ->
 221       disjunct_all_bindings (List.map (function x -> unify_fullType x ft2) ft1)
 222   | (_,Ast.DisjType(ft2)) ->
 223       disjunct_all_bindings (List.map (function x -> unify_fullType ft1 x) ft2)
 224
 225   | (Ast.OptType(_),_)
 226   | (Ast.UniqueType(_),_)
 227   | (_,Ast.OptType(_))
 228   | (_,Ast.UniqueType(_)) -> failwith "unsupported type"
 229
 230 and unify_typeC t1 t2 =
 231   match (Ast.unwrap t1,Ast.unwrap t2) with
 232     (Ast.BaseType(ty1,stringsa),Ast.BaseType(ty2,stringsb)) ->
 233       if ty1 = ty2
 234       then
 235         unify_lists ret_unify_mcode (function _ -> false (* not dots*))
 236           stringsa stringsb
 237       else return false
 238   | (Ast.SignedT(sgn1,ty1),Ast.SignedT(sgn2,ty2)) ->
 239       if unify_mcode sgn1 sgn2
 240       then unify_option unify_typeC ty1 ty2
 241       else return false
 242   | (Ast.Pointer(ty1,s1),Ast.Pointer(ty2,s2)) -> unify_fullType ty1 ty2
 243   | (Ast.FunctionPointer(tya,lp1a,stara,rp1a,lp2a,paramsa,rp2a),
 244      Ast.FunctionPointer(tyb,lp1b,starb,rp1b,lp2b,paramsb,rp2b)) ->
 245        if List.for_all2 unify_mcode
 246            [lp1a;stara;rp1a;lp2a;rp2a] [lp1b;starb;rp1b;lp2b;rp2b]
 247        then
 248          conjunct_bindings (unify_fullType tya tyb)
 249            (unify_dots unify_parameterTypeDef pdots paramsa paramsb)
 250        else return false
 251   | (Ast.FunctionType(_,tya,lp1a,paramsa,rp1a),
 252      Ast.FunctionType(_,tyb,lp1b,paramsb,rp1b)) ->
 253        if List.for_all2 unify_mcode [lp1a;rp1a] [lp1b;rp1b]
 254        then
 255          conjunct_bindings (unify_option unify_fullType tya tyb)
 256            (unify_dots unify_parameterTypeDef pdots paramsa paramsb)
 257        else return false
 258   | (Ast.FunctionType _ , _) -> failwith "not supported"
 259   | (Ast.Array(ty1,lb1,e1,rb1),Ast.Array(ty2,lb2,e2,rb2)) ->
 260       conjunct_bindings
 261         (unify_fullType ty1 ty2) (unify_option unify_expression e1 e2)
 262   | (Ast.EnumName(s1,Some ts1),Ast.EnumName(s2,Some ts2)) ->
 263       if unify_mcode s1 s2 then unify_ident ts1 ts2 else return false
 264   | (Ast.EnumName(s1,None),Ast.EnumName(s2,None)) ->
 265       return true
 266   | (Ast.EnumDef(ty1,lb1,ids1,rb1),Ast.EnumDef(ty2,lb2,ids2,rb2)) ->
 267        conjunct_bindings (unify_fullType ty1 ty2)
 268          (unify_dots unify_expression edots ids1 ids2)
 269   | (Ast.StructUnionName(s1,Some ts1),Ast.StructUnionName(s2,Some ts2)) ->
 270       if unify_mcode s1 s2 then unify_ident ts1 ts2 else return false
 271   | (Ast.StructUnionName(s1,None),Ast.StructUnionName(s2,None)) ->
 272       return (unify_mcode s1 s2)
 273   | (Ast.StructUnionDef(ty1,lb1,decls1,rb1),
 274      Ast.StructUnionDef(ty2,lb2,decls2,rb2)) ->
 275        conjunct_bindings (unify_fullType ty1 ty2)
 276          (unify_dots unify_declaration ddots decls1 decls2)
 277   | (Ast.TypeName(t1),Ast.TypeName(t2)) -> return (unify_mcode t1 t2)
 278
 279   | (Ast.MetaType(_,_,_),_)
 280   | (_,Ast.MetaType(_,_,_)) -> return true
 281   | _ -> return false
 282
 283 (* --------------------------------------------------------------------- *)
 284 (* Variable declaration *)
 285 (* Even if the Cocci program specifies a list of declarations, they are
 286    split out into multiple declarations of a single variable each. *)
 287
 288 and unify_declaration d1 d2 =
 289   match (Ast.unwrap d1,Ast.unwrap d2) with
 290     (Ast.MetaDecl(_,_,_),_) | (_,Ast.MetaDecl(_,_,_)) -> return true
 291   | (Ast.MetaField(_,_,_),_) | (_,Ast.MetaField(_,_,_)) -> return true
 292   | (Ast.Init(stg1,ft1,id1,eq1,i1,s1),Ast.Init(stg2,ft2,id2,eq2,i2,s2)) ->
 293       if bool_unify_option unify_mcode stg1 stg2
 294       then
 295         conjunct_bindings (unify_fullType ft1 ft2)
 296           (conjunct_bindings (unify_ident id1 id2) (unify_initialiser i1 i2))
 297       else return false
 298   | (Ast.UnInit(stg1,ft1,id1,s1),Ast.UnInit(stg2,ft2,id2,s2)) ->
 299       if bool_unify_option unify_mcode stg1 stg2
 300       then conjunct_bindings (unify_fullType ft1 ft2) (unify_ident id1 id2)
 301       else return false
 302   | (Ast.MacroDecl(n1,lp1,args1,rp1,sem1),
 303      Ast.MacroDecl(n2,lp2,args2,rp2,sem2)) ->
 304        conjunct_bindings (unify_ident n1 n2)
 305          (unify_dots unify_expression edots args1 args2)
 306   | (Ast.TyDecl(ft1,s1),Ast.TyDecl(ft2,s2)) -> unify_fullType ft1 ft2
 307   | (Ast.Typedef(stg1,ft1,id1,s1),Ast.Typedef(stg2,ft2,id2,s2)) ->
 308       conjunct_bindings (unify_fullType ft1 ft2) (unify_typeC id1 id2)
 309   | (Ast.DisjDecl(d1),_) ->
 310       disjunct_all_bindings
 311         (List.map (function x -> unify_declaration x d2) d1)
 312   | (_,Ast.DisjDecl(d2)) ->
 313       disjunct_all_bindings
 314         (List.map (function x -> unify_declaration d1 x) d2)
 315   (* dots can match against anything.  return true to be safe. *)
 316   | (Ast.Ddots(_,_),_) | (_,Ast.Ddots(_,_)) -> return true
 317
 318   | (Ast.OptDecl(_),_)
 319   | (Ast.UniqueDecl(_),_)
 320   | (_,Ast.OptDecl(_))
 321   | (_,Ast.UniqueDecl(_)) -> failwith "unsupported decl"
 322   | _ -> return false
 323
 324 (* --------------------------------------------------------------------- *)
 325 (* Initializer *)
 326
 327 and unify_initialiser i1 i2 =
 328   match (Ast.unwrap i1,Ast.unwrap i2) with
 329     (Ast.MetaInit(_,_,_),_) | (_,Ast.MetaInit(_,_,_)) -> return true
 330   | (Ast.InitExpr(expa),Ast.InitExpr(expb)) ->
 331       unify_expression expa expb
 332   | (Ast.ArInitList(_,initlista,_),
 333      Ast.ArInitList(_,initlistb,_)) ->
 334       (* ignore whencode - returns true safely *)
 335       unify_dots unify_initialiser idots initlista initlistb
 336   | (Ast.StrInitList(_,_,initlista,_,whena),
 337      Ast.StrInitList(_,_,initlistb,_,whenb)) ->
 338       (* ignore whencode - returns true safely *)
 339       unify_lists unify_initialiser (function _ -> false) initlista initlistb
 340   | (Ast.InitGccExt(designatorsa,_,inia),
 341      Ast.InitGccExt(designatorsb,_,inib)) ->
 342        conjunct_bindings
 343          (unify_lists unify_designator (function _ -> false)
 344             designatorsa designatorsb)
 345          (unify_initialiser inia inib)
 346   | (Ast.InitGccName(namea,_,inia),Ast.InitGccName(nameb,_,inib)) ->
 347       conjunct_bindings (unify_ident namea nameb) (unify_initialiser inia inib)
 348
 349   | (Ast.OptIni(_),_)
 350   | (Ast.UniqueIni(_),_)
 351   | (_,Ast.OptIni(_))
 352   | (_,Ast.UniqueIni(_)) -> failwith "unsupported decl"
 353   | _ -> return false
 354
 355 and unify_designator d1 d2 =
 356   match (d1,d2) with
 357     (Ast.DesignatorField(_,idb),Ast.DesignatorField(_,ida)) ->
 358       unify_ident ida idb
 359   | (Ast.DesignatorIndex(_,expa,_),Ast.DesignatorIndex(_,expb,_)) ->
 360       unify_expression expa expb
 361   | (Ast.DesignatorRange(_,mina,_,maxa,_),
 362      Ast.DesignatorRange(_,minb,_,maxb,_)) ->
 363        conjunct_bindings (unify_expression mina minb)
 364          (unify_expression maxa maxb)
 365   | _ -> return false
 366
 367 (* --------------------------------------------------------------------- *)
 368 (* Parameter *)
 369
 370 and unify_parameterTypeDef p1 p2 =
 371   match (Ast.unwrap p1,Ast.unwrap p2) with
 372     (Ast.VoidParam(ft1),Ast.VoidParam(ft2)) -> unify_fullType ft1 ft2
 373   | (Ast.Param(ft1,i1),Ast.Param(ft2,i2)) ->
 374       conjunct_bindings (unify_fullType ft1 ft2)
 375         (unify_option unify_ident i1 i2)
 376
 377   | (Ast.MetaParam(_,_,_),_)
 378   | (Ast.MetaParamList(_,_,_,_),_)
 379   | (_,Ast.MetaParam(_,_,_))
 380   | (_,Ast.MetaParamList(_,_,_,_)) -> return true
 381
 382   | (Ast.PComma(_),Ast.PComma(_)) -> return true
 383
 384   (* dots can match against anything.  return true to be safe. *)
 385   | (Ast.Pdots(_),_) | (_,Ast.Pdots(_))
 386   | (Ast.Pcircles(_),_) | (_,Ast.Pcircles(_)) -> return true
 387
 388   | (Ast.OptParam(_),_)
 389   | (Ast.UniqueParam(_),_)
 390   | (_,Ast.OptParam(_))
 391   | (_,Ast.UniqueParam(_)) -> failwith "unsupported parameter"
 392   | _ -> return false
 393
 394 (* --------------------------------------------------------------------- *)
 395 (* Define parameter *)
 396
 397 and unify_define_parameters p1 p2 =
 398  match (Ast.unwrap p1,Ast.unwrap p2) with
 399     (Ast.NoParams,Ast.NoParams) -> return true
 400   | (Ast.DParams(lp1,params1,rp1),Ast.DParams(lp2,params2,rp2)) ->
 401       unify_dots unify_define_param dpdots params1 params2
 402   | _ -> return false
 403
 404 and unify_define_param p1 p2 =
 405   match (Ast.unwrap p1,Ast.unwrap p2) with
 406     (Ast.DParam(i1),Ast.DParam(i2)) ->
 407         (unify_ident i1 i2)
 408   | (Ast.DPComma(_),Ast.DPComma(_)) -> return true
 409
 410   (* dots can match against anything.  return true to be safe. *)
 411   | (Ast.DPdots(_),_) | (_,Ast.DPdots(_))
 412   | (Ast.DPcircles(_),_) | (_,Ast.DPcircles(_)) -> return true
 413
 414   | (Ast.OptDParam(_),_)
 415   | (Ast.UniqueDParam(_),_)
 416   | (_,Ast.OptDParam(_))
 417   | (_,Ast.UniqueDParam(_)) -> failwith "unsupported parameter"
 418   | _ -> return false
 419
 420 (* --------------------------------------------------------------------- *)
 421 (* Top-level code *)
 422
 423 and unify_rule_elem re1 re2 =
 424   match (Ast.unwrap re1,Ast.unwrap re2) with
 425     (Ast.FunHeader(_,_,fi1,nm1,lp1,params1,rp1),
 426      Ast.FunHeader(_,_,fi2,nm2,lp2,params2,rp2)) ->
 427        conjunct_bindings (unify_fninfo fi1 fi2)
 428          (conjunct_bindings (unify_ident nm1 nm2)
 429             (unify_dots unify_parameterTypeDef pdots params1 params2))
 430   | (Ast.Decl(_,_,d1),Ast.Decl(_,_,d2)) -> unify_declaration d1 d2
 431
 432   | (Ast.SeqStart(lb1),Ast.SeqStart(lb2)) -> return true
 433   | (Ast.SeqEnd(rb1),Ast.SeqEnd(rb2)) -> return true
 434
 435   | (Ast.ExprStatement(e1,s1),Ast.ExprStatement(e2,s2)) ->
 436       unify_expression e1 e2
 437   | (Ast.IfHeader(if1,lp1,e1,rp1),Ast.IfHeader(if2,lp2,e2,rp2)) ->
 438       unify_expression e1 e2
 439   | (Ast.Else(e1),Ast.Else(e2)) -> return true
 440   | (Ast.WhileHeader(wh1,lp1,e1,rp1),Ast.WhileHeader(wh2,lp2,e2,rp2)) ->
 441       unify_expression e1 e2
 442   | (Ast.DoHeader(d1),Ast.DoHeader(d2)) -> return true
 443   | (Ast.WhileTail(wh1,lp1,e1,rp1,s1),Ast.WhileTail(wh2,lp2,e2,rp2,s2)) ->
 444       unify_expression e1 e2
 445   | (Ast.ForHeader(fr1,lp1,e11,s11,e21,s21,e31,rp1),
 446      Ast.ForHeader(fr2,lp2,e12,s12,e22,s22,e32,rp2)) ->
 447        conjunct_bindings
 448          (unify_option unify_expression e11 e12)
 449          (conjunct_bindings
 450             (unify_option unify_expression e21 e22)
 451             (unify_option unify_expression e31 e32))
 452   | (Ast.IteratorHeader(nm1,lp1,args1,rp1),
 453      Ast.IteratorHeader(nm2,lp2,args2,rp2)) ->
 454       conjunct_bindings (unify_ident nm1 nm2)
 455          (unify_dots unify_expression edots args1 args2)
 456   | (Ast.Undef(_,n1),Ast.Undef(_,n2)) -> unify_ident n1 n2
 457   | (Ast.DefineHeader(_,n1,p1),Ast.DefineHeader(_,n2,p2)) ->
 458       conjunct_bindings (unify_ident n1 n2)
 459         (unify_define_parameters p1 p2)
 460   | (Ast.Break(r1,s1),Ast.Break(r2,s2)) -> return true
 461   | (Ast.Continue(r1,s1),Ast.Continue(r2,s2)) -> return true
 462   | (Ast.Label(l1,dd1),Ast.Label(l2,dd2)) -> unify_ident l1 l2
 463   | (Ast.Goto(g1,l1,dd1),Ast.Goto(g2,l2,dd2)) -> unify_ident l1 l2
 464   | (Ast.Return(r1,s1),Ast.Return(r2,s2)) -> return true
 465   | (Ast.ReturnExpr(r1,e1,s1),Ast.ReturnExpr(r2,e2,s2)) ->
 466       unify_expression e1 e2
 467
 468   | (Ast.DisjRuleElem(res1),_) ->
 469       disjunct_all_bindings
 470         (List.map (function x -> unify_rule_elem x re2) res1)
 471   | (_,Ast.DisjRuleElem(res2)) ->
 472       disjunct_all_bindings
 473         (List.map (function x -> unify_rule_elem re1 x) res2)
 474
 475   | (Ast.MetaRuleElem(_,_,_),_)
 476   | (Ast.MetaStmt(_,_,_,_),_)
 477   | (Ast.MetaStmtList(_,_,_),_)
 478   | (_,Ast.MetaRuleElem(_,_,_))
 479   | (_,Ast.MetaStmt(_,_,_,_))
 480   | (_,Ast.MetaStmtList(_,_,_)) -> return true
 481
 482     (* can match a rule_elem in different parts *)
 483   | (Ast.Exp(e1),Ast.Exp(e2)) -> return true
 484   | (Ast.Exp(e1),_) -> subexp (unify_expression e1) re2
 485   | (_,Ast.Exp(e2)) -> subexp (unify_expression e2) re1
 486
 487   | (Ast.TopExp(e1),Ast.TopExp(e2)) -> unify_expression e1 e2
 488   | (Ast.TopInit(i1),Ast.TopInit(i2)) -> unify_initialiser i1 i2
 489
 490     (* can match a rule_elem in different parts *)
 491   | (Ast.Ty(t1),Ast.Ty(t2)) -> return true
 492   | (Ast.Ty(t1),_) -> subtype (unify_fullType t1) re2
 493   | (_,Ast.Ty(t2)) -> subtype (unify_fullType t2) re1
 494   | _ -> return false
 495
 496 and unify_fninfo patterninfo cinfo =
 497   let patterninfo = List.sort compare patterninfo in
 498   let cinfo = List.sort compare cinfo in
 499   let rec loop = function
 500       (Ast.FStorage(sta)::resta,Ast.FStorage(stb)::restb) ->
 501       if unify_mcode sta stb then loop (resta,restb) else return false
 502     | (Ast.FType(tya)::resta,Ast.FType(tyb)::restb) ->
 503         conjunct_bindings (unify_fullType tya tyb) (loop (resta,restb))
 504     | (Ast.FInline(ia)::resta,Ast.FInline(ib)::restb) ->
 505         if unify_mcode ia ib then loop (resta,restb) else return false
 506     | (Ast.FAttr(ia)::resta,Ast.FAttr(ib)::restb) ->
 507         if unify_mcode ia ib then loop (resta,restb) else return false
 508     | (x::resta,((y::_) as restb)) ->
 509         (match compare x y with
 510           -1 -> return false
 511         | 1 -> loop (resta,restb)
 512         | _ -> failwith "not possible")
 513     | _ -> return false in
 514   loop (patterninfo,cinfo)
 515
 516 and subexp f =
 517   let bind = conjunct_bindings in
 518   let option_default = return false in
 519   let mcode r e = option_default in
 520   let expr r k e = conjunct_bindings (f e) (k e) in
 521   let donothing r k e = k e in
 522   let recursor = V.combiner bind option_default
 523       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
 524       donothing donothing donothing donothing donothing
 525       donothing expr donothing donothing donothing donothing donothing
 526       donothing donothing donothing donothing donothing in
 527   recursor.V.combiner_rule_elem
 528
 529 and subtype f =
 530   let bind = conjunct_bindings in
 531   let option_default = return false in
 532   let mcode r e = option_default in
 533   let fullType r k e = conjunct_bindings (f e) (k e) in
 534   let donothing r k e = k e in
 535   let recursor = V.combiner bind option_default
 536       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
 537       donothing donothing donothing donothing donothing
 538       donothing donothing fullType donothing donothing donothing donothing
 539       donothing donothing donothing donothing donothing in
 540   recursor.V.combiner_rule_elem
 541
 542 let rec unify_statement s1 s2 =
 543   match (Ast.unwrap s1,Ast.unwrap s2) with
 544     (Ast.Seq(lb1,s1,rb1),Ast.Seq(lb2,s2,rb2)) ->
 545       conjunct_bindings (unify_rule_elem lb1 lb2)
 546         (conjunct_bindings
 547            (unify_dots unify_statement sdots s1 s2)
 548            (unify_rule_elem rb1 rb2))
 549   | (Ast.IfThen(h1,thn1,_),Ast.IfThen(h2,thn2,_)) ->
 550       conjunct_bindings (unify_rule_elem h1 h2) (unify_statement thn1 thn2)
 551   | (Ast.IfThenElse(h1,thn1,e1,els1,_),Ast.IfThenElse(h2,thn2,e2,els2,_)) ->
 552       conjunct_bindings (unify_rule_elem h1 h2)
 553         (conjunct_bindings (unify_statement thn1 thn2)
 554            (conjunct_bindings (unify_rule_elem e1 e2)
 555               (unify_statement els1 els2)))
 556   | (Ast.While(h1,s1,_),Ast.While(h2,s2,_)) ->
 557       conjunct_bindings (unify_rule_elem h1 h2) (unify_statement s1 s2)
 558   | (Ast.Do(h1,s1,t1),Ast.Do(h2,s2,t2)) ->
 559       conjunct_bindings (unify_rule_elem h1 h2)
 560         (conjunct_bindings (unify_statement s1 s2) (unify_rule_elem t1 t2))
 561   | (Ast.For(h1,s1,_),Ast.For(h2,s2,_)) ->
 562       conjunct_bindings (unify_rule_elem h1 h2) (unify_statement s1 s2)
 563   | (Ast.Atomic(re1),Ast.Atomic(re2)) -> unify_rule_elem re1 re2
 564   | (Ast.Disj(s1),_) ->
 565       let s2 = Ast.rewrap s2 (Ast.DOTS[s2]) in
 566       disjunct_all_bindings
 567         (List.map
 568            (function x -> unify_dots unify_statement sdots x s2)
 569            s1)
 570   | (_,Ast.Disj(s2)) ->
 571       let s1 = Ast.rewrap s1 (Ast.DOTS[s1]) in
 572       disjunct_all_bindings
 573         (List.map
 574            (function x -> unify_dots unify_statement sdots s1 x)
 575            s2)
 576   | (Ast.Nest(_,s1,_,_,_,_,_),Ast.Nest(_,s2,_,_,_,_,_)) ->
 577       unify_dots unify_statement sdots s1 s2
 578   | (Ast.FunDecl(h1,lb1,s1,rb1),Ast.FunDecl(h2,lb2,s2,rb2)) ->
 579       conjunct_bindings (unify_rule_elem h1 h2)
 580         (conjunct_bindings (unify_rule_elem lb1 lb2)
 581            (conjunct_bindings (unify_dots unify_statement sdots s1 s2)
 582               (unify_rule_elem rb1 rb2)))
 583   | (Ast.Define(h1,s1),Ast.Define(h2,s2)) ->
 584       conjunct_bindings (unify_rule_elem h1 h2)
 585         (unify_dots unify_statement sdots s1 s2)
 586   (* dots can match against anything.  return true to be safe. *)
 587   | (Ast.Dots(_,_,_,_),_) | (_,Ast.Dots(_,_,_,_))
 588   | (Ast.Circles(_,_,_,_),_) | (_,Ast.Circles(_,_,_,_))
 589   | (Ast.Stars(_,_,_,_),_) | (_,Ast.Stars(_,_,_,_)) -> return true
 590   | (Ast.OptStm(_),_)
 591   | (Ast.UniqueStm(_),_)
 592   | (_,Ast.OptStm(_))
 593   | (_,Ast.UniqueStm(_)) -> failwith "unsupported statement"
 594   | _ -> return false
 595
 596 let unify_statement_dots = unify_dots unify_statement sdots