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 c_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 c_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 c_qualifierst &qualifiers,
57  const std::string &declarator_str);
58 
59  std::string convert_array_type(
60  const typet &src,
61  const c_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,
68  std::unordered_set<irep_idt, irep_id_hash>,
70  std::unordered_map<irep_idt, irep_idt, irep_id_hash> shorthands;
71 
72  unsigned sizeof_nesting;
73 
74  irep_idt id_shorthand(const irep_idt &identifier) const;
75 
76  std::string convert_typecast(
77  const typecast_exprt &src, unsigned &precedence);
78 
79  std::string convert_pointer_arithmetic(
80  const exprt &src,
81  unsigned &precedence);
82 
83  std::string convert_pointer_difference(
84  const exprt &src,
85  unsigned &precedence);
86 
87  std::string convert_binary(
88  const exprt &src, const std::string &symbol,
89  unsigned precedence, bool full_parentheses);
90 
91  std::string convert_cond(
92  const exprt &src, unsigned precedence);
93 
94  std::string convert_struct_member_value(
95  const exprt &src, unsigned precedence);
96 
97  std::string convert_array_member_value(
98  const exprt &src, unsigned precedence);
99 
100  std::string convert_member(
101  const member_exprt &src, unsigned precedence);
102 
104  const exprt &src, unsigned precedence);
105 
106  std::string convert_array_of(const exprt &src, unsigned precedence);
107 
108  std::string convert_trinary(
109  const exprt &src, const std::string &symbol1,
110  const std::string &symbol2, unsigned precedence);
111 
112  std::string convert_overflow(
113  const exprt &src, unsigned &precedence);
114 
115  std::string convert_quantifier(
116  const exprt &src, const std::string &symbol,
117  unsigned precedence);
118 
119  std::string convert_with(
120  const exprt &src, unsigned precedence);
121 
122  std::string convert_update(
123  const exprt &src, unsigned precedence);
124 
125  std::string convert_member_designator(
126  const exprt &src);
127 
128  std::string convert_index_designator(
129  const exprt &src);
130 
131  std::string convert_index(
132  const exprt &src, unsigned precedence);
133 
134  std::string convert_byte_extract(
135  const exprt &src,
136  unsigned precedence);
137 
138  std::string convert_byte_update(
139  const exprt &src,
140  unsigned precedence);
141 
142  std::string convert_extractbit(
143  const exprt &src,
144  unsigned precedence);
145 
146  std::string convert_extractbits(
147  const exprt &src,
148  unsigned precedence);
149 
150  std::string convert_unary(
151  const exprt &src, const std::string &symbol,
152  unsigned precedence);
153 
154  std::string convert_unary_post(
155  const exprt &src, const std::string &symbol,
156  unsigned precedence);
157 
158  std::string convert_function(
159  const exprt &src, const std::string &symbol,
160  unsigned precedence);
161 
162  std::string convert_complex(
163  const exprt &src,
164  unsigned precedence);
165 
166  std::string convert_comma(
167  const exprt &src,
168  unsigned precedence);
169 
170  std::string convert_Hoare(const exprt &src);
171 
172  std::string convert_code(const codet &src);
173  virtual std::string convert_code(const codet &src, unsigned indent);
174  std::string convert_code_label(const code_labelt &src, unsigned indent);
175  // NOLINTNEXTLINE(whitespace/line_length)
176  std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
177  std::string convert_code_asm(const code_asmt &src, unsigned indent);
178  std::string convert_code_assign(const code_assignt &src, unsigned indent);
179  std::string convert_code_free(const codet &src, unsigned indent);
180  std::string convert_code_init(const codet &src, unsigned indent);
181  // NOLINTNEXTLINE(whitespace/line_length)
182  std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
183  std::string convert_code_for(const code_fort &src, unsigned indent);
184  std::string convert_code_while(const code_whilet &src, unsigned indent);
185  std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent);
186  std::string convert_code_block(const code_blockt &src, unsigned indent);
187  std::string convert_code_expression(const codet &src, unsigned indent);
188  std::string convert_code_return(const codet &src, unsigned indent);
189  std::string convert_code_goto(const codet &src, unsigned indent);
190  std::string convert_code_assume(const codet &src, unsigned indent);
191  std::string convert_code_assert(const codet &src, unsigned indent);
192  std::string convert_code_break(const codet &src, unsigned indent);
193  std::string convert_code_switch(const codet &src, unsigned indent);
194  std::string convert_code_continue(const codet &src, unsigned indent);
195  std::string convert_code_decl(const codet &src, unsigned indent);
196  std::string convert_code_decl_block(const codet &src, unsigned indent);
197  std::string convert_code_dead(const codet &src, unsigned indent);
198  // NOLINTNEXTLINE(whitespace/line_length)
199  std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
200  std::string convert_code_lock(const codet &src, unsigned indent);
201  std::string convert_code_unlock(const codet &src, unsigned indent);
202  std::string convert_code_printf(const codet &src, unsigned indent);
203  std::string convert_code_fence(const codet &src, unsigned indent);
204  std::string convert_code_input(const codet &src, unsigned indent);
205  std::string convert_code_output(const codet &src, unsigned indent);
206  std::string convert_code_array_set(const codet &src, unsigned indent);
207  std::string convert_code_array_copy(const codet &src, unsigned indent);
208  std::string convert_code_array_replace(const codet &src, unsigned indent);
209 
210  virtual std::string convert_with_precedence(
211  const exprt &src, unsigned &precedence);
212 
213  // NOLINTNEXTLINE(whitespace/line_length)
214  std::string convert_function_application(const function_application_exprt &src, unsigned &precedence);
215  // NOLINTNEXTLINE(whitespace/line_length)
216  std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence);
217  std::string convert_malloc(const exprt &src, unsigned &precedence);
218  std::string convert_nondet(const exprt &src, unsigned &precedence);
219  std::string convert_prob_coin(const exprt &src, unsigned &precedence);
220  std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
221  // NOLINTNEXTLINE(whitespace/line_length)
222  std::string convert_statement_expression(const exprt &src, unsigned &precendence);
223 
224  virtual std::string convert_symbol(const exprt &src, unsigned &precedence);
225  std::string convert_predicate_symbol(const exprt &src, unsigned &precedence);
226  // NOLINTNEXTLINE(whitespace/line_length)
227  std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence);
228  // NOLINTNEXTLINE(whitespace/line_length)
229  std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence);
230  std::string convert_nondet_symbol(const exprt &src, 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 
252  std::string convert_struct(
253  const exprt &src,
254  unsigned &precedence,
255  bool include_padding_components);
256 };
257 
258 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
Definition: expr2c.cpp:1142
The type of an expression.
Definition: type.h:20
std::string convert_code_assume(const codet &src, unsigned indent)
Definition: expr2c.cpp:3208
semantic type conversion
Definition: std_expr.h:1725
std::string convert_complex(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1228
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:652
void get_shorthands(const exprt &expr)
Definition: expr2c.cpp:95
application of (mathematical) function
Definition: std_expr.h:3785
std::string convert_code_expression(const codet &src, unsigned indent)
Definition: expr2c.cpp:2780
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1180
std::string convert_code_continue(const codet &src, unsigned indent)
Definition: expr2c.cpp:2640
std::string convert_code_fence(const codet &src, unsigned indent)
Definition: expr2c.cpp:3057
std::string convert_Hoare(const exprt &src)
Definition: expr2c.cpp:3274
std::string convert_union(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2079
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1344
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
Definition: expr2c.cpp:3239
std::string convert_overflow(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2346
std::string convert_code_block(const code_blockt &src, unsigned indent)
Definition: expr2c.cpp:2742
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3269
std::string convert_array_of(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1279
std::string convert_code_unlock(const codet &src, unsigned indent)
Definition: expr2c.cpp:2974
virtual std::string convert_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1591
A constant literal expression.
Definition: std_expr.h:3685
std::string convert_code_break(const codet &src, unsigned indent)
Definition: expr2c.cpp:2586
std::string convert_code_decl(const codet &src, unsigned indent)
Definition: expr2c.cpp:2651
std::string convert_code_return(const codet &src, unsigned indent)
Definition: expr2c.cpp:2552
std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1649
std::unordered_map< irep_idt, irep_idt, irep_id_hash > shorthands
Definition: expr2c_class.h:70
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:158
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:2987
std::string convert_malloc(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1106
irep_idt id_shorthand(const irep_idt &identifier) const
Definition: expr2c.cpp:55
std::string convert_sizeof(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3349
std::string convert_code_printf(const codet &src, unsigned indent)
Definition: expr2c.cpp:3035
unsigned sizeof_nesting
Definition: expr2c_class.h:72
Extract member of struct or union.
Definition: std_expr.h:3214
std::string convert_binary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:1014
std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1657
std::string convert_code_free(const codet &src, unsigned indent)
Definition: expr2c.cpp:2939
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1704
std::string convert_unary(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1063
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1944
std::string convert_literal(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1163
std::string convert_code_assign(const code_assignt &src, unsigned indent)
Definition: expr2c.cpp:2928
std::string convert_code_label(const code_labelt &src, unsigned indent)
Definition: expr2c.cpp:3221
std::unordered_map< irep_idt, std::unordered_set< irep_idt, irep_id_hash >, irep_id_hash > ns_collision
Definition: expr2c_class.h:69
std::string convert_byte_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1314
std::string convert_pointer_object_has_type(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1086
std::string convert_nondet_bool(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1673
std::string convert_code_input(const codet &src, unsigned indent)
Definition: expr2c.cpp:3087
virtual ~expr2ct()
Definition: expr2c_class.h:27
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1153
std::string convert_index_designator(const exprt &src)
Definition: expr2c.cpp:1474
std::string convert_code_array_set(const codet &src, unsigned indent)
Definition: expr2c.cpp:3130
std::string convert_member(const member_exprt &src, unsigned precedence)
Definition: expr2c.cpp:1484
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1427
std::string convert_trinary(const exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
Definition: expr2c.cpp:795
API to expression classes.
std::string convert_code_asm(const code_asmt &src, unsigned indent)
Definition: expr2c.cpp:2382
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::string convert_initializer_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2240
std::string convert_code_dead(const codet &src, unsigned indent)
Definition: expr2c.cpp:2691
A label for branch targets.
Definition: std_code.h:760
std::string convert_code_lock(const codet &src, unsigned indent)
Definition: expr2c.cpp:2961
virtual std::string convert_array_type(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator_str)
To generate a C-like type declaration of an array.
Definition: expr2c.cpp:725
A function call.
Definition: std_code.h:657
std::string convert_array_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2206
std::string convert_with(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:868
const namespacet & ns
Definition: expr2c_class.h:35
A `while&#39; instruction.
Definition: std_code.h:457
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1170
std::string convert_extractbits(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3332
std::string convert_extractbit(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3317
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence)
Definition: expr2c.cpp:2316
std::string convert_vector(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2032
std::string convert_concatenation(const exprt &src, unsigned &precedence)
std::string convert_predicate_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1641
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:163
std::string convert_nondet(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1132
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1580
std::string convert_code_assert(const codet &src, unsigned indent)
Definition: expr2c.cpp:3195
std::string convert_index(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1366
std::string convert_array_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1560
A function call side effect.
Definition: std_code.h:1052
std::string convert_byte_extract(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1289
std::string convert_member_designator(const exprt &src)
Definition: expr2c.cpp:1464
std::string convert_nondet_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1633
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
Definition: expr2c.cpp:2486
std::string convert_quantified_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1665
std::string convert_code_array_copy(const codet &src, unsigned indent)
Definition: expr2c.cpp:3152
Base class for all expressions.
Definition: expr.h:46
std::string convert_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:936
std::string convert_cond(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:980
std::string convert_code_for(const code_fort &src, unsigned indent)
Definition: expr2c.cpp:2705
A `do while&#39; instruction.
Definition: std_code.h:502
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3363
An inline assembler statement.
Definition: std_code.h:920
std::string convert_code_decl_block(const codet &src, unsigned indent)
Definition: expr2c.cpp:2765
std::string convert_code_array_replace(const codet &src, unsigned indent)
Definition: expr2c.cpp:3174
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1390
Sequential composition.
Definition: std_code.h:63
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1570
std::string convert_array(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2100
An if-then-else.
Definition: std_code.h:350
std::string convert_designated_initializer(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2268
A switch-case.
Definition: std_code.h:817
std::string convert_code_goto(const codet &src, unsigned indent)
Definition: expr2c.cpp:2574
dstringt irep_idt
Definition: irep.h:32
A statement in a programming language.
Definition: std_code.h:19
A `for&#39; instruction.
Definition: std_code.h:547
std::string convert_comma(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1204
std::string convert_code_while(const code_whilet &src, unsigned indent)
Definition: expr2c.cpp:2460
std::string convert_code_output(const codet &src, unsigned indent)
Definition: expr2c.cpp:3109
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1680
std::string convert_code_init(const codet &src, unsigned indent)
Definition: expr2c.cpp:2952
std::string convert_quantifier(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:846
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
Definition: expr2c.cpp:1935
std::string convert_code_switch(const codet &src, unsigned indent)
Definition: expr2c.cpp:2597
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:761
Assignment.
Definition: std_code.h:144
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2377
std::string convert_function_application(const function_application_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2286
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
Definition: expr2c.cpp:2515