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/bitvector_expr.h>
20 #include <util/byte_operators.h>
21 #include <util/mathematical_expr.h>
22 #include <util/std_code.h>
23 #include <util/std_expr.h>
24 
25 class qualifierst;
26 class namespacet;
27 
28 class expr2ct
29 {
30 public:
31  explicit expr2ct(
32  const namespacet &_ns,
36  {
37  }
38  virtual ~expr2ct() { }
39 
40  virtual std::string convert(const typet &src);
41  virtual std::string convert(const exprt &src);
42 
43  void get_shorthands(const exprt &expr);
44 
45  std::string
46  convert_with_identifier(const typet &src, const std::string &identifier);
47 
48 protected:
49  const namespacet &ns;
51 
52  virtual std::string convert_rec(
53  const typet &src,
54  const qualifierst &qualifiers,
55  const std::string &declarator);
56 
57  virtual std::string convert_struct_type(
58  const typet &src,
59  const std::string &qualifiers_str,
60  const std::string &declarator_str);
61 
62  std::string convert_struct_type(
63  const typet &src,
64  const std::string &qualifer_str,
65  const std::string &declarator_str,
66  bool inc_struct_body,
67  bool inc_padding_components);
68 
69  virtual std::string convert_array_type(
70  const typet &src,
71  const qualifierst &qualifiers,
72  const std::string &declarator_str);
73 
74  std::string convert_array_type(
75  const typet &src,
76  const qualifierst &qualifiers,
77  const std::string &declarator_str,
78  bool inc_size_if_possible);
79 
80  static std::string indent_str(unsigned indent);
81 
82  std::unordered_map<irep_idt, std::unordered_set<irep_idt>> ns_collision;
83  std::unordered_map<irep_idt, irep_idt> shorthands;
84 
85  unsigned sizeof_nesting;
86 
87  irep_idt id_shorthand(const irep_idt &identifier) const;
88 
89  std::string convert_typecast(
90  const typecast_exprt &src, unsigned &precedence);
91 
92  std::string convert_pointer_arithmetic(
93  const exprt &src,
94  unsigned &precedence);
95 
96  std::string convert_pointer_difference(
97  const exprt &src,
98  unsigned &precedence);
99 
100  std::string convert_binary(
101  const binary_exprt &,
102  const std::string &symbol,
103  unsigned precedence,
104  bool full_parentheses);
105 
106  std::string convert_multi_ary(
107  const exprt &src, const std::string &symbol,
108  unsigned precedence, bool full_parentheses);
109 
110  std::string convert_cond(
111  const exprt &src, unsigned precedence);
112 
113  std::string convert_struct_member_value(
114  const exprt &src, unsigned precedence);
115 
116  std::string convert_array_member_value(
117  const exprt &src, unsigned precedence);
118 
119  std::string convert_member(
120  const member_exprt &src, unsigned precedence);
121 
122  std::string convert_array_of(const exprt &src, unsigned precedence);
123 
124  std::string convert_trinary(
125  const ternary_exprt &src,
126  const std::string &symbol1,
127  const std::string &symbol2,
128  unsigned precedence);
129 
130  std::string convert_overflow(
131  const exprt &src, unsigned &precedence);
132 
133  std::string convert_quantifier(
134  const quantifier_exprt &,
135  const std::string &symbol,
136  unsigned precedence);
137 
138  std::string convert_with(
139  const exprt &src, unsigned precedence);
140 
141  std::string convert_update(const update_exprt &, unsigned precedence);
142 
143  std::string convert_member_designator(
144  const exprt &src);
145 
146  std::string convert_index_designator(
147  const exprt &src);
148 
149  std::string convert_index(
150  const exprt &src, unsigned precedence);
151 
152  std::string
153  convert_byte_extract(const byte_extract_exprt &, unsigned precedence);
154 
155  std::string
156  convert_byte_update(const byte_update_exprt &, unsigned precedence);
157 
158  std::string convert_extractbit(const extractbit_exprt &, unsigned precedence);
159 
160  std::string
161  convert_extractbits(const extractbits_exprt &src, unsigned precedence);
162 
163  std::string convert_unary(
164  const unary_exprt &,
165  const std::string &symbol,
166  unsigned precedence);
167 
168  std::string convert_unary_post(
169  const exprt &src, const std::string &symbol,
170  unsigned precedence);
171 
172  std::string convert_function(const exprt &src, const std::string &symbol);
173 
174  std::string convert_complex(
175  const exprt &src,
176  unsigned precedence);
177 
178  std::string convert_comma(
179  const exprt &src,
180  unsigned precedence);
181 
182  std::string convert_Hoare(const exprt &src);
183 
184  std::string convert_code(const codet &src);
185  virtual std::string convert_code(const codet &src, unsigned indent);
186  std::string convert_code_label(const code_labelt &src, unsigned indent);
187  // NOLINTNEXTLINE(whitespace/line_length)
188  std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
189  std::string convert_code_asm(const code_asmt &src, unsigned indent);
190  std::string convert_code_assign(const code_assignt &src, unsigned indent);
191  // NOLINTNEXTLINE(whitespace/line_length)
192  std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
193  std::string convert_code_for(const code_fort &src, unsigned indent);
194  std::string convert_code_while(const code_whilet &src, unsigned indent);
195  std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent);
196  std::string convert_code_block(const code_blockt &src, unsigned indent);
197  std::string convert_code_expression(const codet &src, unsigned indent);
198  std::string convert_code_return(const codet &src, unsigned indent);
199  std::string convert_code_goto(const codet &src, unsigned indent);
200  std::string convert_code_assume(const codet &src, unsigned indent);
201  std::string convert_code_assert(const codet &src, unsigned indent);
202  std::string convert_code_break(unsigned indent);
203  std::string convert_code_switch(const codet &src, unsigned indent);
204  std::string convert_code_continue(unsigned indent);
205  std::string convert_code_decl(const codet &src, unsigned indent);
206  std::string convert_code_decl_block(const codet &src, unsigned indent);
207  std::string convert_code_dead(const codet &src, unsigned indent);
208  // NOLINTNEXTLINE(whitespace/line_length)
209  std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
210  std::string convert_code_lock(const codet &src, unsigned indent);
211  std::string convert_code_unlock(const codet &src, unsigned indent);
212  std::string convert_code_printf(const codet &src, unsigned indent);
213  std::string convert_code_fence(const codet &src, unsigned indent);
214  std::string convert_code_input(const codet &src, unsigned indent);
215  std::string convert_code_output(const codet &src, unsigned indent);
216  std::string convert_code_array_set(const codet &src, unsigned indent);
217  std::string convert_code_array_copy(const codet &src, unsigned indent);
218  std::string convert_code_array_replace(const codet &src, unsigned indent);
219 
220  virtual std::string convert_with_precedence(
221  const exprt &src, unsigned &precedence);
222 
223  std::string
227  std::string convert_allocate(const exprt &src, unsigned &precedence);
228  std::string convert_nondet(const exprt &src, unsigned &precedence);
229  std::string convert_prob_coin(const exprt &src, unsigned &precedence);
230  std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
231  // NOLINTNEXTLINE(whitespace/line_length)
232  std::string convert_statement_expression(const exprt &src, unsigned &precendence);
233 
234  virtual std::string convert_symbol(const exprt &src);
235  std::string convert_predicate_symbol(const exprt &src);
236  std::string convert_predicate_next_symbol(const exprt &src);
237  std::string convert_predicate_passive_symbol(const exprt &src);
238  std::string convert_nondet_symbol(const nondet_symbol_exprt &);
239  std::string convert_quantified_symbol(const exprt &src);
240  std::string convert_nondet_bool();
241  std::string convert_object_descriptor(const exprt &src, unsigned &precedence);
242  std::string convert_literal(const exprt &src);
243  // NOLINTNEXTLINE(whitespace/line_length)
244  virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence);
245  virtual std::string convert_constant_bool(bool boolean_value);
246 
247  std::string convert_norep(const exprt &src, unsigned &precedence);
248 
249  virtual std::string convert_struct(const exprt &src, unsigned &precedence);
250  std::string convert_union(const exprt &src, unsigned &precedence);
251  std::string convert_vector(const exprt &src, unsigned &precedence);
252  std::string convert_array(const exprt &src);
253  std::string convert_array_list(const exprt &src, unsigned &precedence);
254  std::string convert_initializer_list(const exprt &src);
255  std::string convert_designated_initializer(const exprt &src);
256  std::string convert_concatenation(const exprt &src, unsigned &precedence);
257  std::string convert_sizeof(const exprt &src, unsigned &precedence);
258  std::string convert_let(const let_exprt &, unsigned precedence);
259 
260  std::string convert_struct(
261  const exprt &src,
262  unsigned &precedence,
263  bool include_padding_components);
264 };
265 
266 #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:551
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:1701
A codet representing an assignment in the program.
Definition: std_code.h:295
A codet representing sequential composition of program statements.
Definition: std_code.h:170
codet representation of a do while statement.
Definition: std_code.h:990
codet representation of a for statement.
Definition: std_code.h:1052
codet representation of a function call statement.
Definition: std_code.h:1215
codet representation of an if-then-else statement.
Definition: std_code.h:778
codet representation of a label for branch targets.
Definition: std_code.h:1407
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1471
codet representing a while statement.
Definition: std_code.h:928
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
A constant literal expression.
Definition: std_expr.h:2668
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:1137
std::string convert_literal(const exprt &src)
Definition: expr2c.cpp:1172
std::string convert_code_continue(unsigned indent)
Definition: expr2c.cpp:2668
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:686
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
Definition: expr2c.cpp:3265
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:723
std::string convert_comma(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1209
std::string convert_code_assert(const codet &src, unsigned indent)
Definition: expr2c.cpp:3220
std::string convert_quantifier(const quantifier_exprt &, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:804
std::string convert_union(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2097
std::string convert_code_expression(const codet &src, unsigned indent)
Definition: expr2c.cpp:2811
std::string convert_code_goto(const codet &src, unsigned indent)
Definition: expr2c.cpp:2604
std::string convert_code_switch(const codet &src, unsigned indent)
Definition: expr2c.cpp:2625
std::string convert_initializer_list(const exprt &src)
Definition: expr2c.cpp:2251
std::string convert_quantified_symbol(const exprt &src)
Definition: expr2c.cpp:1658
std::string convert_function_application(const function_application_exprt &src)
Definition: expr2c.cpp:2320
std::string convert_code_unlock(const codet &src, unsigned indent)
Definition: expr2c.cpp:2999
std::string convert_code_decl_block(const codet &src, unsigned indent)
Definition: expr2c.cpp:2796
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2408
std::string convert_byte_update(const byte_update_exprt &, unsigned precedence)
Definition: expr2c.cpp:1319
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3295
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1390
std::string convert_let(const let_exprt &, unsigned precedence)
Definition: expr2c.cpp:896
std::string convert_nondet_bool()
Definition: expr2c.cpp:1664
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1580
const expr2c_configurationt & configuration
Definition: expr2c_class.h:50
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
Definition: expr2c_class.h:82
std::string convert_code_output(const codet &src, unsigned indent)
Definition: expr2c.cpp:3134
std::string convert_code_while(const code_whilet &src, unsigned indent)
Definition: expr2c.cpp:2491
std::string convert_index_designator(const exprt &src)
Definition: expr2c.cpp:1476
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1427
std::string convert_code_block(const code_blockt &src, unsigned indent)
Definition: expr2c.cpp:2773
std::string convert_code_asm(const code_asmt &src, unsigned indent)
Definition: expr2c.cpp:2413
std::string convert_allocate(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1110
std::string convert_Hoare(const exprt &src)
Definition: expr2c.cpp:3300
std::string convert_sizeof(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3367
std::string convert_code_lock(const codet &src, unsigned indent)
Definition: expr2c.cpp:2986
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
Definition: expr2c.cpp:2517
irep_idt id_shorthand(const irep_idt &identifier) const
Definition: expr2c.cpp:77
std::string convert_cond(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:955
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src)
Definition: expr2c.cpp:2348
std::string convert_overflow(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2377
std::string convert_member(const member_exprt &src, unsigned precedence)
Definition: expr2c.cpp:1486
void get_shorthands(const exprt &expr)
Definition: expr2c.cpp:118
std::string convert_code_for(const code_fort &src, unsigned indent)
Definition: expr2c.cpp:2736
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:3914
std::string convert_extractbits(const extractbits_exprt &src, unsigned precedence)
Definition: expr2c.cpp:3355
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1961
std::string convert_code_decl(const codet &src, unsigned indent)
Definition: expr2c.cpp:2677
std::string convert_trinary(const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
Definition: expr2c.cpp:757
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1162
std::string convert_update(const update_exprt &, unsigned precedence)
Definition: expr2c.cpp:917
std::string convert_nondet_symbol(const nondet_symbol_exprt &)
Definition: expr2c.cpp:1634
std::string convert_code_printf(const codet &src, unsigned indent)
Definition: expr2c.cpp:3060
std::string convert_unary(const unary_exprt &, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1090
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
Definition: expr2c.cpp:2546
std::string convert_member_designator(const exprt &src)
Definition: expr2c.cpp:1466
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:192
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
Definition: expr2c.cpp:1293
std::string convert_code_label(const code_labelt &src, unsigned indent)
Definition: expr2c.cpp:3247
virtual std::string convert_symbol(const exprt &src)
Definition: expr2c.cpp:1591
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1693
std::string convert_code_array_copy(const codet &src, unsigned indent)
Definition: expr2c.cpp:3177
std::string convert_concatenation(const exprt &src, unsigned &precedence)
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
Definition: expr2c.cpp:1147
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1570
std::string convert_code_dead(const codet &src, unsigned indent)
Definition: expr2c.cpp:2722
const namespacet & ns
Definition: expr2c_class.h:49
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3381
std::string convert_designated_initializer(const exprt &src)
Definition: expr2c.cpp:2277
std::string convert_vector(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2050
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:1041
std::string convert_array_member_value(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1560
virtual ~expr2ct()
Definition: expr2c_class.h:38
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1344
std::unordered_map< irep_idt, irep_idt > shorthands
Definition: expr2c_class.h:83
std::string convert_complex(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1233
std::string convert_code_assign(const code_assignt &src, unsigned indent)
Definition: expr2c.cpp:2978
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2c.cpp:3012
std::string convert_code_fence(const codet &src, unsigned indent)
Definition: expr2c.cpp:3082
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:187
std::string convert_code_return(const codet &src, unsigned indent)
Definition: expr2c.cpp:2583
std::string convert_code_break(unsigned indent)
Definition: expr2c.cpp:2616
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:609
std::string convert_with(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:827
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1669
std::string convert_predicate_passive_symbol(const exprt &src)
Definition: expr2c.cpp:1652
std::string convert_array_list(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:2217
unsigned sizeof_nesting
Definition: expr2c_class.h:85
std::string convert_array_of(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1283
std::string convert_code_array_replace(const codet &src, unsigned indent)
Definition: expr2c.cpp:3199
std::string convert_index(const exprt &src, unsigned precedence)
Definition: expr2c.cpp:1366
std::string convert_code_assume(const codet &src, unsigned indent)
Definition: expr2c.cpp:3233
std::string convert_code_input(const codet &src, unsigned indent)
Definition: expr2c.cpp:3112
std::string convert_extractbit(const extractbit_exprt &, unsigned precedence)
Definition: expr2c.cpp:3344
std::string convert_predicate_next_symbol(const exprt &src)
Definition: expr2c.cpp:1646
std::string convert_code_array_set(const codet &src, unsigned indent)
Definition: expr2c.cpp:3155
std::string convert_function(const exprt &src, const std::string &symbol)
Definition: expr2c.cpp:1188
std::string convert_binary(const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)
Definition: expr2c.cpp:989
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
Definition: expr2c.cpp:1953
std::string convert_predicate_symbol(const exprt &src)
Definition: expr2c.cpp:1640
expr2ct(const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration)
Definition: expr2c_class.h:31
std::string convert_array(const exprt &src)
Definition: expr2c.cpp:2116
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1177
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:2816
Extract member of struct or union.
Definition: std_expr.h:2528
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
Expression to hold a nondeterministic choice.
Definition: std_expr.h:210
A base class for quantifier expressions.
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
An expression with three operands.
Definition: std_expr.h:54
Semantic type conversion.
Definition: std_expr.h:1781
The type of an expression, extends irept.
Definition: type.h:28
Generic base class for unary expressions.
Definition: std_expr.h:282
Operator to update elements in structs and arrays.
Definition: std_expr.h:2357
API to expression classes for 'mathematical' expressions.
API to expression classes.
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