add support for enum, struct, tuple in llbc backend

tests/expected/llbc/basic0/TestRNvCshcvyQEKZjUj4test4main.symtab.lean

@@ -0,0 +1,24 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::tuple_fn]:
+   Source: 'test.rs', lines 38:1-38:33 -/
+def tuple_fn (t : (I32 × I32)) : Result I32 :=
+  let (i, i1) := t
+  i + i1
+
+/- [test::main]:
+   Source: 'test.rs', lines 43:1-43:10 -/
+def main : Result Unit :=
+  do
+  let _ ← tuple_fn (1#i32, 2#i32)
+  Result.ok ()
+
+end test

tests/expected/llbc/basic0/expected

@@ -5,4 +5,4 @@ fn test::is_zero(@1: i32) -> bool\
 
     @0 := copy (i@1) == const (0 : i32)\
     return\
-}
+}

tests/expected/llbc/basic1/TestRNvCshcvyQEKZjUj4test4main.symtab.lean

@@ -0,0 +1,25 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::select]:
+   Source: 'test.rs', lines 8:1-8:42 -/
+def select (s : Bool) (x : I32) (y : I32) : Result I32 :=
+  if s
+  then Result.ok x
+  else Result.ok y
+
+/- [test::main]:
+   Source: 'test.rs', lines 13:1-13:10 -/
+def main : Result Unit :=
+  do
+  let _ ← select true 3#i32 7#i32
+  Result.ok ()
+
+end test

tests/expected/llbc/enum_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean

@@ -0,0 +1,31 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::MyEnum]
+   Source: 'test.rs', lines 8:1-8:12 -/
+inductive MyEnum :=
+| A : I32 → MyEnum
+| B : MyEnum
+
+/- [test::enum_match]:
+   Source: 'test.rs', lines 14:1-14:32 -/
+def enum_match (e : MyEnum) : Result I32 :=
+  match e with
+  | MyEnum.A i => Result.ok i
+  | MyEnum.B => Result.ok 0#i32
+
+/- [test::main]:
+   Source: 'test.rs', lines 24:1-24:10 -/
+def main : Result Unit :=
+  do
+  let _ ← enum_match (MyEnum.A 1#i32)
+  Result.ok ()
+
+end test

tests/expected/llbc/enum_test/expected

@@ -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_test/test.rs

@@ -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/projection_test/expected

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

tests/expected/llbc/projection_test/test.rs

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

tests/expected/llbc/struct_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean

@@ -0,0 +1,29 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::MyStruct]
+   Source: 'test.rs', lines 7:1-7:16 -/
+structure MyStruct where
+  a : I32
+  b : Bool
+
+/- [test::struct_project]:
+   Source: 'test.rs', lines 12:1-12:38 -/
+def struct_project (s : MyStruct) : Result I32 :=
+  Result.ok s.a
+
+/- [test::main]:
+   Source: 'test.rs', lines 17:1-17:10 -/
+def main : Result Unit :=
+  do
+  let _ ← struct_project { a := 1#i32, b := true }
+  Result.ok ()
+
+end test

tests/expected/llbc/struct_test/expected

@@ -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 := @Fun0(move (s@1))
+    drop a@2
+    @0 := ()
+    return
+}

tests/expected/llbc/struct_test/test.rs

@@ -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/tuple_test/TestRNvCshcvyQEKZjUj4test4main.symtab.lean

@@ -0,0 +1,24 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [test]
+import Base
+open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace test
+
+/- [test::tuple_add]:
+   Source: 'test.rs', lines 7:1-7:36 -/
+def tuple_add (t : (I32 × I32)) : Result I32 :=
+  let (i, i1) := t
+  i + i1
+
+/- [test::main]:
+   Source: 'test.rs', lines 12:1-12:10 -/
+def main : Result Unit :=
+  do
+  let _ ← tuple_add (1#i32, 2#i32)
+  Result.ok ()
+
+end test

tests/expected/llbc/tuple_test/expected

@@ -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 := @Fun0(move (@2))
+    drop @2
+    drop s@1
+    @0 := ()
+    return
+}

tests/expected/llbc/tuple_test/test.rs

@@ -0,0 +1,14 @@
+// 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 tuple
+
+fn tuple_add(t: (i32, i32)) -> i32 {
+    t.0 + t.1
+}
+
+#[kani::proof]
+fn main() {
+    let s = tuple_add((1, 2));
+}