Fix out-of-bounds access in ExprManager

The size of `d_exprStatisticsVars` was `LAST_TYPE` which was not enough
because the INC_STAT macro tries to access
`d_exprStatisticsVars[LAST_TYPE]` in some cases, resulting in an
out-of-bounds access. Found bug with UBSan.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 53e16751e119538ccf5a109b90b66a9069b434c2..2dc3aebe5b3d55fd7dbaa84b9af6ce0376e355c4 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -75,7 +75,7 @@ ExprManager::ExprManager() :
   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
     d_exprStatistics[i] = NULL;
   }
-  for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+  for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
     d_exprStatisticsVars[i] = NULL;
   }
 #endif
@@ -84,7 +84,7 @@ ExprManager::ExprManager() :
 ExprManager::ExprManager(const Options& options) :
   d_nodeManager(new NodeManager(this, options)) {
 #ifdef CVC4_STATISTICS_ON
-  for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+  for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
     d_exprStatisticsVars[i] = NULL;
   }
   for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
@@ -106,7 +106,7 @@ ExprManager::~ExprManager() throw() {
         d_exprStatistics[i] = NULL;
       }
     }
-    for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+    for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
       if (d_exprStatisticsVars[i] != NULL) {
         d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatisticsVars[i]);
         delete d_exprStatisticsVars[i];

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 31c911736648c95d975959fecb68448dbdaa369c..f30b720dedc1ff5a01818a04f8404462667387aa 100644 (file)
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -57,7 +57,7 @@ private:
   NodeManager* d_nodeManager;
 
   /** Counts of expressions and variables created of a given kind */
-  IntStat* d_exprStatisticsVars[LAST_TYPE];
+  IntStat* d_exprStatisticsVars[LAST_TYPE + 1];
   IntStat* d_exprStatistics[kind::LAST_KIND];
 
   /**