Set up project

.cruft.json

@@ -0,0 +1,18 @@
+{
+  "template": "https://github.com/runtimeverification/python-project-template",
+  "commit": "601d5e2a0e8a98c87dcb1ae694d22d76d0114e01",
+  "checkout": null,
+  "context": {
+    "cookiecutter": {
+      "project_name": "kriscv",
+      "project_slug": "kriscv",
+      "package_name": "kriscv",
+      "version": "0.1.0",
+      "description": "K tooling for the RISC-V architecture",
+      "author_name": "Runtime Verification, Inc.",
+      "author_email": "[email protected]",
+      "_template": "https://github.com/runtimeverification/python-project-template"
+    }
+  },
+  "directory": null
+}

.flake8

@@ -0,0 +1,7 @@
+[flake8]
+max-line-length = 120
+extend-select = B9, TC1
+extend-ignore = B950,E,W1,W2,W3,W4,W5
+per-file-ignores =
+    */__init__.py: F401
+type-checking-strict = true

.github/actions/with-docker/Dockerfile

@@ -0,0 +1,22 @@
+ARG K_VERSION
+FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
+
+ARG PYTHON_VERSION=3.10
+
+RUN    apt-get -y update             \
+    && apt-get -y install            \
+         graphviz                    \
+         python${PYTHON_VERSION}     \
+         python${PYTHON_VERSION}-dev \
+    && apt-get -y clean
+
+ARG USER_ID=9876
+ARG GROUP_ID=9876
+RUN    groupadd -g ${GROUP_ID} user \
+    && useradd -m -u ${USER_ID} -s /bin/bash -g user user
+
+USER user
+WORKDIR /home/user
+
+ENV PATH=/home/user/.local/bin:${PATH}
+RUN curl -sSL https://install.python-poetry.org | python3 -

.github/actions/with-docker/action.yml

@@ -0,0 +1,32 @@
+name: 'With Docker'
+description: 'Run a given stage with Docker Image'
+inputs:
+  container-name:
+    description: 'Docker container name to use'
+    type: string
+    required: true
+runs:
+  using: 'composite'
+  steps:
+  - name: 'Set up Docker'
+    shell: bash {0}
+    run: |
+      set -euxo pipefail
+      CONTAINER_NAME=${{ inputs.container-name }}
+      TAG=runtimeverificationinc/${CONTAINER_NAME}
+      K_VERSION=$(cat deps/k_release)
+      docker build .                                  \
+        --file .github/actions/with-docker/Dockerfile \
+        --tag ${TAG}                                  \
+        --build-arg K_VERSION=${K_VERSION}
+      docker run                          \
+        --name ${CONTAINER_NAME}          \
+        --rm                              \
+        --interactive                     \
+        --tty                             \
+        --detach                          \
+        --user root                       \
+        --workdir /home/user              \
+        ${TAG}
+      docker cp . ${CONTAINER_NAME}:/home/user
+      docker exec ${CONTAINER_NAME} chown -R user:user /home/user

.github/workflows/master.yml

@@ -0,0 +1,24 @@
+name: 'Master Push'
+on:
+  push:
+    branches:
+      - master
+
+jobs:
+
+  release:
+    name: 'Publish Release'
+    runs-on: [self-hosted, linux, flyweight]
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+        with:
+          ref: ${{ github.event.push.head.sha }}
+          fetch-depth: 0
+      - name: 'Make release'
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+        run: |
+          set -x
+          VERSION=v$(cat package/version)
+          gh release create ${VERSION} --target ${{ github.sha }}

.github/workflows/test.yml

