Cache subtype computations in KeYProgModelInfo

key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java

@@ -56,6 +56,21 @@ public class KeYProgModelInfo {
     private final JP2KeYTypeConverter typeConverter;
     private final Map<KeYJavaType, Map<String, IProgramMethod>> implicits = new LinkedHashMap<>();
 
+    /**
+     * Caches subtype lookup. First it is a general win, but second JavaParser pretty prints AST
+     * nodes
+     * on every as part of checking assignability, which causes a lot of String creations.
+     * The cache is invalidated if the backing Java models number of types changes
+     * {@code subtypeCachedSize}.
+     */
+    private final Map<KeYJavaType, List<ResolvedReferenceTypeDeclaration>> subtypeCache =
+        new HashMap<>();
+
+    /** Size of the type model {@link #subtypeCache} was computed from. */
+    private int subtypeCachedSize = -1;
+
+
+
     public KeYProgModelInfo(JavaService service) {
         this.typeConverter = service.getTypeConverter();
         this.mapping = service.getMapping();
@@ -507,8 +522,38 @@ private List<Field> getVisibleArrayFields(KeYJavaType arrayType) {
 
     /**
      * returns all proper subtypes of class <code>ct</code> (i.e. without <code>ct</code> itself)
+     *
+     * @return an unmodifiable list of all proper subtypes
      */
     private List<ResolvedReferenceTypeDeclaration> getAllRecoderSubtypes(KeYJavaType ct) {
+        final int size = rec2key().elemsRec().size();
+        synchronized (subtypeCache) {
+            if (size != subtypeCachedSize) {
+                subtypeCache.clear();
+                subtypeCachedSize = size;
+            }
+            List<ResolvedReferenceTypeDeclaration> hit = subtypeCache.get(ct);
+            if (hit != null) {
+                return hit;
+            }
+        }
+        // Computed outside the lock: this is the expensive part and it only reads the model.
+        final List<ResolvedReferenceTypeDeclaration> res =
+            Collections.unmodifiableList(computeAllRecoderSubtypes(ct));
+        synchronized (subtypeCache) {
+            // check if the number of known types has changed and invalidate cache if so
+            // assumes: no changes to existing types happen
+            if (rec2key().elemsRec().size() == subtypeCachedSize) {
+                subtypeCache.put(ct, res);
+            }
+        }
+        return res;
+    }
+
+    /**
+     * computes all proper subtypes of class <code>ct</code> (i.e. without <code>ct</code> itself)
+     */
+    private List<ResolvedReferenceTypeDeclaration> computeAllRecoderSubtypes(KeYJavaType ct) {
         final ResolvedType rt = getJavaParserType(ct);
         final ResolvedReferenceTypeDeclaration rtAsTypeDecl =
             rt.asReferenceType().getTypeDeclaration().get();