Merge branch 'main' into toolchain-2023-12-09

.github/workflows/audit.yml

@@ -16,7 +16,7 @@ jobs:
   audit:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: EmbarkStudios/cargo-deny-action@v1
         with:
           arguments: --all-features --workspace

.github/workflows/bench.yml

@@ -30,14 +30,14 @@ jobs:
           echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
 
       - name: Check out Kani (old variant)
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: ./old
           ref: ${{ env.OLD_REF }}
           fetch-depth: 2
 
       - name: Check out Kani (new variant)
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: ./new
           ref: ${{ env.NEW_REF }}

.github/workflows/cbmc-latest.yml

@@ -22,7 +22,7 @@ jobs:
         os: [macos-12, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani under "kani"
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: kani
 
@@ -37,7 +37,7 @@ jobs:
         run: cargo build-dev
 
       - name: Checkout CBMC under "cbmc"
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           repository: diffblue/cbmc
           path: cbmc
@@ -58,7 +58,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani under "kani"
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: kani
 
@@ -73,7 +73,7 @@ jobs:
         run: cargo build-dev -- --release
 
       - name: Checkout CBMC under "cbmc"
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           repository: diffblue/cbmc
           path: cbmc

.github/workflows/cbmc-update.yml

@@ -19,7 +19,7 @@ jobs:
     runs-on: ubuntu-22.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup

.github/workflows/extra_jobs.yml

@@ -33,7 +33,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout Kani
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
 
     - name: Label PR
       id: labeler

.github/workflows/format-check.yml

@@ -14,7 +14,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Execute copyright check
         run: ./scripts/ci/run-copyright-check.sh
@@ -33,7 +33,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup

.github/workflows/kani-m1.yml

@@ -16,7 +16,7 @@ jobs:
     runs-on: macos-13-xlarge
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup

.github/workflows/kani.yml

@@ -20,7 +20,7 @@ jobs:
         os: [macos-12, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
@@ -37,7 +37,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
@@ -58,7 +58,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Install benchcomp dependencies
         run: |
@@ -81,7 +81,7 @@ jobs:
     runs-on: ubuntu-20.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
@@ -102,7 +102,7 @@ jobs:
       contents: write
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup

.github/workflows/release.yml

@@ -30,7 +30,7 @@ jobs:
       crate_version: ${{ steps.bundle.outputs.crate_version }}
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup
@@ -135,7 +135,7 @@ jobs:
           cargo kani setup --use-local-bundle ./${{ matrix.prev_job.bundle }}
 
       - name: Checkout tests
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Run tests
         # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests.
@@ -160,7 +160,7 @@ jobs:
       KANI_SRC: ./kani_src
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           path: ${{ env.KANI_SRC }}
 
@@ -204,7 +204,7 @@ jobs:
       upload_url: ${{ steps.create_release.outputs.upload_url }}
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Get version
         run: |
@@ -235,7 +235,7 @@ jobs:
 
       - name: Create release
         id: create_release
-        uses: ncipollo/release-action@v1.12.0
+        uses: ncipollo/release-action@v1.13.0
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         with:
@@ -258,7 +258,7 @@ jobs:
       target: x86_64-unknown-linux-gnu
     steps:
       - name: Checkout code
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup

.github/workflows/slow-tests.yml

@@ -21,7 +21,7 @@ jobs:
         os: [macos-12, ubuntu-20.04, ubuntu-22.04]
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup

.github/workflows/toolchain-upgrade.yml

@@ -19,7 +19,7 @@ jobs:
     runs-on: ubuntu-22.04
     steps:
       - name: Checkout Kani
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup Kani Dependencies
         uses: ./.github/actions/setup

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -22,6 +22,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
 use rustc_span::Span;
+use stable_mir::ty::Span as SpanStable;
 use std::convert::AsRef;
 use strum_macros::{AsRefStr, EnumString};
 use tracing::debug;
@@ -138,8 +139,8 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Generate code to cover the given condition at the current location
-    pub fn codegen_cover(&self, cond: Expr, msg: &str, span: Option<Span>) -> Stmt {
-        let loc = self.codegen_caller_span(&span);
+    pub fn codegen_cover(&self, cond: Expr, msg: &str, span: SpanStable) -> Stmt {
+        let loc = self.codegen_caller_span_stable(span);
         // Should use Stmt::cover, but currently this doesn't work with CBMC
         // unless it is run with '--cover cover' (see
         // https://github.com/diffblue/cbmc/issues/6613). So for now use
@@ -172,12 +173,8 @@ impl<'tcx> GotocCtx<'tcx> {
     /// reachability check.
     /// If reachability checks are disabled, the function returns the message
     /// unmodified and an empty (skip) statement.
-    pub fn codegen_reachability_check(
-        &mut self,
-        msg: String,
-        span: Option<Span>,
-    ) -> (String, Stmt) {
-        let loc = self.codegen_caller_span(&span);
+    pub fn codegen_reachability_check(&mut self, msg: String, span: SpanStable) -> (String, Stmt) {
+        let loc = self.codegen_caller_span_stable(span);
         if self.queries.args().check_assertion_reachability {
             // Generate a unique ID for the assert
             let assert_id = self.next_check_id();
@@ -224,15 +221,16 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Kani hooks function calls to `panic` and calls this intead.
-    pub fn codegen_panic(&self, span: Option<Span>, fargs: Vec<Expr>) -> Stmt {
+    pub fn codegen_panic(&self, span: SpanStable, fargs: Vec<Expr>) -> Stmt {
         // CBMC requires that the argument to the assertion must be a string constant.
         // If there is one in the MIR, use it; otherwise, explain that we can't.
         assert!(!fargs.is_empty(), "Panic requires a string message");
         let msg = self.extract_const_message(&fargs[0]).unwrap_or(String::from(
             "This is a placeholder message; Kani doesn't support message formatted at runtime",
         ));
 
-        self.codegen_fatal_error(PropertyClass::Assertion, &msg, span)
+        let loc = self.codegen_caller_span_stable(span);
+        self.codegen_assert_assume_false(PropertyClass::Assertion, &msg, loc)
     }
 
     /// Kani does not currently support all MIR constructs.

kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs

@@ -3,8 +3,13 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use rustc_middle::mir::{BasicBlock, BasicBlockData};
+use stable_mir::mir::BasicBlockIdx;
 use tracing::debug;
 
+pub fn bb_label(bb: BasicBlockIdx) -> String {
+    format!("bb{bb}")
+}
+
 impl<'tcx> GotocCtx<'tcx> {
     /// Generates Goto-C for a basic block.
     ///
@@ -14,7 +19,6 @@ impl<'tcx> GotocCtx<'tcx> {
     /// `self.current_fn_mut().push_onto_block(...)`
     pub fn codegen_block(&mut self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) {
         debug!(?bb, "Codegen basicblock");
-        self.current_fn_mut().set_current_bb(bb);
         let label: String = self.current_fn().find_label(&bb);
         let check_coverage = self.queries.args().check_coverage;
         // the first statement should be labelled. if there is no statements, then the
@@ -67,6 +71,5 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.current_fn_mut().push_onto_block(tcode);
             }
         }
-        self.current_fn_mut().reset_current_bb();
     }
 }

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -28,7 +28,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// - Indices [1, N] represent the function parameters where N is the number of parameters.
     /// - Indices that are greater than N represent local variables.
     fn codegen_declare_variables(&mut self) {
-        let mir = self.current_fn().mir();
+        let mir = self.current_fn().body_internal();
         let ldecls = mir.local_decls();
         let num_args = self.get_params_size();
         ldecls.indices().enumerate().for_each(|(idx, lc)| {
@@ -76,7 +76,7 @@ impl<'tcx> GotocCtx<'tcx> {
             debug!("Double codegen of {:?}", old_sym);
         } else {
             assert!(old_sym.is_function());
-            let mir = self.current_fn().mir();
+            let mir = self.current_fn().body_internal();
             self.print_instance(instance, mir);
             self.codegen_function_prelude();
             self.codegen_declare_variables();
@@ -94,7 +94,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Codegen changes required due to the function ABI.
     /// We currently untuple arguments for RustCall ABI where the `spread_arg` is set.
     fn codegen_function_prelude(&mut self) {
-        let mir = self.current_fn().mir();
+        let mir = self.current_fn().body_internal();
         if let Some(spread_arg) = mir.spread_arg {
             self.codegen_spread_arg(mir, spread_arg);
         }
@@ -228,7 +228,7 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!(krate = self.current_fn().krate().as_str());
         debug!(is_std = self.current_fn().is_std());
         self.ensure(&self.current_fn().name(), |ctx, fname| {
-            let mir = ctx.current_fn().mir();
+            let mir = ctx.current_fn().body_internal();
             Symbol::function(
                 fname,
                 ctx.fn_typ(),

kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs

@@ -17,7 +17,9 @@ mod statement;
 mod static_var;
 
 // Visible for all codegen module.
+mod ty_stable;
 pub(super) mod typ;
 
 pub use assert::PropertyClass;
+pub use block::bb_label;
 pub use typ::TypeExt;

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -10,9 +10,13 @@ use rustc_middle::mir::interpret::{read_target_uint, AllocId, Allocation, Global
 use rustc_middle::mir::{Const as mirConst, ConstOperand, ConstValue, Operand, UnevaluatedConst};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uint, UintTy};
+use rustc_smir::rustc_internal;
 use rustc_span::def_id::DefId;
 use rustc_span::Span;
 use rustc_target::abi::{Size, TagEncoding, Variants};
+use stable_mir::mir::mono::Instance as InstanceStable;
+use stable_mir::ty::{FnDef, GenericArgs, Span as SpanStable};
+use stable_mir::CrateDef;
 use tracing::{debug, trace};
 
 enum AllocData<'a> {
@@ -702,6 +706,20 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_fn_item(instance, span)
     }
 
+    pub fn codegen_fndef_stable(
+        &mut self,
+        def: FnDef,
+        args: &GenericArgs,
+        span: Option<SpanStable>,
+    ) -> Expr {
+        let instance = InstanceStable::resolve(def, args)
+            .expect(&format!("Failed to instantiate `{}` with `{args:?}`", def.name()));
+        self.codegen_fn_item(
+            rustc_internal::internal(instance),
+            rustc_internal::internal(span).as_ref(),
+        )
+    }
+
     /// Ensure that the given instance is in the symbol table, returning the symbol.
     ///
     /// FIXME: The function should not have to return the type of the function symbol as well
@@ -735,6 +753,12 @@ impl<'tcx> GotocCtx<'tcx> {
             .with_location(self.codegen_span_option(span.cloned()))
     }
 
+    pub fn codegen_func_expr_stable(&mut self, instance: InstanceStable, span: SpanStable) -> Expr {
+        let (func_symbol, func_typ) = self.codegen_func_symbol(rustc_internal::internal(instance));
+        Expr::symbol_expression(func_symbol.name, func_typ)
+            .with_location(self.codegen_span_stable(span))
+    }
+
     /// Generate a goto expression referencing the singleton value for a MIR "function item".
     ///
     /// For a given function instance, generate a ZST struct and return a singleton reference to that.