Fix a couple of memory leaks that existed even if you did

vc_Destroy(): make a constant table used in the bitvector code static,
and delete temporary ASTNode objects in vc_simplify. A simple
createVC, build expression, simplify, destroy loop (test included) now
can run forever without leaking.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@60 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/c-api-tests/squares-leak.c b/c-api-tests/squares-leak.c
new file mode 100644 (file)
index 0000000..d151444
--- /dev/null
+++ b/c-api-tests/squares-leak.c
@@ -0,0 +1,27 @@
+/* g++ -I$(HOME)/stp/c_interface squares-leak.c -L$(HOME)/stp/lib -lstp -o squares-leak */
+/* then, */
+/* valgrind --leak-check=full --show-reachable=yes ./squares-leak */
+
+#include <stdio.h>
+#include "c_interface.h"
+
+int main(int argc, char **argv) {
+  unsigned int i;
+
+  /* Do some simple arithmetic by creating an expression involving
+     constants and then simplifying it. Since we create and destroy
+     a fresh VC each time, we shouldn't leak any memory. */
+  for (i = 1; i <= 100000; i++) {
+    VC vc = vc_createValidityChecker();
+    Expr arg = vc_bvConstExprFromLL(vc, 64, (unsigned long long)i);
+    Expr product = vc_bvMultExpr(vc, 64, arg, arg);
+    Expr simp = vc_simplify(vc, product);
+    unsigned long long j = getBVUnsignedLongLong(simp);
+    vc_DeleteExpr(arg);
+    vc_DeleteExpr(product);
+    vc_DeleteExpr(simp);
+    if (i % 10000 == 0)
+      printf("%u**2 = %llu\n", i, j);
+    vc_Destroy(vc);
+  }
+}

diff --git a/c_interface/c_interface.cpp b/c_interface/c_interface.cpp
index 518268081f4c62cd26ec2c9c7d6c4870ae6c1e0b..b8882d56b2c9394402b285e81e8a321d22fe0fc6 100644 (file)
--- a/c_interface/c_interface.cpp
+++ b/c_interface/c_interface.cpp
@@ -1328,19 +1328,21 @@ Expr vc_simplify(VC vc, Expr e) {
   nodestar a = (nodestar)e;
 
   if(BEEV::BOOLEAN_TYPE == a->GetType()) {
-    nodestar output = new node(b->SimplifyFormula_TopLevel(*a,false));
-    //if(cinterface_exprdelete_on) created_exprs.push_back(output);
+    nodestar round1 = new node(b->SimplifyFormula_TopLevel(*a,false));
     b->Begin_RemoveWrites = true;
-    output = new node(b->SimplifyFormula_TopLevel(*output,false));
+    nodestar output = new node(b->SimplifyFormula_TopLevel(*round1,false));
+    //if(cinterface_exprdelete_on) created_exprs.push_back(output);
     b->Begin_RemoveWrites = false;
+    delete round1;
     return output;    
   }
   else {
-    nodestar output = new node(b->SimplifyTerm(*a));
-    //if(cinterface_exprdelete_on) created_exprs.push_back(output);
+    nodestar round1 = new node(b->SimplifyTerm(*a));
     b->Begin_RemoveWrites = true;
-    output = new node(b->SimplifyTerm(*output));
+    nodestar output = new node(b->SimplifyTerm(*round1));
+    //if(cinterface_exprdelete_on) created_exprs.push_back(output);
     b->Begin_RemoveWrites = false;
+    delete round1;
     return output;
   }
 }

diff --git a/constantbv/constantbv.cpp b/constantbv/constantbv.cpp
index 65698981d950b8a431ee4831a9324a9c9f3a1d92..d874d43b8755c4b19eac528ccb5e2543389c6725 100644 (file)
--- a/constantbv/constantbv.cpp
+++ b/constantbv/constantbv.cpp
@@ -79,7 +79,7 @@ static unsigned int EXP10;    /* = largest possible power of 10 in signed int
     /* global bit mask table for fast access (set by "BitVector_Boot"): */
     /********************************************************************/
 
-static unsigned int *  BITMASKTAB;
+static unsigned int BITMASKTAB[sizeof(unsigned int) << 3];
 
     /*****************************/
     /* global macro definitions: */
@@ -300,10 +300,6 @@ ErrCode BitVector_Boot(void) {
     FACTOR = LOGBITS - 3;  /* ld(BITS / 8) = ld(BITS) - ld(8) = ld(BITS) - 3 */
     MSB = (LSB << MODMASK);
 
-    BITMASKTAB = (unsigned int * ) malloc((size_t) (BITS << FACTOR));
-
-    if (BITMASKTAB == NULL) return(ErrCode_Null);
-
     for ( sample = 0; sample < BITS; sample++ ) {
         BITMASKTAB[sample] = (LSB << sample);
     }