Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 24 commits into from
Nov 22, 2024
Merged
Show file tree
Hide file tree
Changes from 20 commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
e7f4152
add support for enum, struct, tuple in mod.rs, add some tests
thanhnguyen-aws Nov 15, 2024
0937022
revert changes
thanhnguyen-aws Nov 15, 2024
bb789a7
format code
thanhnguyen-aws Nov 15, 2024
cebeff5
edit according to clippy suggestions
thanhnguyen-aws Nov 15, 2024
694f7ac
add new line at the send of basic0/expected, remove comments in mod.rs
thanhnguyen-aws Nov 18, 2024
6998703
remove more commented functions
thanhnguyen-aws Nov 18, 2024
75dcb09
format code
thanhnguyen-aws Nov 18, 2024
ad57da7
Merge branch 'model-checking:main' into thanh-llbc
thanhnguyen-aws Nov 18, 2024
7ac77f3
add end lines to expected files for the 4 test cases
thanhnguyen-aws Nov 18, 2024
4d40b53
remove comments
thanhnguyen-aws Nov 18, 2024
7977233
update s2n-quic
thanhnguyen-aws Nov 18, 2024
28395c5
re-run kani and fix the expected file
thanhnguyen-aws Nov 18, 2024
2d2f6ce
change function namne find_type_decl_id to get_type_decl_id
thanhnguyen-aws Nov 19, 2024
c729818
change function namne find_type_decl_id to get_type_decl_id
thanhnguyen-aws Nov 19, 2024
dbd7215
added the translation for generic params, fixed the formatting
thanhnguyen-aws Nov 20, 2024
e3bb0ca
Merge branch 'main' into thanh-llbc
thanhnguyen-aws Nov 20, 2024
997db12
comment change
thanhnguyen-aws Nov 20, 2024
3ec593d
fixed the expected testes
thanhnguyen-aws Nov 20, 2024
000d098
fixed clippy
thanhnguyen-aws Nov 20, 2024
4107f81
fixed format
thanhnguyen-aws Nov 20, 2024
43bd739
group use statements and add a test that use generic args
thanhnguyen-aws Nov 21, 2024
137008c
fixed unreachable -> todo
thanhnguyen-aws Nov 21, 2024
df89b51
fixed format
thanhnguyen-aws Nov 21, 2024
2cb0e56
changing some test folders' names
thanhnguyen-aws Nov 22, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
922 changes: 743 additions & 179 deletions kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

Large diffs are not rendered by default.

36 changes: 36 additions & 0 deletions tests/expected/llbc/enum_test/expected
Original file line number Diff line number Diff line change
@@ -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
}
23 changes: 23 additions & 0 deletions tests/expected/llbc/enum_test/test.rs
Original file line number Diff line number Diff line change
@@ -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);
}
84 changes: 84 additions & 0 deletions tests/expected/llbc/projection_test/expected
Original file line number Diff line number Diff line change
@@ -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
}
38 changes: 38 additions & 0 deletions tests/expected/llbc/projection_test/test.rs
Original file line number Diff line number Diff line change
@@ -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);
}
27 changes: 27 additions & 0 deletions tests/expected/llbc/struct_test/expected
Original file line number Diff line number Diff line change
@@ -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
}
20 changes: 20 additions & 0 deletions tests/expected/llbc/struct_test/test.rs
Original file line number Diff line number Diff line change
@@ -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);
}
28 changes: 28 additions & 0 deletions tests/expected/llbc/tuple_test/expected
Original file line number Diff line number Diff line change
@@ -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
}
14 changes: 14 additions & 0 deletions tests/expected/llbc/tuple_test/test.rs
Original file line number Diff line number Diff line change
@@ -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));
}
Loading