Rebase

model-checking · Oct 27, 2023 · 0e75fee · 0e75fee
1 parent 6fd3970
commit 0e75fee
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 12 deletions.
diff --git 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
@@ -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!(),
         }
     }