Fix decodeKoreString again

k-distribution/tests/regression-new/issue-2356-koreDecode/1.test

@@ -0,0 +1 @@
+#fail , ?_0 , _V_9 , ^-_<>&

k-distribution/tests/regression-new/issue-2356-koreDecode/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  #fail , ?_0 , _V_9 , ^-_<>& , .Exps ~> .
+</k>

k-distribution/tests/regression-new/issue-2356-koreDecode/Makefile

@@ -0,0 +1,10 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=haskell
+KAST_FLAGS=-i kore -o pretty
+
+include ../../../include/kframework/ktest.mak
+
+result2.kore.kast: kompile
+	${K_BIN}/kore-print result.kore.kast $(CHECK) result.kore.kast.out

k-distribution/tests/regression-new/issue-2356-koreDecode/result.kore.kast

@@ -0,0 +1,37 @@
+/* Fl Fn D Sfa Cl */
+Lbl'-LT-'generatedTop'-GT-'{}(
+    /* Fl Fn D Sfa Cl */
+    Lbl'-LT-'k'-GT-'{}(
+        /* Fl Fn D Sfa Cl */
+        kseq{}(
+            /* Fl Fn D Sfa Cli */
+            /* Inj: */ inj{SortExps{}, SortKItem{}}(
+                /* Fl Fn D Sfa Cl */
+                Lbl'UndsCommUndsUnds'TEST-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
+                    /* Fl Fn D Sfa Cl */
+                    Lbl'Hash'fail'Unds'TEST-SYNTAX'Unds'Exp{}(),
+                    /* Fl Fn D Sfa Cl */
+                    Lbl'UndsCommUndsUnds'TEST-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
+                        /* Fl Fn D Sfa Cl */
+                        Lbl'QuesUnds'0'Unds'TEST-SYNTAX'Unds'Exp{}(),
+                        /* Fl Fn D Sfa Cl */
+                        Lbl'UndsCommUndsUnds'TEST-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
+                            /* Fl Fn D Sfa Cl */
+                            Lbl'Unds'V'Unds'9'Unds'TEST-SYNTAX'Unds'Exp{}(),
+                            /* Fl Fn D Sfa Cl */
+                            Lbl'UndsCommUndsUnds'TEST-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps{}(
+                                /* Fl Fn D Sfa Cl */
+                                Lbl'Xor-'-'Unds-LT--GT-And-Unds'TEST-SYNTAX'Unds'Exp{}(),
+                                /* Fl Fn D Sfa Cl */
+                                Lbl'Stop'List'LBraQuotUndsCommUndsUnds'TEST-SYNTAX'Unds'Exps'Unds'Exp'Unds'Exps'QuotRBraUnds'Exps{}()
+                            )
+                        )
+                    )
+                )
+            ),
+            /* Fl Fn D Sfa Cl */ dotk{}()
+        )
+    ),
+    /* Fl Fn D Sfa Cl */
+    Lbl'-LT-'generatedCounter'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0"))
+)

k-distribution/tests/regression-new/issue-2356-koreDecode/result.kore.kast.out

@@ -0,0 +1,3 @@
+<k>
+  #fail , ?_0 , _V_9 , ^-_<>& , .Exps ~> .
+</k>

k-distribution/tests/regression-new/issue-2356-koreDecode/test.k

@@ -0,0 +1,10 @@
+module TEST-SYNTAX
+  syntax Exps ::= List{Exp,","}
+
+  syntax Exp ::= "#fail" | "?_0" | "_V_9" | "^-_<>&"
+endmodule
+
+module TEST
+  imports TEST-SYNTAX
+  configuration <k> $PGM:Exps </k>
+endmodule

k-distribution/tests/regression-new/llvm-kompile-type/Makefile

@@ -6,3 +6,5 @@ all:
 	$(MAKE) -C ../imp-llvm clean
 	$(MAKE) -C ../imp-llvm
 	$(MAKE) -C ../imp-llvm clean
+
+clean:

kernel/src/test/java/org/kframework/utils/StringUtilTest.java

@@ -3,6 +3,9 @@
 
 import junit.framework.Assert;
 import org.junit.Test;
+import org.kframework.backend.kore.ModuleToKORE;
+
+import java.util.regex.Pattern;
 
 public class StringUtilTest {
 
@@ -33,7 +36,15 @@ public void StringUtilUnquote() throws Exception {
 
     @Test
     public void decodeKoreString() {
-        Assert.assertEquals(StringUtil.decodeKoreString("'Unds'V'Unds'9"), "_V_9");
+        Assert.assertEquals("_V_9", StringUtil.decodeKoreString("'Unds'V'Unds'9"));
+        Assert.assertEquals("?_0", StringUtil.decodeKoreString("'QuesUnds'0"));
+        Pattern identChar = Pattern.compile("[A-Za-z0-9\\-]");
+        StringBuilder buffer = new StringBuilder();
+        StringUtil.encodeStringToAlphanumeric(buffer, "?_0", ModuleToKORE.asciiReadableEncodingKore, identChar, "'");
+        Assert.assertEquals("'QuesUnds'0", buffer.toString());
+        buffer.setLength(0);
+        StringUtil.encodeStringToAlphanumeric(buffer, "_V_9", ModuleToKORE.asciiReadableEncodingKore, identChar, "'");
+        Assert.assertEquals("'Unds'V'Unds'9", buffer.toString());
     }
 
     @Test

kore/src/main/java/org/kframework/utils/StringUtil.java

@@ -635,9 +635,15 @@ public static String escapeKoreKLabel(String value) {
     private static final Map<String, Character> asciiReadableEncodingDefaultMap = new HashMap<>();
     static {
         for (int i = 0; i < asciiReadableEncodingDefault.length; i++)
-            asciiReadableEncodingDefaultMap.put(asciiReadableEncodingDefault[i], (char) i);
+            if (asciiReadableEncodingDefault[i] != null && asciiReadableEncodingDefault[i].length() > 1)
+                asciiReadableEncodingDefaultMap.put(asciiReadableEncodingDefault[i], (char) i);
     }
 
+    /**
+     * Encode special characters depending on context.
+     * @param asciiReadableEncodingTable Override the default `asciiReadableEncodingDefault` depending on language requirements
+     * @param identChar which characters to replace
+     */
     public static void encodeStringToAlphanumeric(StringBuilder sb, String name, String[] asciiReadableEncodingTable, Pattern identChar, String escapeChar) {
         boolean inIdent = true;
         for (int i = 0; i < name.length(); i++) {
@@ -668,18 +674,17 @@ public static void encodeStringToAlphanumeric(StringBuilder sb, String name, Str
     public static String decodeKoreString(String encoded) {
         boolean quotedState = false;
         StringBuilder resultedEncoding = new StringBuilder();
-        StringBuilder tempSb = new StringBuilder();
         for (int i = 0; i < encoded.length(); i++) {
             if (quotedState) {
                 if (encoded.charAt(i) == '\'') {
                     quotedState = false;
-                    resultedEncoding.append(asciiReadableEncodingDefaultMap.get(tempSb.toString()));
-                } else
-                    tempSb.append(encoded.charAt(i));
+                } else {
+                    resultedEncoding.append(asciiReadableEncodingDefaultMap.get(encoded.substring(i, i + 4)));
+                    i += 3;
+                }
             } else {
                 if (encoded.charAt(i) == '\'') {
                     quotedState = true;
-                    tempSb = new StringBuilder();
                 } else
                     resultedEncoding.append(encoded.charAt(i));
             }