'union' syntax support

doc/vs-cmurphi.rst

@@ -37,7 +37,25 @@ Type System
 -----------
 CMurphi supports real arithmetic using the ``real`` data type. Rumur does not
 support this type and there are no plans to implement this or any floating point
-support. Similarly, Rumur does not support the ``union`` or ``multiset`` types.
+support. Similarly, Rumur does not support the ``multiset`` type.
+
+Unions
+^^^^^^
+Models that use the ``union`` type can be parsed with librumur, but generation
+of a checker using ``rumur`` is not supported. Some of the Rumur tools fully
+support union types, e.g. ``murphi2xml``, but others reject models with union
+types, e.g. ``murphi2uclid``.
+
+CMurphi only supports unions of scalarset and enum types. librumur supports
+unions of any types, simple or complex, including recursive (unions of unions).
+In contrast to CMurphi, librumur allows union types with 0 or 1 members. A union
+type with 0 members is vacuous, in the sense that values of this type can only
+ever be ``undefined``.
+
+CMurphi requires the first argument to the ``ismember`` predicate to be a
+designator. librumur allows any expression. CMurphi requires the second argument
+to ``ismember`` to be a scalarset or enum type. librumur, in line with
+supporting unions of any types, allows the second argument to be any type.
 
 Assumptions
 -----------

librumur/include/rumur/Expr.h

@@ -676,6 +676,25 @@ struct RUMUR_API_WITH_RTTI Forall : public Expr {
   bool is_pure() const override;
 };
 
+struct RUMUR_API_WITH_RTTI IsMember : public Expr {
+
+  Ptr<Expr> peg;
+  Ptr<TypeExpr> hole;
+
+  IsMember(const Ptr<Expr> &peg_, const Ptr<TypeExpr> &hole_,
+           const location &loc_);
+  IsMember *clone() const override;
+
+  void visit(BaseTraversal &visitor) override;
+  void visit(ConstBaseTraversal &visitor) const override;
+
+  bool constant() const override;
+  Ptr<TypeExpr> type() const override;
+  mpz_class constant_fold() const override;
+  void to_stream(std::ostream &out) const override;
+  bool is_pure() const override;
+};
+
 struct RUMUR_API_WITH_RTTI IsUndefined : public UnaryExpr {
 
   IsUndefined(const Ptr<Expr> &expr_, const location &loc_);

librumur/include/rumur/TypeExpr.h

@@ -190,4 +190,22 @@ struct RUMUR_API_WITH_RTTI TypeExprID : public TypeExpr {
   bool constant() const override;
 };
 
+struct RUMUR_API_WITH_RTTI Union : public TypeExpr {
+  std::vector<Ptr<TypeExpr>> members;
+
+  Union(const std::vector<Ptr<TypeExpr>> &members_, const location &loc_);
+  Union *clone() const override;
+
+  void visit(BaseTraversal &visitor) override;
+  void visit(ConstBaseTraversal &visitor) const override;
+
+  mpz_class count() const override;
+  bool is_simple() const override;
+  void validate() const override;
+  mpz_class lower_bound() const override;
+  mpz_class upper_bound() const override;
+  void to_stream(std::ostream &out) const override;
+  bool constant() const override;
+};
+
 } // namespace rumur

librumur/include/rumur/indexer.h

