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.

Author: kroening

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 '[' '('
 
 %%
 
@@ -819,7 +819,26 @@ constant   : NUMBER_Token             { init($$, ID_constant); stack_expr($$).se
            ;
 
 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); }
@@ -845,6 +864,9 @@ 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 '[' basic_expr ':' basic_expr ']'
+                                                  { init($$, ID_extractbits); mto($$, $1); mto($$, $3); mto($$, $5); }
            | 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); }

src/smvlang/smv_typecheck.cpp

@@ -1724,6 +1724,32 @@ void smv_typecheckt::convert(exprt &expr)
       expr.remove(ID_identifier);
     }
   }
+  else if(expr.id() == ID_member)
+  {
+    auto &member_expr = to_member_expr(expr);
+    if(member_expr.compound().id() != ID_symbol)
+      DATA_INVARIANT_WITH_DIAGNOSTICS(
+        false, "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);
+    if(index_expr.array().id() != ID_symbol)
+      DATA_INVARIANT_WITH_DIAGNOSTICS(
+        false, "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")
   {