From b06f9b64b55780de693ce9e1a38565f1e34cc5a0 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 3 Jan 2019 19:29:43 -0800 Subject: [PATCH] New C++ API: Add missing catch blocks for std::invalid_argument. (#2772) --- src/api/cvc4cpp.cpp | 240 +++++++++++++++++++++++++++++++------------- 1 file changed, 172 insertions(+), 68 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index dbbb4b535..d9a395d15 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1037,7 +1037,7 @@ Term Term::notTerm() const { return d_expr->notExpr(); } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -1049,7 +1049,7 @@ Term Term::andTerm(const Term& t) const { return d_expr->andExpr(*t.d_expr); } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -1061,7 +1061,7 @@ Term Term::orTerm(const Term& t) const { return d_expr->orExpr(*t.d_expr); } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -1073,7 +1073,7 @@ Term Term::xorTerm(const Term& t) const { return d_expr->xorExpr(*t.d_expr); } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -1085,7 +1085,7 @@ Term Term::eqTerm(const Term& t) const { return d_expr->eqExpr(*t.d_expr); } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -1097,7 +1097,7 @@ Term Term::impTerm(const Term& t) const { return d_expr->impExpr(*t.d_expr); } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -1109,7 +1109,7 @@ Term Term::iteTerm(const Term& then_t, const Term& else_t) const { return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr); } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -1926,7 +1926,17 @@ Term Solver::mkBoolean(bool val) const { return d_exprMgr->mkConst(val); } Term Solver::mkPi() const { - return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); + try + { + Term res = + d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + } + catch (const CVC4::TypeCheckingException& e) + { + throw CVC4ApiException(e.getMessage()); + } } template @@ -1938,7 +1948,7 @@ Term Solver::mkConstHelper(T t) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (CVC4::TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -1947,19 +1957,19 @@ Term Solver::mkConstHelper(T t) const /* Split out to avoid nested API calls (problematic with API tracing). */ Term Solver::mkRealFromStrHelper(std::string s) const { + /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP + * throws an std::invalid_argument exception. For consistency, we treat it + * as invalid. */ + CVC4_API_ARG_CHECK_EXPECTED(s != ".", s) + << "a string representing an integer, real or rational value."; try { - /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP - * throws an std::invalid_argument exception. For consistency, we treat it - * as invalid. */ - CVC4_API_ARG_CHECK_EXPECTED(s != ".", s) - << "a string representing an integer, real or rational value."; CVC4::Rational r = s.find('/') != std::string::npos ? CVC4::Rational(s) : CVC4::Rational::fromDecimal(s); return mkConstHelper(r); } - catch (std::invalid_argument& e) + catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } @@ -1978,42 +1988,98 @@ Term Solver::mkReal(const std::string& s) const Term Solver::mkReal(int32_t val) const { - return mkConstHelper(CVC4::Rational(val)); + try + { + return mkConstHelper(CVC4::Rational(val)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkReal(int64_t val) const { - return mkConstHelper(CVC4::Rational(val)); + try + { + return mkConstHelper(CVC4::Rational(val)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkReal(uint32_t val) const { - return mkConstHelper(CVC4::Rational(val)); + try + { + return mkConstHelper(CVC4::Rational(val)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkReal(uint64_t val) const { - return mkConstHelper(CVC4::Rational(val)); + try + { + return mkConstHelper(CVC4::Rational(val)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkReal(int32_t num, int32_t den) const { - return mkConstHelper(CVC4::Rational(num, den)); + try + { + return mkConstHelper(CVC4::Rational(num, den)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkReal(int64_t num, int64_t den) const { - return mkConstHelper(CVC4::Rational(num, den)); + try + { + return mkConstHelper(CVC4::Rational(num, den)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkReal(uint32_t num, uint32_t den) const { - return mkConstHelper(CVC4::Rational(num, den)); + try + { + return mkConstHelper(CVC4::Rational(num, den)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkReal(uint64_t num, uint64_t den) const { - return mkConstHelper(CVC4::Rational(num, den)); + try + { + return mkConstHelper(CVC4::Rational(num, den)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkRegexpEmpty() const @@ -2025,7 +2091,7 @@ Term Solver::mkRegexpEmpty() const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2040,7 +2106,7 @@ Term Solver::mkRegexpSigma() const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2062,7 +2128,7 @@ Term Solver::mkSepNil(Sort sort) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2099,7 +2165,7 @@ Term Solver::mkUniverseSet(Sort sort) const // (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2109,7 +2175,14 @@ Term Solver::mkUniverseSet(Sort sort) const Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const { CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0"; - return mkConstHelper(CVC4::BitVector(size, val)); + try + { + return mkConstHelper(CVC4::BitVector(size, val)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkBitVector(uint32_t size, uint64_t val) const @@ -2120,14 +2193,14 @@ Term Solver::mkBitVector(uint32_t size, uint64_t val) const /* Split out to avoid nested API calls (problematic with API tracing). */ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const { + CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; + CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) + << "base 2, 10, or 16"; try { - CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; - CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) - << "base 2, 10, or 16"; return mkConstHelper(CVC4::BitVector(s, base)); } - catch (std::invalid_argument& e) + catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } @@ -2137,19 +2210,18 @@ Term Solver::mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const { + CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; + CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) + << "base 2, 10, or 16"; try { - CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string"; - CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s) - << "base 2, 10, or 16"; - Integer val(s, base); CVC4_API_CHECK(val.modByPow2(size) == val) << "Overflow in bitvector construction (specified bitvector size " << size << " too small to hold value " << s << ")"; return mkConstHelper(CVC4::BitVector(size, val)); } - catch (std::invalid_argument& e) + catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } @@ -2219,14 +2291,7 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const Term Solver::mkConst(RoundingMode rm) const { - try - { - return mkConstHelper(s_rmodes.at(rm)); - } - catch (std::invalid_argument& e) - { - throw CVC4ApiException(e.what()); - } + return mkConstHelper(s_rmodes.at(rm)); } Term Solver::mkConst(Kind kind, Sort arg) const @@ -2249,7 +2314,7 @@ Term Solver::mkConst(Kind kind, Sort arg) const return res; } } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2286,11 +2351,11 @@ Term Solver::mkConstFromStrHelper(Kind kind, std::string s) const // do not call getType(), for abstract values, type can not be computed // until it is substituted away } - catch (std::invalid_argument& e) + catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2348,12 +2413,23 @@ Term Solver::mkConstFromIntHelper(Kind kind, T a) const // do not call getType(), for abstract values, type can not be computed // until it is substituted away } - catch (TypeCheckingException& e) + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } } - return mkConstHelper(CVC4::Rational(a)); + try + { + return mkConstHelper(CVC4::Rational(a)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkConst(Kind kind, int32_t arg) const @@ -2385,28 +2461,56 @@ Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const { return mkBVFromIntHelper(arg1, arg2); } - return mkConstHelper(CVC4::Rational(arg1, arg2)); + try + { + return mkConstHelper(CVC4::Rational(arg1, arg2)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkConst(Kind kind, int32_t arg1, int32_t arg2) const { CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind) << "CONST_RATIONAL"; - return mkConstHelper(CVC4::Rational(arg1, arg2)); + try + { + return mkConstHelper(CVC4::Rational(arg1, arg2)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkConst(Kind kind, int64_t arg1, int64_t arg2) const { CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind) << "CONST_RATIONAL"; - return mkConstHelper(CVC4::Rational(arg1, arg2)); + try + { + return mkConstHelper(CVC4::Rational(arg1, arg2)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const { CVC4_API_KIND_CHECK_EXPECTED(kind == CONST_RATIONAL, kind) << "CONST_RATIONAL"; - return mkConstHelper(CVC4::Rational(arg1, arg2)); + try + { + return mkConstHelper(CVC4::Rational(arg1, arg2)); + } + catch (const std::invalid_argument& e) + { + throw CVC4ApiException(e.what()); + } } Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const @@ -2447,7 +2551,7 @@ Term Solver::mkVar(const std::string& symbol, Sort sort) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2462,7 +2566,7 @@ Term Solver::mkVar(Sort sort) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2477,7 +2581,7 @@ Term Solver::mkBoundVar(const std::string& symbol, Sort sort) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2492,7 +2596,7 @@ Term Solver::mkBoundVar(Sort sort) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2570,7 +2674,7 @@ Term Solver::mkTerm(Kind kind) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2585,7 +2689,7 @@ Term Solver::mkTerm(Kind kind, Sort sort) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2601,7 +2705,7 @@ Term Solver::mkTerm(Kind kind, Term child) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2619,7 +2723,7 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2641,7 +2745,7 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2666,7 +2770,7 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2682,7 +2786,7 @@ Term Solver::mkTerm(OpTerm opTerm, Term child) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2700,7 +2804,7 @@ Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2719,7 +2823,7 @@ Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } @@ -2741,7 +2845,7 @@ Term Solver::mkTerm(OpTerm opTerm, const std::vector& children) const (void)res.d_expr->getType(true); /* kick off type checking */ return res; } - catch (TypeCheckingException& e) + catch (const CVC4::TypeCheckingException& e) { throw CVC4ApiException(e.getMessage()); } -- 2.30.2