Aggregated RISCV64 + CI work

.github/workflows/binary-decompilation.yml

@@ -0,0 +1,157 @@
+# Copyright 2022 Kry10 Limited
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+name: Binary decompilation
+
+on:
+  repository_dispatch:
+    types:
+      - binary-verification
+  workflow_dispatch:
+    inputs:
+      repo:
+        description: 'Repository'
+        required: true
+        type: string
+        default: 'seL4/l4v'
+      run_id:
+        description: 'Workflow run ID'
+        required: true
+      tag:
+        description: |
+          A brief description of the source of the event,
+          e.g. a workflow identifier. This is used when
+          reporting the results of a binary verification
+          run, to help users identify the proof run that
+          triggered the binary verification run.
+        required: true
+        type: string
+        default: 'workflow-dispatch'
+
+jobs:
+  targets:
+    # Fetch artifacts from the remote workflow that triggered this one,
+    # and store them locally in this workflow for easier access during the
+    # matrix job. Also identify which targets to run in the matrix.
+    name: Prepare decompilation targets
+    runs-on: ubuntu-latest
+    outputs:
+      targets_enabled: ${{ steps.prepare.outputs.targets_enabled }}
+    steps:
+      - name: Indentify trigger
+        id: id_trigger
+        # Different event types use different context variables for the inputs,
+        # so here we figure out which variables to use.
+        run: |
+          # Identify source workflow
+          set -euo pipefail
+          case "${{ github.event_name }}" in
+            repository_dispatch)
+              echo "trigger_repo=${{ github.event.client_payload.repo }}" >> "${GITHUB_OUTPUT}"
+              echo "trigger_run=${{ github.event.client_payload.run_id }}" >> "${GITHUB_OUTPUT}"
+              echo "trigger_tag=${{ github.event.client_payload.tag }}" >> "${GITHUB_OUTPUT}"
+              ;;
+            workflow_dispatch)
+              echo "trigger_repo=${{ github.event.input.repo }}" >> "${GITHUB_OUTPUT}"
+              echo "trigger_run=${{ github.event.input.run_id }}" >> "${GITHUB_OUTPUT}"
+              echo "trigger_tag=${{ github.event.input.tag }}" >> "${GITHUB_OUTPUT}"
+              ;;
+            *)
+              echo "Unexpected github.event_name: ${{ github.event_name }}"
+              exit 1
+              ;;
+          esac
+
+      - name: Download kernel builds from source workflow
+        uses: seL4/ci-actions/await-remote-artifacts@master
+        with:
+          repo: ${{ steps.id_trigger.outputs.trigger_repo }}
+          run-id: ${{ steps.id_trigger.outputs.trigger_run }}
+          artifact-names: kernel-builds
+          token: ${{ secrets.PRIV_REPO_TOKEN }}
+          download-dir: artifacts
+
+      - name: Checkout graph-refine
+        uses: actions/checkout@v3
+        with:
+          path: graph-refine
+
+      - name: Install Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.11'
+      - run: pip install lxml
+
+      - name: Prepare job
+        id: prepare
+        run: graph-refine/ci/github-prepare-decompile.py artifacts/kernel-builds job
+        env:
+          TAG: ${{ steps.id_trigger.outputs.trigger_tag }}
+          PROOF_REPO: ${{ steps.id_trigger.outputs.trigger_repo }}
+          PROOF_RUN: ${{ steps.id_trigger.outputs.trigger_run }}
+          DECOMPILE_REPO: ${{ github.repository }}
+          DECOMPILE_RUN: ${{ github.run_id }}
+
+      - name: Upload job
+        uses: actions/upload-artifact@v3
+        with:
+          name: graph-refine-job
+          path: job
+          if-no-files-found: ignore
+
+  decompilation:
+    name: Decompile
+    needs: targets
+    if: needs.targets.outputs.targets_enabled != '[]'
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        target: ${{ fromJSON(needs.targets.outputs.targets_enabled) }}
+    steps:
+      - name: Download targets
+        uses: actions/download-artifact@v3
+        with:
+          name: graph-refine-job
+          path: job
+      - name: Decompile
+        run: |
+          # Decompile
+          docker run --rm -i \
+            --mount "type=bind,src=${PWD}/job/targets/${{matrix.target}}/target,dst=/target" \
+            --mount "type=tmpfs,dst=/tmp" \
+            ghcr.io/sel4/sel4-decompiler /target
+          # Isolate current target for re-upload,
+          # to avoid interference between matrix jobs.
+          mkdir -p "my-job/targets/${{matrix.target}}"
+          mv "job/targets/${{matrix.target}}/target" "my-job/targets/${{matrix.target}}/target"
+      - name: Re-upload target
+        uses: actions/upload-artifact@v3
+        with:
+          name: graph-refine-job
+          path: my-job
+
+  submission:
+    name: Submit graph-refine job
+    needs: decompilation
+    runs-on: ubuntu-latest
+    steps:
+      - name: Download targets
+        uses: actions/download-artifact@v3
+        with:
+          name: graph-refine-job
+          path: job
+      - name: Checkout graph-refine
+        uses: actions/checkout@v3
+        with:
+          path: graph-refine
+      - name: Submit graph-refine job
+        env:
+          BV_BACKEND_WORK_DIR: bv
+          BV_SSH_CONFIG: "${{ secrets.BV_SSH_CONFIG }}"
+          BV_SSH_KEY: "${{ secrets.BV_SSH_KEY }}"
+          BV_SSH_KNOWN_HOSTS: "${{ secrets.BV_SSH_KNOWN_HOSTS }}"
+          DOCKER_RUN_COMMAND: "${{ secrets.DOCKER_RUN_COMMAND }}"
+          JOB_DIR: job
+        run: graph-refine/ci/submit-graph-refine

