java-backend: Caching toString() for KItem. Speeds up logging options. Enabled with --cache-tostring. (runtimeverification#302)

denis-bogdanas · web-flow · commit 5364302fa8ce · 2019-02-23T12:07:58.000+02:00
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/GlobalContext.java b/java-backend/src/main/java/org/kframework/backend/java/kil/GlobalContext.java
@@ -11,6 +11,7 @@
 import org.kframework.backend.java.util.FormulaSimplificationCache;
 import org.kframework.backend.java.util.Profiler2;
 import org.kframework.backend.java.util.StateLog;
+import org.kframework.backend.java.util.ToStringCache;
 import org.kframework.backend.java.util.Z3Wrapper;
 import org.kframework.krun.KRunOptions;
 import org.kframework.krun.api.io.FileSystem;
@@ -43,6 +44,7 @@ public class GlobalContext implements Serializable {
     public final PrettyPrinter prettyPrinter;
     public final transient FunctionCache functionCache = new FunctionCache();
     public final transient FormulaSimplificationCache formulaCache = new FormulaSimplificationCache();
+    public final transient ToStringCache toStringCache = new ToStringCache();
 
     private boolean isExecutionPhase = true;
 
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/KItem.java b/java-backend/src/main/java/org/kframework/backend/java/kil/KItem.java
@@ -788,6 +788,19 @@ protected int computeHash() {
 
     @Override
     public String toString() {
+        String cached = global.toStringCache.get(this);
+        if (cached != null) {
+            return cached;
+        }
+
+        String result = toStringImpl();
+        if (global.javaExecutionOptions.cacheToString) {
+            global.toStringCache.put(this, result);
+        }
+        return result;
+    }
+
+    public String toStringImpl() {
         return kLabel + "(" + kList.toString() + ")";
     }
 
diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaExecutionOptions.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaExecutionOptions.java
@@ -51,13 +51,18 @@ public final class JavaExecutionOptions {
     @Parameter(names="--cache-func", description="Cache evaluation results of pure functions. Enabled by default.", arity = 1)
     public boolean cacheFunctions = true;
 
-    @Parameter(names="--cache-formulas", description="Cache results of ConjunctiveFormula.simplify().")
-    public boolean cacheFormulas = false;
-
     @Parameter(names="--cache-func-optimized",
             description="Clear function cache after initialization phase. Frees some memory. Use IN ADDITION to --cache-func")
     public boolean cacheFunctionsOptimized = false;
 
+    @Parameter(names="--cache-formulas", description="Cache results of ConjunctiveFormula.simplify().")
+    public boolean cacheFormulas = false;
+
+    @Parameter(names="--cache-tostring",
+            description="Cache toString() result for KItem, Equality and DisjunctiveFormula. " +
+                    "Speeds up logging but eats more memory.", arity = 1)
+    public boolean cacheToString = true;
+
     @Parameter(names="--format-failures", description="Format failure final states. By default they are printed all " +
             "on one line, using ConstrainedTerm.toString(). If option is enabled, they are printed a bit nicer, " +
             "using custom ConjunctiveFormula formatter, but still fast. Disabled by default for output compatibility " +
diff --git a/java-backend/src/main/java/org/kframework/backend/java/util/ToStringCache.java b/java-backend/src/main/java/org/kframework/backend/java/util/ToStringCache.java
@@ -0,0 +1,31 @@
+// Copyright (c) 2019 K Team. All Rights Reserved.
+package org.kframework.backend.java.util;
+
+import org.kframework.backend.java.kil.KItem;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * @author Denis Bogdanas
+ * Created on 31-Jan-19.
+ */
+public class ToStringCache {
+    private Map<KItem, String> toStringCache = new HashMap<>();
+
+    public String get(KItem kItem) {
+        return toStringCache.get(kItem);
+    }
+
+    public void put(KItem kItem, String str) {
+        toStringCache.put(kItem, str);
+    }
+
+    public void clear() {
+        toStringCache.clear();
+    }
+
+    public int size() {
+        return toStringCache.size();
+    }
+}
