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
155  return os << src.pretty();
156 
157  if(src.op().has_operands())
158  return os << '(' << format(src.op()) << ')';
159  else
160  return os << format(src.op());
161 }
162 
164 static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
165 {
166  auto type = src.type().id();
167 
168  if(type == ID_bool)
169  {
170  if(src.is_true())
171  return os << "true";
172  else if(src.is_false())
173  return os << "false";
174  else
175  return os << src.pretty();
176  }
177  else if(type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool)
178  return os << *numeric_cast<mp_integer>(src);
179  else if(type == ID_integer)
180  return os << src.get_value();
181  else if(type == ID_string)
182  return os << '"' << escape(id2string(src.get_value())) << '"';
183  else if(type == ID_floatbv)
184  return os << ieee_floatt(src);
185  else if(type == ID_pointer && src.is_zero())
186  return os << src.get_value();
187  else
188  return os << src.pretty();
189 }
190 
191 std::ostream &fallback_format_rec(std::ostream &os, const exprt &expr)
192 {
193  os << expr.id();
194 
195  for(const auto &s : expr.get_named_sub())
196  if(s.first != ID_type)
197  os << ' ' << s.first << "=\"" << s.second.id() << '"';
198 
199  if(expr.has_operands())
200  {
201  os << '(';
202  bool first = true;
203 
204  for(const auto &op : expr.operands())
205  {
206  if(first)
207  first = false;
208  else
209  os << ", ";
210 
211  os << format(op);
212  }
213 
214  os << ')';
215  }
216 
217  return os;
218 }
219 
221 {
222 public:
224  {
225  setup();
226  }
227 
228  using formattert =
229  std::function<std::ostream &(std::ostream &, const exprt &)>;
230  using expr_mapt = std::unordered_map<irep_idt, formattert>;
231 
233 
235  const formattert &find_formatter(const exprt &);
236 
237 private:
239  void setup();
240 
242 };
243 
244 // The below generates textual output in a generic syntax
245 // that is inspired by C/C++/Java, and is meant for debugging
246 // purposes.
248 {
249  auto multi_ary_expr =
250  [](std::ostream &os, const exprt &expr) -> std::ostream & {
251  return format_rec(os, to_multi_ary_expr(expr));
252  };
253 
254  expr_map[ID_plus] = multi_ary_expr;
255  expr_map[ID_mult] = multi_ary_expr;
256  expr_map[ID_and] = multi_ary_expr;
257  expr_map[ID_or] = multi_ary_expr;
258  expr_map[ID_xor] = multi_ary_expr;
259 
260  auto binary_expr = [](std::ostream &os, const exprt &expr) -> std::ostream & {
261  return format_rec(os, to_binary_expr(expr));
262  };
263 
264  expr_map[ID_lt] = binary_expr;
265  expr_map[ID_gt] = binary_expr;
266  expr_map[ID_ge] = binary_expr;
267  expr_map[ID_le] = binary_expr;
268  expr_map[ID_div] = binary_expr;
269  expr_map[ID_minus] = binary_expr;
270  expr_map[ID_implies] = binary_expr;
271  expr_map[ID_equal] = binary_expr;
272  expr_map[ID_notequal] = binary_expr;
273 
274  auto unary_expr = [](std::ostream &os, const exprt &expr) -> std::ostream & {
275  return format_rec(os, to_unary_expr(expr));
276  };
277 
278  expr_map[ID_not] = unary_expr;
279  expr_map[ID_unary_minus] = unary_expr;
280 
281  expr_map[ID_constant] =
282  [](std::ostream &os, const exprt &expr) -> std::ostream & {
283  return format_rec(os, to_constant_expr(expr));
284  };
285 
286  expr_map[ID_typecast] =
287  [](std::ostream &os, const exprt &expr) -> std::ostream & {
288  return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
289  << format(expr.type()) << ')';
290  };
291 
292  auto byte_extract =
293  [](std::ostream &os, const exprt &expr) -> std::ostream & {
294  const auto &byte_extract_expr = to_byte_extract_expr(expr);
295  return os << expr.id() << '(' << format(byte_extract_expr.op()) << ", "
296  << format(byte_extract_expr.offset()) << ", "
297  << format(byte_extract_expr.type()) << ')';
298  };
299 
300  expr_map[ID_byte_extract_little_endian] = byte_extract;
301  expr_map[ID_byte_extract_big_endian] = byte_extract;
302 
303  auto byte_update = [](std::ostream &os, const exprt &expr) -> std::ostream & {
304  const auto &byte_update_expr = to_byte_update_expr(expr);
305  return os << expr.id() << '(' << format(byte_update_expr.op()) << ", "
306  << format(byte_update_expr.offset()) << ", "
307  << format(byte_update_expr.value()) << ", "
308  << format(byte_update_expr.type()) << ')';
309  };
310 
311  expr_map[ID_byte_update_little_endian] = byte_update;
312  expr_map[ID_byte_update_big_endian] = byte_update;
313 
314  expr_map[ID_member] =
315  [](std::ostream &os, const exprt &expr) -> std::ostream & {
316  return os << format(to_member_expr(expr).op()) << '.'
318  };
319 
320  expr_map[ID_symbol] =
321  [](std::ostream &os, const exprt &expr) -> std::ostream & {
322  return os << to_symbol_expr(expr).get_identifier();
323  };
324 
325  expr_map[ID_index] =
326  [](std::ostream &os, const exprt &expr) -> std::ostream & {
327  const auto &index_expr = to_index_expr(expr);
328  return os << format(index_expr.array()) << '[' << format(index_expr.index())
329  << ']';
330  };
331 
332  expr_map[ID_type] =
333  [](std::ostream &os, const exprt &expr) -> std::ostream & {
334  return format_rec(os, expr.type());
335  };
336 
337  expr_map[ID_forall] =
338  [](std::ostream &os, const exprt &expr) -> std::ostream & {
339  return os << u8"\u2200 " << format(to_quantifier_expr(expr).symbol())
340  << " : " << format(to_quantifier_expr(expr).symbol().type())
341  << " . " << format(to_quantifier_expr(expr).where());
342  };
343 
344  expr_map[ID_exists] =
345  [](std::ostream &os, const exprt &expr) -> std::ostream & {
346  return os << u8"\u2203 " << format(to_quantifier_expr(expr).symbol())
347  << " : " << format(to_quantifier_expr(expr).symbol().type())
348  << " . " << format(to_quantifier_expr(expr).where());
349  };
350 
351  expr_map[ID_let] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
352  return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
353  << format(to_let_expr(expr).value()) << " IN "
354  << format(to_let_expr(expr).where());
355  };
356 
357  expr_map[ID_lambda] =
358  [](std::ostream &os, const exprt &expr) -> std::ostream & {
359  const auto &lambda_expr = to_lambda_expr(expr);
360 
361  os << u8"\u03bb ";
362 
363  bool first = true;
364 
365  for(auto &v : lambda_expr.variables())
366  {
367  if(first)
368  first = false;
369  else
370  os << ", ";
371 
372  os << format(v);
373  }
374 
375  return os << " . " << format(lambda_expr.where());
376  };
377 
378  auto compound = [](std::ostream &os, const exprt &expr) -> std::ostream & {
379  os << "{ ";
380 
381  bool first = true;
382 
383  for(const auto &op : expr.operands())
384  {
385  if(first)
386  first = false;
387  else
388  os << ", ";
389 
390  os << format(op);
391  }
392 
393  return os << " }";
394  };
395 
396  expr_map[ID_array] = compound;
397  expr_map[ID_struct] = compound;
398 
399  expr_map[ID_if] = [](std::ostream &os, const exprt &expr) -> std::ostream & {
400  const auto &if_expr = to_if_expr(expr);
401  return os << '(' << format(if_expr.cond()) << " ? "
402  << format(if_expr.true_case()) << " : "
403  << format(if_expr.false_case()) << ')';
404  };
405 
406  expr_map[ID_code] =
407  [](std::ostream &os, const exprt &expr) -> std::ostream & {
408  const auto &code = to_code(expr);
409  const irep_idt &statement = code.get_statement();
410 
411  if(statement == ID_assign)
412  return os << format(to_code_assign(code).lhs()) << " = "
413  << format(to_code_assign(code).rhs()) << ';';
414  else if(statement == ID_block)
415  {
416  os << '{';
417  for(const auto &s : to_code_block(code).statements())
418  os << ' ' << format(s);
419  return os << " }";
420  }
421  else if(statement == ID_dead)
422  {
423  return os << "dead " << format(to_code_dead(code).symbol()) << ";";
424  }
425  else if(const auto decl = expr_try_dynamic_cast<code_declt>(code))
426  {
427  const auto &declaration_symb = decl->symbol();
428  os << "decl " << format(declaration_symb.type()) << " "
429  << format(declaration_symb);
430  if(const optionalt<exprt> initial_value = decl->initial_value())
431  os << " = " << format(*initial_value);
432  return os << ";";
433  }
434  else if(statement == ID_function_call)
435  {
436  const auto &func_call = to_code_function_call(code);
437  os << to_symbol_expr(func_call.function()).get_identifier() << "(";
438 
439  // Join all our arguments together.
440  join_strings(
441  os,
442  func_call.arguments().begin(),
443  func_call.arguments().end(),
444  ", ",
445  [](const exprt &expr) { return format(expr); });
446 
447  return os << ");";
448  }
449  else
450  return fallback_format_rec(os, expr);
451  };
452 
453  fallback = [](std::ostream &os, const exprt &expr) -> std::ostream & {
454  return fallback_format_rec(os, expr);
455  };
456 }
457 
460 {
461  auto m_it = expr_map.find(expr.id());
462  if(m_it == expr_map.end())
463  return fallback;
464  else
465  return m_it->second;
466 }
467 
469 
470 std::ostream &format_rec(std::ostream &os, const exprt &expr)
471 {
472  auto &formatter = format_expr_config.find_formatter(expr);
473  return formatter(os, expr);
474 }
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:241
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:329
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:741
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:492
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:1297
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
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:282
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
format_expr_configt::expr_map
expr_mapt expr_map
Definition: format_expr.cpp:232
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
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:628
expr.h
format_expr_configt
Definition: format_expr.cpp:221
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:468
fallback_format_rec
std::ostream & fallback_format_rec(std::ostream &os, const exprt &expr)
Definition: format_expr.cpp:191
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:110
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:2940
format_expr_config
format_expr_configt format_expr_config
Definition: format_expr.cpp:468
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
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:294
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:459
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
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:1815
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:1180
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:2612
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:2542
exprt::operands
operandst & operands()
Definition: expr.h:96
format_expr_configt::format_expr_configt
format_expr_configt()
Definition: format_expr.cpp:223
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
format_expr_configt::setup
void setup()
setup the expressions we can format
Definition: format_expr.cpp:247
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:816
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2676
format_type.h
format_expr_configt::expr_mapt
std::unordered_map< irep_idt, formattert > expr_mapt
Definition: format_expr.cpp:230
format_expr_configt::formattert
std::function< std::ostream &(std::ostream &, const exprt &)> formattert
Definition: format_expr.cpp:229
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:2701