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
Globally accessible architectural configuration.
Definition: config.h:106
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1230
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:1290
struct configt::bv_encodingt bv_encoding
bool set(const cmdlinet &cmdline)
Definition: config.cpp:798
optionalt< std::string > main
Definition: config.h:261
struct configt::verilogt verilog
std::string object_bits_info()
Definition: config.cpp:1315
void set_classpath(const std::string &cp)
Definition: config.cpp:1410
static irep_idt this_architecture()
Definition: config.cpp:1326
struct configt::javat java
struct configt::cppt cpp
static irep_idt this_operating_system()
Definition: config.cpp:1426
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The symbol table.
Definition: symbol_table.h:20
configt config
Definition: config.cpp:24
nonstd::optional< T > optionalt
Definition: optional.h:35
std::size_t long_double_width
Definition: config.h:120
std::list< std::string > include_paths
Definition: config.h:205
bool for_has_scope
Definition: config.h:125
void set_arch_spec_x32()
Definition: config.cpp:556
enum configt::ansi_ct::c_standardt c_standard
void set_32()
Definition: config.cpp:31
void set_arch_spec_riscv64()
Definition: config.cpp:402
endiannesst endianness
Definition: config.h:157
void set_16()
Definition: config.cpp:26
void set_arch_spec_sh4()
Definition: config.cpp:645
void set_ILP32()
int=32, long=32, pointer=32
Definition: config.cpp:110
bool ts_18661_3_Floatn_types
Definition: config.h:126
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:124
void set_arch_spec_hppa()
Definition: config.cpp:616
static std::string os_to_string(ost)
Definition: config.cpp:1151
std::size_t pointer_width
Definition: config.h:117
bool gcc__float128_type
Definition: config.h:127
void set_c89()
Definition: config.h:132
std::list< std::string > include_files
Definition: config.h:206
void set_ILP64()
int=64, long=64, pointer=64
Definition: config.cpp:70
irep_idt arch
Definition: config.h:165
std::list< std::string > undefines
Definition: config.h:203
ieee_floatt::rounding_modet rounding_mode
Definition: config.h:136
void set_64()
Definition: config.cpp:36
std::list< std::string > preprocessor_options
Definition: config.h:204
void set_arch_spec_sparc(const irep_idt &subarch)
Definition: config.cpp:485
static ost string_to_os(const std::string &)
Definition: config.cpp:1166
std::list< std::string > defines
Definition: config.h:202
void set_c99()
Definition: config.h:133
bool single_precision_constant
Definition: config.h:128
void set_LLP64()
int=32, long=32, pointer=64
Definition: config.cpp:90
void set_arch_spec_arm(const irep_idt &subarch)
Definition: config.cpp:280
std::size_t wchar_t_width
Definition: config.h:121
preprocessort preprocessor
Definition: config.h:200
@ malloc_failure_mode_return_null
Definition: config.h:217
@ malloc_failure_mode_none
Definition: config.h:216
@ malloc_failure_mode_assert_then_assume
Definition: config.h:218
std::size_t double_width
Definition: config.h:119
bool malloc_may_fail
Definition: config.h:212
bool char_is_unsigned
Definition: config.h:124
static c_standardt default_c_standard()
Definition: config.cpp:675
void set_arch_spec_alpha()
Definition: config.cpp:323
std::size_t alignment
Definition: config.h:150
void set_arch_spec_power(const irep_idt &subarch)
Definition: config.cpp:219
std::size_t bool_width
Definition: config.h:113
bool string_abstraction
Definition: config.h:211
void set_arch_spec_s390()
Definition: config.cpp:428
void set_LP64()
int=32, long=64, pointer=64
Definition: config.cpp:46
void set_arch_spec_x86_64()
Definition: config.cpp:181
void set_LP32()
int=16, long=32, pointer=32
Definition: config.cpp:130
std::size_t memory_operand_size
Definition: config.h:154
std::size_t long_long_int_width
Definition: config.h:116
void set_arch_spec_s390x()
Definition: config.cpp:457
bool NULL_is_zero
Definition: config.h:168
std::size_t long_int_width
Definition: config.h:112
void set_arch_spec_mips(const irep_idt &subarch)
Definition: config.cpp:352
std::size_t single_width
Definition: config.h:118
void set_arch_spec_i386()
Definition: config.cpp:149
std::size_t short_int_width
Definition: config.h:115
std::size_t char_width
Definition: config.h:114
void set_c11()
Definition: config.h:134
static const std::size_t default_object_bits
Definition: config.h:223
flavourt mode
Definition: config.h:196
std::size_t int_width
Definition: config.h:111
malloc_failure_modet malloc_failure_mode
Definition: config.h:221
void set_arch_spec_ia64()
Definition: config.cpp:525
bool is_object_bits_default
Definition: config.h:257
std::size_t object_bits
Definition: config.h:256
void set_cpp14()
Definition: config.h:234
enum configt::cppt::cpp_standardt cpp_standard
void set_cpp11()
Definition: config.h:233
static const std::size_t default_object_bits
Definition: config.h:236
void set_cpp03()
Definition: config.h:232
static cpp_standardt default_cpp_standard()
Definition: config.cpp:690
void set_cpp98()
Definition: config.h:231
classpatht classpath
Definition: config.h:247
std::list< std::string > classpatht
Definition: config.h:246
irep_idt main_class
Definition: config.h:248
static const std::size_t default_object_bits
Definition: config.h:250
std::list< std::string > include_paths
Definition: config.h:241