@@ -0,0 +1,72 @@
+name: 'Test'
+on:
+  pull_request:
+  workflow_dispatch:
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+
+  version-bump:
+    name: 'Version Bump'
+    runs-on: [self-hosted, linux, flyweight]
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+        with:
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
+          fetch-depth: 0
+          ref: ${{ github.event.pull_request.head.sha }}
+      - name: 'Configure GitHub user'
+        run: |
+          git config user.name devops
+          git config user.email [email protected]
+      - name: 'Update version'
+        run: |
+          og_version=$(git show origin/${GITHUB_BASE_REF}:package/version)
+          ./package/version.sh bump ${og_version}
+          ./package/version.sh sub
+          new_version=$(cat package/version)
+          git add --update && git commit --message "Set Version: ${new_version}" || true
+      - name: 'Push updates'
+        run: git push origin HEAD:${GITHUB_HEAD_REF}
+
+  code-quality-checks:
+    needs: version-bump
+    name: 'Code Quality Checks'
+    runs-on: [self-hosted, linux, flyweight]
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+      - name: 'Run code quality checks'
+        run: make check
+      - name: 'Run pyupgrade'
+        run: make pyupgrade
+      - name: 'Run unit tests'
+        run: make test-unit
+
+  integration-tests:
+    needs: code-quality-checks
+    name: 'Integration Tests'
+    runs-on: [self-hosted, linux, normal]
+    env:
+      CONTAINER: riscv-integration-${{ github.sha }}
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-docker
+        with:
+          container-name: ${CONTAINER}
+      - name: 'Build ksoroban'
+        run: docker exec --user user ${CONTAINER} poetry install
+      - name: 'Build semantics'
+        run: docker exec --user user ${CONTAINER} make kdist-build
+      - name: 'Run integration tests'
+        run: docker exec --user user ${CONTAINER} make test-integration
+      - name: 'Tear down Docker'
+        if: always()
+        run: docker stop --time=0 ${CONTAINER}

.github/workflows/update.yml

@@ -0,0 +1,38 @@
+name: 'Update Version'
+on:
+  push:
+    branches:
+      - '_update-deps/runtimeverification/k'
+  workflow_dispatch:
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  update-deps:
+    name: 'Update Dependecies'
+    runs-on: [self-hosted, linux, flyweight]
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
+      - name: 'Configure GitHub user'
+        run: |
+          git config user.name devops
+          git config user.email [email protected]
+      - name: 'Install Python'
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.10'
+      - name: 'Install Poetry'
+        uses: Gr1N/setup-poetry@v9
+      - name: 'Update Poetry files'
+        run: |
+          K_VERSION="$(cat deps/k_release)"
+          sed -i 's!pyk = { git = "https://github.com/runtimeverification/k.git", tag = "[v0-9\.]*", subdirectory = "pyk" }!pyk = { git = "https://github.com/runtimeverification/k.git", tag = "v'${K_VERSION}'", subdirectory = "pyk" }!' pyproject.toml
+          poetry update
+          git add . && git commit -m "Sync Poetry files ${K_VERSION}" || true
+      - name: 'Push updates'
+        run: git push

.gitignore

@@ -0,0 +1,3 @@
+/dist/
+__pycache__/
+.coverage

Makefile

