Skip to content

Commit

Permalink
New C++ API: Add checks for kind arguments. (cvc5#2369)
Browse files Browse the repository at this point in the history 
This should hopefully also take care of the open coverity issues for cvc4cpp.cpp.
  • Loading branch information
@aniemetz @4tXJ7f
aniemetz authored and 4tXJ7f committed Aug 24, 2018
1 parent 11a3420 commit 907cc0a
Show file tree
Hide file tree
Showing 2 changed files with 133 additions and 35 deletions.
161 changes: 126 additions & 35 deletions src/api/cvc4cpp.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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)
Expand Down Expand Up @@ -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)));
Expand All @@ -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)));
Expand All @@ -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)));
Expand All @@ -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)));
Expand All @@ -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)));
Expand All @@ -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)));
Expand All @@ -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>()));
}
Expand Down Expand Up @@ -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>());
Expand All @@ -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));
}

Expand All @@ -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())
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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)
{
Expand Down Expand Up @@ -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)
{
Expand Down
7 changes: 7 additions & 0 deletions src/api/cvc4cppkind.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 907cc0a

Please sign in to comment.