[LFSC] Fix memory leaksfix_eqproof

8 files changed, 57 insertions, 11 deletions

diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp
index 9c7a70fe7..cf68edb87 100644
--- a/proofs/lfsc_checker/check.cpp
+++ b/proofs/lfsc_checker/check.cpp
@@ -353,6 +353,9 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
 	      sym->dec(); // the pivar->val reference
 	      if (create)
 	        return new CExpr(LAM, sym, range);
+              if (range) {
+                range->dec();
+              }
 	      sym->dec(); // the symbol table reference, otherwise in the new LAM
 	      return 0;
       }
@@ -830,6 +833,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
         if (mpq_set_str(num,v.c_str(),10) == -1)
 	        report_error("Error reading a numeral.");
         i = new RatExpr(num);
+        mpq_clear(num);
       }
       else
       {
@@ -837,6 +841,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL,
         if (mpz_init_set_str(num,v.c_str(),10) == -1)
 	        report_error("Error reading a numeral.");
         i = new IntExpr(num);
+        mpz_clear(num);
       }
     }
 
@@ -1374,6 +1379,14 @@ void cleanup() {
       p->dec();
     }
   }
+
+  //std::cout << Expr::to_free.size() << std::endl;
+  expr_ptr_set_t::iterator it, it_end;
+  for (it = Expr::to_free.begin(), it_end = Expr::to_free.end(); it != it_end; it++) {
+    (*it)->debug();
+    std::cout << (*it)->getrefcnt() << std::endl;
+  }
+  
 }
 
 void init() {
diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp
index 48ebc5578..6f6223c8d 100644
--- a/proofs/lfsc_checker/code.cpp
+++ b/proofs/lfsc_checker/code.cpp
@@ -538,6 +538,7 @@ Expr *read_code() {
 	        report_error("Error reading a mpq numeral.");
 
         Expr* e = new RatExpr( num );
+        mpq_clear(num);
         return e;
       }
       else
@@ -545,7 +546,9 @@ Expr *read_code() {
         mpz_t num;
         if (mpz_init_set_str(num,v.c_str(),10) == -1)
           report_error("Error reading a numeral.");
-        return new IntExpr(num);
+        Expr* e = new IntExpr(num);
+        mpz_clear(num);
+        return e;
       }
     }
     default:
@@ -973,7 +976,7 @@ Expr *check_code(Expr *_e) {
 
       if (!mtp)
         mtp = tp;
-      else
+      else {
         if (mtp != tp)
           report_error(string("Types for bodies of match cases or the default differ.")
                        +string("\n1. type for first case's body: ")
@@ -982,6 +985,7 @@ Expr *check_code(Expr *_e) {
                          : (string("\n2. type for the body of case for ")
                             +pat->toString()))
                        +string(": ")+tp->toString());
+      }
 
     }
 
