From 5e9bc5ae05ea0f194fd56d10b422405447c5a0f8 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 10 Oct 2022 15:36:55 +0100 Subject: [PATCH 1/5] Fix quoting in IDs --- .../tests/regression-new/issue-2315-id-quotes/1.test | 1 + .../regression-new/issue-2315-id-quotes/1.test.out | 3 +++ .../regression-new/issue-2315-id-quotes/Makefile | 7 +++++++ .../tests/regression-new/issue-2315-id-quotes/test.k | 11 +++++++++++ .../java/org/kframework/compile/ConstantFolding.java | 3 ++- 5 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 k-distribution/tests/regression-new/issue-2315-id-quotes/1.test create mode 100644 k-distribution/tests/regression-new/issue-2315-id-quotes/1.test.out create mode 100644 k-distribution/tests/regression-new/issue-2315-id-quotes/Makefile create mode 100644 k-distribution/tests/regression-new/issue-2315-id-quotes/test.k diff --git a/k-distribution/tests/regression-new/issue-2315-id-quotes/1.test b/k-distribution/tests/regression-new/issue-2315-id-quotes/1.test new file mode 100644 index 00000000000..9daeafb9864 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-2315-id-quotes/1.test @@ -0,0 +1 @@ +test diff --git a/k-distribution/tests/regression-new/issue-2315-id-quotes/1.test.out b/k-distribution/tests/regression-new/issue-2315-id-quotes/1.test.out new file mode 100644 index 00000000000..d4638597117 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-2315-id-quotes/1.test.out @@ -0,0 +1,3 @@ + + false ~> . + diff --git a/k-distribution/tests/regression-new/issue-2315-id-quotes/Makefile b/k-distribution/tests/regression-new/issue-2315-id-quotes/Makefile new file mode 100644 index 00000000000..d48aaade4fd --- /dev/null +++ b/k-distribution/tests/regression-new/issue-2315-id-quotes/Makefile @@ -0,0 +1,7 @@ +DEF=test +EXT=test +TESTDIR=. +KOMPILE_BACKEND=llvm +KOMPILE_FLAGS=--syntax-module TEST + +include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k b/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k new file mode 100644 index 00000000000..b3ff72829cf --- /dev/null +++ b/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k @@ -0,0 +1,11 @@ +module TEST + imports ID + imports BOOL + imports K-EQUAL + imports STRING + + syntax Bool ::= "test" [function] + + // Evaluates to true + rule test => String2Id("x") ==K #token("\"x\"", "Id") +endmodule diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index c2f599269a0..2f70a436f0f 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -24,6 +24,7 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.List; +import java.util.Objects; import static org.kframework.Collections.*; import static org.kframework.kore.KORE.*; @@ -120,7 +121,7 @@ private K wrap(Object result, Sort sort) { return KToken(((FloatBuiltin)result).value(), sort); } else if (result instanceof BigInteger) { return KToken(result.toString(), sort); - } else if (result instanceof String) { + } else if (result instanceof String && !Objects.equals(sort.name(), "Id")) { return KToken(StringUtil.enquoteKString((String)result), sort); } else { return KToken(result.toString(), sort); From 94ecce4ae7ddd0e45d184b5382e79c9561b15fea Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 10 Oct 2022 15:49:20 +0100 Subject: [PATCH 2/5] Trailing whitespace --- k-distribution/tests/regression-new/issue-2315-id-quotes/test.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k b/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k index b3ff72829cf..d582c393dc5 100644 --- a/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k +++ b/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k @@ -1,4 +1,4 @@ -module TEST +module TEST imports ID imports BOOL imports K-EQUAL From 9f9c1fa364ab9de67b1538f8e19e593b291eec49 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 10 Oct 2022 15:55:10 +0100 Subject: [PATCH 3/5] Fix test --- k-distribution/tests/regression-new/issue-2315-id-quotes/test.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k b/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k index d582c393dc5..fbcf585406d 100644 --- a/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k +++ b/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k @@ -6,6 +6,6 @@ module TEST syntax Bool ::= "test" [function] - // Evaluates to true + // Evaluates to true if the Id constructed by String2Id contains extra quotes rule test => String2Id("x") ==K #token("\"x\"", "Id") endmodule From 260aa4c7f2c0bf9852f3f04389c94a0431b2268d Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 10 Oct 2022 16:19:33 +0100 Subject: [PATCH 4/5] Fix dependence on Id sort --- .../java/org/kframework/compile/ConstantFolding.java | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 2f70a436f0f..227e04056d4 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -114,14 +114,17 @@ private Object unwrap(String token, String hook) { } } - private K wrap(Object result, Sort sort) { + private K wrap(Object result, Sort sort, Module module) { + String resultHookName = module.sortAttributesFor().apply(sort.head()).getOptional(Att.HOOK()).orElse(""); + boolean hasStringHook = resultHookName.equals("STRING.String") || resultHookName.equals("BYTES.Bytes"); + if (result instanceof Boolean) { return KToken(result.toString(), sort); } else if (result instanceof FloatBuiltin) { return KToken(((FloatBuiltin)result).value(), sort); } else if (result instanceof BigInteger) { return KToken(result.toString(), sort); - } else if (result instanceof String && !Objects.equals(sort.name(), "Id")) { + } else if (result instanceof String && hasStringHook) { return KToken(StringUtil.enquoteKString((String)result), sort); } else { return KToken(result.toString(), sort); @@ -142,7 +145,7 @@ private K doFolding(String hook, List args, Sort resultSort, Module module) t try { Method m = ConstantFolding.class.getDeclaredMethod(renamedHook, paramTypes.toArray(new Class[args.size()])); Object result = m.invoke(this, unwrappedArgs.toArray(new Object[args.size()])); - return wrap(result, resultSort); + return wrap(result, resultSort, module); } catch (IllegalAccessException e) { throw KEMException.internalError("Error invoking constant folding function", e); } catch (InvocationTargetException e) { From 655b63abb9807769f072b385334e8502b487528b Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 10 Oct 2022 16:34:07 +0100 Subject: [PATCH 5/5] Additional test case --- .../tests/regression-new/issue-2315-id-quotes/2.test | 1 + .../tests/regression-new/issue-2315-id-quotes/2.test.out | 3 +++ .../tests/regression-new/issue-2315-id-quotes/test.k | 7 ++++++- 3 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 k-distribution/tests/regression-new/issue-2315-id-quotes/2.test create mode 100644 k-distribution/tests/regression-new/issue-2315-id-quotes/2.test.out diff --git a/k-distribution/tests/regression-new/issue-2315-id-quotes/2.test b/k-distribution/tests/regression-new/issue-2315-id-quotes/2.test new file mode 100644 index 00000000000..180cf832802 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-2315-id-quotes/2.test @@ -0,0 +1 @@ +test2 diff --git a/k-distribution/tests/regression-new/issue-2315-id-quotes/2.test.out b/k-distribution/tests/regression-new/issue-2315-id-quotes/2.test.out new file mode 100644 index 00000000000..123601721d8 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-2315-id-quotes/2.test.out @@ -0,0 +1,3 @@ + + true ~> . + diff --git a/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k b/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k index fbcf585406d..6895d1438d3 100644 --- a/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k +++ b/k-distribution/tests/regression-new/issue-2315-id-quotes/test.k @@ -3,9 +3,14 @@ module TEST imports BOOL imports K-EQUAL imports STRING + imports INT - syntax Bool ::= "test" [function] + syntax Bool ::= "test" [function] + | "test2" [function] // Evaluates to true if the Id constructed by String2Id contains extra quotes rule test => String2Id("x") ==K #token("\"x\"", "Id") + + // Test that hooks producing a result of sort String are wrapped + rule test2 => Int2String(2) ==K "2" endmodule