simplify concat of adjacent slices

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

Hide file tree

Showing 2 changed files with 37 additions and 13 deletions.
diff --git a/src/expr/simplify.rs b/src/expr/simplify.rs
@@ -374,21 +374,39 @@ fn simplify_bv_sign_ext(ctx: &mut Context, e: ExprRef, by: WidthInt) -> Option<E
 }
 
 fn simplify_bv_concat(ctx: &mut Context, a: ExprRef, b: ExprRef) -> Option<ExprRef> {
-    match *ctx.get(a) {
+    match (ctx.get(a).clone(), ctx.get(b).clone()) {
         // normalize concat to be right recursive
-        Expr::BVConcat(a_a, a_b, _) => Some(ctx.build(|c| c.concat(a_a, c.concat(a_b, b)))),
-        Expr::BVLiteral(va) => match *ctx.get(b) {
-            Expr::BVLiteral(vb) => Some(ctx.bv_lit(&va.get(ctx).concat(&vb.get(ctx)))),
-            Expr::BVConcat(b_a, b_b, _) => {
-                if let Expr::BVLiteral(v_b_a) = *ctx.get(b_a) {
-                    let lit = ctx.bv_lit(&va.get(ctx).concat(&v_b_a.get(ctx)));
-                    Some(ctx.concat(lit, b_b))
-                } else {
-                    None
-                }
+        (Expr::BVConcat(a_a, a_b, _), _) => Some(ctx.build(|c| c.concat(a_a, c.concat(a_b, b)))),
+        (Expr::BVLiteral(va), Expr::BVLiteral(vb)) => {
+            Some(ctx.bv_lit(&va.get(ctx).concat(&vb.get(ctx))))
+        }
+        (Expr::BVLiteral(va), Expr::BVConcat(b_a, b_b, _)) => {
+            if let Expr::BVLiteral(v_b_a) = *ctx.get(b_a) {
+                let lit = ctx.bv_lit(&va.get(ctx).concat(&v_b_a.get(ctx)));
+                Some(ctx.concat(lit, b_b))
+            } else {
+                None
             }
-            _ => None,
-        },
+        }
+        (
+            Expr::BVSlice {
+                e: a,
+                hi: hi_a,
+                lo: lo_a,
+            },
+            Expr::BVSlice {
+                e: b,
+                hi: hi_b,
+                lo: lo_b,
+            },
+        ) => {
+            // slice of the same thing + adjacent
+            if a == b && lo_a == hi_b + 1 {
+                Some(ctx.slice(a, hi_a, lo_b))
+            } else {
+                None
+            }
+        }
         _ => None,
     }
 }

diff --git a/tests/simplify.rs b/tests/simplify.rs
@@ -426,6 +426,12 @@ fn test_slice_of_ite() {
     );
 }
 
+#[test]
+fn test_simplify_concat_of_adjacent_slices() {
+    ts("concat(a:bv<32>[20:19], a[18:0])", "a:bv<32>[20:0]");
+    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
 
 // TODO: add missing literals simplifications: https://github.com/ekiwi/maltese-private/blob/main/test/maltese/smt/SMTSimplifierLiteralsSpec.scala