From ee85eb0e55ac8f7fd0e6bd74c8e449b5f881a14e Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 15 Mar 2021 10:40:31 -0700 Subject: [PATCH] New C++ Api: Comprehensive guards for member functions of Datatype classes. (#6141) --- src/api/checks.h | 71 +++++++++-- src/api/cvc4cpp.cpp | 295 ++++++++++++++++++++++++++++++++++++++++---- src/api/cvc4cpp.h | 44 +++++++ 3 files changed, 378 insertions(+), 32 deletions(-) diff --git a/src/api/checks.h b/src/api/checks.h index bc99825db..fe7b14653 100644 --- a/src/api/checks.h +++ b/src/api/checks.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file cvc4cpp.h +/*! \file checks.h ** \verbatim ** Top contributors (to current version): ** Aina Niemetz @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef CVC5__API__CHECKS_H -#define CVC5__API__CHECKS_H +#ifndef CVC4__API__CHECKS_H +#define CVC4__API__CHECKS_H namespace cvc4 { namespace api { @@ -134,24 +134,75 @@ namespace api { << "Invalid size of argument '" << #arg << "', expected " /** - * Check condition 'cond' for given argument 'arg' at given index. + * Check condition 'cond' for the argument at given index in container 'args'. * Argument 'what' identifies what is being checked (e.g., "term"). * Creates a stream to provide a message that identifies what was expected to * hold if condition is false. * Usage: - * CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(, "what", , ) - * << "message"; + * CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + * , "what", , ) << "message"; */ -#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \ +#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, args, idx) \ CVC4_PREDICT_TRUE(cond) \ ? (void)0 \ : OstreamVoider() \ & CVC4ApiExceptionStream().ostream() \ - << "Invalid " << what << " '" << arg << "' at index " << idx \ - << ", expected " + << "Invalid " << (what) << " in '" << #args << "' at index " \ + << (idx) << ", expected " /* -------------------------------------------------------------------------- */ -/* Solver checks. */ +/* Solver checks. */ +/* -------------------------------------------------------------------------- */ + +/** + * Solver check for member functions of classes other than class Solver. + * Check if given solver matches the solver object this object is associated + * with. + */ +#define CVC4_API_ARG_CHECK_SOLVER(what, arg) \ + CVC4_API_CHECK(this->d_solver == arg.d_solver) \ + << "Given " << (what) << " is not associated with the solver this " \ + << (what) \ + << " is " \ + "associated with"; + +/* -------------------------------------------------------------------------- */ +/* Sort checks. */ +/* -------------------------------------------------------------------------- */ + +/** + * Sort check for member functions of classes other than class Solver. + * Check if given sort is not null and associated with the solver object this + * Sort object is associated with. + */ +#define CVC4_API_CHECK_SORT(sort) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(sort); \ + CVC4_API_ARG_CHECK_SOLVER("sort", sort); \ + } while (0) + +/** + * Sort check for member functions of classes other than class Solver. + * Check if each sort in the given container of sorts is not null and + * associated with the solver object this Sort object is associated with. + */ +#define CVC4_API_CHECK_SORTS(sorts) \ + do \ + { \ + size_t i = 0; \ + for (const auto& s : sorts) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", s, sorts, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this->d_solver == s.d_solver, "sort", sorts, i) \ + << "a sort associated with the solver this sort is associated with"; \ + i += 1; \ + } \ + } while (0) + +/* -------------------------------------------------------------------------- */ +/* Checks for class Solver. */ /* -------------------------------------------------------------------------- */ /** Sort checks for member functions of class Solver. */ diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 06fe1e788..72fa55d6f 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2266,22 +2266,46 @@ void DatatypeConstructorDecl::addSelector(const std::string& name, const Sort& sort) { NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + CVC4_API_CHECK_SORT(sort); CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null range sort for selector"; + //////// all checks before this line d_ctor->addArg(name, *sort.d_type); + //////// + CVC4_API_TRY_CATCH_END; } void DatatypeConstructorDecl::addSelectorSelf(const std::string& name) { NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line d_ctor->addArgSelf(name); + //////// + CVC4_API_TRY_CATCH_END; +} + +bool DatatypeConstructorDecl::isNull() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return isNullHelper(); + //////// + CVC4_API_TRY_CATCH_END; } std::string DatatypeConstructorDecl::toString() const { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line std::stringstream ss; ss << *d_ctor; return ss.str(); + //////// + CVC4_API_TRY_CATCH_END; } std::ostream& operator<<(std::ostream& out, @@ -2298,6 +2322,8 @@ std::ostream& operator<<(std::ostream& out, return out; } +bool DatatypeConstructorDecl::isNullHelper() const { return d_ctor == nullptr; } + /* DatatypeDecl ------------------------------------------------------------- */ DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {} @@ -2345,37 +2371,66 @@ DatatypeDecl::~DatatypeDecl() void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor) { NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; + CVC4_API_ARG_CHECK_NOT_NULL(ctor); + CVC4_API_ARG_CHECK_SOLVER("datatype constructor declaration", ctor); + //////// all checks before this line d_dtype->addConstructor(ctor.d_ctor); + //////// + CVC4_API_TRY_CATCH_END; } size_t DatatypeDecl::getNumConstructors() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return d_dtype->getNumConstructors(); + //////// + CVC4_API_TRY_CATCH_END; } bool DatatypeDecl::isParametric() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return d_dtype->isParametric(); + //////// + CVC4_API_TRY_CATCH_END; } std::string DatatypeDecl::toString() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line std::stringstream ss; ss << *d_dtype; return ss.str(); + //////// + CVC4_API_TRY_CATCH_END; } std::string DatatypeDecl::getName() const { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return d_dtype->getName(); + //////// + CVC4_API_TRY_CATCH_END; } -bool DatatypeDecl::isNull() const { return isNullHelper(); } +bool DatatypeDecl::isNull() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return isNullHelper(); + //////// + CVC4_API_TRY_CATCH_END; +} std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) { @@ -2406,24 +2461,54 @@ DatatypeSelector::~DatatypeSelector() } } -std::string DatatypeSelector::getName() const { return d_stor->getName(); } +std::string DatatypeSelector::getName() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_stor->getName(); + //////// + CVC4_API_TRY_CATCH_END; +} Term DatatypeSelector::getSelectorTerm() const { - Term sel = Term(d_solver, d_stor->getSelector()); - return sel; + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return Term(d_solver, d_stor->getSelector()); + //////// + CVC4_API_TRY_CATCH_END; } Sort DatatypeSelector::getRangeSort() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return Sort(d_solver, d_stor->getRangeType()); + //////// + CVC4_API_TRY_CATCH_END; +} + +bool DatatypeSelector::isNull() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return isNullHelper(); + //////// + CVC4_API_TRY_CATCH_END; } std::string DatatypeSelector::toString() const { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line std::stringstream ss; ss << *d_stor; return ss.str(); + //////// + CVC4_API_TRY_CATCH_END; } std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor) @@ -2432,6 +2517,8 @@ std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor) return out; } +bool DatatypeSelector::isNullHelper() const { return d_stor == nullptr; } + /* DatatypeConstructor ------------------------------------------------------ */ DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr) @@ -2456,24 +2543,38 @@ DatatypeConstructor::~DatatypeConstructor() } } -std::string DatatypeConstructor::getName() const { return d_ctor->getName(); } +std::string DatatypeConstructor::getName() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_ctor->getName(); + //////// + CVC4_API_TRY_CATCH_END; +} Term DatatypeConstructor::getConstructorTerm() const { - Term ctor = Term(d_solver, d_ctor->getConstructor()); - return ctor; + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return Term(d_solver, d_ctor->getConstructor()); + //////// + CVC4_API_TRY_CATCH_END; } Term DatatypeConstructor::getSpecializedConstructorTerm( const Sort& retSort) const { NodeManagerScope scope(d_solver->getNodeManager()); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(d_ctor->isResolved()) << "Expected resolved datatype constructor"; CVC4_API_CHECK(retSort.isDatatype()) << "Cannot get specialized constructor type for non-datatype type " << retSort; - CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line NodeManager* nm = d_solver->getNodeManager(); Node ret = @@ -2491,34 +2592,62 @@ Term DatatypeConstructor::getSpecializedConstructorTerm( Term DatatypeConstructor::getTesterTerm() const { - Term tst = Term(d_solver, d_ctor->getTester()); - return tst; + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return Term(d_solver, d_ctor->getTester()); + //////// + CVC4_API_TRY_CATCH_END; } size_t DatatypeConstructor::getNumSelectors() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return d_ctor->getNumArgs(); + //////// + CVC4_API_TRY_CATCH_END; } DatatypeSelector DatatypeConstructor::operator[](size_t index) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return DatatypeSelector(d_solver, (*d_ctor)[index]); + //////// + CVC4_API_TRY_CATCH_END; } DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return getSelectorForName(name); + //////// + CVC4_API_TRY_CATCH_END; } DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return getSelectorForName(name); + //////// + CVC4_API_TRY_CATCH_END; } Term DatatypeConstructor::getSelectorTerm(const std::string& name) const { - DatatypeSelector sel = getSelector(name); - return sel.getSelectorTerm(); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return getSelector(name).getSelectorTerm(); + //////// + CVC4_API_TRY_CATCH_END; } DatatypeConstructor::const_iterator DatatypeConstructor::begin() const @@ -2600,13 +2729,28 @@ bool DatatypeConstructor::const_iterator::operator!=( return d_int_stors != other.d_int_stors || d_idx != other.d_idx; } +bool DatatypeConstructor::isNull() const +{ + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + return isNullHelper(); + //////// + CVC4_API_TRY_CATCH_END; +} + std::string DatatypeConstructor::toString() const { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line std::stringstream ss; ss << *d_ctor; return ss.str(); + //////// + CVC4_API_TRY_CATCH_END; } +bool DatatypeConstructor::isNullHelper() const { return d_ctor == nullptr; } + DatatypeSelector DatatypeConstructor::getSelectorForName( const std::string& name) const { @@ -2664,48 +2808,153 @@ Datatype::~Datatype() DatatypeConstructor Datatype::operator[](size_t idx) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds."; + //////// all checks before this line return DatatypeConstructor(d_solver, (*d_dtype)[idx]); + //////// + CVC4_API_TRY_CATCH_END; } DatatypeConstructor Datatype::operator[](const std::string& name) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return getConstructorForName(name); + //////// + CVC4_API_TRY_CATCH_END; } DatatypeConstructor Datatype::getConstructor(const std::string& name) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return getConstructorForName(name); + //////// + CVC4_API_TRY_CATCH_END; } Term Datatype::getConstructorTerm(const std::string& name) const { - DatatypeConstructor ctor = getConstructor(name); - return ctor.getConstructorTerm(); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return getConstructor(name).getConstructorTerm(); + //////// + CVC4_API_TRY_CATCH_END; } -std::string Datatype::getName() const { return d_dtype->getName(); } +std::string Datatype::getName() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_dtype->getName(); + //////// + CVC4_API_TRY_CATCH_END; +} size_t Datatype::getNumConstructors() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return d_dtype->getNumConstructors(); + //////// + CVC4_API_TRY_CATCH_END; } -bool Datatype::isParametric() const { return d_dtype->isParametric(); } -bool Datatype::isCodatatype() const { return d_dtype->isCodatatype(); } +bool Datatype::isParametric() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_dtype->isParametric(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Datatype::isTuple() const { return d_dtype->isTuple(); } +bool Datatype::isCodatatype() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_dtype->isCodatatype(); + //////// + CVC4_API_TRY_CATCH_END; +} + +bool Datatype::isTuple() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_dtype->isTuple(); + //////// + CVC4_API_TRY_CATCH_END; +} + +bool Datatype::isRecord() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_dtype->isRecord(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Datatype::isRecord() const { return d_dtype->isRecord(); } +bool Datatype::isFinite() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_dtype->isFinite(); + //////// + CVC4_API_TRY_CATCH_END; +} -bool Datatype::isFinite() const { return d_dtype->isFinite(); } -bool Datatype::isWellFounded() const { return d_dtype->isWellFounded(); } +bool Datatype::isWellFounded() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_dtype->isWellFounded(); + //////// + CVC4_API_TRY_CATCH_END; +} bool Datatype::hasNestedRecursion() const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line return d_dtype->hasNestedRecursion(); + //////// + CVC4_API_TRY_CATCH_END; +} + +bool Datatype::isNull() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return isNullHelper(); + //////// + CVC4_API_TRY_CATCH_END; } -std::string Datatype::toString() const { return d_dtype->getName(); } +std::string Datatype::toString() const +{ + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_dtype->getName(); + //////// + CVC4_API_TRY_CATCH_END; +} Datatype::const_iterator Datatype::begin() const { @@ -2811,6 +3060,8 @@ bool Datatype::const_iterator::operator!=( return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx; } +bool Datatype::isNullHelper() const { return d_dtype == nullptr; } + /* -------------------------------------------------------------------------- */ /* Grammar */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 968ed0522..5a1a75024 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1411,6 +1411,11 @@ class CVC4_PUBLIC DatatypeConstructorDecl */ void addSelectorSelf(const std::string& name); + /** + * @return true if this DatatypeConstructorDecl is a null declaration. + */ + bool isNull() const; + /** * @return a string representation of this datatype constructor declaration */ @@ -1425,6 +1430,12 @@ class CVC4_PUBLIC DatatypeConstructorDecl */ DatatypeConstructorDecl(const Solver* slv, const std::string& name); + /** + * Helper for isNull checks. This prevents calling an API function with + * CVC4_API_CHECK_NOT_NULL + */ + bool isNullHelper() const; + /** * The associated solver object. */ @@ -1576,6 +1587,11 @@ class CVC4_PUBLIC DatatypeSelector /** @return the range sort of this argument. */ Sort getRangeSort() const; + /** + * @return true if this DatatypeSelector is a null object + */ + bool isNull() const; + /** * @return a string representation of this datatype selector */ @@ -1590,6 +1606,12 @@ class CVC4_PUBLIC DatatypeSelector */ DatatypeSelector(const Solver* slv, const CVC4::DTypeSelector& stor); + /** + * Helper for isNull checks. This prevents calling an API function with + * CVC4_API_CHECK_NOT_NULL + */ + bool isNullHelper() const; + /** * The associated solver object. */ @@ -1688,6 +1710,11 @@ class CVC4_PUBLIC DatatypeConstructor */ Term getSelectorTerm(const std::string& name) const; + /** + * @return true if this DatatypeConstructor is a null object + */ + bool isNull() const; + /** * @return a string representation of this datatype constructor */ @@ -1805,6 +1832,12 @@ class CVC4_PUBLIC DatatypeConstructor */ DatatypeSelector getSelectorForName(const std::string& name) const; + /** + * Helper for isNull checks. This prevents calling an API function with + * CVC4_API_CHECK_NOT_NULL + */ + bool isNullHelper() const; + /** * The associated solver object. */ @@ -1901,6 +1934,11 @@ class CVC4_PUBLIC Datatype */ bool hasNestedRecursion() const; + /** + * @return true if this Datatype is a null object + */ + bool isNull() const; + /** * @return a string representation of this datatype */ @@ -2015,6 +2053,12 @@ class CVC4_PUBLIC Datatype */ DatatypeConstructor getConstructorForName(const std::string& name) const; + /** + * Helper for isNull checks. This prevents calling an API function with + * CVC4_API_CHECK_NOT_NULL + */ + bool isNullHelper() const; + /** * The associated solver object. */ -- 2.30.2