Merge pull request #6092 from diffblue/add_expression_formatters

Add various formatters

Author: kroening

scripts/expected_doxygen_warnings.txt

@@ -7,8 +7,8 @@ warning: Included by graph for 'invariant.h' not generated, too many nodes (172)
 warning: Included by graph for 'irep.h' not generated, too many nodes (80), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'namespace.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (120), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'prefix.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (121), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'prefix.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (67), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (71), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_expr.h' not generated, too many nodes (178), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/util/format_expr.cpp

@@ -17,6 +17,8 @@ Author: Daniel Kroening, [email protected]
 #include "ieee_float.h"
 #include "mathematical_expr.h"
 #include "mp_arith.h"
+#include "pointer_expr.h"
+#include "prefix.h"
 #include "std_code.h"
 #include "string_utils.h"
 
@@ -177,8 +179,30 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
     return os << '"' << escape(id2string(src.get_value())) << '"';
   else if(type == ID_floatbv)
     return os << ieee_floatt(src);
-  else if(type == ID_pointer && src.is_zero())
-    return os << src.get_value();
+  else if(type == ID_pointer)
+  {
+    if(src.is_zero())
+      return os << ID_NULL;
+    else if(has_prefix(id2string(src.get_value()), "INVALID-"))
+    {
+      return os << "INVALID-POINTER";
+    }
+    else if(src.operands().size() == 1)
+    {
+      const auto &unary_expr = to_unary_expr(src);
+      const auto &pointer_type = to_pointer_type(src.type());
+      return os << "pointer(" << format(unary_expr.op()) << ", "
+                << format(pointer_type.subtype()) << ')';
+    }
+    else
+    {
+      const auto &pointer_type = to_pointer_type(src.type());
+      const auto width = pointer_type.get_width();
+      auto int_value = bvrep2integer(src.get_value(), width, false);
+      return os << "pointer(0x" << integer2string(int_value, 16) << ", "
+                << format(pointer_type.subtype()) << ')';
+    }
+  }
   else
     return os << src.pretty();
 }
@@ -445,6 +469,39 @@ void format_expr_configt::setup()
       return fallback_format_rec(os, expr);
   };
 
+  expr_map[ID_string_constant] =
+    [](std::ostream &os, const exprt &expr) -> std::ostream & {
+    return os << '"' << expr.get_string(ID_value) << '"';
+  };
+
+  expr_map[ID_function_application] =
+    [](std::ostream &os, const exprt &expr) -> std::ostream & {
+    const auto &function_application_expr = to_function_application_expr(expr);
+    os << format(function_application_expr.function()) << '(';
+    bool first = true;
+    for(auto &argument : function_application_expr.arguments())
+    {
+      if(first)
+        first = false;
+      else
+        os << ", ";
+      os << format(argument);
+    }
+    os << ')';
+    return os;
+  };
+
+  expr_map[ID_dereference] =
+    [](std::ostream &os, const exprt &expr) -> std::ostream & {
+    const auto &dereference_expr = to_dereference_expr(expr);
+    os << '*';
+    if(dereference_expr.pointer().id() != ID_symbol)
+      os << '(' << format(dereference_expr.pointer()) << ')';
+    else
+      os << format(dereference_expr.pointer());
+    return os;
+  };
+
   fallback = [](std::ostream &os, const exprt &expr) -> std::ostream & {
     return fallback_format_rec(os, expr);
   };

src/util/format_type.cpp

@@ -9,7 +9,9 @@ Author: Daniel Kroening, [email protected]
 #include "format_type.h"
 #include "c_types.h"
 #include "format_expr.h"
+#include "mathematical_types.h"
 #include "pointer_expr.h"
+#include "std_types.h"
 
 #include <ostream>
 
@@ -98,6 +100,21 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
     return os << "\xe2\x84\x95"; // u+2115, 'N'
   else if(id == ID_rational)
     return os << "\xe2\x84\x9a"; // u+211A, 'Q'
+  else if(id == ID_mathematical_function)
+  {
+    const auto &mathematical_function = to_mathematical_function_type(type);
+    bool first = true;
+    for(const auto &domain : mathematical_function.domain())
+    {
+      if(first)
+        first = false;
+      else
+        os << u8" \u00d7 "; // ×
+      os << format(domain);
+    }
+    os << u8" \u2192 "; // → -- we don't use ⟶  since that doesn't render well
+    return os << format(mathematical_function.codomain());
+  }
   else
     return os << id;
 }