From d7eb479a1e8223c2af52b152c835d96df2f121d3 Mon Sep 17 00:00:00 2001 From: Yihong Zhang Date: Thu, 30 May 2024 15:13:40 -0700 Subject: [PATCH 1/2] fix ternary operator rules --- dag_in_context/src/type_analysis.egg | 14 +++++++++++++- dag_in_context/src/utility/add_context.egg | 6 ++++++ dag_in_context/src/utility/drop_at.egg | 8 ++++++++ dag_in_context/src/utility/expr_size.egg | 6 +++++- dag_in_context/src/utility/subst.egg | 8 ++++++++ 5 files changed, 40 insertions(+), 2 deletions(-) diff --git a/dag_in_context/src/type_analysis.egg b/dag_in_context/src/type_analysis.egg index c22bde6d7..72706aaa4 100644 --- a/dag_in_context/src/type_analysis.egg +++ b/dag_in_context/src/type_analysis.egg @@ -73,6 +73,18 @@ (HasArgType b ty)) ((HasArgType lhs ty)) :ruleset type-analysis) +(rule ((= lhs (Top _ a b c)) + (HasArgType a ty)) + ((HasArgType lhs ty)) + :ruleset type-analysis) +(rule ((= lhs (Top _ a b c)) + (HasArgType b ty)) + ((HasArgType lhs ty)) + :ruleset type-analysis) +(rule ((= lhs (Top _ a b c)) + (HasArgType c ty)) + ((HasArgType lhs ty)) + :ruleset type-analysis) (rule ((= lhs (Get e _)) (HasArgType e ty)) ((HasArgType lhs ty)) @@ -285,7 +297,7 @@ (rule ( (= lhs (Top (Write) ptr val state)) (HasType ptr (Base (PointerT ty))) - (HasType val (Base t)) ; TODO need to support pointers to pointers + (HasType val (Base ty)) ; TODO need to support pointers to pointers ) ((HasType lhs (Base (StateT)))) ; Write returns () :ruleset type-analysis) diff --git a/dag_in_context/src/utility/add_context.egg b/dag_in_context/src/utility/add_context.egg index 58e76f65c..ff601a7b5 100644 --- a/dag_in_context/src/utility/add_context.egg +++ b/dag_in_context/src/utility/add_context.egg @@ -36,6 +36,12 @@ ;; ######################################### Operators +(rewrite (AddContext ctx (Top op c1 c2 c3)) + (Top op + (AddContext ctx c1) + (AddContext ctx c2) + (AddContext ctx c3)) + :ruleset context) (rewrite (AddContext ctx (Bop op c1 c2)) (Bop op (AddContext ctx c1) diff --git a/dag_in_context/src/utility/drop_at.egg b/dag_in_context/src/utility/drop_at.egg index 91f24a0db..69992490b 100644 --- a/dag_in_context/src/utility/drop_at.egg +++ b/dag_in_context/src/utility/drop_at.egg @@ -38,6 +38,14 @@ :ruleset drop) ;; Operators +(rule ((= lhs (DropAtInternal newty newctx idx (Top op c1 c2 c3))) + (ExprIsResolved (Top op c1 c2 c3))) + ((DelayedDropUnion lhs (Top op + (DropAtInternal newty newctx idx c1) + (DropAtInternal newty newctx idx c2) + (DropAtInternal newty newctx idx c3)))) + :ruleset drop) + (rule ((= lhs (DropAtInternal newty newctx idx (Bop op c1 c2))) (ExprIsResolved (Bop op c1 c2))) ((DelayedDropUnion lhs (Bop op diff --git a/dag_in_context/src/utility/expr_size.egg b/dag_in_context/src/utility/expr_size.egg index 4f80805e2..664605698 100644 --- a/dag_in_context/src/utility/expr_size.egg +++ b/dag_in_context/src/utility/expr_size.egg @@ -9,6 +9,10 @@ (rule ((= expr (Const n ty assum))) ((set (Expr-size expr) 1)) :ruleset always-run) +(rule ((= expr (Top op x y z)) + (= sum (+ (Expr-size z) (+ (Expr-size y) (Expr-size x))))) + ((set (Expr-size expr) (+ sum 1))) :ruleset always-run) + (rule ((= expr (Bop op x y)) (= sum (+ (Expr-size y) (Expr-size x)))) ((set (Expr-size expr) (+ sum 1))) :ruleset always-run) @@ -59,4 +63,4 @@ (rule ((= expr (Alloc id e state ty)) ;; do state edge's expr should be counted? (= sum (Expr-size e))) - ((set (Expr-size expr) (+ sum 1))) :ruleset always-run) \ No newline at end of file + ((set (Expr-size expr) (+ sum 1))) :ruleset always-run) diff --git a/dag_in_context/src/utility/subst.egg b/dag_in_context/src/utility/subst.egg index e6fc57017..00d34d476 100644 --- a/dag_in_context/src/utility/subst.egg +++ b/dag_in_context/src/utility/subst.egg @@ -44,6 +44,14 @@ :ruleset subst) ;; Operators +(rule ((= lhs (Subst assum to (Top op c1 c2 c3))) + (ExprIsResolved (Top op c1 c2 c3))) + ((DelayedSubstUnion lhs + (Top op (Subst assum to c1) + (Subst assum to c2) + (Subst assum to c3)))) + :ruleset subst) + (rule ((= lhs (Subst assum to (Bop op c1 c2))) (ExprIsResolved (Bop op c1 c2))) ((DelayedSubstUnion lhs From f011b91323f371c175bfb8159358e5e32bb4af2a Mon Sep 17 00:00:00 2001 From: Yihong Zhang Date: Thu, 30 May 2024 15:20:08 -0700 Subject: [PATCH 2/2] snapshot --- tests/snapshots/files__gamma_condition_and-optimize.snap | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/snapshots/files__gamma_condition_and-optimize.snap b/tests/snapshots/files__gamma_condition_and-optimize.snap index 7c5c9df1f..e55e8d259 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_;