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