cprover
Loading...
Searching...
No Matches
format_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Expression Pretty Printing
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "format_expr.h"
13
14#include "arith_tools.h"
15#include "byte_operators.h"
16#include "format_type.h"
17#include "ieee_float.h"
18#include "mathematical_expr.h"
19#include "mp_arith.h"
20#include "pointer_expr.h"
21#include "prefix.h"
22#include "string_utils.h"
23
24#include <map>
25#include <ostream>
26
27// expressions that are rendered with infix operators
29{
30 const char *rep;
31};
32
33const std::map<irep_idt, infix_opt> infix_map = {
34 {ID_plus, {"+"}},
35 {ID_minus, {"-"}},
36 {ID_mult, {"*"}},
37 {ID_div, {"/"}},
38 {ID_equal, {"="}},
39 {ID_notequal, {u8"\u2260"}}, // /=, U+2260
40 {ID_and, {u8"\u2227"}}, // wedge, U+2227
41 {ID_or, {u8"\u2228"}}, // vee, U+2228
42 {ID_xor, {u8"\u2295"}}, // + in circle, U+2295
43 {ID_implies, {u8"\u21d2"}}, // =>, U+21D2
44 {ID_le, {u8"\u2264"}}, // <=, U+2264
45 {ID_ge, {u8"\u2265"}}, // >=, U+2265
46 {ID_lt, {"<"}},
47 {ID_gt, {">"}},
48};
49
53static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
54{
55 // no need for parentheses whenever the subexpression
56 // doesn't have operands
57 if(!sub_expr.has_operands())
58 return false;
59
60 // no need if subexpression isn't an infix operator
61 if(infix_map.find(sub_expr.id()) == infix_map.end())
62 return false;
63
64 // * and / bind stronger than + and -
65 if(
66 (sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
67 (expr.id() == ID_plus || expr.id() == ID_minus))
68 return false;
69
70 // ==, !=, <, <=, >, >= bind stronger than && and ||
71 if(
72 (sub_expr.id() == ID_equal || sub_expr.id() == ID_notequal ||
73 sub_expr.id() == ID_lt || sub_expr.id() == ID_gt ||
74 sub_expr.id() == ID_le || sub_expr.id() == ID_ge) &&
75 (expr.id() == ID_and || expr.id() == ID_or))
76 return false;
77
78 // +, -, *, / bind stronger than ==, !=, <, <=, >, >=
79 if(
80 (sub_expr.id() == ID_plus || sub_expr.id() == ID_minus ||
81 sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
82 (expr.id() == ID_equal || expr.id() == ID_notequal || expr.id() == ID_lt ||
83 expr.id() == ID_gt || expr.id() == ID_le || expr.id() == ID_ge))
84 {
85 return false;
86 }
87
88 return true;
89}
90
93static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
94{
95 bool first = true;
96
97 std::string operator_str = id2string(src.id()); // default
98
99 if(src.id() == ID_equal && to_equal_expr(src).op0().type().id() == ID_bool)
100 {
101 operator_str = u8"\u21d4"; // <=>, U+21D4
102 }
103 else
104 {
105 auto infix_map_it = infix_map.find(src.id());
106 if(infix_map_it != infix_map.end())
107 operator_str = infix_map_it->second.rep;
108 }
109
110 for(const auto &op : src.operands())
111 {
112 if(first)
113 first = false;
114 else
115 os << ' ' << operator_str << ' ';
116
117 const bool need_parentheses = bracket_subexpression(op, src);
118
119 if(need_parentheses)
120 os << '(';
121
122 os << format(op);
123
124 if(need_parentheses)
125 os << ')';
126 }
127
128 return os;
129}
130
133static std::ostream &format_rec(std::ostream &os, const binary_exprt &src)
134{
135 return format_rec(os, to_multi_ary_expr(src));
136}
137
140static std::ostream &format_rec(std::ostream &os, const unary_exprt &src)
141{
142 if(src.id() == ID_not)
143 os << u8"\u00ac"; // neg, U+00AC
144 else if(src.id() == ID_unary_minus)
145 os << '-';
146 else if(src.id() == ID_count_leading_zeros)
147 os << "clz";
148 else if(src.id() == ID_count_trailing_zeros)
149 os << "ctz";
150 else
151 return os << src.pretty();
152
153 if(src.op().has_operands())
154 return os << '(' << format(src.op()) << ')';
155 else
156 return os << format(src.op());
157}
158
160static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
161{
162 auto type = src.type().id();
163
164 if(type == ID_bool)
165 {
166 if(src.is_true())
167 return os << "true";
168 else if(src.is_false())
169 return os << "false";
170 else
171 return os << src.pretty();
172 }
173 else if(
174 type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool ||
175 type == ID_c_bit_field)
176 return os << *numeric_cast<mp_integer>(src);
177 else if(type == ID_integer)
178 return os << src.get_value();
179 else if(type == ID_string)
180 return os << '"' << escape(id2string(src.get_value())) << '"';
181 else if(type == ID_floatbv)
182 return os << ieee_floatt(src);
183 else if(type == ID_pointer)
184 {
185 if(src.is_zero())
186 return os << ID_NULL;
187 else if(has_prefix(id2string(src.get_value()), "INVALID-"))
188 {
189 return os << "INVALID-POINTER";
190 }
191 else if(src.operands().size() == 1)
192 {
193 const auto &unary_expr = to_unary_expr(src);
194 const auto &pointer_type = to_pointer_type(src.type());
195 return os << "pointer(" << format(unary_expr.op()) << ", "
196 << format(pointer_type.base_type()) << ')';
197 }
198 else
199 {
200 const auto &pointer_type = to_pointer_type(src.type());
201 const auto width = pointer_type.get_width();
202 auto int_value = bvrep2integer(src.get_value(), width, false);
203 return os << "pointer(0x" << integer2string(int_value, 16) << ", "
204 << format(pointer_type.base_type()) << ')';
205 }
206 }
207 else
208 return os << src.pretty();
209}
210
211std::ostream &fallback_format_rec(std::ostream &os, const exprt &expr)
212{
213 os << expr.id();
214
215 for(const auto &s : expr.get_named_sub())
216 if(s.first != ID_type)
217 os << ' ' << s.first << "=\"" << s.second.id() << '"';
218
219 if(expr.has_operands())
220 {
221 os << '(';
222 bool first = true;
223
224 for(const auto &op : expr.operands())
225 {
226 if(first)
227 first = false;
228 else
229 os << ", ";
230
231 os << format(op);
232 }
233
234 os << ')';
235 }
236
237 return os;
238}
239
241{
242public:
244 {
245 setup();
246 }
247
249 std::function<std::ostream &(std::ostream &, const exprt &)>;
250 using expr_mapt = std::unordered_map<irep_idt, formattert>;
251
253
255 const formattert &find_formatter(const exprt &);
256
257private:
259 void setup();
260
262};
263
264// The below generates textual output in a generic syntax
265// that is inspired by C/C++/Java, and is meant for debugging
266// purposes.
268{
269 auto multi_ary_expr =
270 [](std::ostream &os, const exprt &expr) -> std::ostream & {
271 return format_rec(os, to_multi_ary_expr(expr));
272 };
273
274 expr_map[ID_plus] = multi_ary_expr;
275 expr_map[ID_mult] = multi_ary_expr;
276 expr_map[ID_and] = multi_ary_expr;
277 expr_map[ID_or] = multi_ary_expr;
278 expr_map[ID_xor] = multi_ary_expr;
279
280 auto binary_expr = [](std::ostream &os, const exprt &expr) -> std::ostream & {
281 return format_rec(os, to_binary_expr(expr));
282 };
283
284 expr_map[ID_lt] = binary_expr;
285 expr_map[ID_gt] = binary_expr;
286 expr_map[ID_ge] = binary_expr;
287 expr_map[ID_le] = binary_expr;
288 expr_map[ID_div] = binary_expr;
289 expr_map[ID_minus] = binary_expr;
290 expr_map[ID_implies] = binary_expr;
291 expr_map[ID_equal] = binary_expr;
292 expr_map[ID_notequal] = binary_expr;
293
294 auto unary_expr = [](std::ostream &os, const exprt &expr) -> std::ostream & {
295 return format_rec(os, to_unary_expr(expr));
296 };
297
298 expr_map[ID_not] = unary_expr;
299 expr_map[ID_unary_minus] = unary_expr;
300
301 expr_map[ID_constant] =
302 [](std::ostream &os, const exprt &expr) -> std::ostream & {
303 return format_rec(os, to_constant_expr(expr));
304 };
305
306 expr_map[ID_typecast] =
307 [](std::ostream &os, const exprt &expr) -> std::ostream & {
308 return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
309 << format(expr.type()) << ')';
310 };
311
312 auto byte_extract =
313 [](std::ostream &os, const exprt &expr) -> std::ostream & {
314 const auto &byte_extract_expr = to_byte_extract_expr(expr);
315 return os << expr.id() << '(' << format(byte_extract_expr.op()) << ", "
316 << format(byte_extract_expr.offset()) << ", "
317 << format(byte_extract_expr.type()) << ')';
318 };
319
320 expr_map[ID_byte_extract_little_endian] = byte_extract;
321 expr_map[ID_byte_extract_big_endian] = byte_extract;
322
323 auto byte_update = [](std::ostream &os, const exprt &expr) -> std::ostream & {
324 const auto &byte_update_expr = to_byte_update_expr(expr);
325 return os << expr.id() << '(' << format(byte_update_expr.op()) << ", "
326 << format(byte_update_expr.offset()) << ", "
327 << format(byte_update_expr.value()) << ", "
328 << format(byte_update_expr.type()) << ')';
329 };
330
331 expr_map[ID_byte_update_little_endian] = byte_update;
332 expr_map[ID_byte_update_big_endian] = byte_update;
333
334 expr_map[ID_member] =
335 [](std::ostream &os, const exprt &expr) -> std::ostream & {
336 return os << format(to_member_expr(expr).op()) << '.'
338 };
339
340 expr_map[ID_symbol] =
341 [](std::ostream &os, const exprt &expr) -> std::ostream & {
342 return os << to_symbol_expr(expr).get_identifier();
343 };
344
345 expr_map[ID_index] =
346 [](std::ostream &os, const exprt &expr) -> std::ostream & {
347 const auto &index_expr = to_index_expr(expr);
348 return os << format(index_expr.array()) << '[' << format(index_expr.index())
349 << ']';
350 };
351
352 expr_map[ID_type] =
353 [](std::ostream &os, const exprt &expr) -> std::ostream & {
354 return format_rec(os, expr.type());
355 };
356
357 expr_map[ID_forall] =
358 [](std::ostream &os, const exprt &expr) -> std::ostream & {
359 os << u8"\u2200 ";
360 bool first = true;
361 for(const auto &symbol : to_quantifier_expr(expr).variables())
362 {
363 if(first)
364 first = false;
365 else
366 os << ", ";
367 os << format(symbol) << " : " << format(symbol.type());
368 }
369 return os << " . " << format(to_quantifier_expr(expr).where());
370 };
371
372 expr_map[ID_exists] =
373 [](std::ostream &os, const exprt &expr) -> std::ostream & {
374 os << u8"\u2203 ";
375 bool first = true;
376 for(const auto &symbol : to_quantifier_expr(expr).variables())
377 {
378 if(first)
379 first = false;
380 else
381 os << ", ";
382 os << format(symbol) << " : " << format(symbol.type());
383 }
384 return os << " . " << format(to_quantifier_expr(expr).where());
385 };
386
387 expr_map[ID_let] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
388 const auto &let_expr = to_let_expr(expr);
389
390 os << "LET ";
391
392 bool first = true;
393
394 const auto &values = let_expr.values();
395 auto values_it = values.begin();
396 for(auto &v : let_expr.variables())
397 {
398 if(first)
399 first = false;
400 else
401 os << ", ";
402
403 os << format(v) << " = " << format(*values_it);
404 ++values_it;
405 }
406
407 return os << " IN " << format(let_expr.where());
408 };
409
410 expr_map[ID_lambda] =
411 [](std::ostream &os, const exprt &expr) -> std::ostream & {
412 const auto &lambda_expr = to_lambda_expr(expr);
413
414 os << u8"\u03bb ";
415
416 bool first = true;
417
418 for(auto &v : lambda_expr.variables())
419 {
420 if(first)
421 first = false;
422 else
423 os << ", ";
424
425 os << format(v);
426 }
427
428 return os << " . " << format(lambda_expr.where());
429 };
430
431 auto compound = [](std::ostream &os, const exprt &expr) -> std::ostream & {
432 os << "{ ";
433
434 bool first = true;
435
436 for(const auto &op : expr.operands())
437 {
438 if(first)
439 first = false;
440 else
441 os << ", ";
442
443 os << format(op);
444 }
445
446 return os << " }";
447 };
448
449 expr_map[ID_array] = compound;
450 expr_map[ID_struct] = compound;
451
452 expr_map[ID_if] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
453 const auto &if_expr = to_if_expr(expr);
454 return os << '(' << format(if_expr.cond()) << " ? "
455 << format(if_expr.true_case()) << " : "
456 << format(if_expr.false_case()) << ')';
457 };
458
459 expr_map[ID_string_constant] =
460 [](std::ostream &os, const exprt &expr) -> std::ostream & {
461 return os << '"' << expr.get_string(ID_value) << '"';
462 };
463
464 expr_map[ID_function_application] =
465 [](std::ostream &os, const exprt &expr) -> std::ostream & {
466 const auto &function_application_expr = to_function_application_expr(expr);
467 os << format(function_application_expr.function()) << '(';
468 bool first = true;
469 for(auto &argument : function_application_expr.arguments())
470 {
471 if(first)
472 first = false;
473 else
474 os << ", ";
475 os << format(argument);
476 }
477 os << ')';
478 return os;
479 };
480
481 expr_map[ID_dereference] =
482 [](std::ostream &os, const exprt &expr) -> std::ostream & {
483 const auto &dereference_expr = to_dereference_expr(expr);
484 os << '*';
485 if(dereference_expr.pointer().id() != ID_symbol)
486 os << '(' << format(dereference_expr.pointer()) << ')';
487 else
488 os << format(dereference_expr.pointer());
489 return os;
490 };
491
492 fallback = [](std::ostream &os, const exprt &expr) -> std::ostream & {
493 return fallback_format_rec(os, expr);
494 };
495}
496
499{
500 auto m_it = expr_map.find(expr.id());
501 if(m_it == expr_map.end())
502 return fallback;
503 else
504 return m_it->second;
505}
506
508
509std::ostream &format_rec(std::ostream &os, const exprt &expr)
510{
511 auto &formatter = format_expr_config.find_formatter(expr);
512 return formatter(os, expr);
513}
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
uint64_t u8
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:253
A base class for binary expressions.
Definition std_expr.h:550
variablest & variables()
Definition std_expr.h:2921
std::size_t get_width() const
Definition std_types.h:864
A constant literal expression.
Definition std_expr.h:2807
const irep_idt & get_value() const
Definition std_expr.h:2815
Base class for all expressions.
Definition expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:89
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:64
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
std::function< std::ostream &(std::ostream &, const exprt &)> formattert
void setup()
setup the expressions we can format
std::unordered_map< irep_idt, formattert > expr_mapt
const formattert & find_formatter(const exprt &)
find the formatter for a given expression
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:495
const irep_idt & id() const
Definition irep.h:396
named_subt & get_named_sub()
Definition irep.h:458
irep_idt get_component_name() const
Definition std_expr.h:2681
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:824
const typet & base_type() const
The type of the data what we point to.
const irep_idt & get_identifier() const
Definition std_expr.h:109
Generic base class for unary expressions.
Definition std_expr.h:281
const exprt & op() const
Definition std_expr.h:293
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
static format_containert< T > format(const T &o)
Definition format.h:37
static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
We use the precendences that most readers expect (i.e., the ones you learn in primary school),...
format_expr_configt format_expr_config
const std::map< irep_idt, infix_opt > infix_map
std::ostream & fallback_format_rec(std::ostream &os, const exprt &expr)
static std::ostream & format_rec(std::ostream &os, const multi_ary_exprt &src)
This formats a multi-ary expression, adding parentheses where indicated by bracket_subexpression.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:899
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition std_expr.h:3097
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1265
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
const char * rep