From cd08b517ec5ac9948e2ef21179b05ba4bfecb4b5 Mon Sep 17 00:00:00 2001 From: zhiyuan yan Date: Tue, 25 Jun 2024 17:08:12 -0700 Subject: [PATCH 1/3] readd hoist test. change loop_hoist.bril to make it only work for loop hoisting --- dag_in_context/src/from_egglog.rs | 5 +- .../src/optimizations/loop_invariant.rs | 66 +++++++++++++++++++ dag_in_context/src/schedule.rs | 2 +- tests/passing/small/loop_hoist.bril | 7 +- .../files__block-diamond-optimize.snap | 26 ++++---- .../files__gamma_condition_and-optimize.snap | 2 +- .../files__if_dead_code_nested-optimize.snap | 4 +- .../snapshots/files__if_in_loop-optimize.snap | 50 +++++++------- .../files__implicit-return-optimize.snap | 63 +++++++++--------- .../snapshots/files__loop_hoist-optimize.snap | 40 ++++++----- tests/snapshots/files__sqrt-optimize.snap | 4 +- 11 files changed, 169 insertions(+), 100 deletions(-) diff --git a/dag_in_context/src/from_egglog.rs b/dag_in_context/src/from_egglog.rs index a0e296340..7b07b84ad 100644 --- a/dag_in_context/src/from_egglog.rs +++ b/dag_in_context/src/from_egglog.rs @@ -143,7 +143,10 @@ impl<'a> FromEgglog<'a> { }; Assumption::InIf(boolean, self.expr_from_egglog(self.termdag.get(*pred_expr)), self.expr_from_egglog(self.termdag.get(*input_expr))) } - _ => panic!("Invalid assumption: {:?}", assumption), + (name, _) => { + eprintln!("Invalid assumption: {:?}", assumption); + Assumption::WildCard(name.into()) + } }) } diff --git a/dag_in_context/src/optimizations/loop_invariant.rs b/dag_in_context/src/optimizations/loop_invariant.rs index bf55804ea..84886bc45 100644 --- a/dag_in_context/src/optimizations/loop_invariant.rs +++ b/dag_in_context/src/optimizations/loop_invariant.rs @@ -209,3 +209,69 @@ fn test_invariant_detect() -> crate::Result { vec![], ) } + +#[test] +fn test_invariant_hoist() -> crate::Result { + use crate::add_context::ContextCache; + use crate::ast::*; + use crate::schema::Assumption; + + let mut cache = ContextCache::new_dummy_ctx(); + let output_ty = tuplet!(intt(), intt(), intt(), statet()); + let inner_inv = sub(getat(2), getat(1)); + let inv = add(inner_inv.clone(), int(1)); + let print = tprint(inv.clone(), getat(3)); + + let my_loop = dowhile( + parallel!(getat(0), getat(1), getat(2), getat(3)), + parallel!( + less_than(getat(0), getat(1)), + int(3), + getat(1), + getat(2), + print, + ), + ) + .with_arg_types(output_ty.clone(), output_ty.clone()) + .add_ctx_with_cache(Assumption::dummy(), &mut cache); + + let new_out_ty = tuplet!(intt(), intt(), intt(), statet(), intt()); + let mut cache = ContextCache::new_symbolic_ctx(); + + let hoisted_loop = dowhile( + parallel!( + getat(0), + getat(1), + getat(2), + getat(3), + add(int(1), sub(getat(2), getat(1))) + ), + parallel!( + less_than(getat(0), getat(1)), + int(3), + getat(1), + getat(2), + tprint(getat(4), getat(3)), + getat(4) + ), + ) + .with_arg_types(output_ty.clone(), new_out_ty) + .add_ctx_with_cache(Assumption::dummy(), &mut cache); + + let build = format!("(let loop {}) \n", my_loop); + let check = format!( + "(check {}) + (check (= loop (SubTuple {} 0 4)))", + hoisted_loop.clone(), + hoisted_loop + ); + + egglog_test( + &build, + &check, + vec![], + Value::Tuple(vec![]), + Value::Tuple(vec![]), + vec![], + ) +} diff --git a/dag_in_context/src/schedule.rs b/dag_in_context/src/schedule.rs index 77a38f32b..381a6c4f2 100644 --- a/dag_in_context/src/schedule.rs +++ b/dag_in_context/src/schedule.rs @@ -60,7 +60,7 @@ pub fn mk_schedule() -> String { cheap-optimizations switch_rewrite - ;loop-inv-motion + loop-inv-motion loop-strength-reduction loop-peel ) diff --git a/tests/passing/small/loop_hoist.bril b/tests/passing/small/loop_hoist.bril index ecfeffebe..2774af7f9 100644 --- a/tests/passing/small/loop_hoist.bril +++ b/tests/passing/small/loop_hoist.bril @@ -1,8 +1,5 @@ -@main() { - arg1: int = const 1; - arg2: int = const 2; - arg3: int = const 3; - arg4: int = const 4; +# ARGS: 1 2 3 4 +@main(arg1 : int, arg2 : int, arg3 : int, arg4 : int) { .entry: zero: int = const 0; sub: int = sub arg3 arg2; diff --git a/tests/snapshots/files__block-diamond-optimize.snap b/tests/snapshots/files__block-diamond-optimize.snap index 9263fd9ba..d730eb3ad 100644 --- a/tests/snapshots/files__block-diamond-optimize.snap +++ b/tests/snapshots/files__block-diamond-optimize.snap @@ -4,30 +4,30 @@ expression: visualization.result --- @main(v0: int) { .b1_: - c2_: int = const 2; - v3_: bool = lt v0 c2_; - v4_: bool = not v3_; - c5_: int = const 0; - c6_: int = const 1; + c2_: int = const 1; + c3_: int = const 2; + v4_: bool = lt v0 c3_; + v5_: bool = not v4_; + c6_: int = const 0; c7_: int = const 5; - v8_: int = id c6_; - v9_: int = id c6_; - v10_: int = id c2_; - br v3_ .b11_ .b12_; + v8_: int = id c2_; + v9_: int = id c2_; + v10_: int = id c3_; + br v4_ .b11_ .b12_; .b11_: c13_: int = const 4; v8_: int = id c13_; - v9_: int = id c6_; - v10_: int = id c2_; + v9_: int = id c2_; + v10_: int = id c3_; .b12_: v14_: int = id v8_; v15_: int = id v9_; - br v4_ .b16_ .b17_; + br v5_ .b16_ .b17_; .b16_: v18_: int = add v10_ v8_; v14_: int = id v18_; v15_: int = id v9_; .b17_: - v19_: int = add c6_ v14_; + v19_: int = add c2_ v14_; print v19_; } diff --git a/tests/snapshots/files__gamma_condition_and-optimize.snap b/tests/snapshots/files__gamma_condition_and-optimize.snap index e55e8d259..7c5c9df1f 100644 --- a/tests/snapshots/files__gamma_condition_and-optimize.snap +++ b/tests/snapshots/files__gamma_condition_and-optimize.snap @@ -6,7 +6,7 @@ expression: visualization.result .b1_: c2_: int = const 0; v3_: bool = lt v0 c2_; - v4_: bool = lt c2_ v0; + v4_: bool = gt v0 c2_; c5_: int = const 1; c6_: int = const 3; v7_: int = id c6_; diff --git a/tests/snapshots/files__if_dead_code_nested-optimize.snap b/tests/snapshots/files__if_dead_code_nested-optimize.snap index e6ffbdca9..9e48d1fac 100644 --- a/tests/snapshots/files__if_dead_code_nested-optimize.snap +++ b/tests/snapshots/files__if_dead_code_nested-optimize.snap @@ -31,7 +31,7 @@ expression: visualization.result print v18_; ret; .b8_: - v20_: bool = lt c6_ v0; + v20_: bool = gt v0 c6_; c21_: bool = const false; c22_: int = const 2; v23_: int = id c22_; @@ -39,7 +39,7 @@ expression: visualization.result v25_: int = id c4_; br v20_ .b26_ .b27_; .b26_: - v28_: bool = gt v0 c5_; + v28_: bool = lt c5_ v0; c29_: int = const 4; v30_: int = id c29_; v31_: bool = id c21_; diff --git a/tests/snapshots/files__if_in_loop-optimize.snap b/tests/snapshots/files__if_in_loop-optimize.snap index 15e1998c4..187187d12 100644 --- a/tests/snapshots/files__if_in_loop-optimize.snap +++ b/tests/snapshots/files__if_in_loop-optimize.snap @@ -7,39 +7,41 @@ expression: visualization.result c2_: int = const 0; c3_: int = const 1; c4_: int = const 10; - v5_: int = id c2_; - v6_: int = id c3_; - v7_: int = id v0; - v8_: int = id c2_; - v9_: int = id c4_; -.b10_: - v11_: bool = le v7_ v8_; - v12_: bool = lt v5_ v9_; - v13_: bool = id v12_; - v14_: int = id v5_; + v5_: bool = lt v0 c3_; + v6_: int = id c2_; + v7_: int = id c3_; + v8_: int = id v0; + v9_: int = id c2_; + v10_: int = id c4_; + v11_: bool = id v5_; +.b12_: + v13_: bool = lt v6_ v10_; + v14_: bool = id v13_; v15_: int = id v6_; - v16_: int = id v8_; - v17_: int = id v7_; + v16_: int = id v7_; + v17_: int = id v9_; v18_: int = id v8_; v19_: int = id v9_; - br v11_ .b20_ .b21_; -.b20_: - v13_: bool = id v12_; - v14_: int = id v5_; + v20_: int = id v10_; + br v11_ .b21_ .b22_; +.b21_: + v14_: bool = id v13_; v15_: int = id v6_; - v16_: int = id v6_; + v16_: int = id v7_; v17_: int = id v7_; v18_: int = id v8_; v19_: int = id v9_; -.b21_: - print v16_; + v20_: int = id v10_; +.b22_: + print v17_; print v11_; - v22_: int = add v5_ v6_; - v5_: int = id v22_; - v6_: int = id v6_; + v23_: int = add v6_ v7_; + v6_: int = id v23_; v7_: int = id v7_; v8_: int = id v8_; v9_: int = id v9_; - br v12_ .b10_ .b23_; -.b23_: + v10_: int = id v10_; + v11_: bool = id v11_; + br v13_ .b12_ .b24_; +.b24_: } diff --git a/tests/snapshots/files__implicit-return-optimize.snap b/tests/snapshots/files__implicit-return-optimize.snap index da3565f39..091e3490e 100644 --- a/tests/snapshots/files__implicit-return-optimize.snap +++ b/tests/snapshots/files__implicit-return-optimize.snap @@ -5,38 +5,41 @@ expression: visualization.result @pow(v0: int, v1: int) { .b2_: c3_: int = const 0; - v4_: int = id v0; - v5_: int = id c3_; + c4_: int = const 1; + v5_: int = sub v1 c4_; v6_: int = id v0; - v7_: int = id v1; -.b8_: - c9_: int = const 1; - v10_: int = sub v7_ c9_; - v11_: bool = lt v5_ v10_; - v12_: int = id v4_; - v13_: int = id v5_; - v14_: int = id v6_; - v15_: int = id v7_; - br v11_ .b16_ .b17_; -.b16_: - v18_: int = mul v4_ v6_; - c19_: int = const 1; - v20_: int = add c19_ v5_; - v12_: int = id v18_; - v13_: int = id v20_; - v14_: int = id v6_; - v15_: int = id v7_; - v4_: int = id v12_; - v5_: int = id v13_; - v6_: int = id v14_; - v7_: int = id v15_; - jmp .b8_; + v7_: int = id c3_; + v8_: int = id v0; + v9_: int = id v1; + v10_: int = id v5_; +.b11_: + v12_: bool = lt v7_ v10_; + v13_: int = id v6_; + v14_: int = id v7_; + v15_: int = id v8_; + v16_: int = id v9_; + br v12_ .b17_ .b18_; .b17_: - v4_: int = id v12_; - v5_: int = id v13_; - v6_: int = id v14_; - v7_: int = id v15_; - print v4_; + v19_: int = mul v6_ v8_; + c20_: int = const 1; + v21_: int = add c20_ v7_; + v13_: int = id v19_; + v14_: int = id v21_; + v15_: int = id v8_; + v16_: int = id v9_; + v6_: int = id v13_; + v7_: int = id v14_; + v8_: int = id v15_; + v9_: int = id v16_; + v10_: int = id v10_; + jmp .b11_; +.b18_: + v6_: int = id v13_; + v7_: int = id v14_; + v8_: int = id v15_; + v9_: int = id v16_; + v10_: int = id v10_; + print v6_; } @main { .b0_: diff --git a/tests/snapshots/files__loop_hoist-optimize.snap b/tests/snapshots/files__loop_hoist-optimize.snap index 9096261c8..ff0e49058 100644 --- a/tests/snapshots/files__loop_hoist-optimize.snap +++ b/tests/snapshots/files__loop_hoist-optimize.snap @@ -2,27 +2,25 @@ source: tests/files.rs expression: visualization.result --- -@main { -.b0_: - c1_: int = const 1; - c2_: int = const 4; - c3_: int = const 3; - c4_: int = const 2; - v5_: int = id c1_; - v6_: int = id c2_; - v7_: int = id c3_; - v8_: int = id c4_; -.b9_: - c10_: int = const 1; - print c10_; - v11_: int = add c10_ v5_; - v12_: bool = lt v11_ v6_; - v13_: bool = not v12_; - v5_: int = id v11_; - v6_: int = id v6_; +@main(v0: int, v1: int, v2: int, v3: int) { +.b4_: + v5_: int = sub v2 v1; + v6_: int = id v0; + v7_: int = id v3; + v8_: int = id v2; + v9_: int = id v1; + v10_: int = id v5_; +.b11_: + print v10_; + v12_: int = add v10_ v6_; + v13_: bool = lt v12_ v7_; + v14_: bool = not v13_; + v6_: int = id v12_; v7_: int = id v7_; v8_: int = id v8_; - br v13_ .b9_ .b14_; -.b14_: - print v5_; + v9_: int = id v9_; + v10_: int = id v10_; + br v14_ .b11_ .b15_; +.b15_: + print v6_; } diff --git a/tests/snapshots/files__sqrt-optimize.snap b/tests/snapshots/files__sqrt-optimize.snap index c0f3bcce9..0fec351e7 100644 --- a/tests/snapshots/files__sqrt-optimize.snap +++ b/tests/snapshots/files__sqrt-optimize.snap @@ -36,8 +36,8 @@ expression: visualization.result v28_: float = fadd v21_ v27_; v29_: float = fdiv v28_ v24_; v30_: float = fdiv v29_ v21_; - v31_: bool = fle v30_ v22_; - v32_: bool = fge v30_ v23_; + v31_: bool = fge v30_ v23_; + v32_: bool = fle v30_ v22_; v33_: bool = and v31_ v32_; v34_: bool = not v33_; v20_: float = id v20_; From c657577e8371f7e3c28a278fb914883a81231634 Mon Sep 17 00:00:00 2001 From: zhiyuan yan Date: Fri, 28 Jun 2024 13:41:56 -0700 Subject: [PATCH 2/3] snapshot??? --- .../files__block-diamond-optimize.snap | 28 +++++++++---------- .../files__fib_recursive-optimize.snap | 2 +- .../files__gamma_condition_and-optimize.snap | 4 +-- .../files__if_dead_code_nested-optimize.snap | 6 ++-- tests/snapshots/files__sqrt-optimize.snap | 6 ++-- 5 files changed, 23 insertions(+), 23 deletions(-) diff --git a/tests/snapshots/files__block-diamond-optimize.snap b/tests/snapshots/files__block-diamond-optimize.snap index d730eb3ad..02f3d9954 100644 --- a/tests/snapshots/files__block-diamond-optimize.snap +++ b/tests/snapshots/files__block-diamond-optimize.snap @@ -4,30 +4,30 @@ expression: visualization.result --- @main(v0: int) { .b1_: - c2_: int = const 1; - c3_: int = const 2; - v4_: bool = lt v0 c3_; - v5_: bool = not v4_; - c6_: int = const 0; + c2_: int = const 2; + v3_: bool = lt v0 c2_; + v4_: bool = not v3_; + c5_: int = const 0; + c6_: int = const 1; c7_: int = const 5; - v8_: int = id c2_; - v9_: int = id c2_; - v10_: int = id c3_; - br v4_ .b11_ .b12_; + v8_: int = id c6_; + v9_: int = id c6_; + v10_: int = id c2_; + br v3_ .b11_ .b12_; .b11_: c13_: int = const 4; v8_: int = id c13_; - v9_: int = id c2_; - v10_: int = id c3_; + v9_: int = id c6_; + v10_: int = id c2_; .b12_: v14_: int = id v8_; v15_: int = id v9_; - br v5_ .b16_ .b17_; + br v4_ .b16_ .b17_; .b16_: v18_: int = add v10_ v8_; v14_: int = id v18_; v15_: int = id v9_; .b17_: - v19_: int = add c2_ v14_; + v19_: int = add c6_ v14_; print v19_; -} +} \ No newline at end of file diff --git a/tests/snapshots/files__fib_recursive-optimize.snap b/tests/snapshots/files__fib_recursive-optimize.snap index e674c7e56..d6714b0ed 100644 --- a/tests/snapshots/files__fib_recursive-optimize.snap +++ b/tests/snapshots/files__fib_recursive-optimize.snap @@ -339,4 +339,4 @@ expression: visualization.result jmp .b38_; .b6_: print v5_; -} +} \ No newline at end of file diff --git a/tests/snapshots/files__gamma_condition_and-optimize.snap b/tests/snapshots/files__gamma_condition_and-optimize.snap index 7c5c9df1f..7e90cb098 100644 --- a/tests/snapshots/files__gamma_condition_and-optimize.snap +++ b/tests/snapshots/files__gamma_condition_and-optimize.snap @@ -6,7 +6,7 @@ expression: visualization.result .b1_: c2_: int = const 0; v3_: bool = lt v0 c2_; - v4_: bool = gt v0 c2_; + v4_: bool = lt c2_ v0; c5_: int = const 1; c6_: int = const 3; v7_: int = id c6_; @@ -21,4 +21,4 @@ expression: visualization.result v7_: int = id v11_; .b9_: print v7_; -} +} \ No newline at end of file diff --git a/tests/snapshots/files__if_dead_code_nested-optimize.snap b/tests/snapshots/files__if_dead_code_nested-optimize.snap index 9e48d1fac..75ea2ad08 100644 --- a/tests/snapshots/files__if_dead_code_nested-optimize.snap +++ b/tests/snapshots/files__if_dead_code_nested-optimize.snap @@ -31,7 +31,7 @@ expression: visualization.result print v18_; ret; .b8_: - v20_: bool = gt v0 c6_; + v20_: bool = lt c6_ v0; c21_: bool = const false; c22_: int = const 2; v23_: int = id c22_; @@ -39,7 +39,7 @@ expression: visualization.result v25_: int = id c4_; br v20_ .b26_ .b27_; .b26_: - v28_: bool = lt c5_ v0; + v28_: bool = gt v0 c5_; c29_: int = const 4; v30_: int = id c29_; v31_: bool = id c21_; @@ -61,4 +61,4 @@ expression: visualization.result print v19_; print v3_; print v18_; -} +} \ No newline at end of file diff --git a/tests/snapshots/files__sqrt-optimize.snap b/tests/snapshots/files__sqrt-optimize.snap index 0fec351e7..dd0c9576c 100644 --- a/tests/snapshots/files__sqrt-optimize.snap +++ b/tests/snapshots/files__sqrt-optimize.snap @@ -36,8 +36,8 @@ expression: visualization.result v28_: float = fadd v21_ v27_; v29_: float = fdiv v28_ v24_; v30_: float = fdiv v29_ v21_; - v31_: bool = fge v30_ v23_; - v32_: bool = fle v30_ v22_; + v31_: bool = fle v30_ v22_; + v32_: bool = fge v30_ v23_; v33_: bool = and v31_ v32_; v34_: bool = not v33_; v20_: float = id v20_; @@ -61,4 +61,4 @@ expression: visualization.result print v37_; jmp .b36_; .b38_: -} +} \ No newline at end of file From 63f05655c0d267fe97af46158c4ce64aa4ede8de Mon Sep 17 00:00:00 2001 From: zhiyuan yan Date: Fri, 28 Jun 2024 13:58:00 -0700 Subject: [PATCH 3/3] snapshot?? --- tests/snapshots/files__block-diamond-optimize.snap | 2 +- tests/snapshots/files__fib_recursive-optimize.snap | 2 +- tests/snapshots/files__gamma_condition_and-optimize.snap | 2 +- tests/snapshots/files__if_dead_code_nested-optimize.snap | 2 +- tests/snapshots/files__sqrt-optimize.snap | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/snapshots/files__block-diamond-optimize.snap b/tests/snapshots/files__block-diamond-optimize.snap index 02f3d9954..9263fd9ba 100644 --- a/tests/snapshots/files__block-diamond-optimize.snap +++ b/tests/snapshots/files__block-diamond-optimize.snap @@ -30,4 +30,4 @@ expression: visualization.result .b17_: v19_: int = add c6_ v14_; print v19_; -} \ No newline at end of file +} diff --git a/tests/snapshots/files__fib_recursive-optimize.snap b/tests/snapshots/files__fib_recursive-optimize.snap index d6714b0ed..e674c7e56 100644 --- a/tests/snapshots/files__fib_recursive-optimize.snap +++ b/tests/snapshots/files__fib_recursive-optimize.snap @@ -339,4 +339,4 @@ expression: visualization.result jmp .b38_; .b6_: print v5_; -} \ No newline at end of file +} diff --git a/tests/snapshots/files__gamma_condition_and-optimize.snap b/tests/snapshots/files__gamma_condition_and-optimize.snap index 7e90cb098..e55e8d259 100644 --- a/tests/snapshots/files__gamma_condition_and-optimize.snap +++ b/tests/snapshots/files__gamma_condition_and-optimize.snap @@ -21,4 +21,4 @@ expression: visualization.result v7_: int = id v11_; .b9_: print v7_; -} \ No newline at end of file +} diff --git a/tests/snapshots/files__if_dead_code_nested-optimize.snap b/tests/snapshots/files__if_dead_code_nested-optimize.snap index 75ea2ad08..e6ffbdca9 100644 --- a/tests/snapshots/files__if_dead_code_nested-optimize.snap +++ b/tests/snapshots/files__if_dead_code_nested-optimize.snap @@ -61,4 +61,4 @@ expression: visualization.result print v19_; print v3_; print v18_; -} \ No newline at end of file +} diff --git a/tests/snapshots/files__sqrt-optimize.snap b/tests/snapshots/files__sqrt-optimize.snap index dd0c9576c..c0f3bcce9 100644 --- a/tests/snapshots/files__sqrt-optimize.snap +++ b/tests/snapshots/files__sqrt-optimize.snap @@ -61,4 +61,4 @@ expression: visualization.result print v37_; jmp .b36_; .b38_: -} \ No newline at end of file +}