main.yml

# This is a basic workflow to help you get started with Actions

name: CI

# Controls when the workflow will run
on:
  # Triggers the workflow on push or pull request events but only for the develop branch
  push:
  #pull_request:

  # Allows you to run this workflow manually from the Actions tab
  #workflow_dispatch:

# A workflow run is made up of one or more jobs that can run sequentially or in parallel
jobs:
  prove_specs:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository and submodules
        uses: actions/checkout@v2
        with:
          submodules: recursive
      - name: Prove specs
        uses: addnab/docker-run-action@v3
        with:
          image: galoisinc/hardens
          options: -v ${{ github.workspace }}:/HARDENS
          run: |
            make -C saw
            make -C models
            make -C specs validate
            make -C specs clean
            make -C specs

  prove_framac:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository and submodules
        uses: actions/checkout@v2
        with:
          submodules: recursive
      - name: Run Frama-C proofs
        uses: addnab/docker-run-action@v3
        with:
          image: framac/frama-c:dev
          options: -v ${{ github.workspace }}:/HARDENS
          run: |
            cp -r /HARDENS/ /tmp
            make -C /tmp/HARDENS/src -f frama_c.mk proofs

  rts_posix_scenarios:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository and submodules
        uses: actions/checkout@v2
        with:
          submodules: recursive
      - name: Build RTS and run test scenarios
        uses: addnab/docker-run-action@v3
        with:
          image: galoisinc/hardens
          options: -v ${{ github.workspace }}:/HARDENS
          run: |
            make rts
            cd tests && 
            pip3 install -r requirements.txt &&
            RTS_DEBUG=1 QUICK=1 python3 ./run_all.py

  rts_riscv_build_verilator:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository and submodules
        uses: actions/checkout@v2
        with:
          submodules: recursive
      - name: Build RTS and run test scenarios
        uses: addnab/docker-run-action@v3
        with:
          image: galoisinc/hardens
          options: -v ${{ github.workspace }}:/HARDENS
          run: |
            make rts
            PLATFORM=RV32_bare_metal make rts
# NOTE: there is currently no way to run RISCV scenarios

  rts_riscv_build_fpga:
    runs-on: ubuntu-latest
    steps:
      - name: Checkout repository and submodules
        uses: actions/checkout@v2
        with:
          submodules: recursive
      - name: Build RTS and run test scenarios
        uses: addnab/docker-run-action@v3
        with:
          image: galoisinc/hardens
          options: -v ${{ github.workspace }}:/HARDENS
          run: |
            make rts
            PLATFORM=RV32_bare_metal DEV_BOARD=LFE5UM5G_85F_EVN make rts