[Rodin-b-sharp-user] NewPP memory leak

[Jann R. <roe...@et...>]

Hi all,
I invested a couple of hours in trying to find the memory leak in NewPP.
While the exact reason and the necessary circumstances still remain a
mystery, I was able to detect it and perform an "emergency abort" when
the prover starts going crazy. I pasted the patch below.

In the patch the limit is set to 75000, I used to run it with 100000
which corresponds to a memory usage of about 700MB.

So the memory leak is not really a memory leak but the prover creating
too many instantations.

The strange thing is, that the problem only shows up when you run a
series of proofs and then always accurs on the same proof obligation. If
you try to prove just the offending proof obligation, everything works fine.

I'm sure there are better ways to detect the problem - but I think this
patch is still valuable.

Jann


Index:
src/org/eventb/internal/pp/core/provers/seedsearch/SeedSearchProver.java
===================================================================
---
src/org/eventb/internal/pp/core/provers/seedsearch/SeedSearchProver.java	(revision
8018)
+++
src/org/eventb/internal/pp/core/provers/seedsearch/SeedSearchProver.java	(working
copy)
@@ -42,6 +42,8 @@
 		System.out.println(message);
 	}

+	final int instantiationLImit = 75000;
+	
 	private SeedSearchManager manager = new SeedSearchManager();
 	private InstantiationInferrer inferrer;
 	private VariableContext context;
@@ -68,6 +70,10 @@
 				if (instantiatedClause != null) {
 					instantiatedClauses.add(instantiatedClause);
 				}
+				if (instantiatedClauses.size() > instantiationLImit) {
+					System.out.println("Set of instantiated clauses incomplete due to
overflow");
+					break;
+				}
 			}
 			if (!instantiatedClauses.isEmpty())
generatedClausesStack.add(instantiatedClauses);
 		}