HAL
symbolic_execution.cpp
Go to the documentation of this file.
1 #include "hal_core/netlist/boolean_function/symbolic_execution.h"
2 #include "hal_core/utilities/log.h"
3 
4 namespace hal
5 {
6  namespace SMT
7  {
8  namespace ConstantPropagation
9  {
17  BooleanFunction And(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
18  {
19  std::vector<BooleanFunction::Value> simplified;
20  simplified.reserve(p0.size());
21  for (auto i = 0u; i < p0.size(); i++)
22  {
23  if ((p0[i] == 0) || (p1[i] == 0))
24  {
25  simplified.emplace_back(BooleanFunction::Value::ZERO);
26  }
27  else if ((p0[i] == 1) && (p1[i] == 1))
28  {
29  simplified.emplace_back(BooleanFunction::Value::ONE);
30  }
31  else
32  {
33  simplified.emplace_back(BooleanFunction::Value::X);
34  }
35  }
36  return BooleanFunction::Const(simplified);
37  }
38 
46  BooleanFunction Or(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
47  {
48  std::vector<BooleanFunction::Value> simplified;
49  simplified.reserve(p0.size());
50  for (auto i = 0u; i < p0.size(); i++)
51  {
52  if ((p0[i] == 0) && (p1[i] == 0))
53  {
54  simplified.emplace_back(BooleanFunction::Value::ZERO);
55  }
56  else if ((p0[i] == 1) || (p1[i] == 1))
57  {
58  simplified.emplace_back(BooleanFunction::Value::ONE);
59  }
60  else
61  {
62  simplified.emplace_back(BooleanFunction::Value::X);
63  }
64  }
65  return BooleanFunction::Const(simplified);
66  }
67 
74  BooleanFunction Not(const std::vector<BooleanFunction::Value>& p)
75  {
76  std::vector<BooleanFunction::Value> simplified;
77  simplified.reserve(p.size());
78  for (const auto& value : p)
79  {
80  if (value == BooleanFunction::Value::ZERO)
81  {
82  simplified.emplace_back(BooleanFunction::Value::ONE);
83  }
84  else if (value == BooleanFunction::Value::ONE)
85  {
86  simplified.emplace_back(BooleanFunction::Value::ZERO);
87  }
88  else
89  {
90  simplified.emplace_back(value);
91  }
92  }
93  return BooleanFunction::Const(simplified);
94  }
95 
103  BooleanFunction Xor(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
104  {
105  std::vector<BooleanFunction::Value> simplified;
106  simplified.reserve(p0.size());
107  for (auto i = 0u; i < p0.size(); i++)
108  {
109  if (((p0[i] == 0) && (p1[i] == 1)) || ((p0[i] == 1) && (p1[i] == 0)))
110  {
111  simplified.emplace_back(BooleanFunction::Value::ONE);
112  }
113  else if (((p0[i] == 0) && (p1[i] == 0)) || ((p0[i] == 1) && (p1[i] == 1)))
114  {
115  simplified.emplace_back(BooleanFunction::Value::ZERO);
116  }
117  else
118  {
119  simplified.emplace_back(BooleanFunction::Value::X);
120  }
121  }
122  return BooleanFunction::Const(simplified);
123  }
124 
132  BooleanFunction Add(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
133  {
134  if (p0.size() <= 64 && p1.size() <= 64)
135  {
136  const auto a_res = BooleanFunction::to_u64(p0);
137  const auto b_res = BooleanFunction::to_u64(p1);
138 
139  if (a_res.is_ok() && b_res.is_ok())
140  {
141  const auto res = (a_res.get() + b_res.get()) & 0xffffffff;
142  return BooleanFunction::Const(res, p0.size());
143  }
144 
145  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
146  }
147 
148  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
149  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
150  {
151  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
152  }
153 
154  std::vector<BooleanFunction::Value> simplified;
155  simplified.reserve(p0.size());
156  auto carry = BooleanFunction::Value::ZERO;
157  for (auto i = 0u; i < p0.size(); i++)
158  {
159  auto res = p0[i] + p1[i] + carry;
160  simplified.emplace_back(static_cast<BooleanFunction::Value>(res & 0x1));
161  carry = static_cast<BooleanFunction::Value>(res >> 1);
162  }
163  return BooleanFunction::Const(simplified);
164  }
165 
173  BooleanFunction Sub(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
174  {
175  if (p0.size() <= 64 && p1.size() <= 64)
176  {
177  const auto a_res = BooleanFunction::to_u64(p0);
178  const auto b_res = BooleanFunction::to_u64(p1);
179 
180  if (a_res.is_ok() && b_res.is_ok())
181  {
182  const auto res = (a_res.get() - b_res.get()) & 0xffffffff;
183  return BooleanFunction::Const(res, p0.size());
184  }
185 
186  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
187  }
188 
189  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
190  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
191  {
192  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
193  }
194 
195  std::vector<BooleanFunction::Value> simplified;
196  simplified.reserve(p0.size());
197  auto carry = BooleanFunction::Value::ONE;
198  for (auto i = 0u; i < p0.size(); i++)
199  {
200  auto res = p0[i] + !(p1[i]) + carry;
201  simplified.emplace_back(static_cast<BooleanFunction::Value>(res & 0x1));
202  carry = static_cast<BooleanFunction::Value>(res >> 1);
203  }
204  return BooleanFunction::Const(simplified);
205  }
206 
214  BooleanFunction Mul(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
215  {
216  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
217  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
218  {
219  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
220  }
221 
222  auto bitsize = p0.size();
223  std::vector<BooleanFunction::Value> simplified(bitsize, BooleanFunction::Value::ZERO);
224  for (auto i = 0u; i < bitsize; i++)
225  {
226  auto carry = BooleanFunction::Value::ZERO;
227  for (auto j = 0u; j < bitsize - i; j++)
228  {
229  auto res = simplified[i + j] + (p0[i] & p1[j]) + carry;
230  simplified[i + j] = static_cast<BooleanFunction::Value>(res & 0x1);
231  carry = static_cast<BooleanFunction::Value>(res >> 1);
232  }
233  }
234  return BooleanFunction::Const(simplified);
235  }
236 
244  BooleanFunction Shl(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
245  {
246  if (p1 >= p0.size())
247  {
248  // Shift amount is too large, result is all zeros
249  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::ZERO));
250  }
251 
252  std::vector<BooleanFunction::Value> result(p0.size(), BooleanFunction::Value::ZERO);
253 
254  // Copy bits from original position to shifted position
255  for (auto i = p1; i < p0.size(); i++)
256  {
257  result[i] = p0[i - p1];
258  }
259 
260  return BooleanFunction::Const(result);
261  }
262 
270  BooleanFunction Lshr(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
271  {
272  if (p1 >= p0.size())
273  {
274  // Shift amount is too large, result is all zeros
275  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::ZERO));
276  }
277 
278  std::vector<BooleanFunction::Value> result(p0.size(), BooleanFunction::Value::ZERO);
279 
280  // Copy bits from original position to shifted position
281  for (auto i = 0u; i < p0.size() - p1; i++)
282  {
283  result[i] = p0[i + p1];
284  }
285 
286  return BooleanFunction::Const(result);
287  }
288 
296  BooleanFunction Ashr(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
297  {
298  auto sign_bit = p0.back(); // MSB is the sign bit
299 
300  if (p1 >= p0.size())
301  {
302  // Shift amount is too large, result is all sign bits
303  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), sign_bit));
304  }
305 
306  std::vector<BooleanFunction::Value> result(p0.size(), sign_bit);
307 
308  // Copy bits from original position to shifted position
309  for (auto i = 0u; i < p0.size() - p1; i++)
310  {
311  result[i] = p0[i + p1];
312  }
313 
314  return BooleanFunction::Const(result);
315  }
316 
324  BooleanFunction Rol(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
325  {
326  auto rotate_amount = p1 % p0.size(); // Modulo for rotation
327 
328  if (rotate_amount == 0)
329  {
330  return BooleanFunction::Const(p0); // No rotation needed
331  }
332 
333  std::vector<BooleanFunction::Value> result(p0.size());
334 
335  // Perform the rotation
336  for (auto i = 0u; i < p0.size(); i++)
337  {
338  auto new_pos = (i + rotate_amount) % p0.size();
339  result[new_pos] = p0[i];
340  }
341 
342  return BooleanFunction::Const(result);
343  }
344 
352  BooleanFunction Ror(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
353  {
354  auto rotate_amount = p1 % p0.size(); // Modulo for rotation
355 
356  if (rotate_amount == 0)
357  {
358  return BooleanFunction::Const(p0); // No rotation needed
359  }
360 
361  std::vector<BooleanFunction::Value> result(p0.size());
362 
363  // Perform the rotation
364  for (auto i = 0u; i < p0.size(); i++)
365  {
366  auto new_pos = (i + p0.size() - rotate_amount) % p0.size();
367  result[new_pos] = p0[i];
368  }
369 
370  return BooleanFunction::Const(result);
371  }
379  BooleanFunction Sle(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
380  {
381  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
382  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
383  {
384  return BooleanFunction::Const({BooleanFunction::Value::X});
385  }
386 
387  auto msb_p0 = p0.back();
388  auto msb_p1 = p1.back();
389  if (msb_p0 == BooleanFunction::Value::ONE && msb_p1 == BooleanFunction::Value::ZERO)
390  {
391  return BooleanFunction::Const(1, 1);
392  }
393  else if (msb_p0 == BooleanFunction::Value::ZERO && msb_p1 == BooleanFunction::Value::ONE)
394  {
395  return BooleanFunction::Const(0, 1);
396  }
397 
398  std::vector<BooleanFunction::Value> simplified;
399  u8 carry = 1;
400  u8 neq = 0;
401  u8 res = 0;
402  for (auto i = 0u; i < p0.size(); i++)
403  {
404  res = p0[i] + !(p1[i]) + carry;
405  carry = res >> 1;
406  neq |= res & 1;
407  }
408 
409  return BooleanFunction::Const({static_cast<BooleanFunction::Value>((res & 1) | !neq)});
410  }
411 
419  BooleanFunction Slt(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
420  {
421  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
422  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
423  {
424  return BooleanFunction::Const({BooleanFunction::Value::X});
425  }
426 
427  auto msb_p0 = p0.back();
428  auto msb_p1 = p1.back();
429  if (msb_p0 == BooleanFunction::Value::ONE && msb_p1 == BooleanFunction::Value::ZERO)
430  {
431  return BooleanFunction::Const(1, 1);
432  }
433  else if (msb_p0 == BooleanFunction::Value::ZERO && msb_p1 == BooleanFunction::Value::ONE)
434  {
435  return BooleanFunction::Const(0, 1);
436  }
437 
438  std::vector<BooleanFunction::Value> simplified;
439  u8 res = 0;
440  u8 carry = 1;
441  for (auto i = 0u; i < p0.size(); i++)
442  {
443  res = p0[i] + !(p1[i]) + carry;
444  carry = (res >> 1) & 1;
445  }
446 
447  return BooleanFunction::Const({static_cast<BooleanFunction::Value>(res & 1)});
448  }
449 
457  BooleanFunction Ule(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
458  {
459  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
460  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
461  {
462  return BooleanFunction::Const({BooleanFunction::Value::X});
463  }
464 
465  for (i32 i = p0.size() - 1; i >= 0; i--)
466  {
467  if (p0[i] == BooleanFunction::Value::ONE && p1[i] == BooleanFunction::Value::ZERO)
468  {
469  return BooleanFunction::Const(0, 1);
470  }
471  else if (p0[i] == BooleanFunction::Value::ZERO && p1[i] == BooleanFunction::Value::ONE)
472  {
473  return BooleanFunction::Const(1, 1);
474  }
475  }
476  return BooleanFunction::Const(1, 1);
477  }
478 
486  BooleanFunction Ult(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
487  {
488  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
489  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
490  {
491  return BooleanFunction::Const({BooleanFunction::Value::X});
492  }
493 
494  for (i32 i = p0.size() - 1; i >= 0; i--)
495  {
496  if (p0[i] == BooleanFunction::Value::ONE && p1[i] == BooleanFunction::Value::ZERO)
497  {
498  return BooleanFunction::Const(0, 1);
499  }
500  else if (p0[i] == BooleanFunction::Value::ZERO && p1[i] == BooleanFunction::Value::ONE)
501  {
502  return BooleanFunction::Const(1, 1);
503  }
504  }
505  return BooleanFunction::Const(0, 1);
506  }
507 
516  BooleanFunction Ite(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1, const std::vector<BooleanFunction::Value>& p2)
517  {
518  if (p0.front() == BooleanFunction::Value::ONE)
519  {
520  return BooleanFunction::Const(p1);
521  }
522  else if (p0.front() == BooleanFunction::Value::ZERO)
523  {
524  return BooleanFunction::Const(p2);
525  }
526  else
527  {
528  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X));
529  }
530  }
531 
532  } // namespace ConstantPropagation
533 
534  namespace
535  {
542  BooleanFunction One(u16 size)
543  {
544  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(size, BooleanFunction::Value::ONE));
545  }
546  } // namespace
547 
548  SymbolicExecution::SymbolicExecution(const std::vector<BooleanFunction>& variables) : state(SymbolicState(variables))
549  {
550  }
551 
552  Result<BooleanFunction> SymbolicExecution::evaluate(const BooleanFunction& function) const
553  {
554  std::vector<BooleanFunction> stack;
555  for (const auto& node : function.get_nodes())
556  {
557  std::vector<BooleanFunction> parameters;
558  std::move(stack.end() - static_cast<i64>(node.get_arity()), stack.end(), std::back_inserter(parameters));
559  stack.erase(stack.end() - static_cast<i64>(node.get_arity()), stack.end());
560 
561  if (auto simplified = this->simplify(node, std::move(parameters)); simplified.is_ok())
562  {
563  stack.emplace_back(simplified.get());
564  }
565  else
566  {
567  return ERR_APPEND(simplified.get_error(), "could not evaluate Boolean function within symbolic state: simplification failed");
568  }
569  }
570 
571  switch (stack.size())
572  {
573  case 1:
574  return OK(stack.back());
575  default:
576  return ERR("could not evaluate Boolean function within symbolic state: stack is imbalanced");
577  }
578  }
579 
580  Result<std::monostate> SymbolicExecution::evaluate(const Constraint& constraint)
581  {
582  if (constraint.is_assignment())
583  {
584  const auto& assignment = constraint.get_assignment().get();
585  if (auto res = this->evaluate(assignment->first).map<std::monostate>([&](auto&& rhs) -> Result<std::monostate> {
586  this->state.set(assignment->second.clone(), std::move(rhs));
587  return OK({});
588  });
589  res.is_error())
590  {
591  return ERR_APPEND(res.get_error(), "could not to evaluate assignment constraint within the symbolic state: evaluation failed");
592  }
593  else
594  {
595  return OK({});
596  }
597  }
598  else
599  {
600  const auto& function = constraint.get_function().get();
601  auto node_type = function->get_top_level_node().type;
602  if (!(node_type == BooleanFunction::NodeType::Eq || node_type == BooleanFunction::NodeType::Slt || node_type == BooleanFunction::NodeType::Sle
603  || node_type == BooleanFunction::NodeType::Ult || node_type == BooleanFunction::NodeType::Ule))
604  {
605  return ERR("invalid node type in function '" + function->to_string() + "'");
606  }
607  if (auto res = this->evaluate(*function); res.is_error())
608  {
609  return ERR_APPEND(res.get_error(), "could not to evaluate function constraint within the symbolic state: evaluation failed");
610  }
611  else
612  {
613  return OK({});
614  }
615  }
616  }
617 
618  std::vector<BooleanFunction> SymbolicExecution::normalize(std::vector<BooleanFunction>&& p)
619  {
620  if (p.size() <= 1ul)
621  {
622  return std::move(p);
623  }
624 
625  std::sort(p.begin(), p.end(), [](const auto& lhs, const auto& rhs) {
626  if (lhs.get_top_level_node().type == rhs.get_top_level_node().type)
627  {
628  return lhs < rhs;
629  }
630  return rhs.is_constant();
631  });
632  return std::move(p);
633  }
634 
635  namespace
636  {
640  bool is_x_not_y(const BooleanFunction& x, const BooleanFunction& y)
641  {
642  const BooleanFunction& smaller = (x.get_nodes().size() < y.get_nodes().size()) ? x : y;
643  const BooleanFunction& bigger = (x.get_nodes().size() < y.get_nodes().size()) ? y : x;
644 
645  // The node vector of the first function needs to be exactly one element shorter than the second
646  if (smaller.get_nodes().size() != (bigger.get_nodes().size() - 1))
647  {
648  return false;
649  }
650 
651  // The top level node of the bigger node vector needs to be a NOT node
652  if (bigger.get_top_level_node().type != BooleanFunction::NodeType::Not)
653  {
654  return false;
655  }
656 
657  // Every n'th element in the smaller node vector has to be identical to the n'th element of the bigger node vector, except the last/top level node
658  for (u32 idx = 0; idx < smaller.get_nodes().size(); idx++)
659  {
660  if (smaller.get_nodes().at(idx) != bigger.get_nodes().at(idx))
661  {
662  return false;
663  }
664  }
665 
666  return true;
667  }
668  } // namespace
669 
670  Result<BooleanFunction> SymbolicExecution::simplify(const BooleanFunction::Node& node, std::vector<BooleanFunction>&& p) const
671  {
672  if (!p.empty() && std::all_of(p.begin(), p.end(), [](const auto& function) { return function.is_constant() || function.is_index(); }))
673  {
674  if (auto res = SymbolicExecution::constant_propagation(node, std::move(p)); res.is_error())
675  {
676  return ERR_APPEND(res.get_error(), "could not simplify sub-expression in abstract syntax tree: constant propagation failed");
677  }
678  else
679  {
680  return res;
681  }
682  }
683 
684  if (node.is_commutative())
685  {
686  p = SymbolicExecution::normalize(std::move(p));
687  }
688 
694 
695  switch (node.type)
696  {
697  case BooleanFunction::NodeType::Constant: {
698  return OK(BooleanFunction::Const(node.constant));
699  }
700  case BooleanFunction::NodeType::Index: {
701  return OK(BooleanFunction::Index(node.index, node.size));
702  }
703  case BooleanFunction::NodeType::Variable: {
704  return OK(this->state.get(BooleanFunction::Var(node.variable, node.size)));
705  }
706  case BooleanFunction::NodeType::And: {
707  // X & 0 => 0
708  if (p[1].has_constant_value(0))
709  {
710  return OK(BooleanFunction::Const(0, node.size));
711  }
712  // X & 1 => X
713  if (p[1] == One(node.size))
714  {
715  return OK(p[0]);
716  }
717  // X & X => X
718  if (p[0] == p[1])
719  {
720  return OK(p[0]);
721  }
722  // X & ~X => 0
723  if (is_x_not_y(p[0], p[1]))
724  {
725  return OK(BooleanFunction::Const(0, node.size));
726  }
727 
728  if (p[0].is(BooleanFunction::NodeType::Or) && p[1].is(BooleanFunction::NodeType::Or))
729  {
730  auto p0_parameter = p[0].get_parameters();
731  auto p1_parameter = p[1].get_parameters();
732 
733  // (X | Y) & (X | Z) => X | (Y & Z)
734  if (p0_parameter[0] == p1_parameter[0])
735  {
736  return OK(p0_parameter[0] | (p0_parameter[1] & p1_parameter[1]));
737  }
738  // (X | Y) & (Z | X) => X | (Y & Z)
739  if (p0_parameter[0] == p1_parameter[1])
740  {
741  return OK(p0_parameter[0] | (p0_parameter[1] & p1_parameter[0]));
742  }
743 
744  // (X | Y) & (Y | Z) => Y | (X & Z)
745  if (p0_parameter[1] == p1_parameter[0])
746  {
747  return OK(p0_parameter[1] | (p0_parameter[0] & p1_parameter[1]));
748  }
749  // (X | Y) & (Z | Y) => Y | (X & Z)
750  if (p0_parameter[1] == p1_parameter[1])
751  {
752  return OK(p0_parameter[1] | (p0_parameter[0] & p1_parameter[0]));
753  }
754  }
755 
756  if (p[1].is(BooleanFunction::NodeType::And))
757  {
758  auto p1_parameter = p[1].get_parameters();
759  // X & (X & Y) => (X & Y)
760  if (p[0] == p1_parameter[1])
761  {
762  return OK(p[1]);
763  }
764  // X & (Y & X) => (Y & X)
765  if (p[0] == p1_parameter[0])
766  {
767  return OK(p[1]);
768  }
769 
770  // X & (~X & Y) => 0
771  if (is_x_not_y(p1_parameter[0], p[0]))
772  {
773  return OK(BooleanFunction::Const(0, node.size));
774  }
775  // X & (Y & ~X) => 0
776  if (is_x_not_y(p1_parameter[1], p[0]))
777  {
778  return OK(BooleanFunction::Const(0, node.size));
779  }
780  }
781 
782  if (p[1].is(BooleanFunction::NodeType::Or))
783  {
784  auto p1_parameter = p[1].get_parameters();
785 
786  // X & (X | Y) => X
787  if (p1_parameter[0] == p[0])
788  {
789  return OK(p[0]);
790  }
791  // X & (Y | X) => X
792  if (p1_parameter[1] == p[0])
793  {
794  return OK(p[0]);
795  }
796  // X & (~X | Y) => X & Y
797  if (is_x_not_y(p1_parameter[0], p[0]))
798  {
799  return BooleanFunction::And(p[0].clone(), p1_parameter[1].clone(), node.size);
800  }
801  // X & (Y | ~X) => X & Y
802  if (is_x_not_y(p1_parameter[1], p[0]))
803  {
804  return BooleanFunction::And(p[0].clone(), p1_parameter[0].clone(), node.size);
805  }
806  }
807 
808  if (p[0].is(BooleanFunction::NodeType::And))
809  {
810  auto p0_parameter = p[0].get_parameters();
811 
812  // (X & Y) & X => X & Y
813  if (p0_parameter[0] == p[1])
814  {
815  return OK(p[0]);
816  }
817 
818  // (Y & X) & X => Y & X
819  if (p0_parameter[1] == p[1])
820  {
821  return OK(p[0]);
822  }
823  // (~X & Y) & X => 0
824  if (is_x_not_y(p0_parameter[0], p[1]))
825  {
826  return OK(BooleanFunction::Const(0, node.size));
827  }
828  // (Y & ~X) & X => 0
829  if (is_x_not_y(p0_parameter[1], p[1]))
830  {
831  return OK(BooleanFunction::Const(0, node.size));
832  }
833  }
834 
835  if (p[0].is(BooleanFunction::NodeType::Or))
836  {
837  auto p0_parameter = p[0].get_parameters();
838 
839  // (X | Y) & X => X
840  if (p0_parameter[0] == p[1])
841  {
842  return OK(p[1]);
843  }
844  // (Y | X) & X => X
845  if (p0_parameter[1] == p[1])
846  {
847  return OK(p[1]);
848  }
849  // (~X | Y) & X => X & Y
850  if (is_x_not_y(p0_parameter[0], p[1]))
851  {
852  return BooleanFunction::And(p[1].clone(), p0_parameter[1].clone(), node.size);
853  }
854  // (Y | ~X) & X => X & Y
855  if (is_x_not_y(p0_parameter[1], p[1]))
856  {
857  return BooleanFunction::And(p[1].clone(), p0_parameter[0].clone(), node.size);
858  }
859  }
860 
861  return OK(p[0] & p[1]);
862  }
863  case BooleanFunction::NodeType::Not: {
864  // ~~X => X
865  if (p[0].is(BooleanFunction::NodeType::Not))
866  {
867  return OK(p[0].get_parameters()[0]);
868  }
869 
870  // ~(~X & ~Y) => X | Y
871  if (p[0].is(BooleanFunction::NodeType::And))
872  {
873  auto p0_parameter = p[0].get_parameters();
874  if (p0_parameter[0].is(BooleanFunction::NodeType::Not) && p0_parameter[1].is(BooleanFunction::NodeType::Not))
875  {
876  return BooleanFunction::Or(p0_parameter[0].get_parameters()[0].clone(), p0_parameter[1].get_parameters()[0].clone(), node.size);
877  }
878  }
879 
880  // ~(~X | ~Y) => X & Y
881  if (p[0].is(BooleanFunction::NodeType::Or))
882  {
883  auto p0_parameter = p[0].get_parameters();
884  if (p0_parameter[0].is(BooleanFunction::NodeType::Not) && p0_parameter[1].is(BooleanFunction::NodeType::Not))
885  {
886  return BooleanFunction::And(p0_parameter[0].get_parameters()[0].clone(), p0_parameter[1].get_parameters()[0].clone(), node.size);
887  }
888  }
889 
890  // ~(X | Y) => ~X & ~Y
891  if (p[0].is(BooleanFunction::NodeType::Or))
892  {
893  auto p0_parameter = p[0].get_parameters();
894  return OK((~p0_parameter[0]) & (~p0_parameter[1]));
895  }
896 
897  // ~(X & Y) => ~X | ~Y
898  if (p[0].is(BooleanFunction::NodeType::And))
899  {
900  auto p0_parameter = p[0].get_parameters();
901  return OK((~p0_parameter[0]) | (~p0_parameter[1]));
902  }
903 
904  return BooleanFunction::Not(p[0].clone(), node.size);
905  }
906 
907  case BooleanFunction::NodeType::Or: {
908  // X | 0 => X
909  if (p[1].has_constant_value(0))
910  {
911  return OK(p[0]);
912  }
913 
914  // X | 1 => 1
915  if (p[1] == One(node.size))
916  {
917  return OK(p[1]);
918  }
919 
920  // X | X => X
921  if (p[0] == p[1])
922  {
923  return OK(p[0]);
924  }
925 
926  // X | ~X => 111...1
927  if (is_x_not_y(p[0], p[1]))
928  {
929  return OK(One(node.size));
930  }
931 
932  if (p[0].is(BooleanFunction::NodeType::And) && p[1].is(BooleanFunction::NodeType::And))
933  {
934  auto p0_parameter = p[0].get_parameters();
935  auto p1_parameter = p[1].get_parameters();
936 
937  // (X & Y) | (X & Z) => X & (Y | Z)
938  if (p0_parameter[0] == p1_parameter[0])
939  {
940  return OK(p0_parameter[0] & (p0_parameter[1] | p1_parameter[1]));
941  }
942  // (X & Y) | (Z & X) => X & (Y | Z)
943  if (p0_parameter[0] == p1_parameter[1])
944  {
945  return OK(p0_parameter[0] & (p0_parameter[1] | p1_parameter[0]));
946  }
947  // (X & Y) | (Y & Z) => Y & (Y | Z)
948  if (p0_parameter[1] == p1_parameter[0])
949  {
950  return OK(p0_parameter[1] & (p0_parameter[0] | p1_parameter[1]));
951  }
952  // (X & Y) | (Z & Y) => Y & (X | Z)
953  if (p0_parameter[1] == p1_parameter[1])
954  {
955  return OK(p0_parameter[1] & (p0_parameter[0] | p1_parameter[0]));
956  }
957  }
958 
959  if (p[1].is(BooleanFunction::NodeType::And))
960  {
961  auto p1_parameter = p[1].get_parameters();
962  // X | (Y & !X) => X | Y
963  if (is_x_not_y(p1_parameter[1], p[0]))
964  {
965  return BooleanFunction::Or(p[0].clone(), p1_parameter[0].clone(), node.size);
966  }
967 
968  // X | (X & Y) => X
969  if ((p1_parameter[0] == p[0]) || (p1_parameter[1] == p[0]))
970  {
971  return OK(p[0]);
972  }
973 
974  // X | (~X & Y) => X | Y
975  if (is_x_not_y(p1_parameter[0], p[0]))
976  {
977  return BooleanFunction::Or(p[0].clone(), p1_parameter[1].clone(), node.size);
978  }
979  // X | (Y & ~X) => X | Y
980  if (is_x_not_y(p1_parameter[1], p[0]))
981  {
982  return BooleanFunction::Or(p[0].clone(), p1_parameter[0].clone(), node.size);
983  }
984  }
985 
986  if (p[1].is(BooleanFunction::NodeType::Or))
987  {
988  auto p1_parameter = p[1].get_parameters();
989 
990  // X | (X | Y) => (X | Y)
991  if (p1_parameter[0] == p[0])
992  {
993  return OK(p[1]);
994  }
995  // X | (Y | X) => (Y | X)
996  if (p1_parameter[1] == p[0])
997  {
998  return OK(p[1]);
999  }
1000 
1001  // X | (~X | Y) => 1
1002  if (is_x_not_y(p1_parameter[0], p[0]))
1003  {
1004  return OK(One(node.size));
1005  }
1006 
1007  // X | (Y | ~X) => 1
1008  if (is_x_not_y(p1_parameter[1], p[0]))
1009  {
1010  return OK(One(node.size));
1011  }
1012  }
1013 
1014  if (p[0].is(BooleanFunction::NodeType::Or))
1015  {
1016  auto p0_parameter = p[0].get_parameters();
1017 
1018  // (X | Y) | X => (X | Y)
1019  if (p0_parameter[0] == p[1])
1020  {
1021  return OK(p[0]);
1022  }
1023  // (Y | X) | X => (Y | X)
1024  if (p0_parameter[1] == p[1])
1025  {
1026  return OK(p[0]);
1027  }
1028 
1029  // (~X | Y) | X => 1
1030  if (is_x_not_y(p0_parameter[0], p[1]))
1031  {
1032  return OK(One(node.size));
1033  }
1034 
1035  // (Y | ~X) | X => 1
1036  if (is_x_not_y(p0_parameter[1], p[1]))
1037  {
1038  return OK(One(node.size));
1039  }
1040  }
1041 
1042  if (p[0].is(BooleanFunction::NodeType::And))
1043  {
1044  auto p0_parameter = p[0].get_parameters();
1045 
1046  // (X & Y) | X => X
1047  if (p0_parameter[0] == p[1])
1048  {
1049  return OK(p[1]);
1050  }
1051  // (Y & X) | X => X
1052  if (p0_parameter[1] == p[1])
1053  {
1054  return OK(p[1]);
1055  }
1056 
1057  // (~X & Y) | X => X | Y
1058  if (is_x_not_y(p0_parameter[0], p[1]))
1059  {
1060  return BooleanFunction::Or(p0_parameter[1].clone(), p[1].clone(), node.size);
1061  }
1062 
1063  // (X & ~Y) | Y => X | Y
1064  if (is_x_not_y(p0_parameter[1], p[1]))
1065  {
1066  return BooleanFunction::Or(p0_parameter[0].clone(), p[1].clone(), node.size);
1067  }
1068  }
1069 
1070  return BooleanFunction::Or(p[0].clone(), p[1].clone(), node.size);
1071  }
1072  case BooleanFunction::NodeType::Xor: {
1073  // X ^ 0 => X
1074  if (p[1].has_constant_value(0))
1075  {
1076  return OK(p[0]);
1077  }
1078  // X ^ 1 => ~X
1079  if (p[1] == One(node.size))
1080  {
1081  return BooleanFunction::Not(p[0].clone(), node.size);
1082  }
1083  // X ^ X => 0
1084  if (p[0] == p[1])
1085  {
1086  return OK(BooleanFunction::Const(0, node.size));
1087  }
1088  // X ^ ~X => 1
1089  if (is_x_not_y(p[0], p[1]))
1090  {
1091  return OK(One(node.size));
1092  }
1093 
1094  return BooleanFunction::Xor(p[0].clone(), p[1].clone(), node.size);
1095  }
1096  case BooleanFunction::NodeType::Add: {
1097  // X + 0 => X
1098  if (p[1].has_constant_value(0))
1099  {
1100  return OK(p[0]);
1101  }
1102 
1103  return BooleanFunction::Add(p[0].clone(), p[1].clone(), node.size);
1104  }
1105  case BooleanFunction::NodeType::Sub: {
1106  // X - 0 => X
1107  if (p[1].has_constant_value(0))
1108  {
1109  return OK(p[0]);
1110  }
1111  // X - X => 0
1112  if (p[0] == p[1])
1113  {
1114  return OK(BooleanFunction::Const(0, node.size));
1115  }
1116 
1117  return BooleanFunction::Sub(p[0].clone(), p[1].clone(), node.size);
1118  }
1119  case BooleanFunction::NodeType::Mul: {
1120  // X * 0 => 0
1121  if (p[1].has_constant_value(0))
1122  {
1123  return OK(BooleanFunction::Const(0, node.size));
1124  }
1125  // X * 1 => X
1126  if (p[1].has_constant_value(1))
1127  {
1128  return OK(p[0]);
1129  }
1130 
1131  return BooleanFunction::Mul(p[0].clone(), p[1].clone(), node.size);
1132  }
1133  case BooleanFunction::NodeType::Sdiv: {
1134  // X /s 1 => X
1135  if (p[1].has_constant_value(1))
1136  {
1137  return OK(p[0]);
1138  }
1139  // X /s X => 1
1140  if (p[0] == p[1])
1141  {
1142  return OK(BooleanFunction::Const(1, node.size));
1143  }
1144 
1145  return BooleanFunction::Sdiv(p[0].clone(), p[1].clone(), node.size);
1146  }
1147  case BooleanFunction::NodeType::Udiv: {
1148  // X / 1 => X
1149  if (p[1].has_constant_value(1))
1150  {
1151  return OK(p[0]);
1152  }
1153  // X / X => 1
1154  if (p[0] == p[1])
1155  {
1156  return OK(BooleanFunction::Const(1, node.size));
1157  }
1158 
1159  return BooleanFunction::Udiv(p[0].clone(), p[1].clone(), node.size);
1160  }
1161  case BooleanFunction::NodeType::Srem: {
1162  // X %s 1 => 0
1163  if (p[1].has_constant_value(1))
1164  {
1165  return OK(BooleanFunction::Const(0, node.size));
1166  }
1167  // X %s X => 0
1168  if (p[0] == p[1])
1169  {
1170  return OK(BooleanFunction::Const(0, node.size));
1171  }
1172 
1173  return BooleanFunction::Srem(p[0].clone(), p[1].clone(), node.size);
1174  }
1175  case BooleanFunction::NodeType::Urem: {
1176  // X %s 1 => 0
1177  if (p[1].has_constant_value(1))
1178  {
1179  return OK(BooleanFunction::Const(0, node.size));
1180  }
1181  // X %s X => 0
1182  if (p[0] == p[1])
1183  {
1184  return OK(BooleanFunction::Const(0, node.size));
1185  }
1186 
1187  return BooleanFunction::Urem(p[0].clone(), p[1].clone(), node.size);
1188  }
1189  case BooleanFunction::NodeType::Slice: {
1190  // SLICE(p, 0, 0) => p (if p is 1-bit wide)
1191  // if ((p[0].size() == 1) && p[1].has_index_value(0) && p[2].has_index_value(0) && (node.size == 1))
1192  // {
1193  // return OK(p[0]);
1194  // }
1195 
1196  // SLICE(p, 0, size-1) => p
1197  if (node.size == p[0].size() && p[1].has_index_value(0) && p[2].has_index_value(node.size - 1))
1198  {
1199  return OK(p[0]);
1200  }
1201 
1202  return BooleanFunction::Slice(p[0].clone(), p[1].clone(), p[2].clone(), node.size);
1203  }
1204  case BooleanFunction::NodeType::Concat: {
1205  // CONCAT(X, Y) => CONST(X || Y)
1206  if (p[0].is_constant() && p[1].is_constant())
1207  {
1208  if ((p[0].size() + p[1].size()) <= 64)
1209  {
1210  return OK(BooleanFunction::Const((p[0].get_constant_value_u64().get() << p[1].size()) + p[1].get_constant_value_u64().get(), p[0].size() + p[1].size()));
1211  }
1212  }
1213 
1214  // We intend to group slices into the same concatination, so that they maybe can be merged into one slice. We try to do this from right to left to make succeeding simplifications easier.
1215  if (p[0].is(BooleanFunction::NodeType::Slice) && p[1].is(BooleanFunction::NodeType::Concat))
1216  {
1217  auto p1_parameter = p[1].get_parameters();
1218 
1219  if (p1_parameter[0].is(BooleanFunction::NodeType::Slice))
1220  {
1221  auto p0_parameter = p[0].get_parameters();
1222  auto p10_parameter = p1_parameter[0].get_parameters();
1223 
1224  if (p0_parameter[0] == p10_parameter[0])
1225  {
1226  if (p1_parameter[1].is(BooleanFunction::NodeType::Slice))
1227  {
1228  auto p11_parameter = p1_parameter[1].get_parameters();
1229 
1230  // CONCAT(SLICE(X, i, j), CONCAT(SLICE(X, k, l), SLICE(Z, m, n))) => CONCAT(CONCAT(SLICE(X, i, j), SLICE(X, k, l)), SLICE(Z, m, n)))
1231  if (p11_parameter[0] != p10_parameter[0])
1232  {
1233  if (auto concatination = BooleanFunction::Concat(p[0].clone(), p1_parameter[0].clone(), p[0].size() + p1_parameter[0].size()); concatination.is_ok())
1234  {
1235  return BooleanFunction::Concat(concatination.get(), p1_parameter[1].clone(), concatination.get().size() + p1_parameter[1].size());
1236  }
1237  }
1238  }
1239  else if (p1_parameter[1].is(BooleanFunction::NodeType::Concat))
1240  {
1241  auto p11_parameter = p1_parameter[1].get_parameters();
1242 
1243  if (p11_parameter[0].is(BooleanFunction::NodeType::Slice))
1244  {
1245  auto p110_parameter = p11_parameter[0].get_parameters();
1246 
1247  // CONCAT(SLICE(X, i, j), CONCAT(SLICE(X, k, l), CONCAT(SLICE(Y, m, n), Z))) => CONCAT(CONCAT(SLICE(X, i, j), SLICE(X, k, l)), CONCAT(SLICE(Y, m, n), Z)))
1248  if (p110_parameter[0] != p10_parameter[0])
1249  {
1250  auto c1 = BooleanFunction::Concat(p[0].clone(), p1_parameter[0].clone(), p[0].size() + p1_parameter[0].size());
1251 
1252  return BooleanFunction::Concat(c1.get().clone(), p1_parameter[1].clone(), c1.get().size() + p1_parameter[1].size());
1253  }
1254  }
1255  }
1256  else
1257  {
1258  // CONCAT(SLICE(X, i, j), CONCAT(SLICE(X, k, l), Y)) => CONCAT(CONCAT(SLICE(X, i, j), SLICE(X, k, l)), Y))
1259  if (auto concatination = BooleanFunction::Concat(p[0].clone(), p1_parameter[0].clone(), p[0].size() + p1_parameter[0].size()); concatination.is_ok())
1260  {
1261  return BooleanFunction::Concat(concatination.get(), p1_parameter[1].clone(), concatination.get().size() + p1_parameter[1].size());
1262  }
1263  }
1264  }
1265  }
1266  }
1267 
1268  if (p[0].is(BooleanFunction::NodeType::Slice) && p[1].is(BooleanFunction::NodeType::Slice))
1269  {
1270  auto p0_parameter = p[0].get_parameters();
1271  auto p1_parameter = p[1].get_parameters();
1272 
1273  if (p0_parameter[0] == p1_parameter[0])
1274  {
1275  // CONCAT(SLICE(X, j+1, k), SLICE(X, i, j)) => SLICE(X, i, k)
1276  if ((p1_parameter[2].get_index_value().get() == (p0_parameter[1].get_index_value().get() - 1)))
1277  {
1278  return BooleanFunction::Slice(p0_parameter[0].clone(), p1_parameter[1].clone(), p0_parameter[2].clone(), p[0].size() + p[1].size());
1279  }
1280 
1281  // CONCAT(SLICE(X, j, j), SLICE(X, i, j)) => SEXT(SLICE(X, i, j), j-i+1)
1282  if ((p1_parameter[2].get_index_value().get() == p0_parameter[1].get_index_value().get())
1283  && (p1_parameter[2].get_index_value().get() == p0_parameter[2].get_index_value().get()))
1284  {
1285  return BooleanFunction::Sext(p[1].clone(), BooleanFunction::Index(p[1].size() + 1, p[1].size() + 1), p[1].size() + 1);
1286  }
1287  }
1288  }
1289 
1290  // CONCAT(SLICE(X, j, j), SEXT(SLICE(X, i, j), j-i+n)) => SEXT(SLICE(X, i, j), j-i+n+1)
1291  if (p[0].is(BooleanFunction::NodeType::Slice) && p[1].is(BooleanFunction::NodeType::Sext))
1292  {
1293  auto p1_parameter = p[1].get_parameters();
1294 
1295  if (p1_parameter[0].is(BooleanFunction::NodeType::Slice))
1296  {
1297  auto p0_parameter = p[0].get_parameters();
1298  auto p10_parameter = p1_parameter[0].get_parameters();
1299 
1300  if ((p0_parameter[0] == p10_parameter[0]) && (p0_parameter[1] == p0_parameter[2]) && (p0_parameter[1].get_index_value().get() == p10_parameter[2].get_index_value().get()))
1301  {
1302  return BooleanFunction::Sext(p1_parameter[0].clone(), BooleanFunction::Index(p[1].size() + 1, p[1].size() + 1), p[1].size() + 1);
1303  }
1304  }
1305  }
1306 
1307  // CONCAT(SLICE(X, j, j), CONCAT(SEXT(SLICE(X, i, j), j-i+n), Y)) => CONCAT(SEXT(SLICE(X, i, j), j-i+n+1), Y)
1308  if (p[0].is(BooleanFunction::NodeType::Slice) && p[1].is(BooleanFunction::NodeType::Concat))
1309  {
1310  auto p1_parameter = p[1].get_parameters();
1311 
1312  if (p1_parameter[0].is(BooleanFunction::NodeType::Sext))
1313  {
1314  auto p10_parameter = p1_parameter[0].get_parameters();
1315 
1316  if (p10_parameter[0].is(BooleanFunction::NodeType::Slice))
1317  {
1318  auto p0_parameter = p[0].get_parameters();
1319  auto p100_parameter = p10_parameter[0].get_parameters();
1320 
1321  if ((p0_parameter[0] == p100_parameter[0]) && (p0_parameter[1] == p0_parameter[2])
1322  && (p0_parameter[1].get_index_value().get() == p100_parameter[2].get_index_value().get()))
1323  {
1324  if (auto extension =
1325  BooleanFunction::Sext(p10_parameter[0].clone(), BooleanFunction::Index(p1_parameter[0].size() + 1, p1_parameter[0].size() + 1), p1_parameter[0].size() + 1);
1326  extension.is_ok())
1327  {
1328  return BooleanFunction::Concat(extension.get(), p1_parameter[1].clone(), extension.get().size() + p1_parameter[1].size());
1329  }
1330  }
1331  }
1332  }
1333  }
1334 
1335  return BooleanFunction::Concat(p[0].clone(), p[1].clone(), node.size);
1336  }
1337  case BooleanFunction::NodeType::Zext: {
1338  return BooleanFunction::Zext(p[0].clone(), p[1].clone(), node.size);
1339  }
1340  case BooleanFunction::NodeType::Sext: {
1341  return BooleanFunction::Sext(p[0].clone(), p[1].clone(), node.size);
1342  }
1343  case BooleanFunction::NodeType::Eq: {
1344  // X == X => 1
1345  if (p[0] == p[1])
1346  {
1347  return OK(BooleanFunction::Const(1, node.size));
1348  }
1349 
1350  return BooleanFunction::Eq(p[0].clone(), p[1].clone(), node.size);
1351  }
1352  case BooleanFunction::NodeType::Sle: {
1353  // X <=s X => 1
1354  if (p[0] == p[1])
1355  {
1356  return OK(BooleanFunction::Const(1, node.size));
1357  }
1358 
1359  return BooleanFunction::Sle(p[0].clone(), p[1].clone(), node.size);
1360  }
1361  case BooleanFunction::NodeType::Slt: {
1362  // X <s X => 0
1363  if (p[0] == p[1])
1364  {
1365  return OK(BooleanFunction::Const(0, node.size));
1366  }
1367 
1368  return BooleanFunction::Slt(p[0].clone(), p[1].clone(), node.size);
1369  }
1370  case BooleanFunction::NodeType::Ule: {
1371  // X <= X => 1
1372  if (p[0] == p[1])
1373  {
1374  return OK(BooleanFunction::Const(1, node.size));
1375  }
1376 
1377  return BooleanFunction::Ule(p[0].clone(), p[1].clone(), node.size);
1378  }
1379  case BooleanFunction::NodeType::Ult: {
1380  // X < 0 => 0
1381  if (p[1].has_constant_value(0))
1382  {
1383  return OK(BooleanFunction::Const(0, node.size));
1384  }
1385  // X < X => 0
1386  if (p[0] == p[1])
1387  {
1388  return OK(BooleanFunction::Const(0, node.size));
1389  }
1390 
1391  return BooleanFunction::Ult(p[0].clone(), p[1].clone(), node.size);
1392  }
1393  case BooleanFunction::NodeType::Ite: {
1394  // ITE(0, a, b) => b
1395  if (p[0].has_constant_value(0))
1396  {
1397  return OK(p[2]);
1398  }
1399  // ITE(1, a, b) => a
1400  if (p[0].has_constant_value(1))
1401  {
1402  return OK(p[1]);
1403  }
1404  // ITE(a, b, b) => b
1405  if (p[1] == p[2])
1406  {
1407  return OK(p[1]);
1408  }
1409 
1410  return BooleanFunction::Ite(p[0].clone(), p[1].clone(), p[2].clone(), node.size);
1411  }
1412  default:
1413  return ERR("could not simplify sub-expression in abstract syntax tree: not implemented for given node type");
1414  }
1415  }
1416 
1417  Result<BooleanFunction> SymbolicExecution::constant_propagation(const BooleanFunction::Node& node, std::vector<BooleanFunction>&& p)
1418  {
1419  if (node.get_arity() != p.size())
1420  {
1421  return ERR("could not propagate constants: arity does not match number of parameters");
1422  }
1423 
1424  std::vector<std::vector<BooleanFunction::Value>> values;
1425  std::vector<u16> indices;
1426 
1427  for (const auto& parameter : p)
1428  {
1429  if (parameter.is_index())
1430  {
1431  indices.push_back(parameter.get_index_value().get());
1432  }
1433  else
1434  {
1435  const auto v = parameter.get_top_level_node().constant;
1436  values.emplace_back(v);
1437  }
1438  }
1439 
1440  switch (node.type)
1441  {
1442  case BooleanFunction::NodeType::And:
1443  return OK(ConstantPropagation::And(values[0], values[1]));
1444  case BooleanFunction::NodeType::Or:
1445  return OK(ConstantPropagation::Or(values[0], values[1]));
1446  case BooleanFunction::NodeType::Not:
1447  return OK(ConstantPropagation::Not(values[0]));
1448  case BooleanFunction::NodeType::Xor:
1449  return OK(ConstantPropagation::Xor(values[0], values[1]));
1450 
1451  case BooleanFunction::NodeType::Add:
1452  return OK(ConstantPropagation::Add(values[0], values[1]));
1453  case BooleanFunction::NodeType::Sub:
1454  return OK(ConstantPropagation::Sub(values[0], values[1]));
1455  case BooleanFunction::NodeType::Mul:
1456  return OK(ConstantPropagation::Mul(values[0], values[1]));
1457 
1458  case BooleanFunction::NodeType::Sdiv: {
1459  // TODO implement
1460  return ERR("could not propagate constants: not implemented for given node type");
1461  }
1462  case BooleanFunction::NodeType::Udiv: {
1463  // TODO implement
1464  return ERR("could not propagate constants: not implemented for given node type");
1465  }
1466  case BooleanFunction::NodeType::Srem: {
1467  // TODO implement
1468  return ERR("could not propagate constants: not implemented for given node type");
1469  }
1470  case BooleanFunction::NodeType::Urem: {
1471  // TODO implement
1472  return ERR("could not propagate constants: not implemented for given node type");
1473  }
1474 
1475  case BooleanFunction::NodeType::Concat: {
1476  values[1].insert(values[1].end(), values[0].begin(), values[0].end());
1477  return OK(BooleanFunction::Const(values[1]));
1478  }
1479  case BooleanFunction::NodeType::Slice: {
1480  auto start = p[1].get_index_value().get();
1481  auto end = p[2].get_index_value().get();
1482  return OK(BooleanFunction::Const(std::vector<BooleanFunction::Value>(values[0].begin() + start, values[0].begin() + end + 1)));
1483  }
1484  case BooleanFunction::NodeType::Zext: {
1485  values[0].resize(node.size, BooleanFunction::Value::ZERO);
1486  return OK(BooleanFunction::Const(values[0]));
1487  }
1488  case BooleanFunction::NodeType::Sext: {
1489  values[0].resize(node.size, static_cast<BooleanFunction::Value>(values[0].back()));
1490  return OK(BooleanFunction::Const(values[0]));
1491  }
1492 
1493  case BooleanFunction::NodeType::Shl:
1494  return OK(ConstantPropagation::Shl(values[0], indices[0]));
1495  case BooleanFunction::NodeType::Lshr:
1496  return OK(ConstantPropagation::Lshr(values[0], indices[0]));
1497  case BooleanFunction::NodeType::Ashr:
1498  return OK(ConstantPropagation::Ashr(values[0], indices[0]));
1499  case BooleanFunction::NodeType::Rol:
1500  return OK(ConstantPropagation::Rol(values[0], indices[0]));
1501  case BooleanFunction::NodeType::Ror:
1502  return OK(ConstantPropagation::Ror(values[0], indices[0]));
1503 
1504  case BooleanFunction::NodeType::Eq:
1505  return OK((values[0] == values[1]) ? BooleanFunction::Const(1, 1) : BooleanFunction::Const(0, 1));
1506  case BooleanFunction::NodeType::Sle:
1507  return OK(ConstantPropagation::Sle(values[0], values[1]));
1508  case BooleanFunction::NodeType::Slt:
1509  return OK(ConstantPropagation::Slt(values[0], values[1]));
1510  case BooleanFunction::NodeType::Ule:
1511  return OK(ConstantPropagation::Ule(values[0], values[1]));
1512  case BooleanFunction::NodeType::Ult:
1513  return OK(ConstantPropagation::Ult(values[0], values[1]));
1514  case BooleanFunction::NodeType::Ite:
1515  return OK(ConstantPropagation::Ite(values[0], values[1], values[2]));
1516 
1517  default:
1518  return ERR("could not propagate constants: not implemented for given node type");
1519  }
1520  }
1521  } // namespace SMT
1522 } // namespace hal
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
hal::BooleanFunction::to_u64
static Result< u64 > to_u64(const std::vector< BooleanFunction::Value > &value)
Definition: boolean_function.cpp:208
hal::SMT::SymbolicExecution::SymbolicExecution
SymbolicExecution(const std::vector< BooleanFunction > &variables={})
Definition: symbolic_execution.cpp:548
hal::SMT::SymbolicExecution::evaluate
Result< BooleanFunction > evaluate(const BooleanFunction &function) const
Definition: symbolic_execution.cpp:552
u16
uint16_t u16
Definition: defines.h:40
i64
int64_t i64
Definition: defines.h:37
u8
uint8_t u8
Definition: defines.h:39
i32
int32_t i32
Definition: defines.h:36
ERR
#define ERR(message)
Definition: result.h:53
OK
#define OK(...)
Definition: result.h:49
ERR_APPEND
#define ERR_APPEND(prev_error, message)
Definition: result.h:57
hal::SMT::ConstantPropagation::Slt
BooleanFunction Slt(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:419
hal::SMT::ConstantPropagation::Or
BooleanFunction Or(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:46
hal::SMT::ConstantPropagation::Not
BooleanFunction Not(const std::vector< BooleanFunction::Value > &p)
Definition: symbolic_execution.cpp:74
hal::SMT::ConstantPropagation::Sle
BooleanFunction Sle(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:379
hal::SMT::ConstantPropagation::Ite
BooleanFunction Ite(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1, const std::vector< BooleanFunction::Value > &p2)
Definition: symbolic_execution.cpp:516
hal::SMT::ConstantPropagation::Ule
BooleanFunction Ule(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:457
hal::SMT::ConstantPropagation::Rol
BooleanFunction Rol(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:324
hal::SMT::ConstantPropagation::Ult
BooleanFunction Ult(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:486
hal::SMT::ConstantPropagation::Shl
BooleanFunction Shl(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:244
hal::SMT::ConstantPropagation::Mul
BooleanFunction Mul(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:214
hal::SMT::ConstantPropagation::Ror
BooleanFunction Ror(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:352
hal::SMT::ConstantPropagation::Sub
BooleanFunction Sub(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:173
hal::SMT::ConstantPropagation::Add
BooleanFunction Add(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:132
hal::SMT::ConstantPropagation::Ashr
BooleanFunction Ashr(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:296
hal::SMT::ConstantPropagation::Xor
BooleanFunction Xor(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:103
hal::SMT::ConstantPropagation::And
BooleanFunction And(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:17
hal::SMT::ConstantPropagation::Lshr
BooleanFunction Lshr(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:270
u32
quint32 u32
Definition: net_layout_point.h:40
hal::SMT::Constraint::is_assignment
bool is_assignment() const
Definition: types.cpp:173
hal::SMT::Constraint::get_assignment
Result< const std::pair< BooleanFunction, BooleanFunction > * > get_assignment() const
Definition: types.cpp:178
symbolic_execution.h