Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Fix quoting in IDs #2968

Merged
merged 5 commits into from
Oct 10, 2022
Merged

Fix quoting in IDs #2968

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
5e9bc5a
Fix quoting in IDs
Baltoli Oct 10, 2022
94ecce4
Trailing whitespace
Baltoli Oct 10, 2022
9f9c1fa
Fix test
Baltoli Oct 10, 2022
260aa4c
Fix dependence on Id sort
Baltoli Oct 10, 2022
655b63a
Additional test case
Baltoli Oct 10, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions k-distribution/tests/regression-new/issue-2315-id-quotes/1.test
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
test
3 changes: 3 additions & 0 deletions k-distribution/tests/regression-new/issue-2315-id-quotes/1.test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
<k>
false ~> .
</k>
7 changes: 7 additions & 0 deletions k-distribution/tests/regression-new/issue-2315-id-quotes/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
DEF=test
EXT=test
TESTDIR=.
KOMPILE_BACKEND=llvm
KOMPILE_FLAGS=--syntax-module TEST

include ../../../include/kframework/ktest.mak
11 changes: 11 additions & 0 deletions k-distribution/tests/regression-new/issue-2315-id-quotes/test.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
module TEST
imports ID
imports BOOL
imports K-EQUAL
imports STRING

syntax Bool ::= "test" [function]

// Evaluates to true if the Id constructed by String2Id contains extra quotes
rule test => String2Id("x") ==K #token("\"x\"", "Id")
endmodule
10 changes: 7 additions & 3 deletions kernel/src/main/java/org/kframework/compile/ConstantFolding.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.*;
Expand Down Expand Up @@ -113,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) {
} else if (result instanceof String && hasStringHook) {
return KToken(StringUtil.enquoteKString((String)result), sort);
} else {
return KToken(result.toString(), sort);
Expand All @@ -141,7 +145,7 @@ private K doFolding(String hook, List<K> 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) {
Expand Down