Skip to content

pre-commit: PR166935 #3107

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.

Sign up for GitHub

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

Open
zyw-bot wants to merge 3 commits into
base: main
Choose a base branch
from
Open

pre-commit: PR166935 #3107

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8faebac
pre-commit: PR166935
nikic Dec 4, 2025
86375d1
pre-commit: Update
github-actions[bot] Dec 4, 2025
9699001
pre-commit: Remap
github-actions[bot] Dec 4, 2025
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
224 changes: 108 additions & 116 deletions bench/abc/optimized/cuddZddLin.ll
View file
Open in desktop

Large diffs are not rendered by default.

44 changes: 16 additions & 28 deletions bench/lean4/optimized/AndFlatten.ll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13070,56 +13070,44 @@ lean_alloc_closure.exit: ; preds = %7
define ptr @l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_BVDecide_Frontend_Normalize_andFlatteningPass_processGoal___spec__1___boxed(ptr noundef %0, ptr noundef %1, ptr noundef %2, ptr noundef %3, ptr noundef %4, ptr noundef %5, ptr noundef %6, ptr noundef %7, ptr noundef %8, ptr noundef %9) local_unnamed_addr #1 {
%11 = getelementptr i8, ptr %1, i64 8
%.val = load i64, ptr %11, align 8, !tbaa !12
%12 = ptrtoint ptr %1 to i64
%13 = and i64 %12, 1
%.not = icmp eq i64 %13, 0
br i1 %.not, label %14, label %lean_dec.exit16
%12 = load i32, ptr %1, align 8, !tbaa !4
%13 = icmp sgt i32 %12, 1
br i1 %13, label %14, label %16, !prof !11

14: ; preds = %10
%15 = load i32, ptr %1, align 4, !tbaa !4
%16 = icmp sgt i32 %15, 1
br i1 %16, label %17, label %19, !prof !11

17: ; preds = %14
%18 = add nsw i32 %15, -1
store i32 %18, ptr %1, align 4, !tbaa !4
%15 = add nsw i32 %12, -1
store i32 %15, ptr %1, align 4, !tbaa !4
br label %lean_dec.exit16

19: ; preds = %14
%.not.i = icmp eq i32 %15, 0
19: ; preds = %10
%.not.i = icmp eq i32 %12, 0
br i1 %.not.i, label %lean_dec.exit16, label %20

20: ; preds = %19
tail call void @lean_dec_ref_cold(ptr noundef nonnull %1) #4
br label %lean_dec.exit16

lean_dec.exit16: ; preds = %20, %19, %17, %10
lean_dec.exit16: ; preds = %20, %19, %14
%21 = getelementptr i8, ptr %2, i64 8
%.val21 = load i64, ptr %21, align 8, !tbaa !12
%22 = ptrtoint ptr %2 to i64
%23 = and i64 %22, 1
%.not22 = icmp eq i64 %23, 0
br i1 %.not22, label %24, label %lean_dec.exit15

24: ; preds = %lean_dec.exit16
%25 = load i32, ptr %2, align 4, !tbaa !4
%26 = icmp sgt i32 %25, 1
br i1 %26, label %27, label %29, !prof !11
%19 = load i32, ptr %2, align 8, !tbaa !4
%20 = icmp sgt i32 %19, 1
br i1 %20, label %21, label %23, !prof !11

27: ; preds = %24
%28 = add nsw i32 %25, -1
27: ; preds = %lean_dec.exit16
%28 = add nsw i32 %19, -1
store i32 %28, ptr %2, align 4, !tbaa !4
br label %lean_dec.exit15

29: ; preds = %24
%.not.i17 = icmp eq i32 %25, 0
29: ; preds = %lean_dec.exit16
%.not.i17 = icmp eq i32 %19, 0
br i1 %.not.i17, label %lean_dec.exit15, label %30

30: ; preds = %29
tail call void @lean_dec_ref_cold(ptr noundef nonnull %2) #4
br label %lean_dec.exit15

