Add pretty-printer extension mechanism

The existing language printers are used as-is for now, which works
as they are always the top of the printer chain, and so direct
recursion is equivalent to top_printer->convert.

Author: smowton

src/ansi-c/ansi_c_language.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "ansi_c_typecheck.h"
 #include "ansi_c_parser.h"
 #include "expr2c.h"
+#include "expr2c_class.h"
 #include "c_preprocess.h"
 #include "ansi_c_internal_additions.h"
 #include "type2name.h"
@@ -285,6 +286,24 @@ bool ansi_c_languaget::from_type(
 
 /*******************************************************************\
 
+Function: ansi_c_languaget::get_pretty_printer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::unique_ptr<pretty_printert>
+ansi_c_languaget::get_pretty_printer(const namespacet &ns)
+{
+  return std::unique_ptr<pretty_printert>(new expr2ct(ns));
+}
+
+/*******************************************************************\
+
 Function: ansi_c_languaget::type_to_name
 
   Inputs:

src/ansi-c/ansi_c_language.h

@@ -53,6 +53,9 @@ class ansi_c_languaget:public languaget
     std::string &code,
     const namespacet &ns) override;
 
+  std::unique_ptr<pretty_printert>
+    get_pretty_printer(const namespacet &) override;
+
   bool type_to_name(
     const typet &type,
     std::string &name,

src/ansi-c/expr2c.cpp

@@ -204,6 +204,7 @@ Function: expr2ct::convert
 
 std::string expr2ct::convert(const typet &src)
 {
+  assert(next_pretty_printer && "Next pretty-printer should be set");
   return convert_rec(src, c_qualifierst(), "");
 }
 
@@ -679,14 +680,7 @@ std::string expr2ct::convert_rec(
     return q+"__attribute__(("+id2string(src.id())+")) void"+d;
   }
 
-  {
-    lispexprt lisp;
-    irep2lisp(src, lisp);
-    std::string dest="irep(\""+MetaString(lisp.expr2string())+"\")";
-    dest+=d;
-
-    return dest;
-  }
+  return next_pretty_printer->convert(src);
 }
 
 /*******************************************************************\
@@ -5009,7 +5003,7 @@ std::string expr2ct::convert(
     return convert(src.type());
 
   // no C language expression for internal representation
-  return convert_norep(src, precedence);
+  return next_pretty_printer->convert(src);
 }
 
 /*******************************************************************\
@@ -5046,7 +5040,9 @@ std::string expr2c(const exprt &expr, const namespacet &ns)
 {
   std::string code;
   expr2ct expr2c(ns);
+  norep_pretty_printert norep;
   expr2c.get_shorthands(expr);
+  expr2c.set_next_pretty_printer(&norep);
   return expr2c.convert(expr);
 }
 
@@ -5065,6 +5061,8 @@ Function: type2c
 std::string type2c(const typet &type, const namespacet &ns)
 {
   expr2ct expr2c(ns);
+  norep_pretty_printert norep;
+  expr2c.set_next_pretty_printer(&norep);
   // expr2c.get_shorthands(expr);
   return expr2c.convert(type);
 }

src/ansi-c/expr2c_class.h

@@ -16,17 +16,19 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
+#include <langapi/pretty_printer.h>
+
 class c_qualifierst;
 class namespacet;
 
-class expr2ct
+class expr2ct:public pretty_printert
 {
 public:
   explicit expr2ct(const namespacet &_ns):ns(_ns), sizeof_nesting(0) { }
   virtual ~expr2ct() { }
 
-  virtual std::string convert(const typet &src);
-  virtual std::string convert(const exprt &src);
+  std::string convert(const typet &src) override;
+  std::string convert(const exprt &src) override;
 
   void get_shorthands(const exprt &expr);
 

src/cpp/cpp_language.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include "cpp_internal_additions.h"
 #include "cpp_language.h"
 #include "expr2cpp.h"
+#include "expr2cpp_class.h"
 #include "cpp_parser.h"
 #include "cpp_typecheck.h"
 #include "cpp_type2name.h"
@@ -362,6 +363,24 @@ bool cpp_languaget::from_type(
 
 /*******************************************************************\
 
+Function: cpp_languaget::get_pretty_printer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::unique_ptr<pretty_printert>
+cpp_languaget::get_pretty_printer(const namespacet &ns)
+{
+  return std::unique_ptr<pretty_printert>(new expr2cppt(ns));
+}
+
+/*******************************************************************\
+
 Function: cpp_languaget::type_to_name
 
   Inputs:

src/cpp/cpp_language.h

@@ -62,6 +62,9 @@ class cpp_languaget:public languaget
     std::string &code,
     const namespacet &ns) override;
 
+  std::unique_ptr<pretty_printert>
+    get_pretty_printer(const namespacet &) override;
+
   bool type_to_name(
     const typet &type,
     std::string &name,

src/cpp/expr2cpp.cpp

@@ -17,44 +17,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/c_misc.h>
 #include <ansi-c/c_qualifiers.h>
-#include <ansi-c/expr2c_class.h>
 
 #include "expr2cpp.h"
-
-class expr2cppt:public expr2ct
-{
-public:
-  explicit expr2cppt(const namespacet &_ns):expr2ct(_ns) { }
-
-  std::string convert(const exprt &src) override
-  {
-    return expr2ct::convert(src);
-  }
-
-  std::string convert(const typet &src) override
-  {
-    return expr2ct::convert(src);
-  }
-
-protected:
-  std::string convert(const exprt &src, unsigned &precedence) override;
-  std::string convert_cpp_this(const exprt &src, unsigned precedence);
-  std::string convert_cpp_new(const exprt &src, unsigned precedence);
-  std::string convert_extractbit(const exprt &src, unsigned precedence);
-  std::string convert_extractbits(const exprt &src, unsigned precedence);
-  std::string convert_code_cpp_delete(const exprt &src, unsigned precedence);
-  std::string convert_struct(const exprt &src, unsigned &precedence) override;
-  std::string convert_code(const codet &src, unsigned indent) override;
-  // NOLINTNEXTLINE(whitespace/line_length)
-  std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
-
-  std::string convert_rec(
-    const typet &src,
-    const c_qualifierst &qualifiers,
-    const std::string &declarator) override;
-
-  typedef std::unordered_set<std::string, string_hash> id_sett;
-};
+#include "expr2cpp_class.h"
 
 /*******************************************************************\
 
@@ -647,6 +612,8 @@ std::string expr2cpp(const exprt &expr, const namespacet &ns)
 {
   expr2cppt expr2cpp(ns);
   expr2cpp.get_shorthands(expr);
+  norep_pretty_printert norep;
+  expr2cpp.set_next_pretty_printer(&norep);
   return expr2cpp.convert(expr);
 }
 
@@ -665,5 +632,7 @@ Function: type2cpp
 std::string type2cpp(const typet &type, const namespacet &ns)
 {
   expr2cppt expr2cpp(ns);
+  norep_pretty_printert norep;
+  expr2cpp.set_next_pretty_printer(&norep);
   return expr2cpp.convert(type);
 }

src/cpp/expr2cpp_class.h

@@ -0,0 +1,49 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_CPP_EXPR2CPP_CLASS_H
+#define CPROVER_CPP_EXPR2CPP_CLASS_H
+
+#include <ansi-c/expr2c_class.h>
+
+class expr2cppt:public expr2ct
+{
+public:
+  explicit expr2cppt(const namespacet &_ns):expr2ct(_ns) { }
+
+  std::string convert(const exprt &src) override
+  {
+    return expr2ct::convert(src);
+  }
+
+  std::string convert(const typet &src) override
+  {
+    return expr2ct::convert(src);
+  }
+
+protected:
+  std::string convert(const exprt &src, unsigned &precedence) override;
+  std::string convert_cpp_this(const exprt &src, unsigned precedence);
+  std::string convert_cpp_new(const exprt &src, unsigned precedence);
+  std::string convert_extractbit(const exprt &src, unsigned precedence);
+  std::string convert_extractbits(const exprt &src, unsigned precedence);
+  std::string convert_code_cpp_delete(const exprt &src, unsigned precedence);
+  std::string convert_struct(const exprt &src, unsigned &precedence) override;
+  std::string convert_code(const codet &src, unsigned indent) override;
+  // NOLINTNEXTLINE(whitespace/line_length)
+  std::string convert_constant(const constant_exprt &src, unsigned &precedence) override;
+
+  std::string convert_rec(
+    const typet &src,
+    const c_qualifierst &qualifiers,
+    const std::string &declarator) override;
+
+  typedef std::unordered_set<std::string, string_hash> id_sett;
+};
+
+#endif

src/java_bytecode/expr2java.cpp

@@ -565,6 +565,8 @@ std::string expr2java(const exprt &expr, const namespacet &ns)
 {
   expr2javat expr2java(ns);
   expr2java.get_shorthands(expr);
+  norep_pretty_printert norep;
+  expr2java.set_next_pretty_printer(&norep);
   return expr2java.convert(expr);
 }
 
@@ -583,5 +585,7 @@ Function: type2java
 std::string type2java(const typet &type, const namespacet &ns)
 {
   expr2javat expr2java(ns);
+  norep_pretty_printert norep;
+  expr2java.set_next_pretty_printer(&norep);
   return expr2java.convert(type);
 }

src/java_bytecode/java_bytecode_language.cpp

@@ -850,6 +850,24 @@ bool java_bytecode_languaget::from_type(
 
 /*******************************************************************\
 
+Function: java_bytecode_languaget::get_pretty_printer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::unique_ptr<pretty_printert>
+java_bytecode_languaget::get_pretty_printer(const namespacet &ns)
+{
+  return std::unique_ptr<pretty_printert>(new expr2javat(ns));
+}
+
+/*******************************************************************\
+
 Function: java_bytecode_languaget::to_expr
 
   Inputs:

src/java_bytecode/java_bytecode_language.h

@@ -70,6 +70,9 @@ class java_bytecode_languaget:public languaget
     std::string &code,
     const namespacet &ns) override;
 
+  std::unique_ptr<pretty_printert>
+    get_pretty_printer(const namespacet &) override;
+
   bool to_expr(
     const std::string &code,
     const std::string &module,

src/jsil/expr2jsil.cpp

@@ -9,24 +9,7 @@ Author: Michael Tautschnig, [email protected]
 #include <ansi-c/expr2c_class.h>
 
 #include "expr2jsil.h"
-
-class expr2jsilt:public expr2ct
-{
-public:
-  explicit expr2jsilt(const namespacet &_ns):expr2ct(_ns) { }
-
-  virtual std::string convert(const exprt &src)
-  {
-    return expr2ct::convert(src);
-  }
-
-  virtual std::string convert(const typet &src)
-  {
-    return expr2ct::convert(src);
-  }
-
-protected:
-};
+#include "expr2jsil_class.h"
 
 /*******************************************************************\
 
@@ -44,6 +27,8 @@ std::string expr2jsil(const exprt &expr, const namespacet &ns)
 {
   expr2jsilt expr2jsil(ns);
   expr2jsil.get_shorthands(expr);
+  norep_pretty_printert norep;
+  expr2jsil.set_next_pretty_printer(&norep);
   return expr2jsil.convert(expr);
 }
 
@@ -62,5 +47,7 @@ Function: type2jsil
 std::string type2jsil(const typet &type, const namespacet &ns)
 {
   expr2jsilt expr2jsil(ns);
+  norep_pretty_printert norep;
+  expr2jsil.set_next_pretty_printer(&norep);
   return expr2jsil.convert(type);
 }