Merge pull request #1154 from diffblue/smv-enumeration-type

introduce SMV enumeration type

Author: kroening

regression/smv/enums/enum3.desc

@@ -1,7 +1,7 @@
 CORE
 enum3.smv
 
-^file .* line 7: enum c not a member of \{ a, b \}$
+^file .* line 7: Expected expression of type `\{ a, b \}', but got expression `c', which is of type `\{ c \}'$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/enums/enum5.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE broken-smt-backend
 enum5.smv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This fails in the decision procedure.

src/hw_cbmc_irep_ids.h

@@ -21,6 +21,7 @@ IREP_ID_ONE(smv_abs)
 IREP_ID_ONE(smv_bitimplies)
 IREP_ID_ONE(smv_bool)
 IREP_ID_ONE(smv_count)
+IREP_ID_ONE(smv_enumeration)
 IREP_ID_ONE(smv_extend)
 IREP_ID_ONE(smv_max)
 IREP_ID_ONE(smv_min)

src/smvlang/Makefile

@@ -2,6 +2,7 @@ SRC = smv_expr.cpp \
       smv_language.cpp \
       smv_parser.cpp \
       smv_typecheck.cpp \
+      smv_types.cpp \
       expr2smv.cpp \
       smv_y.tab.cpp \
       lex.yy.cpp \

src/smvlang/expr2smv.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_types.h>
 
 #include "smv_expr.h"
+#include "smv_types.h"
 
 /*******************************************************************\
 
@@ -337,6 +338,12 @@ expr2smvt::resultt expr2smvt::convert_typecast(const typecast_exprt &expr)
       return convert_rec(smv_resize_exprt{expr.op(), dest_width, dest_type});
     }
   }
+  else if(
+    src_type.id() == ID_smv_enumeration && dest_type.id() == ID_smv_enumeration)
+  {
+    // added by SMV typechecker, implicit
+    return convert_rec(expr.op());
+  }
   else
     return convert_norep(expr);
 }
@@ -593,10 +600,9 @@ expr2smvt::resultt expr2smvt::convert_constant(const constant_exprt &src)
     else
       dest+="FALSE";
   }
-  else if(type.id()==ID_integer ||
-          type.id()==ID_natural ||
-          type.id()==ID_range ||
-          type.id()==ID_enumeration)
+  else if(
+    type.id() == ID_integer || type.id() == ID_natural ||
+    type.id() == ID_range || type.id() == ID_smv_enumeration)
   {
     dest = id2string(src.get_value());
   }
@@ -903,15 +909,15 @@ std::string type2smv(const typet &type, const namespacet &ns)
     code += type2smv(to_array_type(type).element_type(), ns);
     return code;
   }
-  else if(type.id()==ID_enumeration)
+  else if(type.id() == ID_smv_enumeration)
   {
-    const irept::subt &elements=to_enumeration_type(type).elements();
+    auto elements = to_smv_enumeration_type(type).elements();
     std::string code = "{ ";
     bool first=true;
     for(auto &element : elements)
     {
       if(first) first=false; else code+=", ";
-      code += element.id_string();
+      code += id2string(element);
     }
     code+=" }";
     return code;

src/smvlang/parser.y

@@ -642,7 +642,7 @@ parameter_list:
 
 enum_list  : enum_element
            {
-             init($$, ID_enumeration);
+             init($$, ID_smv_enumeration);
              stack_expr($$).add(ID_elements).get_sub().push_back(irept(stack_expr($1).id()));
            }
            | enum_list ',' enum_element
@@ -946,7 +946,7 @@ variable_identifier: complex_identifier
              else if(is_enum)
              {
                init($$, ID_constant);
-               stack_expr($$).type()=typet(ID_enumeration);
+               stack_expr($$).type()=typet(ID_smv_enumeration);
                stack_expr($$).set(ID_value, id);
              }
              else // not an enum, probably a variable