Skip to content

Commit b38ecc3

Browse files
author
Daniel Kroening
committed
added format() for exprt and typet
1 parent 76b93e8 commit b38ecc3

File tree

9 files changed

+362
-7
lines changed

9 files changed

+362
-7
lines changed

‎src/util/Makefile

+2
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,9 @@ SRC = arith_tools.cpp \
1717
find_symbols.cpp \
1818
fixedbv.cpp \
1919
format_constant.cpp \
20+
format_expr.cpp \
2021
format_number_range.cpp \
22+
format_type.cpp \
2123
fresh_symbol.cpp \
2224
get_base_name.cpp \
2325
get_module.cpp \

‎src/util/expr.cpp

-4
Original file line numberDiff line numberDiff line change
@@ -9,17 +9,13 @@ Author: Daniel Kroening, [email protected]
99
/// \file
1010
/// Expression Representation
1111

12-
#include "arith_tools.h"
1312
#include "expr.h"
1413
#include "expr_iterator.h"
1514
#include "fixedbv.h"
1615
#include "ieee_float.h"
17-
#include "invariant.h"
18-
#include "mp_arith.h"
1916
#include "rational.h"
2017
#include "rational_tools.h"
2118
#include "std_expr.h"
22-
#include "string2int.h"
2319

2420
#include <stack>
2521

‎src/util/expr.h

+1-2
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,12 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
109
#ifndef CPROVER_UTIL_EXPR_H
1110
#define CPROVER_UTIL_EXPR_H
1211

13-
#include <functional>
1412
#include "type.h"
1513

14+
#include <functional>
1615
#include <list>
1716

1817
#define forall_operands(it, expr) \

‎src/util/format.h

+40
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_UTIL_FORMAT_H
10+
#define CPROVER_UTIL_FORMAT_H
11+
12+
#include <iosfwd>
13+
14+
//! The below enables convenient syntax for feeding
15+
//! objects into streams, via stream << format(o)
16+
template <typename T>
17+
class format_containert
18+
{
19+
public:
20+
explicit format_containert(const T &_o) : o(_o)
21+
{
22+
}
23+
24+
const T &o;
25+
};
26+
27+
template <typename T>
28+
static inline std::ostream &
29+
operator<<(std::ostream &os, const format_containert<T> &f)
30+
{
31+
return format_rec(os, f.o);
32+
}
33+
34+
template <typename T>
35+
static inline format_containert<T> format(const T &o)
36+
{
37+
return format_containert<T>(o);
38+
}
39+
40+
#endif // CPROVER_UTIL_FORMAT_H

‎src/util/format_expr.cpp

