Merge pull request #2713 from thk123/dump/expr2c-configuration

Configurable expr2c

Author: Thomas Kiley

src/ansi-c/expr2c.cpp

@@ -30,6 +30,27 @@ Author: Daniel Kroening, [email protected]
 #include "c_qualifiers.h"
 #include "expr2c_class.h"
 
+// clang-format off
+
+expr2c_configurationt expr2c_configurationt::default_configuration
+{
+  true,
+  true,
+  true,
+  "TRUE",
+  "FALSE"
+};
+
+expr2c_configurationt expr2c_configurationt::clean_configuration
+{
+  false,
+  false,
+  false,
+  "1",
+  "0"
+};
+
+// clang-format on
 /*
 
 Precedences are as follows. Higher values mean higher precedence.
@@ -661,7 +682,12 @@ std::string expr2ct::convert_struct_type(
   const std::string &qualifiers_str,
   const std::string &declarator_str)
 {
-  return convert_struct_type(src, qualifiers_str, declarator_str, true, true);
+  return convert_struct_type(
+    src,
+    qualifiers_str,
+    declarator_str,
+    configuration.print_struct_body_in_type,
+    configuration.include_struct_padding_components);
 }
 
 /// To generate C-like string for declaring (or defining) the given struct
@@ -734,7 +760,8 @@ std::string expr2ct::convert_array_type(
   const qualifierst &qualifiers,
   const std::string &declarator_str)
 {
-  return convert_array_type(src, qualifiers, declarator_str, true);
+  return convert_array_type(
+    src, qualifiers, declarator_str, configuration.include_array_size);
 }
 
 /// To generate a C-like type declaration of an array. Optionally can include or
@@ -1996,18 +2023,18 @@ std::string expr2ct::convert_constant(
 ///   FALSE.
 std::string expr2ct::convert_constant_bool(bool boolean_value)
 {
-  // C doesn't really have these
   if(boolean_value)
-    return "TRUE";
+    return configuration.true_string;
   else
-    return "FALSE";
+    return configuration.false_string;
 }
 
 std::string expr2ct::convert_struct(
   const exprt &src,
   unsigned &precedence)
 {
-  return convert_struct(src, precedence, true);
+  return convert_struct(
+    src, precedence, configuration.include_struct_padding_components);
 }
 
 /// To generate a C-like string representing a struct. Can optionally include
@@ -3947,17 +3974,55 @@ std::string expr2ct::convert(const exprt &src)
   return convert_with_precedence(src, precedence);
 }
 
-std::string expr2c(const exprt &expr, const namespacet &ns)
+/// Build a declaration string, which requires converting both a type and
+/// putting an identifier in the syntactically correct position.
+/// \param src: the type to convert
+/// \param identifier: the identifier to use as the type
+/// \return A C declaration of the given type with the right identifier.
+std::string expr2ct::convert_with_identifier(
+  const typet &src,
+  const std::string &identifier)
+{
+  return convert_rec(src, c_qualifierst(), identifier);
+}
+
+std::string expr2c(
+  const exprt &expr,
+  const namespacet &ns,
+  const expr2c_configurationt &configuration)
 {
   std::string code;
-  expr2ct expr2c(ns);
+  expr2ct expr2c(ns, configuration);
   expr2c.get_shorthands(expr);
   return expr2c.convert(expr);
 }
 
-std::string type2c(const typet &type, const namespacet &ns)
+std::string expr2c(const exprt &expr, const namespacet &ns)
+{
+  return expr2c(expr, ns, expr2c_configurationt::default_configuration);
+}
+
+std::string type2c(
+  const typet &type,
+  const namespacet &ns,
+  const expr2c_configurationt &configuration)
 {
-  expr2ct expr2c(ns);
+  expr2ct expr2c(ns, configuration);
   // expr2c.get_shorthands(expr);
   return expr2c.convert(type);
 }
+
+std::string type2c(const typet &type, const namespacet &ns)
+{
+  return type2c(type, ns, expr2c_configurationt::default_configuration);
+}
+
+std::string type2c(
+  const typet &type,
+  const std::string &identifier,
+  const namespacet &ns,
+  const expr2c_configurationt &configuration)
+{
+  expr2ct expr2c(ns, configuration);
+  return expr2c.convert_with_identifier(type, identifier);
+}

src/ansi-c/expr2c.h

@@ -16,7 +16,67 @@ class exprt;
 class namespacet;
 class typet;
 
+/// Used for configuring the behaviour of expr2c and type2c
+struct expr2c_configurationt final
+{
+  /// When printing struct_typet or struct_exprt, include the artificial padding
+  /// components introduced to keep the struct aligned.
+  bool include_struct_padding_components;
+
+  /// When printing a struct_typet, should the components of the struct be
+  /// printed inline.
+  bool print_struct_body_in_type;
+
+  /// When printing array_typet, should the size of the array be printed
+  bool include_array_size;
+
+  /// This is the string that will be printed for the true boolean expression
+  std::string true_string;
+
+  /// This is the string that will be printed for the false boolean expression
+  std::string false_string;
+
+  expr2c_configurationt(
+    const bool include_struct_padding_components,
+    const bool print_struct_body_in_type,
+    const bool include_array_size,
+    std::string true_string,
+    std::string false_string)
+    : include_struct_padding_components(include_struct_padding_components),
+      print_struct_body_in_type(print_struct_body_in_type),
+      include_array_size(include_array_size),
+      true_string(std::move(true_string)),
+      false_string(std::move(false_string))
+  {
+  }
+
+  /// This prints a human readable C like syntax that closely mirrors the
+  /// internals of the GOTO program
+  static expr2c_configurationt default_configuration;
+
+  /// This prints compilable C that loses some of the internal details of the
+  /// GOTO program
+  static expr2c_configurationt clean_configuration;
+};
+
 std::string expr2c(const exprt &expr, const namespacet &ns);
+
+std::string expr2c(
+  const exprt &expr,
+  const namespacet &ns,
+  const expr2c_configurationt &configuration);
+
 std::string type2c(const typet &type, const namespacet &ns);
 
+std::string type2c(
+  const typet &type,
+  const namespacet &ns,
+  const expr2c_configurationt &configuration);
+
+std::string type2c(
+  const typet &type,
+  const std::string &identifier,
+  const namespacet &ns,
+  const expr2c_configurationt &configuration);
+
 #endif // CPROVER_ANSI_C_EXPR2C_H

src/ansi-c/expr2c_class.h

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANSI_C_EXPR2C_CLASS_H
 #define CPROVER_ANSI_C_EXPR2C_CLASS_H
 
+#include "expr2c.h"
+
 #include <string>
 #include <unordered_map>
 #include <unordered_set>
@@ -23,16 +25,26 @@ class namespacet;
 class expr2ct
 {
 public:
-  explicit expr2ct(const namespacet &_ns):ns(_ns), sizeof_nesting(0) { }
+  explicit expr2ct(
+    const namespacet &_ns,
+    const expr2c_configurationt &configuration =
+      expr2c_configurationt::default_configuration)
+    : ns(_ns), configuration(configuration), sizeof_nesting(0)
+  {
+  }
   virtual ~expr2ct() { }
 
   virtual std::string convert(const typet &src);
   virtual std::string convert(const exprt &src);
 
   void get_shorthands(const exprt &expr);
 
+  std::string
+  convert_with_identifier(const typet &src, const std::string &identifier);
+
 protected:
   const namespacet &ns;
+  const expr2c_configurationt &configuration;
 
   virtual std::string convert_rec(
     const typet &src,