Source file mergecil.ml

(*

   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.

 *)

(* mergecil.ml *)
(* This module is responsible for merging multiple CIL source trees into
   a single, coherent CIL tree which contains the union of all the
   definitions in the source files.  It effectively acts like a linker,
   but at the source code level instead of the object code level. *)

 module P = Pretty
 open Cil
 module E = Errormsg
 module H = Hashtbl
 module A = Alpha
 open Trace

 let debugMerge = false
 let debugInlines = false
 let ignore_merge_conflicts = ref false

 (* Try to merge structure with the same name. However, do not complain if
    they are not the same *)
 let mergeSynonyms = true

 (** Whether to use path compression *)
 let usePathCompression = false

 (* Try to merge definitions of inline functions. They can appear in multiple
    files and we would like them all to be the same. This can slow down the
    merger an order of magnitude !!! *)
 let merge_inlines = ref false
 let mergeInlinesRepeat () = !merge_inlines && true
 let mergeInlinesWithAlphaConvert () = !merge_inlines && true

 (* when true, merge duplicate definitions of externally-visible functions;
    this uses a mechanism which is faster than the one for inline functions,
    but only probabilistically accurate *)
 let mergeGlobals = true

 (* C99: inline functions are internal unless specified to be external
    GNU89: inline functions are external unless specified to be static or extern
    GNU89 inline semantics is used also when gnu_inline attribute is present on all inline declarations *)
 let externallyVisible vi =
  match vi.vstorage with
  | Static -> false
  | _ -> (match !Cil.cstd, !Cil.gnu89inline, hasAttribute "gnu_inline" (typeAttrs vi.vtype) with
    | Cil.C90, _, _
    | _, true, _
    | _, _, true -> not vi.vinline || vi.vstorage <> Extern
    | _, _, _ -> not vi.vinline || vi.vstorage = Extern)

 (* Return true if 's' starts with the prefix 'p' *)
 let prefix p s =
   let lp = String.length p in
   let ls = String.length s in
   lp <= ls && String.sub s 0 lp = p

 (* A name is identified by the index of the file in which it occurs (starting
    at 0 with the first file) and by the actual name. We'll keep name spaces
    separate *)

 (* We define a data structure for the equivalence classes *)
 type 'a node = {
   nname : string; (* The actual name *)
   nfidx : int; (* The file index *)
   ndata : 'a; (* Data associated with the node *)
   mutable nloc : (location * int) option;
   (* location where defined and index within the file of the definition.
      If None then it means that this node actually DOES NOT appear in the
      given file. In rare occasions we need to talk in a given file about
      types that are not defined in that file. This happens with undefined
      structures but also due to cross-contamination of types in a few of
      the cases of combineType (see the definition of combineTypes). We
      try never to choose as representatives nodes without a definition.
      We also choose as representative the one that appears earliest *)
   mutable nrep : 'a node;
   (* A pointer to another node in its class (one
      closer to the representative). The nrep node
      is always in an earlier file, except for the
      case where a name is undefined in one file
      and defined in a later file. If this pointer
      points to the node itself then this is the
      representative. *)
   mutable nmergedSyns : bool;
       (* Whether we have merged the synonyms for
          the node of this name *)
 }

 let d_nloc () (lo : (location * int) option) : P.doc =
   match lo with
   | None -> P.text "None"
   | Some (l, idx) -> P.dprintf "Some(%d at %a)" idx d_loc l

 (* Make a node with a self loop. This is quite tricky. *)
 let mkSelfNode (eq : (int * string, 'a node) H.t) (* The equivalence table *)
     (syn : (string, 'a node) H.t) (* The synonyms table *) (fidx : int)
     (name : string) (data : 'a) (l : (location * int) option) =
   let rec res =
     {
       nname = name;
       nfidx = fidx;
       ndata = data;
       nloc = l;
       nrep = res;
       nmergedSyns = false;
     }
   in
   H.add eq (fidx, name) res;
   (* Add it to the proper table *)
   if mergeSynonyms && not (prefix "__anon" name) then H.add syn name res;
   res

 let debugFind = false

 (* Find the representative with or without path compression *)
 let rec find (pathcomp : bool) (nd : 'a node) =
   if debugFind then ignore (E.log "  find %s(%d)\n" nd.nname nd.nfidx);
   if nd.nrep == nd then (
     if debugFind then ignore (E.log "  = %s(%d)\n" nd.nname nd.nfidx);
     nd)
   else
     let res = find pathcomp nd.nrep in
     if usePathCompression && pathcomp && nd.nrep != res then nd.nrep <- res;
     (* Compress the paths *)
     res

 (* Union two nodes and return the new representative. We prefer as the
    representative a node defined earlier. We try not to use as
    representatives nodes that are not defined in their files. We return a
    function for undoing the union. Make sure that between the union and the
    undo you do not do path compression *)
 let union (nd1 : 'a node) (nd2 : 'a node) : 'a node * (unit -> unit) =
   (* Move to the representatives *)
   let nd1 = find true nd1 in
   let nd2 = find true nd2 in
   if nd1 == nd2 then
     ( (* It can happen that we are trying to union two nodes that are already
          equivalent. This is because between the time we check that two nodes
          are not already equivalent and the time we invoke the union operation
          we check type isomorphism which might change the equivalence classes *)
       (*
     ignore (warn "unioning already equivalent nodes for %s(%d)"
               nd1.nname nd1.nfidx);
 *)
       nd1,
       fun x -> x )
   else
     let rep, norep =
       (* Choose the representative *)
       if nd1.nloc != None = (nd2.nloc != None) then (
         if
           (* They have the same defined status. Choose the earliest *)
           nd1.nfidx < nd2.nfidx
         then (nd1, nd2)
         else if nd1.nfidx > nd2.nfidx then (nd2, nd1)
         else
           (* In the same file. Choose the one with the earliest index *)
           match (nd1.nloc, nd2.nloc) with
           | Some (_, didx1), Some (_, didx2) ->
               if didx1 < didx2 then (nd1, nd2)
               else if didx1 > didx2 then (nd2, nd1)
               else (
                 ignore
                   (warn
                      "Merging two elements (%s and %s) in the same file (%d) \
                       with the same idx (%d) within the file"
                      nd1.nname nd2.nname nd1.nfidx didx1);
                 (nd1, nd2))
           | _, _ ->
               (* both none. Does not matter which one we choose. Should
                    not happen though. *)
               (* sm: it does happen quite a bit when, e.g. merging STLport with
                  some client source; I'm disabling the warning since it supposedly
                  is harmless anyway, so is useless noise *)
               (* sm: re-enabling on claim it now will probably not happen *)
               ignore
                 (warn
                    "Merging two undefined elements in the same file: %s and %s"
                    nd1.nname nd2.nname);
               (nd1, nd2))
       else if
         (* One is defined, the other is not. Choose the defined one *)
         nd1.nloc != None
       then (nd1, nd2)
       else (nd2, nd1)
     in
     let oldrep = norep.nrep in
     norep.nrep <- rep;
     (rep, fun () -> norep.nrep <- oldrep)

 (*
 let union (nd1: 'a node) (nd2: 'a node) : 'a node * (unit -> unit) =
   if nd1 == nd2 && nd1.nname = "!!!intEnumInfo!!!" then begin
     ignore (warn "unioning two identical nodes for %s(%d)"
               nd1.nname nd1.nfidx);
     nd1, fun x -> x
   end else
     union nd1 nd2
 *)
 (* Find the representative for a node and compress the paths in the process *)
 let findReplacement (pathcomp : bool) (eq : (int * string, 'a node) H.t)
     (fidx : int) (name : string) : ('a * int) option =
   if debugFind then ignore (E.log "findReplacement for %s(%d)\n" name fidx);
   try
     let nd = H.find eq (fidx, name) in
     if nd.nrep == nd then (
       if debugFind then ignore (E.log "  is a representative\n");
       None (* No replacement if this is the representative of its class *))
     else
       let rep = find pathcomp nd in
       if rep != rep.nrep then
         E.s (bug "find does not return the representative\n");
       if debugFind then ignore (E.log "  RES = %s(%d)\n" rep.nname rep.nfidx);
       Some (rep.ndata, rep.nfidx)
   with Not_found ->
     if debugFind then ignore (E.log "  not found in the map\n");
     None

 (* Make a node if one does not already exist. Otherwise return the
    representative *)
 let getNode (eq : (int * string, 'a node) H.t) (syn : (string, 'a node) H.t)
     (fidx : int) (name : string) (data : 'a) (l : (location * int) option) =
   let debugGetNode = false in
   if debugGetNode then ignore (E.log "getNode(%s(%d), %a)\n" name fidx d_nloc l);
   try
     let res = H.find eq (fidx, name) in

     (match (res.nloc, l) with
     (* Maybe we have a better location now *)
     | None, Some _ -> res.nloc <- l
     | Some (old_l, old_idx), Some (l, idx) ->
         if old_idx != idx then
           ignore
             (warn
                "Duplicate definition of node %s(%d) at indices %d(%a) and \
                 %d(%a)"
                name fidx old_idx d_loc old_l idx d_loc l)
         else ()
     | _, _ -> ());
     if debugGetNode then ignore (E.log "  node already found\n");
     find false res
     (* No path compression *)
   with Not_found ->
     let res = mkSelfNode eq syn fidx name data l in
     if debugGetNode then ignore (E.log "   made a new one\n");
     res

 (* Dump a graph *)
 let dumpGraph (what : string) (eq : (int * string, 'a node) H.t) : unit =
   ignore (E.log "Equivalence graph for %s is:\n" what);
   H.iter
     (fun (fidx, name) nd ->
       ignore
         (E.log "  %s(%d) %s-> " name fidx
            (if nd.nloc = None then "(undef)" else ""));
       if nd.nrep == nd then ignore (E.log "*\n")
       else ignore (E.log " %s(%d)\n" nd.nrep.nname nd.nrep.nfidx))
     eq

 (* For each name space we define a set of equivalence classes *)
 let vEq : (int * string, varinfo node) H.t = H.create 111 (* Vars *)

 let sEq : (int * string, compinfo node) H.t = H.create 111 (* Struct + union *)

 let eEq : (int * string, enuminfo node) H.t = H.create 111 (* Enums *)

 let tEq : (int * string, typeinfo node) H.t = H.create 111 (* Type names*)

 let iEq : (int * string, varinfo node) H.t = H.create 111 (* Inlines *)

 (* Sometimes we want to merge synonyms. We keep some tables indexed by names.
    Each name is mapped to multiple entries *)
 let vSyn : (string, varinfo node) H.t = H.create 111 (* Not actually used *)

 let iSyn : (string, varinfo node) H.t = H.create 111 (* Inlines *)

 let sSyn : (string, compinfo node) H.t = H.create 111
 let eSyn : (string, enuminfo node) H.t = H.create 111
 let tSyn : (string, typeinfo node) H.t = H.create 111

 (** A global environment for variables. Put in here only the non-static
     variables, indexed by their name.  *)
 let vEnv : (string, varinfo node) H.t = H.create 111

 (* A set of inline functions indexed by their printout ! *)
 let inlineBodies : (P.doc, varinfo node) H.t = H.create 111

 (** A number of alpha conversion tables. We ought to keep one table for each
    name space. Unfortunately, because of the way the C lexer works, type
    names must be different from variable names!! We one alpha table both for
    variables and types. *)
 let vtAlpha : (string, location A.alphaTableData ref) H.t = H.create 57
 (* Variables and types *)

 let sAlpha : (string, location A.alphaTableData ref) H.t = H.create 57
 (* Structures and unions have the same name space *)

 let eAlpha : (string, location A.alphaTableData ref) H.t = H.create 57
 (* Enumerations *)

 (** Keep track, for all global function definitions, of the names of the formal
    arguments. They might change during merging of function types if the
    prototype occurs after the function definition and uses different names.
    We'll restore the names at the end *)
 let formalNames : (int * string, string list) H.t = H.create 111

 (* Accumulate here the globals in the merged file *)
 let theFileTypes = ref []
 let theFile = ref []

 (* add 'g' to the merged file *)
 let mergePushGlobal (g : global) : unit =
   pushGlobal g ~types:theFileTypes ~variables:theFile

 let mergePushGlobals gl = List.iter mergePushGlobal gl

 (* The index of the current file being scanned *)
 let currentFidx = ref 0
 let currentDeclIdx = ref 0
 (* The index of the definition in a file. This is
    maintained both in pass 1 and in pass 2. Make
    sure you count the same things in both passes. *)

 (* Keep here the file names *)
 let fileNames : (int, string) H.t = H.create 113

 (* Remember the composite types that we have already declared *)
 let emittedCompDecls : (string, bool) H.t = H.create 113

 (* Remember the variables also *)
 let emittedVarDecls : (string, bool) H.t = H.create 113

 (* also keep track of externally-visible function definitions;
    name maps to declaration, location, and semantic checksum *)
 let emittedFunDefn : (string, fundec * location * int) H.t = H.create 113

 (* and same for variable definitions; name maps to GVar fields *)
 let emittedVarDefn : (string, varinfo * init option * location) H.t =
   H.create 113

 (** A mapping from the new names to the original names. Used in PASS2 when we
    rename variables. *)
 let originalVarNames : (string, string) H.t = H.create 113

 (* Initialize the module *)
 let init () =
   H.clear sAlpha;
   H.clear eAlpha;
   H.clear vtAlpha;

   H.clear vEnv;

   H.clear vEq;
   H.clear sEq;
   H.clear eEq;
   H.clear tEq;
   H.clear iEq;

   H.clear vSyn;
   H.clear sSyn;
   H.clear eSyn;
   H.clear tSyn;
   H.clear iSyn;

   theFile := [];
   theFileTypes := [];

   H.clear formalNames;
   H.clear inlineBodies;

   currentFidx := 0;
   currentDeclIdx := 0;
   H.clear fileNames;

   H.clear emittedVarDecls;
   H.clear emittedCompDecls;

   H.clear emittedFunDefn;
   H.clear emittedVarDefn;

   H.clear originalVarNames

 (* Some enumerations have to be turned into an integer. We implement this by
    introducing a special enumeration type which we'll recognize later to be
    an integer *)
 let intEnumInfo =
   {
     ename = "!!!intEnumInfo!!!";
     (* This is otherwise invalid *)
     eitems = [];
     eattr = [];
     ereferenced = false;
     ekind = IInt;
   }

 (* And add it to the equivalence graph *)
 let intEnumInfoNode =
   getNode eEq eSyn 0 intEnumInfo.ename intEnumInfo (Some (locUnknown, 0))

 (* Combine the types. Raises the Failure exception with an error message.
    isdef says whether the new type is for a definition *)
 type combineWhat =
   | CombineFundef (* The new definition is for a function definition. The old
                      is for a prototype *)
   | CombineFunarg (* Comparing a function argument type with an old prototype
                      arg *)
   | CombineFunret (* Comparing the return of a function with that from an old
                      prototype *)
   | CombineOther

 (** Construct the composite type of [oldt] and [t] if they are compatible.
     Raise [Failure] if they are incompatible. *)
 let rec combineTypes (what : combineWhat) (oldfidx : int) (oldt : typ)
     (fidx : int) (t : typ) : typ =
   let oldq, olda = partitionQualifierAttributes (typeAttrsOuter oldt) in
   let q, a = partitionQualifierAttributes (typeAttrsOuter t) in
   if oldq <> q then
     raise
       (Failure
          (P.sprint ~width:80
             (P.dprintf "(different type qualifiers %a and %a)" d_attrlist oldq
                d_attrlist q)))
   else if q <> [] then
     typeAddAttributes q
       (combineTypes what oldfidx (setTypeAttrs oldt olda) fidx
          (setTypeAttrs t a))
   else
     match (oldt, t) with
     | TVoid olda, TVoid a -> TVoid (addAttributes olda a)
     | TInt (oldik, olda), TInt (ik, a) ->
         let combineIK oldk k =
           if oldk == k then oldk
           else if
             (* GCC allows a function definition to have a more precise integer
                type than a prototype that says "int" *)
             oldk = IInt
             && bitsSizeOf t <= 32
             && (what = CombineFunarg || what = CombineFunret)
           then k
           else
             let msg =
               P.sprint ~width:80
                 (P.dprintf "(different integer types %a and %a)" d_type oldt
                    d_type t)
             in
             raise (Failure msg)
         in
         TInt (combineIK oldik ik, addAttributes olda a)
     | TFloat (oldfk, olda), TFloat (fk, a) ->
         let combineFK oldk k =
           if oldk == k then oldk
           else if
             (* GCC allows a function definition to have a more precise integer
                type than a prototype that says "double" *)
             oldk = FDouble && k = FFloat
             && (what = CombineFunarg || what = CombineFunret)
           then k
           else raise (Failure "(different floating point types)")
         in
         TFloat (combineFK oldfk fk, addAttributes olda a)
     | TEnum (oldei, olda), TEnum (ei, a) ->
         (* Matching enumerations always succeeds. But sometimes it maps both
            enumerations to integers *)
         matchEnumInfo oldfidx oldei fidx ei;
         TEnum (oldei, addAttributes olda a)
         (* Strange one. But seems to be handled by GCC *)
     | TEnum (oldei, olda), TInt (IInt, a) ->
         TEnum (oldei, addAttributes olda a)
         (* Strange one. But seems to be handled by GCC. Warning. Here we are
            leaking types from new to old *)
     | TInt (IInt, olda), TEnum (ei, a) -> TEnum (ei, addAttributes olda a)
     | TComp (oldci, olda), TComp (ci, a) ->
         matchCompInfo oldfidx oldci fidx ci;
         (* If we get here we were successful *)
         TComp (oldci, addAttributes olda a)
     | TArray (oldbt, oldsz, olda), TArray (bt, sz, a) ->
         let combbt = combineTypes CombineOther oldfidx oldbt fidx bt in
         let combinesz =
           match (oldsz, sz) with
           | None, Some _ -> sz
           | Some _, None -> oldsz
           | None, None -> oldsz
           | Some oldsz', Some sz' ->
               let samesz =
                 match (constFold true oldsz', constFold true sz') with
                 | Const (CInt (oldi, _, _)), Const (CInt (i, _, _)) ->
                     Cilint.compare_cilint oldi i = 0
                 | _, _ -> false
               in
               if samesz then oldsz
               else raise (Failure "(different array sizes)")
         in
         TArray (combbt, combinesz, addAttributes olda a)
     | TPtr (oldbt, olda), TPtr (bt, a) ->
         TPtr
           (combineTypes CombineOther oldfidx oldbt fidx bt, addAttributes olda a)
         (* WARNING: In this case we are leaking types from new to old !! *)
     | TFun (_, _, _, [ Attr ("missingproto", _) ]), TFun _ -> t
     | TFun _, TFun (_, _, _, [ Attr ("missingproto", _) ]) -> oldt
     | TFun (oldrt, oldargs, oldva, olda), TFun (rt, args, va, a) ->
         let newrt =
           combineTypes
             (if what = CombineFundef then CombineFunret else CombineOther)
             oldfidx oldrt fidx rt
         in
         if oldva != va then raise (Failure "(different vararg specifiers)");
         (* If one does not have arguments, believe the one with the
              arguments *)
         let newargs =
           if oldargs = None then args
           else if args = None then oldargs
           else
             let oldargslist = argsToList oldargs in
             let argslist = argsToList args in
             if List.length oldargslist <> List.length argslist then
               raise (Failure "(different number of arguments)")
             else
               (* Go over the arguments and update the old ones with the
                    adjusted types *)
               Some
                 (List.map2
                    (fun (on, ot, oa) (an, at, aa) ->
                      let n = if an <> "" then an else on in
                      let t =
                        combineTypes
                          (if what = CombineFundef then CombineFunarg
                          else CombineOther)
                          oldfidx
                          (removeOuterQualifierAttributes ot)
                          fidx
                          (removeOuterQualifierAttributes at)
                      in
                      let a = addAttributes oa aa in
                      (n, t, a))
                    oldargslist argslist)
         in
         TFun (newrt, newargs, oldva, addAttributes olda a)
     | TBuiltin_va_list olda, TBuiltin_va_list a ->
         TBuiltin_va_list (addAttributes olda a)
     | TNamed (oldt, olda), TNamed (t, a) ->
         matchTypeInfo oldfidx oldt fidx t;
         (* If we get here we were able to match *)
         TNamed (oldt, addAttributes olda a)
         (* Unroll first the new type *)
     | _, TNamed (t, a) ->
         let res = combineTypes what oldfidx oldt fidx t.ttype in
         typeAddAttributes a res
         (* And unroll the old type as well if necessary *)
     | TNamed (oldt, a), _ ->
         let res = combineTypes what oldfidx oldt.ttype fidx t in
         typeAddAttributes a res
     | _ ->
         (* raise (Failure "(different type constructors)") *)
         let msg : string =
           P.sprint ~width:1000
             (P.dprintf "(different type constructors: %a vs. %a)" d_type oldt
                d_type t)
         in
         raise (Failure msg)

 (* Match two compinfos and throw a Failure if they do not match *)
 and matchCompInfo (oldfidx : int) (oldci : compinfo) (fidx : int)
     (ci : compinfo) : unit =
   if oldci.cstruct <> ci.cstruct then
     raise (Failure "(different struct/union types)");
   (* See if we have a mapping already *)
   (* Make the nodes if not already made. Actually return the
        representatives *)
   let oldcinode = getNode sEq sSyn oldfidx oldci.cname oldci None in
   let cinode = getNode sEq sSyn fidx ci.cname ci None in
   if oldcinode == cinode then (* We already know they are the same *)
     ()
   else
     (* Replace with the representative data *)
     let oldci = oldcinode.ndata in
     let oldfidx = oldcinode.nfidx in
     let ci = cinode.ndata in
     let fidx = cinode.nfidx in

     let old_len = List.length oldci.cfields in
     let len = List.length ci.cfields in
     (* It is easy to catch here the case when the new structure is undefined
        and the old one was defined. We just reuse the old *)
     (* More complicated is the case when the old one is not defined but the
        new one is. We still reuse the old one and we'll take care of defining
        it later with the new fields.
        GN: 7/10/04, I could not find when is "later", so I added it below *)
     if len <> 0 && old_len <> 0 && old_len <> len then (
       let curLoc = !currentLoc in
       (* d_global blows this away.. *)
       trace "merge"
         (P.dprintf "different # of fields\n%d: %a\n%d: %a\n" old_len d_global
            (GCompTag (oldci, locUnknown))
            len d_global
            (GCompTag (ci, locUnknown)));
       currentLoc := curLoc;
       let msg =
         Printf.sprintf "(different number of fields in %s and %s: %d != %d.)"
           oldci.cname ci.cname old_len len
       in
       raise (Failure msg));
     (* We check that they are defined in the same way. While doing this there
        might be recursion and we have to watch for going into an infinite
        loop. So we add the assumption that they are equal *)
     let newrep, undo = union oldcinode cinode in
     (* We check the fields but watch for Failure. We only do the check when
        the lengths are the same. Due to the code above this the other
        possibility is that one of the length is 0, in which case we reuse the
        old compinfo. *)
     (* But what if the old one is the empty one ? *)
     if old_len = len then (
       try
         List.iter2
           (fun oldf f ->
             if oldf.fbitfield <> f.fbitfield then
               raise (Failure "(different bitfield info)");
             if oldf.fattr <> f.fattr then
               raise (Failure "(different field attributes)");
             (* Make sure the types are compatible *)
             let newtype =
               combineTypes CombineOther oldfidx oldf.ftype fidx f.ftype
             in
             (* Change the type in the representative *)
             oldf.ftype <- newtype)
           oldci.cfields ci.cfields
       with Failure reason ->
         (* Our assumption was wrong. Forget the isomorphism *)
         undo ();
         let msg =
           P.sprint ~width:80
             (P.dprintf
                "\n\tFailed assumption that %s and %s are isomorphic %s@!%a@!%a"
                (compFullName oldci) (compFullName ci) reason dn_global
                (GCompTag (oldci, locUnknown))
                dn_global
                (GCompTag (ci, locUnknown)))
         in
         raise (Failure msg))
     else if
       (* We will reuse the old one. One of them is empty. If the old one is
          empty, copy over the fields from the new one. Won't this result in
          all sorts of undefined types??? *)
       old_len = 0
     then oldci.cfields <- ci.cfields;
     (* We get here when we succeeded checking that they are equal, or one of
        them was empty *)
     newrep.ndata.cattr <- addAttributes oldci.cattr ci.cattr;
     ()

 (* Match two enuminfos and throw a Failure if they do not match *)
 and matchEnumInfo (oldfidx : int) (oldei : enuminfo) (fidx : int)
     (ei : enuminfo) : unit =
   (* Find the node for this enum, no path compression. *)
   let oldeinode = getNode eEq eSyn oldfidx oldei.ename oldei None in
   let einode = getNode eEq eSyn fidx ei.ename ei None in
   if oldeinode == einode then (* We already know they are the same *)
     ()
   else
     (* Replace with the representative data *)
     let oldei = oldeinode.ndata in
     let ei = einode.ndata in
     (* Try to match them. But if you cannot just make them both integers *)
     try
       (* We do not have a mapping. They better be defined in the same way *)
       if List.length oldei.eitems <> List.length ei.eitems then
         raise (Failure "(different number of enumeration elements)");
       (* We check that they are defined in the same way. This is a fairly
            conservative check. *)
       List.iter2
         (fun (old_iname, old_attrs, old_iv, _) (iname, attrs, iv, _) ->
           if old_iname <> iname then
             raise (Failure "(different names for enumeration items)");
           if old_attrs <> attrs then
             raise (Failure "(different enumerator attributes)");
           let samev =
             match (constFold true old_iv, constFold true iv) with
             | Const (CInt (oldi, _, _)), Const (CInt (i, _, _)) ->
                 Cilint.compare_cilint oldi i = 0
             | _ -> false
           in
           if not samev then
             raise (Failure "(different values for enumeration items)"))
         oldei.eitems ei.eitems;
       (* Set the representative *)
       let newrep, _ = union oldeinode einode in
       (* We get here if the enumerations match *)
       newrep.ndata.eattr <- addAttributes oldei.eattr ei.eattr;
       ()
     with Failure msg ->
       (* Get here if you cannot merge two enumeration nodes *)
       (if oldeinode != intEnumInfoNode then
        let _ = union oldeinode intEnumInfoNode in
        ());
       if einode != intEnumInfoNode then
         let _ = union einode intEnumInfoNode in
         ()

 (* Match two typeinfos and throw a Failure if they do not match *)
 and matchTypeInfo (oldfidx : int) (oldti : typeinfo) (fidx : int)
     (ti : typeinfo) : unit =
   if oldti.tname = "" || ti.tname = "" then
     E.s (bug "matchTypeInfo for anonymous type\n");
   (* Find the node for this enum, no path compression. *)
   let oldtnode = getNode tEq tSyn oldfidx oldti.tname oldti None in
   let tnode = getNode tEq tSyn fidx ti.tname ti None in
   if oldtnode == tnode then (* We already know they are the same *)
     ()
   else
     (* Replace with the representative data *)
     let oldti = oldtnode.ndata in
     let oldfidx = oldtnode.nfidx in
     let ti = tnode.ndata in
     let fidx = tnode.nfidx in
     (* Check that they are the same *)
     (try ignore (combineTypes CombineOther oldfidx oldti.ttype fidx ti.ttype)
      with Failure reason ->
        let msg =
          P.sprint ~width:80
            (P.dprintf "\n\tFailed assumption that %s and %s are isomorphic %s"
               oldti.tname ti.tname reason)
        in
        raise (Failure msg));
     let _ = union oldtnode tnode in
     ()

 (* Scan all files and do two things *)
 (* 1. Initialize the alpha renaming tables with the names of the globals so
    that when we come in the second pass to generate new names, we do not run
    into conflicts. *)
 (* 2. For all declarations of globals unify their types. In the process
    construct a set of equivalence classes on type names, structure and
    enumeration tags *)
 (* 3. We clean the referenced flags *)

 let oneFilePass1 (f : file) : unit =
   H.add fileNames !currentFidx f.fileName;
   if debugMerge || !E.verboseFlag then
     ignore (E.log "Pre-merging (%d) %s\n" !currentFidx f.fileName);
   currentDeclIdx := 0;
   if f.globinitcalled || f.globinit <> None then
     E.s (E.warn "Merging file %s has global initializer" f.fileName);

   (* We scan each file and we look at all global varinfo. We see if globals
      with the same name have been encountered before and we merge those types
      *)
   let matchVarinfo (vi : varinfo) (l : location * int) =
     ignore
       (Alpha.registerAlphaName ~alphaTable:vtAlpha ~undolist:None
          ~lookupname:vi.vname ~data:!currentLoc);
     (* Make a node for it and put it in vEq *)
     let vinode = mkSelfNode vEq vSyn !currentFidx vi.vname vi (Some l) in
     try
       let oldvinode = find true (H.find vEnv vi.vname) in
       let oldloc, _ =
         match oldvinode.nloc with
         | None -> E.s (bug "old variable is undefined")
         | Some l -> l
       in
       let oldvi = oldvinode.ndata in
       (* There is an old definition. We must combine the types. Do this first
          because it might fail *)
       let newtype =
         try
           combineTypes CombineOther oldvinode.nfidx oldvi.vtype !currentFidx
             vi.vtype
         with Failure reason ->
           (* Go ahead *)
           let f = if !ignore_merge_conflicts then warn else error in
           ignore
             (f
                "Incompatible declaration for %s (from %s(%d)).@! Previous was \
                 at %a (from %s (%d)) %s "
                vi.vname
                (H.find fileNames !currentFidx)
                !currentFidx d_loc oldloc
                (H.find fileNames oldvinode.nfidx)
                oldvinode.nfidx reason);
           raise Not_found
       in
       let newrep, _ = union oldvinode vinode in
       (* We do not want to turn non-"const" globals into "const" one. That
          can happen if one file declares the variable a non-const while
          others declare it as "const". *)
       if
         hasAttribute "const" (typeAttrs vi.vtype)
         != hasAttribute "const" (typeAttrs oldvi.vtype)
         || hasAttribute "pconst" (typeAttrs vi.vtype)
            != hasAttribute "pconst" (typeAttrs oldvi.vtype)
       then
         newrep.ndata.vtype <- typeRemoveAttributes [ "const"; "pconst" ] newtype
       else newrep.ndata.vtype <- newtype;
       (* clean up the storage. *)
       let newstorage =
         if vi.vstorage = oldvi.vstorage || vi.vstorage = Extern then
           oldvi.vstorage
         else if oldvi.vstorage = Extern then vi.vstorage
           (* Sometimes we turn the NoStorage specifier into Static for inline
              functions *)
         else if oldvi.vstorage = Static && vi.vstorage = NoStorage then Static
         else (
           ignore
             (warn
                "Inconsistent storage specification for %s. Now is %a and \
                 previous was %a at %a"
                vi.vname d_storage vi.vstorage d_storage oldvi.vstorage d_loc
                oldloc);
           vi.vstorage)
       in
       newrep.ndata.vstorage <- newstorage;
       newrep.ndata.vattr <- addAttributes oldvi.vattr vi.vattr;
       ()
     with Not_found ->
       (* Not present in the previous files. Remember it for
          later *)
       H.add vEnv vi.vname vinode
   in

   List.iter
     (function
       | GVarDecl (vi, l) | GVar (vi, _, l) ->
           currentLoc := l;
           incr currentDeclIdx;
           vi.vreferenced <- false;
           if externallyVisible vi then matchVarinfo vi (l, !currentDeclIdx)
       | GFun (fdec, l) ->
           currentLoc := l;
           incr currentDeclIdx;
           (* Save the names of the formal arguments *)
           let _, args, _, _ = splitFunctionTypeVI fdec.svar in
           H.add formalNames
             (!currentFidx, fdec.svar.vname)
             (Util.list_map (fun (fn, _, _) -> fn) (argsToList args));
           fdec.svar.vreferenced <- false;
           if externallyVisible fdec.svar then
             (* function with external linkage *)
             matchVarinfo fdec.svar (l, !currentDeclIdx)
           else if fdec.svar.vinline && !merge_inlines then
             (* Just create the nodes for inline functions *)
             ignore
               (getNode iEq iSyn !currentFidx fdec.svar.vname fdec.svar
                  (Some (l, !currentDeclIdx)))
           (* Make nodes for the defined type and structure tags *)
       | GType (t, l) -> (
           incr currentDeclIdx;
           t.treferenced <- false;
           if t.tname <> "" then
             (* The empty names are just for introducing
                undefined comp tags *)
             ignore
               (getNode tEq tSyn !currentFidx t.tname t
                  (Some (l, !currentDeclIdx)))
           else
             (* Go inside and clean the referenced flag for the
                declared tags *)
             match t.ttype with
             | TComp (ci, _) ->
                 ci.creferenced <- false;
                 (* Create a node for it *)
                 ignore (getNode sEq sSyn !currentFidx ci.cname ci None)
             | TEnum (ei, _) ->
                 ei.ereferenced <- false;
                 ignore (getNode eEq eSyn !currentFidx ei.ename ei None)
             | _ -> E.s (bug "Anonymous Gtype is not TComp"))
       | GCompTag (ci, l) ->
           incr currentDeclIdx;
           ci.creferenced <- false;
           ignore
             (getNode sEq sSyn !currentFidx ci.cname ci
                (Some (l, !currentDeclIdx)))
       | GEnumTag (ei, l) ->
           incr currentDeclIdx;
           ei.ereferenced <- false;
           ignore
             (getNode eEq eSyn !currentFidx ei.ename ei
                (Some (l, !currentDeclIdx)))
       | _ -> ())
     f.globals

 (* Try to merge synonyms. Do not give an error if they fail to merge *)
 let doMergeSynonyms (syn : (string, 'a node) H.t)
     (eq : (int * string, 'a node) H.t)
     (compare : int -> 'a -> int -> 'a -> unit) : unit =
   (* A comparison function that
      throws Failure if no match *)
   H.iter
     (fun n node ->
       if not node.nmergedSyns then
         (* find all the nodes for the same name *)
         let all = H.find_all syn n in
         let tryone (classes : 'a node list)
             (* A number of representatives
                    for this name *) (nd : 'a node) : 'a node list
             (* Returns an expanded set
                of classes *) =
           nd.nmergedSyns <- true;
           (* Compare in turn with all the classes we have so far *)
           let rec compareWithClasses = function
             | [] -> [ nd ] (* No more classes. Add this as a new class *)
             | c :: restc -> (
                 try
                   compare c.nfidx c.ndata nd.nfidx nd.ndata;
                   (* Success. Stop here the comparison *)
                   c :: restc
                 with Failure _ ->
                   (* Failed. Try next class *)
                   c :: compareWithClasses restc)
           in
           compareWithClasses classes
         in
         (* Start with an empty set of classes for this name *)
         let _ = List.fold_left tryone [] all in
         ())
     syn

 let matchInlines (oldfidx : int) (oldi : varinfo) (fidx : int) (i : varinfo) =
   let oldinode = getNode iEq iSyn oldfidx oldi.vname oldi None in
   let inode = getNode iEq iSyn fidx i.vname i None in
   if oldinode == inode then ()
   else
     (* Replace with the representative data *)
     let oldi = oldinode.ndata in
     let oldfidx = oldinode.nfidx in
     let i = inode.ndata in
     let fidx = inode.nfidx in
     (* There is an old definition. We must combine the types. Do this first
        because it might fail *)
     oldi.vtype <- combineTypes CombineOther oldfidx oldi.vtype fidx i.vtype;
     (* We get here if we have success *)
     (* Combine the attributes as well *)
     oldi.vattr <- addAttributes oldi.vattr i.vattr;
     (* Do not union them yet because we do not know that they are the same.
        We have checked only the types so far *)
     ()

 (************************************************************

     PASS 2


  ************************************************************)

 (** Keep track of the functions we have used already in the file. We need
     this to avoid removing an inline function that has been used already.
     This can only occur if the inline function is defined after it is used
     already; a bad style anyway *)
 let varUsedAlready : (string, unit) H.t = H.create 111

 (** A visitor that renames uses of variables and types *)
 class renameVisitorClass =
   object (self)
     inherit nopCilVisitor

     (* This is either a global variable which we took care of, or a local
        variable. Must do its type and attributes. *)
     method! vvdec (vi : varinfo) = DoChildren

     method! vglob (g : global) : global list visitAction =
       match g with
       | GVar (v, init, loc) ->
           let update_init glob =
             match glob with
             | GVar (u, uinit, loc) -> GVar (u, u.vinit, loc)
             | _ -> glob
           in
           let update_all_inits = List.map update_init in
           let () =
             match (v.vinit.init, init.init) with
             | None, None -> ()
             (* This case may happen when a definition is encountered, but
                the variable was already seen through a declaration and thus
                has no definition *)
             | None, Some _ -> v.vinit.init <- init.init
             (* The following case should never happen because it should never be emitted *)
             | Some _, None -> assert false
             (* The following case is either never emitted (same
                initializations, or different initializations but an error is
                thrown) or emitted when first encountering a definition
                (hence the initializations are supposed to be identical) *)
             | Some _, Some _ -> ()
           in
           ChangeDoChildrenPost ([ g ], update_all_inits)
       | _ -> DoChildren

     (* This is a variable use. See if we must change it *)
     method! vvrbl (vi : varinfo) : varinfo visitAction =
       if not vi.vglob then DoChildren
       else if vi.vreferenced then (
         H.add varUsedAlready vi.vname ();
         DoChildren)
       else
         match findReplacement true vEq !currentFidx vi.vname with
         | None -> DoChildren
         | Some (vi', oldfidx) ->
             if debugMerge then
               ignore
                 (E.log "Renaming use of var %s(%d) to %s(%d)\n" vi.vname
                    !currentFidx vi'.vname oldfidx);
             vi'.vreferenced <- true;
             H.add varUsedAlready vi'.vname ();
             ChangeTo vi'

     (* The use of a type. Change only those types whose underlying info
        is not a root. *)
     method! vtype (t : typ) =
       match t with
       | TComp (ci, a) when not ci.creferenced -> (
           match findReplacement true sEq !currentFidx ci.cname with
           | None -> DoChildren
           | Some (ci', oldfidx) ->
               if debugMerge then
                 ignore
                   (E.log "Renaming use of %s(%d) to %s(%d)\n" ci.cname
                      !currentFidx ci'.cname oldfidx);
               ChangeTo (TComp (ci', visitCilAttributes (self :> cilVisitor) a)))
       | TEnum (ei, a) when not ei.ereferenced -> (
           match findReplacement true eEq !currentFidx ei.ename with
           | None -> DoChildren
           | Some (ei', _) ->
               if ei' == intEnumInfo then
                 (* This is actually our friend intEnumInfo *)
                 ChangeTo
                   (TInt (IInt, visitCilAttributes (self :> cilVisitor) a))
               else
                 ChangeTo
                   (TEnum (ei', visitCilAttributes (self :> cilVisitor) a)))
       | TNamed (ti, a) when not ti.treferenced -> (
           match findReplacement true tEq !currentFidx ti.tname with
           | None -> DoChildren
           | Some (ti', _) ->
               ChangeTo (TNamed (ti', visitCilAttributes (self :> cilVisitor) a))
           )
       | _ -> DoChildren

     (* The Field offset might need to be changed to use new compinfo *)
     method! voffs =
       function
       | Field (f, o) -> (
           if (* See if the compinfo was changed *)
              f.fcomp.creferenced then DoChildren
           else
             match findReplacement true sEq !currentFidx f.fcomp.cname with
             | None -> DoChildren (* We did not replace it *)
             | Some (ci', oldfidx) ->
                 (* First, find out the index of the original field *)
                 let rec indexOf (i : int) = function
                   | [] ->
                       E.s
                         (bug "Cannot find field %s in %s(%d)\n" f.fname
                            (compFullName f.fcomp) !currentFidx)
                   | f' :: rest when f' == f -> i
                   | _ :: rest -> indexOf (i + 1) rest
                 in
                 let index = indexOf 0 f.fcomp.cfields in
                 if List.length ci'.cfields <= index then
                   E.s
                     (bug "Too few fields in replacement %s(%d) for %s(%d)\n"
                        (compFullName ci') oldfidx (compFullName f.fcomp)
                        !currentFidx);
                 let f' = List.nth ci'.cfields index in
                 ChangeDoChildrenPost (Field (f', o), fun x -> x))
       | _ -> DoChildren

     method! vinitoffs o = self#voffs o
     (* treat initializer offsets same as lvalue offsets *)
   end

 let renameVisitor = new renameVisitorClass

 (** A visitor that renames uses of inline functions that were discovered in
    pass 2 to be used before they are defined. This is like the renameVisitor
    except it only looks at the variables (thus it is a bit more efficient)
    and it also renames forward declarations of the inlines to be removed. *)

 class renameInlineVisitorClass =
   object (self)
     inherit nopCilVisitor

     (* This is a variable use. See if we must change it *)
     method! vvrbl (vi : varinfo) : varinfo visitAction =
       if not vi.vglob then DoChildren
       else if vi.vreferenced then (* Already renamed *)
         DoChildren
       else
         match findReplacement true vEq !currentFidx vi.vname with
         | None -> DoChildren
         | Some (vi', oldfidx) ->
             if debugMerge then
               ignore
                 (E.log "Renaming var %s(%d) to %s(%d)\n" vi.vname !currentFidx
                    vi'.vname oldfidx);
             vi'.vreferenced <- true;
             ChangeTo vi'

     (* And rename some declarations of inlines to remove. We cannot drop this
        declaration (see small1/combineinline6) *)
     method! vglob =
       function
       | GVarDecl (vi, l) when vi.vinline -> (
           (* Get the original name *)
           let origname =
             try H.find originalVarNames vi.vname with Not_found -> vi.vname
           in
           (* Now see if this must be replaced *)
           match findReplacement true vEq !currentFidx origname with
           | None -> DoChildren
           | Some (vi', _) -> ChangeTo [ GVarDecl (vi', l) ])
       | _ -> DoChildren
   end

 let renameInlinesVisitor = new renameInlineVisitorClass

 (* sm: First attempt at a semantic checksum for function bodies.
    Ideally, two function's checksums would be equal only when their
    bodies were provably equivalent; but I'm using a much simpler and
    less accurate heuristic here.  It should be good enough for the
    purpose I have in mind, which is doing duplicate removal of
    multiply-instantiated template functions. *)
 let functionChecksum (dec : fundec) : int =
   (* checksum the structure of the statements (only) *)
   let rec stmtListSum (lst : stmt list) : int =
     List.fold_left (fun acc s -> acc + stmtSum s) 0 lst
   and stmtSum (s : stmt) : int =
     (* strategy is to just throw a lot of prime numbers into the
        computation in hopes of avoiding accidental collision.. *)
     match s.skind with
     | Instr l -> 13 + (67 * List.length l)
     | Return _ -> 17
     | Goto _ -> 19
     | ComputedGoto _ -> 131
     | Break _ -> 23
     | Continue _ -> 29
     | If (_, b1, b2, _, _) -> 31 + (37 * stmtListSum b1.bstmts) + (41 * stmtListSum b2.bstmts)
     | Switch (_, b, _, _, _) -> 43 + (47 * stmtListSum b.bstmts) (* don't look at stmt list b/c is not part of tree *)
     | Loop (b, _, _, _, _) -> 49 + (53 * stmtListSum b.bstmts)
     | Block b -> 59 + (61 * stmtListSum b.bstmts)
   in

   (* disabled 2nd and 3rd measure because they appear to get different
      values, for the same code, depending on whether the code was just
      parsed into CIL or had previously been parsed into CIL, printed
      out, then re-parsed into CIL *)
   let a, b, c, d, e =
     ( List.length dec.sformals,
       (* # formals *)
       0 (*(List.length dec.slocals)*),
       (* # locals *)
       0 (*dec.smaxid*),
       (* estimate of internal statement count *)
       List.length dec.sbody.bstmts,
       (* number of statements at outer level *)
       stmtListSum dec.sbody.bstmts )
   in
   (* checksum of statement structure *)
   (*(trace "sm" (P.dprintf "sum: %s is %d %d %d %d %d\n"*)
   (*                       dec.svar.vname a b c d e));*)
   (2 * a) + (3 * b) + (5 * c) + (7 * d) + (11 * e)

 (* sm: equality for initializers, etc.; this is like '=', except
    when we reach shared pieces (like references into the type
    structure), we use '==', to prevent circularity *)
 (* update: that's no good; I'm using this to find things which
    are equal but from different CIL trees, so nothing will ever
    be '=='.. as a hack I'll just change those places to 'true',
    so these functions are not now checking proper equality..
    places where equality is not complete are marked "INC" *)
 let rec equalInits (x : init) (y : init) : bool =
   match (x, y) with
   | SingleInit xe, SingleInit ye -> equalExps xe ye
   | CompoundInit (xt, xoil), CompoundInit (yt, yoil) ->
       (*(xt == yt) &&*)
       (* INC *)
       (* types need to be identically equal *)
       let rec equalLists xoil yoil : bool =
         match (xoil, yoil) with
         | (xo, xi) :: xrest, (yo, yi) :: yrest -> equalOffsets xo yo && equalInits xi yi && equalLists xrest yrest
         | [], [] -> true
         | _, _ -> false
       in
       equalLists xoil yoil
   | _, _ -> false

 and equalOffsets (x : offset) (y : offset) : bool =
   match (x, y) with
   | NoOffset, NoOffset -> true
   | Field (xfi, xo), Field (yfi, yo) ->
       xfi.fname = yfi.fname
       && (* INC: same fieldinfo name.. *)
       equalOffsets xo yo
   | Index (xe, xo), Index (ye, yo) -> equalExps xe ye && equalOffsets xo yo
   | _, _ -> false

 and equalExps (x : exp) (y : exp) : bool =
   match (x, y) with
   | Const xc, Const yc -> (
       xc = yc
       ||
       (* safe to use '=' on literals *)
       (* CIL changes (unsigned)0 into 0U during printing.. *)
       match (xc, yc) with
       | CInt (a, _, _), CInt (b, _, _) -> Cilint.is_zero_cilint a && Cilint.is_zero_cilint b (* ok if they're both 0 *)
       | _, _ -> false)
   | Lval xl, Lval yl -> equalLvals xl yl
   | SizeOf xt, SizeOf yt ->
       true
       (*INC: xt == yt*)
       (* identical types *)
   | SizeOfE xe, SizeOfE ye -> equalExps xe ye
   | AlignOf xt, AlignOf yt -> true (*INC: xt == yt*)
   | AlignOfE xe, AlignOfE ye -> equalExps xe ye
   | UnOp (xop, xe, xt), UnOp (yop, ye, yt) ->
       xop = yop && equalExps xe ye && true (*INC: xt == yt*)
   | BinOp (xop, xe1, xe2, xt), BinOp (yop, ye1, ye2, yt) ->
       xop = yop && equalExps xe1 ye1 && equalExps xe2 ye2 && true
       (*INC: xt == yt*)
   | CastE (xt, xe), CastE (yt, ye) ->
       (*INC: xt == yt &&*)
       equalExps xe ye
   | AddrOf xl, AddrOf yl -> equalLvals xl yl
   | StartOf xl, StartOf yl -> equalLvals xl yl
   (* initializers that go through CIL multiple times sometimes lose casts they
      had the first time; so allow a different of a cast *)
   | CastE (xt, xe), ye -> equalExps xe ye
   | xe, CastE (yt, ye) -> equalExps xe ye
   | _, _ -> false

 and equalLvals (x : lval) (y : lval) : bool =
   match (x, y) with
   | (Var xv, xo), (Var yv, yo) ->
       (* I tried, I really did.. the problem is I see these names
          before merging collapses them, so __T123 != __T456,
          so whatever *)
       (*(xv.vname = vy.vname) &&      (* INC: same varinfo names.. *)*)
       equalOffsets xo yo
   | (Mem xe, xo), (Mem ye, yo) -> equalExps xe ye && equalOffsets xo yo
   | _, _ -> false

 let equalInitOpts (x : init option) (y : init option) : bool =
   match (x, y) with
   | None, None -> true
   | Some xi, Some yi -> equalInits xi yi
   | _, _ -> false

 (* The comparion of inline functions is based on pretty printing (!?) *)
 let printInlineForComparison fdec' g' =
   (* Temporarily turn off printing of lines *)
   let oldprintln = !lineDirectiveStyle in
   lineDirectiveStyle := None;
   (* Temporarily set the name to all functions in the same way *)
   let newname = fdec'.svar.vname in
   fdec'.svar.vname <- "@@alphaname@@";
   (* If we must do alpha conversion then temporarily set the
      names of the local variables and formals in a standard way *)
   let nameId = ref 0 in
   let oldNames : string list ref = ref [] in
   let renameOne (v : varinfo) =
     oldNames := v.vname :: !oldNames;
     incr nameId;
     v.vname <- "___alpha" ^ string_of_int !nameId
   in
   let undoRenameOne (v : varinfo) =
     match !oldNames with
     | n :: rest ->
         oldNames := rest;
         v.vname <- n
     | _ -> E.s (bug "undoRenameOne")
   in
   (* Remember the original type *)
   let origType = fdec'.svar.vtype in
   if mergeInlinesWithAlphaConvert () then (
     (* Rename the formals *)
     List.iter renameOne fdec'.sformals;
     (* Reflect in the type *)
     setFormals fdec' fdec'.sformals;
     (* Now do the locals *)
     List.iter renameOne fdec'.slocals);
   (* Now print it *)
   let res = d_global () g' in
   lineDirectiveStyle := oldprintln;
   fdec'.svar.vname <- newname;
   if mergeInlinesWithAlphaConvert () then (
     (* Do the locals in reverse order *)
     List.iter undoRenameOne (List.rev fdec'.slocals);
     (* Do the formals in reverse order *)
     List.iter undoRenameOne (List.rev fdec'.sformals);
     (* Restore the type *)
     fdec'.svar.vtype <- origType);
   res

 (* Now we go once more through the file and we rename the globals that we
    keep. We also scan the entire body and we replace references to the
    representative types or variables. We set the referenced flags once we
    have replaced the names. *)
 let oneFilePass2 (f : file) =
   if debugMerge || !E.verboseFlag then
     ignore (E.log "Final merging phase (%d): %s\n" !currentFidx f.fileName);
   currentDeclIdx := 0;
   (* Even though we don't need it anymore *)
   H.clear varUsedAlready;
   H.clear originalVarNames;
   (* If we find inline functions that are used before being defined, and thus
      before knowing that we can throw them away, then we mark this flag so
      that we can make another pass over the file *)
   let repeatPass2 = ref false in
   (* Keep a pointer to the contents of the file so far *)
   let savedTheFile = !theFile in

   let processOneGlobal (g : global) : unit =
     (* Process a varinfo. Reuse an old one, or rename it if necessary *)
     let processVarinfo ~isadef (vi : varinfo) (vloc : location) : varinfo =
       if vi.vreferenced then vi (* Already done *)
       else if not (externallyVisible vi) then
          (* rename static and not-external inline functions no matter if merge_inlines is enabled or not,
          renaming is undone using originalVarNames in case merging is successful *)
        (
         (* Maybe it is static or inline and we are not merging inlines. Rename it then *)
         let newName, _ = A.newAlphaName ~alphaTable:vtAlpha ~undolist:None ~lookupname:vi.vname ~data:!currentLoc in
         (* Remember the original name *)
         H.add originalVarNames newName vi.vname;
         if debugMerge then ignore (E.log "renaming %s at %a to %s\n" vi.vname d_loc vloc newName);
         vi.vname <- newName;
         vi.vid <- newVID ();
         vi.vreferenced <- true;
         vi
        )
       else
         (* Find the representative *)
         match findReplacement true vEq !currentFidx vi.vname with
         | None -> vi (* This is the representative *)
         | Some (vi', _) ->
             (* Reuse some previous one *)
             vi'.vreferenced <- true;
             (* Mark it as done already *)
             vi'.vaddrof <- vi.vaddrof || vi'.vaddrof;
             if isadef then
               vi'.vdecl <- vi.vdecl;
             vi'
     in
     try
       match g with
       | GVarDecl (vi, l) as g ->
           currentLoc := l;
           incr currentDeclIdx;
           let vi' = processVarinfo ~isadef:false vi l in
           if vi != vi' then (* Drop this declaration *) ()
           else if H.mem emittedVarDecls vi'.vname then
             (* No need to keep it *)
             ()
           else (
             H.add emittedVarDecls vi'.vname true;
             (* Remember that we emitted it *)
             mergePushGlobals (visitCilGlobal renameVisitor g))
       | GVar (vi, init, l) ->
           currentLoc := l;
           incr currentDeclIdx;
           let vi' = processVarinfo ~isadef:(init.init <> None) vi l in
           (* We must keep this definition even if we reuse this varinfo, because maybe the previous one was a declaration *)
           H.add emittedVarDecls vi.vname true;
           if mergeGlobals then
             match H.find_opt emittedVarDefn vi'.vname with
             | None ->
               (* no previous definition *)
               H.add emittedVarDefn vi'.vname (vi', init.init, l);
               mergePushGlobals (visitCilGlobal renameVisitor (GVar (vi', init, l)))
             | Some (prevVar, prevInitOpt, prevLoc) ->
               if equalInitOpts prevInitOpt init.init || init.init = None then
                 trace "mergeGlob" (P.dprintf "dropping global var %s at %a in favor of the one at %a\n" vi'.vname d_loc l d_loc prevLoc)
                 (* do not emit *)
               else if prevInitOpt = None then
                 (* We have an initializer, but the previous one didn't. We should really convert the previous global from GVar to GVarDecl, but that's not convenient to do here. *)
                 mergePushGlobals (visitCilGlobal renameVisitor (GVar (vi', init, l)))
               else
                 (* Both GVars have initializers. *)
                 E.s (error "global var %s at %a has different initializer than %a" vi'.vname d_loc l d_loc prevLoc)
           else
             (* Not merging globals, nothing to be done*)
             mergePushGlobals (visitCilGlobal renameVisitor (GVar (vi', init, l)))
       | GFun (fdec, l) as g ->
           currentLoc := l;
           incr currentDeclIdx;
           (* We apply the renaming *)
           fdec.svar <- processVarinfo ~isadef:true fdec.svar l;
           (* Get the original name. *)
           let origname = try H.find originalVarNames fdec.svar.vname with Not_found -> fdec.svar.vname in
           (* Go in there and rename everything as needed *)
           let fdec' = match visitCilGlobal renameVisitor g with
             | [ GFun (fdec', _) ] -> fdec'
             | _ -> E.s (unimp "renameVisitor for GFun returned something else")
           in
           let g' = GFun (fdec', l) in
           (* Now restore the parameter names *)
           let _, args, _, _ = splitFunctionTypeVI fdec'.svar in
           (match H.find_opt formalNames (!currentFidx, origname) with
            | Some oldnames ->
               let argl = argsToList args in
               if List.length oldnames <> List.length argl then E.s (unimp "After merging the function has more arguments");
               List.iter2 (fun oldn a -> if oldn <> "" then a.vname <- oldn) oldnames fdec.sformals;
               (* Reflect them in the type *)
               setFormals fdec fdec.sformals
            | None -> ignore (warnOpt "Cannot find %s in formalNames" origname)
           );
           (* See if we can remove this inline function *)
           if fdec'.svar.vinline && !merge_inlines then (
             let printout = printInlineForComparison fdec' g' in
             (* Make a node for this inline function using the original name. *)
             let inode = getNode vEq vSyn !currentFidx origname fdec'.svar (Some (l, !currentDeclIdx))
             in
             if debugInlines then (
               ignore (E.log "getNode %s(%d) with loc=%a. declidx=%d\n" inode.nname inode.nfidx d_nloc inode.nloc !currentDeclIdx);
               ignore (E.log "Looking for previous definition of inline %s(%d)\n" origname !currentFidx)
             );
             try
               let oldinode = H.find inlineBodies printout in
               if debugInlines then ignore (E.log "  Matches %s(%d)\n" oldinode.nname oldinode.nfidx);
               (* There is some other inline function with the same printout.
                  We should reuse this, but watch for the case when the inline
                  was already used. *)
               if H.mem varUsedAlready fdec'.svar.vname then
                 if mergeInlinesRepeat () then repeatPass2 := true
                 else (
                   ignore (warn "Inline function %s because it is used before it is defined" fdec'.svar.vname);
                   raise Not_found);
               let _ = union oldinode inode in
               (* Clean up the vreferenced bit in the new inline, so that we
                  can rename it. Reset the name to the original one so that
                  we can find the replacement name. *)
               fdec'.svar.vreferenced <- false;
               fdec'.svar.vname <- origname;
               ()
               (* Drop this definition *)
             with Not_found ->
               if debugInlines then ignore (E.log " Not found\n");
               H.add inlineBodies printout inode;
               mergePushGlobal g')
           else if mergeGlobals && not (fdec'.svar.vstorage = Static || fdec'.svar.vinline) then ( (* !merge_inlines is false here anyway *)
             (* either the function is not inline, or we're not attempting to  merge inlines *)
             (* sm: this is a non-inline, non-static function. I want to consider dropping it if a same-named function has already been put into the merged file *)
             let sum = functionChecksum fdec' in
             (*(trace "mergeGlob" (P.dprintf "I see extern function %s, sum is %d\n" fdec'.svar.vname curSum));*)
             match H.find_opt emittedFunDefn fdec'.svar.vname with
             | None ->
               (* there was no previous definition *)
               mergePushGlobal g';
               H.add emittedFunDefn fdec'.svar.vname (fdec', l, sum)
             | Some (prevFun, prevLoc, prevSum) ->
               (* previous was found *)
               if sum = prevSum then
                 trace "mergeGlob" (P.dprintf "dropping duplicate def'n of func %s at %a in favor of that at %a\n" fdec'.svar.vname d_loc l d_loc prevLoc)
               else
                 (* the checksums differ, so print a warning but keep the older one to avoid a link error later. *)
                 (* I think this is a reasonable approximation of what ld does. *)
                 ignore (warn
                      "def'n of func %s at %a (sum %d) conflicts with the one at %a (sum %d); keeping the one at %a."
                      fdec'.svar.vname d_loc l sum d_loc prevLoc prevSum d_loc
                      prevLoc)
            )
           else
             (* not attempting to merge global functions, or it was static or inline *)
             mergePushGlobal g'
       | GCompTag (ci, l) as g -> (
           currentLoc := l;
           incr currentDeclIdx;
           if ci.creferenced then ()
           else
             match findReplacement true sEq !currentFidx ci.cname with
             | None ->
                 (* A new one, we must rename it and keep the definition *)
                 (* Make sure this is root *)
                 (try
                    let nd = H.find sEq (!currentFidx, ci.cname) in
                    if nd.nrep != nd then
                      E.s
                        (bug
                           "Setting creferenced for struct %s(%d) which is not \
                            root!\n"
                           ci.cname !currentFidx)
                  with Not_found ->
                    E.s
                      (bug
                         "Setting creferenced for struct %s(%d) which is not in \
                          the sEq!\n"
                         ci.cname !currentFidx));
                 let newname, _ =
                   A.newAlphaName ~alphaTable:sAlpha ~undolist:None
                     ~lookupname:ci.cname ~data:!currentLoc
                 in
                 ci.cname <- newname;
                 ci.creferenced <- true;
                 ci.ckey <- H.hash (compFullName ci);
                 (* Now we should visit the fields as well *)
                 H.add emittedCompDecls ci.cname true;
                 (* Remember that we
                    emitted it *)
                 mergePushGlobals (visitCilGlobal renameVisitor g)
             | Some (oldci, oldfidx) ->
                 (* We are not the representative. Drop this declaration
                    because we'll not be using it. *)
                 ())
       | GEnumTag (ei, l) as g -> (
           currentLoc := l;
           incr currentDeclIdx;
           if ei.ereferenced then ()
           else
             match findReplacement true eEq !currentFidx ei.ename with
             | None ->
                 (* We must rename it *)
                 let newname, _ =
                   A.newAlphaName ~alphaTable:eAlpha ~undolist:None
                     ~lookupname:ei.ename ~data:!currentLoc
                 in
                 ei.ename <- newname;
                 ei.ereferenced <- true;
                 (* And we must rename the items to using the same name space
                    as the variables *)
                 ei.eitems <-
                   Util.list_map
                     (fun (n, attrs, i, loc) ->
                       let newname, _ =
                         A.newAlphaName ~alphaTable:vtAlpha ~undolist:None
                           ~lookupname:n ~data:!currentLoc
                       in
                       (newname, attrs, i, loc))
                     ei.eitems;
                 mergePushGlobals (visitCilGlobal renameVisitor g)
             | Some (ei', _) ->
                 (* Drop this since we are reusing it from
                    before *)
                 ())
       | GCompTagDecl (ci, l) ->
           currentLoc := l;
           (* This is here just to introduce an undefined
              structure. But maybe the structure was defined
              already. *)
           (* Do not increment currentDeclIdx because it is not incremented in
              pass 1*)
           if H.mem emittedCompDecls ci.cname then ()
             (* It was already declared *)
           else (
             H.add emittedCompDecls ci.cname true;
             (* Keep it as a declaration *)
             mergePushGlobal g)
       | GEnumTagDecl (ei, l) ->
           currentLoc := l;
           (* Do not increment currentDeclIdx because it is not incremented in
              pass 1*)
           (* Keep it as a declaration *)
           mergePushGlobal g
       | GType (ti, l) as g -> (
           currentLoc := l;
           incr currentDeclIdx;
           if ti.treferenced then ()
           else
             match findReplacement true tEq !currentFidx ti.tname with
             | None ->
                 (* We must rename it and keep it *)
                 let newname, _ =
                   A.newAlphaName ~alphaTable:vtAlpha ~undolist:None
                     ~lookupname:ti.tname ~data:!currentLoc
                 in
                 ti.tname <- newname;
                 ti.treferenced <- true;
                 mergePushGlobals (visitCilGlobal renameVisitor g)
             | Some (ti', _) ->
                 (* Drop this since we are reusing it from
                      before *)
                 ())
       | g -> mergePushGlobals (visitCilGlobal renameVisitor g)
     with e ->
       let globStr : string =
         P.sprint ~width:1000
           (P.dprintf "error when merging global %a: %s" d_global g
              (Printexc.to_string e))
       in
       ignore (E.log "%s" globStr);
       (*"error when merging global: %s" (Printexc.to_string e);*)
       mergePushGlobal
         (GText (P.sprint ~width:80 (P.dprintf "/* error at %t:" d_thisloc)));
       mergePushGlobal g;
       mergePushGlobal (GText "*************** end of error*/");
       raise e
   in
   (* Now do the real PASS 2 *)
   List.iter processOneGlobal f.globals;
   (* See if we must re-visit the globals in this file because an inline that
      is being removed was used before we saw the definition and we decided to
      remove it *)
   if mergeInlinesRepeat () && !repeatPass2 then (
     if debugMerge || !E.verboseFlag then
       ignore
         (E.log "Repeat final merging phase (%d): %s\n" !currentFidx f.fileName);
     (* We are going to rescan the globals we have added while processing this
        file. *)
     let theseGlobals : global list ref = ref [] in
     (* Scan a list of globals until we hit a given tail *)
     let rec scanUntil (tail : 'a list) (l : 'a list) =
       if tail == l then ()
       else
         match l with
         | [] -> E.s (bug "mergecil: scanUntil could not find the marker\n")
         | g :: rest ->
             theseGlobals := g :: !theseGlobals;
             scanUntil tail rest
     in
     (* Collect in theseGlobals all the globals from this file *)
     theseGlobals := [];
     scanUntil savedTheFile !theFile;
     (* Now reprocess them *)
     theFile := savedTheFile;
     List.iter
       (fun g -> theFile := visitCilGlobal renameInlinesVisitor g @ !theFile)
       !theseGlobals
     (* Now check if we have inlines that we could not remove
        H.iter (fun name _ ->
          if not (H.mem inlinesRemoved name) then
            ignore (warn "Could not remove inline %s. I have no idea why!"
                      name))
          inlinesToRemove *))

 let merge (files : file list) (newname : string) : file =
   init ();

   (* Make the first pass over the files *)
   currentFidx := 0;
   List.iter
     (fun f ->
       oneFilePass1 f;
       incr currentFidx)
     files;

   (* Now maybe try to force synonyms to be equal *)
   if mergeSynonyms then (
     doMergeSynonyms sSyn sEq matchCompInfo;
     doMergeSynonyms eSyn eEq matchEnumInfo;
     doMergeSynonyms tSyn tEq matchTypeInfo;
     if !merge_inlines then (
       (* Copy all the nodes from the iEq to vEq as well. This is needed
          because vEq will be used for variable renaming *)
       H.iter (fun k n -> H.add vEq k n) iEq;
       doMergeSynonyms iSyn iEq matchInlines));

   (* Now maybe dump the graph *)
   if debugMerge then (
     dumpGraph "type" tEq;
     dumpGraph "struct and union" sEq;
     dumpGraph "enum" eEq;
     dumpGraph "variable" vEq;
     if !merge_inlines then dumpGraph "inline" iEq);
   (* Make the second pass over the files. This is when we start rewriting the
      file *)
   currentFidx := 0;
   List.iter
     (fun f ->
       oneFilePass2 f;
       incr currentFidx)
     files;

   (* Now reverse the result and return the resulting file *)
   let rec revonto acc = function [] -> acc | x :: t -> revonto (x :: acc) t in
   let res =
     {
       fileName = newname;
       globals = revonto (revonto [] !theFile) !theFileTypes;
       globinit = None;
       globinitcalled = false;
     }
   in
   init ();
   (* Make the GC happy *)
   (* We have made many renaming changes and sometimes we have just guessed a
      name wrong. Make sure now that the local names are unique. *)
   uniqueVarNames res;
   res