Merge pull request #1507 from diffblue/invalid_width1

SMV: allow any expression in SMV types

Author: tautschnig

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())