From 957f87c57b6f4a87d385f7402a2b3a974b74569d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2022 19:50:27 +0000 Subject: [PATCH 1/2] ansi_c_convert_typet is not a messaget Use a message handler instead. --- src/ansi-c/ansi_c_convert_type.cpp | 89 ++++++++++++++++-------------- src/ansi-c/ansi_c_convert_type.h | 19 ++++--- src/cpp/cpp_convert_type.cpp | 17 +++--- 3 files changed, 68 insertions(+), 57 deletions(-) diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 431a9f0a908..7fe0a391980 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -286,6 +287,8 @@ void ansi_c_convert_typet::read_rec(const typet &type) void ansi_c_convert_typet::write(typet &type) { + messaget log{message_handler}; + type.clear(); // first, do "other" @@ -302,8 +305,8 @@ void ansi_c_convert_typet::write(typet &type) gcc_float128_cnt || gcc_float128x_cnt || gcc_int128_cnt || bv_cnt) { - error().source_location=source_location; - error() << "illegal type modifier for defined type" << eom; + log.error().source_location = source_location; + log.error() << "illegal type modifier for defined type" << messaget::eom; throw 0; } @@ -318,8 +321,8 @@ void ansi_c_convert_typet::write(typet &type) if(other.size()!=1) { - error().source_location=source_location; - error() << "illegal combination of defined types" << eom; + log.error().source_location = source_location; + log.error() << "illegal combination of defined types" << messaget::eom; throw 0; } @@ -342,9 +345,9 @@ void ansi_c_convert_typet::write(typet &type) { if(constructor && destructor) { - error().source_location=source_location; - error() << "combining constructor and destructor not supported" - << eom; + log.error().source_location = source_location; + log.error() << "combining constructor and destructor not supported" + << messaget::eom; throw 0; } @@ -354,9 +357,9 @@ void ansi_c_convert_typet::write(typet &type) else if(type_p->id()!=ID_empty) { - error().source_location=source_location; - error() << "constructor and destructor required to be type void, " - << "found " << type_p->pretty() << eom; + log.error().source_location = source_location; + log.error() << "constructor and destructor required to be type void, " + << "found " << type_p->pretty() << messaget::eom; throw 0; } @@ -365,9 +368,9 @@ void ansi_c_convert_typet::write(typet &type) } else if(constructor || destructor) { - error().source_location=source_location; - error() << "constructor and destructor required to be type void, " - << "found " << type.pretty() << eom; + log.error().source_location = source_location; + log.error() << "constructor and destructor required to be type void, " + << "found " << type.pretty() << messaget::eom; throw 0; } else if(gcc_float16_cnt || @@ -380,8 +383,9 @@ void ansi_c_convert_typet::write(typet &type) gcc_int128_cnt || bv_cnt || short_cnt || char_cnt) { - error().source_location=source_location; - error() << "cannot combine integer type with floating-point type" << eom; + log.error().source_location = source_location; + log.error() << "cannot combine integer type with floating-point type" + << messaget::eom; throw 0; } @@ -391,8 +395,8 @@ void ansi_c_convert_typet::write(typet &type) gcc_float64_cnt+gcc_float64x_cnt+ gcc_float128_cnt+gcc_float128x_cnt>=2) { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; + log.error().source_location = source_location; + log.error() << "conflicting type modifiers" << messaget::eom; throw 0; } @@ -421,15 +425,16 @@ void ansi_c_convert_typet::write(typet &type) gcc_int128_cnt|| bv_cnt || short_cnt || char_cnt) { - error().source_location=source_location; - error() << "cannot combine integer type with floating-point type" << eom; + log.error().source_location = source_location; + log.error() << "cannot combine integer type with floating-point type" + << messaget::eom; throw 0; } if(double_cnt && float_cnt) { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; + log.error().source_location = source_location; + log.error() << "conflicting type modifiers" << messaget::eom; throw 0; } @@ -446,15 +451,15 @@ void ansi_c_convert_typet::write(typet &type) type=long_double_type(); else { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; + log.error().source_location = source_location; + log.error() << "conflicting type modifiers" << messaget::eom; throw 0; } } else { - error().source_location=source_location; - error() << "illegal type modifier for float" << eom; + log.error().source_location = source_location; + log.error() << "illegal type modifier for float" << messaget::eom; throw 0; } } @@ -465,8 +470,9 @@ void ansi_c_convert_typet::write(typet &type) gcc_float128_cnt || bv_cnt || proper_bool_cnt || char_cnt || long_cnt) { - error().source_location=source_location; - error() << "illegal type modifier for C boolean type" << eom; + log.error().source_location = source_location; + log.error() << "illegal type modifier for C boolean type" + << messaget::eom; throw 0; } @@ -479,8 +485,9 @@ void ansi_c_convert_typet::write(typet &type) gcc_float128_cnt || bv_cnt || char_cnt || long_cnt) { - error().source_location=source_location; - error() << "illegal type modifier for proper boolean type" << eom; + log.error().source_location = source_location; + log.error() << "illegal type modifier for proper boolean type" + << messaget::eom; throw 0; } @@ -498,15 +505,15 @@ void ansi_c_convert_typet::write(typet &type) int8_cnt || int16_cnt || int32_cnt || int64_cnt || gcc_float128_cnt || bv_cnt || proper_bool_cnt) { - error().source_location=source_location; - error() << "illegal type modifier for char type" << eom; + log.error().source_location = source_location; + log.error() << "illegal type modifier for char type" << messaget::eom; throw 0; } if(signed_cnt && unsigned_cnt) { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; + log.error().source_location = source_location; + log.error() << "conflicting type modifiers" << messaget::eom; throw 0; } else if(unsigned_cnt) @@ -524,8 +531,8 @@ void ansi_c_convert_typet::write(typet &type) if(signed_cnt && unsigned_cnt) { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; + log.error().source_location = source_location; + log.error() << "conflicting type modifiers" << messaget::eom; throw 0; } else if(unsigned_cnt) @@ -537,8 +544,8 @@ void ansi_c_convert_typet::write(typet &type) { if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt) { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; + log.error().source_location = source_location; + log.error() << "conflicting type modifiers" << messaget::eom; throw 0; } @@ -594,8 +601,8 @@ void ansi_c_convert_typet::write(typet &type) { if(long_cnt || char_cnt) { - error().source_location=source_location; - error() << "conflicting type modifiers" << eom; + log.error().source_location = source_location; + log.error() << "conflicting type modifiers" << messaget::eom; throw 0; } @@ -627,8 +634,8 @@ void ansi_c_convert_typet::write(typet &type) } else { - error().source_location=source_location; - error() << "illegal type modifier for integer type" << eom; + log.error().source_location = source_location; + log.error() << "illegal type modifier for integer type" << messaget::eom; throw 0; } } diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index 7aff1a9953b..251882fa417 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -12,15 +12,16 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H #define CPROVER_ANSI_C_ANSI_C_CONVERT_TYPE_H -#include - -#include -#include +#include #include "c_qualifiers.h" #include "c_storage_spec.h" -class ansi_c_convert_typet:public messaget +#include + +class message_handlert; + +class ansi_c_convert_typet { public: unsigned unsigned_cnt, signed_cnt, char_cnt, @@ -62,9 +63,9 @@ class ansi_c_convert_typet:public messaget std::list other; - explicit ansi_c_convert_typet(message_handlert &_message_handler): - messaget(_message_handler) - // class members are initialized by calling read() + explicit ansi_c_convert_typet(message_handlert &_message_handler) + : message_handler(_message_handler) + // class members are initialized by calling read() { } @@ -98,6 +99,8 @@ class ansi_c_convert_typet:public messaget } protected: + message_handlert &message_handler; + virtual void read_rec(const typet &type); virtual void build_type_with_subtype(typet &type) const; virtual void set_attributes(typet &type) const; diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index a39616be24d..6ea85f07e8f 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include +#include #include #include @@ -86,7 +87,7 @@ void cpp_convert_typet::read_rec(const typet &type) { other.push_back(type); cpp_convert_plain_type( - to_array_type(other.back()).element_type(), get_message_handler()); + to_array_type(other.back()).element_type(), message_handler); } else if(type.id()==ID_template) { @@ -125,8 +126,7 @@ void cpp_convert_typet::read_template(const typet &type) other.push_back(type); typet &t=other.back(); - cpp_convert_plain_type( - to_type_with_subtype(t).subtype(), get_message_handler()); + cpp_convert_plain_type(to_type_with_subtype(t).subtype(), message_handler); irept &arguments=t.add(ID_arguments); @@ -142,7 +142,7 @@ void cpp_convert_typet::read_template(const typet &type) } else { - cpp_convert_plain_type(decl.type(), get_message_handler()); + cpp_convert_plain_type(decl.type(), message_handler); } // TODO: initializer @@ -163,7 +163,7 @@ void cpp_convert_typet::read_function_type(const typet &type) t.remove_subtype(); if(return_type.is_not_nil()) - cpp_convert_plain_type(return_type, get_message_handler()); + cpp_convert_plain_type(return_type, message_handler); // take care of parameter types code_typet::parameterst ¶meters = t.parameters(); @@ -182,7 +182,7 @@ void cpp_convert_typet::read_function_type(const typet &type) cpp_declarationt &declaration=to_cpp_declaration(parameter_expr); source_locationt type_location=declaration.type().source_location(); - cpp_convert_plain_type(declaration.type(), get_message_handler()); + cpp_convert_plain_type(declaration.type(), message_handler); // there should be only one declarator assert(declaration.declarators().size()==1); @@ -252,8 +252,9 @@ void cpp_convert_typet::write(typet &type) { if(wchar_t_count || char16_t_count || char32_t_count) { - error().source_location = source_location; - error() << "illegal type modifier for defined type" << eom; + messaget log{message_handler}; + log.error().source_location = source_location; + log.error() << "illegal type modifier for defined type" << messaget::eom; throw 0; } From 794f6f738e2545a53abddb1ebab0ecdd01fa31c9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 1 Dec 2022 19:53:33 +0000 Subject: [PATCH 2/2] Clean up ansi_c_convert_typet's interface The need to invoke read() was only specified in a comment. Make the constructor take care of this. Also, make the constructor initialise all members rather than leaving this to clear(), which is thus no longer necessary. --- src/ansi-c/ansi_c_convert_type.cpp | 7 --- src/ansi-c/ansi_c_convert_type.h | 83 ++++++++++++++++++------------ src/ansi-c/c_typecheck_type.cpp | 4 +- src/cpp/cpp_convert_type.cpp | 17 +++--- 4 files changed, 57 insertions(+), 54 deletions(-) diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index 7fe0a391980..809e6f4b461 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -19,13 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "gcc_types.h" -void ansi_c_convert_typet::read(const typet &type) -{ - clear(); - source_location=type.source_location(); - read_rec(type); -} - void ansi_c_convert_typet::read_rec(const typet &type) { if(type.id()==ID_merged_type) diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h index 251882fa417..a0e2ad650f9 100644 --- a/src/ansi-c/ansi_c_convert_type.h +++ b/src/ansi-c/ansi_c_convert_type.h @@ -56,51 +56,68 @@ class ansi_c_convert_typet // qualifiers c_qualifierst c_qualifiers; - virtual void read(const typet &type); virtual void write(typet &type); source_locationt source_location; std::list other; - explicit ansi_c_convert_typet(message_handlert &_message_handler) - : message_handler(_message_handler) - // class members are initialized by calling read() - { - } - - virtual void clear() + ansi_c_convert_typet(message_handlert &_message_handler, const typet &type) + : ansi_c_convert_typet(_message_handler) { - unsigned_cnt=signed_cnt=char_cnt=int_cnt=short_cnt= - long_cnt=double_cnt=float_cnt=c_bool_cnt=proper_bool_cnt=complex_cnt= - int8_cnt=int16_cnt=int32_cnt=int64_cnt= - ptr32_cnt=ptr64_cnt= - gcc_float16_cnt= - gcc_float32_cnt=gcc_float32x_cnt= - gcc_float64_cnt=gcc_float64x_cnt= - gcc_float128_cnt=gcc_float128x_cnt= - gcc_int128_cnt=bv_cnt=floatbv_cnt=fixedbv_cnt=0; - vector_size.make_nil(); - alignment.make_nil(); - bv_width.make_nil(); - fraction_width.make_nil(); - msc_based.make_nil(); - gcc_attribute_mode.make_nil(); - - assigns.clear(); - requires.clear(); - ensures.clear(); - - packed=aligned=constructor=destructor=false; - - other.clear(); - c_storage_spec.clear(); - c_qualifiers.clear(); + source_location = type.source_location(); + read_rec(type); } protected: message_handlert &message_handler; + // Default-initialize all members. To be used by classes deriving from this + // one to make sure additional members can be initialized before invoking + // read_rec. + explicit ansi_c_convert_typet(message_handlert &_message_handler) + : unsigned_cnt(0), + signed_cnt(0), + char_cnt(0), + int_cnt(0), + short_cnt(0), + long_cnt(0), + double_cnt(0), + float_cnt(0), + c_bool_cnt(0), + proper_bool_cnt(0), + complex_cnt(0), + int8_cnt(0), + int16_cnt(0), + int32_cnt(0), + int64_cnt(0), + ptr32_cnt(0), + ptr64_cnt(0), + gcc_float16_cnt(0), + gcc_float32_cnt(0), + gcc_float32x_cnt(0), + gcc_float64_cnt(0), + gcc_float64x_cnt(0), + gcc_float128_cnt(0), + gcc_float128x_cnt(0), + gcc_int128_cnt(0), + bv_cnt(0), + floatbv_cnt(0), + fixedbv_cnt(0), + gcc_attribute_mode(static_cast(get_nil_irep())), + packed(false), + aligned(false), + vector_size(nil_exprt{}), + alignment(nil_exprt{}), + bv_width(nil_exprt{}), + fraction_width(nil_exprt{}), + msc_based(nil_exprt{}), + constructor(false), + destructor(false), + message_handler(_message_handler) + { + } + virtual void read_rec(const typet &type); virtual void build_type_with_subtype(typet &type) const; virtual void set_attributes(typet &type) const; diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index ca17a7746ea..b9c7390b9d5 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -35,9 +35,7 @@ void c_typecheck_baset::typecheck_type(typet &type) { // we first convert, and then check { - ansi_c_convert_typet ansi_c_convert_type(get_message_handler()); - - ansi_c_convert_type.read(type); + ansi_c_convert_typet ansi_c_convert_type{get_message_handler(), type}; ansi_c_convert_type.write(type); } diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index 6ea85f07e8f..1f0454e9d08 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -33,21 +33,16 @@ class cpp_convert_typet : public ansi_c_convert_typet void write(typet &type) override; cpp_convert_typet(message_handlert &message_handler, const typet &type) - : ansi_c_convert_typet(message_handler) + : ansi_c_convert_typet(message_handler), + wchar_t_count(0), + char16_t_count(0), + char32_t_count(0) { - read(type); + source_location = type.source_location(); + read_rec(type); } protected: - void clear() override - { - wchar_t_count = 0; - char16_t_count = 0; - char32_t_count = 0; - - ansi_c_convert_typet::clear(); - } - void read_rec(const typet &type) override; void read_function_type(const typet &type); void read_template(const typet &type);