Syntax for parsing Rust (#1)

* Syntax for parsing Rust

* Run tests on PRs

* Fix review comments

* Make sure we re-run failing tests

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

@@ -0,0 +1,33 @@
+name: 'With Docker'
+description: 'Run a given stage with Docker Image'
+inputs:
+  container-name:
+    description: 'Docker container name to use'
+    required: true
+runs:
+  using: 'composite'
+  steps:
+  - name: 'Set up Docker'
+    shell: bash {0}
+    env:
+      CONTAINER_NAME: ${{ inputs.container-name }}
+    run: |
+      set -euxo pipefail
+
+      TAG=runtimeverificationinc/${CONTAINER_NAME}
+      K_COMMIT=$(cat ./deps/k_release)
+
+      docker build . --tag ${TAG} --build-arg K_COMMIT=${K_COMMIT}
+
+      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/build-and-test.yaml

@@ -0,0 +1,30 @@
+---
+  name: 'Build And Test'
+  on:
+    pull_request:
+  # Stop in progress workflows on the same branch and same workflow to use latest committed code
+  concurrency:
+    group: ${{ github.workflow }}-${{ github.ref }}
+    cancel-in-progress: true
+
+  jobs:
+    build-test:
+      name: 'Build And Test'
+      runs-on: [self-hosted, linux, normal]
+      steps:
+        - name: 'Check out code'
+          uses: actions/checkout@v3
+          with:
+            submodules: recursive
+        - name: 'Set up Docker'
+          uses: ./.github/actions/with-docker
+          with:
+            container-name: k-rust-demo-${{ github.sha }}
+        - name: 'Build the semantics'
+          run: docker exec -t k-rust-demo-${{ github.sha }} /bin/bash -c 'make build -j4'
+        - name: 'Run Tests'
+          run: docker exec -t k-rust-demo-${{ github.sha }} /bin/bash -c 'make -j4 test'
+        - name: 'Tear down Docker'
+          if: always()
+          run: |
+            docker stop k-rust-demo-${{ github.sha }}

Dockerfile

@@ -0,0 +1,36 @@
+ARG Z3_VERSION
+ARG K_COMMIT
+
+ARG Z3_VERSION=4.12.1
+FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3
+
+ARG K_COMMIT
+FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_COMMIT}
+
+COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
+
+# RUN    apt-get update              \
+#     && apt-get upgrade --yes       \
+#     && apt-get install --yes       \
+#                        cmake       \
+#                        curl        \
+#                        pandoc      \
+#                        python3     \
+#                        python3-pip \
+#                        wabt
+
+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:user
+WORKDIR /home/user
+
+# RUN    curl -sSL https://install.python-poetry.org | python3 - \
+#     && poetry --version
+
+# RUN pip3 install --user  \
+#            cytoolz       \
+#            numpy
+
+# ENV PATH=/home/user/wabt/build:/home/user/.local/bin:$PATH

Makefile

@@ -0,0 +1,26 @@
+SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -name '*')
+RUST_KOMPILED ::= .build/rust-kompiled
+RUST_TIMESTAMP ::= $(RUST_KOMPILED)/timestamp
+SYNTAX_INPUT_DIR ::= tests/syntax
+SYNTAX_OUTPUTS_DIR ::= .build/syntax-output
+
+SYNTAX_INPUTS ::= $(wildcard $(SYNTAX_INPUT_DIR)/*.rs)
+SYNTAX_OUTPUTS ::= $(patsubst $(SYNTAX_INPUT_DIR)/%.rs,$(SYNTAX_OUTPUTS_DIR)/%.rs-parsed,$(SYNTAX_INPUTS))
+
+.PHONY: clean build test syntax-test
+
+clean:
+	rm -r .build
+
+build: $(RUST_TIMESTAMP)
+
+test: syntax-test
+
+syntax-test: $(SYNTAX_OUTPUTS)
+
+$(RUST_TIMESTAMP): $(SEMANTICS_FILES)
+	$$(which kompile) rust-semantics/rust.md -o $(RUST_KOMPILED)
+
+$(SYNTAX_OUTPUTS_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_TIMESTAMP)
+	mkdir -p $(SYNTAX_OUTPUTS_DIR)
+	kast --definition $(RUST_KOMPILED) $< --sort Crate > $@ || (rm $@ && false)

deps/k_release

@@ -0,0 +1 @@
+7.1.92

rust-semantics/rust.md

@@ -0,0 +1,8 @@
+```k
+requires "syntax.md"
+
+module RUST
+  imports RUST-SHARED-SYNTAX
+endmodule
+
+```