cprover
Loading...
Searching...
No Matches
config.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_CONFIG_H
10#define CPROVER_UTIL_CONFIG_H
11
12#include "ieee_float.h"
13#include "irep.h"
14
15#include <list>
16#include <optional>
17
18class cmdlinet;
20
21// Configt is the one place beyond *_parse_options where options are ... parsed.
22// Options that are handled by configt are documented here.
23
24#define OPT_CONFIG_C_CPP \
25 "D:I:(include)(function)" \
26 "(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
27 "(unsigned-char)" \
28 "(round-to-even)(round-to-nearest)" \
29 "(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
30 "(no-library)"
31
32#define HELP_CONFIG_C_CPP \
33 " {y-I} {upath} \t set include path (C/C++)\n" \
34 " {y--include} {ufile} \t set include file (C/C++)\n" \
35 " {y-D} {umacro} \t define preprocessor macro (C/C++)\n" \
36 " {y--c89}, {y--c99}, {y--c11} \t " \
37 "set C language standard (default: " + \
38 std::string( \
39 configt::ansi_ct::default_c_standard() == \
40 configt::ansi_ct::c_standardt::C89 \
41 ? "c89" \
42 : configt::ansi_ct::default_c_standard() == \
43 configt::ansi_ct::c_standardt::C99 \
44 ? "c99" \
45 : configt::ansi_ct::default_c_standard() == \
46 configt::ansi_ct::c_standardt::C11 \
47 ? "c11" \
48 : "") + \
49 ")\n" \
50 " {y--cpp98}, {y--cpp03}, {y--cpp11} \t " \
51 "set C++ language standard (default: " + \
52 std::string( \
53 configt::cppt::default_cpp_standard() == \
54 configt::cppt::cpp_standardt::CPP98 \
55 ? "cpp98" \
56 : configt::cppt::default_cpp_standard() == \
57 configt::cppt::cpp_standardt::CPP03 \
58 ? "cpp03" \
59 : configt::cppt::default_cpp_standard() == \
60 configt::cppt::cpp_standardt::CPP11 \
61 ? "cpp11" \
62 : "") + \
63 ")\n" \
64 " {y--unsigned-char} \t make \"char\" unsigned by default\n" \
65 " {y--round-to-nearest}, {y--round-to-even} \t " \
66 "rounding towards nearest even (default)\n" \
67 " {y--round-to-plus-inf} \t rounding towards plus infinity\n" \
68 " {y--round-to-minus-inf} \t rounding towards minus infinity\n" \
69 " {y--round-to-zero} \t rounding towards zero\n" \
70 " {y--no-library} \t disable built-in abstract C library\n"
71
72#define OPT_CONFIG_LIBRARY \
73 "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \
74 "(no-malloc-may-fail)" \
75 "(string-abstraction)"
76
77#define HELP_CONFIG_LIBRARY \
78 " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n" \
79 " {y--no-malloc-may-fail} \t disable potential malloc failure\n" \
80 " {y--malloc-fail-assert} \t " \
81 "set malloc failure mode to assert-then-assume\n" \
82 " {y--malloc-fail-null} \t set malloc failure mode to return null\n" \
83 " {y--string-abstraction} \t track C string lengths and zero-termination\n"
84
85#define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)"
86
87#define OPT_CONFIG_PLATFORM \
88 "(arch):(os):" \
89 "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
90 "(little-endian)(big-endian)" \
91 "(i386-linux)" \
92 "(i386-win32)(win32)(winx64)" \
93 "(i386-macos)(ppc-macos)" \
94 "(gcc)"
95
96#define HELP_CONFIG_PLATFORM \
97 " {y--arch} {uarch_name} \t " \
98 "set architecture (default: " + \
99 id2string(configt::this_architecture()) + \
100 ") to one of: {yalpha}, {yarm}, {yarm64}, {yarmel}, {yarmhf}, {yhppa}, " \
101 "{yi386}, {yia64}, {ymips}, {ymips64}, {ymips64el}, {ymipsel}, " \
102 "{ymipsn32}, " \
103 "{ymipsn32el}, {ypowerpc}, {yppc64}, {yppc64le}, {yriscv64}, {ys390}, " \
104 "{ys390x}, {ysh4}, {ysparc}, {ysparc64}, {yv850}, {yx32}, {yx86_64}, or " \
105 "{ynone}\n" \
106 " {y--os} {uos_name} \t " \
107 "set operating system (default: " + \
108 id2string(configt::this_operating_system()) + \
109 ") to one of: {yfreebsd}, {ylinux}, {ymacos}, {ynetbsd}, {yopenbsd}, " \
110 "{ysolaris}, {yhurd}, or {ywindows}\n" \
111 " {y--i386-linux}, {y--i386-win32}, {y--i386-macos}, {y--ppc-macos}, " \
112 "{y--win32}, {y--winx64} \t " \
113 "set architecture and operating system\n" \
114 " {y--LP64}, {y--ILP64}, {y--LLP64}, {y--ILP32}, {y--LP32} \t " \
115 "set width of int, long and pointers, but don't override default " \
116 "architecture and operating system\n" \
117 " {y--16}, {y--32}, {y--64} \t " \
118 "equivalent to {y--LP32}, {y--ILP32}, {y--LP64} (on Windows: " \
119 "{y--LLP64})\n" \
120 " {y--little-endian} \t allow little-endian word-byte conversions\n" \
121 " {y--big-endian} \t allow big-endian word-byte conversions\n" \
122 " {y--gcc} \t use GCC as preprocessor\n"
123
124#define OPT_CONFIG_BACKEND "(object-bits):"
125
126#define HELP_CONFIG_BACKEND \
127 " {y--object-bits} {un} \t number of bits used for object addresses\n"
128
132{
133public:
134 struct ansi_ct
135 {
136 // for ANSI-C
137 std::size_t int_width;
138 std::size_t long_int_width;
139 std::size_t bool_width;
140 std::size_t char_width;
141 std::size_t short_int_width;
143 std::size_t pointer_width;
144 std::size_t single_width;
145 std::size_t double_width;
146 std::size_t long_double_width;
147 std::size_t wchar_t_width;
148
149 // various language options
152 bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
153 bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5
154 bool __float128_is_keyword; // __float128 as a keyword (and not typedef)
155 bool float16_type; // _Float16 (Clang >= 15, GCC >= 12)
156 bool bf16_type; // __bf16 (Clang >= 15, GCC >= 13)
157 bool fp16_type; // __fp16 (GCC >= 4.5 on ARM, Clang >= 6)
166
167 void set_c89()
168 {
170 for_has_scope = false;
171 }
172 void set_c99()
173 {
175 for_has_scope = true;
176 }
177 void set_c11()
178 {
180 for_has_scope = true;
181 }
182
184
185 void set_16();
186 void set_32();
187 void set_64();
188
189 // http://www.unix.org/version2/whatsnew/lp64_wp.html
190 void set_LP64(); // int=32, long=64, pointer=64
191 void set_ILP64(); // int=64, long=64, pointer=64
192 void set_LLP64(); // int=32, long=32, pointer=64
193 void set_ILP32(); // int=32, long=32, pointer=32
194 void set_LP32(); // int=16, long=32, pointer=32
195
196 // minimum alignment (in structs) measured in bytes
197 std::size_t alignment;
198
199 // maximum minimum size of the operands for a machine
200 // instruction (in bytes)
202
210
219
220 static std::string os_to_string(ost);
221 static ost string_to_os(const std::string &);
222
224
225 // architecture-specific integer value of null pointer constant
227
228 void set_arch_spec_i386();
230 void set_arch_spec_power(const irep_idt &subarch);
231 void set_arch_spec_arm(const irep_idt &subarch);
232 void set_arch_spec_alpha();
233 void set_arch_spec_mips(const irep_idt &subarch);
235 void set_arch_spec_s390();
236 void set_arch_spec_s390x();
237 void set_arch_spec_sparc(const irep_idt &subarch);
238 void set_arch_spec_ia64();
239 void set_arch_spec_x32();
240 void set_arch_spec_v850();
241 void set_arch_spec_hppa();
242 void set_arch_spec_sh4();
245
256 flavourt mode; // the syntax of source files
257
267 preprocessort preprocessor; // the preprocessor to use
268
269 std::list<std::string> defines;
270 std::list<std::string> undefines;
271 std::list<std::string> preprocessor_options;
272 std::list<std::string> include_paths;
273 std::list<std::string> include_files;
274
275 enum class libt
276 {
279 };
281
283 bool malloc_may_fail = true;
284
291
293
294 static const std::size_t default_object_bits = 8;
295
299 std::optional<mp_integer> max_argc;
301
302 struct cppt
303 {
313
315 {
317 }
319 {
321 }
323 {
325 }
327 {
329 }
331 {
333 }
334
335 static const std::size_t default_object_bits = 8;
337
338 struct verilogt
339 {
340 std::list<std::string> include_paths;
342
343 struct javat
344 {
345 typedef std::list<std::string> classpatht;
348
349 static const std::size_t default_object_bits = 16;
351
353 {
354 // number of bits to encode heap object addresses
355 std::size_t object_bits = 8;
358
359 // this is the function to start executing
360 std::optional<std::string> main;
361
362 void set_arch(const irep_idt &);
363
365
366 bool set(const cmdlinet &cmdline);
367
369 std::string object_bits_info();
371
374
375private:
376 void set_classpath(const std::string &cp);
377};
378
379extern configt config;
380
381#endif // CPROVER_UTIL_CONFIG_H
configt config
Definition config.cpp:25
Globally accessible architectural configuration.
Definition config.h:132
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
Definition config.cpp:1406
void set_arch(const irep_idt &)
Definition config.cpp:763
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
Definition config.cpp:863
struct configt::verilogt verilog
std::string object_bits_info()
Definition config.cpp:1431
void set_classpath(const std::string &cp)
Definition config.cpp:1530
mp_integer max_malloc_size() const
The maximum allocation size is determined by the number of bits that are left in the pointer of width...
Definition config.cpp:1587
void set_from_symbol_table(const symbol_table_baset &)
Definition config.cpp:1347
static irep_idt this_architecture()
Definition config.cpp:1442
std::optional< std::string > main
Definition config.h:360
struct configt::javat java
struct configt::cppt cpp
static irep_idt this_operating_system()
Definition config.cpp:1546
struct configt::ansi_ct ansi_c
The symbol table base class interface.
BigInt mp_integer
Definition smt_terms.h:17
std::size_t long_double_width
Definition config.h:146
std::list< std::string > include_paths
Definition config.h:272
bool for_has_scope
Definition config.h:151
void set_arch_spec_x32()
Definition config.cpp:560
enum configt::ansi_ct::c_standardt c_standard
void set_arch_spec_riscv64()
Definition config.cpp:406
endiannesst endianness
Definition config.h:209
bool float16_type
Definition config.h:155
void set_arch_spec_sh4()
Definition config.cpp:648
void set_arch_spec_loongarch64()
Definition config.cpp:678
void set_ILP32()
int=32, long=32, pointer=32
Definition config.cpp:111
bool ts_18661_3_Floatn_types
Definition config.h:152
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition config.cpp:596
bool wchar_t_is_unsigned
Definition config.h:150
void set_arch_spec_hppa()
Definition config.cpp:619
static std::string os_to_string(ost)
Definition config.cpp:1268
std::size_t pointer_width
Definition config.h:143
bool gcc__float128_type
Definition config.h:153
std::optional< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...
Definition config.h:299
void set_c89()
Definition config.h:167
std::list< std::string > include_files
Definition config.h:273
void set_ILP64()
int=64, long=64, pointer=64
Definition config.cpp:71
irep_idt arch
Definition config.h:223
std::list< std::string > undefines
Definition config.h:270
ieee_floatt::rounding_modet rounding_mode
Definition config.h:183
bool __float128_is_keyword
Definition config.h:154
std::list< std::string > preprocessor_options
Definition config.h:271
void set_arch_spec_sparc(const irep_idt &subarch)
Definition config.cpp:489
static ost string_to_os(const std::string &)
Definition config.cpp:1283
std::list< std::string > defines
Definition config.h:269
void set_c99()
Definition config.h:172
bool single_precision_constant
Definition config.h:158
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:147
preprocessort preprocessor
Definition config.h:267
@ malloc_failure_mode_return_null
Definition config.h:288
@ malloc_failure_mode_none
Definition config.h:287
@ malloc_failure_mode_assert_then_assume
Definition config.h:289
std::size_t double_width
Definition config.h:145
bool malloc_may_fail
Definition config.h:283
bool char_is_unsigned
Definition config.h:150
static c_standardt default_c_standard()
Definition config.cpp:736
void set_arch_spec_alpha()
Definition config.cpp:327
std::size_t alignment
Definition config.h:197
void set_arch_spec_power(const irep_idt &subarch)
Definition config.cpp:220
std::size_t bool_width
Definition config.h:139
bool string_abstraction
Definition config.h:282
void set_arch_spec_s390()
Definition config.cpp:432
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:201
std::size_t long_long_int_width
Definition config.h:142
void set_arch_spec_s390x()
Definition config.cpp:461
bool NULL_is_zero
Definition config.h:226
std::size_t long_int_width
Definition config.h:138
void set_arch_spec_mips(const irep_idt &subarch)
Definition config.cpp:356
std::size_t single_width
Definition config.h:144
void set_arch_spec_i386()
Definition config.cpp:150
std::size_t short_int_width
Definition config.h:141
std::size_t char_width
Definition config.h:140
void set_c11()
Definition config.h:177
static const std::size_t default_object_bits
Definition config.h:294
flavourt mode
Definition config.h:256
std::size_t int_width
Definition config.h:137
malloc_failure_modet malloc_failure_mode
Definition config.h:292
void set_arch_spec_ia64()
Definition config.cpp:529
void set_arch_spec_emscripten()
Definition config.cpp:707
bool is_object_bits_default
Definition config.h:356
std::size_t object_bits
Definition config.h:355
void set_cpp14()
Definition config.h:326
enum configt::cppt::cpp_standardt cpp_standard
void set_cpp11()
Definition config.h:322
static const std::size_t default_object_bits
Definition config.h:335
void set_cpp17()
Definition config.h:330
void set_cpp03()
Definition config.h:318
static cpp_standardt default_cpp_standard()
Definition config.cpp:751
void set_cpp98()
Definition config.h:314
classpatht classpath
Definition config.h:346
std::list< std::string > classpatht
Definition config.h:345
irep_idt main_class
Definition config.h:347
static const std::size_t default_object_bits
Definition config.h:349
std::list< std::string > include_paths
Definition config.h:340
dstringt irep_idt