diff --git a/key.core/build.gradle b/key.core/build.gradle index 128931a290c..a0a0a14cc34 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -97,6 +97,21 @@ classes.dependsOn << generateSolverPropsList tasks.withType(Test) { enableAssertions = true + // Forward retention-probe knobs (see MtRetentionProbe) to the test JVM. + systemProperties += System.properties.findAll { it.key.toString().startsWith("key.mt.retention") } + if (project.hasProperty("stressHeap")) { + maxHeapSize = project.property("stressHeap") + } + if (System.getProperty("key.mt.retention.root") == "true") { + jvmArgs += [ + "--add-opens", "java.base/java.lang=ALL-UNNAMED", + "--add-opens", "java.base/java.lang.ref=ALL-UNNAMED", + "--add-opens", "java.base/java.util=ALL-UNNAMED", + "--add-opens", "java.base/java.util.concurrent=ALL-UNNAMED", + "--add-opens", "java.base/java.util.concurrent.locks=ALL-UNNAMED", + "--add-opens", "java.base/java.util.concurrent.atomic=ALL-UNNAMED" + ] + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java index c35f79a9552..b4a0970e06c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java @@ -473,6 +473,15 @@ public JavaService getJavaService() { return javaService; } + /** + * @return the {@link JavaService}, or {@code null} if Java was never activated for this + * {@link Services} (e.g. a pure first-order proof). Unlike {@link #getJavaService()} + * this never asserts and is safe to call during disposal. + */ + public @Nullable JavaService getJavaServiceOrNull() { + return javaService; + } + private JavaService activateJavaPath(@NonNull Path bootClassPath, @NonNull Collection libraryPaths, FileRepo fileRepo) { if (javaService != null && javaService.getBootClassPath().equals(bootClassPath) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java index 0c846670cca..061e521bcc3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java @@ -28,6 +28,7 @@ import com.github.javaparser.resolution.declarations.ResolvedReferenceTypeDeclaration; import com.github.javaparser.resolution.model.SymbolReference; import com.github.javaparser.symbolsolver.JavaSymbolSolver; +import com.github.javaparser.symbolsolver.javaparsermodel.JavaParserFacade; import com.github.javaparser.symbolsolver.resolution.typesolvers.CombinedTypeSolver; import com.google.common.cache.Cache; import com.google.common.cache.CacheBuilder; @@ -118,6 +119,38 @@ public TypeSolver getTypeSolver() { return typeSolver; } + /** + * Drops the global {@link JavaParserFacade} resolution cache so that this factory's + * {@link #typeSolver} (and through it the owning {@link Services} and its whole proof tree) can + * be garbage-collected once the proof is disposed. + * + *

+ * {@link JavaParserFacade} keeps a {@code static WeakHashMap} + * ({@code JavaParserFacade.instances}) whose value strongly references its own + * key: each value is created as {@code new JavaParserFacade(typeSolver)} and stores + * that very type solver. A weak key that stays strongly reachable from its own value can never + * become weakly reachable, so the entry is never evicted. Since our type solvers transitively + * reference the owning {@link Services}, every disposed proof would otherwise be retained + * forever through this cache — a long-standing, proof-sized memory leak. + * + *

+ * A single proof registers several short-lived type-solver keys (the {@code DynamicTypeSolver} + * wrapper plus every {@code CombinedTypeSolver} produced by {@code rebuild()}), and the fork + * exposes no per-key removal, so the only complete remedy is to drop the cache wholesale via + * the + * public {@link JavaParserFacade#clearInstances()}. This is safe: the facade is a pure + * resolution cache that is only populated while parsing Java during loading and is rebuilt + * lazily on the next {@code get}. We synchronize on the same monitor + * {@code JavaParserFacade.get} + * uses, because the backing map is a plain {@link java.util.WeakHashMap} and + * {@code clearInstances()} is itself unsynchronized. + */ + public void dispose() { + synchronized (JavaParserFacade.class) { + JavaParserFacade.clearInstances(); + } + } + public JavaSymbolSolver getSymbolSolver() { return symbolResolver; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java index 5e1ecaa95ec..3e504851cf8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java @@ -278,6 +278,13 @@ public void dispose() { // Do required cleanup if (getServices() != null) { getServices().getSpecificationRepository().removeProof(this); + // Drop the global JavaParserFacade resolution cache. It is a WeakHashMap whose values + // strongly reference their own (weak) keys, so without this the proof's Services - and + // thus the whole proof tree - would leak through it. See JavaParserFactory#dispose. + var javaService = getServices().getJavaServiceOrNull(); + if (javaService != null) { + javaService.getProgramFactory().dispose(); + } } if (localMgt != null) { localMgt.removeProofListener(); // This is strongly required because the listener is diff --git a/key.core/src/test/java/de/uka/ilkd/key/prover/mt/HeapRootFinder.java b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/HeapRootFinder.java new file mode 100644 index 00000000000..2fef257f5cb --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/HeapRootFinder.java @@ -0,0 +1,290 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.prover.mt; + +import java.lang.management.ManagementFactory; +import java.lang.reflect.Array; +import java.lang.reflect.Field; +import java.lang.reflect.Modifier; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.IdentityHashMap; +import java.util.List; + +/** + * In-process, MAT-free "path to GC roots" finder. Seeds a breadth-first search from the static + * fields of every loaded class (discovered via the {@code gcClassHistogram} diagnostic command) and + * walks the object graph by reflection until it reaches a given target object, then prints the + * shortest static-rooted reference chain. Used by {@link MtRetentionProbe} to name the exact static + * field/cache pinning a disposed {@code Proof}. + * + *

+ * The target is held only in a stack local of the caller, never in a static or in any field + * reachable + * from a static, so the only chain this search can find is the genuine leak path. + */ +final class HeapRootFinder { + + private HeapRootFinder() {} + + /** edge to the object that referenced this one, plus a human label for the edge. */ + private record Edge(Object parent, String label) { + } + + static void reportPath(Object target) { + System.out.println("[root] searching for static path to " + brief(target)); + IdentityHashMap parent = new IdentityHashMap<>(); + ArrayDeque queue = new ArrayDeque<>(); + + // ---- seed from static fields of every loaded class ---- + int seeded = 0; + for (String cn : loadedClassNames()) { + Class c; + try { + c = Class.forName(cn, false, HeapRootFinder.class.getClassLoader()); + } catch (Throwable t) { + continue; + } + for (Field f : declaredFieldsSafe(c)) { + if (!Modifier.isStatic(f.getModifiers()) || f.getType().isPrimitive()) { + continue; + } + Object v = readStatic(f); + if (v == null) { + continue; + } + if (parent.containsKey(v)) { + continue; + } + parent.put(v, new Edge(null, c.getName() + "." + f.getName())); + if (v == target) { + printChain(parent, target); + return; + } + queue.add(v); + seeded++; + } + } + System.out.println("[root] seeded " + seeded + " static roots"); + + // ---- seed from live threads and their thread-locals ---- + int threadSeeds = 0; + for (Thread t : Thread.getAllStackTraces().keySet()) { + for (Object v : threadRoots(t)) { + if (v == null || parent.containsKey(v)) { + continue; + } + parent.put(v, new Edge(null, "Thread[" + t.getName() + "] threadLocal/field")); + if (v == target) { + printChain(parent, target); + return; + } + queue.add(v); + threadSeeds++; + } + } + System.out.println( + "[root] seeded " + threadSeeds + " thread roots; walking graph..."); + + // ---- BFS over the object graph ---- + long visited = 0; + while (!queue.isEmpty()) { + Object cur = queue.poll(); + visited++; + for (Edge e : children(cur)) { + Object child = e.parent(); // here Edge.parent holds the child value + if (child == null || parent.containsKey(child)) { + continue; + } + parent.put(child, new Edge(cur, e.label())); + if (child == target) { + System.out.println("[root] found after visiting " + visited + " objects"); + printChain(parent, target); + return; + } + if (traversable(child)) { + queue.add(child); + } + } + } + System.out.println("[root] NO static path found after visiting " + visited + + " objects (target is not statically reachable, or is held by a thread/JNI root)"); + } + + /** Returns the outgoing references of {@code o} as (child, label) pairs (reusing Edge). */ + private static List children(Object o) { + List out = new ArrayList<>(); + Class c = o.getClass(); + if (c.isArray()) { + if (!c.getComponentType().isPrimitive()) { + int n = Array.getLength(o); + for (int i = 0; i < n; i++) { + Object v = Array.get(o, i); + if (v != null) { + out.add(new Edge(v, "[" + i + "]")); + } + } + } + return out; + } + boolean isRef = o instanceof java.lang.ref.Reference; + for (Class k = c; k != null && k != Object.class; k = k.getSuperclass()) { + for (Field f : declaredFieldsSafe(k)) { + if (Modifier.isStatic(f.getModifiers()) || f.getType().isPrimitive()) { + continue; + } + // Exclude weak/soft/phantom edges: only report a strong retention path. + if (isRef && f.getName().equals("referent")) { + continue; + } + Object v = readInstance(f, o); + if (v != null) { + out.add(new Edge(v, "." + f.getName())); + } + } + } + return out; + } + + /** Skip walking through huge value-type fan-outs that can't be a short root path. */ + private static boolean traversable(Object o) { + return !(o instanceof String) && !(o instanceof Number) && !(o instanceof Boolean) + && !(o instanceof Character) && !(o instanceof Class); + } + + private static void printChain(IdentityHashMap parent, Object target) { + ArrayList chain = new ArrayList<>(); + Object node = target; + Edge e = parent.get(node); + chain.add(brief(node)); + while (e != null && e.parent() != null) { + chain.add(e.label() + " -> " + brief(e.parent())); + node = e.parent(); + e = parent.get(node); + } + if (e != null) { + chain.add("[static root] " + e.label()); + } + System.out.println("[root] ===== PATH TO GC ROOT (root first) ====="); + for (int i = chain.size() - 1; i >= 0; i--) { + System.out.println("[root] " + chain.get(i)); + } + } + + private static String brief(Object o) { + if (o == null) { + return "null"; + } + String cn = o.getClass().getName(); + String extra = ""; + try { + if (o.getClass().isArray()) { + extra = "[len=" + Array.getLength(o) + "]"; + } + } catch (Throwable ignore) { + // ignore + } + return cn + "@" + Integer.toHexString(System.identityHashCode(o)) + extra; + } + + private static Field[] declaredFieldsSafe(Class c) { + try { + return c.getDeclaredFields(); + } catch (Throwable t) { + return new Field[0]; + } + } + + private static Object readStatic(Field f) { + try { + f.setAccessible(true); + return f.get(null); + } catch (Throwable t) { + return null; + } + } + + private static Object readInstance(Field f, Object o) { + try { + f.setAccessible(true); + return f.get(o); + } catch (Throwable t) { + return null; + } + } + + /** ThreadLocal values + non-primitive instance fields of a thread (its target, locals map). */ + private static List threadRoots(Thread t) { + List out = new ArrayList<>(); + // instance fields of the Thread object itself (e.g. the Runnable target) + for (Field f : declaredFieldsSafe(Thread.class)) { + if (Modifier.isStatic(f.getModifiers()) || f.getType().isPrimitive()) { + continue; + } + Object v = readInstance(f, t); + if (v != null) { + out.add(v); + } + } + // ThreadLocalMap entries (both thread-local and inheritable) + for (String mapField : new String[] { "threadLocals", "inheritableThreadLocals" }) { + try { + Field f = Thread.class.getDeclaredField(mapField); + f.setAccessible(true); + Object map = f.get(t); + if (map == null) { + continue; + } + Field tableF = map.getClass().getDeclaredField("table"); + tableF.setAccessible(true); + Object table = tableF.get(map); + if (table == null) { + continue; + } + int n = Array.getLength(table); + Field valF = null; + for (int i = 0; i < n; i++) { + Object entry = Array.get(table, i); + if (entry == null) { + continue; + } + if (valF == null) { + valF = entry.getClass().getDeclaredField("value"); + valF.setAccessible(true); + } + Object val = valF.get(entry); + if (val != null) { + out.add(val); + } + } + } catch (Throwable ignore) { + // field layout differs or inaccessible + } + } + return out; + } + + private static List loadedClassNames() { + List names = new ArrayList<>(); + try { + String out = (String) ManagementFactory.getPlatformMBeanServer().invoke( + new javax.management.ObjectName("com.sun.management:type=DiagnosticCommand"), + "gcClassHistogram", new Object[] { new String[0] }, + new String[] { String[].class.getName() }); + for (String line : out.split("\n")) { + String[] p = line.trim().split("\\s+"); + if (p.length >= 4 && p[0].endsWith(":")) { + String name = p[3]; + if (name.startsWith("[") || name.contains("/")) { + continue; // arrays, lambdas/hidden classes + } + names.add(name); + } + } + } catch (Exception e) { + System.out.println("[root] class enumeration failed: " + e); + } + return names; + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtRetentionProbe.java b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtRetentionProbe.java new file mode 100644 index 00000000000..8d3b0674b1a --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtRetentionProbe.java @@ -0,0 +1,194 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.prover.mt; + +import java.lang.management.ManagementFactory; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.Comparator; +import java.util.Map; +import java.util.TreeMap; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.util.ProofStarter; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.condition.EnabledIfSystemProperty; + +/** + * Measures whether memory accumulates across repeated load/prove/dispose cycles of the + * same obligation in one JVM. The 128-core stress run #1 was GC-bound with a steadily growing ~17 + * GB + * live set, which suggested per-proof state was retained after {@link KeYEnvironment#dispose()} + * rather + * than something intrinsic to the parallel prover; this probe isolates that on a single thread. + * + *

+ * It proves the obligation {@code reps} times, and after each cycle forces a full GC and records + * the + * live heap. A flat trend means {@code dispose()} releases everything; a rising trend quantifies + * the + * leak (MB per proof). With {@code -Dkey.mt.retention.histo=true} it additionally prints, at the + * end, + * the classes whose live-instance count grew the most between an early and the final cycle (a cheap + * "what is being retained" histogram via the diagnostic command on this JVM). + * + *

+ * Enable with {@code -Dkey.mt.retention=true}. Knobs: {@code -Dkey.mt.retention.proof} (example + * relative, default symmArray), {@code -Dkey.mt.retention.reps} (default 12), + * {@code -Dkey.mt.retention.histo} (default false). Run with a fixed, modest {@code -Xmx} so growth + * is visible (e.g. {@code -PstressHeap} on the dedicated task), single-threaded by default. + * + */ +@EnabledIfSystemProperty(named = "key.mt.retention", matches = "true") +public class MtRetentionProbe { + + private static final long MB = 1024 * 1024; + + @Test + void retention() throws Exception { + String rel = + System.getProperty("key.mt.retention.proof", "standard_key/java_dl/symmArray.key"); + int reps = Integer.getInteger("key.mt.retention.reps", 12); + boolean histo = Boolean.getBoolean("key.mt.retention.histo"); + + Path examples = FindResources.getExampleDirectory(); + if (examples == null) { + System.out.println("[retention] examples directory not found; nothing to do"); + return; + } + Path keyFile = examples.resolve(rel); + if (!Files.exists(keyFile)) { + System.out.printf("[retention] missing proof %s%n", rel); + return; + } + + System.out.printf("[retention] proof=%s reps=%d maxHeap=%dMB histo=%s%n", rel, reps, + Runtime.getRuntime().maxMemory() / MB, histo); + + boolean findRoot = Boolean.getBoolean("key.mt.retention.root"); + + Map histoEarly = null; + long[] usedMb = new long[reps]; + Proof retainedTarget = null; // stack-local only: the genuine leak path is the only one + // found + for (int i = 0; i < reps; i++) { + KeYEnvironment env = KeYEnvironment.load(keyFile); + Proof proof = null; + try { + proof = env.getLoadedProof(); + ProofStarter starter = new ProofStarter(false); + starter.init(proof); + starter.start(); + } finally { + env.dispose(); + } + if (findRoot && i == 0) { + retainedTarget = proof; // a disposed proof; we will hunt its static referrer + } + usedMb[i] = usedAfterGc() / MB; + System.out.printf("[retention] rep=%-2d liveMB=%d%n", i, usedMb[i]); + if (histo && i == 1) { + histoEarly = classHistogram(); + } + } + + long first = usedMb[0]; + long last = usedMb[reps - 1]; + double perRep = reps > 1 ? (double) (last - first) / (reps - 1) : 0.0; + System.out.printf("[retention] RESULT first=%dMB last=%dMB delta=%dMB (%+.1f MB/proof)%n", + first, last, last - first, perRep); + System.out.printf("[retention] verdict: %s%n", + perRep > 2.0 ? "RETENTION (live heap grows across disposed proofs)" + : "flat (dispose releases per-proof state)"); + + if (histo && histoEarly != null) { + printGrowth(histoEarly, classHistogram()); + } + + String dump = System.getProperty("key.mt.retention.dump"); + if (dump != null) { + usedAfterGc(); // settle before dumping + dumpHeap(dump); + } + + if (findRoot && retainedTarget != null) { + usedAfterGc(); + HeapRootFinder.reportPath(retainedTarget); + } + } + + /** Writes a live-objects-only HPROF heap dump for Eclipse MAT analysis. */ + private static void dumpHeap(String path) { + try { + Path p = Path.of(path); + Files.deleteIfExists(p); + Object bean = ManagementFactory.newPlatformMXBeanProxy( + ManagementFactory.getPlatformMBeanServer(), + "com.sun.management:type=HotSpotDiagnostic", + Class.forName("com.sun.management.HotSpotDiagnosticMXBean")); + bean.getClass().getMethod("dumpHeap", String.class, boolean.class) + .invoke(bean, p.toAbsolutePath().toString(), true); + System.out.printf("[retention] heap dump written: %s%n", p.toAbsolutePath()); + } catch (Exception e) { + System.out.println("[retention] heap dump failed: " + e); + } + } + + /** Live heap after several full GCs, to drain finalizers/soft refs as far as is practical. */ + private static long usedAfterGc() throws InterruptedException { + Runtime rt = Runtime.getRuntime(); + for (int k = 0; k < 5; k++) { + System.gc(); + Thread.sleep(120); + } + return rt.totalMemory() - rt.freeMemory(); + } + + /** class name -> live instance count, via the JVM's GC.class_histogram diagnostic command. */ + private static Map classHistogram() { + Map m = new TreeMap<>(); + try { + String out = (String) ManagementFactory.getPlatformMBeanServer().invoke( + new javax.management.ObjectName("com.sun.management:type=DiagnosticCommand"), + "gcClassHistogram", new Object[] { new String[0] }, + new String[] { String[].class.getName() }); + for (String line : out.split("\n")) { + String[] p = line.trim().split("\\s+"); + // columns: num #instances #bytes class name + if (p.length >= 4 && p[0].endsWith(":")) { + try { + m.put(p[3], Long.parseLong(p[1])); + } catch (NumberFormatException ignore) { + // header / non-data line + } + } + } + } catch (Exception e) { + System.out.println("[retention] histogram unavailable: " + e); + } + return m; + } + + private static void printGrowth(Map early, Map late) { + record Growth(String cls, long delta, long late) { + } + var list = new java.util.ArrayList(); + for (var e : late.entrySet()) { + long d = e.getValue() - early.getOrDefault(e.getKey(), 0L); + if (d > 0) { + list.add(new Growth(e.getKey(), d, e.getValue())); + } + } + list.sort(Comparator.comparingLong((Growth g) -> g.delta).reversed()); + System.out.println("[retention] top live-instance growth (rep1 -> final):"); + for (int i = 0; i < Math.min(25, list.size()); i++) { + Growth g = list.get(i); + System.out.printf("[retention] +%-10d (now %-10d) %s%n", g.delta, g.late, g.cls); + } + } +}