cprover
format_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Expression Pretty Printing
4 
5 Author: 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
28 struct infix_opt
29 {
30  const char *rep;
31 };
32 
33 const 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 
53 static 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 
93 static 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 
133 static std::ostream &format_rec(std::ostream &os, const binary_exprt &src)
134 {
135  return format_rec(os, to_multi_ary_expr(src));
136 }
137 
140 static 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 
160 static 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 
211 std::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 {
242 public:
244  {
245  setup();
246  }
247 
248  using formattert =
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 
257 private:
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 
509 std::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
Definition: bytecode_info.h:58
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
named_subt & get_named_sub()
Definition: irep.h:458
const irep_idt & id() const
Definition: irep.h:396
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.
Definition: pointer_expr.h:35
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),...
Definition: format_expr.cpp:53
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.
Definition: format_expr.cpp:93
format_expr_configt format_expr_config
const std::map< irep_idt, infix_opt > infix_map
Definition: format_expr.cpp:33
std::ostream & fallback_format_rec(std::ostream &os, const exprt &expr)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:3097
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 typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
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 binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1265
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
const char * rep
Definition: format_expr.cpp:30