lean_dec.exit15: ; preds = %30, %29, %27, %lean_dec.exit16
lean_dec.exit15: ; preds = %30, %29, %21
%31 = tail call ptr @l_Array_foldlMUnsafe_fold___at_Lean_Elab_Tactic_BVDecide_Frontend_Normalize_andFlatteningPass_processGoal___spec__1(ptr noundef %0, i64 noundef %.val, i64 noundef %.val21, ptr noundef %3, ptr noundef %4, ptr noundef %5, ptr noundef %6, ptr noundef %7, ptr noundef %8, ptr noundef %9)
%32 = ptrtoint ptr %0 to i64
%33 = and i64 %32, 1
Expand Down
22 changes: 8 additions & 14 deletions bench/lean4/optimized/Assumption.ll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6169,30 +6169,24 @@ define ptr @l_Lean_LocalContext_findDeclRevM_x3f___at_Lean_Meta_findLocalDeclWit
%8 = getelementptr inbounds nuw i8, ptr %1, i64 16
%9 = load ptr, ptr %8, align 8, !tbaa !11
%10 = tail call ptr @l_Lean_PersistentArray_findSomeRevM_x3f___at_Lean_Meta_findLocalDeclWithType_x3f___spec__2(ptr noundef %0, ptr noundef %9, ptr noundef %2, ptr noundef %3, ptr noundef %4, ptr noundef %5, ptr noundef %6)
%11 = ptrtoint ptr %1 to i64
%12 = and i64 %11, 1
%.not = icmp eq i64 %12, 0
br i1 %.not, label %13, label %lean_dec.exit
%11 = load i32, ptr %1, align 8, !tbaa !5
%12 = icmp sgt i32 %11, 1
br i1 %12, label %13, label %15, !prof !10

13: ; preds = %7
%14 = load i32, ptr %1, align 4, !tbaa !5
%15 = icmp sgt i32 %14, 1
br i1 %15, label %16, label %18, !prof !10

16: ; preds = %13
%17 = add nsw i32 %14, -1
store i32 %17, ptr %1, align 4, !tbaa !5
%14 = add nsw i32 %11, -1
store i32 %14, ptr %1, align 4, !tbaa !5
br label %lean_dec.exit

18: ; preds = %13
%.not.i = icmp eq i32 %14, 0
18: ; preds = %7
%.not.i = icmp eq i32 %11, 0
br i1 %.not.i, label %lean_dec.exit, label %19

19: ; preds = %18
tail call void @lean_dec_ref_cold(ptr noundef nonnull %1) #4
br label %lean_dec.exit

lean_dec.exit: ; preds = %19, %18, %16, %7
lean_dec.exit: ; preds = %19, %18, %13
ret ptr %10
}

Expand Down
144 changes: 54 additions & 90 deletions bench/lean4/optimized/Attach.ll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -205,56 +205,44 @@ lean_alloc_closure.exit: ; preds = %3
define ptr @l_Array_mapMUnsafe_map___at_Vector_pmap___spec__1___rarg___boxed(ptr noundef %0, ptr noundef %1, ptr noundef %2, ptr noundef %3) #0 {
%5 = getelementptr i8, ptr %1, i64 8
%.val = load i64, ptr %5, align 8, !tbaa !14
%6 = ptrtoint ptr %1 to i64
%7 = and i64 %6, 1
%.not = icmp eq i64 %7, 0
br i1 %.not, label %8, label %lean_dec.exit8
%6 = load i32, ptr %1, align 8, !tbaa !4
%7 = icmp sgt i32 %6, 1
br i1 %7, label %8, label %10, !prof !9

8: ; preds = %4
%9 = load i32, ptr %1, align 4, !tbaa !4
%10 = icmp sgt i32 %9, 1
br i1 %10, label %11, label %13, !prof !9

11: ; preds = %8
%12 = add nsw i32 %9, -1
store i32 %12, ptr %1, align 4, !tbaa !4
%9 = add nsw i32 %6, -1
store i32 %9, ptr %1, align 4, !tbaa !4
br label %lean_dec.exit8

13: ; preds = %8
%.not.i = icmp eq i32 %9, 0
13: ; preds = %4
%.not.i = icmp eq i32 %6, 0
br i1 %.not.i, label %lean_dec.exit8, label %14

14: ; preds = %13
tail call void @lean_dec_ref_cold(ptr noundef nonnull %1) #3
br label %lean_dec.exit8

lean_dec.exit8: ; preds = %14, %13, %11, %4
lean_dec.exit8: ; preds = %14, %13, %8
%15 = getelementptr i8, ptr %2, i64 8
%.val11 = load i64, ptr %15, align 8, !tbaa !14
%16 = ptrtoint ptr %2 to i64
%17 = and i64 %16, 1
%.not12 = icmp eq i64 %17, 0
br i1 %.not12, label %18, label %lean_dec.exit

