cprover
Loading...
Searching...
No Matches
expr2c_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_ANSI_C_EXPR2C_CLASS_H
11#define CPROVER_ANSI_C_EXPR2C_CLASS_H
12
13#include "expr2c.h"
14
15#include <string>
16#include <unordered_map>
17#include <unordered_set>
18
20
21#include <util/bitvector_expr.h>
22#include <util/byte_operators.h>
24#include <util/std_code.h>
25
26class qualifierst;
27class namespacet;
28
30{
31public:
39 virtual ~expr2ct() { }
40
41 virtual std::string convert(const typet &src);
42 virtual std::string convert(const exprt &src);
43
44 void get_shorthands(const exprt &expr);
45
46 std::string
47 convert_with_identifier(const typet &src, const std::string &identifier);
48
49protected:
50 const namespacet &ns;
52
53 virtual std::string convert_rec(
54 const typet &src,
56 const std::string &declarator);
57
58 virtual std::string convert_struct_type(
59 const typet &src,
60 const std::string &qualifiers_str,
61 const std::string &declarator_str);
62
63 std::string convert_struct_type(
64 const typet &src,
65 const std::string &qualifer_str,
66 const std::string &declarator_str,
67 bool inc_struct_body,
69
70 virtual std::string convert_array_type(
71 const typet &src,
73 const std::string &declarator_str);
74
75 std::string convert_array_type(
76 const typet &src,
78 const std::string &declarator_str,
80
81 static std::string indent_str(unsigned indent);
82
83 std::unordered_map<irep_idt, std::unordered_set<irep_idt>> ns_collision;
84 std::unordered_map<irep_idt, irep_idt> shorthands;
85
87
88 irep_idt id_shorthand(const irep_idt &identifier) const;
89
90 std::string convert_typecast(
91 const typecast_exprt &src, unsigned &precedence);
92
94 const exprt &src,
95 unsigned &precedence);
96
98 const exprt &src,
99 unsigned &precedence);
100
101 std::string convert_binary(
102 const binary_exprt &,
103 const std::string &symbol,
104 unsigned precedence,
105 bool full_parentheses);
106
107 std::string convert_multi_ary(
108 const exprt &src, const std::string &symbol,
109 unsigned precedence, bool full_parentheses);
110
111 std::string convert_cond(
112 const exprt &src, unsigned precedence);
113
114 std::string convert_struct_member_value(
115 const exprt &src, unsigned precedence);
116
117 std::string convert_array_member_value(
118 const exprt &src, unsigned precedence);
119
120 std::string convert_member(
121 const member_exprt &src, unsigned precedence);
122
123 std::string convert_array_of(const exprt &src, unsigned precedence);
124
125 std::string convert_trinary(
126 const ternary_exprt &src,
127 const std::string &symbol1,
128 const std::string &symbol2,
129 unsigned precedence);
130
138 std::string convert_rox(const shift_exprt &src, unsigned precedence);
139
140 std::string convert_overflow(
141 const exprt &src, unsigned &precedence);
142
143 std::string convert_quantifier(
144 const quantifier_exprt &,
145 const std::string &symbol,
146 unsigned precedence);
147
148 std::string convert_with(
149 const exprt &src, unsigned precedence);
150
151 std::string convert_update(const update_exprt &, unsigned precedence);
152
153 std::string convert_member_designator(
154 const exprt &src);
155
156 std::string convert_index_designator(
157 const exprt &src);
158
159 std::string convert_index(
160 const exprt &src, unsigned precedence);
161
162 std::string
164
165 std::string
167
168 std::string convert_extractbit(const extractbit_exprt &, unsigned precedence);
169
170 std::string
172
173 std::string convert_unary(
174 const unary_exprt &,
175 const std::string &symbol,
176 unsigned precedence);
177
178 std::string convert_unary_post(
179 const exprt &src, const std::string &symbol,
180 unsigned precedence);
181
185 std::string convert_function(const exprt &src, const std::string &symbol);
186
187 std::string convert_complex(
188 const exprt &src,
189 unsigned precedence);
190
191 std::string convert_comma(
192 const exprt &src,
193 unsigned precedence);
194
195 std::string convert_Hoare(const exprt &src);
196
197 std::string convert_code(const codet &src);
198 virtual std::string convert_code(const codet &src, unsigned indent);
199 std::string convert_code_label(const code_labelt &src, unsigned indent);
200 // NOLINTNEXTLINE(whitespace/line_length)
201 std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
202 std::string convert_code_asm(const code_asmt &src, unsigned indent);
203 std::string
204 convert_code_frontend_assign(const code_frontend_assignt &, unsigned indent);
205 // NOLINTNEXTLINE(whitespace/line_length)
206 std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
207 std::string convert_code_for(const code_fort &src, unsigned indent);
208 std::string convert_code_while(const code_whilet &src, unsigned indent);
209 std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent);
210 std::string convert_code_block(const code_blockt &src, unsigned indent);
211 std::string convert_code_expression(const codet &src, unsigned indent);
212 std::string convert_code_return(const codet &src, unsigned indent);
213 std::string convert_code_goto(const codet &src, unsigned indent);
214 std::string convert_code_assume(const codet &src, unsigned indent);
215 std::string convert_code_assert(const codet &src, unsigned indent);
216 std::string convert_code_break(unsigned indent);
217 std::string convert_code_switch(const codet &src, unsigned indent);
218 std::string convert_code_continue(unsigned indent);
219 std::string convert_code_frontend_decl(const codet &, unsigned indent);
220 std::string convert_code_decl_block(const codet &src, unsigned indent);
221 std::string convert_code_dead(const codet &src, unsigned indent);
222 // NOLINTNEXTLINE(whitespace/line_length)
223 std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
224 std::string convert_code_lock(const codet &src, unsigned indent);
225 std::string convert_code_unlock(const codet &src, unsigned indent);
226 std::string convert_code_printf(const codet &src, unsigned indent);
227 std::string convert_code_fence(const codet &src, unsigned indent);
228 std::string convert_code_input(const codet &src, unsigned indent);
229 std::string convert_code_output(const codet &src, unsigned indent);
230 std::string convert_code_array_set(const codet &src, unsigned indent);
231 std::string convert_code_array_copy(const codet &src, unsigned indent);
232 std::string convert_code_array_replace(const codet &src, unsigned indent);
233
234 virtual std::string convert_with_precedence(
235 const exprt &src, unsigned &precedence);
236
237 std::string
241 std::string convert_allocate(const exprt &src, unsigned &precedence);
242 std::string convert_nondet(const exprt &src, unsigned &precedence);
243 std::string convert_prob_coin(const exprt &src, unsigned &precedence);
244 std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
245 // NOLINTNEXTLINE(whitespace/line_length)
246 std::string convert_statement_expression(const exprt &src, unsigned &precendence);
247
248 virtual std::string convert_symbol(const exprt &src);
249 std::string convert_predicate_symbol(const exprt &src);
250 std::string convert_predicate_next_symbol(const exprt &src);
251 std::string convert_predicate_passive_symbol(const exprt &src);
252 std::string convert_nondet_symbol(const nondet_symbol_exprt &);
253 std::string convert_quantified_symbol(const exprt &src);
254 std::string convert_nondet_bool();
255 std::string convert_object_descriptor(const exprt &src, unsigned &precedence);
256 std::string convert_literal(const exprt &src);
257 // NOLINTNEXTLINE(whitespace/line_length)
258 virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence);
259 virtual std::string convert_constant_bool(bool boolean_value);
260
261 std::string convert_norep(const exprt &src, unsigned &precedence);
262
263 virtual std::string convert_struct(const exprt &src, unsigned &precedence);
264 std::string convert_union(const exprt &src, unsigned &precedence);
265 std::string convert_vector(const exprt &src, unsigned &precedence);
266 std::string convert_array(const exprt &src);
267 std::string convert_array_list(const exprt &src, unsigned &precedence);
268 std::string convert_initializer_list(const exprt &src);
269 std::string convert_designated_initializer(const exprt &src);
270 std::string convert_concatenation(const exprt &src, unsigned &precedence);
271 std::string convert_sizeof(const exprt &src, unsigned &precedence);
272 std::string convert_let(const let_exprt &, unsigned precedence);
273
274 std::string convert_struct(
275 const exprt &src,
276 unsigned &precedence,
278
279 std::string convert_conditional_target_group(const exprt &src);
280 std::string convert_bitreverse(const bitreverse_exprt &src);
281};
282
283#endif // CPROVER_ANSI_C_EXPR2C_CLASS_H
API to expression classes for bitvectors.
Expression classes for byte-level operators.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A base class for binary expressions.
Definition std_expr.h:550
Reverse the order of bits in a bit-vector.
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
codet representation of an inline assembler statement.
Definition std_code.h:1253
A codet representing sequential composition of program statements.
Definition std_code.h:130
codet representation of a do while statement.
Definition std_code.h:672
codet representation of a for statement.
Definition std_code.h:734
A codet representing an assignment in the program.
Definition std_code.h:24
codet representation of a function call statement.
codet representation of an if-then-else statement.
Definition std_code.h:460
codet representation of a label for branch targets.
Definition std_code.h:959
codet representation of a switch-case, i.e. a case statement within a switch.
Definition std_code.h:1023
codet representing a while statement.
Definition std_code.h:610
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Definition std_expr.h:2807
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
std::string convert_nondet(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:1175
std::string convert_literal(const exprt &src)
Definition expr2c.cpp:1210
std::string convert_code_continue(unsigned indent)
Definition expr2c.cpp:2767
virtual std::string convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str)
To generate a C-like type declaration of an array.
Definition expr2c.cpp:715
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
Definition expr2c.cpp:3363
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
Definition expr2c.cpp:754
std::string convert_comma(const exprt &src, unsigned precedence)
Definition expr2c.cpp:1247
std::string convert_code_assert(const codet &src, unsigned indent)
Definition expr2c.cpp:3318
std::string convert_quantifier(const quantifier_exprt &, const std::string &symbol, unsigned precedence)
Definition expr2c.cpp:835
std::string convert_union(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:2136
std::string convert_code_expression(const codet &src, unsigned indent)
Definition expr2c.cpp:2909
std::string convert_code_goto(const codet &src, unsigned indent)
Definition expr2c.cpp:2703
std::string convert_code_switch(const codet &src, unsigned indent)
Definition expr2c.cpp:2724
std::string convert_initializer_list(const exprt &src)
Definition expr2c.cpp:2290
std::string convert_quantified_symbol(const exprt &src)
Definition expr2c.cpp:1696
std::string convert_function_application(const function_application_exprt &src)
Definition expr2c.cpp:2419
std::string convert_code_unlock(const codet &src, unsigned indent)
Definition expr2c.cpp:3097
std::string convert_code_decl_block(const codet &src, unsigned indent)
Definition expr2c.cpp:2894
static std::string indent_str(unsigned indent)
Definition expr2c.cpp:2507
std::string convert_byte_update(const byte_update_exprt &, unsigned precedence)
Definition expr2c.cpp:1357
std::string convert_code(const codet &src)
Definition expr2c.cpp:3393
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:1428
std::string convert_let(const let_exprt &, unsigned precedence)
Definition expr2c.cpp:927
std::string convert_nondet_bool()
Definition expr2c.cpp:1702
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:1618
const expr2c_configurationt & configuration
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
std::string convert_code_output(const codet &src, unsigned indent)
Definition expr2c.cpp:3232
std::string convert_code_while(const code_whilet &src, unsigned indent)
Definition expr2c.cpp:2590
std::string convert_index_designator(const exprt &src)
Definition expr2c.cpp:1514
std::string convert_code_frontend_decl(const codet &, unsigned indent)
Definition expr2c.cpp:2777
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:1465
std::string convert_code_block(const code_blockt &src, unsigned indent)
Definition expr2c.cpp:2871
std::string convert_code_asm(const code_asmt &src, unsigned indent)
Definition expr2c.cpp:2512
std::string convert_allocate(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:1147
std::string convert_Hoare(const exprt &src)
Definition expr2c.cpp:3398
std::string convert_sizeof(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:3465
std::string convert_code_lock(const codet &src, unsigned indent)
Definition expr2c.cpp:3084
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
Definition expr2c.cpp:2616
irep_idt id_shorthand(const irep_idt &identifier) const
Definition expr2c.cpp:76
std::string convert_cond(const exprt &src, unsigned precedence)
Definition expr2c.cpp:992
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src)
Definition expr2c.cpp:2447
std::string convert_overflow(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:2476
std::string convert_member(const member_exprt &src, unsigned precedence)
Definition expr2c.cpp:1524
void get_shorthands(const exprt &expr)
Definition expr2c.cpp:117
std::string convert_code_for(const code_fort &src, unsigned indent)
Definition expr2c.cpp:2834
std::string convert_with_identifier(const typet &src, const std::string &identifier)
Build a declaration string, which requires converting both a type and putting an identifier in the sy...
Definition expr2c.cpp:4004
std::string convert_extractbits(const extractbits_exprt &src, unsigned precedence)
Definition expr2c.cpp:3453
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:2000
optionalt< std::string > convert_function(const exprt &src)
Returns a string if src is a function with a known conversion, else returns nullopt.
Definition expr2c.cpp:3939
std::string convert_trinary(const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
Definition expr2c.cpp:788
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:1200
std::string convert_update(const update_exprt &, unsigned precedence)
Definition expr2c.cpp:954
std::string convert_nondet_symbol(const nondet_symbol_exprt &)
Definition expr2c.cpp:1672
std::string convert_code_printf(const codet &src, unsigned indent)
Definition expr2c.cpp:3158
std::string convert_unary(const unary_exprt &, const std::string &symbol, unsigned precedence)
Definition expr2c.cpp:1127
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
Definition expr2c.cpp:2645
std::string convert_member_designator(const exprt &src)
Definition expr2c.cpp:1504
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition expr2c.cpp:219
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
Definition expr2c.cpp:1331
std::string convert_code_label(const code_labelt &src, unsigned indent)
Definition expr2c.cpp:3345
virtual std::string convert_symbol(const exprt &src)
Definition expr2c.cpp:1629
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition expr2c.cpp:1731
std::string convert_code_array_copy(const codet &src, unsigned indent)
Definition expr2c.cpp:3275
std::string convert_concatenation(const exprt &src, unsigned &precedence)
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
Definition expr2c.cpp:1185
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
Definition expr2c.cpp:1608
std::string convert_code_dead(const codet &src, unsigned indent)
Definition expr2c.cpp:2820
const namespacet & ns
std::string convert_rox(const shift_exprt &src, unsigned precedence)
Conversion function from rol/ror expressions to C code strings Note that this constructs a complex ex...
Definition expr2c.cpp:2316
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:3520
std::string convert_designated_initializer(const exprt &src)
Definition expr2c.cpp:2376
std::string convert_vector(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:2089
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition expr2c.cpp:1078
std::string convert_array_member_value(const exprt &src, unsigned precedence)
Definition expr2c.cpp:1598
virtual ~expr2ct()
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
Definition expr2c.cpp:1382
std::unordered_map< irep_idt, irep_idt > shorthands
std::string convert_complex(const exprt &src, unsigned precedence)
Definition expr2c.cpp:1271
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition expr2c.cpp:3110
std::string convert_code_fence(const codet &src, unsigned indent)
Definition expr2c.cpp:3180
std::string convert_bitreverse(const bitreverse_exprt &src)
Definition expr2c.cpp:3504
virtual std::string convert(const typet &src)
Definition expr2c.cpp:214
std::string convert_code_return(const codet &src, unsigned indent)
Definition expr2c.cpp:2682
std::string convert_code_break(unsigned indent)
Definition expr2c.cpp:2715
virtual std::string convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str)
To generate C-like string for defining the given struct.
Definition expr2c.cpp:638
std::string convert_with(const exprt &src, unsigned precedence)
Definition expr2c.cpp:858
std::string convert_code_frontend_assign(const code_frontend_assignt &, unsigned indent)
Definition expr2c.cpp:3076
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:1707
std::string convert_predicate_passive_symbol(const exprt &src)
Definition expr2c.cpp:1690
std::string convert_array_list(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:2256
unsigned sizeof_nesting
std::string convert_array_of(const exprt &src, unsigned precedence)
Definition expr2c.cpp:1321
std::string convert_code_array_replace(const codet &src, unsigned indent)
Definition expr2c.cpp:3297
std::string convert_conditional_target_group(const exprt &src)
Definition expr2c.cpp:3479
std::string convert_index(const exprt &src, unsigned precedence)
Definition expr2c.cpp:1404
std::string convert_code_assume(const codet &src, unsigned indent)
Definition expr2c.cpp:3331
std::string convert_code_input(const codet &src, unsigned indent)
Definition expr2c.cpp:3210
std::string convert_extractbit(const extractbit_exprt &, unsigned precedence)
Definition expr2c.cpp:3442
std::string convert_predicate_next_symbol(const exprt &src)
Definition expr2c.cpp:1684
std::string convert_code_array_set(const codet &src, unsigned indent)
Definition expr2c.cpp:3253
std::string convert_binary(const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition expr2c.cpp:1026
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
Definition expr2c.cpp:1992
std::string convert_predicate_symbol(const exprt &src)
Definition expr2c.cpp:1678
expr2ct(const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration)
std::string convert_array(const exprt &src)
Definition expr2c.cpp:2155
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Definition expr2c.cpp:1215
Base class for all expressions.
Definition expr.h:54
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
Application of (mathematical) function.
A let expression.
Definition std_expr.h:2973
Extract member of struct or union.
Definition std_expr.h:2667
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a nondeterministic choice.
Definition std_expr.h:209
A base class for quantifier expressions.
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
An expression with three operands.
Definition std_expr.h:53
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:281
Operator to update elements in structs and arrays.
Definition std_expr.h:2496
API to expression classes for 'mathematical' expressions.
Used for configuring the behaviour of expr2c and type2c.
Definition expr2c.h:21
static expr2c_configurationt default_configuration
This prints a human readable C like syntax that closely mirrors the internals of the GOTO program.
Definition expr2c.h:41