Fix per-proof memory leak: clear JavaParserFacade cache on dispose

[unp1]

Intended Change

This bug was found thanks to stress testing the MT PRs on 128 core :-)

Repeatedly loading, proving and disposing the same obligation in a single JVM leaked roughly a
whole proof tree per cycle — about +56.6 MB per proof, growing linearly — so a disposed Proof
was never garbage-collected. This is long-standing (it is why RunAllProofs forks a JVM per group)
and is not multithreading-specific.

Root cause

javaparser's JavaParserFacade keeps a process-global cache:

private static final Map<TypeSolver, JavaParserFacade> instances = new WeakHashMap<>();
public static synchronized JavaParserFacade get(TypeSolver ts) {
    return instances.computeIfAbsent(ts.getRoot(), JavaParserFacade::new);
}

Each value (new JavaParserFacade(typeSolver)) strongly references its own weak key. A weak
key that stays strongly reachable from its own value can never become weakly reachable, so the
entry is never evicted. KeY's JavaParserFactory type solvers (DynamicTypeSolver,
LogicalTypeSolver) are non-static inner classes that transitively reference the owning Services,
so every disposed proof's entire proof tree was pinned through this cache.

The exact GC-root chain (found with the in-process root finder added here):

static JavaParserFacade.instances  (WeakHashMap)
  → table[].value → JavaParserFacade
     .typeSolver → CombinedTypeSolver → LogicalTypeSolver.this$0
        → JavaParserFactory → Services → Proof  (+ whole tree)

Fix

A single proof registers several short-lived type-solver keys (the DynamicTypeSolver wrapper
plus every CombinedTypeSolver produced by rebuild()), and the fork exposes no per-key removal, so
JavaParserFactory.dispose() drops the cache wholesale via the public
JavaParserFacade.clearInstances(). It synchronizes on the JavaParserFacade class monitor that
get() uses, because the backing map is a plain WeakHashMap and clearInstances() is itself
unsynchronized. The facade is a pure resolution cache that is only populated while parsing Java
during loading and is rebuilt lazily on the next get, so clearing it on dispose is safe.

Proof.dispose() invokes this via the new nullable accessor Services.getJavaServiceOrNull(), which
avoids the assertion in getJavaService() for pure first-order proofs.

Result

Measured with MtRetentionProbe (8 load/prove/dispose cycles of symmArray, -Xmx2g):

	Before	After
Slope	+56.6 MB / proof	+0.1 MB / proof
Live heap (rep 0 → rep 7)	130 → 526 MB	130 → 131 MB
Verdict	RETENTION	flat

All eight proofs still load, prove and close after the fix, confirming that clearing the cache
between proofs does not break symbol resolution.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• There are changes to the (Java) code
• There are changes to the deployment/CI infrastructure (gradle, github, ...)

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I added new test case(s) for new functionality.
• I have tested the feature as follows:

  ./gradlew :key.core:test --tests '*MtRetentionProbe' -PstressHeap=2g \
      -Dkey.mt.retention=true -Dkey.mt.retention.reps=8
  

  → verdict: flat (dispose releases per-proof state) (+0.1 MB/proof); before the fix the same
  command reports RETENTION (+56.6 MB/proof).
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

This change is orthogonal to the multithreading PRs (those merely mitigate the same leak for the
stress battery by forking one JVM per proof); this is the underlying fix.

Relationship to the JavaParser fork fix (wadoon/key-javaparser#7)

The true root cause is in our JavaParser fork and is addressed there by
wadoon/key-javaparser#7, which holds the JavaParserFacade.instances cache values weakly so the
self-cycle can no longer pin a TypeSolver. The two fixes are complementary:

• This PR works against the currently published org.key-project.proofjava artifact and forces
  immediate release on dispose(). It is the fix we can ship today.
• Fix memory leak: hold JavaParserFacade cache values weakly wadoon/key-javaparser#7 is the upstream cure: it makes the cache self-healing for every
  consumer (release happens lazily, a GC cycle or two after a proof is dropped).

What to do once wadoon/key-javaparser#7 is released and the JP_VERSION dependency is bumped:
this dispose()-time clearInstances() becomes belt-and-suspenders and can be relaxed. Concretely:

1. Bump JP_VERSION in the build to the fork release containing <deleted> #7 and confirm the leak stays flat
   (re-run MtRetentionProbe; it should remain flat without the clearInstances() call).

2. Then either:

   • remove JavaParserFactory.dispose() and its call in Proof.dispose() entirely (rely on the
     fork's weak values), or
   • keep a dispose() but switch it from the global clearInstances() to a targeted eviction of
     just this factory's type-solver entries — gentler for the IDE / multi-proof case, where clearing
     the whole shared cache on every proof disposal is wasteful.

   The global clearInstances() is used here only because the published fork exposes no per-key
   removal and a proof registers several short-lived type-solver keys; <deleted> #7 removes the need for it.
   Services.getJavaServiceOrNull() can stay regardless (it is a generally useful nullable accessor).

Two opt-in, test-only diagnostics are included as a regression guard and for future leak hunts, both
gated behind -Dkey.mt.retention=true so they never run in normal CI:

• MtRetentionProbe — quantifies live-heap growth across disposed proofs.
• HeapRootFinder — a MAT-free, in-process "path to GC roots" (enumerates loaded classes via the
  gcClassHistogram diagnostic command, BFS from static fields and every thread's ThreadLocalMap,
  excluding weak/soft referents). JFR's OldObjectSample only reached "VM Global / Global Object
  Handle", which is why this was needed.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.