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 <list>
13
14#include "ieee_float.h"
15#include "irep.h"
16#include "optional.h"
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 "(string-abstraction)"
75
76#define HELP_CONFIG_LIBRARY \
77 " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n" \
78 " {y--malloc-fail-assert} \t " \
79 "set malloc failure mode to assert-then-assume\n" \
80 " {y--malloc-fail-null} \t set malloc failure mode to return null\n" \
81 " {y--string-abstraction} \t track C string lengths and zero-termination\n"
82
83#define OPT_CONFIG_JAVA "(classpath)(cp)(main-class)"
84
85#define OPT_CONFIG_PLATFORM \
86 "(arch):(os):" \
87 "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
88 "(little-endian)(big-endian)" \
89 "(i386-linux)" \
90 "(i386-win32)(win32)(winx64)" \
91 "(i386-macos)(ppc-macos)" \
92 "(gcc)"
93
94#define HELP_CONFIG_PLATFORM \
95 " {y--arch} {uarch_name} \t " \
96 "set architecture (default: " + \
97 id2string(configt::this_architecture()) + \
98 ") to one of: {yalpha}, {yarm}, {yarm64}, {yarmel}, {yarmhf}, {yhppa}, " \
99 "{yi386}, {yia64}, {ymips}, {ymips64}, {ymips64el}, {ymipsel}, " \
100 "{ymipsn32}, " \
101 "{ymipsn32el}, {ypowerpc}, {yppc64}, {yppc64le}, {yriscv64}, {ys390}, " \
102 "{ys390x}, {ysh4}, {ysparc}, {ysparc64}, {yv850}, {yx32}, {yx86_64}, or " \
103 "{ynone}\n" \
104 " {y--os} {uos_name} \t " \
105 "set operating system (default: " + \
106 id2string(configt::this_operating_system()) + \
107 ") to one of: {yfreebsd}, {ylinux}, {ymacos}, {ysolaris}, or {ywindows}\n" \
108 " {y--i386-linux}, {y--i386-win32}, {y--i386-macos}, {y--ppc-macos}, " \
109 "{y--win32}, {y--winx64} \t " \
110 "set architecture and operating system\n" \
111 " {y--LP64}, {y--ILP64}, {y--LLP64}, {y--ILP32}, {y--LP32} \t " \
112 "set width of int, long and pointers, but don't override default " \
113 "architecture and operating system\n" \
114 " {y--16}, {y--32}, {y--64} \t " \
115 "equivalent to {y--LP32}, {y--ILP32}, {y--LP64} (on Windows: " \
116 "{y--LLP64})\n" \
117 " {y--little-endian} \t allow little-endian word-byte conversions\n" \
118 " {y--big-endian} \t allow big-endian word-byte conversions\n" \
119 " {y--gcc} \t use GCC as preprocessor\n"
120
121#define OPT_CONFIG_BACKEND "(object-bits):"
122
123#define HELP_CONFIG_BACKEND \
124 " {y--object-bits} {un} \t number of bits used for object addresses\n"
125
129{
130public:
131 struct ansi_ct
132 {
133 // for ANSI-C
134 std::size_t int_width;
135 std::size_t long_int_width;
136 std::size_t bool_width;
137 std::size_t char_width;
138 std::size_t short_int_width;
140 std::size_t pointer_width;
141 std::size_t single_width;
142 std::size_t double_width;
143 std::size_t long_double_width;
144 std::size_t wchar_t_width;
145
146 // various language options
149 bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
150 bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5
151 bool float16_type; // _Float16 (Clang >= 15, GCC >= 12)
152 bool bf16_type; // __bf16 (Clang >= 15, GCC >= 13)
154 enum class c_standardt
155 {
156 C89,
157 C99,
158 C11
161
162 void set_c89()
163 {
165 for_has_scope = false;
166 }
167 void set_c99()
168 {
170 for_has_scope = true;
171 }
172 void set_c11()
173 {
175 for_has_scope = true;
176 }
177
179
180 void set_16();
181 void set_32();
182 void set_64();
183
184 // http://www.unix.org/version2/whatsnew/lp64_wp.html
185 void set_LP64(); // int=32, long=64, pointer=64
186 void set_ILP64(); // int=64, long=64, pointer=64
187 void set_LLP64(); // int=32, long=32, pointer=64
188 void set_ILP32(); // int=32, long=32, pointer=32
189 void set_LP32(); // int=16, long=32, pointer=32
190
191 // minimum alignment (in structs) measured in bytes
192 std::size_t alignment;
193
194 // maximum minimum size of the operands for a machine
195 // instruction (in bytes)
197
198 enum class endiannesst
199 {
203 };
205
206 enum class ost
207 {
208 NO_OS,
209 OS_LINUX,
210 OS_MACOS,
211 OS_WIN
212 };
214
215 static std::string os_to_string(ost);
216 static ost string_to_os(const std::string &);
217
219
220 // architecture-specific integer value of null pointer constant
222
223 void set_arch_spec_i386();
225 void set_arch_spec_power(const irep_idt &subarch);
226 void set_arch_spec_arm(const irep_idt &subarch);
227 void set_arch_spec_alpha();
228 void set_arch_spec_mips(const irep_idt &subarch);
230 void set_arch_spec_s390();
231 void set_arch_spec_s390x();
232 void set_arch_spec_sparc(const irep_idt &subarch);
233 void set_arch_spec_ia64();
234 void set_arch_spec_x32();
235 void set_arch_spec_v850();
236 void set_arch_spec_hppa();
237 void set_arch_spec_sh4();
238
239 enum class flavourt
240 {
241 NONE,
242 ANSI,
243 GCC,
244 ARM,
245 CLANG,
248 };
249 flavourt mode; // the syntax of source files
250
251 enum class preprocessort
252 {
253 NONE,
254 GCC,
255 CLANG,
258 ARM
259 };
260 preprocessort preprocessor; // the preprocessor to use
261
262 std::list<std::string> defines;
263 std::list<std::string> undefines;
264 std::list<std::string> preprocessor_options;
265 std::list<std::string> include_paths;
266 std::list<std::string> include_files;
267
268 enum class libt
269 {
270 LIB_NONE,
272 };
274
276 bool malloc_may_fail = false;
277
284
286
287 static const std::size_t default_object_bits = 8;
288
294
295 struct cppt
296 {
297 enum class cpp_standardt
298 {
299 CPP98,
300 CPP03,
301 CPP11,
302 CPP14,
303 CPP17
306
308 {
310 }
312 {
314 }
316 {
318 }
320 {
322 }
324 {
326 }
327
328 static const std::size_t default_object_bits = 8;
330
331 struct verilogt
332 {
333 std::list<std::string> include_paths;
335
336 struct javat
337 {
338 typedef std::list<std::string> classpatht;
341
342 static const std::size_t default_object_bits = 16;
344
346 {
347 // number of bits to encode heap object addresses
348 std::size_t object_bits = 8;
351
352 // this is the function to start executing
354
355 void set_arch(const irep_idt &);
356
358
359 bool set(const cmdlinet &cmdline);
360
362 std::string object_bits_info();
363
366
367private:
368 void set_classpath(const std::string &cp);
369};
370
371extern configt config;
372
373#endif // CPROVER_UTIL_CONFIG_H
Globally accessible architectural configuration.
Definition config.h:129
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
Definition config.cpp:1317
void set_arch(const irep_idt &)
Definition config.cpp:702
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
Definition config.cpp:798
optionalt< std::string > main
Definition config.h:353
struct configt::verilogt verilog
std::string object_bits_info()
Definition config.cpp:1342
void set_classpath(const std::string &cp)
Definition config.cpp:1437
void set_from_symbol_table(const symbol_table_baset &)
Definition config.cpp:1258
static irep_idt this_architecture()
Definition config.cpp:1353
struct configt::javat java
struct configt::cppt cpp
static irep_idt this_operating_system()
Definition config.cpp:1453
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:39
The symbol table base class interface.
configt config
Definition config.cpp:25
nonstd::optional< T > optionalt
Definition optional.h:35
std::size_t long_double_width
Definition config.h:143
std::list< std::string > include_paths
Definition config.h:265
bool for_has_scope
Definition config.h:148
optionalt< mp_integer > max_argc
Maximum value of argc, which is operating-systems dependent: Windows limits the number of characters ...
Definition config.h:292
void set_arch_spec_x32()
Definition config.cpp:557
enum configt::ansi_ct::c_standardt c_standard
void set_arch_spec_riscv64()
Definition config.cpp:403
endiannesst endianness
Definition config.h:204
bool float16_type
Definition config.h:151
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:149
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:147
void set_arch_spec_hppa()
Definition config.cpp:616
static std::string os_to_string(ost)
Definition config.cpp:1179
std::size_t pointer_width
Definition config.h:140
bool gcc__float128_type
Definition config.h:150
void set_c89()
Definition config.h:162
std::list< std::string > include_files
Definition config.h:266
void set_ILP64()
int=64, long=64, pointer=64
Definition config.cpp:71
irep_idt arch
Definition config.h:218
std::list< std::string > undefines
Definition config.h:263
ieee_floatt::rounding_modet rounding_mode
Definition config.h:178
std::list< std::string > preprocessor_options
Definition config.h:264
void set_arch_spec_sparc(const irep_idt &subarch)
Definition config.cpp:486
static ost string_to_os(const std::string &)
Definition config.cpp:1194
std::list< std::string > defines
Definition config.h:262
void set_c99()
Definition config.h:167
bool single_precision_constant
Definition config.h:153
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:144
preprocessort preprocessor
Definition config.h:260
@ malloc_failure_mode_return_null
Definition config.h:281
@ malloc_failure_mode_none
Definition config.h:280
@ malloc_failure_mode_assert_then_assume
Definition config.h:282
std::size_t double_width
Definition config.h:142
bool malloc_may_fail
Definition config.h:276
bool char_is_unsigned
Definition config.h:147
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:192
void set_arch_spec_power(const irep_idt &subarch)
Definition config.cpp:220
std::size_t bool_width
Definition config.h:136
bool string_abstraction
Definition config.h:275
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:196
std::size_t long_long_int_width
Definition config.h:139
void set_arch_spec_s390x()
Definition config.cpp:458
bool NULL_is_zero
Definition config.h:221
std::size_t long_int_width
Definition config.h:135
void set_arch_spec_mips(const irep_idt &subarch)
Definition config.cpp:353
std::size_t single_width
Definition config.h:141
void set_arch_spec_i386()
Definition config.cpp:150
std::size_t short_int_width
Definition config.h:138
std::size_t char_width
Definition config.h:137
void set_c11()
Definition config.h:172
static const std::size_t default_object_bits
Definition config.h:287
flavourt mode
Definition config.h:249
std::size_t int_width
Definition config.h:134
malloc_failure_modet malloc_failure_mode
Definition config.h:285
void set_arch_spec_ia64()
Definition config.cpp:526
bool is_object_bits_default
Definition config.h:349
std::size_t object_bits
Definition config.h:348
void set_cpp14()
Definition config.h:319
enum configt::cppt::cpp_standardt cpp_standard
void set_cpp11()
Definition config.h:315
static const std::size_t default_object_bits
Definition config.h:328
void set_cpp17()
Definition config.h:323
void set_cpp03()
Definition config.h:311
static cpp_standardt default_cpp_standard()
Definition config.cpp:690
void set_cpp98()
Definition config.h:307
classpatht classpath
Definition config.h:339
std::list< std::string > classpatht
Definition config.h:338
irep_idt main_class
Definition config.h:340
static const std::size_t default_object_bits
Definition config.h:342
std::list< std::string > include_paths
Definition config.h:333