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 
10 #ifndef CPROVER_UTIL_CONFIG_H
11 #define CPROVER_UTIL_CONFIG_H
12 
13 #include <list>
14 
15 #include "ieee_float.h"
16 #include "irep.h"
17 #include "optional.h"
18 
19 class cmdlinet;
20 class symbol_tablet;
21 
22 // Configt is the one place beyond *_parse_options where options are ... parsed.
23 // Options that are handled by configt are documented here.
24 
25 // clang-format off
26 #define OPT_CONFIG_C_CPP \
27  "D:I:(include)(function)" \
28  "(c89)(c99)(c11)(cpp98)(cpp03)(cpp11)" \
29  "(unsigned-char)" \
30  "(round-to-even)(round-to-nearest)" \
31  "(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
32  "(no-library)" \
33 
34 #define HELP_CONFIG_C_CPP \
35  " -I path set include path (C/C++)\n" \
36  " -D macro define preprocessor macro (C/C++)\n" \
37  " --c89/99/11 set C language standard (default: " \
38  << (configt::ansi_ct::default_c_standard()== \
39  configt::ansi_ct::c_standardt::C89?"c89": \
40  configt::ansi_ct::default_c_standard()== \
41  configt::ansi_ct::c_standardt::C99?"c99": \
42  configt::ansi_ct::default_c_standard()== \
43  configt::ansi_ct::c_standardt::C11?"c11":"") << ")\n"\
44  " --cpp98/03/11 set C++ language standard (default: " \
45  << (configt::cppt::default_cpp_standard()== \
46  configt::cppt::cpp_standardt::CPP98?"cpp98":\
47  configt::cppt::default_cpp_standard()== \
48  configt::cppt::cpp_standardt::CPP03?"cpp03":\
49  configt::cppt::default_cpp_standard()== \
50  configt::cppt::cpp_standardt::CPP11?"cpp11":"") << ")\n"\
51  " --unsigned-char make \"char\" unsigned by default\n" \
52  " --round-to-nearest rounding towards nearest even (default)\n" \
53  " --round-to-plus-inf rounding towards plus infinity\n" \
54  " --round-to-minus-inf rounding towards minus infinity\n" \
55  " --round-to-zero rounding towards zero\n" \
56  " --no-library disable built-in abstract C library\n" \
57 
58 
59 #define OPT_CONFIG_LIBRARY \
60  "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)" \
61  "(string-abstraction)" \
62 
63 #define HELP_CONFIG_LIBRARY \
64 " --malloc-may-fail allow malloc calls to return a null pointer\n" \
65 " --malloc-fail-assert set malloc failure mode to assert-then-assume\n"\
66 " --malloc-fail-null set malloc failure mode to return null\n" \
67 
68 
69 #define OPT_CONFIG_JAVA \
70  "(classpath)(cp)(main-class)" \
71 
72 
73 #define OPT_CONFIG_PLATFORM \
74  "(arch):(os):" \
75  "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
76  "(little-endian)(big-endian)" \
77  "(i386-linux)" \
78  "(i386-win32)(win32)(winx64)" \
79  "(i386-macos)(ppc-macos)" \
80  "(gcc)" \
81 
82 #define HELP_CONFIG_PLATFORM \
83  " --arch set architecture (default: " \
84  << configt::this_architecture() << ")\n" \
85  " --os set operating system (default: " \
86  << configt::this_operating_system() << ")\n" \
87  " --16, --32, --64 set width of int\n" \
88  " --LP64, --ILP64, --LLP64,\n" \
89  " --ILP32, --LP32 set width of int, long and pointers\n" \
90  " --little-endian allow little-endian word-byte conversions\n" \
91  " --big-endian allow big-endian word-byte conversions\n" \
92  " --gcc use GCC as preprocessor\n" \
93 
94 #define OPT_CONFIG_BACKEND \
95  "(object-bits):" \
96 
97 #define HELP_CONFIG_BACKEND \
98  " --object-bits n number of bits used for object addresses\n"
99 
100 // clang-format on
101 
104 class configt
105 {
106 public:
107  struct ansi_ct
108  {
109  // for ANSI-C
110  std::size_t int_width;
111  std::size_t long_int_width;
112  std::size_t bool_width;
113  std::size_t char_width;
114  std::size_t short_int_width;
115  std::size_t long_long_int_width;
116  std::size_t pointer_width;
117  std::size_t single_width;
118  std::size_t double_width;
119  std::size_t long_double_width;
120  std::size_t wchar_t_width;
121 
122  // various language options
125  bool ts_18661_3_Floatn_types; // ISO/IEC TS 18661-3:2015
126  bool gcc__float128_type; // __float128, a gcc extension since 4.3/4.5
128  enum class c_standardt { C89, C99, C11 } c_standard;
130 
134 
136 
137  void set_16();
138  void set_32();
139  void set_64();
140 
141  // http://www.unix.org/version2/whatsnew/lp64_wp.html
142  void set_LP64(); // int=32, long=64, pointer=64
143  void set_ILP64(); // int=64, long=64, pointer=64
144  void set_LLP64(); // int=32, long=32, pointer=64
145  void set_ILP32(); // int=32, long=32, pointer=32
146  void set_LP32(); // int=16, long=32, pointer=32
147 
148  // minimum alignment (in structs) measured in bytes
149  std::size_t alignment;
150 
151  // maximum minimum size of the operands for a machine
152  // instruction (in bytes)
153  std::size_t memory_operand_size;
154 
157 
158  enum class ost { NO_OS, OS_LINUX, OS_MACOS, OS_WIN };
160 
161  static std::string os_to_string(ost);
162  static ost string_to_os(const std::string &);
163 
165 
166  // architecture-specific integer value of null pointer constant
168 
169  void set_arch_spec_i386();
170  void set_arch_spec_x86_64();
171  void set_arch_spec_power(const irep_idt &subarch);
172  void set_arch_spec_arm(const irep_idt &subarch);
173  void set_arch_spec_alpha();
174  void set_arch_spec_mips(const irep_idt &subarch);
175  void set_arch_spec_riscv64();
176  void set_arch_spec_s390();
177  void set_arch_spec_s390x();
178  void set_arch_spec_sparc(const irep_idt &subarch);
179  void set_arch_spec_ia64();
180  void set_arch_spec_x32();
181  void set_arch_spec_v850();
182  void set_arch_spec_hppa();
183  void set_arch_spec_sh4();
184 
185  enum class flavourt
186  {
187  NONE,
188  ANSI,
189  GCC,
190  ARM,
191  CLANG,
194  };
195  flavourt mode; // the syntax of source files
196 
198  CODEWARRIOR, ARM };
199  preprocessort preprocessor; // the preprocessor to use
200 
201  std::list<std::string> defines;
202  std::list<std::string> undefines;
203  std::list<std::string> preprocessor_options;
204  std::list<std::string> include_paths;
205  std::list<std::string> include_files;
206 
207  enum class libt { LIB_NONE, LIB_FULL };
209 
211  bool malloc_may_fail = false;
212 
214  {
218  };
219 
221 
222  static const std::size_t default_object_bits=8;
224 
225  struct cppt
226  {
229 
234 
235  static const std::size_t default_object_bits=8;
236  } cpp;
237 
238  struct verilogt
239  {
240  std::list<std::string> include_paths;
242 
243  struct javat
244  {
245  typedef std::list<std::string> classpatht;
248 
249  static const std::size_t default_object_bits=16;
250  } java;
251 
253  {
254  // number of bits to encode heap object addresses
255  std::size_t object_bits = 8;
258 
259  // this is the function to start executing
261 
262  void set_arch(const irep_idt &);
263 
264  void set_from_symbol_table(const symbol_tablet &);
265 
266  bool set(const cmdlinet &cmdline);
267 
269  std::string object_bits_info();
270 
271  static irep_idt this_architecture();
273 
274 private:
275  void set_classpath(const std::string &cp);
276 };
277 
278 extern configt config;
279 
280 #endif // CPROVER_UTIL_CONFIG_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
configt::ansi_ct::ts_18661_3_Floatn_types
bool ts_18661_3_Floatn_types
Definition: config.h:125
configt::cppt::cpp_standardt::CPP98
@ CPP98
configt::bv_encodingt::object_bits
std::size_t object_bits
Definition: config.h:255
configt::ansi_ct::defines
std::list< std::string > defines
Definition: config.h:201
configt::ansi_ct::bool_width
std::size_t bool_width
Definition: config.h:112
configt::verilog
struct configt::verilogt verilog
configt::object_bits_info
std::string object_bits_info()
Definition: config.cpp:1316
configt::ansi_ct::set_c99
void set_c99()
Definition: config.h:132
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
configt::cppt
Definition: config.h:226
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:167
configt::javat::main_class
irep_idt main_class
Definition: config.h:247
configt::ansi_ct::string_to_os
static ost string_to_os(const std::string &)
Definition: config.cpp:1167
configt::ansi_ct::ost
ost
Definition: config.h:158
configt::bv_encoding
struct configt::bv_encodingt bv_encoding
configt::ansi_ct::for_has_scope
bool for_has_scope
Definition: config.h:124
configt::cppt::cpp_standardt
cpp_standardt
Definition: config.h:227
configt::ansi_ct::set_arch_spec_s390x
void set_arch_spec_s390x()
Definition: config.cpp:458
configt::ansi_ct::wchar_t_width
std::size_t wchar_t_width
Definition: config.h:120
configt::ansi_ct::endiannesst
endiannesst
Definition: config.h:155
configt::ansi_ct::ost::OS_MACOS
@ OS_MACOS
configt::ansi_ct::preprocessort::CLANG
@ CLANG
configt::ansi_ct::include_paths
std::list< std::string > include_paths
Definition: config.h:204
configt::ansi_ct::malloc_failure_mode_assert_then_assume
@ malloc_failure_mode_assert_then_assume
Definition: config.h:217
configt::ansi_ct::flavourt::CODEWARRIOR
@ CODEWARRIOR
optional.h
configt::ansi_ct::set_arch_spec_mips
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:353
configt::ansi_ct::os
ost os
Definition: config.h:159
configt::cppt::cpp_standardt::CPP03
@ CPP03
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
configt::ansi_ct::set_32
void set_32()
Definition: config.cpp:32
configt::ansi_ct::set_64
void set_64()
Definition: config.cpp:37
configt::main
optionalt< std::string > main
Definition: config.h:260
configt::ansi_ct::set_arch_spec_i386
void set_arch_spec_i386()
Definition: config.cpp:150
configt::ansi_ct::set_16
void set_16()
Definition: config.cpp:27
configt::ansi_ct::rounding_mode
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:135
configt::ansi_ct::alignment
std::size_t alignment
Definition: config.h:149
configt::ansi_ct::set_LP32
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:131
configt::ansi_ct::set_arch_spec_power
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:220
configt::ansi_ct::undefines
std::list< std::string > undefines
Definition: config.h:202
configt::ansi_c
struct configt::ansi_ct ansi_c
configt::ansi_ct::flavourt::ARM
@ ARM
configt::ansi_ct::set_arch_spec_hppa
void set_arch_spec_hppa()
Definition: config.cpp:616
configt::javat::classpath
classpatht classpath
Definition: config.h:246
configt::ansi_ct::libt::LIB_NONE
@ LIB_NONE
configt::ansi_ct::flavourt::CLANG
@ CLANG
configt::ansi_ct
Definition: config.h:108
configt
Globally accessible architectural configuration.
Definition: config.h:105
configt::ansi_ct::flavourt::NONE
@ NONE
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:113
configt::cppt::set_cpp98
void set_cpp98()
Definition: config.h:230
configt::ansi_ct::endiannesst::NO_ENDIANNESS
@ NO_ENDIANNESS
configt::ansi_ct::set_arch_spec_ia64
void set_arch_spec_ia64()
Definition: config.cpp:526
config
configt config
Definition: config.cpp:25
configt::ansi_ct::libt
libt
Definition: config.h:207
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
configt::bv_encodingt
Definition: config.h:253
configt::ansi_ct::c_standardt::C89
@ C89
configt::cppt::set_cpp14
void set_cpp14()
Definition: config.h:233
cmdlinet
Definition: cmdline.h:21
configt::ansi_ct::set_arch_spec_arm
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:281
configt::ansi_ct::wchar_t_is_unsigned
bool wchar_t_is_unsigned
Definition: config.h:123
configt::ansi_ct::set_arch_spec_s390
void set_arch_spec_s390()
Definition: config.cpp:429
configt::ansi_ct::double_width
std::size_t double_width
Definition: config.h:118
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:199
configt::ansi_ct::malloc_failure_mode_return_null
@ malloc_failure_mode_return_null
Definition: config.h:216
configt::ansi_ct::set_arch_spec_riscv64
void set_arch_spec_riscv64()
Definition: config.cpp:403
configt::verilogt::include_paths
std::list< std::string > include_paths
Definition: config.h:240
configt::ansi_ct::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:222
configt::cppt::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:235
configt::ansi_ct::string_abstraction
bool string_abstraction
Definition: config.h:210
configt::ansi_ct::set_arch_spec_alpha
void set_arch_spec_alpha()
Definition: config.cpp:324
configt::bv_encodingt::is_object_bits_default
bool is_object_bits_default
Definition: config.h:256
configt::cppt::set_cpp11
void set_cpp11()
Definition: config.h:232
configt::ansi_ct::memory_operand_size
std::size_t memory_operand_size
Definition: config.h:153
configt::ansi_ct::ost::OS_LINUX
@ OS_LINUX
configt::ansi_ct::flavourt::ANSI
@ ANSI
configt::ansi_ct::set_ILP64
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:71
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:115
configt::this_operating_system
static irep_idt this_operating_system()
Definition: config.cpp:1427
configt::ansi_ct::malloc_failure_mode_none
@ malloc_failure_mode_none
Definition: config.h:215
configt::javat::classpatht
std::list< std::string > classpatht
Definition: config.h:245
configt::ansi_ct::arch
irep_idt arch
Definition: config.h:164
configt::ansi_ct::ost::OS_WIN
@ OS_WIN
configt::ansi_ct::set_LLP64
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:91
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1231
ieee_floatt::rounding_modet
rounding_modet
Definition: ieee_float.h:124
configt::ansi_ct::os_to_string
static std::string os_to_string(ost)
Definition: config.cpp:1152
configt::javat::default_object_bits
static const std::size_t default_object_bits
Definition: config.h:249
configt::ansi_ct::preprocessor_options
std::list< std::string > preprocessor_options
Definition: config.h:203
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
configt::ansi_ct::include_files
std::list< std::string > include_files
Definition: config.h:205
configt::ansi_ct::ost::NO_OS
@ NO_OS
configt::ansi_ct::preprocessort::GCC
@ GCC
configt::ansi_ct::set_ILP32
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:111
configt::ansi_ct::default_c_standard
static c_standardt default_c_standard()
Definition: config.cpp:675
configt::ansi_ct::c_standardt::C99
@ C99
configt::ansi_ct::preprocessort::NONE
@ NONE
configt::ansi_ct::set_c11
void set_c11()
Definition: config.h:133
configt::this_architecture
static irep_idt this_architecture()
Definition: config.cpp:1327
configt::ansi_ct::libt::LIB_FULL
@ LIB_FULL
configt::verilogt
Definition: config.h:239
configt::ansi_ct::mode
flavourt mode
Definition: config.h:195
configt::ansi_ct::c_standardt::C11
@ C11
preprocessort
Definition: preprocessor.h:21
configt::ansi_ct::set_c89
void set_c89()
Definition: config.h:131
configt::ansi_ct::preprocessort::VISUAL_STUDIO
@ VISUAL_STUDIO
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
configt::set
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
configt::cppt::default_cpp_standard
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
configt::ansi_ct::c_standard
enum configt::ansi_ct::c_standardt c_standard
configt::ansi_ct::set_arch_spec_sparc
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:486
ieee_float.h
configt::ansi_ct::set_LP64
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:47
configt::ansi_ct::set_arch_spec_sh4
void set_arch_spec_sh4()
Definition: config.cpp:645
configt::ansi_ct::long_double_width
std::size_t long_double_width
Definition: config.h:119
configt::java
struct configt::javat java
configt::cppt::cpp_standardt::CPP14
@ CPP14
configt::ansi_ct::set_arch_spec_v850
void set_arch_spec_v850()
Sets up the widths of variables for the Renesas V850.
Definition: config.cpp:593
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:114
configt::ansi_ct::char_is_unsigned
bool char_is_unsigned
Definition: config.h:123
configt::ansi_ct::flavourt::GCC
@ GCC
configt::ansi_ct::set_arch_spec_x86_64
void set_arch_spec_x86_64()
Definition: config.cpp:182
configt::cppt::cpp_standardt::CPP11
@ CPP11
configt::ansi_ct::set_arch_spec_x32
void set_arch_spec_x32()
Definition: config.cpp:557
configt::ansi_ct::malloc_failure_mode
malloc_failure_modet malloc_failure_mode
Definition: config.h:220
configt::ansi_ct::pointer_width
std::size_t pointer_width
Definition: config.h:116
configt::ansi_ct::single_width
std::size_t single_width
Definition: config.h:117
configt::ansi_ct::flavourt
flavourt
Definition: config.h:186
configt::ansi_ct::lib
libt lib
Definition: config.h:208
configt::cpp
struct configt::cppt cpp
configt::ansi_ct::malloc_failure_modet
malloc_failure_modet
Definition: config.h:214
configt::set_classpath
void set_classpath(const std::string &cp)
Definition: config.cpp:1411
configt::ansi_ct::malloc_may_fail
bool malloc_may_fail
Definition: config.h:211
configt::ansi_ct::single_precision_constant
bool single_precision_constant
Definition: config.h:127
configt::ansi_ct::gcc__float128_type
bool gcc__float128_type
Definition: config.h:126
configt::set_object_bits_from_symbol_table
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1291
configt::ansi_ct::c_standardt
c_standardt
Definition: config.h:128
configt::set_arch
void set_arch(const irep_idt &)
Definition: config.cpp:702
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:110
configt::javat
Definition: config.h:244
configt::ansi_ct::preprocessort::ARM
@ ARM
configt::ansi_ct::preprocessort::CODEWARRIOR
@ CODEWARRIOR
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:156
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:111
irep.h
configt::cppt::cpp_standard
enum configt::cppt::cpp_standardt cpp_standard
configt::cppt::set_cpp03
void set_cpp03()
Definition: config.h:231