introduce add_format_hook(...)

This commit adds a function to extend the expression formatter at runtime.

Author: kroening

src/util/format_expr.cpp

@@ -616,6 +616,11 @@ format_expr_configt::find_formatter(const exprt &expr)
 
 format_expr_configt format_expr_config;
 
+void add_format_hook(irep_idt id, format_expr_configt::formattert formatter)
+{
+  format_expr_config.expr_map[id] = std::move(formatter);
+}
+
 std::ostream &format_rec(std::ostream &os, const exprt &expr)
 {
   auto &formatter = format_expr_config.find_formatter(expr);

src/util/format_expr.h

@@ -10,11 +10,21 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_UTIL_FORMAT_EXPR_H
 
 #include "format.h"
+#include "irep.h"
+
+#include <functional>
 
 class exprt;
 
 //! 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 &);
 
+/// Adds a formatter for expressions with the given ID at runtime.
+/// The formatter is given as a function that receives the output
+/// stream and the expression as arguments.
+void add_format_hook(
+  irep_idt,
+  std::function<std::ostream &(std::ostream &, const exprt &)>);
+
 #endif // CPROVER_UTIL_FORMAT_EXPR_H

unit/Makefile

@@ -135,6 +135,7 @@ SRC += analyses/ai/ai.cpp \
        util/expr_iterator.cpp \
        util/file_util.cpp \
        util/format.cpp \
+       util/format_expr.cpp \
        util/format_number_range.cpp \
        util/get_base_name.cpp \
        util/graph.cpp \

unit/util/format_expr.cpp

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+ Module: Unit tests for `format` function on expressions
+
+ Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include <util/exception_utils.h>
+#include <util/expr.h>
+#include <util/format_expr.h>
+
+#include <testing-utils/use_catch.h>
+
+TEST_CASE(
+  "Format an expression with a format hook",
+  "[core][util][format_hook]")
+{
+  irep_idt custom_id("custom_id");
+  add_format_hook(
+    custom_id, [](std::ostream &out, const exprt &expr) -> std::ostream & {
+      out << "output";
+      return out;
+    });
+  REQUIRE(format_to_string(exprt{custom_id}) == "output");
+}