added format() for exprt and typet

Author: Daniel Kroening

src/util/expr.cpp

@@ -9,19 +9,21 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Expression Representation
 
+#include "arith_tools.h"
 #include "expr.h"
-#include <cassert>
-#include <stack>
-#include "string2int.h"
-#include "mp_arith.h"
+#include "expr_iterator.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
 #include "invariant.h"
-#include "expr_iterator.h"
+#include "mp_arith.h"
 #include "rational.h"
 #include "rational_tools.h"
-#include "arith_tools.h"
 #include "std_expr.h"
+#include "string2int.h"
+
+#include <cassert>
+#include <stack>
+#include <ostream>
 
 void exprt::move_to_operands(exprt &expr)
 {
@@ -535,3 +537,182 @@ const_unique_depth_iteratort exprt::unique_depth_cbegin() const
 { return const_unique_depth_iteratort(*this); }
 const_unique_depth_iteratort exprt::unique_depth_cend() const
 { return const_unique_depth_iteratort(); }
+
+/// We use the precendences that most readers expect
+/// (i.e., the ones you learn in primary school),
+/// and stay clear of the surprising ones that C has.
+static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
+{
+  // no need for parentheses whenever the subexpression
+  // doesn't have operands
+  if(!sub_expr.has_operands())
+    return false;
+
+  // * and / bind stronger than + and -
+  if(
+    (sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
+    (expr.id() == ID_plus || expr.id() == ID_minus))
+    return false;
+
+  // ==, !=, <, <=, >, >= bind stronger than && and ||
+  if(
+    (sub_expr.id() == ID_equal || sub_expr.id() == ID_notequal ||
+     sub_expr.id() == ID_lt || sub_expr.id() == ID_gt ||
+     sub_expr.id() == ID_le || sub_expr.id() == ID_ge) &&
+    (expr.id() == ID_and || expr.id() == ID_or))
+    return false;
+
+  return true;
+}
+
+/// This formats turns a multi-ary expression,
+/// adding parentheses where indicated by the precedence.
+static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
+{
+  bool first = true;
+
+  for(const auto &op : src.operands())
+  {
+    if(first)
+      first = false;
+    else
+      os << ' ' << src.id() << ' ';
+
+    const bool need_parentheses = bracket_subexpression(op, src);
+
+    if(need_parentheses)
+      os << '(';
+
+    os << format(op);
+
+    if(need_parentheses)
+      os << ')';
+  }
+
+  return os;
+}
+
+/// This formats a binary expression
+static std::ostream &format_rec(std::ostream &os, const binary_exprt &src)
+{
+  return format_rec(os, to_multi_ary_expr(src));
+}
+
+/// This formats a unary expression,
+/// adding parentheses very aggressively.
+static std::ostream &format_rec(std::ostream &os, const unary_exprt &src)
+{
+  if(src.id() == ID_not)
+    os << '!';
+  else if(src.id() == ID_unary_minus)
+    os << '-';
+  else
+    return os << src.pretty();
+
+  if(src.op0().has_operands())
+    return os << '(' << format(src.op0()) << ')';
+  else
+    return os << format(src.op0());
+}
+
+static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
+{
+  auto type = src.type().id();
+
+  if(type == ID_bool)
+  {
+    if(src.is_true())
+      return os << "true";
+    else if(src.is_false())
+      return os << "false";
+    else
+      return os << src.pretty();
+  }
+  else if(type == ID_unsignedbv || type == ID_signedbv)
+    return os << *numeric_cast<mp_integer>(src);
+  else if(type == ID_integer)
+    return os << src.get_value();
+  else if(type == ID_floatbv)
+    return os << ieee_floatt(src);
+  else
+    return os << src.pretty();
+}
+
+// The below generates a string in a generic syntax
+// that is inspired by C/C++/Java, and is meant for debugging
+// purposes.
+std::ostream &format_rec(std::ostream &os, const exprt &expr)
+{
+  const auto &id = expr.id();
+
+  if(id == ID_plus || id == ID_mult || id == ID_and || id == ID_or)
+    return format_rec(os, to_multi_ary_expr(expr));
+  else if(
+    id == ID_lt || id == ID_gt || id == ID_ge || id == ID_le ||
+    id == ID_minus || id == ID_implies || id == ID_equal || id == ID_notequal)
+    return format_rec(os, to_binary_expr(expr));
+  else if(id == ID_not || id == ID_unary_minus)
+    return format_rec(os, to_unary_expr(expr));
+  else if(id == ID_constant)
+    return format_rec(os, to_constant_expr(expr));
+  else if(id == ID_typecast)
+    return os << "cast(" << format(to_typecast_expr(expr).op()) << ", "
+              << format(expr.type()) << ')';
+  else if(id == ID_member)
+    return os << format(to_member_expr(expr).op()) << '.'
+              << to_member_expr(expr).get_component_name();
+  else if(id == ID_symbol)
+    return os << to_symbol_expr(expr).get_identifier();
+  else if(id == ID_forall || id == ID_exists)
+    return os << id << ' ' << format(to_quantifier_expr(expr).symbol()) << " : "
+              << format(to_quantifier_expr(expr).symbol().type()) << " . "
+              << format(to_quantifier_expr(expr).where());
+  else if(id == ID_let)
+    return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
+              << format(to_let_expr(expr).value()) << " IN "
+              << format(to_let_expr(expr).where());
+  else if(id == ID_array || id == ID_struct)
+  {
+    os << "{ ";
+
+    bool first = true;
+
+    for(const auto &op : expr.operands())
+    {
+      if(first)
+        first = false;
+      else
+        os << ", ";
+
+      os << format(op);
+    }
+
+    return os << '}';
+  }
+  else if(id == ID_if)
+  {
+    const auto &if_expr = to_if_expr(expr);
+    return os << format(if_expr.cond()) << '?' << format(if_expr.true_case())
+              << ':' << format(if_expr.false_case());
+  }
+  else
+  {
+    if(!expr.has_operands())
+      return os << id;
+
+    os << id << '(';
+    bool first = true;
+
+    for(const auto &op : expr.operands())
+    {
+      if(first)
+        first = false;
+      else
+        os << ", ";
+
+      os << format(op);
+    }
+
+    return os << ')';
+  }
+}

src/util/expr.h

@@ -6,13 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #ifndef CPROVER_UTIL_EXPR_H
 #define CPROVER_UTIL_EXPR_H
 
-#include <functional>
 #include "type.h"
 
+#include <functional>
 #include <list>
 
 #define forall_operands(it, expr) \
@@ -164,6 +163,10 @@ class exprt:public irept
   const_unique_depth_iteratort unique_depth_cend() const;
 };
 
+//! Formats an expression in a generic syntax
+//! that is inspired by C/C++/Java, and is meant for debugging
+std::ostream &format_rec(std::ostream &, const exprt &);
+
 class expr_visitort
 {
 public:

src/util/format.h

@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_FORMAT_H
+#define CPROVER_UTIL_FORMAT_H
+
+#include <iosfwd>
+
+//! The below enables convenient syntax for feeding
+//! objects into streams, via stream << format(o)
+template <typename T>
+class format_containert
+{
+public:
+  explicit format_containert(const T &_o) : o(_o)
+  {
+  }
+
+  const T &o;
+};
+
+template <typename T>
+static inline std::ostream &
+operator<<(std::ostream &os, const format_containert<T> &f)
+{
+  return format_rec(os, f.o);
+}
+
+template <typename T>
+static inline format_containert<T> format(const T &o)
+{
+  return format_containert<T>(o);
+}
+
+#endif // CPROVER_UTIL_FORMAT_H

src/util/type.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "std_types.h"
 #include "namespace.h"
 
+#include <ostream>
+
 void typet::copy_to_subtypes(const typet &type)
 {
   subtypes().push_back(type);
@@ -106,3 +108,47 @@ bool is_constant_or_has_constant_components(
 
   return false;
 }
+
+static std::ostream &format_rec(std::ostream &os, const struct_typet &src)
+{
+  os << "struct"
+     << " {";
+  bool first = true;
+
+  for(const auto &c : src.components())
+  {
+    if(first)
+      first = false;
+    else
+      os << ',';
+
+    os << ' ' << format(c.type()) << ' ' << c.get_name();
+  }
+
+  return os << " }";
+}
+
+// The below generates a string in a generic syntax
+// that is inspired by C/C++/Java, and is meant for debugging
+// purposes.
+std::ostream &format_rec(std::ostream &os, const typet &type)
+{
+  const auto &id = type.id();
+
+  if(id == ID_pointer)
+    return os << '*' << format(type.subtype());
+  else if(id == ID_array)
+  {
+    const auto &t = to_array_type(type);
+    if(t.is_complete())
+      return os << format(type.subtype()) << '[' << format(t.size()) << ']';
+    else
+      return os << format(type.subtype()) << "[]";
+  }
+  else if(id == ID_struct)
+    return format_rec(os, to_struct_type(type));
+  else if(id == ID_symbol)
+    return os << "symbol_type " << to_symbol_type(type).get_identifier();
+  else
+    return os << id;
+}

src/util/type.h

@@ -10,7 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_TYPE_H
 #define CPROVER_UTIL_TYPE_H
 
-#include <util/source_location.h>
+#include "format.h"
+#include "source_location.h"
 
 #define SUBTYPE_IN_GETSUB
 #define SUBTYPES_IN_GETSUB
@@ -115,6 +116,10 @@ class typet:public irept
   }
 };
 
+//! Formats a type in a generic syntax
+//! that is inspired by C/C++/Java, and is meant for debugging
+std::ostream &format_rec(std::ostream &, const typet &);
+
 class type_with_subtypet:public typet
 {
 public: