Changing ArrayStoreAll's constructor to delay allocation until it is done checking...

diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index c8e346e48752d1371407b1aa47f939bce9a9a7cc..05710a636b8c3bc5a11bc2c004baba37ba2e2269 100644 (file)
--- 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 6465a6301108a3f70d27fe43713ab7b9592a889e..981ed418d5f2298d8c5af76163255bc08714487c 100644 (file)
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -17,21 +17,19 @@
 #include <cxxtest/TestSuite.h>
 
 #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 */