From b2cce898ae81f893cb9fbdfd15c3ef21956229f3 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 15 Nov 2024 04:58:05 +0000 Subject: [PATCH 1/3] chore: unify bv_auto and bv_bench --- SSA/Projects/InstCombine/AliveStatements.lean | 93 +++++++++++++++++++ SSA/Projects/InstCombine/TacticAuto.lean | 16 ++-- .../InstCombine/update_alive_statements.py | 2 +- 3 files changed, 102 insertions(+), 9 deletions(-) diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean index 68d3f5b1c..d5c89e4f5 100644 --- a/SSA/Projects/InstCombine/AliveStatements.lean +++ b/SSA/Projects/InstCombine/AliveStatements.lean @@ -13,6 +13,7 @@ theorem bv_AddSub_1043 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -21,6 +22,7 @@ theorem bv_AddSub_1152 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -29,6 +31,7 @@ theorem bv_AddSub_1156 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -37,6 +40,7 @@ theorem bv_AddSub_1164 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -46,6 +50,7 @@ theorem bv_AddSub_1165 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -54,6 +59,7 @@ theorem bv_AddSub_1176 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -62,6 +68,7 @@ theorem bv_AddSub_1202 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -70,6 +77,7 @@ theorem bv_AddSub_1295 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -78,6 +86,7 @@ theorem bv_AddSub_1309 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -86,6 +95,7 @@ theorem bv_AddSub_1539 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -94,6 +104,7 @@ theorem bv_AddSub_1539_2 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -102,6 +113,7 @@ theorem bv_AddSub_1556 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -110,6 +122,7 @@ theorem bv_AddSub_1560 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -118,6 +131,7 @@ theorem bv_AddSub_1564 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -126,6 +140,7 @@ theorem bv_AddSub_1574 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -134,6 +149,7 @@ theorem bv_AddSub_1614 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -142,6 +158,7 @@ theorem bv_AddSub_1619 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -150,6 +167,7 @@ theorem bv_AddSub_1624 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -158,6 +176,7 @@ theorem bv_AndOrXor_135 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -166,6 +185,7 @@ theorem bv_AndOrXor_144 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -177,6 +197,7 @@ theorem bv_AndOrXor_698 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -187,6 +208,7 @@ theorem bv_AndOrXor_709 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -198,6 +220,7 @@ theorem bv_AndOrXor_716 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -208,6 +231,7 @@ theorem bv_AndOrXor_794 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -218,6 +242,7 @@ theorem bv_AndOrXor_827 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -227,6 +252,7 @@ theorem bv_AndOrXor_887_2 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -237,6 +263,7 @@ theorem bv_AndOrXor_1230__A__B___A__B : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -245,6 +272,7 @@ theorem bv_AndOrXor_1241_AB__AB__AB : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -253,6 +281,7 @@ theorem bv_AndOrXor_1247_AB__AB__AB : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -261,6 +290,7 @@ theorem bv_AndOrXor_1253_A__AB___A__B : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -269,6 +299,7 @@ theorem bv_AndOrXor_1280_ABA___AB : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -279,6 +310,7 @@ theorem bv_AndOrXor_1288_A__B__B__C__A___A__B__C : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -287,6 +319,7 @@ theorem bv_AndOrXor_1294_A__B__A__B___A__B : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -297,6 +330,7 @@ theorem bv_AndOrXor_1683_1 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -306,6 +340,7 @@ theorem bv_AndOrXor_1683_2 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -316,6 +351,7 @@ theorem bv_AndOrXor_1704 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -326,6 +362,7 @@ theorem bv_AndOrXor_1705 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -336,6 +373,7 @@ theorem bv_AndOrXor_1733 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -344,6 +382,7 @@ theorem bv_AndOrXor_2063__X__C1__C2____X__C2__C1__C2 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -352,6 +391,7 @@ theorem bv_AndOrXor_2113___A__B__A___A__B : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -361,6 +401,7 @@ theorem bv_AndOrXor_2118___A__B__A___A__B : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -369,6 +410,7 @@ theorem bv_AndOrXor_2123___A__B__A__B___A__B : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -379,6 +421,7 @@ theorem bv_AndOrXor_2188 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -387,6 +430,7 @@ theorem bv_AndOrXor_2231__A__B__B__C__A___A__B__C : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -395,6 +439,7 @@ theorem bv_AndOrXor_2243__B__C__A__B___B__A__C : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -405,6 +450,7 @@ theorem bv_AndOrXor_2247__A__B__A__B : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -413,6 +459,7 @@ theorem bv_AndOrXor_2263 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -422,6 +469,7 @@ theorem bv_AndOrXor_2264 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -430,6 +478,7 @@ theorem bv_AndOrXor_2265 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -439,6 +488,7 @@ theorem bv_AndOrXor_2284 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -448,6 +498,7 @@ theorem bv_AndOrXor_2285 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -458,6 +509,7 @@ theorem bv_AndOrXor_2297 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -466,6 +518,7 @@ theorem bv_AndOrXor_2367 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -476,6 +529,7 @@ theorem bv_AndOrXor_2416 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -486,6 +540,7 @@ theorem bv_AndOrXor_2417 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -496,6 +551,7 @@ theorem bv_AndOrXor_2429 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -506,6 +562,7 @@ theorem bv_AndOrXor_2430 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -515,6 +572,7 @@ theorem bv_AndOrXor_2443 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -524,6 +582,7 @@ theorem bv_AndOrXor_2453 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -532,6 +591,7 @@ theorem bv_AndOrXor_2475 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -540,6 +600,7 @@ theorem bv_AndOrXor_2486 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -548,6 +609,7 @@ theorem bv_AndOrXor_2581__BAB___A__B : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -556,6 +618,7 @@ theorem bv_AndOrXor_2587__BAA___B__A : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -564,6 +627,7 @@ theorem bv_AndOrXor_2595 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -574,6 +638,7 @@ theorem bv_AndOrXor_2607 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -584,6 +649,7 @@ theorem bv_AndOrXor_2617 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -593,6 +659,7 @@ theorem bv_AndOrXor_2627 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -601,6 +668,7 @@ theorem bv_AndOrXor_2647 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -611,6 +679,7 @@ theorem bv_AndOrXor_2658 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -621,6 +690,7 @@ theorem bv_AndOrXor_2663 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -629,6 +699,7 @@ theorem bv_152 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -637,6 +708,7 @@ theorem bv_229 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -645,6 +717,7 @@ theorem bv_239 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -653,6 +726,7 @@ theorem bv_275 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -661,6 +735,7 @@ theorem bv_275_2 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -669,6 +744,7 @@ theorem bv_276 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -677,6 +753,7 @@ theorem bv_276_2 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -685,6 +762,7 @@ theorem bv_283 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -693,6 +771,7 @@ theorem bv_290__292 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -701,6 +780,7 @@ theorem bv_820 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -709,6 +789,7 @@ theorem bv_820' : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -717,6 +798,7 @@ theorem bv_1030 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -726,6 +808,7 @@ theorem bv_Select_858 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -735,6 +818,7 @@ theorem bv_Select_859' : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -743,6 +827,7 @@ theorem bv_select_1100 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -751,6 +836,7 @@ theorem bv_Select_1105 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -759,6 +845,7 @@ theorem bv_InstCombineShift__239 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -767,6 +854,7 @@ theorem bv_InstCombineShift__279 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -777,6 +865,7 @@ theorem bv_InstCombineShift__440 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -787,6 +876,7 @@ theorem bv_InstCombineShift__476 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -795,6 +885,7 @@ theorem bv_InstCombineShift__497 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -803,6 +894,7 @@ theorem bv_InstCombineShift__497''' : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry @@ -811,5 +903,6 @@ theorem bv_InstCombineShift__582 : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split try alive_auto all_goals sorry diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean index 2b2ab78c0..39f2eae1e 100644 --- a/SSA/Projects/InstCombine/TacticAuto.lean +++ b/SSA/Projects/InstCombine/TacticAuto.lean @@ -188,8 +188,8 @@ macro "bv_ring" : tactic => ( simp (config := {failIfUnchanged := false}) only [← BitVec.allOnes_sub_eq_xor, ← BitVec.negOne_eq_allOnes] - ring_nf - rfl + try ring_nf + try rfl done ) ) @@ -207,12 +207,9 @@ macro "bv_ac" : tactic => macro "bv_auto": tactic => `(tactic| ( - intros - try simp (config := {failIfUnchanged := false}) [-Bool.and_iff_left_iff_imp, (BitVec.negOne_eq_allOnes)] - try ring_nf - try bv_eliminate_bool - repeat (split) - <;> try simp (config := {failIfUnchanged := false}) + simp (config := { failIfUnchanged := false }) only + [BitVec.ofBool_or_ofBool, BitVec.ofBool_and_ofBool, + BitVec.ofBool_xor_ofBool, BitVec.ofBool_eq_iff_eq] try solve | bv_bitwise | bv_ac @@ -281,6 +278,9 @@ macro "simp_alive_benchmark": tactic => macro "bv_bench": tactic => `(tactic| ( + simp (config := { failIfUnchanged := false }) only + [BitVec.ofBool_or_ofBool, BitVec.ofBool_and_ofBool, + BitVec.ofBool_xor_ofBool, BitVec.ofBool_eq_iff_eq] all_goals ( tac_bench [ "rfl" : (rfl; done), diff --git a/SSA/Projects/InstCombine/update_alive_statements.py b/SSA/Projects/InstCombine/update_alive_statements.py index 0750848fe..b8ad151b9 100755 --- a/SSA/Projects/InstCombine/update_alive_statements.py +++ b/SSA/Projects/InstCombine/update_alive_statements.py @@ -93,7 +93,7 @@ def getStatement(preamble: List[str], id : int, proof: List[str]) -> (str, str): stmt = name stmt += msg stmt_sorry = stmt + " := by\n sorry" - stmt += " := by\n simp_alive_undef\n simp_alive_ops\n simp_alive_case_bash\n try alive_auto\n all_goals sorry" + stmt += " := by\n simp_alive_undef\n simp_alive_ops\n simp_alive_case_bash\n simp_alive_split\n try alive_auto\n all_goals sorry" print(stmt) From 978c8d1a140862f798f97b97543591ad6c72caa2 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 15 Nov 2024 05:11:40 +0000 Subject: [PATCH 2/3] Fix --- SSA/Projects/InstCombine/AliveHandwrittenExamples.lean | 1 + SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean index 468044823..e01e8b9fd 100644 --- a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean +++ b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean @@ -45,6 +45,7 @@ theorem alive_DivRemOfSelect (w : Nat) : simp_alive_undef simp_alive_ops simp_alive_case_bash + simp_alive_split alive_auto end AliveHandwritten diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean index e97403b55..42aaa04b0 100644 --- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean +++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean @@ -44,6 +44,7 @@ theorem alive_DivRemOfSelect (w : Nat) : simp_alive_ssa simp_alive_undef simp_alive_case_bash + simp_alive_split alive_auto /--info: 'AliveHandwritten.DivRemOfSelect.alive_DivRemOfSelect' depends on From 64977ae36f3843ea6f719252fbab6e5ba00737df Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 15 Nov 2024 05:26:26 +0000 Subject: [PATCH 3/3] Fix --- SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean index 42aaa04b0..ecabe7867 100644 --- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean +++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean @@ -414,7 +414,9 @@ def alive_simplifyAndOrXor2515 (w : Nat) : simp only [simp_llvm_wrap] simp_alive_ssa simp_alive_undef + simp_alive_ops simp_alive_case_bash + simp_alive_split alive_auto /-- info: 'AliveHandwritten.AndOrXor.alive_simplifyAndOrXor2515' depends on axioms: