parsing_cocci/unify_ast.ml

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