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 "expr.h"
17 #include "expr_iterator.h"
18 #include "fixedbv.h"
19 #include "format_type.h"
20 #include "ieee_float.h"
21 #include "invariant.h"
22 #include "mathematical_expr.h"
23 #include "mp_arith.h"
24 #include "rational.h"
25 #include "rational_tools.h"
26 #include "std_code.h"
27 #include "std_expr.h"
28 #include "string2int.h"
29 #include "string_utils.h"
30 
31 #include <map>
32 #include <ostream>
33 #include <stack>
34 
35 // expressions that are rendered with infix operators
36 struct infix_opt
37 {
38  const char *rep;
39 };
40 
41 const std::map<irep_idt, infix_opt> infix_map = {
42  {ID_plus, {"+"}},
43  {ID_minus, {"-"}},
44  {ID_mult, {"*"}},
45  {ID_div, {"/"}},
46  {ID_equal, {"="}},
47  {ID_notequal, {u8"\u2260"}}, // /=, U+2260
48  {ID_and, {u8"\u2227"}}, // wedge, U+2227
49  {ID_or, {u8"\u2228"}}, // vee, U+2228
50  {ID_xor, {u8"\u2295"}}, // + in circle, U+2295
51  {ID_implies, {u8"\u21d2"}}, // =>, U+21D2
52  {ID_le, {u8"\u2264"}}, // <=, U+2264
53  {ID_ge, {u8"\u2265"}}, // >=, U+2265
54  {ID_lt, {"<"}},
55  {ID_gt, {">"}},
56 };
57 
61 static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
62 {
63  // no need for parentheses whenever the subexpression
64  // doesn't have operands
65  if(!sub_expr.has_operands())
66  return false;
67 
68  // no need if subexpression isn't an infix operator
69  if(infix_map.find(sub_expr.id()) == infix_map.end())
70  return false;
71 
72  // * and / bind stronger than + and -
73  if(
74  (sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
75  (expr.id() == ID_plus || expr.id() == ID_minus))
76  return false;
77 
78  // ==, !=, <, <=, >, >= bind stronger than && and ||
79  if(
80  (sub_expr.id() == ID_equal || sub_expr.id() == ID_notequal ||
81  sub_expr.id() == ID_lt || sub_expr.id() == ID_gt ||
82  sub_expr.id() == ID_le || sub_expr.id() == ID_ge) &&
83  (expr.id() == ID_and || expr.id() == ID_or))
84  return false;
85 
86  // +, -, *, / bind stronger than ==, !=, <, <=, >, >=
87  if(
88  (sub_expr.id() == ID_plus || sub_expr.id() == ID_minus ||
89  sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
90  (expr.id() == ID_equal || expr.id() == ID_notequal || expr.id() == ID_lt ||
91  expr.id() == ID_gt || expr.id() == ID_le || expr.id() == ID_ge))
92  {
93  return false;
94  }
95 
96  return true;
97 }
98 
101 static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
102 {
103  bool first = true;
104 
105  std::string operator_str = id2string(src.id()); // default
106 
107  if(src.id() == ID_equal && to_equal_expr(src).op0().type().id() == ID_bool)
108  {
109  operator_str = u8"\u21d4"; // <=>, U+21D4
110  }
111  else
112  {
113  auto infix_map_it = infix_map.find(src.id());
114  if(infix_map_it != infix_map.end())
115  operator_str = infix_map_it->second.rep;
116  }
117 
118  for(const auto &op : src.operands())
119  {
120  if(first)
121  first = false;
122  else
123  os << ' ' << operator_str << ' ';
124 
125  const bool need_parentheses = bracket_subexpression(op, src);
126 
127  if(need_parentheses)
128  os << '(';
129 
130  os << format(op);
131 
132  if(need_parentheses)
133  os << ')';
134  }
135 
136  return os;
137 }
138 
141 static std::ostream &format_rec(std::ostream &os, const binary_exprt &src)
142 {
143  return format_rec(os, to_multi_ary_expr(src));
144 }
145 
148 static std::ostream &format_rec(std::ostream &os, const unary_exprt &src)
149 {
150  if(src.id() == ID_not)
151  os << u8"\u00ac"; // neg, U+00AC
152  else if(src.id() == ID_unary_minus)
153  os << '-';
154  else if(src.id() == ID_count_leading_zeros)
155  os << "clz";
156  else
157  return os << src.pretty();
158 
159  if(src.op().has_operands())
160  return os << '(' << format(src.op()) << ')';
161  else
162  return os << format(src.op());
163 }
164 
166 static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
167 {
168  auto type = src.type().id();
169 
170  if(type == ID_bool)
171  {
172  if(src.is_true())
173  return os << "true";
174  else if(src.is_false())
175  return os << "false";
176  else
177  return os << src.pretty();
178  }
179  else if(type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool)
180  return os << *numeric_cast<mp_integer>(src);
181  else if(type == ID_integer)
182  return os << src.get_value();
183  else if(type == ID_string)
184  return os << '"' << escape(id2string(src.get_value())) << '"';
185  else if(type == ID_floatbv)
186  return os << ieee_floatt(src);
187  else if(type == ID_pointer && src.is_zero())
188  return os << src.get_value();
189  else
190  return os << src.pretty();
191 }
192 
193 std::ostream &fallback_format_rec(std::ostream &os, const exprt &expr)
194 {
195  os << expr.id();
196 
197  for(const auto &s : expr.get_named_sub())
198  if(s.first != ID_type)
199  os << ' ' << s.first << "=\"" << s.second.id() << '"';
200 
201  if(expr.has_operands())
202  {
203  os << '(';
204  bool first = true;
205 
206  for(const auto &op : expr.operands())
207  {
208  if(first)
209  first = false;
210  else
211  os << ", ";
212 
213  os << format(op);
214  }
215 
216  os << ')';
217  }
218 
219  return os;
220 }
221 
223 {
224 public:
226  {
227  setup();
228  }
229 
230  using formattert =
231  std::function<std::ostream &(std::ostream &, const exprt &)>;
232  using expr_mapt = std::unordered_map<irep_idt, formattert>;
233 
235 
237  const formattert &find_formatter(const exprt &);
238 
239 private:
241  void setup();
242 
244 };
245 
246 // The below generates textual output in a generic syntax
247 // that is inspired by C/C++/Java, and is meant for debugging
248 // purposes.
250 {
251  auto multi_ary_expr =
252  [](std::ostream &os, const exprt &expr) -> std::ostream & {
253  return format_rec(os, to_multi_ary_expr(expr));
254  };
255 
256  expr_map[ID_plus] = multi_ary_expr;
257  expr_map[ID_mult] = multi_ary_expr;
258  expr_map[ID_and] = multi_ary_expr;
259  expr_map[ID_or] = multi_ary_expr;
260  expr_map[ID_xor] = multi_ary_expr;
261 
262  auto binary_expr = [](std::ostream &os, const exprt &expr) -> std::ostream & {
263  return format_rec(os, to_binary_expr(expr));
264  };
265 
266  expr_map[ID_lt] = binary_expr;
267  expr_map[ID_gt] = binary_expr;
268  expr_map[ID_ge] = binary_expr;
269  expr_map[ID_le] = binary_expr;
270  expr_map[ID_div] = binary_expr;
271  expr_map[ID_minus] = binary_expr;
272  expr_map[ID_implies] = binary_expr;
273  expr_map[ID_equal] = binary_expr;
274  expr_map[ID_notequal] = binary_expr;
275 
276  auto unary_expr = [](std::ostream &os, const exprt &expr) -> std::ostream & {
277  return format_rec(os, to_unary_expr(expr));
278  };
279 
280  expr_map[ID_not] = unary_expr;
281  expr_map[ID_unary_minus] = unary_expr;
282 
283  expr_map[ID_constant] =
284  [](std::ostream &os, const exprt &expr) -> std::ostream & {
285  return format_rec(os, to_constant_expr(expr));
286  };
287 
288  expr_map[ID_typecast] =
289  [](std::ostream &os, const exprt &expr) -> std::ostream & {
290  return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
291  << format(expr.type()) << ')';
292  };
293 
294  auto byte_extract =
295  [](std::ostream &os, const exprt &expr) -> std::ostream & {
296  const auto &byte_extract_expr = to_byte_extract_expr(expr);
297  return os << expr.id() << '(' << format(byte_extract_expr.op()) << ", "
298  << format(byte_extract_expr.offset()) << ", "
299  << format(byte_extract_expr.type()) << ')';
300  };
301 
302  expr_map[ID_byte_extract_little_endian] = byte_extract;
303  expr_map[ID_byte_extract_big_endian] = byte_extract;
304 
305  auto byte_update = [](std::ostream &os, const exprt &expr) -> std::ostream & {
306  const auto &byte_update_expr = to_byte_update_expr(expr);
307  return os << expr.id() << '(' << format(byte_update_expr.op()) << ", "
308  << format(byte_update_expr.offset()) << ", "
309  << format(byte_update_expr.value()) << ", "
310  << format(byte_update_expr.type()) << ')';
311  };
312 
313  expr_map[ID_byte_update_little_endian] = byte_update;
314  expr_map[ID_byte_update_big_endian] = byte_update;
315 
316  expr_map[ID_member] =
317  [](std::ostream &os, const exprt &expr) -> std::ostream & {
318  return os << format(to_member_expr(expr).op()) << '.'
320  };
321 
322  expr_map[ID_symbol] =
323  [](std::ostream &os, const exprt &expr) -> std::ostream & {
324  return os << to_symbol_expr(expr).get_identifier();
325  };
326 
327  expr_map[ID_index] =
328  [](std::ostream &os, const exprt &expr) -> std::ostream & {
329  const auto &index_expr = to_index_expr(expr);
330  return os << format(index_expr.array()) << '[' << format(index_expr.index())
331  << ']';
332  };
333 
334  expr_map[ID_type] =
335  [](std::ostream &os, const exprt &expr) -> std::ostream & {
336  return format_rec(os, expr.type());
337  };
338 
339  expr_map[ID_forall] =
340  [](std::ostream &os, const exprt &expr) -> std::ostream & {
341  return os << u8"\u2200 " << format(to_quantifier_expr(expr).symbol())
342  << " : " << format(to_quantifier_expr(expr).symbol().type())
343  << " . " << format(to_quantifier_expr(expr).where());
344  };
345 
346  expr_map[ID_exists] =
347  [](std::ostream &os, const exprt &expr) -> std::ostream & {
348  return os << u8"\u2203 " << format(to_quantifier_expr(expr).symbol())
349  << " : " << format(to_quantifier_expr(expr).symbol().type())
350  << " . " << format(to_quantifier_expr(expr).where());
351  };
352 
353  expr_map[ID_let] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
354  return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
355  << format(to_let_expr(expr).value()) << " IN "
356  << format(to_let_expr(expr).where());
357  };
358 
359  expr_map[ID_lambda] =
360  [](std::ostream &os, const exprt &expr) -> std::ostream & {
361  const auto &lambda_expr = to_lambda_expr(expr);
362 
363  os << u8"\u03bb ";
364 
365  bool first = true;
366 
367  for(auto &v : lambda_expr.variables())
368  {
369  if(first)
370  first = false;
371  else
372  os << ", ";
373 
374  os << format(v);
375  }
376 
377  return os << " . " << format(lambda_expr.where());
378  };
379 
380  auto compound = [](std::ostream &os, const exprt &expr) -> std::ostream & {
381  os << "{ ";
382 
383  bool first = true;
384 
385  for(const auto &op : expr.operands())
386  {
387  if(first)
388  first = false;
389  else
390  os << ", ";
391 
392  os << format(op);
393  }
394 
395  return os << " }";
396  };
397 
398  expr_map[ID_array] = compound;
399  expr_map[ID_struct] = compound;
400 
401  expr_map[ID_if] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
402  const auto &if_expr = to_if_expr(expr);
403  return os << '(' << format(if_expr.cond()) << " ? "
404  << format(if_expr.true_case()) << " : "
405  << format(if_expr.false_case()) << ')';
406  };
407 
408  expr_map[ID_code] =
409  [](std::ostream &os, const exprt &expr) -> std::ostream & {
410  const auto &code = to_code(expr);
411  const irep_idt &statement = code.get_statement();
412 
413  if(statement == ID_assign)
414  return os << format(to_code_assign(code).lhs()) << " = "
415  << format(to_code_assign(code).rhs()) << ';';
416  else if(statement == ID_block)
417  {
418  os << '{';
419  for(const auto &s : to_code_block(code).statements())
420  os << ' ' << format(s);
421  return os << " }";
422  }
423  else if(statement == ID_dead)
424  {
425  return os << "dead " << format(to_code_dead(code).symbol()) << ";";
426  }
427  else if(const auto decl = expr_try_dynamic_cast<code_declt>(code))
428  {
429  const auto &declaration_symb = decl->symbol();
430  os << "decl " << format(declaration_symb.type()) << " "
431  << format(declaration_symb);
432  if(const optionalt<exprt> initial_value = decl->initial_value())
433  os << " = " << format(*initial_value);
434  return os << ";";
435  }
436  else if(statement == ID_function_call)
437  {
438  const auto &func_call = to_code_function_call(code);
439  os << to_symbol_expr(func_call.function()).get_identifier() << "(";
440 
441  // Join all our arguments together.
442  join_strings(
443  os,
444  func_call.arguments().begin(),
445  func_call.arguments().end(),
446  ", ",
447  [](const exprt &expr) { return format(expr); });
448 
449  return os << ");";
450  }
451  else
452  return fallback_format_rec(os, expr);
453  };
454 
455  fallback = [](std::ostream &os, const exprt &expr) -> std::ostream & {
456  return fallback_format_rec(os, expr);
457  };
458 }
459 
462 {
463  auto m_it = expr_map.find(expr.id());
464  if(m_it == expr_map.end())
465  return fallback;
466  else
467  return m_it->second;
468 }
469 
471 
472 std::ostream &format_rec(std::ostream &os, const exprt &expr)
473 {
474  auto &formatter = format_expr_config.find_formatter(expr);
475  return formatter(os, expr);
476 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ieee_floatt
Definition: ieee_float.h:120
format
static format_containert< T > format(const T &o)
Definition: format.h:37
format_expr_configt::fallback
formattert fallback
Definition: format_expr.cpp:243
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:740
to_lambda_expr
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
Definition: mathematical_expr.h:423
infix_map
const std::map< irep_idt, infix_opt > infix_map
Definition: format_expr.cpp:41
arith_tools.h
mp_arith.h
rational.h
rational_tools.h
string_utils.h
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:501
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
u8
uint64_t u8
Definition: bytecode_info.h:58
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
infix_opt::rep
const char * rep
Definition: format_expr.cpp:38
format_rec
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:101
fixedbv.h
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:60
format_expr_configt::expr_map
expr_mapt expr_map
Definition: format_expr.cpp:234
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:69
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
expr.h
format_expr_configt
Definition: format_expr.cpp:223
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
byte_operators.h
Expression classes for byte-level operators.
infix_opt
Definition: format_expr.cpp:37
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:469
fallback_format_rec
std::ostream & fallback_format_rec(std::ostream &os, const exprt &expr)
Definition: format_expr.cpp:193
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:120
join_strings
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:62
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:551
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2928
format_expr_config
format_expr_configt format_expr_config
Definition: format_expr.cpp:470
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
format_expr_configt::find_formatter
const formattert & find_formatter(const exprt &)
find the formatter for a given expression
Definition: format_expr.cpp:461
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:91
bracket_subexpression
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:61
format_expr.h
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
to_quantifier_expr
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: mathematical_expr.h:316
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
ieee_float.h
invariant.h
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1179
to_code_block
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:256
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2541
exprt::operands
operandst & operands()
Definition: expr.h:96
format_expr_configt::format_expr_configt
format_expr_configt()
Definition: format_expr.cpp:225
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
format_expr_configt::setup
void setup()
setup the expressions we can format
Definition: format_expr.cpp:249
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:815
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2675
format_type.h
format_expr_configt::expr_mapt
std::unordered_map< irep_idt, formattert > expr_mapt
Definition: format_expr.cpp:232
format_expr_configt::formattert
std::function< std::ostream &(std::ostream &, const exprt &)> formattert
Definition: format_expr.cpp:231
escape
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
Definition: string_utils.cpp:138
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700