Skip to content

Commit

Permalink
Merge branch 'master' into docs/build-std
Browse files Browse the repository at this point in the history
  • Loading branch information
dkcumming authored Jan 23, 2025
2 parents 798ce16 + 5314e1f commit 1830b89
Show file tree
Hide file tree
Showing 83 changed files with 95,173 additions and 695 deletions.
60 changes: 60 additions & 0 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
name: 'Test'
on:
pull_request:
branches: [ "master" ]
push:
branches: [ "master" ]
workflow_dispatch:
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

env:
CARGO_TERM_COLOR: always

jobs:

integration-tests:
name: "Integration tests"
runs-on: [self-hosted, linux, normal]
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
# Check out pull request HEAD instead of merge commit.
ref: ${{ github.event.pull_request.head.sha }}
submodules: recursive

- name: "Set up nightly Rust" # https://github.com/rust-lang/rustup/issues/3409
uses: dtolnay/rust-toolchain@master
with:
toolchain: nightly-2024-08-28

- name: 'Set up tree for rust dependency'
run: make setup

- name: 'Cache smir_pretty and rustc'
uses: Swatinem/rust-cache@v2
with:
workspaces: |
.
deps/rust/src
cache-directories: |
target
deps/rust/src/build
deps/rust/src/target
- name: 'Build smir_pretty and its rustc dependency'
run: | # rustc bootstrap checks this and refuses stage 1 in "CI"
export GITHUB_ACTIONS="in denial" && \
echo "GITHUB_ACTIONS = ${GITHUB_ACTIONS}" && \
make build_all
- name: 'Run smir integration tests'
run: |
make integration-test
- name: 'Clean up toolchain'
if: always()
run: |
make rustup-clear-toolchain
4 changes: 2 additions & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

53 changes: 48 additions & 5 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,27 @@ RUST_LIB_DIR=${RUST_INSTALL_DIR}/lib
RUST_DEP_DIR=${RUST_BUILD_DIR}/stage1-rustc/${RUST_ARCH}/release/deps
TARGET_DEP_DIR=${CURDIR}/target/${TARGET}/deps
TEMP_DIR=${RUST_DIR}/temp
RUST_REPO=https://github.com/runtimeverification/rust
RUST_BRANCH=smir_serde_derive_intern_scripts
TOOLCHAIN_NAME=smir_serde_derive_intern_scripts
#############################################
# depend on the rust compiler
RUST_REPO=https://github.com/rust-lang/rust
# tip of the `beta` branch on 2025-01-14
RUST_BRANCH=beta
RUST_COMMIT=fe9b975
#############################################
TOOLCHAIN_NAME=smir_pretty
RELEASE_FLAG=
ifeq (${TARGET}, release)
RELEASE_FLAG=--release
endif

default: build

build_all: rust_build rust_set_toolchain build

setup: rust_clone

update: ${RUST_SRC}
cd "${RUST_SRC}"; git fetch origin; git reset --hard origin/${RUST_BRANCH}
cd "${RUST_SRC}"; git fetch origin; git checkout ${RUST_COMMIT}

build:
cargo build ${RELEASE_FLAG}
Expand All @@ -53,7 +60,9 @@ prebuild_clean: ${RUST_SRC}

# NOTE: a deeper clone depth is needed for the build process
rust_clone:
git clone --depth 70 --single-branch --branch "${RUST_BRANCH}" "${RUST_REPO}" "${RUST_SRC}"
git clone --depth 70 --single-branch --branch "${RUST_BRANCH}" "${RUST_REPO}" "${RUST_SRC}" && \
cd "${RUST_SRC}" && \
git checkout ${RUST_COMMIT}


# rust_build for linking against custom rustc is involved
Expand All @@ -79,8 +88,42 @@ rust_set_toolchain: ${RUST_LIB_DIR}
rustup override set "${TOOLCHAIN_NAME}"
echo ${STAGE} > ${STAGE_FILE}

.PHONY: rustup-clear-toolchain
rustup-clear-toolchain:
rustup override unset
rustup override unset --nonexistent
rustup toolchain uninstall "${TOOLCHAIN_NAME}"

generate_ui_tests:
mkdir -p "${RUST_DIR}"/tests
cd "${RUST_SRC}"; ./get_runpass.sh tests/ui > "${RUST_DIR}"/tests_ui_sources
-cd "${RUST_SRC}"; ./ui_compiletest.sh "${RUST_SRC}" "${RUST_DIR}"/tests/ui/upstream "${RUST_DIR}"/tests_ui_sources --pass check --force-rerun 2>&1 > "${RUST_DIR}"/tests_ui_upstream.log
-cd "${RUST_SRC}"; RUST_BIN="${PWD}"/run.sh ./ui_compiletest.sh "${RUST_SRC}" "${RUST_DIR}"/tests/ui/smir "${RUST_DIR}"/tests_ui_sources --pass check --force-rerun 2>&1 > "${RUST_DIR}"/tests_ui_smir.log

TESTDIR=$(CURDIR)/tests/integration/programs

.PHONY: integration-test
integration-test: TESTS ?= $(shell find $(TESTDIR) -type f -name "*.rs")
integration-test: SMIR ?= $(CURDIR)/run.sh -Z no-codegen
# override this to tweak how expectations are formatted
integration-test: NORMALIZE ?= jq -S -e -f $(TESTDIR)/../normalise-filter.jq
# override this to re-make golden files
integration-test: DIFF ?= | diff -
integration-test: build
errors=""; \
report() { echo "$$1: $$2"; errors="$$errors\n$$1: $$2"; }; \
for rust in ${TESTS}; do \
target=$${rust%.rs}.smir.json; \
dir=$$(dirname $${rust}); \
echo "$$rust"; \
${SMIR} --out-dir $${dir} $${rust} || report "$$rust" "Conversion failed"; \
[ -f $${target} ] \
&& ${NORMALIZE} $${target} ${DIFF} $${target}.expected \
&& rm $${target} \
|| report "$$rust" "Unexpected json output"; \
done; \
[ -z "$$errors" ] || (echo "===============\nFAILING TESTS:$$errors"; exit 1)


golden:
make integration-test DIFF=">"
3 changes: 0 additions & 3 deletions panic_example.rs

This file was deleted.

1 change: 1 addition & 0 deletions panic_example.rs
1 change: 0 additions & 1 deletion panic_example.smir.json

This file was deleted.

1 change: 1 addition & 0 deletions panic_example.smir.json
12 changes: 3 additions & 9 deletions src/driver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ extern crate rustc_smir;
extern crate rustc_session;
use rustc_middle::ty::TyCtxt;
use rustc_driver::Compilation;
use rustc_interface::{interface::Compiler, Queries};
use rustc_interface::interface::Compiler;
use rustc_smir::rustc_internal;

struct StableMirCallbacks {
Expand All @@ -35,16 +35,10 @@ impl rustc_driver::Callbacks for StableMirCallbacks {
fn after_analysis<'tcx>(
&mut self,
_compiler: &Compiler,
queries: &'tcx Queries<'tcx>,
tcx: TyCtxt<'tcx>,
) -> Compilation {

let _q = queries
.global_ctxt()
.unwrap()
.get_mut()
.enter(|tcx| {
let _ = rustc_internal::run(tcx, || (self.callback_fn)(tcx));
});
let _ = rustc_internal::run(tcx, || (self.callback_fn)(tcx));

Compilation::Continue
}
Expand Down
23 changes: 0 additions & 23 deletions src/kani_lib/LICENSE-MIT

This file was deleted.

Loading

0 comments on commit 1830b89

Please sign in to comment.