@@ -1084,7 +1088,9 @@ Expr *run_code(Expr *_e) {
         mpz_cdiv_q(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n);
       r1->dec();
       r2->dec();
-      return new IntExpr(r);
+      Expr* result = new IntExpr(r);
+      mpz_clear(r);
+      return result;
     }
     else if( r1->getclass()==RAT_EXPR && r2->getclass()==RAT_EXPR )
     {
@@ -1098,7 +1104,9 @@ Expr *run_code(Expr *_e) {
         mpq_div(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n);
       r1->dec();
       r2->dec();
-      return new RatExpr(q);
+      Expr* result = new RatExpr(q);
+      mpq_clear(q);
+      return result;
     }
     else
     {
@@ -1117,14 +1125,18 @@ Expr *run_code(Expr *_e) {
       mpz_init(r);
       mpz_neg(r, ((IntExpr *)r1)->n);
       r1->dec();
-      return new IntExpr(r);
+      Expr* result = new IntExpr(r);
+      mpz_clear(r);
+      return result;
     }
     else if( r1->getclass() == RAT_EXPR ) {
       mpq_t q;
       mpq_init(q);
       mpq_neg(q, ((RatExpr *)r1)->n);
       r1->dec();
-      return new RatExpr(q);
+      Expr* result = new RatExpr(q);
+      mpq_clear(q);
+      return result;
     }
     else
     {
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index 8c8120edb..0ee164655 100644
--- a/proofs/lfsc_checker/expr.cpp
+++ b/proofs/lfsc_checker/expr.cpp
@@ -10,6 +10,7 @@ using namespace std;
 
 int HoleExpr::next_id = 0;
 int Expr::markedCount = 0;
+expr_ptr_set_t Expr::to_free;
 
 C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(CExpr,kids,32768);
 
@@ -50,6 +51,9 @@ void Expr::destroy(Expr *_e, bool dec_kids) {
   case INT_EXPR:
     delete (IntExpr *)_e;
     break;
+  case RAT_EXPR:
+    delete (RatExpr *)_e;
+    break;
   case SYMS_EXPR:  {
     SymSExpr *e = (SymSExpr *)_e;
     if (e->val && e->val->getop() != PROG) {
diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
index 3473a9eae..f5cf3d02a 100644
--- a/proofs/lfsc_checker/expr.h
+++ b/proofs/lfsc_checker/expr.h
@@ -103,12 +103,15 @@ protected:
 
   Expr(int _class, int _op)
     : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class)
-  { }
+  { /*Expr::to_free.insert(this);*/ }
 
   bool _free_in(Expr *x, expr_ptr_set_t *visited);
 
  public:
-  virtual ~Expr() {}
+  static expr_ptr_set_t to_free;
+  virtual ~Expr() {
+      Expr::to_free.erase(this);
+	}
 
   static int markedCount;
   inline Expr* followDefs();
@@ -143,8 +146,9 @@ protected:
     debugrefcnt(ref,DEC);
 #endif
     assert(ref >= 0);
-    if (ref == 0)
+    if (ref == 0) {
       destroy(this,dec_kids);
+    }
     else
       data = (ref << 9) | (data & 511);
   }
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 2fa659b51..521e19e88 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -71,6 +71,10 @@ private:
   ArrayProofPrinter d_proofPrinter;
 public:
   ProofArray(theory::eq::EqProof* pf) : d_reasonRow(0), d_reasonRow1(0), d_reasonExt(0), d_proofPrinter(), d_proof(pf)  {}
+  ~ProofArray() {
+    delete d_proof;
+  }
+  
   //it is simply an equality engine proof
   theory::eq::EqProof *d_proof;
   void toStream(std::ostream& out);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d74adbbe3..12e31ec1c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1163,6 +1163,13 @@ SmtEngine::~SmtEngine() throw() {
   try {
     shutdown();
 
+    PROOF(
+    std::vector<Command*>::const_iterator itg = d_defineCommands.begin();
+    for (; itg != d_defineCommands.end();  ++itg) {
+      delete (*itg);
+    }
+    );
+
     // global push/pop around everything, to ensure proper destruction
     // of context-dependent data structures
     d_context->popto(0);
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 2c7418a77..d8835277b 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2254,6 +2254,8 @@ void TheoryArrays::conflict(TNode a, TNode b) {
     }
 
     d_out->conflict(d_conflictNode, proof_array);
+  } else {
+    delete proof;
   }
 
   d_conflict = true;
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 7a6e0bdfc..943ffafe7 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -996,8 +996,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
         eqp->d_id = MERGED_THROUGH_CONSTANTS;
       } else if (eqp->num_children() == 1) {
         // The transitivity proof has just one child. Simplify.
-        EqProof* temp = eqp->get_child(0);
-        eqp->remove_all_children();
+        EqProof* temp = eqp->take_child(0);
+        eqp->discard_children();
         *eqp = *temp;
         delete temp;
       }