From b5c0672bf122f3b98aad6013a5900232924e9592 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 9 Nov 2025 13:05:55 -0800 Subject: [PATCH 1/2] SMV: submodule type This introduces a class to document the existing SMV submodule type. --- src/hw_cbmc_irep_ids.h | 1 + src/smvlang/expr2smv.cpp | 4 ++-- src/smvlang/parser.y | 9 ++++---- src/smvlang/smv_language.cpp | 10 +++++---- src/smvlang/smv_typecheck.cpp | 4 ++-- src/smvlang/smv_types.h | 42 +++++++++++++++++++++++++++++++++++ 6 files changed, 58 insertions(+), 12 deletions(-) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index f7b99ef11..cdfce027b 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -37,6 +37,7 @@ IREP_ID_ONE(smv_setin) IREP_ID_ONE(smv_setnotin) IREP_ID_ONE(smv_signed_cast) IREP_ID_ONE(smv_sizeof) +IREP_ID_ONE(smv_submodule) IREP_ID_ONE(smv_swconst) IREP_ID_ONE(smv_union) IREP_ID_ONE(smv_unsigned_cast) diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp index f9791f342..4039d552a 100644 --- a/src/smvlang/expr2smv.cpp +++ b/src/smvlang/expr2smv.cpp @@ -1058,9 +1058,9 @@ std::string type2smv(const typet &type, const namespacet &ns) { return "set"; } - else if(type.id()=="submodule") + else if(type.id() == ID_smv_submodule) { - auto code = type.get_string(ID_identifier); + auto code = id2string(to_smv_submodule_type(type).identifier()); const exprt &e=(exprt &)type; if(e.has_operands()) { diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index b79e5cf00..926055882 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -5,6 +5,7 @@ #include "smv_expr.h" #include "smv_parser.h" #include "smv_typecheck.h" +#include "smv_types.h" #include #include @@ -657,14 +658,14 @@ simple_type_specifier: module_type_specifier: module_name { - init($$, "submodule"); - stack_expr($$).set(ID_identifier, + init($$, ID_smv_submodule); + to_smv_submodule_type(stack_type($$)).identifier( smv_module_symbol(stack_expr($1).id_string())); } | module_name '(' parameter_list ')' { - init($$, "submodule"); - stack_expr($$).set(ID_identifier, + init($$, ID_smv_submodule); + to_smv_submodule_type(stack_type($$)).identifier( smv_module_symbol(stack_expr($1).id_string())); stack_expr($$).operands().swap(stack_expr($3).operands()); } diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp index 30ed6e66b..8a2f6b692 100644 --- a/src/smvlang/smv_language.cpp +++ b/src/smvlang/smv_language.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr2smv.h" #include "smv_parser.h" #include "smv_typecheck.h" +#include "smv_types.h" /*******************************************************************\ @@ -69,8 +70,9 @@ void smv_languaget::dependencies( for(smv_parse_treet::mc_varst::const_iterator it=smv_module.vars.begin(); it!=smv_module.vars.end(); it++) - if(it->second.type.id()=="submodule") - module_set.insert(it->second.type.get_string("identifier")); + if(it->second.type.id() == ID_smv_submodule) + module_set.insert( + id2string(to_smv_submodule_type(it->second.type).identifier())); } /*******************************************************************\ @@ -145,7 +147,7 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &) for(smv_parse_treet::mc_varst::const_iterator it=module.vars.begin(); it!=module.vars.end(); it++) - if(it->second.type.id()!="submodule") + if(it->second.type.id() != ID_smv_submodule) { symbol_tablet symbol_table; namespacet ns{symbol_table}; @@ -160,7 +162,7 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &) for(smv_parse_treet::mc_varst::const_iterator it=module.vars.begin(); it!=module.vars.end(); it++) - if(it->second.type.id()=="submodule") + if(it->second.type.id() == ID_smv_submodule) { symbol_tablet symbol_table; namespacet ns(symbol_table); diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 625edab91..a47c02311 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -196,7 +196,7 @@ void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module) { for(auto &item : smv_module.items) { - if(item.is_var() && item.expr.type().id() == "submodule") + if(item.is_var() && item.expr.type().id() == ID_smv_submodule) { exprt &inst = static_cast(static_cast(item.expr.type())); @@ -2167,7 +2167,7 @@ void smv_typecheckt::create_var_symbols( else symbol.pretty_name = strip_smv_prefix(symbol.name); - if(symbol.type.id() == "submodule") + if(symbol.type.id() == ID_smv_submodule) symbol.is_input = false; else symbol.is_input = true; diff --git a/src/smvlang/smv_types.h b/src/smvlang/smv_types.h index b32330958..594d68e24 100644 --- a/src/smvlang/smv_types.h +++ b/src/smvlang/smv_types.h @@ -71,4 +71,46 @@ inline smv_enumeration_typet &to_smv_enumeration_type(typet &type) return static_cast(type); } +/// The type used for VAR declarations that are in fact module instantiations +class smv_submodule_typet : public typet +{ +public: + explicit smv_submodule_typet(irep_idt _identifier) : typet{ID_smv_submodule} + { + identifier(_identifier); + } + + irep_idt identifier() const + { + return get(ID_identifier); + } + + void identifier(irep_idt _identifier) + { + set(ID_identifier, _identifier); + } +}; + +/*! \brief Cast a generic typet to a \ref smv_submodule_typet + * + * This is an unchecked conversion. \a type must be known to be \ref + * smv_submodule_typet. + * + * \param type Source type + * \return Object of type \ref smv_submodule_typet + * + * \ingroup gr_std_types +*/ +inline const smv_submodule_typet &to_smv_submodule_type(const typet &type) +{ + PRECONDITION(type.id() == ID_smv_submodule); + return static_cast(type); +} + +inline smv_submodule_typet &to_smv_submodule_type(typet &type) +{ + PRECONDITION(type.id() == ID_smv_submodule); + return static_cast(type); +} + #endif // CPROVER_SMV_TYPES_H From 08ae32e3dd357d074e42e89b09d20d7d75f76b7f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 9 Nov 2025 12:57:47 -0800 Subject: [PATCH 2/2] SMV: avoid vars member in SMV parse tree This replaces the use of the vars member in the SMV parse tree by use of the items list. --- src/smvlang/smv_language.cpp | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp index 8a2f6b692..1dc850a32 100644 --- a/src/smvlang/smv_language.cpp +++ b/src/smvlang/smv_language.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "expr2smv.h" +#include "smv_expr.h" #include "smv_parser.h" #include "smv_typecheck.h" #include "smv_types.h" @@ -68,11 +69,10 @@ void smv_languaget::dependencies( const smv_parse_treet::modulet &smv_module=m_it->second; - for(smv_parse_treet::mc_varst::const_iterator it=smv_module.vars.begin(); - it!=smv_module.vars.end(); it++) - if(it->second.type.id() == ID_smv_submodule) + for(auto &item : smv_module.items) + if(item.is_var() && item.expr.type().id() == ID_smv_submodule) module_set.insert( - id2string(to_smv_submodule_type(it->second.type).identifier())); + id2string(to_smv_submodule_type(item.expr.type()).identifier())); } /*******************************************************************\ @@ -145,29 +145,28 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &) out << " VARIABLES:" << std::endl; - for(smv_parse_treet::mc_varst::const_iterator it=module.vars.begin(); - it!=module.vars.end(); it++) - if(it->second.type.id() != ID_smv_submodule) + for(auto &item : module.items) + if(item.is_var() && item.expr.type().id() != ID_smv_submodule) { symbol_tablet symbol_table; namespacet ns{symbol_table}; - auto msg = type2smv(it->second.type, ns); - out << " " << it->first << ": " << msg << ";\n"; + auto identifier = to_smv_identifier_expr(item.expr).identifier(); + auto msg = type2smv(item.expr.type(), ns); + out << " " << identifier << ": " << msg << ";\n"; } out << std::endl; out << " SUBMODULES:" << std::endl; - for(smv_parse_treet::mc_varst::const_iterator - it=module.vars.begin(); - it!=module.vars.end(); it++) - if(it->second.type.id() == ID_smv_submodule) + for(auto &item : module.items) + if(item.is_var() && item.expr.type().id() == ID_smv_submodule) { symbol_tablet symbol_table; namespacet ns(symbol_table); - auto msg = type2smv(it->second.type, ns); - out << " " << it->first << ": " << msg << ";\n"; + auto identifier = to_smv_identifier_expr(item.expr).identifier(); + auto msg = type2smv(item.expr.type(), ns); + out << " " << identifier << ": " << msg << ";\n"; } out << std::endl;