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