From: Andres Notzli <andres.noetzli@gmail.com>
Date: Wed, 27 Jul 2016 21:06:56 +0000 (-0700)
Subject: Fix out-of-bounds access in ExprManager
X-Git-Tag: cvc5-1.0.0~6040^2~14^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2db836a8d785cb4d3c7f364dc5a968b5f6394b5c;p=cvc5.git

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 53e16751e..2dc3aebe5 100644
--- 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 31c911736..f30b720de 100644
--- 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];
 
   /**