introduce SMV enumeration type

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>
@@ -82,8 +83,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 &);
@@ -141,6 +140,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); });
@@ -149,40 +150,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:
@@ -498,15 +465,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
@@ -556,36 +523,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);
+    auto &e_type1 = to_smv_enumeration_type(type1);
+    auto &e_type2 = to_smv_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());
-
-    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 "
@@ -868,10 +815,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)
@@ -1252,6 +1198,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);
@@ -1274,6 +1223,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:
@@ -1340,35 +1310,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))
-        {
-          // re-type the constant
-          expr.type() = type;
-          return;
-        }
-        else
+        // subset?
+        if(to_smv_enumeration_type(expr.type()).is_subset_of(e_type))
         {
-          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;
+          }
         }
       }
     }
@@ -1861,9 +1836,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);
@@ -1902,12 +1874,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);
+  }
 }
 
 /*******************************************************************\

src/smvlang/smv_types.cpp

@@ -0,0 +1,85 @@
+/*******************************************************************\
+
+Module: SMV Types
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "smv_types.h"
+
+#include <set>
+
+smv_enumeration_typet::smv_enumeration_typet(
+  const std::vector<irep_idt> &element_ids)
+  : typet(ID_smv_enumeration)
+{
+  auto &sub = elements_sub();
+  for(auto &element_id : element_ids)
+    sub.push_back(irept{element_id});
+}
+
+std::vector<irep_idt> smv_enumeration_typet::elements() const
+{
+  std::vector<irep_idt> result;
+
+  auto &elements_sub = find(ID_elements).get_sub();
+
+  result.reserve(elements_sub.size());
+
+  for(auto &e : elements_sub)
+    result.push_back(e.id());
+
+  return result;
+}
+
+bool smv_enumeration_typet::is_subset_of(
+  const smv_enumeration_typet &other) const
+{
+  // This is quadratic.
+  for(auto &element1 : elements())
+  {
+    bool found = false;
+    for(auto &element2 : other.elements())
+      if(element1 == element2)
+      {
+        found = true;
+        break;
+      }
+
+    if(!found)
+      return false;
+  }
+
+  return true;
+}
+
+smv_enumeration_typet type_union(
+  const smv_enumeration_typet &e_type1,
+  const smv_enumeration_typet &e_type2)
+{
+  if(e_type2.is_subset_of(e_type1))
+    return e_type1;
+
+  if(e_type1.is_subset_of(e_type2))
+    return e_type2;
+
+  // make union
+  std::set<irep_idt> enum_set;
+
+  for(auto &e : e_type1.elements())
+    enum_set.insert(e);
+
+  for(auto &e : e_type2.elements())
+    enum_set.insert(e);
+
+  // turn into vector
+  std::vector<irep_idt> elements;
+
+  elements.reserve(enum_set.size());
+
+  for(auto &e : enum_set)
+    elements.push_back(e);
+
+  return smv_enumeration_typet{std::move(elements)};
+}

src/smvlang/smv_types.h

@@ -0,0 +1,64 @@
+/*******************************************************************\
+
+Module: SMV Types
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_TYPES_H
+#define CPROVER_SMV_TYPES_H
+
+#include <util/type.h>
+
+/// The SMV enumerated type
+class smv_enumeration_typet : public typet
+{
+public:
+  smv_enumeration_typet() : typet(ID_smv_enumeration)
+  {
+  }
+
+  explicit smv_enumeration_typet(const std::vector<irep_idt> &);
+
+  bool is_subset_of(const smv_enumeration_typet &) const;
+
+  // the ordering does not matter; this makes a copy
+  std::vector<irep_idt> elements() const;
+
+  subt &elements_sub()
+  {
+    return add(ID_elements).get_sub();
+  }
+};
+
+/// compute the union of the given enumeration types
+smv_enumeration_typet
+type_union(const smv_enumeration_typet &, const smv_enumeration_typet &);
+
+/*! \brief Cast a generic typet to a \ref smv_enumeration_typet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * smv_enumeration_typet.
+ *
+ * \param type Source type
+ * \return Object of type \ref smv_enumeration_typet
+ *
+ * \ingroup gr_std_types
+*/
+inline const smv_enumeration_typet &to_smv_enumeration_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_smv_enumeration);
+  return static_cast<const smv_enumeration_typet &>(type);
+}
+
+/*! \copydoc to_smv_enumeration_type(const typet &)
+ * \ingroup gr_std_types
+*/
+inline smv_enumeration_typet &to_smv_enumeration_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_smv_enumeration);
+  return static_cast<smv_enumeration_typet &>(type);
+}
+
+#endif // CPROVER_SMV_TYPES_H