1
(**************************************************************************)
3
(* Copyright (C) 2001-2003, *)
4
(* George C. Necula <necula@cs.berkeley.edu> *)
5
(* Scott McPeak <smcpeak@cs.berkeley.edu> *)
6
(* Wes Weimer <weimer@cs.berkeley.edu> *)
7
(* Ben Liblit <liblit@cs.berkeley.edu> *)
8
(* All rights reserved. *)
10
(* Redistribution and use in source and binary forms, with or without *)
11
(* modification, are permitted provided that the following conditions *)
14
(* 1. Redistributions of source code must retain the above copyright *)
15
(* notice, this list of conditions and the following disclaimer. *)
17
(* 2. Redistributions in binary form must reproduce the above copyright *)
18
(* notice, this list of conditions and the following disclaimer in the *)
19
(* documentation and/or other materials provided with the distribution. *)
21
(* 3. The names of the contributors may not be used to endorse or *)
22
(* promote products derived from this software without specific prior *)
23
(* written permission. *)
25
(* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS *)
26
(* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT *)
27
(* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS *)
28
(* FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE *)
29
(* COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, *)
30
(* INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, *)
31
(* BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; *)
32
(* LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER *)
33
(* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT *)
34
(* LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN *)
35
(* ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE *)
36
(* POSSIBILITY OF SUCH DAMAGE. *)
38
(* File modified by CEA (Commissariat � l'�nergie Atomique). *)
39
(**************************************************************************)
42
(* This module is responsible for merging multiple CIL source trees into
43
* a single, coherent CIL tree which contains the union of all the
44
* definitions in the source files. It effectively acts like a linker,
45
* but at the source code level instead of the object code level. *)
59
let debugMerge = false
60
let debugInlines = false
62
let ignore_merge_conflicts = ref false
64
(* Try to merge structure with the same name. However, do not complain if
65
* they are not the same *)
66
let mergeSynonyms = true
69
(** Whether to use path compression *)
70
let usePathCompression = false
72
(* Try to merge definitions of inline functions. They can appear in multiple
73
* files and we would like them all to be the same. This can slow down the
74
* merger an order of magnitude !!! *)
75
let mergeInlines = true
77
let mergeInlinesRepeat = mergeInlines && true
79
let mergeInlinesWithAlphaConvert = mergeInlines && true
81
(* when true, merge duplicate definitions of externally-visible functions;
82
* this uses a mechanism which is faster than the one for inline functions,
83
* but only probabilistically accurate *)
84
let mergeGlobals = true
87
(* Return true if 's' starts with the prefix 'p' *)
89
let lp = String.length p in
90
let ls = String.length s in
91
lp <= ls && String.sub s 0 lp = p
95
(* A name is identified by the index of the file in which it occurs (starting
96
* at 0 with the first file) and by the actual name. We'll keep name spaces
99
(* We define a data structure for the equivalence classes *)
101
{ nname: string; (* The actual name *)
102
nfidx: int; (* The file index *)
103
ndata: 'a; (* Data associated with the node *)
104
mutable nloc: (location * int) option;
105
(* location where defined and index within the file of the definition.
106
* If None then it means that this node actually DOES NOT appear in the
107
* given file. In rare occasions we need to talk in a given file about
108
* types that are not defined in that file. This happens with undefined
109
* structures but also due to cross-contamination of types in a few of
110
* the cases of combineType (see the definition of combineTypes). We
111
* try never to choose as representatives nodes without a definition.
112
* We also choose as representative the one that appears earliest *)
113
mutable nrep: 'a node; (* A pointer to another node in its class (one
114
* closer to the representative). The nrep node
115
* is always in an earlier file, except for the
116
* case where a name is undefined in one file
117
* and defined in a later file. If this pointer
118
* points to the node itself then this is the
120
mutable nmergedSyns: bool (* Whether we have merged the synonyms for
121
* the node of this name *)
124
let d_nloc fmt (lo: (location * int) option) =
126
None -> Format.fprintf fmt "None"
127
| Some (l, idx) -> Format.fprintf fmt "Some(%d at %a)" idx d_loc l
129
(* Make a node with a self loop. This is quite tricky. *)
130
let mkSelfNode (eq: (int * string, 'a node) H.t) (* The equivalence table *)
131
(syn: (string, 'a node) H.t) (* The synonyms table *)
132
(fidx: int) (name: string) (data: 'a)
133
(l: (location * int) option) =
134
let rec res = { nname = name; nfidx = fidx; ndata = data; nloc = l;
135
nrep = res; nmergedSyns = false; }
137
H.add eq (fidx, name) res; (* Add it to the proper table *)
138
if mergeSynonyms && not (prefix "__anon" name) then
142
let debugFind = false
144
(* Find the representative with or without path compression *)
145
let rec find (pathcomp: bool) (nd: 'a node) =
147
ignore (log " find %s(%d)\n" nd.nname nd.nfidx);
148
if nd.nrep == nd then begin
150
ignore (log " = %s(%d)\n" nd.nname nd.nfidx);
153
let res = find pathcomp nd.nrep in
154
if usePathCompression && pathcomp && nd.nrep != res then
155
nd.nrep <- res; (* Compress the paths *)
160
(* Union two nodes and return the new representative. We prefer as the
161
* representative a node defined earlier. We try not to use as
162
* representatives nodes that are not defined in their files. We return a
163
* function for undoing the union. Make sure that between the union and the
164
* undo you do not do path compression *)
165
let union (nd1: 'a node) (nd2: 'a node) : 'a node * (unit -> unit) =
166
(* Move to the representatives *)
167
let nd1 = find true nd1 in
168
let nd2 = find true nd2 in
169
if nd1 == nd2 then begin
170
(* It can happen that we are trying to union two nodes that are already
171
* equivalent. This is because between the time we check that two nodes
172
* are not already equivalent and the time we invoke the union operation
173
* we check type isomorphism which might change the equivalence classes *)
175
ignore (warn "unioning already equivalent nodes for %s(%d)"
176
nd1.nname nd1.nfidx);
180
let rep, norep = (* Choose the representative *)
181
if (nd1.nloc != None) = (nd2.nloc != None) then
182
(* They have the same defined status. Choose the earliest *)
183
if nd1.nfidx < nd2.nfidx then nd1, nd2
184
else if nd1.nfidx > nd2.nfidx then nd2, nd1
185
else (* In the same file. Choose the one with the earliest index *) begin
186
match nd1.nloc, nd2.nloc with
187
Some (_, didx1), Some (_, didx2) ->
188
if didx1 < didx2 then nd1, nd2 else
189
if didx1 > didx2 then nd2, nd1
192
"Merging two elements (%s and %s) in the same file (%d) with the same idx (%d) within the file"
193
nd1.nname nd2.nname nd1.nfidx didx1);
196
| _, _ -> (* both none. Does not matter which one we choose. Should
197
* not happen though. *)
198
(* sm: it does happen quite a bit when, e.g. merging STLport with
199
* some client source; I'm disabling the warning since it supposedly
200
* is harmless anyway, so is useless noise *)
201
(* sm: re-enabling on claim it now will probably not happen *)
202
ignore (warn "Merging two undefined elements in the same file: %s and %s\n" nd1.nname nd2.nname);
205
else (* One is defined, the other is not. Choose the defined one *)
206
if nd1.nloc != None then nd1, nd2 else nd2, nd1
208
let oldrep = norep.nrep in
210
rep, (fun () -> norep.nrep <- oldrep)
213
let union (nd1: 'a node) (nd2: 'a node) : 'a node * (unit -> unit) =
214
if nd1 == nd2 && nd1.nname = "!!!intEnumInfo!!!" then begin
215
ignore (warn "unioning two identical nodes for %s(%d)"
216
nd1.nname nd1.nfidx);
221
(* Find the representative for a node and compress the paths in the process *)
224
(eq: (int * string, 'a node) H.t)
226
(name: string) : ('a * int) option =
228
ignore (log "findReplacement for %s(%d)\n" name fidx);
230
let nd = H.find eq (fidx, name) in
231
if nd.nrep == nd then begin
233
ignore (log " is a representative\n");
234
None (* No replacement if this is the representative of its class *)
236
let rep = find pathcomp nd in
237
if rep != rep.nrep then
238
bug "find does not return the representative\n";
240
ignore (log " RES = %s(%d)\n" rep.nname rep.nfidx);
241
Some (rep.ndata, rep.nfidx)
242
with Not_found -> begin
244
ignore (log " not found in the map\n");
248
(* Make a node if one does not already exist. Otherwise return the
250
let getNode (eq: (int * string, 'a node) H.t)
251
(syn: (string, 'a node) H.t)
252
(fidx: int) (name: string) (data: 'a)
253
(l: (location * int) option) =
254
let debugGetNode = false in
256
ignore (log "getNode(%s(%d), %a)\n"
259
let res = H.find eq (fidx, name) in
261
(match res.nloc, l with
262
(* Maybe we have a better location now *)
263
None, Some _ -> res.nloc <- l
264
| Some (old_l, old_idx), Some (l, idx) ->
265
if old_idx != idx then
266
ignore (warn "Duplicate definition of node %s(%d) at indices %d(%a) and %d(%a)"
267
name fidx old_idx d_loc old_l idx d_loc l)
273
ignore (log " node already found\n");
274
find false res (* No path compression *)
275
with Not_found -> begin
276
let res = mkSelfNode eq syn fidx name data l in
278
ignore (log " made a new one\n");
285
let dumpGraph (what: string) (eq: (int * string, 'a node) H.t) : unit =
286
ignore (log "Equivalence graph for %s is:\n" what);
287
H.iter (fun (fidx, name) nd ->
288
ignore (log " %s(%d) %s-> "
289
name fidx (if nd.nloc = None then "(undef)" else ""));
290
if nd.nrep == nd then
293
ignore (log " %s(%d)\n" nd.nrep.nname nd.nrep.nfidx ))
299
(* For each name space we define a set of equivalence classes *)
300
let vEq: (int * string, varinfo node) H.t = H.create 111 (* Vars *)
301
let sEq: (int * string, compinfo node) H.t = H.create 111 (* Struct + union *)
302
let eEq: (int * string, enuminfo node) H.t = H.create 111 (* Enums *)
303
let tEq: (int * string, typeinfo node) H.t = H.create 111 (* Type names*)
304
let iEq: (int * string, varinfo node) H.t = H.create 111 (* Inlines *)
307
let pEq: (int * string, predicate_info node) H.t = H.create 111 (* Predicates *)
309
let lfEq: (int * string, logic_info node) H.t = H.create 111 (* Logic functions *)
310
let ltEq: (int * string, (string * logic_type_info) node) H.t = H.create 111 (* Logic types *)
311
let lcEq: (int * string, logic_ctor_info node) H.t = H.create 111 (* Logic constructors *)
313
let laEq: (int * string, (string * global_annotation list) node) H.t = H.create 111
315
let llEq: (int * string, (string * (bool * logic_label list * string list *
316
predicate named)) node) H.t = H.create 111
319
let translate table data get_info =
321
let result = ref None in
325
if get_info node.ndata == get_info data then
326
(result := Some node;
332
| None -> raise NotHere
335
if result == result.nrep then (* Name is already correct *) data
336
else result.nrep.ndata
338
let translate_vinfo info =
340
let new_vi = translate vEq info (fun v -> v.vid) in
341
(* Format.eprintf "TRANS %s(%d) to %s(%d)@\n"
342
info.vname info.vid new_vi.vname new_vi.vid;*)
345
let translate_typinfo info =
346
try translate tEq info (fun v -> v.tname) with NotHere -> info
349
(* Sometimes we want to merge synonyms. We keep some tables indexed by names.
350
* Each name is mapped to multiple exntries *)
351
let vSyn: (string, varinfo node) H.t = H.create 111 (* Not actually used *)
352
let iSyn: (string, varinfo node) H.t = H.create 111 (* Inlines *)
353
let sSyn: (string, compinfo node) H.t = H.create 111
354
let eSyn: (string, enuminfo node) H.t = H.create 111
355
let tSyn: (string, typeinfo node) H.t = H.create 111
357
let pSyn: (string, predicate_info node) H.t = H.create 111
359
let lfSyn: (string, logic_info node) H.t = H.create 111
360
let ltSyn: (string, (string * logic_type_info) node) H.t = H.create 111
361
let lcSyn: (string, logic_ctor_info node) H.t = H.create 111
362
let laSyn: (string, (string * global_annotation list) node) H.t = H.create 111
363
let llSyn: (string, (string * (bool * logic_label list * string list *
364
predicate named)) node) H.t = H.create 111
366
(** A global environment for variables. Put in here only the non-static
367
* variables, indexed by their name. *)
368
let vEnv : (string, varinfo node) H.t = H.create 111
370
(* A set of inline functions indexed by their printout ! *)
371
let inlineBodies : (string, varinfo node) H.t = H.create 111
373
(** A number of alpha conversion tables. We ought to keep one table for each
374
* name space. Unfortunately, because of the way the C lexer works, type
375
* names must be different from variable names!! We one alpha table both for
376
* variables and types. *)
377
let vtAlpha : (string, location A.alphaTableData ref) H.t
378
= H.create 57 (* Variables and
380
let sAlpha : (string, location A.alphaTableData ref) H.t
381
= H.create 57 (* Structures and
385
let eAlpha : (string, location A.alphaTableData ref) H.t
386
= H.create 57 (* Enumerations *)
389
(** Keep track, for all global function definitions, of the names of the formal
390
* arguments. They might change during merging of function types if the
391
* prototype occurs after the function definition and uses different names.
392
* We'll restore the names at the end *)
393
let formalNames: (int * string, string list) H.t = H.create 111
396
(* Accumulate here the globals in the merged file *)
397
let theFileTypes = ref []
400
(* we keep only one declaration for each function. The other ones are simply
401
discarded, but we need to merge their spec. This is done at the end
402
of the 2nd pass, to avoid going through theFile too many times.
404
let spec_to_merge = Hashtbl.create 59;;
406
(* renaming to be performed in spec found in declarations when there is
407
a definition for the given function. Similar to spec_to_merge table.
409
let formals_renaming = Hashtbl.create 59;;
411
(* add 'g' to the merged file *)
412
let mergePushGlobal (g: global) : unit =
413
pushGlobal g ~types:theFileTypes ~variables:theFile
415
let mergePushGlobals gl = List.iter mergePushGlobal gl
417
let add_to_merge_spec vi spec =
419
try Hashtbl.find spec_to_merge vi.vid
421
in Hashtbl.replace spec_to_merge vi.vid (spec::l)
423
let add_alpha_renaming old_vi old_args new_args =
424
Hashtbl.add formals_renaming old_vi.vid
425
(Cil.create_alpha_renaming old_args new_args)
427
let mergeSpec vi_ref vi_disc spec =
428
if Cil.is_empty_funspec spec then () (* no need keep empty specs *)
432
Cil.create_alpha_renaming
433
(Cil.getFormalsDecl vi_disc) (Cil.getFormalsDecl vi_ref)
436
Cil.visitCilFunspec alpha spec
437
with Not_found -> assert false
438
with Not_found -> spec
440
add_to_merge_spec vi_ref spec
446
(* The index of the current file being scanned *)
447
let currentFidx = ref 0
449
let currentDeclIdx = ref 0 (* The index of the definition in a file. This is
450
* maintained both in pass 1 and in pass 2. Make
451
* sure you count the same things in both passes. *)
452
(* Keep here the file names *)
453
let fileNames : (int, string) H.t = H.create 113
457
(* Remember the composite types that we have already declared *)
458
let emittedCompDecls: (string, bool) H.t = H.create 113
459
(* Remember the variables also *)
460
let emittedVarDecls: (string, bool) H.t = H.create 113
462
(* also keep track of externally-visible function definitions;
463
* name maps to declaration, location, and semantic checksum *)
464
let emittedFunDefn: (string, fundec * location * int) H.t = H.create 113
465
(* and same for variable definitions; name maps to GVar fields *)
466
let emittedVarDefn: (string, varinfo * init option * location) H.t = H.create 113
468
(** A mapping from the new names to the original names. Used in PASS2 when we
469
* rename variables. *)
470
let originalVarNames: (string, string) H.t = H.create 113
472
(* Initialize the module *)
473
let init ?(all=true) () =
480
if all then H.clear vEq;
497
H.clear inlineBodies;
503
H.clear emittedVarDecls;
504
H.clear emittedCompDecls;
506
H.clear emittedFunDefn;
507
H.clear emittedVarDefn;
509
H.clear originalVarNames;
510
if all then Logic_env.prepare_tables ()
512
let rec global_annot_pass1 l g = match g with
514
| Dpredicate_reads (pi,_,_,_)
515
| Dinductive_def(pi,_,_,_)
516
| Dpredicate_def (pi,_,_,_) ->
517
ignore (getNode pEq pSyn !currentFidx pi.p_name pi
518
(Some (l, !currentDeclIdx)))
520
| Dlogic_def (li, _, _, _, _)
521
| Dlogic_axiomatic(li, _, _ , _ , _)
522
| Dlogic_reads (li, _, _, _, _) ->
523
let mynode = getNode lfEq lfSyn !currentFidx li.l_name li None in
524
(* NB: in case of mix decl/def it is the decl location that is taken. *)
525
if mynode.nloc = None then
526
ignore (getNode lfEq lfSyn !currentFidx li.l_name li
527
(Some (l, !currentDeclIdx)))
529
| Daxiomatic(id,decls) ->
530
ignore (getNode laEq laSyn !currentFidx id (id,decls)
531
(Some (l,!currentDeclIdx)));
532
List.iter (global_annot_pass1 l) decls
534
(* FIXME: this is a copy of above, is it still correct for predicate ? *)
535
let mynode = getNode lfEq lfSyn !currentFidx li.l_name li None in
536
(* NB: in case of mix decl/def it is the decl location that is taken. *)
537
if mynode.nloc = None then
538
ignore (getNode lfEq lfSyn !currentFidx li.l_name li
539
(Some (l, !currentDeclIdx)))
542
ignore (getNode lfEq lfSyn !currentFidx pi.l_name pi
543
(Some (l, !currentDeclIdx)))
545
ignore (getNode lfEq lfSyn !currentFidx pi.l_name pi
546
(Some (l, !currentDeclIdx)))
548
let pi = { nb_params = List.length vars } in
549
ignore (getNode ltEq ltSyn !currentFidx n (n,pi)
550
(Some (l, !currentDeclIdx)))
552
| Dlemma (n,is_ax,labs,typs,st) ->
553
ignore (getNode llEq llSyn !currentFidx n (n,(is_ax,labs,typs,st))
554
(Some (l, !currentDeclIdx)))
558
(* Some enumerations have to be turned into an integer. We implement this by
559
* introducing a special enumeration type which we'll recognize later to be
562
{ ename = "!!!intEnumInfo!!!"; (* This is otherwise invalid *)
567
(* And add it to the equivalence graph *)
568
let intEnumInfoNode =
569
getNode eEq eSyn 0 intEnumInfo.ename intEnumInfo
570
(Some (Cilutil.locUnknown, 0))
572
(* Combine the types. Raises the Failure exception with an error message.
573
* isdef says whether the new type is for a definition *)
575
CombineFundef (* The new definition is for a function definition. The old
576
* is for a prototype *)
577
| CombineFunarg (* Comparing a function argument type with an old prototype
579
| CombineFunret (* Comparing the return of a function with that from an old
584
let rec combineTypes (what: combineWhat)
585
(oldfidx: int) (oldt: typ)
586
(fidx: int) (t: typ) : typ =
588
| TVoid olda, TVoid a -> TVoid (addAttributes olda a)
589
| TInt (oldik, olda), TInt (ik, a) ->
590
let combineIK oldk k =
591
if oldk == k then oldk else
592
(* GCC allows a function definition to have a more precise integer
593
* type than a prototype that says "int" *)
594
if not theMachine.msvcMode && oldk = IInt && bitsSizeOf t <= 32
595
&& (what = CombineFunarg || what = CombineFunret)
601
"(different integer types %a and %a)"
606
TInt (combineIK oldik ik, addAttributes olda a)
608
| TFloat (oldfk, olda), TFloat (fk, a) ->
609
let combineFK oldk k =
610
if oldk == k then oldk else
611
(* GCC allows a function definition to have a more precise integer
612
* type than a prototype that says "double" *)
613
if not theMachine.msvcMode && oldk = FDouble && k = FFloat
614
&& (what = CombineFunarg || what = CombineFunret)
618
raise (Failure "(different floating point types)")
620
TFloat (combineFK oldfk fk, addAttributes olda a)
622
| TEnum (oldei, olda), TEnum (ei, a) ->
623
(* Matching enumerations always succeeds. But sometimes it maps both
624
* enumerations to integers *)
625
matchEnumInfo oldfidx oldei fidx ei;
626
TEnum (oldei, addAttributes olda a)
629
(* Strange one. But seems to be handled by GCC *)
630
| TEnum (oldei, olda) , TInt(IInt, a) -> TEnum(oldei,
631
addAttributes olda a)
633
(* Strange one. But seems to be handled by GCC. Warning. Here we are
634
* leaking types from new to old *)
635
| TInt(IInt, olda), TEnum (ei, a) -> TEnum(ei, addAttributes olda a)
637
| TComp (oldci, olda) , TComp (ci, a) ->
638
matchCompInfo oldfidx oldci fidx ci;
639
(* If we get here we were successful *)
640
TComp (oldci, addAttributes olda a)
642
| TArray (oldbt, oldsz, olda), TArray (bt, sz, a) ->
643
let combbt = combineTypes CombineOther oldfidx oldbt fidx bt in
647
| Some _, None -> oldsz
648
| None, None -> oldsz
649
| Some oldsz', Some sz' ->
651
match constFold true oldsz', constFold true sz' with
652
Const(CInt64(oldi, _, _)), Const(CInt64(i, _, _)) -> oldi = i
655
if samesz then oldsz else
656
raise (Failure "(different array sizes)")
658
TArray (combbt, combinesz, addAttributes olda a)
660
| TPtr (oldbt, olda), TPtr (bt, a) ->
661
TPtr (combineTypes CombineOther oldfidx oldbt fidx bt,
662
addAttributes olda a)
664
(* WARNING: In this case we are leaking types from new to old !! *)
665
| TFun (_, _, _, [Attr("missingproto",_)]), TFun _ -> t
668
| TFun _, TFun (_, _, _, [Attr("missingproto",_)]) -> oldt
670
| TFun (oldrt, oldargs, oldva, olda), TFun (rt, args, va, a) ->
673
(if what = CombineFundef then CombineFunret else CombineOther)
674
oldfidx oldrt fidx rt
677
raise (Failure "(diferent vararg specifiers)");
678
(* If one does not have arguments, believe the one with the
681
if oldargs = None then args else
682
if args = None then oldargs else
683
let oldargslist = argsToList oldargs in
684
let argslist = argsToList args in
685
if List.length oldargslist <> List.length argslist then
686
raise (Failure "(different number of arguments)")
688
(* Go over the arguments and update the old ones with the
692
(fun (on, ot, oa) (an, at, aa) ->
693
let n = if an <> "" then an else on in
696
(if what = CombineFundef then CombineFunarg
700
let a = addAttributes oa aa in
702
oldargslist argslist)
705
TFun (newrt, newargs, oldva, addAttributes olda a)
707
| TBuiltin_va_list olda, TBuiltin_va_list a ->
708
TBuiltin_va_list (addAttributes olda a)
710
| TNamed (oldt, olda), TNamed (t, a) ->
711
matchTypeInfo oldfidx oldt fidx t;
712
(* If we get here we were able to match *)
713
TNamed(oldt, addAttributes olda a)
715
(* Unroll first the new type *)
716
| _, TNamed (t, a) ->
717
let res = combineTypes what oldfidx oldt fidx t.ttype in
718
typeAddAttributes a res
720
(* And unroll the old type as well if necessary *)
721
| TNamed (oldt, a), _ ->
722
let res = combineTypes what oldfidx oldt.ttype fidx t in
723
typeAddAttributes a res
726
(* raise (Failure "(different type constructors)") *)
729
"(different type constructors: %a vs. %a)"
735
(* Match two compinfos and throw a Failure if they do not match *)
736
and matchCompInfo (oldfidx: int) (oldci: compinfo)
737
(fidx: int) (ci: compinfo) : unit =
738
if oldci.cstruct <> ci.cstruct then
739
raise (Failure "(different struct/union types)");
740
(* See if we have a mapping already *)
741
(* Make the nodes if not already made. Actually return the
743
let oldcinode = getNode sEq sSyn oldfidx oldci.cname oldci None in
744
let cinode = getNode sEq sSyn fidx ci.cname ci None in
745
if oldcinode == cinode then (* We already know they are the same *)
748
(* Replace with the representative data *)
749
let oldci = oldcinode.ndata in
750
let oldfidx = oldcinode.nfidx in
751
let ci = cinode.ndata in
752
let fidx = cinode.nfidx in
754
let old_len = List.length oldci.cfields in
755
let len = List.length ci.cfields in
756
(* It is easy to catch here the case when the new structure is undefined
757
* and the old one was defined. We just reuse the old *)
758
(* More complicated is the case when the old one is not defined but the
759
* new one is. We still reuse the old one and we'll take care of defining
760
* it later with the new fields.
761
* GN: 7/10/04, I could not find when is "later", so I added it below *)
762
if len <> 0 && old_len <> 0 && old_len <> len then (
763
let curLoc = CurrentLoc.get () in (* d_global blows this away.. *)
764
(* (trace "merge" (P.dprintf "different # of fields\n%d: %a\n%d: %a\n"
765
old_len d_global (GCompTag(oldci,locUnknown))
766
len d_global (GCompTag(ci,locUnknown))
768
CurrentLoc.set curLoc;
769
let msg = Printf.sprintf
770
"(different number of fields in %s and %s: %d != %d.)"
771
oldci.cname ci.cname old_len len in
774
(* We check that they are defined in the same way. While doing this there
775
* might be recursion and we have to watch for going into an infinite
776
* loop. So we add the assumption that they are equal *)
777
let newrep, undo = union oldcinode cinode in
778
(* We check the fields but watch for Failure. We only do the check when
779
* the lengths are the same. Due to the code above this the other
780
* possibility is that one of the length is 0, in which case we reuse the
782
(* But what if the old one is the empty one ? *)
783
if old_len = len then begin
787
if oldf.fbitfield <> f.fbitfield then
788
raise (Failure "(different bitfield info)");
789
if oldf.fattr <> f.fattr then
790
raise (Failure "(different field attributes)");
791
(* Make sure the types are compatible *)
793
combineTypes CombineOther oldfidx oldf.ftype fidx f.ftype
795
(* Change the type in the representative *)
796
oldf.ftype <- newtype;
798
oldci.cfields ci.cfields
799
with Failure reason -> begin
800
(* Our assumption was wrong. Forget the isomorphism *)
804
"\n\tFailed assumption that %s and %s are isomorphic %s@?%a@?%a"
805
(compFullName oldci) (compFullName ci) reason
806
dn_global (GCompTag(oldci,Cilutil.locUnknown))
807
dn_global (GCompTag(ci,Cilutil.locUnknown))
812
(* We will reuse the old one. One of them is empty. If the old one is
813
* empty, copy over the fields from the new one. Won't this result in
814
* all sorts of undefined types??? *)
816
oldci.cfields <- ci.cfields;
818
(* We get here when we succeeded checking that they are equal, or one of
820
newrep.ndata.cattr <- addAttributes oldci.cattr ci.cattr;
824
(* Match two enuminfos and throw a Failure if they do not match *)
825
and matchEnumInfo (oldfidx: int) (oldei: enuminfo)
826
(fidx: int) (ei: enuminfo) : unit =
827
(* Find the node for this enum, no path compression. *)
828
let oldeinode = getNode eEq eSyn oldfidx oldei.ename oldei None in
829
let einode = getNode eEq eSyn fidx ei.ename ei None in
830
if oldeinode == einode then (* We already know they are the same *)
833
(* Replace with the representative data *)
834
let oldei = oldeinode.ndata in
835
let ei = einode.ndata in
836
(* Try to match them. But if you cannot just make them both integers *)
838
(* We do not have a mapping. They better be defined in the same way *)
839
if List.length oldei.eitems <> List.length ei.eitems then
840
raise (Failure "(different number of enumeration elements)");
841
(* We check that they are defined in the same way. This is a fairly
842
* conservative check. *)
844
(fun old_item item ->
845
if old_item.einame <> item.einame then
846
raise (Failure "(different names for enumeration items)");
848
match constFold true old_item.eival, constFold true item.eival with
849
Const(CInt64(oldi, _, _)), Const(CInt64(i, _, _)) -> oldi = i
853
raise (Failure "(different values for enumeration items)"))
854
oldei.eitems ei.eitems;
855
(* Set the representative *)
856
let newrep, _ = union oldeinode einode in
857
(* We get here if the enumerations match *)
858
newrep.ndata.eattr <- addAttributes oldei.eattr ei.eattr;
860
with Failure _msg -> begin
861
(* Get here if you cannot merge two enumeration nodes *)
862
if oldeinode != intEnumInfoNode then begin
863
let _ = union oldeinode intEnumInfoNode in ()
865
if einode != intEnumInfoNode then begin
866
let _ = union einode intEnumInfoNode in ()
872
(* Match two typeinfos and throw a Failure if they do not match *)
873
and matchTypeInfo (oldfidx: int) (oldti: typeinfo)
874
(fidx: int) (ti: typeinfo) : unit =
875
if oldti.tname = "" || ti.tname = "" then
876
(bug "matchTypeInfo for anonymous type\n");
877
(* Find the node for this enum, no path compression. *)
878
let oldtnode = getNode tEq tSyn oldfidx oldti.tname oldti None in
879
let tnode = getNode tEq tSyn fidx ti.tname ti None in
880
if oldtnode == tnode then (* We already know they are the same *)
883
(* Replace with the representative data *)
884
let oldti = oldtnode.ndata in
885
let oldfidx = oldtnode.nfidx in
886
let ti = tnode.ndata in
887
let fidx = tnode.nfidx in
888
(* Check that they are the same *)
890
ignore (combineTypes CombineOther oldfidx oldti.ttype fidx ti.ttype);
891
with Failure reason -> begin
895
"\n\tFailed assumption that %s and %s are isomorphic %s"
896
oldti.tname ti.tname reason) in
899
let _ = union oldtnode tnode in
903
let static_var_visitor = object
904
inherit Cil.nopCilVisitor
905
method vvrbl vi = if vi.vstorage = Static then raise Exit; DoChildren
909
let has_static_ref_predicate pred_info =
911
ignore (visitCilPredicateInfo static_var_visitor pred_info); false
915
let has_static_ref_logic_function lf_info =
917
ignore (visitCilLogicInfo static_var_visitor lf_info); false
921
let matchPredicateInfo oldfidx oldpi fidx pi =
922
let oldtnode = getNode pEq pSyn oldfidx oldpi.p_name oldpi None in
923
let tnode = getNode pEq pSyn fidx pi.p_name pi None in
924
if oldtnode == tnode then (* We already know they are the same *)
927
let oldpi = oldtnode.ndata in
928
let oldfidx = oldtnode.nfidx in
929
let pi = tnode.ndata in
930
let fidx = tnode.nfidx in
931
(* TODO: allow for multiple declarations and one definition.
932
Needs to allow for reads and body in the AST.
934
if Logic_const.is_same_predicate_info oldpi pi then begin
935
if has_static_ref_predicate oldpi then
937
"multiple inclusion of predicate %s referring to a static variable"
939
else if oldfidx < fidx then
940
tnode.nrep <- oldtnode.nrep (* NB: when we can mix decl and defs, the
941
chosen representative will not always
944
oldtnode.nrep <- tnode.nrep
946
error "invalid multiple predicate declarations %s" pi.p_name
950
let matchLogicInfo oldfidx oldpi fidx pi =
951
let oldtnode = getNode lfEq lfSyn oldfidx oldpi.l_name oldpi None in
952
let tnode = getNode lfEq lfSyn fidx pi.l_name pi None in
953
if oldtnode == tnode then (* We already know they are the same *)
956
let oldpi = oldtnode.ndata in
957
let oldfidx = oldtnode.nfidx in
958
let pi = tnode.ndata in
959
let fidx = tnode.nfidx in
960
if Logic_const.is_same_logic_info oldpi pi then begin
961
if has_static_ref_logic_function oldpi then
963
"multiple inclusion of logic function %s referring to a static variable"
965
else if oldfidx < fidx then
966
tnode.nrep <- oldtnode.nrep
968
oldtnode.nrep <- tnode.nrep
971
match oldpi.l_definition, pi.l_definition with
972
| None, None | Some _, Some _ ->
973
error "invalid multiple logic function declarations %s" pi.l_name
975
Printf.eprintf "old is declared, new is defined\n";
976
Logic_const.merge_logic_reads tnode.nrep.ndata oldtnode.nrep.ndata;
977
oldtnode.nrep <- tnode.nrep;
979
Logic_const.merge_logic_reads oldtnode.nrep.ndata tnode.nrep.ndata;
980
tnode.nrep <- oldtnode.nrep;
982
error "invalid multiple logic function declarations %s" pi.l_name
985
let matchLogicType oldfidx (oldid, _ as oldnode) fidx (id, _ as node) =
986
let oldtnode = getNode ltEq ltSyn oldfidx oldid oldnode None in
987
let tnode = getNode ltEq ltSyn fidx oldid node None in
988
if oldtnode == tnode then (* We already know they are the same *)
991
let (_,oldty) = oldtnode.ndata in
992
let oldfidx = oldtnode.nfidx in
993
let (_,ty) = tnode.ndata in
994
let fidx = tnode.nfidx in
995
if oldty.nb_params = ty.nb_params then begin
996
if oldfidx < fidx then
997
tnode.nrep <- oldtnode.nrep
999
oldtnode.nrep <- tnode.nrep
1001
error "invalid multiple logic type declarations %s" id
1004
let matchLogicCtor oldfidx oldpi fidx pi =
1005
let oldtnode = getNode lcEq lcSyn oldfidx oldpi.ctor_name oldpi None in
1006
let tnode = getNode lcEq lcSyn fidx pi.ctor_name pi None in
1007
if oldtnode == tnode then (* We already know they are the same *)
1010
error "invalid multiple logic constructors declarations %s" pi.ctor_name
1013
let matchLogicAxiomatic oldfidx (oldid,_ as oldnode) fidx (id,_ as node) =
1014
let oldanode = getNode laEq laSyn oldfidx oldid oldnode None in
1015
let anode = getNode laEq laSyn fidx id node None in
1016
if oldanode == anode then
1019
let (_,oldax) = oldanode.ndata in
1020
let oldaidx = oldanode.nfidx in
1021
let (_,ax) = anode.ndata in
1022
let aidx = anode.nfidx in
1023
if Logic_const.is_same_axiomatic oldax ax then begin
1024
if oldaidx < aidx then
1025
anode.nrep <- oldanode.nrep
1027
oldanode.nrep <- anode.nrep
1029
error "invalid multiple axiomatic declarations %s" id
1032
let matchLogicLemma oldfidx (oldid, _ as oldnode) fidx (id, _ as node) =
1033
let oldlnode = getNode llEq llSyn oldfidx oldid oldnode None in
1034
let lnode = getNode llEq llSyn fidx id node None in
1035
if oldlnode == lnode then ()
1037
let (oldid,(oldax,oldlabs,oldtyps,oldst)) = oldlnode.ndata in
1038
let oldfidx = oldlnode.nfidx in
1039
let (id,(ax,labs,typs,st)) = lnode.ndata in
1040
let fidx = lnode.nfidx in
1041
if Logic_const.is_same_global_annotation
1042
(Dlemma (oldid,oldax,oldlabs,oldtyps,oldst))
1043
(Dlemma (id,ax,labs,typs,st))
1045
if oldfidx < fidx then
1046
lnode.nrep <- oldlnode.nrep
1048
oldlnode.nrep <- lnode.nrep
1050
error "invalid multiple lemmas or axioms declarations for %s" id
1053
(* Scan all files and do two things *)
1054
(* 1. Initialize the alpha renaming tables with the names of the globals so
1055
* that when we come in the second pass to generate new names, we do not run
1056
* into conflicts. *)
1057
(* 2. For all declarations of globals unify their types. In the process
1058
* construct a set of equivalence classes on type names, structure and
1059
* enumeration tags *)
1060
(* 3. We clean the referenced flags *)
1062
let rec oneFilePass1 (f:file) : unit =
1063
H.add fileNames !currentFidx f.fileName;
1064
if debugMerge || !E.verboseFlag then
1065
ignore (log "Pre-merging (%d) %s\n" !currentFidx f.fileName);
1066
currentDeclIdx := 0;
1067
if f.globinitcalled || f.globinit <> None then
1068
warn "Merging file %s has global initializer" f.fileName;
1070
(* We scan each file and we look at all global varinfo. We see if globals
1071
* with the same name have been encountered before and we merge those types
1073
let matchVarinfo (vi: varinfo) (l: location * int) =
1074
ignore (Alpha.registerAlphaName vtAlpha None vi.vname (CurrentLoc.get ()));
1075
(* Make a node for it and put it in vEq *)
1076
let vinode = mkSelfNode vEq vSyn !currentFidx vi.vname vi (Some l) in
1078
let oldvinode = find true (H.find vEnv vi.vname) in
1080
match oldvinode.nloc with
1081
None -> (bug "old variable is undefined")
1084
let oldvi = oldvinode.ndata in
1085
(* There is an old definition. We must combine the types. Do this first
1086
* because it might fail *)
1089
combineTypes CombineOther
1090
oldvinode.nfidx oldvi.vtype
1091
!currentFidx vi.vtype;
1092
with (Failure reason) -> begin
1094
let f = if !ignore_merge_conflicts then warn else error in
1095
ignore (f "Incompatible declaration for %s (from %s(%d)). Previous was at %a (from %s (%d)) %s "
1097
(H.find fileNames !currentFidx) !currentFidx
1099
(H.find fileNames oldvinode.nfidx) oldvinode.nfidx
1104
let newrep, _ = union oldvinode vinode in
1105
(* We do not want to turn non-"const" globals into "const" one. That
1106
* can happen if one file declares the variable a non-const while
1107
* others declare it as "const". *)
1108
if hasAttribute "const" (typeAttrs vi.vtype) !=
1109
hasAttribute "const" (typeAttrs oldvi.vtype) then begin
1110
newrep.ndata.vtype <- typeRemoveAttributes ["const"] newtype;
1112
newrep.ndata.vtype <- newtype;
1114
(* clean up the storage. *)
1116
if vi.vstorage = oldvi.vstorage || vi.vstorage = Extern then
1118
else if oldvi.vstorage = Extern then vi.vstorage
1119
(* Sometimes we turn the NoStorage specifier into Static for inline
1121
else if oldvi.vstorage = Static &&
1122
vi.vstorage = NoStorage then Static
1124
ignore (warn "Inconsistent storage specification for %s. Now is %a and previous was %a at %a"
1126
d_storage vi.vstorage d_storage oldvi.vstorage
1131
newrep.ndata.vstorage <- newstorage;
1132
newrep.ndata.vattr <- addAttributes oldvi.vattr vi.vattr
1133
with Not_found -> (* Not present in the previous files. Remember it for
1135
H.add vEnv vi.vname vinode
1139
| GVarDecl (_,vi, l) | GVar (vi, _, l) ->
1141
incr currentDeclIdx;
1142
vi.vreferenced <- false;
1143
if vi.vstorage <> Static then begin
1144
matchVarinfo vi (l, !currentDeclIdx);
1149
incr currentDeclIdx;
1150
(* Save the names of the formal arguments *)
1151
let _, args, _, _ = splitFunctionTypeVI fdec.svar in
1152
H.add formalNames (!currentFidx, fdec.svar.vname)
1153
(List.map (fun (n,_,_) -> n) (argsToList args));
1154
fdec.svar.vreferenced <- false;
1155
(* Force inline functions to be static. *)
1156
(* GN: This turns out to be wrong. inline functions are external,
1157
* unless specified to be static. *)
1159
if fdec.svar.vinline && fdec.svar.vstorage = NoStorage then
1160
fdec.svar.vstorage <- Static;
1162
if fdec.svar.vstorage <> Static then begin
1163
matchVarinfo fdec.svar (l, !currentDeclIdx)
1165
if fdec.svar.vinline && mergeInlines then
1166
(* Just create the nodes for inline functions *)
1167
ignore (getNode iEq iSyn !currentFidx
1168
fdec.svar.vname fdec.svar (Some (l, !currentDeclIdx)))
1170
(* Make nodes for the defined type and structure tags *)
1172
incr currentDeclIdx;
1173
t.treferenced <- false;
1174
if t.tname <> "" then (* The empty names are just for introducing
1175
* undefined comp tags *)
1176
ignore (getNode tEq tSyn !currentFidx t.tname t
1177
(Some (l, !currentDeclIdx)))
1178
else begin (* Go inside and clean the referenced flag for the
1182
ci.creferenced <- false;
1183
(* Create a node for it *)
1184
ignore (getNode sEq sSyn !currentFidx ci.cname ci None)
1187
ei.ereferenced <- false;
1188
ignore (getNode eEq eSyn !currentFidx ei.ename ei None);
1190
| _ -> (bug "Anonymous Gtype is not TComp")
1193
| GCompTag (ci, l) ->
1194
incr currentDeclIdx;
1195
ci.creferenced <- false;
1196
ignore (getNode sEq sSyn !currentFidx ci.cname ci
1197
(Some (l, !currentDeclIdx)))
1198
| GEnumTag (ei, l) ->
1199
incr currentDeclIdx;
1200
ei.ereferenced <- false;
1201
ignore (getNode eEq eSyn !currentFidx ei.ename ei
1202
(Some (l, !currentDeclIdx)))
1204
| GAnnot (gannot,l) ->
1206
incr currentDeclIdx;
1207
global_annot_pass1 l gannot
1212
(* Try to merge synonyms. Do not give an error if they fail to merge *)
1214
(syn : (string, 'a node) H.t)
1215
(_eq : (int * string, 'a node) H.t)
1216
(compare : int -> 'a -> int -> 'a -> unit) (* A comparison function that
1217
* throws Failure if no match *)
1219
H.iter (fun n node ->
1220
if not node.nmergedSyns then begin
1221
(* find all the nodes for the same name *)
1222
let all = H.find_all syn n in
1223
let rec tryone (classes: 'a node list) (* A number of representatives
1225
(nd: 'a node) : 'a node list (* Returns an expanded set
1227
nd.nmergedSyns <- true;
1228
(* Compare in turn with all the classes we have so far *)
1229
let rec compareWithClasses = function
1230
[] -> [nd](* No more classes. Add this as a new class *)
1233
compare c.nfidx c.ndata nd.nfidx nd.ndata;
1234
(* Success. Stop here the comparison *)
1236
with Failure _ -> (* Failed. Try next class *)
1237
c :: (compareWithClasses restc)
1239
compareWithClasses classes
1241
(* Start with an empty set of classes for this name *)
1242
let _ = List.fold_left tryone [] all in
1248
let matchInlines (oldfidx: int) (oldi: varinfo)
1249
(fidx: int) (i: varinfo) =
1250
let oldinode = getNode iEq iSyn oldfidx oldi.vname oldi None in
1251
let inode = getNode iEq iSyn fidx i.vname i None in
1252
if oldinode != inode then begin
1253
(* Replace with the representative data *)
1254
let oldi = oldinode.ndata in
1255
let oldfidx = oldinode.nfidx in
1256
let i = inode.ndata in
1257
let fidx = inode.nfidx in
1258
(* There is an old definition. We must combine the types. Do this first
1259
* because it might fail *)
1261
combineTypes CombineOther
1262
oldfidx oldi.vtype fidx i.vtype;
1263
(* We get here if we have success *)
1264
(* Combine the attributes as well *)
1265
oldi.vattr <- addAttributes oldi.vattr i.vattr
1266
(* Do not union them yet because we do not know that they are the same.
1267
* We have checked only the types so far *)
1270
(************************************************************
1275
************************************************************)
1278
(** Keep track of the functions we have used already in the file. We need
1279
* this to avoid removing an inline function that has been used already.
1280
* This can only occur if the inline function is defined after it is used
1281
* already; a bad style anyway *)
1282
let varUsedAlready: (string, unit) H.t = H.create 111
1284
(** A visitor that renames uses of variables and types *)
1285
class renameVisitorClass = object (self)
1286
inherit nopCilVisitor
1288
(* This is either a global variable which we took care of, or a local
1289
* variable. Must do its type and attributes. *)
1290
method vvdec (_vi: varinfo) = DoChildren
1292
(* This is a variable use. See if we must change it *)
1293
method vvrbl (vi: varinfo) : varinfo visitAction =
1294
if not vi.vglob then DoChildren else
1295
if vi.vreferenced then begin
1296
H.add varUsedAlready vi.vname ();
1299
match findReplacement true vEq !currentFidx vi.vname with
1301
| Some (vi', oldfidx) ->
1303
ignore (log "Renaming use of var %s(%d) to %s(%d)\n"
1305
!currentFidx vi'.vname oldfidx);
1306
vi'.vreferenced <- true;
1307
H.add varUsedAlready vi'.vname ();
1312
method vpredicate_info_use pi =
1313
match findReplacement true pEq !currentFidx pi.p_name with
1315
| Some(pi',oldfidx) ->
1317
ignore (log "Renaming use of predicate %s(%d) to %s(%d)\n"
1319
!currentFidx pi'.p_name oldfidx);
1322
method vpredicate_info_decl pi =
1323
match findReplacement true pEq !currentFidx pi.p_name with
1325
| Some(pi',oldfidx) ->
1327
ignore (log "Renaming use of predicate %s(%d) to %s(%d)\n"
1329
!currentFidx pi'.p_name oldfidx);
1333
method vlogic_info_use li =
1334
match findReplacement true lfEq !currentFidx li.l_name with
1335
None -> if debugMerge then
1336
ignore (log "Using logic function %s(%d)"
1340
| Some(li',oldfidx) ->
1342
ignore (log "Renaming use of logic function %s(%d) to %s(%d)\n"
1344
!currentFidx li'.l_name oldfidx);
1347
method vlogic_info_decl li =
1348
match findReplacement true lfEq !currentFidx li.l_name with
1351
ignore (log "Using logic function %s(%d)"
1355
| Some(li',oldfidx) ->
1357
ignore (log "Renaming use of logic function %s(%d) to %s(%d)\n"
1359
!currentFidx li'.l_name oldfidx);
1363
(* The use of a type. Change only those types whose underlying info
1365
method vtype (t: typ) =
1367
TComp (ci, a) when not ci.creferenced -> begin
1368
match findReplacement true sEq !currentFidx ci.cname with
1370
| Some (ci', oldfidx) ->
1372
ignore (log "Renaming use of %s(%d) to %s(%d)\n"
1373
ci.cname !currentFidx ci'.cname oldfidx);
1374
ChangeTo (TComp (ci', visitCilAttributes (self :> cilVisitor) a))
1376
| TEnum (ei, a) when not ei.ereferenced -> begin
1377
match findReplacement true eEq !currentFidx ei.ename with
1380
if ei' == intEnumInfo then
1381
(* This is actually our friend intEnumInfo *)
1382
ChangeTo (TInt(IInt, visitCilAttributes (self :> cilVisitor) a))
1384
ChangeTo (TEnum (ei', visitCilAttributes (self :> cilVisitor) a))
1387
| TNamed (ti, a) when not ti.treferenced -> begin
1388
match findReplacement true tEq !currentFidx ti.tname with
1391
ChangeTo (TNamed (ti', visitCilAttributes (self :> cilVisitor) a))
1396
(* The Field offset might need to be changed to use new compinfo *)
1397
method voffs = function
1398
Field (f, o) -> begin
1399
(* See if the compinfo was changed *)
1400
if f.fcomp.creferenced then
1403
match findReplacement true sEq !currentFidx f.fcomp.cname with
1404
None -> DoChildren (* We did not replace it *)
1405
| Some (ci', oldfidx) -> begin
1406
(* First, find out the index of the original field *)
1407
let rec indexOf (i: int) = function
1409
(bug "Cannot find field %s in %s(%d)\n"
1410
f.fname (compFullName f.fcomp) !currentFidx)
1411
| f' :: _ when f' == f -> i
1412
| _ :: rest -> indexOf (i + 1) rest
1414
let index = indexOf 0 f.fcomp.cfields in
1415
if List.length ci'.cfields <= index then
1416
(bug "Too few fields in replacement %s(%d) for %s(%d)\n"
1417
(compFullName ci') oldfidx
1418
(compFullName f.fcomp) !currentFidx);
1419
let f' = List.nth ci'.cfields index in
1420
ChangeDoChildrenPost (Field (f', o), fun x -> x)
1426
method vterm_offset = function
1427
TField (f, o) -> begin
1428
(* See if the compinfo was changed *)
1429
if f.fcomp.creferenced then
1432
match findReplacement true sEq !currentFidx f.fcomp.cname with
1433
None -> DoChildren (* We did not replace it *)
1434
| Some (ci', oldfidx) -> begin
1435
(* First, find out the index of the original field *)
1436
let rec indexOf (i: int) = function
1438
(bug "Cannot find field %s in %s(%d)\n"
1439
f.fname (compFullName f.fcomp) !currentFidx)
1440
| f' :: _ when f' == f -> i
1441
| _ :: rest -> indexOf (i + 1) rest
1443
let index = indexOf 0 f.fcomp.cfields in
1444
if List.length ci'.cfields <= index then
1445
(bug "Too few fields in replacement %s(%d) for %s(%d)\n"
1446
(compFullName ci') oldfidx
1447
(compFullName f.fcomp) !currentFidx);
1448
let f' = List.nth ci'.cfields index in
1449
ChangeDoChildrenPost (TField (f', o), fun x -> x)
1455
method vtsets_offset = function
1456
TSField (f, o) -> begin
1457
(* See if the compinfo was changed *)
1458
if f.fcomp.creferenced then
1461
match findReplacement true sEq !currentFidx f.fcomp.cname with
1462
None -> DoChildren (* We did not replace it *)
1463
| Some (ci', oldfidx) -> begin
1464
(* First, find out the index of the original field *)
1465
let rec indexOf (i: int) = function
1467
(bug "Cannot find field %s in %s(%d)\n"
1468
f.fname (compFullName f.fcomp) !currentFidx)
1469
| f' :: _ when f' == f -> i
1470
| _ :: rest -> indexOf (i + 1) rest
1472
let index = indexOf 0 f.fcomp.cfields in
1473
if List.length ci'.cfields <= index then
1474
(bug "Too few fields in replacement %s(%d) for %s(%d)\n"
1475
(compFullName ci') oldfidx
1476
(compFullName f.fcomp) !currentFidx);
1477
let f' = List.nth ci'.cfields index in
1478
ChangeDoChildrenPost (TSField (f', o), fun x -> x)
1484
method vinitoffs o =
1485
(self#voffs o) (* treat initializer offsets same as lvalue offsets *)
1489
let renameVisitor = new renameVisitorClass
1492
(** A visitor that renames uses of inline functions that were discovered in
1493
* pass 2 to be used before they are defined. This is like the renameVisitor
1494
* except it only looks at the variables (thus it is a bit more efficient)
1495
* and it also renames forward declarations of the inlines to be removed. *)
1497
class renameInlineVisitorClass = object
1498
inherit nopCilVisitor
1500
(* This is a variable use. See if we must change it *)
1501
method vvrbl (vi: varinfo) : varinfo visitAction =
1502
if not vi.vglob then DoChildren else
1503
if vi.vreferenced then begin (* Already renamed *)
1506
match findReplacement true vEq !currentFidx vi.vname with
1508
| Some (vi', oldfidx) ->
1510
ignore (log "Renaming var %s(%d) to %s(%d)\n"
1512
!currentFidx vi'.vname oldfidx);
1513
vi'.vreferenced <- true;
1517
(* And rename some declarations of inlines to remove. We cannot drop this
1518
* declaration (see small1/combineinline6) *)
1519
method vglob = function
1520
GVarDecl(spec,vi, l) when vi.vinline -> begin
1521
(* Get the original name *)
1523
try H.find originalVarNames vi.vname
1524
with Not_found -> vi.vname
1526
(* Now see if this must be replaced *)
1527
match findReplacement true vEq !currentFidx origname with
1530
(*TODO: visit the spec to change references to formals *)
1531
ChangeTo [GVarDecl (spec,vi', l)]
1536
let renameInlinesVisitor = new renameInlineVisitorClass
1538
let collect_type_vars l =
1539
let tvars = ref [] in
1541
inherit Cil.nopCilVisitor
1542
method vlogic_type t =
1544
Lvar v when not (List.mem v !tvars) -> tvars:=v::!tvars; DoChildren
1548
List.iter (fun x -> ignore(visitCilLogicType vis x.lv_type)) l;
1551
let rec logic_annot_pass2 ~in_axiomatic g a = match a with
1553
| GAnnot ((Dinductive_def(pi,_,_,_)|
1554
Dpredicate_reads(pi,_,_,_)|
1555
Dpredicate_def (pi,_,_,_)),_) ->
1557
match findReplacement true pEq !currentFidx pi.p_name with
1559
mergePushGlobals (visitCilGlobal renameVisitor g);
1560
Logic_env.add_predicate pi
1563
| GAnnot(Dlogic_def (li,_,_,_,_),_) ->
1565
match findReplacement true lfEq !currentFidx li.l_name with
1567
mergePushGlobals (visitCilGlobal renameVisitor g);
1568
(* The function may have been added in the global env by
1569
a preceding declaration. *)
1570
if not (Logic_env.is_logic_function li.l_name) then
1571
Logic_env.add_logic_function li
1574
| GAnnot(Dlogic_axiomatic(li,_,_,_,_),_) ->
1576
match findReplacement true lfEq !currentFidx li.l_name with
1578
mergePushGlobals (visitCilGlobal renameVisitor g);
1579
(* The function may have been added in the global env by
1580
a preceding declaration. *)
1581
if not (Logic_env.is_logic_function li.l_name) then
1582
Logic_env.add_logic_function li
1585
| GAnnot (Dlogic_reads(li,_,_,_,_),l) ->
1587
match findReplacement true lfEq !currentFidx li.l_name with
1588
| None when not (Logic_env.is_logic_function li.l_name) ->
1589
mergePushGlobals (visitCilGlobal renameVisitor g);
1590
Logic_env.add_logic_function li;
1591
| Some (li',_) when not (Logic_env.is_logic_function li'.l_name) ->
1592
(*FIXME: this should be in the logic_info record. *)
1593
let vars = collect_type_vars li'.l_profile in
1595
(visitCilGlobal renameVisitor
1598
(li',vars,li'.l_profile,li'.l_type,li'.l_reads),l)));
1599
Logic_env.add_logic_function li';
1604
| Dfun_or_pred li ->
1606
match findReplacement true lfEq !currentFidx li.l_name with
1608
if not in_axiomatic then
1609
mergePushGlobals (visitCilGlobal renameVisitor g);
1610
Logic_env.add_logic_function li;
1612
(* FIXME: should we perform same actions
1613
as the case Dlogic_reads above ? *)
1617
match findReplacement true ltEq !currentFidx n with
1619
if not in_axiomatic then
1620
mergePushGlobals (visitCilGlobal renameVisitor g);
1621
Logic_env.add_logic_type n (snd (H.find ltEq (!currentFidx,n)).ndata)
1624
| Dinvariant {l_name = n} ->
1626
match findReplacement true lfEq !currentFidx n with
1628
assert (not in_axiomatic);
1629
mergePushGlobals (visitCilGlobal renameVisitor g);
1630
Logic_env.add_logic_function (H.find lfEq (!currentFidx,n)).ndata
1635
match findReplacement true lfEq !currentFidx n.l_name with
1637
let g = visitCilGlobal renameVisitor g in
1638
if not in_axiomatic then
1640
Logic_env.add_logic_function (H.find lfEq (!currentFidx,n.l_name)).ndata
1643
| Dlemma (n,_,_,_,_) ->
1645
match findReplacement true llEq !currentFidx n with
1647
if not in_axiomatic then
1648
mergePushGlobals (visitCilGlobal renameVisitor g)
1651
| Daxiomatic(n,l) ->
1653
match findReplacement true laEq !currentFidx n with
1655
assert (not in_axiomatic);
1656
mergePushGlobals (visitCilGlobal renameVisitor g);
1657
List.iter (logic_annot_pass2 ~in_axiomatic:true g) l
1661
let global_annot_pass2 g a = logic_annot_pass2 ~in_axiomatic:false g a
1663
(* sm: First attempt at a semantic checksum for function bodies.
1664
* Ideally, two function's checksums would be equal only when their
1665
* bodies were provably equivalent; but I'm using a much simpler and
1666
* less accurate heuristic here. It should be good enough for the
1667
* purpose I have in mind, which is doing duplicate removal of
1668
* multiply-instantiated template functions. *)
1669
let functionChecksum (dec: fundec) : int =
1671
(* checksum the structure of the statements (only) *)
1672
let rec stmtListSum (lst : stmt list) : int =
1673
(List.fold_left (fun acc s -> acc + (stmtSum s)) 0 lst)
1674
and stmtSum (s: stmt) : int =
1675
(* strategy is to just throw a lot of prime numbers into the
1676
* computation in hopes of avoiding accidental collision.. *)
1678
| UnspecifiedSequence seq ->
1679
131*(stmtListSum (List.map (fun (x,_,_) -> x) seq)) + 127
1680
| Instr _ -> 13 + 67
1685
| If(_,b1,b2,_) -> 31 + 37*(stmtListSum b1.bstmts)
1686
+ 41*(stmtListSum b2.bstmts)
1687
| Switch(_,b,_,_) -> 43 + 47*(stmtListSum b.bstmts)
1688
(* don't look at stmt list b/c is not part of tree *)
1689
| Loop(_,b,_,_,_) -> 49 + 53*(stmtListSum b.bstmts)
1690
| Block(b) -> 59 + 61*(stmtListSum b.bstmts)
1691
| TryExcept (b, (_, _), h, _) ->
1692
67 + 83*(stmtListSum b.bstmts) + 97*(stmtListSum h.bstmts)
1693
| TryFinally (b, h, _) ->
1694
103 + 113*(stmtListSum b.bstmts) + 119*(stmtListSum h.bstmts)
1697
(* disabled 2nd and 3rd measure because they appear to get different
1698
* values, for the same code, depending on whether the code was just
1699
* parsed into CIL or had previously been parsed into CIL, printed
1700
* out, then re-parsed into CIL *)
1702
(List.length dec.sformals), (* # formals *)
1703
0 (*(List.length dec.slocals)*), (* # locals *)
1704
0 (*dec.smaxid*), (* estimate of internal statement count *)
1705
(List.length dec.sbody.bstmts), (* number of statements at outer level *)
1706
(stmtListSum dec.sbody.bstmts) in (* checksum of statement structure *)
1707
(*(trace "sm" (P.dprintf "sum: %s is %d %d %d %d %d\n"*)
1708
(* dec.svar.vname a b c d e));*)
1709
2*a + 3*b + 5*c + 7*d + 11*e
1713
(* sm: equality for initializers, etc.; this is like '=', except
1714
* when we reach shared pieces (like references into the type
1715
* structure), we use '==', to prevent circularity *)
1716
(* update: that's no good; I'm using this to find things which
1717
* are equal but from different CIL trees, so nothing will ever
1718
* be '=='.. as a hack I'll just change those places to 'true',
1719
* so these functions are not now checking proper equality..
1720
* places where equality is not complete are marked "INC" *)
1721
let rec equalInits (x: init) (y: init) : bool =
1724
| SingleInit(xe), SingleInit(ye) -> (equalExps xe ye)
1725
| CompoundInit(_xt, xoil), CompoundInit(_yt, yoil) ->
1726
(*(xt == yt) &&*) (* INC *) (* types need to be identically equal *)
1727
let rec equalLists xoil yoil : bool =
1728
match xoil,yoil with
1729
| ((xo,xi) :: xrest), ((yo,yi) :: yrest) ->
1730
(equalOffsets xo yo) &&
1731
(equalInits xi yi) &&
1732
(equalLists xrest yrest)
1736
(equalLists xoil yoil)
1740
and equalOffsets (x: offset) (y: offset) : bool =
1743
| NoOffset, NoOffset -> true
1744
| Field(xfi,xo), Field(yfi,yo) ->
1745
(xfi.fname = yfi.fname) && (* INC: same fieldinfo name.. *)
1746
(equalOffsets xo yo)
1747
| Index(xe,xo), Index(ye,yo) ->
1748
(equalExps xe ye) &&
1749
(equalOffsets xo yo)
1753
and equalExps (x: exp) (y: exp) : bool =
1756
| Const(xc), Const(yc) -> xc = yc || (* safe to use '=' on literals *)
1758
(* CIL changes (unsigned)0 into 0U during printing.. *)
1760
| CInt64(xv,_,_),CInt64(yv,_,_) ->
1761
(Int64.to_int xv) = 0 && (* ok if they're both 0 *)
1762
(Int64.to_int yv) = 0
1765
| Lval(xl), Lval(yl) -> (equalLvals xl yl)
1766
| SizeOf(_xt), SizeOf(_yt) -> true (*INC: xt == yt*) (* identical types *)
1767
| SizeOfE(xe), SizeOfE(ye) -> (equalExps xe ye)
1768
| AlignOf(_xt), AlignOf(_yt) -> true (*INC: xt == yt*)
1769
| AlignOfE(xe), AlignOfE(ye) -> (equalExps xe ye)
1770
| UnOp(xop,xe,_xt), UnOp(yop,ye,_yt) ->
1772
(equalExps xe ye) &&
1773
true (*INC: xt == yt*)
1774
| BinOp(xop,xe1,xe2,_xt), BinOp(yop,ye1,ye2,_yt) ->
1776
(equalExps xe1 ye1) &&
1777
(equalExps xe2 ye2) &&
1778
true (*INC: xt == yt*)
1779
| CastE(_xt,xe), CastE(_yt,ye) ->
1780
(*INC: xt == yt &&*)
1782
| AddrOf(xl), AddrOf(yl) -> (equalLvals xl yl)
1783
| StartOf(xl), StartOf(yl) -> (equalLvals xl yl)
1785
(* initializers that go through CIL multiple times sometimes lose casts they
1786
* had the first time; so allow a different of a cast *)
1787
| CastE(_xt,xe), ye ->
1789
| xe, CastE(_yt,ye) ->
1795
and equalLvals (x: lval) (y: lval) : bool =
1798
| (Var _xv,xo), (Var _yv,yo) ->
1799
(* I tried, I really did.. the problem is I see these names
1800
* before merging collapses them, so __T123 != __T456,
1802
(*(xv.vname = vy.vname) && (* INC: same varinfo names.. *)*)
1803
(equalOffsets xo yo)
1805
| (Mem(xe),xo), (Mem(ye),yo) ->
1806
(equalExps xe ye) &&
1807
(equalOffsets xo yo)
1811
let equalInitOpts (x: init option) (y: init option) : bool =
1815
| Some(xi), Some(yi) -> (equalInits xi yi)
1820
(* Now we go once more through the file and we rename the globals that we
1821
* keep. We also scan the entire body and we replace references to the
1822
* representative types or variables. We set the referenced flags once we
1823
* have replaced the names. *)
1824
let oneFilePass2 (f: file) =
1825
if debugMerge || !E.verboseFlag then
1826
ignore (log "Final merging phase (%d): %s\n"
1827
!currentFidx f.fileName);
1828
currentDeclIdx := 0; (* Even though we don't need it anymore *)
1829
H.clear varUsedAlready;
1830
H.clear originalVarNames;
1831
(* If we find inline functions that are used before being defined, and thus
1832
* before knowing that we can throw them away, then we mark this flag so
1833
* that we can make another pass over the file *)
1834
let repeatPass2 = ref false in
1835
(* Keep a pointer to the contents of the file so far *)
1836
let savedTheFile = !theFile in
1838
let processOneGlobal (g: global) : unit =
1839
(* Process a varinfo. Reuse an old one, or rename it if necessary *)
1840
let processVarinfo (vi: varinfo) (vloc: location) : varinfo =
1841
if vi.vreferenced then
1842
vi (* Already done *)
1844
(* Maybe it is static. Rename it then *)
1845
if vi.vstorage = Static then begin
1847
A.newAlphaName vtAlpha None vi.vname (CurrentLoc.get ())
1850
try ignore (Cil.getFormalsDecl vi); true
1851
with Not_found -> false
1853
(* Remember the original name *)
1854
H.add originalVarNames newName vi.vname;
1855
if debugMerge then ignore (log "renaming %s at %a to %s\n"
1859
vi.vname <- newName;
1860
vi.vreferenced <- true;
1862
if formals_decl then Cil.setFormalsDecl vi vi.vtype;
1865
(* Find the representative *)
1866
match findReplacement true vEq !currentFidx vi.vname with
1867
None -> vi (* This is the representative *)
1868
| Some (vi', _) -> (* Reuse some previous one *)
1869
vi'.vreferenced <- true; (* Mark it as done already *)
1870
vi'.vaddrof <- vi.vaddrof || vi'.vaddrof;
1877
| GVarDecl (spec,vi, l) as g ->
1879
incr currentDeclIdx;
1880
let vi' = processVarinfo vi l in
1881
if vi != vi' then begin
1882
(* Drop the decl, keep the spec *)
1883
mergeSpec vi' vi spec end
1884
else if H.mem emittedVarDecls vi'.vname then begin
1885
mergeSpec vi' vi spec
1887
H.add emittedVarDecls vi'.vname true; (* Remember that we emitted
1889
mergePushGlobals (visitCilGlobal renameVisitor g)
1892
| GVar (vi, init, l) ->
1894
incr currentDeclIdx;
1895
let vi' = processVarinfo vi l in
1896
(* We must keep this definition even if we reuse this varinfo,
1897
* because maybe the previous one was a declaration *)
1898
H.add emittedVarDecls vi.vname true; (* Remember that we emitted it*)
1900
let emitIt:bool = (not mergeGlobals) ||
1902
let _prevVar, prevInitOpt, prevLoc =
1903
(H.find emittedVarDefn vi'.vname) in
1904
(* previously defined; same initializer? *)
1905
if (equalInitOpts prevInitOpt init.init)
1906
|| (init.init = None) then (
1907
(* (trace "mergeGlob"
1908
(P.dprintf "dropping global var %s at %a in favor of the one at %a\n"
1909
vi'.vname d_loc l d_loc prevLoc));*)
1910
false (* do not emit *)
1912
else if prevInitOpt = None then (
1913
(* We have an initializer, but the previous one didn't.
1914
We should really convert the previous global from GVar
1915
to GVarDecl, but that's not convenient to do here. *)
1919
(* Both GVars have initializers. *)
1920
(error "global var %s at %a has different initializer than %a\n"
1922
d_loc l d_loc prevLoc);
1926
(* no previous definition *)
1927
(H.add emittedVarDefn vi'.vname (vi', init.init, l));
1933
mergePushGlobals (visitCilGlobal renameVisitor (GVar(vi', init, l)))
1935
| GFun (fdec, l) as g ->
1937
incr currentDeclIdx;
1938
(* We apply the renaming *)
1939
let vi = processVarinfo fdec.svar l in
1940
if fdec.svar != vi then begin
1942
add_alpha_renaming vi (Cil.getFormalsDecl vi) fdec.sformals;
1943
with Not_found -> ());
1946
(* Get the original name. *)
1948
try H.find originalVarNames fdec.svar.vname
1949
with Not_found -> fdec.svar.vname
1951
(* Go in there and rename everything as needed *)
1953
match visitCilGlobal renameVisitor g with
1954
[GFun(fdec', _)] -> fdec'
1955
| _ -> (bug "renameVisitor for GFun returned something else")
1957
let g' = GFun(fdec', l) in
1958
(* Now restore the parameter names *)
1959
let _, args, _, _ = splitFunctionTypeVI fdec'.svar in
1960
let oldnames, foundthem =
1961
try H.find formalNames (!currentFidx, origname), true
1962
with Not_found -> begin
1963
ignore (warnOpt "Cannot find %s in formalNames" origname);
1967
if foundthem then begin
1968
let argl = argsToList args in
1969
if List.length oldnames <> List.length argl then
1970
(unimp "After merging the function has more arguments");
1972
(fun oldn a -> if oldn <> "" then a.vname <- oldn)
1973
oldnames fdec.sformals;
1974
(* Reflect them in the type *)
1975
setFormals fdec fdec.sformals
1977
(** See if we can remove this inline function *)
1978
if fdec'.svar.vinline && mergeInlines then begin
1980
(* Temporarily turn of printing of lines *)
1981
let oldprintln = miscState.lineDirectiveStyle in
1982
miscState.lineDirectiveStyle <- None;
1983
(* Temporarily set the name to all functions in the same way *)
1984
let newname = fdec'.svar.vname in
1985
fdec'.svar.vname <- "@@alphaname@@";
1986
(* If we must do alpha conversion then temporarily set the
1987
* names of the local variables and formals in a standard way *)
1988
let nameId = ref 0 in
1989
let oldNames : string list ref = ref [] in
1990
let renameOne (v: varinfo) =
1991
oldNames := v.vname :: !oldNames;
1993
v.vname <- "___alpha" ^ string_of_int !nameId
1995
let undoRenameOne (v: varinfo) =
1996
match !oldNames with
2000
| _ -> (bug "undoRenameOne")
2002
(* Remember the original type *)
2003
let origType = fdec'.svar.vtype in
2004
if mergeInlinesWithAlphaConvert then begin
2005
(* Rename the formals *)
2006
List.iter renameOne fdec'.sformals;
2007
(* Reflect in the type *)
2008
setFormals fdec' fdec'.sformals;
2009
(* Now do the locals *)
2010
List.iter renameOne fdec'.slocals
2018
miscState.lineDirectiveStyle <- oldprintln;
2019
fdec'.svar.vname <- newname;
2020
if mergeInlinesWithAlphaConvert then begin
2021
(* Do the locals in reverse order *)
2022
List.iter undoRenameOne (List.rev fdec'.slocals);
2023
(* Do the formals in reverse order *)
2024
List.iter undoRenameOne (List.rev fdec'.sformals);
2025
(* Restore the type *)
2026
fdec'.svar.vtype <- origType;
2030
(* Make a node for this inline function using the original
2033
getNode vEq vSyn !currentFidx origname fdec'.svar
2034
(Some (l, !currentDeclIdx))
2036
if debugInlines then begin
2037
ignore (log "getNode %s(%d) with loc=%a. declidx=%d\n"
2038
inode.nname inode.nfidx
2042
"Looking for previous definition of inline %s(%d)\n"
2043
origname !currentFidx);
2046
let oldinode = H.find inlineBodies printout in
2047
if debugInlines then
2048
ignore (log " Matches %s(%d)\n"
2049
oldinode.nname oldinode.nfidx);
2050
(* There is some other inline function with the same printout.
2051
* We should reuse this, but watch for the case when the inline
2052
* was already used. *)
2053
if H.mem varUsedAlready fdec'.svar.vname then begin
2054
if mergeInlinesRepeat then begin
2057
ignore (warn "Inline function %s because it is used before it is defined" fdec'.svar.vname);
2061
let _ = union oldinode inode in
2062
(* Clean up the vreferenced bit in the new inline, so that we
2063
* can rename it. Reset the name to the original one so that
2064
* we can find the replacement name. *)
2065
fdec'.svar.vreferenced <- false;
2066
fdec'.svar.vname <- origname;
2067
() (* Drop this definition *)
2068
with Not_found -> begin
2069
if debugInlines then ignore (log " Not found\n");
2070
H.add inlineBodies printout inode;
2074
(* either the function is not inline, or we're not attempting to
2077
not fdec'.svar.vinline &&
2078
fdec'.svar.vstorage <> Static) then
2080
(* sm: this is a non-inline, non-static function. I want to
2081
* consider dropping it if a same-named function has already
2082
* been put into the merged file *)
2083
let curSum = (functionChecksum fdec') in
2084
(*(trace "mergeGlob" (P.dprintf "I see extern function %s, sum is %d\n"*)
2085
(* fdec'.svar.vname curSum));*)
2087
let _prevFun, prevLoc, prevSum =
2088
(H.find emittedFunDefn fdec'.svar.vname) in
2089
(* previous was found *)
2090
if (curSum = prevSum) then
2091
(*trace "mergeGlob"*)
2093
"dropping duplicate def'n of func %s at %a in favor of that at %a@\n"
2095
d_loc l d_loc prevLoc
2097
(* the checksums differ, so print a warning but keep the
2098
* older one to avoid a link error later. I think this is
2099
* a reasonable approximation of what ld does. *)
2100
warn "def'n of func %s at %a (sum %d) conflicts with the one at %a (sum %d); keeping the one at %a.\n"
2102
d_loc l curSum d_loc prevLoc
2103
prevSum d_loc prevLoc
2105
with Not_found -> begin
2106
(* there was no previous definition *)
2107
(mergePushGlobal g');
2108
(H.add emittedFunDefn fdec'.svar.vname (fdec', l, curSum))
2111
(* not attempting to merge global functions, or it was static
2117
| GCompTag (ci, l) as g -> begin
2119
incr currentDeclIdx;
2120
if ci.creferenced then
2123
match findReplacement true sEq !currentFidx ci.cname with
2125
(* A new one, we must rename it and keep the definition *)
2126
(* Make sure this is root *)
2128
let nd = H.find sEq (!currentFidx, ci.cname) in
2129
if nd.nrep != nd then
2130
(bug "Setting creferenced for struct %s(%d) which is not root!\n"
2131
ci.cname !currentFidx);
2132
with Not_found -> begin
2133
(bug "Setting creferenced for struct %s(%d) which is not in the sEq!\n"
2134
ci.cname !currentFidx);
2137
A.newAlphaName sAlpha None ci.cname (CurrentLoc.get ()) in
2138
ci.cname <- newname;
2139
ci.creferenced <- true;
2140
ci.ckey <- H.hash (compFullName ci);
2141
(* Now we should visit the fields as well *)
2142
H.add emittedCompDecls ci.cname true; (* Remember that we
2144
mergePushGlobals (visitCilGlobal renameVisitor g)
2145
| Some (_oldci, _oldfidx) -> begin
2146
(* We are not the representative. Drop this declaration
2147
* because we'll not be using it. *)
2152
| GEnumTag (ei, l) as g -> begin
2154
incr currentDeclIdx;
2155
if ei.ereferenced then
2158
match findReplacement true eEq !currentFidx ei.ename with
2159
None -> (* We must rename it *)
2161
A.newAlphaName eAlpha None ei.ename (CurrentLoc.get ()) in
2162
ei.ename <- newname;
2163
ei.ereferenced <- true;
2164
(* And we must rename the items to using the same name space
2165
* as the variables *)
2168
let newname,_= A.newAlphaName vtAlpha None item.einame
2170
in item.einame <- newname)
2172
mergePushGlobals (visitCilGlobal renameVisitor g);
2173
| Some (_ei', _) -> (* Drop this since we are reusing it from
2178
| GCompTagDecl (ci, l) -> begin
2179
CurrentLoc.set l; (* This is here just to introduce an undefined
2180
* structure. But maybe the structure was defined
2182
(* Do not increment currentDeclIdx because it is not incremented in
2184
if H.mem emittedCompDecls ci.cname then
2185
() (* It was already declared *)
2187
H.add emittedCompDecls ci.cname true;
2188
(* Keep it as a declaration *)
2193
| GEnumTagDecl (_ei, l) ->
2195
(* Do not increment currentDeclIdx because it is not incremented in
2197
(* Keep it as a declaration *)
2201
| GType (ti, l) as g -> begin
2203
incr currentDeclIdx;
2204
if ti.treferenced then
2207
match findReplacement true tEq !currentFidx ti.tname with
2208
None -> (* We must rename it and keep it *)
2210
A.newAlphaName vtAlpha None ti.tname (CurrentLoc.get ()) in
2211
ti.tname <- newname;
2212
ti.treferenced <- true;
2213
mergePushGlobals (visitCilGlobal renameVisitor g);
2214
| Some (_ti', _) ->(* Drop this since we are reusing it from
2219
| GAnnot (a, l) as g ->
2221
incr currentDeclIdx;
2222
global_annot_pass2 g a
2223
| g -> mergePushGlobals (visitCilGlobal renameVisitor g)
2226
"error when merging global %a: %s"
2228
(Printexc.to_string e);
2229
(*"error when merging global: %s\n" (Printexc.to_string e);*)
2230
mergePushGlobal (GText (fprintf_to_string "/* error at %t:" d_thisloc));
2232
mergePushGlobal (GText ("*************** end of error*/"));
2236
(* Now do the real PASS 2 *)
2237
List.iter processOneGlobal f.globals;
2238
(* See if we must re-visit the globals in this file because an inline that
2239
* is being removed was used before we saw the definition and we decided to
2241
if mergeInlinesRepeat && !repeatPass2 then begin
2242
if debugMerge || !E.verboseFlag then
2243
ignore (log "Repeat final merging phase (%d): %s\n"
2244
!currentFidx f.fileName);
2245
(* We are going to rescan the globals we have added while processing this
2247
let theseGlobals : global list ref = ref [] in
2248
(* Scan a list of globals until we hit a given tail *)
2249
let rec scanUntil (tail: 'a list) (l: 'a list) =
2250
if tail == l then ()
2253
| [] -> (bug "mergecil: scanUntil could not find the marker\n")
2255
theseGlobals := g :: !theseGlobals;
2258
(* Collect in theseGlobals all the globals from this file *)
2260
scanUntil savedTheFile !theFile;
2261
(* Now reprocess them *)
2262
theFile := savedTheFile;
2264
theFile := (visitCilGlobal renameInlinesVisitor g) @ !theFile)
2266
(* Now check if we have inlines that we could not remove
2267
H.iter (fun name _ ->
2268
if not (H.mem inlinesRemoved name) then
2269
ignore (warn "Could not remove inline %s. I have no idea why!\n"
2275
let merge_specs orig to_merge =
2276
let initial = { orig with spec_requires = orig.spec_requires } in
2277
let merge_one_spec spec =
2278
if is_same_spec initial spec then ()
2279
else Logic_const.merge_funspec orig spec
2281
List.iter merge_one_spec to_merge
2283
let global_merge_spec g =
2288
Hashtbl.find spec_to_merge fdec.svar.vid
2290
merge_specs fdec.sspec specs
2291
with Not_found -> ())
2292
| GVarDecl(spec,v,_) ->
2295
let alpha = Hashtbl.find formals_renaming v.vid in
2296
ignore (visitCilFunspec alpha spec)
2297
with Not_found -> ()
2301
Hashtbl.find spec_to_merge v.vid
2303
merge_specs spec specs;
2305
with Not_found -> rename spec
2309
let merge (files: file list) (newname: string) : file =
2312
(* Make the first pass over the files *)
2314
List.iter (fun f -> oneFilePass1 f; incr currentFidx) files;
2316
(* Now maybe try to force synonyms to be equal *)
2317
if mergeSynonyms then begin
2318
doMergeSynonyms sSyn sEq matchCompInfo;
2319
doMergeSynonyms eSyn eEq matchEnumInfo;
2320
doMergeSynonyms tSyn tEq matchTypeInfo;
2323
doMergeSynonyms pSyn pEq matchPredicateInfo;
2325
doMergeSynonyms lfSyn lfEq matchLogicInfo;
2326
doMergeSynonyms ltSyn ltEq matchLogicType;
2327
doMergeSynonyms lcSyn lcEq matchLogicCtor;
2328
doMergeSynonyms laSyn laEq matchLogicAxiomatic;
2329
doMergeSynonyms llSyn llEq matchLogicLemma;
2331
if mergeInlines then begin
2332
(* Copy all the nodes from the iEq to vEq as well. This is needed
2333
* because vEq will be used for variable renaming *)
2334
H.iter (fun k n -> H.add vEq k n) iEq;
2335
doMergeSynonyms iSyn iEq matchInlines;
2339
(* Now maybe dump the graph *)
2340
if debugMerge then begin
2341
dumpGraph "type" tEq;
2342
dumpGraph "struct and union" sEq;
2343
dumpGraph "enum" eEq;
2344
dumpGraph "variable" vEq;
2345
if mergeInlines then dumpGraph "inline" iEq;
2347
(* Make the second pass over the files. This is when we start rewriting the
2350
List.iter (fun f -> oneFilePass2 f; incr currentFidx) files;
2352
(* Now reverse the result and return the resulting file *)
2353
let rec revonto acc = function
2356
revonto (x :: acc) t
2359
{ fileName = newname;
2360
globals = revonto (revonto [] !theFile) !theFileTypes;
2362
globinitcalled = false } in
2363
List.iter global_merge_spec res.globals;
2364
init ~all:false (); (* Make the GC happy BUT KEEP some tables *)
2365
(* We have made many renaming changes and sometimes we have just guessed a
2366
* name wrong. Make sure now that the local names are unique. *)
2368
if !Errormsg.hadErrors then begin
2369
Format.eprintf "Error during linking@.";
2370
{ fileName = newname;
2373
globinitcalled = false }
added
removed
cil/src/mergecil.ml
