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 let rec 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.DisjId(i1),_) ->
 135       disjunct_all_bindings (List.map (function x -> unify_ident x i2) i1)
 136   | (_,Ast.DisjId(i2)) ->
 137       disjunct_all_bindings (List.map (function x -> unify_ident i1 x) i2)
 138
 139   | (Ast.OptIdent(_),_)
 140   | (Ast.UniqueIdent(_),_)
 141   | (_,Ast.OptIdent(_))
 142   | (_,Ast.UniqueIdent(_)) -> failwith "unsupported ident"
 143
 144 (* --------------------------------------------------------------------- *)
 145 (* Expression *)
 146
 147 and unify_expression e1 e2 =
 148   match (Ast.unwrap e1,Ast.unwrap e2) with
 149     (Ast.Ident(i1),Ast.Ident(i2)) -> unify_ident i1 i2
 150   | (Ast.Constant(c1),Ast.Constant(c2))-> return (unify_mcode c1 c2)
 151   | (Ast.FunCall(f1,lp1,args1,rp1),Ast.FunCall(f2,lp2,args2,rp2)) ->
 152       conjunct_bindings
 153         (unify_expression f1 f2)
 154         (unify_dots unify_expression edots args1 args2)
 155   | (Ast.Assignment(l1,op1,r1,_),Ast.Assignment(l2,op2,r2,_)) ->
 156       if unify_mcode op1 op2
 157       then conjunct_bindings (unify_expression l1 l2) (unify_expression r1 r2)
 158       else return false
 159   | (Ast.CondExpr(tst1,q1,thn1,c1,els1),Ast.CondExpr(tst2,q2,thn2,c2,els2)) ->
 160       conjunct_bindings (unify_expression tst1 tst2)
 161         (conjunct_bindings (unify_option unify_expression thn1 thn2)
 162            (unify_expression els1 els2))
 163   | (Ast.Postfix(e1,op1),Ast.Postfix(e2,op2)) ->
 164       if unify_mcode op1 op2 then unify_expression e1 e2 else return false
 165   | (Ast.Infix(e1,op1),Ast.Infix(e2,op2)) ->
 166       if unify_mcode op1 op2 then unify_expression e1 e2 else return false
 167   | (Ast.Unary(e1,op1),Ast.Unary(e2,op2)) ->
 168       if unify_mcode op1 op2 then unify_expression e1 e2 else return false
 169   | (Ast.Binary(l1,op1,r1),Ast.Binary(l2,op2,r2)) ->
 170       if unify_mcode op1 op2
 171       then conjunct_bindings (unify_expression l1 l2) (unify_expression r1 r2)
 172       else return false
 173   | (Ast.ArrayAccess(ar1,lb1,e1,rb1),Ast.ArrayAccess(ar2,lb2,e2,rb2)) ->
 174       conjunct_bindings (unify_expression ar1 ar2) (unify_expression e1 e2)
 175   | (Ast.RecordAccess(e1,d1,fld1),Ast.RecordAccess(e2,d2,fld2)) ->
 176       conjunct_bindings (unify_expression e1 e2) (unify_ident fld1 fld2)
 177   | (Ast.RecordPtAccess(e1,pt1,fld1),Ast.RecordPtAccess(e2,pt2,fld2)) ->
 178       conjunct_bindings (unify_expression e1 e2) (unify_ident fld1 fld2)
 179   | (Ast.Cast(lp1,ty1,rp1,e1),Ast.Cast(lp2,ty2,rp2,e2)) ->
 180       conjunct_bindings (unify_fullType ty1 ty2) (unify_expression e1 e2)
 181   | (Ast.SizeOfExpr(szf1,e1),Ast.SizeOfExpr(szf2,e2)) ->
 182       unify_expression e1 e2
 183   | (Ast.SizeOfType(szf1,lp1,ty1,rp1),Ast.SizeOfType(szf2,lp2,ty2,rp2)) ->
 184       unify_fullType ty1 ty2
 185   | (Ast.TypeExp(ty1),Ast.TypeExp(ty2)) -> unify_fullType ty1 ty2
 186   | (Ast.Paren(lp1,e1,rp1),Ast.Paren(lp2,e2,rp2)) ->
 187       unify_expression e1 e2
 188
 189   | (Ast.MetaErr(_,_,_,_),_)
 190   | (Ast.MetaExpr(_,_,_,_,_,_),_)
 191   | (Ast.MetaExprList(_,_,_,_),_)
 192   | (_,Ast.MetaErr(_,_,_,_))
 193   | (_,Ast.MetaExpr(_,_,_,_,_,_))
 194   | (_,Ast.MetaExprList(_,_,_,_)) -> return true
 195
 196   | (Ast.EComma(cm1),Ast.EComma(cm2)) -> return true
 197
 198   | (Ast.DisjExpr(e1),_) ->
 199       disjunct_all_bindings (List.map (function x -> unify_expression x e2) e1)
 200   | (_,Ast.DisjExpr(e2)) ->
 201       disjunct_all_bindings (List.map (function x -> unify_expression e1 x) e2)
 202   | (Ast.NestExpr(_,e1,_,_,_),Ast.NestExpr(_,e2,_,_,_)) ->
 203       unify_dots unify_expression edots e1 e2
 204
 205   (* dots can match against anything.  return true to be safe. *)
 206   | (Ast.Edots(_,_),_) | (_,Ast.Edots(_,_))
 207   | (Ast.Ecircles(_,_),_) | (_,Ast.Ecircles(_,_))
 208   | (Ast.Estars(_,_),_) | (_,Ast.Estars(_,_)) -> return true
 209
 210   | (Ast.OptExp(_),_)
 211   | (Ast.UniqueExp(_),_)
 212   | (_,Ast.OptExp(_))
 213   | (_,Ast.UniqueExp(_)) -> failwith "unsupported expression"
 214   | _ -> return false
 215
 216 (* --------------------------------------------------------------------- *)
 217 (* Types *)
 218
 219 and unify_fullType ft1 ft2 =
 220   match (Ast.unwrap ft1,Ast.unwrap ft2) with
 221     (Ast.Type(cv1,ty1),Ast.Type(cv2,ty2)) ->
 222       if bool_unify_option unify_mcode cv1 cv2
 223       then unify_typeC ty1 ty2
 224       else return false
 225   | (Ast.DisjType(ft1),_) ->
 226       disjunct_all_bindings (List.map (function x -> unify_fullType x ft2) ft1)
 227   | (_,Ast.DisjType(ft2)) ->
 228       disjunct_all_bindings (List.map (function x -> unify_fullType ft1 x) ft2)
 229
 230   | (Ast.OptType(_),_)
 231   | (Ast.UniqueType(_),_)
 232   | (_,Ast.OptType(_))
 233   | (_,Ast.UniqueType(_)) -> failwith "unsupported type"
 234
 235 and unify_typeC t1 t2 =
 236   match (Ast.unwrap t1,Ast.unwrap t2) with
 237     (Ast.BaseType(ty1,stringsa),Ast.BaseType(ty2,stringsb)) ->
 238       if ty1 = ty2
 239       then
 240         unify_lists ret_unify_mcode (function _ -> false (* not dots*))
 241           stringsa stringsb
 242       else return false
 243   | (Ast.SignedT(sgn1,ty1),Ast.SignedT(sgn2,ty2)) ->
 244       if unify_mcode sgn1 sgn2
 245       then unify_option unify_typeC ty1 ty2
 246       else return false
 247   | (Ast.Pointer(ty1,s1),Ast.Pointer(ty2,s2)) -> unify_fullType ty1 ty2
 248   | (Ast.FunctionPointer(tya,lp1a,stara,rp1a,lp2a,paramsa,rp2a),
 249      Ast.FunctionPointer(tyb,lp1b,starb,rp1b,lp2b,paramsb,rp2b)) ->
 250        if List.for_all2 unify_mcode
 251            [lp1a;stara;rp1a;lp2a;rp2a] [lp1b;starb;rp1b;lp2b;rp2b]
 252        then
 253          conjunct_bindings (unify_fullType tya tyb)
 254            (unify_dots unify_parameterTypeDef pdots paramsa paramsb)
 255        else return false
 256   | (Ast.FunctionType(_,tya,lp1a,paramsa,rp1a),
 257      Ast.FunctionType(_,tyb,lp1b,paramsb,rp1b)) ->
 258        if List.for_all2 unify_mcode [lp1a;rp1a] [lp1b;rp1b]
 259        then
 260          conjunct_bindings (unify_option unify_fullType tya tyb)
 261            (unify_dots unify_parameterTypeDef pdots paramsa paramsb)
 262        else return false
 263   | (Ast.FunctionType _ , _) -> failwith "not supported"
 264   | (Ast.Array(ty1,lb1,e1,rb1),Ast.Array(ty2,lb2,e2,rb2)) ->
 265       conjunct_bindings
 266         (unify_fullType ty1 ty2) (unify_option unify_expression e1 e2)
 267   | (Ast.EnumName(s1,Some ts1),Ast.EnumName(s2,Some ts2)) ->
 268       if unify_mcode s1 s2 then unify_ident ts1 ts2 else return false
 269   | (Ast.EnumName(s1,None),Ast.EnumName(s2,None)) ->
 270       return true
 271   | (Ast.EnumDef(ty1,lb1,ids1,rb1),Ast.EnumDef(ty2,lb2,ids2,rb2)) ->
 272        conjunct_bindings (unify_fullType ty1 ty2)
 273          (unify_dots unify_expression edots ids1 ids2)
 274   | (Ast.StructUnionName(s1,Some ts1),Ast.StructUnionName(s2,Some ts2)) ->
 275       if unify_mcode s1 s2 then unify_ident ts1 ts2 else return false
 276   | (Ast.StructUnionName(s1,None),Ast.StructUnionName(s2,None)) ->
 277       return (unify_mcode s1 s2)
 278   | (Ast.StructUnionDef(ty1,lb1,decls1,rb1),
 279      Ast.StructUnionDef(ty2,lb2,decls2,rb2)) ->
 280        conjunct_bindings (unify_fullType ty1 ty2)
 281          (unify_dots unify_declaration ddots decls1 decls2)
 282   | (Ast.TypeName(t1),Ast.TypeName(t2)) -> return (unify_mcode t1 t2)
 283
 284   | (Ast.MetaType(_,_,_),_)
 285   | (_,Ast.MetaType(_,_,_)) -> return true
 286   | _ -> return false
 287
 288 (* --------------------------------------------------------------------- *)
 289 (* Variable declaration *)
 290 (* Even if the Cocci program specifies a list of declarations, they are
 291    split out into multiple declarations of a single variable each. *)
 292
 293 and unify_declaration d1 d2 =
 294   match (Ast.unwrap d1,Ast.unwrap d2) with
 295     (Ast.MetaDecl(_,_,_),_) | (_,Ast.MetaDecl(_,_,_)) -> return true
 296   | (Ast.MetaField(_,_,_),_) | (_,Ast.MetaField(_,_,_)) -> return true
 297   | (Ast.MetaFieldList(_,_,_,_),_) | (_,Ast.MetaFieldList(_,_,_,_)) ->
 298       return true
 299   | (Ast.Init(stg1,ft1,id1,eq1,i1,s1),Ast.Init(stg2,ft2,id2,eq2,i2,s2)) ->
 300       if bool_unify_option unify_mcode stg1 stg2
 301       then
 302         conjunct_bindings (unify_fullType ft1 ft2)
 303           (conjunct_bindings (unify_ident id1 id2) (unify_initialiser i1 i2))
 304       else return false
 305   | (Ast.UnInit(stg1,ft1,id1,s1),Ast.UnInit(stg2,ft2,id2,s2)) ->
 306       if bool_unify_option unify_mcode stg1 stg2
 307       then conjunct_bindings (unify_fullType ft1 ft2) (unify_ident id1 id2)
 308       else return false
 309   | (Ast.MacroDecl(n1,lp1,args1,rp1,sem1),
 310      Ast.MacroDecl(n2,lp2,args2,rp2,sem2)) ->
 311        conjunct_bindings (unify_ident n1 n2)
 312          (unify_dots unify_expression edots args1 args2)
 313   | (Ast.TyDecl(ft1,s1),Ast.TyDecl(ft2,s2)) -> unify_fullType ft1 ft2
 314   | (Ast.Typedef(stg1,ft1,id1,s1),Ast.Typedef(stg2,ft2,id2,s2)) ->
 315       conjunct_bindings (unify_fullType ft1 ft2) (unify_typeC id1 id2)
 316   | (Ast.DisjDecl(d1),_) ->
 317       disjunct_all_bindings
 318         (List.map (function x -> unify_declaration x d2) d1)
 319   | (_,Ast.DisjDecl(d2)) ->
 320       disjunct_all_bindings
 321         (List.map (function x -> unify_declaration d1 x) d2)
 322   (* dots can match against anything.  return true to be safe. *)
 323   | (Ast.Ddots(_,_),_) | (_,Ast.Ddots(_,_)) -> return true
 324
 325   | (Ast.OptDecl(_),_)
 326   | (Ast.UniqueDecl(_),_)
 327   | (_,Ast.OptDecl(_))
 328   | (_,Ast.UniqueDecl(_)) -> failwith "unsupported decl"
 329   | _ -> return false
 330
 331 (* --------------------------------------------------------------------- *)
 332 (* Initializer *)
 333
 334 and unify_initialiser i1 i2 =
 335   match (Ast.unwrap i1,Ast.unwrap i2) with
 336     (Ast.MetaInit(_,_,_),_) | (_,Ast.MetaInit(_,_,_)) -> return true
 337   | (Ast.InitExpr(expa),Ast.InitExpr(expb)) ->
 338       unify_expression expa expb
 339   | (Ast.ArInitList(_,initlista,_),
 340      Ast.ArInitList(_,initlistb,_)) ->
 341       (* ignore whencode - returns true safely *)
 342       unify_dots unify_initialiser idots initlista initlistb
 343   | (Ast.StrInitList(_,_,initlista,_,whena),
 344      Ast.StrInitList(_,_,initlistb,_,whenb)) ->
 345       (* ignore whencode - returns true safely *)
 346       unify_lists unify_initialiser (function _ -> false) initlista initlistb
 347   | (Ast.InitGccExt(designatorsa,_,inia),
 348      Ast.InitGccExt(designatorsb,_,inib)) ->
 349        conjunct_bindings
 350          (unify_lists unify_designator (function _ -> false)
 351             designatorsa designatorsb)
 352          (unify_initialiser inia inib)
 353   | (Ast.InitGccName(namea,_,inia),Ast.InitGccName(nameb,_,inib)) ->
 354       conjunct_bindings (unify_ident namea nameb) (unify_initialiser inia inib)
 355
 356   | (Ast.OptIni(_),_)
 357   | (Ast.UniqueIni(_),_)
 358   | (_,Ast.OptIni(_))
 359   | (_,Ast.UniqueIni(_)) -> failwith "unsupported decl"
 360   | _ -> return false
 361
 362 and unify_designator d1 d2 =
 363   match (d1,d2) with
 364     (Ast.DesignatorField(_,idb),Ast.DesignatorField(_,ida)) ->
 365       unify_ident ida idb
 366   | (Ast.DesignatorIndex(_,expa,_),Ast.DesignatorIndex(_,expb,_)) ->
 367       unify_expression expa expb
 368   | (Ast.DesignatorRange(_,mina,_,maxa,_),
 369      Ast.DesignatorRange(_,minb,_,maxb,_)) ->
 370        conjunct_bindings (unify_expression mina minb)
 371          (unify_expression maxa maxb)
 372   | _ -> return false
 373
 374 (* --------------------------------------------------------------------- *)
 375 (* Parameter *)
 376
 377 and unify_parameterTypeDef p1 p2 =
 378   match (Ast.unwrap p1,Ast.unwrap p2) with
 379     (Ast.VoidParam(ft1),Ast.VoidParam(ft2)) -> unify_fullType ft1 ft2
 380   | (Ast.Param(ft1,i1),Ast.Param(ft2,i2)) ->
 381       conjunct_bindings (unify_fullType ft1 ft2)
 382         (unify_option unify_ident i1 i2)
 383
 384   | (Ast.MetaParam(_,_,_),_)
 385   | (Ast.MetaParamList(_,_,_,_),_)
 386   | (_,Ast.MetaParam(_,_,_))
 387   | (_,Ast.MetaParamList(_,_,_,_)) -> return true
 388
 389   | (Ast.PComma(_),Ast.PComma(_)) -> return true
 390
 391   (* dots can match against anything.  return true to be safe. *)
 392   | (Ast.Pdots(_),_) | (_,Ast.Pdots(_))
 393   | (Ast.Pcircles(_),_) | (_,Ast.Pcircles(_)) -> return true
 394
 395   | (Ast.OptParam(_),_)
 396   | (Ast.UniqueParam(_),_)
 397   | (_,Ast.OptParam(_))
 398   | (_,Ast.UniqueParam(_)) -> failwith "unsupported parameter"
 399   | _ -> return false
 400
 401 (* --------------------------------------------------------------------- *)
 402 (* Define parameter *)
 403
 404 and unify_define_parameters p1 p2 =
 405  match (Ast.unwrap p1,Ast.unwrap p2) with
 406     (Ast.NoParams,Ast.NoParams) -> return true
 407   | (Ast.DParams(lp1,params1,rp1),Ast.DParams(lp2,params2,rp2)) ->
 408       unify_dots unify_define_param dpdots params1 params2
 409   | _ -> return false
 410
 411 and unify_define_param p1 p2 =
 412   match (Ast.unwrap p1,Ast.unwrap p2) with
 413     (Ast.DParam(i1),Ast.DParam(i2)) ->
 414         (unify_ident i1 i2)
 415   | (Ast.DPComma(_),Ast.DPComma(_)) -> return true
 416
 417   (* dots can match against anything.  return true to be safe. *)
 418   | (Ast.DPdots(_),_) | (_,Ast.DPdots(_))
 419   | (Ast.DPcircles(_),_) | (_,Ast.DPcircles(_)) -> return true
 420
 421   | (Ast.OptDParam(_),_)
 422   | (Ast.UniqueDParam(_),_)
 423   | (_,Ast.OptDParam(_))
 424   | (_,Ast.UniqueDParam(_)) -> failwith "unsupported parameter"
 425   | _ -> return false
 426
 427 (* --------------------------------------------------------------------- *)
 428 (* Top-level code *)
 429
 430 and unify_rule_elem re1 re2 =
 431   match (Ast.unwrap re1,Ast.unwrap re2) with
 432     (Ast.FunHeader(_,_,fi1,nm1,lp1,params1,rp1),
 433      Ast.FunHeader(_,_,fi2,nm2,lp2,params2,rp2)) ->
 434        conjunct_bindings (unify_fninfo fi1 fi2)
 435          (conjunct_bindings (unify_ident nm1 nm2)
 436             (unify_dots unify_parameterTypeDef pdots params1 params2))
 437   | (Ast.Decl(_,_,d1),Ast.Decl(_,_,d2)) -> unify_declaration d1 d2
 438
 439   | (Ast.SeqStart(lb1),Ast.SeqStart(lb2)) -> return true
 440   | (Ast.SeqEnd(rb1),Ast.SeqEnd(rb2)) -> return true
 441
 442   | (Ast.ExprStatement(e1,s1),Ast.ExprStatement(e2,s2)) ->
 443       unify_expression e1 e2
 444   | (Ast.IfHeader(if1,lp1,e1,rp1),Ast.IfHeader(if2,lp2,e2,rp2)) ->
 445       unify_expression e1 e2
 446   | (Ast.Else(e1),Ast.Else(e2)) -> return true
 447   | (Ast.WhileHeader(wh1,lp1,e1,rp1),Ast.WhileHeader(wh2,lp2,e2,rp2)) ->
 448       unify_expression e1 e2
 449   | (Ast.DoHeader(d1),Ast.DoHeader(d2)) -> return true
 450   | (Ast.WhileTail(wh1,lp1,e1,rp1,s1),Ast.WhileTail(wh2,lp2,e2,rp2,s2)) ->
 451       unify_expression e1 e2
 452   | (Ast.ForHeader(fr1,lp1,e11,s11,e21,s21,e31,rp1),
 453      Ast.ForHeader(fr2,lp2,e12,s12,e22,s22,e32,rp2)) ->
 454        conjunct_bindings
 455          (unify_option unify_expression e11 e12)
 456          (conjunct_bindings
 457             (unify_option unify_expression e21 e22)
 458             (unify_option unify_expression e31 e32))
 459   | (Ast.IteratorHeader(nm1,lp1,args1,rp1),
 460      Ast.IteratorHeader(nm2,lp2,args2,rp2)) ->
 461       conjunct_bindings (unify_ident nm1 nm2)
 462          (unify_dots unify_expression edots args1 args2)
 463   | (Ast.Undef(_,n1),Ast.Undef(_,n2)) -> unify_ident n1 n2
 464   | (Ast.DefineHeader(_,n1,p1),Ast.DefineHeader(_,n2,p2)) ->
 465       conjunct_bindings (unify_ident n1 n2)
 466         (unify_define_parameters p1 p2)
 467   | (Ast.Break(r1,s1),Ast.Break(r2,s2)) -> return true
 468   | (Ast.Continue(r1,s1),Ast.Continue(r2,s2)) -> return true
 469   | (Ast.Label(l1,dd1),Ast.Label(l2,dd2)) -> unify_ident l1 l2
 470   | (Ast.Goto(g1,l1,dd1),Ast.Goto(g2,l2,dd2)) -> unify_ident l1 l2
 471   | (Ast.Return(r1,s1),Ast.Return(r2,s2)) -> return true
 472   | (Ast.ReturnExpr(r1,e1,s1),Ast.ReturnExpr(r2,e2,s2)) ->
 473       unify_expression e1 e2
 474
 475   | (Ast.DisjRuleElem(res1),_) ->
 476       disjunct_all_bindings
 477         (List.map (function x -> unify_rule_elem x re2) res1)
 478   | (_,Ast.DisjRuleElem(res2)) ->
 479       disjunct_all_bindings
 480         (List.map (function x -> unify_rule_elem re1 x) res2)
 481
 482   | (Ast.MetaRuleElem(_,_,_),_)
 483   | (Ast.MetaStmt(_,_,_,_),_)
 484   | (Ast.MetaStmtList(_,_,_),_)
 485   | (_,Ast.MetaRuleElem(_,_,_))
 486   | (_,Ast.MetaStmt(_,_,_,_))
 487   | (_,Ast.MetaStmtList(_,_,_)) -> return true
 488
 489     (* can match a rule_elem in different parts *)
 490   | (Ast.Exp(e1),Ast.Exp(e2)) -> return true
 491   | (Ast.Exp(e1),_) -> subexp (unify_expression e1) re2
 492   | (_,Ast.Exp(e2)) -> subexp (unify_expression e2) re1
 493
 494   | (Ast.TopExp(e1),Ast.TopExp(e2)) -> unify_expression e1 e2
 495   | (Ast.TopInit(i1),Ast.TopInit(i2)) -> unify_initialiser i1 i2
 496
 497     (* can match a rule_elem in different parts *)
 498   | (Ast.Ty(t1),Ast.Ty(t2)) -> return true
 499   | (Ast.Ty(t1),_) -> subtype (unify_fullType t1) re2
 500   | (_,Ast.Ty(t2)) -> subtype (unify_fullType t2) re1
 501   | _ -> return false
 502
 503 and unify_fninfo patterninfo cinfo =
 504   let patterninfo = List.sort compare patterninfo in
 505   let cinfo = List.sort compare cinfo in
 506   let rec loop = function
 507       (Ast.FStorage(sta)::resta,Ast.FStorage(stb)::restb) ->
 508       if unify_mcode sta stb then loop (resta,restb) else return false
 509     | (Ast.FType(tya)::resta,Ast.FType(tyb)::restb) ->
 510         conjunct_bindings (unify_fullType tya tyb) (loop (resta,restb))
 511     | (Ast.FInline(ia)::resta,Ast.FInline(ib)::restb) ->
 512         if unify_mcode ia ib then loop (resta,restb) else return false
 513     | (Ast.FAttr(ia)::resta,Ast.FAttr(ib)::restb) ->
 514         if unify_mcode ia ib then loop (resta,restb) else return false
 515     | (x::resta,((y::_) as restb)) ->
 516         (match compare x y with
 517           -1 -> return false
 518         | 1 -> loop (resta,restb)
 519         | _ -> failwith "not possible")
 520     | _ -> return false in
 521   loop (patterninfo,cinfo)
 522
 523 and subexp f =
 524   let bind = conjunct_bindings in
 525   let option_default = return false in
 526   let mcode r e = option_default in
 527   let expr r k e = conjunct_bindings (f e) (k e) in
 528   let donothing r k e = k e in
 529   let recursor = V.combiner bind option_default
 530       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
 531       donothing donothing donothing donothing donothing
 532       donothing expr donothing donothing donothing donothing donothing
 533       donothing donothing donothing donothing donothing in
 534   recursor.V.combiner_rule_elem
 535
 536 and subtype f =
 537   let bind = conjunct_bindings in
 538   let option_default = return false in
 539   let mcode r e = option_default in
 540   let fullType r k e = conjunct_bindings (f e) (k e) in
 541   let donothing r k e = k e in
 542   let recursor = V.combiner bind option_default
 543       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
 544       donothing donothing donothing donothing donothing
 545       donothing donothing fullType donothing donothing donothing donothing
 546       donothing donothing donothing donothing donothing in
 547   recursor.V.combiner_rule_elem
 548
 549 let rec unify_statement s1 s2 =
 550   match (Ast.unwrap s1,Ast.unwrap s2) with
 551     (Ast.Seq(lb1,s1,rb1),Ast.Seq(lb2,s2,rb2)) ->
 552       conjunct_bindings (unify_rule_elem lb1 lb2)
 553         (conjunct_bindings
 554            (unify_dots unify_statement sdots s1 s2)
 555            (unify_rule_elem rb1 rb2))
 556   | (Ast.IfThen(h1,thn1,_),Ast.IfThen(h2,thn2,_)) ->
 557       conjunct_bindings (unify_rule_elem h1 h2) (unify_statement thn1 thn2)
 558   | (Ast.IfThenElse(h1,thn1,e1,els1,_),Ast.IfThenElse(h2,thn2,e2,els2,_)) ->
 559       conjunct_bindings (unify_rule_elem h1 h2)
 560         (conjunct_bindings (unify_statement thn1 thn2)
 561            (conjunct_bindings (unify_rule_elem e1 e2)
 562               (unify_statement els1 els2)))
 563   | (Ast.While(h1,s1,_),Ast.While(h2,s2,_)) ->
 564       conjunct_bindings (unify_rule_elem h1 h2) (unify_statement s1 s2)
 565   | (Ast.Do(h1,s1,t1),Ast.Do(h2,s2,t2)) ->
 566       conjunct_bindings (unify_rule_elem h1 h2)
 567         (conjunct_bindings (unify_statement s1 s2) (unify_rule_elem t1 t2))
 568   | (Ast.For(h1,s1,_),Ast.For(h2,s2,_)) ->
 569       conjunct_bindings (unify_rule_elem h1 h2) (unify_statement s1 s2)
 570   | (Ast.Atomic(re1),Ast.Atomic(re2)) -> unify_rule_elem re1 re2
 571   | (Ast.Disj(s1),_) ->
 572       let s2 = Ast.rewrap s2 (Ast.DOTS[s2]) in
 573       disjunct_all_bindings
 574         (List.map
 575            (function x -> unify_dots unify_statement sdots x s2)
 576            s1)
 577   | (_,Ast.Disj(s2)) ->
 578       let s1 = Ast.rewrap s1 (Ast.DOTS[s1]) in
 579       disjunct_all_bindings
 580         (List.map
 581            (function x -> unify_dots unify_statement sdots s1 x)
 582            s2)
 583   | (Ast.Nest(_,s1,_,_,_,_,_),Ast.Nest(_,s2,_,_,_,_,_)) ->
 584       unify_dots unify_statement sdots s1 s2
 585   | (Ast.FunDecl(h1,lb1,s1,rb1),Ast.FunDecl(h2,lb2,s2,rb2)) ->
 586       conjunct_bindings (unify_rule_elem h1 h2)
 587         (conjunct_bindings (unify_rule_elem lb1 lb2)
 588            (conjunct_bindings (unify_dots unify_statement sdots s1 s2)
 589               (unify_rule_elem rb1 rb2)))
 590   | (Ast.Define(h1,s1),Ast.Define(h2,s2)) ->
 591       conjunct_bindings (unify_rule_elem h1 h2)
 592         (unify_dots unify_statement sdots s1 s2)
 593   (* dots can match against anything.  return true to be safe. *)
 594   | (Ast.Dots(_,_,_,_),_) | (_,Ast.Dots(_,_,_,_))
 595   | (Ast.Circles(_,_,_,_),_) | (_,Ast.Circles(_,_,_,_))
 596   | (Ast.Stars(_,_,_,_),_) | (_,Ast.Stars(_,_,_,_)) -> return true
 597   | (Ast.OptStm(_),_)
 598   | (Ast.UniqueStm(_),_)
 599   | (_,Ast.OptStm(_))
 600   | (_,Ast.UniqueStm(_)) -> failwith "unsupported statement"
 601   | _ -> return false
 602
 603 let unify_statement_dots = unify_dots unify_statement sdots