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