cprover
config.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "config.h"
10 
11 #include <cstdlib>
12 
13 #include "namespace.h"
14 #include "symbol_table.h"
15 #include "arith_tools.h"
16 #include "cmdline.h"
17 #include "simplify_expr.h"
18 #include "std_expr.h"
19 #include "cprover_prefix.h"
20 #include "string2int.h"
21 #include "string_utils.h"
22 
24 
26 {
27  set_LP32();
28 }
29 
31 {
32  set_ILP32();
33 }
34 
36 {
37  #ifdef _WIN32
38  set_LLP64();
39  #else
40  set_LP64();
41  #endif
42 }
43 
46 {
47  bool_width=1*8;
48  int_width=4*8;
49  long_int_width=8*8;
50  char_width=1*8;
51  short_int_width=2*8;
52  long_long_int_width=8*8;
53  pointer_width=8*8;
54  single_width=4*8;
55  double_width=8*8;
56  long_double_width=16*8;
57  char_is_unsigned=false;
58  wchar_t_is_unsigned=false;
59  wchar_t_width=4*8;
60  alignment=1;
61  memory_operand_size=int_width/8;
62 }
63 
65 // TODO: find the alignment restrictions (per type) of the different
66 // architectures (currently: sizeof=alignedof)
67 // TODO: implement the __attribute__((__aligned__(val)))
68 
70 {
71  bool_width=1*8;
72  int_width=8*8;
73  long_int_width=8*8;
74  char_width=1*8;
75  short_int_width=2*8;
76  long_long_int_width=8*8;
77  pointer_width=8*8;
78  single_width=4*8;
79  double_width=8*8;
80  long_double_width=8*8;
81  char_is_unsigned=false;
82  wchar_t_is_unsigned=false;
83  wchar_t_width=4*8;
84  alignment=1;
85  memory_operand_size=int_width/8;
86 }
87 
90 {
91  bool_width=1*8;
92  int_width=4*8;
93  long_int_width=4*8;
94  char_width=1*8;
95  short_int_width=2*8;
96  long_long_int_width=8*8;
97  pointer_width=8*8;
98  single_width=4*8;
99  double_width=8*8;
100  long_double_width=8*8;
101  char_is_unsigned=false;
102  wchar_t_is_unsigned=false;
103  wchar_t_width=4*8;
104  alignment=1;
105  memory_operand_size=int_width/8;
106 }
107 
110 {
111  bool_width=1*8;
112  int_width=4*8;
113  long_int_width=4*8;
114  char_width=1*8;
115  short_int_width=2*8;
116  long_long_int_width=8*8;
117  pointer_width=4*8;
118  single_width=4*8;
119  double_width=8*8;
120  long_double_width=12*8; // really 96 bits on GCC
121  char_is_unsigned=false;
122  wchar_t_is_unsigned=false;
123  wchar_t_width=4*8;
124  alignment=1;
125  memory_operand_size=int_width/8;
126 }
127 
130 {
131  bool_width=1*8;
132  int_width=2*8;
133  long_int_width=4*8;
134  char_width=1*8;
135  short_int_width=2*8;
136  long_long_int_width=8*8;
137  pointer_width=4*8;
138  single_width=4*8;
139  double_width=8*8;
140  long_double_width=8*8;
141  char_is_unsigned=false;
142  wchar_t_is_unsigned=false;
143  wchar_t_width=4*8;
144  alignment=1;
145  memory_operand_size=int_width/8;
146 }
147 
149 {
150  set_ILP32();
151  endianness=endiannesst::IS_LITTLE_ENDIAN;
152  char_is_unsigned=false;
153  NULL_is_zero=true;
154 
155  switch(mode)
156  {
157  case flavourt::GCC:
158  case flavourt::APPLE:
159  defines.push_back("i386");
160  defines.push_back("__i386");
161  defines.push_back("__i386__");
162  if(mode==flavourt::APPLE)
163  defines.push_back("__LITTLE_ENDIAN__");
164  break;
165 
166  case flavourt::VISUAL_STUDIO:
167  defines.push_back("_M_IX86");
168  break;
169 
170  case flavourt::CODEWARRIOR:
171  case flavourt::ARM:
172  case flavourt::ANSI:
173  break;
174 
175  case flavourt::NONE:
176  UNREACHABLE;
177  }
178 }
179 
181 {
182  set_LP64();
183  endianness=endiannesst::IS_LITTLE_ENDIAN;
184  long_double_width=16*8;
185  char_is_unsigned=false;
186  NULL_is_zero=true;
187 
188  switch(mode)
189  {
190  case flavourt::GCC:
191  case flavourt::APPLE:
192  defines.push_back("__LP64__");
193  defines.push_back("__x86_64");
194  defines.push_back("__x86_64__");
195  defines.push_back("_LP64");
196  defines.push_back("__amd64__");
197  defines.push_back("__amd64");
198  if(mode==flavourt::APPLE)
199  defines.push_back("__LITTLE_ENDIAN__");
200  break;
201 
202  case flavourt::VISUAL_STUDIO:
203  defines.push_back("_M_X64");
204  defines.push_back("_M_AMD64");
205  break;
206 
207  case flavourt::CODEWARRIOR:
208  case flavourt::ARM:
209  case flavourt::ANSI:
210  break;
211 
212  case flavourt::NONE:
213  UNREACHABLE;
214  }
215 }
216 
218 {
219  if(subarch=="powerpc")
220  set_ILP32();
221  else // ppc64 or ppc64le
222  set_LP64();
223 
224  if(subarch=="ppc64le")
225  endianness=endiannesst::IS_LITTLE_ENDIAN;
226  else
227  endianness=endiannesst::IS_BIG_ENDIAN;
228 
229  long_double_width=16*8;
230  char_is_unsigned=true;
231  NULL_is_zero=true;
232 
233  switch(mode)
234  {
235  case flavourt::GCC:
236  case flavourt::APPLE:
237  defines.push_back("__powerpc");
238  defines.push_back("__powerpc__");
239  defines.push_back("__POWERPC__");
240  defines.push_back("__ppc__");
241 
242  if(mode==flavourt::APPLE)
243  defines.push_back("__BIG_ENDIAN__");
244 
245  if(subarch!="powerpc")
246  {
247  defines.push_back("__powerpc64");
248  defines.push_back("__powerpc64__");
249  defines.push_back("__PPC64__");
250  defines.push_back("__ppc64__");
251  if(subarch=="ppc64le")
252  {
253  defines.push_back("_CALL_ELF=2");
254  defines.push_back("__LITTLE_ENDIAN__");
255  }
256  else
257  {
258  defines.push_back("_CALL_ELF=1");
259  defines.push_back("__BIG_ENDIAN__");
260  }
261  }
262  break;
263 
264  case flavourt::VISUAL_STUDIO:
265  defines.push_back("_M_PPC");
266  break;
267 
268  case flavourt::CODEWARRIOR:
269  case flavourt::ARM:
270  case flavourt::ANSI:
271  break;
272 
273  case flavourt::NONE:
274  UNREACHABLE;
275  }
276 }
277 
279 {
280  if(subarch=="arm64")
281  {
282  set_LP64();
283  long_double_width=16*8;
284  }
285  else
286  {
287  set_ILP32();
288  long_double_width=8*8;
289  }
290 
291  endianness=endiannesst::IS_LITTLE_ENDIAN;
292  char_is_unsigned=true;
293  NULL_is_zero=true;
294 
295  switch(mode)
296  {
297  case flavourt::GCC:
298  case flavourt::APPLE:
299  if(subarch=="arm64")
300  defines.push_back("__aarch64__");
301  else
302  defines.push_back("__arm__");
303  if(subarch=="armhf")
304  defines.push_back("__ARM_PCS_VFP");
305  break;
306 
307  case flavourt::VISUAL_STUDIO:
308  defines.push_back("_M_ARM");
309  break;
310 
311  case flavourt::CODEWARRIOR:
312  case flavourt::ARM:
313  case flavourt::ANSI:
314  break;
315 
316  case flavourt::NONE:
317  UNREACHABLE;
318  }
319 }
320 
322 {
323  set_LP64();
324  endianness=endiannesst::IS_LITTLE_ENDIAN;
325  long_double_width=16*8;
326  char_is_unsigned=false;
327  NULL_is_zero=true;
328 
329  switch(mode)
330  {
331  case flavourt::GCC:
332  defines.push_back("__alpha__");
333  break;
334 
335  case flavourt::VISUAL_STUDIO:
336  defines.push_back("_M_ALPHA");
337  break;
338 
339  case flavourt::APPLE:
340  case flavourt::CODEWARRIOR:
341  case flavourt::ARM:
342  case flavourt::ANSI:
343  break;
344 
345  case flavourt::NONE:
346  UNREACHABLE;
347  }
348 }
349 
351 {
352  if(subarch=="mipsel" ||
353  subarch=="mips" ||
354  subarch=="mipsn32el" ||
355  subarch=="mipsn32")
356  {
357  set_ILP32();
358  long_double_width=8*8;
359  }
360  else
361  {
362  set_LP64();
363  long_double_width=16*8;
364  }
365 
366  if(subarch=="mipsel" ||
367  subarch=="mipsn32el" ||
368  subarch=="mips64el")
369  endianness=endiannesst::IS_LITTLE_ENDIAN;
370  else
371  endianness=endiannesst::IS_BIG_ENDIAN;
372 
373  char_is_unsigned=false;
374  NULL_is_zero=true;
375 
376  switch(mode)
377  {
378  case flavourt::GCC:
379  defines.push_back("__mips__");
380  defines.push_back("mips");
381  defines.push_back(
382  "_MIPS_SZPTR="+std::to_string(config.ansi_c.pointer_width));
383  break;
384 
385  case flavourt::VISUAL_STUDIO:
386  UNREACHABLE; // not supported by Visual Studio
387  break;
388 
389  case flavourt::APPLE:
390  case flavourt::CODEWARRIOR:
391  case flavourt::ARM:
392  case flavourt::ANSI:
393  break;
394 
395  case flavourt::NONE:
396  UNREACHABLE;
397  }
398 }
399 
401 {
402  set_ILP32();
403  endianness=endiannesst::IS_BIG_ENDIAN;
404  long_double_width=16*8;
405  char_is_unsigned=true;
406  NULL_is_zero=true;
407 
408  switch(mode)
409  {
410  case flavourt::GCC:
411  defines.push_back("__s390__");
412  break;
413 
414  case flavourt::VISUAL_STUDIO:
415  UNREACHABLE; // not supported by Visual Studio
416  break;
417 
418  case flavourt::APPLE:
419  case flavourt::CODEWARRIOR:
420  case flavourt::ARM:
421  case flavourt::ANSI:
422  break;
423 
424  case flavourt::NONE:
425  UNREACHABLE;
426  }
427 }
428 
430 {
431  set_LP64();
432  endianness=endiannesst::IS_BIG_ENDIAN;
433  char_is_unsigned=true;
434  NULL_is_zero=true;
435 
436  switch(mode)
437  {
438  case flavourt::GCC:
439  defines.push_back("__s390x__");
440  break;
441 
442  case flavourt::VISUAL_STUDIO:
443  UNREACHABLE; // not supported by Visual Studio
444  break;
445 
446  case flavourt::APPLE:
447  case flavourt::CODEWARRIOR:
448  case flavourt::ARM:
449  case flavourt::ANSI:
450  break;
451 
452  case flavourt::NONE:
453  UNREACHABLE;
454  }
455 }
456 
458 {
459  if(subarch=="sparc64")
460  {
461  set_LP64();
462  long_double_width=16*8;
463  }
464  else
465  {
466  set_ILP32();
467  long_double_width=16*8;
468  }
469 
470  endianness=endiannesst::IS_BIG_ENDIAN;
471  char_is_unsigned=false;
472  NULL_is_zero=true;
473 
474  switch(mode)
475  {
476  case flavourt::GCC:
477  defines.push_back("__sparc__");
478  if(subarch=="sparc64")
479  defines.push_back("__arch64__");
480  break;
481 
482  case flavourt::VISUAL_STUDIO:
483  UNREACHABLE; // not supported by Visual Studio
484  break;
485 
486  case flavourt::APPLE:
487  case flavourt::CODEWARRIOR:
488  case flavourt::ARM:
489  case flavourt::ANSI:
490  break;
491 
492  case flavourt::NONE:
493  UNREACHABLE;
494  }
495 }
496 
498 {
499  set_LP64();
500  long_double_width=16*8;
501  endianness=endiannesst::IS_LITTLE_ENDIAN;
502  char_is_unsigned=false;
503  NULL_is_zero=true;
504 
505  switch(mode)
506  {
507  case flavourt::GCC:
508  defines.push_back("__ia64__");
509  defines.push_back("_IA64");
510  defines.push_back("__IA64__");
511  break;
512 
513  case flavourt::VISUAL_STUDIO:
514  defines.push_back("_M_IA64");
515  break;
516 
517  case flavourt::APPLE:
518  case flavourt::CODEWARRIOR:
519  case flavourt::ARM:
520  case flavourt::ANSI:
521  break;
522 
523  case flavourt::NONE:
524  UNREACHABLE;
525  }
526 }
527 
529 {
530  // This is a variant of x86_64 that has
531  // 32-bit long int and 32-bit pointers.
532  set_ILP32();
533  long_double_width=16*8; // different from i386
534  endianness=endiannesst::IS_LITTLE_ENDIAN;
535  char_is_unsigned=false;
536  NULL_is_zero=true;
537 
538  switch(mode)
539  {
540  case flavourt::GCC:
541  defines.push_back("__ILP32__");
542  defines.push_back("__x86_64");
543  defines.push_back("__x86_64__");
544  defines.push_back("__amd64__");
545  defines.push_back("__amd64");
546  break;
547 
548  case flavourt::VISUAL_STUDIO:
549  UNREACHABLE; // not supported by Visual Studio
550  break;
551 
552  case flavourt::APPLE:
553  case flavourt::CODEWARRIOR:
554  case flavourt::ARM:
555  case flavourt::ANSI:
556  break;
557 
558  case flavourt::NONE:
559  UNREACHABLE;
560  }
561 }
562 
566 {
567  // The Renesas V850 is a 32-bit microprocessor used in
568  // many automotive applications. This spec is written from the
569  // architecture manual rather than having access to a running
570  // system. Thus some assumptions have been made.
571 
572  set_ILP32();
573 
574  // Technically, the V850's don't have floating-point at all.
575  // However, the RH850, aimed at automotive has both 32-bit and
576  // 64-bit IEEE-754 float.
577  double_width=8*8;
578  long_double_width=8*8;
579  endianness=endiannesst::IS_LITTLE_ENDIAN;
580 
581  // Without information about the compiler and RTOS, these are guesses
582  char_is_unsigned=false;
583  NULL_is_zero=true;
584 
585  // No preprocessor definitions due to lack of information
586 }
587 
589 {
590  set_ILP32();
591  long_double_width=8*8; // different from i386
592  endianness=endiannesst::IS_BIG_ENDIAN;
593  char_is_unsigned=false;
594  NULL_is_zero=true;
595 
596  switch(mode)
597  {
598  case flavourt::GCC:
599  defines.push_back("__hppa__");
600  break;
601 
602  case flavourt::VISUAL_STUDIO:
603  UNREACHABLE; // not supported by Visual Studio
604  break;
605 
606  case flavourt::APPLE:
607  case flavourt::CODEWARRIOR:
608  case flavourt::ARM:
609  case flavourt::ANSI:
610  break;
611 
612  case flavourt::NONE:
613  UNREACHABLE;
614  }
615 }
616 
618 {
619  set_ILP32();
620  long_double_width=8*8; // different from i386
621  endianness=endiannesst::IS_LITTLE_ENDIAN;
622  char_is_unsigned=false;
623  NULL_is_zero=true;
624 
625  switch(mode)
626  {
627  case flavourt::GCC:
628  defines.push_back("__sh__");
629  defines.push_back("__SH4__");
630  break;
631 
632  case flavourt::VISUAL_STUDIO:
633  UNREACHABLE; // not supported by Visual Studio
634  break;
635 
636  case flavourt::APPLE:
637  case flavourt::CODEWARRIOR:
638  case flavourt::ARM:
639  case flavourt::ANSI:
640  break;
641 
642  case flavourt::NONE:
643  UNREACHABLE;
644  }
645 }
646 
648 {
649  #if defined(__APPLE__)
650  // By default, clang on the Mac builds C code in GNU C11
651  return c_standardt::C11;
652  #elif defined(__FreeBSD__)
653  // By default, clang on FreeBSD builds C code in GNU C99
654  return c_standardt::C99;
655  #else
656  // By default, gcc 5.4 or higher use gnu11; older versions use gnu89
657  return c_standardt::C11;
658  #endif
659 }
660 
662 {
663  // g++ 6.3 uses gnu++14
664  // g++ 5.4 uses gnu++98
665  // clang 6.0 uses c++14
666  #if defined _WIN32
667  return cpp_standardt::CPP14;
668  #else
669  return cpp_standardt::CPP98;
670  #endif
671 }
672 
673 void configt::set_arch(const irep_idt &arch)
674 {
675  ansi_c.arch=arch;
676 
677  if(arch=="none")
678  {
679  // the architecture for people who can't commit
682  ansi_c.NULL_is_zero=false;
683 
684  if(sizeof(long int)==8)
685  ansi_c.set_64();
686  else
687  ansi_c.set_32();
688  }
689  else if(arch=="alpha")
691  else if(arch=="arm64" ||
692  arch=="armel" ||
693  arch=="armhf" ||
694  arch=="arm")
696  else if(arch=="mips64el" ||
697  arch=="mipsn32el" ||
698  arch=="mipsel" ||
699  arch=="mips64" ||
700  arch=="mipsn32" ||
701  arch=="mips")
703  else if(arch=="powerpc" ||
704  arch=="ppc64" ||
705  arch=="ppc64le")
707  else if(arch=="sparc" ||
708  arch=="sparc64")
710  else if(arch=="ia64")
712  else if(arch=="s390x")
714  else if(arch=="s390")
716  else if(arch=="x32")
718  else if(arch=="v850")
720  else if(arch=="hppa")
722  else if(arch=="sh4")
724  else if(arch=="x86_64")
726  else if(arch=="i386")
728  else
729  {
730  // We run on something new and unknown.
731  // We verify for i386 instead.
733  ansi_c.arch="i386";
734  }
735 }
736 
737 bool configt::set(const cmdlinet &cmdline)
738 {
739  // defaults -- we match the architecture we have ourselves
740 
742 
744  // This will allow us to override by language defaults later.
746 
748  ansi_c.for_has_scope=true; // C99 or later
753  ansi_c.arch="none";
755  // NOLINTNEXTLINE(readability/casting)
756  ansi_c.NULL_is_zero=reinterpret_cast<size_t>(nullptr)==0;
757 
758  // Default is ROUND_TO_EVEN, justified by C99:
759  // 1 At program startup the floating-point environment is initialized as
760  // prescribed by IEC 60559:
761  // - All floating-point exception status flags are cleared.
762  // - The rounding direction mode is rounding to nearest.
764 
765  if(cmdline.isset("function"))
766  main=cmdline.get_value("function");
767 
768  if(cmdline.isset('D'))
769  ansi_c.defines=cmdline.get_values('D');
770 
771  if(cmdline.isset('I'))
772  ansi_c.include_paths=cmdline.get_values('I');
773 
774  if(cmdline.isset("classpath"))
775  {
776  // Specifying -classpath or -cp overrides any setting of the
777  // CLASSPATH environment variable.
778  set_classpath(cmdline.get_value("classpath"));
779  }
780  else if(cmdline.isset("cp"))
781  {
782  // Specifying -classpath or -cp overrides any setting of the
783  // CLASSPATH environment variable.
784  set_classpath(cmdline.get_value("cp"));
785  }
786  else
787  {
788  // environment variable set?
789  const char *CLASSPATH=getenv("CLASSPATH");
790  if(CLASSPATH!=nullptr)
791  set_classpath(CLASSPATH);
792  else
793  set_classpath("."); // default
794  }
795 
796  if(cmdline.isset("main-class"))
797  java.main_class=cmdline.get_value("main-class");
798 
799  if(cmdline.isset("include"))
800  ansi_c.include_files=cmdline.get_values("include");
801 
802  // the default architecture is the one we run on
803  irep_idt this_arch=this_architecture();
804  irep_idt arch=this_arch;
805 
806  // let's pick an OS now
807  // the default is the one we run on
809  irep_idt os=this_os;
810 
811  if(cmdline.isset("i386-linux"))
812  {
813  os="linux";
814  arch="i386";
815  }
816  else if(cmdline.isset("i386-win32") ||
817  cmdline.isset("win32"))
818  {
819  os="windows";
820  arch="i386";
821  }
822  else if(cmdline.isset("winx64"))
823  {
824  os="windows";
825  arch="x86_64";
826  }
827  else if(cmdline.isset("i386-macos"))
828  {
829  os="macos";
830  arch="i386";
831  }
832  else if(cmdline.isset("ppc-macos"))
833  {
834  arch="powerpc";
835  os="macos";
836  }
837 
838  if(cmdline.isset("arch"))
839  {
840  arch=cmdline.get_value("arch");
841  }
842 
843  if(cmdline.isset("os"))
844  {
845  os=cmdline.get_value("os");
846  }
847 
848  if(os=="windows")
849  {
850  // Cygwin uses GCC throughout, use i386-linux
851  // MinGW needs --win32 --gcc
854 
855  if(cmdline.isset("gcc"))
856  {
857  // There are gcc versions that target Windows (MinGW for example),
858  // and we support that.
861 
862  // enable Cygwin
863  #ifdef _WIN32
864  ansi_c.defines.push_back("__CYGWIN__");
865  #endif
866 
867  // MinGW has extra defines
868  ansi_c.defines.push_back("__int64=long long");
869  }
870  else
871  {
872  // On Windows, our default is Visual Studio.
873  // On FreeBSD, it's clang.
874  // On anything else, it's GCC as the preprocessor,
875  // but we recognize the Visual Studio language,
876  // which is somewhat inconsistent.
877  #ifdef _WIN32
880  #elif __FreeBSD__
883  #else
886  #endif
887  }
888  }
889  else if(os=="macos")
890  {
895  }
896  else if(os=="linux" || os=="solaris")
897  {
902  }
903  else if(os=="freebsd")
904  {
909  }
910  else
911  {
912  // give up, but use reasonable defaults
917  }
918 
920  ansi_c.Float128_type = true;
921 
922  set_arch(arch);
923 
924  if(os=="windows")
925  {
926  // note that sizeof(void *)==8, but sizeof(long)==4!
927  if(arch=="x86_64")
928  ansi_c.set_LLP64();
929 
930  // On Windows, wchar_t is unsigned 16 bit, regardless
931  // of the compiler used.
932  ansi_c.wchar_t_width=2*8;
934 
935  // long double is the same as double in Visual Studio,
936  // but it's 16 bytes with GCC with the 64-bit target.
937  if(arch=="x64_64" && cmdline.isset("gcc"))
939  else
941  }
942 
943  // Let's check some of the type widths in case we run
944  // the same architecture and OS that we are verifying for.
945  if(arch==this_arch && os==this_os)
946  {
947  assert(ansi_c.int_width==sizeof(int)*8);
948  assert(ansi_c.long_int_width==sizeof(long)*8);
949  assert(ansi_c.bool_width==sizeof(bool)*8);
950  assert(ansi_c.char_width==sizeof(char)*8);
951  assert(ansi_c.short_int_width==sizeof(short)*8);
952  assert(ansi_c.long_long_int_width==sizeof(long long)*8);
953  assert(ansi_c.pointer_width==sizeof(void *)*8);
954  assert(ansi_c.single_width==sizeof(float)*8);
955  assert(ansi_c.double_width==sizeof(double)*8);
956  assert(ansi_c.char_is_unsigned==(static_cast<char>(255)==255));
957 
958  #ifndef _WIN32
959  // On Windows, long double width varies by compiler
960  assert(ansi_c.long_double_width==sizeof(long double)*8);
961  #endif
962  }
963 
964  // the following allows overriding the defaults
965 
966  if(cmdline.isset("16"))
967  ansi_c.set_16();
968 
969  if(cmdline.isset("32"))
970  ansi_c.set_32();
971 
972  if(cmdline.isset("64"))
973  ansi_c.set_64();
974 
975  if(cmdline.isset("LP64"))
976  ansi_c.set_LP64(); // int=32, long=64, pointer=64
977 
978  if(cmdline.isset("ILP64"))
979  ansi_c.set_ILP64(); // int=64, long=64, pointer=64
980 
981  if(cmdline.isset("LLP64"))
982  ansi_c.set_LLP64(); // int=32, long=32, pointer=64
983 
984  if(cmdline.isset("ILP32"))
985  ansi_c.set_ILP32(); // int=32, long=32, pointer=32
986 
987  if(cmdline.isset("LP32"))
988  ansi_c.set_LP32(); // int=16, long=32, pointer=32
989 
990  if(cmdline.isset("string-abstraction"))
992  else
994 
995  if(cmdline.isset("no-library"))
997 
998  if(cmdline.isset("little-endian"))
1000 
1001  if(cmdline.isset("big-endian"))
1003 
1004  if(cmdline.isset("little-endian") &&
1005  cmdline.isset("big-endian"))
1006  return true;
1007 
1008  if(cmdline.isset("unsigned-char"))
1009  ansi_c.char_is_unsigned=true;
1010 
1011  if(cmdline.isset("round-to-even") ||
1012  cmdline.isset("round-to-nearest"))
1014 
1015  if(cmdline.isset("round-to-plus-inf"))
1017 
1018  if(cmdline.isset("round-to-minus-inf"))
1020 
1021  if(cmdline.isset("round-to-zero"))
1023 
1024  if(cmdline.isset("object-bits"))
1025  {
1027  unsafe_string2unsigned(cmdline.get_value("object-bits"));
1029 
1030  if(!(0<bv_encoding.object_bits &&
1032  {
1033  throw "object-bits must be positive and less than the pointer width ("+
1035  }
1036  }
1037 
1038  return false;
1039 }
1040 
1042 {
1043  switch(os)
1044  {
1045  case ost::OS_LINUX: return "linux";
1046  case ost::OS_MACOS: return "macos";
1047  case ost::OS_WIN: return "win";
1048  default: return "none";
1049  }
1050 }
1051 
1053 {
1054  if(os=="linux")
1055  return ost::OS_LINUX;
1056  else if(os=="macos")
1057  return ost::OS_MACOS;
1058  else if(os=="win")
1059  return ost::OS_WIN;
1060  else
1061  return ost::NO_OS;
1062 }
1063 
1065  const namespacet &ns,
1066  const std::string &what)
1067 {
1068  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1069  const symbolt *symbol;
1070 
1071  if(ns.lookup(id, symbol))
1072  throw "failed to find "+id2string(id);
1073 
1074  const exprt &tmp=symbol->value;
1075 
1076  if(tmp.id()!=ID_address_of ||
1077  tmp.operands().size()!=1 ||
1078  tmp.op0().id()!=ID_index ||
1079  tmp.op0().operands().size()!=2 ||
1080  tmp.op0().op0().id()!=ID_string_constant)
1081  {
1082  throw
1083  "symbol table configuration entry `"+id2string(id)+
1084  "' is not a string constant";
1085  }
1086 
1087  return tmp.op0().op0().get(ID_value);
1088 }
1089 
1090 static unsigned unsigned_from_ns(
1091  const namespacet &ns,
1092  const std::string &what)
1093 {
1094  const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1095  const symbolt *symbol;
1096 
1097  if(ns.lookup(id, symbol))
1098  throw "failed to find "+id2string(id);
1099 
1100  exprt tmp=symbol->value;
1101  simplify(tmp, ns);
1102 
1103  if(tmp.id()!=ID_constant)
1104  throw
1105  "symbol table configuration entry `"+id2string(id)+"' is not a constant";
1106 
1107  mp_integer int_value;
1108 
1109  if(to_integer(to_constant_expr(tmp), int_value))
1110  throw
1111  "failed to convert symbol table configuration entry `"+id2string(id)+"'";
1112 
1113  return integer2unsigned(int_value);
1114 }
1115 
1117  const symbol_tablet &symbol_table)
1118 {
1119  // maybe not compiled from C/C++
1120  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1121  symbol_table.symbols.end())
1122  return;
1123 
1124  namespacet ns(symbol_table);
1125 
1126  // clear defines
1127  ansi_c.defines.clear();
1128 
1129  // first set architecture to get some defaults
1130  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1131  symbol_table.symbols.end())
1133  else
1134  set_arch(string_from_ns(ns, "arch"));
1135 
1136  ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1137  ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1138  ansi_c.bool_width=1*8;
1139  ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1140  ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1141  ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1142  ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1143  ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1144  ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1145  ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1146  ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1147 
1148  ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1149  ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1150  // for_has_scope, single_precision_constant, rounding_mode,
1151  // ts_18661_3_Floatn_types are not architectural features,
1152  // and thus not stored in namespace
1153 
1154  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1155 
1156  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1157 
1159 
1160  if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1161  symbol_table.symbols.end())
1163  else
1165 
1166  // NULL_is_zero=from_ns("NULL_is_zero");
1167  ansi_c.NULL_is_zero=true;
1168 
1169  // mode, preprocessor (and all preprocessor command line options),
1170  // lib, string_abstraction not stored in namespace
1171 
1172  set_object_bits_from_symbol_table(symbol_table);
1173 }
1174 
1178  const symbol_tablet &symbol_table)
1179 {
1180  // has been overridden by command line option,
1181  // thus do not apply language defaults
1183  return;
1184 
1185  // set object_bits according to entry point language
1186  if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
1187  {
1188  const symbolt &entry_point_symbol=*maybe_symbol;
1189 
1190  if(entry_point_symbol.mode==ID_java)
1192  else if(entry_point_symbol.mode==ID_C)
1194  else if(entry_point_symbol.mode==ID_cpp)
1198  "object_bits should fit into pointer width");
1199  }
1200 }
1201 
1203 {
1204  return "Running with "+std::to_string(bv_encoding.object_bits)+
1205  " object bits, "+
1207  " offset bits ("+
1208  (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
1209  ")";
1210 }
1211 
1213 {
1214  irep_idt this_arch;
1215 
1216  // following http://wiki.debian.org/ArchitectureSpecificsMemo
1217 
1218  #ifdef __alpha__
1219  this_arch="alpha";
1220  #elif __armel__
1221  this_arch="armel";
1222  #elif __aarch64__
1223  this_arch="arm64";
1224  #elif __arm__
1225  #ifdef __ARM_PCS_VFP
1226  this_arch="armhf"; // variant of arm with hard float
1227  #else
1228  this_arch="arm";
1229  #endif
1230  #elif __mipsel__
1231  #if _MIPS_SIM==_ABIO32
1232  this_arch="mipsel";
1233  #elif _MIPS_SIM==_ABIN32
1234  this_arch="mipsn32el";
1235  #else
1236  this_arch="mips64el";
1237  #endif
1238  #elif __mips__
1239  #if _MIPS_SIM==_ABIO32
1240  this_arch="mips";
1241  #elif _MIPS_SIM==_ABIN32
1242  this_arch="mipsn32";
1243  #else
1244  this_arch="mips64";
1245  #endif
1246  #elif __powerpc__
1247  #if defined(__ppc64__) || defined(__PPC64__) || \
1248  defined(__powerpc64__) || defined(__POWERPC64__)
1249  #ifdef __LITTLE_ENDIAN__
1250  this_arch="ppc64le";
1251  #else
1252  this_arch="ppc64";
1253  #endif
1254  #else
1255  this_arch="powerpc";
1256  #endif
1257  #elif __sparc__
1258  #ifdef __arch64__
1259  this_arch="sparc64";
1260  #else
1261  this_arch="sparc";
1262  #endif
1263  #elif __ia64__
1264  this_arch="ia64";
1265  #elif __s390x__
1266  this_arch="s390x";
1267  #elif __s390__
1268  this_arch="s390";
1269  #elif __x86_64__
1270  #ifdef __ILP32__
1271  this_arch="x32"; // variant of x86_64 with 32-bit pointers
1272  #else
1273  this_arch="x86_64";
1274  #endif
1275  #elif __i386__
1276  this_arch="i386";
1277  #elif _WIN64
1278  this_arch="x86_64";
1279  #elif _WIN32
1280  this_arch="i386";
1281  #elif __hppa__
1282  this_arch="hppa";
1283  #elif __sh__
1284  this_arch="sh4";
1285  #else
1286  // something new and unknown!
1287  this_arch="unknown";
1288  #endif
1289 
1290  return this_arch;
1291 }
1292 
1293 void configt::set_classpath(const std::string &cp)
1294 {
1295 // These are separated by colons on Unix, and semicolons on
1296 // Windows.
1297 #ifdef _WIN32
1298  const char cp_separator = ';';
1299 #else
1300  const char cp_separator = ':';
1301 #endif
1302 
1303  std::vector<std::string> class_path;
1304  split_string(cp, cp_separator, class_path);
1305  java.classpath.insert(
1306  java.classpath.end(), class_path.begin(), class_path.end());
1307 }
1308 
1310 {
1311  irep_idt this_os;
1312 
1313  #ifdef _WIN32
1314  this_os="windows";
1315  #elif __APPLE__
1316  this_os="macos";
1317  #elif __FreeBSD__
1318  this_os="freebsd";
1319  #elif __linux__
1320  this_os="linux";
1321  #elif __SVR4
1322  this_os="solaris";
1323  #else
1324  this_os="unknown";
1325  #endif
1326 
1327  return this_os;
1328 }
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:278
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:110
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:129
struct configt::ansi_ct ansi_c
BigInt mp_integer
Definition: mp_arith.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:217
Globally accessible architectural configuration.
Definition: config.h:24
exprt & op0()
Definition: expr.h:72
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:52
void set_classpath(const std::string &cp)
Definition: config.cpp:1293
std::size_t alignment
Definition: config.h:69
std::string object_bits_info()
Definition: config.cpp:1202
static std::string os_to_string(ost)
Definition: config.cpp:1041
std::size_t single_width
Definition: config.h:37
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
bool single_precision_constant
Definition: config.h:47
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition: config.cpp:565
endiannesst endianness
Definition: config.h:76
std::list< std::string > defines
Definition: config.h:112
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1064
exprt value
Initial value of symbol.
Definition: symbol.h:37
std::string get_value(char option) const
Definition: cmdline.cpp:45
bool NULL_is_zero
Definition: config.h:87
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:45
std::size_t double_width
Definition: config.h:38
void set_arch_spec_ia64()
Definition: config.cpp:497
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
configt config
Definition: config.cpp:23
std::size_t char_width
Definition: config.h:33
static const std::size_t default_object_bits
Definition: config.h:159
void set_16()
Definition: config.cpp:25
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:350
static const std::size_t default_object_bits
Definition: config.h:136
struct configt::bv_encodingt bv_encoding
preprocessort preprocessor
Definition: config.h:110
bool set(const cmdlinet &cmdline)
Definition: config.cpp:737
const irep_idt & id() const
Definition: irep.h:189
std::list< std::string > include_files
Definition: config.h:116
classpatht classpath
Definition: config.h:147
std::size_t long_long_int_width
Definition: config.h:35
virtual bool isset(char option) const
Definition: cmdline.cpp:27
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:457
flavourt mode
Definition: config.h:106
void set_arch_spec_x86_64()
Definition: config.cpp:180
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1090
static const std::size_t default_object_bits
Definition: config.h:150
std::string main
Definition: config.h:163
void set_arch(const irep_idt &)
Definition: config.cpp:673
std::size_t object_bits
Definition: config.h:156
API to expression classes.
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:21
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
irep_idt arch
Definition: config.h:84
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void set_arch_spec_alpha()
Definition: config.cpp:321
enum configt::cppt::cpp_standardt cpp_standard
void set_32()
Definition: config.cpp:30
void set_arch_spec_x32()
Definition: config.cpp:528
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:109
std::size_t int_width
Definition: config.h:30
void set_arch_spec_sh4()
Definition: config.cpp:617
bool for_has_scope
Definition: config.h:44
struct configt::javat java
Author: Diffblue Ltd.
void set_arch_spec_s390()
Definition: config.cpp:400
const symbolst & symbols
std::size_t pointer_width
Definition: config.h:36
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
bool char_is_unsigned
Definition: config.h:43
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1116
enum configt::ansi_ct::c_standardt c_standard
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:202
static c_standardt default_c_standard()
Definition: config.cpp:647
std::size_t wchar_t_width
Definition: config.h:40
bool Float128_type
Definition: config.h:46
static irep_idt this_operating_system()
Definition: config.cpp:1309
struct configt::cppt cpp
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:55
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter...
bool string_abstraction
Definition: config.h:121
bool is_object_bits_default
Definition: config.h:157
Base class for all expressions.
Definition: expr.h:42
void set_arch_spec_hppa()
Definition: config.cpp:588
void set_arch_spec_i386()
Definition: config.cpp:148
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define UNREACHABLE
Definition: invariant.h:250
void set_64()
Definition: config.cpp:35
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:89
static ost string_to_os(const std::string &)
Definition: config.cpp:1052
std::size_t memory_operand_size
Definition: config.h:73
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
std::size_t bool_width
Definition: config.h:32
irep_idt main_class
Definition: config.h:148
bool wchar_t_is_unsigned
Definition: config.h:43
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
std::size_t long_int_width
Definition: config.h:31
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
static cpp_standardt default_cpp_standard()
Definition: config.cpp:661
bool ts_18661_3_Floatn_types
Definition: config.h:45
static const std::size_t default_object_bits
Definition: config.h:123
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
static irep_idt this_architecture()
Definition: config.cpp:1212
std::size_t short_int_width
Definition: config.h:34
void set_arch_spec_s390x()
Definition: config.cpp:429
std::size_t long_double_width
Definition: config.h:39
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1177
bool simplify(exprt &expr, const namespacet &ns)
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:69
std::list< std::string > include_paths
Definition: config.h:115