Update dependency: deps/llvm-backend_release (#4565)

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Dwight Guth <dwight.guth@runtimeverification.com>
Co-authored-by: Roberto Rosmaninho <robertogomes@dcc.ufmg.br>

.github/workflows/Dockerfile

@@ -65,6 +65,7 @@ RUN    apt-get update              \
         python3-dev                \
         python3-distutils          \
         python3-pip                \
+        xxd                        \
         zlib1g-dev
 
 COPY --from=Z3 /usr/bin/z3 /usr/bin/z3

README.md

@@ -104,6 +104,7 @@ The following dependencies are needed either at build time or runtime:
 *   [pkg-config](https://www.freedesktop.org/wiki/Software/pkg-config/)
 *   [python](https://www.python.org)
 *   [stack](https://docs.haskellstack.org/en/stable/README/)
+*   [xxd](https://github.com/vim/vim/blob/master/runtime/doc/xxd.man)
 *   [zlib](https://www.zlib.net/)
 *   [z3](https://github.com/Z3Prover/z3) (on some distributions libz3 is also
     needed and packaged separately) Note that you need version 4.12.1 of Z3,

deps/llvm-backend_release

@@ -1 +1 @@
-0.1.69
+0.1.75

flake.nix

@@ -1,7 +1,7 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.69";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.75";
     haskell-backend = {
       url = "github:runtimeverification/haskell-backend/v0.1.58";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

install-build-deps

@@ -34,6 +34,7 @@ inst_Debian() {
         pkg-config              \
         python3                 \
         python3-dev             \
+        xxd                     \
         z3                      \
         zlib1g-dev
 

package/debian/kframework/control.jammy

@@ -2,7 +2,7 @@ Source: kframework
 Section: devel
 Priority: optional
 Maintainer: Dwight Guth <dwight.guth@runtimeverification.com>
-Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev
+Build-Depends: clang-15 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libunwind-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , xxd , zlib1g-dev
 Standards-Version: 3.9.6
 Homepage: https://github.com/runtimeverification/k
 

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))

pyk/src/tests/integration/kllvm/test_patterns.py

@@ -50,7 +50,7 @@ def test_string() -> None:
 
     # Then
     assert str(pattern) == '"abc"'
-    assert pattern.contents == 'abc'
+    assert pattern.contents.decode('latin-1') == 'abc'
 
 
 def test_variable() -> None:

pyk/src/tests/integration/test_string.py

@@ -40,6 +40,12 @@
     '🙂',
 )
 
+SKIPPED_BINDINGS_TESTS: Final = {
+    '𐍈',
+    '武天老師',
+    '🙂',
+}
+
 KOMPILE_DEFINITION = """
     module STRING-REWRITE
         imports STRING-SYNTAX
@@ -217,6 +223,9 @@ def test_krun(backend: str, definition_dir: Path, text: str) -> None:
 def test_bindings(runtime: Runtime, text: str) -> None:
     from pyk.kllvm.convert import llvm_to_pattern, pattern_to_llvm
 
+    if text in SKIPPED_BINDINGS_TESTS:
+        pytest.skip()
+
     # Given
     kore = kore_config(text, '')
     expected = kore_config(None, text)