From 5bae74047037d0916b9e5a8b319a6122e1703de8 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Wed, 7 Aug 2024 14:50:54 -0600 Subject: [PATCH] Update dependency: deps/llvm-backend_release (#4565) Co-authored-by: devops Co-authored-by: Dwight Guth Co-authored-by: Roberto Rosmaninho --- .github/workflows/Dockerfile | 1 + README.md | 1 + deps/llvm-backend_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- install-build-deps | 1 + llvm-backend/src/main/native/llvm-backend | 2 +- package/debian/kframework/control.jammy | 2 +- pyk/src/pyk/kllvm/convert.py | 4 ++-- pyk/src/tests/integration/kllvm/test_patterns.py | 2 +- pyk/src/tests/integration/test_string.py | 9 +++++++++ 11 files changed, 23 insertions(+), 11 deletions(-) diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index 7f7197756a9..422333bb4e6 100644 --- a/.github/workflows/Dockerfile +++ b/.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 diff --git a/README.md b/README.md index 7a4f9fe2895..ea1be3d0d2e 100644 --- a/README.md +++ b/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, diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 9adbab1b3a2..d9ba7470869 100644 --- a/deps/llvm-backend_release +++ b/deps/llvm-backend_release @@ -1 +1 @@ -0.1.69 +0.1.75 diff --git a/flake.lock b/flake.lock index 90fb6ea5de0..18b4fa3950e 100644 --- a/flake.lock +++ b/flake.lock @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1722454948, - "narHash": "sha256-8mcRIlTAmQ1J3oxi0QibxmSlFWkOTRlyWy5kSHJFf6U=", + "lastModified": 1722973323, + "narHash": "sha256-lD8Mc5sftYa4pqyUoglFzYDzTXiJ7m/SiMbeKy2tn2c=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "5be14fe74740a15cb707c102425032ffdee98281", + "rev": "9cb2137d96059c8751bb57216cc1d0cea5746161", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.69", + "ref": "v0.1.75", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 80d9fa75a6c..48ca100e172 100644 --- a/flake.nix +++ b/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"; diff --git a/install-build-deps b/install-build-deps index ee741eca574..d89338691f9 100755 --- a/install-build-deps +++ b/install-build-deps @@ -34,6 +34,7 @@ inst_Debian() { pkg-config \ python3 \ python3-dev \ + xxd \ z3 \ zlib1g-dev diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 5be14fe7474..9cb2137d960 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 5be14fe74740a15cb707c102425032ffdee98281 +Subproject commit 9cb2137d96059c8751bb57216cc1d0cea5746161 diff --git a/package/debian/kframework/control.jammy b/package/debian/kframework/control.jammy index 635e40cb2d9..b8b3a5acdbf 100644 --- a/package/debian/kframework/control.jammy +++ b/package/debian/kframework/control.jammy @@ -2,7 +2,7 @@ Source: kframework Section: devel Priority: optional Maintainer: Dwight Guth -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 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/kllvm/test_patterns.py b/pyk/src/tests/integration/kllvm/test_patterns.py index 20b07cf9b5a..d6c6bfff44c 100644 --- a/pyk/src/tests/integration/kllvm/test_patterns.py +++ b/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: diff --git a/pyk/src/tests/integration/test_string.py b/pyk/src/tests/integration/test_string.py index 2847e05ab7c..699542bd180 100644 --- a/pyk/src/tests/integration/test_string.py +++ b/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)