cprover
config.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
18 class cmdlinet;
19 class symbol_tablet;
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 // clang-format off
25 #define OPT_CONFIG_C_CPP \
26  "D:I:(include)(function)" \
27  "(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
28  "(unsigned-char)" \
29  "(round-to-even)(round-to-nearest)" \
30  "(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
31  "(no-library)" \
32 
33 #define HELP_CONFIG_C_CPP \
34  " -I path set include path (C/C++)\n" \
35  " -D macro define preprocessor macro (C/C++)\n" \
36  " --c89/99/11 set C language standard (default: " \
37  << (configt::ansi_ct::default_c_standard()== \
38  configt::ansi_ct::c_standardt::C89?"c89": \
39  configt::ansi_ct::default_c_standard()== \
40  configt::ansi_ct::c_standardt::C99?"c99": \
41  configt::ansi_ct::default_c_standard()== \
42  configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n"\
43  " --cpp98/03/11 set C++ language standard (default: " \
44  << (configt::cppt::default_cpp_standard()== \
45  configt::cppt::cpp_standardt::CPP98?"cpp98":\
46  configt::cppt::default_cpp_standard()== \
47  configt::cppt::cpp_standardt::CPP03?"cpp03":\
48  configt::cppt::default_cpp_standard()== \
49  configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n"\
50  " --unsigned-char make \"char\" unsigned by default\n" \
51  " --round-to-nearest rounding towards nearest even (default)\n" \
52  " --round-to-plus-inf rounding towards plus infinity\n" \
53  " --round-to-minus-inf rounding towards minus infinity\n" \
54  " --round-to-zero rounding towards zero\n" \
55  " --no-library disable built-in abstract C library\n" \
56 
57 
58 #define OPT_CONFIG_LIBRARY \
59  "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \
60  "(string-abstraction)" \
61 
62 #define HELP_CONFIG_LIBRARY \
63 " --malloc-may-fail allow malloc calls to return a null pointer\n" \
64 " --malloc-fail-assert set malloc failure mode to assert-then-assume\n"\
65 " --malloc-fail-null set malloc failure mode to return null\n" \
66 
67 
68 #define OPT_CONFIG_JAVA \
69  "(classpath)(cp)(main-class)" \
70 
71 
72 #define OPT_CONFIG_PLATFORM \
73  "(arch):(os):" \
74  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
75  "(little-endian)(big-endian)" \
76  "(i386-linux)" \
77  "(i386-win32)(win32)(winx64)" \
78  "(i386-macos)(ppc-macos)" \
79  "(gcc)" \
80 
81 #define HELP_CONFIG_PLATFORM \
82  " --arch set architecture (default: " \
83  << configt::this_architecture() << ")\n" \
84  " --os set operating system (default: " \
85  << configt::this_operating_system() << ")\n" \
86  " --16, --32, --64 set width of int\n" \
87  " --LP64, --ILP64, --LLP64,\n" \
88  " --ILP32, --LP32 set width of int, long and pointers\n" \
89  " --little-endian allow little-endian word-byte conversions\n" \
90  " --big-endian allow big-endian word-byte conversions\n" \
91  " --gcc use GCC as preprocessor\n" \
92 
93 #define OPT_CONFIG_BACKEND \
94  "(object-bits):" \
95 
96 #define HELP_CONFIG_BACKEND \
97  " --object-bits n number of bits used for object addresses\n"
98 
99 // clang-format on
100 
103 class configt
104 {
105 public:
106  struct ansi_ct
107  {
108  // for ANSI-C
109  std::size_t int_width;
110  std::size_t long_int_width;
111  std::size_t bool_width;
112  std::size_t char_width;
113  std::size_t short_int_width;
114  std::size_t long_long_int_width;
115  std::size_t pointer_width;
116  std::size_t single_width;
117  std::size_t double_width;
118  std::size_t long_double_width;
119  std::size_t wchar_t_width;
120 
121  // various language options
124  bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
125  bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5
127  enum class c_standardt
128  {
129  C89,
130  C99,
131  C11
134 
135  void set_c89()
136  {
138  for_has_scope = false;
139  }
140  void set_c99()
141  {
143  for_has_scope = true;
144  }
145  void set_c11()
146  {
148  for_has_scope = true;
149  }
150 
152 
153  void set_16();
154  void set_32();
155  void set_64();
156 
157  // http://www.unix.org/version2/whatsnew/lp64_wp.html
158  void set_LP64(); // int=32, long=64, pointer=64
159  void set_ILP64(); // int=64, long=64, pointer=64
160  void set_LLP64(); // int=32, long=32, pointer=64
161  void set_ILP32(); // int=32, long=32, pointer=32
162  void set_LP32(); // int=16, long=32, pointer=32
163 
164  // minimum alignment (in structs) measured in bytes
165  std::size_t alignment;
166 
167  // maximum minimum size of the operands for a machine
168  // instruction (in bytes)
169  std::size_t memory_operand_size;
170 
171  enum class endiannesst
172  {
176  };
178 
179  enum class ost
180  {
181  NO_OS,
182  OS_LINUX,
183  OS_MACOS,
184  OS_WIN
185  };
187 
188  static std::string os_to_string(ost);
189  static ost string_to_os(const std::string &);
190 
192 
193  // architecture-specific integer value of null pointer constant
195 
196  void set_arch_spec_i386();
197  void set_arch_spec_x86_64();
198  void set_arch_spec_power(const irep_idt &subarch);
199  void set_arch_spec_arm(const irep_idt &subarch);
200  void set_arch_spec_alpha();
201  void set_arch_spec_mips(const irep_idt &subarch);
202  void set_arch_spec_riscv64();
203  void set_arch_spec_s390();
204  void set_arch_spec_s390x();
205  void set_arch_spec_sparc(const irep_idt &subarch);
206  void set_arch_spec_ia64();
207  void set_arch_spec_x32();
208  void set_arch_spec_v850();
209  void set_arch_spec_hppa();
210  void set_arch_spec_sh4();
211 
212  enum class flavourt
213  {
214  NONE,
215  ANSI,
216  GCC,
217  ARM,
218  CLANG,
221  };
222  flavourt mode; // the syntax of source files
223 
224  enum class preprocessort
225  {
226  NONE,
227  GCC,
228  CLANG,
230  CODEWARRIOR,
231  ARM
232  };
233  preprocessort preprocessor; // the preprocessor to use
234 
235  std::list<std::string> defines;
236  std::list<std::string> undefines;
237  std::list<std::string> preprocessor_options;
238  std::list<std::string> include_paths;
239  std::list<std::string> include_files;
240 
241  enum class libt
242  {
243  LIB_NONE,
244  LIB_FULL
245  };
247 
249  bool malloc_may_fail = false;
250 
252  {
256  };
257 
259 
260  static const std::size_t default_object_bits = 8;
261 
267 
268  struct cppt
269  {
270  enum class cpp_standardt
271  {
272  CPP98,
273  CPP03,
274  CPP11,
275  CPP14,
276  CPP17
279 
280  void set_cpp98()
281  {
283  }
284  void set_cpp03()
285  {
287  }
288  void set_cpp11()
289  {
291  }
292  void set_cpp14()
293  {
295  }
296  void set_cpp17()
297  {
299  }
300 
301  static const std::size_t default_object_bits = 8;
302  } cpp;
303 
304  struct verilogt
305  {
306  std::list<std::string> include_paths;
308 
309  struct javat
310  {
311  typedef std::list<std::string> classpatht;
314 
315  static const std::size_t default_object_bits = 16;
316  } java;
317 
319  {
320  // number of bits to encode heap object addresses
321  std::size_t object_bits = 8;
324 
325  // this is the function to start executing
327 
328  void set_arch(const irep_idt &);
329 
330  void set_from_symbol_table(const symbol_tablet &);
331 
332  bool set(const cmdlinet &cmdline);
333 
335  std::string object_bits_info();
336 
337  static irep_idt this_architecture();
339 
340 private:
341  void set_classpath(const std::string &cp);
342 };
343 
344 extern configt config;
345 
346 #endif // CPROVER_UTIL_CONFIG_H
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
struct configt::verilogt verilog
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
The symbol table.
Definition: symbol_table.h:14
configt config
Definition: config.cpp:25
nonstd::optional< T > optionalt
Definition: optional.h:35
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
std::list< std::string > undefines
Definition: config.h:236
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:151
void set_64()
Definition: config.cpp:37
std::list< std::string > preprocessor_options
Definition: config.h:237
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_none
Definition: config.h:253
@ 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
void set_cpp14()
Definition: config.h:292
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_cpp17()
Definition: config.h:296
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
std::list< std::string > classpatht
Definition: config.h:311
irep_idt main_class
Definition: config.h:313
static const std::size_t default_object_bits
Definition: config.h:315
std::list< std::string > include_paths
Definition: config.h:306