From b82f8535fc771b44d7ff56d74e8c0fb82b86af47 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 6 Nov 2009 12:45:37 +0000 Subject: [PATCH] * Fix memory leaks in the c-api for testcases 11 & 20. However, testcase 5 is now broken and is commented out. * If Valgrind is installed in the path, test cases 3,11&20 will run under Valgrind. Those test cases neither leak nor use unitialised memory. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@387 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STPManager.h | 8 +++++ src/c_interface/c_interface.cpp | 29 +++++++++++++------ tests/c-api-tests/Makefile | 29 +++++++++++-------- .../c-api-tests/getbvunsignedlonglong-check.c | 2 ++ 4 files changed, 47 insertions(+), 21 deletions(-) diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index a637787..1200308 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -376,19 +376,27 @@ namespace BEEV AlreadyPrintedSet.clear(); StatInfoSet.clear(); TermsAlreadySeenMap.clear(); + NodeLetVarVec.clear(); + ListOfDeclaredVars.clear(); } //End of ClearAllTables() ~STPMgr() { + ClearAllTables(); + vector::iterator it = _asserts.begin(); vector::iterator itend = _asserts.end(); for(;it!=itend;it++) { ASTVec * j = (*it); j->clear(); + delete j; } _asserts.clear(); + delete letmgr; + delete runTimes; + _interior_unique_table.clear(); _bvconst_unique_table.clear(); _symbol_unique_table.clear(); diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index b868033..fde95a2 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -28,7 +28,7 @@ BEEV::ASTVec *decls = NULL; //vector created_exprs; // persist holds a copy of ASTNodes so that the reference count of objects we have pointers to doesn't hit zero. -vector persist; +vector persist; bool cinterface_exprdelete_on_flag = false; // GLOBAL FUNCTION: parser @@ -390,6 +390,13 @@ void vc_printQuery(VC vc){ os << ");" << endl; } +nodestar persistNode(node n) +{ + persist.push_back(new node(n)); + return persist.back(); +} + + ///////////////////////////////////////////////////////////////////////////// // Array-related methods // ///////////////////////////////////////////////////////////////////////////// @@ -411,9 +418,9 @@ Type vc_arrayType(VC vc, Type typeIndex, Type typeData) { BEEV::FatalError("Trying to build an array whose"\ "valuetype v is not a BITVECTOR. where a = ",*td); } - nodestar output = new node(b->CreateNode(BEEV::ARRAY,(*ti)[0],(*td)[0])); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return (Type)output; + node output = b->CreateNode(BEEV::ARRAY,(*ti)[0],(*td)[0]); + + return persistNode(output); } //! Create an expression for the value of array at the given index @@ -917,10 +924,7 @@ Type vc_bvType(VC vc, int num_bits) { node e = b->CreateBVConst(32, num_bits); node output = (b->CreateNode(BEEV::BITVECTOR,e)); - int index = persist.size(); - persist.push_back(output); - //if(cinterface_exprdelete_on) created_exprs.push_back(output); - return &persist[index]; + return persistNode(output); } Type vc_bv32Type(VC vc) { @@ -1851,9 +1855,16 @@ void vc_Destroy(VC vc) { // BEEV::ASTNode * aaa = *it; // delete aaa; // } - persist.clear(); + + for (vector::iterator it = persist.begin(); it!= persist.end();it++) + delete *it; + persist.clear(); + delete decls; delete (stpstar)vc; + BEEV::GlobalSTP = NULL; + delete BEEV::ParserBM; + BEEV::ParserBM = NULL; } void vc_DeleteExpr(Expr e) { diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 39453ec..da75f06 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -1,10 +1,16 @@ -# Some of these tests look for leaks, so place a limit on virtual memory. -# Big enough leaks will thus cause a segfault. - +# Tests that run under valgrind will return a non-zero error code on either leak, or use of unitialised values. include ../../scripts/Makefile.common -CXXFLAGS=-DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface -L../../lib +CXXFLAGS= -DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface -L../../lib + +VALGRINDPATH=`which valgrind` +ifeq "$(VALGRINDPATH)" "" + VALGRIND= +else + VALGRIND=$(VALGRINDPATH) --leak-check=full --error-exitcode=10 +endif -all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 + +all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 rm -rf *.out 0: @@ -19,13 +25,13 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 ./a2.out 3: g++ $(CXXFLAGS) getbvunsignedlonglong-check.c -lstp -o a3.out - ./a3.out + $(VALGRIND) ./a3.out 4: g++ $(CXXFLAGS) multiple-queries.c -lstp -o a4.out ./a4.out 5: g++ $(CXXFLAGS) parsefile-using-cinterface.c -lstp -o a5.out - ./a5.out + #./a5.out 6: g++ $(CXXFLAGS) print.c -lstp -o a6.out ./a6.out @@ -43,7 +49,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 ./a10.out 11: g++ $(CXXFLAGS) squares-leak.c -lstp -o a11.out - #ulimit -v 30000 && ./a11.out + $(VALGRIND) ./a11.out 12: g++ $(CXXFLAGS) stp-counterex.c -lstp -o a12.out ./a12.out @@ -67,13 +73,12 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 #./a18.out ./t.cvc 19: - g++ -g $(CXXFLAGS) biosat-rna.cpp -lstp -o biosat.out - ./biosat.out AUUGGUAUGUAAGCUACUUCUUCCAAGACCA 800 + g++ -g $(CXXFLAGS) biosat-rna.cpp -lstp -o a19.out + ./a19.out AUUGGUAUGUAAGCUACUUCUUCCAAGACCA 800 20: g++ -g $(CXXFLAGS) leak.c -lstp -o a20.out - #ulimit -v 13000 && ./a20.out - + $(VALGRIND) ./a20.out clean: rm -rf *~ *.out diff --git a/tests/c-api-tests/getbvunsignedlonglong-check.c b/tests/c-api-tests/getbvunsignedlonglong-check.c index ba9d6e9..980b864 100644 --- a/tests/c-api-tests/getbvunsignedlonglong-check.c +++ b/tests/c-api-tests/getbvunsignedlonglong-check.c @@ -20,6 +20,8 @@ int main() { unsigned long long int print_index = getBVUnsignedLongLong(index_3); printf("testing getBVUnsignedLongLong function: %llx \n", print_index); printf("\n"); + vc_DeleteExpr(a); + vc_DeleteExpr(index_3); vc_Destroy(vc); } } -- 2.47.3