New C++ API: Add checks for kind arguments. (#2369)

This should hopefully also take care of the open coverity issues for cvc4cpp.cpp.

2 files changed, 133 insertions, 35 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 3bc8a5cf5..24c4ef833 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -609,6 +609,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
     };
 
 namespace {
+bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
+
 Kind intToExtKind(CVC4::Kind k)
 {
   auto it = s_kinds_internal.find(k);
@@ -630,6 +632,12 @@ CVC4::Kind extToIntKind(Kind k)
 }
 }  // namespace
 
+std::string kindToString(Kind k)
+{
+  return k == INTERNAL_KIND ? "INTERNAL_KIND"
+                            : CVC4::kind::kindToString(extToIntKind(k));
+}
+
 std::ostream& operator<<(std::ostream& out, Kind k)
 {
   switch (k)
@@ -1793,46 +1801,63 @@ Term Solver::mkBitVector(std::string& s, uint32_t base) const
 
 Term Solver::mkConst(RoundingMode rm) const
 {
-  // CHECK: kind == CONST_ROUNDINGMODE
   // CHECK: valid rm?
   return d_exprMgr->mkConst(s_rmodes.at(rm));
 }
 
 Term Solver::mkConst(Kind kind, Sort arg) const
 {
-  // CHECK: kind == EMPTYSET
+  PrettyCheckArgument(kind == EMPTYSET,
+                      kind,
+                      "Invalid kind '%s', expected EMPTY_SET",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::EmptySet(*arg.d_type));
 }
 
 Term Solver::mkConst(Kind kind, Sort arg1, int32_t arg2) const
 {
-  // CHECK: kind == UNINTERPRETED_CONSTANT
+  PrettyCheckArgument(kind == UNINTERPRETED_CONSTANT,
+                      kind,
+                      "Invalid kind '%s', expected UNINTERPRETED_CONSTANT",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::UninterpretedConstant(*arg1.d_type, arg2));
 }
 
 Term Solver::mkConst(Kind kind, bool arg) const
 {
-  // CHECK: kind == CONST_BOOLEAN
+  PrettyCheckArgument(kind == CONST_BOOLEAN,
+                      kind,
+                      "Invalid kind '%s', expected CONST_BOOLEAN",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst<bool>(arg);
 }
 
 Term Solver::mkConst(Kind kind, const char* arg) const
 {
-  // CHECK: kind == CONST_STRING
+  PrettyCheckArgument(kind == CONST_STRING,
+                      kind,
+                      "Invalid kind '%s', expected CONST_STRING",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::String(arg));
 }
 
 Term Solver::mkConst(Kind kind, const std::string& arg) const
 {
-  // CHECK: kind == CONST_STRING
+  PrettyCheckArgument(kind == CONST_STRING,
+                      kind,
+                      "Invalid kind '%s', expected CONST_STRING",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::String(arg));
 }
 
 Term Solver::mkConst(Kind kind, const char* arg1, uint32_t arg2) const
 {
-  // CHECK: kind == ABSTRACT_VALUE
-  //           || kind == CONST_RATIONAL
-  //           || kind == CONST_BITVECTOR
+  PrettyCheckArgument(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL
+                          || kind == CONST_BITVECTOR,
+                      kind,
+                      "Invalid kind '%s', expected ABSTRACT_VALUE or "
+                      "CONST_RATIONAL or CONST_BITVECTOR",
+                      kindToString(kind).c_str());
   if (kind == ABSTRACT_VALUE)
   {
     return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2)));
@@ -1846,9 +1871,12 @@ Term Solver::mkConst(Kind kind, const char* arg1, uint32_t arg2) const
 
 Term Solver::mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const
 {
-  // CHECK: kind == ABSTRACT_VALUE
-  //           || kind == CONST_RATIONAL
-  //           || kind == CONST_BITVECTOR
+  PrettyCheckArgument(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL
+                          || kind == CONST_BITVECTOR,
+                      kind,
+                      "Invalid kind '%s', expected ABSTRACT_VALUE or "
+                      "CONST_RATIONAL or CONST_BITVECTOR",
+                      kindToString(kind).c_str());
   if (kind == ABSTRACT_VALUE)
   {
     return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2)));
