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 "mp_arith.h"
23 #include "rational.h"
24 #include "rational_tools.h"
25 #include "std_code.h"
26 #include "std_expr.h"
27 #include "string2int.h"
28 #include "string_utils.h"
29 
30 #include <ostream>
31 #include <stack>
32 
33 // expressions that are rendered with infix operators
34 struct infix_opt
35 {
36  const char *rep;
37 };
38 
39 const std::map<irep_idt, infix_opt> infix_map = {
40  {ID_plus, {"+"}},
41  {ID_minus, {"-"}},
42  {ID_mult, {"*"}},
43  {ID_div, {"/"}},
44  {ID_equal, {"="}},
45  {ID_notequal, {u8"\u2260"}}, // /=, U+2260
46  {ID_and, {u8"\u2227"}}, // wedge, U+2227
47  {ID_or, {u8"\u2228"}}, // vee, U+2228
48  {ID_xor, {u8"\u2295"}}, // + in circle, U+2295
49  {ID_implies, {u8"\u21d2"}}, // =>, U+21D2
50  {ID_le, {u8"\u2264"}}, // <=, U+2264
51  {ID_ge, {u8"\u2265"}}, // >=, U+2265
52  {ID_lt, {"<"}},
53  {ID_gt, {">"}},
54 };
55 
59 static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
60 {
61  // no need for parentheses whenever the subexpression
62  // doesn't have operands
63  if(!sub_expr.has_operands())
64  return false;
65 
66  // no need if subexpression isn't an infix operator
67  if(infix_map.find(sub_expr.id()) == infix_map.end())
68  return false;
69 
70  // * and / bind stronger than + and -
71  if(
72  (sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
73  (expr.id() == ID_plus || expr.id() == ID_minus))
74  return false;
75 
76  // ==, !=, <, <=, >, >= bind stronger than && and ||
77  if(
78  (sub_expr.id() == ID_equal || sub_expr.id() == ID_notequal ||
79  sub_expr.id() == ID_lt || sub_expr.id() == ID_gt ||
80  sub_expr.id() == ID_le || sub_expr.id() == ID_ge) &&
81  (expr.id() == ID_and || expr.id() == ID_or))
82  return false;
83 
84  // +, -, *, / bind stronger than ==, !=, <, <=, >, >=
85  if(
86  (sub_expr.id() == ID_plus || sub_expr.id() == ID_minus ||
87  sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
88  (expr.id() == ID_equal || expr.id() == ID_notequal || expr.id() == ID_lt ||
89  expr.id() == ID_gt || expr.id() == ID_le || expr.id() == ID_ge))
90  {
91  return false;
92  }
93 
94  return true;
95 }
96 
99 static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
100 {
101  bool first = true;
102 
103  std::string operator_str = id2string(src.id()); // default
104 
105  if(
106  src.id() == ID_equal && !src.operands().empty() &&
107  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 
220 // The below generates a string in a generic syntax
221 // that is inspired by C/C++/Java, and is meant for debugging
222 // purposes.
223 std::ostream &format_rec(std::ostream &os, const exprt &expr)
224 {
225  const auto &id = expr.id();
226 
227  if(id == ID_plus || id == ID_mult || id == ID_and || id == ID_or)
228  return format_rec(os, to_multi_ary_expr(expr));
229  else if(
230  id == ID_lt || id == ID_gt || id == ID_ge || id == ID_le ||
231  id == ID_minus || id == ID_implies || id == ID_equal || id == ID_notequal)
232  return format_rec(os, to_binary_expr(expr));
233  else if(id == ID_not || id == ID_unary_minus)
234  return format_rec(os, to_unary_expr(expr));
235  else if(id == ID_constant)
236  return format_rec(os, to_constant_expr(expr));
237  else if(id == ID_typecast)
238  return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
239  << format(expr.type()) << ')';
240  else if(
241  id == ID_byte_extract_little_endian || id == ID_byte_extract_big_endian)
242  {
243  const auto &byte_extract_expr = to_byte_extract_expr(expr);
244  return os << id << '(' << format(byte_extract_expr.op()) << ", "
245  << format(byte_extract_expr.offset()) << ", "
246  << format(byte_extract_expr.type()) << ')';
247  }
248  else if(id == ID_byte_update_little_endian || id == ID_byte_update_big_endian)
249  {
250  const auto &byte_update_expr = to_byte_update_expr(expr);
251  return os << id << '(' << format(byte_update_expr.op()) << ", "
252  << format(byte_update_expr.offset()) << ", "
253  << format(byte_update_expr.value()) << ", "
254  << format(byte_update_expr.type()) << ')';
255  }
256  else if(id == ID_member)
257  return os << format(to_member_expr(expr).op()) << '.'
259  else if(id == ID_symbol)
260  return os << to_symbol_expr(expr).get_identifier();
261  else if(id == ID_index)
262  {
263  const auto &index_expr = to_index_expr(expr);
264  return os << format(index_expr.array()) << '[' << format(index_expr.index())
265  << ']';
266  }
267  else if(id == ID_type)
268  return format_rec(os, expr.type());
269  else if(id == ID_forall)
270  return os << u8"\u2200 " << format(to_quantifier_expr(expr).symbol())
271  << " : " << format(to_quantifier_expr(expr).symbol().type())
272  << " . " << format(to_quantifier_expr(expr).where());
273  else if(id == ID_exists)
274  return os << u8"\u2203 " << format(to_quantifier_expr(expr).symbol())
275  << " : " << format(to_quantifier_expr(expr).symbol().type())
276  << " . " << format(to_quantifier_expr(expr).where());
277  else if(id == ID_let)
278  return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
279  << format(to_let_expr(expr).value()) << " IN "
280  << format(to_let_expr(expr).where());
281  else if(id == ID_array || id == ID_struct)
282  {
283  os << "{ ";
284 
285  bool first = true;
286 
287  for(const auto &op : expr.operands())
288  {
289  if(first)
290  first = false;
291  else
292  os << ", ";
293 
294  os << format(op);
295  }
296 
297  return os << " }";
298  }
299  else if(id == ID_if)
300  {
301  const auto &if_expr = to_if_expr(expr);
302  return os << '(' << format(if_expr.cond()) << " ? "
303  << format(if_expr.true_case()) << " : "
304  << format(if_expr.false_case()) << ')';
305  }
306  else if(id == ID_code)
307  {
308  const auto &code = to_code(expr);
309  const irep_idt &statement = code.get_statement();
310 
311  if(statement == ID_assign)
312  return os << format(to_code_assign(code).lhs()) << " = "
313  << format(to_code_assign(code).rhs()) << ';';
314  else if(statement == ID_block)
315  {
316  os << '{';
317  for(const auto &s : to_code_block(code).statements())
318  os << ' ' << format(s);
319  return os << " }";
320  }
321  else
322  return fallback_format_rec(os, expr);
323  }
324  else
325  return fallback_format_rec(os, expr);
326 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
const char * rep
Definition: format_expr.cpp:36
std::ostream & fallback_format_rec(std::ostream &os, const exprt &expr)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
uint64_t u8
Definition: bytecode_info.h:58
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
const exprt & op() const
Definition: std_expr.h:371
const irep_idt & get_identifier() const
Definition: std_expr.h:176
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
const irep_idt & get_value() const
Definition: std_expr.h:4403
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
typet & type()
Return the type of the expression.
Definition: expr.h:68
A constant literal expression.
Definition: std_expr.h:4384
Forward depth-first search iterators These iterators&#39; copy operations are expensive, so use auto&, and avoid std::next(), std::prev() and post-increment iterator.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4683
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:59
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:259
Expression classes for byte-level operators.
A base class for binary expressions.
Definition: std_expr.h:738
API to expression classes.
Generic base class for unary expressions.
Definition: std_expr.h:331
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
const std::map< irep_idt, infix_opt > infix_map
Definition: format_expr.cpp:39
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
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:99
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Definition: std_expr.h:4746
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
named_subt & get_named_sub()
Definition: irep.h:319
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:1028
Base class for all expressions.
Definition: expr.h:54
irep_idt get_component_name() const
Definition: std_expr.h:3915
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:810
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:973
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:395
operandst & operands()
Definition: expr.h:78
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
static format_containert< T > format(const T &o)
Definition: format.h:35