18: ; preds = %lean_dec.exit8
%19 = load i32, ptr %2, align 4, !tbaa !4
%20 = icmp sgt i32 %19, 1
br i1 %20, label %21, label %23, !prof !9

21: ; preds = %18
%22 = add nsw i32 %19, -1
store i32 %22, ptr %2, align 4, !tbaa !4
%13 = load i32, ptr %2, align 8, !tbaa !4
%14 = icmp sgt i32 %13, 1
br i1 %14, label %15, label %17, !prof !9

15: ; preds = %lean_dec.exit8
%16 = add nsw i32 %13, -1
store i32 %16, ptr %2, align 4, !tbaa !4
br label %lean_dec.exit

23: ; preds = %18
%.not.i9 = icmp eq i32 %19, 0
23: ; preds = %lean_dec.exit8
%.not.i9 = icmp eq i32 %13, 0
br i1 %.not.i9, label %lean_dec.exit, label %24

24: ; preds = %23
tail call void @lean_dec_ref_cold(ptr noundef nonnull %2) #3
br label %lean_dec.exit

lean_dec.exit: ; preds = %24, %23, %21, %lean_dec.exit8
lean_dec.exit: ; preds = %24, %23, %15
%25 = tail call ptr @l_Array_mapMUnsafe_map___at_Vector_pmap___spec__1___rarg(ptr noundef %0, i64 noundef %.val, i64 noundef %.val11, ptr noundef %3)
ret ptr %25
}
Expand Down Expand Up @@ -835,56 +823,44 @@ lean_alloc_closure.exit: ; preds = %3
define ptr @l_Array_mapMUnsafe_map___at___private_Init_Data_Vector_Attach_0__Vector_pmapImpl___spec__1___rarg___boxed(ptr noundef %0, ptr noundef %1, ptr noundef %2, ptr noundef %3) #0 {
%5 = getelementptr i8, ptr %1, i64 8
%.val11 = load i64, ptr %5, align 8, !tbaa !14
%6 = ptrtoint ptr %1 to i64
%7 = and i64 %6, 1
%.not = icmp eq i64 %7, 0
br i1 %.not, label %8, label %lean_dec.exit8
%6 = load i32, ptr %1, align 8, !tbaa !4
%7 = icmp sgt i32 %6, 1
br i1 %7, label %8, label %10, !prof !9

8: ; preds = %4
%9 = load i32, ptr %1, align 4, !tbaa !4
%10 = icmp sgt i32 %9, 1
br i1 %10, label %11, label %13, !prof !9

11: ; preds = %8
%12 = add nsw i32 %9, -1
store i32 %12, ptr %1, align 4, !tbaa !4
%9 = add nsw i32 %6, -1
store i32 %9, ptr %1, align 4, !tbaa !4
br label %lean_dec.exit8

13: ; preds = %8
%.not.i = icmp eq i32 %9, 0
13: ; preds = %4
%.not.i = icmp eq i32 %6, 0
br i1 %.not.i, label %lean_dec.exit8, label %14

14: ; preds = %13
tail call void @lean_dec_ref_cold(ptr noundef nonnull %1) #3
br label %lean_dec.exit8

lean_dec.exit8: ; preds = %14, %13, %11, %4
lean_dec.exit8: ; preds = %14, %13, %8
%15 = getelementptr i8, ptr %2, i64 8
%.val = load i64, ptr %15, align 8, !tbaa !14
%16 = ptrtoint ptr %2 to i64
%17 = and i64 %16, 1
%.not12 = icmp eq i64 %17, 0
br i1 %.not12, label %18, label %lean_dec.exit

18: ; preds = %lean_dec.exit8
%19 = load i32, ptr %2, align 4, !tbaa !4
%20 = icmp sgt i32 %19, 1
br i1 %20, label %21, label %23, !prof !9

21: ; preds = %18
%22 = add nsw i32 %19, -1
store i32 %22, ptr %2, align 4, !tbaa !4
%13 = load i32, ptr %2, align 8, !tbaa !4
%14 = icmp sgt i32 %13, 1
br i1 %14, label %15, label %17, !prof !9

15: ; preds = %lean_dec.exit8
%16 = add nsw i32 %13, -1
store i32 %16, ptr %2, align 4, !tbaa !4
br label %lean_dec.exit