@@ -52,6 +52,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal {
   void visit_if(If &n) override;
   void visit_ifclause(IfClause &n) override;
   void visit_implication(Implication &n) override;
+  void visit_ismember(IsMember &n) override;
   void visit_isundefined(IsUndefined &n) override;
   void visit_leq(Leq &n) override;
   void visit_lsh(Lsh &n) override;
@@ -85,6 +86,7 @@ class RUMUR_API_WITH_RTTI Indexer : public BaseTraversal {
   void visit_typedecl(TypeDecl &n) override;
   void visit_typeexprid(TypeExprID &n) override;
   void visit_undefine(Undefine &n) override;
+  void visit_union(Union &n) override;
   void visit_vardecl(VarDecl &n) override;
   void visit_while(While &n) override;
   void visit_xor(Xor &n) override;

librumur/include/rumur/traverse.h

@@ -98,6 +98,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal {
   virtual void visit_if(If &n) = 0;
   virtual void visit_ifclause(IfClause &n) = 0;
   virtual void visit_implication(Implication &n) = 0;
+  virtual void visit_ismember(IsMember &n) = 0;
   virtual void visit_isundefined(IsUndefined &n) = 0;
   virtual void visit_leq(Leq &n) = 0;
   virtual void visit_lsh(Lsh &n) = 0;
@@ -131,6 +132,7 @@ class RUMUR_API_WITH_RTTI BaseTraversal {
   virtual void visit_typedecl(TypeDecl &n) = 0;
   virtual void visit_typeexprid(TypeExprID &n) = 0;
   virtual void visit_undefine(Undefine &n) = 0;
+  virtual void visit_union(Union &n) = 0;
   virtual void visit_vardecl(VarDecl &n) = 0;
   virtual void visit_while(While &n) = 0;
   virtual void visit_xor(Xor &n) = 0;
@@ -184,6 +186,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal {
   void visit_if(If &n) override;
   void visit_ifclause(IfClause &n) override;
   void visit_implication(Implication &n) override;
+  void visit_ismember(IsMember &n) override;
   void visit_isundefined(IsUndefined &n) override;
   void visit_leq(Leq &n) override;
   void visit_lsh(Lsh &n) override;
@@ -217,6 +220,7 @@ class RUMUR_API_WITH_RTTI Traversal : public BaseTraversal {
   void visit_typedecl(TypeDecl &n) override;
   void visit_typeexprid(TypeExprID &n) override;
   void visit_undefine(Undefine &n) override;
+  void visit_union(Union &n) override;
   void visit_vardecl(VarDecl &n) override;
   void visit_while(While &n) override;
   void visit_xor(Xor &n) override;
@@ -262,6 +266,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal {
   virtual void visit_if(const If &n) = 0;
   virtual void visit_ifclause(const IfClause &n) = 0;
   virtual void visit_implication(const Implication &n) = 0;
+  virtual void visit_ismember(const IsMember &n) = 0;
   virtual void visit_isundefined(const IsUndefined &n) = 0;
   virtual void visit_leq(const Leq &n) = 0;
   virtual void visit_lsh(const Lsh &n) = 0;
@@ -295,6 +300,7 @@ class RUMUR_API_WITH_RTTI ConstBaseTraversal {
   virtual void visit_typedecl(const TypeDecl &n) = 0;
   virtual void visit_typeexprid(const TypeExprID &n) = 0;
   virtual void visit_undefine(const Undefine &n) = 0;
+  virtual void visit_union(const Union &n) = 0;
   virtual void visit_vardecl(const VarDecl &n) = 0;
   virtual void visit_while(const While &n) = 0;
   virtual void visit_xor(const Xor &n) = 0;
@@ -340,6 +346,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal {
   void visit_if(const If &n) override;
   void visit_ifclause(const IfClause &n) override;
   void visit_implication(const Implication &n) override;
+  void visit_ismember(const IsMember &n) override;
   void visit_isundefined(const IsUndefined &n) override;
   void visit_leq(const Leq &n) override;
   void visit_lsh(const Lsh &n) override;
@@ -373,6 +380,7 @@ class RUMUR_API_WITH_RTTI ConstTraversal : public ConstBaseTraversal {
   void visit_typedecl(const TypeDecl &n) override;
   void visit_typeexprid(const TypeExprID &n) override;
   void visit_undefine(const Undefine &n) override;
+  void visit_union(const Union &n) override;
   void visit_vardecl(const VarDecl &n) override;
   void visit_while(const While &n) override;
   void visit_xor(const Xor &n) override;
@@ -424,6 +432,7 @@ class RUMUR_API_WITH_RTTI ConstExprTraversal : public ConstBaseTraversal {
   void visit_typedecl(const TypeDecl &n) final;
   void visit_typeexprid(const TypeExprID &n) final;
   void visit_undefine(const Undefine &n) final;
+  void visit_union(const Union &n) final;
   void visit_vardecl(const VarDecl &n) final;
   void visit_while(const While &n) final;
 };
@@ -458,6 +467,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal {
   void visit_gt(const Gt &n) final;
   void visit_ifclause(const IfClause &n) final;
   void visit_implication(const Implication &n) final;
+  void visit_ismember(const IsMember &n) final;
   void visit_isundefined(const IsUndefined &n) final;
   void visit_leq(const Leq &n) final;
   void visit_lsh(const Lsh &n) final;
@@ -485,6 +495,7 @@ class RUMUR_API_WITH_RTTI ConstStmtTraversal : public ConstBaseTraversal {
   void visit_ternary(const Ternary &n) final;
   void visit_typedecl(const TypeDecl &n) final;
   void visit_typeexprid(const TypeExprID &n) final;
+  void visit_union(const Union &n) final;
   void visit_vardecl(const VarDecl &n) final;
   void visit_xor(const Xor &n) final;
 
@@ -524,6 +535,7 @@ class RUMUR_API_WITH_RTTI ConstTypeTraversal : public ConstBaseTraversal {
   void visit_if(const If &n) final;
   void visit_ifclause(const IfClause &n) final;
   void visit_implication(const Implication &n) final;
+  void visit_ismember(const IsMember &n) final;
   void visit_isundefined(const IsUndefined &n) final;
   void visit_leq(const Leq &n) final;
   void visit_lsh(const Lsh &n) final;

librumur/src/Expr.cc

@@ -1398,8 +1398,10 @@ void FunctionCall::validate() const {
     // callee’s handles are compatible
     if (!v->is_readonly() && isa<Range>(param_type)) {
       const Ptr<TypeExpr> arg_type = a_type->resolve();
-      assert(isa<Range>(arg_type) &&
-             "non-range considered type-compatible with range");
+      if (!isa<Range>(arg_type))
+        throw Error("non-range typed function call argument passed as "
+                    "range-typed var parameter",
+                    (*it)->loc);
 
       auto p = dynamic_cast<const Range &>(*param_type);
       auto a = dynamic_cast<const Range &>(*arg_type);
@@ -1672,6 +1674,34 @@ void Forall::to_stream(std::ostream &out) const {
 
 bool Forall::is_pure() const { return quantifier.is_pure() && expr->is_pure(); }
 
+IsMember::IsMember(const Ptr<Expr> &peg_, const Ptr<TypeExpr> &hole_,
+                   const location &loc_)
+    : Expr(loc_), peg(peg_), hole(hole_) {}
+
+IsMember *IsMember::clone() const { return new IsMember(*this); }
+
+void IsMember::visit(BaseTraversal &visitor) {
+  return visitor.visit_ismember(*this);
+}
+
+void IsMember::visit(ConstBaseTraversal &visitor) const {
+  return visitor.visit_ismember(*this);
+}
+
+bool IsMember::constant() const { return false; }
+
+Ptr<TypeExpr> IsMember::type() const { return Boolean; }
+
+mpz_class IsMember::constant_fold() const {
+  throw Error("ismember used in constant", loc);
+}
+
+void IsMember::to_stream(std::ostream &out) const {
+  out << "ismember(" << *peg << ", " << *hole << ')';
+}
+
+bool IsMember::is_pure() const { return peg->is_pure(); }
+
 IsUndefined::IsUndefined(const Ptr<Expr> &expr_, const location &loc_)
     : UnaryExpr(expr_, loc_) {}
 

librumur/src/TypeExpr.cc

@@ -147,6 +147,19 @@ static bool equal(const TypeExpr &t1, const TypeExpr &t2) {
     }
 
     void visit_typeexprid(const TypeExprID &n) final { dispatch(*n.referent); }
+
+    void visit_union(const Union &n) final {
+      if (auto u = dynamic_cast<const Union *>(t.get())) {
+        if (u->members.size() != n.members.size()) {
+          result = false;
+        } else {
+          for (size_t i = 0; i < n.members.size(); ++i)
+            result &= equal(*u->members[i], *n.members[i]);
+        }
+      } else {
+        result = false;
+      }
+    }
   };
 
   Equater eq(t1);
@@ -162,6 +175,22 @@ bool TypeExpr::coerces_to(const TypeExpr &other) const {
   if (isa<Range>(t1) && isa<Range>(t2))
     return true;
 
+  if (auto u = dynamic_cast<const Union *>(t2.get())) {
+    for (const Ptr<TypeExpr> &m : u->members) {
+      if (t1->coerces_to(*m))
+        return true;
+    }
+    return false;
+  }
+
+  if (auto u = dynamic_cast<const Union *>(t1.get())) {
+    for (const Ptr<TypeExpr> &m : u->members) {
+      if (m->coerces_to(*t2))
+        return true;
+    }
+    return false;
+  }
+
   return equal(*t1, *t2);
 }
 
@@ -477,4 +506,99 @@ bool TypeExprID::constant() const {
   return referent->value->constant();
 }
 
+Union::Union(const std::vector<Ptr<TypeExpr>> &members_, const location &loc_)
+    : TypeExpr(loc_), members(members_) {}
+
+Union *Union::clone() const { return new Union(*this); }
+
+void Union::visit(BaseTraversal &visitor) { visitor.visit_union(*this); }
+
+void Union::visit(ConstBaseTraversal &visitor) const {
+  visitor.visit_union(*this);
+}
+
+mpz_class Union::count() const {
+  mpz_class c = 1;
+  for (const Ptr<TypeExpr> &m : members)
+    c += m->count();
+  return c;
+}
+
+bool Union::is_simple() const {
+  for (const Ptr<TypeExpr> &m : members) {
+    if (!m->is_simple())
+      return false;
+  }
+  return true;
+}
+
+void Union::validate() const {
+  // In contrast to CMurphi, we treat unions containing 0 or 1 members as legal.
+  // We also allow a single type to appear multiple times within the union.
+  // There is no known practical use for most of these edge cases, but it
+  // simplifies work for generators of Murphi models.
+}
+
+mpz_class Union::lower_bound() const {
+  if (!is_simple())
+    throw Error("union is not a simple type and thus its lower bound cannot be "
+                "determined",
+                loc);
+
+  mpz_class bound;
+  bool set = false;
+  for (const Ptr<TypeExpr> &m : members) {
+    const mpz_class b = m->lower_bound();
+    if (!set || b < bound)
+      bound = b;
+    set = true;
+  }
+
+  if (!set)
+    bound = 0;
+
+  return bound;
+}
+
+mpz_class Union::upper_bound() const {
+  if (!is_simple())
+    throw Error("union is not a simple type and thus its upper bound cannot be "
+                "determined",
+                loc);
+
+  mpz_class bound;
+  bool set = false;
+  for (const Ptr<TypeExpr> &m : members) {
+    const mpz_class b = m->upper_bound();
+    if (!set || b > bound)
+      bound = b;
+    set = true;
+  }
+
+  if (!set)
+    bound = 0;
+
+  return bound;
+}
+
+void Union::to_stream(std::ostream &out) const {
+  out << "union {";
+  const char *separator = "";
+  for (const Ptr<TypeExpr> &m : members) {
+    out << separator << *m;
+    separator = ", ";
+  }
+  out << "}";
+}
+
+bool Union::constant() const {
+  for (const Ptr<TypeExpr> &m : members) {
+    if (!m->is_simple())
+      return false;
+    if (!m->constant())
+      return false;
+  }
+  return true;
+}
+
 } // namespace rumur