CBMC: /home/runner/work/cbmc/cbmc/src/linking/linking.cpp Source File

CBMC
Loading...
Searching...
No Matches
linking.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Linking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "linking.h"
13#include "linking_class.h"
14
15#include <util/c_types.h>
16#include <util/find_symbols.h>
17#include <util/message.h>
18#include <util/pointer_offset_size.h>
19#include <util/simplify_expr.h>
20#include <util/symbol_table_base.h>
21
22#include <langapi/language_util.h>
23
24#include "linking_diagnostics.h"
25
26#include <deque>
27
29 const namespacet &ns,
30 const typet &type)
31{
32 if(type.id() == ID_c_enum_tag)
33 return ns.follow_tag(to_c_enum_tag_type(type));
34 else if(type.id()==ID_struct_tag)
35 return ns.follow_tag(to_struct_tag_type(type));
36 else if(type.id()==ID_union_tag)
37 return ns.follow_tag(to_union_tag_type(type));
38 else
39 return type;
40}
41
42irep_idt
44{
45 unsigned cnt=0;
46
47 while(true)
48 {
50 id2string(id)+"$link"+std::to_string(++cnt);
51
54 continue; // already in main symbol table
55
56 if(!renamed_ids.insert(new_identifier).second)
57 continue; // used this for renaming already
58
59 if(src_symbol_table.symbols.find(new_identifier)!=
60 src_symbol_table.symbols.end())
61 continue; // used by some earlier linking call already
62
63 return new_identifier;
64 }
65}
66
68 const symbolt &old_symbol,
69 const symbolt &new_symbol)
70{
71 // We first take care of file-local non-type symbols.
72 // These are static functions, or static variables
73 // inside static function bodies.
74 if(new_symbol.is_file_local)
76 else if(old_symbol.is_file_local)
78 else
80}
81
83 symbolt &old_symbol,
84 symbolt &new_symbol)
85{
87
88 // Both are functions.
89 if(old_symbol.type != new_symbol.type)
90 {
91 const code_typet &old_t=to_code_type(old_symbol.type);
92 const code_typet &new_t=to_code_type(new_symbol.type);
93
94 if(old_symbol.type.get_bool(ID_C_incomplete) && old_symbol.value.is_nil())
95 {
96 diag.warning(old_symbol, new_symbol, "implicit function declaration");
97
98 old_symbol.type=new_symbol.type;
99 old_symbol.location=new_symbol.location;
100 old_symbol.is_weak=new_symbol.is_weak;
101 }
102 else if(
103 new_symbol.type.get_bool(ID_C_incomplete) && new_symbol.value.is_nil())
104 {
105 diag.warning(
106 old_symbol,
107 new_symbol,
108 "ignoring conflicting implicit function declaration");
109 }
110 // handle (incomplete) function prototypes
111 else if(((old_t.parameters().empty() && old_t.has_ellipsis() &&
112 old_symbol.value.is_nil()) ||
113 (new_t.parameters().empty() && new_t.has_ellipsis() &&
114 new_symbol.value.is_nil())))
115 {
116 if(old_t.parameters().empty() &&
117 old_t.has_ellipsis() &&
118 old_symbol.value.is_nil())
119 {
120 old_symbol.type=new_symbol.type;
121 old_symbol.location=new_symbol.location;
122 old_symbol.is_weak=new_symbol.is_weak;
123 }
124 }
125 // replace weak symbols
126 else if(old_symbol.is_weak)
127 {
128 if(new_symbol.value.is_nil())
129 {
130 diag.warning(
131 old_symbol,
132 new_symbol,
133 "function declaration conflicts with with weak definition");
134 }
135 else
136 old_symbol.value.make_nil();
137 }
138 else if(new_symbol.is_weak)
139 {
140 if(new_symbol.value.is_nil() ||
141 old_symbol.value.is_not_nil())
142 {
143 new_symbol.value.make_nil();
144
145 diag.warning(
146 old_symbol,
147 new_symbol,
148 "ignoring conflicting weak function declaration");
149 }
150 }
151 // aliasing may alter the type
152 else if((new_symbol.is_macro &&
153 new_symbol.value.is_not_nil() &&
154 old_symbol.value.is_nil()) ||
155 (old_symbol.is_macro &&
156 old_symbol.value.is_not_nil() &&
157 new_symbol.value.is_nil()))
158 {
159 diag.warning(
160 old_symbol,
161 new_symbol,
162 "ignoring conflicting function alias declaration");
163 }
164 // conflicting declarations without a definition, matching return
165 // types
166 else if(old_symbol.value.is_nil() && new_symbol.value.is_nil())
167 {
168 diag.warning(
169 old_symbol, new_symbol, "ignoring conflicting function declarations");
170
171 if(old_t.parameters().size()<new_t.parameters().size())
172 {
173 old_symbol.type=new_symbol.type;
174 old_symbol.location=new_symbol.location;
175 old_symbol.is_weak=new_symbol.is_weak;
176 }
177 }
178 // mismatch on number of parameters is definitively an error
179 else if((old_t.parameters().size()<new_t.parameters().size() &&
180 new_symbol.value.is_not_nil() &&
181 !old_t.has_ellipsis()) ||
182 (old_t.parameters().size()>new_t.parameters().size() &&
183 old_symbol.value.is_not_nil() &&
184 !new_t.has_ellipsis()))
185 {
186 diag.error(
187 old_symbol,
188 new_symbol,
189 "conflicting parameter counts of function declarations");
190
191 // error logged, continue typechecking other symbols
192 return;
193 }
194 else
195 {
196 // the number of parameters matches, collect all the conflicts
197 // and see whether they can be cured
198 std::string warn_msg;
199 bool replace=false;
200 typedef std::deque<std::pair<typet, typet> > conflictst;
202
203 if(old_t.return_type() != new_t.return_type())
204 {
205 diag.warning(old_symbol, new_symbol, "conflicting return types");
206
207 conflicts.emplace_back(old_t.return_type(), new_t.return_type());
208 }
209
210 code_typet::parameterst::const_iterator
211 n_it=new_t.parameters().begin(),
212 o_it=old_t.parameters().begin();
213 for( ;
214 o_it!=old_t.parameters().end() &&
215 n_it!=new_t.parameters().end();
216 ++o_it, ++n_it)
217 {
218 if(o_it->type() != n_it->type())
219 conflicts.push_back(
220 std::make_pair(o_it->type(), n_it->type()));
221 }
222 if(o_it!=old_t.parameters().end())
223 {
224 if(!new_t.has_ellipsis() && old_symbol.value.is_not_nil())
225 {
226 diag.error(
227 old_symbol,
228 new_symbol,
229 "conflicting parameter counts of function declarations");
230
231 // error logged, continue typechecking other symbols
232 return;
233 }
234
235 replace=new_symbol.value.is_not_nil();
236 }
237 else if(n_it!=new_t.parameters().end())
238 {
239 if(!old_t.has_ellipsis() && new_symbol.value.is_not_nil())
240 {
241 diag.error(
242 old_symbol,
243 new_symbol,
244 "conflicting parameter counts of function declarations");
245
246 // error logged, continue typechecking other symbols
247 return;
248 }
249
250 replace=new_symbol.value.is_not_nil();
251 }
252
253 while(!conflicts.empty())
254 {
255 const typet &t1=follow_tags_symbols(ns, conflicts.front().first);
256 const typet &t2=follow_tags_symbols(ns, conflicts.front().second);
257
258 // different pointer arguments without implementation may work
259 if(
260 (t1.id() == ID_pointer || t2.id() == ID_pointer) &&
262 old_symbol.value.is_nil() && new_symbol.value.is_nil())
263 {
264 if(warn_msg.empty())
265 warn_msg="different pointer types in extern function";
266 }
267 // different pointer arguments with implementation - the
268 // implementation is always right, even though such code may
269 // be severely broken
270 else if((t1.id()==ID_pointer || t2.id()==ID_pointer) &&
272 old_symbol.value.is_nil()!=new_symbol.value.is_nil())
273 {
274 if(warn_msg.empty())
275 {
276 warn_msg="pointer parameter types differ between "
277 "declaration and definition";
278 }
279
280 replace=new_symbol.value.is_not_nil();
281 }
282 // transparent union with (or entirely without) implementation is
283 // ok -- this primarily helps all those people that don't get
284 // _GNU_SOURCE consistent
285 else if((t1.id()==ID_union &&
286 (t1.get_bool(ID_C_transparent_union) ||
287 conflicts.front().first.get_bool(ID_C_transparent_union))) ||
288 (t2.id()==ID_union &&
289 (t2.get_bool(ID_C_transparent_union) ||
290 conflicts.front().second.get_bool(ID_C_transparent_union))))
291 {
292 const bool use_old=
293 t1.id()==ID_union &&
294 (t1.get_bool(ID_C_transparent_union) ||
295 conflicts.front().first.get_bool(ID_C_transparent_union)) &&
296 new_symbol.value.is_nil();
297
298 const union_typet &union_type=
300 const typet &src_type=t1.id()==ID_union?t2:t1;
301
302 bool found=false;
303 for(const auto &c : union_type.components())
304 if(c.type() == src_type)
305 {
306 found=true;
307 if(warn_msg.empty())
308 warn_msg="conflict on transparent union parameter in function";
310 }
311
312 if(!found)
313 break;
314 }
315 // different non-pointer arguments with implementation - the
316 // implementation is always right, even though such code may
317 // be severely broken
319 old_symbol.value.is_nil()!=new_symbol.value.is_nil())
320 {
321 if(warn_msg.empty())
322 warn_msg="non-pointer parameter types differ between "
323 "declaration and definition";
324 replace=new_symbol.value.is_not_nil();
325 }
326 else
327 break;
328
329 conflicts.pop_front();
330 }
331
332 if(!conflicts.empty())
333 {
334 diag.detailed_conflict_report(
335 old_symbol,
336 new_symbol,
337 conflicts.front().first,
338 conflicts.front().second);
339
340 diag.error(old_symbol, new_symbol, "conflicting function declarations");
341
342 // error logged, continue typechecking other symbols
343 return;
344 }
345 else
346 {
347 // warns about the first inconsistency
348 diag.warning(old_symbol, new_symbol, warn_msg);
349
350 if(replace)
351 {
352 old_symbol.type=new_symbol.type;
353 old_symbol.location=new_symbol.location;
354 }
355 }
356 }
357
359 old_symbol.symbol_expr(), old_symbol.symbol_expr());
360 }
361
362 if(!new_symbol.value.is_nil())
363 {
364 if(old_symbol.value.is_nil())
365 {
366 // the one with body wins!
367 rename_new_symbol(new_symbol.value);
368 rename_new_symbol(new_symbol.type);
369 old_symbol.value=new_symbol.value;
370 old_symbol.type=new_symbol.type; // for parameter identifiers
371 old_symbol.is_weak=new_symbol.is_weak;
372 old_symbol.location=new_symbol.location;
373 old_symbol.is_macro=new_symbol.is_macro;
374
375 // replace any previous update
376 object_type_updates.erase(old_symbol.name);
378 old_symbol.symbol_expr(), old_symbol.symbol_expr());
379 }
380 else if(to_code_type(old_symbol.type).get_inlined())
381 {
382 // ok, silently ignore
383 }
384 else if(old_symbol.type == new_symbol.type)
385 {
386 // keep the one in old_symbol -- libraries come last!
388 log.debug().source_location = new_symbol.location;
389 log.debug() << "function '" << old_symbol.name << "' in module '"
390 << new_symbol.module
391 << "' is shadowed by a definition in module '"
392 << old_symbol.module << "'" << messaget::eom;
393 }
394 else
395 {
396 diag.error(old_symbol, new_symbol, "duplicate definition of function");
397 }
398 }
399}
400
402 const typet &t1,
403 const typet &t2,
405{
406 if(t1 == t2)
407 return false;
408
409 if(
410 t1.id() == ID_struct_tag || t1.id() == ID_union_tag ||
411 t1.id() == ID_c_enum_tag)
412 {
413 const irep_idt &identifier = to_tag_type(t1).get_identifier();
414
415 if(info.o_symbols.insert(identifier).second)
416 {
417 bool result=
419 info.o_symbols.erase(identifier);
420
421 return result;
422 }
423
424 return false;
425 }
426 else if(
427 t2.id() == ID_struct_tag || t2.id() == ID_union_tag ||
428 t2.id() == ID_c_enum_tag)
429 {
430 const irep_idt &identifier = to_tag_type(t2).get_identifier();
431
432 if(info.n_symbols.insert(identifier).second)
433 {
434 bool result=
436 info.n_symbols.erase(identifier);
437
438 return result;
439 }
440
441 return false;
442 }
443 else if(t1.id()==ID_pointer && t2.id()==ID_array)
444 {
445 info.set_to_new=true; // store new type
446
447 return false;
448 }
449 else if(t1.id()==ID_array && t2.id()==ID_pointer)
450 {
451 // ignore
452 return false;
453 }
454 else if(
455 t1.id() == ID_struct && to_struct_type(t1).is_incomplete() &&
456 t2.id() == ID_struct && !to_struct_type(t2).is_incomplete())
457 {
458 info.set_to_new=true; // store new type
459
460 return false;
461 }
462 else if(
463 t1.id() == ID_union && to_union_type(t1).is_incomplete() &&
464 t2.id() == ID_union && !to_union_type(t2).is_incomplete())
465 {
466 info.set_to_new = true; // store new type
467
468 return false;
469 }
470 else if(
471 t1.id() == ID_struct && !to_struct_type(t1).is_incomplete() &&
472 t2.id() == ID_struct && to_struct_type(t2).is_incomplete())
473 {
474 // ignore
475 return false;
476 }
477 else if(
478 t1.id() == ID_union && !to_union_type(t1).is_incomplete() &&
479 t2.id() == ID_union && to_union_type(t2).is_incomplete())
480 {
481 // ignore
482 return false;
483 }
484 else if(t1.id()!=t2.id())
485 {
486 // type classes do not match and can't be fixed
487 return true;
488 }
489
490 if(t1.id()==ID_pointer)
491 {
493#if 0
494 bool s=info.set_to_new;
495 if(adjust_object_type_rec(t1.subtype(), t2.subtype(), info))
496 {
497 diag.warning(
498 info.old_symbol,
499 info.new_symbol,
500 "conflicting pointer types for variable");
501 info.set_to_new=s;
502 }
503#else
504 diag.warning(
505 info.old_symbol,
506 info.new_symbol,
507 "conflicting pointer types for variable");
508#endif
509
510 if(info.old_symbol.is_extern && !info.new_symbol.is_extern)
511 {
512 info.set_to_new = true; // store new type
513 }
514
515 return false;
516 }
517 else if(
518 t1.id() == ID_array &&
520 to_array_type(t1).element_type(), to_array_type(t2).element_type(), info))
521 {
522 // still need to compare size
523 const exprt &old_size=to_array_type(t1).size();
524 const exprt &new_size=to_array_type(t2).size();
525
526 if(
527 (old_size.is_nil() && new_size.is_not_nil()) ||
528 (old_size == 0 && new_size.is_not_nil()) || info.old_symbol.is_weak)
529 {
530 info.set_to_new=true; // store new type
531 }
532 else if(new_size.is_nil() || new_size == 0 || info.new_symbol.is_weak)
533 {
534 // ok, we will use the old type
535 }
536 else
537 {
538 if(new_size.type() != old_size.type())
539 {
541 diag.error(
542 info.old_symbol,
543 info.new_symbol,
544 "conflicting array sizes for variable");
545
546 // error logged, continue typechecking other symbols
547 return true;
548 }
549
551
552 if(simplify_expr(eq, ns) != true)
553 {
555 diag.error(
556 info.old_symbol,
557 info.new_symbol,
558 "conflicting array sizes for variable");
559
560 // error logged, continue typechecking other symbols
561 return true;
562 }
563 }
564
565 return false;
566 }
567 else if(t1.id()==ID_struct || t1.id()==ID_union)
568 {
570 to_struct_union_type(t1).components();
571
573 to_struct_union_type(t2).components();
574
575 struct_union_typet::componentst::const_iterator
576 it1=components1.begin(), it2=components2.begin();
577 for( ;
578 it1!=components1.end() && it2!=components2.end();
579 ++it1, ++it2)
580 {
581 if(it1->get_name()!=it2->get_name() ||
582 adjust_object_type_rec(it1->type(), it2->type(), info))
583 return true;
584 }
585 if(it1!=components1.end() || it2!=components2.end())
586 return true;
587
588 return false;
589 }
590
591 return true;
592}
593
595 const symbolt &old_symbol,
596 const symbolt &new_symbol,
597 bool &set_to_new)
598{
599 const typet &old_type=follow_tags_symbols(ns, old_symbol.type);
600 const typet &new_type=follow_tags_symbols(ns, new_symbol.type);
601
602 adjust_type_infot info(old_symbol, new_symbol);
604 set_to_new=info.set_to_new;
605
606 return result;
607}
608
610 symbolt &old_symbol,
611 symbolt &new_symbol)
612{
613 // both are variables
614 bool set_to_new = false;
615
616 if(old_symbol.type != new_symbol.type)
617 {
618 bool failed=
619 adjust_object_type(old_symbol, new_symbol, set_to_new);
620
621 if(failed)
622 {
623 const typet &old_type=follow_tags_symbols(ns, old_symbol.type);
624
626
627 // provide additional diagnostic output for
628 // struct/union/array/enum
629 if(old_type.id()==ID_struct ||
630 old_type.id()==ID_union ||
631 old_type.id()==ID_array ||
632 old_type.id()==ID_c_enum)
633 {
634 diag.detailed_conflict_report(
635 old_symbol, new_symbol, old_symbol.type, new_symbol.type);
636 }
637
638 diag.error(old_symbol, new_symbol, "conflicting types for variable");
639
640 // error logged, continue typechecking other symbols
641 return;
642 }
643 else if(set_to_new)
644 old_symbol.type=new_symbol.type;
645
647 old_symbol.symbol_expr(), old_symbol.symbol_expr());
648 }
649
650 // care about initializers
651
652 if(!new_symbol.value.is_nil())
653 {
654 if(old_symbol.value.is_nil() ||
655 old_symbol.is_weak)
656 {
657 // new_symbol wins
658 old_symbol.value=new_symbol.value;
659 old_symbol.is_macro=new_symbol.is_macro;
660 }
661 else if(!new_symbol.is_weak)
662 {
663 // try simplifier
664 exprt tmp_old=old_symbol.value,
665 tmp_new=new_symbol.value;
666
669
670 if(tmp_old == tmp_new)
671 {
672 // ok, the same
673 }
674 else
675 {
677 log.warning().source_location = new_symbol.location;
678
679 log.warning() << "conflicting initializers for"
680 << " variable " << messaget::quote_begin
681 << old_symbol.name << messaget::quote_end << '\n';
682 log.warning() << "using old value in module " << messaget::quote_begin
683 << old_symbol.module << messaget::quote_end << " "
684 << old_symbol.value.find_source_location() << '\n'
685 << from_expr(ns, old_symbol.name, tmp_old) << '\n';
686 log.warning() << "ignoring new value in module "
687 << messaget::quote_begin << new_symbol.module
688 << messaget::quote_end << " "
689 << new_symbol.value.find_source_location() << '\n'
690 << from_expr(ns, new_symbol.name, tmp_new)
691 << messaget::eom;
692 }
693 }
694 }
695 else if(set_to_new && !old_symbol.value.is_nil())
696 {
697 // the type has been updated, now make sure that the initialising assignment
698 // will have matching types
699 old_symbol.value = typecast_exprt(old_symbol.value, old_symbol.type);
700 }
701}
702
704 symbolt &old_symbol,
705 symbolt &new_symbol)
706{
707 // we do not permit different contracts with the same name to be defined, or
708 // cases where only one of the symbols is a contract
709 if(
710 old_symbol.is_property != new_symbol.is_property ||
711 (old_symbol.is_property && new_symbol.is_property &&
712 old_symbol.type != new_symbol.type))
713 {
715 diag.error(old_symbol, new_symbol, "conflict on code contract");
716 }
717
718 // see if it is a function or a variable
719
720 bool is_code_old_symbol=old_symbol.type.id()==ID_code;
721 bool is_code_new_symbol=new_symbol.type.id()==ID_code;
722
724 {
726 diag.error(old_symbol, new_symbol, "conflicting definition for symbol");
727
728 // error logged, continue typechecking other symbols
729 return;
730 }
731
733 duplicate_code_symbol(old_symbol, new_symbol);
734 else
735 duplicate_object_symbol(old_symbol, new_symbol);
736
737 // care about flags
738
739 if(old_symbol.is_extern && !new_symbol.is_extern)
740 old_symbol.location=new_symbol.location;
741
742 // it's enough that one isn't extern for the final one not to be
743 old_symbol.is_extern=old_symbol.is_extern && new_symbol.is_extern;
744}
745
747 symbolt &old_symbol,
748 const symbolt &new_symbol)
749{
750 PRECONDITION(new_symbol.is_type);
751
752 if(!old_symbol.is_type)
753 {
755 diag.error(old_symbol, new_symbol, "conflicting definition for symbol");
756
757 // error logged, continue typechecking other symbols
758 return;
759 }
760
761 if(old_symbol.type==new_symbol.type)
762 return;
763
764 if(
765 old_symbol.type.id() == ID_struct &&
766 to_struct_type(old_symbol.type).is_incomplete() &&
767 new_symbol.type.id() == ID_struct &&
768 !to_struct_type(new_symbol.type).is_incomplete())
769 {
770 old_symbol.type=new_symbol.type;
771 old_symbol.location=new_symbol.location;
772 return;
773 }
774
775 if(
776 old_symbol.type.id() == ID_struct &&
777 !to_struct_type(old_symbol.type).is_incomplete() &&
778 new_symbol.type.id() == ID_struct &&
779 to_struct_type(new_symbol.type).is_incomplete())
780 {
781 // ok, keep old
782 return;
783 }
784
785 if(
786 old_symbol.type.id() == ID_union &&
787 to_union_type(old_symbol.type).is_incomplete() &&
788 new_symbol.type.id() == ID_union &&
789 !to_union_type(new_symbol.type).is_incomplete())
790 {
791 old_symbol.type=new_symbol.type;
792 old_symbol.location=new_symbol.location;
793 return;
794 }
795
796 if(
797 old_symbol.type.id() == ID_union &&
798 !to_union_type(old_symbol.type).is_incomplete() &&
799 new_symbol.type.id() == ID_union &&
800 to_union_type(new_symbol.type).is_incomplete())
801 {
802 // ok, keep old
803 return;
804 }
805
806 if(
807 old_symbol.type.id() == ID_array && new_symbol.type.id() == ID_array &&
808 to_array_type(old_symbol.type).element_type() ==
809 to_array_type(new_symbol.type).element_type())
810 {
811 if(to_array_type(old_symbol.type).size().is_nil() &&
812 to_array_type(new_symbol.type).size().is_not_nil())
813 {
814 to_array_type(old_symbol.type).size()=
815 to_array_type(new_symbol.type).size();
816 return;
817 }
818
819 if(to_array_type(new_symbol.type).size().is_nil() &&
820 to_array_type(old_symbol.type).size().is_not_nil())
821 {
822 // ok, keep old
823 return;
824 }
825 }
826
828
829 diag.detailed_conflict_report(
830 old_symbol, new_symbol, old_symbol.type, new_symbol.type);
831
832 diag.error(
833 old_symbol, new_symbol, "unexpected difference between type symbols");
834}
835
837 const symbolt &old_symbol,
838 const symbolt &new_symbol)
839{
840 PRECONDITION(new_symbol.is_type);
841
842 if(!old_symbol.is_type)
844
845 if(old_symbol.type==new_symbol.type)
847
848 if(
849 old_symbol.type.id() == ID_struct &&
850 to_struct_type(old_symbol.type).is_incomplete() &&
851 new_symbol.type.id() == ID_struct &&
852 !to_struct_type(new_symbol.type).is_incomplete())
853 {
854 return renamingt::NO_RENAMING; // not different
855 }
856
857 if(
858 old_symbol.type.id() == ID_struct &&
859 !to_struct_type(old_symbol.type).is_incomplete() &&
860 new_symbol.type.id() == ID_struct &&
861 to_struct_type(new_symbol.type).is_incomplete())
862 {
863 return renamingt::NO_RENAMING; // not different
864 }
865
866 if(
867 old_symbol.type.id() == ID_union &&
868 to_union_type(old_symbol.type).is_incomplete() &&
869 new_symbol.type.id() == ID_union &&
870 !to_union_type(new_symbol.type).is_incomplete())
871 {
872 return renamingt::NO_RENAMING; // not different
873 }
874
875 if(
876 old_symbol.type.id() == ID_union &&
877 !to_union_type(old_symbol.type).is_incomplete() &&
878 new_symbol.type.id() == ID_union &&
879 to_union_type(new_symbol.type).is_incomplete())
880 {
881 return renamingt::NO_RENAMING; // not different
882 }
883
884 if(
885 old_symbol.type.id() == ID_array && new_symbol.type.id() == ID_array &&
886 to_array_type(old_symbol.type).element_type() ==
887 to_array_type(new_symbol.type).element_type())
888 {
889 if(to_array_type(old_symbol.type).size().is_nil() &&
890 to_array_type(new_symbol.type).size().is_not_nil())
891 {
892 return renamingt::NO_RENAMING; // not different
893 }
894
895 if(to_array_type(new_symbol.type).size().is_nil() &&
896 to_array_type(old_symbol.type).size().is_not_nil())
897 {
898 return renamingt::NO_RENAMING; // not different
899 }
900 }
901
902 return renamingt::RENAME_NEW; // different
903}
904
907 std::unordered_set<irep_idt> &needs_to_be_renamed,
908 message_handlert &message_handler)
909{
910 // Any type that uses a symbol that will be renamed also
911 // needs to be renamed, and so on, until saturation.
912
913 // X -> Y iff Y uses X for new symbol type IDs X and Y
914 std::unordered_map<irep_idt, std::unordered_set<irep_idt>> used_by;
915
916 for(const auto &symbol_pair : src_symbol_table.symbols)
917 {
918 if(symbol_pair.second.is_type)
919 {
920 // find type and array-size symbols
923
924 for(const auto &symbol_used : symbols_used)
925 {
926 used_by[symbol_used].insert(symbol_pair.first);
927 }
928 }
929 }
930
931 std::deque<irep_idt> queue(
933
934 while(!queue.empty())
935 {
936 irep_idt id = queue.back();
937 queue.pop_back();
938
939 const std::unordered_set<irep_idt> &u = used_by[id];
940
941 for(const auto &dep : u)
942 if(needs_to_be_renamed.insert(dep).second)
943 {
944 queue.push_back(dep);
945 #ifdef DEBUG
946 messaget log{message_handler};
947 log.debug() << "LINKING: needs to be renamed (dependency): " << dep
948 << messaget::eom;
949#endif
950 }
951 }
952}
953
954 std::unordered_map<irep_idt, irep_idt> linkingt::rename_symbols(
956 const std::unordered_set<irep_idt> &needs_to_be_renamed)
957{
958 std::unordered_map<irep_idt, irep_idt> new_identifiers;
960
961 for(const irep_idt &id : needs_to_be_renamed)
962 {
963 const symbolt &new_symbol = src_ns.lookup(id);
964
966
967 if(new_symbol.is_type)
968 new_identifier=type_to_name(src_ns, id, new_symbol.type);
969 else
971
972 new_identifiers.emplace(id, new_identifier);
973
974#ifdef DEBUG
976 log.debug() << "LINKING: renaming " << id << " to " << new_identifier
977 << messaget::eom;
978#endif
979
980 if(new_symbol.is_type)
982 else
984 }
985
986 return new_identifiers;
987}
988
991 const std::unordered_map<irep_idt, irep_idt> &new_identifiers)
992{
993 std::map<irep_idt, symbolt> src_symbols;
994 // First apply the renaming
995 for(const auto &named_symbol : src_symbol_table.symbols)
996 {
997 symbolt symbol=named_symbol.second;
998 // apply the renaming
999 rename_new_symbol(symbol.type);
1000 rename_new_symbol(symbol.value);
1001 auto it = new_identifiers.find(named_symbol.first);
1002 if(it != new_identifiers.end())
1003 symbol.name = it->second;
1004
1005 src_symbols.emplace(named_symbol.first, std::move(symbol));
1006 }
1007
1008 // Move over all the non-colliding ones
1009 std::unordered_set<irep_idt> collisions;
1010
1011 for(const auto &named_symbol : src_symbols)
1012 {
1013 // renamed?
1014 if(named_symbol.first!=named_symbol.second.name)
1015 {
1016 // new
1018 }
1019 else
1020 {
1022 {
1023 // new
1025 }
1026 else
1027 collisions.insert(named_symbol.first);
1028 }
1029 }
1030
1031 // Now do the collisions
1032 for(const irep_idt &collision : collisions)
1033 {
1035 symbolt &new_symbol=src_symbols.at(collision);
1036
1037 if(new_symbol.is_type)
1038 duplicate_type_symbol(old_symbol, new_symbol);
1039 else
1040 duplicate_non_type_symbol(old_symbol, new_symbol);
1041 }
1042
1043 // Apply type updates to initializers
1044 for(auto it = main_symbol_table.begin(); it != main_symbol_table.end(); ++it)
1045 {
1046 if(
1047 !it->second.is_type && !it->second.is_macro &&
1048 it->second.value.is_not_nil())
1049 {
1050 object_type_updates(it.get_writeable_symbol().value);
1051 }
1052 }
1053}
1054
1056{
1057 const unsigned errors_before =
1059
1060 // We do this in three phases. We first figure out which symbols need to
1061 // be renamed, and then build the renaming, and finally apply this
1062 // renaming in the second pass over the symbol table.
1063
1064 // PHASE 1: identify symbols to be renamed
1065
1066 std::unordered_set<irep_idt> needs_to_be_renamed;
1067
1068 for(const auto &symbol_pair : src_symbol_table.symbols)
1069 {
1070 symbol_table_baset::symbolst::const_iterator m_it =
1072
1073 if(m_it != main_symbol_table.symbols.end())
1074 {
1075 // duplicate
1076 switch(needs_renaming(m_it->second, symbol_pair.second))
1077 {
1079 break;
1081 {
1082 symbolt renamed_symbol = m_it->second;
1084 if(m_it->second.is_type)
1086 else
1090 break;
1091 }
1093 {
1094 needs_to_be_renamed.insert(symbol_pair.first);
1095#ifdef DEBUG
1097 log.debug() << "LINKING: needs to be renamed: " << symbol_pair.first
1098 << messaget::eom;
1099#endif
1100 break;
1101 }
1102 }
1103 }
1104 }
1105
1106 // rename within main symbol table
1107 for(auto &symbol_pair : main_symbol_table)
1108 {
1109 symbolt tmp = symbol_pair.second;
1110 bool unmodified = rename_main_symbol(tmp.value);
1112 if(!unmodified)
1113 {
1116 *sym_ptr = std::move(tmp);
1117 }
1118 }
1119
1120 // renaming types may trigger further renaming
1122
1123 // PHASE 2: actually rename them
1125
1126 // PHASE 3: copy new symbols to main table
1128
1130}
1131
1134 const symbol_table_baset &new_symbol_table,
1135 message_handlert &message_handler)
1136{
1137 linkingt linking(dest_symbol_table, message_handler);
1138
1139 return linking.link(new_symbol_table);
1140}
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Base type of functions.
Definition std_types.h:582
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Equality.
Definition std_expr.h:1339
Base class for all expressions.
Definition expr.h:57
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:68
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
bool is_not_nil() const
Definition irep.h:372
void make_nil()
Definition irep.h:446
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
std::unordered_map< irep_idt, irep_idt > rename_symbols(const symbol_table_baset &, const std::unordered_set< irep_idt > &needs_to_be_renamed)
Definition linking.cpp:954
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition linking.cpp:703
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
Definition linking.cpp:594
bool link(const symbol_table_baset &src_symbol_table)
Merges the symbol table src_symbol_table into main_symbol_table, renaming symbols from src_symbol_tab...
Definition linking.cpp:1055
renamingt needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
Definition linking_class.h:60
namespacet ns
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
Definition linking.cpp:401
rename_symbolt rename_main_symbol
Definition linking_class.h:43
void copy_symbols(const symbol_table_baset &, const std::unordered_map< irep_idt, irep_idt > &)
Definition linking.cpp:989
irep_idt rename(const symbol_table_baset &, const irep_idt &)
Definition linking.cpp:43
renamingt needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition linking.cpp:836
symbol_table_baset & main_symbol_table
renamingt needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition linking.cpp:67
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition linking.cpp:609
casting_replace_symbolt object_type_updates
Definition linking_class.h:44
std::unordered_set< irep_idt > renamed_ids
void duplicate_type_symbol(symbolt &old_symbol, const symbolt &new_symbol)
Definition linking.cpp:746
rename_symbolt rename_new_symbol
Definition linking_class.h:43
@ NO_RENAMING
Definition linking_class.h:49
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition linking.cpp:82
message_handlert & message_handler
Definition message.h:27
std::size_t get_message_count(unsigned level) const
Definition message.h:55
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static const commandt quote_begin
Start quoted text.
Definition message.h:389
static const commandt quote_end
End quoted text.
Definition message.h:393
@ M_ERROR
Definition message.h:169
static eomt eom
Definition message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
void insert_type(const irep_idt &old_id, const irep_idt &new_id)
Definition rename_symbol.h:40
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition rename_symbol.h:31
std::size_t erase(const irep_idt &id)
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
std::vector< componentt > componentst
Definition std_types.h:139
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
virtual iteratort begin()=0
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual iteratort end()=0
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_extern
Definition symbol.h:74
bool is_macro
Definition symbol.h:62
bool is_file_local
Definition symbol.h:73
bool is_property
Definition symbol.h:67
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
bool is_weak
Definition symbol.h:78
irep_idt name
The unique identifier.
Definition symbol.h:40
exprt value
Initial value of symbol.
Definition symbol.h:34
Semantic type conversion.
Definition std_expr.h:1995
The type of an expression, extends irept.
Definition type.h:29
The union type.
Definition c_types.h:147
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
std::unordered_set< irep_idt > find_symbols_sett
Definition find_symbols.h:22
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
static void do_type_dependencies(const symbol_table_baset &src_symbol_table, std::unordered_set< irep_idt > &needs_to_be_renamed, message_handlert &message_handler)
Definition linking.cpp:905
static const typet & follow_tags_symbols(const namespacet &ns, const typet &type)
Definition linking.cpp:28
bool linking(symbol_table_baset &dest_symbol_table, const symbol_table_baset &new_symbol_table, message_handlert &message_handler)
Merges the symbol table new_symbol_table into dest_symbol_table, renaming symbols from new_symbol_tab...
Definition linking.cpp:1132
ANSI-C Linking.
ANSI-C Linking.
ANSI-C Linking.
double log(double x)
Definition math.c:2416
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:787
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:307
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:517
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:213
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition std_types.h:433
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition linking_class.h:93
Author: Diffblue Ltd.
static bool failed(bool error_indicator)

AltStyle によって変換されたページ (->オリジナル) /