HAL  v4.5.0-83-g30c8f0afc
The Hardware Analyzer - a comprehensive reverse engineering and manipulation framework for gate-level netlists.
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  {
10  namespace
11  {
15  std::vector<BooleanFunction::Value> to_values(u64 value, u16 size)
16  {
17  std::vector<BooleanFunction::Value> res;
18  res.reserve(size);
19  for (u16 i = 0; i < size; i++)
20  {
21  res.emplace_back(((value >> i) & 1) ? BooleanFunction::Value::ONE : BooleanFunction::Value::ZERO);
22  }
23  return res;
24  }
25  } // namespace
33  std::vector<BooleanFunction::Value> And(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
34  {
35  std::vector<BooleanFunction::Value> simplified;
36  simplified.reserve(p0.size());
37  for (auto i = 0u; i < p0.size(); i++)
38  {
39  if ((p0[i] == 0) || (p1[i] == 0))
40  {
41  simplified.emplace_back(BooleanFunction::Value::ZERO);
42  }
43  else if ((p0[i] == 1) && (p1[i] == 1))
44  {
45  simplified.emplace_back(BooleanFunction::Value::ONE);
46  }
47  else
48  {
49  simplified.emplace_back(BooleanFunction::Value::X);
50  }
51  }
52  return simplified;
53  }
54 
62  std::vector<BooleanFunction::Value> Or(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
63  {
64  std::vector<BooleanFunction::Value> simplified;
65  simplified.reserve(p0.size());
66  for (auto i = 0u; i < p0.size(); i++)
67  {
68  if ((p0[i] == 0) && (p1[i] == 0))
69  {
70  simplified.emplace_back(BooleanFunction::Value::ZERO);
71  }
72  else if ((p0[i] == 1) || (p1[i] == 1))
73  {
74  simplified.emplace_back(BooleanFunction::Value::ONE);
75  }
76  else
77  {
78  simplified.emplace_back(BooleanFunction::Value::X);
79  }
80  }
81  return simplified;
82  }
83 
90  std::vector<BooleanFunction::Value> Not(const std::vector<BooleanFunction::Value>& p)
91  {
92  std::vector<BooleanFunction::Value> simplified;
93  simplified.reserve(p.size());
94  for (const auto& value : p)
95  {
96  if (value == BooleanFunction::Value::ZERO)
97  {
98  simplified.emplace_back(BooleanFunction::Value::ONE);
99  }
100  else if (value == BooleanFunction::Value::ONE)
101  {
102  simplified.emplace_back(BooleanFunction::Value::ZERO);
103  }
104  else
105  {
106  simplified.emplace_back(value);
107  }
108  }
109  return simplified;
110  }
111 
119  std::vector<BooleanFunction::Value> Xor(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
120  {
121  std::vector<BooleanFunction::Value> simplified;
122  simplified.reserve(p0.size());
123  for (auto i = 0u; i < p0.size(); i++)
124  {
125  if (((p0[i] == 0) && (p1[i] == 1)) || ((p0[i] == 1) && (p1[i] == 0)))
126  {
127  simplified.emplace_back(BooleanFunction::Value::ONE);
128  }
129  else if (((p0[i] == 0) && (p1[i] == 0)) || ((p0[i] == 1) && (p1[i] == 1)))
130  {
131  simplified.emplace_back(BooleanFunction::Value::ZERO);
132  }
133  else
134  {
135  simplified.emplace_back(BooleanFunction::Value::X);
136  }
137  }
138  return simplified;
139  }
140 
148  std::vector<BooleanFunction::Value> Add(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
149  {
150  if (p0.size() <= 64 && p1.size() <= 64)
151  {
152  const auto a_res = BooleanFunction::to_u64(p0);
153  const auto b_res = BooleanFunction::to_u64(p1);
154 
155  if (a_res.is_ok() && b_res.is_ok())
156  {
157  // no mask needed, Const() takes exactly p0.size() bits. Masking to 32 bit here
158  // silently truncated every result of a wider operation.
159  const auto res = a_res.get() + b_res.get();
160  return to_values(res, p0.size());
161  }
162 
163  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
164  }
165 
166  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
167  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
168  {
169  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
170  }
171 
172  std::vector<BooleanFunction::Value> simplified;
173  simplified.reserve(p0.size());
174  auto carry = BooleanFunction::Value::ZERO;
175  for (auto i = 0u; i < p0.size(); i++)
176  {
177  auto res = p0[i] + p1[i] + carry;
178  simplified.emplace_back(static_cast<BooleanFunction::Value>(res & 0x1));
179  carry = static_cast<BooleanFunction::Value>(res >> 1);
180  }
181  return simplified;
182  }
183 
191  std::vector<BooleanFunction::Value> Sub(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
192  {
193  if (p0.size() <= 64 && p1.size() <= 64)
194  {
195  const auto a_res = BooleanFunction::to_u64(p0);
196  const auto b_res = BooleanFunction::to_u64(p1);
197 
198  if (a_res.is_ok() && b_res.is_ok())
199  {
200  // no mask needed, Const() takes exactly p0.size() bits. Masking to 32 bit here
201  // silently truncated every result of a wider operation.
202  const auto res = a_res.get() - b_res.get();
203  return to_values(res, p0.size());
204  }
205 
206  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
207  }
208 
209  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
210  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
211  {
212  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
213  }
214 
215  std::vector<BooleanFunction::Value> simplified;
216  simplified.reserve(p0.size());
217  auto carry = BooleanFunction::Value::ONE;
218  for (auto i = 0u; i < p0.size(); i++)
219  {
220  auto res = p0[i] + !(p1[i]) + carry;
221  simplified.emplace_back(static_cast<BooleanFunction::Value>(res & 0x1));
222  carry = static_cast<BooleanFunction::Value>(res >> 1);
223  }
224  return simplified;
225  }
226 
234  std::vector<BooleanFunction::Value> Mul(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
235  {
236  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
237  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
238  {
239  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
240  }
241 
242  auto bitsize = p0.size();
243  std::vector<BooleanFunction::Value> simplified(bitsize, BooleanFunction::Value::ZERO);
244  for (auto i = 0u; i < bitsize; i++)
245  {
246  auto carry = BooleanFunction::Value::ZERO;
247  for (auto j = 0u; j < bitsize - i; j++)
248  {
249  auto res = simplified[i + j] + (p0[i] & p1[j]) + carry;
250  simplified[i + j] = static_cast<BooleanFunction::Value>(res & 0x1);
251  carry = static_cast<BooleanFunction::Value>(res >> 1);
252  }
253  }
254  return simplified;
255  }
256 
261  namespace
262  {
263  bool is_zero(const std::vector<BooleanFunction::Value>& value)
264  {
265  return std::all_of(value.begin(), value.end(), [](auto v) { return v == BooleanFunction::Value::ZERO; });
266  }
267 
268  bool is_negative(const std::vector<BooleanFunction::Value>& value)
269  {
270  return value.back() == BooleanFunction::Value::ONE;
271  }
272 
276  bool greater_equal_unsigned(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
277  {
278  for (auto i = p0.size(); i-- > 0;)
279  {
280  if (p0[i] != p1[i])
281  {
282  return p0[i] == BooleanFunction::Value::ONE;
283  }
284  }
285  return true;
286  }
287 
291  std::vector<BooleanFunction::Value> subtract(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
292  {
293  std::vector<BooleanFunction::Value> res;
294  res.reserve(p0.size());
295 
296  auto borrow = 0;
297  for (auto i = 0u; i < p0.size(); i++)
298  {
299  const auto difference = static_cast<int>(p0[i]) - static_cast<int>(p1[i]) - borrow;
300  borrow = (difference < 0) ? 1 : 0;
301  res.emplace_back(static_cast<BooleanFunction::Value>(difference & 1));
302  }
303  return res;
304  }
305 
309  std::vector<BooleanFunction::Value> negate(const std::vector<BooleanFunction::Value>& value)
310  {
311  return subtract(std::vector<BooleanFunction::Value>(value.size(), BooleanFunction::Value::ZERO), value);
312  }
313 
323  std::pair<std::vector<BooleanFunction::Value>, std::vector<BooleanFunction::Value>> divide_unsigned(const std::vector<BooleanFunction::Value>& dividend,
324  const std::vector<BooleanFunction::Value>& divisor)
325  {
326  const auto size = dividend.size();
327 
328  if (is_zero(divisor))
329  {
330  return {std::vector<BooleanFunction::Value>(size, BooleanFunction::Value::ONE), dividend};
331  }
332 
333  // the shifted remainder needs one bit more than the operands to not overflow
334  auto divisor_extended = divisor;
335  divisor_extended.push_back(BooleanFunction::Value::ZERO);
336 
337  std::vector<BooleanFunction::Value> quotient(size, BooleanFunction::Value::ZERO);
338  std::vector<BooleanFunction::Value> remainder(size + 1, BooleanFunction::Value::ZERO);
339 
340  for (auto i = size; i-- > 0;)
341  {
342  for (auto j = remainder.size(); j-- > 1;)
343  {
344  remainder[j] = remainder[j - 1];
345  }
346  remainder[0] = dividend[i];
347 
348  if (greater_equal_unsigned(remainder, divisor_extended))
349  {
350  remainder = subtract(remainder, divisor_extended);
351  quotient[i] = BooleanFunction::Value::ONE;
352  }
353  }
354 
355  remainder.pop_back();
356  return {quotient, remainder};
357  }
358 
359  bool any_undefined(const std::vector<BooleanFunction::Value>& value)
360  {
361  return std::any_of(value.begin(), value.end(), [](auto v) { return v == BooleanFunction::Value::X || v == BooleanFunction::Value::Z; });
362  }
363  } // namespace
364 
375  std::vector<BooleanFunction::Value> Eq(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
376  {
377  auto undefined = false;
378  for (auto i = 0u; i < p0.size(); i++)
379  {
380  if ((p0[i] == BooleanFunction::Value::X) || (p0[i] == BooleanFunction::Value::Z) || (p1[i] == BooleanFunction::Value::X) || (p1[i] == BooleanFunction::Value::Z))
381  {
382  undefined = true;
383  }
384  else if (p0[i] != p1[i])
385  {
386  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ZERO});
387  }
388  }
389 
390  return undefined ? std::vector<BooleanFunction::Value>({BooleanFunction::Value::X}) : std::vector<BooleanFunction::Value>({BooleanFunction::Value::ONE});
391  }
392 
400  std::vector<BooleanFunction::Value> Udiv(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
401  {
402  if (any_undefined(p0) || any_undefined(p1))
403  {
404  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
405  }
406 
407  return divide_unsigned(p0, p1).first;
408  }
409 
417  std::vector<BooleanFunction::Value> Urem(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
418  {
419  if (any_undefined(p0) || any_undefined(p1))
420  {
421  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
422  }
423 
424  return divide_unsigned(p0, p1).second;
425  }
426 
436  std::vector<BooleanFunction::Value> Sdiv(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
437  {
438  if (any_undefined(p0) || any_undefined(p1))
439  {
440  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
441  }
442 
443  const auto dividend_negative = is_negative(p0), divisor_negative = is_negative(p1);
444 
445  if (!dividend_negative && !divisor_negative)
446  {
447  return divide_unsigned(p0, p1).first;
448  }
449  if (dividend_negative && !divisor_negative)
450  {
451  return negate(divide_unsigned(negate(p0), p1).first);
452  }
453  if (!dividend_negative && divisor_negative)
454  {
455  return negate(divide_unsigned(p0, negate(p1)).first);
456  }
457  return divide_unsigned(negate(p0), negate(p1)).first;
458  }
459 
469  std::vector<BooleanFunction::Value> Srem(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
470  {
471  if (any_undefined(p0) || any_undefined(p1))
472  {
473  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
474  }
475 
476  const auto dividend_negative = is_negative(p0), divisor_negative = is_negative(p1);
477 
478  if (!dividend_negative && !divisor_negative)
479  {
480  return divide_unsigned(p0, p1).second;
481  }
482  if (dividend_negative && !divisor_negative)
483  {
484  return negate(divide_unsigned(negate(p0), p1).second);
485  }
486  if (!dividend_negative && divisor_negative)
487  {
488  return divide_unsigned(p0, negate(p1)).second;
489  }
490  return negate(divide_unsigned(negate(p0), negate(p1)).second);
491  }
492 
500  std::vector<BooleanFunction::Value> Shl(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
501  {
502  if (p1 >= p0.size())
503  {
504  // Shift amount is too large, result is all zeros
505  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::ZERO);
506  }
507 
508  std::vector<BooleanFunction::Value> result(p0.size(), BooleanFunction::Value::ZERO);
509 
510  // Copy bits from original position to shifted position
511  for (auto i = p1; i < p0.size(); i++)
512  {
513  result[i] = p0[i - p1];
514  }
515 
516  return result;
517  }
518 
526  std::vector<BooleanFunction::Value> Lshr(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
527  {
528  if (p1 >= p0.size())
529  {
530  // Shift amount is too large, result is all zeros
531  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::ZERO);
532  }
533 
534  std::vector<BooleanFunction::Value> result(p0.size(), BooleanFunction::Value::ZERO);
535 
536  // Copy bits from original position to shifted position
537  for (auto i = 0u; i < p0.size() - p1; i++)
538  {
539  result[i] = p0[i + p1];
540  }
541 
542  return result;
543  }
544 
552  std::vector<BooleanFunction::Value> Ashr(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
553  {
554  auto sign_bit = p0.back(); // MSB is the sign bit
555 
556  if (p1 >= p0.size())
557  {
558  // Shift amount is too large, result is all sign bits
559  return std::vector<BooleanFunction::Value>(p0.size(), sign_bit);
560  }
561 
562  std::vector<BooleanFunction::Value> result(p0.size(), sign_bit);
563 
564  // Copy bits from original position to shifted position
565  for (auto i = 0u; i < p0.size() - p1; i++)
566  {
567  result[i] = p0[i + p1];
568  }
569 
570  return result;
571  }
572 
580  std::vector<BooleanFunction::Value> Rol(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
581  {
582  auto rotate_amount = p1 % p0.size(); // Modulo for rotation
583 
584  if (rotate_amount == 0)
585  {
586  return p0; // No rotation needed
587  }
588 
589  std::vector<BooleanFunction::Value> result(p0.size());
590 
591  // Perform the rotation
592  for (auto i = 0u; i < p0.size(); i++)
593  {
594  auto new_pos = (i + rotate_amount) % p0.size();
595  result[new_pos] = p0[i];
596  }
597 
598  return result;
599  }
600 
608  std::vector<BooleanFunction::Value> Ror(const std::vector<BooleanFunction::Value>& p0, const u16 p1)
609  {
610  auto rotate_amount = p1 % p0.size(); // Modulo for rotation
611 
612  if (rotate_amount == 0)
613  {
614  return p0; // No rotation needed
615  }
616 
617  std::vector<BooleanFunction::Value> result(p0.size());
618 
619  // Perform the rotation
620  for (auto i = 0u; i < p0.size(); i++)
621  {
622  auto new_pos = (i + p0.size() - rotate_amount) % p0.size();
623  result[new_pos] = p0[i];
624  }
625 
626  return result;
627  }
635  std::vector<BooleanFunction::Value> Sle(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
636  {
637  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
638  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
639  {
640  return {BooleanFunction::Value::X};
641  }
642 
643  auto msb_p0 = p0.back();
644  auto msb_p1 = p1.back();
645  if (msb_p0 == BooleanFunction::Value::ONE && msb_p1 == BooleanFunction::Value::ZERO)
646  {
647  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ONE});
648  }
649  else if (msb_p0 == BooleanFunction::Value::ZERO && msb_p1 == BooleanFunction::Value::ONE)
650  {
651  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ZERO});
652  }
653 
654  std::vector<BooleanFunction::Value> simplified;
655  u8 carry = 1;
656  u8 neq = 0;
657  u8 res = 0;
658  for (auto i = 0u; i < p0.size(); i++)
659  {
660  res = p0[i] + !(p1[i]) + carry;
661  carry = res >> 1;
662  neq |= res & 1;
663  }
664 
665  return {static_cast<BooleanFunction::Value>((res & 1) | !neq)};
666  }
667 
675  std::vector<BooleanFunction::Value> Slt(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
676  {
677  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
678  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
679  {
680  return {BooleanFunction::Value::X};
681  }
682 
683  auto msb_p0 = p0.back();
684  auto msb_p1 = p1.back();
685  if (msb_p0 == BooleanFunction::Value::ONE && msb_p1 == BooleanFunction::Value::ZERO)
686  {
687  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ONE});
688  }
689  else if (msb_p0 == BooleanFunction::Value::ZERO && msb_p1 == BooleanFunction::Value::ONE)
690  {
691  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ZERO});
692  }
693 
694  std::vector<BooleanFunction::Value> simplified;
695  u8 res = 0;
696  u8 carry = 1;
697  for (auto i = 0u; i < p0.size(); i++)
698  {
699  res = p0[i] + !(p1[i]) + carry;
700  carry = (res >> 1) & 1;
701  }
702 
703  return {static_cast<BooleanFunction::Value>(res & 1)};
704  }
705 
713  std::vector<BooleanFunction::Value> Ule(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
714  {
715  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
716  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
717  {
718  return {BooleanFunction::Value::X};
719  }
720 
721  for (i32 i = p0.size() - 1; i >= 0; i--)
722  {
723  if (p0[i] == BooleanFunction::Value::ONE && p1[i] == BooleanFunction::Value::ZERO)
724  {
725  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ZERO});
726  }
727  else if (p0[i] == BooleanFunction::Value::ZERO && p1[i] == BooleanFunction::Value::ONE)
728  {
729  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ONE});
730  }
731  }
732  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ONE});
733  }
734 
742  std::vector<BooleanFunction::Value> Ult(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1)
743  {
744  if (std::any_of(p0.begin(), p0.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; })
745  || std::any_of(p1.begin(), p1.end(), [](auto val) { return val == BooleanFunction::Value::X || val == BooleanFunction::Value::Z; }))
746  {
747  return {BooleanFunction::Value::X};
748  }
749 
750  for (i32 i = p0.size() - 1; i >= 0; i--)
751  {
752  if (p0[i] == BooleanFunction::Value::ONE && p1[i] == BooleanFunction::Value::ZERO)
753  {
754  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ZERO});
755  }
756  else if (p0[i] == BooleanFunction::Value::ZERO && p1[i] == BooleanFunction::Value::ONE)
757  {
758  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ONE});
759  }
760  }
761  return std::vector<BooleanFunction::Value>({BooleanFunction::Value::ZERO});
762  }
763 
772  std::vector<BooleanFunction::Value> Ite(const std::vector<BooleanFunction::Value>& p0, const std::vector<BooleanFunction::Value>& p1, const std::vector<BooleanFunction::Value>& p2)
773  {
774  if (p0.front() == BooleanFunction::Value::ONE)
775  {
776  return p1;
777  }
778  else if (p0.front() == BooleanFunction::Value::ZERO)
779  {
780  return p2;
781  }
782  else
783  {
784  return std::vector<BooleanFunction::Value>(p0.size(), BooleanFunction::Value::X);
785  }
786  }
787 
800  Result<std::vector<BooleanFunction::Value>> fold(const BooleanFunction::Node& node,
801  std::vector<std::vector<BooleanFunction::Value>>& values,
802  const std::vector<u16>& indices)
803  {
804  UNUSED(indices);
805  switch (node.type)
806  {
807  case BooleanFunction::NodeType::And:
808  return OK(ConstantPropagation::And(values[0], values[1]));
809  case BooleanFunction::NodeType::Or:
810  return OK(ConstantPropagation::Or(values[0], values[1]));
811  case BooleanFunction::NodeType::Not:
812  return OK(ConstantPropagation::Not(values[0]));
813  case BooleanFunction::NodeType::Xor:
814  return OK(ConstantPropagation::Xor(values[0], values[1]));
815 
816  case BooleanFunction::NodeType::Add:
817  return OK(ConstantPropagation::Add(values[0], values[1]));
818  case BooleanFunction::NodeType::Sub:
819  return OK(ConstantPropagation::Sub(values[0], values[1]));
820  case BooleanFunction::NodeType::Mul:
821  return OK(ConstantPropagation::Mul(values[0], values[1]));
822 
823  case BooleanFunction::NodeType::Sdiv:
824  return OK(ConstantPropagation::Sdiv(values[0], values[1]));
825  case BooleanFunction::NodeType::Udiv:
826  return OK(ConstantPropagation::Udiv(values[0], values[1]));
827  case BooleanFunction::NodeType::Srem:
828  return OK(ConstantPropagation::Srem(values[0], values[1]));
829  case BooleanFunction::NodeType::Urem:
830  return OK(ConstantPropagation::Urem(values[0], values[1]));
831 
832  case BooleanFunction::NodeType::Concat: {
833  values[1].insert(values[1].end(), values[0].begin(), values[0].end());
834  return OK((values[1]));
835  }
836  case BooleanFunction::NodeType::Slice: {
837  auto start = indices[0];
838  auto end = indices[1];
839  return OK((std::vector<BooleanFunction::Value>(values[0].begin() + start, values[0].begin() + end + 1)));
840  }
841  case BooleanFunction::NodeType::Zext: {
842  values[0].resize(node.size, BooleanFunction::Value::ZERO);
843  return OK((values[0]));
844  }
845  case BooleanFunction::NodeType::Sext: {
846  values[0].resize(node.size, static_cast<BooleanFunction::Value>(values[0].back()));
847  return OK((values[0]));
848  }
849 
850  case BooleanFunction::NodeType::Shl:
851  return OK(ConstantPropagation::Shl(values[0], indices[0]));
852  case BooleanFunction::NodeType::Lshr:
853  return OK(ConstantPropagation::Lshr(values[0], indices[0]));
854  case BooleanFunction::NodeType::Ashr:
855  return OK(ConstantPropagation::Ashr(values[0], indices[0]));
856  case BooleanFunction::NodeType::Rol:
857  return OK(ConstantPropagation::Rol(values[0], indices[0]));
858  case BooleanFunction::NodeType::Ror:
859  return OK(ConstantPropagation::Ror(values[0], indices[0]));
860 
861  case BooleanFunction::NodeType::Eq:
862  return OK(ConstantPropagation::Eq(values[0], values[1]));
863  case BooleanFunction::NodeType::Sle:
864  return OK(ConstantPropagation::Sle(values[0], values[1]));
865  case BooleanFunction::NodeType::Slt:
866  return OK(ConstantPropagation::Slt(values[0], values[1]));
867  case BooleanFunction::NodeType::Ule:
868  return OK(ConstantPropagation::Ule(values[0], values[1]));
869  case BooleanFunction::NodeType::Ult:
870  return OK(ConstantPropagation::Ult(values[0], values[1]));
871  case BooleanFunction::NodeType::Ite:
872  return OK(ConstantPropagation::Ite(values[0], values[1], values[2]));
873 
874  default:
875  return ERR("could not propagate constants: not implemented for given node type");
876  }
877  }
878 
879  } // namespace ConstantPropagation
880 
881  namespace
882  {
889  BooleanFunction One(u16 size)
890  {
891  return BooleanFunction::Const(std::vector<BooleanFunction::Value>(size, BooleanFunction::Value::ONE));
892  }
893  } // namespace
894 
895  SymbolicExecution::SymbolicExecution(const std::vector<BooleanFunction>& variables) : state(SymbolicState(variables))
896  {
897  }
898 
899  std::optional<std::vector<BooleanFunction::Value>> SymbolicExecution::evaluate_constant(const BooleanFunction& function) const
900  {
901  // Resolve the bindings once by name. Going through SymbolicState::get() per variable would build
902  // a temporary Var() and look it up in a std::map keyed by whole Boolean functions, which compares
903  // them node by node and therefore string by string.
904  const auto bindings = this->state.get_bindings();
905 
906  std::vector<std::vector<BooleanFunction::Value>> values;
907  std::vector<u16> indices;
908 
909  // operands of a node are the trailing entries of the two stacks, an operation consumes as many of
910  // them as its arity and pushes its result back
911  std::vector<std::vector<BooleanFunction::Value>> operands;
912  std::vector<u16> operand_indices;
913 
914  for (const auto& node : function.get_nodes())
915  {
916  if (node.is_constant())
917  {
918  values.push_back(node.constant);
919  continue;
920  }
921 
922  if (node.is_index())
923  {
924  indices.push_back(node.index);
925  continue;
926  }
927 
928  if (node.is_variable())
929  {
930  const auto it = bindings.find(node.variable);
931  if ((it == bindings.end()) || !it->second->is_constant() || (it->second->size() != node.size))
932  {
933  return std::nullopt; // not bound to a constant, the general path has to take over
934  }
935  values.push_back(it->second->get_top_level_node().constant);
936  continue;
937  }
938 
939  // an operation, collect its operands from the back of the stacks. Which of the two a given
940  // operand sits on is decided by the node type, so count the index operands it expects.
941  const auto arity = node.get_arity();
942  const auto index_arity = (node.type == BooleanFunction::NodeType::Slice) ? 2
943  : (node.type == BooleanFunction::NodeType::Zext || node.type == BooleanFunction::NodeType::Sext
944  || node.type == BooleanFunction::NodeType::Shl || node.type == BooleanFunction::NodeType::Lshr
945  || node.type == BooleanFunction::NodeType::Ashr || node.type == BooleanFunction::NodeType::Rol
946  || node.type == BooleanFunction::NodeType::Ror)
947  ? 1
948  : 0;
949  const auto value_arity = arity - index_arity;
950 
951  if (values.size() < value_arity || indices.size() < index_arity)
952  {
953  return std::nullopt;
954  }
955 
956  operands.assign(std::make_move_iterator(values.end() - value_arity), std::make_move_iterator(values.end()));
957  values.erase(values.end() - value_arity, values.end());
958  operand_indices.assign(indices.end() - index_arity, indices.end());
959  indices.erase(indices.end() - index_arity, indices.end());
960 
961  auto folded = ConstantPropagation::fold(node, operands, operand_indices);
962  if (folded.is_error())
963  {
964  return std::nullopt;
965  }
966  values.push_back(folded.get());
967  }
968 
969  if ((values.size() != 1) || !indices.empty())
970  {
971  return std::nullopt;
972  }
973  return values.front();
974  }
975 
976  Result<BooleanFunction> SymbolicExecution::evaluate(const BooleanFunction& function) const
977  {
978  // Whenever every variable of the function is bound to a constant, which is the case for anything
979  // computing a truth table, the whole result is a constant and no sub-expression can survive. The
980  // general path below would still build a Boolean function per node, each owning a vector of nodes
981  // that own a string and a vector of values, which costs several allocations per operation. Fold
982  // the values directly instead and fall back to the general path as soon as that is not possible.
983  if (auto folded = this->evaluate_constant(function); folded.has_value())
984  {
985  return OK(BooleanFunction::Const(folded.value()));
986  }
987 
988  std::vector<BooleanFunction> stack;
989  for (const auto& node : function.get_nodes())
990  {
991  std::vector<BooleanFunction> parameters;
992  std::move(stack.end() - static_cast<i64>(node.get_arity()), stack.end(), std::back_inserter(parameters));
993  stack.erase(stack.end() - static_cast<i64>(node.get_arity()), stack.end());
994 
995  if (auto simplified = this->simplify(node, std::move(parameters)); simplified.is_ok())
996  {
997  stack.emplace_back(simplified.get());
998  }
999  else
1000  {
1001  return ERR_APPEND(simplified.get_error(), "could not evaluate Boolean function within symbolic state: simplification failed");
1002  }
1003  }
1004 
1005  switch (stack.size())
1006  {
1007  case 1:
1008  return OK(stack.back());
1009  default:
1010  return ERR("could not evaluate Boolean function within symbolic state: stack is imbalanced");
1011  }
1012  }
1013 
1014  Result<std::monostate> SymbolicExecution::evaluate(const Constraint& constraint)
1015  {
1016  if (constraint.is_assignment())
1017  {
1018  const auto& assignment = constraint.get_assignment().get();
1019  if (auto res = this->evaluate(assignment->first).map<std::monostate>([&](auto&& rhs) -> Result<std::monostate> {
1020  this->state.set(assignment->second.clone(), std::move(rhs));
1021  return OK({});
1022  });
1023  res.is_error())
1024  {
1025  return ERR_APPEND(res.get_error(), "could not to evaluate assignment constraint within the symbolic state: evaluation failed");
1026  }
1027  else
1028  {
1029  return OK({});
1030  }
1031  }
1032  else
1033  {
1034  const auto& function = constraint.get_function().get();
1035  auto node_type = function->get_top_level_node().type;
1036  if (!(node_type == BooleanFunction::NodeType::Eq || node_type == BooleanFunction::NodeType::Slt || node_type == BooleanFunction::NodeType::Sle
1037  || node_type == BooleanFunction::NodeType::Ult || node_type == BooleanFunction::NodeType::Ule))
1038  {
1039  return ERR("invalid node type in function '" + function->to_string() + "'");
1040  }
1041  if (auto res = this->evaluate(*function); res.is_error())
1042  {
1043  return ERR_APPEND(res.get_error(), "could not to evaluate function constraint within the symbolic state: evaluation failed");
1044  }
1045  else
1046  {
1047  return OK({});
1048  }
1049  }
1050  }
1051 
1052  std::vector<BooleanFunction> SymbolicExecution::normalize(std::vector<BooleanFunction>&& p)
1053  {
1054  if (p.size() <= 1ul)
1055  {
1056  return std::move(p);
1057  }
1058 
1059  std::sort(p.begin(), p.end(), [](const auto& lhs, const auto& rhs) {
1060  if (lhs.get_top_level_node().type == rhs.get_top_level_node().type)
1061  {
1062  return lhs < rhs;
1063  }
1064  return rhs.is_constant();
1065  });
1066  return std::move(p);
1067  }
1068 
1069  namespace
1070  {
1074  bool is_x_not_y(const BooleanFunction& x, const BooleanFunction& y)
1075  {
1076  const BooleanFunction& smaller = (x.get_nodes().size() < y.get_nodes().size()) ? x : y;
1077  const BooleanFunction& bigger = (x.get_nodes().size() < y.get_nodes().size()) ? y : x;
1078 
1079  // The node vector of the first function needs to be exactly one element shorter than the second
1080  if (smaller.get_nodes().size() != (bigger.get_nodes().size() - 1))
1081  {
1082  return false;
1083  }
1084 
1085  // The top level node of the bigger node vector needs to be a NOT node
1086  if (bigger.get_top_level_node().type != BooleanFunction::NodeType::Not)
1087  {
1088  return false;
1089  }
1090 
1091  // 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
1092  for (u32 idx = 0; idx < smaller.get_nodes().size(); idx++)
1093  {
1094  if (smaller.get_nodes().at(idx) != bigger.get_nodes().at(idx))
1095  {
1096  return false;
1097  }
1098  }
1099 
1100  return true;
1101  }
1102  } // namespace
1103 
1104  Result<BooleanFunction> SymbolicExecution::simplify(const BooleanFunction::Node& node, std::vector<BooleanFunction>&& p) const
1105  {
1106  if (!p.empty() && std::all_of(p.begin(), p.end(), [](const auto& function) { return function.is_constant() || function.is_index(); }))
1107  {
1108  if (auto res = SymbolicExecution::constant_propagation(node, std::move(p)); res.is_error())
1109  {
1110  return ERR_APPEND(res.get_error(), "could not simplify sub-expression in abstract syntax tree: constant propagation failed");
1111  }
1112  else
1113  {
1114  return res;
1115  }
1116  }
1117 
1118  if (node.is_commutative())
1119  {
1120  p = SymbolicExecution::normalize(std::move(p));
1121  }
1122 
1128 
1129  switch (node.type)
1130  {
1131  case BooleanFunction::NodeType::Constant: {
1132  return OK(BooleanFunction::Const(node.constant));
1133  }
1134  case BooleanFunction::NodeType::Index: {
1135  return OK(BooleanFunction::Index(node.index, node.size));
1136  }
1137  case BooleanFunction::NodeType::Variable: {
1138  return OK(this->state.get(BooleanFunction::Var(node.variable, node.size)));
1139  }
1140  case BooleanFunction::NodeType::And: {
1141  // X & 0 => 0
1142  if (p[1].has_constant_value(0))
1143  {
1144  return OK(BooleanFunction::Const(0, node.size));
1145  }
1146  // X & 1 => X
1147  if (p[1] == One(node.size))
1148  {
1149  return OK(p[0]);
1150  }
1151  // X & X => X
1152  if (p[0] == p[1])
1153  {
1154  return OK(p[0]);
1155  }
1156  // X & ~X => 0
1157  if (is_x_not_y(p[0], p[1]))
1158  {
1159  return OK(BooleanFunction::Const(0, node.size));
1160  }
1161 
1162  if (p[0].is(BooleanFunction::NodeType::Or) && p[1].is(BooleanFunction::NodeType::Or))
1163  {
1164  auto p0_parameter = p[0].get_parameters();
1165  auto p1_parameter = p[1].get_parameters();
1166 
1167  // (X | Y) & (X | Z) => X | (Y & Z)
1168  if (p0_parameter[0] == p1_parameter[0])
1169  {
1170  return OK(p0_parameter[0] | (p0_parameter[1] & p1_parameter[1]));
1171  }
1172  // (X | Y) & (Z | X) => X | (Y & Z)
1173  if (p0_parameter[0] == p1_parameter[1])
1174  {
1175  return OK(p0_parameter[0] | (p0_parameter[1] & p1_parameter[0]));
1176  }
1177 
1178  // (X | Y) & (Y | Z) => Y | (X & Z)
1179  if (p0_parameter[1] == p1_parameter[0])
1180  {
1181  return OK(p0_parameter[1] | (p0_parameter[0] & p1_parameter[1]));
1182  }
1183  // (X | Y) & (Z | Y) => Y | (X & Z)
1184  if (p0_parameter[1] == p1_parameter[1])
1185  {
1186  return OK(p0_parameter[1] | (p0_parameter[0] & p1_parameter[0]));
1187  }
1188  }
1189 
1190  if (p[1].is(BooleanFunction::NodeType::And))
1191  {
1192  auto p1_parameter = p[1].get_parameters();
1193  // X & (X & Y) => (X & Y)
1194  if (p[0] == p1_parameter[1])
1195  {
1196  return OK(p[1]);
1197  }
1198  // X & (Y & X) => (Y & X)
1199  if (p[0] == p1_parameter[0])
1200  {
1201  return OK(p[1]);
1202  }
1203 
1204  // X & (~X & Y) => 0
1205  if (is_x_not_y(p1_parameter[0], p[0]))
1206  {
1207  return OK(BooleanFunction::Const(0, node.size));
1208  }
1209  // X & (Y & ~X) => 0
1210  if (is_x_not_y(p1_parameter[1], p[0]))
1211  {
1212  return OK(BooleanFunction::Const(0, node.size));
1213  }
1214  }
1215 
1216  if (p[1].is(BooleanFunction::NodeType::Or))
1217  {
1218  auto p1_parameter = p[1].get_parameters();
1219 
1220  // X & (X | Y) => X
1221  if (p1_parameter[0] == p[0])
1222  {
1223  return OK(p[0]);
1224  }
1225  // X & (Y | X) => X
1226  if (p1_parameter[1] == p[0])
1227  {
1228  return OK(p[0]);
1229  }
1230  // X & (~X | Y) => X & Y
1231  if (is_x_not_y(p1_parameter[0], p[0]))
1232  {
1233  return BooleanFunction::And(p[0].clone(), p1_parameter[1].clone(), node.size);
1234  }
1235  // X & (Y | ~X) => X & Y
1236  if (is_x_not_y(p1_parameter[1], p[0]))
1237  {
1238  return BooleanFunction::And(p[0].clone(), p1_parameter[0].clone(), node.size);
1239  }
1240  }
1241 
1242  if (p[0].is(BooleanFunction::NodeType::And))
1243  {
1244  auto p0_parameter = p[0].get_parameters();
1245 
1246  // (X & Y) & X => X & Y
1247  if (p0_parameter[0] == p[1])
1248  {
1249  return OK(p[0]);
1250  }
1251 
1252  // (Y & X) & X => Y & X
1253  if (p0_parameter[1] == p[1])
1254  {
1255  return OK(p[0]);
1256  }
1257  // (~X & Y) & X => 0
1258  if (is_x_not_y(p0_parameter[0], p[1]))
1259  {
1260  return OK(BooleanFunction::Const(0, node.size));
1261  }
1262  // (Y & ~X) & X => 0
1263  if (is_x_not_y(p0_parameter[1], p[1]))
1264  {
1265  return OK(BooleanFunction::Const(0, node.size));
1266  }
1267  }
1268 
1269  if (p[0].is(BooleanFunction::NodeType::Or))
1270  {
1271  auto p0_parameter = p[0].get_parameters();
1272 
1273  // (X | Y) & X => X
1274  if (p0_parameter[0] == p[1])
1275  {
1276  return OK(p[1]);
1277  }
1278  // (Y | X) & X => X
1279  if (p0_parameter[1] == p[1])
1280  {
1281  return OK(p[1]);
1282  }
1283  // (~X | Y) & X => X & Y
1284  if (is_x_not_y(p0_parameter[0], p[1]))
1285  {
1286  return BooleanFunction::And(p[1].clone(), p0_parameter[1].clone(), node.size);
1287  }
1288  // (Y | ~X) & X => X & Y
1289  if (is_x_not_y(p0_parameter[1], p[1]))
1290  {
1291  return BooleanFunction::And(p[1].clone(), p0_parameter[0].clone(), node.size);
1292  }
1293  }
1294 
1295  return OK(p[0] & p[1]);
1296  }
1297  case BooleanFunction::NodeType::Not: {
1298  // ~~X => X
1299  if (p[0].is(BooleanFunction::NodeType::Not))
1300  {
1301  return OK(p[0].get_parameters()[0]);
1302  }
1303 
1304  // ~(~X & ~Y) => X | Y
1305  if (p[0].is(BooleanFunction::NodeType::And))
1306  {
1307  auto p0_parameter = p[0].get_parameters();
1308  if (p0_parameter[0].is(BooleanFunction::NodeType::Not) && p0_parameter[1].is(BooleanFunction::NodeType::Not))
1309  {
1310  return BooleanFunction::Or(p0_parameter[0].get_parameters()[0].clone(), p0_parameter[1].get_parameters()[0].clone(), node.size);
1311  }
1312  }
1313 
1314  // ~(~X | ~Y) => X & Y
1315  if (p[0].is(BooleanFunction::NodeType::Or))
1316  {
1317  auto p0_parameter = p[0].get_parameters();
1318  if (p0_parameter[0].is(BooleanFunction::NodeType::Not) && p0_parameter[1].is(BooleanFunction::NodeType::Not))
1319  {
1320  return BooleanFunction::And(p0_parameter[0].get_parameters()[0].clone(), p0_parameter[1].get_parameters()[0].clone(), node.size);
1321  }
1322  }
1323 
1324  // ~(X | Y) => ~X & ~Y
1325  if (p[0].is(BooleanFunction::NodeType::Or))
1326  {
1327  auto p0_parameter = p[0].get_parameters();
1328  return OK((~p0_parameter[0]) & (~p0_parameter[1]));
1329  }
1330 
1331  // ~(X & Y) => ~X | ~Y
1332  if (p[0].is(BooleanFunction::NodeType::And))
1333  {
1334  auto p0_parameter = p[0].get_parameters();
1335  return OK((~p0_parameter[0]) | (~p0_parameter[1]));
1336  }
1337 
1338  return BooleanFunction::Not(p[0].clone(), node.size);
1339  }
1340 
1341  case BooleanFunction::NodeType::Or: {
1342  // X | 0 => X
1343  if (p[1].has_constant_value(0))
1344  {
1345  return OK(p[0]);
1346  }
1347 
1348  // X | 1 => 1
1349  if (p[1] == One(node.size))
1350  {
1351  return OK(p[1]);
1352  }
1353 
1354  // X | X => X
1355  if (p[0] == p[1])
1356  {
1357  return OK(p[0]);
1358  }
1359 
1360  // X | ~X => 111...1
1361  if (is_x_not_y(p[0], p[1]))
1362  {
1363  return OK(One(node.size));
1364  }
1365 
1366  if (p[0].is(BooleanFunction::NodeType::And) && p[1].is(BooleanFunction::NodeType::And))
1367  {
1368  auto p0_parameter = p[0].get_parameters();
1369  auto p1_parameter = p[1].get_parameters();
1370 
1371  // (X & Y) | (X & Z) => X & (Y | Z)
1372  if (p0_parameter[0] == p1_parameter[0])
1373  {
1374  return OK(p0_parameter[0] & (p0_parameter[1] | p1_parameter[1]));
1375  }
1376  // (X & Y) | (Z & X) => X & (Y | Z)
1377  if (p0_parameter[0] == p1_parameter[1])
1378  {
1379  return OK(p0_parameter[0] & (p0_parameter[1] | p1_parameter[0]));
1380  }
1381  // (X & Y) | (Y & Z) => Y & (Y | Z)
1382  if (p0_parameter[1] == p1_parameter[0])
1383  {
1384  return OK(p0_parameter[1] & (p0_parameter[0] | p1_parameter[1]));
1385  }
1386  // (X & Y) | (Z & Y) => Y & (X | Z)
1387  if (p0_parameter[1] == p1_parameter[1])
1388  {
1389  return OK(p0_parameter[1] & (p0_parameter[0] | p1_parameter[0]));
1390  }
1391  }
1392 
1393  if (p[1].is(BooleanFunction::NodeType::And))
1394  {
1395  auto p1_parameter = p[1].get_parameters();
1396  // X | (Y & !X) => X | Y
1397  if (is_x_not_y(p1_parameter[1], p[0]))
1398  {
1399  return BooleanFunction::Or(p[0].clone(), p1_parameter[0].clone(), node.size);
1400  }
1401 
1402  // X | (X & Y) => X
1403  if ((p1_parameter[0] == p[0]) || (p1_parameter[1] == p[0]))
1404  {
1405  return OK(p[0]);
1406  }
1407 
1408  // X | (~X & Y) => X | Y
1409  if (is_x_not_y(p1_parameter[0], p[0]))
1410  {
1411  return BooleanFunction::Or(p[0].clone(), p1_parameter[1].clone(), node.size);
1412  }
1413  // X | (Y & ~X) => X | Y
1414  if (is_x_not_y(p1_parameter[1], p[0]))
1415  {
1416  return BooleanFunction::Or(p[0].clone(), p1_parameter[0].clone(), node.size);
1417  }
1418  }
1419 
1420  if (p[1].is(BooleanFunction::NodeType::Or))
1421  {
1422  auto p1_parameter = p[1].get_parameters();
1423 
1424  // X | (X | Y) => (X | Y)
1425  if (p1_parameter[0] == p[0])
1426  {
1427  return OK(p[1]);
1428  }
1429  // X | (Y | X) => (Y | X)
1430  if (p1_parameter[1] == p[0])
1431  {
1432  return OK(p[1]);
1433  }
1434 
1435  // X | (~X | Y) => 1
1436  if (is_x_not_y(p1_parameter[0], p[0]))
1437  {
1438  return OK(One(node.size));
1439  }
1440 
1441  // X | (Y | ~X) => 1
1442  if (is_x_not_y(p1_parameter[1], p[0]))
1443  {
1444  return OK(One(node.size));
1445  }
1446  }
1447 
1448  if (p[0].is(BooleanFunction::NodeType::Or))
1449  {
1450  auto p0_parameter = p[0].get_parameters();
1451 
1452  // (X | Y) | X => (X | Y)
1453  if (p0_parameter[0] == p[1])
1454  {
1455  return OK(p[0]);
1456  }
1457  // (Y | X) | X => (Y | X)
1458  if (p0_parameter[1] == p[1])
1459  {
1460  return OK(p[0]);
1461  }
1462 
1463  // (~X | Y) | X => 1
1464  if (is_x_not_y(p0_parameter[0], p[1]))
1465  {
1466  return OK(One(node.size));
1467  }
1468 
1469  // (Y | ~X) | X => 1
1470  if (is_x_not_y(p0_parameter[1], p[1]))
1471  {
1472  return OK(One(node.size));
1473  }
1474  }
1475 
1476  if (p[0].is(BooleanFunction::NodeType::And))
1477  {
1478  auto p0_parameter = p[0].get_parameters();
1479 
1480  // (X & Y) | X => X
1481  if (p0_parameter[0] == p[1])
1482  {
1483  return OK(p[1]);
1484  }
1485  // (Y & X) | X => X
1486  if (p0_parameter[1] == p[1])
1487  {
1488  return OK(p[1]);
1489  }
1490 
1491  // (~X & Y) | X => X | Y
1492  if (is_x_not_y(p0_parameter[0], p[1]))
1493  {
1494  return BooleanFunction::Or(p0_parameter[1].clone(), p[1].clone(), node.size);
1495  }
1496 
1497  // (X & ~Y) | Y => X | Y
1498  if (is_x_not_y(p0_parameter[1], p[1]))
1499  {
1500  return BooleanFunction::Or(p0_parameter[0].clone(), p[1].clone(), node.size);
1501  }
1502  }
1503 
1504  return BooleanFunction::Or(p[0].clone(), p[1].clone(), node.size);
1505  }
1506  case BooleanFunction::NodeType::Xor: {
1507  // X ^ 0 => X
1508  if (p[1].has_constant_value(0))
1509  {
1510  return OK(p[0]);
1511  }
1512  // X ^ 1 => ~X
1513  if (p[1] == One(node.size))
1514  {
1515  return BooleanFunction::Not(p[0].clone(), node.size);
1516  }
1517  // X ^ X => 0
1518  if (p[0] == p[1])
1519  {
1520  return OK(BooleanFunction::Const(0, node.size));
1521  }
1522  // X ^ ~X => 1
1523  if (is_x_not_y(p[0], p[1]))
1524  {
1525  return OK(One(node.size));
1526  }
1527 
1528  return BooleanFunction::Xor(p[0].clone(), p[1].clone(), node.size);
1529  }
1530  case BooleanFunction::NodeType::Add: {
1531  // X + 0 => X
1532  if (p[1].has_constant_value(0))
1533  {
1534  return OK(p[0]);
1535  }
1536 
1537  return BooleanFunction::Add(p[0].clone(), p[1].clone(), node.size);
1538  }
1539  case BooleanFunction::NodeType::Sub: {
1540  // X - 0 => X
1541  if (p[1].has_constant_value(0))
1542  {
1543  return OK(p[0]);
1544  }
1545  // X - X => 0
1546  if (p[0] == p[1])
1547  {
1548  return OK(BooleanFunction::Const(0, node.size));
1549  }
1550 
1551  return BooleanFunction::Sub(p[0].clone(), p[1].clone(), node.size);
1552  }
1553  case BooleanFunction::NodeType::Mul: {
1554  // X * 0 => 0
1555  if (p[1].has_constant_value(0))
1556  {
1557  return OK(BooleanFunction::Const(0, node.size));
1558  }
1559  // X * 1 => X
1560  if (p[1].has_constant_value(1))
1561  {
1562  return OK(p[0]);
1563  }
1564 
1565  return BooleanFunction::Mul(p[0].clone(), p[1].clone(), node.size);
1566  }
1567  case BooleanFunction::NodeType::Sdiv: {
1568  // X /s 1 => X
1569  if (p[1].has_constant_value(1))
1570  {
1571  return OK(p[0]);
1572  }
1573  // X /s X => 1
1574  if (p[0] == p[1])
1575  {
1576  return OK(BooleanFunction::Const(1, node.size));
1577  }
1578 
1579  return BooleanFunction::Sdiv(p[0].clone(), p[1].clone(), node.size);
1580  }
1581  case BooleanFunction::NodeType::Udiv: {
1582  // X / 1 => X
1583  if (p[1].has_constant_value(1))
1584  {
1585  return OK(p[0]);
1586  }
1587  // X / X => 1
1588  if (p[0] == p[1])
1589  {
1590  return OK(BooleanFunction::Const(1, node.size));
1591  }
1592 
1593  return BooleanFunction::Udiv(p[0].clone(), p[1].clone(), node.size);
1594  }
1595  case BooleanFunction::NodeType::Srem: {
1596  // X %s 1 => 0
1597  if (p[1].has_constant_value(1))
1598  {
1599  return OK(BooleanFunction::Const(0, node.size));
1600  }
1601  // X %s X => 0
1602  if (p[0] == p[1])
1603  {
1604  return OK(BooleanFunction::Const(0, node.size));
1605  }
1606 
1607  return BooleanFunction::Srem(p[0].clone(), p[1].clone(), node.size);
1608  }
1609  case BooleanFunction::NodeType::Urem: {
1610  // X % 1 => 0
1611  if (p[1].has_constant_value(1))
1612  {
1613  return OK(BooleanFunction::Const(0, node.size));
1614  }
1615  // X % X => 0
1616  if (p[0] == p[1])
1617  {
1618  return OK(BooleanFunction::Const(0, node.size));
1619  }
1620 
1621  return BooleanFunction::Urem(p[0].clone(), p[1].clone(), node.size);
1622  }
1623  case BooleanFunction::NodeType::Slice: {
1624  // SLICE(p, 0, 0) => p (if p is 1-bit wide)
1625  // if ((p[0].size() == 1) && p[1].has_index_value(0) && p[2].has_index_value(0) && (node.size == 1))
1626  // {
1627  // return OK(p[0]);
1628  // }
1629 
1630  // SLICE(p, 0, size-1) => p
1631  if (node.size == p[0].size() && p[1].has_index_value(0) && p[2].has_index_value(node.size - 1))
1632  {
1633  return OK(p[0]);
1634  }
1635 
1636  if (const auto start_res = p[1].get_index_value(), end_res = p[2].get_index_value(); start_res.is_ok() && end_res.is_ok())
1637  {
1638  const auto start = start_res.get(), end = end_res.get();
1639 
1640  // SLICE(SLICE(X, i, j), k, l) => SLICE(X, i+k, i+l)
1641  if (p[0].is(BooleanFunction::NodeType::Slice))
1642  {
1643  const auto inner = p[0].get_parameters();
1644  if (const auto inner_start = inner[1].get_index_value(); inner_start.is_ok())
1645  {
1646  const auto offset = inner_start.get();
1647  return BooleanFunction::Slice(inner[0].clone(),
1648  BooleanFunction::Index(offset + start, inner[0].size()),
1649  BooleanFunction::Index(offset + end, inner[0].size()),
1650  node.size);
1651  }
1652  }
1653 
1654  // a slice of an extension either sees only the padding or only the original value
1655  if (p[0].is(BooleanFunction::NodeType::Zext) || p[0].is(BooleanFunction::NodeType::Sext))
1656  {
1657  const auto extended = p[0].get_parameters();
1658  const auto original = extended[0].size();
1659 
1660  // SLICE(ZEXT(X, n), i, j) => 0, the range lies entirely in the zero padding
1661  if (p[0].is(BooleanFunction::NodeType::Zext) && (start >= original))
1662  {
1663  return OK(BooleanFunction::Const(0, node.size));
1664  }
1665  // SLICE(ZEXT(X, n), i, j) => SLICE(X, i, j), the range lies entirely within X
1666  // SLICE(SEXT(X, n), i, j) => SLICE(X, i, j), which holds for both extensions
1667  if (end < original)
1668  {
1669  return BooleanFunction::Slice(extended[0].clone(), BooleanFunction::Index(start, original), BooleanFunction::Index(end, original), node.size);
1670  }
1671  }
1672 
1673  // a slice that falls entirely into one half of a concatenation only needs that half,
1674  // where the second parameter of the concatenation holds the least significant bits
1675  if (p[0].is(BooleanFunction::NodeType::Concat))
1676  {
1677  const auto halves = p[0].get_parameters();
1678  const auto lower = halves[1].size();
1679 
1680  // SLICE(CONCAT(X, Y), i, j) => SLICE(Y, i, j)
1681  if (end < lower)
1682  {
1683  return BooleanFunction::Slice(halves[1].clone(), BooleanFunction::Index(start, lower), BooleanFunction::Index(end, lower), node.size);
1684  }
1685  // SLICE(CONCAT(X, Y), i, j) => SLICE(X, i-|Y|, j-|Y|)
1686  if (start >= lower)
1687  {
1688  return BooleanFunction::Slice(halves[0].clone(),
1689  BooleanFunction::Index(start - lower, halves[0].size()),
1690  BooleanFunction::Index(end - lower, halves[0].size()),
1691  node.size);
1692  }
1693  }
1694  }
1695 
1696  return BooleanFunction::Slice(p[0].clone(), p[1].clone(), p[2].clone(), node.size);
1697  }
1698  case BooleanFunction::NodeType::Concat: {
1699  // CONCAT(X, Y) => CONST(X || Y)
1700  if (p[0].is_constant() && p[1].is_constant())
1701  {
1702  if ((p[0].size() + p[1].size()) <= 64)
1703  {
1704  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()));
1705  }
1706  }
1707 
1708  // 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.
1709  if (p[0].is(BooleanFunction::NodeType::Slice) && p[1].is(BooleanFunction::NodeType::Concat))
1710  {
1711  auto p1_parameter = p[1].get_parameters();
1712 
1713  if (p1_parameter[0].is(BooleanFunction::NodeType::Slice))
1714  {
1715  auto p0_parameter = p[0].get_parameters();
1716  auto p10_parameter = p1_parameter[0].get_parameters();
1717 
1718  if (p0_parameter[0] == p10_parameter[0])
1719  {
1720  if (p1_parameter[1].is(BooleanFunction::NodeType::Slice))
1721  {
1722  auto p11_parameter = p1_parameter[1].get_parameters();
1723 
1724  // 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)))
1725  if (p11_parameter[0] != p10_parameter[0])
1726  {
1727  if (auto concatination = BooleanFunction::Concat(p[0].clone(), p1_parameter[0].clone(), p[0].size() + p1_parameter[0].size()); concatination.is_ok())
1728  {
1729  return BooleanFunction::Concat(concatination.get(), p1_parameter[1].clone(), concatination.get().size() + p1_parameter[1].size());
1730  }
1731  }
1732  }
1733  else if (p1_parameter[1].is(BooleanFunction::NodeType::Concat))
1734  {
1735  auto p11_parameter = p1_parameter[1].get_parameters();
1736 
1737  if (p11_parameter[0].is(BooleanFunction::NodeType::Slice))
1738  {
1739  auto p110_parameter = p11_parameter[0].get_parameters();
1740 
1741  // 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)))
1742  if (p110_parameter[0] != p10_parameter[0])
1743  {
1744  auto c1 = BooleanFunction::Concat(p[0].clone(), p1_parameter[0].clone(), p[0].size() + p1_parameter[0].size());
1745 
1746  return BooleanFunction::Concat(c1.get().clone(), p1_parameter[1].clone(), c1.get().size() + p1_parameter[1].size());
1747  }
1748  }
1749  }
1750  else
1751  {
1752  // CONCAT(SLICE(X, i, j), CONCAT(SLICE(X, k, l), Y)) => CONCAT(CONCAT(SLICE(X, i, j), SLICE(X, k, l)), Y))
1753  if (auto concatination = BooleanFunction::Concat(p[0].clone(), p1_parameter[0].clone(), p[0].size() + p1_parameter[0].size()); concatination.is_ok())
1754  {
1755  return BooleanFunction::Concat(concatination.get(), p1_parameter[1].clone(), concatination.get().size() + p1_parameter[1].size());
1756  }
1757  }
1758  }
1759  }
1760  }
1761 
1762  if (p[0].is(BooleanFunction::NodeType::Slice) && p[1].is(BooleanFunction::NodeType::Slice))
1763  {
1764  auto p0_parameter = p[0].get_parameters();
1765  auto p1_parameter = p[1].get_parameters();
1766 
1767  if (p0_parameter[0] == p1_parameter[0])
1768  {
1769  // CONCAT(SLICE(X, j+1, k), SLICE(X, i, j)) => SLICE(X, i, k)
1770  if ((p1_parameter[2].get_index_value().get() == (p0_parameter[1].get_index_value().get() - 1)))
1771  {
1772  return BooleanFunction::Slice(p0_parameter[0].clone(), p1_parameter[1].clone(), p0_parameter[2].clone(), p[0].size() + p[1].size());
1773  }
1774 
1775  // CONCAT(SLICE(X, j, j), SLICE(X, i, j)) => SEXT(SLICE(X, i, j), j-i+1)
1776  if ((p1_parameter[2].get_index_value().get() == p0_parameter[1].get_index_value().get())
1777  && (p1_parameter[2].get_index_value().get() == p0_parameter[2].get_index_value().get()))
1778  {
1779  return BooleanFunction::Sext(p[1].clone(), BooleanFunction::Index(p[1].size() + 1, p[1].size() + 1), p[1].size() + 1);
1780  }
1781  }
1782  }
1783 
1784  // CONCAT(SLICE(X, j, j), SEXT(SLICE(X, i, j), j-i+n)) => SEXT(SLICE(X, i, j), j-i+n+1)
1785  if (p[0].is(BooleanFunction::NodeType::Slice) && p[1].is(BooleanFunction::NodeType::Sext))
1786  {
1787  auto p1_parameter = p[1].get_parameters();
1788 
1789  if (p1_parameter[0].is(BooleanFunction::NodeType::Slice))
1790  {
1791  auto p0_parameter = p[0].get_parameters();
1792  auto p10_parameter = p1_parameter[0].get_parameters();
1793 
1794  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()))
1795  {
1796  return BooleanFunction::Sext(p1_parameter[0].clone(), BooleanFunction::Index(p[1].size() + 1, p[1].size() + 1), p[1].size() + 1);
1797  }
1798  }
1799  }
1800 
1801  // 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)
1802  if (p[0].is(BooleanFunction::NodeType::Slice) && p[1].is(BooleanFunction::NodeType::Concat))
1803  {
1804  auto p1_parameter = p[1].get_parameters();
1805 
1806  if (p1_parameter[0].is(BooleanFunction::NodeType::Sext))
1807  {
1808  auto p10_parameter = p1_parameter[0].get_parameters();
1809 
1810  if (p10_parameter[0].is(BooleanFunction::NodeType::Slice))
1811  {
1812  auto p0_parameter = p[0].get_parameters();
1813  auto p100_parameter = p10_parameter[0].get_parameters();
1814 
1815  if ((p0_parameter[0] == p100_parameter[0]) && (p0_parameter[1] == p0_parameter[2])
1816  && (p0_parameter[1].get_index_value().get() == p100_parameter[2].get_index_value().get()))
1817  {
1818  if (auto extension =
1819  BooleanFunction::Sext(p10_parameter[0].clone(), BooleanFunction::Index(p1_parameter[0].size() + 1, p1_parameter[0].size() + 1), p1_parameter[0].size() + 1);
1820  extension.is_ok())
1821  {
1822  return BooleanFunction::Concat(extension.get(), p1_parameter[1].clone(), extension.get().size() + p1_parameter[1].size());
1823  }
1824  }
1825  }
1826  }
1827  }
1828 
1829  return BooleanFunction::Concat(p[0].clone(), p[1].clone(), node.size);
1830  }
1831  case BooleanFunction::NodeType::Zext: {
1832  // ZEXT(X, |X|) => X
1833  if (node.size == p[0].size())
1834  {
1835  return OK(p[0]);
1836  }
1837  // ZEXT(ZEXT(X, n), m) => ZEXT(X, m), only for two extensions of the same kind
1838  if (p[0].is(BooleanFunction::NodeType::Zext))
1839  {
1840  const auto inner = p[0].get_parameters();
1841  return BooleanFunction::Zext(inner[0].clone(), BooleanFunction::Index(node.size, node.size), node.size);
1842  }
1843 
1844  return BooleanFunction::Zext(p[0].clone(), p[1].clone(), node.size);
1845  }
1846  case BooleanFunction::NodeType::Sext: {
1847  // SEXT(X, |X|) => X
1848  if (node.size == p[0].size())
1849  {
1850  return OK(p[0]);
1851  }
1852  // SEXT(SEXT(X, n), m) => SEXT(X, m), only for two extensions of the same kind
1853  if (p[0].is(BooleanFunction::NodeType::Sext))
1854  {
1855  const auto inner = p[0].get_parameters();
1856  return BooleanFunction::Sext(inner[0].clone(), BooleanFunction::Index(node.size, node.size), node.size);
1857  }
1858 
1859  return BooleanFunction::Sext(p[0].clone(), p[1].clone(), node.size);
1860  }
1861  case BooleanFunction::NodeType::Eq: {
1862  // X == X => 1
1863  if (p[0] == p[1])
1864  {
1865  return OK(BooleanFunction::Const(1, node.size));
1866  }
1867  // X == ~X => 0, the two differ in every single bit
1868  if (is_x_not_y(p[0], p[1]))
1869  {
1870  return OK(BooleanFunction::Const(0, node.size));
1871  }
1872  // on a single bit an equality is the operand itself, or its negation
1873  if (p[0].size() == 1)
1874  {
1875  // X == 1 => X
1876  if (p[1] == One(1))
1877  {
1878  return OK(p[0]);
1879  }
1880  // X == 0 => ~X
1881  if (p[1].has_constant_value(0))
1882  {
1883  return OK(~p[0]);
1884  }
1885  }
1886 
1887  return BooleanFunction::Eq(p[0].clone(), p[1].clone(), node.size);
1888  }
1889  case BooleanFunction::NodeType::Sle: {
1890  // X <=s X => 1
1891  if (p[0] == p[1])
1892  {
1893  return OK(BooleanFunction::Const(1, node.size));
1894  }
1895 
1896  return BooleanFunction::Sle(p[0].clone(), p[1].clone(), node.size);
1897  }
1898  case BooleanFunction::NodeType::Slt: {
1899  // X <s X => 0
1900  if (p[0] == p[1])
1901  {
1902  return OK(BooleanFunction::Const(0, node.size));
1903  }
1904 
1905  return BooleanFunction::Slt(p[0].clone(), p[1].clone(), node.size);
1906  }
1907  case BooleanFunction::NodeType::Ule: {
1908  // X <= X => 1
1909  if (p[0] == p[1])
1910  {
1911  return OK(BooleanFunction::Const(1, node.size));
1912  }
1913  // 0 <= X => 1, no unsigned value is below zero
1914  if (p[0].has_constant_value(0))
1915  {
1916  return OK(BooleanFunction::Const(1, node.size));
1917  }
1918  // X <= 111...1 => 1, no unsigned value is above the maximum
1919  if (p[1] == One(p[1].size()))
1920  {
1921  return OK(BooleanFunction::Const(1, node.size));
1922  }
1923 
1924  return BooleanFunction::Ule(p[0].clone(), p[1].clone(), node.size);
1925  }
1926  case BooleanFunction::NodeType::Ult: {
1927  // X < 0 => 0
1928  if (p[1].has_constant_value(0))
1929  {
1930  return OK(BooleanFunction::Const(0, node.size));
1931  }
1932  // X < X => 0
1933  if (p[0] == p[1])
1934  {
1935  return OK(BooleanFunction::Const(0, node.size));
1936  }
1937  // 111...1 < X => 0, no unsigned value is above the maximum
1938  if (p[0] == One(p[0].size()))
1939  {
1940  return OK(BooleanFunction::Const(0, node.size));
1941  }
1942 
1943  return BooleanFunction::Ult(p[0].clone(), p[1].clone(), node.size);
1944  }
1945  case BooleanFunction::NodeType::Ite: {
1946  // ITE(0, a, b) => b
1947  if (p[0].has_constant_value(0))
1948  {
1949  return OK(p[2]);
1950  }
1951  // ITE(1, a, b) => a
1952  if (p[0].has_constant_value(1))
1953  {
1954  return OK(p[1]);
1955  }
1956  // ITE(a, b, b) => b
1957  if (p[1] == p[2])
1958  {
1959  return OK(p[1]);
1960  }
1961  // a single bit choice between 1 and 0 is the condition itself, or its negation
1962  if (node.size == 1)
1963  {
1964  // ITE(a, 1, 0) => a
1965  if ((p[1] == One(1)) && p[2].has_constant_value(0))
1966  {
1967  return OK(p[0]);
1968  }
1969  // ITE(a, 0, 1) => ~a
1970  if (p[1].has_constant_value(0) && (p[2] == One(1)))
1971  {
1972  return OK(~p[0]);
1973  }
1974  }
1975 
1976  return BooleanFunction::Ite(p[0].clone(), p[1].clone(), p[2].clone(), node.size);
1977  }
1978  default:
1979  return ERR("could not simplify sub-expression in abstract syntax tree: not implemented for given node type");
1980  }
1981  }
1982 
1983  Result<BooleanFunction> SymbolicExecution::constant_propagation(const BooleanFunction::Node& node, std::vector<BooleanFunction>&& p)
1984  {
1985  if (node.get_arity() != p.size())
1986  {
1987  return ERR("could not propagate constants: arity does not match number of parameters");
1988  }
1989 
1990  std::vector<std::vector<BooleanFunction::Value>> values;
1991  std::vector<u16> indices;
1992  values.reserve(p.size());
1993 
1994  for (const auto& parameter : p)
1995  {
1996  if (parameter.is_index())
1997  {
1998  indices.push_back(parameter.get_index_value().get());
1999  }
2000  else
2001  {
2002  // some of the cases below modify the value in place, so it has to be a copy, but one is enough
2003  values.emplace_back(parameter.get_top_level_node().constant);
2004  }
2005  }
2006 
2007  if (auto res = ConstantPropagation::fold(node, values, indices); res.is_ok())
2008  {
2009  return OK(BooleanFunction::Const(res.get()));
2010  }
2011  else
2012  {
2013  return ERR(res.get_error());
2014  }
2015  }
2016  } // namespace SMT
2017 } // namespace hal
size
u32 size
Definition: candidate_search.cpp:62
hal::BooleanFunction::Value
Value
represents the type of the node
Definition: boolean_function.h:74
hal::BooleanFunction::Const
static BooleanFunction Const(const BooleanFunction::Value &value)
Definition: boolean_function.cpp:256
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:895
hal::SMT::SymbolicExecution::evaluate
Result< BooleanFunction > evaluate(const BooleanFunction &function) const
Definition: symbolic_execution.cpp:976
hal::SMT::SymbolicExecution::state
SymbolicState state
The current symbolic state.
Definition: symbolic_execution.h:50
hal::SMT::SymbolicState::get_bindings
std::unordered_map< std::string, const BooleanFunction * > get_bindings() const
Definition: symbolic_state.cpp:24
u64
uint64_t u64
Definition: defines.h:42
u16
uint16_t u16
Definition: defines.h:40
u32
uint32_t u32
Definition: defines.h:41
i64
int64_t i64
Definition: defines.h:37
u8
uint8_t u8
Definition: defines.h:39
UNUSED
#define UNUSED(expr)
Definition: defines.h:49
i32
int32_t i32
Definition: defines.h:36
ERR
#define ERR(message)
Definition: result.h:60
OK
#define OK(...)
Definition: result.h:56
ERR_APPEND
#define ERR_APPEND(prev_error, message)
Definition: result.h:64
hal::BV_ConstantPropagation::constant_propagation
Result< BooleanFunction > constant_propagation(const BooleanFunction::Node &node, std::vector< BooleanFunction > &&p)
Definition: simplification.cpp:379
hal::SMT::ConstantPropagation::Sle
std::vector< BooleanFunction::Value > Sle(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:635
hal::SMT::ConstantPropagation::Sdiv
std::vector< BooleanFunction::Value > Sdiv(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:436
hal::SMT::ConstantPropagation::Ite
std::vector< BooleanFunction::Value > Ite(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1, const std::vector< BooleanFunction::Value > &p2)
Definition: symbolic_execution.cpp:772
hal::SMT::ConstantPropagation::Xor
std::vector< BooleanFunction::Value > Xor(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:119
hal::SMT::ConstantPropagation::Ashr
std::vector< BooleanFunction::Value > Ashr(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:552
hal::SMT::ConstantPropagation::Ror
std::vector< BooleanFunction::Value > Ror(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:608
hal::SMT::ConstantPropagation::fold
Result< std::vector< BooleanFunction::Value > > fold(const BooleanFunction::Node &node, std::vector< std::vector< BooleanFunction::Value >> &values, const std::vector< u16 > &indices)
Definition: symbolic_execution.cpp:800
hal::SMT::ConstantPropagation::Srem
std::vector< BooleanFunction::Value > Srem(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:469
hal::SMT::ConstantPropagation::Urem
std::vector< BooleanFunction::Value > Urem(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:417
hal::SMT::ConstantPropagation::Ule
std::vector< BooleanFunction::Value > Ule(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:713
hal::SMT::ConstantPropagation::Sub
std::vector< BooleanFunction::Value > Sub(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:191
hal::SMT::ConstantPropagation::Add
std::vector< BooleanFunction::Value > Add(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:148
hal::SMT::ConstantPropagation::Or
std::vector< BooleanFunction::Value > Or(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:62
hal::SMT::ConstantPropagation::Not
std::vector< BooleanFunction::Value > Not(const std::vector< BooleanFunction::Value > &p)
Definition: symbolic_execution.cpp:90
hal::SMT::ConstantPropagation::Rol
std::vector< BooleanFunction::Value > Rol(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:580
hal::SMT::ConstantPropagation::Mul
std::vector< BooleanFunction::Value > Mul(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:234
hal::SMT::ConstantPropagation::And
std::vector< BooleanFunction::Value > And(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:33
hal::SMT::ConstantPropagation::Shl
std::vector< BooleanFunction::Value > Shl(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:500
hal::SMT::ConstantPropagation::Udiv
std::vector< BooleanFunction::Value > Udiv(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:400
hal::SMT::ConstantPropagation::Slt
std::vector< BooleanFunction::Value > Slt(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:675
hal::SMT::ConstantPropagation::Ult
std::vector< BooleanFunction::Value > Ult(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:742
hal::SMT::ConstantPropagation::Eq
std::vector< BooleanFunction::Value > Eq(const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
Definition: symbolic_execution.cpp:375
hal::SMT::ConstantPropagation::Lshr
std::vector< BooleanFunction::Value > Lshr(const std::vector< BooleanFunction::Value > &p0, const u16 p1)
Definition: symbolic_execution.cpp:526
hal::module_identification::has_constant_value
bool has_constant_value(const z3::expr &e, const u64 &val)
Definition: create_functional_candidates.cpp:209
hal
Definition: defines.h:45
x
u64 x
Definition: netlist_preprocessing.cpp:2204
y
u64 y
Definition: netlist_preprocessing.cpp:2205
hal::BooleanFunction::Node::type
u16 type
The type of the node.
Definition: boolean_function.h:993
hal::BooleanFunction::Node::size
u16 size
The bit-size of the node.
Definition: boolean_function.h:995
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