adding an expected test for trait

model-checking · Jan 3, 2025 · f336b0a · f336b0a
1 parent f585369
commit f336b0a
Show file tree

Hide file tree

Showing 3 changed files with 98 additions and 9 deletions.
diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
@@ -284,7 +284,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let tid = match self.id_map.get(&def_id) {
             Some(tid) => *tid,
             None => {
-                debug!("***Not found!");
+                debug!("***Not found fun_decl_id!");
                 let tid = CharonAnyTransId::Fun(self.translated.fun_decls.reserve_slot());
                 self.id_map.insert(def_id, tid);
                 self.translated.all_ids.insert(tid);
@@ -300,7 +300,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let tid = match self.id_map.get(&def_id) {
             Some(tid) => *tid,
             None => {
-                debug!("***Not found!");
+                debug!("***Not found type_decl_id!");
                 let tid = CharonAnyTransId::Type(self.translated.type_decls.reserve_slot());
                 self.id_map.insert(def_id, tid);
                 self.translated.all_ids.insert(tid);
@@ -316,7 +316,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let tid = match self.id_map.get(&def_id) {
             Some(tid) => *tid,
             None => {
-                debug!("***Not found!");
+                debug!("***Not found trait_decl_id!");
                 let tid = CharonAnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot());
                 self.id_map.insert(def_id, tid);
                 self.translated.all_ids.insert(tid);
@@ -332,7 +332,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let tid = match self.id_map.get(&def_id) {
             Some(tid) => *tid,
             None => {
-                debug!("***Not found!");
+                debug!("***Not found trait_impl_id!");
                 let tid = CharonAnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot());
                 self.id_map.insert(def_id, tid);
                 self.translated.all_ids.insert(tid);
@@ -348,7 +348,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let tid = match self.id_map.get(&def_id) {
             Some(tid) => *tid,
             None => {
-                debug!("***Not found!");
+                debug!("***Not found global_decl_id!");
                 let tid = CharonAnyTransId::Global(self.translated.global_decls.reserve_slot());
                 self.id_map.insert(def_id, tid);
                 self.translated.all_ids.insert(tid);
@@ -750,7 +750,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let name = self.def_to_name(func_def).unwrap();
         let crate_name = match name.name.first().unwrap() {
             CharonPathElem::Ident(cn, _) => cn,
-            _ => panic!("Imple name"),
+            _ => panic!("Expected function name"),
         };
         crate_name.starts_with("std")
             || crate_name.starts_with("core")
@@ -761,11 +761,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         let name = self.defid_to_name(traitdef.def_id()).unwrap();
         let crate_name = match name.name.first().unwrap() {
             CharonPathElem::Ident(cn, _) => cn,
-            _ => panic!("Imple name"),
+            _ => panic!("Expected crate name"),
         };
         let marker = match name.name.get(1).unwrap() {
             CharonPathElem::Ident(cn, _) => cn,
-            _ => panic!("Imple name"),
+            _ => panic!("Expected trait name"),
         };
         crate_name.starts_with("core") && marker.starts_with("marker")
     }
@@ -1892,7 +1892,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             RegionKind::ReErased => CharonRegion::Erased,
             RegionKind::ReEarlyParam(epr) => {
                 let debr = CharonDeBruijnVar::bound(
-                    CharonDeBruijnId { index: 0 as usize },
+                    CharonDeBruijnId { index: 0_usize },
                     CharonRegionId::from_usize(epr.index as usize),
                 );
                 CharonRegion::Var(debr)

diff --git a/tests/expected/llbc/traitimpl/expected b/tests/expected/llbc/traitimpl/expected
@@ -0,0 +1,53 @@
+struct main::B =
+{
+  index: i32,
+}
+
+fn main::get_valB<'_0>(@1: &'_0 (@Adt0)) -> i32
+{
+    let @0: i32; // return
+    let self@1: &'_ (@Adt0); // arg #1
+
+    @0 := copy ((*(self@1)).index)
+    return
+}
+
+struct main::A =
+{
+  val: i32,
+}
+
+fn main::get_valA<'_0>(@1: &'_0 (@Adt1)) -> i32
+{
+    let @0: i32; // return
+    let self@1: &'_ (@Adt1); // arg #1
+
+    @0 := copy ((*(self@1)).val)
+    return
+}
+
+fn main::main()
+{
+    let @0: (); // return
+    let e@1: @Adt1; // local
+    let k@2: @Adt0; // local
+    let i@3: i32; // local
+    let @4: &'_ (@Adt1); // anonymous local
+    let j@5: i32; // local
+    let @6: &'_ (@Adt0); // anonymous local
+
+    e@1 := @Adt1 { val: const (3 : i32) }
+    k@2 := @Adt0 { index: const (3 : i32) }
+    @4 := &e@1
+    i@3 := @Fun2(move (@4))
+    drop @4
+    @6 := &k@2
+    j@5 := @Fun0(move (@6))
+    drop @6
+    drop j@5
+    drop i@3
+    drop k@2
+    drop e@1
+    @0 := ()
+    return
+}
diff --git a/tests/expected/llbc/traitimpl/test.rs b/tests/expected/llbc/traitimpl/test.rs
@@ -0,0 +1,36 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zlean --print-llbc
+
+//! This test checks that Kani's LLBC backend handles simple trait impl
+
+trait T {
+    fn get_val(&self) -> i32;
+}
+struct A {
+    val: i32,
+}
+
+struct B {
+    index: i32,
+}
+
+impl T for A {
+    fn get_val(&self) -> i32 {
+        self.val
+    }
+}
+
+impl T for B {
+    fn get_val(&self) -> i32 {
+        self.index
+    }
+}
+
+#[kani::proof]
+fn main() {
+    let e = A { val: 3 };
+    let k = B { index: 3 };
+    let i = e.get_val();
+    let j = k.get_val();
+}