@@ -0,0 +1,101 @@
+POETRY     := poetry
+POETRY_RUN := $(POETRY) run
+
+
+default: check test-unit
+
+all: check cov
+
+.PHONY: clean
+clean:
+	rm -rf dist .coverage cov-* .mypy_cache .pytest_cache
+	find -type d -name __pycache__ -prune -exec rm -rf {} \;
+
+.PHONY: build
+build:
+	$(POETRY) build
+
+.PHONY: poetry-install
+poetry-install:
+	$(POETRY) install
+
+
+# Semantics
+
+kdist-build: poetry-install
+	$(POETRY) run kdist -v build riscv-semantics.llvm
+
+kdist-clean: poetry-install
+	$(POETRY) run kdist clean
+
+
+# Tests
+
+TEST_ARGS :=
+
+test: test-all
+
+test-all: poetry-install
+	$(POETRY_RUN) pytest src/tests --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
+
+test-unit: poetry-install
+	$(POETRY_RUN) pytest src/tests/unit --maxfail=1 --verbose $(TEST_ARGS)
+
+test-integration: poetry-install
+	$(POETRY_RUN) pytest src/tests/integration --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
+
+
+# Coverage
+
+COV_ARGS :=
+
+cov: cov-all
+
+cov-%: TEST_ARGS += --cov=kriscv --no-cov-on-fail --cov-branch --cov-report=term
+
+cov-all: TEST_ARGS += --cov-report=html:cov-all-html $(COV_ARGS)
+cov-all: test-all
+
+cov-unit: TEST_ARGS += --cov-report=html:cov-unit-html $(COV_ARGS)
+cov-unit: test-unit
+
+cov-integration: TEST_ARGS += --cov-report=html:cov-integration-html $(COV_ARGS)
+cov-integration: test-integration
+
+
+# Checks and formatting
+
+format: autoflake isort black
+check: check-flake8 check-mypy check-autoflake check-isort check-black
+
+check-flake8: poetry-install
+	$(POETRY_RUN) flake8 src
+
+check-mypy: poetry-install
+	$(POETRY_RUN) mypy src
+
+autoflake: poetry-install
+	$(POETRY_RUN) autoflake --quiet --in-place src
+
+check-autoflake: poetry-install
+	$(POETRY_RUN) autoflake --quiet --check src
+
+isort: poetry-install
+	$(POETRY_RUN) isort src
+
+check-isort: poetry-install
+	$(POETRY_RUN) isort --check src
+
+black: poetry-install
+	$(POETRY_RUN) black src
+
+check-black: poetry-install
+	$(POETRY_RUN) black --check src
+
+
+# Optional tools
+
+SRC_FILES := $(shell find src -type f -name '*.py')
+
+pyupgrade: poetry-install
+	$(POETRY_RUN) pyupgrade --py310-plus $(SRC_FILES)

README.md

@@ -1 +1,23 @@
-# riscv-semantics
+# kriscv
+
+
+## Installation
+
+Prerequsites: `python >= 3.10`, `pip >= 20.0.2`, `poetry >= 1.3.2`.
+
+```bash
+make build
+pip install dist/*.whl
+```
+
+
+## For Developers
+
+Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets).
+
+* `make build`: Build wheel
+* `make check`: Check code style
+* `make format`: Format code
+* `make test-unit`: Run unit tests
+
+For interactive use, spawn a shell with `poetry shell` (after `poetry install`), then run an interpreter.

deps/k_release

@@ -0,0 +1 @@
+7.0.60

flake.nix

@@ -0,0 +1,41 @@
+{
+  description = "kriscv - K tooling for the RISC-V architecture";
+  inputs = {
+    nixpkgs.url = "nixpkgs/nixos-22.05";
+    flake-utils.url = "github:numtide/flake-utils";
+    poetry2nix.url = "github:nix-community/poetry2nix";
+  };
+  outputs = { self, nixpkgs, flake-utils, poetry2nix }:
+    let
+      allOverlays = [
+        poetry2nix.overlay
+        (final: prev: {
+          kriscv = prev.poetry2nix.mkPoetryApplication {
+            python = prev.python310;
+            projectDir = ./.;
+            groups = [];
+            # We remove `dev` from `checkGroups`, so that poetry2nix does not try to resolve dev dependencies.
+            checkGroups = [];
+           };
+        })
+      ];
+    in flake-utils.lib.eachSystem [
+      "x86_64-linux"
+      "x86_64-darwin"
+      "aarch64-linux"
+      "aarch64-darwin"
+    ] (system:
+      let
+        pkgs = import nixpkgs {
+          inherit system;
+          overlays = allOverlays;
+        };
+      in {
+        packages = rec {
+          inherit (pkgs) kriscv;
+          default = kriscv;
+        };
+      }) // {
+        overlay = nixpkgs.lib.composeManyExtensions allOverlays;
+      };
+}

package/version

@@ -1 +1 @@
-0.1.0
+0.1.1