From 2fc9d2b1394570f0ccaff000bada70fffa5617c6 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 12 Jun 2025 10:08:43 -0700 Subject: [PATCH] introduce SMV enumeration type SMV enumerations behave differently from enumeration_typet; hence, this introduces smv_enumeration_typet, which is subsequently lowered to enumeration_typet. --- regression/smv/enums/enum3.desc | 2 +- src/hw_cbmc_irep_ids.h | 1 + src/smvlang/Makefile | 1 + src/smvlang/expr2smv.cpp | 20 ++-- src/smvlang/parser.y | 4 +- src/smvlang/smv_typecheck.cpp | 175 ++++++++++++++------------------ src/smvlang/smv_types.cpp | 85 ++++++++++++++++ src/smvlang/smv_types.h | 64 ++++++++++++ 8 files changed, 245 insertions(+), 107 deletions(-) create mode 100644 src/smvlang/smv_types.cpp create mode 100644 src/smvlang/smv_types.h diff --git a/regression/smv/enums/enum3.desc b/regression/smv/enums/enum3.desc index 3f7b3c21c..8df6f3fdd 100644 --- a/regression/smv/enums/enum3.desc +++ b/regression/smv/enums/enum3.desc @@ -1,7 +1,7 @@ CORE enum3.smv -^file .* line 7: enum c not a member of \{ a, b \}$ +^file .* line 7: Expected expression of type `\{ a, b \}', but got expression `c', which is of type `\{ c \}'$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 399325f7d..a68ec9fd7 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -18,6 +18,7 @@ IREP_ID_ONE(E) IREP_ID_ONE(G) IREP_ID_ONE(X) IREP_ID_ONE(smv_bitimplies) +IREP_ID_ONE(smv_enumeration) IREP_ID_ONE(smv_extend) IREP_ID_ONE(smv_next) IREP_ID_ONE(smv_iff) diff --git a/src/smvlang/Makefile b/src/smvlang/Makefile index 528ec680a..248dced76 100644 --- a/src/smvlang/Makefile +++ b/src/smvlang/Makefile @@ -2,6 +2,7 @@ SRC = smv_expr.cpp \ smv_language.cpp \ smv_parser.cpp \ smv_typecheck.cpp \ + smv_types.cpp \ expr2smv.cpp \ smv_y.tab.cpp \ lex.yy.cpp \ diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index 2981504db..f1b4dd462 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "smv_expr.h" +#include "smv_types.h" /*******************************************************************\ @@ -337,6 +338,12 @@ expr2smvt::resultt expr2smvt::convert_typecast(const typecast_exprt &expr) return convert_rec(smv_resize_exprt{expr.op(), dest_width, dest_type}); } } + else if( + src_type.id() == ID_smv_enumeration && dest_type.id() == ID_smv_enumeration) + { + // added by SMV typechecker, implicit + return convert_rec(expr.op()); + } else return convert_norep(expr); } @@ -593,10 +600,9 @@ expr2smvt::resultt expr2smvt::convert_constant(const constant_exprt &src) else dest+="FALSE"; } - else if(type.id()==ID_integer || - type.id()==ID_natural || - type.id()==ID_range || - type.id()==ID_enumeration) + else if( + type.id() == ID_integer || type.id() == ID_natural || + type.id() == ID_range || type.id() == ID_smv_enumeration) { dest = id2string(src.get_value()); } @@ -885,15 +891,15 @@ std::string type2smv(const typet &type, const namespacet &ns) code += type2smv(to_array_type(type).element_type(), ns); return code; } - else if(type.id()==ID_enumeration) + else if(type.id() == ID_smv_enumeration) { - const irept::subt &elements=to_enumeration_type(type).elements(); + auto elements = to_smv_enumeration_type(type).elements(); std::string code = "{ "; bool first=true; for(auto &element : elements) { if(first) first=false; else code+=", "; - code += element.id_string(); + code += id2string(element); } code+=" }"; return code; diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 04ee871a0..bc4a0da96 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -522,7 +522,7 @@ module_type_specifier: enum_list : enum_element { - init($$, ID_enumeration); + init($$, ID_smv_enumeration); stack_expr($$).add(ID_elements).get_sub().push_back(irept(stack_expr($1).id())); } | enum_list ',' enum_element @@ -808,7 +808,7 @@ variable_identifier: complex_identifier else if(is_enum) { init($$, ID_constant); - stack_expr($$).type()=typet(ID_enumeration); + stack_expr($$).type()=typet(ID_smv_enumeration); stack_expr($$).set(ID_value, id); } else // not an enum, probably a variable diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 009f5e55d..a493673ef 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr2smv.h" #include "smv_expr.h" #include "smv_range.h" +#include "smv_types.h" #include #include @@ -82,8 +83,6 @@ class smv_typecheckt:public typecheckt void check_type(const typet &); smv_ranget convert_type(const typet &); - static bool - is_contained_in(const enumeration_typet &, const enumeration_typet &); void convert(smv_parse_treet::modulet::itemt &); void typecheck(smv_parse_treet::modulet::itemt &); @@ -141,6 +140,8 @@ class smv_typecheckt:public typecheckt void lower_node(exprt &) const; + void lower(typet &) const; + void lower(exprt &expr) const { expr.visit_post([this](exprt &expr) { lower_node(expr); }); @@ -149,40 +150,6 @@ class smv_typecheckt:public typecheckt /*******************************************************************\ -Function: smv_typecheckt::is_contained_in - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool smv_typecheckt::is_contained_in( - const enumeration_typet &type1, - const enumeration_typet &type2) -{ - // This is quadratic. - for(auto &element1 : type1.elements()) - { - bool found = false; - for(auto &element2 : type2.elements()) - if(element1.id() == element2.id()) - { - found = true; - break; - } - - if(!found) - return false; - } - - return true; -} - -/*******************************************************************\ - Function: smv_typecheckt::convert_ports Inputs: @@ -498,15 +465,15 @@ smv_ranget smv_typecheckt::convert_type(const typet &src) { return smv_ranget::from_type(to_range_type(src)); } - else if(src.id()==ID_enumeration) + else if(src.id() == ID_smv_enumeration) { smv_ranget dest; dest.from=0; - std::size_t number_of_elements= - to_enumeration_type(src).elements().size(); - + std::size_t number_of_elements = + to_smv_enumeration_type(src).elements().size(); + if(number_of_elements==0) dest.to=0; else @@ -556,36 +523,16 @@ typet smv_typecheckt::type_union( } // both enums? - if(type1.id()==ID_enumeration && type2.id()==ID_enumeration) + if(type1.id() == ID_smv_enumeration && type2.id() == ID_smv_enumeration) { - auto &e_type1 = to_enumeration_type(type1); - auto &e_type2 = to_enumeration_type(type2); + auto &e_type1 = to_smv_enumeration_type(type1); + auto &e_type2 = to_smv_enumeration_type(type2); - if(is_contained_in(e_type2, e_type1)) - return type1; - - if(is_contained_in(e_type1, e_type2)) - return type2; - - // make union - std::set enum_set; - - for(auto &e : e_type1.elements()) - enum_set.insert(e.id()); - - for(auto &e : e_type2.elements()) - enum_set.insert(e.id()); - - enumeration_typet union_type; - union_type.elements().reserve(enum_set.size()); - for(auto &e : enum_set) - union_type.elements().push_back(irept{e}); - - return std::move(union_type); + return ::type_union(e_type1, e_type2); } // one of them enum? - if(type1.id() == ID_enumeration || type2.id() == ID_enumeration) + if(type1.id() == ID_smv_enumeration || type2.id() == ID_smv_enumeration) { throw errort().with_location(source_location) << "no type union for types " << to_string(type1) << " and " @@ -868,10 +815,9 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode) mp_integer int_value = string2integer(id2string(value)); expr.type() = range_typet{int_value, int_value}; } - else if(type.id() == ID_enumeration) + else if(type.id() == ID_smv_enumeration) { - auto t = enumeration_typet{}; - t.elements().push_back(irept{value}); + auto t = smv_enumeration_typet{{value}}; expr.type() = std::move(t); } else if(type.id() == ID_bool) @@ -1252,6 +1198,9 @@ Function: smv_typecheckt::lower_node void smv_typecheckt::lower_node(exprt &expr) const { + // lower the type + lower(expr.type()); + if(expr.id() == ID_smv_extend) { auto &smv_extend = to_smv_extend_expr(expr); @@ -1274,6 +1223,27 @@ void smv_typecheckt::lower_node(exprt &expr) const /*******************************************************************\ +Function: smv_typecheckt::lower + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void smv_typecheckt::lower(typet &type) const +{ + // lower the type + if(type.id() == ID_smv_enumeration) + { + type.id(ID_enumeration); + } +} + +/*******************************************************************\ + Function: smv_typecheckt::convert_expr_to Inputs: @@ -1340,35 +1310,40 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type) } } } - else if(type.id() == ID_enumeration) + else if(type.id() == ID_smv_enumeration) { - auto &e_type = to_enumeration_type(type); + auto &e_type = to_smv_enumeration_type(type); - if(expr.id() == ID_constant && expr.type().id() == ID_enumeration) + if(expr.type().id() == ID_smv_enumeration) { - if(is_contained_in(to_enumeration_type(expr.type()), e_type)) - { - // re-type the constant - expr.type() = type; - return; - } - else + // subset? + if(to_smv_enumeration_type(expr.type()).is_subset_of(e_type)) { - throw errort().with_location(expr.find_source_location()) - << "enum " << to_string(expr) << " not a member of " - << to_string(type); - } - } - else if(expr.id() == ID_typecast) - { - // created by type unions - auto &op = to_typecast_expr(expr).op(); - if( - expr.type().id() == ID_enumeration && - op.type().id() == ID_enumeration) - { - convert_expr_to(op, type); - expr = std::move(op); + // yes, it's a subset + if(expr.is_constant()) + { + // re-type the constant + expr.type() = type; + return; + } + else if(expr.id() == ID_typecast) + { + // created by type unions + auto &op = to_typecast_expr(expr).op(); + if( + expr.type().id() == ID_smv_enumeration && + op.type().id() == ID_smv_enumeration) + { + convert_expr_to(op, type); + expr = std::move(op); + return; + } + } + else // anything else + { + expr = typecast_exprt{std::move(expr), type}; + return; + } } } } @@ -1861,9 +1836,6 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) transt{ID_trans, conjunction(trans_invar), conjunction(trans_init), conjunction(trans_trans), module_symbol.type}; - // lowering - lower(module_symbol.value); - module_symbol.pretty_name = strip_smv_prefix(module_symbol.name); symbol_table.add(module_symbol); @@ -1902,12 +1874,21 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) spec_symbol.pretty_name = strip_smv_prefix(spec_symbol.name); // lowering - lower(spec_symbol.value); symbol_table.add(spec_symbol); } } } + + // lowering + for(auto v_it=symbol_table.symbol_module_map.lower_bound(smv_module.name); + v_it!=symbol_table.symbol_module_map.upper_bound(smv_module.name); + v_it++) + { + auto &symbol = symbol_table.get_writeable_ref(v_it->second); + lower(symbol.type); + lower(symbol.value); + } } /*******************************************************************\ diff --git a/src/smvlang/smv_types.cpp b/src/smvlang/smv_types.cpp new file mode 100644 index 000000000..b74f79281 --- /dev/null +++ b/src/smvlang/smv_types.cpp @@ -0,0 +1,85 @@ +/*******************************************************************\ + +Module: SMV Types + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "smv_types.h" + +#include + +smv_enumeration_typet::smv_enumeration_typet( + const std::vector &element_ids) + : typet(ID_smv_enumeration) +{ + auto &sub = elements_sub(); + for(auto &element_id : element_ids) + sub.push_back(irept{element_id}); +} + +std::vector smv_enumeration_typet::elements() const +{ + std::vector result; + + auto &elements_sub = find(ID_elements).get_sub(); + + result.reserve(elements_sub.size()); + + for(auto &e : elements_sub) + result.push_back(e.id()); + + return result; +} + +bool smv_enumeration_typet::is_subset_of( + const smv_enumeration_typet &other) const +{ + // This is quadratic. + for(auto &element1 : elements()) + { + bool found = false; + for(auto &element2 : other.elements()) + if(element1 == element2) + { + found = true; + break; + } + + if(!found) + return false; + } + + return true; +} + +smv_enumeration_typet type_union( + const smv_enumeration_typet &e_type1, + const smv_enumeration_typet &e_type2) +{ + if(e_type2.is_subset_of(e_type1)) + return e_type1; + + if(e_type1.is_subset_of(e_type2)) + return e_type2; + + // make union + std::set enum_set; + + for(auto &e : e_type1.elements()) + enum_set.insert(e); + + for(auto &e : e_type2.elements()) + enum_set.insert(e); + + // turn into vector + std::vector elements; + + elements.reserve(enum_set.size()); + + for(auto &e : enum_set) + elements.push_back(e); + + return smv_enumeration_typet{std::move(elements)}; +} diff --git a/src/smvlang/smv_types.h b/src/smvlang/smv_types.h new file mode 100644 index 000000000..51cd673ca --- /dev/null +++ b/src/smvlang/smv_types.h @@ -0,0 +1,64 @@ +/*******************************************************************\ + +Module: SMV Types + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_SMV_TYPES_H +#define CPROVER_SMV_TYPES_H + +#include + +/// The SMV enumerated type +class smv_enumeration_typet : public typet +{ +public: + smv_enumeration_typet() : typet(ID_smv_enumeration) + { + } + + explicit smv_enumeration_typet(const std::vector &); + + bool is_subset_of(const smv_enumeration_typet &) const; + + // the ordering does not matter; this makes a copy + std::vector elements() const; + + subt &elements_sub() + { + return add(ID_elements).get_sub(); + } +}; + +/// compute the union of the given enumeration types +smv_enumeration_typet +type_union(const smv_enumeration_typet &, const smv_enumeration_typet &); + +/*! \brief Cast a generic typet to a \ref smv_enumeration_typet + * + * This is an unchecked conversion. \a type must be known to be \ref + * smv_enumeration_typet. + * + * \param type Source type + * \return Object of type \ref smv_enumeration_typet + * + * \ingroup gr_std_types +*/ +inline const smv_enumeration_typet &to_smv_enumeration_type(const typet &type) +{ + PRECONDITION(type.id() == ID_smv_enumeration); + return static_cast(type); +} + +/*! \copydoc to_smv_enumeration_type(const typet &) + * \ingroup gr_std_types +*/ +inline smv_enumeration_typet &to_smv_enumeration_type(typet &type) +{ + PRECONDITION(type.id() == ID_smv_enumeration); + return static_cast(type); +} + +#endif // CPROVER_SMV_TYPES_H