.github/workflows/docker-build.yml

@@ -0,0 +1,122 @@
+# Copyright (c) 2022, Kry10 Limited
+# SPDX-License-Identifier: BSD-2-Clause
+
+name: Build
+
+on:
+  # FIXME: When RISC-V and ARM branches are merged to master:
+  #        - switch the push trigger to master,
+  #        - add schedule and pull_request triggers.
+  push:
+    branches:
+      - ci-riscv64
+
+# Ensure Docker image builds are fully serialised,
+# so there is not a race to set the `latest` tag.
+concurrency:
+  group: graph-refine-docker-builds
+  cancel-in-progress: true
+
+jobs:
+  build:
+    name: Build
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout graph-refine
+        uses: actions/checkout@v3
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@v2
+        with:
+          registry: ghcr.io
+          username: seL4
+          password: ${{ secrets.GITHUB_TOKEN }}
+      - name: Set up Git
+        env:
+          CI_SSH: ${{ secrets.CI_SSH }}
+        shell: bash
+        run: |
+          # Configure SSH access and Git identity
+          eval $(ssh-agent)
+          ssh-add -q - <<< "${CI_SSH}"
+          echo "SSH_AUTH_SOCK=${SSH_AUTH_SOCK}" >> "${GITHUB_ENV}"
+          git config --global user.name "seL4 CI"
+          git config --global user.email "ci@sel4.systems"
+      # We use the Nix package manager to build Docker images.
+      - name: Install Nix
+        uses: cachix/install-nix-action@v20
+        with:
+          nix_path: nixpkgs=channel:nixos-unstable
+      # We cache Nix builds using cachix.org.
+      - name: Install Cachix
+        uses: cachix/cachix-action@v12
+        with:
+          name: sel4-bv
+          authToken: "${{ secrets.BV_CACHIX_AUTH_TOKEN }}"
+      - name: Build graph-refine
+        shell: bash
+        run: |
+          # Build graph-refine
+          build_image() { nix-build -A "$1" -o "$1" nix/graph-refine.nix; }
+          build_image graph-refine-image
+          build_image graph-refine-runner-image
+      - name: Load and tag graph-refine images
+        id: image_tags
+        run: |
+          # Load and tag graph-refine images
+          ./graph-refine-image | docker load
+          ./graph-refine-runner-image | docker load
+          TAG="$(docker image ls --format '{{.Tag}}' graph-refine)"
+          RUN_TAG="$(docker image ls --format '{{.Tag}}' graph-refine-runner)"
+          echo "runner_tag=$RUN_TAG" >> "$GITHUB_OUTPUT"
+          docker tag "graph-refine:$TAG" ghcr.io/sel4/graph-refine:latest
+          docker tag "graph-refine:$TAG" ghcr.io/sel4/graph-refine:"$TAG"
+          docker tag "graph-refine-runner:$RUN_TAG" ghcr.io/sel4/graph-refine-runner:latest
+          docker tag "graph-refine-runner:$RUN_TAG" ghcr.io/sel4/graph-refine-runner:"$RUN_TAG"
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.10'
+      - name: Checkout HOL4 and polyml
+        run: decompiler/setup-decompiler.py checkout --upstream --ssh
+      - name: Build decompiler
+        run: |
+          # Build decompiler
+          nix-build -A decompiler-image -o decompiler-image decompiler
+          nix-build -A sel4-decompiler-image -o sel4-decompiler-image seL4-example
+      - name: Load and tag decompiler image
+        run: |
+          # Load and tag decompiler image
+          ./decompiler-image | docker load
+          ./sel4-decompiler-image | docker load
+          IMAGE_TAG="$(docker image ls --format '{{.Tag}}' decompiler)"
+          SEL4_IMAGE_TAG="$(docker image ls --format '{{.Tag}}' sel4-decompiler)"
+          docker tag "decompiler:$IMAGE_TAG" ghcr.io/sel4/decompiler:latest
+          docker tag "decompiler:$IMAGE_TAG" ghcr.io/sel4/decompiler:"$IMAGE_TAG"
+          docker tag "sel4-decompiler:$SEL4_IMAGE_TAG" ghcr.io/sel4/sel4-decompiler:latest
+          docker tag "sel4-decompiler:$SEL4_IMAGE_TAG" ghcr.io/sel4/sel4-decompiler:"$SEL4_IMAGE_TAG"
+      - name: Push upstream branches
+        if: github.event_name == 'push' || github.event_name == 'schedule'
+        run: |
+          # Push upstream branches
+          (cd decompiler/src/HOL4 && git push)
+          (cd decompiler/src/polyml && git push)
+      - name: Push Docker images
+        if: github.event_name == 'push' || github.event_name == 'schedule'
+        run: |
+          # Push Docker images
+          docker push --all-tags ghcr.io/sel4/graph-refine
+          docker push --all-tags ghcr.io/sel4/graph-refine-runner
+          docker push --all-tags ghcr.io/sel4/decompiler
+          docker push --all-tags ghcr.io/sel4/sel4-decompiler
+      # Ensure the graph-refine backend is using an up-to-date runner
+      - name: Install graph-refine-runner
+        if: github.event_name == 'push' || github.event_name == 'schedule'
+        env:
+          BV_BACKEND_WORK_DIR: bv
+          BV_BACKEND_CONCURRENCY: 64
+          BV_SSH_CONFIG: "${{ secrets.BV_SSH_CONFIG }}"
+          BV_SSH_KEY: "${{ secrets.BV_SSH_KEY }}"
+          BV_SSH_KNOWN_HOSTS: "${{ secrets.BV_SSH_KNOWN_HOSTS }}"
+          DOCKER_RUN_COMMAND: "${{ secrets.DOCKER_RUN_COMMAND }}"
+          RUNNER_TAG: "${{ steps.image_tags.outputs.runner_tag }}"
+        run: ci/install-runner

