[fix]

misonijnik · Feb 20, 2024 · 753eaee · 753eaee
1 parent 591e020
commit 753eaee
Show file tree

Hide file tree

Showing 5 changed files with 47 additions and 7 deletions.
diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp
@@ -537,13 +537,6 @@ Term BitwuzlaBuilder::constructActual(ref<Expr> e, int *width_out) {
     Term left = construct(ce->getLeft(), width_out);
     Term right = construct(ce->getRight(), width_out);
     Term eq = eqExpr(left, right);
-    unsigned numKids = ce->getNumKids();
-    std::vector<Term> term_args;
-    term_args.reserve(numKids);
-
-    for (unsigned i = 0; i < numKids; ++i) {
-      term_args.push_back(construct(ce->getKid(i), 0));
-    }
 
     *width_out = ce->getWidth();
     return iteExpr(eq, left, null);

diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
@@ -748,6 +748,19 @@ MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) {
     break;
   }
 
+  case Expr::Convol: {
+    ConvolExpr *ce = cast<ConvolExpr>(e);
+
+    *width_out = ce->getWidth();
+    res = evaluate(
+        _solver,
+        metaSMT::logic::Ite(
+            construct(EqExpr::create(ce->getLeft(), ce->getRight()), 0),
+            construct(ce->getLeft(), width_out),
+            construct(ConstantExpr::create(0, ce->getWidth()), width_out)));
+    break;
+  }
+
   case Expr::Concat: {
     ConcatExpr *ce = cast<ConcatExpr>(e);
     assert(ce);

diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
@@ -627,6 +627,17 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     return res;
   }
 
+  case Expr::Convol: {
+    ConvolExpr *ce = cast<ConvolExpr>(e);
+    ExprHandle null = construct(ConstantExpr::create(0, ce->getWidth()));
+    ExprHandle left = construct(ce->getLeft(), width_out);
+    ExprHandle right = construct(ce->getRight(), width_out);
+    ExprHandle eq = eqExpr(left, right);
+
+    *width_out = ce->getWidth();
+    return vc_iteExpr(vc, eq, left, null);
+  }
+
   case Expr::Extract: {
     ExtractExpr *ee = cast<ExtractExpr>(e);
     ExprHandle src = construct(ee->expr, width_out);

diff --git a/lib/Solver/Z3BitvectorBuilder.cpp b/lib/Solver/Z3BitvectorBuilder.cpp
@@ -7,6 +7,7 @@
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
+#include "Z3Builder.h"
 #include "klee/Config/config.h"
 
 #ifdef ENABLE_Z3
@@ -339,6 +340,17 @@ Z3ASTHandle Z3BitvectorBuilder::constructActual(ref<Expr> e, int *width_out) {
     return iteExpr(cond, tExpr, fExpr);
   }
 
+  case Expr::Convol: {
+    ConvolExpr *ce = cast<ConvolExpr>(e);
+    Z3ASTHandle null = construct(ConstantExpr::create(0, ce->getWidth()));
+    Z3ASTHandle left = construct(ce->getLeft(), width_out);
+    Z3ASTHandle right = construct(ce->getRight(), width_out);
+    Z3ASTHandle eq = eqExpr(left, right);
+
+    *width_out = ce->getWidth();
+    return iteExpr(eq, left, null);
+  }
+
   case Expr::Concat: {
     ConcatExpr *ce = cast<ConcatExpr>(e);
     unsigned numKids = ce->getNumKids();

diff --git a/lib/Solver/Z3CoreBuilder.cpp b/lib/Solver/Z3CoreBuilder.cpp
@@ -266,6 +266,17 @@ Z3ASTHandle Z3CoreBuilder::constructActual(ref<Expr> e, int *width_out) {
     return iteExpr(cond, tExpr, fExpr);
   }
 
+  case Expr::Convol: {
+    ConvolExpr *ce = cast<ConvolExpr>(e);
+    Z3ASTHandle null = construct(ConstantExpr::create(0, ce->getWidth()));
+    Z3ASTHandle left = construct(ce->getLeft(), width_out);
+    Z3ASTHandle right = construct(ce->getRight(), width_out);
+    Z3ASTHandle eq = eqExpr(left, right);
+
+    *width_out = ce->getWidth();
+    return iteExpr(eq, left, null);
+  }
+
   case Expr::Concat: {
     ConcatExpr *ce = cast<ConcatExpr>(e);
     unsigned numKids = ce->getNumKids();