diff options
Diffstat (limited to 'cil/src/frontc/patch.ml')
-rw-r--r-- | cil/src/frontc/patch.ml | 837 |
1 files changed, 837 insertions, 0 deletions
diff --git a/cil/src/frontc/patch.ml b/cil/src/frontc/patch.ml new file mode 100644 index 00000000..fcb4ba62 --- /dev/null +++ b/cil/src/frontc/patch.ml @@ -0,0 +1,837 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula <necula@cs.berkeley.edu> + * Scott McPeak <smcpeak@cs.berkeley.edu> + * Wes Weimer <weimer@cs.berkeley.edu> + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) + + +(* patch.ml *) +(* CABS file patching *) + +open Cabs +open Trace +open Pretty +open Cabsvisit + +(* binding of a unification variable to a syntactic construct *) +type binding = + | BSpecifier of string * spec_elem list + | BName of string * string + | BExpr of string * expression + +(* thrown when unification fails *) +exception NoMatch + +(* thrown when an attempt to find the associated binding fails *) +exception BadBind of string + +(* trying to isolate performance problems; will hide all the *) +(* potentially expensive debugging output behind "if verbose .." *) +let verbose : bool = true + + +(* raise NoMatch if x and y are not equal *) +let mustEq (x : 'a) (y : 'a) : unit = +begin + if (x <> y) then ( + if verbose then + (trace "patchDebug" (dprintf "mismatch by structural disequality\n")); + raise NoMatch + ) +end + +(* why isn't this in the core Ocaml library? *) +let identity x = x + + +let isPatternVar (s : string) : bool = +begin + ((String.length s) >= 1) && ((String.get s 0) = '@') +end + +(* 's' is actually "@name(blah)"; extract the 'blah' *) +let extractPatternVar (s : string) : string = + (*(trace "patch" (dprintf "extractPatternVar %s\n" s));*) + (String.sub s 6 ((String.length s) - 7)) + + +(* a few debugging printers.. *) +let printExpr (e : expression) = +begin + if (verbose && traceActive "patchDebug") then ( + Cprint.print_expression e; Cprint.force_new_line (); + Cprint.flush () + ) +end + +let printSpec (spec: spec_elem list) = +begin + if (verbose && traceActive "patchDebug") then ( + Cprint.print_specifiers spec; Cprint.force_new_line (); + Cprint.flush () + ) +end + +let printSpecs (pat : spec_elem list) (tgt : spec_elem list) = +begin + (printSpec pat); + (printSpec tgt) +end + +let printDecl (pat : name) (tgt : name) = +begin + if (verbose && traceActive "patchDebug") then ( + Cprint.print_name pat; Cprint.force_new_line (); + Cprint.print_name tgt; Cprint.force_new_line (); + Cprint.flush () + ) +end + +let printDeclType (pat : decl_type) (tgt : decl_type) = +begin + if (verbose && traceActive "patchDebug") then ( + Cprint.print_decl "__missing_field_name" pat; Cprint.force_new_line (); + Cprint.print_decl "__missing_field_name" tgt; Cprint.force_new_line (); + Cprint.flush () + ) +end + +let printDefn (d : definition) = +begin + if (verbose && traceActive "patchDebug") then ( + Cprint.print_def d; + Cprint.flush () + ) +end + + +(* class to describe how to modify the tree for subtitution *) +class substitutor (bindings : binding list) = object(self) + inherit nopCabsVisitor as super + + (* look in the binding list for a given name *) + method findBinding (name : string) : binding = + begin + try + (List.find + (fun b -> + match b with + | BSpecifier(n, _) -> n=name + | BName(n, _) -> n=name + | BExpr(n, _) -> n=name) + bindings) + with + Not_found -> raise (BadBind ("name not found: " ^ name)) + end + + method vexpr (e:expression) : expression visitAction = + begin + match e with + | EXPR_PATTERN(name) -> ( + match (self#findBinding name) with + | BExpr(_, expr) -> ChangeTo(expr) (* substitute bound expression *) + | _ -> raise (BadBind ("wrong type: " ^ name)) + ) + | _ -> DoChildren + end + + (* use of a name *) + method vvar (s:string) : string = + begin + if (isPatternVar s) then ( + let nameString = (extractPatternVar s) in + match (self#findBinding nameString) with + | BName(_, str) -> str (* substitute *) + | _ -> raise (BadBind ("wrong type: " ^ nameString)) + ) + else + s + end + + (* binding introduction of a name *) + method vname (k: nameKind) (spec: specifier) (n: name) : name visitAction = + begin + match n with (s (*variable name*), dtype, attrs, loc) -> ( + let replacement = (self#vvar s) in (* use replacer from above *) + if (s <> replacement) then + ChangeTo(replacement, dtype, attrs, loc) + else + DoChildren (* no replacement *) + ) + end + + method vspec (specList: specifier) : specifier visitAction = + begin + if verbose then (trace "patchDebug" (dprintf "substitutor: vspec\n")); + (printSpec specList); + + (* are any of the specifiers SpecPatterns? we have to check the entire *) + (* list, not just the head, because e.g. "typedef @specifier(foo)" has *) + (* "typedef" as the head of the specifier list *) + if (List.exists (fun elt -> match elt with + | SpecPattern(_) -> true + | _ -> false) + specList) then begin + (* yes, replace the existing list with one got by *) + (* replacing all occurrences of SpecPatterns *) + (trace "patchDebug" (dprintf "at least one spec pattern\n")); + ChangeTo + (List.flatten + (List.map + (* for each specifier element, yield the specifier list *) + (* to which it maps; then we'll flatten the final result *) + (fun elt -> + match elt with + | SpecPattern(name) -> ( + match (self#findBinding name) with + | BSpecifier(_, replacement) -> ( + (trace "patchDebug" (dprintf "replacing pattern %s\n" name)); + replacement + ) + | _ -> raise (BadBind ("wrong type: " ^ name)) + ) + | _ -> [elt] (* leave this one alone *) + ) + specList + ) + ) + end + else + (* none of the specifiers in specList are patterns *) + DoChildren + end + + method vtypespec (tspec: typeSpecifier) : typeSpecifier visitAction = + begin + match tspec with + | Tnamed(str) when (isPatternVar str) -> + ChangeTo(Tnamed(self#vvar str)) + | Tstruct(str, fields, extraAttrs) when (isPatternVar str) -> ( + (trace "patchDebug" (dprintf "substituting %s\n" str)); + ChangeDoChildrenPost(Tstruct((self#vvar str), fields, extraAttrs), identity) + ) + | Tunion(str, fields, extraAttrs) when (isPatternVar str) -> + (trace "patchDebug" (dprintf "substituting %s\n" str)); + ChangeDoChildrenPost(Tunion((self#vvar str), fields, extraAttrs), identity) + | _ -> DoChildren + end + +end + + +(* why can't I have forward declarations in the language?!! *) +let unifyExprFwd : (expression -> expression -> binding list) ref + = ref (fun e e -> []) + + +(* substitution for expressions *) +let substExpr (bindings : binding list) (expr : expression) : expression = +begin + if verbose then + (trace "patchDebug" (dprintf "substExpr with %d bindings\n" (List.length bindings))); + (printExpr expr); + + (* apply the transformation *) + let result = (visitCabsExpression (new substitutor bindings :> cabsVisitor) expr) in + (printExpr result); + + result +end + +let d_loc (_:unit) (loc: cabsloc) : doc = + text loc.filename ++ chr ':' ++ num loc.lineno + + +(* class to describe how to modify the tree when looking for places *) +(* to apply expression transformers *) +class exprTransformer (srcpattern : expression) (destpattern : expression) + (patchline : int) (srcloc : cabsloc) = object(self) + inherit nopCabsVisitor as super + + method vexpr (e:expression) : expression visitAction = + begin + (* see if the source pattern matches this subexpression *) + try ( + let bindings = (!unifyExprFwd srcpattern e) in + + (* match! *) + (trace "patch" (dprintf "expr match: patch line %d, src %a\n" + patchline d_loc srcloc)); + ChangeTo(substExpr bindings destpattern) + ) + + with NoMatch -> ( + (* doesn't apply *) + DoChildren + ) + end + + (* other constructs left unchanged *) +end + + +let unifyList (pat : 'a list) (tgt : 'a list) + (unifyElement : 'a -> 'a -> binding list) : binding list = +begin + if verbose then + (trace "patchDebug" (dprintf "unifyList (pat len %d, tgt len %d)\n" + (List.length pat) (List.length tgt))); + + (* walk down the lists *) + let rec loop pat tgt : binding list = + match pat, tgt with + | [], [] -> [] + | (pelt :: prest), (telt :: trest) -> + (unifyElement pelt telt) @ + (loop prest trest) + | _,_ -> ( + (* no match *) + if verbose then ( + (trace "patchDebug" (dprintf "mismatching list length\n")); + ); + raise NoMatch + ) + in + (loop pat tgt) +end + + +let gettime () : float = + (Unix.times ()).Unix.tms_utime + +let rec applyPatch (patchFile : file) (srcFile : file) : file = +begin + let patch : definition list = (snd patchFile) in + let srcFname : string = (fst srcFile) in + let src : definition list = (snd srcFile) in + + (trace "patchTime" (dprintf "applyPatch start: %f\n" (gettime ()))); + if (traceActive "patchDebug") then + Cprint.out := stdout (* hack *) + else (); + + (* more hackery *) + unifyExprFwd := unifyExpr; + + (* patch a single source definition, yield transformed *) + let rec patchDefn (patch : definition list) (d : definition) : definition list = + begin + match patch with + | TRANSFORMER(srcpattern, destpattern, loc) :: rest -> ( + if verbose then + (trace "patchDebug" + (dprintf "considering applying defn pattern at line %d to src at %a\n" + loc.lineno d_loc (get_definitionloc d))); + + (* see if the source pattern matches the definition 'd' we have *) + try ( + let bindings = (unifyDefn srcpattern d) in + + (* we have a match! apply the substitutions *) + (trace "patch" (dprintf "defn match: patch line %d, src %a\n" + loc.lineno d_loc (get_definitionloc d))); + + (List.map (fun destElt -> (substDefn bindings destElt)) destpattern) + ) + + with NoMatch -> ( + (* no match, continue down list *) + (*(trace "patch" (dprintf "no match\n"));*) + (patchDefn rest d) + ) + ) + + | EXPRTRANSFORMER(srcpattern, destpattern, loc) :: rest -> ( + if verbose then + (trace "patchDebug" + (dprintf "considering applying expr pattern at line %d to src at %a\n" + loc.lineno d_loc (get_definitionloc d))); + + (* walk around in 'd' looking for expressions to modify *) + let dList = (visitCabsDefinition + ((new exprTransformer srcpattern destpattern + loc.lineno (get_definitionloc d)) + :> cabsVisitor) + d + ) in + + (* recursively invoke myself to try additional patches *) + (* since visitCabsDefinition might return a list, I'll try my *) + (* addtional patches on every yielded definition, then collapse *) + (* all of them into a single list *) + (List.flatten (List.map (fun d -> (patchDefn rest d)) dList)) + ) + + | _ :: rest -> ( + (* not a transformer; just keep going *) + (patchDefn rest d) + ) + | [] -> ( + (* reached the end of the patch file with no match *) + [d] (* have to wrap it in a list ... *) + ) + end in + + (* transform all the definitions *) + let result : definition list = + (List.flatten (List.map (fun d -> (patchDefn patch d)) src)) in + + (*Cprint.print_defs result;*) + + if (traceActive "patchDebug") then ( + (* avoid flush bug? yes *) + Cprint.force_new_line (); + Cprint.flush () + ); + + (trace "patchTime" (dprintf "applyPatch finish: %f\n" (gettime ()))); + (srcFname, result) +end + + +(* given a definition pattern 'pat', and a target concrete defintion 'tgt', *) +(* determine if they can be unified; if so, return the list of bindings of *) +(* unification variables in pat; otherwise raise NoMatch *) +and unifyDefn (pat : definition) (tgt : definition) : binding list = +begin + match pat, tgt with + | DECDEF((pspecifiers, pdeclarators), _), + DECDEF((tspecifiers, tdeclarators), _) -> ( + if verbose then + (trace "patchDebug" (dprintf "unifyDefn of DECDEFs\n")); + (unifySpecifiers pspecifiers tspecifiers) @ + (unifyInitDeclarators pdeclarators tdeclarators) + ) + + | TYPEDEF((pspec, pdecl), _), + TYPEDEF((tspec, tdecl), _) -> ( + if verbose then + (trace "patchDebug" (dprintf "unifyDefn of TYPEDEFs\n")); + (unifySpecifiers pspec tspec) @ + (unifyDeclarators pdecl tdecl) + ) + + | ONLYTYPEDEF(pspec, _), + ONLYTYPEDEF(tspec, _) -> ( + if verbose then + (trace "patchDebug" (dprintf "unifyDefn of ONLYTYPEDEFs\n")); + (unifySpecifiers pspec tspec) + ) + + | _, _ -> ( + if verbose then + (trace "patchDebug" (dprintf "mismatching definitions\n")); + raise NoMatch + ) +end + +and unifySpecifier (pat : spec_elem) (tgt : spec_elem) : binding list = +begin + if verbose then + (trace "patchDebug" (dprintf "unifySpecifier\n")); + (printSpecs [pat] [tgt]); + + if (pat = tgt) then [] else + + match pat, tgt with + | SpecType(tspec1), SpecType(tspec2) -> + (unifyTypeSpecifier tspec1 tspec2) + | SpecPattern(name), _ -> + (* record that future occurrances of @specifier(name) will yield this specifier *) + if verbose then + (trace "patchDebug" (dprintf "found specifier match for %s\n" name)); + [BSpecifier(name, [tgt])] + | _,_ -> ( + (* no match *) + if verbose then ( + (trace "patchDebug" (dprintf "mismatching specifiers\n")); + ); + raise NoMatch + ) +end + +and unifySpecifiers (pat : spec_elem list) (tgt : spec_elem list) : binding list = +begin + if verbose then + (trace "patchDebug" (dprintf "unifySpecifiers\n")); + (printSpecs pat tgt); + + (* canonicalize the specifiers by sorting them *) + let pat' = (List.stable_sort compare pat) in + let tgt' = (List.stable_sort compare tgt) in + + (* if they are equal, they match with no further checking *) + if (pat' = tgt') then [] else + + (* walk down the lists; don't walk the sorted lists because the *) + (* pattern must always be last, if it occurs *) + let rec loop pat tgt : binding list = + match pat, tgt with + | [], [] -> [] + | [SpecPattern(name)], _ -> + (* final SpecPattern matches anything which comes after *) + (* record that future occurrences of @specifier(name) will yield this specifier *) + if verbose then + (trace "patchDebug" (dprintf "found specifier match for %s\n" name)); + [BSpecifier(name, tgt)] + | (pspec :: prest), (tspec :: trest) -> + (unifySpecifier pspec tspec) @ + (loop prest trest) + | _,_ -> ( + (* no match *) + if verbose then ( + (trace "patchDebug" (dprintf "mismatching specifier list length\n")); + ); + raise NoMatch + ) + in + (loop pat tgt) +end + +and unifyTypeSpecifier (pat: typeSpecifier) (tgt: typeSpecifier) : binding list = +begin + if verbose then + (trace "patchDebug" (dprintf "unifyTypeSpecifier\n")); + + if (pat = tgt) then [] else + + match pat, tgt with + | Tnamed(s1), Tnamed(s2) -> (unifyString s1 s2) + | Tstruct(name1, None, _), Tstruct(name2, None, _) -> + (unifyString name1 name2) + | Tstruct(name1, Some(fields1), _), Tstruct(name2, Some(fields2), _) -> + (* ignoring extraAttrs b/c we're just trying to come up with a list + * of substitutions, and there's no unify_attributes function, and + * I don't care at this time about checking that they are equal .. *) + (unifyString name1 name2) @ + (unifyList fields1 fields2 unifyField) + | Tunion(name1, None, _), Tstruct(name2, None, _) -> + (unifyString name1 name2) + | Tunion(name1, Some(fields1), _), Tunion(name2, Some(fields2), _) -> + (unifyString name1 name2) @ + (unifyList fields1 fields2 unifyField) + | Tenum(name1, None, _), Tenum(name2, None, _) -> + (unifyString name1 name2) + | Tenum(name1, Some(items1), _), Tenum(name2, Some(items2), _) -> + (mustEq items1 items2); (* enum items *) + (unifyString name1 name2) + | TtypeofE(exp1), TtypeofE(exp2) -> + (unifyExpr exp1 exp2) + | TtypeofT(spec1, dtype1), TtypeofT(spec2, dtype2) -> + (unifySpecifiers spec1 spec2) @ + (unifyDeclType dtype1 dtype2) + | _ -> ( + if verbose then (trace "patchDebug" (dprintf "mismatching typeSpecifiers\n")); + raise NoMatch + ) +end + +and unifyField (pat : field_group) (tgt : field_group) : binding list = +begin + match pat,tgt with (spec1, list1), (spec2, list2) -> ( + (unifySpecifiers spec1 spec2) @ + (unifyList list1 list2 unifyNameExprOpt) + ) +end + +and unifyNameExprOpt (pat : name * expression option) + (tgt : name * expression option) : binding list = +begin + match pat,tgt with + | (name1, None), (name2, None) -> (unifyName name1 name2) + | (name1, Some(exp1)), (name2, Some(exp2)) -> + (unifyName name1 name2) @ + (unifyExpr exp1 exp2) + | _,_ -> [] +end + +and unifyName (pat : name) (tgt : name) : binding list = +begin + match pat,tgt with (pstr, pdtype, pattrs, ploc), (tstr, tdtype, tattrs, tloc) -> + (mustEq pattrs tattrs); + (unifyString pstr tstr) @ + (unifyDeclType pdtype tdtype) +end + +and unifyInitDeclarators (pat : init_name list) (tgt : init_name list) : binding list = +begin + (* + if verbose then + (trace "patchDebug" (dprintf "unifyInitDeclarators, pat %d, tgt %d\n" + (List.length pat) (List.length tgt))); + *) + + match pat, tgt with + | ((pdecl, piexpr) :: prest), + ((tdecl, tiexpr) :: trest) -> + (unifyDeclarator pdecl tdecl) @ + (unifyInitExpr piexpr tiexpr) @ + (unifyInitDeclarators prest trest) + | [], [] -> [] + | _, _ -> ( + if verbose then + (trace "patchDebug" (dprintf "mismatching init declarators\n")); + raise NoMatch + ) +end + +and unifyDeclarators (pat : name list) (tgt : name list) : binding list = + (unifyList pat tgt unifyDeclarator) + +and unifyDeclarator (pat : name) (tgt : name) : binding list = +begin + if verbose then + (trace "patchDebug" (dprintf "unifyDeclarator\n")); + (printDecl pat tgt); + + match pat, tgt with + | (pname, pdtype, pattr, ploc), + (tname, tdtype, tattr, tloc) -> + (mustEq pattr tattr); + (unifyDeclType pdtype tdtype) @ + (unifyString pname tname) +end + +and unifyDeclType (pat : decl_type) (tgt : decl_type) : binding list = +begin + if verbose then + (trace "patchDebug" (dprintf "unifyDeclType\n")); + (printDeclType pat tgt); + + match pat, tgt with + | JUSTBASE, JUSTBASE -> [] + | PARENTYPE(pattr1, ptype, pattr2), + PARENTYPE(tattr1, ttype, tattr2) -> + (mustEq pattr1 tattr1); + (mustEq pattr2 tattr2); + (unifyDeclType ptype ttype) + | ARRAY(ptype, pattr, psz), + ARRAY(ttype, tattr, tsz) -> + (mustEq pattr tattr); + (unifyDeclType ptype ttype) @ + (unifyExpr psz tsz) + | PTR(pattr, ptype), + PTR(tattr, ttype) -> + (mustEq pattr tattr); + (unifyDeclType ptype ttype) + | PROTO(ptype, pformals, pva), + PROTO(ttype, tformals, tva) -> + (mustEq pva tva); + (unifyDeclType ptype ttype) @ + (unifySingleNames pformals tformals) + | _ -> ( + if verbose then + (trace "patchDebug" (dprintf "mismatching decl_types\n")); + raise NoMatch + ) +end + +and unifySingleNames (pat : single_name list) (tgt : single_name list) : binding list = +begin + if verbose then + (trace "patchDebug" (dprintf "unifySingleNames, pat %d, tgt %d\n" + (List.length pat) (List.length tgt))); + + match pat, tgt with + | [], [] -> [] + | (pspec, pdecl) :: prest, + (tspec, tdecl) :: trest -> + (unifySpecifiers pspec tspec) @ + (unifyDeclarator pdecl tdecl) @ + (unifySingleNames prest trest) + | _, _ -> ( + if verbose then + (trace "patchDebug" (dprintf "mismatching single_name lists\n")); + raise NoMatch + ) +end + +and unifyString (pat : string) (tgt : string) : binding list = +begin + (* equal? match with no further ado *) + if (pat = tgt) then [] else + + (* is the pattern a variable? *) + if (isPatternVar pat) then + (* pat is actually "@name(blah)"; extract the 'blah' *) + let varname = (extractPatternVar pat) in + + (* when substituted, this name becomes 'tgt' *) + if verbose then + (trace "patchDebug" (dprintf "found name match for %s\n" varname)); + [BName(varname, tgt)] + + else ( + if verbose then + (trace "patchDebug" (dprintf "mismatching names: %s and %s\n" pat tgt)); + raise NoMatch + ) +end + +and unifyExpr (pat : expression) (tgt : expression) : binding list = +begin + (* if they're equal, that's good enough *) + if (pat = tgt) then [] else + + (* shorter name *) + let ue = unifyExpr in + + (* because of the equality check above, I can omit some cases *) + match pat, tgt with + | UNARY(pop, pexpr), + UNARY(top, texpr) -> + (mustEq pop top); + (ue pexpr texpr) + | BINARY(pop, pexp1, pexp2), + BINARY(top, texp1, texp2) -> + (mustEq pop top); + (ue pexp1 texp1) @ + (ue pexp2 texp2) + | QUESTION(p1, p2, p3), + QUESTION(t1, t2, t3) -> + (ue p1 t1) @ + (ue p2 t2) @ + (ue p3 t3) + | CAST((pspec, ptype), piexpr), + CAST((tspec, ttype), tiexpr) -> + (mustEq ptype ttype); + (unifySpecifiers pspec tspec) @ + (unifyInitExpr piexpr tiexpr) + | CALL(pfunc, pargs), + CALL(tfunc, targs) -> + (ue pfunc tfunc) @ + (unifyExprs pargs targs) + | COMMA(pexprs), + COMMA(texprs) -> + (unifyExprs pexprs texprs) + | EXPR_SIZEOF(pexpr), + EXPR_SIZEOF(texpr) -> + (ue pexpr texpr) + | TYPE_SIZEOF(pspec, ptype), + TYPE_SIZEOF(tspec, ttype) -> + (mustEq ptype ttype); + (unifySpecifiers pspec tspec) + | EXPR_ALIGNOF(pexpr), + EXPR_ALIGNOF(texpr) -> + (ue pexpr texpr) + | TYPE_ALIGNOF(pspec, ptype), + TYPE_ALIGNOF(tspec, ttype) -> + (mustEq ptype ttype); + (unifySpecifiers pspec tspec) + | INDEX(parr, pindex), + INDEX(tarr, tindex) -> + (ue parr tarr) @ + (ue pindex tindex) + | MEMBEROF(pexpr, pfield), + MEMBEROF(texpr, tfield) -> + (mustEq pfield tfield); + (ue pexpr texpr) + | MEMBEROFPTR(pexpr, pfield), + MEMBEROFPTR(texpr, tfield) -> + (mustEq pfield tfield); + (ue pexpr texpr) + | GNU_BODY(pblock), + GNU_BODY(tblock) -> + (mustEq pblock tblock); + [] + | EXPR_PATTERN(name), _ -> + (* match, and contribute binding *) + if verbose then + (trace "patchDebug" (dprintf "found expr match for %s\n" name)); + [BExpr(name, tgt)] + | a, b -> + if (verbose && traceActive "patchDebug") then ( + (trace "patchDebug" (dprintf "mismatching expression\n")); + (printExpr a); + (printExpr b) + ); + raise NoMatch +end + +and unifyInitExpr (pat : init_expression) (tgt : init_expression) : binding list = +begin + (* + Cprint.print_init_expression pat; Cprint.force_new_line (); + Cprint.print_init_expression tgt; Cprint.force_new_line (); + Cprint.flush (); + *) + + match pat, tgt with + | NO_INIT, NO_INIT -> [] + | SINGLE_INIT(pe), SINGLE_INIT(te) -> + (unifyExpr pe te) + | COMPOUND_INIT(plist), + COMPOUND_INIT(tlist) -> ( + let rec loop plist tlist = + match plist, tlist with + | ((pwhat, piexpr) :: prest), + ((twhat, tiexpr) :: trest) -> + (mustEq pwhat twhat); + (unifyInitExpr piexpr tiexpr) @ + (loop prest trest) + | [], [] -> [] + | _, _ -> ( + if verbose then + (trace "patchDebug" (dprintf "mismatching compound init exprs\n")); + raise NoMatch + ) + in + (loop plist tlist) + ) + | _,_ -> ( + if verbose then + (trace "patchDebug" (dprintf "mismatching init exprs\n")); + raise NoMatch + ) +end + +and unifyExprs (pat : expression list) (tgt : expression list) : binding list = + (unifyList pat tgt unifyExpr) + + +(* given the list of bindings 'b', substitute them into 'd' to yield a new definition *) +and substDefn (bindings : binding list) (defn : definition) : definition = +begin + if verbose then + (trace "patchDebug" (dprintf "substDefn with %d bindings\n" (List.length bindings))); + (printDefn defn); + + (* apply the transformation *) + match (visitCabsDefinition (new substitutor bindings :> cabsVisitor) defn) with + | [d] -> d (* expect a singleton list *) + | _ -> (failwith "didn't get a singleton list where I expected one") +end + + +(* end of file *) |