[kevm debugging] lightweight toString

yzhang90 · daejunpark · commit 5c25763980fd · 2018-05-07T02:36:08.000-05:00
diff --git a/java-backend/src/main/java/org/kframework/backend/java/kil/BuiltinMap.java b/java-backend/src/main/java/org/kframework/backend/java/kil/BuiltinMap.java
@@ -6,6 +6,7 @@
 import com.google.common.collect.Lists;
 import org.apache.commons.collections4.map.UnmodifiableMap;
 import org.apache.commons.lang3.tuple.Triple;
+import org.kframework.backend.java.builtins.IntToken;
 import org.kframework.backend.java.symbolic.Transformer;
 import org.kframework.backend.java.symbolic.Visitor;
 import org.kframework.backend.java.util.Constants;
@@ -120,6 +121,12 @@ public String toString() {
 
     private String toString(String operator, String mapsTo, String identity) {
         if (!isEmpty()) {
+            IntToken key1 = IntToken.of(0);
+            IntToken key2 = IntToken.of(2);
+            if(entries.containsKey(key1) && entries.get(key1).toString().equals("PUSH(Int(#\"1\"),, Int(#\"0\"))") &&
+               entries.containsKey(key2) && entries.get(key2).toString().equals("CALLDATALOAD_EVM(.KList)")) {
+                return "CodeMap(" + entries.size() + ")";
+            }
             return Joiner.on(operator).join(
                     Joiner.on(operator).withKeyValueSeparator(mapsTo).join(entries),
                     Joiner.on(operator).join(collectionPatterns),
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
@@ -15,6 +15,7 @@
 import org.kframework.backend.java.util.Constants;
 import org.kframework.builtin.KLabels;
 import org.kframework.kil.Attribute;
+import org.kframework.kore.mini.KVariable;
 import org.kframework.main.GlobalOptions;
 import org.kframework.backend.java.utils.BitSet;
 import org.kframework.utils.errorsystem.KException.ExceptionType;
@@ -706,7 +707,21 @@ protected int computeHash() {
 
     @Override
     public String toString() {
-        return kLabel + "(" + kList.toString() + ")";
+        String label = kLabel.toString();
+        if(label.equals("<programBytes>") || label.equals("<code>")) {
+            return kLabel + "(" + ((KList)kList).getContents().size() + ")";
+        } else if (label.equals("#mkCall__________EVM")) {
+            return kLabel + "()";
+        } else if(label.equals("{_|_|_|_|_|_|_|_|_|_|_|_|_}_EVM")) {
+            return kLabel + "()";
+        } else if(label.equals("{_|_}_EVM")) {
+            return kLabel + "()";
+        } else if(label.equals("<callState>-fragment")){
+            return kLabel + "()";
+        }
+        else {
+            return kLabel + "(" + kList.toString() + ")";
+        }
     }
 
     @Override
diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java
@@ -675,6 +675,7 @@ public List<ConstrainedTerm> proveRule(
             guarded = true;
         }
 
+        System.out.println("Prove steps: " + step);
         return proofResults;
     }
 

Original file line number	Diff line number	Diff line change
`@@ -675,6 +675,7 @@ public List<ConstrainedTerm> proveRule(`
`675`	`675`	`guarded = true;`
`676`	`676`	`}`
`677`	`677`
	`678`	`+ System.out.println("Prove steps: " + step);`
`678`	`679`	`return proofResults;`
`679`	`680`	`}`
`680`	`681`