Add abs and make Oliver's example work

Cargo.toml

@@ -23,14 +23,14 @@ rpds = "1.1.0"
 
 syn = { version = "2.0", features = ["full", "extra-traits"] }
 # currently using the uwplse/bril fork of bril, on eggcc-main
-bril2json = { git = "https://github.com/uwplse/bril", rev = "f303a7d384f21a891d0215dc47e5ea947f014cf5" }
-brilirs = { git = "https://github.com/uwplse/bril", rev = "f303a7d384f21a891d0215dc47e5ea947f014cf5" }
-bril-rs = { git = "https://github.com/uwplse/bril", rev = "f303a7d384f21a891d0215dc47e5ea947f014cf5" }
-brilift = { git = "https://github.com/uwplse/bril", rev = "f303a7d384f21a891d0215dc47e5ea947f014cf5" }
-rs2bril = { git = "https://github.com/uwplse/bril", rev = "f303a7d384f21a891d0215dc47e5ea947f014cf5" ,features = [
+bril2json = { git = "https://github.com/uwplse/bril", rev = "1f12195d043dccee1815cf6a1d88bf91b686d426" }
+brilirs = { git = "https://github.com/uwplse/bril", rev = "1f12195d043dccee1815cf6a1d88bf91b686d426" }
+bril-rs = { git = "https://github.com/uwplse/bril", rev = "1f12195d043dccee1815cf6a1d88bf91b686d426" }
+brilift = { git = "https://github.com/uwplse/bril", rev = "1f12195d043dccee1815cf6a1d88bf91b686d426" }
+rs2bril = { git = "https://github.com/uwplse/bril", rev = "1f12195d043dccee1815cf6a1d88bf91b686d426" ,features = [
   "import",
 ] }
-brillvm = { git = "https://github.com/uwplse/bril", rev = "f303a7d384f21a891d0215dc47e5ea947f014cf5" }
+brillvm = { git = "https://github.com/uwplse/bril", rev = "1f12195d043dccee1815cf6a1d88bf91b686d426" }
 
 ordered-float = "3.7.0"
 serde_json = "1.0.103"

dag_in_context/src/ast.rs

@@ -86,6 +86,10 @@ macro_rules! tuplev {
 }
 pub use tuplev;
 
+pub fn abs(l: RcExpr) -> RcExpr {
+    RcExpr::new(Expr::Uop(UnaryOp::Abs, l))
+}
+
 pub fn add(l: RcExpr, r: RcExpr) -> RcExpr {
     RcExpr::new(Expr::Bop(BinaryOp::Add, l, r))
 }

dag_in_context/src/from_egglog.rs

@@ -200,6 +200,7 @@ impl<'a> FromEgglog<'a> {
     fn uop_from_egglog(&mut self, uop: Term) -> UnaryOp {
         match_term_app!(uop.clone();
         {
+          ("Abs", []) => UnaryOp::Abs,
           ("Not", []) => UnaryOp::Not,
           _ => panic!("Invalid unary op: {:?}", uop),
         })

dag_in_context/src/greedy_dag_extractor.rs

@@ -996,7 +996,7 @@ impl CostModel for DefaultCostModel {
             "Base" | "TupleT" | "TNil" | "TCons" => 0.,
             "Int" | "Bool" | "Float" => 0.,
             // Algebra
-            "Add" | "PtrAdd" | "Sub" | "And" | "Or" | "Not" | "Shl" | "Shr" => 10.,
+            "Abs" | "Add" | "PtrAdd" | "Sub" | "And" | "Or" | "Not" | "Shl" | "Shr" => 10.,
             "FAdd" | "FSub" | "Fmax" | "Fmin" => 50.,
             "Mul" => 30.,
             "FMul" => 150.,

dag_in_context/src/interpreter.rs

@@ -334,8 +334,10 @@ impl<'a> VirtualMachine<'a> {
     }
 
     fn interpret_uop(&mut self, uop: &UnaryOp, e: &RcExpr, arg: &Value) -> Value {
+        let get_int = |e: &RcExpr, vm: &mut Self| vm.interp_int_expr(e, arg);
         match uop {
             UnaryOp::Not => Const(Constant::Bool(!self.interp_bool_expr(e, arg))),
+            UnaryOp::Abs => Const(Constant::Int(get_int(e, self).abs())),
         }
     }
 

dag_in_context/src/interval_analysis.egg

@@ -164,6 +164,39 @@
       :ruleset interval-analysis)
 
 ; negative * negative is positive
+(rule (
+        (= lhs (Bop (Mul) x y))
+        (= (IntB hi-x) (hi-bound x))
+        (= (IntB hi-y) (hi-bound y))
+        (< hi-x 0)
+        (< hi-y 0) 
+      )
+      ((set (lo-bound lhs) (IntB 1)))
+      :ruleset interval-analysis)
+
+; negative * positive is negative
+(rule (
+        (= lhs (Bop (Mul) x y))
+        (= (IntB hi-x) (hi-bound x))
+        (= (IntB lo-y) (lo-bound y))
+        (< hi-x 0) ; x < 0 (x is negative)
+        (> lo-y 0) ; y > 0 (y is positive)
+      )
+      ((set (hi-bound lhs) (IntB -1)))
+      :ruleset interval-analysis)
+
+; positive * positive is positive
+(rule (
+        (= lhs (Bop (Mul) x y))
+        (= (IntB lo-x) (lo-bound x))
+        (= (IntB lo-y) (lo-bound y))
+        (> lo-x 0)
+        (> lo-y 0)
+      )
+      ((set (lo-bound lhs) (IntB 1)))
+      :ruleset interval-analysis)
+
+; non-positive * non-positive is non-negative
 (rule (
         (= lhs (Bop (Mul) x y))
         (= (IntB hi-x) (hi-bound x))
@@ -174,18 +207,18 @@
       ((set (lo-bound lhs) (IntB 0)))
       :ruleset interval-analysis)
 
-; negative * positive is negative
+; non-positive * non-negative is non-positive
 (rule (
         (= lhs (Bop (Mul) x y))
         (= (IntB hi-x) (hi-bound x))
         (= (IntB lo-y) (lo-bound y))
-        (<= hi-x 0) ; x <= 0 (x is negative)
-        (>= lo-y 0) ; y >= 0 (y is positive)
+        (<= hi-x 0) ; x <= 0 (x is non-positive)
+        (>= lo-y 0) ; y >= 0 (y is non-negative)
       )
       ((set (hi-bound lhs) (IntB 0)))
       :ruleset interval-analysis)
 
-; positive * positive is positive
+; non-negative * non-negative is non-negative
 (rule (
         (= lhs (Bop (Mul) x y))
         (= (IntB lo-x) (lo-bound x))
@@ -214,6 +247,35 @@
       ((set (hi-bound lhs) (BoolB (bool-< la hb))))
       :ruleset interval-analysis)
 
+; Abs
+
+; absolute value is non-negative
+(rule (
+        (= lhs (Uop (Abs) x))
+      )
+      ((set (lo-bound lhs) (IntB 0)))
+      :ruleset interval-analysis)
+
+; abs(x) = x if x >= 0
+(rule (
+        (= lhs (Uop (Abs) x))
+        (= (IntB lx) (lo-bound x))
+        (>= lx 0)
+      )
+      ((union lhs x))
+      :ruleset interval-analysis)
+
+; abs(x) = -x if x <= 0
+(rule (
+        (= lhs (Uop (Abs) x))
+        (= (IntB hx) (hi-bound x))
+        (<= hx 0)
+        (HasArgType lhs ty)
+        (ContextOf lhs ctx)
+      )
+      ((union lhs (Bop (Sub) (Const (Int 0) ty ctx) x)))
+      :ruleset interval-analysis)
+
 ; =================================
 ; Conditionals
 ; =================================
@@ -282,7 +344,7 @@
         (HasType inputs ty)
       )
       ; expr < value was true, so we know expr is at most (hi-bound value) - 1
-      ((set (hi-bound (Get ctx i)) (IntB (- v 1)))) 
+      ((set (hi-bound (Get ctx i)) (IntB (- v 1))))
       :ruleset interval-analysis)
 (rule (
         ; expr < value

dag_in_context/src/optimizations/peepholes.egg

@@ -20,3 +20,17 @@
 (rewrite (Bop (Or) e (Const (Bool false) ty ctx)) e :ruleset peepholes)
 (rewrite (Bop (Or) (Const (Bool true) ty ctx) e) (Const (Bool true) ty ctx) :ruleset peepholes)
 (rewrite (Bop (Or) e (Const (Bool true) ty ctx)) (Const (Bool true) ty ctx) :ruleset peepholes)
+
+(rule (
+        (= expr (Bop (Sub) x x))
+        (HasArgType expr ty)
+        (ContextOf expr ctx)
+      )
+      ((union expr (Const (Int 0) ty ctx)))
+      :ruleset peepholes)
+
+; (x - y) + z => x + (z - y)
+(rewrite (Bop (Add) (Bop (Sub) x y) z) (Bop (Add) x (Bop (Sub) z y)) :ruleset peepholes)
+
+; (a + b) - c => a + (b - c)
+(rewrite (Bop (Sub) (Bop (Add) a b) c) (Bop (Add) a (Bop (Sub) b c)) :ruleset peepholes)

dag_in_context/src/optimizations/purity_analysis.egg

@@ -32,6 +32,7 @@
 (BinaryOpIsPure (Or))
 (BinaryOpIsPure (PtrAdd))
 (UnaryOpIsPure (Not))
+(UnaryOpIsPure (Abs))
 
 (rule ((Function _name _tyin _tyout _out) (ExprIsPure _out))
         ((ExprIsPure (Function _name _tyin _tyout _out)))

dag_in_context/src/pretty_print.rs

@@ -662,8 +662,9 @@ impl TernaryOp {
 
 impl UnaryOp {
     pub fn to_ast(&self) -> String {
-        use schema::UnaryOp::Not;
+        use schema::UnaryOp::{Abs, Not};
         match self {
+            Abs => "abs".into(),
             Not => "not".into(),
         }
     }

dag_in_context/src/schema.egg

@@ -130,6 +130,7 @@
   ; given a pointer and state edge, frees the whole memory region at the pointer
   (Free))
 (datatype UnaryOp
+  (Abs)
   (Not))
 
 ; Operators

dag_in_context/src/schema.rs

@@ -73,6 +73,7 @@ pub enum BinaryOp {
 
 #[derive(Debug, Clone, PartialEq, Eq, EnumIter, PartialOrd, Ord)]
 pub enum UnaryOp {
+    Abs,
     Not,
 }
 

dag_in_context/src/schema_helpers.rs

@@ -100,6 +100,7 @@ impl UnaryOp {
     pub(crate) fn name(&self) -> &'static str {
         use UnaryOp::*;
         match self {
+            Abs => "Abs",
             Not => "Not",
         }
     }
@@ -861,6 +862,7 @@ impl BinaryOp {
 impl UnaryOp {
     pub(crate) fn types(&self) -> Option<(Type, Type)> {
         match self {
+            UnaryOp::Abs => Some((base(intt()), base(intt()))),
             UnaryOp::Not => Some((base(boolt()), base(boolt()))),
         }
     }

dag_in_context/src/type_analysis.egg

@@ -186,6 +186,16 @@
       ((ExpectType e (Base (BoolT)) "(Not)"))
       :ruleset type-analysis)
 
+(rule (
+        (= lhs (Uop (Abs) e))
+        (HasType e (Base (IntT)))
+      )
+      ((HasType lhs (Base (IntT))))
+      :ruleset type-analysis)
+(rule ((= lhs (Uop (Abs) e)))
+      ((ExpectType e (Base (IntT)) "(Abs)"))
+      :ruleset type-analysis)
+
 
 (rule (
         (= lhs (Bop (Print) e state))

src/rvsdg/from_dag.rs

@@ -194,12 +194,14 @@ fn effect_op_from_binary_op(bop: BinaryOp) -> Option<EffectOps> {
 
 fn value_op_from_unary_op(uop: UnaryOp) -> Option<ValueOps> {
     match uop {
+        UnaryOp::Abs => Some(ValueOps::Abs),
         UnaryOp::Not => Some(ValueOps::Not),
     }
 }
 
 fn effect_op_from_unary_op(uop: UnaryOp) -> Option<EffectOps> {
     match uop {
+        UnaryOp::Abs => None,
         UnaryOp::Not => None,
     }
 }

src/rvsdg/to_dag.rs

@@ -263,6 +263,7 @@ impl<'a> DagTranslator<'a> {
                     (ValueOps::And, [a, b]) => and(a.clone(), b.clone()),
                     (ValueOps::Or, [a, b]) => or(a.clone(), b.clone()),
                     (ValueOps::Not, [a]) => not(a.clone()),
+                    (ValueOps::Abs, [a]) => abs(a.clone()),
 
                     (ValueOps::PtrAdd, [a, b]) => ptradd(a.clone(), b.clone()),
                     (ValueOps::Load, [a, b]) => load(a.clone(), b.clone()),