.gitignore

@@ -5,4 +5,12 @@
 #
 
 .pyc
-/internal/
+__pycache__/
+
+# Nix
+/result*
+
+# Decompiler setup
+/decompiler/decompile
+/decompiler/src/
+/decompiler/install/

README.md

@@ -15,7 +15,7 @@ use of SMT solvers.
 The design and theory of this tool are described in the paper [Translation
 Validation for a Verified OS Kernel][1] by Sewell, Myreen & Klein.
 
-  [1]: https://ts.data61.csiro.au/publications/nictaabstracts/Sewell_MK_13.abstract "Translation Validation for a Verified OS Kernel"
+  [1]: https://trustworthy.systems/publications/nictaabstracts/Sewell_MK_13.abstract "Translation Validation for a Verified OS Kernel"
 
 Repository Setup
 ----------------

c_rodata.py

@@ -8,35 +8,35 @@
 import target_objects
 
 def get_cache (p):
-	k = 'c_rodata_hook_cache'
-	if k not in p.cached_analysis:
-		p.cached_analysis[k] = {}
-	return p.cached_analysis[k]
+    k = 'c_rodata_hook_cache'
+    if k not in p.cached_analysis:
+        p.cached_analysis[k] = {}
+    return p.cached_analysis[k]
 
 def hook (rep, (n, vc)):
-	p = rep.p
-	tag = p.node_tags[n][0]
-	is_C = tag == 'C' or p.hook_tag_hints.get (tag, None) == 'C'
-	if not is_C:
-		return
-	upd_ps = [rep.to_smt_expr (ptr, (n, vc))
-		for (kind, ptr, v, m) in p.nodes[n].get_mem_accesses ()
-		if kind == 'MemUpdate']
-	if not upd_ps:
-		return
-	cache = get_cache (p)
-	for ptr in set (upd_ps):
-		pc = rep.get_pc ((n, vc))
-		eq_rodata = rep.solv.get_eq_rodata_witness (ptr)
-		hyp = rep.to_smt_expr (syntax.mk_implies (pc,
-			syntax.mk_not (eq_rodata)), (n, vc))
-		if ((n, vc), ptr) in cache:
-			res = cache[((n, vc), ptr)]
-		else:
-			res = rep.test_hyp_whyps (hyp, [], cache = cache)
-			cache[((n, vc), ptr)] = res
-		if res:
-			rep.solv.assert_fact (hyp, {})
+    p = rep.p
+    tag = p.node_tags[n][0]
+    is_C = tag == 'C' or p.hook_tag_hints.get (tag, None) == 'C'
+    if not is_C:
+        return
+    upd_ps = [rep.to_smt_expr (ptr, (n, vc))
+              for (kind, ptr, v, m) in p.nodes[n].get_mem_accesses ()
+              if kind == 'MemUpdate']
+    if not upd_ps:
+        return
+    cache = get_cache (p)
+    for ptr in set (upd_ps):
+        pc = rep.get_pc ((n, vc))
+        eq_rodata = rep.solv.get_eq_rodata_witness (ptr)
+        hyp = rep.to_smt_expr (syntax.mk_implies (pc,
+                                                  syntax.mk_not (eq_rodata)), (n, vc))
+        if ((n, vc), ptr) in cache:
+            res = cache[((n, vc), ptr)]
+        else:
+            res = rep.test_hyp_whyps (hyp, [], cache = cache)
+            cache[((n, vc), ptr)] = res
+        if res:
+            rep.solv.assert_fact (hyp, {})
 
 module_hook_k = 'c_rodata'
 target_objects.add_hook ('post_emit_node', module_hook_k, hook)