parsing_cocci/unify_ast.ml

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