From 262266945c953dcbfb9547bad252bfb91a993945 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 13 Dec 2025 09:08:49 -0800 Subject: [PATCH 1/2] SMV: add lhs() and rhs() helper methods This adds lhs() and rhs() helper methods to the SMV parse tree node class. --- src/smvlang/smv_parse_tree.h | 25 +++++++++++++++--- src/smvlang/smv_typecheck.cpp | 50 +++++++++++++++-------------------- 2 files changed, 42 insertions(+), 33 deletions(-) diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h index 37cf2bf7f..f5d211e36 100644 --- a/src/smvlang/smv_parse_tree.h +++ b/src/smvlang/smv_parse_tree.h @@ -142,20 +142,37 @@ class smv_parse_treet } // for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE - const equal_exprt &equal_expr() const + const exprt &lhs() const { PRECONDITION( is_assign_current() || is_assign_init() || is_assign_next() || is_define()); - return to_equal_expr(expr); + return to_equal_expr(expr).lhs(); } - equal_exprt &equal_expr() + exprt &lhs() { PRECONDITION( is_assign_current() || is_assign_init() || is_assign_next() || is_define()); - return to_equal_expr(expr); + return to_equal_expr(expr).lhs(); + } + + // for ASSIGN_CURRENT, ASSIGN_INIT, ASSIGN_NEXT, DEFINE + const exprt &rhs() const + { + PRECONDITION( + is_assign_current() || is_assign_init() || is_assign_next() || + is_define()); + return to_equal_expr(expr).rhs(); + } + + exprt &rhs() + { + PRECONDITION( + is_assign_current() || is_assign_init() || is_assign_next() || + is_define()); + return to_equal_expr(expr).rhs(); } void show(std::ostream &) const; diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index c7cee85eb..83f78c5d3 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -62,7 +62,7 @@ class smv_typecheckt:public typecheckt void create_var_symbols(const smv_parse_treet::modulet::element_listt &); - void collect_define(const equal_exprt &); + void collect_define(const exprt &lhs, const exprt &rhs); void convert_defines(exprt::operandst &invar); void convert_define(const irep_idt &identifier); @@ -1966,33 +1966,30 @@ void smv_typecheckt::typecheck(smv_parse_treet::modulet::elementt &element) return; case smv_parse_treet::modulet::elementt::ASSIGN_CURRENT: - typecheck(element.equal_expr().lhs(), OTHER); - typecheck(element.equal_expr().rhs(), OTHER); - convert_expr_to( - element.equal_expr().rhs(), element.equal_expr().lhs().type()); - element.equal_expr().type() = bool_typet{}; + typecheck(element.lhs(), OTHER); + typecheck(element.rhs(), OTHER); + convert_expr_to(element.rhs(), element.lhs().type()); + element.expr.type() = bool_typet{}; return; case smv_parse_treet::modulet::elementt::ASSIGN_INIT: - typecheck(element.equal_expr().lhs(), INIT); - typecheck(element.equal_expr().rhs(), INIT); - convert_expr_to( - element.equal_expr().rhs(), element.equal_expr().lhs().type()); - element.equal_expr().type() = bool_typet{}; - no_next_allowed(element.equal_expr().rhs()); + typecheck(element.lhs(), INIT); + typecheck(element.rhs(), INIT); + convert_expr_to(element.rhs(), element.lhs().type()); + no_next_allowed(element.rhs()); + element.expr.type() = bool_typet{}; return; case smv_parse_treet::modulet::elementt::ASSIGN_NEXT: - typecheck(element.equal_expr().lhs(), TRANS); - typecheck(element.equal_expr().rhs(), TRANS); - convert_expr_to( - element.equal_expr().rhs(), element.equal_expr().lhs().type()); - element.equal_expr().type() = bool_typet{}; + typecheck(element.lhs(), TRANS); + typecheck(element.rhs(), TRANS); + convert_expr_to(element.rhs(), element.lhs().type()); + element.expr.type() = bool_typet{}; return; case smv_parse_treet::modulet::elementt::DEFINE: typecheck(element.expr, OTHER); - element.equal_expr().type() = bool_typet{}; + element.expr.type() = bool_typet{}; return; case smv_parse_treet::modulet::elementt::ENUM: @@ -2077,8 +2074,7 @@ void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module) } else if(element.is_define()) { - const auto &identifier_expr = - to_smv_identifier_expr(to_equal_expr(element.expr).lhs()); + const auto &identifier_expr = to_smv_identifier_expr(element.lhs()); irep_idt base_name = identifier_expr.identifier(); // already used as enum? @@ -2202,8 +2198,7 @@ void smv_typecheckt::create_var_symbols( } else if(element.is_define()) { - const auto &identifier_expr = - to_smv_identifier_expr(to_equal_expr(element.expr).lhs()); + const auto &identifier_expr = to_smv_identifier_expr(element.lhs()); irep_idt base_name = identifier_expr.identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); @@ -2264,11 +2259,8 @@ Function: smv_typecheckt::collect_define \*******************************************************************/ -void smv_typecheckt::collect_define(const equal_exprt &expr) +void smv_typecheckt::collect_define(const exprt &lhs, const exprt &rhs) { - const exprt &lhs = expr.lhs(); - const exprt &rhs = expr.rhs(); - if(lhs.id() != ID_symbol) throw errort() << "collect_define expects symbol on left hand side"; @@ -2294,9 +2286,9 @@ void smv_typecheckt::collect_define(const equal_exprt &expr) if(!result.second) { - throw errort().with_location(expr.find_source_location()) + throw errort().with_location(lhs.source_location()) << "variable `" << symbol.display_name() << "' already defined"; - } + } } /*******************************************************************\ @@ -2475,7 +2467,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module) for(auto &element : smv_module.elements) { if(element.is_define() || element.is_assign_current()) - collect_define(element.equal_expr()); + collect_define(element.lhs(), element.rhs()); } // now turn them into INVARs convert_defines(trans_invar); From 7985a4b7000eab168e9ede7a3c9843bedb051df5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 13 Dec 2025 08:51:17 -0800 Subject: [PATCH 2/2] SMV: do not merge identifiers in the parser This moves the merging of complex identifiers from the SMV parser to the type checker. --- src/smvlang/parser.y | 41 ------------------- src/smvlang/smv_typecheck.cpp | 77 ++++++++++++++++++++++++++--------- 2 files changed, 58 insertions(+), 60 deletions(-) diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index 70e14599a..f7745c8b5 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -132,41 +132,6 @@ static void j_binary(YYSTYPE & dest, YYSTYPE & op1, const irep_idt &id, YYSTYPE /*******************************************************************\ -Function: merge_complex_identifier - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -irep_idt merge_complex_identifier(const exprt &expr) -{ - if(expr.id() == ID_smv_identifier) - return to_smv_identifier_expr(expr).identifier(); - else if(expr.id() == ID_member) - { - auto &member_expr = to_member_expr(expr); - return id2string(merge_complex_identifier(member_expr.compound())) + '.' + id2string(member_expr.get_component_name()); - } - else if(expr.id() == ID_index) - { - auto &index_expr = to_index_expr(expr); - auto &index = index_expr.index(); - PRECONDITION(index.is_constant()); - auto index_string = id2string(to_constant_expr(index).get_value()); - return id2string(merge_complex_identifier(index_expr.array())) + '.' + index_string; - } - else - { - DATA_INVARIANT_WITH_DIAGNOSTICS(false, "unexpected complex_identifier", expr.pretty()); - } -} - -/*******************************************************************\ - Function: new_module Inputs: @@ -910,12 +875,6 @@ identifier : IDENTIFIER_Token ; variable_identifier: complex_identifier - { - // Could be a variable, or an enum - auto id = merge_complex_identifier(stack_expr($1)); - init($$, ID_smv_identifier); - stack_expr($$).set(ID_identifier, id); - } | STRING_Token { // Not in the NuSMV grammar. diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 83f78c5d3..2049e2bea 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -155,6 +155,44 @@ class smv_typecheckt:public typecheckt /*******************************************************************\ +Function: merge_complex_identifier + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +irep_idt merge_complex_identifier(const exprt &expr) +{ + if(expr.id() == ID_smv_identifier) + return to_smv_identifier_expr(expr).identifier(); + else if(expr.id() == ID_member) + { + auto &member_expr = to_member_expr(expr); + return id2string(merge_complex_identifier(member_expr.compound())) + '.' + + id2string(member_expr.get_component_name()); + } + else if(expr.id() == ID_index) + { + auto &index_expr = to_index_expr(expr); + auto &index = index_expr.index(); + PRECONDITION(index.is_constant()); + auto index_string = id2string(to_constant_expr(index).get_value()); + return id2string(merge_complex_identifier(index_expr.array())) + '.' + + index_string; + } + else + { + DATA_INVARIANT_WITH_DIAGNOSTICS( + false, "unexpected complex_identifier", expr.pretty()); + } +} + +/*******************************************************************\ + Function: smv_typecheckt::convert_ports Inputs: @@ -2039,34 +2077,34 @@ void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module) { if(element.is_var() || element.is_ivar()) { - const auto &identifier_expr = to_smv_identifier_expr(element.expr); - irep_idt base_name = identifier_expr.identifier(); + irep_idt base_name = merge_complex_identifier(element.expr); + auto location = element.expr.source_location(); // already used as enum? if(enums.find(base_name) != enums.end()) { - throw errort{}.with_location(identifier_expr.source_location()) + throw errort{}.with_location(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()) + throw errort{}.with_location(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()) + throw errort{}.with_location(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()) + throw errort{}.with_location(location) << "identifier " << base_name << " already used as define"; } @@ -2074,34 +2112,34 @@ void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module) } else if(element.is_define()) { - const auto &identifier_expr = to_smv_identifier_expr(element.lhs()); - irep_idt base_name = identifier_expr.identifier(); + irep_idt base_name = merge_complex_identifier(element.lhs()); + auto location = to_equal_expr(element.expr).lhs().source_location(); // already used as enum? if(enums.find(base_name) != enums.end()) { - throw errort{}.with_location(identifier_expr.source_location()) + throw errort{}.with_location(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()) + throw errort{}.with_location(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()) + throw errort{}.with_location(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()) + throw errort{}.with_location(location) << "identifier " << base_name << " already used as define"; } @@ -2159,13 +2197,14 @@ void smv_typecheckt::create_var_symbols( { if(element.is_var() || element.is_ivar()) { - irep_idt base_name = to_smv_identifier_expr(element.expr).identifier(); + irep_idt base_name = merge_complex_identifier(element.expr); + auto location = element.expr.source_location(); irep_idt identifier = module + "::var::" + id2string(base_name); auto symbol_ptr = symbol_table.lookup(identifier); if(symbol_ptr != nullptr) { - throw errort{}.with_location(element.expr.source_location()) + throw errort{}.with_location(location) << "variable " << base_name << " already declared, at " << symbol_ptr->location; } @@ -2192,20 +2231,20 @@ void smv_typecheckt::create_var_symbols( symbol.is_state_var = false; symbol.value = nil_exprt{}; - symbol.location = element.expr.source_location(); + symbol.location = location; symbol_table.insert(std::move(symbol)); } else if(element.is_define()) { - const auto &identifier_expr = to_smv_identifier_expr(element.lhs()); - irep_idt base_name = identifier_expr.identifier(); + irep_idt base_name = merge_complex_identifier(element.lhs()); + auto location = to_equal_expr(element.expr).lhs().source_location(); 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()) + throw errort{}.with_location(location) << "variable `" << base_name << "' already declared, at " << symbol_ptr->location; } @@ -2227,7 +2266,7 @@ void smv_typecheckt::create_var_symbols( symbol.value = nil_exprt{}; symbol.is_input = true; symbol.is_state_var = false; - symbol.location = identifier_expr.source_location(); + symbol.location = location; symbol_table.insert(std::move(symbol)); }