push slices into ops

cucapra · Nov 21, 2024 · 35b84f9 · 35b84f9
1 parent e80a033
commit 35b84f9
Show file tree

Hide file tree

Showing 3 changed files with 3,070 additions and 896 deletions.
diff --git a/src/expr/simplify.rs b/src/expr/simplify.rs
@@ -452,6 +452,25 @@ fn simplify_bv_slice(ctx: &mut Context, e: ExprRef, hi: WidthInt, lo: WidthInt)
         Expr::BVIte { cond, tru, fals } => {
             Some(ctx.build(|c| c.bv_ite(cond, c.slice(tru, hi, lo), c.slice(fals, hi, lo))))
         }
+        // slice of not
+        Expr::BVNot(e, _) => Some(ctx.build(|c| c.not(c.slice(e, hi, lo)))),
+        // slice of neg
+        Expr::BVNegate(e, _) if lo == 0 => Some(ctx.build(|c| c.negate(c.slice(e, hi, lo)))),
+        // slice of bit-wise ops
+        Expr::BVAnd(a, b, _) => Some(ctx.build(|c| c.and(c.slice(a, hi, lo), c.slice(b, hi, lo)))),
+        Expr::BVOr(a, b, _) => Some(ctx.build(|c| c.or(c.slice(a, hi, lo), c.slice(b, hi, lo)))),
+        Expr::BVXor(a, b, _) => Some(ctx.build(|c| c.xor(c.slice(a, hi, lo), c.slice(b, hi, lo)))),
+        // these ops have information flow from low to high bits
+        Expr::BVAdd(a, b, _) if lo == 0 => {
+            Some(ctx.build(|c| c.add(c.slice(a, hi, lo), c.slice(b, hi, lo))))
+        }
+        Expr::BVSub(a, b, _) if lo == 0 => {
+            Some(ctx.build(|c| c.sub(c.slice(a, hi, lo), c.slice(b, hi, lo))))
+        }
+        Expr::BVMul(a, b, _) if lo == 0 => {
+            Some(ctx.build(|c| c.mul(c.slice(a, hi, lo), c.slice(b, hi, lo))))
+        }
+
         _ => None,
     }
 }

diff --git a/tests/simplify.rs b/tests/simplify.rs
@@ -432,6 +432,40 @@ fn test_simplify_concat_of_adjacent_slices() {
     ts("concat(a:bv<32>[31:19], a[18:0])", "a:bv<32>");
 }
 
-// TODO: add slice simplifications: https://github.com/ekiwi/maltese-private/blob/main/test/maltese/smt/SMTSimplifierSliceSpec.scala
+#[test]
+fn test_simplify_slice_of_op() {
+    // push into not
+    ts("not(a:bv<32>)[20:1]", "not(a:bv<32>[20:1])");
+    ts("not(a:bv<32>)[15:0]", "not(a:bv<32>[15:0])");
+
+    // push slice into neg, which we can only for msbs
+    ts("neg(a:bv<32>)[20:1]", "neg(a:bv<32>)[20:1]");
+    ts("neg(a:bv<32>)[15:0]", "neg(a:bv<32>[15:0])");
+
+    // push into bit-wise and arithmetic binary ops
+    for op in ["and", "or", "xor", "add", "sub", "mul"] {
+        ts(
+            &format!("{op}(a:bv<32>, b:bv<32>)[30:0]"),
+            &format!("{op}(a:bv<32>[30:0], b:bv<32>[30:0])"),
+        );
+        if op == "and" || op == "or" || op == "xor" {
+            ts(
+                &format!("{op}(a:bv<32>, b:bv<32>)[30:2]"),
+                &format!("{op}(a:bv<32>[30:2], b:bv<32>[30:2])"),
+            );
+        } else {
+            ts(
+                &format!("{op}(a:bv<32>, b:bv<32>)[30:2]"),
+                &format!("{op}(a:bv<32>, b:bv<32>)[30:2]"),
+            );
+        }
+
+        // examples that show up in actual code
+        ts(
+            &format!("{op}(zext(a:bv<32>, 1), zext(b:bv<32>, 1))[31:0]"),
+            &format!("{op}(a:bv<32>, b:bv<32>)"),
+        );
+    }
+}
 
 // TODO: add missing literals simplifications: https://github.com/ekiwi/maltese-private/blob/main/test/maltese/smt/SMTSimplifierLiteralsSpec.scala