From: Tim King Date: Mon, 7 Nov 2016 19:44:52 +0000 (-0800) Subject: Changing ArrayStoreAll's constructor to delay allocation until it is done checking... X-Git-Tag: cvc5-1.0.0~5997 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9608e29789960cd50704689d39e9a35d01be321;p=cvc5.git Changing ArrayStoreAll's constructor to delay allocation until it is done checking error conditions. This prevents a memory leak in exception throwing branches. --- diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index c8e346e48..05710a636 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -28,78 +28,72 @@ using namespace std; namespace CVC4 { -ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other) - : d_type(new ArrayType(other.getType())) - , d_expr(new Expr(other.getExpr())) {} - -ArrayStoreAll::~ArrayStoreAll() throw() { - delete d_expr; - delete d_type; -} - -ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other){ - (*d_type) = other.getType(); - (*d_expr) = other.getExpr(); - return *this; -} - -ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr) - throw(IllegalArgumentException) - : d_type(new ArrayType(type)) - , d_expr(new Expr(expr)) -{ - // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types +ArrayStoreAll::ArrayStoreAll(const ArrayType& type, + const Expr& expr) throw(IllegalArgumentException) + : d_type(NULL), d_expr(NULL) { + // this check is stronger than the assertion check in the expr manager that + // ArrayTypes are actually array types // because this check is done in production builds too PrettyCheckArgument( - type.isArray(), - type, + type.isArray(), type, "array store-all constants can only be created for array types, not `%s'", type.toString().c_str()); PrettyCheckArgument( - expr.getType().isComparableTo(type.getConstituentType()), - expr, + expr.getType().isComparableTo(type.getConstituentType()), expr, "expr type `%s' does not match constituent type of array type `%s'", - expr.getType().toString().c_str(), - type.toString().c_str()); + expr.getType().toString().c_str(), type.toString().c_str()); - PrettyCheckArgument( - expr.isConst(), - expr, - "ArrayStoreAll requires a constant expression"); + PrettyCheckArgument(expr.isConst(), expr, + "ArrayStoreAll requires a constant expression"); + + // Delay allocation until the checks above have been performed. If these fail, + // the memory for d_type and d_expr should not leak. The alternative is catch, + // delete and re-throw. + d_type = new ArrayType(type); + d_expr = new Expr(expr); } +ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other) + : d_type(new ArrayType(other.getType())), + d_expr(new Expr(other.getExpr())) {} -const ArrayType& ArrayStoreAll::getType() const throw() { - return *d_type; +ArrayStoreAll::~ArrayStoreAll() throw() { + delete d_expr; + delete d_type; } -const Expr& ArrayStoreAll::getExpr() const throw() { - return *d_expr; +ArrayStoreAll& ArrayStoreAll::operator=(const ArrayStoreAll& other) { + (*d_type) = other.getType(); + (*d_expr) = other.getExpr(); + return *this; } +const ArrayType& ArrayStoreAll::getType() const throw() { return *d_type; } + +const Expr& ArrayStoreAll::getExpr() const throw() { return *d_expr; } + bool ArrayStoreAll::operator==(const ArrayStoreAll& asa) const throw() { return getType() == asa.getType() && getExpr() == asa.getExpr(); } - bool ArrayStoreAll::operator<(const ArrayStoreAll& asa) const throw() { return (getType() < asa.getType()) || - (getType() == asa.getType() && getExpr() < asa.getExpr()); + (getType() == asa.getType() && getExpr() < asa.getExpr()); } bool ArrayStoreAll::operator<=(const ArrayStoreAll& asa) const throw() { return (getType() < asa.getType()) || - (getType() == asa.getType() && getExpr() <= asa.getExpr()); + (getType() == asa.getType() && getExpr() <= asa.getExpr()); } std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) { - return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() << ')'; + return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() + << ')'; } size_t ArrayStoreAllHashFunction::operator()(const ArrayStoreAll& asa) const { return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr()); } - -}/* CVC4 namespace */ +} /* CVC4 namespace */ diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index 6465a6301..981ed418d 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -17,21 +17,19 @@ #include #include "expr/array_store_all.h" +#include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" #include "expr/type.h" -#include "expr/expr.h" using namespace CVC4; using namespace std; class ArrayStoreAllBlack : public CxxTest::TestSuite { - ExprManager* d_em; ExprManagerScope* d_scope; -public: - + public: void setUp() { d_em = new ExprManager(); d_scope = new ExprManagerScope(*d_em); @@ -44,25 +42,42 @@ public: void testStoreAll() { Type usort = d_em->mkSort("U"); - ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()), d_em->mkConst(Rational(9, 2))); - ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkConst(UninterpretedConstant(usort, 0))); - ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()), d_em->mkConst(Rational(0))); - ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()), d_em->mkConst(Rational(0))); + ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()), + d_em->mkConst(Rational(9, 2))); + ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), + d_em->mkConst(UninterpretedConstant(usort, 0))); + ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()), + d_em->mkConst(Rational(0))); + ArrayStoreAll( + d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()), + d_em->mkConst(Rational(0))); } void testTypeErrors() { - // these two throw an AssertionException in assertions-enabled builds, and an IllegalArgumentException in production builds - TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(UninterpretedConstant(d_em->mkSort("U"), 0))) ); - TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))) ); + // these two throw an AssertionException in assertions-enabled builds, and + // an IllegalArgumentException in production builds + TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( + d_em->integerType(), + d_em->mkConst(UninterpretedConstant(d_em->mkSort("U"), 0)))); + TS_ASSERT_THROWS_ANYTHING( + ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2)))); - TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")), d_em->mkConst(Rational(9, 2))), IllegalArgumentException ); + TS_ASSERT_THROWS( + ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")), + d_em->mkConst(Rational(9, 2))), + IllegalArgumentException); } void testConstError() { Type usort = d_em->mkSort("U"); - TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort)) ); - TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkVar("x", d_em->integerType())) ); - TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)), d_em->mkConst(Rational(0)))) ); + TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( + d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort))); + TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll( + d_em->integerType(), d_em->mkVar("x", d_em->integerType()))); + TS_ASSERT_THROWS_ANYTHING( + ArrayStoreAll(d_em->integerType(), + d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)), + d_em->mkConst(Rational(0))))); } -};/* class ArrayStoreAllBlack */ +}; /* class ArrayStoreAllBlack */