add support for enum, struct, tuple in llbc backend (#3721)

This pull request added some more features to Stable-mir to Ullbc
translation:
1. Added support for translation of enum, struct, tuple and the
projection associated with them.
2. Edited 3 Binops translation.
3. Added 4 simple tests for enum, struct, tuple and the projection .
4. If you had to perform any manual test, please describe them.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: thanhnguyen-aws

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -0,0 +1,36 @@
+enum test::MyEnum =
+|  A(0: i32)
+|  B()
+
+
+fn test::enum_match(@1: @Adt0) -> i32
+{
+    let @0: i32; // return
+    let e@1: @Adt0; // arg #1
+    let i@2: i32; // local
+
+    match e@1 {
+        0 => {
+            i@2 := copy ((e@1 as variant @0).0)
+            @0 := copy (i@2)
+            drop i@2
+        },
+        1 => {
+            @0 := const (0 : i32)
+        },
+    }
+    return
+}
+
+fn test::main()
+{
+    let @0: (); // return
+    let e@1: @Adt0; // local
+    let i@2: i32; // local
+
+    e@1 := test::MyEnum::A { 0: const (1 : i32) }
+    i@2 := @Fun0(move (e@1))
+    drop i@2
+    @0 := ()
+    return
+}

tests/expected/llbc/enum/expected

@@ -0,0 +1,23 @@
+// 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 enum
+
+enum MyEnum {
+    A(i32),
+    B,
+}
+
+fn enum_match(e: MyEnum) -> i32 {
+    match e {
+        MyEnum::A(i) => i,
+        MyEnum::B => 0,
+    }
+}
+
+#[kani::proof]
+fn main() {
+    let e = MyEnum::A(1);
+    let i = enum_match(e);
+}

tests/expected/llbc/enum/test.rs

@@ -0,0 +1,52 @@
+enum core::option::Option<T> =
+|  None()
+|  Some(0: T)
+
+
+fn test::add_opt(@1: @Adt0<i32>, @2: @Adt0<i32>) -> @Adt0<i32>
+{
+    let @0: @Adt0<i32>; // return
+    let x@1: @Adt0<i32>; // arg #1
+    let y@2: @Adt0<i32>; // arg #2
+    let u@3: i32; // local
+    let v@4: i32; // local
+    let @5: i32; // anonymous local
+
+    match x@1 {
+        1 => {
+            u@3 := copy ((x@1 as variant @1).0)
+            match y@2 {
+                1 => {
+                    v@4 := copy ((y@2 as variant @1).0)
+                    @5 := copy (u@3) + copy (v@4)
+                    @0 := core::option::Option::Some { 0: move (@5) }
+                    drop @5
+                },
+                0 => {
+                    @0 := core::option::Option::None {  }
+                },
+            }
+        },
+        0 => {
+            @0 := core::option::Option::None {  }
+        },
+    }
+    return
+}
+
+fn test::main()
+{
+    let @0: (); // return
+    let e@1: @Adt0<i32>; // local
+    let @2: @Adt0<i32>; // anonymous local
+    let @3: @Adt0<i32>; // anonymous local
+
+    @2 := core::option::Option::Some { 0: const (1 : i32) }
+    @3 := core::option::Option::Some { 0: const (2 : i32) }
+    e@1 := @Fun0(move (@2), move (@3))
+    drop @3
+    drop @2
+    drop e@1
+    @0 := ()
+    return
+}

tests/expected/llbc/generic/expected

@@ -0,0 +1,20 @@
+// 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 generic args for option
+
+fn add_opt(x: Option<i32>, y: Option<i32>) -> Option<i32> {
+    match x {
+        Some(u) => match y {
+            Some(v) => Some(u + v),
+            _ => None,
+        },
+        _ => None,
+    }
+}
+
+#[kani::proof]
+fn main() {
+    let e = add_opt(Some(1), Some(2));
+}

tests/expected/llbc/generic/test.rs

@@ -0,0 +1,84 @@
+struct test::MyStruct =
+{
+  a: i32,
+  b: i32,
+}
+
+enum test::MyEnum0 =
+|  A(0: @Adt1, 1: i32)
+|  B()
+
+
+enum test::MyEnum =
+|  A(0: @Adt1, 1: @Adt2)
+|  B(0: (i32, i32))
+
+
+fn test::enum_match(@1: @Adt0) -> i32
+{
+    let @0: i32; // return
+    let e@1: @Adt0; // arg #1
+    let s@2: @Adt1; // local
+    let e0@3: @Adt2; // local
+    let s1@4: @Adt1; // local
+    let b@5: i32; // local
+    let @6: i32; // anonymous local
+    let @7: i32; // anonymous local
+    let @8: i32; // anonymous local
+    let a@9: i32; // local
+    let b@10: i32; // local
+
+    match e@1 {
+        0 => {
+            s@2 := move ((e@1 as variant @0).0)
+            e0@3 := move ((e@1 as variant @0).1)
+            match e0@3 {
+                0 => {
+                    s1@4 := move ((e0@3 as variant @0).0)
+                    b@5 := copy ((e0@3 as variant @0).1)
+                    @6 := copy ((s1@4).a)
+                    @0 := copy (@6) + copy (b@5)
+                    drop @6
+                    drop s1@4
+                    drop e0@3
+                    drop s@2
+                },
+                1 => {
+                    @7 := copy ((s@2).a)
+                    @8 := copy ((s@2).b)
+                    @0 := copy (@7) + copy (@8)
+                    drop @8
+                    drop @7
+                    drop e0@3
+                    drop s@2
+                },
+            }
+        },
+        1 => {
+            a@9 := copy (((e@1 as variant @1).0).0)
+            b@10 := copy (((e@1 as variant @1).0).1)
+            @0 := copy (a@9) + copy (b@10)
+        },
+    }
+    return
+}
+
+fn test::main()
+{
+    let @0: (); // return
+    let s@1: @Adt1; // local
+    let s0@2: @Adt1; // local
+    let e@3: @Adt0; // local
+    let @4: @Adt2; // anonymous local
+    let i@5: i32; // local
+
+    s@1 := @Adt1 { a: const (1 : i32), b: const (2 : i32) }
+    s0@2 := @Adt1 { a: const (1 : i32), b: const (2 : i32) }
+    @4 := test::MyEnum0::A { 0: move (s0@2), 1: const (1 : i32) }
+    e@3 := test::MyEnum::A { 0: move (s@1), 1: move (@4) }
+    drop @4
+    i@5 := @Fun0(move (e@3))
+    drop i@5
+    @0 := ()
+    return
+}

tests/expected/llbc/projection/expected

@@ -0,0 +1,38 @@
+// 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 projection
+
+struct MyStruct {
+    a: i32,
+    b: i32,
+}
+
+enum MyEnum0 {
+    A(MyStruct, i32),
+    B,
+}
+
+enum MyEnum {
+    A(MyStruct, MyEnum0),
+    B((i32, i32)),
+}
+
+fn enum_match(e: MyEnum) -> i32 {
+    match e {
+        MyEnum::A(s, e0) => match e0 {
+            MyEnum0::A(s1, b) => s1.a + b,
+            MyEnum0::B => s.a + s.b,
+        },
+        MyEnum::B((a, b)) => a + b,
+    }
+}
+
+#[kani::proof]
+fn main() {
+    let s = MyStruct { a: 1, b: 2 };
+    let s0 = MyStruct { a: 1, b: 2 };
+    let e = MyEnum::A(s, MyEnum0::A(s0, 1));
+    let i = enum_match(e);
+}

tests/expected/llbc/projection/test.rs

@@ -0,0 +1,27 @@
+struct test::MyStruct =
+{
+  a: i32,
+  b: bool,
+}
+
+fn test::struct_project(@1: @Adt0) -> i32
+{
+    let @0: i32; // return
+    let s@1: @Adt0; // arg #1
+
+    @0 := copy ((s@1).a)
+    return
+}
+
+fn test::main()
+{
+    let @0: (); // return
+    let s@1: @Adt0; // local
+    let a@2: i32; // local
+
+    s@1 := @Adt0 { a: const (1 : i32), b: const (true) }
+    a@2 := @Fun1(move (s@1))
+    drop a@2
+    @0 := ()
+    return
+}

tests/expected/llbc/struct/expected

@@ -0,0 +1,20 @@
+// 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 struct
+
+struct MyStruct {
+    a: i32,
+    b: bool,
+}
+
+fn struct_project(s: MyStruct) -> i32 {
+    s.a
+}
+
+#[kani::proof]
+fn main() {
+    let s = MyStruct { a: 1, b: true };
+    let a = struct_project(s);
+}

tests/expected/llbc/struct/test.rs

@@ -0,0 +1,28 @@
+fn test::tuple_add(@1: (i32, i32)) -> i32
+{
+    let @0: i32; // return
+    let t@1: (i32, i32); // arg #1
+    let @2: i32; // anonymous local
+    let @3: i32; // anonymous local
+
+    @2 := copy ((t@1).0)
+    @3 := copy ((t@1).1)
+    @0 := copy (@2) + copy (@3)
+    drop @3
+    drop @2
+    return
+}
+
+fn test::main()
+{
+    let @0: (); // return
+    let s@1: i32; // local
+    let @2: (i32, i32); // anonymous local
+
+    @2 := (const (1 : i32), const (2 : i32))
+    s@1 := @Fun1(move (@2))
+    drop @2
+    drop s@1
+    @0 := ()
+    return
+}