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