cprover
linking.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Linking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "linking.h"
13 
14 #include <cassert>
15 #include <stack>
16 
17 #include <util/find_symbols.h>
18 #include <util/source_location.h>
19 #include <util/base_type.h>
20 #include <util/std_expr.h>
21 #include <util/std_types.h>
22 #include <util/simplify_expr.h>
24 
25 #include <langapi/language_util.h>
26 
27 #include "linking_class.h"
28 
30  const namespacet &ns,
31  const irep_idt &identifier,
32  const exprt &expr) const
33 {
34  return from_expr(ns, identifier, expr);
35 }
36 
38  const namespacet &ns,
39  const irep_idt &identifier,
40  const typet &type) const
41 {
42  return from_type(ns, identifier, type);
43 }
44 
45 static const typet &follow_tags_symbols(
46  const namespacet &ns,
47  const typet &type)
48 {
49  if(type.id()==ID_symbol)
50  return ns.follow(type);
51  else if(type.id()==ID_c_enum_tag)
52  return ns.follow_tag(to_c_enum_tag_type(type));
53  else if(type.id()==ID_struct_tag)
54  return ns.follow_tag(to_struct_tag_type(type));
55  else if(type.id()==ID_union_tag)
56  return ns.follow_tag(to_union_tag_type(type));
57  else
58  return type;
59 }
60 
62  const namespacet &ns,
63  const symbolt &symbol,
64  const typet &type) const
65 {
66  const typet &followed=follow_tags_symbols(ns, type);
67 
68  if(followed.id()==ID_struct || followed.id()==ID_union)
69  {
70  std::string result=followed.id_string();
71 
72  const std::string &tag=followed.get_string(ID_tag);
73  if(tag!="")
74  result+=" "+tag;
75  result+=" {\n";
76 
77  const struct_union_typet::componentst &components=
78  to_struct_union_type(followed).components();
79 
80  for(struct_union_typet::componentst::const_iterator
81  it=components.begin();
82  it!=components.end();
83  it++)
84  {
85  const typet &subtype=it->type();
86  result+=" ";
87  result+=type_to_string(ns, symbol.name, subtype);
88  result+=' ';
89 
90  if(it->get_base_name()!="")
91  result+=id2string(it->get_base_name());
92  else
93  result+=id2string(it->get_name());
94 
95  result+=";\n";
96  }
97 
98  result+='}';
99 
100  return result;
101  }
102  else if(followed.id()==ID_pointer)
103  {
104  return type_to_string_verbose(ns, symbol, followed.subtype())+" *";
105  }
106  else if(followed.id()==ID_incomplete_struct ||
107  followed.id()==ID_incomplete_union)
108  {
109  return type_to_string(ns, symbol.name, type)+" (incomplete)";
110  }
111 
112  return type_to_string(ns, symbol.name, type);
113 }
114 
116  const symbolt &old_symbol,
117  const symbolt &new_symbol,
118  const typet &type1,
119  const typet &type2,
120  unsigned depth,
121  exprt &conflict_path)
122 {
123  #ifdef DEBUG
124  debug() << "<BEGIN DEPTH " << depth << ">" << eom;
125  #endif
126 
127  std::string msg;
128 
129  const typet &t1=follow_tags_symbols(ns, type1);
130  const typet &t2=follow_tags_symbols(ns, type2);
131 
132  if(t1.id()!=t2.id())
133  msg="type classes differ";
134  else if(t1.id()==ID_pointer ||
135  t1.id()==ID_array)
136  {
137  if(depth>0 &&
138  !base_type_eq(t1.subtype(), t2.subtype(), ns))
139  {
140  conflict_path=dereference_exprt(conflict_path);
141 
143  old_symbol,
144  new_symbol,
145  t1.subtype(),
146  t2.subtype(),
147  depth-1,
148  conflict_path);
149  }
150  else if(t1.id()==ID_pointer)
151  msg="pointer types differ";
152  else
153  msg="array types differ";
154  }
155  else if(t1.id()==ID_struct ||
156  t1.id()==ID_union)
157  {
158  const struct_union_typet::componentst &components1=
160 
161  const struct_union_typet::componentst &components2=
163 
164  exprt conflict_path_before=conflict_path;
165 
166  if(components1.size()!=components2.size())
167  {
168  msg="number of members is different (";
169  msg+=std::to_string(components1.size())+'/';
170  msg+=std::to_string(components2.size())+')';
171  }
172  else
173  {
174  for(std::size_t i=0; i<components1.size(); ++i)
175  {
176  const typet &subtype1=components1[i].type();
177  const typet &subtype2=components2[i].type();
178 
179  if(components1[i].get_name()!=components2[i].get_name())
180  {
181  msg="names of member "+std::to_string(i)+" differ (";
182  msg+=id2string(components1[i].get_name())+'/';
183  msg+=id2string(components2[i].get_name())+')';
184  break;
185  }
186  else if(!base_type_eq(subtype1, subtype2, ns))
187  {
188  typedef std::unordered_set<typet, irep_hash> type_sett;
189  type_sett parent_types;
190 
191  exprt e=conflict_path_before;
192  while(e.id()==ID_dereference ||
193  e.id()==ID_member ||
194  e.id()==ID_index)
195  {
196  parent_types.insert(e.type());
197  e=e.op0();
198  }
199 
200  conflict_path=conflict_path_before;
201  conflict_path.type()=t1;
202  conflict_path=
203  member_exprt(conflict_path, components1[i].get_name());
204 
205  if(depth>0 &&
206  parent_types.find(t1)==parent_types.end())
208  old_symbol,
209  new_symbol,
210  subtype1,
211  subtype2,
212  depth-1,
213  conflict_path);
214  else
215  {
216  msg="type of member "+
217  id2string(components1[i].get_name())+
218  " differs";
219  if(depth>0)
220  {
221  std::string msg_bak;
222  msg_bak.swap(msg);
223  symbol_exprt c(ID_C_this);
225  old_symbol,
226  new_symbol,
227  subtype1,
228  subtype2,
229  depth-1,
230  c);
231  msg.swap(msg_bak);
232  }
233  }
234 
235  if(parent_types.find(t1)==parent_types.end())
236  break;
237  }
238  }
239  }
240  }
241  else if(t1.id()==ID_c_enum)
242  {
243  const c_enum_typet::memberst &members1=
244  to_c_enum_type(t1).members();
245 
246  const c_enum_typet::memberst &members2=
247  to_c_enum_type(t2).members();
248 
249  if(t1.subtype()!=t2.subtype())
250  {
251  msg="enum value types are different (";
252  msg+=type_to_string(ns, old_symbol.name, t1.subtype())+'/';
253  msg+=type_to_string(ns, new_symbol.name, t2.subtype())+')';
254  }
255  else if(members1.size()!=members2.size())
256  {
257  msg="number of enum members is different (";
258  msg+=std::to_string(members1.size())+'/';
259  msg+=std::to_string(members2.size())+')';
260  }
261  else
262  {
263  for(std::size_t i=0; i<members1.size(); ++i)
264  {
265  if(members1[i].get_base_name()!=members2[i].get_base_name())
266  {
267  msg="names of member "+std::to_string(i)+" differ (";
268  msg+=id2string(members1[i].get_base_name())+'/';
269  msg+=id2string(members2[i].get_base_name())+')';
270  break;
271  }
272  else if(members1[i].get_value()!=members2[i].get_value())
273  {
274  msg="values of member "+std::to_string(i)+" differ (";
275  msg+=id2string(members1[i].get_value())+'/';
276  msg+=id2string(members2[i].get_value())+')';
277  break;
278  }
279  }
280  }
281 
282  msg+="\nenum declarations at\n";
283  msg+=t1.source_location().as_string()+" and\n";
284  msg+=t1.source_location().as_string();
285  }
286  else if(t1.id()==ID_code)
287  {
288  const code_typet::parameterst &parameters1=
289  to_code_type(t1).parameters();
290 
291  const code_typet::parameterst &parameters2=
292  to_code_type(t2).parameters();
293 
294  const typet &return_type1=to_code_type(t1).return_type();
295  const typet &return_type2=to_code_type(t2).return_type();
296 
297  if(parameters1.size()!=parameters2.size())
298  {
299  msg="parameter counts differ (";
300  msg+=std::to_string(parameters1.size())+'/';
301  msg+=std::to_string(parameters2.size())+')';
302  }
303  else if(!base_type_eq(return_type1, return_type2, ns))
304  {
305  conflict_path=
306  index_exprt(conflict_path,
307  constant_exprt(std::to_string(-1), integer_typet()));
308 
309  if(depth>0)
311  old_symbol,
312  new_symbol,
313  return_type1,
314  return_type2,
315  depth-1,
316  conflict_path);
317  else
318  msg="return types differ";
319  }
320  else
321  {
322  for(std::size_t i=0; i<parameters1.size(); i++)
323  {
324  const typet &subtype1=parameters1[i].type();
325  const typet &subtype2=parameters2[i].type();
326 
327  if(!base_type_eq(subtype1, subtype2, ns))
328  {
329  conflict_path=
330  index_exprt(conflict_path,
331  constant_exprt(std::to_string(i), integer_typet()));
332 
333  if(depth>0)
335  old_symbol,
336  new_symbol,
337  subtype1,
338  subtype2,
339  depth-1,
340  conflict_path);
341  else
342  msg="parameter types differ";
343 
344  break;
345  }
346  }
347  }
348  }
349  else
350  msg="conflict on POD";
351 
352  if(!msg.empty())
353  {
354  error() << '\n';
355  error() << "reason for conflict at "
356  << expr_to_string(ns, "", conflict_path)
357  << ": " << msg << '\n';
358 
359  error() << '\n';
360  error() << type_to_string_verbose(ns, old_symbol, t1) << '\n';
361  error() << type_to_string_verbose(ns, new_symbol, t2) << '\n';
362  }
363 
364  #ifdef DEBUG
365  debug() << "<END DEPTH " << depth << ">" << eom;
366  #endif
367 }
368 
370  const symbolt &old_symbol,
371  const symbolt &new_symbol,
372  const std::string &msg)
373 {
374  error().source_location=new_symbol.location;
375 
376  error() << "error: " << msg << " `"
377  << old_symbol.display_name()
378  << "'" << '\n';
379  error() << "old definition in module `" << old_symbol.module
380  << "' " << old_symbol.location << '\n'
381  << type_to_string_verbose(ns, old_symbol) << '\n';
382  error() << "new definition in module `" << new_symbol.module
383  << "' " << new_symbol.location << '\n'
384  << type_to_string_verbose(ns, new_symbol) << eom;
385 
386  throw 0;
387 }
388 
390  const symbolt &old_symbol,
391  const symbolt &new_symbol,
392  const std::string &msg)
393 {
394  warning().source_location=new_symbol.location;
395 
396  warning() << "warning: " << msg << " \""
397  << old_symbol.display_name()
398  << "\"" << '\n';
399  warning() << "old definition in module " << old_symbol.module
400  << " " << old_symbol.location << '\n'
401  << type_to_string_verbose(ns, old_symbol) << '\n';
402  warning() << "new definition in module " << new_symbol.module
403  << " " << new_symbol.location << '\n'
404  << type_to_string_verbose(ns, new_symbol) << eom;
405 }
406 
408 {
409  unsigned cnt=0;
410 
411  while(true)
412  {
413  irep_idt new_identifier=
414  id2string(id)+"$link"+std::to_string(++cnt);
415 
416  if(main_symbol_table.symbols.find(new_identifier)!=
418  continue; // already in main symbol table
419 
420  if(!renamed_ids.insert(new_identifier).second)
421  continue; // used this for renaming already
422 
423  if(src_symbol_table.symbols.find(new_identifier)!=
425  continue; // used by some earlier linking call already
426 
427  return new_identifier;
428  }
429 }
430 
432  const symbolt &old_symbol,
433  const symbolt &new_symbol)
434 {
435  // We first take care of file-local non-type symbols.
436  // These are static functions, or static variables
437  // inside static function bodies.
438  if(new_symbol.is_file_local ||
439  old_symbol.is_file_local)
440  return true;
441 
442  return false;
443 }
444 
446  symbolt &old_symbol,
447  symbolt &new_symbol)
448 {
449  // Both are functions.
450  if(!base_type_eq(old_symbol.type, new_symbol.type, ns))
451  {
452  const code_typet &old_t=to_code_type(old_symbol.type);
453  const code_typet &new_t=to_code_type(new_symbol.type);
454 
455  // if one of them was an implicit declaration, just issue a warning
456  if(!old_symbol.location.get_function().empty() &&
457  old_symbol.value.is_nil())
458  {
459  // issue a warning and overwrite
460  link_warning(
461  old_symbol,
462  new_symbol,
463  "implicit function declaration");
464 
465  old_symbol.type=new_symbol.type;
466  old_symbol.location=new_symbol.location;
467  old_symbol.is_weak=new_symbol.is_weak;
468  }
469  else if(!new_symbol.location.get_function().empty() &&
470  new_symbol.value.is_nil())
471  {
472  // issue a warning
473  link_warning(
474  old_symbol,
475  new_symbol,
476  "ignoring conflicting implicit function declaration");
477  }
478  // handle (incomplete) function prototypes
479  else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&
480  ((old_t.parameters().empty() &&
481  old_t.has_ellipsis() &&
482  old_symbol.value.is_nil()) ||
483  (new_t.parameters().empty() &&
484  new_t.has_ellipsis() &&
485  new_symbol.value.is_nil())))
486  {
487  if(old_t.parameters().empty() &&
488  old_t.has_ellipsis() &&
489  old_symbol.value.is_nil())
490  {
491  old_symbol.type=new_symbol.type;
492  old_symbol.location=new_symbol.location;
493  old_symbol.is_weak=new_symbol.is_weak;
494  }
495  }
496  // replace weak symbols
497  else if(old_symbol.is_weak)
498  {
499  if(new_symbol.value.is_nil())
500  link_warning(
501  old_symbol,
502  new_symbol,
503  "function declaration conflicts with with weak definition");
504  else
505  old_symbol.value.make_nil();
506  }
507  else if(new_symbol.is_weak)
508  {
509  if(new_symbol.value.is_nil() ||
510  old_symbol.value.is_not_nil())
511  {
512  new_symbol.value.make_nil();
513 
514  link_warning(
515  old_symbol,
516  new_symbol,
517  "ignoring conflicting weak function declaration");
518  }
519  }
520  // aliasing may alter the type
521  else if((new_symbol.is_macro &&
522  new_symbol.value.is_not_nil() &&
523  old_symbol.value.is_nil()) ||
524  (old_symbol.is_macro &&
525  old_symbol.value.is_not_nil() &&
526  new_symbol.value.is_nil()))
527  {
528  link_warning(
529  old_symbol,
530  new_symbol,
531  "ignoring conflicting function alias declaration");
532  }
533  // conflicting declarations without a definition, matching return
534  // types
535  else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&
536  old_symbol.value.is_nil() &&
537  new_symbol.value.is_nil())
538  {
539  link_warning(
540  old_symbol,
541  new_symbol,
542  "ignoring conflicting function declarations");
543 
544  if(old_t.parameters().size()<new_t.parameters().size())
545  {
546  old_symbol.type=new_symbol.type;
547  old_symbol.location=new_symbol.location;
548  old_symbol.is_weak=new_symbol.is_weak;
549  }
550  }
551  // mismatch on number of parameters is definitively an error
552  else if((old_t.parameters().size()<new_t.parameters().size() &&
553  new_symbol.value.is_not_nil() &&
554  !old_t.has_ellipsis()) ||
555  (old_t.parameters().size()>new_t.parameters().size() &&
556  old_symbol.value.is_not_nil() &&
557  !new_t.has_ellipsis()))
558  {
559  link_error(
560  old_symbol,
561  new_symbol,
562  "conflicting parameter counts of function declarations");
563  }
564  else
565  {
566  // the number of parameters matches, collect all the conflicts
567  // and see whether they can be cured
568  std::string warn_msg;
569  bool replace=false;
570  typedef std::deque<std::pair<typet, typet> > conflictst;
571  conflictst conflicts;
572 
573  if(!base_type_eq(old_t.return_type(), new_t.return_type(), ns))
574  conflicts.push_back(
575  std::make_pair(old_t.return_type(), new_t.return_type()));
576 
577  code_typet::parameterst::const_iterator
578  n_it=new_t.parameters().begin(),
579  o_it=old_t.parameters().begin();
580  for( ;
581  o_it!=old_t.parameters().end() &&
582  n_it!=new_t.parameters().end();
583  ++o_it, ++n_it)
584  {
585  if(!base_type_eq(o_it->type(), n_it->type(), ns))
586  conflicts.push_back(
587  std::make_pair(o_it->type(), n_it->type()));
588  }
589  if(o_it!=old_t.parameters().end())
590  {
591  if(!new_t.has_ellipsis() && old_symbol.value.is_not_nil())
592  link_error(
593  old_symbol,
594  new_symbol,
595  "conflicting parameter counts of function declarations");
596  replace=new_symbol.value.is_not_nil();
597  }
598  else if(n_it!=new_t.parameters().end())
599  {
600  if(!old_t.has_ellipsis() && new_symbol.value.is_not_nil())
601  link_error(
602  old_symbol,
603  new_symbol,
604  "conflicting parameter counts of function declarations");
605  replace=new_symbol.value.is_not_nil();
606  }
607 
608  while(!conflicts.empty())
609  {
610  const typet &t1=follow_tags_symbols(ns, conflicts.front().first);
611  const typet &t2=follow_tags_symbols(ns, conflicts.front().second);
612 
613  // void vs. non-void return type may be acceptable if the
614  // return value is never used
615  if((t1.id()==ID_empty || t2.id()==ID_empty) &&
616  (old_symbol.value.is_nil() || new_symbol.value.is_nil()))
617  {
618  if(warn_msg.empty())
619  warn_msg="void/non-void return type conflict on function";
620  replace=
621  new_symbol.value.is_not_nil() ||
622  (old_symbol.value.is_nil() && t2.id()==ID_empty);
623  }
624  // different pointer arguments without implementation may work
625  else if((t1.id()==ID_pointer || t2.id()==ID_pointer) &&
627  old_symbol.value.is_nil() && new_symbol.value.is_nil())
628  {
629  if(warn_msg.empty())
630  warn_msg="different pointer types in extern function";
631  }
632  // different pointer arguments with implementation - the
633  // implementation is always right, even though such code may
634  // be severely broken
635  else if((t1.id()==ID_pointer || t2.id()==ID_pointer) &&
637  old_symbol.value.is_nil()!=new_symbol.value.is_nil())
638  {
639  if(warn_msg.empty())
640  warn_msg="pointer parameter types differ between "
641  "declaration and definition";
642  replace=new_symbol.value.is_not_nil();
643  }
644  // transparent union with (or entirely without) implementation is
645  // ok -- this primarily helps all those people that don't get
646  // _GNU_SOURCE consistent
647  else if((t1.id()==ID_union &&
648  (t1.get_bool(ID_C_transparent_union) ||
649  conflicts.front().first.get_bool(ID_C_transparent_union))) ||
650  (t2.id()==ID_union &&
651  (t2.get_bool(ID_C_transparent_union) ||
652  conflicts.front().second.get_bool(ID_C_transparent_union))))
653  {
654  const bool use_old=
655  t1.id()==ID_union &&
656  (t1.get_bool(ID_C_transparent_union) ||
657  conflicts.front().first.get_bool(ID_C_transparent_union)) &&
658  new_symbol.value.is_nil();
659 
660  const union_typet &union_type=
661  to_union_type(t1.id()==ID_union?t1:t2);
662  const typet &src_type=t1.id()==ID_union?t2:t1;
663 
664  bool found=false;
665  for(union_typet::componentst::const_iterator
666  it=union_type.components().begin();
667  !found && it!=union_type.components().end();
668  it++)
669  if(base_type_eq(it->type(), src_type, ns))
670  {
671  found=true;
672  if(warn_msg.empty())
673  warn_msg="conflict on transparent union parameter in function";
674  replace=!use_old;
675  }
676 
677  if(!found)
678  break;
679  }
680  else
681  break;
682 
683  conflicts.pop_front();
684  }
685 
686  if(!conflicts.empty())
687  {
689  old_symbol,
690  new_symbol,
691  conflicts.front().first,
692  conflicts.front().second);
693 
694  link_error(
695  old_symbol,
696  new_symbol,
697  "conflicting function declarations");
698  }
699  else
700  {
701  // warns about the first inconsistency
702  link_warning(old_symbol, new_symbol, warn_msg);
703 
704  if(replace)
705  {
706  old_symbol.type=new_symbol.type;
707  old_symbol.location=new_symbol.location;
708  }
709  }
710  }
711  }
712 
713  if(!new_symbol.value.is_nil())
714  {
715  if(old_symbol.value.is_nil())
716  {
717  // the one with body wins!
718  rename_symbol(new_symbol.value);
719  rename_symbol(new_symbol.type);
720  old_symbol.value=new_symbol.value;
721  old_symbol.type=new_symbol.type; // for parameter identifiers
722  old_symbol.is_weak=new_symbol.is_weak;
723  old_symbol.location=new_symbol.location;
724  old_symbol.is_macro=new_symbol.is_macro;
725  }
726  else if(to_code_type(old_symbol.type).get_inlined())
727  {
728  // ok, silently ignore
729  }
730  else if(base_type_eq(old_symbol.type, new_symbol.type, ns))
731  {
732  // keep the one in old_symbol -- libraries come last!
733  warning().source_location=new_symbol.location;
734 
735  warning() << "function `" << old_symbol.name << "' in module `"
736  << new_symbol.module << "' is shadowed by a definition in module `"
737  << old_symbol.module << "'" << eom;
738  }
739  else
740  link_error(
741  old_symbol,
742  new_symbol,
743  "duplicate definition of function");
744  }
745 }
746 
748  const typet &t1,
749  const typet &t2,
750  adjust_type_infot &info)
751 {
752  if(base_type_eq(t1, t2, ns))
753  return false;
754 
755  if(t1.id()==ID_symbol ||
756  t1.id()==ID_struct_tag ||
757  t1.id()==ID_union_tag ||
758  t1.id()==ID_c_enum_tag)
759  {
760  const irep_idt &identifier=t1.get(ID_identifier);
761 
762  if(info.o_symbols.insert(identifier).second)
763  {
764  bool result=
766  info.o_symbols.erase(identifier);
767 
768  return result;
769  }
770 
771  return false;
772  }
773  else if(t2.id()==ID_symbol ||
774  t2.id()==ID_struct_tag ||
775  t2.id()==ID_union_tag ||
776  t2.id()==ID_c_enum_tag)
777  {
778  const irep_idt &identifier=t2.get(ID_identifier);
779 
780  if(info.n_symbols.insert(identifier).second)
781  {
782  bool result=
784  info.n_symbols.erase(identifier);
785 
786  return result;
787  }
788 
789  return false;
790  }
791  else if(t1.id()==ID_pointer && t2.id()==ID_array)
792  {
793  info.set_to_new=true; // store new type
794 
795  return false;
796  }
797  else if(t1.id()==ID_array && t2.id()==ID_pointer)
798  {
799  // ignore
800  return false;
801  }
802  else if((t1.id()==ID_incomplete_struct && t2.id()==ID_struct) ||
803  (t1.id()==ID_incomplete_union && t2.id()==ID_union))
804  {
805  info.set_to_new=true; // store new type
806 
807  return false;
808  }
809  else if((t1.id()==ID_struct && t2.id()==ID_incomplete_struct) ||
810  (t1.id()==ID_union && t2.id()==ID_incomplete_union))
811  {
812  // ignore
813  return false;
814  }
815  else if(t1.id()!=t2.id())
816  {
817  // type classes do not match and can't be fixed
818  return true;
819  }
820 
821  if(t1.id()==ID_pointer)
822  {
823  #if 0
824  bool s=info.set_to_new;
825  if(adjust_object_type_rec(t1.subtype(), t2.subtype(), info))
826  {
827  link_warning(
828  info.old_symbol,
829  info.new_symbol,
830  "conflicting pointer types for variable");
831  info.set_to_new=s;
832  }
833  #else
834  link_warning(
835  info.old_symbol,
836  info.new_symbol,
837  "conflicting pointer types for variable");
838  #endif
839 
840  return false;
841  }
842  else if(t1.id()==ID_array &&
843  !adjust_object_type_rec(t1.subtype(), t2.subtype(), info))
844  {
845  // still need to compare size
846  const exprt &old_size=to_array_type(t1).size();
847  const exprt &new_size=to_array_type(t2).size();
848 
849  if((old_size.is_nil() && new_size.is_not_nil()) ||
850  (old_size.is_zero() && new_size.is_not_nil()) ||
851  info.old_symbol.is_weak)
852  {
853  info.set_to_new=true; // store new type
854  }
855  else if(new_size.is_nil() ||
856  new_size.is_zero() ||
857  info.new_symbol.is_weak)
858  {
859  // ok, we will use the old type
860  }
861  else
862  {
863  equal_exprt eq(old_size, new_size);
864 
865  if(!simplify_expr(eq, ns).is_true())
866  link_error(
867  info.old_symbol,
868  info.new_symbol,
869  "conflicting array sizes for variable");
870  }
871 
872  return false;
873  }
874  else if(t1.id()==ID_struct || t1.id()==ID_union)
875  {
876  const struct_union_typet::componentst &components1=
878 
879  const struct_union_typet::componentst &components2=
881 
882  struct_union_typet::componentst::const_iterator
883  it1=components1.begin(), it2=components2.begin();
884  for( ;
885  it1!=components1.end() && it2!=components2.end();
886  ++it1, ++it2)
887  {
888  if(it1->get_name()!=it2->get_name() ||
889  adjust_object_type_rec(it1->type(), it2->type(), info))
890  return true;
891  }
892  if(it1!=components1.end() || it2!=components2.end())
893  return true;
894 
895  return false;
896  }
897 
898  return true;
899 }
900 
902  const symbolt &old_symbol,
903  const symbolt &new_symbol,
904  bool &set_to_new)
905 {
906  const typet &old_type=follow_tags_symbols(ns, old_symbol.type);
907  const typet &new_type=follow_tags_symbols(ns, new_symbol.type);
908 
909  adjust_type_infot info(old_symbol, new_symbol);
910  bool result=adjust_object_type_rec(old_type, new_type, info);
911  set_to_new=info.set_to_new;
912 
913  return result;
914 }
915 
917  symbolt &old_symbol,
918  symbolt &new_symbol)
919 {
920  // both are variables
921 
922  if(!base_type_eq(old_symbol.type, new_symbol.type, ns))
923  {
924  bool set_to_new=false;
925  bool failed=
926  adjust_object_type(old_symbol, new_symbol, set_to_new);
927 
928  if(failed)
929  {
930  const typet &old_type=follow_tags_symbols(ns, old_symbol.type);
931 
932  // provide additional diagnostic output for
933  // struct/union/array/enum
934  if(old_type.id()==ID_struct ||
935  old_type.id()==ID_union ||
936  old_type.id()==ID_array ||
937  old_type.id()==ID_c_enum)
939  old_symbol,
940  new_symbol,
941  old_symbol.type,
942  new_symbol.type);
943 
944  link_error(
945  old_symbol,
946  new_symbol,
947  "conflicting types for variable");
948  }
949  else if(set_to_new)
950  old_symbol.type=new_symbol.type;
951 
952  object_type_updates.insert(old_symbol.name, old_symbol.symbol_expr());
953  }
954 
955  // care about initializers
956 
957  if(!new_symbol.value.is_nil() &&
958  !new_symbol.value.get_bool(ID_C_zero_initializer))
959  {
960  if(old_symbol.value.is_nil() ||
961  old_symbol.value.get_bool(ID_C_zero_initializer) ||
962  old_symbol.is_weak)
963  {
964  // new_symbol wins
965  old_symbol.value=new_symbol.value;
966  old_symbol.is_macro=new_symbol.is_macro;
967  }
968  else if(!new_symbol.is_weak)
969  {
970  // try simplifier
971  exprt tmp_old=old_symbol.value,
972  tmp_new=new_symbol.value;
973 
974  simplify(tmp_old, ns);
975  simplify(tmp_new, ns);
976 
977  if(base_type_eq(tmp_old, tmp_new, ns))
978  {
979  // ok, the same
980  }
981  else
982  {
983  warning().source_location=new_symbol.location;
984 
985  warning() << "warning: conflicting initializers for"
986  << " variable \"" << old_symbol.name << "\"\n";
987  warning() << "using old value in module "
988  << old_symbol.module << " "
989  << old_symbol.value.find_source_location() << '\n'
990  << expr_to_string(ns, old_symbol.name, tmp_old)
991  << '\n';
992  warning() << "ignoring new value in module "
993  << new_symbol.module << " "
994  << new_symbol.value.find_source_location() << '\n'
995  << expr_to_string(ns, new_symbol.name, tmp_new)
996  << eom;
997  }
998  }
999  }
1000 }
1001 
1003  symbolt &old_symbol,
1004  symbolt &new_symbol)
1005 {
1006  // see if it is a function or a variable
1007 
1008  bool is_code_old_symbol=old_symbol.type.id()==ID_code;
1009  bool is_code_new_symbol=new_symbol.type.id()==ID_code;
1010 
1011  if(is_code_old_symbol!=is_code_new_symbol)
1012  link_error(
1013  old_symbol,
1014  new_symbol,
1015  "conflicting definition for symbol");
1016 
1017  if(is_code_old_symbol)
1018  duplicate_code_symbol(old_symbol, new_symbol);
1019  else
1020  duplicate_object_symbol(old_symbol, new_symbol);
1021 
1022  // care about flags
1023 
1024  if(old_symbol.is_extern && !new_symbol.is_extern)
1025  old_symbol.location=new_symbol.location;
1026 
1027  // it's enough that one isn't extern for the final one not to be
1028  old_symbol.is_extern=old_symbol.is_extern && new_symbol.is_extern;
1029 }
1030 
1032  symbolt &old_symbol,
1033  symbolt &new_symbol)
1034 {
1035  assert(new_symbol.is_type);
1036 
1037  if(!old_symbol.is_type)
1038  link_error(
1039  old_symbol,
1040  new_symbol,
1041  "conflicting definition for symbol");
1042 
1043  if(old_symbol.type==new_symbol.type)
1044  return;
1045 
1046  if(old_symbol.type.id()==ID_incomplete_struct &&
1047  new_symbol.type.id()==ID_struct)
1048  {
1049  old_symbol.type=new_symbol.type;
1050  old_symbol.location=new_symbol.location;
1051  return;
1052  }
1053 
1054  if(old_symbol.type.id()==ID_struct &&
1055  new_symbol.type.id()==ID_incomplete_struct)
1056  {
1057  // ok, keep old
1058  return;
1059  }
1060 
1061  if(old_symbol.type.id()==ID_incomplete_union &&
1062  new_symbol.type.id()==ID_union)
1063  {
1064  old_symbol.type=new_symbol.type;
1065  old_symbol.location=new_symbol.location;
1066  return;
1067  }
1068 
1069  if(old_symbol.type.id()==ID_union &&
1070  new_symbol.type.id()==ID_incomplete_union)
1071  {
1072  // ok, keep old
1073  return;
1074  }
1075 
1076  if(old_symbol.type.id()==ID_array &&
1077  new_symbol.type.id()==ID_array &&
1078  base_type_eq(old_symbol.type.subtype(), new_symbol.type.subtype(), ns))
1079  {
1080  if(to_array_type(old_symbol.type).size().is_nil() &&
1081  to_array_type(new_symbol.type).size().is_not_nil())
1082  {
1083  to_array_type(old_symbol.type).size()=
1084  to_array_type(new_symbol.type).size();
1085  return;
1086  }
1087 
1088  if(to_array_type(new_symbol.type).size().is_nil() &&
1089  to_array_type(old_symbol.type).size().is_not_nil())
1090  {
1091  // ok, keep old
1092  return;
1093  }
1094  }
1095 
1097  old_symbol,
1098  new_symbol,
1099  old_symbol.type,
1100  new_symbol.type);
1101 
1102  link_error(
1103  old_symbol,
1104  new_symbol,
1105  "unexpected difference between type symbols");
1106 }
1107 
1109  const symbolt &old_symbol,
1110  const symbolt &new_symbol)
1111 {
1112  assert(new_symbol.is_type);
1113 
1114  if(!old_symbol.is_type)
1115  return true;
1116 
1117  if(old_symbol.type==new_symbol.type)
1118  return false;
1119 
1120  if(old_symbol.type.id()==ID_incomplete_struct &&
1121  new_symbol.type.id()==ID_struct)
1122  return false; // not different
1123 
1124  if(old_symbol.type.id()==ID_struct &&
1125  new_symbol.type.id()==ID_incomplete_struct)
1126  return false; // not different
1127 
1128  if(old_symbol.type.id()==ID_incomplete_union &&
1129  new_symbol.type.id()==ID_union)
1130  return false; // not different
1131 
1132  if(old_symbol.type.id()==ID_union &&
1133  new_symbol.type.id()==ID_incomplete_union)
1134  return false; // not different
1135 
1136  if(old_symbol.type.id()==ID_array &&
1137  new_symbol.type.id()==ID_array &&
1138  base_type_eq(old_symbol.type.subtype(), new_symbol.type.subtype(), ns))
1139  {
1140  if(to_array_type(old_symbol.type).size().is_nil() &&
1141  to_array_type(new_symbol.type).size().is_not_nil())
1142  return false; // not different
1143 
1144  if(to_array_type(new_symbol.type).size().is_nil() &&
1145  to_array_type(old_symbol.type).size().is_not_nil())
1146  return false; // not different
1147  }
1148 
1149  return true; // different
1150 }
1151 
1152 void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed)
1153 {
1154  // Any type that uses a symbol that will be renamed also
1155  // needs to be renamed, and so on, until saturation.
1156 
1157  used_byt used_by;
1158 
1160  {
1161  if(s_it->second.is_type)
1162  {
1163  // find type and array-size symbols
1164  find_symbols_sett symbols_used;
1165  find_type_and_expr_symbols(s_it->second.type, symbols_used);
1166 
1167  for(find_symbols_sett::const_iterator
1168  it=symbols_used.begin();
1169  it!=symbols_used.end();
1170  it++)
1171  {
1172  used_by[*it].insert(s_it->first);
1173  }
1174  }
1175  }
1176 
1177  std::stack<irep_idt> queue;
1178 
1179  for(id_sett::const_iterator
1180  d_it=needs_to_be_renamed.begin();
1181  d_it!=needs_to_be_renamed.end();
1182  d_it++)
1183  queue.push(*d_it);
1184 
1185  while(!queue.empty())
1186  {
1187  irep_idt id=queue.top();
1188  queue.pop();
1189 
1190  const id_sett &u=used_by[id];
1191 
1192  for(id_sett::const_iterator
1193  d_it=u.begin();
1194  d_it!=u.end();
1195  d_it++)
1196  if(needs_to_be_renamed.insert(*d_it).second)
1197  {
1198  queue.push(*d_it);
1199  #ifdef DEBUG
1200  debug() << "LINKING: needs to be renamed (dependency): "
1201  << *d_it << eom;
1202  #endif
1203  }
1204  }
1205 }
1206 
1207 void linkingt::rename_symbols(const id_sett &needs_to_be_renamed)
1208 {
1209  namespacet src_ns(src_symbol_table);
1210 
1211  for(id_sett::const_iterator
1212  it=needs_to_be_renamed.begin();
1213  it!=needs_to_be_renamed.end();
1214  it++)
1215  {
1216  symbolt &new_symbol=src_symbol_table.symbols[*it];
1217 
1218  irep_idt new_identifier;
1219 
1220  if(new_symbol.is_type)
1221  new_identifier=type_to_name(src_ns, *it, new_symbol.type);
1222  else
1223  new_identifier=rename(*it);
1224 
1225  new_symbol.name=new_identifier;
1226 
1227  #ifdef DEBUG
1228  debug() << "LINKING: renaming " << *it << " to "
1229  << new_identifier << eom;
1230  #endif
1231 
1232  if(new_symbol.is_type)
1233  rename_symbol.insert_type(*it, new_identifier);
1234  else
1235  rename_symbol.insert_expr(*it, new_identifier);
1236  }
1237 }
1238 
1240 {
1241  // First apply the renaming
1243  {
1244  // apply the renaming
1245  rename_symbol(s_it->second.type);
1246  rename_symbol(s_it->second.value);
1247  }
1248 
1249  // Move over all the non-colliding ones
1250  id_sett collisions;
1251 
1253  {
1254  // renamed?
1255  if(s_it->first!=s_it->second.name)
1256  {
1257  // new
1258  main_symbol_table.add(s_it->second);
1259  }
1260  else
1261  {
1262  symbol_tablet::symbolst::iterator
1263  m_it=main_symbol_table.symbols.find(s_it->first);
1264 
1265  if(m_it==main_symbol_table.symbols.end())
1266  {
1267  // new
1268  main_symbol_table.add(s_it->second);
1269  }
1270  else
1271  collisions.insert(s_it->first);
1272  }
1273  }
1274 
1275  // Now do the collisions
1276  for(id_sett::const_iterator
1277  i_it=collisions.begin();
1278  i_it!=collisions.end();
1279  i_it++)
1280  {
1281  symbolt &old_symbol=main_symbol_table.symbols[*i_it];
1282  symbolt &new_symbol=src_symbol_table.symbols[*i_it];
1283 
1284  if(new_symbol.is_type)
1285  duplicate_type_symbol(old_symbol, new_symbol);
1286  else
1287  duplicate_non_type_symbol(old_symbol, new_symbol);
1288  }
1289 
1290  // Apply type updates to initializers
1292  {
1293  if(!s_it->second.is_type &&
1294  !s_it->second.is_macro &&
1295  s_it->second.value.is_not_nil())
1296  object_type_updates(s_it->second.value);
1297  }
1298 }
1299 
1301 {
1302  // We do this in three phases. We first figure out which symbols need to
1303  // be renamed, and then build the renaming, and finally apply this
1304  // renaming in the second pass over the symbol table.
1305 
1306  // PHASE 1: identify symbols to be renamed
1307 
1308  id_sett needs_to_be_renamed;
1309 
1311  {
1312  symbol_tablet::symbolst::const_iterator
1313  m_it=main_symbol_table.symbols.find(s_it->first);
1314 
1315  if(m_it!=main_symbol_table.symbols.end() && // duplicate
1316  needs_renaming(m_it->second, s_it->second))
1317  {
1318  needs_to_be_renamed.insert(s_it->first);
1319  #ifdef DEBUG
1320  debug() << "LINKING: needs to be renamed: "
1321  << s_it->first << eom;
1322  #endif
1323  }
1324  }
1325 
1326  // renaming types may trigger further renaming
1327  do_type_dependencies(needs_to_be_renamed);
1328 
1329  // PHASE 2: actually rename them
1330  rename_symbols(needs_to_be_renamed);
1331 
1332  // PHASE 3: copy new symbols to main table
1333  copy_symbols();
1334 }
1335 
1336 bool linking(
1337  symbol_tablet &dest_symbol_table,
1338  symbol_tablet &new_symbol_table,
1340 {
1341  linkingt linking(
1342  dest_symbol_table, new_symbol_table, message_handler);
1343 
1344  return linking.typecheck_main();
1345 }
The type of an expression.
Definition: type.h:20
mstreamt & warning()
Definition: message.h:228
irep_idt name
The unique identifier.
Definition: symbol.h:46
mstreamt & result()
Definition: message.h:233
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
virtual void typecheck()
Definition: linking.cpp:1300
std::unordered_map< irep_idt, id_sett, irep_id_hash > used_byt
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:369
exprt & op0()
Definition: expr.h:84
ANSI-C Linking.
exprt simplify_expr(const exprt &src, const namespacet &ns)
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
bool has_ellipsis() const
Definition: std_types.h:803
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
void insert_type(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:40
const irep_idt & get_function() const
std::string as_string() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
Definition: std_types.h:240
std::vector< parametert > parameterst
Definition: std_types.h:829
void do_type_dependencies(id_sett &)
Definition: linking.cpp:1152
exprt value
Initial value of symbol.
Definition: symbol.h:40
const componentst & components() const
Definition: std_types.h:242
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1336
const memberst & members() const
Definition: std_types.h:664
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
symbol_tablet & main_symbol_table
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:389
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
std::string expr_to_string(const namespacet &ns, const irep_idt &identifier, const exprt &expr) const
Definition: linking.cpp:29
A constant literal expression.
Definition: std_expr.h:3685
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
std::string get_base_name(const std::string &in, bool strip_suffix)
cleans a filename from path and extension
void detailed_conflict_report_rec(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2, unsigned depth, exprt &conflict_path)
Definition: linking.cpp:115
bool needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:431
Extract member of struct or union.
Definition: std_expr.h:3214
std::unordered_set< irep_idt, irep_id_hash > find_symbols_sett
Definition: find_symbols.h:20
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
#define Forall_symbols(it, expr)
Definition: symbol_table.h:32
equality
Definition: std_expr.h:1082
const symbolt & new_symbol
Definition: linking_class.h:95
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
const irep_idt & id() const
Definition: irep.h:189
bool needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking_class.h:51
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
void rename_symbols(const id_sett &needs_to_be_renamed)
Definition: linking.cpp:1207
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
Definition: std_types.h:680
symbolst symbols
Definition: symbol_table.h:57
std::string type_to_name(const namespacet &ns, const irep_idt &identifier, const typet &type)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:717
const source_locationt & find_source_location() const
Definition: expr.cpp:466
virtual std::string id() const
Definition: language.h:82
source_locationt source_location
Definition: message.h:175
Operator to dereference a pointer.
Definition: std_expr.h:2701
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
const symbolt & old_symbol
Definition: linking_class.h:94
const exprt & size() const
Definition: std_types.h:915
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
bool needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1108
namespacet ns
irep_idt rename(irep_idt)
Definition: linking.cpp:407
id_sett renamed_ids
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::string type_to_string(const namespacet &ns, const irep_idt &identifier, const typet &type) const
Definition: linking.cpp:37
static const typet & follow_tags_symbols(const namespacet &ns, const typet &type)
Definition: linking.cpp:45
replace_symbolt object_type_updates
Definition: linking_class.h:38
Pointer Logic.
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:445
const source_locationt & source_location() const
Definition: type.h:95
const irep_idt & display_name() const
Definition: symbol.h:60
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
Definition: linking.cpp:747
bool is_extern
Definition: symbol.h:71
Unbounded, signed integers.
Definition: std_types.h:69
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
mstreamt & debug()
Definition: message.h:253
API to type classes.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:536
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:573
symbol_tablet & src_symbol_table
Base class for all expressions.
Definition: expr.h:46
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1002
The union type.
Definition: std_types.h:424
const parameterst & parameters() const
Definition: std_types.h:841
ANSI-C Linking.
void copy_symbols()
Definition: linking.cpp:1239
rename_symbolt rename_symbol
Definition: linking_class.h:37
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:916
bool is_file_local
Definition: symbol.h:71
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void make_nil()
Definition: irep.h:243
const std::string & id_string() const
Definition: irep.h:192
mstreamt & error()
Definition: message.h:223
bool is_weak
Definition: symbol.h:71
bool is_zero() const
Definition: expr.cpp:236
void insert(const irep_idt &identifier, const exprt &expr)
std::string type_to_string_verbose(const namespacet &ns, const symbolt &symbol, const typet &type) const
Definition: linking.cpp:61
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
Definition: linking.cpp:901
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
bool is_type
Definition: symbol.h:66
void duplicate_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1031
Base Type Computation.
const typet & subtype() const
Definition: type.h:31
std::unordered_set< irep_idt, irep_id_hash > id_sett
Definition: linking_class.h:41
bool get_inlined() const
Definition: std_types.h:851
message_handlert * message_handler
Definition: message.h:259
std::vector< c_enum_membert > memberst
Definition: std_types.h:662
bool empty() const
Definition: dstring.h:61
const typet & return_type() const
Definition: std_types.h:831
bool is_macro
Definition: symbol.h:66
bool simplify(exprt &expr, const namespacet &ns)
array index operator
Definition: std_expr.h:1170