From d848ecb30f6c85f60e544918facfdf92550be62e Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 1 Nov 2025 14:37:20 -0700
Subject: [PATCH] SMV: move conversion of . and [...] to type checker

This moves the conversion of the .  (dot) and [...] index operators from the
SMV parser to the type checker, to enable array index and bit extract
operators.
---
 src/smvlang/parser.y          | 24 ++++++++++++++++++++++--
 src/smvlang/smv_typecheck.cpp | 28 ++++++++++++++++++++++++++++
 2 files changed, 50 insertions(+), 2 deletions(-)

diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index bf1cc1ff7..31f0973f6 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -341,7 +341,7 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &module_name)
 %left  TIMES_Token DIVIDE_Token
 %left  COLONCOLON_Token
 %left  UMINUS           /* supplies precedence for unary minus */
-%left  DOT_Token
+%left  DOT_Token '[' '('
 
 %%
 
@@ -842,7 +842,26 @@ integer_constant:
            ;
 
 basic_expr : constant
-           | variable_identifier
+           | identifier
+           {
+             // This rule is part of "complex_identifier" in the NuSMV manual.
+             $$ = $1;
+             irep_idt identifier = stack_expr($$).id();
+             stack_expr($$).id(ID_smv_identifier);
+             stack_expr($$).set(ID_identifier, identifier);
+             PARSER.set_source_location(stack_expr($$));
+           }
+           | basic_expr DOT_Token IDENTIFIER_Token
+           {
+             // This rule is part of "complex_identifier" in the NuSMV manual.
+             unary($$, ID_member, $1);
+             stack_expr($$).set(ID_component_name, stack_expr($3).id());
+           }
+           | basic_expr '(' basic_expr ')'
+           {
+             // Not in the NuSMV grammar.
+             binary($$, $1, ID_index, $3);
+           }
            | '(' formula ')'                      { $$=$2; }
            | NOT_Token basic_expr                 { init($$, ID_not); mto($$, $2); }
            | "abs" '(' basic_expr ')'             { unary($$, ID_smv_abs, $3); }
@@ -868,6 +887,7 @@ basic_expr : constant
            | basic_expr mod_Token basic_expr      { binary($$, $1, ID_mod, $3); }
            | basic_expr GTGT_Token basic_expr     { binary($$, $1, ID_shr, $3); }
            | basic_expr LTLT_Token basic_expr     { binary($$, $1, ID_shl, $3); }
+           | basic_expr '[' basic_expr ']'        { binary($$, $1, ID_index, $3); }
            | basic_expr COLONCOLON_Token basic_expr { binary($$, $1, ID_concatenation, $3); }
            | "word1" '(' basic_expr ')'           { unary($$, ID_smv_word1, $3); }
            | "bool" '(' basic_expr ')'            { unary($$, ID_smv_bool, $3); }
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index eb9d49e84..170e3a40e 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -1724,6 +1724,34 @@ void smv_typecheckt::convert(exprt &expr)
       expr.remove(ID_identifier);
     }
   }
+  else if(expr.id() == ID_member)
+  {
+    auto &member_expr = to_member_expr(expr);
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      member_expr.compound().id() == ID_symbol,
+      "unexpected complex_identifier",
+      expr.pretty());
+
+    auto tmp = to_symbol_expr(member_expr.compound());
+    tmp.set_identifier(
+      id2string(tmp.get_identifier()) + '.' +
+      id2string(member_expr.get_component_name()));
+    expr = tmp;
+  }
+  else if(expr.id() == ID_index)
+  {
+    auto &index_expr = to_index_expr(expr);
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      index_expr.array().id() == ID_symbol,
+      "unexpected complex_identifier",
+      expr.pretty());
+    auto &index = index_expr.index();
+    PRECONDITION(index.is_constant());
+    auto index_string = id2string(to_constant_expr(index).get_value());
+    auto tmp = to_symbol_expr(index_expr.array());
+    tmp.set_identifier(id2string(tmp.get_identifier()) + '.' + index_string);
+    expr = tmp;
+  }
   else if(expr.id()=="smv_nondet_choice" ||
           expr.id()=="smv_union")
   {