From 61c576a469f90e53b9e86103a785a75890be84cf Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 28 Jul 2025 13:57:42 -0700 Subject: [PATCH] SMV: move checks for duplicate declarations into type checker This moves the check whether an identifier for a variable has already been declared from the parser to the type checker. --- regression/smv/define/define3.desc | 4 ++-- regression/smv/var/already_declared1.desc | 8 ++++++++ regression/smv/var/already_declared1.smv | 6 ++++++ regression/smv/var/already_declared2.desc | 8 ++++++++ regression/smv/var/already_declared2.smv | 6 ++++++ regression/smv/var/already_declared3.desc | 8 ++++++++ regression/smv/var/already_declared3.smv | 8 ++++++++ regression/smv/var/already_declared4.desc | 8 ++++++++ regression/smv/var/already_declared4.smv | 8 ++++++++ regression/smv/var/already_declared5.desc | 8 ++++++++ regression/smv/var/already_declared5.smv | 6 ++++++ src/smvlang/parser.y | 6 ------ src/smvlang/smv_typecheck.cpp | 14 ++++++++++++-- 13 files changed, 88 insertions(+), 10 deletions(-) create mode 100644 regression/smv/var/already_declared1.desc create mode 100644 regression/smv/var/already_declared1.smv create mode 100644 regression/smv/var/already_declared2.desc create mode 100644 regression/smv/var/already_declared2.smv create mode 100644 regression/smv/var/already_declared3.desc create mode 100644 regression/smv/var/already_declared3.smv create mode 100644 regression/smv/var/already_declared4.desc create mode 100644 regression/smv/var/already_declared4.smv create mode 100644 regression/smv/var/already_declared5.desc create mode 100644 regression/smv/var/already_declared5.smv diff --git a/regression/smv/define/define3.desc b/regression/smv/define/define3.desc index 259caa10a..a69176ac9 100644 --- a/regression/smv/define/define3.desc +++ b/regression/smv/define/define3.desc @@ -1,8 +1,8 @@ CORE define3.smv -^file .* line 6: variable `x' already defined.*$ -^EXIT=1$ +^file .* line 6: variable x already declared, at file .* line 3$ +^EXIT=2$ ^SIGNAL=0$ -- -- diff --git a/regression/smv/var/already_declared1.desc b/regression/smv/var/already_declared1.desc new file mode 100644 index 000000000..0910f0f55 --- /dev/null +++ b/regression/smv/var/already_declared1.desc @@ -0,0 +1,8 @@ +CORE +already_declared1.smv + +^file .* line 6: variable x already declared, at file .* line 3$ +^EXIT=2$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/var/already_declared1.smv b/regression/smv/var/already_declared1.smv new file mode 100644 index 000000000..f7bf68cc5 --- /dev/null +++ b/regression/smv/var/already_declared1.smv @@ -0,0 +1,6 @@ +MODULE main + +VAR x : 1..10; + +-- x again +VAR x : 1..10; diff --git a/regression/smv/var/already_declared2.desc b/regression/smv/var/already_declared2.desc new file mode 100644 index 000000000..cfacd32a3 --- /dev/null +++ b/regression/smv/var/already_declared2.desc @@ -0,0 +1,8 @@ +CORE +already_declared2.smv + +^file .* line 6: variable x already declared, at file .* line 3$ +^EXIT=2$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/var/already_declared2.smv b/regression/smv/var/already_declared2.smv new file mode 100644 index 000000000..43041df77 --- /dev/null +++ b/regression/smv/var/already_declared2.smv @@ -0,0 +1,6 @@ +MODULE main + +DEFINE x := 1; + +-- x again +VAR x : 1..10; diff --git a/regression/smv/var/already_declared3.desc b/regression/smv/var/already_declared3.desc new file mode 100644 index 000000000..22e8c3575 --- /dev/null +++ b/regression/smv/var/already_declared3.desc @@ -0,0 +1,8 @@ +CORE +already_declared3.smv + +^file .* line 8: variable x already declared, at file .* line 5$ +^EXIT=2$ +^SIGNAL=0$ +-- +-- diff --git a/regression/smv/var/already_declared3.smv b/regression/smv/var/already_declared3.smv new file mode 100644 index 000000000..75e3239e4 --- /dev/null +++ b/regression/smv/var/already_declared3.smv @@ -0,0 +1,8 @@ +MODULE some_module + +MODULE main + +VAR x : some_module; + +-- x again +VAR x : 1..10; diff --git a/regression/smv/var/already_declared4.desc b/regression/smv/var/already_declared4.desc new file mode 100644 index 000000000..9df5fac5c --- /dev/null +++ b/regression/smv/var/already_declared4.desc @@ -0,0 +1,8 @@ +KNOWNBUG +already_declared4.smv + +^EXIT=2$ +^SIGNAL=0$ +-- +-- +This should be errored. diff --git a/regression/smv/var/already_declared4.smv b/regression/smv/var/already_declared4.smv new file mode 100644 index 000000000..d4598c356 --- /dev/null +++ b/regression/smv/var/already_declared4.smv @@ -0,0 +1,8 @@ +MODULE some_module(x) + +-- already used as module parameter +VAR x : 1..10; + +MODULE main + +VAR m : some_module(1); diff --git a/regression/smv/var/already_declared5.desc b/regression/smv/var/already_declared5.desc new file mode 100644 index 000000000..be316c863 --- /dev/null +++ b/regression/smv/var/already_declared5.desc @@ -0,0 +1,8 @@ +KNOWNBUG +already_declared5.smv + +^EXIT=2$ +^SIGNAL=0$ +-- +-- +This crashes. diff --git a/regression/smv/var/already_declared5.smv b/regression/smv/var/already_declared5.smv new file mode 100644 index 000000000..50ab67c86 --- /dev/null +++ b/regression/smv/var/already_declared5.smv @@ -0,0 +1,6 @@ +MODULE main + +VAR some_enum : {x, y, z}; + +-- x is already declared +VAR x : boolean; diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index e6170e972..43eb16e81 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -673,13 +673,7 @@ var_decl : variable_identifier ':' type_specifier ';' break; case smv_parse_treet::mc_vart::DEFINED: - yyerror("variable `"+id2string(identifier)+"' already defined"); - YYERROR; - break; - case smv_parse_treet::mc_vart::DECLARED: - yyerror("variable `"+id2string(identifier)+"' already declared as variable"); - YYERROR; break; case smv_parse_treet::mc_vart::ARGUMENT: diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 059dbbf3a..8dd18ffe2 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1916,6 +1916,14 @@ void smv_typecheckt::create_var_symbols( irep_idt base_name = to_symbol_expr(item.expr).get_identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); + auto symbol_ptr = symbol_table.lookup(identifier); + if(symbol_ptr != nullptr) + { + throw errort{}.with_location(item.expr.source_location()) + << "variable " << base_name << " already declared, at " + << symbol_ptr->location; + } + typet type = item.expr.type(); // check the type @@ -1934,13 +1942,14 @@ void smv_typecheckt::create_var_symbols( symbol.value = nil_exprt{}; symbol.is_input = true; symbol.is_state_var = false; + symbol.location = item.expr.source_location(); symbol_table.insert(std::move(symbol)); } else if(item.is_define()) { - irep_idt base_name = - to_symbol_expr(to_equal_expr(item.expr).lhs()).get_identifier(); + const auto &symbol_expr = to_symbol_expr(to_equal_expr(item.expr).lhs()); + irep_idt base_name = symbol_expr.get_identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); typet type; type.make_nil(); @@ -1959,6 +1968,7 @@ void smv_typecheckt::create_var_symbols( symbol.value = nil_exprt{}; symbol.is_input = true; symbol.is_state_var = false; + symbol.location = symbol_expr.source_location(); symbol_table.insert(std::move(symbol)); }