+220
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,220 @@
1+
/*******************************************************************\
2+
3+
Module: Expression Pretty Printing
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Expression Pretty Printing
11+
12+
#include "arith_tools.h"
13+
#include "expr.h"
14+
#include "expr_iterator.h"
15+
#include "fixedbv.h"
16+
#include "format_expr.h"
17+
#include "format_type.h"
18+
#include "ieee_float.h"
19+
#include "invariant.h"
20+
#include "mp_arith.h"
21+
#include "rational.h"
22+
#include "rational_tools.h"
23+
#include "std_expr.h"
24+
#include "string2int.h"
25+
26+
#include <stack>
27+
#include <ostream>
28+
29+
/// We use the precendences that most readers expect
30+
/// (i.e., the ones you learn in primary school),
31+
/// and stay clear of the surprising ones that C has.
32+
static bool bracket_subexpression(
33+
const exprt &sub_expr,
34+
const exprt &expr)
35+
{
36+
// no need for parentheses whenever the subexpression
37+
// doesn't have operands
38+
if(!sub_expr.has_operands())
39+
return false;
40+
41+
// * and / bind stronger than + and -
42+
if(
43+
(sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
44+
(expr.id() == ID_plus || expr.id() == ID_minus))
45+
return false;
46+
47+
// ==, !=, <, <=, >, >= bind stronger than && and ||
48+
if(
49+
(sub_expr.id() == ID_equal || sub_expr.id() == ID_notequal ||
50+
sub_expr.id() == ID_lt || sub_expr.id() == ID_gt ||
51+
sub_expr.id() == ID_le || sub_expr.id() == ID_ge) &&
52+
(expr.id() == ID_and || expr.id() == ID_or))
53+
return false;
54+
55+
return true;
56+
}
57+
58+
/// This formats a multi-ary expression,
59+
/// adding parentheses where indicated by \ref bracket_subexpression
60+
static std::ostream &format_rec(
61+
std::ostream &os,
62+
const multi_ary_exprt &src)
63+
{
64+
bool first = true;
65+
66+
for(const auto &op : src.operands())
67+
{
68+
if(first)
69+
first = false;
70+
else
71+
os << ' ' << src.id() << ' ';
72+
73+
const bool need_parentheses = bracket_subexpression(op, src);
74+
75+
if(need_parentheses)
76+
os << '(';
77+
78+
os << format(op);
79+
80+
if(need_parentheses)
81+
os << ')';
82+
}
83+
84+
return os;
85+
}
86+
87+
/// This formats a binary expression,
88+
/// which we do as for multi-ary expressions
89+
static std::ostream &format_rec(
90+
std::ostream &os,
91+
const binary_exprt &src)
92+
{
93+
return format_rec(os, to_multi_ary_expr(src));
94+
}
95+
96+
/// This formats a unary expression,
97+
/// adding parentheses very aggressively.
98+
static std::ostream &format_rec(
99+
std::ostream &os,
100+
const unary_exprt &src)
101+
{
102+
if(src.id() == ID_not)
103+
os << '!';
104+
else if(src.id() == ID_unary_minus)
105+
os << '-';
106+
else
107+
return os << src.pretty();
108+
109+
if(src.op0().has_operands())
110+
return os << '(' << format(src.op0()) << ')';
111+
else
112+
return os << format(src.op0());
113+
}
114+
115+
/// This formats a constant
116+
static std::ostream &format_rec(
117+
std::ostream &os,
118+
const constant_exprt &src)
119+
{
120+
auto type = src.type().id();
121+
122+
if(type == ID_bool)
123+
{
124+
if(src.is_true())
125+
return os << "true";
126+
else if(src.is_false())
127+
return os << "false";
128+
else
129+
return os << src.pretty();
130+
}
131+
else if(type == ID_unsignedbv || type == ID_signedbv)
132+
return os << *numeric_cast<mp_integer>(src);
133+
else if(type == ID_integer)
134+
return os << src.get_value();
135+
else if(type == ID_floatbv)
136+
return os << ieee_floatt(src);
137+
else
138+
return os << src.pretty();
139+
}
140+
141+
// The below generates a string in a generic syntax
142+
// that is inspired by C/C++/Java, and is meant for debugging
143+
// purposes.
144+
std::ostream &format_rec(
145+
std::ostream &os,
146+
const exprt &expr)
147+
{
148+
const auto &id = expr.id();
149+
150+
if(id == ID_plus || id == ID_mult || id == ID_and || id == ID_or)
151+
return format_rec(os, to_multi_ary_expr(expr));
152+
else if(
153+
id == ID_lt || id == ID_gt || id == ID_ge || id == ID_le ||
154+
id == ID_minus || id == ID_implies || id == ID_equal || id == ID_notequal)
155+
return format_rec(os, to_binary_expr(expr));
156+
else if(id == ID_not || id == ID_unary_minus)
157+
return format_rec(os, to_unary_expr(expr));
158+
else if(id == ID_constant)
159+
return format_rec(os, to_constant_expr(expr));
160+
else if(id == ID_typecast)
161+
return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
162+
<< format(expr.type()) << ')';
163+
else if(id == ID_member)
164+
return os << format(to_member_expr(expr).op()) << '.'
165+
<< to_member_expr(expr).get_component_name();
166+
else if(id == ID_symbol)
167+
return os << to_symbol_expr(expr).get_identifier();
168+
else if(id == ID_forall || id == ID_exists)
169+
return os << id << ' ' << format(to_quantifier_expr(expr).symbol()) << " : "
170+
<< format(to_quantifier_expr(expr).symbol().type()) << " . "
171+
<< format(to_quantifier_expr(expr).where());
172+
else if(id == ID_let)
173+
return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
174+
<< format(to_let_expr(expr).value()) << " IN "
175+
<< format(to_let_expr(expr).where());
176+
else if(id == ID_array || id == ID_struct)
177+
{
178+
os << "{ ";
179+
180+
bool first = true;
181+
182+
for(const auto &op : expr.operands())
183+
{
184+
if(first)
185+
first = false;
186+
else
187+
os << ", ";
188+
189+
os << format(op);
190+
}
191+
192+
return os << '}';
193+
}
194+
else if(id == ID_if)
195+
{
196+
const auto &if_expr = to_if_expr(expr);
197+
return os << format(if_expr.cond()) << '?' << format(if_expr.true_case())
198+
<< ':' << format(if_expr.false_case());
199+
}
200+
else
201+
{
202+
if(!expr.has_operands())
203+
return os << id;
204+
205+
os << id << '(';
206+
bool first = true;
207+
208+
for(const auto &op : expr.operands())
209+
{
210+
if(first)
211+
first = false;
212+
else
213+
os << ", ";
214+
215+
os << format(op);
216+
}
217+
218+
return os << ')';
219+
}
220+
}

‎src/util/format_expr.h

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_UTIL_FORMAT_EXPR_H
10+
#define CPROVER_UTIL_FORMAT_EXPR_H
11+
12+
#include "format.h"
13+
#include "expr.h"
14+
15+
//! Formats an expression in a generic syntax
16+
//! that is inspired by C/C++/Java, and is meant for debugging
17+
std::ostream &format_rec(std::ostream &, const exprt &);
18+
19+
#endif // CPROVER_UTIL_FORMAT_EXPR_H

‎src/util/format_type.cpp

+60
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "format_expr.h"
10+
#include "format_type.h"
11+
#include "std_types.h"
12+
13+
#include <ostream>
14+
15+
/// format a \ref struct_typet
16+
static std::ostream &format_rec(
17+
std::ostream &os,
18+
const struct_typet &src)
19+
{
20+
os << "struct"
21+
<< " {";
22+
bool first = true;
23+
24+
for(const auto &c : src.components())
25+
{
26+
if(first)
27+
first = false;
28+
else
29+
os << ',';
30+
31+
os << ' ' << format(c.type()) << ' ' << c.get_name();
32+
}
33+
34+
return os << " }";
35+
}
36+
37+
// The below generates a string in a generic syntax
38+
// that is inspired by C/C++/Java, and is meant for debugging
39+
// purposes.
40+
std::ostream &format_rec(std::ostream &os, const typet &type)
41+
{
42+
const auto &id = type.id();
43+
44+
if(id == ID_pointer)
45+
return os << '*' << format(type.subtype());
46+
else if(id == ID_array)
47+
{
48+
const auto &t = to_array_type(type);
49+
if(t.is_complete())
50+
return os << format(type.subtype()) << '[' << format(t.size()) << ']';
51+
else
52+
return os << format(type.subtype()) << "[]";
53+
}
54+
else if(id == ID_struct)
55+
return format_rec(os, to_struct_type(type));
56+
else if(id == ID_symbol)
57+
return os << "symbol_type " << to_symbol_type(type).get_identifier();
58+
else
59+
return os << id;
60+
}

0 commit comments

Comments
 (0)