From 3a40db1e76b0bf1a4fbfe8790dbdf4dc9d70dc99 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 9 Aug 2018 18:18:14 +0100 Subject: [PATCH 1/4] Make expr2ct configurable in a number of ways This makes the subclassing of it redundant and should instead be customsied via the configuration. --- src/ansi-c/expr2c.cpp | 48 +++++++++++++++++++++++++++++-------- src/ansi-c/expr2c.h | 50 +++++++++++++++++++++++++++++++++++++++ src/ansi-c/expr2c_class.h | 11 ++++++++- 3 files changed, 98 insertions(+), 11 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 80b5515dd0f..c9642eacc9a 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -30,6 +30,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_qualifiers.h" #include "expr2c_class.h" +expr2c_configurationt expr2c_configurationt::default_configuration{true, + true, + true, + "TRUE", + "FALSE"}; + /* Precedences are as follows. Higher values mean higher precedence. @@ -661,7 +667,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 +745,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 +2008,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 +3959,33 @@ std::string expr2ct::convert(const exprt &src) return convert_with_precedence(src, precedence); } -std::string expr2c(const exprt &expr, const namespacet &ns) +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) { - expr2ct expr2c(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, 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); +} diff --git a/src/ansi-c/expr2c.h b/src/ansi-c/expr2c.h index 2bbcad3832e..1f3e612968d 100644 --- a/src/ansi-c/expr2c.h +++ b/src/ansi-c/expr2c.h @@ -16,7 +16,57 @@ 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; +}; + 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); + #endif // CPROVER_ANSI_C_EXPR2C_H diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index a2424b8e5e3..36fd130a16c 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANSI_C_EXPR2C_CLASS_H #define CPROVER_ANSI_C_EXPR2C_CLASS_H +#include "expr2c.h" + #include #include #include @@ -23,7 +25,13 @@ 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); @@ -33,6 +41,7 @@ class expr2ct protected: const namespacet &ns; + const expr2c_configurationt &configuration; virtual std::string convert_rec( const typet &src, From c3fef700c1eef76f1f39cd45079b5f5254a857ff Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 10 Aug 2018 15:13:57 +0100 Subject: [PATCH 2/4] Add a clean configuration for expr2c This configuration can be used in place of expr2cleanc --- src/ansi-c/expr2c.cpp | 6 ++++++ src/ansi-c/expr2c.h | 4 ++++ 2 files changed, 10 insertions(+) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index c9642eacc9a..64a1a07b6b5 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -36,6 +36,12 @@ expr2c_configurationt expr2c_configurationt::default_configuration{true, "TRUE", "FALSE"}; +expr2c_configurationt expr2c_configurationt::clean_configuration{false, + false, + false, + "1", + "0"}; + /* Precedences are as follows. Higher values mean higher precedence. diff --git a/src/ansi-c/expr2c.h b/src/ansi-c/expr2c.h index 1f3e612968d..8f364c53dac 100644 --- a/src/ansi-c/expr2c.h +++ b/src/ansi-c/expr2c.h @@ -53,6 +53,10 @@ struct expr2c_configurationt final /// 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); From 0cfacb898f379ba704b6baf3c30512e9817d1576 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 10 Aug 2018 15:14:33 +0100 Subject: [PATCH 3/4] Add type2c conversion for specifying a type name --- src/ansi-c/expr2c.cpp | 22 ++++++++++++++++++++++ src/ansi-c/expr2c.h | 6 ++++++ src/ansi-c/expr2c_class.h | 3 +++ 3 files changed, 31 insertions(+) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 64a1a07b6b5..cae49e09b39 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3965,6 +3965,18 @@ std::string expr2ct::convert(const exprt &src) return convert_with_precedence(src, precedence); } +/// 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, @@ -3995,3 +4007,13 @@ 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); +} diff --git a/src/ansi-c/expr2c.h b/src/ansi-c/expr2c.h index 8f364c53dac..3689c5478bb 100644 --- a/src/ansi-c/expr2c.h +++ b/src/ansi-c/expr2c.h @@ -73,4 +73,10 @@ std::string type2c( 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 diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 36fd130a16c..e705260cc01 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -39,6 +39,9 @@ class expr2ct 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; From 6e04213b8b3202745a30a3a3da49d0d9a6709715 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 14 Aug 2018 11:17:38 +0100 Subject: [PATCH 4/4] Reformatting the structs to aid readability --- src/ansi-c/expr2c.cpp | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index cae49e09b39..3a0a0ba2f84 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -30,18 +30,27 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_qualifiers.h" #include "expr2c_class.h" -expr2c_configurationt expr2c_configurationt::default_configuration{true, - true, - true, - "TRUE", - "FALSE"}; - -expr2c_configurationt expr2c_configurationt::clean_configuration{false, - false, - false, - "1", - "0"}; +// 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.