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)(c17)(c23)(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},\n {y--c17}, {y--c23} \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 : configt::ansi_ct::default_c_standard() == \
49 configt::ansi_ct::c_standardt::C17 \
50 ? "c17" \
51 : configt::ansi_ct::default_c_standard() == \
52 configt::ansi_ct::c_standardt::C23 \
53 ? "c23" \
54 : "") + \
55 ")\n" \
56 " {y--cpp98}, {y--cpp03}, {y--cpp11} \t " \
57 "set C++ language standard (default: " + \
58 std::string( \
59 configt::cppt::default_cpp_standard() == \
60 configt::cppt::cpp_standardt::CPP98 \
61 ? "cpp98" \
62 : configt::cppt::default_cpp_standard() == \
63 configt::cppt::cpp_standardt::CPP03 \
64 ? "cpp03" \
65 : configt::cppt::default_cpp_standard() == \
66 configt::cppt::cpp_standardt::CPP11 \
67 ? "cpp11" \
68 : "") + \
69 ")\n" \
70 " {y--unsigned-char} \t make \"char\" unsigned by default\n" \
71 " {y--round-to-nearest}, {y--round-to-even} \t " \
72 "rounding towards nearest even (default)\n" \
73 " {y--round-to-plus-inf} \t rounding towards plus infinity\n" \
74 " {y--round-to-minus-inf} \t rounding towards minus infinity\n" \
75 " {y--round-to-zero} \t rounding towards zero\n" \
76 " {y--no-library} \t disable built-in abstract C library\n"
77
78#define OPT_CONFIG_LIBRARY \
79 "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \
80 "(no-malloc-may-fail)" \
81 "(string-abstraction)"
82
83#define HELP_CONFIG_LIBRARY \
84 " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n" \
85 " {y--no-malloc-may-fail} \t disable potential malloc failure\n" \
86 " {y--malloc-fail-assert} \t " \
87 "set malloc failure mode to assert-then-assume\n" \
88 " {y--malloc-fail-null} \t set malloc failure mode to return null\n" \
89 " {y--string-abstraction} \t track C string lengths and zero-termination\n"
90
91#define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)"
92
93#define OPT_CONFIG_PLATFORM \
94 "(arch):(os):" \
95 "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
96 "(little-endian)(big-endian)" \
97 "(i386-linux)" \
98 "(i386-win32)(win32)(winx64)" \
99 "(i386-macos)(ppc-macos)" \
100 "(gcc)"
101
102#define HELP_CONFIG_PLATFORM \
103 " {y--arch} {uarch_name} \t " \
104 "set architecture (default: " + \
105 id2string(configt::this_architecture()) + \
106 ") to one of: {yalpha}, {yarm}, {yarm64}, {yarmel}, {yarmhf}, {yhppa}, " \
107 "{yi386}, {yia64}, {ymips}, {ymips64}, {ymips64el}, {ymipsel}, " \
108 "{ymipsn32}, " \
109 "{ymipsn32el}, {ypowerpc}, {yppc64}, {yppc64le}, {yriscv64}, {ys390}, " \
110 "{ys390x}, {ysh4}, {ysparc}, {ysparc64}, {yv850}, {yx32}, {yx86_64}, or " \
111 "{ynone}\n" \
112 " {y--os} {uos_name} \t " \
113 "set operating system (default: " + \
114 id2string(configt::this_operating_system()) + \
115 ") to one of: {yfreebsd}, {ylinux}, {ymacos}, {ynetbsd}, {yopenbsd}, " \
116 "{ysolaris}, {yhurd}, or {ywindows}\n" \
117 " {y--i386-linux}, {y--i386-win32}, {y--i386-macos}, {y--ppc-macos}, " \
118 "{y--win32}, {y--winx64} \t " \
119 "set architecture and operating system\n" \
120 " {y--LP64}, {y--ILP64}, {y--LLP64}, {y--ILP32}, {y--LP32} \t " \
121 "set width of int, long and pointers, but don't override default " \
122 "architecture and operating system\n" \
123 " {y--16}, {y--32}, {y--64} \t " \
124 "equivalent to {y--LP32}, {y--ILP32}, {y--LP64} (on Windows: " \
125 "{y--LLP64})\n" \
126 " {y--little-endian} \t allow little-endian word-byte conversions\n" \
127 " {y--big-endian} \t allow big-endian word-byte conversions\n" \
128 " {y--gcc} \t use GCC as preprocessor\n"
129
130#define OPT_CONFIG_BACKEND "(object-bits):"
131
132#define HELP_CONFIG_BACKEND \
133 " {y--object-bits} {un} \t number of bits used for object addresses\n"
134
138{
139public:
140 struct ansi_ct
141 {
142 // for ANSI-C
143 std::size_t int_width;
144 std::size_t long_int_width;
145 std::size_t bool_width;
146 std::size_t char_width;
147 std::size_t short_int_width;
149 std::size_t pointer_width;
150 std::size_t single_width;
151 std::size_t double_width;
152 std::size_t long_double_width;
153 std::size_t wchar_t_width;
154
155 // various language options
158 bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
159 bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5
160 bool __float128_is_keyword; // __float128 as a keyword (and not typedef)
161 bool float16_type; // _Float16 (Clang >= 15, GCC >= 12)
162 bool bf16_type; // __bf16 (Clang >= 15, GCC >= 13)
163 bool fp16_type; // __fp16 (GCC >= 4.5 on ARM, Clang >= 6)
174
175 void set_c89()
176 {
178 for_has_scope = false;
179 }
180 void set_c99()
181 {
183 for_has_scope = true;
184 }
185 void set_c11()
186 {
188 for_has_scope = true;
189 }
190 void set_c17()
191 {
193 for_has_scope = true;
194 }
195 void set_c23()
196 {
198 for_has_scope = true;
199 }
200
202
203 void set_16();
204 void set_32();
205 void set_64();
206
207 // http://www.unix.org/version2/whatsnew/lp64_wp.html
208 void set_LP64(); // int=32, long=64, pointer=64
209 void set_ILP64(); // int=64, long=64, pointer=64
210 void set_LLP64(); // int=32, long=32, pointer=64
211 void set_ILP32(); // int=32, long=32, pointer=32
212 void set_LP32(); // int=16, long=32, pointer=32
213
214 // minimum alignment (in structs) measured in bytes
215 std::size_t alignment;
216
217 // maximum minimum size of the operands for a machine
218 // instruction (in bytes)
220
228
237
238 static std::string os_to_string(ost);
239 static ost string_to_os(const std::string &);
240
242
243 // architecture-specific integer value of null pointer constant
245
246 void set_arch_spec_i386();
248 void set_arch_spec_power(const irep_idt &subarch);
249 void set_arch_spec_arm(const irep_idt &subarch);
250 void set_arch_spec_alpha();
251 void set_arch_spec_mips(const irep_idt &subarch);
253 void set_arch_spec_s390();
254 void set_arch_spec_s390x();
255 void set_arch_spec_sparc(const irep_idt &subarch);
256 void set_arch_spec_ia64();
257 void set_arch_spec_x32();
258 void set_arch_spec_v850();
259 void set_arch_spec_hppa();
260 void set_arch_spec_sh4();
263
274 flavourt mode; // the syntax of source files
275
285 preprocessort preprocessor; // the preprocessor to use
286
287 std::list<std::string> defines;
288 std::list<std::string> undefines;
289 std::list<std::string> preprocessor_options;
290 std::list<std::string> include_paths;
291 std::list<std::string> include_files;
292
293 enum class libt
294 {
297 };
299
301 bool malloc_may_fail = true;
302
309
311
312 static const std::size_t default_object_bits = 8;
313
317 std::optional<mp_integer> max_argc;
319
320 struct cppt
321 {
331
333 {
335 }
337 {
339 }
341 {
343 }
345 {
347 }
349 {
351 }
352
353 static const std::size_t default_object_bits = 8;
355
356 struct verilogt
357 {
358 std::list<std::string> include_paths;
360
361 struct javat
362 {
363 typedef std::list<std::string> classpatht;
366
367 static const std::size_t default_object_bits = 16;
369
371 {
372 // number of bits to encode heap object addresses
373 std::size_t object_bits = 8;
376
377 // this is the function to start executing
378 std::optional<std::string> main;
379
380 void set_arch(const irep_idt &);
381
383
384 bool set(const cmdlinet &cmdline);
385
387 std::string object_bits_info();
389
392
393private:
394 void set_classpath(const std::string &cp);
395};
396
397extern configt config;
398
399#endif // CPROVER_UTIL_CONFIG_H
configt config
Definition config.cpp:25
Globally accessible architectural configuration.
Definition config.h:138
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
Definition config.cpp:1412
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:1437
void set_classpath(const std::string &cp)
Definition config.cpp:1536
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:1593
void set_from_symbol_table(const symbol_table_baset &)
Definition config.cpp:1353
static irep_idt this_architecture()
Definition config.cpp:1448
std::optional< std::string > main
Definition config.h:378
struct configt::javat java
struct configt::cppt cpp
static irep_idt this_operating_system()
Definition config.cpp:1552
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:152
std::list< std::string > include_paths
Definition config.h:290
bool for_has_scope
Definition config.h:157
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
void set_c23()
Definition config.h:195
endiannesst endianness
Definition config.h:227
bool float16_type
Definition config.h:161
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:158
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:156
void set_arch_spec_hppa()
Definition config.cpp:619
static std::string os_to_string(ost)
Definition config.cpp:1274
std::size_t pointer_width
Definition config.h:149
bool gcc__float128_type
Definition config.h:159
std::optional< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...
Definition config.h:317
void set_c89()
Definition config.h:175
std::list< std::string > include_files
Definition config.h:291
void set_ILP64()
int=64, long=64, pointer=64
Definition config.cpp:71
irep_idt arch
Definition config.h:241
std::list< std::string > undefines
Definition config.h:288
ieee_floatt::rounding_modet rounding_mode
Definition config.h:201
bool __float128_is_keyword
Definition config.h:160
std::list< std::string > preprocessor_options
Definition config.h:289
void set_arch_spec_sparc(const irep_idt &subarch)
Definition config.cpp:489
static ost string_to_os(const std::string &)
Definition config.cpp:1289
std::list< std::string > defines
Definition config.h:287
void set_c99()
Definition config.h:180
bool single_precision_constant
Definition config.h:164
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:153
preprocessort preprocessor
Definition config.h:285
@ malloc_failure_mode_return_null
Definition config.h:306
@ malloc_failure_mode_none
Definition config.h:305
@ malloc_failure_mode_assert_then_assume
Definition config.h:307
std::size_t double_width
Definition config.h:151
bool malloc_may_fail
Definition config.h:301
bool char_is_unsigned
Definition config.h:156
static c_standardt default_c_standard()
Definition config.cpp:736
void set_arch_spec_alpha()
Definition config.cpp:327
void set_c17()
Definition config.h:190
std::size_t alignment
Definition config.h:215
void set_arch_spec_power(const irep_idt &subarch)
Definition config.cpp:220
std::size_t bool_width
Definition config.h:145
bool string_abstraction
Definition config.h:300
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:219
std::size_t long_long_int_width
Definition config.h:148
void set_arch_spec_s390x()
Definition config.cpp:461
bool NULL_is_zero
Definition config.h:244
std::size_t long_int_width
Definition config.h:144
void set_arch_spec_mips(const irep_idt &subarch)
Definition config.cpp:356
std::size_t single_width
Definition config.h:150
void set_arch_spec_i386()
Definition config.cpp:150
std::size_t short_int_width
Definition config.h:147
std::size_t char_width
Definition config.h:146
void set_c11()
Definition config.h:185
static const std::size_t default_object_bits
Definition config.h:312
flavourt mode
Definition config.h:274
std::size_t int_width
Definition config.h:143
malloc_failure_modet malloc_failure_mode
Definition config.h:310
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:374
std::size_t object_bits
Definition config.h:373
void set_cpp14()
Definition config.h:344
enum configt::cppt::cpp_standardt cpp_standard
void set_cpp11()
Definition config.h:340
static const std::size_t default_object_bits
Definition config.h:353
void set_cpp17()
Definition config.h:348
void set_cpp03()
Definition config.h:336
static cpp_standardt default_cpp_standard()
Definition config.cpp:751
void set_cpp98()
Definition config.h:332
classpatht classpath
Definition config.h:364
std::list< std::string > classpatht
Definition config.h:363
irep_idt main_class
Definition config.h:365
static const std::size_t default_object_bits
Definition config.h:367
std::list< std::string > include_paths
Definition config.h:358
dstringt irep_idt