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