From fc420ae2547b67b0313daa21e7320372b9b193e3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 26 Oct 2025 13:00:34 -0700 Subject: [PATCH] SMV: introduce smv_identifier_exprt This introduces a class for the identifiers used in the SMV parse tree. The type checker subsequently turns them into symbols, when this is appropriate. --- src/hw_cbmc_irep_ids.h | 1 + src/smvlang/parser.y | 13 +++++++------ src/smvlang/smv_expr.h | 36 +++++++++++++++++++++++++++++++++++ src/smvlang/smv_typecheck.cpp | 16 +++++++++------- 4 files changed, 53 insertions(+), 13 deletions(-) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 912591f66..87ca0a2a7 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -26,6 +26,7 @@ IREP_ID_ONE(smv_extend) IREP_ID_ONE(smv_max) IREP_ID_ONE(smv_min) IREP_ID_ONE(smv_next) +IREP_ID_ONE(smv_identifier) IREP_ID_ONE(smv_iff) IREP_ID_TWO(C_smv_iff, "#smv_iff") IREP_ID_ONE(smv_resize) diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y index d2e37796c..564d5b365 100644 --- a/src/smvlang/parser.y +++ b/src/smvlang/parser.y @@ -2,6 +2,7 @@ %define parse.error verbose %{ +#include "smv_expr.h" #include "smv_parser.h" #include "smv_typecheck.h" @@ -142,8 +143,8 @@ Function: merge_complex_identifier irep_idt merge_complex_identifier(const exprt &expr) { - if(expr.id() == ID_symbol) - return to_symbol_expr(expr).get_identifier(); + 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); @@ -677,7 +678,7 @@ enum_element: IDENTIFIER_Token $$=$1; PARSER.module->enum_set.insert(stack_expr($1).id_string()); - exprt expr(ID_symbol); + exprt expr(ID_smv_identifier); expr.set(ID_identifier, stack_expr($1).id()); PARSER.set_source_location(expr); PARSER.module->add_enum(std::move(expr)); @@ -970,7 +971,7 @@ variable_identifier: complex_identifier } else // not an enum, probably a variable { - init($$, ID_symbol); + init($$, ID_smv_identifier); stack_expr($$).set(ID_identifier, id); auto var_it = PARSER.module->vars.find(id); if(var_it!= PARSER.module->vars.end()) @@ -983,7 +984,7 @@ variable_identifier: complex_identifier // Not in the NuSMV grammar. const irep_idt &id=stack_expr($1).id(); - init($$, ID_symbol); + init($$, ID_smv_identifier); stack_expr($$).set(ID_identifier, id); PARSER.module->vars[id]; } @@ -994,7 +995,7 @@ complex_identifier: { $$ = $1; irep_idt identifier = stack_expr($$).id(); - stack_expr($$).id(ID_symbol); + stack_expr($$).id(ID_smv_identifier); stack_expr($$).set(ID_identifier, identifier); } | complex_identifier DOT_Token QIDENTIFIER_Token diff --git a/src/smvlang/smv_expr.h b/src/smvlang/smv_expr.h index eda40fc59..e1bad9c97 100644 --- a/src/smvlang/smv_expr.h +++ b/src/smvlang/smv_expr.h @@ -326,4 +326,40 @@ inline smv_word1_exprt &to_smv_word1_expr(exprt &expr) return static_cast(expr); } +// parse tree only -- used for identifiers, which may turn into +// symbols or enums +class smv_identifier_exprt : public nullary_exprt +{ +public: + explicit smv_identifier_exprt(irep_idt _identifier) + : nullary_exprt{ID_smv_identifier, typet{}} + { + identifier(_identifier); + } + + irep_idt identifier() const + { + return get(ID_identifier); + } + + void identifier(irep_idt _identifier) + { + set(ID_identifier, _identifier); + } +}; + +inline const smv_identifier_exprt &to_smv_identifier_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_identifier); + smv_identifier_exprt::check(expr); + return static_cast(expr); +} + +inline smv_identifier_exprt &to_smv_identifier_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_smv_identifier); + smv_identifier_exprt::check(expr); + return static_cast(expr); +} + #endif // CPROVER_SMV_EXPR_H diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index 610dec517..4e0e58d07 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -203,7 +203,7 @@ void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module) for(auto &op : inst.operands()) convert(op); - auto instance_base_name = to_symbol_expr(item.expr).get_identifier(); + auto instance_base_name = to_smv_identifier_expr(item.expr).identifier(); instantiate( smv_module, @@ -1701,7 +1701,7 @@ void smv_typecheckt::convert(exprt &expr) for(auto &op : expr.operands()) convert(op); - if(expr.id()==ID_symbol) + if(expr.id() == ID_smv_identifier) { const std::string &identifier=expr.get_string(ID_identifier); @@ -1711,6 +1711,7 @@ void smv_typecheckt::convert(exprt &expr) std::string id = module + "::var::" + identifier; expr.set(ID_identifier, id); + expr.id(ID_symbol); } else if(expr.id()=="smv_nondet_choice" || expr.id()=="smv_union") @@ -1914,7 +1915,7 @@ void smv_typecheckt::create_var_symbols( { if(item.is_var()) { - irep_idt base_name = to_symbol_expr(item.expr).get_identifier(); + irep_idt base_name = to_smv_identifier_expr(item.expr).identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); auto symbol_ptr = symbol_table.lookup(identifier); @@ -1953,8 +1954,9 @@ void smv_typecheckt::create_var_symbols( } else if(item.is_define()) { - const auto &symbol_expr = to_symbol_expr(to_equal_expr(item.expr).lhs()); - irep_idt base_name = symbol_expr.get_identifier(); + const auto &identifier_expr = + 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); typet type; type.make_nil(); @@ -1973,13 +1975,13 @@ 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.location = identifier_expr.source_location(); symbol_table.insert(std::move(symbol)); } else if(item.is_enum()) { - irep_idt base_name = to_symbol_expr(item.expr).get_identifier(); + irep_idt base_name = to_smv_identifier_expr(item.expr).identifier(); irep_idt identifier = module + "::var::" + id2string(base_name); auto symbol_ptr = symbol_table.lookup(identifier);