cprover
expr2c_class.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_ANSI_C_EXPR2C_CLASS_H
11 #define CPROVER_ANSI_C_EXPR2C_CLASS_H
12 
13 #include <string>
14 #include <unordered_map>
15 #include <unordered_set>
16 
17 #include <util/std_code.h>
18 #include <util/std_expr.h>
19 
20 class qualifierst;
21 class namespacet;
22 
23 class expr2ct
24 {
25 public:
26  explicit expr2ct(const namespacet &_ns):ns(_ns), sizeof_nesting(0) { }
27  virtual ~expr2ct() { }
28 
29  virtual std::string convert(const typet &src);
30  virtual std::string convert(const exprt &src);
31 
32  void get_shorthands(const exprt &expr);
33 
34 protected:
35  const namespacet &ns;
36 
37  virtual std::string convert_rec(
38  const typet &src,
39  const qualifierst &qualifiers,
40  const std::string &declarator);
41 
42  virtual std::string convert_struct_type(
43  const typet &src,
44  const std::string &qualifiers_str,
45  const std::string &declarator_str);
46 
47  std::string convert_struct_type(
48  const typet &src,
49  const std::string &qualifer_str,
50  const std::string &declarator_str,
51  bool inc_struct_body,
52  bool inc_padding_components);
53 
54  virtual std::string convert_array_type(
55  const typet &src,
56  const qualifierst &qualifiers,
57  const std::string &declarator_str);
58 
59  std::string convert_array_type(
60  const typet &src,
61  const qualifierst &qualifiers,
62  const std::string &declarator_str,
63  bool inc_size_if_possible);
64 
65  static std::string indent_str(unsigned indent);
66 
67  std::unordered_map<irep_idt, std::unordered_set<irep_idt>> ns_collision;
68  std::unordered_map<irep_idt, irep_idt> shorthands;
69 
70  unsigned sizeof_nesting;
71 
72  irep_idt id_shorthand(const irep_idt &identifier) const;
73 
74  std::string convert_typecast(
75  const typecast_exprt &src, unsigned &precedence);
76 
77  std::string convert_pointer_arithmetic(
78  const exprt &src,
79  unsigned &precedence);
80 
81  std::string convert_pointer_difference(
82  const exprt &src,
83  unsigned &precedence);
84 
85  std::string convert_binary(
86  const exprt &src, const std::string &symbol,
87  unsigned precedence, bool full_parentheses);
88 
89  std::string convert_multi_ary(
90  const exprt &src, const std::string &symbol,
91  unsigned precedence, bool full_parentheses);
92 
93  std::string convert_cond(
94  const exprt &src, unsigned precedence);
95 
96  std::string convert_struct_member_value(
97  const exprt &src, unsigned precedence);
98 
99  std::string convert_array_member_value(
100  const exprt &src, unsigned precedence);
101 
102  std::string convert_member(
103  const member_exprt &src, unsigned precedence);
104 
105  std::string convert_array_of(const exprt &src, unsigned precedence);
106 
107  std::string convert_trinary(
108  const exprt &src, const std::string &symbol1,
109  const std::string &symbol2, unsigned precedence);
110 
111  std::string convert_overflow(
112  const exprt &src, unsigned &precedence);
113 
114  std::string convert_quantifier(
115  const exprt &src, const std::string &symbol,
116  unsigned precedence);
117 
118  std::string convert_with(
119  const exprt &src, unsigned precedence);
120 
121  std::string convert_update(
122  const exprt &src, unsigned precedence);
123 
124  std::string convert_member_designator(
125  const exprt &src);
126 
127  std::string convert_index_designator(
128  const exprt &src);
129 
130  std::string convert_index(
131  const exprt &src, unsigned precedence);
132 
133  std::string convert_byte_extract(
134  const exprt &src,
135  unsigned precedence);
136 
137  std::string convert_byte_update(
138  const exprt &src,
139  unsigned precedence);
140 
141  std::string convert_extractbit(
142  const exprt &src,
143  unsigned precedence);
144 
145  std::string convert_extractbits(
146  const exprt &src,
147  unsigned precedence);
148 
149  std::string convert_unary(
150  const exprt &src, const std::string &symbol,
151  unsigned precedence);
152 
153  std::string convert_unary_post(
154  const exprt &src, const std::string &symbol,
155  unsigned precedence);
156 
157  std::string convert_function(
158  const exprt &src, const std::string &symbol,
159  unsigned precedence);
160 
161  std::string convert_complex(
162  const exprt &src,
163  unsigned precedence);
164 
165  std::string convert_comma(
166  const exprt &src,
167  unsigned precedence);
168 
169  std::string convert_Hoare(const exprt &src);
170 
171  std::string convert_code(const codet &src);
172  virtual std::string convert_code(const codet &src, unsigned indent);
173  std::string convert_code_label(const code_labelt &src, unsigned indent);
174  // NOLINTNEXTLINE(whitespace/line_length)
175  std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
176  std::string convert_code_asm(const code_asmt &src, unsigned indent);
177  std::string convert_code_assign(const code_assignt &src, unsigned indent);
178  std::string convert_code_free(const codet &src, unsigned indent);
179  std::string convert_code_init(const codet &src, unsigned indent);
180  // NOLINTNEXTLINE(whitespace/line_length)
181  std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
182  std::string convert_code_for(const code_fort &src, unsigned indent);
183  std::string convert_code_while(const code_whilet &src, unsigned indent);
184  std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent);
185  std::string convert_code_block(const code_blockt &src, unsigned indent);
186  std::string convert_code_expression(const codet &src, unsigned indent);
187  std::string convert_code_return(const codet &src, unsigned indent);
188  std::string convert_code_goto(const codet &src, unsigned indent);
189  std::string convert_code_assume(const codet &src, unsigned indent);
190  std::string convert_code_assert(const codet &src, unsigned indent);
191  std::string convert_code_break(const codet &src, unsigned indent);
192  std::string convert_code_switch(const codet &src, unsigned indent);
193  std::string convert_code_continue(const codet &src, unsigned indent);
194  std::string convert_code_decl(const codet &src, unsigned indent);
195  std::string convert_code_decl_block(const codet &src, unsigned indent);
196  std::string convert_code_dead(const codet &src, unsigned indent);
197  // NOLINTNEXTLINE(whitespace/line_length)
198  std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
199  std::string convert_code_lock(const codet &src, unsigned indent);
200  std::string convert_code_unlock(const codet &src, unsigned indent);
201  std::string convert_code_printf(const codet &src, unsigned indent);
202  std::string convert_code_fence(const codet &src, unsigned indent);
203  std::string convert_code_input(const codet &src, unsigned indent);
204  std::string convert_code_output(const codet &src, unsigned indent);
205  std::string convert_code_array_set(const codet &src, unsigned indent);
206  std::string convert_code_array_copy(const codet &src, unsigned indent);
207  std::string convert_code_array_replace(const codet &src, unsigned indent);
208 
209  virtual std::string convert_with_precedence(
210  const exprt &src, unsigned &precedence);
211 
212  // NOLINTNEXTLINE(whitespace/line_length)
213  std::string convert_function_application(const function_application_exprt &src, unsigned &precedence);
214  // NOLINTNEXTLINE(whitespace/line_length)
215  std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence);
216  std::string convert_allocate(const exprt &src, unsigned &precedence);
217  std::string convert_nondet(const exprt &src, unsigned &precedence);
218  std::string convert_prob_coin(const exprt &src, unsigned &precedence);
219  std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
220  // NOLINTNEXTLINE(whitespace/line_length)
221  std::string convert_statement_expression(const exprt &src, unsigned &precendence);
222 
223  virtual std::string convert_symbol(const exprt &src, unsigned &precedence);
224  std::string convert_predicate_symbol(const exprt &src, unsigned &precedence);
225  // NOLINTNEXTLINE(whitespace/line_length)
226  std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence);
227  // NOLINTNEXTLINE(whitespace/line_length)
228  std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence);
229  // NOLINTNEXTLINE(whitespace/line_length)
230  std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence);
231  std::string convert_quantified_symbol(const exprt &src, unsigned &precedence);
232  std::string convert_nondet_bool(const exprt &src, unsigned &precedence);
233  std::string convert_object_descriptor(const exprt &src, unsigned &precedence);
234  std::string convert_literal(const exprt &src, unsigned &precedence);
235  // NOLINTNEXTLINE(whitespace/line_length)
236  virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence);
237  virtual std::string convert_constant_bool(bool boolean_value);
238 
239  std::string convert_norep(const exprt &src, unsigned &precedence);
240 
241  virtual std::string convert_struct(const exprt &src, unsigned &precedence);
242  std::string convert_union(const exprt &src, unsigned &precedence);
243  std::string convert_vector(const exprt &src, unsigned &precedence);
244  std::string convert_array(const exprt &src, unsigned &precedence);
245  std::string convert_array_list(const exprt &src, unsigned &precedence);
246  std::string convert_initializer_list(const exprt &src, unsigned &precedence);
247  // NOLINTNEXTLINE(whitespace/line_length)
248  std::string convert_designated_initializer(const exprt &src, unsigned &precedence);
249  std::string convert_concatenation(const exprt &src, unsigned &precedence);
250  std::string convert_sizeof(const exprt &src, unsigned &precedence);
251  std::string convert_let(const let_exprt &, unsigned precedence);
252 
253  std::string convert_struct(
254  const exprt &src,
255  unsigned &precedence,
256  bool include_padding_components);
257 };
258 
259 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
Definition: expr2c.cpp:1204
The type of an expression.
Definition: type.h:22
std::string convert_code_assume(const codet &src, unsigned indent)
Definition: expr2c.cpp:3281
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:166
semantic type conversion
Definition: std_expr.h:2111
std::string convert_complex(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1290
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:659
void get_shorthands(const exprt &expr)
Definition: expr2c.cpp:87
application of (mathematical) function
Definition: std_expr.h:4529
std::string convert_code_expression(const codet &src, unsigned indent)
Definition: expr2c.cpp:2847
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:1095
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1242
std::string convert_code_continue(const codet &src, unsigned indent)
Definition: expr2c.cpp:2702
std::string convert_code_fence(const codet &src, unsigned indent)
Definition: expr2c.cpp:3130
std::string convert_Hoare(const exprt &src)
Definition: expr2c.cpp:3347
std::string convert_union(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2141
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1406
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
Definition: expr2c.cpp:3312
std::string convert_overflow(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2408
std::string convert_code_block(const code_blockt &src, unsigned indent)
Definition: expr2c.cpp:2809
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3342
std::string convert_array_of(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1341
std::string convert_code_unlock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3047
virtual std::string convert_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1653
A constant literal expression.
Definition: std_expr.h:4422
std::string convert_code_break(const codet &src, unsigned indent)
Definition: expr2c.cpp:2648
std::string convert_code_decl(const codet &src, unsigned indent)
Definition: expr2c.cpp:2713
std::string convert_code_return(const codet &src, unsigned indent)
Definition: expr2c.cpp:2614
std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1711
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:161
expr2ct(const namespacet &_ns)
Definition: expr2c_class.h:26
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2c.cpp:3060
std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence)
Definition: expr2c.cpp:1695
irep_idt id_shorthand(const irep_idt &identifier) const
Definition: expr2c.cpp:44
std::string convert_sizeof(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3422
std::string convert_code_printf(const codet &src, unsigned indent)
Definition: expr2c.cpp:3108
unsigned sizeof_nesting
Definition: expr2c_class.h:70
Extract member of struct or union.
Definition: std_expr.h:3869
std::string convert_binary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:1040
std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1719
std::string convert_code_free(const codet &src, unsigned indent)
Definition: expr2c.cpp:3012
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1766
std::string convert_unary(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1144
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2006
std::string convert_literal(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1225
std::string convert_code_assign(const code_assignt &src, unsigned indent)
Definition: expr2c.cpp:3001
std::string convert_code_label(const code_labelt &src, unsigned indent)
Definition: expr2c.cpp:3294
std::string convert_byte_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1376
std::string convert_nondet_bool(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1735
std::string convert_code_input(const codet &src, unsigned indent)
Definition: expr2c.cpp:3160
virtual ~expr2ct()
Definition: expr2c_class.h:27
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
Definition: expr2c_class.h:67
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1215
std::string convert_index_designator(const exprt &src)
Definition: expr2c.cpp:1536
std::string convert_code_array_set(const codet &src, unsigned indent)
Definition: expr2c.cpp:3203
std::string convert_member(const member_exprt &src, unsigned precedence)
Definition: expr2c.cpp:1546
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1489
std::string convert_trinary(const exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
Definition: expr2c.cpp:802
API to expression classes.
std::string convert_code_asm(const code_asmt &src, unsigned indent)
Definition: expr2c.cpp:2444
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::string convert_initializer_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2302
std::string convert_code_dead(const codet &src, unsigned indent)
Definition: expr2c.cpp:2758
A label for branch targets.
Definition: std_code.h:977
std::string convert_code_lock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3034
A function call.
Definition: std_code.h:858
std::string convert_array_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2268
std::string convert_with(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:874
const namespacet & ns
Definition: expr2c_class.h:35
A ‘while’ instruction.
Definition: std_code.h:601
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1232
std::unordered_map< irep_idt, irep_idt > shorthands
Definition: expr2c_class.h:68
std::string convert_extractbits(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3405
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::string convert_extractbit(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3390
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence)
Definition: expr2c.cpp:2378
std::string convert_vector(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2094
std::string convert_concatenation(const exprt &src, unsigned &precedence)
std::string convert_predicate_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1703
std::string convert_nondet(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1194
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1642
std::string convert_code_assert(const codet &src, unsigned indent)
Definition: expr2c.cpp:3268
std::string convert_index(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1428
std::string convert_array_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1622
A function call side effect.
Definition: std_code.h:1395
std::string convert_byte_extract(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1351
std::string convert_member_designator(const exprt &src)
Definition: expr2c.cpp:1526
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
Definition: expr2c.cpp:2548
Expression to hold a nondeterministic choice.
Definition: std_expr.h:239
std::string convert_quantified_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1727
std::string convert_code_array_copy(const codet &src, unsigned indent)
Definition: expr2c.cpp:3225
Base class for all expressions.
Definition: expr.h:42
std::string convert_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:962
std::string convert_cond(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1006
std::string convert_code_for(const code_fort &src, unsigned indent)
Definition: expr2c.cpp:2772
A ‘do while’ instruction.
Definition: std_code.h:664
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3436
An inline assembler statement.
Definition: std_code.h:1175
std::string convert_code_decl_block(const codet &src, unsigned indent)
Definition: expr2c.cpp:2832
std::string convert_code_array_replace(const codet &src, unsigned indent)
Definition: expr2c.cpp:3247
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1452
Sequential composition.
Definition: std_code.h:89
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1632
std::string convert_array(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2162
std::string convert_allocate(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1167
An if-then-else.
Definition: std_code.h:466
std::string convert_designated_initializer(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2330
A switch-case.
Definition: std_code.h:1045
std::string convert_code_goto(const codet &src, unsigned indent)
Definition: expr2c.cpp:2636
A statement in a programming language.
Definition: std_code.h:21
A ‘for’ instruction.
Definition: std_code.h:727
std::string convert_comma(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1266
A let expression.
Definition: std_expr.h:4703
std::string convert_code_while(const code_whilet &src, unsigned indent)
Definition: expr2c.cpp:2522
std::string convert_code_output(const codet &src, unsigned indent)
Definition: expr2c.cpp:3182
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1742
std::string convert_code_init(const codet &src, unsigned indent)
Definition: expr2c.cpp:3025
std::string convert_quantifier(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:852
std::string convert_let(const let_exprt &, unsigned precedence)
Definition: expr2c.cpp:942
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
Definition: expr2c.cpp:1997
std::string convert_code_switch(const codet &src, unsigned indent)
Definition: expr2c.cpp:2659
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:768
Assignment.
Definition: std_code.h:196
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2439
std::string convert_function_application(const function_application_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2348
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:732
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
Definition: expr2c.cpp:2577