Merge branch 'main' into toolchain-2023-12-03-manual

model-checking · Dec 8, 2023 · 0ed32e4 · 0ed32e4
2 parents 9be3d1f + 01bf411
commit 0ed32e4
Show file tree

Hide file tree

Showing 6 changed files with 13 additions and 9 deletions.
diff --git 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

diff --git 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
@@ -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 → docs/src/stable-mir.md b/docs/src/stable_mir.md → docs/src/stable-mir.md
diff --git 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<VarDebugInfo> {
+        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
@@ -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,
         }
     }