cprover
Loading...
Searching...
No Matches
config.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "config.h"
10
11#include <climits>
12#include <cstdlib>
13
14#include "arith_tools.h"
15#include "cmdline.h"
16#include "cprover_prefix.h"
17#include "exception_utils.h"
18#include "namespace.h"
19#include "pointer_expr.h"
20#include "simplify_expr.h"
21#include "string2int.h"
22#include "string_utils.h"
23#include "symbol_table.h"
24
26
28{
29 set_LP32();
30}
31
33{
34 set_ILP32();
35}
36
38{
39 #ifdef _WIN32
40 set_LLP64();
41 #else
42 set_LP64();
43 #endif
44}
45
48{
49 bool_width=1*8;
50 int_width=4*8;
51 long_int_width=8*8;
52 char_width=1*8;
53 short_int_width=2*8;
54 long_long_int_width=8*8;
55 pointer_width=8*8;
56 single_width=4*8;
57 double_width=8*8;
58 long_double_width=16*8;
59 char_is_unsigned=false;
60 wchar_t_is_unsigned=false;
61 wchar_t_width=4*8;
62 alignment=1;
63 memory_operand_size=int_width/8;
64}
65
67// TODO: find the alignment restrictions (per type) of the different
68// architectures (currently: sizeof=alignedof)
69// TODO: implement the __attribute__((__aligned__(val)))
70
72{
73 bool_width=1*8;
74 int_width=8*8;
75 long_int_width=8*8;
76 char_width=1*8;
77 short_int_width=2*8;
78 long_long_int_width=8*8;
79 pointer_width=8*8;
80 single_width=4*8;
81 double_width=8*8;
82 long_double_width=8*8;
83 char_is_unsigned=false;
84 wchar_t_is_unsigned=false;
85 wchar_t_width=4*8;
86 alignment=1;
87 memory_operand_size=int_width/8;
88}
89
92{
93 bool_width=1*8;
94 int_width=4*8;
95 long_int_width=4*8;
96 char_width=1*8;
97 short_int_width=2*8;
98 long_long_int_width=8*8;
99 pointer_width=8*8;
100 single_width=4*8;
101 double_width=8*8;
102 long_double_width=8*8;
103 char_is_unsigned=false;
104 wchar_t_is_unsigned=false;
105 wchar_t_width=4*8;
106 alignment=1;
107 memory_operand_size=int_width/8;
108}
109
112{
113 bool_width=1*8;
114 int_width=4*8;
115 long_int_width=4*8;
116 char_width=1*8;
117 short_int_width=2*8;
118 long_long_int_width=8*8;
119 pointer_width=4*8;
120 single_width=4*8;
121 double_width=8*8;
122 long_double_width=12*8; // really 96 bits on GCC
123 char_is_unsigned=false;
124 wchar_t_is_unsigned=false;
125 wchar_t_width=4*8;
126 alignment=1;
127 memory_operand_size=int_width/8;
128}
129
132{
133 bool_width=1*8;
134 int_width=2*8;
135 long_int_width=4*8;
136 char_width=1*8;
137 short_int_width=2*8;
138 long_long_int_width=8*8;
139 pointer_width=4*8;
140 single_width=4*8;
141 double_width=8*8;
142 long_double_width=8*8;
143 char_is_unsigned=false;
144 wchar_t_is_unsigned=false;
145 wchar_t_width=4*8;
146 alignment=1;
147 memory_operand_size=int_width/8;
148}
149
151{
152 set_ILP32();
153 endianness=endiannesst::IS_LITTLE_ENDIAN;
154 char_is_unsigned=false;
155 NULL_is_zero=true;
156
157 switch(mode)
158 {
159 case flavourt::GCC:
160 case flavourt::CLANG:
161 defines.push_back("i386");
162 defines.push_back("__i386");
163 defines.push_back("__i386__");
164 if(mode == flavourt::CLANG)
165 defines.push_back("__LITTLE_ENDIAN__");
166 break;
167
168 case flavourt::VISUAL_STUDIO:
169 defines.push_back("_M_IX86");
170 break;
171
172 case flavourt::CODEWARRIOR:
173 case flavourt::ARM:
174 case flavourt::ANSI:
175 break;
176
177 case flavourt::NONE:
179 }
180}
181
183{
184 set_LP64();
185 endianness=endiannesst::IS_LITTLE_ENDIAN;
186 long_double_width=16*8;
187 char_is_unsigned=false;
188 NULL_is_zero=true;
189
190 switch(mode)
191 {
192 case flavourt::GCC:
193 case flavourt::CLANG:
194 defines.push_back("__LP64__");
195 defines.push_back("__x86_64");
196 defines.push_back("__x86_64__");
197 defines.push_back("_LP64");
198 defines.push_back("__amd64__");
199 defines.push_back("__amd64");
200
201 if(os == ost::OS_MACOS)
202 defines.push_back("__LITTLE_ENDIAN__");
203 break;
204
205 case flavourt::VISUAL_STUDIO:
206 defines.push_back("_M_X64");
207 defines.push_back("_M_AMD64");
208 break;
209
210 case flavourt::CODEWARRIOR:
211 case flavourt::ARM:
212 case flavourt::ANSI:
213 break;
214
215 case flavourt::NONE:
217 }
218}
219
221{
222 if(subarch=="powerpc")
223 set_ILP32();
224 else // ppc64 or ppc64le
225 set_LP64();
226
227 if(subarch=="ppc64le")
228 endianness=endiannesst::IS_LITTLE_ENDIAN;
229 else
230 endianness=endiannesst::IS_BIG_ENDIAN;
231
232 long_double_width=16*8;
233 char_is_unsigned=true;
234 NULL_is_zero=true;
235
236 switch(mode)
237 {
238 case flavourt::GCC:
239 case flavourt::CLANG:
240 defines.push_back("__powerpc");
241 defines.push_back("__powerpc__");
242 defines.push_back("__POWERPC__");
243 defines.push_back("__ppc__");
244
245 if(os == ost::OS_MACOS)
246 defines.push_back("__BIG_ENDIAN__");
247
248 if(subarch!="powerpc")
249 {
250 defines.push_back("__powerpc64");
251 defines.push_back("__powerpc64__");
252 defines.push_back("__PPC64__");
253 defines.push_back("__ppc64__");
254 if(subarch=="ppc64le")
255 {
256 defines.push_back("_CALL_ELF=2");
257 defines.push_back("__LITTLE_ENDIAN__");
258 }
259 else
260 {
261 defines.push_back("_CALL_ELF=1");
262 defines.push_back("__BIG_ENDIAN__");
263 }
264 }
265 break;
266
267 case flavourt::VISUAL_STUDIO:
268 defines.push_back("_M_PPC");
269 break;
270
271 case flavourt::CODEWARRIOR:
272 case flavourt::ARM:
273 case flavourt::ANSI:
274 break;
275
276 case flavourt::NONE:
278 }
279}
280
282{
283 if(subarch=="arm64")
284 {
285 set_LP64();
286 long_double_width=16*8;
287 }
288 else
289 {
290 set_ILP32();
291 long_double_width=8*8;
292 }
293
294 endianness=endiannesst::IS_LITTLE_ENDIAN;
295 char_is_unsigned=true;
296 NULL_is_zero=true;
297
298 switch(mode)
299 {
300 case flavourt::GCC:
301 case flavourt::CLANG:
302 if(subarch=="arm64")
303 defines.push_back("__aarch64__");
304 else
305 defines.push_back("__arm__");
306 if(subarch=="armhf")
307 defines.push_back("__ARM_PCS_VFP");
308 break;
309
310 case flavourt::VISUAL_STUDIO:
311 defines.push_back("_M_ARM");
312 break;
313
314 case flavourt::CODEWARRIOR:
315 case flavourt::ARM:
316 case flavourt::ANSI:
317 break;
318
319 case flavourt::NONE:
321 }
322}
323
325{
326 set_LP64();
327 endianness=endiannesst::IS_LITTLE_ENDIAN;
328 long_double_width=16*8;
329 char_is_unsigned=false;
330 NULL_is_zero=true;
331
332 switch(mode)
333 {
334 case flavourt::GCC:
335 defines.push_back("__alpha__");
336 break;
337
338 case flavourt::VISUAL_STUDIO:
339 defines.push_back("_M_ALPHA");
340 break;
341
342 case flavourt::CLANG:
343 case flavourt::CODEWARRIOR:
344 case flavourt::ARM:
345 case flavourt::ANSI:
346 break;
347
348 case flavourt::NONE:
350 }
351}
352
354{
355 if(subarch=="mipsel" ||
356 subarch=="mips" ||
357 subarch=="mipsn32el" ||
358 subarch=="mipsn32")
359 {
360 set_ILP32();
361 long_double_width=8*8;
362 }
363 else
364 {
365 set_LP64();
366 long_double_width=16*8;
367 }
368
369 if(subarch=="mipsel" ||
370 subarch=="mipsn32el" ||
371 subarch=="mips64el")
372 endianness=endiannesst::IS_LITTLE_ENDIAN;
373 else
374 endianness=endiannesst::IS_BIG_ENDIAN;
375
376 char_is_unsigned=false;
377 NULL_is_zero=true;
378
379 switch(mode)
380 {
381 case flavourt::GCC:
382 defines.push_back("__mips__");
383 defines.push_back("mips");
384 defines.push_back(
385 "_MIPS_SZPTR="+std::to_string(config.ansi_c.pointer_width));
386 break;
387
388 case flavourt::VISUAL_STUDIO:
389 UNREACHABLE; // not supported by Visual Studio
390 break;
391
392 case flavourt::CLANG:
393 case flavourt::CODEWARRIOR:
394 case flavourt::ARM:
395 case flavourt::ANSI:
396 break;
397
398 case flavourt::NONE:
400 }
401}
402
404{
405 set_LP64();
406 endianness = endiannesst::IS_LITTLE_ENDIAN;
407 long_double_width = 16 * 8;
408 char_is_unsigned = true;
409 NULL_is_zero = true;
410
411 switch(mode)
412 {
413 case flavourt::GCC:
414 defines.push_back("__riscv");
415 break;
416
417 case flavourt::VISUAL_STUDIO:
418 case flavourt::CLANG:
419 case flavourt::CODEWARRIOR:
420 case flavourt::ARM:
421 case flavourt::ANSI:
422 break;
423
424 case flavourt::NONE:
426 }
427}
428
430{
431 set_ILP32();
432 endianness=endiannesst::IS_BIG_ENDIAN;
433 long_double_width=16*8;
434 char_is_unsigned=true;
435 NULL_is_zero=true;
436
437 switch(mode)
438 {
439 case flavourt::GCC:
440 defines.push_back("__s390__");
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:
455 }
456}
457
459{
460 set_LP64();
461 endianness=endiannesst::IS_BIG_ENDIAN;
462 char_is_unsigned=true;
463 NULL_is_zero=true;
464
465 switch(mode)
466 {
467 case flavourt::GCC:
468 defines.push_back("__s390x__");
469 break;
470
471 case flavourt::VISUAL_STUDIO:
472 UNREACHABLE; // not supported by Visual Studio
473 break;
474
475 case flavourt::CLANG:
476 case flavourt::CODEWARRIOR:
477 case flavourt::ARM:
478 case flavourt::ANSI:
479 break;
480
481 case flavourt::NONE:
483 }
484}
485
487{
488 if(subarch=="sparc64")
489 {
490 set_LP64();
491 long_double_width=16*8;
492 }
493 else
494 {
495 set_ILP32();
496 long_double_width=16*8;
497 }
498
499 endianness=endiannesst::IS_BIG_ENDIAN;
500 char_is_unsigned=false;
501 NULL_is_zero=true;
502
503 switch(mode)
504 {
505 case flavourt::GCC:
506 defines.push_back("__sparc__");
507 if(subarch=="sparc64")
508 defines.push_back("__arch64__");
509 break;
510
511 case flavourt::VISUAL_STUDIO:
512 UNREACHABLE; // not supported by Visual Studio
513 break;
514
515 case flavourt::CLANG:
516 case flavourt::CODEWARRIOR:
517 case flavourt::ARM:
518 case flavourt::ANSI:
519 break;
520
521 case flavourt::NONE:
523 }
524}
525
527{
528 set_LP64();
529 long_double_width=16*8;
530 endianness=endiannesst::IS_LITTLE_ENDIAN;
531 char_is_unsigned=false;
532 NULL_is_zero=true;
533
534 switch(mode)
535 {
536 case flavourt::GCC:
537 defines.push_back("__ia64__");
538 defines.push_back("_IA64");
539 defines.push_back("__IA64__");
540 break;
541
542 case flavourt::VISUAL_STUDIO:
543 defines.push_back("_M_IA64");
544 break;
545
546 case flavourt::CLANG:
547 case flavourt::CODEWARRIOR:
548 case flavourt::ARM:
549 case flavourt::ANSI:
550 break;
551
552 case flavourt::NONE:
554 }
555}
556
558{
559 // This is a variant of x86_64 that has
560 // 32-bit long int and 32-bit pointers.
561 set_ILP32();
562 long_double_width=16*8; // different from i386
563 endianness=endiannesst::IS_LITTLE_ENDIAN;
564 char_is_unsigned=false;
565 NULL_is_zero=true;
566
567 switch(mode)
568 {
569 case flavourt::GCC:
570 defines.push_back("__ILP32__");
571 defines.push_back("__x86_64");
572 defines.push_back("__x86_64__");
573 defines.push_back("__amd64__");
574 defines.push_back("__amd64");
575 break;
576
577 case flavourt::VISUAL_STUDIO:
578 UNREACHABLE; // not supported by Visual Studio
579 break;
580
581 case flavourt::CLANG:
582 case flavourt::CODEWARRIOR:
583 case flavourt::ARM:
584 case flavourt::ANSI:
585 break;
586
587 case flavourt::NONE:
589 }
590}
591
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:
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:
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__) || defined(__OpenBSD__)
681 // By default, clang on FreeBSD builds C code in GNU C99
682 // By default, clang on OpenBSD builds C code in C99
683 return c_standardt::C99;
684#else
685 // By default, gcc 5.4 or higher use gnu11; older versions use gnu89
686 return c_standardt::C11;
687#endif
688}
689
691{
692 // g++ 6.3 uses gnu++14
693 // g++ 5.4 uses gnu++98
694 // clang 6.0 uses c++14
695 #if defined _WIN32
696 return cpp_standardt::CPP14;
697 #else
698 return cpp_standardt::CPP98;
699 #endif
700}
701
703{
704 ansi_c.arch=arch;
705
706 if(arch=="none")
707 {
708 // the architecture for people who can't commit
711 ansi_c.NULL_is_zero=false;
712
713 if(sizeof(long int)==8)
714 ansi_c.set_64();
715 else
716 ansi_c.set_32();
717 }
718 else if(arch=="alpha")
720 else if(arch=="arm64" ||
721 arch=="armel" ||
722 arch=="armhf" ||
723 arch=="arm")
725 else if(arch=="mips64el" ||
726 arch=="mipsn32el" ||
727 arch=="mipsel" ||
728 arch=="mips64" ||
729 arch=="mipsn32" ||
730 arch=="mips")
732 else if(arch=="powerpc" ||
733 arch=="ppc64" ||
734 arch=="ppc64le")
736 else if(arch == "riscv64")
738 else if(arch=="sparc" ||
739 arch=="sparc64")
741 else if(arch=="ia64")
743 else if(arch=="s390x")
745 else if(arch=="s390")
747 else if(arch=="x32")
749 else if(arch=="v850")
751 else if(arch=="hppa")
753 else if(arch=="sh4")
755 else if(arch=="x86_64")
757 else if(arch=="i386")
759 else
760 {
761 // We run on something new and unknown.
762 // We verify for i386 instead.
764 ansi_c.arch="i386";
765 }
766}
767
776 const std::string &argument,
777 const std::size_t pointer_width)
778{
779 const auto throw_for_reason = [&](const std::string &reason) {
781 "Value of \"" + argument + "\" given for object-bits is " + reason +
782 ". object-bits must be positive and less than the pointer width (" +
783 std::to_string(pointer_width) + ") ",
784 "--object_bits");
785 };
786 const auto object_bits = string2optional<unsigned int>(argument);
787 if(!object_bits)
788 throw_for_reason("not a valid unsigned integer");
789 if(*object_bits == 0 || *object_bits >= pointer_width)
790 throw_for_reason("out of range");
791
793 bv_encoding.object_bits = *object_bits;
795 return bv_encoding;
796}
797
798bool configt::set(const cmdlinet &cmdline)
799{
800 // defaults -- we match the architecture we have ourselves
801
803
805 ansi_c.for_has_scope=true; // C99 or later
810 ansi_c.arch="none";
812 // NOLINTNEXTLINE(readability/casting)
813 ansi_c.NULL_is_zero=reinterpret_cast<size_t>(nullptr)==0;
814
815 // Default is ROUND_TO_EVEN, justified by C99:
816 // 1 At program startup the floating-point environment is initialized as
817 // prescribed by IEC 60559:
818 // - All floating-point exception status flags are cleared.
819 // - The rounding direction mode is rounding to nearest.
821
822 if(cmdline.isset("function"))
823 main=cmdline.get_value("function");
824
825 if(cmdline.isset('D'))
826 ansi_c.defines=cmdline.get_values('D');
827
828 if(cmdline.isset('I'))
829 ansi_c.include_paths=cmdline.get_values('I');
830
831 if(cmdline.isset("classpath"))
832 {
833 // Specifying -classpath or -cp overrides any setting of the
834 // CLASSPATH environment variable.
835 set_classpath(cmdline.get_value("classpath"));
836 }
837 else if(cmdline.isset("cp"))
838 {
839 // Specifying -classpath or -cp overrides any setting of the
840 // CLASSPATH environment variable.
841 set_classpath(cmdline.get_value("cp"));
842 }
843 else
844 {
845 // environment variable set?
846 const char *CLASSPATH=getenv("CLASSPATH");
847 if(CLASSPATH!=nullptr)
848 set_classpath(CLASSPATH);
849 else
850 set_classpath("."); // default
851 }
852
853 if(cmdline.isset("main-class"))
854 java.main_class=cmdline.get_value("main-class");
855
856 if(cmdline.isset("include"))
857 ansi_c.include_files=cmdline.get_values("include");
858
859 // the default architecture is the one we run on
860 irep_idt this_arch=this_architecture();
861 irep_idt arch=this_arch;
862
863 // let's pick an OS now
864 // the default is the one we run on
866 irep_idt os=this_os;
867
868 if(cmdline.isset("i386-linux"))
869 {
870 os="linux";
871 arch="i386";
872 }
873 else if(cmdline.isset("i386-win32") ||
874 cmdline.isset("win32"))
875 {
876 os="windows";
877 arch="i386";
878 }
879 else if(cmdline.isset("winx64"))
880 {
881 os="windows";
882 arch="x86_64";
883 }
884 else if(cmdline.isset("i386-macos"))
885 {
886 os="macos";
887 arch="i386";
888 }
889 else if(cmdline.isset("ppc-macos"))
890 {
891 arch="powerpc";
892 os="macos";
893 }
894
895 if(cmdline.isset("arch"))
896 {
897 arch=cmdline.get_value("arch");
898 }
899
900 if(cmdline.isset("os"))
901 {
902 os=cmdline.get_value("os");
903 }
904
905 if(os=="windows")
906 {
907 // Cygwin uses GCC throughout, use i386-linux
908 // MinGW needs --win32 --gcc
911
912 if(cmdline.isset("gcc"))
913 {
914 // There are gcc versions that target Windows (MinGW for example),
915 // and we support that.
918
919 // enable Cygwin
920 #ifdef _WIN32
921 ansi_c.defines.push_back("__CYGWIN__");
922 #endif
923
924 // MinGW has extra defines
925 ansi_c.defines.push_back("__int64=long long");
926 }
927 else
928 {
929 // On Windows, our default is Visual Studio.
930 // On FreeBSD, it's clang.
931 // On anything else, it's GCC as the preprocessor,
932 // but we recognize the Visual Studio language,
933 // which is somewhat inconsistent.
934 #ifdef _WIN32
937 #elif __FreeBSD__
940 #else
943 #endif
944
946 }
947 }
948 else if(os=="macos")
949 {
954 }
955 else if(os=="linux" || os=="solaris")
956 {
961 }
962 else if(os=="freebsd")
963 {
968 }
969 else
970 {
971 // give up, but use reasonable defaults
976 }
977
980
981 set_arch(arch);
982
983 if(os=="windows")
984 {
985 // note that sizeof(void *)==8, but sizeof(long)==4!
986 if(arch=="x86_64")
988
989 // On Windows, wchar_t is unsigned 16 bit, regardless
990 // of the compiler used.
993
994 // long double is the same as double in Visual Studio,
995 // but it's 16 bytes with GCC with the 64-bit target.
996 if(arch=="x64_64" && cmdline.isset("gcc"))
998 else
1000 }
1001 else if(os == "macos" && arch == "arm64")
1002 {
1003 // https://developer.apple.com/documentation/xcode/
1004 // writing_arm64_code_for_apple_platforms#//apple_ref/doc/uid/TP40013702-SW1
1005 ansi_c.char_is_unsigned = false;
1006 ansi_c.long_double_width = 8 * 8;
1007 }
1008
1009 // Let's check some of the type widths in case we run
1010 // the same architecture and OS that we are verifying for.
1011 if(arch==this_arch && os==this_os)
1012 {
1013 INVARIANT(
1014 ansi_c.int_width == sizeof(int) * CHAR_BIT,
1015 "int width shall be equal to the system int width");
1016 INVARIANT(
1017 ansi_c.long_int_width == sizeof(long) * CHAR_BIT,
1018 "long int width shall be equal to the system long int width");
1019 INVARIANT(
1020 ansi_c.bool_width == sizeof(bool) * CHAR_BIT,
1021 "bool width shall be equal to the system bool width");
1022 INVARIANT(
1023 ansi_c.char_width == sizeof(char) * CHAR_BIT,
1024 "char width shall be equal to the system char width");
1025 INVARIANT(
1026 ansi_c.short_int_width == sizeof(short) * CHAR_BIT,
1027 "short int width shall be equal to the system short int width");
1028 INVARIANT(
1029 ansi_c.long_long_int_width == sizeof(long long) * CHAR_BIT,
1030 "long long int width shall be equal to the system long long int width");
1031 INVARIANT(
1032 ansi_c.pointer_width == sizeof(void *) * CHAR_BIT,
1033 "pointer width shall be equal to the system pointer width");
1034 INVARIANT(
1035 ansi_c.single_width == sizeof(float) * CHAR_BIT,
1036 "float width shall be equal to the system float width");
1037 INVARIANT(
1038 ansi_c.double_width == sizeof(double) * CHAR_BIT,
1039 "double width shall be equal to the system double width");
1040 INVARIANT(
1042 (static_cast<char>((1 << CHAR_BIT) - 1) == (1 << CHAR_BIT) - 1),
1043 "char_is_unsigned flag shall indicate system char unsignedness");
1044
1045#ifndef _WIN32
1046 // On Windows, long double width varies by compiler
1047 INVARIANT(
1048 ansi_c.long_double_width == sizeof(long double) * CHAR_BIT,
1049 "long double width shall be equal to the system long double width");
1050#endif
1051 }
1052
1053 // the following allows overriding the defaults
1054
1055 if(cmdline.isset("16"))
1056 ansi_c.set_16();
1057
1058 if(cmdline.isset("32"))
1059 ansi_c.set_32();
1060
1061 if(cmdline.isset("64"))
1062 ansi_c.set_64();
1063
1064 if(cmdline.isset("LP64"))
1065 ansi_c.set_LP64(); // int=32, long=64, pointer=64
1066
1067 if(cmdline.isset("ILP64"))
1068 ansi_c.set_ILP64(); // int=64, long=64, pointer=64
1069
1070 if(cmdline.isset("LLP64"))
1071 ansi_c.set_LLP64(); // int=32, long=32, pointer=64
1072
1073 if(cmdline.isset("ILP32"))
1074 ansi_c.set_ILP32(); // int=32, long=32, pointer=32
1075
1076 if(cmdline.isset("LP32"))
1077 ansi_c.set_LP32(); // int=16, long=32, pointer=32
1078
1079 if(cmdline.isset("string-abstraction"))
1081 else
1083
1084 if(cmdline.isset("no-library"))
1086
1087 if(cmdline.isset("little-endian"))
1089
1090 if(cmdline.isset("big-endian"))
1092
1093 if(cmdline.isset("little-endian") &&
1094 cmdline.isset("big-endian"))
1095 return true;
1096
1097 if(cmdline.isset("unsigned-char"))
1099
1100 if(cmdline.isset("round-to-even") ||
1101 cmdline.isset("round-to-nearest"))
1103
1104 if(cmdline.isset("round-to-plus-inf"))
1106
1107 if(cmdline.isset("round-to-minus-inf"))
1109
1110 if(cmdline.isset("round-to-zero"))
1112
1113 if(cmdline.isset("object-bits"))
1114 {
1116 cmdline.get_value("object-bits"), ansi_c.pointer_width);
1117 }
1118
1119 if(cmdline.isset("malloc-fail-assert") && cmdline.isset("malloc-fail-null"))
1120 {
1122 "at most one malloc failure mode is acceptable", "--malloc-fail-null"};
1123 }
1124 if(cmdline.isset("malloc-fail-null"))
1126 if(cmdline.isset("malloc-fail-assert"))
1128
1129 ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
1130
1131 if(cmdline.isset("c89"))
1132 ansi_c.set_c89();
1133
1134 if(cmdline.isset("c99"))
1135 ansi_c.set_c99();
1136
1137 if(cmdline.isset("c11"))
1138 ansi_c.set_c11();
1139
1140 if(cmdline.isset("cpp98"))
1141 cpp.set_cpp98();
1142
1143 if(cmdline.isset("cpp03"))
1144 cpp.set_cpp03();
1145
1146 if(cmdline.isset("cpp11"))
1147 cpp.set_cpp11();
1148
1149 // set the upper bound for argc
1150 if(os == "windows")
1151 {
1152 // On Windows, CreateProcess accepts no more than 32767 characters, so make
1153 // that a hard limit.
1154 ansi_c.max_argc = mp_integer{32767};
1155 }
1156 else
1157 {
1158 // For other systems assume argc is no larger than the what would make argv
1159 // consume all available memory space:
1160 // 2^pointer_width / (pointer_width / char_width) is the maximum number of
1161 // argv elements sysconf(ARG_MAX) is likely much lower than this, but we
1162 // don't know that value for the verification target platform.
1163 const auto pointer_bits_2log =
1165 if(ansi_c.pointer_width - pointer_bits_2log <= ansi_c.int_width)
1166 {
1167 ansi_c.max_argc = power(2, config.ansi_c.int_width - pointer_bits_2log);
1168 }
1169 // otherwise we leave argc unconstrained
1170 }
1171
1172 return false;
1173}
1174
1176{
1177 // clang-format off
1178 switch(os)
1179 {
1180 case ost::OS_LINUX: return "linux";
1181 case ost::OS_MACOS: return "macos";
1182 case ost::OS_WIN: return "win";
1183 case ost::NO_OS: return "none";
1184 }
1185 // clang-format on
1186
1188}
1189
1191{
1192 if(os=="linux")
1193 return ost::OS_LINUX;
1194 else if(os=="macos")
1195 return ost::OS_MACOS;
1196 else if(os=="win")
1197 return ost::OS_WIN;
1198 else
1199 return ost::NO_OS;
1200}
1201
1203 const namespacet &ns,
1204 const std::string &what)
1205{
1206 const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1207 const symbolt *symbol;
1208
1209 const bool not_found = ns.lookup(id, symbol);
1210 INVARIANT(!not_found, id2string(id) + " must be in namespace");
1211
1212 const exprt &tmp=symbol->value;
1213
1214 INVARIANT(
1215 tmp.id() == ID_address_of &&
1216 to_address_of_expr(tmp).object().id() == ID_index &&
1217 to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
1218 ID_string_constant,
1219 "symbol table configuration entry '" + id2string(id) +
1220 "' must be a string constant");
1221
1222 return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
1223}
1224
1225static unsigned unsigned_from_ns(
1226 const namespacet &ns,
1227 const std::string &what)
1228{
1229 const irep_idt id=CPROVER_PREFIX "architecture_"+what;
1230 const symbolt *symbol;
1231
1232 const bool not_found = ns.lookup(id, symbol);
1233 INVARIANT(!not_found, id2string(id) + " must be in namespace");
1234
1235 exprt tmp=symbol->value;
1236 simplify(tmp, ns);
1237
1238 INVARIANT(
1239 tmp.id() == ID_constant,
1240 "symbol table configuration entry '" + id2string(id) +
1241 "' must be a constant");
1242
1243 mp_integer int_value;
1244
1245 const bool error = to_integer(to_constant_expr(tmp), int_value);
1246 INVARIANT(
1247 !error,
1248 "symbol table configuration entry '" + id2string(id) +
1249 "' must be convertible to mp_integer");
1250
1251 return numeric_cast_v<unsigned>(int_value);
1252}
1253
1255 const symbol_tablet &symbol_table)
1256{
1257 // maybe not compiled from C/C++
1258 if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "int_width")==
1259 symbol_table.symbols.end())
1260 return;
1261
1262 namespacet ns(symbol_table);
1263
1264 // clear defines
1265 ansi_c.defines.clear();
1266
1267 // first set architecture to get some defaults
1268 if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "arch")==
1269 symbol_table.symbols.end())
1271 else
1272 set_arch(string_from_ns(ns, "arch"));
1273
1274 ansi_c.int_width=unsigned_from_ns(ns, "int_width");
1275 ansi_c.long_int_width=unsigned_from_ns(ns, "long_int_width");
1276 ansi_c.bool_width=1*8;
1277 ansi_c.char_width=unsigned_from_ns(ns, "char_width");
1278 ansi_c.short_int_width=unsigned_from_ns(ns, "short_int_width");
1279 ansi_c.long_long_int_width=unsigned_from_ns(ns, "long_long_int_width");
1280 ansi_c.pointer_width=unsigned_from_ns(ns, "pointer_width");
1281 ansi_c.single_width=unsigned_from_ns(ns, "single_width");
1282 ansi_c.double_width=unsigned_from_ns(ns, "double_width");
1283 ansi_c.long_double_width=unsigned_from_ns(ns, "long_double_width");
1284 ansi_c.wchar_t_width=unsigned_from_ns(ns, "wchar_t_width");
1285
1286 ansi_c.char_is_unsigned=unsigned_from_ns(ns, "char_is_unsigned")!=0;
1287 ansi_c.wchar_t_is_unsigned=unsigned_from_ns(ns, "wchar_t_is_unsigned")!=0;
1288 // for_has_scope, single_precision_constant, rounding_mode,
1289 // ts_18661_3_Floatn_types are not architectural features,
1290 // and thus not stored in namespace
1291
1292 ansi_c.alignment=unsigned_from_ns(ns, "alignment");
1293
1294 ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
1295
1297
1298 if(symbol_table.symbols.find(CPROVER_PREFIX "architecture_" "os")==
1299 symbol_table.symbols.end())
1301 else
1303
1304 ansi_c.NULL_is_zero = unsigned_from_ns(ns, "NULL_is_zero") != 0;
1305
1306 // mode, preprocessor (and all preprocessor command line options),
1307 // lib, string_abstraction not stored in namespace
1308
1310}
1311
1315 const symbol_tablet &symbol_table)
1316{
1317 // has been overridden by command line option,
1318 // thus do not apply language defaults
1320 return;
1321
1322 // set object_bits according to entry point language
1323 if(const auto maybe_symbol=symbol_table.lookup(CPROVER_PREFIX "_start"))
1324 {
1325 const symbolt &entry_point_symbol=*maybe_symbol;
1326
1327 if(entry_point_symbol.mode==ID_java)
1329 else if(entry_point_symbol.mode==ID_C)
1331 else if(entry_point_symbol.mode==ID_cpp)
1335 "object_bits should fit into pointer width");
1336 }
1337}
1338
1340{
1341 return "Running with "+std::to_string(bv_encoding.object_bits)+
1342 " object bits, "+
1344 " offset bits ("+
1345 (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
1346 ")";
1347}
1348
1349// clang-format off
1351{
1352 irep_idt this_arch;
1353
1354 // following http://wiki.debian.org/ArchitectureSpecificsMemo
1355
1356 #ifdef __alpha__
1357 this_arch = "alpha";
1358 #elif defined(__armel__)
1359 this_arch = "armel";
1360 #elif defined(__aarch64__)
1361 this_arch = "arm64";
1362 #elif defined(__arm__)
1363 #ifdef __ARM_PCS_VFP
1364 this_arch = "armhf"; // variant of arm with hard float
1365 #else
1366 this_arch = "arm";
1367 #endif
1368 #elif defined(__mipsel__)
1369 #if _MIPS_SIM==_ABIO32
1370 this_arch = "mipsel";
1371 #elif _MIPS_SIM==_ABIN32
1372 this_arch = "mipsn32el";
1373 #else
1374 this_arch = "mips64el";
1375 #endif
1376 #elif defined(__mips__)
1377 #if _MIPS_SIM==_ABIO32
1378 this_arch = "mips";
1379 #elif _MIPS_SIM==_ABIN32
1380 this_arch = "mipsn32";
1381 #else
1382 this_arch = "mips64";
1383 #endif
1384 #elif defined(__powerpc__)
1385 #if defined(__ppc64__) || defined(__PPC64__) || \
1386 defined(__powerpc64__) || defined(__POWERPC64__)
1387 #ifdef __LITTLE_ENDIAN__
1388 this_arch = "ppc64le";
1389 #else
1390 this_arch = "ppc64";
1391 #endif
1392 #else
1393 this_arch = "powerpc";
1394 #endif
1395 #elif defined(__riscv)
1396 this_arch = "riscv64";
1397 #elif defined(__sparc__)
1398 #ifdef __arch64__
1399 this_arch = "sparc64";
1400 #else
1401 this_arch = "sparc";
1402 #endif
1403 #elif defined(__ia64__)
1404 this_arch = "ia64";
1405 #elif defined(__s390x__)
1406 this_arch = "s390x";
1407 #elif defined(__s390__)
1408 this_arch = "s390";
1409 #elif defined(__x86_64__)
1410 #ifdef __ILP32__
1411 this_arch = "x32"; // variant of x86_64 with 32-bit pointers
1412 #else
1413 this_arch = "x86_64";
1414 #endif
1415 #elif defined(__i386__)
1416 this_arch = "i386";
1417 #elif defined(_WIN64)
1418 this_arch = "x86_64";
1419 #elif defined(_WIN32)
1420 this_arch = "i386";
1421 #elif defined(__hppa__)
1422 this_arch = "hppa";
1423 #elif defined(__sh__)
1424 this_arch = "sh4";
1425 #else
1426 // something new and unknown!
1427 this_arch = "unknown";
1428 #endif
1429
1430 return this_arch;
1431}
1432// clang-format on
1433
1434void configt::set_classpath(const std::string &cp)
1435{
1436// These are separated by colons on Unix, and semicolons on
1437// Windows.
1438#ifdef _WIN32
1439 const char cp_separator = ';';
1440#else
1441 const char cp_separator = ':';
1442#endif
1443
1444 std::vector<std::string> class_path =
1445 split_string(cp, cp_separator);
1446 java.classpath.insert(
1447 java.classpath.end(), class_path.begin(), class_path.end());
1448}
1449
1451{
1452 irep_idt this_os;
1453
1454 #ifdef _WIN32
1455 this_os="windows";
1456 #elif __APPLE__
1457 this_os="macos";
1458 #elif __FreeBSD__
1459 this_os="freebsd";
1460 #elif __linux__
1461 this_os="linux";
1462 #elif __SVR4
1463 this_os="solaris";
1464 #else
1465 this_os="unknown";
1466 #endif
1467
1468 return this_os;
1469}
std::size_t address_bits(const mp_integer &size)
ceil(log2(size))
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
std::string get_value(char option) const
Definition: cmdline.cpp:48
virtual bool isset(char option) const
Definition: cmdline.cpp:30
const std::list< std::string > & get_values(const std::string &option) const
Definition: cmdline.cpp:109
Globally accessible architectural configuration.
Definition: config.h:104
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1254
void set_arch(const irep_idt &)
Definition: config.cpp:702
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1314
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
optionalt< std::string > main
Definition: config.h:326
std::string object_bits_info()
Definition: config.cpp:1339
void set_classpath(const std::string &cp)
Definition: config.cpp:1434
static irep_idt this_architecture()
Definition: config.cpp:1350
struct configt::javat java
struct configt::cppt cpp
static irep_idt this_operating_system()
Definition: config.cpp:1450
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
@ ROUND_TO_PLUS_INF
Definition: ieee_float.h:126
@ ROUND_TO_MINUS_INF
Definition: ieee_float.h:125
exprt & array()
Definition: std_expr.h:1353
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
configt::bv_encodingt parse_object_bits_encoding(const std::string &argument, const std::size_t pointer_width)
Parses the object_bits argument from the command line arguments.
Definition: config.cpp:775
static unsigned unsigned_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1225
configt config
Definition: config.cpp:25
static irep_idt string_from_ns(const namespacet &ns, const std::string &what)
Definition: config.cpp:1202
configt config
Definition: config.cpp:25
#define CPROVER_PREFIX
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:23
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
bool simplify(exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
std::size_t long_double_width
Definition: config.h:118
std::list< std::string > include_paths
Definition: config.h:238
bool for_has_scope
Definition: config.h:123
optionalt< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...
Definition: config.h:265
void set_arch_spec_x32()
Definition: config.cpp:557
enum configt::ansi_ct::c_standardt c_standard
void set_32()
Definition: config.cpp:32
void set_arch_spec_riscv64()
Definition: config.cpp:403
endiannesst endianness
Definition: config.h:177
void set_16()
Definition: config.cpp:27
void set_arch_spec_sh4()
Definition: config.cpp:645
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:111
bool ts_18661_3_Floatn_types
Definition: config.h:124
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition: config.cpp:593
bool wchar_t_is_unsigned
Definition: config.h:122
void set_arch_spec_hppa()
Definition: config.cpp:616
static std::string os_to_string(ost)
Definition: config.cpp:1175
std::size_t pointer_width
Definition: config.h:115
bool gcc__float128_type
Definition: config.h:125
void set_c89()
Definition: config.h:135
std::list< std::string > include_files
Definition: config.h:239
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:71
irep_idt arch
Definition: config.h:191
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:151
void set_64()
Definition: config.cpp:37
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:486
static ost string_to_os(const std::string &)
Definition: config.cpp:1190
std::list< std::string > defines
Definition: config.h:235
void set_c99()
Definition: config.h:140
bool single_precision_constant
Definition: config.h:126
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:91
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:281
std::size_t wchar_t_width
Definition: config.h:119
preprocessort preprocessor
Definition: config.h:233
@ malloc_failure_mode_return_null
Definition: config.h:254
@ malloc_failure_mode_assert_then_assume
Definition: config.h:255
std::size_t double_width
Definition: config.h:117
bool malloc_may_fail
Definition: config.h:249
bool char_is_unsigned
Definition: config.h:122
static c_standardt default_c_standard()
Definition: config.cpp:675
void set_arch_spec_alpha()
Definition: config.cpp:324
std::size_t alignment
Definition: config.h:165
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:220
std::size_t bool_width
Definition: config.h:111
bool string_abstraction
Definition: config.h:248
void set_arch_spec_s390()
Definition: config.cpp:429
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:47
void set_arch_spec_x86_64()
Definition: config.cpp:182
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:131
std::size_t memory_operand_size
Definition: config.h:169
std::size_t long_long_int_width
Definition: config.h:114
void set_arch_spec_s390x()
Definition: config.cpp:458
bool NULL_is_zero
Definition: config.h:194
std::size_t long_int_width
Definition: config.h:110
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:353
std::size_t single_width
Definition: config.h:116
void set_arch_spec_i386()
Definition: config.cpp:150
std::size_t short_int_width
Definition: config.h:113
std::size_t char_width
Definition: config.h:112
void set_c11()
Definition: config.h:145
static const std::size_t default_object_bits
Definition: config.h:260
flavourt mode
Definition: config.h:222
std::size_t int_width
Definition: config.h:109
malloc_failure_modet malloc_failure_mode
Definition: config.h:258
void set_arch_spec_ia64()
Definition: config.cpp:526
bool is_object_bits_default
Definition: config.h:322
std::size_t object_bits
Definition: config.h:321
enum configt::cppt::cpp_standardt cpp_standard
void set_cpp11()
Definition: config.h:288
static const std::size_t default_object_bits
Definition: config.h:301
void set_cpp03()
Definition: config.h:284
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
void set_cpp98()
Definition: config.h:280
classpatht classpath
Definition: config.h:312
irep_idt main_class
Definition: config.h:313
static const std::size_t default_object_bits
Definition: config.h:315
Author: Diffblue Ltd.