From dd0e36bbedff6f0b628ba287f0fc95d9541ffb90 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Fri, 13 Oct 2023 09:43:56 -0700
Subject: [PATCH] Rebase

---
 .../src/codegen_boogie/compiler_interface.rs        |  8 ++------
 .../src/codegen_boogie/context/boogie_ctx.rs        | 13 +++++++------
 2 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/kani-compiler/src/codegen_boogie/compiler_interface.rs b/kani-compiler/src/codegen_boogie/compiler_interface.rs
index 1aab1d7249c1..d7487998562c 100644
--- a/kani-compiler/src/codegen_boogie/compiler_interface.rs
+++ b/kani-compiler/src/codegen_boogie/compiler_interface.rs
@@ -32,8 +32,8 @@ use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::mir::mono::MonoItem;
-use rustc_middle::query::{ExternProviders, Providers};
 use rustc_middle::ty::TyCtxt;
+use rustc_middle::util::Providers;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::cstore::MetadataLoaderDyn;
 use rustc_session::output::out_filename;
@@ -189,10 +189,6 @@ impl CodegenBackend for BoogieCodegenBackend {
         provide::provide(providers, &self.queries.lock().unwrap());
     }
 
-    fn provide_extern(&self, providers: &mut ExternProviders) {
-        provide::provide_extern(providers, &self.queries.lock().unwrap());
-    }
-
     fn print_version(&self) {
         println!("Kani-boogie version: {}", env!("CARGO_PKG_VERSION"));
     }
@@ -265,7 +261,7 @@ impl CodegenBackend for BoogieCodegenBackend {
                         if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
                     let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
                     let test_model_path = &metadata.goto_file.as_ref().unwrap();
-                    std::fs::copy(&model_path, &test_model_path).expect(&format!(
+                    std::fs::copy(&model_path, test_model_path).expect(&format!(
                         "Failed to copy {} to {}",
                         model_path.display(),
                         test_model_path.display()
diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
index fd767743dd63..32c947ee8297 100644
--- a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
+++ b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs
@@ -5,11 +5,12 @@ use std::io::Write;
 
 use crate::kani_queries::QueryDb;
 use boogie_ast::boogie_program::{BinaryOp, BoogieProgram, Expr, Literal, Procedure, Stmt, Type};
-use rustc_middle::mir::interpret::{ConstValue, Scalar};
+use rustc_middle::mir::interpret::Scalar;
 use rustc_middle::mir::traversal::reverse_postorder;
 use rustc_middle::mir::{
-    BasicBlock, BasicBlockData, BinOp, Constant, ConstantKind, HasLocalDecls, Local, LocalDecls,
-    Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
+    BasicBlock, BasicBlockData, BinOp, Const as mirConst, ConstOperand, ConstValue, HasLocalDecls,
+    Local, LocalDecls, Operand, Place, Rvalue, Statement, StatementKind, Terminator,
+    TerminatorKind,
 };
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
@@ -279,11 +280,11 @@ impl<'tcx> BoogieCtx<'tcx> {
         Expr::Symbol { name: format!("{local:?}") }
     }
 
-    fn codegen_constant(&self, c: &Constant<'tcx>) -> Expr {
+    fn codegen_constant(&self, c: &ConstOperand<'tcx>) -> Expr {
         trace!(constant=?c, "codegen_constant");
         // TODO: monomorphize
-        match c.literal {
-            ConstantKind::Val(val, ty) => self.codegen_constant_value(val, ty),
+        match c.const_ {
+            mirConst::Val(val, ty) => self.codegen_constant_value(val, ty),
             _ => todo!(),
         }
     }