@@ -1862,9 +1890,12 @@ Term Solver::mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const
 
 Term Solver::mkConst(Kind kind, uint32_t arg) const
 {
-  // CHECK: kind == ABSTRACT_VALUE
-  //           || kind == CONST_RATIONAL
-  //           || kind == CONST_BITVECTOR
+  PrettyCheckArgument(kind == ABSTRACT_VALUE || kind == CONST_RATIONAL
+                          || kind == CONST_BITVECTOR,
+                      kind,
+                      "Invalid kind '%s', expected ABSTRACT_VALUE or "
+                      "CONST_RATIONAL or CONST_BITVECTOR",
+                      kindToString(kind).c_str());
   if (kind == ABSTRACT_VALUE)
   {
     return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
@@ -1878,8 +1909,11 @@ Term Solver::mkConst(Kind kind, uint32_t arg) const
 
 Term Solver::mkConst(Kind kind, int32_t arg) const
 {
-  // CHECK: kind == ABSTRACT_VALUE
-  //           || kind == CONST_RATIONAL
+  PrettyCheckArgument(
+      kind == ABSTRACT_VALUE || kind == CONST_RATIONAL,
+      kind,
+      "Invalid kind '%s', expected ABSTRACT_VALUE or CONST_RATIONAL",
+      kindToString(kind).c_str());
   if (kind == ABSTRACT_VALUE)
   {
     return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
@@ -1889,8 +1923,11 @@ Term Solver::mkConst(Kind kind, int32_t arg) const
 
 Term Solver::mkConst(Kind kind, int64_t arg) const
 {
-  // CHECK: kind == ABSTRACT_VALUE
-  //           || kind == CONST_RATIONAL
+  PrettyCheckArgument(
+      kind == ABSTRACT_VALUE || kind == CONST_RATIONAL,
+      kind,
+      "Invalid kind '%s', expected ABSTRACT_VALUE or CONST_RATIONAL",
+      kindToString(kind).c_str());
   if (kind == ABSTRACT_VALUE)
   {
     return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
@@ -1900,8 +1937,11 @@ Term Solver::mkConst(Kind kind, int64_t arg) const
 
 Term Solver::mkConst(Kind kind, uint64_t arg) const
 {
-  // CHECK: kind == ABSTRACT_VALUE
-  //           || kind == CONST_RATIONAL
+  PrettyCheckArgument(
+      kind == ABSTRACT_VALUE || kind == CONST_RATIONAL,
+      kind,
+      "Invalid kind '%s', expected ABSTRACT_VALUE or CONST_RATIONAL",
+      kindToString(kind).c_str());
   if (kind == ABSTRACT_VALUE)
   {
     return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
@@ -1911,38 +1951,56 @@ Term Solver::mkConst(Kind kind, uint64_t arg) const
 
 Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const
 {
-  // CHECK: kind == CONST_RATIONAL
+  PrettyCheckArgument(kind == CONST_RATIONAL,
+                      kind,
+                      "Invalid kind '%s', expected CONST_RATIONAL",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
 }
 
 Term Solver::mkConst(Kind kind, int32_t arg1, int32_t arg2) const
 {
-  // CHECK: kind == CONST_RATIONAL
+  PrettyCheckArgument(kind == CONST_RATIONAL,
+                      kind,
+                      "Invalid kind '%s', expected CONST_RATIONAL",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
 }
 
 Term Solver::mkConst(Kind kind, int64_t arg1, int64_t arg2) const
 {
-  // CHECK: kind == CONST_RATIONAL
+  PrettyCheckArgument(kind == CONST_RATIONAL,
+                      kind,
+                      "Invalid kind '%s', expected CONST_RATIONAL",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
 }
 
 Term Solver::mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const
 {
-  // CHECK: kind == CONST_RATIONAL
+  PrettyCheckArgument(kind == CONST_RATIONAL,
+                      kind,
+                      "Invalid kind '%s', expected CONST_RATIONAL",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
 }
 
 Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const
 {
-  // CHECK: kind == CONST_BITVECTOR
+  PrettyCheckArgument(kind == CONST_BITVECTOR,
+                      kind,
+                      "Invalid kind '%s', expected CONST_BITVECTOR",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
 }
 
 Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const
 {
-  // CHECK: kind == CONST_FLOATINGPOINT
   // CHECK: arg 3 is bit-vector constant
+  PrettyCheckArgument(kind == CONST_FLOATINGPOINT,
+                      kind,
+                      "Invalid kind '%s', expected CONST_FLOATINGPOINT",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(
       CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst<BitVector>()));
 }
@@ -1979,9 +2037,11 @@ Term Solver::mkBoundVar(Sort sort) const
 
 Term Solver::mkTerm(Kind kind) const
 {
-  // CHECK: kind == PI
-  //          || kind == REGEXP_EMPTY
-  //          || kind == REGEXP_SIGMA
+  PrettyCheckArgument(
+      kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA,
+      kind,
+      "Invalid kind '%s', expected PI or REGEXP_EMPTY or REGEXP_SIGMA",
+      kindToString(kind).c_str());
   if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
   {
     return d_exprMgr->mkExpr(extToIntKind(kind), std::vector<Expr>());
@@ -1992,8 +2052,10 @@ Term Solver::mkTerm(Kind kind) const
 
 Term Solver::mkTerm(Kind kind, Sort sort) const
 {
-  // CHECK: kind == SEP_NIL
-  //          || kind == UNIVERSE_SET
+  PrettyCheckArgument(kind == SEP_NIL || kind == UNIVERSE_SET,
+                      kind,
+                      "Invalid kind '%s'",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkNullaryOperator(*sort.d_type, extToIntKind(kind));
 }
 
@@ -2013,11 +2075,19 @@ Term Solver::mkTerm(Kind kind, Term child) const
   // n < minArity(kind) || n > maxArity(kind)
   // else "Exprs with kind %s must have at least %u children and "
   //      "at most %u children (the one under construction has %u)"
+  PrettyCheckArgument(isDefinedKind(kind),
+                      kind,
+                      "Invalid kind '%s'",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
 }
 
 Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
 {
+  PrettyCheckArgument(isDefinedKind(kind),
+                      kind,
+                      "Invalid kind '%s'",
+                      kindToString(kind).c_str());
   // CHECK:
   // NodeManager::fromExprManager(d_exprMgr)
   // == NodeManager::fromExprManager(child1.getExprManager())
@@ -2057,6 +2127,10 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
   // n < minArity(kind) || n > maxArity(kind)
   // else "Exprs with kind %s must have at least %u children and "
   //      "at most %u children (the one under construction has %u)"
+  PrettyCheckArgument(isDefinedKind(kind),
+                      kind,
+                      "Invalid kind '%s'",
+                      kindToString(kind).c_str());
   std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr};
   CVC4::Kind k = extToIntKind(kind);
   return kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
@@ -2080,6 +2154,10 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
   // 1 : 0); n < minArity(kind) || n > maxArity(kind) else "Exprs with kind %s
   // must have at least %u children and "
   //      "at most %u children (the one under construction has %u)"
+  PrettyCheckArgument(isDefinedKind(kind),
+                      kind,
+                      "Invalid kind '%s'",
+                      kindToString(kind).c_str());
   std::vector<Expr> echildren = termVectorToExprs(children);
   CVC4::Kind k = extToIntKind(kind);
   return kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren)
@@ -2204,19 +2282,28 @@ std::vector<Expr> Solver::termVectorToExprs(
 
 OpTerm Solver::mkOpTerm(Kind kind, Kind k)
 {
-  // CHECK: kind == CHAIN_OP
+  PrettyCheckArgument(kind == CHAIN_OP,
+                      kind,
+                      "Invalid kind '%s', expected CHAIN_OP",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::Chain(extToIntKind(k)));
 }
 
 OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg)
 {
-  // CHECK:
-  // kind == RECORD_UPDATE_OP
+  PrettyCheckArgument(kind == RECORD_UPDATE_OP,
+                      kind,
+                      "Invalid kind '%s', expected RECORD_UPDATE_OP",
+                      kindToString(kind).c_str());
   return d_exprMgr->mkConst(CVC4::RecordUpdate(arg));
 }
 
 OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
 {
+  PrettyCheckArgument(isDefinedKind(kind),
+                      kind,
+                      "Invalid kind '%s'",
+                      kindToString(kind).c_str());
   OpTerm res;
   switch (kind)
   {
@@ -2263,6 +2350,10 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
 
 OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
 {
+  PrettyCheckArgument(isDefinedKind(kind),
+                      kind,
+                      "Invalid kind '%s'",
+                      kindToString(kind).c_str());
   OpTerm res;
   switch (kind)
   {
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 0b5f0ad06..65affcad4 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -2314,6 +2314,13 @@ enum CVC4_PUBLIC Kind
 };
 
 /**
+ * Get the string representation of a given kind.
+ * @param k the kind
+ * @return the string representation of kind k
+ */
+std::string kindToString(Kind k) CVC4_PUBLIC;
+
+/**
  * Serialize a kind to given stream.
  * @param out the output stream
  * @param k the kind to be serialized to the given output stream