diff --git a/pyk/src/pyk/kllvm/convert.py b/pyk/src/pyk/kllvm/convert.py index a705ab8f170..0b68505dc96 100644 --- a/pyk/src/pyk/kllvm/convert.py +++ b/pyk/src/pyk/kllvm/convert.py @@ -108,7 +108,7 @@ def sentence_to_llvm(sentence: Sentence) -> kllvm.Declaration: def pattern_to_llvm(pattern: Pattern) -> kllvm.Pattern: match pattern: case String(value): - return kllvm.StringPattern(value) + return kllvm.StringPattern(value.encode('latin-1')) case VarPattern(name, sort): return kllvm.VariablePattern(name, sort_to_llvm(sort)) case App(symbol, sorts, args): @@ -201,7 +201,7 @@ def llvm_to_sentence(decl: kllvm.Declaration) -> Sentence: def llvm_to_pattern(pattern: kllvm.Pattern) -> Pattern: match pattern: case kllvm.StringPattern(): # type: ignore - return String(pattern.contents) + return String(pattern.contents.decode('latin-1')) case kllvm.VariablePattern(): # type: ignore if pattern.name and pattern.name[0] == '@': return SVar(pattern.name, llvm_to_sort(pattern.sort)) diff --git a/pyk/src/tests/integration/test_string.py b/pyk/src/tests/integration/test_string.py index 2847e05ab7c..7af3a737b75 100644 --- a/pyk/src/tests/integration/test_string.py +++ b/pyk/src/tests/integration/test_string.py @@ -40,6 +40,13 @@ '🙂', ) +BINDINGS_TEST_DATA: Final = ( + 'hello', + '\n', + '\x01', + '£', +) + KOMPILE_DEFINITION = """ module STRING-REWRITE imports STRING-SYNTAX @@ -213,7 +220,7 @@ def test_krun(backend: str, definition_dir: Path, text: str) -> None: assert actual == expected -@pytest.mark.parametrize('text', TEST_DATA, ids=TEST_DATA) +@pytest.mark.parametrize('text', BINDINGS_TEST_DATA, ids=BINDINGS_TEST_DATA) def test_bindings(runtime: Runtime, text: str) -> None: from pyk.kllvm.convert import llvm_to_pattern, pattern_to_llvm