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 "expr2c.h"
14 
15 #include <string>
16 #include <unordered_map>
17 #include <unordered_set>
18 
19 #include <util/std_code.h>
20 #include <util/std_expr.h>
21 
22 class qualifierst;
23 class namespacet;
24 
25 class expr2ct
26 {
27 public:
28  explicit expr2ct(
29  const namespacet &_ns,
33  {
34  }
35  virtual ~expr2ct() { }
36 
37  virtual std::string convert(const typet &src);
38  virtual std::string convert(const exprt &src);
39 
40  void get_shorthands(const exprt &expr);
41 
42  std::string
43  convert_with_identifier(const typet &src, const std::string &identifier);
44 
45 protected:
46  const namespacet &ns;
48 
49  virtual std::string convert_rec(
50  const typet &src,
51  const qualifierst &qualifiers,
52  const std::string &declarator);
53 
54  virtual std::string convert_struct_type(
55  const typet &src,
56  const std::string &qualifiers_str,
57  const std::string &declarator_str);
58 
59  std::string convert_struct_type(
60  const typet &src,
61  const std::string &qualifer_str,
62  const std::string &declarator_str,
63  bool inc_struct_body,
64  bool inc_padding_components);
65 
66  virtual std::string convert_array_type(
67  const typet &src,
68  const qualifierst &qualifiers,
69  const std::string &declarator_str);
70 
71  std::string convert_array_type(
72  const typet &src,
73  const qualifierst &qualifiers,
74  const std::string &declarator_str,
75  bool inc_size_if_possible);
76 
77  static std::string indent_str(unsigned indent);
78 
79  std::unordered_map<irep_idt, std::unordered_set<irep_idt>> ns_collision;
80  std::unordered_map<irep_idt, irep_idt> shorthands;
81 
82  unsigned sizeof_nesting;
83 
84  irep_idt id_shorthand(const irep_idt &identifier) const;
85 
86  std::string convert_typecast(
87  const typecast_exprt &src, unsigned &precedence);
88 
89  std::string convert_pointer_arithmetic(
90  const exprt &src,
91  unsigned &precedence);
92 
93  std::string convert_pointer_difference(
94  const exprt &src,
95  unsigned &precedence);
96 
97  std::string convert_binary(
98  const exprt &src, const std::string &symbol,
99  unsigned precedence, bool full_parentheses);
100 
101  std::string convert_multi_ary(
102  const exprt &src, const std::string &symbol,
103  unsigned precedence, bool full_parentheses);
104 
105  std::string convert_cond(
106  const exprt &src, unsigned precedence);
107 
108  std::string convert_struct_member_value(
109  const exprt &src, unsigned precedence);
110 
111  std::string convert_array_member_value(
112  const exprt &src, unsigned precedence);
113 
114  std::string convert_member(
115  const member_exprt &src, unsigned precedence);
116 
117  std::string convert_array_of(const exprt &src, unsigned precedence);
118 
119  std::string convert_trinary(
120  const exprt &src, const std::string &symbol1,
121  const std::string &symbol2, unsigned precedence);
122 
123  std::string convert_overflow(
124  const exprt &src, unsigned &precedence);
125 
126  std::string convert_quantifier(
127  const exprt &src, const std::string &symbol,
128  unsigned precedence);
129 
130  std::string convert_with(
131  const exprt &src, unsigned precedence);
132 
133  std::string convert_update(
134  const exprt &src, unsigned precedence);
135 
136  std::string convert_member_designator(
137  const exprt &src);
138 
139  std::string convert_index_designator(
140  const exprt &src);
141 
142  std::string convert_index(
143  const exprt &src, unsigned precedence);
144 
145  std::string convert_byte_extract(
146  const exprt &src,
147  unsigned precedence);
148 
149  std::string convert_byte_update(
150  const exprt &src,
151  unsigned precedence);
152 
153  std::string convert_extractbit(
154  const exprt &src,
155  unsigned precedence);
156 
157  std::string convert_extractbits(
158  const exprt &src,
159  unsigned precedence);
160 
161  std::string convert_unary(
162  const exprt &src, const std::string &symbol,
163  unsigned precedence);
164 
165  std::string convert_unary_post(
166  const exprt &src, const std::string &symbol,
167  unsigned precedence);
168 
169  std::string convert_function(
170  const exprt &src, const std::string &symbol,
171  unsigned precedence);
172 
173  std::string convert_complex(
174  const exprt &src,
175  unsigned precedence);
176 
177  std::string convert_comma(
178  const exprt &src,
179  unsigned precedence);
180 
181  std::string convert_Hoare(const exprt &src);
182 
183  std::string convert_code(const codet &src);
184  virtual std::string convert_code(const codet &src, unsigned indent);
185  std::string convert_code_label(const code_labelt &src, unsigned indent);
186  // NOLINTNEXTLINE(whitespace/line_length)
187  std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
188  std::string convert_code_asm(const code_asmt &src, unsigned indent);
189  std::string convert_code_assign(const code_assignt &src, unsigned indent);
190  // NOLINTNEXTLINE(whitespace/line_length)
191  std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
192  std::string convert_code_for(const code_fort &src, unsigned indent);
193  std::string convert_code_while(const code_whilet &src, unsigned indent);
194  std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent);
195  std::string convert_code_block(const code_blockt &src, unsigned indent);
196  std::string convert_code_expression(const codet &src, unsigned indent);
197  std::string convert_code_return(const codet &src, unsigned indent);
198  std::string convert_code_goto(const codet &src, unsigned indent);
199  std::string convert_code_assume(const codet &src, unsigned indent);
200  std::string convert_code_assert(const codet &src, unsigned indent);
201  std::string convert_code_break(const codet &src, unsigned indent);
202  std::string convert_code_switch(const codet &src, unsigned indent);
203  std::string convert_code_continue(const codet &src, unsigned indent);
204  std::string convert_code_decl(const codet &src, unsigned indent);
205  std::string convert_code_decl_block(const codet &src, unsigned indent);
206  std::string convert_code_dead(const codet &src, unsigned indent);
207  // NOLINTNEXTLINE(whitespace/line_length)
208  std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
209  std::string convert_code_lock(const codet &src, unsigned indent);
210  std::string convert_code_unlock(const codet &src, unsigned indent);
211  std::string convert_code_printf(const codet &src, unsigned indent);
212  std::string convert_code_fence(const codet &src, unsigned indent);
213  std::string convert_code_input(const codet &src, unsigned indent);
214  std::string convert_code_output(const codet &src, unsigned indent);
215  std::string convert_code_array_set(const codet &src, unsigned indent);
216  std::string convert_code_array_copy(const codet &src, unsigned indent);
217  std::string convert_code_array_replace(const codet &src, unsigned indent);
218 
219  virtual std::string convert_with_precedence(
220  const exprt &src, unsigned &precedence);
221 
222  // NOLINTNEXTLINE(whitespace/line_length)
223  std::string convert_function_application(const function_application_exprt &src, unsigned &precedence);
224  // NOLINTNEXTLINE(whitespace/line_length)
225  std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence);
226  std::string convert_allocate(const exprt &src, unsigned &precedence);
227  std::string convert_nondet(const exprt &src, unsigned &precedence);
228  std::string convert_prob_coin(const exprt &src, unsigned &precedence);
229  std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
230  // NOLINTNEXTLINE(whitespace/line_length)
231  std::string convert_statement_expression(const exprt &src, unsigned &precendence);
232 
233  virtual std::string convert_symbol(const exprt &src, unsigned &precedence);
234  std::string convert_predicate_symbol(const exprt &src, unsigned &precedence);
235  // NOLINTNEXTLINE(whitespace/line_length)
236  std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence);
237  // NOLINTNEXTLINE(whitespace/line_length)
238  std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence);
239  // NOLINTNEXTLINE(whitespace/line_length)
240  std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence);
241  std::string convert_quantified_symbol(const exprt &src, unsigned &precedence);
242  std::string convert_nondet_bool(const exprt &src, unsigned &precedence);
243  std::string convert_object_descriptor(const exprt &src, unsigned &precedence);
244  std::string convert_literal(const exprt &src, unsigned &precedence);
245  // NOLINTNEXTLINE(whitespace/line_length)
246  virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence);
247  virtual std::string convert_constant_bool(bool boolean_value);
248 
249  std::string convert_norep(const exprt &src, unsigned &precedence);
250 
251  virtual std::string convert_struct(const exprt &src, unsigned &precedence);
252  std::string convert_union(const exprt &src, unsigned &precedence);
253  std::string convert_vector(const exprt &src, unsigned &precedence);
254  std::string convert_array(const exprt &src, unsigned &precedence);
255  std::string convert_array_list(const exprt &src, unsigned &precedence);
256  std::string convert_initializer_list(const exprt &src, unsigned &precedence);
257  // NOLINTNEXTLINE(whitespace/line_length)
258  std::string convert_designated_initializer(const exprt &src, unsigned &precedence);
259  std::string convert_concatenation(const exprt &src, unsigned &precedence);
260  std::string convert_sizeof(const exprt &src, unsigned &precedence);
261  std::string convert_let(const let_exprt &, unsigned precedence);
262 
263  std::string convert_struct(
264  const exprt &src,
265  unsigned &precedence,
266  bool include_padding_components);
267 };
268 
269 #endif // CPROVER_ANSI_C_EXPR2C_CLASS_H
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
Definition: expr2c.cpp:1225
The type of an expression, extends irept.
Definition: type.h:27
std::string convert_code_assume(const codet &src, unsigned indent)
Definition: expr2c.cpp:3272
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:188
Semantic type conversion.
Definition: std_expr.h:2277
std::string convert_complex(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1311
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:675
void get_shorthands(const exprt &expr)
Definition: expr2c.cpp:109
Application of (mathematical) function.
Definition: std_expr.h:4481
std::string convert_code_expression(const codet &src, unsigned indent)
Definition: expr2c.cpp:2866
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:1116
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1263
Used for configuring the behaviour of expr2c and type2c.
Definition: expr2c.h:20
std::string convert_code_continue(const codet &src, unsigned indent)
Definition: expr2c.cpp:2721
std::string convert_code_fence(const codet &src, unsigned indent)
Definition: expr2c.cpp:3121
std::string convert_Hoare(const exprt &src)
Definition: expr2c.cpp:3339
std::string convert_union(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2163
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1427
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
Definition: expr2c.cpp:3304
std::string convert_overflow(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2427
std::string convert_code_block(const code_blockt &src, unsigned indent)
Definition: expr2c.cpp:2828
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3334
std::string convert_array_of(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1362
std::string convert_code_unlock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3038
virtual std::string convert_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1674
A constant literal expression.
Definition: std_expr.h:4384
std::string convert_code_break(const codet &src, unsigned indent)
Definition: expr2c.cpp:2667
std::string convert_code_decl(const codet &src, unsigned indent)
Definition: expr2c.cpp:2732
std::string convert_code_return(const codet &src, unsigned indent)
Definition: expr2c.cpp:2633
std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1732
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:183
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:3948
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2c.cpp:3051
std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence)
Definition: expr2c.cpp:1716
irep_idt id_shorthand(const irep_idt &identifier) const
Definition: expr2c.cpp:66
std::string convert_sizeof(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3414
const expr2c_configurationt & configuration
Definition: expr2c_class.h:47
std::string convert_code_printf(const codet &src, unsigned indent)
Definition: expr2c.cpp:3099
expr2ct(const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration)
Definition: expr2c_class.h:28
unsigned sizeof_nesting
Definition: expr2c_class.h:82
Extract member of struct or union.
Definition: std_expr.h:3890
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:55
std::string convert_binary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:1061
std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1740
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1787
std::string convert_unary(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1165
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2027
std::string convert_literal(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1246
std::string convert_code_assign(const code_assignt &src, unsigned indent)
Definition: expr2c.cpp:3014
std::string convert_code_label(const code_labelt &src, unsigned indent)
Definition: expr2c.cpp:3286
std::string convert_byte_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1397
std::string convert_nondet_bool(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1756
std::string convert_code_input(const codet &src, unsigned indent)
Definition: expr2c.cpp:3151
virtual ~expr2ct()
Definition: expr2c_class.h:35
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
Definition: expr2c_class.h:79
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1236
std::string convert_index_designator(const exprt &src)
Definition: expr2c.cpp:1557
std::string convert_code_array_set(const codet &src, unsigned indent)
Definition: expr2c.cpp:3194
std::string convert_member(const member_exprt &src, unsigned precedence)
Definition: expr2c.cpp:1567
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1510
std::string convert_trinary(const exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
Definition: expr2c.cpp:823
API to expression classes.
std::string convert_code_asm(const code_asmt &src, unsigned indent)
Definition: expr2c.cpp:2463
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
std::string convert_initializer_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2321
std::string convert_code_dead(const codet &src, unsigned indent)
Definition: expr2c.cpp:2777
codet representation of a label for branch targets.
Definition: std_code.h:1256
std::string convert_code_lock(const codet &src, unsigned indent)
Definition: expr2c.cpp:3025
codet representation of a function call statement.
Definition: std_code.h:1036
std::string convert_array_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2287
std::string convert_with(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:895
const namespacet & ns
Definition: expr2c_class.h:46
codet representing a while statement.
Definition: std_code.h:767
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1253
std::unordered_map< irep_idt, irep_idt > shorthands
Definition: expr2c_class.h:80
std::string convert_extractbits(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3397
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
std::string convert_extractbit(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:3382
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence)
Definition: expr2c.cpp:2397
std::string convert_vector(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2116
std::string convert_concatenation(const exprt &src, unsigned &precedence)
std::string convert_predicate_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1724
std::string convert_nondet(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1215
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1663
std::string convert_code_assert(const codet &src, unsigned indent)
Definition: expr2c.cpp:3259
std::string convert_index(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1449
std::string convert_array_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1643
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1691
std::string convert_byte_extract(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1372
std::string convert_member_designator(const exprt &src)
Definition: expr2c.cpp:1547
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
Definition: expr2c.cpp:2567
Expression to hold a nondeterministic choice.
Definition: std_expr.h:277
std::string convert_quantified_symbol(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1748
std::string convert_code_array_copy(const codet &src, unsigned indent)
Definition: expr2c.cpp:3216
Base class for all expressions.
Definition: expr.h:54
std::string convert_update(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:983
std::string convert_cond(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1027
std::string convert_code_for(const code_fort &src, unsigned indent)
Definition: expr2c.cpp:2791
codet representation of a do while statement.
Definition: std_code.h:829
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3428
codet representation of an inline assembler statement.
Definition: std_code.h:1459
std::string convert_code_decl_block(const codet &src, unsigned indent)
Definition: expr2c.cpp:2851
std::string convert_code_array_replace(const codet &src, unsigned indent)
Definition: expr2c.cpp:3238
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1473
A codet representing sequential composition of program statements.
Definition: std_code.h:150
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1653
std::string convert_array(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2184
std::string convert_allocate(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1188
codet representation of an if-then-else statement.
Definition: std_code.h:614
std::string convert_designated_initializer(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2349
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1326
std::string convert_code_goto(const codet &src, unsigned indent)
Definition: expr2c.cpp:2655
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
codet representation of a for statement.
Definition: std_code.h:893
std::string convert_comma(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1287
A let expression.
Definition: std_expr.h:4635
std::string convert_code_while(const code_whilet &src, unsigned indent)
Definition: expr2c.cpp:2541
std::string convert_code_output(const codet &src, unsigned indent)
Definition: expr2c.cpp:3173
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1763
std::string convert_quantifier(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:873
std::string convert_let(const let_exprt &, unsigned precedence)
Definition: expr2c.cpp:963
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
Definition: expr2c.cpp:2019
std::string convert_code_switch(const codet &src, unsigned indent)
Definition: expr2c.cpp:2678
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:789
A codet representing an assignment in the program.
Definition: std_code.h:256
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2458
std::string convert_function_application(const function_application_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2367
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:752
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
Definition: expr2c.cpp:2596