introduce SMV enumeration type

SMV enumerations behave differently from enumeration_typet; hence, this
introduces smv_enumeration_typet, which is subsequently lowered to
enumeration_typet.

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$
 --

src/hw_cbmc_irep_ids.h

@@ -18,6 +18,7 @@ IREP_ID_ONE(E)
 IREP_ID_ONE(G)
 IREP_ID_ONE(X)
 IREP_ID_ONE(smv_bitimplies)
+IREP_ID_ONE(smv_enumeration)
 IREP_ID_ONE(smv_extend)
 IREP_ID_ONE(smv_next)
 IREP_ID_ONE(smv_iff)

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, [email protected]
 #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());
   }
@@ -885,15 +891,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

@@ -522,7 +522,7 @@ module_type_specifier:
 
 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
@@ -808,7 +808,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

src/smvlang/smv_typecheck.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include "expr2smv.h"
 #include "smv_expr.h"
 #include "smv_range.h"
+#include "smv_types.h"
 
 #include <algorithm>
 #include <cassert>
@@ -83,8 +84,6 @@ class smv_typecheckt:public typecheckt
 
   void check_type(const typet &);
   smv_ranget convert_type(const typet &);
-  static bool
-  is_contained_in(const enumeration_typet &, const enumeration_typet &);
 
   void convert(smv_parse_treet::modulet::itemt &);
   void typecheck(smv_parse_treet::modulet::itemt &);
@@ -142,6 +141,8 @@ class smv_typecheckt:public typecheckt
 
   void lower_node(exprt &) const;
 
