From ad081dc343dcf44e941f7accab2e0430586c69cd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 19 Nov 2025 15:26:08 -0800 Subject: [PATCH] SMV: flatten hierarchy on parse tree SMV module flattening is now implemented as an operation on SMV parse trees, as opposed to an operation on a symbol table post type checking. --- regression/smv/modules/parameters2.desc | 3 +- .../smv/modules/use_before_declaration1.desc | 7 + .../smv/modules/use_before_declaration1.smv | 10 + src/smvlang/smv_parse_tree.h | 2 +- src/smvlang/smv_typecheck.cpp | 229 +++++------------- 5 files changed, 74 insertions(+), 177 deletions(-) create mode 100644 regression/smv/modules/use_before_declaration1.desc create mode 100644 regression/smv/modules/use_before_declaration1.smv diff --git a/regression/smv/modules/parameters2.desc b/regression/smv/modules/parameters2.desc index 18158a51a..2288ee0fa 100644 --- a/regression/smv/modules/parameters2.desc +++ b/regression/smv/modules/parameters2.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE parameters2.smv ^EXIT=10$ @@ -6,4 +6,3 @@ parameters2.smv -- ^warning: ignoring -- -This yields a type-checking error. diff --git a/regression/smv/modules/use_before_declaration1.desc b/regression/smv/modules/use_before_declaration1.desc new file mode 100644 index 000000000..4355eca2a --- /dev/null +++ b/regression/smv/modules/use_before_declaration1.desc @@ -0,0 +1,7 @@ +CORE +use_before_declaration1.smv +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/smv/modules/use_before_declaration1.smv b/regression/smv/modules/use_before_declaration1.smv new file mode 100644 index 000000000..a0d3b443b --- /dev/null +++ b/regression/smv/modules/use_before_declaration1.smv @@ -0,0 +1,10 @@ +MODULE main + +-- you can use modules before they are declared +SPEC sub.something = 123 + +VAR sub : my-module; + +MODULE my-module + +DEFINE something := 123; diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h index 72b088128..80500cb9b 100644 --- a/src/smvlang/smv_parse_tree.h +++ b/src/smvlang/smv_parse_tree.h @@ -29,7 +29,7 @@ class smv_parse_treet struct modulet { irep_idt name, base_name; - std::list parameters; + std::vector parameters; struct elementt { diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 12606f117..4a3f9647d 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -60,6 +60,7 @@ class smv_typecheckt:public typecheckt } modet; void convert(smv_parse_treet::modulet &); + void create_var_symbols(const smv_parse_treet::modulet::element_listt &); void collect_define(const equal_exprt &); @@ -104,7 +105,7 @@ class smv_typecheckt:public typecheckt smv_parse_treet::modulet &, const irep_idt &identifier, const irep_idt &instance, - const exprt::operandst &operands, + const exprt::operandst &arguments, const source_locationt &); typet @@ -112,8 +113,6 @@ class smv_typecheckt:public typecheckt typedef std::map rename_mapt; - void instantiate_rename(exprt &, const rename_mapt &rename_map); - void convert_ports(smv_parse_treet::modulet &, typet &dest); // for defines @@ -196,8 +195,14 @@ Function: smv_typecheckt::flatten_hierarchy void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module) { - for(auto &element : smv_module.elements) + // Not using ranged for since we will append to the list we are + // iterating over! This avoids recursion. + for(auto element_it = smv_module.elements.begin(); + element_it != smv_module.elements.end(); + ++element_it) { + auto &element = *element_it; + if(element.is_var() && element.expr.type().id() == ID_smv_submodule) { exprt &inst = @@ -235,195 +240,66 @@ void smv_typecheckt::instantiate( smv_parse_treet::modulet &smv_module, const irep_idt &identifier, const irep_idt &instance, - const exprt::operandst &operands, + const exprt::operandst &arguments, const source_locationt &location) { - symbol_table_baset::symbolst::const_iterator s_it = - symbol_table.symbols.find(identifier); + // Find the module + auto module_it = smv_parse_tree.module_map.find(identifier); - if(s_it==symbol_table.symbols.end()) + if(module_it == smv_parse_tree.module_map.end()) { throw errort().with_location(location) << "submodule `" << identifier << "' not found"; } - if(s_it->second.type.id()!=ID_module) - { - throw errort().with_location(location) - << "submodule `" << identifier << "' not a module"; - } - - const irept::subt &ports=s_it->second.type.find(ID_ports).get_sub(); - - // do the arguments/ports + const auto &instantiated_module = *module_it->second; + const auto ¶meters = instantiated_module.parameters; - if(ports.size()!=operands.size()) + // map the arguments to parameters + if(parameters.size() != arguments.size()) { throw errort().with_location(location) << "submodule `" << identifier << "' has wrong number of arguments"; } - std::set port_identifiers; - rename_mapt rename_map; - - for(std::size_t i = 0; i < ports.size(); i++) - { - const irep_idt &identifier=ports[i].get(ID_identifier); - rename_map.insert(std::pair(identifier, operands[i])); - port_identifiers.insert(identifier); - } - - // do the variables - - std::string new_prefix= - id2string(smv_module.name)+"::var::"+id2string(instance)+"."; - - std::set var_identifiers; - - for(auto v_it=symbol_table.symbol_module_map.lower_bound(identifier); - v_it!=symbol_table.symbol_module_map.upper_bound(identifier); - v_it++) - { - symbol_table_baset::symbolst::const_iterator s_it2 = - symbol_table.symbols.find(v_it->second); - - if(s_it2==symbol_table.symbols.end()) - { - throw errort() << "symbol `" << v_it->second << "' not found"; - } - - if(port_identifiers.find(s_it2->first) != port_identifiers.end()) - { - } - else if(s_it2->second.type.id() == ID_module) - { - } - else - { - symbolt symbol(s_it2->second); - - symbol.name=new_prefix+id2string(symbol.base_name); - symbol.module=smv_module.name; - - if(smv_module.name == "smv::main") - { - symbol.pretty_name = - id2string(instance) + '.' + id2string(symbol.base_name); - } - else - { - symbol.pretty_name = strip_smv_prefix(symbol.name); - } - - rename_map.insert( - std::pair(s_it2->first, symbol.symbol_expr())); - - var_identifiers.insert(symbol.name); - - symbol_table.add(symbol); - } - } - - // fix values (macros) - - for(const auto &v_id : var_identifiers) - { - auto s_it2 = symbol_table.get_writeable(v_id); - - if(s_it2==nullptr) - { - throw errort() << "symbol `" << v_id << "' not found"; - } - - symbolt &symbol=*s_it2; - - if(!symbol.value.is_nil()) - { - instantiate_rename(symbol.value, rename_map); - typecheck(symbol.value, OTHER); - convert_expr_to(symbol.value, symbol.type); - } - } - - // get the transition system - - const transt &trans=to_trans_expr(s_it->second.value); + rename_mapt parameter_map; - std::string old_prefix=id2string(s_it->first)+"::var::"; - - // do the transition system - - if(!trans.invar().is_true()) - { - exprt tmp(trans.invar()); - instantiate_rename(tmp, rename_map); - smv_module.add_invar(tmp); - } - - if(!trans.init().is_true()) - { - exprt tmp(trans.init()); - instantiate_rename(tmp, rename_map); - smv_module.add_init(tmp); - } - - if(!trans.trans().is_true()) + for(std::size_t i = 0; i < parameters.size(); i++) { - exprt tmp(trans.trans()); - instantiate_rename(tmp, rename_map); - smv_module.add_trans(tmp); + parameter_map.emplace(parameters[i], arguments[i]); } -} - -/*******************************************************************\ - -Function: smv_typecheckt::instantiate_rename - - Inputs: - - Outputs: - - Purpose: + const std::string prefix = id2string(instance) + '.'; -\*******************************************************************/ - -void smv_typecheckt::instantiate_rename( - exprt &expr, - const rename_mapt &rename_map) -{ - for(auto &op : expr.operands()) - instantiate_rename(op, rename_map); - - if(expr.id()==ID_symbol || expr.id()==ID_next_symbol) + // copy the parse tree elements + for(auto &src_element : instantiated_module.elements) { - const irep_idt &old_identifier=expr.get(ID_identifier); - bool next=expr.id()==ID_next_symbol; - - rename_mapt::const_iterator it= - rename_map.find(old_identifier); + auto copy = src_element; - if(it!=rename_map.end()) - { - expr=it->second; - - if(next) + // replace the parameter identifiers, + // and add the prefix to non-parameter identifiers + copy.expr.visit_post( + [¶meter_map, &prefix](exprt &expr) { - if(expr.id()==ID_symbol) - { - expr=it->second; - expr.id(ID_next_symbol); - } - else + if(expr.id() == ID_smv_identifier) { - throw errort().with_location(expr.find_source_location()) - << "expected symbol expression here, but got " - << to_string(it->second); + auto identifier = to_smv_identifier_expr(expr).identifier(); + auto parameter_it = parameter_map.find(identifier); + if(parameter_it != parameter_map.end()) + { + expr = parameter_it->second; + } + else + { + // add the prefix + to_smv_identifier_expr(expr).identifier( + prefix + id2string(identifier)); + } } - } - else - expr=it->second; - } + }); + + // add to main parse tree + smv_module.elements.push_back(copy); } } @@ -2497,10 +2373,10 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) define_map.clear(); - // check for re-use of variables/defines/parameter identifiers - variable_checks(smv_module); + // expand the module hierarchy + flatten_hierarchy(smv_module); - // variables/defines first, can be used before their declaration + // Now do variables/defines, which can be used before their declaration create_var_symbols(smv_module.elements); // transition relation @@ -2524,8 +2400,6 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) if(!element.is_var() && !element.is_ivar()) convert(element); - flatten_hierarchy(smv_module); - // we first need to collect all the defines for(auto &element : smv_module.elements) @@ -2631,6 +2505,13 @@ Function: smv_typecheckt::typecheck void smv_typecheckt::typecheck() { + if(module != "smv::main") + return; + + // check all modules for duplicate identifiers + for(auto &module : smv_parse_tree.module_list) + variable_checks(module); + auto it = smv_parse_tree.module_map.find(module); if(it == smv_parse_tree.module_map.end())