Finish migration of compiler-interface

celinval · celinval · commit b672e9b94b04 · 2023-12-19T16:21:42.000-08:00
diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
@@ -446,7 +446,14 @@ mod tests {
     use rustc_hir::definitions::DefPathHash;
     use std::collections::HashMap;
 
-    fn mock_next_id() -> HarnessId {
+    fn mock_next_harness() -> HarnessId {
+        static mut COUNTER: u64 = 0;
+        unsafe { COUNTER += 1 };
+        let id = unsafe { COUNTER };
+        format!("mod::harness-{id}").intern()
+    }
+
+    fn mock_next_stub() -> DefPathHash {
         static mut COUNTER: u64 = 0;
         unsafe { COUNTER += 1 };
         let id = unsafe { COUNTER };
@@ -473,15 +480,15 @@ mod tests {
     #[test]
     fn test_group_by_stubs_works() {
         // Set up the inputs
-        let harness_1 = mock_next_id();
-        let harness_2 = mock_next_id();
-        let harness_3 = mock_next_id();
+        let harness_1 = mock_next_harness();
+        let harness_2 = mock_next_harness();
+        let harness_3 = mock_next_harness();
         let harnesses = vec![harness_1, harness_2, harness_3];
 
-        let stub_1 = (mock_next_id(), mock_next_id());
-        let stub_2 = (mock_next_id(), mock_next_id());
-        let stub_3 = (mock_next_id(), mock_next_id());
-        let stub_4 = (stub_3.0, mock_next_id());
+        let stub_1 = (mock_next_stub(), mock_next_stub());
+        let stub_2 = (mock_next_stub(), mock_next_stub());
+        let stub_3 = (mock_next_stub(), mock_next_stub());
+        let stub_4 = (stub_3.0, mock_next_stub());
 
         let set_1 = Stubs::from([stub_1, stub_2, stub_3]);
         let set_2 = Stubs::from([stub_1, stub_2, stub_4]);
@@ -516,7 +523,7 @@ mod tests {
 
         let mut info = mock_info_with_stubs(Stubs::default());
         info.metadata.attributes.proof = true;
-        let id = mock_next_id();
+        let id = mock_next_harness();
         let all_harnesses = HashMap::from([(id, info.clone())]);
 
         // Call generate metadata.
@@ -553,7 +560,7 @@ mod tests {
         let infos = harnesses.map(|harness| {
             let mut metadata = mock_metadata(harness.to_string(), krate.clone());
             metadata.attributes.proof = true;
-            (mock_next_id(), HarnessInfo { stub_map: Stubs::default(), metadata })
+            (mock_next_harness(), HarnessInfo { stub_map: Stubs::default(), metadata })
         });
         let all_harnesses = HashMap::from(infos.clone());
 
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
@@ -23,7 +23,9 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
     let mangled_name =
         if pretty_name == "main" { pretty_name.clone() } else { instance.mangled_name() };
 
-    let loc = SourceLocation::new(&instance.def.span());
+    // We get the body span to include the entire function definition.
+    // This is required for concrete playback to properly position the generated test.
+    let loc = SourceLocation::new(instance.body().unwrap().span);
     let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
     let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto);
 
@@ -50,7 +52,7 @@ pub fn gen_test_metadata(
 ) -> HarnessMetadata {
     let pretty_name = test_harness_name(tcx, &test_desc);
     let mangled_name = test_fn.mangled_name();
-    let loc = SourceLocation::new(&test_desc.span());
+    let loc = SourceLocation::new(test_desc.span());
     let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
     let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto);
 
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
@@ -14,15 +14,17 @@ use rustc_middle::ty::layout::{
     FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError,
     LayoutOfHelpers, TyAndLayout,
 };
-use rustc_middle::ty::{self, Instance as InstanceInternal, Ty, TyCtxt};
+use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt};
 use rustc_session::config::OutputType;
 use rustc_smir::rustc_internal;
 use rustc_span::source_map::respan;
 use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem};
-use stable_mir::ty::{BoundVariableKind, Span as SpanStable};
+use stable_mir::mir::pretty::pretty_ty;
+use stable_mir::ty::{BoundVariableKind, RigidTy, Span as SpanStable, Ty, TyKind};
+use stable_mir::visitor::{Visitable, Visitor as TypeVisitor};
 use stable_mir::{CrateDef, DefId};
 use std::fs::File;
 use std::io::BufWriter;
@@ -104,10 +106,9 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
 /// This is a temporary safety measure because contracts cannot yet reason
 /// about the heap.
 fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
-    use ty::TypeVisitor;
     struct NoMutPtr<'tcx> {
         tcx: TyCtxt<'tcx>,
-        is_prohibited: fn(ty::Ty<'tcx>) -> bool,
+        is_prohibited: fn(Ty) -> bool,
         /// Where (top level) did the type we're analyzing come from. Used for
         /// composing error messages.
         r#where: &'static str,
@@ -116,14 +117,15 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
         what: &'static str,
     }
 
-    impl<'tcx> TypeVisitor<TyCtxt<'tcx>> for NoMutPtr<'tcx> {
-        fn visit_ty(&mut self, t: ty::Ty<'tcx>) -> std::ops::ControlFlow<Self::BreakTy> {
-            use ty::TypeSuperVisitable;
-            if (self.is_prohibited)(t) {
+    impl<'tcx> TypeVisitor for NoMutPtr<'tcx> {
+        type Break = ();
+        fn visit_ty(&mut self, ty: &Ty) -> std::ops::ControlFlow<Self::Break> {
+            if (self.is_prohibited)(*ty) {
                 // TODO make this more user friendly
                 self.tcx.sess.err(format!(
-                    "{} contains a {}pointer ({t:?}). This is prohibited for functions with contracts, \
-                    as they cannot yet reason about the pointer behavior.", self.r#where, self.what));
+                    "{} contains a {}pointer ({}). This is prohibited for functions with contracts, \
+                    as they cannot yet reason about the pointer behavior.", self.r#where, self.what,
+                    pretty_ty(ty.kind())));
             }
 
             // Rust's type visitor only recurses into type arguments, (e.g.
@@ -134,28 +136,28 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
             // Since the field types also must contain in some form all the type
             // arguments the visitor will see them as it inspects the fields and
             // we don't need to call back to `super`.
-            if let ty::TyKind::Adt(adt_def, generics) = t.kind() {
+            if let TyKind::RigidTy(RigidTy::Adt(adt_def, generics)) = ty.kind() {
                 for variant in adt_def.variants() {
-                    for field in &variant.fields {
-                        let ctrl = self.visit_ty(field.ty(self.tcx, generics));
-                        if ctrl.is_break() {
-                            // Technically we can just ignore this because we
-                            // know this case will never happen, but just to be
-                            // safe.
-                            return ctrl;
-                        }
+                    for field in &variant.fields() {
+                        self.visit_ty(&field.ty_with_args(&generics))?;
                     }
                 }
                 std::ops::ControlFlow::Continue(())
             } else {
                 // For every other type.
-                t.super_visit_with(self)
+                ty.super_visit(self)
             }
         }
     }
 
-    fn is_raw_mutable_ptr(t: ty::Ty) -> bool {
-        matches!(t.kind(), ty::TyKind::RawPtr(tmut) if tmut.mutbl == rustc_ast::Mutability::Mut)
+    fn is_raw_mutable_ptr(ty: Ty) -> bool {
+        let kind = ty.kind();
+        kind.is_raw_ptr() && kind.is_mutable_ptr()
+    }
+
+    fn is_raw_ptr(ty: Ty) -> bool {
+        let kind = ty.kind();
+        kind.is_raw_ptr()
     }
 
     // TODO: Replace this with fn_abi.
@@ -173,15 +175,15 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
 
     let fn_typ = bound_fn_sig.skip_binder();
 
-    for (typ, (is_prohibited, r#where, what)) in fn_typ
+    for (input_ty, (is_prohibited, r#where, what)) in fn_typ
         .inputs()
         .iter()
         .copied()
         .zip(std::iter::repeat((is_raw_mutable_ptr as fn(_) -> _, "This argument", "mutable ")))
-        .chain([(fn_typ.output(), (ty::Ty::is_unsafe_ptr as fn(_) -> _, "The return", ""))])
+        .chain([(fn_typ.output(), (is_raw_ptr as fn(_) -> _, "The return", ""))])
     {
         let mut v = NoMutPtr { tcx, is_prohibited, r#where, what };
-        v.visit_ty(rustc_internal::internal(typ));
+        v.visit_ty(&input_ty);
     }
 }
 
@@ -226,7 +228,7 @@ pub struct SourceLocation {
 }
 
 impl SourceLocation {
-    pub fn new(span: &SpanStable) -> Self {
+    pub fn new(span: SpanStable) -> Self {
         let loc = span.get_lines();
         let filename = span.get_filename().to_string();
         let start_line = loc.start_line;
@@ -243,7 +245,7 @@ impl SourceLocation {
 pub fn fn_abi<'tcx>(
     tcx: TyCtxt<'tcx>,
     instance: InstanceInternal<'tcx>,
-) -> &'tcx FnAbi<'tcx, Ty<'tcx>> {
+) -> &'tcx FnAbi<'tcx, TyInternal<'tcx>> {
     let helper = CompilerHelpers { tcx };
     helper.fn_abi_of_instance(instance, ty::List::empty())
 }
@@ -274,14 +276,14 @@ impl<'tcx> LayoutOfHelpers<'tcx> for CompilerHelpers<'tcx> {
     type LayoutOfResult = TyAndLayout<'tcx>;
 
     #[inline]
-    fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: Ty<'tcx>) -> ! {
+    fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: TyInternal<'tcx>) -> ! {
         span_bug!(span, "failed to get layout for `{}`: {}", ty, err)
     }
 }
 
 /// Implement error handling for extracting function ABI information.
 impl<'tcx> FnAbiOfHelpers<'tcx> for CompilerHelpers<'tcx> {
-    type FnAbiOfResult = &'tcx FnAbi<'tcx, Ty<'tcx>>;
+    type FnAbiOfResult = &'tcx FnAbi<'tcx, TyInternal<'tcx>>;
 
     #[inline]
     fn handle_fn_abi_err(
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
@@ -31,8 +31,8 @@ use stable_mir::mir::{
     TerminatorKind,
 };
 use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
-use stable_mir::CrateDef;
 use stable_mir::{self, CrateItem};
+use stable_mir::{CrateDef, ItemKind};
 
 use crate::kani_middle::coercion;
 use crate::kani_middle::coercion::CoercionBase;
@@ -73,10 +73,19 @@ where
     crate_items
         .iter()
         .filter_map(|item| {
+            tracing::warn!(?item, name = item.name(), "crate_item");
+            tracing::warn!(body=?item.body().blocks.len(), "crate_item");
             // Only collect monomorphic items.
-            Instance::try_from(*item)
-                .ok()
-                .and_then(|instance| predicate(tcx, instance).then_some(instance))
+            // TODO: Remove the def_kind check once https://github.com/rust-lang/rust/pull/119135 has been released.
+            let def_id = rustc_internal::internal(item.def_id());
+            (matches!(tcx.def_kind(def_id), rustc_hir::def::DefKind::Ctor(..))
+                || matches!(item.kind(), ItemKind::Fn))
+            .then(|| {
+                Instance::try_from(*item)
+                    .ok()
+                    .and_then(|instance| predicate(tcx, instance).then_some(instance))
+            })
+            .flatten()
         })
         .collect::<Vec<_>>()
 }
diff --git a/tests/cargo-kani/assess-workspace-artifacts/expected b/tests/cargo-kani/assess-workspace-artifacts/expected
@@ -11,10 +11,10 @@ Analyzed 2 packages
  unsupported_construct |               3
  none (success)        |               3
 =========================================
-=======================================================================================================================
+=================================================
  Candidate for proof harness          | Location
---------------------------------------+--------------------------------------------------------------------------------
+--------------------------------------+----------
  a_supported_test_from_tests          |
  a_supported_test_from_the_lib        |
  a_supported_test_from_the_subpackage |
-=======================================================================================================================
+==================================================
