HAL  v4.5.0-83-g30c8f0afc
The Hardware Analyzer - a comprehensive reverse engineering and manipulation framework for gate-level netlists.
simplification.cpp
Go to the documentation of this file.
1 #include "z3_utils/simplification.h"
2 
3 #include "hal_core/netlist/boolean_function.h"
4 #include "hal_core/utilities/log.h"
5 #include "z3_utils/z3_utils.h"
6 
7 #include <deque>
8 
9 namespace hal
10 {
11  namespace BV_ConstantPropagation
12  {
20  BooleanFunction And(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
21  {
22  std::vector<BooleanFunction::Value> simplified;
23  simplified.reserve(p0.size());
24  for (auto i = 0u; i < p0.size(); i++)
25  {
26  if ((p0[i] == 0) || (p1[i] == 0))
27  {
28  simplified.emplace_back(BooleanFunction::Value::ZERO);
29  }
30  else if ((p0[i] == 1) && (p1[i] == 1))
31  {
32  simplified.emplace_back(BooleanFunction::Value::ONE);
33  }
34  else
35  {
36  simplified.emplace_back(BooleanFunction::Value::X);
37  }
38  }
39  return BooleanFunction::Const(simplified);
40  }
41 
49  BooleanFunction Or(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
50  {
51  std::vector<BooleanFunction::Value> simplified;
52  simplified.reserve(p0.size());
53  for (auto i = 0u; i < p0.size(); i++)
54  {
55  if ((p0[i] == 0) && (p1[i] == 0))
56  {
57  simplified.emplace_back(BooleanFunction::Value::ZERO);
58  }
59  else if ((p0[i] == 1) || (p1[i] == 1))
60  {
61  simplified.emplace_back(BooleanFunction::Value::ONE);
62  }
63  else
64  {
65  simplified.emplace_back(BooleanFunction::Value::X);
66  }
67  }
68  return BooleanFunction::Const(simplified);
69  }
70 
77  BooleanFunction Not(const std::vector<BooleanFunction::Value>& p)
78  {
79  std::vector<BooleanFunction::Value> simplified;
80  simplified.reserve(p.size());
81  for (const auto& value : p)
82  {
83  if (value == BooleanFunction::Value::ZERO)
84  {
85  simplified.emplace_back(BooleanFunction::Value::ONE);
86  }
87  else if (value == BooleanFunction::Value::ONE)
88  {
89  simplified.emplace_back(BooleanFunction::Value::ZERO);
90  }
91  else
92  {
93  simplified.emplace_back(value);
94  }
95  }
96  return BooleanFunction::Const(simplified);
97  }
98 
106  BooleanFunction Xor(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
107  {
108  std::vector<BooleanFunction::Value> simplified;
109  simplified.reserve(p0.size());
110  for (auto i = 0u; i < p0.size(); i++)
111  {
112  if (((p0[i] == 0) && (p1[i] == 1)) || ((p0[i] == 1) && (p1[i] == 0)))
113  {
114  simplified.emplace_back(BooleanFunction::Value::ONE);
115  }
116  else if (((p0[i] == 0) && (p1[i] == 0)) || ((p0[i] == 1) && (p1[i] == 1)))
117  {
118  simplified.emplace_back(BooleanFunction::Value::ZERO);
119  }
120  else
121  {
122  simplified.emplace_back(BooleanFunction::Value::X);
123  }
124  }
125  return BooleanFunction::Const(simplified);
126  }
127 
135  BooleanFunction Add(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
136  {
137  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
138  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
139  {
140  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
141  }
142 
143  std::vector<BooleanFunction::Value> simplified;
144  simplified.reserve(p0.size());
145  auto carry = BooleanFunction::Value::ZERO;
146  for (auto i = 0u; i < p0.size(); i++)
147  {
148  auto res = p0[i] + p1[i] + carry;
149  simplified.emplace_back(static_cast<BooleanFunction::Value>(res & 0x1));
150  carry = static_cast<BooleanFunction::Value>(res >> 1);
151  }
152  return BooleanFunction::Const(simplified);
153  }
154 
162  BooleanFunction Sub(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
163  {
164  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
165  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
166  {
167  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
168  }
169 
170  std::vector<BooleanFunction::Value> simplified;
171  simplified.reserve(p0.size());
172  auto carry = BooleanFunction::Value::ONE;
173  for (auto i = 0u; i < p0.size(); i++)
174  {
175  auto res = p0[i] + !(p1[i]) + carry;
176  simplified.emplace_back(static_cast<BooleanFunction::Value>(res & 0x1));
177  carry = static_cast<BooleanFunction::Value>(res >> 1);
178  }
179  return BooleanFunction::Const(simplified);
180  }
181 
189  BooleanFunction Mul(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
190  {
191  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
192  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
193  {
194  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
195  }
196 
197  auto bitsize = p0.size();
198  std::vector<BooleanFunction::Value> simplified(bitsize, BooleanFunction::Value::ZERO);
199  for (auto i = 0u; i < bitsize; i++)
200  {
201  auto carry = BooleanFunction::Value::ZERO;
202  for (auto j = 0u; j < bitsize - i; j++)
203  {
204  auto res = simplified[i + j] + (p0[i] & p1[j]) + carry;
205  simplified[i + j] = static_cast<BooleanFunction::Value>(res & 0x1);
206  carry = static_cast<BooleanFunction::Value>(res >> 1);
207  }
208  }
209  return BooleanFunction::Const(simplified);
210  }
211 
219  BooleanFunction Sle(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
220  {
221  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
222  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
223  {
224  return BooleanFunction::Const({BooleanFunction::Value::X});
225  }
226 
227  auto msb_p0 = p0.back();
228  auto msb_p1 = p1.back();
229  if (msb_p0 == BooleanFunction::Value::ONE && msb_p1 == BooleanFunction::Value::ZERO)
230  {
231  return BooleanFunction::Const(1, 1);
232  }
233  else if (msb_p0 == BooleanFunction::Value::ZERO && msb_p1 == BooleanFunction::Value::ONE)
234  {
235  return BooleanFunction::Const(0, 1);
236  }
237 
238  std::vector<BooleanFunction::Value> simplified;
239  u8 carry = 1;
240  u8 neq = 0;
241  u8 res = 0;
242  for (auto i = 0u; i < p0.size(); i++)
243  {
244  res = p0[i] + !(p1[i]) + carry;
245  carry = res >> 1;
246  neq |= res & 1;
247  }
248 
249  return BooleanFunction::Const({static_cast<BooleanFunction::Value>((res & 1) | !neq)});
250  }
251 
259  BooleanFunction Slt(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
260  {
261  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
262  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
263  {
264  return BooleanFunction::Const({BooleanFunction::Value::X});
265  }
266 
267  auto msb_p0 = p0.back();
268  auto msb_p1 = p1.back();
269  if (msb_p0 == BooleanFunction::Value::ONE && msb_p1 == BooleanFunction::Value::ZERO)
270  {
271  return BooleanFunction::Const(1, 1);
272  }
273  else if (msb_p0 == BooleanFunction::Value::ZERO && msb_p1 == BooleanFunction::Value::ONE)
274  {
275  return BooleanFunction::Const(0, 1);
276  }
277 
278  std::vector<BooleanFunction::Value> simplified;
279  u8 res = 0;
280  u8 carry = 1;
281  for (auto i = 0u; i < p0.size(); i++)
282  {
283  res = p0[i] + !(p1[i]) + carry;
284  carry = (res >> 1) & 1;
285  }
286 
287  return BooleanFunction::Const({static_cast<BooleanFunction::Value>(res & 1)});
288  }
289 
297  BooleanFunction Ule(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
298  {
299  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
300  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
301  {
302  return BooleanFunction::Const({BooleanFunction::Value::X});
303  }
304 
305  for (i32 i = p0.size() - 1; i >= 0; i--)
306  {
307  if (p0[i] == BooleanFunction::Value::ONE && p1[i] == BooleanFunction::Value::ZERO)
308  {
309  return BooleanFunction::Const(0, 1);
310  }
311  else if (p0[i] == BooleanFunction::Value::ZERO && p1[i] == BooleanFunction::Value::ONE)
312  {
313  return BooleanFunction::Const(1, 1);
314  }
315  }
316  return BooleanFunction::Const(1, 1);
317  }
318 
326  BooleanFunction Ult(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
327  {
328  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
329  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
330  {
331  return BooleanFunction::Const({BooleanFunction::Value::X});
332  }
333 
334  for (i32 i = p0.size() - 1; i >= 0; i--)
335  {
336  if (p0[i] == BooleanFunction::Value::ONE && p1[i] == BooleanFunction::Value::ZERO)
337  {
338  return BooleanFunction::Const(0, 1);
339  }
340  else if (p0[i] == BooleanFunction::Value::ZERO && p1[i] == BooleanFunction::Value::ONE)
341  {
342  return BooleanFunction::Const(1, 1);
343  }
344  }
345  return BooleanFunction::Const(0, 1);
346  }
347 
356  BooleanFunction Ite(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1, const std::vector<BooleanFunction::Value>& p2)
357  {
358  if (p0.front() == BooleanFunction::Value::ONE)
359  {
360  return BooleanFunction::Const(p1);
361  }
362  else if (p0.front() == BooleanFunction::Value::ZERO)
363  {
364  return BooleanFunction::Const(p2);
365  }
366  else
367  {
368  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
369  }
370  }
371 
379  Result<BooleanFunction> constant_propagation(const BooleanFunction::Node& node, std::vector<BooleanFunction>&& p)
380  {
381  std::vector<std::vector<BooleanFunction::Value>> values;
382  for (const auto& parameter : p)
383  {
384  values.emplace_back(parameter.get_top_level_node().constant);
385  }
386 
387  switch (node.type)
388  {
389  case BooleanFunction::NodeType::And:
390  return OK(And(values[0], values[1]));
391  case BooleanFunction::NodeType::Or:
392  return OK(Or(values[0], values[1]));
393  case BooleanFunction::NodeType::Not:
394  return OK(Not(values[0]));
395  case BooleanFunction::NodeType::Xor:
396  return OK(Xor(values[0], values[1]));
397  case BooleanFunction::NodeType::Add:
398  return OK(Add(values[0], values[1]));
399  case BooleanFunction::NodeType::Sub:
400  return OK(Sub(values[0], values[1]));
401  case BooleanFunction::NodeType::Mul:
402  return OK(Mul(values[0], values[1]));
403 
404  case BooleanFunction::NodeType::Sle:
405  // TODO implement for z3 where Boolean and bitvector sort exist
406  return OK(BooleanFunction());
407  case BooleanFunction::NodeType::Slt:
408  // TODO implement for z3 where Boolean and bitvector sort exist
409  return OK(BooleanFunction());
410  case BooleanFunction::NodeType::Ule:
411  // TODO implement for z3 where Boolean and bitvector sort exist
412  return OK(BooleanFunction());
413  case BooleanFunction::NodeType::Ult:
414  // TODO implement for z3 where Boolean and bitvector sort exist
415  return OK(BooleanFunction());
416  case BooleanFunction::NodeType::Ite:
417  // TODO implement for z3 where Boolean and bitvector sort exist
418  return OK(BooleanFunction());
419  case BooleanFunction::NodeType::Eq:
420  // TODO implement for z3 where Boolean and bitvector sort exist
421  return OK(BooleanFunction());
422  case BooleanFunction::NodeType::Zext:
423  // TODO implement for z3 where indices are not part of the parameters
424  return OK(BooleanFunction());
425  case BooleanFunction::NodeType::Sext:
426  // TODO implement for z3 where indices are not part of the parameters
427  return OK(BooleanFunction());
428  case BooleanFunction::NodeType::Slice:
429  // TODO implement for z3 where indices are not part of the parameters
430  return OK(BooleanFunction());
431  case BooleanFunction::NodeType::Concat:
432  // TODO implement for z3 where indices are not part of the parameters
433  return OK(BooleanFunction());
434  case BooleanFunction::NodeType::Sdiv:
435  // TODO implement
436  case BooleanFunction::NodeType::Udiv:
437  // TODO implement
438  case BooleanFunction::NodeType::Srem:
439  // TODO implement
440  case BooleanFunction::NodeType::Urem:
441  // TODO implement
442  default:
443  return ERR("could not propagate constants: not implemented for given node type");
444  }
445  }
446 
447  } // namespace BV_ConstantPropagation
448 
449  namespace
450  {
451 
455  bool is_x_y(const z3::expr& x, const z3::expr& y)
456  {
457  if (x.id() == y.id())
458  {
459  return true;
460  }
461 
462  if (z3::eq(x, y))
463  {
464  return true;
465  }
466 
467  return false;
468  }
469 
473  bool is_x_not_y(const z3::expr& x, const z3::expr& y)
474  {
475  const auto x_kind = x.decl().decl_kind();
476  const auto y_kind = y.decl().decl_kind();
477 
478  if (x_kind == Z3_OP_BNOT || x_kind == Z3_OP_NOT)
479  {
480  if (is_x_y(x.arg(0), y))
481  {
482  return true;
483  }
484  }
485  if (y_kind == Z3_OP_BNOT || y_kind == Z3_OP_NOT)
486  {
487  if (is_x_y(y.arg(0), x))
488  {
489  return true;
490  }
491  }
492 
493  return false;
494  }
495 
499  std::vector<z3::expr> get_parameters(const z3::expr& e)
500  {
501  std::vector<z3::expr> p;
502  for (u32 i = 0; i < e.num_args(); i++)
503  {
504  p.push_back(e.arg(i));
505  }
506 
507  return p;
508  }
509 
513  bool is_ones(const z3::expr& e)
514  {
515  if (!e.is_numeral())
516  {
517  return false;
518  }
519 
520  const std::string val_str = Z3_get_numeral_binary_string(e.ctx(), e);
521 
522  // Check if the binary representation consists only of '1's
523  return val_str.find('0') == std::string::npos;
524  }
525 
529  bool is_zero(const z3::expr& e)
530  {
531  if (!e.is_numeral())
532  {
533  return false;
534  }
535 
536  const std::string val_str = Z3_get_numeral_binary_string(e.ctx(), e);
537 
538  // Check if the binary representation consists only of '0's
539  return val_str.find('1') == std::string::npos;
540  }
541 
546  bool has_constant_value(const z3::expr& e, const u64& val)
547  {
548  if (!e.is_numeral())
549  {
550  return false;
551  }
552 
553  if (e.get_sort().bv_size() > 64)
554  {
555  return false;
556  }
557 
558  return e.get_numeral_uint64() == val;
559  }
560 
564  bool is_kind(const z3::expr& e, const Z3_decl_kind& t)
565  {
566  return e.decl().decl_kind() == t;
567  }
568 
572  bool is_commutative(const Z3_decl_kind& t)
573  {
574  switch (t)
575  {
576  case Z3_OP_TRUE:
577  case Z3_OP_FALSE:
578  case Z3_OP_AND:
579  case Z3_OP_OR:
580  case Z3_OP_NOT:
581  case Z3_OP_BAND:
582  case Z3_OP_BNOT:
583  case Z3_OP_BOR:
584  case Z3_OP_BXOR:
585  case Z3_OP_BADD:
586  return true;
587 
588  case Z3_OP_BNEG:
589  case Z3_OP_BSUB:
590  return false;
591 
592  case Z3_OP_BMUL:
593  return true;
594 
595  case Z3_OP_BSDIV:
596  case Z3_OP_BUDIV:
597  case Z3_OP_BSREM:
598  case Z3_OP_BUREM:
599  return false;
600 
601  case Z3_OP_EXTRACT:
602  return true;
603 
604  case Z3_OP_CONCAT:
605  return false;
606 
607  case Z3_OP_ZERO_EXT:
608  case Z3_OP_SIGN_EXT:
609  case Z3_OP_EQ:
610  return true;
611 
612  case Z3_OP_SLEQ:
613  case Z3_OP_SLT:
614  case Z3_OP_ULEQ:
615  case Z3_OP_ULT:
616  case Z3_OP_ITE:
617  return false;
618 
619  default: {
620  log_error("z3_utils", "commutative check not implemeted for type {}!", static_cast<int>(t));
621  return false;
622  }
623  }
624  }
625 
629  std::vector<z3::expr> normalize(std::vector<z3::expr>&& p)
630  {
631  if (p.size() <= 1ul)
632  {
633  return std::move(p);
634  }
635 
636  std::sort(p.begin(), p.end(), [](const auto& lhs, const auto& rhs) { return lhs.decl().decl_kind() > rhs.decl().decl_kind(); });
637  return std::move(p);
638  }
639 
643  bool check_simplification_for_correctness(const z3::expr& org, const z3::expr& smp)
644  {
645  log_warning("z3_utils", "Checking simplification for correctness. This is slow and expensive!");
646 
647  z3::solver s(org.ctx());
648  s.add(org != smp);
649  const auto r = s.check();
650 
651  if (r != z3::unsat)
652  {
653  std::cout << "Correctness Check failed!!!" << std::endl;
654  std::cout << "ORG: " << org << std::endl;
655  std::cout << "NEW: " << smp << std::endl;
656 
657  return false;
658  }
659 
660  return true;
661  }
662 
666  std::vector<z3::expr> simplify_concat(z3::context& ctx, const z3::expr& p0, const z3::expr& p1)
667  {
668  const u64 p0_size = p0.get_sort().bv_size();
669  const u64 p1_size = p1.get_sort().bv_size();
670 
671  // TODO make this able to handle more than 64 bits
672  // CONCAT(CONST(X), CONST(Y)) => CONST(X || Y)
673  if (p0.is_numeral() && p1.is_numeral())
674  {
675  if ((p0_size + p1_size) <= 64)
676  {
677  return {ctx.bv_val((p1.get_numeral_uint64() << p0_size) + p0.get_numeral_uint64(), p0_size + p1_size)};
678  }
679  }
680 
681  if (is_kind(p0, Z3_OP_EXTRACT) && is_kind(p1, Z3_OP_EXTRACT))
682  {
683  auto p0_parameter = get_parameters(p0);
684  auto p1_parameter = get_parameters(p1);
685 
686  if (is_x_y(p0_parameter[0], p1_parameter[0]))
687  {
688  // CONCAT(SLICE(X, j+1, k), SLICE(X, i, j)) => SLICE(X, i, k)
689  if (p1.lo() == (p0.hi() + 1))
690  {
691  const auto res = p0_parameter[0].extract(p1.hi(), p0.lo());
692  return {res};
693  }
694 
695  // CONCAT(SLICE(X, j, j), SLICE(X, j, i)) => SEXT(SLICE(X, j, i), 1)
696  if ((p1.lo() == p1.hi()) && (p1.lo() == p0.hi()))
697  {
698  const auto res = z3::expr(ctx, Z3_mk_sign_ext(ctx, 1, p0));
699  return {res};
700  }
701  }
702  }
703 
704  if (is_kind(p0, Z3_OP_EXTRACT) && p1.is_numeral())
705  {
706  // CONCAT(00..00, SLICE(X, i, j)) => ZEXT(SLICE(X, i, k), n)
707  if (is_zero(p1))
708  {
709  const auto res = z3::expr(ctx, Z3_mk_zero_ext(ctx, p1_size, p0));
710  return {res};
711  }
712  }
713 
714  if (is_kind(p0, Z3_OP_SIGN_EXT) && is_kind(p1, Z3_OP_EXTRACT))
715  {
716  auto p0_parameter = get_parameters(p0);
717  auto p1_parameter = get_parameters(p1);
718  auto p00_parameter = get_parameters(p0_parameter[0]);
719 
720  if (is_x_y(p00_parameter[0], p1_parameter[0]))
721  {
722  // CONCAT(SLICE(X, j, j), SEXT(SLICE(X, j, i), n)) => SEXT(SLICE(X, j, i), n + 1)
723  if ((p1.lo() == p1.hi()) && (p1.lo() == p0_parameter[0].hi()))
724  {
725  const u32 extend_by = p0.get_sort().bv_size() - p0_parameter[0].get_sort().bv_size() + 1;
726  auto res = z3::expr(ctx, Z3_mk_sign_ext(ctx, extend_by, p0_parameter[0]));
727  return {res};
728  }
729  }
730  }
731 
732  if (is_kind(p0, Z3_OP_ZERO_EXT) && p1.is_numeral())
733  {
734  auto p0_parameter = get_parameters(p0);
735 
736  // CONCAT(00..00, ZEXT(SLICE(X, j, i), n)) => ZEXT(SLICE(X, j, i), n + m))
737  if (is_zero(p1))
738  {
739  const u32 extend_by = p0.get_sort().bv_size() - p0_parameter[0].get_sort().bv_size() + p1_size;
740  const auto res = z3::expr(ctx, Z3_mk_zero_ext(ctx, extend_by, p0_parameter[0]));
741 
742  return {res};
743  }
744  }
745 
746  return {p0, p1};
747  }
748 
752  Result<z3::expr> simplify_internal(const z3::expr& e, std::unordered_map<u32, z3::expr>& cache, const bool check_correctness)
753  {
754  if (const auto it = cache.find(e.id()); it != cache.end())
755  {
756  return OK(it->second);
757  }
758 
759  u64 size;
760  if (e.is_bv())
761  {
762  if (e.is_numeral())
763  {
764  return OK(e);
765  }
766  else if (e.is_const())
767  {
768  return OK(e);
769  }
770  else if (e.is_var())
771  {
772  return OK(e);
773  }
774  size = e.get_sort().bv_size();
775  }
776 
777  auto& ctx = e.ctx();
778 
779  // 1. Simplify all parameters of the function recursively
780  const auto op = e.decl().decl_kind();
781  std::vector<z3::expr> p;
782  for (u32 i = 0; i < e.num_args(); i++)
783  {
784  const auto arg = e.arg(i);
785 
786  const auto res = simplify_internal(arg, cache, check_correctness);
787 
788  if (res.is_ok())
789  {
790  if (check_correctness && !check_simplification_for_correctness(arg, res.get()))
791  {
792  return ERR("simplification failed correctness check!");
793  }
794 
795  const auto [it, _] = cache.insert({arg.id(), res.get()});
796  p.push_back(it->second);
797  }
798  else
799  {
800  return ERR(res.get_error());
801  }
802  }
803 
804  // 2. If all simplified parameters are constants apply constant propagation
805  if (!p.empty() && std::all_of(p.begin(), p.end(), [](const auto& p_e) { return p_e.is_numeral() && p_e.is_bv(); }))
806  {
807  const auto bf = z3_utils::to_bf(e).get();
808 
809  std::vector<BooleanFunction> p_bf;
810  for (const auto& p_e : p)
811  {
812  const auto t = z3_utils::to_bf(p_e).get();
813  p_bf.push_back(t);
814  }
815 
816  auto res = BV_ConstantPropagation::constant_propagation(bf.get_top_level_node(), std::move(p_bf));
817  if (res.is_error())
818  {
819  return ERR_APPEND(res.get_error(), "could not simplify sub-expression in abstract syntax tree: constant propagation failed");
820  }
821 
822  auto bf_c = res.get();
823  if (!bf_c.is_empty())
824  {
825  const auto bf_z3 = z3_utils::from_bf(bf_c, ctx);
826  return OK(bf_z3);
827  }
828  }
829 
830  // 3. If the operation is commutative normalize the order of operands
831  if (is_commutative(op))
832  {
833  p = normalize(std::move(p));
834  }
835 
836  // 4. Apply various simplifcation rules based on the operation
837  switch (op)
838  {
839  case Z3_OP_TRUE: {
840  return OK(e);
841  }
842 
843  case Z3_OP_FALSE: {
844  return OK(e);
845  }
846 
847  case Z3_OP_AND: {
848  // X & False => False
849  if (p[1].is_bool() && p[1].is_false())
850  {
851  return OK(ctx.bool_val(false));
852  }
853  // X & True => X
854  if (p[1].is_bool() && p[1].is_true())
855  {
856  return OK(p[0]);
857  }
858  // X & X => X
859  if (is_x_y(p[0], p[1]))
860  {
861  return OK(p[0]);
862  }
863  // X & ~X => False
864  if (is_x_not_y(p[0], p[1]))
865  {
866  return OK(ctx.bool_val(false));
867  }
868 
869  if (p[0].is_or() && p[1].is_or())
870  {
871  auto p0_parameter = get_parameters(p[0]);
872  auto p1_parameter = get_parameters(p[1]);
873 
874  // (X | Y) & (X | Z) => X | (Y & Z)
875  if (is_x_y(p0_parameter[0], p1_parameter[0]))
876  {
877  return OK(p0_parameter[0] | (p0_parameter[1] & p1_parameter[1]));
878  }
879  // (X | Y) & (Z | X) => X | (Y & Z)
880  if (is_x_y(p0_parameter[0], p1_parameter[1]))
881  {
882  return OK(p0_parameter[0] | (p0_parameter[1] & p1_parameter[0]));
883  }
884 
885  // (X | Y) & (Y | Z) => Y | (X & Z)
886  if (is_x_y(p0_parameter[1], p1_parameter[0]))
887  {
888  return OK(p0_parameter[1] | (p0_parameter[0] & p1_parameter[1]));
889  }
890  // (X | Y) & (Z | Y) => Y | (X & Z)
891  if (is_x_y(p0_parameter[1], p1_parameter[1]))
892  {
893  return OK(p0_parameter[1] | (p0_parameter[0] & p1_parameter[0]));
894  }
895  }
896 
897  if (p[1].is_and())
898  {
899  auto p1_parameter = get_parameters(p[1]);
900  // X & (X & Y) => (X & Y)
901  if (is_x_y(p[0], p1_parameter[1]))
902  {
903  return OK(p[1]);
904  }
905  // X & (Y & X) => (Y & X)
906  if (is_x_y(p[0], p1_parameter[0]))
907  {
908  return OK(p[1]);
909  }
910 
911  // X & (~X & Y) => 0
912  if (is_x_not_y(p1_parameter[0], p[0]))
913  {
914  return OK(ctx.bool_val(false));
915  }
916  // X & (Y & ~X) => 0
917  if (is_x_not_y(p1_parameter[1], p[0]))
918  {
919  return OK(ctx.bool_val(false));
920  }
921  }
922 
923  if (p[1].is_or())
924  {
925  auto p1_parameter = get_parameters(p[1]);
926 
927  // X & (X | Y) => X
928  if (is_x_y(p1_parameter[0], p[0]))
929  {
930  return OK(p[0]);
931  }
932  // X & (Y | X) => X
933  if (is_x_y(p1_parameter[1], p[0]))
934  {
935  return OK(p[0]);
936  }
937  // X & (~X | Y) => X & Y
938  if (is_x_not_y(p1_parameter[0], p[0]))
939  {
940  return OK(p[0] & p1_parameter[1]);
941  }
942  // X & (Y | ~X) => X & Y
943  if (is_x_not_y(p1_parameter[1], p[0]))
944  {
945  return OK(p[0] & p1_parameter[0]);
946  }
947  }
948 
949  if (p[0].is_and())
950  {
951  auto p0_parameter = get_parameters(p[0]);
952 
953  // (X & Y) & X => X & Y
954  if (is_x_y(p0_parameter[0], p[1]))
955  {
956  return OK(p[0]);
957  }
958 
959  // (Y & X) & X => Y & X
960  if (is_x_y(p0_parameter[1], p[1]))
961  {
962  return OK(p[0]);
963  }
964  // (~X & Y) & X => 0
965  if (is_x_not_y(p0_parameter[0], p[1]))
966  {
967  return OK(ctx.bool_val(false));
968  }
969  // (Y & ~X) & X => 0
970  if (is_x_not_y(p0_parameter[1], p[1]))
971  {
972  return OK(ctx.bool_val(false));
973  }
974  }
975 
976  if (p[0].is_or())
977  {
978  auto p0_parameter = get_parameters(p[0]);
979 
980  // (X | Y) & X => X
981  if (is_x_y(p0_parameter[0], p[1]))
982  {
983  return OK(p[1]);
984  }
985  // (Y | X) & X => X
986  if (is_x_y(p0_parameter[1], p[1]))
987  {
988  return OK(p[1]);
989  }
990  // (~X | Y) & X => X & Y
991  if (is_x_not_y(p0_parameter[0], p[1]))
992  {
993  return OK(p[1] & p0_parameter[1]);
994  }
995  // (Y | ~X) & X => X & Y
996  if (is_x_not_y(p0_parameter[1], p[1]))
997  {
998  return OK(p[1] & p0_parameter[0]);
999  }
1000  }
1001 
1002  return OK(p[0] & p[1]);
1003  }
1004 
1005  case Z3_OP_OR: {
1006  // X | False => X
1007  if (p[1].is_false())
1008  {
1009  return OK(p[0]);
1010  }
1011 
1012  // X | True => True
1013  if (p[1].is_true())
1014  {
1015  return OK(p[1]);
1016  }
1017 
1018  // X | X => X
1019  if (is_x_y(p[0], p[1]))
1020  {
1021  return OK(p[0]);
1022  }
1023 
1024  // X | ~X => True
1025  if (is_x_not_y(p[0], p[1]))
1026  {
1027  return OK(ctx.bool_val(true));
1028  }
1029 
1030  if (p[0].is_and() && p[1].is_and())
1031  {
1032  auto p0_parameter = get_parameters(p[0]);
1033  auto p1_parameter = get_parameters(p[1]);
1034 
1035  // (X & Y) | (X & Z) => X & (Y | Z)
1036  if (is_x_y(p0_parameter[0], p1_parameter[0]))
1037  {
1038  return OK(p0_parameter[0] & (p0_parameter[1] | p1_parameter[1]));
1039  }
1040  // (X & Y) | (Z & X) => X & (Y | Z)
1041  if (is_x_y(p0_parameter[0], p1_parameter[1]))
1042  {
1043  return OK(p0_parameter[0] & (p0_parameter[1] | p1_parameter[0]));
1044  }
1045  // (X & Y) | (Y & Z) => Y & (Y | Z)
1046  if (is_x_y(p0_parameter[1], p1_parameter[0]))
1047  {
1048  return OK(p0_parameter[1] & (p0_parameter[0] | p1_parameter[1]));
1049  }
1050  // (X & Y) | (Z & Y) => Y & (X | Z)
1051  if (is_x_y(p0_parameter[1], p1_parameter[1]))
1052  {
1053  return OK(p0_parameter[1] & (p0_parameter[0] | p1_parameter[0]));
1054  }
1055  }
1056 
1057  if (p[1].is_and())
1058  {
1059  auto p1_parameter = get_parameters(p[1]);
1060  // X | (Y & !X) => X | Y
1061  if (is_x_not_y(p1_parameter[1], p[0]))
1062  {
1063  return OK(p[0] | p1_parameter[0]);
1064  }
1065 
1066  // X | (X & Y) => X
1067  if ((is_x_y(p1_parameter[0], p[0])) || (is_x_y(p1_parameter[1], p[0])))
1068  {
1069  return OK(p[0]);
1070  }
1071 
1072  // X | (~X & Y) => X | Y
1073  if (is_x_not_y(p1_parameter[0], p[0]))
1074  {
1075  return OK(p[0] | p1_parameter[1]);
1076  }
1077  // X | (Y & ~X) => X | Y
1078  if (is_x_not_y(p1_parameter[1], p[0]))
1079  {
1080  return OK(p[0] | p1_parameter[0]);
1081  }
1082  }
1083 
1084  if (p[1].is_or())
1085  {
1086  auto p1_parameter = get_parameters(p[1]);
1087 
1088  // X | (X | Y) => (X | Y)
1089  if (is_x_y(p1_parameter[0], p[0]))
1090  {
1091  return OK(p[1]);
1092  }
1093  // X | (Y | X) => (Y | X)
1094  if (is_x_y(p1_parameter[1], p[0]))
1095  {
1096  return OK(p[1]);
1097  }
1098 
1099  // X | (~X | Y) => True
1100  if (is_x_not_y(p1_parameter[0], p[0]))
1101  {
1102  return OK(ctx.bool_val(true));
1103  }
1104 
1105  // X | (Y | ~X) => True
1106  if (is_x_not_y(p1_parameter[1], p[0]))
1107  {
1108  return OK(ctx.bool_val(true));
1109  }
1110  }
1111 
1112  if (p[0].is_or())
1113  {
1114  auto p0_parameter = get_parameters(p[0]);
1115 
1116  // (X | Y) | X => (X | Y)
1117  if (is_x_y(p0_parameter[0], p[1]))
1118  {
1119  return OK(p[0]);
1120  }
1121  // (Y | X) | X => (Y | X)
1122  if (is_x_y(p0_parameter[1], p[1]))
1123  {
1124  return OK(p[0]);
1125  }
1126 
1127  // (~X | Y) | X => True
1128  if (is_x_not_y(p0_parameter[0], p[1]))
1129  {
1130  return OK(ctx.bool_val(true));
1131  }
1132 
1133  // (Y | ~X) | X => True
1134  if (is_x_not_y(p0_parameter[1], p[1]))
1135  {
1136  return OK(ctx.bool_val(true));
1137  }
1138  }
1139 
1140  if (p[0].is_and())
1141  {
1142  auto p0_parameter = get_parameters(p[0]);
1143 
1144  // (X & Y) | X => X
1145  if (is_x_y(p0_parameter[0], p[1]))
1146  {
1147  return OK(p[1]);
1148  }
1149  // (Y & X) | X => X
1150  if (is_x_y(p0_parameter[1], p[1]))
1151  {
1152  return OK(p[1]);
1153  }
1154 
1155  // (~X & Y) | X => X | Y
1156  if (is_x_not_y(p0_parameter[0], p[1]))
1157  {
1158  return OK(p0_parameter[1] | p[1]);
1159  }
1160 
1161  // (X & ~Y) | Y => X | Y
1162  if (is_x_not_y(p0_parameter[1], p[1]))
1163  {
1164  return OK(p0_parameter[0] | p[1]);
1165  }
1166  }
1167 
1168  if (p[0].is_eq() && p[1].is_eq())
1169  {
1170  auto p0_parameter = get_parameters(p[0]);
1171  auto p1_parameter = get_parameters(p[1]);
1172 
1173  // eq(X, 1) | eq(X, 0) => True
1174  if (p0_parameter[0].get_sort().is_bv() && is_x_y(p0_parameter[0], p1_parameter[0]))
1175  {
1176  if (p0_parameter[0].get_sort().bv_size() == 1)
1177  {
1178  if (is_ones(p0_parameter[1]) && is_zero(p1_parameter[1]))
1179  {
1180  return OK(ctx.bool_val(true));
1181  }
1182 
1183  if (is_zero(p0_parameter[1]) && is_ones(p1_parameter[1]))
1184  {
1185  return OK(ctx.bool_val(true));
1186  }
1187  }
1188  }
1189  }
1190 
1191  return OK(p[0] | p[1]);
1192  }
1193 
1194  case Z3_OP_NOT: {
1195  // ~~X => X
1196  if (p[0].is_not())
1197  {
1198  return OK(get_parameters(p[0])[0]);
1199  }
1200 
1201  // ~(~X & ~Y) => X | Y
1202  if (is_kind(p[0], Z3_OP_BAND))
1203  {
1204  auto p0_parameter = get_parameters(p[0]);
1205  if (p0_parameter[0].is_not() && p0_parameter[1].is_not())
1206  {
1207  return OK(get_parameters(p0_parameter[0])[0] | get_parameters(p0_parameter[1])[0]);
1208  }
1209  }
1210 
1211  // ~(~X | ~Y) => X & Y
1212  if (is_kind(p[0], Z3_OP_BOR))
1213  {
1214  auto p0_parameter = get_parameters(p[0]);
1215  if (p0_parameter[0].is_not() && p0_parameter[1].is_not())
1216  {
1217  return OK(get_parameters(p0_parameter[0])[0] & get_parameters(p0_parameter[1])[0]);
1218  }
1219  }
1220 
1221  // ~(X | Y) => ~X & ~Y
1222  if (p[0].is_or())
1223  {
1224  auto p0_parameter = get_parameters(p[0]);
1225  return OK((~p0_parameter[0]) & (~p0_parameter[1]));
1226  }
1227 
1228  // ~(X & Y) => ~X | ~Y
1229  if (p[0].is_and())
1230  {
1231  auto p0_parameter = get_parameters(p[0]);
1232  return OK((~p0_parameter[0]) | (~p0_parameter[1]));
1233  }
1234 
1235  return OK(~p[0]);
1236  }
1237 
1238  case Z3_OP_BAND: {
1239  if (p.size() == 2)
1240  {
1241  // X & 0 => 0
1242  if (is_zero(p[1]))
1243  {
1244  return OK(ctx.bv_val(0, size));
1245  }
1246  // X & 1 => X
1247  if (is_ones(p[1]))
1248  {
1249  return OK(p[0]);
1250  }
1251  // X & X => X
1252  if (is_x_y(p[0], p[1]))
1253  {
1254  return OK(p[0]);
1255  }
1256  // X & ~X => 0
1257  if (is_x_not_y(p[0], p[1]))
1258  {
1259  return OK(ctx.bv_val(0, size));
1260  }
1261 
1262  if (is_kind(p[0], Z3_OP_BOR) && is_kind(p[1], Z3_OP_BOR))
1263  {
1264  auto p0_parameter = get_parameters(p[0]);
1265  auto p1_parameter = get_parameters(p[1]);
1266 
1267  // (X | Y) & (X | Z) => X | (Y & Z)
1268  if (is_x_y(p0_parameter[0], p1_parameter[0]))
1269  {
1270  return OK(p0_parameter[0] | (p0_parameter[1] & p1_parameter[1]));
1271  }
1272  // (X | Y) & (Z | X) => X | (Y & Z)
1273  if (is_x_y(p0_parameter[0], p1_parameter[1]))
1274  {
1275  return OK(p0_parameter[0] | (p0_parameter[1] & p1_parameter[0]));
1276  }
1277 
1278  // (X | Y) & (Y | Z) => Y | (X & Z)
1279  if (is_x_y(p0_parameter[1], p1_parameter[0]))
1280  {
1281  return OK(p0_parameter[1] | (p0_parameter[0] & p1_parameter[1]));
1282  }
1283  // (X | Y) & (Z | Y) => Y | (X & Z)
1284  if (is_x_y(p0_parameter[1], p1_parameter[1]))
1285  {
1286  return OK(p0_parameter[1] | (p0_parameter[0] & p1_parameter[0]));
1287  }
1288  }
1289 
1290  if (is_kind(p[1], Z3_OP_BAND))
1291  {
1292  auto p1_parameter = get_parameters(p[1]);
1293  // X & (X & Y) => (X & Y)
1294  if (is_x_y(p[0], p1_parameter[1]))
1295  {
1296  return OK(p[1]);
1297  }
1298  // X & (Y & X) => (Y & X)
1299  if (is_x_y(p[0], p1_parameter[0]))
1300  {
1301  return OK(p[1]);
1302  }
1303 
1304  // X & (~X & Y) => 0
1305  if (is_x_not_y(p1_parameter[0], p[0]))
1306  {
1307  return OK(ctx.bv_val(0, size));
1308  }
1309  // X & (Y & ~X) => 0
1310  if (is_x_not_y(p1_parameter[1], p[0]))
1311  {
1312  return OK(ctx.bv_val(0, size));
1313  }
1314  }
1315 
1316  if (is_kind(p[1], Z3_OP_BOR))
1317  {
1318  auto p1_parameter = get_parameters(p[1]);
1319 
1320  // X & (X | Y) => X
1321  if (is_x_y(p1_parameter[0], p[0]))
1322  {
1323  return OK(p[0]);
1324  }
1325  // X & (Y | X) => X
1326  if (is_x_y(p1_parameter[1], p[0]))
1327  {
1328  return OK(p[0]);
1329  }
1330  // X & (~X | Y) => X & Y
1331  if (is_x_not_y(p1_parameter[0], p[0]))
1332  {
1333  return OK(p[0] & p1_parameter[1]);
1334  }
1335  // X & (Y | ~X) => X & Y
1336  if (is_x_not_y(p1_parameter[1], p[0]))
1337  {
1338  return OK(p[0] & p1_parameter[0]);
1339  }
1340  }
1341 
1342  if (is_kind(p[0], Z3_OP_BAND))
1343  {
1344  auto p0_parameter = get_parameters(p[0]);
1345 
1346  // (X & Y) & X => X & Y
1347  if (is_x_y(p0_parameter[0], p[1]))
1348  {
1349  return OK(p[0]);
1350  }
1351 
1352  // (Y & X) & X => Y & X
1353  if (is_x_y(p0_parameter[1], p[1]))
1354  {
1355  return OK(p[0]);
1356  }
1357  // (~X & Y) & X => 0
1358  if (is_x_not_y(p0_parameter[0], p[1]))
1359  {
1360  return OK(ctx.bv_val(0, size));
1361  }
1362  // (Y & ~X) & X => 0
1363  if (is_x_not_y(p0_parameter[1], p[1]))
1364  {
1365  return OK(ctx.bv_val(0, size));
1366  }
1367  }
1368 
1369  if (is_kind(p[0], Z3_OP_BOR))
1370  {
1371  auto p0_parameter = get_parameters(p[0]);
1372 
1373  // (X | Y) & X => X
1374  if (is_x_y(p0_parameter[0], p[1]))
1375  {
1376  return OK(p[1]);
1377  }
1378  // (Y | X) & X => X
1379  if (is_x_y(p0_parameter[1], p[1]))
1380  {
1381  return OK(p[1]);
1382  }
1383  // (~X | Y) & X => X & Y
1384  if (is_x_not_y(p0_parameter[0], p[1]))
1385  {
1386  return OK(p[1] & p0_parameter[1]);
1387  }
1388  // (Y | ~X) & X => X & Y
1389  if (is_x_not_y(p0_parameter[1], p[1]))
1390  {
1391  return OK(p[1] & p0_parameter[0]);
1392  }
1393  }
1394 
1395  return OK(p[0] & p[1]);
1396  }
1397 
1398  // TODO simplify with more than two parameters
1399  z3::expr res = p[0] & p[1];
1400  for (u32 i = 2; i < p.size(); i++)
1401  {
1402  res = res & p[i];
1403  }
1404  return OK(res);
1405  }
1406 
1407  case Z3_OP_BNOT: {
1408  // ~~X => X
1409  if (is_kind(p[0], Z3_OP_BNOT))
1410  {
1411  return OK(get_parameters(p[0])[0]);
1412  }
1413 
1414  // ~(~X & ~Y) => X | Y
1415  if (is_kind(p[0], Z3_OP_BAND))
1416  {
1417  auto p0_parameter = get_parameters(p[0]);
1418  if (is_kind(p0_parameter[0], Z3_OP_BNOT) && is_kind(p0_parameter[1], Z3_OP_BNOT))
1419  {
1420  return OK(get_parameters(p0_parameter[0])[0] | get_parameters(p0_parameter[1])[0]);
1421  }
1422  }
1423 
1424  // ~(~X | ~Y) => X & Y
1425  if (is_kind(p[0], Z3_OP_BOR))
1426  {
1427  auto p0_parameter = get_parameters(p[0]);
1428  if (is_kind(p0_parameter[0], Z3_OP_BNOT) && is_kind(p0_parameter[1], Z3_OP_BNOT))
1429  {
1430  return OK(get_parameters(p0_parameter[0])[0] & get_parameters(p0_parameter[1])[0]);
1431  }
1432  }
1433 
1434  // ~(X | Y) => ~X & ~Y
1435  if (is_kind(p[0], Z3_OP_BOR))
1436  {
1437  auto p0_parameter = get_parameters(p[0]);
1438  return OK((~p0_parameter[0]) & (~p0_parameter[1]));
1439  }
1440 
1441  // ~(X & Y) => ~X | ~Y
1442  if (is_kind(p[0], Z3_OP_BAND))
1443  {
1444  auto p0_parameter = get_parameters(p[0]);
1445  return OK((~p0_parameter[0]) | (~p0_parameter[1]));
1446  }
1447 
1448  return OK(~p[0]);
1449  }
1450 
1451  case Z3_OP_BOR: {
1452  if (p.size() == 2)
1453  {
1454  // X | 0 => X
1455  if (is_zero(p[1]))
1456  {
1457  return OK(p[0]);
1458  }
1459 
1460  // X | 1 => 1
1461  if (is_ones(p[1]))
1462  {
1463  return OK(p[1]);
1464  }
1465 
1466  // X | X => X
1467  if (is_x_y(p[0], p[1]))
1468  {
1469  return OK(p[0]);
1470  }
1471 
1472  // X | ~X => 1
1473  if (is_x_not_y(p[0], p[1]))
1474  {
1475  return OK(ctx.bv_val(-1, size));
1476  }
1477 
1478  if (is_kind(p[0], Z3_OP_BAND) && is_kind(p[1], Z3_OP_BAND))
1479  {
1480  auto p0_parameter = get_parameters(p[0]);
1481  auto p1_parameter = get_parameters(p[1]);
1482 
1483  // (X & Y) | (X & Z) => X & (Y | Z)
1484  if (is_x_y(p0_parameter[0], p1_parameter[0]))
1485  {
1486  return OK(p0_parameter[0] & (p0_parameter[1] | p1_parameter[1]));
1487  }
1488  // (X & Y) | (Z & X) => X & (Y | Z)
1489  if (is_x_y(p0_parameter[0], p1_parameter[1]))
1490  {
1491  return OK(p0_parameter[0] & (p0_parameter[1] | p1_parameter[0]));
1492  }
1493  // (X & Y) | (Y & Z) => Y & (Y | Z)
1494  if (is_x_y(p0_parameter[1], p1_parameter[0]))
1495  {
1496  return OK(p0_parameter[1] & (p0_parameter[0] | p1_parameter[1]));
1497  }
1498  // (X & Y) | (Z & Y) => Y & (X | Z)
1499  if (is_x_y(p0_parameter[1], p1_parameter[1]))
1500  {
1501  return OK(p0_parameter[1] & (p0_parameter[0] | p1_parameter[0]));
1502  }
1503  }
1504 
1505  if (is_kind(p[1], Z3_OP_BAND))
1506  {
1507  auto p1_parameter = get_parameters(p[1]);
1508  // X | (Y & !X) => X | Y
1509  if (is_x_not_y(p1_parameter[1], p[0]))
1510  {
1511  return OK(p[0] | p1_parameter[0]);
1512  }
1513 
1514  // X | (X & Y) => X
1515  if ((is_x_y(p1_parameter[0], p[0])) || (is_x_y(p1_parameter[1], p[0])))
1516  {
1517  return OK(p[0]);
1518  }
1519 
1520  // X | (~X & Y) => X | Y
1521  if (is_x_not_y(p1_parameter[0], p[0]))
1522  {
1523  return OK(p[0] | p1_parameter[1]);
1524  }
1525  // X | (Y & ~X) => X | Y
1526  if (is_x_not_y(p1_parameter[1], p[0]))
1527  {
1528  return OK(p[0] | p1_parameter[0]);
1529  }
1530  }
1531 
1532  if (is_kind(p[1], Z3_OP_BOR))
1533  {
1534  auto p1_parameter = get_parameters(p[1]);
1535 
1536  // X | (X | Y) => (X | Y)
1537  if (is_x_y(p1_parameter[0], p[0]))
1538  {
1539  return OK(p[1]);
1540  }
1541  // X | (Y | X) => (Y | X)
1542  if (is_x_y(p1_parameter[1], p[0]))
1543  {
1544  return OK(p[1]);
1545  }
1546 
1547  // X | (~X | Y) => 1
1548  if (is_x_not_y(p1_parameter[0], p[0]))
1549  {
1550  return OK(ctx.bv_val(-1, size));
1551  }
1552 
1553  // X | (Y | ~X) => 1
1554  if (is_x_not_y(p1_parameter[1], p[0]))
1555  {
1556  return OK(ctx.bv_val(-1, size));
1557  }
1558  }
1559 
1560  if (is_kind(p[0], Z3_OP_BOR))
1561  {
1562  auto p0_parameter = get_parameters(p[0]);
1563 
1564  // (X | Y) | X => (X | Y)
1565  if (is_x_y(p0_parameter[0], p[1]))
1566  {
1567  return OK(p[0]);
1568  }
1569  // (Y | X) | X => (Y | X)
1570  if (is_x_y(p0_parameter[1], p[1]))
1571  {
1572  return OK(p[0]);
1573  }
1574 
1575  // (~X | Y) | X => 1
1576  if (is_x_not_y(p0_parameter[0], p[1]))
1577  {
1578  return OK(ctx.bv_val(-1, size));
1579  }
1580 
1581  // (Y | ~X) | X => 1
1582  if (is_x_not_y(p0_parameter[1], p[1]))
1583  {
1584  return OK(ctx.bv_val(-1, size));
1585  }
1586  }
1587 
1588  if (is_kind(p[0], Z3_OP_BAND))
1589  {
1590  auto p0_parameter = get_parameters(p[0]);
1591 
1592  // (X & Y) | X => X
1593  if (is_x_y(p0_parameter[0], p[1]))
1594  {
1595  return OK(p[1]);
1596  }
1597  // (Y & X) | X => X
1598  if (is_x_y(p0_parameter[1], p[1]))
1599  {
1600  return OK(p[1]);
1601  }
1602 
1603  // (~X & Y) | X => X | Y
1604  if (is_x_not_y(p0_parameter[0], p[1]))
1605  {
1606  return OK(p0_parameter[1] | p[1]);
1607  }
1608 
1609  // (X & ~Y) | Y => X | Y
1610  if (is_x_not_y(p0_parameter[1], p[1]))
1611  {
1612  return OK(p0_parameter[0] | p[1]);
1613  }
1614  }
1615 
1616  return OK(p[0] | p[1]);
1617  }
1618 
1619  // TODO simplify with more than two parameters
1620  z3::expr res = p[0] | p[1];
1621  for (u32 i = 2; i < p.size(); i++)
1622  {
1623  res = res | p[i];
1624  }
1625  return OK(res);
1626  }
1627 
1628  case Z3_OP_BXOR: {
1629  if (p.size() == 2)
1630  {
1631  // X ^ 0 => X
1632  if (is_zero(p[1]))
1633  {
1634  return OK(p[0]);
1635  }
1636  // X ^ 1 => ~X
1637  if (is_ones(p[1]))
1638  {
1639  return OK(~p[0]);
1640  }
1641  // X ^ X => 0
1642  if (is_x_y(p[0], p[1]))
1643  {
1644  return OK(ctx.bv_val(0, size));
1645  }
1646  // X ^ ~X => 1
1647  if (is_x_not_y(p[0], p[1]))
1648  {
1649  return OK(ctx.bv_val(-1, size));
1650  }
1651 
1652  return OK(p[0] ^ p[1]);
1653  }
1654 
1655  // TODO simplify with more than two parameters
1656  z3::expr res = p[0] ^ p[1];
1657  for (u32 i = 2; i < p.size(); i++)
1658  {
1659  res = res ^ p[i];
1660  }
1661  return OK(res);
1662  }
1663 
1664  case Z3_OP_BNEG: {
1665  // --X => X
1666  if (is_kind(p[0], Z3_OP_BNEG))
1667  {
1668  return OK(get_parameters(p[0])[0]);
1669  }
1670 
1671  return OK(-p[0]);
1672  }
1673 
1674  case Z3_OP_BADD: {
1675  if (p.size() == 2)
1676  {
1677  // X + 0 => X
1678  if (is_zero(p[1]))
1679  {
1680  return OK(p[0]);
1681  }
1682 
1683  const u64 p0_size = p[0].get_sort().bv_size();
1684  const u64 p1_size = p[1].get_sort().bv_size();
1685 
1686  if (is_kind(p[0], Z3_OP_BNEG))
1687  {
1688  const auto p0_parameter = get_parameters(p[0]);
1689 
1690  return OK(p[1] - p0_parameter[0]);
1691  }
1692 
1693  if (is_kind(p[1], Z3_OP_BNEG))
1694  {
1695  const auto p1_parameter = get_parameters(p[1]);
1696 
1697  return OK(p[0] - p1_parameter[0]);
1698  }
1699 
1700  // SLICE(X, 0, 0) + SLICE(Y, 0, 0) => SLICE(X + Y, 0, 0)
1701  if ((is_kind(p[0], Z3_OP_EXTRACT)) && is_kind(p[1], Z3_OP_EXTRACT))
1702  {
1703  if ((p[0].lo() == 0) && (p[0].hi() == 0) && (p[1].lo() == 0) && (p[1].hi() == 0))
1704  {
1705  auto p0_parameter = get_parameters(p[0]);
1706  auto p1_parameter = get_parameters(p[1]);
1707 
1708  return OK((p0_parameter[0] + p1_parameter[0]).extract(0, 0));
1709  }
1710  }
1711 
1712  return OK(p[0] + p[1]);
1713  }
1714 
1715  // TODO simplify SUM with more than two parameters
1716  z3::expr sum = p[0] + p[1];
1717  for (u32 i = 2; i < p.size(); i++)
1718  {
1719  sum = sum + p[i];
1720  }
1721  return OK(sum);
1722  }
1723 
1724  case Z3_OP_BSUB: {
1725  if (p.size() == 2)
1726  {
1727  // X - 0 => X
1728  if (is_zero(p[1]))
1729  {
1730  return OK(p[0]);
1731  }
1732  // X - X => 0
1733  if (is_x_y(p[0], p[1]))
1734  {
1735  return OK(ctx.bv_val(0, size));
1736  }
1737 
1738  // X - (-Y) => X + Y
1739  if (is_kind(p[1], Z3_OP_BNEG))
1740  {
1741  const auto p1_parameter = get_parameters(p[1]);
1742 
1743  return OK(p[0] + p1_parameter[0]);
1744  }
1745 
1746  return OK(p[0] - p[1]);
1747  }
1748 
1749  // TODO implement for more than two parameters
1750  z3::expr sum = p[0] - p[1];
1751  for (u32 i = 2; i < p.size(); i++)
1752  {
1753  sum = sum - p[i];
1754  }
1755  return OK(sum);
1756  }
1757 
1758  case Z3_OP_BMUL: {
1759  // X * 0 => 0
1760  if (is_zero(p[1]))
1761  {
1762  return OK(ctx.bv_val(0, size));
1763  }
1764  // X * 1 => X
1765  if (has_constant_value(p[1], 1))
1766  {
1767  return OK(p[0]);
1768  }
1769 
1770  // This currently leads to problems, since the HAL boolean function can not handle this, so translation causes errors
1771  // // X * -1 => -X
1772  // if (is_ones(p[1]))
1773  // {
1774  // return OK(-p[0]);
1775  // }
1776 
1777  return OK(p[0] * p[1]);
1778  }
1779 
1780  case Z3_OP_BSDIV: {
1781  // X /s 1 => X
1782  if (has_constant_value(p[1], 1))
1783  {
1784  return OK(p[0]);
1785  }
1786  // X /s X => 1
1787  if (is_x_y(p[0], p[1]))
1788  {
1789  return OK(ctx.bv_val(1, size));
1790  }
1791 
1792  return OK(p[0] / p[1]);
1793  }
1794 
1795  case Z3_OP_BUDIV: {
1796  // X / 1 => X
1797  if (has_constant_value(p[1], 1))
1798  {
1799  return OK(p[0]);
1800  }
1801  // X / X => 1
1802  if (is_x_y(p[0], p[1]))
1803  {
1804  return OK(ctx.bv_val(1, size));
1805  }
1806 
1807  return OK(z3::expr(ctx, Z3_mk_bvudiv(ctx, p[0], p[1])));
1808  }
1809 
1810  case Z3_OP_BSREM: {
1811  // X %s 1 => 0
1812  if (has_constant_value(p[1], 1))
1813  {
1814  return OK(ctx.bv_val(0, size));
1815  }
1816  // X %s X => 0
1817  if (is_x_y(p[0], p[1]))
1818  {
1819  return OK(ctx.bv_val(0, size));
1820  }
1821 
1822  return OK(z3::expr(ctx, Z3_mk_bvsrem(ctx, p[0], p[1])));
1823  }
1824 
1825  case Z3_OP_BUREM: {
1826  // X % 1 => 0
1827  if (has_constant_value(p[1], 1))
1828  {
1829  return OK(ctx.bv_val(0, size));
1830  }
1831  // X % X => 0
1832  if (is_x_y(p[0], p[1]))
1833  {
1834  return OK(ctx.bv_val(0, size));
1835  }
1836 
1837  return OK(z3::expr(ctx, Z3_mk_bvurem(ctx, p[0], p[1])));
1838  }
1839 
1840  case Z3_OP_EXTRACT: {
1841  // SLICE(p, 0, 0) => p (if p is 1-bit wide)
1842  if ((e.lo() == 0) && (e.hi() == 0) && (p[0].get_sort().bv_size() == 1))
1843  {
1844  return OK(p[0]);
1845  }
1846 
1847  // SLICE(p, n, 0) => p (if size of p is n+1)
1848  if (((e.hi() - e.lo()) == (p[0].get_sort().bv_size() - 1)) && (e.lo() == 0))
1849  {
1850  return OK(p[0]);
1851  }
1852 
1853  // SLICE(011..010, i, j) => 010..001
1854  if (p[0].is_numeral())
1855  {
1856  const std::string p0_str = Z3_get_numeral_binary_string(e.ctx(), p[0]);
1857  const std::string p0_pad = std::string(p[0].get_sort().bv_size() - p0_str.length(), '0') + p0_str;
1858 
1859  // reverse string to place bit 0 at index 0 of string
1860  std::string p0_rev = p0_pad;
1861  std::reverse(p0_rev.begin(), p0_rev.end());
1862 
1863  const std::string ex_str = p0_rev.substr(e.lo(), e.hi() - e.lo() + 1);
1864 
1865  const auto res = z3_utils::value_from_binary_string(ctx, ex_str);
1866 
1867  return res;
1868  }
1869 
1870  return OK(p[0].extract(e.hi(), e.lo()));
1871  }
1872 
1873  case Z3_OP_CONCAT: {
1874  std::vector<z3::expr> q = {p.begin(), p.end()};
1875  std::vector<z3::expr> res;
1876 
1877  while (q.size() > 1)
1878  {
1879  const auto p0 = q.back();
1880  q.pop_back();
1881 
1882  const auto p1 = q.back();
1883  q.pop_back();
1884 
1885  const auto sc = simplify_concat(ctx, p0, p1);
1886 
1887  if (sc.size() == 1)
1888  {
1889  q.push_back(sc.front());
1890  }
1891  else
1892  {
1893  res.insert(res.begin(), sc.back());
1894  q.push_back(sc.front());
1895  }
1896  }
1897 
1898  res.push_back(q.front());
1899 
1900  if (res.size() > 1)
1901  {
1902  z3::expr_vector res_e(ctx);
1903  for (const auto& e : res)
1904  {
1905  res_e.push_back(e);
1906  }
1907 
1908  return OK(z3::concat(res_e));
1909  }
1910 
1911  return OK(res.front());
1912  }
1913 
1914  case Z3_OP_ZERO_EXT: {
1915  const u64 i = e.get_sort().bv_size() - p[0].get_sort().bv_size();
1916  return OK(z3::expr(ctx, Z3_mk_zero_ext(ctx, i, p[0])));
1917  }
1918 
1919  case Z3_OP_SIGN_EXT: {
1920  const u64 i = e.get_sort().bv_size() - p[0].get_sort().bv_size();
1921  return OK(z3::expr(ctx, Z3_mk_sign_ext(ctx, i, p[0])));
1922  }
1923 
1924  case Z3_OP_EQ: {
1925  // X == X => true
1926  if (is_x_y(p[0], p[1]))
1927  {
1928  return OK(ctx.bool_val(true));
1929  }
1930 
1931  // 010..010 == 101..101 => false
1932  if (p[0].is_numeral() && p[1].is_numeral())
1933  {
1934  const std::string p0_str = Z3_get_numeral_binary_string(e.ctx(), p[0]);
1935  const std::string p1_str = Z3_get_numeral_binary_string(e.ctx(), p[1]);
1936 
1937  if (p0_str != p1_str)
1938  {
1939  return OK(ctx.bool_val(false));
1940  }
1941  }
1942 
1943  return OK(p[0] == p[1]);
1944  }
1945 
1946  case Z3_OP_SLEQ: {
1947  // X <=s X => true
1948  if (is_x_y(p[0], p[1]))
1949  {
1950  return OK(ctx.bool_val(true));
1951  }
1952 
1953  return OK(z3::expr(ctx, Z3_mk_bvsle(ctx, p[0], p[1])));
1954  }
1955 
1956  case Z3_OP_SLT: {
1957  // X <s X => 0
1958  if (is_x_y(p[0], p[1]))
1959  {
1960  return OK(ctx.bool_val(false));
1961  }
1962 
1963  return OK(z3::expr(ctx, Z3_mk_bvslt(ctx, p[0], p[1])));
1964  }
1965 
1966  case Z3_OP_ULEQ: {
1967  // X <= X => 1
1968  if (is_x_y(p[0], p[1]))
1969  {
1970  return OK(ctx.bool_val(true));
1971  }
1972 
1973  return OK(z3::expr(ctx, Z3_mk_bvule(ctx, p[0], p[1])));
1974  }
1975 
1976  case Z3_OP_ULT: {
1977  // X < 0 => 0
1978  if (is_zero(p[1]))
1979  {
1980  return OK(ctx.bool_val(false));
1981  }
1982  // X < X => 0
1983  if (is_x_y(p[0], p[1]))
1984  {
1985  return OK(ctx.bool_val(false));
1986  }
1987 
1988  return OK(z3::expr(ctx, Z3_mk_bvult(ctx, p[0], p[1])));
1989  }
1990 
1991  case Z3_OP_ITE: {
1992  // ITE(false, a, b) => b
1993  if (p[0].is_false())
1994  {
1995  return OK(p[2]);
1996  }
1997  // ITE(true, a, b) => a
1998  if (p[0].is_true())
1999  {
2000  return OK(p[1]);
2001  }
2002  // ITE(a, b, b) => b
2003  if (is_x_y(p[1], p[2]))
2004  {
2005  return OK(p[1]);
2006  }
2007 
2008  return OK(z3::ite(p[0], p[1], p[2]));
2009  }
2010 
2011  default:
2012  return ERR("could not simplify sub-expression in abstract syntax tree: not implemented for given node type " + std::to_string(op));
2013  }
2014  }
2015 
2016  } // namespace
2017 
2018  namespace z3_utils
2019  {
2020  Result<z3::expr> simplify_local(const z3::expr& e, std::unordered_map<u32, z3::expr>& cache, const bool check_correctness)
2021  {
2022  const u32 max_loop_iterations = 128;
2023  u32 iteration = 0;
2024 
2025  z3::expr res = e;
2026  z3::expr prev_res = res;
2027 
2028  do
2029  {
2030  prev_res = res;
2031  const auto simplify_res = simplify_internal(res, cache, check_correctness);
2032  if (simplify_res.is_error())
2033  {
2034  return simplify_res;
2035  }
2036  const auto [it, _] = cache.insert({e.id(), simplify_res.get()});
2037  res = it->second;
2038 
2039  iteration++;
2040  if (iteration > max_loop_iterations)
2041  {
2042  return ERR("Triggered max iteration counter during simplificaton!");
2043  }
2044  } while (!z3::eq(prev_res, res));
2045 
2046  if (check_correctness && !check_simplification_for_correctness(e, res))
2047  {
2048  return ERR("Simplification failed");
2049  }
2050 
2051  return OK(res);
2052  }
2053 
2054  Result<z3::expr> simplify_local(const z3::expr& e, const bool check_correctness)
2055  {
2056  std::unordered_map<u32, z3::expr> cache;
2057  return simplify_local(e, cache, check_correctness);
2058  }
2059 
2060  } // namespace z3_utils
2061 } // namespace hal
boolean_function.h
size
u32 size
Definition: candidate_search.cpp:62
hal::BooleanFunction::Value
Value
represents the type of the node
Definition: boolean_function.h:74
hal::BooleanFunction::Const
static BooleanFunction Const(const BooleanFunction::Value &value)
Definition: boolean_function.cpp:256
u64
uint64_t u64
Definition: defines.h:42
u32
uint32_t u32
Definition: defines.h:41
u8
uint8_t u8
Definition: defines.h:39
i32
int32_t i32
Definition: defines.h:36
log_error
#define log_error(channel,...)
Definition: log.h:78
log_warning
#define log_warning(channel,...)
Definition: log.h:76
ERR
#define ERR(message)
Definition: result.h:60
OK
#define OK(...)
Definition: result.h:56
ERR_APPEND
#define ERR_APPEND(prev_error, message)
Definition: result.h:64
hal::BV_ConstantPropagation::And
BooleanFunction And(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:20
hal::BV_ConstantPropagation::Sub
BooleanFunction Sub(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:162
hal::BV_ConstantPropagation::Ult
BooleanFunction Ult(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:326
hal::BV_ConstantPropagation::Sle
BooleanFunction Sle(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:219
hal::BV_ConstantPropagation::constant_propagation
Result< BooleanFunction > constant_propagation(const BooleanFunction::Node &node, std::vector< BooleanFunction > &&p)
Definition: simplification.cpp:379
hal::BV_ConstantPropagation::Ule
BooleanFunction Ule(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:297
hal::BV_ConstantPropagation::Mul
BooleanFunction Mul(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:189
hal::BV_ConstantPropagation::Add
BooleanFunction Add(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:135
hal::BV_ConstantPropagation::Or
BooleanFunction Or(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:49
hal::BV_ConstantPropagation::Slt
BooleanFunction Slt(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:259
hal::BV_ConstantPropagation::Xor
BooleanFunction Xor(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: simplification.cpp:106
hal::BV_ConstantPropagation::Not
BooleanFunction Not(const std::vector< BooleanFunction::Value > &p)
Definition: simplification.cpp:77
hal::BV_ConstantPropagation::Ite
BooleanFunction Ite(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1, const std::vector< BooleanFunction::Value > &p2)
Definition: simplification.cpp:356
hal::module_identification::has_constant_value
bool has_constant_value(const z3::expr &e, const u64 &val)
Definition: create_functional_candidates.cpp:209
hal::z3_utils::simplify_local
Result< z3::expr > simplify_local(const z3::expr &e, std::unordered_map< u32, z3::expr > &cache, const bool check_correctness=false)
Applies hand-crafted simplification rules iteratively until no further simplifications can be made.
Definition: simplification.cpp:2020
hal::z3_utils::from_bf
z3::expr from_bf(const BooleanFunction &bf, z3::context &ctx, const std::map< std::string, z3::expr > &var2expr={})
Definition: z3_utils.cpp:15
hal::z3_utils::value_from_binary_string
Result< z3::expr > value_from_binary_string(z3::context &ctx, const std::string &bit_string)
Definition: z3_utils.cpp:145
hal::z3_utils::to_bf
Result< BooleanFunction > to_bf(const z3::expr &e)
Definition: z3_utils.cpp:443
hal
Definition: defines.h:45
x
u64 x
Definition: netlist_preprocessing.cpp:2204
y
u64 y
Definition: netlist_preprocessing.cpp:2205
simplification.h
hal::BooleanFunction::Node::type
u16 type
The type of the node.
Definition: boolean_function.h:993
z3_utils.h