From b5c0672bf122f3b98aad6013a5900232924e9592 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 9 Nov 2025 13:05:55 -0800 Subject: [PATCH 1/3] 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 9463ef53dd64b1cc3872c14c91658aaf64ffaff8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 9 Nov 2025 12:57:47 -0800 Subject: [PATCH 2/3] 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; From 45b79da55a26a6568daf914b9fe6488ed5e6c30a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 10 Nov 2025 07:56:51 -0800 Subject: [PATCH 3/3] SMV: move check for duplicate declarations to type checker This moves the check for duplicate declarations and definitions from the SMV parser to the type checker. --- regression/smv/define/define2.desc | 2 +- regression/smv/define/define4.desc | 2 +- src/smvlang/parser.y | 77 ++---------------------------- src/smvlang/smv_typecheck.cpp | 11 ++++- 4 files changed, 15 insertions(+), 77 deletions(-) diff --git a/regression/smv/define/define2.desc b/regression/smv/define/define2.desc index 50db76004..4fa0eea60 100644 --- a/regression/smv/define/define2.desc +++ b/regression/smv/define/define2.desc @@ -2,7 +2,7 @@ CORE define2.smv ^file .* line 6: variable `x' already declared.*$ -^EXIT=1$ +^EXIT=2$ ^SIGNAL=0$ -- -- diff --git a/regression/smv/define/define4.desc b/regression/smv/define/define4.desc index fbc9008ff..99a900e11 100644 --- a/regression/smv/define/define4.desc +++ b/regression/smv/define/define4.desc @@ -2,7 +2,7 @@ CORE define4.smv ^file .* line 6: variable `x' already defined.*$ -^EXIT=1$ +^EXIT=2$ ^SIGNAL=0$ -- -- diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 926055882..a282a8121 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -704,27 +704,7 @@ var_decl : variable_identifier ':' type_specifier ';' { const irep_idt &identifier=stack_expr($1).get(ID_identifier); smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier]; - - switch(var.var_class) - { - case smv_parse_treet::mc_vart::UNKNOWN: - var.type=stack_type($3); - var.var_class=smv_parse_treet::mc_vart::DECLARED; - break; - - case smv_parse_treet::mc_vart::DEFINED: - case smv_parse_treet::mc_vart::DECLARED: - break; - - case smv_parse_treet::mc_vart::ARGUMENT: - yyerror("variable `"+id2string(identifier)+"' already declared as argument"); - YYERROR; - break; - - default: - DATA_INVARIANT(false, "unexpected variable class"); - } - + (void)var; PARSER.module->add_var(stack_expr($1), stack_type($3)); } ; @@ -748,32 +728,7 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';' { const irep_idt &identifier=stack_expr($1).get(ID_identifier); smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier]; - - switch(var.var_class) - { - case smv_parse_treet::mc_vart::UNKNOWN: - var.type.make_nil(); - var.var_class=smv_parse_treet::mc_vart::DEFINED; - break; - - case smv_parse_treet::mc_vart::DECLARED: - var.var_class=smv_parse_treet::mc_vart::DEFINED; - break; - - case smv_parse_treet::mc_vart::DEFINED: - yyerror("variable `"+id2string(identifier)+"' already defined"); - YYERROR; - break; - - case smv_parse_treet::mc_vart::ARGUMENT: - yyerror("variable `"+id2string(identifier)+"' already declared as argument"); - YYERROR; - break; - - default: - DATA_INVARIANT(false, "unexpected variable class"); - } - + (void)var; PARSER.module->add_assign_current(std::move(stack_expr($1)), std::move(stack_expr($3))); } ; @@ -794,33 +749,7 @@ define : assignment_var BECOMES_Token formula ';' { const irep_idt &identifier=stack_expr($1).get(ID_identifier); smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier]; - - switch(var.var_class) - { - case smv_parse_treet::mc_vart::UNKNOWN: - var.type.make_nil(); - var.var_class=smv_parse_treet::mc_vart::DEFINED; - break; - - case smv_parse_treet::mc_vart::DECLARED: - yyerror("variable `"+id2string(identifier)+"' already declared"); - YYERROR; - break; - - case smv_parse_treet::mc_vart::DEFINED: - yyerror("variable `"+id2string(identifier)+"' already defined"); - YYERROR; - break; - - case smv_parse_treet::mc_vart::ARGUMENT: - yyerror("variable `"+id2string(identifier)+"' already declared as argument"); - YYERROR; - break; - - default: - DATA_INVARIANT(false, "unexpected variable class"); - } - + (void)var; PARSER.module->add_define(std::move(stack_expr($1)), std::move(stack_expr($3))); } ; diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index a47c02311..6654c92fa 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -2184,6 +2184,15 @@ void smv_typecheckt::create_var_symbols( to_smv_identifier_expr(to_equal_expr(item.expr).lhs()); irep_idt base_name = identifier_expr.identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); + + auto symbol_ptr = symbol_table.lookup(identifier); + if(symbol_ptr != nullptr) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "variable `" << base_name << "' already declared, at " + << symbol_ptr->location; + } + typet type; type.make_nil(); @@ -2264,7 +2273,7 @@ void smv_typecheckt::collect_define(const equal_exprt &expr) if(!result.second) { throw errort().with_location(expr.find_source_location()) - << "symbol `" << identifier << "' defined twice"; + << "variable `" << symbol.display_name() << "' already defined"; } }