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 "expr.h"
16 #include "expr_iterator.h"
17 #include "fixedbv.h"
18 #include "format_type.h"
19 #include "ieee_float.h"
20 #include "invariant.h"
21 #include "mp_arith.h"
22 #include "rational.h"
23 #include "rational_tools.h"
24 #include "std_code.h"
25 #include "std_expr.h"
26 #include "string2int.h"
27 #include "string_utils.h"
28 
29 #include <ostream>
30 #include <stack>
31 
35 static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
36 {
37  // no need for parentheses whenever the subexpression
38  // doesn't have operands
39  if(!sub_expr.has_operands())
40  return false;
41 
42  // * and / bind stronger than + and -
43  if(
44  (sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
45  (expr.id() == ID_plus || expr.id() == ID_minus))
46  return false;
47 
48  // ==, !=, <, <=, >, >= bind stronger than && and ||
49  if(
50  (sub_expr.id() == ID_equal || sub_expr.id() == ID_notequal ||
51  sub_expr.id() == ID_lt || sub_expr.id() == ID_gt ||
52  sub_expr.id() == ID_le || sub_expr.id() == ID_ge) &&
53  (expr.id() == ID_and || expr.id() == ID_or))
54  return false;
55 
56  return true;
57 }
58 
61 static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
62 {
63  bool first = true;
64 
65  for(const auto &op : src.operands())
66  {
67  if(first)
68  first = false;
69  else
70  os << ' ' << src.id() << ' ';
71 
72  const bool need_parentheses = bracket_subexpression(op, src);
73 
74  if(need_parentheses)
75  os << '(';
76 
77  os << format(op);
78 
79  if(need_parentheses)
80  os << ')';
81  }
82 
83  return os;
84 }
85 
88 static std::ostream &format_rec(std::ostream &os, const binary_exprt &src)
89 {
90  return format_rec(os, to_multi_ary_expr(src));
91 }
92 
95 static std::ostream &format_rec(std::ostream &os, const unary_exprt &src)
96 {
97  if(src.id() == ID_not)
98  os << '!';
99  else if(src.id() == ID_unary_minus)
100  os << '-';
101  else
102  return os << src.pretty();
103 
104  if(src.op0().has_operands())
105  return os << '(' << format(src.op0()) << ')';
106  else
107  return os << format(src.op0());
108 }
109 
111 static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
112 {
113  auto type = src.type().id();
114 
115  if(type == ID_bool)
116  {
117  if(src.is_true())
118  return os << "true";
119  else if(src.is_false())
120  return os << "false";
121  else
122  return os << src.pretty();
123  }
124  else if(type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool)
125  return os << *numeric_cast<mp_integer>(src);
126  else if(type == ID_integer)
127  return os << src.get_value();
128  else if(type == ID_string)
129  return os << '"' << escape(id2string(src.get_value())) << '"';
130  else if(type == ID_floatbv)
131  return os << ieee_floatt(src);
132  else if(type == ID_pointer && src.is_zero())
133  return os << src.get_value();
134  else
135  return os << src.pretty();
136 }
137 
138 std::ostream &fallback_format_rec(std::ostream &os, const exprt &expr)
139 {
140  os << expr.id();
141 
142  for(const auto &s : expr.get_named_sub())
143  if(s.first != ID_type)
144  os << ' ' << s.first << "=\"" << s.second.id() << '"';
145 
146  if(expr.has_operands())
147  {
148  os << '(';
149  bool first = true;
150 
151  for(const auto &op : expr.operands())
152  {
153  if(first)
154  first = false;
155  else
156  os << ", ";
157 
158  os << format(op);
159  }
160 
161  os << ')';
162  }
163 
164  return os;
165 }
166 
167 // The below generates a string in a generic syntax
168 // that is inspired by C/C++/Java, and is meant for debugging
169 // purposes.
170 std::ostream &format_rec(std::ostream &os, const exprt &expr)
171 {
172  const auto &id = expr.id();
173 
174  if(id == ID_plus || id == ID_mult || id == ID_and || id == ID_or)
175  return format_rec(os, to_multi_ary_expr(expr));
176  else if(
177  id == ID_lt || id == ID_gt || id == ID_ge || id == ID_le ||
178  id == ID_minus || id == ID_implies || id == ID_equal || id == ID_notequal)
179  return format_rec(os, to_binary_expr(expr));
180  else if(id == ID_not || id == ID_unary_minus)
181  return format_rec(os, to_unary_expr(expr));
182  else if(id == ID_constant)
183  return format_rec(os, to_constant_expr(expr));
184  else if(id == ID_typecast)
185  return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
186  << format(expr.type()) << ')';
187  else if(id == ID_member)
188  return os << format(to_member_expr(expr).op()) << '.'
190  else if(id == ID_symbol)
191  return os << to_symbol_expr(expr).get_identifier();
192  else if(id == ID_index)
193  {
194  const auto &index_expr = to_index_expr(expr);
195  return os << format(index_expr.array()) << '[' << format(index_expr.index())
196  << ']';
197  }
198  else if(id == ID_type)
199  return format_rec(os, expr.type());
200  else if(id == ID_forall || id == ID_exists)
201  return os << id << ' ' << format(to_quantifier_expr(expr).symbol()) << " : "
202  << format(to_quantifier_expr(expr).symbol().type()) << " . "
203  << format(to_quantifier_expr(expr).where());
204  else if(id == ID_let)
205  return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
206  << format(to_let_expr(expr).value()) << " IN "
207  << format(to_let_expr(expr).where());
208  else if(id == ID_array || id == ID_struct)
209  {
210  os << "{ ";
211 
212  bool first = true;
213 
214  for(const auto &op : expr.operands())
215  {
216  if(first)
217  first = false;
218  else
219  os << ", ";
220 
221  os << format(op);
222  }
223 
224  return os << '}';
225  }
226  else if(id == ID_if)
227  {
228  const auto &if_expr = to_if_expr(expr);
229  return os << format(if_expr.cond()) << '?' << format(if_expr.true_case())
230  << ':' << format(if_expr.false_case());
231  }
232  else if(id == ID_code)
233  {
234  const auto &code = to_code(expr);
235  const irep_idt &statement = code.get_statement();
236 
237  if(statement == ID_assign)
238  return os << format(to_code_assign(code).lhs()) << " = "
239  << format(to_code_assign(code).rhs()) << ';';
240  else if(statement == ID_block)
241  {
242  os << '{';
243  for(const auto &s : to_code_block(code).operands())
244  os << ' ' << format(s);
245  return os << " }";
246  }
247  else
248  return fallback_format_rec(os, expr);
249  }
250  else
251  return fallback_format_rec(os, expr);
252 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
std::ostream & fallback_format_rec(std::ostream &os, const exprt &expr)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const irep_idt & get_identifier() const
Definition: std_expr.h:128
bool is_false() const
Definition: expr.cpp:131
const irep_idt & get_value() const
Definition: std_expr.h:4441
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
A constant literal expression.
Definition: std_expr.h:4424
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
Definition: std_expr.h:4755
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:35
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
A generic base class for binary expressions.
Definition: std_expr.h:649
API to expression classes.
Generic base class for unary expressions.
Definition: std_expr.h:303
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
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:61
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast a generic exprt to a quantifier_exprt.
Definition: std_expr.h:4830
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
bool has_operands() const
Definition: expr.h:63
named_subt & get_named_sub()
Definition: irep.h:247
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast a generic exprt to a multi_ary_exprt.
Definition: std_expr.h:877
Base class for all expressions.
Definition: expr.h:42
irep_idt get_component_name() const
Definition: std_expr.h:3895
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
bool is_zero() const
Definition: expr.cpp:161
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:164
const binary_exprt & to_binary_expr(const exprt &expr)
Cast a generic exprt to a binary_exprt.
Definition: std_expr.h:702
A generic base class for multi-ary expressions.
Definition: std_expr.h:830
const unary_exprt & to_unary_expr(const exprt &expr)
Cast a generic exprt to a unary_exprt.
Definition: std_expr.h:361
operandst & operands()
Definition: expr.h:66
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
static format_containert< T > format(const T &o)
Definition: format.h:35