+  void lower(typet &) const;
+
   void lower(exprt &expr) const
   {
     expr.visit_post([this](exprt &expr) { lower_node(expr); });
@@ -150,40 +151,6 @@ class smv_typecheckt:public typecheckt
 
 /*******************************************************************\
 
-Function: smv_typecheckt::is_contained_in
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-bool smv_typecheckt::is_contained_in(
-  const enumeration_typet &type1,
-  const enumeration_typet &type2)
-{
-  // This is quadratic.
-  for(auto &element1 : type1.elements())
-  {
-    bool found = false;
-    for(auto &element2 : type2.elements())
-      if(element1.id() == element2.id())
-      {
-        found = true;
-        break;
-      }
-
-    if(!found)
-      return false;
-  }
-
-  return true;
-}
-
-/*******************************************************************\
-
 Function: smv_typecheckt::convert_ports
 
   Inputs:
@@ -499,15 +466,15 @@ smv_ranget smv_typecheckt::convert_type(const typet &src)
   {
     return smv_ranget::from_type(to_range_type(src));
   }
-  else if(src.id()==ID_enumeration)
+  else if(src.id() == ID_smv_enumeration)
   {
     smv_ranget dest;
 
     dest.from=0;
 
-    std::size_t number_of_elements=
-      to_enumeration_type(src).elements().size();
-      
+    std::size_t number_of_elements =
+      to_smv_enumeration_type(src).elements().size();
+
     if(number_of_elements==0)
       dest.to=0;
     else
@@ -557,36 +524,16 @@ typet smv_typecheckt::type_union(
   }
 
   // both enums?
-  if(type1.id()==ID_enumeration && type2.id()==ID_enumeration)
+  if(type1.id() == ID_smv_enumeration && type2.id() == ID_smv_enumeration)
   {
-    auto &e_type1 = to_enumeration_type(type1);
-    auto &e_type2 = to_enumeration_type(type2);
-
-    if(is_contained_in(e_type2, e_type1))
-      return type1;
-
-    if(is_contained_in(e_type1, e_type2))
-      return type2;
-
-    // make union
-    std::set<irep_idt> enum_set;
-
-    for(auto &e : e_type1.elements())
-      enum_set.insert(e.id());
+    auto &e_type1 = to_smv_enumeration_type(type1);
+    auto &e_type2 = to_smv_enumeration_type(type2);
 
-    for(auto &e : e_type2.elements())
-      enum_set.insert(e.id());
-
-    enumeration_typet union_type;
-    union_type.elements().reserve(enum_set.size());
-    for(auto &e : enum_set)
-      union_type.elements().push_back(irept{e});
-
-    return std::move(union_type);
+    return ::type_union(e_type1, e_type2);
   }
 
   // one of them enum?
-  if(type1.id() == ID_enumeration || type2.id() == ID_enumeration)
+  if(type1.id() == ID_smv_enumeration || type2.id() == ID_smv_enumeration)
   {
     throw errort().with_location(source_location)
       << "no type union for types " << to_string(type1) << " and "
@@ -869,10 +816,9 @@ void smv_typecheckt::typecheck_expr_rec(exprt &expr, modet mode)
       mp_integer int_value = string2integer(id2string(value));
       expr.type() = range_typet{int_value, int_value};
     }
-    else if(type.id() == ID_enumeration)
+    else if(type.id() == ID_smv_enumeration)
     {
-      auto t = enumeration_typet{};
-      t.elements().push_back(irept{value});
+      auto t = smv_enumeration_typet{{value}};
       expr.type() = std::move(t);
     }
     else if(type.id() == ID_bool)
@@ -1253,6 +1199,9 @@ Function: smv_typecheckt::lower_node
 
 void smv_typecheckt::lower_node(exprt &expr) const
 {
+  // lower the type
+  lower(expr.type());
+
   if(expr.id() == ID_smv_extend)
   {
     auto &smv_extend = to_smv_extend_expr(expr);
@@ -1275,6 +1224,27 @@ void smv_typecheckt::lower_node(exprt &expr) const
 
 /*******************************************************************\
 
+Function: smv_typecheckt::lower
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::lower(typet &type) const
+{
+  // lower the type
+  if(type.id() == ID_smv_enumeration)
+  {
+    type.id(ID_enumeration);
+  }
+}
+
+/*******************************************************************\
+
 Function: smv_typecheckt::convert_expr_to
 
   Inputs:
@@ -1350,35 +1320,40 @@ void smv_typecheckt::convert_expr_to(exprt &expr, const typet &type)
         }
       }
     }
-    else if(type.id() == ID_enumeration)
+    else if(type.id() == ID_smv_enumeration)
     {
-      auto &e_type = to_enumeration_type(type);
+      auto &e_type = to_smv_enumeration_type(type);
 
-      if(expr.id() == ID_constant && expr.type().id() == ID_enumeration)
+      if(expr.type().id() == ID_smv_enumeration)
       {
-        if(is_contained_in(to_enumeration_type(expr.type()), e_type))
+        // subset?
+        if(to_smv_enumeration_type(expr.type()).is_subset_of(e_type))
         {
-          // re-type the constant
-          expr.type() = type;
-          return;
-        }
-        else
-        {
-          throw errort().with_location(expr.find_source_location())
-            << "enum " << to_string(expr) << " not a member of "
-            << to_string(type);
-        }
-      }
-      else if(expr.id() == ID_typecast)
-      {
-        // created by type unions
-        auto &op = to_typecast_expr(expr).op();
-        if(
-          expr.type().id() == ID_enumeration &&
-          op.type().id() == ID_enumeration)
-        {
-          convert_expr_to(op, type);
-          expr = std::move(op);
+          // yes, it's a subset
+          if(expr.is_constant())
+          {
+            // re-type the constant
+            expr.type() = type;
+            return;
+          }
+          else if(expr.id() == ID_typecast)
+          {
+            // created by type unions
+            auto &op = to_typecast_expr(expr).op();
+            if(
+              expr.type().id() == ID_smv_enumeration &&
+              op.type().id() == ID_smv_enumeration)
+            {
+              convert_expr_to(op, type);
+              expr = std::move(op);
+              return;
+            }
+          }
+          else // anything else
+          {
+            expr = typecast_exprt{std::move(expr), type};
+            return;
+          }
         }
       }
     }
@@ -1875,9 +1850,6 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
         transt{ID_trans, conjunction(trans_invar), conjunction(trans_init),
                conjunction(trans_trans), module_symbol.type};
 
-    // lowering
-    lower(module_symbol.value);
-
     module_symbol.pretty_name = strip_smv_prefix(module_symbol.name);
 
     symbol_table.add(module_symbol);
@@ -1916,12 +1888,21 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
           spec_symbol.pretty_name = strip_smv_prefix(spec_symbol.name);
 
         // lowering
-        lower(spec_symbol.value);
 
         symbol_table.add(spec_symbol);
       }
     }
   }
+
+  // lowering
+  for(auto v_it=symbol_table.symbol_module_map.lower_bound(smv_module.name);
+      v_it!=symbol_table.symbol_module_map.upper_bound(smv_module.name);
+      v_it++)
+  {
+    auto &symbol = symbol_table.get_writeable_ref(v_it->second);
+    lower(symbol.type);
+    lower(symbol.value);
+  }
 }
 
 /*******************************************************************\