From 422ceabc39921c0c12891fe3c08d263da0abf133 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 23 Nov 2025 12:28:12 -0800 Subject: [PATCH] SMV: extract code for duplicate identifiers This extracts the code that checks for re-use of parameter/define/enum identifiers into a separate method. --- regression/smv/define/define2.desc | 2 +- regression/smv/define/define3.desc | 2 +- regression/smv/enums/name_collision1.desc | 6 +- regression/smv/enums/name_collision2.desc | 2 +- regression/smv/enums/name_collision3.desc | 6 +- regression/smv/var/already_declared1.desc | 2 +- regression/smv/var/already_declared2.desc | 2 +- regression/smv/var/already_declared3.desc | 2 +- src/smvlang/smv_typecheck.cpp | 167 ++++++++++++++++------ 9 files changed, 135 insertions(+), 56 deletions(-) diff --git a/regression/smv/define/define2.desc b/regression/smv/define/define2.desc index 4fa0eea60..dfb4457cf 100644 --- a/regression/smv/define/define2.desc +++ b/regression/smv/define/define2.desc @@ -1,7 +1,7 @@ CORE define2.smv -^file .* line 6: variable `x' already declared.*$ +^file .* line 6: identifier x already used as variable$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/smv/define/define3.desc b/regression/smv/define/define3.desc index a69176ac9..79214d15d 100644 --- a/regression/smv/define/define3.desc +++ b/regression/smv/define/define3.desc @@ -1,7 +1,7 @@ CORE define3.smv -^file .* line 6: variable x already declared, at file .* line 3$ +^file .* line 6: identifier x already used as define$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/smv/enums/name_collision1.desc b/regression/smv/enums/name_collision1.desc index fa029e06d..4537a9f2f 100644 --- a/regression/smv/enums/name_collision1.desc +++ b/regression/smv/enums/name_collision1.desc @@ -1,9 +1,9 @@ -KNOWNBUG +CORE name_collision1.smv -^EXIT=0$ +^file .* line 6: identifier red already used as enum$ +^EXIT=2$ ^SIGNAL=0$ -- ^warning: ignoring -- -This crashes. diff --git a/regression/smv/enums/name_collision2.desc b/regression/smv/enums/name_collision2.desc index 7bc17f348..7a2eb1393 100644 --- a/regression/smv/enums/name_collision2.desc +++ b/regression/smv/enums/name_collision2.desc @@ -1,7 +1,7 @@ CORE name_collision2.smv -^file .* line 8: enum red already declared, at file .* line 3$ +^file .* line 8: identifier red already used as variable$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/smv/enums/name_collision3.desc b/regression/smv/enums/name_collision3.desc index 91c3ea2f6..8ae3e5f34 100644 --- a/regression/smv/enums/name_collision3.desc +++ b/regression/smv/enums/name_collision3.desc @@ -1,9 +1,9 @@ -KNOWNBUG +CORE name_collision3.smv -^EXIT=0$ +^file .* line 8: identifier red already used as enum$ +^EXIT=2$ ^SIGNAL=0$ -- ^warning: ignoring -- -This crashes. diff --git a/regression/smv/var/already_declared1.desc b/regression/smv/var/already_declared1.desc index 0910f0f55..8d5b4a1c4 100644 --- a/regression/smv/var/already_declared1.desc +++ b/regression/smv/var/already_declared1.desc @@ -1,7 +1,7 @@ CORE already_declared1.smv -^file .* line 6: variable x already declared, at file .* line 3$ +^file .* line 6: identifier x already used as variable$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/smv/var/already_declared2.desc b/regression/smv/var/already_declared2.desc index cfacd32a3..51fdcee66 100644 --- a/regression/smv/var/already_declared2.desc +++ b/regression/smv/var/already_declared2.desc @@ -1,7 +1,7 @@ CORE already_declared2.smv -^file .* line 6: variable x already declared, at file .* line 3$ +^file .* line 6: identifier x already used as define$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/regression/smv/var/already_declared3.desc b/regression/smv/var/already_declared3.desc index 22e8c3575..33afc32cb 100644 --- a/regression/smv/var/already_declared3.desc +++ b/regression/smv/var/already_declared3.desc @@ -1,7 +1,7 @@ CORE already_declared3.smv -^file .* line 8: variable x already declared, at file .* line 5$ +^file .* line 8: identifier x already used as variable$ ^EXIT=2$ ^SIGNAL=0$ -- diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 95f7edd62..1aaa0b989 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -60,9 +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 &, - const std::list &module_parameters); + void create_var_symbols(const smv_parse_treet::modulet::element_listt &); void collect_define(const equal_exprt &); void convert_defines(exprt::operandst &invar); @@ -88,6 +86,8 @@ class smv_typecheckt:public typecheckt void check_type(typet &); smv_ranget convert_type(const typet &); + void variable_checks(const smv_parse_treet::modulet &); + void convert(smv_parse_treet::modulet::elementt &); void typecheck(smv_parse_treet::modulet::elementt &); void typecheck_expr_rec(exprt &, modet); @@ -2126,7 +2126,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet::elementt &element) /*******************************************************************\ -Function: smv_typecheckt::create_var_symbols +Function: smv_typecheckt::variable_checks Inputs: @@ -2136,42 +2136,141 @@ Function: smv_typecheckt::create_var_symbols \*******************************************************************/ -void smv_typecheckt::create_var_symbols( - const smv_parse_treet::modulet::element_listt &elements, - const std::list &module_parameters) +void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module) { - const irep_idt mode = "SMV"; + std::unordered_set enums, defines, vars, parameters; - // to catch variables that have the same name as enums - std::unordered_set enums; - - // to catch re-use of parameter identifiers - std::unordered_set parameters; - - for(const auto ¶meter : module_parameters) + for(const auto ¶meter : module.parameters) parameters.insert(parameter); - for(const auto &element : elements) + for(const auto &element : module.elements) { if(element.is_var() || element.is_ivar()) { - irep_idt base_name = to_smv_identifier_expr(element.expr).identifier(); - irep_idt identifier = module + "::var::" + id2string(base_name); + const auto &identifier_expr = to_smv_identifier_expr(element.expr); + irep_idt base_name = identifier_expr.identifier(); // already used as enum? if(enums.find(base_name) != enums.end()) { - throw errort{}.with_location(element.expr.source_location()) + throw errort{}.with_location(identifier_expr.source_location()) << "identifier " << base_name << " already used as enum"; } // already used as a parameter? if(parameters.find(base_name) != parameters.end()) { - throw errort{}.with_location(element.expr.source_location()) + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as a parameter"; + } + + // already used as variable? + if(vars.find(base_name) != vars.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as variable"; + } + + // already used as define? + if(defines.find(base_name) != defines.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as define"; + } + + vars.insert(base_name); + } + else if(element.is_define()) + { + const auto &identifier_expr = + to_smv_identifier_expr(to_equal_expr(element.expr).lhs()); + irep_idt base_name = identifier_expr.identifier(); + + // already used as enum? + if(enums.find(base_name) != enums.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as enum"; + } + + // already used as a parameter? + if(parameters.find(base_name) != parameters.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) << "identifier " << base_name << " already used as a parameter"; } + // already used as variable? + if(vars.find(base_name) != vars.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as variable"; + } + + // already used as define? + if(defines.find(base_name) != defines.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as define"; + } + + defines.insert(base_name); + } + else if(element.is_enum()) + { + const auto &identifier_expr = to_smv_identifier_expr(element.expr); + irep_idt base_name = identifier_expr.identifier(); + + // already used as a parameter? + if(parameters.find(base_name) != parameters.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as a parameter"; + } + + // already used as variable? + if(vars.find(base_name) != vars.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as variable"; + } + + // already used as define? + if(defines.find(base_name) != defines.end()) + { + throw errort{}.with_location(identifier_expr.source_location()) + << "identifier " << base_name << " already used as define"; + } + + enums.insert(base_name); + } + } +} + +/*******************************************************************\ + +Function: smv_typecheckt::create_var_symbols + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void smv_typecheckt::create_var_symbols( + const smv_parse_treet::modulet::element_listt &elements) +{ + const irep_idt mode = "SMV"; + + for(const auto &element : elements) + { + if(element.is_var() || element.is_ivar()) + { + irep_idt base_name = to_smv_identifier_expr(element.expr).identifier(); + irep_idt identifier = module + "::var::" + id2string(base_name); + auto symbol_ptr = symbol_table.lookup(identifier); if(symbol_ptr != nullptr) { @@ -2213,20 +2312,6 @@ void smv_typecheckt::create_var_symbols( irep_idt base_name = identifier_expr.identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); - // already used as enum? - if(enums.find(base_name) != enums.end()) - { - throw errort{}.with_location(identifier_expr.source_location()) - << "identifier " << base_name << " already used as enum"; - } - - // already used as a parameter? - if(parameters.find(base_name) != parameters.end()) - { - throw errort{}.with_location(identifier_expr.source_location()) - << "identifier " << base_name << " already used as a parameter"; - } - auto symbol_ptr = symbol_table.lookup(identifier); if(symbol_ptr != nullptr) { @@ -2261,13 +2346,6 @@ void smv_typecheckt::create_var_symbols( irep_idt base_name = to_smv_identifier_expr(element.expr).identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); - // already used as a parameter? - if(parameters.find(base_name) != parameters.end()) - { - throw errort{}.with_location(element.expr.source_location()) - << "identifier " << base_name << " already used as a parameter"; - } - auto symbol_ptr = symbol_table.lookup(identifier); if(symbol_ptr != nullptr) { @@ -2275,8 +2353,6 @@ void smv_typecheckt::create_var_symbols( << "enum " << base_name << " already declared, at " << symbol_ptr->location; } - - enums.insert(base_name); } } } @@ -2421,8 +2497,11 @@ 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); + // variables/defines first, can be used before their declaration - create_var_symbols(smv_module.elements, smv_module.parameters); + create_var_symbols(smv_module.elements); // transition relation