SMV: allow any expression in SMV types

This extends the grammar to allow any expressions as the size of arrays and
as the width of word types.  This matches the NuSMV manual.

The type checker enforces that these are constants.

Author: kroening

regression/smv/word/invalid_width1.desc

@@ -0,0 +1,8 @@
+CORE
+invalid_width1.smv
+
+^file .* line 6: expected constant expression$
+^EXIT=2$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/smv/word/invalid_width1.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR width : 1..10;
+
+-- The width must be constant
+VAR word_var : word[width];

src/smvlang/parser.y

@@ -556,25 +556,25 @@ type_specifier:
            ;
 
 simple_type_specifier:
-             array_Token integer_constant DOTDOT_Token integer_constant of_Token simple_type_specifier
+             array_Token basic_expr DOTDOT_Token basic_expr of_Token simple_type_specifier
            {
              init($$, ID_smv_array);
              stack_type($$).set(ID_from, stack_expr($2));
              stack_type($$).set(ID_to, stack_expr($4));
              stack_type($$).add_subtype()=stack_type($6);
            }
            | boolean_Token { init($$, ID_bool); }
-           | word_Token '[' integer_constant ']'
+           | word_Token '[' basic_expr ']'
            {
              init($$, ID_smv_word);
              stack_type($$).set(ID_width, stack_expr($3));
            }
-           | signed_Token word_Token '[' integer_constant ']'
+           | signed_Token word_Token '[' basic_expr ']'
            {
              init($$, ID_smv_signed_word);
              stack_type($$).set(ID_width, stack_expr($4));
            }
-           | unsigned_Token word_Token '[' integer_constant ']'
+           | unsigned_Token word_Token '[' basic_expr ']'
            {
              init($$, ID_smv_unsigned_word);
              stack_type($$).set(ID_width, stack_expr($4));

src/smvlang/smv_typecheck.cpp

@@ -144,6 +144,8 @@ class smv_typecheckt:public typecheckt
       return id;
   }
 
+  mp_integer require_integer_constant(const irept &) const;
+
   void lower_node(exprt &) const;
 
   void lower(typet &) const;
@@ -363,6 +365,36 @@ void smv_typecheckt::instantiate(
 
 /*******************************************************************\
 
+Function: smv_typecheckt::require_integer_constant
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+mp_integer smv_typecheckt::require_integer_constant(const irept &irep) const
+{
+  auto &as_expr = static_cast<const exprt &>(irep);
+  if(as_expr.id() != ID_constant)
+  {
+    throw errort().with_location(as_expr.source_location())
+      << "expected constant expression";
+  }
+
+  if(as_expr.type().id() != ID_integer)
+  {
+    throw errort().with_location(as_expr.source_location())
+      << "expected integer expression";
+  }
+
+  return numeric_cast_v<mp_integer>(to_constant_expr(as_expr));
+}
+
+/*******************************************************************\
+
 Function: smv_typecheckt::check_type
 
   Inputs:
@@ -377,10 +409,8 @@ void smv_typecheckt::check_type(typet &type)
 {
   if(type.id() == ID_smv_array)
   {
-    auto from = numeric_cast_v<mp_integer>(
-      to_constant_expr(static_cast<const exprt &>(type.find(ID_from))));
-    auto to = numeric_cast_v<mp_integer>(
-      to_constant_expr(static_cast<const exprt &>(type.find(ID_to))));
+    auto from = require_integer_constant(type.find(ID_from));
+    auto to = require_integer_constant(type.find(ID_to));
 
     if(to < from)
       throw errort().with_location(type.source_location())
@@ -402,10 +432,8 @@ void smv_typecheckt::check_type(typet &type)
   }
   else if(type.id() == ID_smv_range)
   {
-    auto from = numeric_cast_v<mp_integer>(
-      to_constant_expr(static_cast<const exprt &>(type.find(ID_from))));
-    auto to = numeric_cast_v<mp_integer>(
-      to_constant_expr(static_cast<const exprt &>(type.find(ID_to))));
+    auto from = require_integer_constant(type.find(ID_from));
+    auto to = require_integer_constant(type.find(ID_to));
 
     if(from > to)
       throw errort().with_location(type.source_location()) << "range is empty";
@@ -416,8 +444,7 @@ void smv_typecheckt::check_type(typet &type)
   }
   else if(type.id() == ID_smv_signed_word)
   {
-    auto width = numeric_cast_v<mp_integer>(
-      to_constant_expr(static_cast<const exprt &>(type.find(ID_width))));
+    auto width = require_integer_constant(type.find(ID_width));
 
     if(width < 1)
       throw errort().with_location(type.source_location())
@@ -428,8 +455,7 @@ void smv_typecheckt::check_type(typet &type)
   }
   else if(type.id() == ID_smv_word || type.id() == ID_smv_unsigned_word)
   {
-    auto width = numeric_cast_v<mp_integer>(
-      to_constant_expr(static_cast<const exprt &>(type.find(ID_width))));
+    auto width = require_integer_constant(type.find(ID_width));
 
     if(width < 1)
       throw errort().with_location(type.source_location())