Skip to content

Commit

Permalink
Include MIR JSON files for Rust standard libs in SAW bindists
Browse files Browse the repository at this point in the history
When distributing SAW binaries, we want users to be able to turn their Rust
code into MIR JSON with relatively minimal effort. To that end, this patch
includes JSON files for the Rust standard libraries in SAW binary distributions
so that users do not have to build this themselves. This mirrors how these
files are included in `crux-mir` binary distributions.

This checks off one box in #1859.
  • Loading branch information
RyanGlScott committed May 10, 2023
1 parent df95bf4 commit c7006f7
Show file tree
Hide file tree
Showing 5 changed files with 48 additions and 1 deletion.
4 changes: 4 additions & 0 deletions .github/ci.sh
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
set -Eeuxo pipefail

[[ "$RUNNER_OS" == 'Windows' ]] && IS_WIN=true || IS_WIN=false
[[ "$RUNNER_OS" == 'Linux' ]] && IS_LINUX=true || IS_LINUX=false
BIN=$(pwd)/bin
EXT=""
$IS_WIN && EXT=".exe"
Expand Down Expand Up @@ -93,6 +94,9 @@ bundle_files() {
cp LICENSE README.md dist/
$IS_WIN || chmod +x dist/bin/*

if $IS_LINUX; then
cp -r deps/crucible/crux-mir/rlibs dist/lib
fi
(cd deps/cryptol-specs && git archive --prefix=cryptol-specs/ --format=tar HEAD) | (cd dist/deps && tar x)
cp doc/extcore.md dist/doc
cp doc/tutorial/sawScriptTutorial.pdf dist/doc/tutorial.pdf
Expand Down
27 changes: 27 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,12 @@ env:
CACHE_VERSION: 1
DISABLED_TESTS: "test0000 test_FNV_a1_rev test0010_jss_cnf_exp test0039_rust test_boilerplate test_external_abc"

# Keep this in sync with the mir-json version documented in
# deps/mir-json/README.md.
RUST_TOOLCHAIN_VERSION: "nightly-2020-03-22"
# Work around https://github.com/rust-lang/cargo/issues/10303
CARGO_NET_GIT_FETCH_WITH_CLI: true

# Solver package snapshot date - also update in the following locations:
# ./saw/Dockerfile
# ./saw-remote-api/Dockerfile
Expand Down Expand Up @@ -119,6 +125,22 @@ jobs:
cabal user-config update -a "extra-include-dirs: \"\""
cabal user-config update -a "extra-lib-dirs: \"\""
- name: Install Rust toolchain
uses: actions-rs/toolchain@v1
# For now, we only run Rust-related steps on Linux. mir-json does not
# currently support Windows, and mir-json is currently broken on macOS
# due to https://github.com/GaloisInc/mir-json/issues/31.
if: runner.os == 'Linux'
with:
toolchain: ${{ env.RUST_TOOLCHAIN_VERSION }}
override: true
components: rustc-dev

- name: Install mir-json
shell: bash
if: runner.os == 'Linux'
run: cd deps/mir-json && cargo install --locked --force

- shell: bash
run: .github/ci.sh install_system_deps
env:
Expand Down Expand Up @@ -146,6 +168,11 @@ jobs:
- shell: bash
run: .github/ci.sh build

- name: Translate Rust standard libraries with mir-json
shell: bash
if: runner.os == 'Linux'
run: cd deps/crucible/crux-mir && bash ./translate_libs.sh

- shell: bash
env:
RELEASE: ${{ needs.config.outputs.release }}
Expand Down
3 changes: 3 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
Expand Up @@ -46,3 +46,6 @@
[submodule "deps/language-sally"]
path = deps/language-sally
url = https://github.com/GaloisInc/language-sally
[submodule "deps/mir-json"]
path = deps/mir-json
url = https://github.com/GaloisInc/mir-json
1 change: 1 addition & 0 deletions deps/mir-json
Submodule mir-json added at 3a621e
14 changes: 13 additions & 1 deletion doc/manual/manual.md
Original file line number Diff line number Diff line change
Expand Up @@ -1715,7 +1715,19 @@ Note that:
the `.linked-mir.json` file that appears after `linking X mir files into`, as
that is the JSON file that must be loaded with SAW.
* `SAW_RUST_LIBRARY_PATH` should point to the the MIR JSON files for the Rust
standard library.
standard libraries.

SAW binary distributions include these MIR JSON files, so if you are using a
SAW binary distribution, it suffices to define
`SAW_RUST_LIBRARY_PATH=<saw-directory>/lib/rlibs`. If you are building SAW
from source, you must also build the MIR JSON files for the Rust standard
libraries from source. To do so, run the following commands:

```
$ cd deps/crucible/crux-mir
$ ./translate_libs.sh
$ export SAW_RUST_LIBRARY_PATH=$(pwd)/rlibs
```

`mir-json` also supports compiling individual `.rs` files through `mir-json`'s
`saw-rustc` command. As the name suggests, it accepts all of the flags that
Expand Down

0 comments on commit c7006f7

Please sign in to comment.