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 
106  const exprt &src, unsigned precedence);
107 
108  std::string convert_array_of(const exprt &src, unsigned precedence);
109 
110  std::string convert_trinary(
111  const exprt &src, const std::string &symbol1,
112  const std::string &symbol2, unsigned precedence);
113 
114  std::string convert_overflow(
115  const exprt &src, unsigned &precedence);
116 
117  std::string convert_quantifier(
118  const exprt &src, const std::string &symbol,
119  unsigned precedence);
120 
121  std::string convert_with(
122  const exprt &src, unsigned precedence);
123 
124  std::string convert_update(
125  const exprt &src, unsigned precedence);
126 
127  std::string convert_member_designator(
128  const exprt &src);
129 
130  std::string convert_index_designator(
131  const exprt &src);
132 
133  std::string convert_index(
134  const exprt &src, unsigned precedence);
135 
136  std::string convert_byte_extract(
137  const exprt &src,
138  unsigned precedence);
139 
140  std::string convert_byte_update(
141  const exprt &src,
142  unsigned precedence);
143 
144  std::string convert_extractbit(
145  const exprt &src,
146  unsigned precedence);
147 
148  std::string convert_extractbits(
149  const exprt &src,
150  unsigned precedence);
151 
152  std::string convert_unary(
153  const exprt &src, const std::string &symbol,
154  unsigned precedence);
155 
156  std::string convert_unary_post(
157  const exprt &src, const std::string &symbol,
158  unsigned precedence);
159 
160  std::string convert_function(
161  const exprt &src, const std::string &symbol,
162  unsigned precedence);
163 
164  std::string convert_complex(
165  const exprt &src,
166  unsigned precedence);
167 
168  std::string convert_comma(
169  const exprt &src,
170  unsigned precedence);
171 
172  std::string convert_Hoare(const exprt &src);
173 
174  std::string convert_code(const codet &src);
175  virtual std::string convert_code(const codet &src, unsigned indent);
176  std::string convert_code_label(const code_labelt &src, unsigned indent);
177  // NOLINTNEXTLINE(whitespace/line_length)
178  std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
179  std::string convert_code_asm(const code_asmt &src, unsigned indent);
180  std::string convert_code_assign(const code_assignt &src, unsigned indent);
181  std::string convert_code_free(const codet &src, unsigned indent);
182  std::string convert_code_init(const codet &src, unsigned indent);
183  // NOLINTNEXTLINE(whitespace/line_length)
184  std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
185  std::string convert_code_for(const code_fort &src, unsigned indent);
186  std::string convert_code_while(const code_whilet &src, unsigned indent);
187  std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent);
188  std::string convert_code_block(const code_blockt &src, unsigned indent);
189  std::string convert_code_expression(const codet &src, unsigned indent);
190  std::string convert_code_return(const codet &src, unsigned indent);
191  std::string convert_code_goto(const codet &src, unsigned indent);
192  std::string convert_code_assume(const codet &src, unsigned indent);
193  std::string convert_code_assert(const codet &src, unsigned indent);
194  std::string convert_code_break(const codet &src, unsigned indent);
195  std::string convert_code_switch(const codet &src, unsigned indent);
196  std::string convert_code_continue(const codet &src, unsigned indent);
197  std::string convert_code_decl(const codet &src, unsigned indent);
198  std::string convert_code_decl_block(const codet &src, unsigned indent);
199  std::string convert_code_dead(const codet &src, unsigned indent);
200  // NOLINTNEXTLINE(whitespace/line_length)
201  std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
202  std::string convert_code_lock(const codet &src, unsigned indent);
203  std::string convert_code_unlock(const codet &src, unsigned indent);
204  std::string convert_code_printf(const codet &src, unsigned indent);
205  std::string convert_code_fence(const codet &src, unsigned indent);
206  std::string convert_code_input(const codet &src, unsigned indent);
207  std::string convert_code_output(const codet &src, unsigned indent);
208  std::string convert_code_array_set(const codet &src, unsigned indent);
209  std::string convert_code_array_copy(const codet &src, unsigned indent);
210  std::string convert_code_array_replace(const codet &src, unsigned indent);
211 
212  virtual std::string convert_with_precedence(
213  const exprt &src, unsigned &precedence);
214 
215  // NOLINTNEXTLINE(whitespace/line_length)
216  std::string convert_function_application(const function_application_exprt &src, unsigned &precedence);
217  // NOLINTNEXTLINE(whitespace/line_length)
218  std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence);
219  std::string convert_allocate(const exprt &src, unsigned &precedence);
220  std::string convert_nondet(const exprt &src, unsigned &precedence);
221  std::string convert_prob_coin(const exprt &src, unsigned &precedence);
222  std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
223  // NOLINTNEXTLINE(whitespace/line_length)
224  std::string convert_statement_expression(const exprt &src, unsigned &precendence);
225 
226  virtual std::string convert_symbol(const exprt &src, unsigned &precedence);
227  std::string convert_predicate_symbol(const exprt &src, unsigned &precedence);
228  // NOLINTNEXTLINE(whitespace/line_length)
229  std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence);
230  // NOLINTNEXTLINE(whitespace/line_length)
231  std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence);
232  // NOLINTNEXTLINE(whitespace/line_length)
233  std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence);
234  std::string convert_quantified_symbol(const exprt &src, unsigned &precedence);
235  std::string convert_nondet_bool(const exprt &src, unsigned &precedence);
236  std::string convert_object_descriptor(const exprt &src, unsigned &precedence);
237  std::string convert_literal(const exprt &src, unsigned &precedence);
238  // NOLINTNEXTLINE(whitespace/line_length)
239  virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence);
240  virtual std::string convert_constant_bool(bool boolean_value);
241 
242  std::string convert_norep(const exprt &src, unsigned &precedence);
243 
244  virtual std::string convert_struct(const exprt &src, unsigned &precedence);
245  std::string convert_union(const exprt &src, unsigned &precedence);
246  std::string convert_vector(const exprt &src, unsigned &precedence);
247  std::string convert_array(const exprt &src, unsigned &precedence);
248  std::string convert_array_list(const exprt &src, unsigned &precedence);
249  std::string convert_initializer_list(const exprt &src, unsigned &precedence);
250  // NOLINTNEXTLINE(whitespace/line_length)
251  std::string convert_designated_initializer(const exprt &src, unsigned &precedence);
252  std::string convert_concatenation(const exprt &src, unsigned &precedence);
253  std::string convert_sizeof(const exprt &src, unsigned &precedence);
254  std::string convert_let(const let_exprt &, unsigned precedence);
255 
256  std::string convert_struct(
257  const exprt &src,
258  unsigned &precedence,
259  bool include_padding_components);
260 };
261 
262 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
Definition: expr2c.cpp:1224
The type of an expression.
Definition: type.h:22
std::string convert_code_assume(const codet &src, unsigned indent)
Definition: expr2c.cpp:3301
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:1310
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:4531
std::string convert_code_expression(const codet &src, unsigned indent)
Definition: expr2c.cpp:2867
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:1262
std::string convert_code_continue(const codet &src, unsigned indent)
Definition: expr2c.cpp:2722
std::string convert_code_fence(const codet &src, unsigned indent)
Definition: expr2c.cpp:3150
std::string convert_Hoare(const exprt &src)
Definition: expr2c.cpp:3367
std::string convert_union(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2161
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1426
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
Definition: expr2c.cpp:3332
std::string convert_overflow(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2428
std::string convert_code_block(const code_blockt &src, unsigned indent)
Definition: expr2c.cpp:2829
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3362
std::string convert_array_of(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1361
std::string convert_code_unlock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3067
virtual std::string convert_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1673
A constant literal expression.
Definition: std_expr.h:4424
std::string convert_code_break(const codet &src, unsigned indent)
Definition: expr2c.cpp:2668
std::string convert_code_decl(const codet &src, unsigned indent)
Definition: expr2c.cpp:2733
std::string convert_code_return(const codet &src, unsigned indent)
Definition: expr2c.cpp:2634
std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1731
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:3080
std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence)
Definition: expr2c.cpp:1715
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:3442
std::string convert_code_printf(const codet &src, unsigned indent)
Definition: expr2c.cpp:3128
unsigned sizeof_nesting
Definition: expr2c_class.h:70
Extract member of struct or union.
Definition: std_expr.h:3871
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:1739
std::string convert_code_free(const codet &src, unsigned indent)
Definition: expr2c.cpp:3032
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1786
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:2026
std::string convert_literal(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1245
std::string convert_code_assign(const code_assignt &src, unsigned indent)
Definition: expr2c.cpp:3021
std::string convert_code_label(const code_labelt &src, unsigned indent)
Definition: expr2c.cpp:3314
std::string convert_byte_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1396
std::string convert_pointer_object_has_type(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1167
std::string convert_nondet_bool(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1755
std::string convert_code_input(const codet &src, unsigned indent)
Definition: expr2c.cpp:3180
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:1235
std::string convert_index_designator(const exprt &src)
Definition: expr2c.cpp:1556
std::string convert_code_array_set(const codet &src, unsigned indent)
Definition: expr2c.cpp:3223
std::string convert_member(const member_exprt &src, unsigned precedence)
Definition: expr2c.cpp:1566
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1509
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:2464
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::string convert_initializer_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2322
std::string convert_code_dead(const codet &src, unsigned indent)
Definition: expr2c.cpp:2778
A label for branch targets.
Definition: std_code.h:947
std::string convert_code_lock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3054
A function call.
Definition: std_code.h:828
std::string convert_array_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2288
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:588
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1252
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:3425
std::string convert_extractbit(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3410
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence)
Definition: expr2c.cpp:2398
std::string convert_vector(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2114
std::string convert_concatenation(const exprt &src, unsigned &precedence)
std::string convert_predicate_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1723
std::string convert_nondet(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1214
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1662
std::string convert_code_assert(const codet &src, unsigned indent)
Definition: expr2c.cpp:3288
std::string convert_index(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1448
std::string convert_array_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1642
A function call side effect.
Definition: std_code.h:1352
std::string convert_byte_extract(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1371
std::string convert_member_designator(const exprt &src)
Definition: expr2c.cpp:1546
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
Definition: expr2c.cpp:2568
Expression to hold a nondeterministic choice.
Definition: std_expr.h:239
std::string convert_quantified_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1747
std::string convert_code_array_copy(const codet &src, unsigned indent)
Definition: expr2c.cpp:3245
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:2792
A ‘do while’ instruction.
Definition: std_code.h:643
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3456
An inline assembler statement.
Definition: std_code.h:1143
std::string convert_code_decl_block(const codet &src, unsigned indent)
Definition: expr2c.cpp:2852
std::string convert_code_array_replace(const codet &src, unsigned indent)
Definition: expr2c.cpp:3267
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1472
Sequential composition.
Definition: std_code.h:88
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1652
std::string convert_array(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2182
std::string convert_allocate(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1187
An if-then-else.
Definition: std_code.h:461
std::string convert_designated_initializer(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2350
A switch-case.
Definition: std_code.h:1014
std::string convert_code_goto(const codet &src, unsigned indent)
Definition: expr2c.cpp:2656
A statement in a programming language.
Definition: std_code.h:21
A ‘for’ instruction.
Definition: std_code.h:698
std::string convert_comma(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1286
A let expression.
Definition: std_expr.h:4705
std::string convert_code_while(const code_whilet &src, unsigned indent)
Definition: expr2c.cpp:2542
std::string convert_code_output(const codet &src, unsigned indent)
Definition: expr2c.cpp:3202
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1762
std::string convert_code_init(const codet &src, unsigned indent)
Definition: expr2c.cpp:3045
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:2017
std::string convert_code_switch(const codet &src, unsigned indent)
Definition: expr2c.cpp:2679
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:768
Assignment.
Definition: std_code.h:195
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2459
std::string convert_function_application(const function_application_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2368
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:2597