From d8db3b87acecc7e974e080ea05c342eba827298e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 5 Dec 2023 13:28:53 -0800 Subject: [PATCH 1/5] Fix StableMIR migration documentation (#2915) Rename the file to use '-' instead of `_` and add the new page to the index. Fixed version can be seen here: https://celinval.github.io/kani-dev/stable-mir.html --- docs/src/SUMMARY.md | 1 + docs/src/dev-documentation.md | 2 +- docs/src/{stable_mir.md => stable-mir.md} | 0 3 files changed, 2 insertions(+), 1 deletion(-) rename docs/src/{stable_mir.md => stable-mir.md} (100%) diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index d4609a87c23b..69be21a07ff5 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -26,6 +26,7 @@ - [Coding conventions](./conventions.md) - [Working with CBMC](./cbmc-hacks.md) - [Working with `rustc`](./rustc-hacks.md) + - [Migrating to StableMIR](./stable-mir.md) - [Command cheat sheets](./cheat-sheets.md) - [cargo kani assess](./dev-assess.md) - [Testing](./testing.md) diff --git a/docs/src/dev-documentation.md b/docs/src/dev-documentation.md index 173588586a3a..c3fe857cf0b6 100644 --- a/docs/src/dev-documentation.md +++ b/docs/src/dev-documentation.md @@ -14,7 +14,7 @@ developers (including external contributors): 3. [Development setup recommendations for working with `cbmc`](./cbmc-hacks.md). 4. [Development setup recommendations for working with `rustc`](./rustc-hacks.md). 5. [Guide for testing in Kani](./testing.md). - 6. [Transition to StableMIR](./stable_mir.md). + 6. [Transition to StableMIR](./stable-mir.md). > **NOTE**: The developer documentation is intended for Kani developers and not users. At present, the project is under heavy development and some items diff --git a/docs/src/stable_mir.md b/docs/src/stable-mir.md similarity index 100% rename from docs/src/stable_mir.md rename to docs/src/stable-mir.md From c59c557c1b8e1a6b65b44aa2cea770e8e2fa0866 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Thu, 7 Dec 2023 15:44:40 +0100 Subject: [PATCH 2/5] Bump actions/labeler from 4 to 5 (#2917) Bumps [actions/labeler](https://github.com/actions/labeler) from 4 to 5. --- .github/workflows/extra_jobs.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml index d4da80fbe132..ea7508776f19 100644 --- a/.github/workflows/extra_jobs.yml +++ b/.github/workflows/extra_jobs.yml @@ -37,7 +37,7 @@ jobs: - name: Label PR id: labeler - uses: actions/labeler@v4 + uses: actions/labeler@v5 with: dot: true From b7968026573b2b142ac137ac739bcef8162686ec Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Dec 2023 21:11:20 +0100 Subject: [PATCH 3/5] Revert "Bump actions/labeler from 4 to 5 (#2917)" (#2923) This reverts commit c59c557c1b8e1a6b65b44aa2cea770e8e2fa0866. See #2922. --- .github/workflows/extra_jobs.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml index ea7508776f19..d4da80fbe132 100644 --- a/.github/workflows/extra_jobs.yml +++ b/.github/workflows/extra_jobs.yml @@ -37,7 +37,7 @@ jobs: - name: Label PR id: labeler - uses: actions/labeler@v5 + uses: actions/labeler@v4 with: dot: true From 2aca488ba9d64d2aaeae3b7774acf367bea42be9 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Thu, 7 Dec 2023 23:09:48 +0100 Subject: [PATCH 4/5] Bump docker/build-push-action from 3 to 5 (#2921) Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 3 to 5. --- .github/workflows/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 74af1c0be544..5a37f5e5c03e 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -284,7 +284,7 @@ jobs: OWNER: '${{ github.repository_owner }}' - name: Build and push - uses: docker/build-push-action@v3 + uses: docker/build-push-action@v5 with: context: . file: scripts/ci/Dockerfile.bundle-release-20-04 From 01bf411b514836a25dc5a2f44b6b0cfbaeacfc36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=C4=9Fuz=20A=C4=9Fcayaz=C4=B1?= Date: Fri, 8 Dec 2023 05:10:08 +0300 Subject: [PATCH 5/5] Stabilize `find_debug_info` (#2912) Last time we stabilized https://github.com/model-checking/kani/pull/2882, this continues the trend and stabilizes `find_debug_info` as well. --- .../src/codegen_cprover_gotoc/codegen/span.rs | 15 +++++++++------ .../src/codegen_cprover_gotoc/utils/names.rs | 2 +- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 9f88bbbe7b55..3fbfd3629775 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -5,9 +5,10 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; -use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents}; +use rustc_middle::mir::{Local, VarDebugInfoContents}; use rustc_smir::rustc_internal; use rustc_span::Span; +use stable_mir::mir::VarDebugInfo; impl<'tcx> GotocCtx<'tcx> { pub fn codegen_span(&self, sp: &Span) -> Location { @@ -43,10 +44,12 @@ impl<'tcx> GotocCtx<'tcx> { sp.map_or(Location::none(), |x| self.codegen_span(&x)) } - pub fn find_debug_info(&self, l: &Local) -> Option<&VarDebugInfo<'tcx>> { - self.current_fn().mir().var_debug_info.iter().find(|info| match info.value { - VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0, - VarDebugInfoContents::Const(_) => false, - }) + pub fn find_debug_info(&self, l: &Local) -> Option { + rustc_internal::stable(self.current_fn().mir().var_debug_info.iter().find(|info| { + match info.value { + VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0, + VarDebugInfoContents::Const(_) => false, + } + })) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index 98f6f533cd12..da684b601668 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -22,7 +22,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_var_base_name(&self, l: &Local) -> String { match self.find_debug_info(l) { None => format!("var_{}", l.index()), - Some(info) => format!("{}", info.name), + Some(info) => info.name, } }