(github/ci) add toml-translator step to CI

rems-project · May 19, 2024 · d401fae · d401fae
1 parent b991613
commit d401fae
Showing 1 changed file with 30 additions and 0 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -4,6 +4,7 @@ on:
   push:
     branches:
       - master
+      - prepare-litmus-toml-translator
   # pull_request: {}
 
 # cancel in-progress job when a new push is performed
@@ -24,12 +25,26 @@ jobs:
     timeout-minutes: 5
     steps:
     - uses: actions/checkout@v3
+    - uses: actions-rs/toolchain@v1
+        with:
+          profile: minimal
+          toolchain: stable
 
     - name: System dependencies (ubuntu)
       run: |
         sudo apt update
         sudo apt install build-essential gcc-aarch64-linux-gnu qemu-system-aarch64
 
+    -name: Setup rems-project dependencies
+    steps:
+        run: |
+          mkdir -p deps/rems-project deps/litmus-tests
+          cd deps/rems-project
+          git clone https://github.com/rems-project/isla
+          git clone https://github.com/rems-project/isla-snapshots
+          cd ../litmus-tests
+          git clone https://github.com/litmus-tests/litmus-tests-armv8a-system-vmsa/
+
     - name: Build harness
       run: |
         make build
@@ -42,3 +57,18 @@ jobs:
       run: |
         ./qemu_unittests --no-test-linear-concretization | tee log
         [ $(tail -c -2 log) -eq 0 ]
+
+    - name: Build tools
+      run: |
+        make tools
+
+    - name: Run TOML translator
+      run: |
+        make translate-toml-tests REMSORGDIR=deps/rems-project LITMUSORGDIR=deps/litmus-tests
+
+    - name: Compile translated tests
+      run: |
+        # should automatically discover and build new tests
+        make build
+        # validate by checking an arbitrarily-picked test was actually compiled
+        [ -f ./bin/litmus/litmus_tests/generated/pgtable/CoWinvT+po.litmus.toml.o ]