From 372a64559c8d8552f923fa4950aa2b7cef9d9bf3 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 15 Mar 2021 16:03:05 -0700 Subject: [PATCH] New C++ Api: Comprehensive guards for member functions of class Grammar. (#6148) --- src/api/checks.h | 122 ++++++++++++++++++++++++++++++++++++++++---- src/api/cvc4cpp.cpp | 75 +++++++++++++++++++-------- 2 files changed, 166 insertions(+), 31 deletions(-) diff --git a/src/api/checks.h b/src/api/checks.h index fe7b14653..aa2919d86 100644 --- a/src/api/checks.h +++ b/src/api/checks.h @@ -151,7 +151,7 @@ namespace api { << (idx) << ", expected " /* -------------------------------------------------------------------------- */ -/* Solver checks. */ +/* Solver checks. */ /* -------------------------------------------------------------------------- */ /** @@ -162,9 +162,7 @@ namespace api { #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"; + << "object is associated with"; /* -------------------------------------------------------------------------- */ /* Sort checks. */ @@ -173,7 +171,7 @@ namespace api { /** * 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. + * object is associated with. */ #define CVC4_API_CHECK_SORT(sort) \ do \ @@ -185,22 +183,124 @@ namespace api { /** * 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. + * associated with the solver object this object is associated with. */ -#define CVC4_API_CHECK_SORTS(sorts) \ +#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 object is associated " \ + "with"; \ + i += 1; \ + } \ + } while (0) + +/* -------------------------------------------------------------------------- */ +/* Term checks. */ +/* -------------------------------------------------------------------------- */ + +/** + * Term check for member functions of classes other than class Solver. + * Check if given term is not null and associated with the solver object this + * object is associated with. + */ +#define CVC4_API_CHECK_TERM(term) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(term); \ + CVC4_API_ARG_CHECK_SOLVER("term", term); \ + } while (0) + +/** + * Term check for member functions of classes other than class Solver. + * Check if each term in the given container of terms is not null and + * associated with the solver object this object is associated with. + */ +#define CVC4_API_CHECK_TERMS(terms) \ + do \ + { \ + size_t i = 0; \ + for (const auto& s : terms) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", s, terms, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this->d_solver == s.d_solver, "term", terms, i) \ + << "a term associated with the solver this object is associated " \ + "with"; \ + i += 1; \ + } \ + } while (0) + +/** + * Term check for member functions of classes other than class Solver. + * Check if each term and sort in the given map (which maps terms to sorts) is + * not null and associated with the solver object this object is associated + * with. + */ +#define CVC4_API_CHECK_TERMS_MAP(map) \ + do \ + { \ + size_t i = 0; \ + for (const auto& p : map) \ + { \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", p.first, map, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this->d_solver == p.first.d_solver, "term", map, i) \ + << "a term associated with the solver this object is associated " \ + "with"; \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", p.second, map, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ + this->d_solver == p.second.d_solver, "sort", map, i) \ + << "a sort associated with the solver this object is associated " \ + "with"; \ + i += 1; \ + } \ + } while (0) + +/** + * Term check for member functions of classes other than class Solver. + * Check if each term in the given container is not null, associated with the + * solver object this object is associated with, and of the given sort. + */ +#define CVC4_API_CHECK_TERMS_WITH_SORT(terms, sort) \ do \ { \ size_t i = 0; \ - for (const auto& s : sorts) \ + for (const auto& t : terms) \ { \ - CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", s, sorts, i); \ + CVC4_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, 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"; \ + this->d_solver == t.d_solver, "term", terms, i) \ + << "a term associated with the solver this object is associated " \ + "with"; \ + CVC4_API_CHECK(t.getSort() == sort) \ + << "Expected term with sort " << sort << " at index " << i << " in " \ + << #terms; \ i += 1; \ } \ } while (0) +/* -------------------------------------------------------------------------- */ +/* DatatypeDecl checks. */ +/* -------------------------------------------------------------------------- */ + +/** + * DatatypeDecl check for member functions of classes other than class Solver. + * Check if given datatype declaration is not null and associated with the + * solver object this DatatypeDecl object is associated with. + */ +#define CVC4_API_CHECK_DTDECL(decl) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(decl); \ + CVC4_API_ARG_CHECK_SOLVER("datatype declaration", decl); \ + } while (0) + /* -------------------------------------------------------------------------- */ /* Checks for class Solver. */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index cbf576deb..933177783 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3121,68 +3121,71 @@ Grammar::Grammar(const Solver* slv, void Grammar::addRule(const Term& ntSymbol, const Term& rule) { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing " "it as an argument to synthFun/synthInv"; - CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol); - CVC4_API_ARG_CHECK_NOT_NULL(rule); + CVC4_API_CHECK_TERM(ntSymbol); + CVC4_API_CHECK_TERM(rule); CVC4_API_ARG_CHECK_EXPECTED( d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol) << "ntSymbol to be one of the non-terminal symbols given in the " "predeclaration"; CVC4_API_CHECK(ntSymbol.d_node->getType() == rule.d_node->getType()) << "Expected ntSymbol and rule to have the same sort"; - + //////// all checks before this line d_ntsToTerms[ntSymbol].push_back(rule); + //////// + CVC4_API_TRY_CATCH_END; } void Grammar::addRules(const Term& ntSymbol, const std::vector& rules) { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing " "it as an argument to synthFun/synthInv"; - CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol); + CVC4_API_CHECK_TERM(ntSymbol); + CVC4_API_CHECK_TERMS_WITH_SORT(rules, ntSymbol.getSort()); CVC4_API_ARG_CHECK_EXPECTED( d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol) << "ntSymbol to be one of the non-terminal symbols given in the " "predeclaration"; - - for (size_t i = 0, n = rules.size(); i < n; ++i) - { - CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( - !rules[i].isNull(), "parameter rule", rules[i], i) - << "non-null term"; - CVC4_API_CHECK(ntSymbol.d_node->getType() == rules[i].d_node->getType()) - << "Expected ntSymbol and rule at index " << i - << " to have the same sort"; - } - + //////// all checks before this line d_ntsToTerms[ntSymbol].insert( d_ntsToTerms[ntSymbol].cend(), rules.cbegin(), rules.cend()); + //////// + CVC4_API_TRY_CATCH_END; } void Grammar::addAnyConstant(const Term& ntSymbol) { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing " "it as an argument to synthFun/synthInv"; - CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol); + CVC4_API_CHECK_TERM(ntSymbol); CVC4_API_ARG_CHECK_EXPECTED( d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol) << "ntSymbol to be one of the non-terminal symbols given in the " "predeclaration"; - + //////// all checks before this line d_allowConst.insert(ntSymbol); + //////// + CVC4_API_TRY_CATCH_END; } void Grammar::addAnyVariable(const Term& ntSymbol) { + CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing " "it as an argument to synthFun/synthInv"; - CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol); + CVC4_API_CHECK_TERM(ntSymbol); CVC4_API_ARG_CHECK_EXPECTED( d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol) << "ntSymbol to be one of the non-terminal symbols given in the " "predeclaration"; - + //////// all checks before this line d_allowVars.insert(ntSymbol); + //////// + CVC4_API_TRY_CATCH_END; } /** @@ -3217,6 +3220,8 @@ std::string join(Iterator first, Iterator last, Function f, std::string sep) std::string Grammar::toString() const { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line std::stringstream ss; ss << " (" // pre-declaration << join( @@ -3255,10 +3260,15 @@ std::string Grammar::toString() const << ')'; return ss.str(); + //////// + CVC4_API_TRY_CATCH_END; } Sort Grammar::resolve() { + CVC4_API_TRY_CATCH_BEGIN; + //////// all checks before this line + d_isResolved = true; Term bvl; @@ -3323,6 +3333,8 @@ Sort Grammar::resolve() // return is the first datatype return Sort(d_solver, datatypeTypes[0]); + //////// + CVC4_API_TRY_CATCH_END; } void Grammar::addSygusConstructorTerm( @@ -3330,6 +3342,12 @@ void Grammar::addSygusConstructorTerm( const Term& term, const std::unordered_map& ntsToUnres) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_DTDECL(dt); + CVC4_API_CHECK_TERM(term); + CVC4_API_CHECK_TERMS_MAP(ntsToUnres); + //////// all checks before this line + // At this point, we should know that dt is well founded, and that its // builtin sygus operators are well-typed. // Now, purify each occurrence of a non-terminal symbol in term, replace by @@ -3356,6 +3374,8 @@ void Grammar::addSygusConstructorTerm( } std::vector cargst = Sort::sortVectorToTypeNodes(cargs); dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst); + //////// + CVC4_API_TRY_CATCH_END; } Term Grammar::purifySygusGTerm( @@ -3364,6 +3384,13 @@ Term Grammar::purifySygusGTerm( std::vector& cargs, const std::unordered_map& ntsToUnres) const { + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_TERM(term); + CVC4_API_CHECK_TERMS(args); + CVC4_API_CHECK_SORTS(cargs); + CVC4_API_CHECK_TERMS_MAP(ntsToUnres); + //////// all checks before this line + std::unordered_map::const_iterator itn = ntsToUnres.find(term); if (itn != ntsToUnres.cend()) @@ -3406,12 +3433,18 @@ Term Grammar::purifySygusGTerm( } return Term(d_solver, nret); + //////// + CVC4_API_TRY_CATCH_END; } void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, const Sort& sort) const { - Assert(!sort.isNull()); + CVC4_API_TRY_CATCH_BEGIN; + CVC4_API_CHECK_DTDECL(dt); + CVC4_API_CHECK_SORT(sort); + //////// all checks before this line + // each variable of appropriate type becomes a sygus constructor in dt. for (unsigned i = 0, size = d_sygusVars.size(); i < size; i++) { @@ -3424,6 +3457,8 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, dt.d_dtype->addSygusConstructor(*v.d_node, ss.str(), cargs); } } + //////// + CVC4_API_TRY_CATCH_END; } std::ostream& operator<<(std::ostream& out, const Grammar& g) -- 2.30.2