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 
20 
21 #include <util/bitvector_expr.h>
22 #include <util/byte_operators.h>
23 #include <util/mathematical_expr.h>
24 #include <util/std_code.h>
25 
26 class qualifierst;
27 class namespacet;
28 
29 class expr2ct
30 {
31 public:
32  explicit expr2ct(
33  const namespacet &_ns,
37  {
38  }
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 
49 protected:
50  const namespacet &ns;
52 
53  virtual std::string convert_rec(
54  const typet &src,
55  const qualifierst &qualifiers,
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,
68  bool inc_padding_components);
69 
70  virtual std::string convert_array_type(
71  const typet &src,
72  const qualifierst &qualifiers,
73  const std::string &declarator_str);
74 
75  std::string convert_array_type(
76  const typet &src,
77  const qualifierst &qualifiers,
78  const std::string &declarator_str,
79  bool inc_size_if_possible);
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 
86  unsigned sizeof_nesting;
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 
93  std::string convert_pointer_arithmetic(
94  const exprt &src,
95  unsigned &precedence);
96 
97  std::string convert_pointer_difference(
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
163  convert_byte_extract(const byte_extract_exprt &, unsigned precedence);
164 
165  std::string
166  convert_byte_update(const byte_update_exprt &, unsigned precedence);
167 
168  std::string convert_extractbit(const extractbit_exprt &, unsigned precedence);
169 
170  std::string
171  convert_extractbits(const extractbits_exprt &src, unsigned precedence);
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,
277  bool include_padding_components);
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.
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.
Definition: std_code_base.h:29
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
Definition: expr2c_class.h:51
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
Definition: expr2c_class.h:83
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
Definition: expr2c_class.h:50
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()
Definition: expr2c_class.h:39
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
Definition: expr2c_class.h:84
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
Definition: expr2c_class.h:86
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)
Definition: expr2c_class.h:32
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.
nonstd::optional< T > optionalt
Definition: optional.h:35
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:71