emulating illegal instructions #411
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| --- | |
| name: Verification tests | |
| on: [push, pull_request] | |
| jobs: | |
| build: | |
| name: Verify | |
| runs-on: ubuntu-latest # container actions require GNU/Linux | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v4 | |
| with: | |
| persist-credentials: false | |
| submodules: 'true' | |
| - name: Install opam dependencies | |
| run: sudo apt update -y && sudo apt install -y pkg-config git rsync tar unzip m4 time curl ocaml build-essential bubblewrap gawk libgmp-dev python2.7 python3 python3-distutils libmpfr-dev | |
| - name: Install opam | |
| run: curl "https://github.com/ocaml/opam/releases/download/2.1.5/opam-2.1.5-x86_64-linux" -Lo /usr/local/bin/opam && chmod +x /usr/local/bin/opam | |
| - name: Setup opam | |
| run: opam init -y | |
| - name: Setup opam switch | |
| run: opam switch create refinedrust-ace --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda | |
| - name: Install coq | |
| run: eval $(opam env) && opam update && opam pin add coq 8.17.1 -y | |
| - name: ls | |
| run: ls -la . | |
| - name: Install openssl dependency | |
| run: sudo apt update && sudo apt install libssl-dev -y | |
| - name: Install rustup | |
| run: curl --proto "=https" --tlsv1.2 -sSf https://sh.rustup.rs | bash /dev/stdin "-y" | |
| - name: Setup Rust toolchain | |
| run: source "$HOME/.cargo/env" && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/setup-rust.sh | |
| - name: Install the RiscV target for RefinedRust's toolchain | |
| run: source "$HOME/.cargo/env" && cd ./verification/refinedrust/rr_frontend && rustup target add riscv64gc-unknown-none-elf | |
| - name: Install frontend | |
| run: source "$HOME/.cargo/env" && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-frontend.sh | |
| - name: Install Opam dependencies | |
| run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/setup-coq.sh | |
| - name: Install RefinedRust type system | |
| run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-typesystem.sh | |
| - name: Install RefinedRust stdlib | |
| run: eval $(opam env) && REFINEDRUST_ROOT=$PWD/verification/refinedrust ./verification/refinedrust/scripts/install-stdlib.sh | |
| - name: Generate stdlib metadata | |
| run: eval $(opam env) && make -C verification/refinedrust/stdlib generate_stdlib | |
| - name: Exclude RefinedRust from dune build | |
| run: echo "(dirs :standard \ generated_code.bak refinedrust)" > verification/dune | |
| - name: install build dependencies | |
| run: sudo apt -qq -y install wget autoconf automake autotools-dev curl python3 libmpc-dev libmpfr-dev libgmp-dev gawk build-essential bison flex texinfo gperf libtool patchutils bc zlib1g-dev libexpat-dev xz-utils | |
| - name: install OpenSBI dependencies | |
| run: sudo apt -qq -y install clang | |
| - name: install Buildroot dependencies | |
| run: sudo apt -qq -y install unzip sed binutils diffutils build-essential bash patch gzip bzip2 perl tar cpio unzip rsync file bc findutils | |
| - name: make setup | |
| run: source "$HOME/.cargo/env" && eval $(opam env) && make setup | |
| - name: make devtools | |
| run: source "$HOME/.cargo/env" && eval $(opam env) && make devtools | |
| - name: Translate specified files using RefinedRust and check proofs | |
| run: source "$HOME/.cargo/env" && eval $(opam env) && make verify |