SMV: type checking of simple types

src/hw_cbmc_irep_ids.h

@@ -18,31 +18,36 @@ IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
 IREP_ID_ONE(smv_abs)
+IREP_ID_ONE(smv_array)
 IREP_ID_ONE(smv_bitimplies)
 IREP_ID_ONE(smv_bit_selection)
 IREP_ID_ONE(smv_bool)
 IREP_ID_ONE(smv_cases)
 IREP_ID_ONE(smv_count)
 IREP_ID_ONE(smv_enumeration)
 IREP_ID_ONE(smv_extend)
+IREP_ID_ONE(smv_identifier)
+IREP_ID_ONE(smv_iff)
 IREP_ID_ONE(smv_max)
 IREP_ID_ONE(smv_min)
+IREP_ID_ONE(smv_module_instance)
 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_range)
 IREP_ID_ONE(smv_resize)
 IREP_ID_ONE(smv_toint)
 IREP_ID_ONE(smv_set)
 IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)
 IREP_ID_ONE(smv_signed_cast)
+IREP_ID_ONE(smv_signed_word)
 IREP_ID_ONE(smv_sizeof)
-IREP_ID_ONE(smv_module_instance)
 IREP_ID_ONE(smv_swconst)
 IREP_ID_ONE(smv_union)
 IREP_ID_ONE(smv_unsigned_cast)
+IREP_ID_ONE(smv_unsigned_word)
 IREP_ID_ONE(smv_uwconst)
+IREP_ID_ONE(smv_word)
 IREP_ID_ONE(smv_word1)
 IREP_ID_ONE(smv_word_constant)
 IREP_ID_ONE(smv_H)

src/smvlang/parser.y

@@ -556,42 +556,33 @@ type_specifier:
            ;
 
 simple_type_specifier:
-             array_Token NUMBER_Token DOTDOT_Token NUMBER_Token of_Token simple_type_specifier
+             array_Token integer_constant DOTDOT_Token integer_constant of_Token simple_type_specifier
            {
-             init($$, ID_array);
-             int start=atoi(stack_expr($2).id().c_str());
-             int end=atoi(stack_expr($4).id().c_str());
-
-             if(end < start)
-             {
-               yyerror("array must end with number >= `"+std::to_string(start)+"'");
-               YYERROR;
-             }
-
-             stack_type($$).set(ID_size, end-start+1);
-             stack_type($$).set(ID_offset, start);
+             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 '[' NUMBER_Token ']'
+           | word_Token '[' integer_constant ']'
            {
-             init($$, ID_unsignedbv);
-             stack_type($$).set(ID_width, stack_expr($3).id());
+             init($$, ID_smv_word);
+             stack_type($$).set(ID_width, stack_expr($3));
            }
-           | signed_Token word_Token '[' NUMBER_Token ']'
+           | signed_Token word_Token '[' integer_constant ']'
            {
-             init($$, ID_signedbv);
-             stack_type($$).set(ID_width, stack_expr($4).id());
+             init($$, ID_smv_signed_word);
+             stack_type($$).set(ID_width, stack_expr($4));
            }
-           | unsigned_Token word_Token '[' NUMBER_Token ']'
+           | unsigned_Token word_Token '[' integer_constant ']'
            {
-             init($$, ID_unsignedbv);
-             stack_type($$).set(ID_width, stack_expr($4).id());
+             init($$, ID_smv_unsigned_word);
+             stack_type($$).set(ID_width, stack_expr($4));
            }
            | '{' enum_list '}' { $$=$2; }
-           | NUMBER_Token DOTDOT_Token NUMBER_Token
+           | integer_constant DOTDOT_Token integer_constant
            {
-             init($$, ID_range);
+             init($$, ID_smv_range);
              stack_type($$).set(ID_from, stack_expr($1));
              stack_type($$).set(ID_to, stack_expr($3));
            }

src/smvlang/smv_typecheck.cpp

@@ -365,18 +365,69 @@ Function: smv_typecheckt::check_type
 
 void smv_typecheckt::check_type(typet &type)
 {
-  if(type.id() == ID_range)
+  if(type.id() == ID_smv_array)
   {
-    auto range = smv_ranget::from_type(to_range_type(type));
+    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))));
 
-    if(range.from > range.to)
-      throw errort().with_location(type.source_location()) << "range is empty";
+    if(to < from)
+      throw errort().with_location(type.source_location())
+        << "array must end with number >= `" << from << '\'';
+
+    type.id(ID_array);
+    type.remove(ID_from);
+    type.remove(ID_to);
+    type.set(ID_size, integer2string(to - from + 1));
+    type.set(ID_offset, integer2string(from));
+
+    // recursive call
+    check_type(to_type_with_subtype(type).subtype());
   }
   else if(type.id() == ID_smv_enumeration)
   {
     // normalize the ordering of elements
     to_smv_enumeration_type(type).normalize();
   }
+  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))));
+
+    if(from > to)
+      throw errort().with_location(type.source_location()) << "range is empty";
+
+    type.id(ID_range);
+    type.set(ID_from, integer2string(from));
+    type.set(ID_to, integer2string(to));
+  }
+  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))));
+
+    if(width < 1)
+      throw errort().with_location(type.source_location())
+        << "word width must be 1 or larger";
+
+    type.id(ID_signedbv);
+    type.set(ID_width, integer2string(width));
+  }
+  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))));
+
+    if(width < 1)
+      throw errort().with_location(type.source_location())
+        << "word width must be 1 or larger";
+
+    type.id(ID_unsignedbv);
+    type.set(ID_width, integer2string(width));
+  }
 }
 
 /*******************************************************************\