diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index 106f8de707e..9dfe5840555 100644 --- a/.github/actions/with-docker/action.yml +++ b/.github/actions/with-docker/action.yml @@ -42,20 +42,13 @@ runs: run: | set -euxo pipefail - Z3_VERSION=4.8.15 + Z3_VERSION=$(cat deps/z3) K_VERSION=$(cat ${SUBDIR}package/version) USER=$(id -un) USER_ID=$(id -u) GROUP=$(id -gn) GROUP_ID=$(id -g) - docker build ${SUBDIR} \ - --build-arg USER=${USER} --build-arg USER_ID=${USER_ID} \ - --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID} \ - --build-arg BASE_OS=${BASE_OS} \ - --build-arg BASE_DISTRO=${BASE_DISTRO} \ - --tag z3:${BASE_DISTRO}-${Z3_VERSION} \ - --file ${SUBDIR}${DOCKERFILE}.z3 docker build ${SUBDIR} \ --build-arg USER=${USER} --build-arg USER_ID=${USER_ID} \ --build-arg GROUP=${GROUP} --build-arg GROUP_ID=${GROUP_ID} \ diff --git a/.github/workflows/Dockerfile b/.github/workflows/Dockerfile index 1e60083f4ef..26b22baa0de 100644 --- a/.github/workflows/Dockerfile +++ b/.github/workflows/Dockerfile @@ -1,8 +1,9 @@ ARG BASE_OS ARG BASE_DISTRO ARG K_VERSION + ARG Z3_VERSION -FROM z3:${BASE_DISTRO}-${Z3_VERSION} as Z3 +FROM runtimeverificationinc/z3:${BASE_OS}-${BASE_DISTRO}-${Z3_VERSION} as Z3 ARG BASE_OS ARG BASE_DISTRO @@ -46,6 +47,7 @@ RUN apt-get update \ libncurses5-dev \ libnss3-dev \ libreadline-dev \ + libsecp256k1-dev \ libsqlite3-dev \ libssl-dev \ libyaml-dev \ diff --git a/.github/workflows/Dockerfile.stack-deps b/.github/workflows/Dockerfile.stack-deps index 6e4b9b72328..0bb07c8cfd1 100644 --- a/.github/workflows/Dockerfile.stack-deps +++ b/.github/workflows/Dockerfile.stack-deps @@ -9,7 +9,9 @@ RUN apt-get update \ && apt-get upgrade --yes \ && apt-get install --yes \ curl \ - libtinfo-dev + libsecp256k1-dev \ + libtinfo-dev \ + pkg-config RUN curl -sSL https://get.haskellstack.org/ | sh @@ -31,4 +33,4 @@ RUN cd /home/$USER/.tmp-haskell && stack build --only-snapshot ENV LC_ALL=C.UTF-8 ADD --chown=$USER:$GROUP hs-backend-booster/src/main/native/hs-backend-booster/stack.yaml /home/$USER/.tmp-booster/ ADD --chown=$USER:$GROUP hs-backend-booster/src/main/native/hs-backend-booster/package.yaml /home/$USER/.tmp-booster/ -RUN cd /home/$USER/.tmp-booster && stack build --only-snapshot \ No newline at end of file +RUN cd /home/$USER/.tmp-booster && stack build --only-snapshot diff --git a/.github/workflows/Dockerfile.z3 b/.github/workflows/Dockerfile.z3 deleted file mode 100644 index c2ec54df25c..00000000000 --- a/.github/workflows/Dockerfile.z3 +++ /dev/null @@ -1,24 +0,0 @@ -ARG BASE_DISTRO -ARG BASE_OS -FROM ${BASE_OS}:${BASE_DISTRO} - -ENV TZ=America/Chicago -RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone - -RUN apt-get update \ - && apt-get upgrade --yes \ - && apt-get install --yes \ - clang \ - cmake \ - git \ - python3 - -ARG Z3_VERSION=4.8.15 -RUN git clone 'https://github.com/z3prover/z3' --branch=z3-${Z3_VERSION} \ - && cd z3 \ - && python3 scripts/mk_make.py \ - && cd build \ - && make -j8 \ - && make install \ - && cd ../.. \ - && rm -rf z3 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index da9fc261086..d70d5d49c42 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -63,7 +63,7 @@ jobs: trusted-public-keys = cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= hydra.iohk.io:f/Ea+s+dFdN+3Y/G+FDgSq+a5NEWhJGzdjvKNGv0/EQ= - name: Upload release.nix - uses: ttuegel/upload-release.nix@v1.0 + uses: runtimeverification/upload-release.nix@v1.1 with: token: ${{ secrets.GITHUB_TOKEN }} @@ -117,59 +117,7 @@ jobs: name: kore-exec.tar.gz path: | **/kore-exec.tar.gz - - ubuntu-focal: - name: 'K Ubuntu Focal Package' - runs-on: [self-hosted, linux, normal] - timeout-minutes: 90 - steps: - - uses: actions/checkout@v3 - - name: 'Build and Test Package' - uses: ./.github/actions/test-package - with: - os: ubuntu - distro: focal - llvm: 12 - jdk: 11 - pkg-name: kframework_amd64_ubuntu_focal.deb - build-package: package/debian/build-package focal - test-package: package/debian/test-package - - name: 'Upload Package to Release' - env: - GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }} - run: | - set -x - version=$(cat package/version) - cp kframework_amd64_ubuntu_focal.deb kframework_${version}_amd64_ubuntu_focal.deb - gh release upload --repo runtimeverification/k --clobber v${version} kframework_${version}_amd64_ubuntu_focal.deb - - name: 'Build, Test, and Push Dockerhub Image' - shell: bash {0} - env: - DOCKERHUB_PASSWORD: ${{ secrets.DOCKERHUB_PASSWORD }} - DOCKERHUB_REPO: runtimeverificationinc/kframework-k - run: | - set -euxo pipefail - version=$(cat package/version) - version_tag=ubuntu-focal-${version} - docker login --username rvdockerhub --password ${DOCKERHUB_PASSWORD} - docker image build . --file package/docker/Dockerfile.ubuntu-focal --tag ${DOCKERHUB_REPO}:${version_tag} - docker run --name k-package-docker-test-focal-${GITHUB_SHA} --rm -it --detach ${DOCKERHUB_REPO}:${version_tag} - docker exec -t k-package-docker-test-focal-${GITHUB_SHA} bash -c 'cd ~ && echo "module TEST imports BOOL endmodule" > test.k' - docker exec -t k-package-docker-test-focal-${GITHUB_SHA} bash -c 'cd ~ && kompile test.k --backend llvm' - docker exec -t k-package-docker-test-focal-${GITHUB_SHA} bash -c 'cd ~ && kompile test.k --backend haskell' - docker image push ${DOCKERHUB_REPO}:${version_tag} - - name: 'Clean up Docker Container' - if: always() - run: | - docker stop --time=0 k-package-docker-test-focal-${GITHUB_SHA} - - name: On Failure, Upload the kore-exec.tar.gz file to the Summary Page - if: failure() - uses: actions/upload-artifact@v2 - with: - name: kore-exec.tar.gz - path: | - **/kore-exec.tar.gz - + debian-bookworm: name: 'K Debian Bookworm Package' runs-on: [self-hosted, linux, normal] @@ -220,7 +168,7 @@ jobs: macos-build: name: 'Build MacOS Package' - runs-on: macos-11 + runs-on: macos-13 timeout-minutes: 120 environment: production needs: [set-release-id, source-tarball] @@ -273,7 +221,7 @@ jobs: git commit Formula/$PACKAGE.rb -m "Update ${PACKAGE} to ${VERSION}: part 1" ../kframework/package/macos/brew-build-and-update-to-local-bottle ${PACKAGE} ${VERSION} ${ROOT_URL} git reset HEAD^ - LOCAL_BOTTLE_NAME=$(basename $(find . -name "kframework--${VERSION}.big_sur.bottle*.tar.gz")) + LOCAL_BOTTLE_NAME=$(basename $(find . -name "kframework--${VERSION}.ventura.bottle*.tar.gz")) BOTTLE_NAME=$(echo ${LOCAL_BOTTLE_NAME#./} | sed 's!kframework--!kframework-!') ../kframework/package/macos/brew-update-to-final ${PACKAGE} ${VERSION} ${ROOT_URL} echo "path=${LOCAL_BOTTLE_NAME}" >> ${GITHUB_OUTPUT} @@ -302,7 +250,7 @@ jobs: macos-test: name: 'Test MacOS Package' - runs-on: macos-11 + runs-on: macos-13 timeout-minutes: 60 environment: production needs: [macos-build, set-release-id] @@ -400,7 +348,7 @@ jobs: name: 'Publish Release' runs-on: [self-hosted, linux, normal] environment: production - needs: [nix-release, macos-build, macos-test, source-tarball, ubuntu-jammy, ubuntu-focal, debian-bookworm, set-release-id, arch] + needs: [nix-release, macos-build, macos-test, source-tarball, ubuntu-jammy, debian-bookworm, set-release-id, arch] steps: - name: 'Check out code' uses: actions/checkout@v3 @@ -416,7 +364,7 @@ jobs: server-id: runtime.verification.snapshots server-username: MAVEN_USERNAME server-password: MAVEN_PASSWORD - + # Build and Run Tests in Docker - name: 'Set up Docker' uses: ./.github/actions/with-docker @@ -477,7 +425,7 @@ jobs: run: | sudo apt update --yes sudo apt install --yes wget texlive-xetex - sudo wget -nv -O- https://download.calibre-ebook.com/linux-installer.sh | sh /dev/stdin version=5.42.0 + sudo wget -nv -O- https://download.calibre-ebook.com/linux-installer.sh | sh /dev/stdin version=5.44.0 sudo wget https://github.com/jgm/pandoc/releases/download/2.18/pandoc-2.18-1-amd64.deb -O /tmp/pandoc.deb sudo dpkg -i /tmp/pandoc.deb - name: 'Checkout code and set up web build' diff --git a/deps/hs-backend-booster_release b/deps/hs-backend-booster_release index bc188d4565e..70e31b8f616 100644 --- a/deps/hs-backend-booster_release +++ b/deps/hs-backend-booster_release @@ -1 +1 @@ -6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566 +5a283f7c85c5b4f66ff477b494c5d138c54706e6 diff --git a/deps/z3 b/deps/z3 new file mode 100644 index 00000000000..53cf85e173b --- /dev/null +++ b/deps/z3 @@ -0,0 +1 @@ +4.12.1 diff --git a/flake.lock b/flake.lock index 5700d98865b..d3694fdac70 100644 --- a/flake.lock +++ b/flake.lock @@ -47,17 +47,17 @@ ] }, "locked": { - "lastModified": 1695839205, - "narHash": "sha256-9USUlWcL4YOseMJdQ1h4XvihR4/FG5zykykI7eY/13A=", + "lastModified": 1696961955, + "narHash": "sha256-HvYHO0Jo7NeV0u2Qi883rsuMyergBCcnbh/lbCGiFug=", "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566", + "rev": "5a283f7c85c5b4f66ff477b494c5d138c54706e6", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566", + "rev": "5a283f7c85c5b4f66ff477b494c5d138c54706e6", "type": "github" } }, @@ -247,11 +247,11 @@ "flake-compat_4": { "flake": false, "locked": { - "lastModified": 1673956053, - "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", "owner": "edolstra", "repo": "flake-compat", - "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", "type": "github" }, "original": { @@ -439,17 +439,17 @@ "z3-src": "z3-src" }, "locked": { - "lastModified": 1695129967, - "narHash": "sha256-wLMrn/a10zH3Zvl+ln2Z37b8n4c013i+udkKfFf61Eg=", + "lastModified": 1696881510, + "narHash": "sha256-NBYDOHpFy0/EGQtg1VeJWn7c8ciAZkhoflf0ZOTsVQs=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "63397c713d21322434d572281c1407d929a1189e", + "rev": "cdc83446c302961cd6abd2bca8c3e73dde8f6eab", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "85b5d086840a0f1e89499f086b50d7258598fc8b", + "rev": "cdc83446c302961cd6abd2bca8c3e73dde8f6eab", "type": "github" } }, @@ -465,17 +465,17 @@ "z3-src": "z3-src_2" }, "locked": { - "lastModified": 1695129967, - "narHash": "sha256-wLMrn/a10zH3Zvl+ln2Z37b8n4c013i+udkKfFf61Eg=", + "lastModified": 1696881510, + "narHash": "sha256-NBYDOHpFy0/EGQtg1VeJWn7c8ciAZkhoflf0ZOTsVQs=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "63397c713d21322434d572281c1407d929a1189e", + "rev": "cdc83446c302961cd6abd2bca8c3e73dde8f6eab", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "63397c713d21322434d572281c1407d929a1189e", + "rev": "cdc83446c302961cd6abd2bca8c3e73dde8f6eab", "type": "github" } }, @@ -784,11 +784,11 @@ "utils": "utils_2" }, "locked": { - "lastModified": 1695738370, - "narHash": "sha256-6H2WXHGjB2UvsZob2PAeV9o53q2LEKZ1LwDL5tV9fik=", + "lastModified": 1696962887, + "narHash": "sha256-UQDvJBCIrujCJYWipYBbSZkCKn0Z5Cm9dL5FBLOLVnM=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "4c9d0101951dc7fa4f07b0b03f5afd84331a40f7", + "rev": "a859fb6d77a48220d9d8b9314371933e8204c1d3", "type": "github" }, "original": { @@ -1227,11 +1227,11 @@ }, "nixpkgs_5": { "locked": { - "lastModified": 1695559356, - "narHash": "sha256-kXZ1pUoImD9OEbPCwpTz4tHsNTr4CIyIfXb3ocuR8sI=", + "lastModified": 1696983906, + "narHash": "sha256-L7GyeErguS7Pg4h8nK0wGlcUTbfUMDu+HMf1UcyP72k=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "261abe8a44a7e8392598d038d2e01f7b33cf26d0", + "rev": "bd1cde45c77891214131cbbea5b1203e485a9d51", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 441f83602c1..8823dd35c94 100644 --- a/flake.nix +++ b/flake.nix @@ -2,9 +2,9 @@ description = "K Framework"; inputs = { nixpkgs.url = "nixpkgs/nixos-23.05"; - haskell-backend.url = "github:runtimeverification/haskell-backend/63397c713d21322434d572281c1407d929a1189e"; + haskell-backend.url = "github:runtimeverification/haskell-backend/cdc83446c302961cd6abd2bca8c3e73dde8f6eab"; booster-backend = { - url = "github:runtimeverification/hs-backend-booster/6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566"; + url = "github:runtimeverification/hs-backend-booster/5a283f7c85c5b4f66ff477b494c5d138c54706e6"; # NB booster-backend will bring in another dependency on haskell-backend, # but the two are not necessarily the same (different more often than not). # We get two transitive dependencies on haskell-nix. diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java index b2fd5daa67a..d86230dbafa 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java @@ -26,6 +26,7 @@ public List getKompileModules() { mods.add(new AbstractModule() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bindOptions(HaskellBackendKModule.this::kompileOptions, binder()); installHaskellBackend(binder()); } @@ -54,6 +55,7 @@ public List getKRunModules() { return Collections.singletonList(new AbstractModule() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); installHaskellRewriter(binder()); } }); @@ -74,6 +76,7 @@ public List getKProveModules() { return Collections.singletonList(new AbstractModule() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); installHaskellBackend(binder()); installHaskellRewriter(binder()); } diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java index 5c20d442625..3a6649ef34c 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java @@ -2,12 +2,15 @@ package org.kframework.backend.haskell; import com.beust.jcommander.Parameter; +import com.google.inject.Inject; import org.kframework.backend.kore.ModuleToKORE; import org.kframework.utils.inject.RequestScoped; import org.kframework.utils.options.BaseEnumConverter; @RequestScoped public class HaskellKRunOptions { + @Inject + public HaskellKRunOptions() {} @Parameter(names="--haskell-backend-command", descriptionKey = "command", description="Command to run the Haskell backend execution engine.", hidden = true) diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java index 69a9c8b4b2c..081be372136 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java @@ -2,11 +2,14 @@ package org.kframework.backend.haskell; import com.beust.jcommander.Parameter; +import com.google.inject.Inject; import org.kframework.utils.inject.RequestScoped; @RequestScoped public class HaskellKompileOptions { + @Inject + public HaskellKompileOptions() {} @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", descriptionKey = "command", hidden = true) public String haskellBackendCommand = "kore-exec"; diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend index 63397c713d2..cdc83446c30 160000 --- a/haskell-backend/src/main/native/haskell-backend +++ b/haskell-backend/src/main/native/haskell-backend @@ -1 +1 @@ -Subproject commit 63397c713d21322434d572281c1407d929a1189e +Subproject commit cdc83446c302961cd6abd2bca8c3e73dde8f6eab diff --git a/hs-backend-booster/src/main/native/hs-backend-booster b/hs-backend-booster/src/main/native/hs-backend-booster index 6c2f5ab988e..5a283f7c85c 160000 --- a/hs-backend-booster/src/main/native/hs-backend-booster +++ b/hs-backend-booster/src/main/native/hs-backend-booster @@ -1 +1 @@ -Subproject commit 6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566 +Subproject commit 5a283f7c85c5b4f66ff477b494c5d138c54706e6 diff --git a/install-k b/install-k index 66754d5fbeb..16fa683d425 100755 --- a/install-k +++ b/install-k @@ -1,6 +1,6 @@ #!/bin/sh -e -K_VERSION=6.0.0 +K_VERSION=6.0.145 if [ `id -u` -ne 0 ]; then echo "$0: error: This script must be run as root." @@ -12,7 +12,7 @@ case $ID in ubuntu) CODENAME=$UBUNTU_CODENAME case $CODENAME in - bionic|focal|jammy) + jammy) ;; *) echo "Unsupported Ubuntu version, try building from source." diff --git a/k-distribution/INSTALL.md b/k-distribution/INSTALL.md index 9c9f509eb6b..48121501073 100644 --- a/k-distribution/INSTALL.md +++ b/k-distribution/INSTALL.md @@ -113,7 +113,7 @@ requires about ~1.4GB of dependencies and will take some time. ### Ubuntu Focal (20.04) ```sh -sudo apt install ./kframework_amd64_ubuntu_focal.deb +sudo apt install ./kframework_amd64_ubuntu_jammy.deb ``` ### Ubuntu Jammy (22.04) @@ -176,19 +176,19 @@ Docker images with K pre-installed are available at the [runtimeverification/kframework-k Docker Hub repository](https://hub.docker.com/repository/docker/runtimeverificationinc/kframework-k). Each release at `COMMIT_ID` has an image associated with it at -`runtimeverificationinc/kframework-k:ubuntu-focal-COMMIT_ID`. +`runtimeverificationinc/kframework-k:ubuntu-jammy-COMMIT_ID`. To run the image directly: ```sh -docker run -it runtimeverificationinc/kframework-k:ubuntu-focal-COMMIT_ID +docker run -it runtimeverificationinc/kframework-k:ubuntu-jammy-COMMIT_ID ``` and to make a Docker Image based on it, use the following line in your `Dockerfile`: ```Dockerfile -FROM runtimeverificationinc/kframework-k:ubuntu-focal-COMMIT_ID +FROM runtimeverificationinc/kframework-k:ubuntu-jammy-COMMIT_ID ``` We also create Ubuntu 22.04 images with the `ubuntu-jammy-COMMIT_ID` tags. diff --git a/k-distribution/include/kframework/builtin/README.md b/k-distribution/include/kframework/README.md similarity index 55% rename from k-distribution/include/kframework/builtin/README.md rename to k-distribution/include/kframework/README.md index 047f612b914..cee97c1a869 100644 --- a/k-distribution/include/kframework/builtin/README.md +++ b/k-distribution/include/kframework/README.md @@ -11,14 +11,14 @@ simpler. These files can be found under `include/kframework/builtin` in your K installation directory, and can be imported with `requires "FILENAME"` (without the path prefix). -- [domains](domains.md): Basic datatypes which are universally useful. -- [kast](kast.md): Representation of K internal data-structures (not to be +- [domains](builtin/domains.md): Basic datatypes which are universally useful. +- [kast](builtin/kast.md): Representation of K internal data-structures (not to be included in normal definitions). -- [prelude](prelude.md): Automatically included into every K definition. -- [ffi](ffi.md): FFI interface for calling out to native C code from K. -- [json](json.md): JSON datatype and parsers/unparsers for JSON strings. -- [rat](rat.md): Rational number representation. -- [substitution](substitution.md): Hooked implementation of capture-aware +- [prelude](builtin/prelude.md): Automatically included into every K definition. +- [ffi](builtin/ffi.md): FFI interface for calling out to native C code from K. +- [json](builtin/json.md): JSON datatype and parsers/unparsers for JSON strings. +- [rat](builtin/rat.md): Rational number representation. +- [substitution](builtin/substitution.md): Hooked implementation of capture-aware sustitution for K definitions. - [unification](https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/unification.k): Hooked implementation of unification exposed directly to K definitions. diff --git a/k-distribution/src/main/assembly/bin.xml b/k-distribution/src/main/assembly/bin.xml index 3ea8529e2bd..d322cd42ab8 100644 --- a/k-distribution/src/main/assembly/bin.xml +++ b/k-distribution/src/main/assembly/bin.xml @@ -69,7 +69,7 @@ ${project.parent.basedir}/package - /lib + /lib/kframework version diff --git a/k-distribution/src/main/scripts/bin/krun b/k-distribution/src/main/scripts/bin/krun index 7f684964a01..e5e88599fe4 100755 --- a/k-distribution/src/main/scripts/bin/krun +++ b/k-distribution/src/main/scripts/bin/krun @@ -37,12 +37,16 @@ filterSubst= if [[ "$OSTYPE" == "darwin"* ]]; then LLDB_FILE="$(dirname "$0")/../lib/kllvm/lldb/k_lldb_path" if [ -f "$LLDB_FILE" ]; then - DBG_CMD="$(cat "$LLDB_FILE") -- " + DBG_EXE="$(cat "$LLDB_FILE")" else - DBG_CMD="lldb --" + DBG_EXE="lldb" fi + DBG_CMD=" --" + DBG_FLAG=" -s " else - DBG_CMD="gdb --args " + DBG_EXE="gdb" + DBG_FLAG=" -x " + DBG_CMD=" --args " fi @@ -112,6 +116,10 @@ $KRUN options: parser. This can be overridden with -p. --debugger Launch the backend in a debugging console. Currently only supported on LLVM backend. + --debugger-batch Launch the backend in a debugging console in batch + mode. Currently only supported on LLVM backend. + --debugger-command FILE Execute GDB commands from FILE to debug program. + Currently only supported on LLVM backend. -d, --directory DIR [DEPRECATED] Look for a kompiled directory ending in "-kompiled" under the directory DIR. --dry-run Do not execute backend, but instead print the @@ -392,9 +400,24 @@ do ;; --debugger) - cmdprefix="$DBG_CMD" + cmdprefix="$DBG_EXE $DBG_CMD" ;; + --debugger-command) + debugCommandFile="$2" + cmdprefix="$DBG_EXE $DBG_FLAG $debugCommandFile $DBG_CMD" + shift + ;; + + --debugger-batch) + if [[ $cmdprefix == *gdb* || $cmdprefix == *lldb* ]]; then + cmdprefix="$DBG_EXE --batch $DBG_FLAG $debugCommandFile $DBG_CMD" + else + DBG_CMD=" --batch $DBG_CMD" + fi + ;; + + --statistics) statistics=true ;; diff --git a/k-distribution/src/main/scripts/lib/k b/k-distribution/src/main/scripts/lib/k index 34f4bf3b639..1d510a2ff60 100755 --- a/k-distribution/src/main/scripts/lib/k +++ b/k-distribution/src/main/scripts/lib/k @@ -22,7 +22,7 @@ for flag in "$@"; do fi if [[ -z "${version}" ]]; then - version="v"$(cat "${K_BASE}"/version) + version="v"$(cat "${K_BASE}"/kframework/version) fi echo "K version: ${version}" diff --git a/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala b/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala index d35afda1970..d6804496815 100644 --- a/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala +++ b/k-distribution/src/test/scala/org/kframework/backend/kore/KoreTest.scala @@ -65,18 +65,28 @@ class KoreTest { attributes.patterns.exists { case p: Application => p.head.ctr == name } } + // get the rewrite associated with a rule or equational axiom + // + // \and(\equals(requires, \dv("true")), \and(_, \rewrites(lhs, rhs))) + // \and(\top(), \and(_, \rewrites(lhs, rhs))) + // \rewrites(\and(\equals(requires, \dv("true")), lhs), \and(_, rhs)) + // \rewrites(\and(\top(), lhs), \and(_, rhs)) + // \implies(\equals(requires, \dv("true")), \and(\equals(lhs, rhs), _)) + // \implies(\top, \and(\equals(lhs, rhs), _)) + // \implies(\and(_, \equals(requires, \dv("true"))), \and(\equals(lhs, rhs), _)) + // \implies(\and(_, \top), \and(\equals(lhs, rhs), _)) + // \equals(lhs, rhs) def getRewrite(axiom: AxiomDeclaration): Option[GeneralizedRewrite] = { def go(pattern: Pattern): Option[GeneralizedRewrite] = { pattern match { - case And(_, Equals(_, _, _, _), And(_, _, rw @ Rewrites(_, _, _))) => Some(rw) - case And(_, Top(_), And(_, _, rw @ Rewrites(_, _, _))) => Some(rw) - case Rewrites(s, And(_, Equals(_, _, _, _), l), And(_, _, r)) => Some(B.Rewrites(s, l, r)) - case Rewrites(s, And(_, Top(_), l), And(_, _, r)) => Some(B.Rewrites(s, l, r)) - case Implies(_, Bottom(_), p) => go(p) - case Implies(_, Equals(_, _, _, _), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq) - case Implies(_, Top(_), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq) - case Implies(_, And(_, _, Equals(_, _, _, _)), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq) - case Implies(_, And(_, _, Top(_)), And(_, eq @ Equals(_, _, Application(_, _), _), _)) => Some(eq) + case And(_, Equals(_, _, _, _) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw) + case And(_, Top(_) +: And(_, _ +: (rw @ Rewrites(_, _, _)) +: Seq()) +: Seq()) => Some(rw) + case Rewrites(s, And(_, Equals(_, _, _, _) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r)) + case Rewrites(s, And(_, Top(_) +: l +: Seq()), And(_, _ +: r +: Seq())) => Some(B.Rewrites(s, l, r)) + case Implies(_, Equals(_, _, _, _), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq) + case Implies(_, Top(_), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq) + case Implies(_, And(_, _ +: Equals(_, _, _, _) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq) + case Implies(_, And(_, _ +: Top(_) +: Seq()), And(_, (eq @ Equals(_, _, Application(_, _), _)) +: _ +: Seq())) => Some(eq) case eq @ Equals(_, _, Application(_, _), _) => Some(eq) case _ => None @@ -91,7 +101,7 @@ class KoreTest { def symbols(pat: Pattern): Seq[SymbolOrAlias] = { pat match { - case And(_, p1, p2) => symbols(p1) ++ symbols(p2) + case And(_, ps) => ps.flatMap(symbols) case Application(s, ps) => Seq(s).filter(isConcrete) ++ ps.flatMap(symbols) case Ceil(_, _, p) => symbols(p) case Equals(_, _, p1, p2) => symbols(p1) ++ symbols(p2) @@ -103,7 +113,7 @@ class KoreTest { case Mem(_, _, p1, p2) => symbols(p1) ++ symbols(p2) // case Next(_, p) => symbols(p) case Not(_, p) => symbols(p) - case Or(_, p1, p2) => symbols(p1) ++ symbols(p2) + case Or(_, ps) => ps.flatMap(symbols) case Rewrites(_, p1, p2) => symbols(p1) ++ symbols(p2) case _ => Seq() } diff --git a/k-distribution/tests/builtins/collections/test-set2list-2.col.out b/k-distribution/tests/builtins/collections/test-set2list-2.col.out index e698f880343..ff7f12e8d9b 100644 --- a/k-distribution/tests/builtins/collections/test-set2list-2.col.out +++ b/k-distribution/tests/builtins/collections/test-set2list-2.col.out @@ -1,6 +1,6 @@ - ListItem ( 4 ) - ListItem ( 3 ) + ListItem ( 1 ) ListItem ( 2 ) - ListItem ( 1 ) ~> . + ListItem ( 3 ) + ListItem ( 4 ) ~> . diff --git a/k-distribution/tests/builtins/collections/test-set2list-3.col.out b/k-distribution/tests/builtins/collections/test-set2list-3.col.out index 42af7fc9c87..af1ebe42178 100644 --- a/k-distribution/tests/builtins/collections/test-set2list-3.col.out +++ b/k-distribution/tests/builtins/collections/test-set2list-3.col.out @@ -1,5 +1,5 @@ - ListItem ( 4 ) + ListItem ( 1 ) ListItem ( 3 ) - ListItem ( 1 ) ~> . + ListItem ( 4 ) ~> . diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile b/k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile new file mode 100644 index 00000000000..5ab56c86a70 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/Makefile @@ -0,0 +1,6 @@ +DEF=test +EXT=test +TESTDIR=. +KAST_FLAGS=--debug-tokens + +include ../../../include/kframework/ktest.mak diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast new file mode 100644 index 00000000000..0d8c763edc3 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast @@ -0,0 +1,14 @@ +1 + 2 + aaaaaaaaaaaa + + + + + + + + + + ++ 10000000 ++ "str" ++ "long str that breaks alighnment" diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out new file mode 100644 index 00000000000..903a7ba1fd5 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/a.test.kast.out @@ -0,0 +1,15 @@ +|"Match" | (location) | Terminal | +|---------------------------------------------------------------------------------|---------------|---------------------| +|"1" | (1,1,1,2) | r"[\\+-]?[0-9]+" | +|"+" | (1,3,1,4) | "+" | +|"2" | (1,5,1,6) | r"[\\+-]?[0-9]+" | +|"+" | (1,7,1,8) | "+" | +|"aaaaaaaaaaaa" | (1,9,1,21) | r"[a-z][a-zA-Z0-9]*"| +|"+" | (12,1,12,2) | "+" | +|"10000000" | (12,3,12,11) | r"[\\+-]?[0-9]+" | +|"+" | (13,1,13,2) | "+" | +|"\"str\"" | (13,3,13,8) | r"[\\\"](([^\\\"\\n\\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]"| +|"+" | (14,1,14,2) | "+" | +|"\"long str that breaks alighnment\"" | (14,3,14,103) | r"[\\\"](([^\\\"\\n\\r\\\\])|([\\\\][nrtf\\\"\\\\])|([\\\\][x][0-9a-fA-F]{2})|([\\\\][u][0-9a-fA-F]{4})|([\\\\][U][0-9a-fA-F]{8}))*[\\\"]"| +|"" | (15,1,15,1) | "" | + diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast new file mode 100644 index 00000000000..f845bb7df41 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast @@ -0,0 +1 @@ +1 + 2 + aaa diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out new file mode 100644 index 00000000000..1525daf1bc8 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/b.test.kast.out @@ -0,0 +1,9 @@ +|"Match" | (location) | Terminal | +|--------|------------|---------------------| +|"1" | (1,1,1,2) | r"[\\+-]?[0-9]+" | +|"+" | (1,3,1,4) | "+" | +|"2" | (1,5,1,6) | r"[\\+-]?[0-9]+" | +|"+" | (1,7,1,8) | "+" | +|"aaa" | (1,9,1,12) | r"[a-z][a-zA-Z0-9]*"| +|"" | (2,1,2,1) | "" | + diff --git a/k-distribution/tests/regression-new/issue-3647-debugTokens/test.k b/k-distribution/tests/regression-new/issue-3647-debugTokens/test.k new file mode 100644 index 00000000000..90b98cf29a9 --- /dev/null +++ b/k-distribution/tests/regression-new/issue-3647-debugTokens/test.k @@ -0,0 +1,14 @@ +// Copyright (c) K Team. All Rights Reserved. + +module TEST-SYNTAX + imports INT-SYNTAX + imports ID-SYNTAX + imports STRING-SYNTAX + syntax Exp ::= Exp "+" Exp [left] | Int | Id | String +endmodule + +module TEST + imports TEST-SYNTAX + configuration $PGM:Exp + +endmodule diff --git a/kernel/pom.xml b/kernel/pom.xml index c932c02dcc6..aa1541af51d 100644 --- a/kernel/pom.xml +++ b/kernel/pom.xml @@ -32,13 +32,13 @@ com.google.inject guice - 4.0-beta5 + 4.0 no_aop com.google.inject.extensions guice-multibindings - 4.0-beta5 + 4.0 com.google.inject @@ -49,7 +49,7 @@ com.google.inject.extensions guice-grapher - 4.0-beta5 + 4.0 com.google.inject @@ -60,7 +60,7 @@ com.google.inject.extensions guice-throwingproviders - 4.0-beta5 + 4.0 com.google.inject diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index 10fa815fecb..a00ac5b32a8 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -713,7 +713,7 @@ private void genNoJunkAxiom(Sort sort, StringBuilder sb) { sbTemp.append(" axiom{} "); boolean hasToken = false; int numTerms = 0; - sbTemp.append("\\right-assoc{}(\\or{"); + sbTemp.append("\\or{"); convert(sort, sbTemp); sbTemp.append("} ("); for (Production prod : iterable(mutable(module.productionsForSort()).getOrDefault(sort.head(), Set()).toSeq().sorted(Production.ord()))) { @@ -776,7 +776,7 @@ private void genNoJunkAxiom(Sort sort, StringBuilder sb) { } sbTemp.append("\\bottom{"); convert(sort, sbTemp); - sbTemp.append("}())) [constructor{}()] // no junk"); + sbTemp.append("}()) [constructor{}()] // no junk"); if (hasToken && !METAVAR) { sbTemp.append(" (TODO: fix bug with \\dv)"); } diff --git a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java b/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java index 9156ed7c766..c222faa9924 100644 --- a/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java +++ b/kernel/src/main/java/org/kframework/kast/KastFrontEnd.java @@ -135,35 +135,39 @@ public int run() { Source source = options.source(); try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(mod, true, null)) { - Tuple2, K>, Set> res = parseInModule.parseString(stringToParse, sort, startSymbolLocation, source); - kem.addAllKException(res._2().stream().map(KEMException::getKException).collect(Collectors.toSet())); - if (res._1().isLeft()) { - throw res._1().left().get().iterator().next(); + if (options.debugTokens) + System.out.println(parseInModule.tokenizeString(stringToParse, source)); + else { + Tuple2, K>, Set> res = parseInModule.parseString(stringToParse, sort, startSymbolLocation, source); + kem.addAllKException(res._2().stream().map(KEMException::getKException).collect(Collectors.toSet())); + if (res._1().isLeft()) { + throw res._1().left().get().iterator().next(); + } + // important to get the extension module for unparsing because it contains generated syntax + // like casts, projections and others + Module unparsingMod = parseInModule.getExtensionModule(); + K parsed = new TreeNodesToKORE(Outer::parseSort, true).down(res._1().right().get()); + + if (options.expandMacros) { + parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed); + } + ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(mod); + LabelInfo labelInfo = new LabelInfoFromModule(mod); + SortInfo sortInfo = SortInfo.fromModule(mod); + + Rule r = Rule.apply(parsed, BooleanUtils.TRUE, BooleanUtils.TRUE, Att.empty()); + if (options.steps.contains(KompileSteps.anonVars)) + r = (Rule) new ResolveAnonVar().resolve(r); + r = (Rule) new ResolveSemanticCasts(false).resolve(r); // move casts to side condition predicates + r = (Rule) new ConstantFolding().fold(unparsingMod, r); + r = (Rule) new CloseCells(configInfo, sortInfo, labelInfo).close(r); + if (options.steps.contains(KompileSteps.concretizeCells)) { + r = (Rule) new AddImplicitComputationCell(configInfo, labelInfo).apply(mod, r); + r = (Rule) new ConcretizeCells(configInfo, labelInfo, sortInfo, mod).concretize(mod, r); + } + K result = r.body(); + kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), result, sort); } - // important to get the extension module for unparsing because it contains generated syntax - // like casts, projections and others - Module unparsingMod = parseInModule.getExtensionModule(); - K parsed = new TreeNodesToKORE(Outer::parseSort, true).down(res._1().right().get()); - - if (options.expandMacros) { - parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed); - } - ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(mod); - LabelInfo labelInfo = new LabelInfoFromModule(mod); - SortInfo sortInfo = SortInfo.fromModule(mod); - - Rule r = Rule.apply(parsed, BooleanUtils.TRUE, BooleanUtils.TRUE, Att.empty()); - if (options.steps.contains(KompileSteps.anonVars)) - r = (Rule) new ResolveAnonVar().resolve(r); - r = (Rule) new ResolveSemanticCasts(false).resolve(r); // move casts to side condition predicates - r = (Rule) new ConstantFolding().fold(unparsingMod, r); - r = (Rule) new CloseCells(configInfo, sortInfo, labelInfo).close(r); - if (options.steps.contains(KompileSteps.concretizeCells)) { - r = (Rule) new AddImplicitComputationCell(configInfo, labelInfo).apply(mod, r); - r = (Rule) new ConcretizeCells(configInfo, labelInfo, sortInfo, mod).concretize(mod, r); - } - K result = r.body(); - kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), result, sort); } sw.printTotal("Total"); @@ -210,17 +214,21 @@ public int run() { } else { Reader stringToParse = options.stringToParse(); Source source = options.source(); - K parsed = kread.prettyRead(parsingMod, sort, startSymbolLocation, def, source, FileUtil.read(stringToParse)); + if (options.debugTokens) + System.out.println(kread.showTokens(parsingMod, def, FileUtil.read(stringToParse), source)); + else { + K parsed = kread.prettyRead(parsingMod, sort, startSymbolLocation, def, source, FileUtil.read(stringToParse)); - if (options.expandMacros) { - parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed); - } + if (options.expandMacros) { + parsed = ExpandMacros.forNonSentences(unparsingMod, files.get(), def.kompileOptions, false).expand(parsed); + } - if (sort.equals(Sorts.K())) { - sort = Sorts.KItem(); - } + if (sort.equals(Sorts.K())) { + sort = Sorts.KItem(); + } - kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), parsed, sort); + kprint.get().prettyPrint(def.kompiledDefinition, unparsingMod, s -> kprint.get().outputFile(s), parsed, sort); + } } sw.printTotal("Total"); diff --git a/kernel/src/main/java/org/kframework/kast/KastModule.java b/kernel/src/main/java/org/kframework/kast/KastModule.java index aeb3976a48d..a28605ce26d 100644 --- a/kernel/src/main/java/org/kframework/kast/KastModule.java +++ b/kernel/src/main/java/org/kframework/kast/KastModule.java @@ -21,6 +21,7 @@ public class KastModule extends AbstractModule { @Override public void configure() { + binder().requireAtInjectOnConstructors(); bind(FrontEnd.class).to(KastFrontEnd.class); bind(Tool.class).toInstance(Tool.KAST); diff --git a/kernel/src/main/java/org/kframework/kast/KastOptions.java b/kernel/src/main/java/org/kframework/kast/KastOptions.java index 2aaa084b516..7ef74e430c6 100644 --- a/kernel/src/main/java/org/kframework/kast/KastOptions.java +++ b/kernel/src/main/java/org/kframework/kast/KastOptions.java @@ -31,6 +31,9 @@ @RequestScoped public final class KastOptions { + @Inject + public KastOptions() {} + @Parameter(description="") private List parameters; @@ -155,4 +158,7 @@ public Class enumClass() { return InputModes.class; } } + + @Parameter(names="--debug-tokens", description="Print a Markdown table of tokens matched by the scanner. Useful for debugging parsing errors.") + public boolean debugTokens = false; } diff --git a/kernel/src/main/java/org/kframework/kdep/KDepModule.java b/kernel/src/main/java/org/kframework/kdep/KDepModule.java index c068f105368..ed6af4762b9 100644 --- a/kernel/src/main/java/org/kframework/kdep/KDepModule.java +++ b/kernel/src/main/java/org/kframework/kdep/KDepModule.java @@ -22,7 +22,7 @@ public class KDepModule extends AbstractModule { @Override protected void configure() { - + binder().requireAtInjectOnConstructors(); bind(FrontEnd.class).to(KDepFrontEnd.class); bind(Tool.class).toInstance(Tool.KDEP); diff --git a/kernel/src/main/java/org/kframework/kdep/KDepOptions.java b/kernel/src/main/java/org/kframework/kdep/KDepOptions.java index d830c3b8bf3..c65cc98273e 100644 --- a/kernel/src/main/java/org/kframework/kdep/KDepOptions.java +++ b/kernel/src/main/java/org/kframework/kdep/KDepOptions.java @@ -3,6 +3,7 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.ParametersDelegate; +import com.google.inject.Inject; import org.kframework.main.GlobalOptions; import org.kframework.utils.inject.RequestScoped; import org.kframework.utils.options.OuterParsingOptions; @@ -16,6 +17,9 @@ @RequestScoped public class KDepOptions { + @Inject + public KDepOptions() {} + @ParametersDelegate public transient GlobalOptions global = new GlobalOptions(); diff --git a/kernel/src/main/java/org/kframework/kil/loader/Context.java b/kernel/src/main/java/org/kframework/kil/loader/Context.java index 2bc8a8252db..a136a3922e6 100644 --- a/kernel/src/main/java/org/kframework/kil/loader/Context.java +++ b/kernel/src/main/java/org/kframework/kil/loader/Context.java @@ -19,6 +19,9 @@ @RequestScoped public class Context implements Serializable { + @Inject + public Context() {} + /** * Represents a map from all Klabels or attributes in string representation * to sets of corresponding productions. diff --git a/kernel/src/main/java/org/kframework/kompile/BackendModule.java b/kernel/src/main/java/org/kframework/kompile/BackendModule.java index 35b91d2654f..5425cabee5c 100644 --- a/kernel/src/main/java/org/kframework/kompile/BackendModule.java +++ b/kernel/src/main/java/org/kframework/kompile/BackendModule.java @@ -14,6 +14,7 @@ public class BackendModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); MapBinder backendBinder = MapBinder.newMapBinder( binder(), String.class, org.kframework.compile.Backend.class); backendBinder.addBinding("kore").to(KoreBackend.class); diff --git a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java index a2342afd40d..289619a9fa7 100644 --- a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java +++ b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java @@ -207,6 +207,12 @@ public K parseSingleTerm(Module module, Sort programStartSymbol, String startSym } } + public String showTokens(Module module, FileUtil files, String s, Source source) { + try (ParseInModule parseInModule = RuleGrammarGenerator.getCombinedGrammar(module, true, files)) { + return parseInModule.tokenizeString(s, source); + } + } + public Module getExtensionModule(Module module, FileUtil files) { return RuleGrammarGenerator.getCombinedGrammar(module, true, files).getExtensionModule(); } diff --git a/kernel/src/main/java/org/kframework/kompile/KompileModule.java b/kernel/src/main/java/org/kframework/kompile/KompileModule.java index 10ed758e44e..3757d7c6432 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileModule.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileModule.java @@ -25,6 +25,7 @@ public KompileModule() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(FrontEnd.class).to(KompileFrontEnd.class); bind(Tool.class).toInstance(Tool.KOMPILE); diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java index 8d494435b6d..ba96c409fdd 100644 --- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java +++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java @@ -3,6 +3,7 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.ParametersDelegate; +import com.google.inject.Inject; import org.apache.commons.io.FilenameUtils; import org.kframework.backend.Backends; import org.kframework.main.GlobalOptions; @@ -23,7 +24,8 @@ @RequestScoped public class KompileOptions implements Serializable { - + @Inject + public KompileOptions() {} /** * WARNING: this field will be non-null in kompile tool, but null when KompileOption is deserialized, diff --git a/kernel/src/main/java/org/kframework/kprove/KProveModule.java b/kernel/src/main/java/org/kframework/kprove/KProveModule.java index 84b17c42eb3..ca375b76ad7 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProveModule.java +++ b/kernel/src/main/java/org/kframework/kprove/KProveModule.java @@ -20,6 +20,7 @@ public class KProveModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(FrontEnd.class).to(KProveFrontEnd.class); bind(Tool.class).toInstance(Tool.KPROVE); diff --git a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java index b5b59d83917..d25a5b6b6c3 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java +++ b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java @@ -4,6 +4,7 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.ParametersDelegate; +import com.google.inject.Inject; import org.kframework.unparser.PrintOptions; import org.kframework.main.GlobalOptions; import org.kframework.utils.file.FileUtil; @@ -20,6 +21,8 @@ @RequestScoped public class KProveOptions { + @Inject + public KProveOptions() {} @ParametersDelegate private final transient GlobalOptions global = new GlobalOptions(); diff --git a/kernel/src/main/java/org/kframework/kprove/RewriterModule.java b/kernel/src/main/java/org/kframework/kprove/RewriterModule.java index 5670711aa9b..90ea42f76b8 100644 --- a/kernel/src/main/java/org/kframework/kprove/RewriterModule.java +++ b/kernel/src/main/java/org/kframework/kprove/RewriterModule.java @@ -17,6 +17,7 @@ public class RewriterModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(FileUtil.class); } diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java index 2ae3035c72b..93328edf004 100644 --- a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java +++ b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternModule.java @@ -22,6 +22,7 @@ public class KSearchPatternModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(FrontEnd.class).to(KSearchPatternFrontEnd.class); bind(Tool.class).toInstance(Tool.KSEARCHPATTERN); diff --git a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java index 1c2d9a32a08..9fcc1baec84 100644 --- a/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java +++ b/kernel/src/main/java/org/kframework/ksearchpattern/KSearchPatternOptions.java @@ -3,6 +3,7 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.ParametersDelegate; +import com.google.inject.Inject; import org.kframework.main.GlobalOptions; import org.kframework.utils.inject.RequestScoped; import org.kframework.utils.options.DefinitionLoadingOptions; @@ -16,6 +17,9 @@ @RequestScoped public class KSearchPatternOptions { + @Inject + public KSearchPatternOptions() {} + @ParametersDelegate public transient GlobalOptions global = new GlobalOptions(); diff --git a/kernel/src/main/java/org/kframework/kserver/KServerModule.java b/kernel/src/main/java/org/kframework/kserver/KServerModule.java index f8e9f4d57bb..865cdfc76f4 100644 --- a/kernel/src/main/java/org/kframework/kserver/KServerModule.java +++ b/kernel/src/main/java/org/kframework/kserver/KServerModule.java @@ -20,6 +20,7 @@ public class KServerModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(Tool.class).toInstance(Tool.KSERVER); bind(FrontEnd.class).to(KServerFrontEnd.class); diff --git a/kernel/src/main/java/org/kframework/kserver/KServerOptions.java b/kernel/src/main/java/org/kframework/kserver/KServerOptions.java index 322b689b874..b09695b0ac3 100644 --- a/kernel/src/main/java/org/kframework/kserver/KServerOptions.java +++ b/kernel/src/main/java/org/kframework/kserver/KServerOptions.java @@ -1,6 +1,7 @@ // Copyright (c) K Team. All Rights Reserved. package org.kframework.kserver; +import com.google.inject.Inject; import org.kframework.main.GlobalOptions; import org.kframework.utils.inject.RequestScoped; @@ -10,6 +11,9 @@ @RequestScoped public class KServerOptions { + @Inject + public KServerOptions() {} + @ParametersDelegate public transient GlobalOptions global = new GlobalOptions(); diff --git a/kernel/src/main/java/org/kframework/main/AbstractKModule.java b/kernel/src/main/java/org/kframework/main/AbstractKModule.java index 9fc12a9cb48..2a8dd35361b 100644 --- a/kernel/src/main/java/org/kframework/main/AbstractKModule.java +++ b/kernel/src/main/java/org/kframework/main/AbstractKModule.java @@ -37,6 +37,7 @@ public List, Boolean>> kproveOptions() { } protected void bindOptions(Supplier, Boolean>>> action, Binder binder) { + binder.requireAtInjectOnConstructors(); Multibinder optionsBinder = Multibinder.newSetBinder(binder, Object.class, Options.class); for (Pair, Boolean> option : action.get()) { optionsBinder.addBinding().to(option.getKey()); @@ -81,6 +82,7 @@ public List getDefinitionSpecificKEqModules() { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); //bind backend implementations of tools to their interfaces } }); diff --git a/kernel/src/main/java/org/kframework/main/FrontEnd.java b/kernel/src/main/java/org/kframework/main/FrontEnd.java index 7417d75ee92..08e015488e0 100644 --- a/kernel/src/main/java/org/kframework/main/FrontEnd.java +++ b/kernel/src/main/java/org/kframework/main/FrontEnd.java @@ -2,6 +2,7 @@ package org.kframework.main; import com.beust.jcommander.ParameterException; +import com.google.inject.Inject; import com.google.inject.Provider; import org.kframework.utils.ExitOnTimeoutThread; import org.kframework.utils.InterrupterRunnable; @@ -22,6 +23,7 @@ public abstract class FrontEnd { private final JarInfo jarInfo; private final Provider files; + @Inject public FrontEnd( KExceptionManager kem, GlobalOptions globalOptions, diff --git a/kernel/src/main/java/org/kframework/main/GlobalOptions.java b/kernel/src/main/java/org/kframework/main/GlobalOptions.java index f0ae7d82c66..d78fad84535 100644 --- a/kernel/src/main/java/org/kframework/main/GlobalOptions.java +++ b/kernel/src/main/java/org/kframework/main/GlobalOptions.java @@ -19,13 +19,6 @@ public final class GlobalOptions { public GlobalOptions() {} - //TODO(dwightguth): remove in Guice 4.0 - /** - * Prevents instantiation by Guice when not explicitly configured in a Module. - */ - @Inject - public GlobalOptions(Void v) {} - public GlobalOptions(boolean debug, Warnings warnings, boolean verbose) { this.debug = debug; this.warnings = warnings; diff --git a/kernel/src/main/java/org/kframework/parser/KRead.java b/kernel/src/main/java/org/kframework/parser/KRead.java index c5b50cf4afb..6ed83e89188 100644 --- a/kernel/src/main/java/org/kframework/parser/KRead.java +++ b/kernel/src/main/java/org/kframework/parser/KRead.java @@ -51,6 +51,10 @@ public KRead( this.globalOptions = globalOptions; } + public String showTokens(Module mod, CompiledDefinition def, String stringToParse, Source source) { + return def.showTokens(mod, files, stringToParse, source); + } + public K prettyRead(Module mod, Sort sort, String startSymbolLocation, CompiledDefinition def, Source source, String stringToParse) { return prettyRead(mod, sort, startSymbolLocation, def, source, stringToParse, this.input); } diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java index 8f456d44ba5..21f12734444 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java +++ b/kernel/src/main/java/org/kframework/parser/inner/ParseInModule.java @@ -7,6 +7,8 @@ import org.kframework.attributes.Source; import org.kframework.builtin.Sorts; import org.kframework.definition.Module; +import org.kframework.definition.Terminal; +import org.kframework.definition.TerminalLike; import org.kframework.kore.K; import org.kframework.kore.Sort; import org.kframework.main.GlobalOptions; @@ -16,6 +18,7 @@ import org.kframework.parser.inner.kernel.EarleyParser; import org.kframework.parser.inner.kernel.Scanner; import org.kframework.parser.outer.Outer; +import org.kframework.utils.StringUtil; import org.kframework.utils.errorsystem.KEMException; import org.kframework.utils.file.FileUtil; import scala.Tuple2; @@ -32,10 +35,9 @@ import java.io.Serializable; import java.io.Writer; import java.nio.charset.StandardCharsets; -import java.util.Collections; -import java.util.Queue; -import java.util.Set; +import java.util.*; import java.util.concurrent.ConcurrentLinkedQueue; +import java.util.stream.Collectors; /** * A wrapper that takes a module and one can call the parser @@ -163,6 +165,52 @@ public void initialize() { } } + /** + * Print the list of tokens matched by the scanner, the location and the Regex Terminal + * The output is a valid Markdown table. + */ + public String tokenizeString(String input, Source source) { + StringBuilder sb = new StringBuilder(); + try (Scanner scanner = getScanner()) { + EarleyParser.ParserMetadata mdata = new EarleyParser.ParserMetadata(input, scanner, source, 1, 1); + Map kind2Token = + scanner.getTokens().entrySet().stream().map(a -> new Tuple2<>(a.getValue()._1, a.getKey())) + .collect(Collectors.toMap(Tuple2::_1, Tuple2::_2)); + List lines = mdata.getLines(); + List columns = mdata.getColumns(); + int maxTokenLen = 7, maxLocLen = 10, maxTerminalLen = 10; + List locs = new ArrayList<>(); + List tokens = new ArrayList<>(); + List terminals = new ArrayList<>(); + List words = mdata.getWords(); + for (Scanner.Token word : mdata.getWords()) { + String loc = String.format("(%d,%d,%d,%d)", + lines.get(word.startLoc), columns.get(word.startLoc), + lines.get(word.endLoc), columns.get(word.endLoc)); + locs.add(loc); + maxLocLen = Math.max(maxLocLen, loc.length()); + String tok = StringUtil.enquoteKString(word.value); + tokens.add(tok); + maxTokenLen = Math.max(maxTokenLen, tok.length()); + String terminal = kind2Token.getOrDefault(word.kind, Terminal.apply("")).toString(); + terminals.add(terminal); + maxTerminalLen = Math.max(maxTerminalLen, terminal.length()); + } + // if the token is absurdly large limit the column to 80 chars to maintain alignment + maxTokenLen = Math.min(maxTokenLen, 80); + maxTerminalLen = Math.min(maxTerminalLen, 20); + sb.append(String.format("|%-" + maxTokenLen + "s | %-" + maxLocLen + "s | %-" + maxTerminalLen + "s|\n", + "\"Match\"", "(location)", "Terminal")); + sb.append(String.format("|-%s|--%s|-%s|\n", "-".repeat(maxTokenLen), "-".repeat(maxLocLen), "-".repeat(maxTerminalLen))); + for (int i = 0; i < words.size(); i++) { + Scanner.Token word = words.get(i); + sb.append(String.format("|%-" + maxTokenLen + "s | %-" + maxLocLen + "s | %-" + maxTerminalLen + "s|\n", + tokens.get(i), locs.get(i), terminals.get(i))); + } + } + return sb.toString(); + } + public Tuple2, K>, Set> parseString(String input, Sort startSymbol, String startSymbolLocation, Source source) { try (Scanner scanner = getScanner()) { diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java index 7f48bda662e..8f3f541295e 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java +++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java @@ -1,6 +1,7 @@ // Copyright (c) K Team. All Rights Reserved. package org.kframework.parser.inner.kernel; +import com.google.common.primitives.Ints; import org.apache.commons.codec.binary.StringUtils; import org.jetbrains.annotations.NotNull; import org.kframework.attributes.Att; @@ -23,18 +24,7 @@ import org.pcollections.ConsPStack; import org.pcollections.PStack; -import java.nio.charset.StandardCharsets; -import java.util.Arrays; -import java.util.ArrayList; -import java.util.BitSet; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Iterator; -import java.util.List; -import java.util.Map; -import java.util.Objects; -import java.util.Optional; -import java.util.Set; +import java.util.*; import java.util.stream.Collectors; import static org.kframework.Collections.*; @@ -525,7 +515,7 @@ public void finish() { * Metadata about the state of the sentence being parsed. We collect this all in a single place in order to simplify * the type signatures of many methods. */ - private static class ParserMetadata { + public static class ParserMetadata { /** * @param input The sentence being parsed * @param scanner The scanner to use to tokenize the sentence @@ -583,15 +573,27 @@ public ParserMetadata(String input, Scanner scanner, Source source, int startLin } // the list of tokens in the sentence - Scanner.Token[] words; + final Scanner.Token[] words; // an array containing the line of each character in the input sentence - int[] lines; + final int[] lines; // an array containing the column of each character in the input sentence - int[] columns; + final int[] columns; // a Source containing the file the sentence was parsed from Source source; // the original un-tokenized input sentence String input; + + public List getWords() { + return List.of(words); + } + + public List getLines() { + return Collections.unmodifiableList(Ints.asList(lines)); + } + + public List getColumns() { + return Collections.unmodifiableList(Ints.asList(columns)); + } } /** diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java index d59300a5b39..b71d0c44c16 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java +++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java @@ -30,14 +30,7 @@ import java.nio.ByteOrder; import java.nio.file.StandardCopyOption; import java.nio.file.Files; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.HashSet; -import java.util.LinkedHashMap; -import java.util.List; -import java.util.Map; -import java.util.Set; -import java.util.TreeMap; +import java.util.*; import java.util.concurrent.Semaphore; import java.util.function.BiConsumer; import java.util.stream.Collectors; @@ -57,6 +50,10 @@ public class Scanner implements AutoCloseable { public static final String COMPILER = OS.current().equals(OS.OSX) ? "clang" : "gcc"; + public Map> getTokens() { + return Collections.unmodifiableMap(tokens); + } + public static Map> getTokens(Module module) { Map tokens = new TreeMap<>(); Set terminals = new HashSet<>(); @@ -349,10 +346,10 @@ public int resolve(TerminalLike terminal) { } public static class Token { - final int kind; - final String value; - final int startLoc; - final int endLoc; + public final int kind; + public final String value; + public final int startLoc; + public final int endLoc; public Token(int kind, String value, long startLoc, long endLoc) { this.kind = kind; diff --git a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java index c74146e45ea..74c860c80da 100644 --- a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java +++ b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java @@ -23,14 +23,6 @@ public PrintOptions(OutputModes output) { this.output = output; } - //TODO(dwightguth): remove in Guice 4.0 - /** - * Prevents instantiation by Guice when not explicitly configured in a Module. - */ - @Inject - public PrintOptions(Void v) { - } - @Parameter(names = "--color", description = "Use colors in output. Default is on.", descriptionKey = "mode", converter=ColorModeConverter.class) private ColorSetting color; diff --git a/kernel/src/main/java/org/kframework/utils/file/JarInfo.java b/kernel/src/main/java/org/kframework/utils/file/JarInfo.java index 5661f04c76e..adc55aebe1c 100644 --- a/kernel/src/main/java/org/kframework/utils/file/JarInfo.java +++ b/kernel/src/main/java/org/kframework/utils/file/JarInfo.java @@ -85,7 +85,7 @@ public void printVersionMessage() { // the release version if we're not (e.g. from a release tarball). String version = mf.getMainAttributes().getValue("Implementation-Git-Describe"); if (version.isEmpty()) { - version = "v" + FileUtils.readFileToString(new File(kBase + "/lib/version")).trim(); + version = "v" + FileUtils.readFileToString(new File(kBase + "/lib/kframework/version")).trim(); } System.out.println("K version: " + version); diff --git a/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java b/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java index 1eedd8619c1..bb1a47f6d2c 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java +++ b/kernel/src/main/java/org/kframework/utils/inject/CommonModule.java @@ -22,6 +22,7 @@ public class CommonModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); SimpleScope requestScope = new SimpleScope(); bindScope(RequestScoped.class, requestScope); DefinitionScope definitionScope = new DefinitionScope(); diff --git a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java index d093fdf0228..9f3f60084de 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java +++ b/kernel/src/main/java/org/kframework/utils/inject/DefinitionLoadingModule.java @@ -27,6 +27,7 @@ public class DefinitionLoadingModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); } @Provides @DefinitionScoped diff --git a/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java b/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java index 5c5f2c87414..495db016164 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java +++ b/kernel/src/main/java/org/kframework/utils/inject/JCommanderModule.java @@ -31,6 +31,7 @@ public class JCommanderModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(String[].class).annotatedWith(Options.class) .toProvider(SimpleScope.seededKeyProvider()).in(RequestScoped.class);; } diff --git a/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java b/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java index f6f0a7eec3c..cdb86466444 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java +++ b/kernel/src/main/java/org/kframework/utils/inject/OuterParsingModule.java @@ -27,7 +27,7 @@ public class OuterParsingModule extends AbstractModule { @Override protected void configure() { - + binder().requireAtInjectOnConstructors(); } @Provides diff --git a/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java b/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java index 2046937054e..14c57e748d1 100644 --- a/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/BackendOptions.java @@ -10,10 +10,6 @@ public class BackendOptions implements Serializable { public BackendOptions() {} - //TODO(dwightguth): remove in Guice 4.0 - @Inject - public BackendOptions(Void v) {} - @Parameter(names="--dry-run", description="Compile program into KORE format but do not run. Only used in Haskell and LLVM backend.") public boolean dryRun = false; } diff --git a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java index 8f9ed1b7b41..a4d1c9c4f8b 100644 --- a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java @@ -8,10 +8,6 @@ public class DefinitionLoadingOptions { public DefinitionLoadingOptions() {} - //TODO(dwightguth): remove in Guice 4.0 - @Inject - public DefinitionLoadingOptions(Void v) {} - @Parameter(names={"--directory", "-d"}, description="[DEPRECATED] Path to the directory in which the kompiled " + "K definition resides. The default is the unique, only directory with the suffix '-kompiled' " + "in the current directory.", descriptionKey = "path", hidden = true) diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java index b1acb132943..9fd7cc13a32 100644 --- a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java +++ b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java @@ -10,12 +10,7 @@ public class SMTOptions implements Serializable { public SMTOptions() {} - //TODO(dwightguth): remove in Guice 4.0 - @Inject - public SMTOptions(Void v) {} - - @Parameter(names="--smt", descriptionKey = "executable", converter=SMTSolverConverter.class, - description="SMT solver to use for checking constraints. is one of [z3|none].", hidden = true) + @Parameter(names="--smt", converter=SMTSolverConverter.class, description="SMT solver to use for checking constraints. is one of [z3|none].", descriptionKey = "executable", hidden = true) public SMTSolver smt = SMTSolver.Z3; public static class SMTSolverConverter extends BaseEnumConverter { diff --git a/kernel/src/test/java/org/kframework/utils/BaseTestCase.java b/kernel/src/test/java/org/kframework/utils/BaseTestCase.java index 17212387f6a..4ccafc4829a 100644 --- a/kernel/src/test/java/org/kframework/utils/BaseTestCase.java +++ b/kernel/src/test/java/org/kframework/utils/BaseTestCase.java @@ -71,6 +71,7 @@ public class DefinitionSpecificTestModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(KompileOptions.class).toInstance(context.kompileOptions); bind(Definition.class).toInstance(definition); bind(File.class).annotatedWith(KompiledDir.class).toInstance(kompiledDir); @@ -88,6 +89,7 @@ public class TestModule extends AbstractModule { @Override protected void configure() { + binder().requireAtInjectOnConstructors(); bind(RunProcess.class).toInstance(rp); bind(KastOptions.class).toInstance(new KastOptions()); } diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index f882997bd1e..d3c3685d33f 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -414,6 +414,11 @@ object Att { val attMap = union.groupBy({ case ((name, _), _) => name}) Att(union.filter { key => attMap(key._1._1).size == 1 }.toMap) } + + implicit val ord: Ordering[Att] = { + import scala.math.Ordering.Implicits._ + Ordering.by[Att, Seq[(String, String, String)]](att => att.att.iterator.map(k => (k._1._1.key, k._1._2, k._2.toString)).toSeq.sorted) + } } trait AttributesToString { diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index 127bb54694c..6931bc8914b 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -414,18 +414,66 @@ trait Sentence extends HasLocation with HasAtt with AttValue { def label: Optional[String] = att.getOptional(Att.LABEL) } +object Sentence { + implicit val ord = new Ordering[Sentence] { + def compare(a: Sentence, b: Sentence): Int = { + (a, b) match { + case (c:SyntaxSort, d:SyntaxSort) => Ordering[SyntaxSort].compare(c, d) + case (c:SortSynonym, d:SortSynonym) => Ordering[SortSynonym].compare(c, d) + case (c:SyntaxLexical, d:SyntaxLexical) => Ordering[SyntaxLexical].compare(c, d) + case (c:Production, d:Production) => Ordering[Production].compare(c, d) + case (c:SyntaxAssociativity, d:SyntaxAssociativity) => Ordering[SyntaxAssociativity].compare(c, d) + case (c:SyntaxPriority, d:SyntaxPriority) => Ordering[SyntaxPriority].compare(c, d) + case (c:ContextAlias, d:ContextAlias) => Ordering[ContextAlias].compare(c, d) + case (c:Context, d:Context) => Ordering[Context].compare(c, d) + case (c:Rule, d:Rule) => Ordering[Rule].compare(c, d) + case (c:Claim, d:Claim) => Ordering[Claim].compare(c, d) + case (_:SyntaxSort, _) => -1 + case (_, _:SyntaxSort) => 1 + case (_:SortSynonym, _) => -1 + case (_, _:SortSynonym) => 1 + case (_:SyntaxLexical, _) => -1 + case (_, _:SyntaxLexical) => 1 + case (_:Production, _) => -1 + case (_, _:Production) => 1 + case (_:SyntaxAssociativity, _) => -1 + case (_, _:SyntaxAssociativity) => 1 + case (_:SyntaxPriority, _) => -1 + case (_, _:SyntaxPriority) => 1 + case (_:ContextAlias, _) => -1 + case (_, _:ContextAlias) => 1 + case (_:Context, _) => -1 + case (_, _:Context) => 1 + case (_:Rule, _) => -1 + case (_, _:Rule) => 1 + case (_:Claim, _) => -1 + case (_, _:Claim) => 1 + case (_, _) => throw KEMException.internalError("Cannot order these sentences:\n" + a.toString() + "\n" + b.toString()) + } + } + } +} + // deprecated case class Context(body: K, requires: K, att: Att = Att.empty) extends Sentence with OuterKORE with ContextToString { override val isSyntax = false override val isNonSyntax = true override def withAtt(att: Att) = Context(body, requires, att) } +object Context { + implicit val ord: Ordering[Context] = Ordering.by[Context, (K, K, Att)](s => (s.body, s.requires, s.att)) +} case class ContextAlias(body: K, requires: K, att: Att = Att.empty) extends Sentence with OuterKORE with ContextAliasToString { override val isSyntax = true override val isNonSyntax = false override def withAtt(att: Att) = ContextAlias(body, requires, att) } +object ContextAlias { + implicit val ord: Ordering[ContextAlias] = { + Ordering.by[ContextAlias, (K, K, Att)](s => (s.body, s.requires, s.att)) + } +} abstract class RuleOrClaim extends Sentence { def body: K @@ -441,6 +489,11 @@ case class Claim(body: K, requires: K, ensures: K, att: Att = Att.empty) extends override def newInstance(body: K, requires: K, ensures: K, att: Att = Att.empty): Claim = Claim(body, requires, ensures, att) } +object Claim { + implicit val ord: Ordering[Claim] = { + Ordering.by[Claim, (K, K, K, Att)](s => (s.body, s.requires, s.ensures, s.att)) + } +} case class Rule(body: K, requires: K, ensures: K, att: Att = Att.empty) extends RuleOrClaim with RuleToString with OuterKORE { override def withAtt(att: Att): Rule = Rule(body, requires, ensures, att) @@ -449,18 +502,8 @@ case class Rule(body: K, requires: K, ensures: K, att: Att = Att.empty) extends } object Rule { - implicit val ord: Ordering[Rule] = new Ordering[Rule] { - def compare(a: Rule, b: Rule): Int = { - val c1 = Ordering[K].compare(a.body, b.body) - if (c1 == 0) { - val c2 = Ordering[K].compare(a.requires, b.requires) - if (c2 == 0) { - Ordering[K].compare(a.ensures, b.ensures) - } - c2 - } - c1 - } + implicit val ord: Ordering[Rule] = { + Ordering.by[Rule, (K, K, K, Att)](r => (r.body, r.requires, r.ensures, r.att)) } } @@ -474,6 +517,12 @@ case class SyntaxPriority(priorities: Seq[Set[Tag]], att: Att = Att.empty) override val isNonSyntax = false override def withAtt(att: Att) = SyntaxPriority(priorities, att) } +object SyntaxPriority { + implicit val ord: Ordering[SyntaxPriority] = { + import scala.math.Ordering.Implicits._ + Ordering.by[SyntaxPriority, (Seq[Seq[Tag]], Att)](s => (s.priorities.map(_.toSeq.sorted), s.att)) + } +} case class SyntaxAssociativity( assoc: Associativity, @@ -484,9 +533,19 @@ case class SyntaxAssociativity( override val isNonSyntax = false override def withAtt(att: Att) = SyntaxAssociativity(assoc, tags, att) } +object SyntaxAssociativity { + implicit val ord: Ordering[SyntaxAssociativity] = { + import scala.math.Ordering.Implicits._ + Ordering.by[SyntaxAssociativity, (Associativity, Seq[Tag], Att)](s => (s.assoc, s.tags.toSeq.sorted, s.att)) + } +} case class Tag(name: String) extends TagToString with OuterKORE +object Tag { + implicit val ord: Ordering[Tag] = Ordering.by[Tag, String](_.name) +} + //trait Production { // def sort: Sort // def att: Att @@ -503,6 +562,13 @@ case class SyntaxSort(params: Seq[Sort], sort: Sort, att: Att = Att.empty) exten override val isNonSyntax = false override def withAtt(att: Att) = SyntaxSort(params, sort, att) } +object SyntaxSort { + implicit val ord: Ordering[SyntaxSort] = { + import scala.math.Ordering.Implicits._ + Ordering.by[SyntaxSort, (Seq[String], String, Att)](s => (s.params.map(_.name), s.sort.name, s.att)) + } +} + case class SortSynonym(newSort: Sort, oldSort: Sort, att: Att = Att.empty) extends Sentence with SortSynonymToString with OuterKORE { @@ -510,6 +576,12 @@ case class SortSynonym(newSort: Sort, oldSort: Sort, att: Att = Att.empty) exten override val isNonSyntax = false override def withAtt(att: Att) = SortSynonym(newSort, oldSort, att) } +object SortSynonym { + implicit val ord: Ordering[SortSynonym] = { + Ordering.by[SortSynonym, (String, String, Att)](s => (s.newSort.name, s.oldSort.name, s.att)) + } +} + case class SyntaxLexical(name: String, regex: String, att: Att = Att.empty) extends Sentence with SyntaxLexicalToString with OuterKORE { @@ -517,6 +589,11 @@ case class SyntaxLexical(name: String, regex: String, att: Att = Att.empty) exte override val isNonSyntax = false override def withAtt(att: Att) = SyntaxLexical(name, regex, att) } +object SyntaxLexical { + implicit val ord: Ordering[SyntaxLexical] = { + Ordering.by[SyntaxLexical, (String, String, Att)](s => (s.name, s.regex, s.att)) + } +} case class Production(klabel: Option[KLabel], params: Seq[Sort], sort: Sort, items: Seq[ProductionItem], att: Att) extends Sentence with ProductionToString { @@ -638,10 +715,8 @@ case class Production(klabel: Option[KLabel], params: Seq[Sort], sort: Sort, ite } object Production { - implicit val ord: Ordering[Production] = new Ordering[Production] { - def compare(a: Production, b: Production): Int = { - Ordering[Option[String]].compare(a.klabel.map(_.name), b.klabel.map(_.name)) - } + implicit val ord: Ordering[Production] = { + Ordering.by[Production, (Option[String], Att)](s => (s.klabel.map(_.name), s.att)) } def apply(klabel: KLabel, params: Seq[Sort], sort: Sort, items: Seq[ProductionItem], att: Att = Att.empty): Production = { diff --git a/kore/src/main/scala/org/kframework/parser/kore/Default.scala b/kore/src/main/scala/org/kframework/parser/kore/Default.scala index e36953b0dbc..c7c2b2b9e47 100644 --- a/kore/src/main/scala/org/kframework/parser/kore/Default.scala +++ b/kore/src/main/scala/org/kframework/parser/kore/Default.scala @@ -39,9 +39,9 @@ object implementation { case class Bottom(s: i.Sort) extends i.Bottom - case class And(s: i.Sort, _1: i.Pattern, _2: i.Pattern) extends i.And + case class And(s: i.Sort, args: Seq[i.Pattern]) extends i.And - case class Or(s: i.Sort, _1: i.Pattern, _2: i.Pattern) extends i.Or + case class Or(s: i.Sort, args: Seq[i.Pattern]) extends i.Or case class Not(s: i.Sort, _1: i.Pattern) extends i.Not @@ -127,9 +127,25 @@ object implementation { def Bottom(s: i.Sort): i.Pattern = d.Bottom(s) - def And(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.And(s, _1, _2) + def And(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.And(s, Seq(_1, _2)) - def Or(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.Or(s, _1, _2) + def And(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = { + args.size match { + case 0 => Top(s) + case 1 => args(0) + case _ => d.And(s, args) + } + } + + def Or(s: i.Sort, _1: i.Pattern, _2: i.Pattern): i.Pattern = d.Or(s, Seq(_1, _2)) + + def Or(s: i.Sort, args: Seq[i.Pattern]): i.Pattern = { + args.size match { + case 0 => Bottom(s) + case 1 => args(0) + case _ => d.Or(s, args) + } + } def Not(s: i.Sort, _1: i.Pattern): i.Pattern = d.Not(s, _1) diff --git a/kore/src/main/scala/org/kframework/parser/kore/Interface.scala b/kore/src/main/scala/org/kframework/parser/kore/Interface.scala index 39161f2a08e..ba7f6d0221c 100644 --- a/kore/src/main/scala/org/kframework/parser/kore/Interface.scala +++ b/kore/src/main/scala/org/kframework/parser/kore/Interface.scala @@ -164,25 +164,21 @@ object Bottom { trait And extends Pattern { def s: Sort - def _1: Pattern - - def _2: Pattern + def args: Seq[Pattern] } object And { - def unapply(arg: And): Option[(Sort, Pattern, Pattern)] = Some(arg.s, arg._1, arg._2) + def unapply(arg: And): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args) } trait Or extends Pattern { def s: Sort - def _1: Pattern - - def _2: Pattern + def args: Seq[Pattern] } object Or { - def unapply(arg: Or): Option[(Sort, Pattern, Pattern)] = Some(arg.s, arg._1, arg._2) + def unapply(arg: Or): Option[(Sort, Seq[Pattern])] = Some(arg.s, arg.args) } trait Not extends Pattern { @@ -511,8 +507,12 @@ trait Builders { def And(s: Sort, _1: Pattern, _2: Pattern): Pattern + def And(s: Sort, args: Seq[Pattern]): Pattern + def Or(s: Sort, _1: Pattern, _2: Pattern): Pattern + def Or(s: Sort, args: Seq[Pattern]): Pattern + def Not(s: Sort, _1: Pattern): Pattern def Implies(s: Sort, _1: Pattern, _2: Pattern): Pattern diff --git a/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala b/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala index ec1f8b0c51d..539cf201420 100644 --- a/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala +++ b/kore/src/main/scala/org/kframework/parser/kore/parser/KoreToK.scala @@ -2,6 +2,7 @@ package org.kframework.parser.kore.parser import org.kframework.builtin.{KLabels, Sorts} +import org.kframework.kore.Assoc import org.kframework.kore.KVariable import org.kframework.kore.KORE import org.kframework.attributes.Att @@ -133,10 +134,12 @@ class KoreToK (sortAtt : Map[String, String]) { KORE.KApply(KORE.KLabel(KLabels.ML_TRUE.name, apply(s))) case kore.Bottom(s) => KORE.KApply(KORE.KLabel(KLabels.ML_FALSE.name, apply(s))) - case kore.And(s, p, q) => - KORE.KApply(KORE.KLabel(KLabels.ML_AND.name, apply(s)), apply(p), apply(q)) - case kore.Or(s, p, q) => - KORE.KApply(KORE.KLabel(KLabels.ML_OR.name, apply(s)), apply(p), apply(q)) + case kore.And(s, items) => + val and = KORE.KLabel(KLabels.ML_AND.name, apply(s)) + KORE.KApply(and, Assoc.flatten(and, items.map(apply), KORE.KLabel(KLabels.ML_TRUE.name, apply(s)))) + case kore.Or(s, items) => + val or = KORE.KLabel(KLabels.ML_OR.name, apply(s)) + KORE.KApply(or, Assoc.flatten(or, items.map(apply), KORE.KLabel(KLabels.ML_FALSE.name, apply(s)))) case kore.Not(s, p) => KORE.KApply(KORE.KLabel(KLabels.ML_NOT.name, apply(s)), apply(p)) case kore.Implies(s, p, q) => diff --git a/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala b/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala index 0dc7637b627..6aebc0de4ac 100644 --- a/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala +++ b/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala @@ -379,21 +379,17 @@ class TextToKore(b: Builders = DefaultBuilders) { val s = parseSort() consumeWithLeadingWhitespaces("}") consumeWithLeadingWhitespaces("(") - val p1 = parsePattern() - consumeWithLeadingWhitespaces(",") - val p2 = parsePattern() + val args = parseList(() => parsePattern(), ',', ')') consumeWithLeadingWhitespaces(")") - b.And(s, p1, p2) + b.And(s, args) case ('o', 'r') => // or consumeWithLeadingWhitespaces("{") val s = parseSort() consumeWithLeadingWhitespaces("}") consumeWithLeadingWhitespaces("(") - val p1 = parsePattern() - consumeWithLeadingWhitespaces(",") - val p2 = parsePattern() + val args = parseList(() => parsePattern(), ',', ')') consumeWithLeadingWhitespaces(")") - b.Or(s, p1, p2) + b.Or(s, args) case ('n', 'o') => // not consume("t") consumeWithLeadingWhitespaces("{") @@ -528,22 +524,6 @@ class TextToKore(b: Builders = DefaultBuilders) { consumeWithLeadingWhitespaces("}") consumeWithLeadingWhitespaces("(") val ctr = scanner.nextWithSkippingWhitespaces() match { - case '\\' => - val c1 = scanner.next() - val c2 = scanner.next() - (c1, c2) match { - case ('a', 'n') => // and - consume("d") - consumeWithLeadingWhitespaces("{") - val s = parseSort() - consumeWithLeadingWhitespaces("}") - (p1: kore.Pattern, p2: kore.Pattern) => b.And(s, p1, p2) - case ('o', 'r') => // or - consumeWithLeadingWhitespaces("{") - val s = parseSort() - consumeWithLeadingWhitespaces("}") - (p1: kore.Pattern, p2: kore.Pattern) => b.Or(s, p1, p2) - } case c => // variable or application scanner.putback(c) val id = parseId() // previousParsingLevel is set here @@ -563,22 +543,6 @@ class TextToKore(b: Builders = DefaultBuilders) { consumeWithLeadingWhitespaces("}") consumeWithLeadingWhitespaces("(") val ctr = scanner.nextWithSkippingWhitespaces() match { - case '\\' => - val c1 = scanner.next() - val c2 = scanner.next() - (c1, c2) match { - case ('a', 'n') => // and - consume("d") - consumeWithLeadingWhitespaces("{") - val s = parseSort() - consumeWithLeadingWhitespaces("}") - (p1: kore.Pattern, p2: kore.Pattern) => b.And(s, p1, p2) - case ('o', 'r') => // or - consumeWithLeadingWhitespaces("{") - val s = parseSort() - consumeWithLeadingWhitespaces("}") - (p1: kore.Pattern, p2: kore.Pattern) => b.Or(s, p1, p2) - } case c => // variable or application scanner.putback(c) val id = parseId() // previousParsingLevel is set here diff --git a/kore/src/test/scala/org/kframework/definition/OuterTest.scala b/kore/src/test/scala/org/kframework/definition/OuterTest.scala index c42cb6fa5d8..54e9beb0399 100644 --- a/kore/src/test/scala/org/kframework/definition/OuterTest.scala +++ b/kore/src/test/scala/org/kframework/definition/OuterTest.scala @@ -4,6 +4,7 @@ package org.kframework.definition import org.junit.{Assert, Test} import org.kframework.attributes.Att +import org.kframework.kore.ADT.KToken import org.kframework.kore.KORE.Sort import org.kframework.kore.KORE.KLabel @@ -90,4 +91,153 @@ class OuterTest { val prod2 = Production(Some(KLabel("foo")), Seq(), Sort("Foo"), Seq(), Att.empty.add(Att.KLABEL, "bar")) Assert.assertNotEquals(prod1, prod2) } + + // Create multiple versions of this sentence with attributes added + def toSentenceAttList(sentence: Sentence): List[Sentence] = { + val att1 = Att.empty.add(Att.ASSOC).add(Att.BAG) + val att2 = Att.empty.add(Att.ASSOC).add(Att.CELL) + val att3 = Att.empty.add(Att.BAG).add(Att.CELL) + val att4 = Att.empty.add(Att.BAG).add(Att.HOOK, "A") + val att5 = Att.empty.add(Att.BAG).add(Att.HOOK, "B") + val att6 = Att.empty.add(Att.BAG).add(Att.LABEL, "A") + val att7 = Att.empty.add(Att.BAG).add(Att.LABEL, "B") + val att8 = Att.empty.add(Att.HOOK, "A").add(Att.LABEL, "B") + val att9 = Att.empty.add(Att.HOOK, "B").add(Att.LABEL, "A") + val sentenceWithAtt1 = sentence.withAtt(att1) + val sentenceWithAtt2 = sentence.withAtt(att2) + val sentenceWithAtt3 = sentence.withAtt(att3) + val sentenceWithAtt4 = sentence.withAtt(att4) + val sentenceWithAtt5 = sentence.withAtt(att5) + val sentenceWithAtt6 = sentence.withAtt(att6) + val sentenceWithAtt7 = sentence.withAtt(att7) + val sentenceWithAtt8 = sentence.withAtt(att8) + val sentenceWithAtt9 = sentence.withAtt(att9) + + List(sentenceWithAtt1, + sentenceWithAtt2, + sentenceWithAtt3, + sentenceWithAtt4, + sentenceWithAtt5, + sentenceWithAtt6, + sentenceWithAtt7, + sentenceWithAtt8, + sentenceWithAtt9) + } + + // Asserts that S1 < S2 < ... < Sn + // Likewise, Sn > ... > S2 > S1 + // And Sx = Sx + def checkOrdering(sentences: List[Sentence]): Unit = { + val ord = Ordering[Sentence] + for (remaining <- sentences.tails.filter(_.nonEmpty)) { + val head = remaining.head + Assert.assertTrue(ord.compare(head, head) == 0) + for (sentence <- remaining.tail) { + Assert.assertTrue(ord.compare(head, sentence) < 0) + Assert.assertTrue(ord.compare(sentence, head) > 0) + } + } + } + + @Test def sentenceOrdering(): Unit = { + val sortA = Sort("A") + val sortB = Sort("B") + val sortC = Sort("C") + + val ktokenA = KToken("A", sortA) + val ktokenB = KToken("B", sortA) + val ktokenC = KToken("C", sortA) + + val tagA = Tag("A") + val tagB = Tag("B") + val tagC = Tag("C") + + val syntaxSort1 = SyntaxSort(Seq(sortA, sortC), sortA) + val syntaxSort2 = SyntaxSort(Seq(sortA, sortC), sortB) + val syntaxSort3 = SyntaxSort(Seq(sortB, sortC), sortA) + + val synonym1 = SortSynonym(sortA, sortA) + val synonym2 = SortSynonym(sortA, sortB) + val synonym3 = SortSynonym(sortB, sortC) + + val lexical1 = SyntaxLexical("A", "A") + val lexical2 = SyntaxLexical("A", "B") + val lexical3 = SyntaxLexical("B", "A") + + val production1 = Production(Seq(), sortA, Seq(), Att.empty) + val production2 = Production(KLabel("A"), Seq(), sortA, Seq(), Att.empty) + val production3 = Production(KLabel("B"), Seq(), sortA, Seq(), Att.empty) + + val syntaxAssoc1 = SyntaxAssociativity(Associativity.Left, Set(tagA)) + val syntaxAssoc2 = SyntaxAssociativity(Associativity.Left, Set(tagB)) + val syntaxAssoc3 = SyntaxAssociativity(Associativity.Right, Set(tagA)) + + val syntaxPriority1 = SyntaxPriority(Seq(Set(tagB, tagA))) + val syntaxPriority2 = SyntaxPriority(Seq(Set(tagA, tagB, tagC), Set(tagB))) + val syntaxPriority3 = SyntaxPriority(Seq(Set(tagA, tagB, tagC), Set(tagC))) + val syntaxPriority4 = SyntaxPriority(Seq(Set(tagA, tagC, tagC), Set(tagB))) + val syntaxPriority5 = SyntaxPriority(Seq(Set(tagB))) + + val contextAlias1 = ContextAlias(ktokenA, ktokenA) + val contextAlias2 = ContextAlias(ktokenA, ktokenB) + val contextAlias3 = ContextAlias(ktokenB, ktokenB) + + val context1 = Context(ktokenA, ktokenA) + val context2 = Context(ktokenA, ktokenB) + val context3 = Context(ktokenB, ktokenA) + + val rule1 = Rule(ktokenA, ktokenA, ktokenA) + val rule2 = Rule(ktokenA, ktokenA, ktokenB) + val rule3 = Rule(ktokenA, ktokenA, ktokenC) + val rule4 = Rule(ktokenA, ktokenB, ktokenA) + val rule5 = Rule(ktokenB, ktokenA, ktokenA) + + val claim1 = Claim(ktokenA, ktokenA, ktokenA) + val claim2 = Claim(ktokenA, ktokenA, ktokenB) + val claim3 = Claim(ktokenA, ktokenA, ktokenC) + val claim4 = Claim(ktokenA, ktokenB, ktokenA) + val claim5 = Claim(ktokenB, ktokenA, ktokenA) + + val sentenceList = List( + syntaxSort1, + syntaxSort2, + syntaxSort3, + synonym1, + synonym2, + synonym3, + lexical1, + lexical2, + lexical3, + production1, + production2, + production3, + syntaxAssoc1, + syntaxAssoc2, + syntaxAssoc3, + syntaxPriority1, + syntaxPriority2, + syntaxPriority3, + syntaxPriority4, + syntaxPriority5, + contextAlias1, + contextAlias2, + contextAlias3, + context1, + context2, + context3, + rule1, + rule2, + rule3, + rule4, + rule5, + claim1, + claim2, + claim3, + claim4, + claim5) + + val sentenceListWithAtts = sentenceList.flatMap(toSentenceAttList(_)) + + checkOrdering(sentenceListWithAtts) + } } diff --git a/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala b/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala index 4cee235b858..48eebe0788a 100644 --- a/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala +++ b/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala @@ -8,27 +8,19 @@ import org.kframework.parser.kore.implementation.{DefaultBuilders => b} class TextToKoreTest { @Test def testMultiOr(): Unit = { - val kore1 = "\\left-assoc{}(\\or{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\")))" + val kore1 = "\\or{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\"))" val parser = new TextToKore() val ast1 = parser.parsePattern(kore1) val int = b.CompoundSort("SortInt", Seq()) - Assert.assertEquals(b.Or(int, b.Or(int, b.DomainValue(int, "1"), b.DomainValue(int, "2")), b.DomainValue(int, "3")), ast1) - - val kore2 = "\\right-assoc{}(\\or{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\")))" - val ast2 = parser.parsePattern(kore2) - Assert.assertEquals(b.Or(int, b.DomainValue(int, "1"), b.Or(int, b.DomainValue(int, "2"), b.DomainValue(int, "3"))), ast2) + Assert.assertEquals(b.Or(int, Seq(b.DomainValue(int, "1"), b.DomainValue(int, "2"), b.DomainValue(int, "3"))), ast1) } @Test def testMultiAnd(): Unit = { - val kore1 = "\\left-assoc{}(\\and{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\")))" + val kore1 = "\\and{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\"))" val parser = new TextToKore() val ast1 = parser.parsePattern(kore1) val int = b.CompoundSort("SortInt", Seq()) - Assert.assertEquals(b.And(int, b.And(int, b.DomainValue(int, "1"), b.DomainValue(int, "2")), b.DomainValue(int, "3")), ast1) - - val kore2 = "\\right-assoc{}(\\and{SortInt{}}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"2\"), \\dv{SortInt{}}(\"3\")))" - val ast2 = parser.parsePattern(kore2) - Assert.assertEquals(b.And(int, b.DomainValue(int, "1"), b.And(int, b.DomainValue(int, "2"), b.DomainValue(int, "3"))), ast2) + Assert.assertEquals(b.And(int, Seq(b.DomainValue(int, "1"), b.DomainValue(int, "2"), b.DomainValue(int, "3"))), ast1) } @Test def testAssocApplication(): Unit = { diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java index e81ce93f110..bb757de59a8 100644 --- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java +++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java @@ -3,6 +3,7 @@ import com.beust.jcommander.Parameter; import com.beust.jcommander.IStringConverter; +import com.google.inject.Inject; import org.kframework.utils.inject.RequestScoped; import java.util.Arrays; @@ -12,6 +13,9 @@ @RequestScoped public class LLVMKompileOptions { + @Inject + public LLVMKompileOptions() {} + @Parameter(names="--enable-llvm-debug", description="Enable debugging support for the LLVM backend.") public boolean debug = false; diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index 4c9d0101951..a859fb6d77a 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit 4c9d0101951dc7fa4f07b0b03f5afd84331a40f7 +Subproject commit a859fb6d77a48220d9d8b9314371933e8204c1d3 diff --git a/nix/mavenix.lock b/nix/mavenix.lock index 7be2b7a378a..541407e5860 100644 --- a/nix/mavenix.lock +++ b/nix/mavenix.lock @@ -282,52 +282,52 @@ "sha1": "1b77ba79f9b2b7dfd4e15ea7bb0d568d5eb9cb8d" }, { - "path": "com/google/inject/extensions/extensions-parent/4.0-beta5/extensions-parent-4.0-beta5.pom", - "sha1": "516d8e5e771cd573364dc6ff53c2c6c13908a713" + "path": "com/google/inject/extensions/extensions-parent/4.0/extensions-parent-4.0.pom", + "sha1": "db8e45ab989a2347421ff0d32be5446528d6f63f" }, { - "path": "com/google/inject/extensions/guice-assistedinject/4.0-beta5/guice-assistedinject-4.0-beta5.jar", - "sha1": "820f10e0650cd9ed2591f398937df50f330b147d" + "path": "com/google/inject/extensions/guice-assistedinject/4.0/guice-assistedinject-4.0.jar", + "sha1": "8fa6431da1a2187817e3e52e967535899e2e46ca" }, { - "path": "com/google/inject/extensions/guice-assistedinject/4.0-beta5/guice-assistedinject-4.0-beta5.pom", - "sha1": "4b9b352e0537b0ca49cb97533387864b185df09b" + "path": "com/google/inject/extensions/guice-assistedinject/4.0/guice-assistedinject-4.0.pom", + "sha1": "00c7fc29684b20dd475f517d5dafc850c613efde" }, { - "path": "com/google/inject/extensions/guice-grapher/4.0-beta5/guice-grapher-4.0-beta5.jar", - "sha1": "dd9a00d72fecfa05a77bf28c7922eacddda23b18" + "path": "com/google/inject/extensions/guice-grapher/4.0/guice-grapher-4.0.jar", + "sha1": "4e611ae9b12bfc4ddd430a58c65ba1c4328eeaf9" }, { - "path": "com/google/inject/extensions/guice-grapher/4.0-beta5/guice-grapher-4.0-beta5.pom", - "sha1": "1cd692901e55d382cdb9e647d74617bb68d63126" + "path": "com/google/inject/extensions/guice-grapher/4.0/guice-grapher-4.0.pom", + "sha1": "86b9c4937ebba7d14054d0f025f0df51d071218d" }, { - "path": "com/google/inject/extensions/guice-multibindings/4.0-beta5/guice-multibindings-4.0-beta5.jar", - "sha1": "f432356db0a167127ffe4a7921238d7205b12682" + "path": "com/google/inject/extensions/guice-multibindings/4.0/guice-multibindings-4.0.jar", + "sha1": "f4509545b4470bbcc865aa500ad6fef2e97d28bf" }, { - "path": "com/google/inject/extensions/guice-multibindings/4.0-beta5/guice-multibindings-4.0-beta5.pom", - "sha1": "3cff7b7b5f418f5edca0fa1b0d4bcd3f3215d9c7" + "path": "com/google/inject/extensions/guice-multibindings/4.0/guice-multibindings-4.0.pom", + "sha1": "2387a1e5163308cd826b348db825973df0800ad3" }, { - "path": "com/google/inject/extensions/guice-throwingproviders/4.0-beta5/guice-throwingproviders-4.0-beta5.jar", - "sha1": "8840bd8267a5b09ee84a314a54dbdc6c1b0a7efb" + "path": "com/google/inject/extensions/guice-throwingproviders/4.0/guice-throwingproviders-4.0.jar", + "sha1": "90876169e80b4db9b61d654367c4c55079ae4e91" }, { - "path": "com/google/inject/extensions/guice-throwingproviders/4.0-beta5/guice-throwingproviders-4.0-beta5.pom", - "sha1": "cb52affb5a89e66a5f1d9ab3a7fde7dda1cc5baa" + "path": "com/google/inject/extensions/guice-throwingproviders/4.0/guice-throwingproviders-4.0.pom", + "sha1": "5118433baea2efed034af00a96e324b5717e8059" }, { - "path": "com/google/inject/guice-parent/4.0-beta5/guice-parent-4.0-beta5.pom", - "sha1": "13d7df2b77236548d1e7cb9ba688686ddd4f19a5" + "path": "com/google/inject/guice-parent/4.0/guice-parent-4.0.pom", + "sha1": "a59ca1d3d70552158088d7f71e6c7e8779b9a8a1" }, { - "path": "com/google/inject/guice/4.0-beta5/guice-4.0-beta5-no_aop.jar", - "sha1": "7706f581d709b1afd89b4e0dbf1bebf250abbd9b" + "path": "com/google/inject/guice/4.0/guice-4.0-no_aop.jar", + "sha1": "199b7acaa05b570bbccf31be998f013963e5e752" }, { - "path": "com/google/inject/guice/4.0-beta5/guice-4.0-beta5.pom", - "sha1": "1e968b8c1da8cb48b7c0b77ffc565f92f313c392" + "path": "com/google/inject/guice/4.0/guice-4.0.pom", + "sha1": "688cb7b0d86456e3706573fe583173ee5e728f4e" }, { "path": "com/google/j2objc/j2objc-annotations/1.3/j2objc-annotations-1.3.jar", diff --git a/package/arch/Dockerfile b/package/arch/Dockerfile index 1dfbce7dd9c..9cd5c8568b6 100644 --- a/package/arch/Dockerfile +++ b/package/arch/Dockerfile @@ -27,6 +27,7 @@ RUN pacman -Sy --noconfirm archlinux-keyring \ hub \ jdk-openjdk \ jemalloc \ + libsecp256k1 \ libyaml \ lld \ llvm \ diff --git a/package/arch/Dockerfile.stack-deps b/package/arch/Dockerfile.stack-deps index 42d333b5952..2c4c3954a4c 100644 --- a/package/arch/Dockerfile.stack-deps +++ b/package/arch/Dockerfile.stack-deps @@ -6,7 +6,9 @@ RUN pacman -Sy --noconfirm archlinux-keyring \ && pacman -Syyu --noconfirm \ && pacman -S --noconfirm \ clang \ + libsecp256k1 \ make \ + pkgconf \ stack # The image is built specifically for an environment with this user/group diff --git a/package/arch/PKGBUILD b/package/arch/PKGBUILD index 562d5f62cc4..12ee1d809ff 100644 --- a/package/arch/PKGBUILD +++ b/package/arch/PKGBUILD @@ -1,6 +1,6 @@ # Maintainer: Dwight Guth pkgname=kframework-git -pkgver=6.0.0 +pkgver=6.0.145 pkgrel=1 epoch= pkgdesc="K framework toolchain. Includes K Framework compiler for K language definitions, and K interpreter and prover for programs written in languages defined in K." @@ -8,8 +8,8 @@ arch=('x86_64') url="https://github.com/runtimeverification/k" license=('custom') groups=() -depends=( 'bison' 'clang' 'diffutils' 'flex' 'fmt' 'gawk' 'gcc' 'gettext' 'gmp' 'grep' 'java-runtime' 'jemalloc' 'libyaml' 'lld' 'llvm' 'make' 'mpfr' 'patch' 'python' 'tar' 'z3' ) -makedepends=( 'boost' 'cmake' 'jdk-openjdk' 'maven' 'python' 'zlib' ) +depends=( 'bison' 'boost' 'clang' 'diffutils' 'flex' 'fmt' 'gawk' 'gcc' 'gettext' 'gmp' 'grep' 'java-runtime' 'jemalloc' 'libsecp256k1' 'libyaml' 'lld' 'llvm' 'make' 'mpfr' 'patch' 'python' 'tar' 'z3' ) +makedepends=( 'cmake' 'jdk-openjdk' 'maven' 'python' 'zlib' ) checkdepends=() optdepends=() provides=() diff --git a/package/debian/Dockerfile b/package/debian/Dockerfile deleted file mode 100644 index 82329034e37..00000000000 --- a/package/debian/Dockerfile +++ /dev/null @@ -1,83 +0,0 @@ -ARG BASE_IMAGE=ubuntu:focal -FROM ${BASE_IMAGE} -ARG BASE_IMAGE - -ARG LLVM_VERSION=10 - -ENV TZ America/Chicago -ENV DEBIAN_FRONTEND=noninteractive - -RUN apt-get update \ - && apt-get install --yes \ - bison \ - build-essential \ - clang-$LLVM_VERSION \ - cmake \ - curl \ - debhelper \ - flex \ - gcc \ - g++ \ - git \ - libboost-dev \ - libboost-test-dev \ - libgdbm-dev \ - libgmp-dev \ - libjemalloc-dev \ - libffi-dev \ - libfmt-dev \ - libmpfr-dev \ - libncurses5-dev \ - libnss3-dev \ - libreadline-dev \ - libsqlite3-dev \ - libssl-dev \ - libyaml-dev \ - libbz2-dev \ - libz3-dev \ - lld-$LLVM_VERSION \ - llvm-$LLVM_VERSION-tools \ - maven \ - openjdk-17-jdk \ - parallel \ - pkg-config \ - python3 \ - python3-dev \ - python3-distutils \ - python3-pip \ - zlib1g-dev - -RUN curl -sSL https://get.haskellstack.org/ | sh - -RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.15 \ - && cd z3 \ - && python3 scripts/mk_make.py \ - && cd build \ - && make -j8 \ - && make install \ - && cd ../.. \ - && rm -rf z3 - -ARG USER_ID=1000 -ARG GROUP_ID=1000 -RUN groupadd -g $GROUP_ID user \ - && useradd -m -u $USER_ID -s /bin/sh -g user user - -USER $USER_ID:$GROUP_ID - -ENV LC_ALL=C.UTF-8 -ADD --chown=user:user haskell-backend/src/main/native/haskell-backend/stack.yaml /home/user/.tmp-haskell/ -ADD --chown=user:user haskell-backend/src/main/native/haskell-backend/kore/kore.cabal /home/user/.tmp-haskell/kore/ -ADD --chown=user:user haskell-backend/src/main/native/haskell-backend/kore-rpc-types/kore-rpc-types.cabal /home/user/.tmp-haskell/kore-rpc-types/ -RUN cd /home/user/.tmp-haskell \ - && stack build --only-snapshot - -ADD pom.xml /home/user/.tmp-maven/ -ADD llvm-backend/pom.xml /home/user/.tmp-maven/llvm-backend/ -ADD llvm-backend/src/main/native/llvm-backend/matching/pom.xml /home/user/.tmp-maven/llvm-backend/src/main/native/llvm-backend/matching/ -ADD haskell-backend/pom.xml /home/user/.tmp-maven/haskell-backend/ -ADD kernel/pom.xml /home/user/.tmp-maven/kernel/ -ADD k-distribution/pom.xml /home/user/.tmp-maven/k-distribution/ -ADD kore/pom.xml /home/user/.tmp-maven/kore/ -RUN cd /home/user/.tmp-maven \ - && mvn --batch-mode dependency:go-offline diff --git a/package/debian/changelog b/package/debian/changelog index 0fa471e68cf..605b0bc1329 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kframework (6.0.0) unstable; urgency=medium +kframework (6.0.145) unstable; urgency=medium * Initial Release. diff --git a/package/debian/compat.focal b/package/debian/compat.focal deleted file mode 100644 index ec635144f60..00000000000 --- a/package/debian/compat.focal +++ /dev/null @@ -1 +0,0 @@ -9 diff --git a/package/debian/control.bookworm b/package/debian/control.bookworm index 7a03ddd4132..dffbfae42c7 100644 --- a/package/debian/control.bookworm +++ b/package/debian/control.bookworm @@ -2,7 +2,7 @@ Source: kframework Section: devel Priority: optional Maintainer: Dwight Guth -Build-Depends: clang-14 , cmake , debhelper (>=9) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-dev , maven , openjdk-17-jdk , zlib1g-dev +Build-Depends: clang-14 , cmake , debhelper (>=9) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , zlib1g-dev Standards-Version: 3.9.6 Homepage: https://github.com/runtimeverification/k @@ -10,7 +10,7 @@ Package: kframework Architecture: any Section: devel Priority: optional -Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-0-2 , libz3-4 , lld-14 , pkg-config , llvm-14 +Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-1 , libyaml-0-2 , libz3-4 , lld-14 , pkg-config , llvm-14 Recommends: z3 Description: K framework toolchain Includes K Framework compiler for K language definitions, and K interpreter diff --git a/package/debian/control.focal b/package/debian/control.focal deleted file mode 100644 index 0d94ac2922f..00000000000 --- a/package/debian/control.focal +++ /dev/null @@ -1,18 +0,0 @@ -Source: kframework -Section: devel -Priority: optional -Maintainer: Dwight Guth -Build-Depends: clang-12 , cmake , debhelper (>=9) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-dev , maven , openjdk-11-jdk , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev -Standards-Version: 3.9.6 -Homepage: https://github.com/runtimeverification/k - -Package: kframework -Architecture: any -Section: devel -Priority: optional -Depends: bison , clang-12 , default-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libtinfo-dev , libyaml-0-2 , libz3-4 , lld-12 , llvm-12 , pkg-config -Recommends: z3 -Description: K framework toolchain - Includes K Framework compiler for K language definitions, and K interpreter - and prover for programs written in languages defined in K. -Homepage: https://github.com/runtimeverification/k diff --git a/package/debian/control.jammy b/package/debian/control.jammy index de8d652e60b..30972fdf9c1 100644 --- a/package/debian/control.jammy +++ b/package/debian/control.jammy @@ -2,7 +2,7 @@ Source: kframework Section: devel Priority: optional Maintainer: Dwight Guth -Build-Depends: clang-14 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev +Build-Depends: clang-14 , cmake , debhelper (>=10) , flex , libboost-test-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-dev , libyaml-dev , maven , openjdk-17-jdk , pkg-config , python3 , python3-dev , python3-distutils , python3-pip , zlib1g-dev Standards-Version: 3.9.6 Homepage: https://github.com/runtimeverification/k @@ -10,7 +10,7 @@ Package: kframework Architecture: any Section: devel Priority: optional -Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libtinfo-dev , libyaml-0-2 , libz3-4 , lld-14 , llvm-14 , pkg-config +Depends: bison , clang-14 , default-jre-headless , flex , gcc , g++ , libboost-dev , libffi-dev , libfmt-dev , libgmp-dev , libjemalloc-dev , libmpfr-dev , libsecp256k1-0 , libtinfo-dev , libyaml-0-2 , libz3-4 , lld-14 , llvm-14 , pkg-config Recommends: z3 Description: K framework toolchain Includes K Framework compiler for K language definitions, and K interpreter diff --git a/package/debian/rules.focal b/package/debian/rules.focal deleted file mode 100755 index 500d34c1e09..00000000000 --- a/package/debian/rules.focal +++ /dev/null @@ -1,39 +0,0 @@ -#!/usr/bin/make -f -# See debhelper(7) (uncomment to enable) -# output every command that modifies files on the build system. -#export DH_VERBOSE = 1 - - -# see FEATURE AREAS in dpkg-buildflags(1) -export DEB_BUILD_MAINT_OPTIONS=hardening=-stackprotector - -# see ENVIRONMENT in dpkg-buildflags(1) -# package maintainers to append CFLAGS -#export DEB_CFLAGS_MAINT_APPEND = -Wall -pedantic -# package maintainers to append LDFLAGS -#export DEB_LDFLAGS_MAINT_APPEND = -Wl,--as-needed - -DESTDIR=$(shell pwd)/debian/kframework -PREFIX=/usr -PYTHON_VERSION=python3.8 -PYTHON_DEB_VERSION=python3 -export DESTDIR -export PREFIX - -%: - dh $@ - -override_dh_auto_build: - mvn --batch-mode package -DskipTests -Dllvm.backend.prefix=$(PREFIX) -Dllvm.backend.destdir=$(DESTDIR) - -override_dh_auto_install: - package/package - -override_dh_strip: - dh_strip -Xliballoc.a -Xlibarithmetic.a -XlibAST.a -Xlibutil.a -XlibParser.a -Xlibcollect.a -Xlibcollections.a -Xlibjson.a -Xlibstrings.a -Xlibmeta.a -Xlibio.a - -# dh_make generated override targets -# This is example for Cmake (See https://bugs.debian.org/641051 ) -#override_dh_auto_configure: -# dh_auto_configure -- # -DCMAKE_LIBRARY_PATH=$(DEB_HOST_MULTIARCH) - diff --git a/package/docker/Dockerfile.ubuntu-focal b/package/docker/Dockerfile.ubuntu-focal deleted file mode 100644 index 58906bc8d21..00000000000 --- a/package/docker/Dockerfile.ubuntu-focal +++ /dev/null @@ -1,28 +0,0 @@ -FROM ubuntu:focal - -ENV TZ=America/Chicago -RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone - -RUN apt-get update \ - && apt-get upgrade --yes \ - && apt-get install --yes \ - build-essential \ - git \ - python3 \ - python3-pip - -RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.15 \ - && cd z3 \ - && python3 scripts/mk_make.py \ - && cd build \ - && make -j8 \ - && make install \ - && cd ../.. \ - && rm -rf z3 - -COPY kframework_amd64_ubuntu_focal.deb /kframework_amd64_ubuntu_focal.deb -RUN apt-get update \ - && apt-get upgrade --yes \ - && apt-get install --yes --no-install-recommends /kframework_amd64_ubuntu_focal.deb - -RUN rm -rf /kframework_amd64_ubuntu_focal.deb diff --git a/package/docker/Dockerfile.ubuntu-jammy b/package/docker/Dockerfile.ubuntu-jammy index c3df771541f..607fcb9a978 100644 --- a/package/docker/Dockerfile.ubuntu-jammy +++ b/package/docker/Dockerfile.ubuntu-jammy @@ -1,4 +1,4 @@ -FROM ubuntu:jammy +FROM runtimeverificationinc/z3:ubuntu-jammy-4.12.1 ENV TZ=America/Chicago RUN ln -snf /usr/share/zoneinfo/$TZ /etc/localtime && echo $TZ > /etc/timezone @@ -11,15 +11,6 @@ RUN apt-get update \ python3 \ python3-pip -RUN git clone 'https://github.com/z3prover/z3' --branch=z3-4.8.15 \ - && cd z3 \ - && python3 scripts/mk_make.py \ - && cd build \ - && make -j8 \ - && make install \ - && cd ../.. \ - && rm -rf z3 - COPY kframework_amd64_ubuntu_jammy.deb /kframework_amd64_ubuntu_jammy.deb RUN apt-get update \ && apt-get upgrade --yes \ diff --git a/package/test-package b/package/test-package index 704750337ac..6c4ae1f0bcb 100755 --- a/package/test-package +++ b/package/test-package @@ -23,5 +23,27 @@ sort_int = kllvm.ast.CompositeSort("SortInt") assert str(sort_int) == "SortInt{}" HERE +# Make sure that the help messages work and that the version of the various components is correct +PACKAGE_VERSION=$(cat /usr/lib/kframework/version) + +kast --help | grep -q -- "--version" +kdep --help | grep -q -- "--version" +kompile --help | grep -q -- "--version" +kprove --help | grep -q -- "--version" +krun --help | grep -q -- "--version" +kserver --help | grep -q -- "--version" +kparse --help | grep -q -- "--version" +kparse-gen --help | grep -q -- "--version" +kore-print --help | grep -q -- "--version" +kast --version | grep -q ${PACKAGE_VERSION} +kdep --version | grep -q ${PACKAGE_VERSION} +kompile --version | grep -q ${PACKAGE_VERSION} +kprove --version | grep -q ${PACKAGE_VERSION} +krun --version | grep -q ${PACKAGE_VERSION} +kserver --version | grep -q ${PACKAGE_VERSION} +kparse --version | grep -q ${PACKAGE_VERSION} +kparse-gen --version | grep -q ${PACKAGE_VERSION} +kore-print --version | grep -q ${PACKAGE_VERSION} + # Make sure that the Haskell Backend Booster has been installed properly. kore-rpc-booster --help diff --git a/package/version b/package/version index 09b254e90c6..dcdec1cb27d 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -6.0.0 +6.0.145 diff --git a/web/toc.md b/web/toc.md index 64f77e088d3..2c458b00ac4 100644 --- a/web/toc.md +++ b/web/toc.md @@ -62,7 +62,7 @@ output: - [K User Manual](/docs/user_manual.md) - [K Cheat Sheet](/docs/cheat_sheet.md) - [K Tool Reference](/docs/ktools.md) -- [K Builtins](/k-distribution/include/kframework/builtin/README.md) +- [K Builtins](/k-distribution/include/kframework/README.md) - [domains](/k-distribution/include/kframework/builtin/domains.md) - [kast](/k-distribution/include/kframework/builtin/kast.md) - [prelude](/k-distribution/include/kframework/builtin/prelude.md)