From 010b8de47856e769146dad196fb093e3cf0b54e4 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 2 Dec 2025 21:56:52 +0000 Subject: [PATCH] Support Windows compilation by disabling the REPL on Windows This also currently includes some incidental CI improvements that I made when trying to punch Github CI in the face until it worked: * Use explicit `os` versions * Use `runner.os ==` instead of `startswith(matrix.os` * Use the `setup-z3` action to set up Z3 * Use the `setup-ocaml` action. This includes caching. Also some of the tarball generation logic is moved from the Makefile into `sail_maker` (OCaml) because it's difficult to make portable Makefiles. --- .github/workflows/build.yml | 82 +++++---- .github/workflows/release.yml | 111 +++++++----- .github/workflows/test-matrix.yml | 2 +- .gitignore | 1 - Makefile | 17 +- dune-project | 9 +- lib/coverage/Makefile | 9 +- sail.opam | 4 +- sail_manifest.opam => sail_maker.opam | 0 sailcov/README.md | 2 +- src/bin/dune | 11 +- src/bin/manifest.ml.in | 4 +- src/bin/repl.disabled.ml | 50 ++++++ .../repl.disabled.mli} | 42 ++--- src/bin/{repl.ml => repl.enabled.ml} | 0 src/bin/{repl.mli => repl.enabled.mli} | 0 src/sail_maker/dune | 5 + src/sail_maker/sail_maker.ml | 167 ++++++++++++++++++ src/sail_manifest/dune | 5 - test/c/run_tests.py | 5 +- test/sailcov/run_tests.py | 2 +- 21 files changed, 394 insertions(+), 134 deletions(-) rename sail_manifest.opam => sail_maker.opam (100%) create mode 100644 src/bin/repl.disabled.ml rename src/{sail_manifest/sail_manifest.ml => bin/repl.disabled.mli} (78%) rename src/bin/{repl.ml => repl.enabled.ml} (100%) rename src/bin/{repl.mli => repl.enabled.mli} (100%) create mode 100644 src/sail_maker/dune create mode 100644 src/sail_maker/sail_maker.ml delete mode 100644 src/sail_manifest/dune diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index d60a000e9..8265f921a 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -2,69 +2,89 @@ name: Build matrix on: [push, workflow_dispatch] +# Required for vcpkg binary caching. See +# https://learn.microsoft.com/en-us/vcpkg/github-integration +permissions: + contents: write + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + VCPKG_FEATURE_FLAGS: dependencygraph OPAMVERBOSE: 1 jobs: build: strategy: matrix: - version: [4.08.1, 5.2.1] - os: [ubuntu-latest, ubuntu-24.04-arm, macos-latest] + ocaml_version: [4.08.1, 5.2.1] + os: [ubuntu-24.04, ubuntu-24.04-arm, macos-26, windows-2025] exclude: - - os: macos-latest - version: 4.08.1 + - os: macos-26 + ocaml_version: 4.08.1 + # Windows is only supported by OCaml 5 or later. + - os: windows-2025 + ocaml_version: 4.08.1 runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v4 - - name: System dependencies (ubuntu) - if: startsWith(matrix.os, 'ubuntu') - run: | - sudo apt install build-essential libgmp-dev z3 cvc4 opam + - name: System dependencies (Linux) + if: runner.os == 'Linux' + run: sudo apt install build-essential libgmp-dev cvc4 - name: System dependencies (macOS) - if: startsWith(matrix.os, 'macos') - run: | - brew install --force --overwrite gpatch gmp z3 pkgconf opam + if: runner.os == 'macOS' + run: brew install --force --overwrite gpatch gmp pkgconf - - name: Restore cached opam - id: cache-opam-restore - uses: actions/cache/restore@v4 - with: - path: ~/.opam - key: ${{ matrix.os }}-${{ matrix.version }} + - name: System dependencies (Windows) + if: runner.os == 'Windows' + run: vcpkg install gmp - - name: Setup opam - if: steps.cache-opam-restore.outputs.cache-hit != 'true' - run: | - opam init --yes --no-setup --shell=sh --compiler=${{ matrix.version }} + - name: Setup Z3 + id: z3 + uses: cda-tum/setup-z3@v1 + with: + version: 4.15.3 - - name: Save cached opam - if: steps.cache-opam-restore.outputs.cache-hit != 'true' - id: cache-opam-save - uses: actions/cache/save@v4 + - name: Set-up OCaml + uses: ocaml/setup-ocaml@v3 with: - path: ~/.opam - key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }} + ocaml-compiler: ${{ matrix.ocaml_version }} + + - name: Set LEMLIB env var + if: runner.os == 'Windows' + # Note we can't use `opam var lem:share` because lem hasn't been installed yet. + run: echo "LEMLIB=$(opam var share)\lem\library" >> $env:GITHUB_ENV + + # This contains a fix for paths on Windows but hasn't been released yet. + - name: Pin latest linksem + if: runner.os == 'Windows' + run: opam pin add linksem https://github.com/rems-project/linksem.git + + # Workaround for https://github.com/rems-project/lem/issues/38 + - name: Install and fix lem + if: runner.os == 'Windows' + run: | + opam install lem + Rename-Item -Path "$(opam var lem:bin)\lem" -NewName "lem.exe" - name: Install Sail run: | - eval $(opam env) opam pin --yes --no-action add . opam install sail --yes - name: Test Sail + # Tests use lots of unix-isms currently (fork, mkdir -p, etc). + if: runner.os != 'Windows' run: | - eval $(opam env) - etc/ci_core_tests.sh + opam exec -- bash etc/ci_core_tests.sh build-docker: strategy: matrix: - os: [ubuntu-latest, ubuntu-24.04-arm] + os: [ubuntu-24.04, ubuntu-24.04-arm] runs-on: ${{ matrix.os }} diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index c9f33bb33..6f2313bd9 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -15,36 +15,33 @@ jobs: matrix: include: - name: Linux-x86_64 - os: ubuntu-latest + os: ubuntu-24.04 container: rockylinux:8 ocaml_version: 5.2.1 - opam_arch: i686 - opam_cache_key: rocky8-5.2.1 + tarball_filename: sail-Linux-x86_64.tar.gz - name: Linux-aarch64 os: ubuntu-24.04-arm container: rockylinux:8 ocaml_version: 5.2.1 - opam_arch: arm64 - opam_cache_key: rocky8-5.2.1-arm + tarball_filename: sail-Linux-aarch64.tar.gz # MacOS disabled for now due to code signing and notarisation requirements - # - name: mac-arm64 */ - # os: macos-latest */ - # container: "" */ - # ocaml_version: 5.2.1 */ - # opam_cache_key: macos-latest-5.2.1 */ + # - name: mac-arm64 + # os: macos-26 + # container: "" + # ocaml_version: 5.2.1 + # tarball_filename: sail-Mac-arm64.tar.gz + - name: Windows-x86_64 + os: windows-2025 + container: "" + ocaml_version: 5.2.1 + tarball_filename: sail-Windows-AMD64.zip runs-on: ${{ matrix.os }} container: ${{ matrix.container }} - env: - # Disable opam warning about running as root. - OPAMROOTISOK: 1 - steps: - # This must be before checkout otherwise Github will use a zip of the - # code instead of git clone. - name: System dependencies (Linux) - if: startsWith(matrix.os, 'ubuntu') + if: runner.os == 'Linux' run: | dnf install --assumeyes \ gmp-devel \ @@ -64,15 +61,20 @@ jobs: diffutils \ rsync \ which \ - cargo - curl -L -o /usr/local/bin/opam https://github.com/ocaml/opam/releases/download/2.1.5/opam-2.1.5-${{ matrix.opam_arch }}-linux - chmod +x /usr/local/bin/opam + cargo \ + bubblewrap - - name: System dependencies (Mac) - if: startsWith(matrix.os, 'macos') + - name: System dependencies (macOS) + if: runner.os == 'macOS' run: | - brew install --force --overwrite gpatch gmp z3 pkgconf opam git rust + brew install --force --overwrite gpatch gmp pkgconf git rust + + - name: System dependencies (Windows) + if: runner.os == 'Windows' + run: vcpkg install gmp + # This must be after git has been installed otherwise Github will use a zip + # of the code instead of git clone. - uses: actions/checkout@v4 # Retreive git history (but not files) so that `git describe` works. This is @@ -89,39 +91,45 @@ jobs: git config --global --add safe.directory '*' git fetch --unshallow - - name: Restore cached ~/.opam - id: cache-opam-restore - uses: actions/cache/restore@v4 + - name: Setup Z3 + id: z3 + uses: cda-tum/setup-z3@v1 with: - path: ~/.opam - key: ${{ matrix.opam_cache_key }} + version: 4.15.3 - - name: Init opam - if: steps.cache-opam-restore.outputs.cache-hit != 'true' - run: | - # Sandboxing doesn't work in Docker. - opam init --disable-sandboxing --yes --no-setup --shell=sh --compiler=${{ matrix.ocaml_version }} && \ - eval "$(opam env)" && \ - ocaml --version - - - name: Save cached opam - if: steps.cache-opam-restore.outputs.cache-hit != 'true' - id: cache-opam-save - uses: actions/cache/save@v4 + # Note this must be after checkout otherwise it doesn't pin local packages + # and create the default switch or something. + - name: Set-up OCaml + uses: ocaml/setup-ocaml@v3 with: - path: ~/.opam - key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }} + ocaml-compiler: ${{ matrix.ocaml_version }} + + - name: Set LEMLIB env var + if: runner.os == 'Windows' + # Note we can't use `opam var lem:share` because lem hasn't been installed yet. + run: echo "LEMLIB=$(opam var share)\lem\library" >> $env:GITHUB_ENV + + # This contains a fix for paths on Windows but hasn't been released yet. + - name: Pin latest linksem + if: runner.os == 'Windows' + run: opam pin add linksem https://github.com/rems-project/linksem.git + + # Workaround for https://github.com/rems-project/lem/issues/38 + - name: Install and fix lem + if: runner.os == 'Windows' + run: | + opam install lem + Rename-Item -Path "$(opam var lem:bin)\lem" -NewName "lem.exe" - name: Install Sail run: | - eval $(opam env) opam pin --yes --no-action add . opam install sail --yes # Build Z3 from source since the binary releases only support glibc 2.31 # and old distros like RHEL 8 have 2.28. - name: Build Z3 - if: startsWith(matrix.os, 'ubuntu') + if: runner.os == 'Linux' run: | git clone --depth 1 --branch z3-4.13.0 https://github.com/Z3Prover/z3.git mkdir z3/build @@ -130,17 +138,22 @@ jobs: make -j4 make install - - name: Make release tarball + - name: Make release tarball (Linux) + if: runner.os == 'Linux' + run: | + opam exec -- make tarball Z3_EXE=z3/build/z3 + + - name: Make release tarball (Windows) + if: runner.os == 'Windows' run: | - eval $(opam env) - make tarball TARBALL_EXTRA_BIN=z3/build/z3 + opam exec -- make tarball "Z3_EXE=$($(Get-Command z3).Source)" "GMP_DLL=$($(Get-Command libgmp-10.dll).Source)" - uses: actions/attest-build-provenance@v1 with: - subject-path: _build/sail-${{ matrix.name }}.tar.gz + subject-path: _build/${{ matrix.tarball_filename }} - name: Upload tarball uses: actions/upload-artifact@v4 with: name: sail-${{ matrix.name }} - path: _build/sail-${{ matrix.name }}.tar.gz + path: _build/${{ matrix.tarball_filename }} diff --git a/.github/workflows/test-matrix.yml b/.github/workflows/test-matrix.yml index 086ec42a4..af20f1fa9 100644 --- a/.github/workflows/test-matrix.yml +++ b/.github/workflows/test-matrix.yml @@ -105,7 +105,7 @@ jobs: name: test-results-${{ matrix.suite }} path: | test/**/tests.xml - test/suite-${{ matrix.suite }}.coverage + test/suite-${{ matrix.suite }}.coverage # Only do this for one job in the test matrix - name: Upload event payload diff --git a/.gitignore b/.gitignore index 1f851a76e..0d2a469c6 100644 --- a/.gitignore +++ b/.gitignore @@ -50,7 +50,6 @@ lib/hol/sail-heap # Sail coverage /lib/coverage/Cargo.lock /lib/coverage/target -/lib/coverage/libsail_coverage.a /sailcov/sailcov # location specific things diff --git a/Makefile b/Makefile index 7409f08ad..04a9ed904 100644 --- a/Makefile +++ b/Makefile @@ -13,24 +13,23 @@ install: sail libsail_coverage: $(MAKE) -C lib/coverage +# TODO: Make this work on Windows. extraction: $(MAKE) -C src/lib/rocq mv src/lib/rocq/*.mli src/lib/extraction mv src/lib/rocq/*.ml src/lib/extraction # Build binary tarball. The lib directory is very large and not needed -# for running the compiler. TARBALL_EXTRA_BIN can be used to bundle z3. +# for running the compiler. Z3_EXE can be used to bundle a z3 binary. +# GMP_DLL can be used to bundle a libgmp DLL (this is only used on Windows currently). tarball: sail libsail_coverage dune install --relocatable --prefix=_build/tarball/sail - rm -rf _build/tarball/sail/lib - cp LICENSE _build/tarball/sail - cp THIRD_PARTY_FILES.md _build/tarball/sail - cp -a etc/tarball_extra/. _build/tarball/sail -ifdef TARBALL_EXTRA_BIN - cp $(TARBALL_EXTRA_BIN) _build/tarball/sail/bin/ -endif - cp lib/coverage/libsail_coverage.a _build/tarball/sail/share/sail/lib/coverage/ + dune exec -- sail_maker tarball --prefix=_build/tarball/sail --z3=$(Z3_EXE) --gmp=$(GMP_DLL) +ifeq ($(OS),Windows_NT) + powershell Compress-Archive -Path "_build/tarball/sail" -DestinationPath "_build/sail-Windows-$(PROCESSOR_ARCHITECTURE).zip" -Force +else tar czvf _build/sail-$(shell uname -s)-$(shell uname -m).tar.gz -C _build/tarball sail +endif coverage: dune build --release --instrument-with bisect_ppx diff --git a/dune-project b/dune-project index b28509dc1..0b69df70c 100644 --- a/dune-project +++ b/dune-project @@ -31,7 +31,7 @@ (package (synopsis "Helper tool for compiling Sail") - (name sail_manifest) + (name sail_maker) (depends (ocaml (>= 4.08.1)))) @@ -139,7 +139,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/. ") (depends (libsail (= :version)) - (sail_manifest (and (= :version) :build)) + (sail_maker (and (= :version) :build)) (sail_ocaml_backend (and (= :version) :post)) (sail_c_backend (and (= :version) :post)) (sail_smt_backend (and (= :version) :post)) @@ -150,4 +150,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/. (sail_latex_backend (and (= :version) :post)) (sail_doc_backend (and (= :version) :post)) (sail_output (and (= :version) :post)) - (linenoise (>= 1.1.0)))) + ; linenoise needs termios.h and some other headers that are not available + ; on windows (at least without installing extra cygwin packages which + ; is tricky). + (linenoise (and (>= 1.1.0) (<> :os "win32"))))) diff --git a/lib/coverage/Makefile b/lib/coverage/Makefile index 55ed9fdc6..553268451 100644 --- a/lib/coverage/Makefile +++ b/lib/coverage/Makefile @@ -1,3 +1,8 @@ -libsail_coverage.a: src/*.rs Cargo.toml Makefile +ifeq ($(OS),Windows_NT) + LIB_NAME = sail_coverage.lib +else + LIB_NAME = libsail_coverage.a +endif + +target/release/$(LIB_NAME): src/*.rs Cargo.toml Makefile cargo build --release - cp target/release/libsail_coverage.a . diff --git a/sail.opam b/sail.opam index 7c17a1156..c59368b91 100644 --- a/sail.opam +++ b/sail.opam @@ -32,7 +32,7 @@ bug-reports: "https://github.com/rems-project/sail/issues" depends: [ "dune" {>= "3.11"} "libsail" {= version} - "sail_manifest" {= version & build} + "sail_maker" {= version & build} "sail_ocaml_backend" {= version & post} "sail_c_backend" {= version & post} "sail_smt_backend" {= version & post} @@ -43,7 +43,7 @@ depends: [ "sail_latex_backend" {= version & post} "sail_doc_backend" {= version & post} "sail_output" {= version & post} - "linenoise" {>= "1.1.0"} + "linenoise" {>= "1.1.0" & os != "win32"} "odoc" {with-doc} ] build: [ diff --git a/sail_manifest.opam b/sail_maker.opam similarity index 100% rename from sail_manifest.opam rename to sail_maker.opam diff --git a/sailcov/README.md b/sailcov/README.md index 0a49f51cc..e7542c430 100644 --- a/sailcov/README.md +++ b/sailcov/README.md @@ -23,7 +23,7 @@ in [lib/coverage/](../lib/coverage/). Currently this is written in Rust for want of an obvious hashset implementation in C and can be built using `cargo build --release` which will produce a `libsail_coverage.a` static library. Once this is done, we can link this into our C -emulator by passing `$SAIL_DIR/lib/coverage/libsail_coverage.a +emulator by passing `$SAIL_DIR/lib/coverage/target/release/libsail_coverage.a -lpthread -ldl` to gcc, where SAIL_DIR is the location of this repository. diff --git a/src/bin/dune b/src/bin/dune index a14b84b6d..811d8127a 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -7,7 +7,7 @@ %{target} (chdir %{workspace_root} - (run sail_manifest -gen_manifest))))) + (run sail_maker gen_manifest))))) (executable (name sail) @@ -15,7 +15,14 @@ (public_name sail) (package sail) (link_flags -linkall) - (libraries libsail linenoise dynlink)) + (libraries + libsail + dynlink + (select + repl.ml + from + (linenoise -> repl.enabled.ml) + (-> repl.disabled.ml)))) ; For legacy reasons install all the Sail files in lib as part of this package diff --git a/src/bin/manifest.ml.in b/src/bin/manifest.ml.in index 659b10ce1..b409008c5 100644 --- a/src/bin/manifest.ml.in +++ b/src/bin/manifest.ml.in @@ -1,9 +1,9 @@ (* This file is used to generate manifest.ml when you use OPAM to install Sail. If instead you use Dune then manifest.ml will not exist and Dune will use -sail_manifest.ml to generate it. +sail_maker.ml to generate it. -So in this file we use OPAM to find the share directory. In sail_manifest.ml +So in this file we use OPAM to find the share directory. In sail_maker.ml we set `dir` to `None` so that Sail will look relative to the `sail` binary. *) diff --git a/src/bin/repl.disabled.ml b/src/bin/repl.disabled.ml new file mode 100644 index 000000000..bdafeaff6 --- /dev/null +++ b/src/bin/repl.disabled.ml @@ -0,0 +1,50 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* SPDX-License-Identifier: BSD-2-Clause *) +(****************************************************************************) + +let start_repl ?(banner = true) ?commands:(script = []) ?auto_rewrites:(rewrites = true) ~config ~options ctx env + effect_info ast = + prerr_endline "The repl is not supported on this platform."; + exit 1 diff --git a/src/sail_manifest/sail_manifest.ml b/src/bin/repl.disabled.mli similarity index 78% rename from src/sail_manifest/sail_manifest.ml rename to src/bin/repl.disabled.mli index e31ef06db..56cc65d0e 100644 --- a/src/sail_manifest/sail_manifest.ml +++ b/src/bin/repl.disabled.mli @@ -44,30 +44,24 @@ (* SPDX-License-Identifier: BSD-2-Clause *) (****************************************************************************) -open Printf +(** This module contains the function that starts an interactive sail read-eval-print loop *) -let opt_gen_manifest = ref false +open Libsail -let options = Arg.align [("-gen_manifest", Arg.Set opt_gen_manifest, "generate manifest.ml")] +(** Start an interactive top-level interpreter. This version is disabled and just prints an error message. -let git_command args = - try - let git_out, git_in, git_err = Unix.open_process_full ("git " ^ args) (Unix.environment ()) in - let res = input_line git_out in - match Unix.close_process_full (git_out, git_in, git_err) with Unix.WEXITED 0 -> Some res | _ -> None - with _ -> None - -let gen_manifest () = - (* See manifest.ml.in for more information about `dir`. *) - ksprintf print_endline "let dir = None"; - ksprintf print_endline "let commit = \"%s\"" (Option.value (git_command "rev-parse HEAD") ~default:"unknown commit"); - ksprintf print_endline "let branch = \"%s\"" - (Option.value (git_command "rev-parse --abbrev-ref HEAD") ~default:"unknown branch") - -let usage = "sail_manifest " - -let main () = - Arg.parse options (fun _ -> ()) usage; - if !opt_gen_manifest then gen_manifest () - -let () = main () + @param banner If true (default), then print an ASCII-art Sail logo. + @param commands An optional list of commands to run automatically in the repl + @param auto_rewrites Performs default rewrites (target "interpreter") on the ast passed to the repl + @param options This is the set of options for the :options interactive command *) +val start_repl : + ?banner:bool -> + ?commands:string list -> + ?auto_rewrites:bool -> + config:Yojson.Safe.t option -> + options:(Arg.key * Arg.spec * Arg.doc) list -> + Initial_check.ctx -> + Type_check.Env.t -> + Effects.side_effect_info -> + Type_check.typed_ast -> + unit diff --git a/src/bin/repl.ml b/src/bin/repl.enabled.ml similarity index 100% rename from src/bin/repl.ml rename to src/bin/repl.enabled.ml diff --git a/src/bin/repl.mli b/src/bin/repl.enabled.mli similarity index 100% rename from src/bin/repl.mli rename to src/bin/repl.enabled.mli diff --git a/src/sail_maker/dune b/src/sail_maker/dune new file mode 100644 index 000000000..4ef53d7ce --- /dev/null +++ b/src/sail_maker/dune @@ -0,0 +1,5 @@ +(executable + (name sail_maker) + (public_name sail_maker) + (package sail_maker) + (libraries unix)) diff --git a/src/sail_maker/sail_maker.ml b/src/sail_maker/sail_maker.ml new file mode 100644 index 000000000..49001f349 --- /dev/null +++ b/src/sail_maker/sail_maker.ml @@ -0,0 +1,167 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2021 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* SPDX-License-Identifier: BSD-2-Clause *) +(****************************************************************************) + +open Printf + +let git_command args = + try + let git_out, git_in, git_err = Unix.open_process_full ("git " ^ args) (Unix.environment ()) in + let res = input_line git_out in + match Unix.close_process_full (git_out, git_in, git_err) with Unix.WEXITED 0 -> Some res | _ -> None + with _ -> None + +let gen_manifest () = + (* See manifest.ml.in for more information about `dir`. *) + ksprintf print_endline "let dir = None"; + ksprintf print_endline "let commit = \"%s\"" (Option.value (git_command "rev-parse HEAD") ~default:"unknown commit"); + ksprintf print_endline "let branch = \"%s\"" + (Option.value (git_command "rev-parse --abbrev-ref HEAD") ~default:"unknown branch") + +(* Copy a single file. Surprisingly there's no built-in function for this. *) +let copy_file (input_path : string) (output_path : string) = + let buffer_size = 8192 in + let buffer = Bytes.create buffer_size in + let ic = open_in_bin input_path in + let oc = open_out_bin output_path in + try + let rec copy_loop () = + let bytes_read = input ic buffer 0 buffer_size in + if bytes_read > 0 then begin + output oc buffer 0 bytes_read; + copy_loop () + end + in + copy_loop (); + close_in ic; + close_out oc + with e -> + close_in_noerr ic; + close_out_noerr oc; + raise e + +(* Recursively remove a file or directory tree. *) +let rec remove_file_or_dir path = + if Sys.file_exists path then + if Sys.is_directory path then begin + (* Remove all contents of the directory *) + let entries = Sys.readdir path in + Array.iter + (fun entry -> + let full_path = Filename.concat path entry in + remove_file_or_dir full_path + ) + entries; + (* Remove the now-empty directory *) + Unix.rmdir path + end + else + (* Remove regular file *) + Sys.remove path + +let parse_tarball_args (args : string list) = + let usage_msg = "sail_maker tarball --prefix=PREFIX [--z3=Z3_EXE_PATH] [--gmp=GMP_DLL_PATH]" in + let prefix = ref "" in + let z3_path = ref "" in + let gmp_path = ref "" in + + let speclist = + [ + ("--prefix", Arg.Set_string prefix, "Path to install prefix"); + ("--z3", Arg.Set_string z3_path, "Set path to z3 executable"); + ("--gmp", Arg.Set_string gmp_path, "Set path to GMP shared library"); + ] + in + + (* Positional arguments are unused and will cause an error. *) + let anon_fun _ = () in + + let args = Array.of_list ("sail_maker" :: args) in + + let () = Arg.parse_argv args speclist anon_fun usage_msg in + + (!prefix, !z3_path, !gmp_path) + +let tarball (prefix : string) (z3 : string) (gmp : string) = + let bindir = Filename.concat prefix "bin" in + (* This contains a load of OCaml source files we don't need in the binary distribution. *) + remove_file_or_dir (Filename.concat prefix "lib"); + (* The sail_maker binary gets installed and I'm not sure how to avoid that with Dune + so just delete it now. *) + remove_file_or_dir (Filename.concat bindir (if Sys.win32 then "sail_maker.exe" else "sail_maker")); + (* Copy in some extra license files. Maybe Dune could do this. *) + copy_file "LICENSE" (Filename.concat prefix "LICENSE"); + copy_file "THIRD_PARTY_FILES.md" (Filename.concat prefix "THIRD_PARTY_FILES.md"); + copy_file "etc/tarball_extra/INSTALL" (Filename.concat prefix "INSTALL"); + copy_file "etc/tarball_extra/Z3_LICENSE" (Filename.concat prefix "Z3_LICENSE"); + (* Copy in precompiled coverage library. *) + let coverage_libname = if Sys.win32 then "sail_coverage.lib" else "libsail_coverage.a" in + copy_file + (Filename.concat "lib/coverage/target/release" coverage_libname) + (Filename.concat (Filename.concat prefix "share/sail/lib/coverage") coverage_libname); + (* For convenience, copy in a z3 executable and GMP shared library (Windows only). *) + if z3 <> "" then copy_file z3 (Filename.concat bindir (Filename.basename z3)); + if gmp <> "" then copy_file gmp (Filename.concat bindir (Filename.basename gmp)); + () + +let usage = + "sail_maker gen_manifest\n\n\ + \ Write manifest.ml to stdout containing Git commit and branch information.\n\n\n\n\ + sail_maker tarball --prefix=PREFIX [--z3=Z3_EXE_PATH] [--gmp=GMP_DLL_PATH]\n\n\ + \ Used for fixing up the `dune install` output in preparation for making release tarballs.\n\n" + +let main () = + (* OCaml's pattern matching support is not very good for arrays so convert + to a list. OCaml loves lists more than ones and zeros. *) + match Array.to_list Sys.argv with + | [_; "gen_manifest"] -> gen_manifest () + | _ :: "tarball" :: args -> + let prefix, z3_path, gmp_path = parse_tarball_args args in + tarball prefix z3_path gmp_path + | _ -> + prerr_endline usage; + exit 1 + +let () = main () diff --git a/src/sail_manifest/dune b/src/sail_manifest/dune deleted file mode 100644 index 3a43baba6..000000000 --- a/src/sail_manifest/dune +++ /dev/null @@ -1,5 +0,0 @@ -(executable - (name sail_manifest) - (public_name sail_manifest) - (package sail_manifest) - (libraries unix)) diff --git a/test/c/run_tests.py b/test/c/run_tests.py index eef0904ca..a667e0dfe 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -229,7 +229,10 @@ def test_coq(name): xml += test_c('optimized C++', '-O2', '-O', True, compiler='c++', actually_cpp=True) if 'interpreter' in targets: - xml += test_interpreter('interpreter') + if os.name == 'posix': + xml += test_interpreter('interpreter') + else: + print('Skipping interpreter tests because the interpreter is only supported on Unix-like platforms') if 'ocaml' in targets: xml += test_ocaml('OCaml') diff --git a/test/sailcov/run_tests.py b/test/sailcov/run_tests.py index d4b45afd4..89d9ae525 100755 --- a/test/sailcov/run_tests.py +++ b/test/sailcov/run_tests.py @@ -39,7 +39,7 @@ def test_sailcov(): tests[filename] = os.fork() if tests[filename] == 0: step('\'{}\' -no_warn -no_memo_z3 -c -c_include sail_coverage.h -c_coverage {}.branches {} -o {}'.format(sail, basename, filename, basename)) - step('cc {}.c \'{}\'/lib/*.c \'{}\'/lib/coverage/libsail_coverage.a -lgmp -lpthread -ldl -I \'{}\'/lib -o {}.bin'.format(basename, sail_dir, sail_dir, sail_dir, basename)) + step('cc {}.c \'{}\'/lib/*.c \'{}\'/lib/coverage/target/release/libsail_coverage.a -lgmp -lpthread -ldl -I \'{}\'/lib -o {}.bin'.format(basename, sail_dir, sail_dir, sail_dir, basename)) step('./{}.bin -c {}.taken'.format(basename, basename)) step('\'{}\' --werror --all {}.branches --taken {}.taken {}'.format(sailcov, basename, basename, filename)) step('diff {}.html {}.expect'.format(basename, basename))