From 531652d017eb47ef00e0320e5718001118ff073f Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Tue, 25 Jun 2024 11:17:03 +0100 Subject: [PATCH 1/3] Use prebuilt haskell backend (#4473) This PR uses the existing infrastructure we have for the LLVM backend to download a pre-packaged release of the Haskell backend when running the K integration tests. It's a bit obscured currently because of degraded CI performance generally, but this should take average-case CI run times down to 20-25 minutes. --- .github/actions/with-k-docker/Dockerfile | 4 +++- .github/actions/with-k-docker/action.yml | 10 +++++++++- package/debian/kframework-frontend/rules.jammy | 2 +- 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/.github/actions/with-k-docker/Dockerfile b/.github/actions/with-k-docker/Dockerfile index 97df8ea4fb5..09f800e3669 100644 --- a/.github/actions/with-k-docker/Dockerfile +++ b/.github/actions/with-k-docker/Dockerfile @@ -5,9 +5,11 @@ FROM ubuntu:${BASE_DISTRO} ARG K_DEB_PATH ARG INSTALL_BACKEND_DEBS ARG LLVM_BACKEND_DEB_PATH +ARG HASKELL_BACKEND_DEB_PATH COPY ${K_DEB_PATH} /kframework.deb COPY ${LLVM_BACKEND_DEB_PATH} /llvm-backend.deb +COPY ${HASKELL_BACKEND_DEB_PATH} /haskell-backend.deb RUN apt-get -y update \ && apt-get -y install \ @@ -19,7 +21,7 @@ RUN apt-get -y update \ /kframework.deb RUN if [ "${INSTALL_BACKEND_DEBS}" = "true" ]; then \ - apt-get -y install /llvm-backend.deb; \ + apt-get -y install /llvm-backend.deb /haskell-backend.deb; \ fi RUN apt-get -y clean diff --git a/.github/actions/with-k-docker/action.yml b/.github/actions/with-k-docker/action.yml index 62c75bed3e1..f5b67cabdc2 100644 --- a/.github/actions/with-k-docker/action.yml +++ b/.github/actions/with-k-docker/action.yml @@ -42,6 +42,7 @@ runs: DOCKERFILE=${{ github.action_path }}/Dockerfile K_DEB_PATH=${{ inputs.k-deb-path }} LLVM_BACKEND_DEB_PATH=llvm-backend.deb + HASKELL_BACKEND_DEB_PATH=haskell-backend.deb gh release download \ --repo runtimeverification/llvm-backend \ @@ -49,13 +50,20 @@ runs: --output "${LLVM_BACKEND_DEB_PATH}" \ v$(cat deps/llvm-backend_release) + gh release download \ + --repo runtimeverification/haskell-backend \ + --pattern "*ubuntu_${BASE_DISTRO}.deb" \ + --output "${HASKELL_BACKEND_DEB_PATH}" \ + $(cat deps/haskell-backend_release) + docker build . \ --file ${DOCKERFILE} \ --tag ${TAG} \ --build-arg BASE_DISTRO=${BASE_DISTRO} \ --build-arg K_DEB_PATH=${K_DEB_PATH} \ --build-arg INSTALL_BACKEND_DEBS=${INSTALL_BACKEND_DEBS} \ - --build-arg LLVM_BACKEND_DEB_PATH=${LLVM_BACKEND_DEB_PATH} + --build-arg LLVM_BACKEND_DEB_PATH=${LLVM_BACKEND_DEB_PATH} \ + --build-arg HASKELL_BACKEND_DEB_PATH=${HASKELL_BACKEND_DEB_PATH} - name: 'Run Docker container' shell: bash {0} diff --git a/package/debian/kframework-frontend/rules.jammy b/package/debian/kframework-frontend/rules.jammy index 5f62a9bc885..def7df0d9e3 100755 --- a/package/debian/kframework-frontend/rules.jammy +++ b/package/debian/kframework-frontend/rules.jammy @@ -23,7 +23,7 @@ export PREFIX dh $@ override_dh_auto_build: - mvn --batch-mode package -DskipTests -Dllvm.backend.skip + mvn --batch-mode package -DskipTests -Dllvm.backend.skip -Dhaskell.backend.skip override_dh_auto_install: package/package --frontend From 94a069d50f711874987b0331eb466df672683e49 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20V=C4=83caru?= <16517508+anvacaru@users.noreply.github.com> Date: Tue, 25 Jun 2024 16:19:48 +0300 Subject: [PATCH 2/3] Add missing operators to prelude.kint (#4477) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adding new functions to the `KInt` module for Integer operations described in [domains.md](https://github.com/runtimeverification/k/blob/master/pyk/src/tests/profiling/test-data/domains.md?plain=1#L1173) for: - integer arithmetic - integer min and max - integer absolute value Adding docstrings to KInt module. Adding labels for `minInt`, `maxInt`, and `absInt`. --------- Co-authored-by: Tamás Tóth --- pyk/src/pyk/prelude/kint.py | 299 +++++++++++++++++++ pyk/src/tests/profiling/test-data/domains.md | 6 +- 2 files changed, 302 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/prelude/kint.py b/pyk/src/pyk/prelude/kint.py index 28a3eff5ff6..c4ed0dd7808 100644 --- a/pyk/src/pyk/prelude/kint.py +++ b/pyk/src/pyk/prelude/kint.py @@ -13,24 +13,323 @@ def intToken(i: int) -> KToken: # noqa: N802 + r"""Instantiate the KAST term ``#token(i, "Int")``. + + Args: + i: The integer literal. + + Returns: + The KAST term ``#token(i, "Int")``. + """ return KToken(str(i), INT) def ltInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_ KApply: # noqa: N802 + r"""Instantiate the KAST term ```_<=Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_<=Int_`(i1, i2)``. + """ return KApply('_<=Int_', i1, i2) def gtInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_>Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_>Int_`(i1, i2)``. + """ return KApply('_>Int_', i1, i2) def geInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_>=Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_>=Int_`(i1, i2)``. + """ return KApply('_>=Int_', i1, i2) def eqInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_==Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_==Int_`(i1, i2)``. + """ return KApply('_==Int_', i1, i2) + + +def neqInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_=/=Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_=/=Int_`(i1, i2)``. + """ + return KApply('_=/=Int_', i1, i2) + + +def notInt(i: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```~Int_`(i)``. + + Args: + i: The integer operand. + + Returns: + The KAST term ```Int_`(i)``. + """ + return KApply('~Int_', i) + + +def expInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_^Int_`(i1, i2)``. + + Args: + i1: The base. + i2: The exponent. + + Returns: + The KAST term ```_^Int_`(i1, i2)``. + """ + return KApply('_^Int_', i1, i2) + + +def expModInt(i1: KInner, i2: KInner, i3: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_^%Int__`(i1, i2, i3)``. + + Args: + i1: The dividend. + i2: The divisior. + i3: The modulus. + + Returns: + The KAST term ```_^%Int__`(i1, i2, i3)``. + """ + return KApply('_^%Int__', i1, i2, i3) + + +def mulInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_*Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_*Int_`(i1, i2)``. + """ + return KApply('_*Int_', i1, i2) + + +def divInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_/Int_`(i1, i2)``. + + Args: + i1: The dividend. + i2: The divisor. + + Returns: + The KAST term ```_/Int_`(i1, i2)``. + """ + return KApply('_/Int_', i1, i2) + + +def modInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_%Int_`(i1, i2)``. + + Args: + i1: The dividend. + i2: The divisor. + + Returns: + The KAST term ```_%Int_`(i1, i2)``. + """ + return KApply('_%Int_', i1, i2) + + +def euclidDivInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_divInt_`(i1, i2)``. + + Args: + i1: The dividend. + i2: The divisor. + + Returns: + The KAST term ```_divInt_`(i1, i2)``. + """ + return KApply('_divInt_', i1, i2) + + +def euclidModInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_modInt_`(i1, i2)``. + + Args: + i1: The dividend. + i2: The divisor. + + Returns: + The KAST term ```_modInt_`(i1, i2)``. + """ + return KApply('_modInt_', i1, i2) + + +def addInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_+Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_+Int_`(i1, i2)``. + """ + return KApply('_+Int_', i1, i2) + + +def subInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_-Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_-Int_`(i1, i2)``. + """ + return KApply('_-Int_', i1, i2) + + +def rshiftInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_>>Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_>>Int_`(i1, i2)``. + """ + return KApply('_>>Int_', i1, i2) + + +def lshiftInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_< KApply: # noqa: N802 + r"""Instantiate the KAST term ```_&Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_&Int_`(i1, i2)``. + """ + return KApply('_&Int_', i1, i2) + + +def xorInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_xorInt_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_xorInt_`(i1, i2)``. + """ + return KApply('_xorInt_', i1, i2) + + +def orInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```_|Int_`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```_|Int_`(i1, i2)``. + """ + return KApply('_|Int_', i1, i2) + + +def minInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```minInt`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```minInt`(i1, i2)``. + """ + return KApply('minInt', i1, i2) + + +def maxInt(i1: KInner, i2: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```maxInt`(i1, i2)``. + + Args: + i1: The left operand. + i2: The right operand. + + Returns: + The KAST term ```maxInt`(i1, i2)``. + """ + return KApply('maxInt', i1, i2) + + +def absInt(i: KInner) -> KApply: # noqa: N802 + r"""Instantiate the KAST term ```absInt`(i)``. + + Args: + i: The integer operand. + + Returns: + The KAST term ```absInt`(i)``. + """ + return KApply('absInt', i) diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md index 1f42f186f28..be0803144fb 100644 --- a/pyk/src/tests/profiling/test-data/domains.md +++ b/pyk/src/tests/profiling/test-data/domains.md @@ -1257,8 +1257,8 @@ You can: You can compute the minimum and maximum `minInt` and `maxInt` of two integers. ```k - syntax Int ::= "minInt" "(" Int "," Int ")" [function, total, smt-hook((ite (< #1 #2) #1 #2)), hook(INT.min)] - | "maxInt" "(" Int "," Int ")" [function, total, smt-hook((ite (< #1 #2) #2 #1)), hook(INT.max)] + syntax Int ::= "minInt" "(" Int "," Int ")" [function, total, symbol(minInt), smt-hook((ite (< #1 #2) #1 #2)), hook(INT.min)] + | "maxInt" "(" Int "," Int ")" [function, total, symbol(maxInt), smt-hook((ite (< #1 #2) #2 #1)), hook(INT.max)] ``` ### Absolute value @@ -1266,7 +1266,7 @@ You can compute the minimum and maximum `minInt` and `maxInt` of two integers. You can compute the absolute value `absInt` of an integer. ```k - syntax Int ::= absInt ( Int ) [function, total, smt-hook((ite (< #1 0) (- 0 #1) #1)), hook(INT.abs)] + syntax Int ::= absInt ( Int ) [function, total, symbol(absInt), smt-hook((ite (< #1 0) (- 0 #1) #1)), hook(INT.abs)] ``` ### Log base 2 From 3bc2373e7000b46e61385195287b393fde85467f Mon Sep 17 00:00:00 2001 From: Juan C <38925412+JuanCoRo@users.noreply.github.com> Date: Tue, 25 Jun 2024 18:02:24 +0200 Subject: [PATCH 3/3] Expose `-Wno` via `ignore-warnings` kompile option (#4471) Address #4470 --- pyk/src/pyk/__main__.py | 1 + pyk/src/pyk/cli/args.py | 5 +++++ pyk/src/pyk/ktool/kompile.py | 10 ++++++++++ 3 files changed, 16 insertions(+) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 8664ccbeee6..4ad22390628 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -346,6 +346,7 @@ def exec_kompile(options: KompileCommandOptions) -> None: type_inference_mode=options.type_inference_mode, warnings=options.warnings, warnings_to_errors=options.warnings_to_errors, + ignore_warnings=options.ignore_warnings, no_exc_wrap=options.no_exc_wrap, ) except RuntimeError as err: diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index 356a17a5a57..3dbea7e72a6 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -206,6 +206,7 @@ class KompileOptions(Options): bison_lists: bool no_exc_wrap: bool outer_parsed_json: bool + ignore_warnings: list[str] @staticmethod def default() -> dict[str, Any]: @@ -230,6 +231,7 @@ def default() -> dict[str, Any]: 'bison_lists': False, 'no_exc_wrap': False, 'outer_parsed_json': False, + 'ignore_warnings': [], } @staticmethod @@ -475,6 +477,9 @@ def kompile_args(self) -> ArgumentParser: action='store_true', help='Do not wrap the output on the CLI.', ) + args.add_argument( + '--ignore-warnings', '-Wno', dest='ignore_warnings', action='append', help='Ignore provided warnings' + ) return args @cached_property diff --git a/pyk/src/pyk/ktool/kompile.py b/pyk/src/pyk/ktool/kompile.py index fa70fa496e0..6d2f7a87f9e 100644 --- a/pyk/src/pyk/ktool/kompile.py +++ b/pyk/src/pyk/ktool/kompile.py @@ -58,6 +58,7 @@ def kompile( type_inference_mode: str | TypeInferenceMode | None = None, warnings: str | Warnings | None = None, warnings_to_errors: bool = False, + ignore_warnings: Iterable[str] = (), no_exc_wrap: bool = False, # --- debug: bool = False, @@ -78,6 +79,7 @@ def kompile( type_inference_mode=type_inference_mode, warnings=warnings, warnings_to_errors=warnings_to_errors, + ignore_warnings=ignore_warnings, no_exc_wrap=no_exc_wrap, debug=debug, verbose=verbose, @@ -96,6 +98,7 @@ def kompile( type_inference_mode=type_inference_mode, warnings=warnings, warnings_to_errors=warnings_to_errors, + ignore_warnings=ignore_warnings, no_exc_wrap=no_exc_wrap, debug=debug, verbose=verbose, @@ -111,6 +114,7 @@ def _booster_kompile( type_inference_mode: str | TypeInferenceMode | None, warnings: str | Warnings | None, warnings_to_errors: bool, + ignore_warnings: Iterable[str], no_exc_wrap: bool, # --- debug: bool, @@ -146,6 +150,7 @@ def kompile_llvm() -> None: type_inference_mode=type_inference_mode, warnings=warnings, warnings_to_errors=warnings_to_errors, + ignore_warnings=ignore_warnings, no_exc_wrap=no_exc_wrap, debug=debug, verbose=verbose, @@ -161,6 +166,7 @@ def kompile_haskell() -> None: type_inference_mode=type_inference_mode, warnings=warnings, warnings_to_errors=warnings_to_errors, + ignore_warnings=ignore_warnings, no_exc_wrap=no_exc_wrap, debug=debug, verbose=verbose, @@ -273,6 +279,7 @@ def __call__( type_inference_mode: str | TypeInferenceMode | None = None, warnings: str | Warnings | None = None, warnings_to_errors: bool = False, + ignore_warnings: Iterable[str] = (), no_exc_wrap: bool = False, debug: bool = False, verbose: bool = False, @@ -321,6 +328,9 @@ def __call__( if outer_parsed_json: args += ['--outer-parsed-json'] + if ignore_warnings: + args += ['-Wno', ','.join(ignore_warnings)] + try: proc_res = run_process(args, logger=_LOGGER, cwd=cwd, check=check) except CalledProcessError as err: