From: Aina Niemetz Date: Fri, 24 Aug 2018 00:03:08 +0000 (-0700) Subject: New C++ API: Add checks for kind arguments. (#2369) X-Git-Tag: cvc5-1.0.0~4728 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=907cc0aceb81b9282f63367652f1f68bae4fb40e;p=cvc5.git New C++ API: Add checks for kind arguments. (#2369) This should hopefully also take care of the open coverity issues for cvc4cpp.cpp. --- 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 }; 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(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())); } @@ -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()); @@ -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 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& 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 echildren = termVectorToExprs(children); CVC4::Kind k = extToIntKind(kind); return kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren) @@ -2204,19 +2282,28 @@ std::vector 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 @@ -2313,6 +2313,13 @@ enum CVC4_PUBLIC Kind LAST_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