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 
24 class qualifierst;
25 class namespacet;
26 
27 class expr2ct
28 {
29 public:
30  explicit expr2ct(
31  const namespacet &_ns,
35  {
36  }
37  virtual ~expr2ct() { }
38 
39  virtual std::string convert(const typet &src);
40  virtual std::string convert(const exprt &src);
41 
42  void get_shorthands(const exprt &expr);
43 
44  std::string
45  convert_with_identifier(const typet &src, const std::string &identifier);
46 
47 protected:
48  const namespacet &ns;
50 
51  virtual std::string convert_rec(
52  const typet &src,
53  const qualifierst &qualifiers,
54  const std::string &declarator);
55 
56  virtual std::string convert_struct_type(
57  const typet &src,
58  const std::string &qualifiers_str,
59  const std::string &declarator_str);
60 
61  std::string convert_struct_type(
62  const typet &src,
63  const std::string &qualifer_str,
64  const std::string &declarator_str,
65  bool inc_struct_body,
66  bool inc_padding_components);
67 
68  virtual std::string convert_array_type(
69  const typet &src,
70  const qualifierst &qualifiers,
71  const std::string &declarator_str);
72 
73  std::string convert_array_type(
74  const typet &src,
75  const qualifierst &qualifiers,
76  const std::string &declarator_str,
77  bool inc_size_if_possible);
78 
79  static std::string indent_str(unsigned indent);
80 
81  std::unordered_map<irep_idt, std::unordered_set<irep_idt>> ns_collision;
82  std::unordered_map<irep_idt, irep_idt> shorthands;
83 
84  unsigned sizeof_nesting;
85 
86  irep_idt id_shorthand(const irep_idt &identifier) const;
87 
88  std::string convert_typecast(
89  const typecast_exprt &src, unsigned &precedence);
90 
92  const exprt &src,
93  unsigned &precedence);
94 
96  const exprt &src,
97  unsigned &precedence);
98 
99  std::string convert_binary(
100  const binary_exprt &,
101  const std::string &symbol,
102  unsigned precedence,
103  bool full_parentheses);
104 
105  std::string convert_multi_ary(
106  const exprt &src, const std::string &symbol,
107  unsigned precedence, bool full_parentheses);
108 
109  std::string convert_cond(
110  const exprt &src, unsigned precedence);
111 
113  const exprt &src, unsigned precedence);
114 
116  const exprt &src, unsigned precedence);
117 
118  std::string convert_member(
119  const member_exprt &src, unsigned precedence);
120 
121  std::string convert_array_of(const exprt &src, unsigned precedence);
122 
123  std::string convert_trinary(
124  const ternary_exprt &src,
125  const std::string &symbol1,
126  const std::string &symbol2,
127  unsigned precedence);
128 
136  std::string convert_rox(const shift_exprt &src, unsigned precedence);
137 
138  std::string convert_overflow(
139  const exprt &src, unsigned &precedence);
140 
141  std::string convert_quantifier(
142  const quantifier_exprt &,
143  const std::string &symbol,
144  unsigned precedence);
145 
146  std::string convert_with(
147  const exprt &src, unsigned precedence);
148 
149  std::string convert_update(const update_exprt &, unsigned precedence);
150 
152  const exprt &src);
153 
155  const exprt &src);
156 
157  std::string convert_index(
158  const exprt &src, unsigned precedence);
159 
160  std::string
161  convert_byte_extract(const byte_extract_exprt &, unsigned precedence);
162 
163  std::string
164  convert_byte_update(const byte_update_exprt &, unsigned precedence);
165 
166  std::string convert_extractbit(const extractbit_exprt &, unsigned precedence);
167 
168  std::string
169  convert_extractbits(const extractbits_exprt &src, unsigned precedence);
170 
171  std::string convert_unary(
172  const unary_exprt &,
173  const std::string &symbol,
174  unsigned precedence);
175 
176  std::string convert_unary_post(
177  const exprt &src, const std::string &symbol,
178  unsigned precedence);
179 
183  std::string convert_function(const exprt &src, const std::string &symbol);
184 
185  std::string convert_complex(
186  const exprt &src,
187  unsigned precedence);
188 
189  std::string convert_comma(
190  const exprt &src,
191  unsigned precedence);
192 
193  std::string convert_Hoare(const exprt &src);
194 
195  std::string convert_code(const codet &src);
196  virtual std::string convert_code(const codet &src, unsigned indent);
197  std::string convert_code_label(const code_labelt &src, unsigned indent);
198  // NOLINTNEXTLINE(whitespace/line_length)
199  std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
200  std::string convert_code_asm(const code_asmt &src, unsigned indent);
201  std::string convert_code_assign(const code_assignt &src, unsigned indent);
202  // NOLINTNEXTLINE(whitespace/line_length)
203  std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
204  std::string convert_code_for(const code_fort &src, unsigned indent);
205  std::string convert_code_while(const code_whilet &src, unsigned indent);
206  std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent);
207  std::string convert_code_block(const code_blockt &src, unsigned indent);
208  std::string convert_code_expression(const codet &src, unsigned indent);
209  std::string convert_code_return(const codet &src, unsigned indent);
210  std::string convert_code_goto(const codet &src, unsigned indent);
211  std::string convert_code_assume(const codet &src, unsigned indent);
212  std::string convert_code_assert(const codet &src, unsigned indent);
213  std::string convert_code_break(unsigned indent);
214  std::string convert_code_switch(const codet &src, unsigned indent);
215  std::string convert_code_continue(unsigned indent);
216  std::string convert_code_decl(const codet &src, unsigned indent);
217  std::string convert_code_decl_block(const codet &src, unsigned indent);
218  std::string convert_code_dead(const codet &src, unsigned indent);
219  // NOLINTNEXTLINE(whitespace/line_length)
220  std::string convert_code_function_call(const code_function_callt &src, unsigned indent);
221  std::string convert_code_lock(const codet &src, unsigned indent);
222  std::string convert_code_unlock(const codet &src, unsigned indent);
223  std::string convert_code_printf(const codet &src, unsigned indent);
224  std::string convert_code_fence(const codet &src, unsigned indent);
225  std::string convert_code_input(const codet &src, unsigned indent);
226  std::string convert_code_output(const codet &src, unsigned indent);
227  std::string convert_code_array_set(const codet &src, unsigned indent);
228  std::string convert_code_array_copy(const codet &src, unsigned indent);
229  std::string convert_code_array_replace(const codet &src, unsigned indent);
230 
231  virtual std::string convert_with_precedence(
232  const exprt &src, unsigned &precedence);
233 
234  std::string
238  std::string convert_allocate(const exprt &src, unsigned &precedence);
239  std::string convert_nondet(const exprt &src, unsigned &precedence);
240  std::string convert_prob_coin(const exprt &src, unsigned &precedence);
241  std::string convert_prob_uniform(const exprt &src, unsigned &precedence);
242  // NOLINTNEXTLINE(whitespace/line_length)
243  std::string convert_statement_expression(const exprt &src, unsigned &precendence);
244 
245  virtual std::string convert_symbol(const exprt &src);
246  std::string convert_predicate_symbol(const exprt &src);
247  std::string convert_predicate_next_symbol(const exprt &src);
248  std::string convert_predicate_passive_symbol(const exprt &src);
250  std::string convert_quantified_symbol(const exprt &src);
251  std::string convert_nondet_bool();
252  std::string convert_object_descriptor(const exprt &src, unsigned &precedence);
253  std::string convert_literal(const exprt &src);
254  // NOLINTNEXTLINE(whitespace/line_length)
255  virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence);
256  virtual std::string convert_constant_bool(bool boolean_value);
257 
258  std::string convert_norep(const exprt &src, unsigned &precedence);
259 
260  virtual std::string convert_struct(const exprt &src, unsigned &precedence);
261  std::string convert_union(const exprt &src, unsigned &precedence);
262  std::string convert_vector(const exprt &src, unsigned &precedence);
263  std::string convert_array(const exprt &src);
264  std::string convert_array_list(const exprt &src, unsigned &precedence);
265  std::string convert_initializer_list(const exprt &src);
266  std::string convert_designated_initializer(const exprt &src);
267  std::string convert_concatenation(const exprt &src, unsigned &precedence);
268  std::string convert_sizeof(const exprt &src, unsigned &precedence);
269  std::string convert_let(const let_exprt &, unsigned precedence);
270 
271  std::string convert_struct(
272  const exprt &src,
273  unsigned &precedence,
274  bool include_padding_components);
275 };
276 
277 #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
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:1699
A codet representing an assignment in the program.
Definition: std_code.h:293
A codet representing sequential composition of program statements.
Definition: std_code.h:168
codet representation of a do while statement.
Definition: std_code.h:988
codet representation of a for statement.
Definition: std_code.h:1050
codet representation of a function call statement.
Definition: std_code.h:1213
codet representation of an if-then-else statement.
Definition: std_code.h:776
codet representation of a label for branch targets.
Definition: std_code.h:1405
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1469
codet representing a while statement.
Definition: std_code.h:926
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
A constant literal expression.
Definition: std_expr.h:2753
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
optionalt< std::string > convert_function(const exprt &src)
Returns a string if src is a function with a known conversion, else returns nullopt.
std::string convert_nondet(const exprt &src, unsigned &precedence)
std::string convert_literal(const exprt &src)
std::string convert_code_continue(unsigned indent)
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
virtual std::string convert_symbol(const exprt &src)
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
std::string convert_comma(const exprt &src, unsigned precedence)
std::string convert_code_assert(const codet &src, unsigned indent)
std::string convert_quantifier(const quantifier_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_union(const exprt &src, unsigned &precedence)
std::string convert_code_expression(const codet &src, unsigned indent)
std::string convert_code_goto(const codet &src, unsigned indent)
std::string convert_code_switch(const codet &src, unsigned indent)
std::string convert_initializer_list(const exprt &src)
std::string convert_quantified_symbol(const exprt &src)
std::string convert_function_application(const function_application_exprt &src)
std::string convert_code_unlock(const codet &src, unsigned indent)
std::string convert_code_decl_block(const codet &src, unsigned indent)
std::string convert_byte_update(const byte_update_exprt &, unsigned precedence)
std::string convert_code(const codet &src)
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
std::string convert_let(const let_exprt &, unsigned precedence)
std::string convert_nondet_bool()
std::string convert_struct(const exprt &src, unsigned &precedence, bool include_padding_components)
std::string convert_norep(const exprt &src, unsigned &precedence)
const expr2c_configurationt & configuration
Definition: expr2c_class.h:49
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
Definition: expr2c_class.h:81
std::string convert_code_output(const codet &src, unsigned indent)
std::string convert_code_while(const code_whilet &src, unsigned indent)
virtual std::string convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str)
std::string convert_index_designator(const exprt &src)
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
std::string convert_code_block(const code_blockt &src, unsigned indent)
std::string convert_code_asm(const code_asmt &src, unsigned indent)
std::string convert_allocate(const exprt &src, unsigned &precedence)
std::string convert_Hoare(const exprt &src)
std::string convert_sizeof(const exprt &src, unsigned &precedence)
std::string convert_code_lock(const codet &src, unsigned indent)
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
irep_idt id_shorthand(const irep_idt &identifier) const
Definition: expr2c.cpp:76
std::string convert_cond(const exprt &src, unsigned precedence)
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src)
std::string convert_overflow(const exprt &src, unsigned &precedence)
std::string convert_member(const member_exprt &src, unsigned precedence)
void get_shorthands(const exprt &expr)
Definition: expr2c.cpp:117
std::string convert_code_for(const code_fort &src, unsigned indent)
std::string convert_with_identifier(const typet &src, const std::string &identifier)
std::string convert_extractbits(const extractbits_exprt &src, unsigned precedence)
std::string convert_code_decl(const codet &src, unsigned indent)
std::string convert_trinary(const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
virtual std::string convert(const exprt &src)
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
std::string convert_update(const update_exprt &, unsigned precedence)
std::string convert_nondet_symbol(const nondet_symbol_exprt &)
std::string convert_code_printf(const codet &src, unsigned indent)
std::string convert_unary(const unary_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
std::string convert_member_designator(const exprt &src)
virtual std::string convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:219
static std::string indent_str(unsigned indent)
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
std::string convert_code_label(const code_labelt &src, unsigned indent)
std::string convert_code_array_copy(const codet &src, unsigned indent)
std::string convert_concatenation(const exprt &src, unsigned &precedence)
virtual std::string convert_constant_bool(bool boolean_value)
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
std::string convert_code_dead(const codet &src, unsigned indent)
const namespacet & ns
Definition: expr2c_class.h:48
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...
std::string convert_designated_initializer(const exprt &src)
std::string convert_vector(const exprt &src, unsigned &precedence)
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string convert_array_member_value(const exprt &src, unsigned precedence)
virtual ~expr2ct()
Definition: expr2c_class.h:37
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
std::unordered_map< irep_idt, irep_idt > shorthands
Definition: expr2c_class.h:82
std::string convert_complex(const exprt &src, unsigned precedence)
std::string convert_code_assign(const code_assignt &src, unsigned indent)
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
std::string convert_code_fence(const codet &src, unsigned indent)
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:214
std::string convert_code_return(const codet &src, unsigned indent)
std::string convert_code_break(unsigned indent)
std::string convert_with(const exprt &src, unsigned precedence)
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
std::string convert_predicate_passive_symbol(const exprt &src)
std::string convert_array_list(const exprt &src, unsigned &precedence)
unsigned sizeof_nesting
Definition: expr2c_class.h:84
std::string convert_array_of(const exprt &src, unsigned precedence)
std::string convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible)
std::string convert_code_array_replace(const codet &src, unsigned indent)
std::string convert_index(const exprt &src, unsigned precedence)
std::string convert_code_assume(const codet &src, unsigned indent)
std::string convert_code_input(const codet &src, unsigned indent)
std::string convert_extractbit(const extractbit_exprt &, unsigned precedence)
virtual std::string convert_code(const codet &src, unsigned indent)
std::string convert_predicate_next_symbol(const exprt &src)
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
std::string convert_code_array_set(const codet &src, unsigned indent)
std::string convert_function(const exprt &src, const std::string &symbol)
std::string convert_binary(const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string convert_predicate_symbol(const exprt &src)
expr2ct(const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration)
Definition: expr2c_class.h:30
std::string convert_struct_type(const typet &src, const std::string &qualifer_str, const std::string &declarator_str, bool inc_struct_body, bool inc_padding_components)
std::string convert_array(const exprt &src)
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
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:2919
Extract member of struct or union.
Definition: std_expr.h:2613
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:2138
An expression with three operands.
Definition: std_expr.h:53
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
Generic base class for unary expressions.
Definition: std_expr.h:281
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
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