23: ; preds = %18
%.not.i9 = icmp eq i32 %19, 0
23: ; preds = %lean_dec.exit8
%.not.i9 = icmp eq i32 %13, 0
br i1 %.not.i9, label %lean_dec.exit, label %24

24: ; preds = %23
tail call void @lean_dec_ref_cold(ptr noundef nonnull %2) #3
br label %lean_dec.exit

lean_dec.exit: ; preds = %24, %23, %21, %lean_dec.exit8
lean_dec.exit: ; preds = %24, %23, %15
%25 = tail call ptr @l_Array_mapMUnsafe_map___at___private_Init_Data_Vector_Attach_0__Vector_pmapImpl___spec__1___rarg(ptr noundef %0, i64 noundef %.val11, i64 noundef %.val, ptr noundef %3)
ret ptr %25
}
Expand Down Expand Up @@ -1120,56 +1096,44 @@ lean_alloc_closure.exit: ; preds = %2
define ptr @l_Array_mapMUnsafe_map___at_Vector_unattach___spec__1___rarg___boxed(ptr noundef %0, ptr noundef %1, ptr noundef %2) #0 {
%4 = getelementptr i8, ptr %0, i64 8
%.val10 = load i64, ptr %4, align 8, !tbaa !14
%5 = ptrtoint ptr %0 to i64
%6 = and i64 %5, 1
%.not = icmp eq i64 %6, 0
br i1 %.not, label %7, label %lean_dec.exit7
%5 = load i32, ptr %0, align 8, !tbaa !4
%6 = icmp sgt i32 %5, 1
br i1 %6, label %7, label %9, !prof !9

7: ; preds = %3
%8 = load i32, ptr %0, align 4, !tbaa !4
%9 = icmp sgt i32 %8, 1
br i1 %9, label %10, label %12, !prof !9

10: ; preds = %7
%11 = add nsw i32 %8, -1
store i32 %11, ptr %0, align 4, !tbaa !4
%8 = add nsw i32 %5, -1
store i32 %8, ptr %0, align 4, !tbaa !4
br label %lean_dec.exit7

12: ; preds = %7
%.not.i = icmp eq i32 %8, 0
12: ; preds = %3
%.not.i = icmp eq i32 %5, 0
br i1 %.not.i, label %lean_dec.exit7, label %13

13: ; preds = %12
tail call void @lean_dec_ref_cold(ptr noundef nonnull %0) #3
br label %lean_dec.exit7

lean_dec.exit7: ; preds = %13, %12, %10, %3
lean_dec.exit7: ; preds = %13, %12, %7
%14 = getelementptr i8, ptr %1, i64 8
%.val = load i64, ptr %14, align 8, !tbaa !14
%15 = ptrtoint ptr %1 to i64
%16 = and i64 %15, 1
%.not11 = icmp eq i64 %16, 0
br i1 %.not11, label %17, label %lean_dec.exit

17: ; preds = %lean_dec.exit7
%18 = load i32, ptr %1, align 4, !tbaa !4
%19 = icmp sgt i32 %18, 1
br i1 %19, label %20, label %22, !prof !9

20: ; preds = %17
%21 = add nsw i32 %18, -1
store i32 %21, ptr %1, align 4, !tbaa !4
%15 = load i32, ptr %1, align 8, !tbaa !4
%13 = icmp sgt i32 %15, 1
br i1 %13, label %14, label %16, !prof !9

14: ; preds = %lean_dec.exit7
%15 = add nsw i32 %12, -1
store i32 %15, ptr %1, align 4, !tbaa !4
br label %lean_dec.exit

22: ; preds = %17
%.not.i8 = icmp eq i32 %18, 0
22: ; preds = %lean_dec.exit7
%.not.i8 = icmp eq i32 %12, 0
br i1 %.not.i8, label %lean_dec.exit, label %23

23: ; preds = %22
tail call void @lean_dec_ref_cold(ptr noundef nonnull %1) #3
br label %lean_dec.exit

lean_dec.exit: ; preds = %23, %22, %20, %lean_dec.exit7
lean_dec.exit: ; preds = %23, %22, %14
%24 = tail call ptr @l_Array_mapMUnsafe_map___at_Vector_unattach___spec__1___rarg(i64 noundef %.val10, i64 noundef %.val, ptr noundef %2)
ret ptr %24
}
Expand Down
Loading