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 
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(
228  id == ID_plus || id == ID_mult || id == ID_and || id == ID_or ||
229  id == ID_xor)
230  {
231  return format_rec(os, to_multi_ary_expr(expr));
232  }
233  else if(
234  id == ID_lt || id == ID_gt || id == ID_ge || id == ID_le || id == ID_div ||
235  id == ID_minus || id == ID_implies || id == ID_equal || id == ID_notequal)
236  {
237  return format_rec(os, to_binary_expr(expr));
238  }
239  else if(id == ID_not || id == ID_unary_minus)
240  return format_rec(os, to_unary_expr(expr));
241  else if(id == ID_constant)
242  return format_rec(os, to_constant_expr(expr));
243  else if(id == ID_typecast)
244  return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
245  << format(expr.type()) << ')';
246  else if(
247  id == ID_byte_extract_little_endian || id == ID_byte_extract_big_endian)
248  {
249  const auto &byte_extract_expr = to_byte_extract_expr(expr);
250  return os << id << '(' << format(byte_extract_expr.op()) << ", "
251  << format(byte_extract_expr.offset()) << ", "
252  << format(byte_extract_expr.type()) << ')';
253  }
254  else if(id == ID_byte_update_little_endian || id == ID_byte_update_big_endian)
255  {
256  const auto &byte_update_expr = to_byte_update_expr(expr);
257  return os << id << '(' << format(byte_update_expr.op()) << ", "
258  << format(byte_update_expr.offset()) << ", "
259  << format(byte_update_expr.value()) << ", "
260  << format(byte_update_expr.type()) << ')';
261  }
262  else if(id == ID_member)
263  return os << format(to_member_expr(expr).op()) << '.'
265  else if(id == ID_symbol)
266  return os << to_symbol_expr(expr).get_identifier();
267  else if(id == ID_index)
268  {
269  const auto &index_expr = to_index_expr(expr);
270  return os << format(index_expr.array()) << '[' << format(index_expr.index())
271  << ']';
272  }
273  else if(id == ID_type)
274  return format_rec(os, expr.type());
275  else if(id == ID_forall)
276  return os << u8"\u2200 " << format(to_quantifier_expr(expr).symbol())
277  << " : " << format(to_quantifier_expr(expr).symbol().type())
278  << " . " << format(to_quantifier_expr(expr).where());
279  else if(id == ID_exists)
280  return os << u8"\u2203 " << format(to_quantifier_expr(expr).symbol())
281  << " : " << format(to_quantifier_expr(expr).symbol().type())
282  << " . " << format(to_quantifier_expr(expr).where());
283  else if(id == ID_let)
284  return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
285  << format(to_let_expr(expr).value()) << " IN "
286  << format(to_let_expr(expr).where());
287  else if(id == ID_array || id == ID_struct)
288  {
289  os << "{ ";
290 
291  bool first = true;
292 
293  for(const auto &op : expr.operands())
294  {
295  if(first)
296  first = false;
297  else
298  os << ", ";
299 
300  os << format(op);
301  }
302 
303  return os << " }";
304  }
305  else if(id == ID_if)
306  {
307  const auto &if_expr = to_if_expr(expr);
308  return os << '(' << format(if_expr.cond()) << " ? "
309  << format(if_expr.true_case()) << " : "
310  << format(if_expr.false_case()) << ')';
311  }
312  else if(id == ID_code)
313  {
314  const auto &code = to_code(expr);
315  const irep_idt &statement = code.get_statement();
316 
317  if(statement == ID_assign)
318  return os << format(to_code_assign(code).lhs()) << " = "
319  << format(to_code_assign(code).rhs()) << ';';
320  else if(statement == ID_block)
321  {
322  os << '{';
323  for(const auto &s : to_code_block(code).statements())
324  os << ' ' << format(s);
325  return os << " }";
326  }
327  else if(statement == ID_dead)
328  {
329  return os << "dead " << format(to_code_dead(code).symbol()) << ";";
330  }
331  else if(statement == ID_decl)
332  {
333  const auto &declaration_symb = to_code_decl(code).symbol();
334  return os << "decl " << format(declaration_symb.type()) << " "
335  << format(declaration_symb) << ";";
336  }
337  else if(statement == ID_function_call)
338  {
339  const auto &func_call = to_code_function_call(code);
340  os << to_symbol_expr(func_call.function()).get_identifier() << "(";
341 
342  // Join all our arguments together.
343  join_strings(
344  os,
345  func_call.arguments().begin(),
346  func_call.arguments().end(),
347  ", ",
348  [](const exprt &expr) { return format(expr); });
349 
350  return os << ");";
351  }
352  else
353  return fallback_format_rec(os, expr);
354  }
355  else
356  return fallback_format_rec(os, expr);
357 }
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:35
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:791
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
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:450
string_utils.h
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
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:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
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:53
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:269
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
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:678
expr.h
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:92
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:479
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:127
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:64
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:519
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4289
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
std_code.h
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
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:322
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:2047
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:1230
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:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
exprt::operands
operandst & operands()
Definition: expr.h:95
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
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:866
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
format_type.h
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:139
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:3939