Gymbo

type.h
Go to the documentation of this file.
1
7 #pragma once
8 #include <unordered_map>
9 #include <unordered_set>
10 #include <utility>
11
12 #include "utils.h"
13
14 namespace gymbo {
15
19 using Word32 = uint32_t;
20
24 enum class InstrType {
25 Add,
26 Sub,
27 Mul,
28 JmpIf,
29 Jmp,
30 And,
31 Or,
32 Not,
33 Lt,
34 Le,
35 Eq,
36 Push,
37 Store,
38 Load,
39 Pop,
40 Read,
41 Print,
42 Swap,
43 Dup,
44 Over,
45 RotL,
46 Done,
47 Nop,
48 };
49
53 class Instr {
54 public:
55 InstrType instr;
56 Word32 word;
57
62 Instr(InstrType instr) : instr(instr) {}
63
69 Instr(InstrType instr, Word32 word) : instr(instr), word(word) {}
70
74 void print() const { printf("%s\n", toString().c_str()); }
75
80 std::string toString() const {
81 switch (instr) {
82 case (InstrType::Add): {
83 return "add";
84 }
85 case (InstrType::Sub): {
86 return "sub";
87 }
88 case (InstrType::Mul): {
89 return "mul";
90 }
91 case (InstrType::And): {
92 return "and";
93 }
94 case (InstrType::Or): {
95 return "or";
96 }
97 case (InstrType::Not): {
98 return "not";
99 }
100 case (InstrType::JmpIf): {
101 return "jmpIf";
102 }
103 case (InstrType::Jmp): {
104 return "jmp";
105 }
106 case (InstrType::Lt): {
107 return "lt";
108 }
109 case (InstrType::Le): {
110 return "le";
111 }
112 case (InstrType::Load): {
113 return "load";
114 }
115 case (InstrType::Read): {
116 return "read";
117 }
118 case (InstrType::Done): {
119 return "ret";
120 }
121 case (InstrType::Nop): {
122 return "nop";
123 }
124 case (InstrType::Swap): {
125 return "swap";
126 }
127 case (InstrType::Store): {
128 return "store";
129 }
130 case (InstrType::Push): {
131 return "push " + std::to_string(word);
132 }
133 default: {
134 return "unknown";
135 }
136 }
137 }
138 };
139
143 using Prog = std::vector<Instr>;
144
148 using Mem = std::unordered_map<Word32, Word32>;
149
153 struct Grad {
154 std::unordered_map<int, float>
155 val;
161 Grad(std::unordered_map<int, float> val) : val(val) {}
162
168 Grad operator+(const Grad &other) {
169 std::unordered_map<int, float> result = val;
170 for (auto &r : result) {
171 if (other.val.find(r.first) != other.val.end()) {
172 result.at(r.first) += other.val.at(r.first);
173 }
174 }
175 for (auto &r : other.val) {
176 if (result.find(r.first) == result.end()) {
177 result.emplace(std::make_pair(r.first, r.second));
178 }
179 }
180 return Grad(result);
181 }
182
189 Grad operator+(float w) {
190 std::unordered_map<int, float> result = val;
191 for (auto &r : result) {
192 result.at(r.first) += w;
193 }
194 return Grad(result);
195 }
196
202 Grad operator-(const Grad &other) {
203 std::unordered_map<int, float> result = val;
204 for (auto &r : result) {
205 if (other.val.find(r.first) != other.val.end()) {
206 result.at(r.first) -= other.val.at(r.first);
207 }
208 }
209 for (auto &r : other.val) {
210 if (result.find(r.first) == result.end()) {
211 result.emplace(std::make_pair(r.first, -1.0f * r.second));
212 }
213 }
214 return Grad(result);
215 }
216
223 Grad operator*(float w) {
224 std::unordered_map<int, float> result = val;
225 for (auto &r : result) {
226 result.at(r.first) *= w;
227 }
228 return Grad(result);
229 }
230
235 Grad abs() {
236 std::unordered_map<int, float> result = val;
237 for (auto &r : result) {
238 result.emplace(std::make_pair(r.first, std::abs(r.second)));
239 }
240 return Grad(result);
241 }
242 };
243
247 enum class SymType {
248 SAdd,
249 SSub,
250 SMul,
251 SEq,
252 SNot,
253 SOr,
254 SCon,
255 SCnt,
256 SAnd,
257 SLt,
258 SLe,
259 SAny
260 };
261
265 struct Sym {
266 SymType symtype;
267 Sym *left;
268 Sym *right;
269 Word32 word;
270 int var_idx;
271 std::unordered_map<int, float>
272 assign;
277 Sym() {}
278
284 Sym(SymType symtype, Sym *left) : symtype(symtype), left(left) {}
285
286 Sym(SymType symtype, Sym *left, std::unordered_map<int, float> &assign)
287 : symtype(symtype), left(left), assign(assign) {}
288
296 Sym(SymType symtype, Sym *left, Sym *right)
297 : symtype(symtype), left(left), right(right) {}
298
304 Sym(SymType symtype, Word32 val) : symtype(symtype) {
305 if (symtype == SymType::SAny) {
306 var_idx = val;
307 } else {
308 word = val;
309 }
310 }
311
312 Sym(SymType symtype, Sym *left, Sym *right, Word32 word, int var_idx)
313 : symtype(symtype),
314 left(left),
315 right(right),
316 word(word),
317 var_idx(var_idx) {}
318
319 Sym *copy() { return new Sym(symtype, left, right, word, var_idx); }
320
325 void gather_var_ids(std::unordered_set<int> &result) const {
326 switch (symtype) {
327 case (SymType::SAdd): {
328 left->gather_var_ids(result);
329 right->gather_var_ids(result);
330 return;
331 }
332 case (SymType::SSub): {
333 left->gather_var_ids(result);
334 right->gather_var_ids(result);
335 return;
336 }
337 case (SymType::SMul): {
338 left->gather_var_ids(result);
339 right->gather_var_ids(result);
340 return;
341 }
342 case (SymType::SAny): {
343 result.emplace(var_idx);
344 return;
345 }
346 case (SymType::SEq): {
347 left->gather_var_ids(result);
348 right->gather_var_ids(result);
349 return;
350 }
351 case (SymType::SNot): {
352 left->gather_var_ids(result);
353 return;
354 }
355 case (SymType::SCnt): {
356 left->gather_var_ids(result);
357 for (auto &a : assign) {
358 result.erase(a.first);
359 }
360 return;
361 }
362 case (SymType::SAnd): {
363 left->gather_var_ids(result);
364 right->gather_var_ids(result);
365 return;
366 }
367 case (SymType::SOr): {
368 left->gather_var_ids(result);
369 right->gather_var_ids(result);
370 return;
371 }
372 case (SymType::SLt): {
373 left->gather_var_ids(result);
374 right->gather_var_ids(result);
375 return;
376 }
377 case (SymType::SLe): {
378 left->gather_var_ids(result);
379 right->gather_var_ids(result);
380 return;
381 }
382 default:
383 return;
384 }
385 }
386
393 Sym *psimplify(const Mem &cvals) {
394 Sym *tmp_left, *tmp_right;
395
396 switch (symtype) {
397 case (SymType::SAny): {
398 if (cvals.find(var_idx) != cvals.end()) {
399 return new Sym(SymType::SCon, cvals.at(var_idx));
400 } else {
401 return this;
402 }
403 }
404 case (SymType::SAdd): {
405 if (left->symtype == SymType::SCon &&
406 right->symtype == SymType::SCon) {
407 return new Sym(SymType::SCon,
408 FloatToWord(wordToFloat(left->word) +
409 wordToFloat(right->word)));
410 } else {
411 tmp_left = left->psimplify(cvals);
412 tmp_right = right->psimplify(cvals);
413 if (tmp_left->symtype == SymType::SCon &&
414 tmp_right->symtype == SymType::SCon) {
415 return new Sym(
416 SymType::SCon,
417 FloatToWord(wordToFloat(tmp_left->word) +
418 wordToFloat(tmp_right->word)));
419 }
420 return new Sym(SymType::SAdd, tmp_left, tmp_right);
421 }
422 }
423 case (SymType::SSub): {
424 if (left->symtype == SymType::SCon &&
425 right->symtype == SymType::SCon) {
426 return new Sym(SymType::SCon,
427 FloatToWord(wordToFloat(left->word) -
428 wordToFloat(right->word)));
429 } else {
430 tmp_left = left->psimplify(cvals);
431 tmp_right = right->psimplify(cvals);
432 if (tmp_left->symtype == SymType::SCon &&
433 tmp_right->symtype == SymType::SCon) {
434 return new Sym(
435 SymType::SCon,
436 FloatToWord(wordToFloat(tmp_left->word) -
437 wordToFloat(tmp_right->word)));
438 }
439 return new Sym(SymType::SSub, tmp_left, tmp_right);
440 }
441 }
442 case (SymType::SMul): {
443 if (left->symtype == SymType::SCon &&
444 right->symtype == SymType::SCon) {
445 return new Sym(SymType::SCon,
446 FloatToWord(wordToFloat(left->word) *
447 wordToFloat(right->word)));
448 } else {
449 tmp_left = left->psimplify(cvals);
450 tmp_right = right->psimplify(cvals);
451 if (tmp_left->symtype == SymType::SCon &&
452 tmp_right->symtype == SymType::SCon) {
453 return new Sym(
454 SymType::SCon,
455 FloatToWord(wordToFloat(tmp_left->word) *
456 wordToFloat(tmp_right->word)));
457 }
458 return new Sym(SymType::SMul, tmp_left, tmp_right);
459 }
460 }
461 case (SymType::SEq): {
462 return new Sym(SymType::SEq, left->psimplify(cvals),
463 right->psimplify(cvals));
464 }
465 case (SymType::SAnd): {
466 return new Sym(SymType::SAnd, left->psimplify(cvals),
467 right->psimplify(cvals));
468 }
469 case (SymType::SOr): {
470 return new Sym(SymType::SOr, left->psimplify(cvals),
471 right->psimplify(cvals));
472 }
473 case (SymType::SLt): {
474 return new Sym(SymType::SLt, left->psimplify(cvals),
475 right->psimplify(cvals));
476 }
477 case (SymType::SLe): {
478 return new Sym(SymType::SLe, left->psimplify(cvals),
479 right->psimplify(cvals));
480 }
481 case (SymType::SNot): {
482 return new Sym(SymType::SNot, left->psimplify(cvals));
483 }
484 case (SymType::SCnt): {
485 return new Sym(SymType::SCnt, left->psimplify(cvals));
486 }
487 default: {
488 return this;
489 }
490 }
491 }
492
499 float eval(const std::unordered_map<int, float> &cvals,
500 const float eps) const {
501 switch (symtype) {
502 case (SymType::SAdd): {
503 return left->eval(cvals, eps) + right->eval(cvals, eps);
504 }
505 case (SymType::SSub): {
506 return left->eval(cvals, eps) - right->eval(cvals, eps);
507 }
508 case (SymType::SMul): {
509 return left->eval(cvals, eps) * right->eval(cvals, eps);
510 }
511 case (SymType::SCon): {
512 return wordToFloat(word);
513 }
514 case (SymType::SCnt): {
515 switch (left->symtype) {
516 case (SymType::SAdd): {
517 return 1;
518 }
519 case (SymType::SSub): {
520 return 1;
521 }
522 case (SymType::SMul): {
523 return 1;
524 }
525 case (SymType::SCon): {
526 return 1;
527 }
528 case (SymType::SCnt): {
529 return 1;
530 }
531 case (SymType::SAny): {
532 return 1;
533 }
534 default: {
535 std::unordered_map<int, float> nvals(cvals);
536 for (const auto &a : assign) {
537 nvals.emplace(a.first, a.second);
538 }
539 if (left->eval(nvals, eps) <= 0.0f) {
540 return 1.0f;
541 } else {
542 return 0.0;
543 }
544 }
545 }
546 }
547 case (SymType::SAny): {
548 if (cvals.find(var_idx) != cvals.end()) {
549 return cvals.at(var_idx);
550 } else {
551 fprintf(stderr,
552 "\x1b[33m Warning!! var_%d should be specified to "
553 "correctly evaluate this "
554 "symbolic expression\x1b[39m\n",
555 var_idx);
556 return 0;
557 }
558 }
559 case (SymType::SEq): {
560 return std::abs(left->eval(cvals, eps) -
561 right->eval(cvals, eps));
562 }
563 case (SymType::SNot): {
564 return left->eval(cvals, eps) * (-1.0f) + eps;
565 }
566 case (SymType::SAnd): {
567 return std::max(left->eval(cvals, eps),
568 right->eval(cvals, eps));
569 }
570 case (SymType::SOr): {
571 return std::min(left->eval(cvals, eps),
572 right->eval(cvals, eps));
573 }
574 case (SymType::SLt): {
575 return left->eval(cvals, eps) - right->eval(cvals, eps) + eps;
576 }
577 case (SymType::SLe): {
578 return left->eval(cvals, eps) - right->eval(cvals, eps);
579 }
580 default: {
581 return 0.0f;
582 }
583 }
584 }
585
593 Grad grad(const std::unordered_map<int, float> &cvals,
594 const float eps) const {
595 switch (symtype) {
596 case (SymType::SAdd): {
597 return left->grad(cvals, eps) + right->grad(cvals, eps);
598 }
599 case (SymType::SSub): {
600 return left->grad(cvals, eps) - right->grad(cvals, eps);
601 }
602 case (SymType::SMul): {
603 return left->grad(cvals, eps) * right->eval(cvals, eps) +
604 right->grad(cvals, eps) * left->eval(cvals, eps);
605 }
606 case (SymType::SCon): {
607 return Grad({});
608 }
609 case (SymType::SCnt): {
610 switch (left->symtype) {
611 case (SymType::SAdd): {
612 return Grad({});
613 }
614 case (SymType::SSub): {
615 return Grad({});
616 }
617 case (SymType::SMul): {
618 return Grad({});
619 }
620 case (SymType::SCon): {
621 return Grad({});
622 }
623 case (SymType::SCnt): {
624 return Grad({});
625 }
626 case (SymType::SAny): {
627 return Grad({});
628 }
629 default: {
630 std::unordered_map<int, float> nvals(cvals);
631 for (const auto &a : assign) {
632 nvals.emplace(a.first, a.second);
633 }
634 if (left->eval(nvals, eps) <= 0.0f) {
635 return left->grad(nvals, eps);
636 } else {
637 return left->grad(nvals, eps) * -1;
638 }
639 }
640 }
641 }
642 case (SymType::SAny): {
643 std::unordered_map<int, float> tmp = {{var_idx, 1.0f}};
644 return Grad(tmp);
645 }
646 case (SymType::SEq): {
647 float lv = left->eval(cvals, eps);
648 float rv = right->eval(cvals, eps);
649 Grad lg = left->grad(cvals, eps);
650 Grad rg = right->grad(cvals, eps);
651 if (lv == rv) {
652 return Grad({});
653 } else if (lv > rv) {
654 return lg - rg;
655 } else {
656 return rg - lg;
657 }
658 }
659 case (SymType::SNot): {
660 return left->grad(cvals, eps) * (-1.0f);
661 }
662 case (SymType::SAnd): {
663 if (left->eval(cvals, eps) < right->eval(cvals, eps)) {
664 return right->grad(cvals, eps);
665 } else {
666 return left->grad(cvals, eps);
667 }
668 }
669 case (SymType::SOr): {
670 if (left->eval(cvals, eps) > right->eval(cvals, eps)) {
671 return right->grad(cvals, eps);
672 } else {
673 return left->grad(cvals, eps);
674 }
675 }
676 case (SymType::SLt): {
677 return left->grad(cvals, eps) - right->grad(cvals, eps);
678 }
679 case (SymType::SLe): {
680 return left->grad(cvals, eps) - right->grad(cvals, eps);
681 }
682 default: {
683 return Grad({});
684 }
685 }
686 }
687
694 std::string toString(bool convert_to_num) const {
695 std::string result = "";
696 float tmp_word;
697
698 switch (symtype) {
699 case (SymType::SAdd): {
700 result = "(" + left->toString(convert_to_num) + "+" +
701 right->toString(convert_to_num) + ")";
702 break;
703 }
704 case (SymType::SSub): {
705 result = "(" + left->toString(convert_to_num) + "-" +
706 right->toString(convert_to_num) + ")";
707 break;
708 }
709 case (SymType::SMul): {
710 result = "(" + left->toString(convert_to_num) + "*" +
711 right->toString(convert_to_num) + ")";
712 break;
713 }
714 case (SymType::SCon): {
715 if (convert_to_num) {
716 tmp_word = wordToFloat(word);
717 if (is_integer(tmp_word)) {
718 result += std::to_string((int)tmp_word);
719 } else {
720 result += std::to_string(tmp_word);
721 }
722 } else {
723 result += std::to_string(word);
724 }
725 break;
726 }
727 case (SymType::SCnt): {
728 result = "[" + left->toString(convert_to_num);
729 if (assign.size() != 0) {
730 result += "{";
731 for (const auto &a : assign) {
732 result += std::to_string(a.first) + "->";
733 float tmp = a.second;
734 if (is_integer(tmp)) {
735 result += std::to_string((int)tmp) + ",";
736 } else {
737 result += std::to_string(tmp) + ",";
738 }
739 }
740 result += "}";
741 }
742 result += "]";
743 return result;
744 }
745 case (SymType::SAny): {
746 result += "var_" + std::to_string(var_idx);
747 break;
748 }
749 case (SymType::SEq): {
750 result += "(" + left->toString(convert_to_num) +
751 "==" + right->toString(convert_to_num) + ")";
752 break;
753 }
754 case (SymType::SNot): {
755 result += "!" + left->toString(convert_to_num) + "";
756 break;
757 }
758 case (SymType::SAnd): {
759 result += "(" + left->toString(convert_to_num) + "&&" +
760 right->toString(convert_to_num) + ")";
761 break;
762 }
763 case (SymType::SOr): {
764 result += "(" + left->toString(convert_to_num) + "||" +
765 right->toString(convert_to_num) + ")";
766 break;
767 }
768 case (SymType::SLt): {
769 result += "(" + left->toString(convert_to_num) + "<" +
770 right->toString(convert_to_num) + ")";
771 break;
772 }
773 case (SymType::SLe): {
774 result += "(" + left->toString(convert_to_num) +
775 "<=" + right->toString(convert_to_num) + ")";
776 break;
777 }
778 }
779 return result;
780 }
781 };
782
787 struct DiscreteDist {
788 std::vector<int> vals;
789 std::vector<float> probs;
794 DiscreteDist() {}
795 };
796
802 struct DiscreteUniformDist : public DiscreteDist {
803 int low;
804 int high;
813 DiscreteUniformDist(int low, int high) : low(low), high(high) {
814 float p = 1.0f / (1.0f + (float)high - (float)low);
815 for (int i = low; i <= high; i++) {
816 vals.emplace_back(i);
817 probs.emplace_back(p);
818 }
819 }
820 };
821
827 struct BernoulliDist : public DiscreteDist {
828 float p ;
829
830 BernoulliDist(float p) : p(p) {
831 vals = {0, 1};
832 probs = {1 - p, p};
833 }
834 };
835
841 struct BinomialDist : public DiscreteDist {
842 int n;
843 float p;
845 BinomialDist(int n, float p) : n(n), p(p) {
846 std::vector<std::vector<long long>> v(n + 1,
847 std::vector<long long>(n + 1, 0));
848 for (int i = 0; i < v.size(); i++) {
849 v[i][0] = 1;
850 v[i][i] = 1;
851 }
852 for (int j = 1; j < v.size(); j++) {
853 for (int k = 1; k < j; k++) {
854 v[j][k] = (v[j - 1][k - 1] + v[j - 1][k]);
855 }
856 }
857
858 for (int i = 0; i <= n; i++) {
859 vals.emplace_back(i);
860 probs.emplace_back((float)v[n][i] * std::pow(p, (float)i) *
861 std::pow(1.0f - p, (float)n - (float)i));
862 }
863 }
864 };
865
870 using SMem = std::unordered_map<Word32, Sym>;
871
878 struct SymProb {
879 Sym *numerator;
881 Sym *denominator;
890 SymProb()
891 : numerator(new Sym(SymType::SCon, FloatToWord(1.0f))),
892 denominator(new Sym(SymType::SCon, FloatToWord(1.0f))) {}
893
902 SymProb(Sym *numerator, Sym *denominator)
903 : numerator(numerator), denominator(denominator) {}
904
910 std::string toString() {
911 return "(" + numerator->toString(true) + ")/(" +
912 denominator->toString(true) + ")";
913 }
914
921 SymProb operator*(SymProb other) {
922 if (denominator->toString(true) == other.numerator->toString(true)) {
923 return SymProb(numerator, other.denominator);
924 } else if (numerator->toString(true) ==
925 other.denominator->toString(true)) {
926 return SymProb(other.numerator, denominator);
927 } else {
928 return SymProb(
929 new Sym(SymType::SMul, numerator, (other.numerator)),
930 new Sym(SymType::SMul, denominator, (other.denominator)));
931 }
932 }
933
940 SymProb *pmul(SymProb *other) {
941 if (denominator->toString(true) == other->numerator->toString(true)) {
942 return new SymProb(numerator, other->denominator);
943 } else if (numerator->toString(true) ==
944 other->denominator->toString(true)) {
945 return new SymProb(other->numerator, denominator);
946 } else {
947 return new SymProb(
948 new Sym(SymType::SMul, numerator, (other->numerator)),
949 new Sym(SymType::SMul, denominator, (other->denominator)));
950 }
951 }
952
961 std::pair<Sym *, Sym *> marginalize(
962 std::unordered_map<int, DiscreteDist> &var2dist,
963 std::vector<std::vector<int>> &D) {
964 int total_num_pvar_combinations = D.size();
965 Sym *q_numerator = new Sym(SymType::SCon, FloatToWord(0.0f));
966 Sym *q_denominator = new Sym(SymType::SCon, FloatToWord(0.0f));
967
968 for (int i = 0; i < total_num_pvar_combinations; i++) {
969 int j = 0;
970 float tmp_p = 1.0f;
971 std::unordered_map<int, float> tmp_assign;
972 for (auto &vd : var2dist) {
973 tmp_assign.emplace(vd.first, D[i][j]);
974 tmp_p *= vd.second.probs[j];
975 j++;
976 }
977 Sym *weight = new Sym(SymType::SCon, FloatToWord(tmp_p));
978 q_numerator =
979 new Sym(SymType::SAdd, q_numerator,
980 new Sym(SymType::SMul, weight,
981 new Sym(SymType::SCnt, numerator, tmp_assign)));
982 q_denominator = new Sym(
983 SymType::SAdd, q_denominator,
984 new Sym(SymType::SMul, weight,
985 new Sym(SymType::SCnt, denominator, tmp_assign)));
986 }
987
988 return std::make_pair(q_numerator, q_denominator);
989 }
990
1001 float eval(std::unordered_map<int, float> &params, float eps,
1002 std::unordered_map<int, DiscreteDist> &var2dist,
1003 std::vector<std::vector<int>> &D) {
1004 std::pair<Sym *, Sym *> mq = marginalize(var2dist, D);
1005 Sym *q_n = mq.first;
1006 Sym *q_d = mq.second;
1007
1008 float v_n = q_n->eval(params, eps);
1009 float v_d = q_d->eval(params, eps);
1010
1011 if (v_d == 0.0f) {
1012 return 0.0f;
1013 } else {
1014 return v_n / v_d;
1015 }
1016 }
1017
1028 Sym query(SymType symtype, Sym &other,
1029 std::unordered_map<int, DiscreteDist> &var2dist,
1030 std::vector<std::vector<int>> &D) {
1031 std::pair<Sym *, Sym *> mq = marginalize(var2dist, D);
1032 Sym *q_left = mq.first;
1033 Sym *q_right = mq.second;
1034 q_right = new Sym(SymType::SMul, q_right, &other);
1035 return Sym(symtype, q_left, q_right);
1036 }
1037 };
1038
1042 struct SymState {
1043 int pc;
1044 int var_cnt;
1045 Mem mem;
1046 SMem smem;
1047 Linkedlist<Sym> symbolic_stack;
1048 std::vector<Sym>
1049 path_constraints;
1050 SymProb *p;
1051 SymProb *cond_p;
1053 bool has_observed_p_cond
1055 ;
1056
1060 SymState()
1061 : pc(0),
1062 var_cnt(0),
1063 p(new SymProb()),
1064 cond_p(new SymProb()),
1065 has_observed_p_cond(false){};
1066
1081 SymState(int pc, int var_cnt, Mem &mem, SMem &smem,
1082 Linkedlist<Sym> &symbolic_stack,
1083 std::vector<Sym> &path_constraints, SymProb *p, SymProb *cond_p,
1084 bool has_observed_p_cond)
1085 : pc(pc),
1086 var_cnt(var_cnt),
1087 mem(mem),
1088 smem(smem),
1089 symbolic_stack(symbolic_stack),
1090 path_constraints(path_constraints),
1091 p(p),
1092 cond_p(cond_p),
1093 has_observed_p_cond(has_observed_p_cond) {}
1094
1098 SymState *copy() {
1099 return new SymState(pc, var_cnt, mem, smem, symbolic_stack,
1100 path_constraints, p, cond_p, has_observed_p_cond);
1101 }
1102
1108 void set_concrete_val(int var_id, float val) {
1109 mem.emplace(var_id, FloatToWord(val));
1110 }
1111
1119 std::string toString(bool include_memory = true) const {
1120 std::string expr = "";
1121
1122 if (include_memory) {
1123 expr += "Concrete Memory: {";
1124 float tmp_word;
1125 for (auto &t : mem) {
1126 tmp_word = wordToFloat(t.second);
1127 if (is_integer(tmp_word)) {
1128 expr += ("var_" + std::to_string(((int)t.first)) + ": " +
1129 std::to_string((int)tmp_word)) +
1130 ", ";
1131 } else {
1132 expr += ("var_" + std::to_string(((int)t.first)) + ": " +
1133 std::to_string(tmp_word)) +
1134 ", ";
1135 }
1136 }
1137 expr += "}\n";
1138
1139 expr += "Symbolic Memory: {";
1140 for (auto &t : smem) {
1141 expr += "var_" + std::to_string((int)t.first) + ": " +
1142 t.second.toString(true) + ", ";
1143 }
1144 expr += "}\n";
1145 }
1146
1147 expr += "Path Constraints: ";
1148 if (path_constraints.size() > 0) {
1149 expr += path_constraints[0].toString(true);
1150 }
1151 for (int i = 1; i < path_constraints.size(); i++) {
1152 expr += "&&" + path_constraints[i].toString(true);
1153 }
1154 expr += "\n";
1155
1156 return expr;
1157 }
1158
1162 void print() const {
1163 printf("Stack: [");
1164 LLNode<Sym> *tmp = symbolic_stack.head;
1165 while (tmp != NULL) {
1166 printf("%s, ", tmp->data.toString(false).c_str());
1167 tmp = tmp->next;
1168 }
1169 printf("]\n");
1170
1171 printf("%s", toString().c_str());
1172 }
1173 };
1174
1187 using PathConstraintsTable =
1188 std::unordered_map<std::string,
1189 std::pair<bool, std::unordered_map<int, float>>>;
1190
1204 using ProbPathConstraintsTable =
1205 std::unordered_map<int, std::vector<std::tuple<Sym, Mem, SymProb>>>;
1206
1210 struct Trace {
1211 SymState data;
1212 std::vector<Trace> children;
1219 Trace(SymState data, std::vector<Trace> children)
1220 : data(data), children(children) {}
1221
1226 void print(int indent_cnt = 0) const {
1227 printf("PC: %d\n", data.pc);
1228 data.print();
1229 for (const Trace &trace : children) {
1230 trace.print();
1231 }
1232 }
1233 };
1234
1235 } // namespace gymbo
gymbo::Instr
Class representing an instruction.
Definition: type.h:53
gymbo::Instr::Instr
Instr(InstrType instr)
Constructor for an instruction without additional data.
Definition: type.h:62
gymbo::Instr::word
Word32 word
Definition: type.h:56
gymbo::Instr::instr
InstrType instr
Definition: type.h:55
gymbo::Instr::Instr
Instr(InstrType instr, Word32 word)
Constructor for an instruction with additional data.
Definition: type.h:69
gymbo::Instr::print
void print() const
Prints a human-readable representation of the instruction.
Definition: type.h:74
gymbo::Instr::toString
std::string toString() const
Converts the instruction to a string representation.
Definition: type.h:80
gymbo::LLNode
Node for a Doubly Linked List.
Definition: utils.h:131
gymbo::LLNode::next
LLNode * next
Pointer to the next node in the linked list.
Definition: utils.h:134
gymbo::LLNode::data
T data
The data stored in the node.
Definition: utils.h:133
gymbo::Linkedlist
Doubly Linked List Implementation.
Definition: utils.h:156
gymbo
Definition: compiler.h:11
gymbo::wordToFloat
float wordToFloat(uint32_t word)
Converts a 32-bit word representation to a float value.
Definition: utils.h:51
gymbo::ProbPathConstraintsTable
std::unordered_map< int, std::vector< std::tuple< Sym, Mem, SymProb > >> ProbPathConstraintsTable
Alias for a table of probabilistic path constraints.
Definition: type.h:1205
gymbo::InstrType
InstrType
Enum representing different instruction types.
Definition: type.h:24
gymbo::InstrType::Pop
@ Pop
gymbo::InstrType::Dup
@ Dup
gymbo::InstrType::Print
@ Print
gymbo::InstrType::Eq
@ Eq
gymbo::InstrType::Or
@ Or
gymbo::InstrType::Lt
@ Lt
gymbo::InstrType::JmpIf
@ JmpIf
gymbo::InstrType::Mul
@ Mul
gymbo::InstrType::Jmp
@ Jmp
gymbo::InstrType::Read
@ Read
gymbo::InstrType::Swap
@ Swap
gymbo::InstrType::Push
@ Push
gymbo::InstrType::Not
@ Not
gymbo::InstrType::Nop
@ Nop
gymbo::InstrType::RotL
@ RotL
gymbo::InstrType::Le
@ Le
gymbo::InstrType::And
@ And
gymbo::InstrType::Sub
@ Sub
gymbo::InstrType::Add
@ Add
gymbo::InstrType::Over
@ Over
gymbo::InstrType::Load
@ Load
gymbo::InstrType::Done
@ Done
gymbo::InstrType::Store
@ Store
gymbo::is_integer
bool is_integer(float x)
Checks if a float is an integer.
Definition: utils.h:25
gymbo::SymType
SymType
Enum representing different symbolic expression types.
Definition: type.h:247
gymbo::SymType::SAnd
@ SAnd
gymbo::SymType::SEq
@ SEq
gymbo::SymType::SLe
@ SLe
gymbo::SymType::SAdd
@ SAdd
gymbo::SymType::SSub
@ SSub
gymbo::SymType::SOr
@ SOr
gymbo::SymType::SCnt
@ SCnt
gymbo::SymType::SNot
@ SNot
gymbo::SymType::SMul
@ SMul
gymbo::SymType::SLt
@ SLt
gymbo::SymType::SAny
@ SAny
gymbo::SymType::SCon
@ SCon
gymbo::Word32
uint32_t Word32
Alias for 32-bit unsigned integer.
Definition: type.h:19
gymbo::FloatToWord
uint32_t FloatToWord(float val)
Converts a float value to a 32-bit word representation.
Definition: utils.h:36
gymbo::Mem
std::unordered_map< Word32, Word32 > Mem
Alias for memory, represented as an unordered map of 32-bit words.
Definition: type.h:148
gymbo::Prog
std::vector< Instr > Prog
Alias for a program, represented as a vector of instructions.
Definition: type.h:143
gymbo::expr
Node * expr(Token *&token, char *user_input)
Parses an expression from a C-like language program.
Definition: parser.h:210
gymbo::SMem
std::unordered_map< Word32, Sym > SMem
Alias for symbolic memory, represented as an unordered map of symbolic expressions.
Definition: type.h:870
gymbo::PathConstraintsTable
std::unordered_map< std::string, std::pair< bool, std::unordered_map< int, float > >> PathConstraintsTable
Alias for a table of path constraints.
Definition: type.h:1189
gymbo::BernoulliDist
Represents a bernoulli distribution derived from DiscreteDist.
Definition: type.h:827
gymbo::BernoulliDist::p
float p
Definition: type.h:828
gymbo::BernoulliDist::BernoulliDist
BernoulliDist(float p)
Definition: type.h:830
gymbo::BinomialDist
Represents a binomial distribution derived from DiscreteDist.
Definition: type.h:841
gymbo::BinomialDist::n
int n
Definition: type.h:842
gymbo::BinomialDist::p
float p
Definition: type.h:843
gymbo::BinomialDist::BinomialDist
BinomialDist(int n, float p)
Definition: type.h:845
gymbo::DiscreteDist
Represents a discrete probability distribution.
Definition: type.h:787
gymbo::DiscreteDist::vals
std::vector< int > vals
Definition: type.h:788
gymbo::DiscreteDist::DiscreteDist
DiscreteDist()
Default constructor for DiscreteDist.
Definition: type.h:794
gymbo::DiscreteDist::probs
std::vector< float > probs
Definition: type.h:789
gymbo::DiscreteUniformDist
Represents a discrete uniform distribution derived from DiscreteDist.
Definition: type.h:802
gymbo::DiscreteUniformDist::high
int high
Definition: type.h:804
gymbo::DiscreteUniformDist::low
int low
Definition: type.h:803
gymbo::DiscreteUniformDist::DiscreteUniformDist
DiscreteUniformDist(int low, int high)
Constructor for DiscreteUniformDist.
Definition: type.h:813
gymbo::Grad
Struct representing the gradient of a symbolic expression.
Definition: type.h:153
gymbo::Grad::abs
Grad abs()
Compute the absolute values of the gradient.
Definition: type.h:235
gymbo::Grad::operator-
Grad operator-(const Grad &other)
Overloaded subtraction operator for subtracting two gradients.
Definition: type.h:202
gymbo::Grad::operator*
Grad operator*(float w)
Overloaded multiplication operator for multiplying the gradient by a constant.
Definition: type.h:223
gymbo::Grad::val
std::unordered_map< int, float > val
Definition: type.h:155
gymbo::Grad::Grad
Grad(std::unordered_map< int, float > val)
Constructor for the gradient.
Definition: type.h:161
gymbo::Grad::operator+
Grad operator+(float w)
Overloaded addition operator for adding a constant to the gradient.
Definition: type.h:189
gymbo::Grad::operator+
Grad operator+(const Grad &other)
Overloaded addition operator for adding two gradients.
Definition: type.h:168
gymbo::SymProb
Represents a symbolic probability with a numerator and denominator.
Definition: type.h:878
gymbo::SymProb::operator*
SymProb operator*(SymProb other)
Multiplies two SymProb instances.
Definition: type.h:921
gymbo::SymProb::marginalize
std::pair< Sym *, Sym * > marginalize(std::unordered_map< int, DiscreteDist > &var2dist, std::vector< std::vector< int >> &D)
Marginalizes the SymProb over given variable assignments.
Definition: type.h:961
gymbo::SymProb::toString
std::string toString()
Converts SymProb to a string.
Definition: type.h:910
gymbo::SymProb::SymProb
SymProb()
Default constructor for SymProb.
Definition: type.h:890
gymbo::SymProb::pmul
SymProb * pmul(SymProb *other)
Multiplies two SymProb instances.
Definition: type.h:940
gymbo::SymProb::denominator
Sym * denominator
Definition: type.h:881
gymbo::SymProb::numerator
Sym * numerator
Definition: type.h:879
gymbo::SymProb::query
Sym query(SymType symtype, Sym &other, std::unordered_map< int, DiscreteDist > &var2dist, std::vector< std::vector< int >> &D)
Queries the SymProb with a given symbolic type, another symbolic expression, and variable assignments...
Definition: type.h:1028
gymbo::SymProb::SymProb
SymProb(Sym *numerator, Sym *denominator)
Parameterized constructor for SymProb.
Definition: type.h:902
gymbo::SymProb::eval
float eval(std::unordered_map< int, float > &params, float eps, std::unordered_map< int, DiscreteDist > &var2dist, std::vector< std::vector< int >> &D)
Evaluates the SymProb for given parameters, epsilon, variable assignments, and distributions.
Definition: type.h:1001
gymbo::SymState
Struct representing the symbolic state of the symbolic execution.
Definition: type.h:1042
gymbo::SymState::p
SymProb * p
Definition: type.h:1050
gymbo::SymState::cond_p
SymProb * cond_p
Definition: type.h:1051
gymbo::SymState::has_observed_p_cond
bool has_observed_p_cond
Definition: type.h:1055
gymbo::SymState::SymState
SymState(int pc, int var_cnt, Mem &mem, SMem &smem, Linkedlist< Sym > &symbolic_stack, std::vector< Sym > &path_constraints, SymProb *p, SymProb *cond_p, bool has_observed_p_cond)
Constructor for symbolic state with specified values.
Definition: type.h:1081
gymbo::SymState::path_constraints
std::vector< Sym > path_constraints
Definition: type.h:1049
gymbo::SymState::var_cnt
int var_cnt
Definition: type.h:1044
gymbo::SymState::copy
SymState * copy()
Create a copy object.
Definition: type.h:1098
gymbo::SymState::print
void print() const
Prints a human-readable representation of the symbolic state.
Definition: type.h:1162
gymbo::SymState::symbolic_stack
Linkedlist< Sym > symbolic_stack
Definition: type.h:1047
gymbo::SymState::pc
int pc
Definition: type.h:1043
gymbo::SymState::smem
SMem smem
Definition: type.h:1046
gymbo::SymState::SymState
SymState()
Default constructor for symbolic state.
Definition: type.h:1060
gymbo::SymState::toString
std::string toString(bool include_memory=true) const
Returns the human-redable string representation of concrete memory, symbolic memory and path constrai...
Definition: type.h:1119
gymbo::SymState::mem
Mem mem
Definition: type.h:1045
gymbo::SymState::set_concrete_val
void set_concrete_val(int var_id, float val)
Sets a concrete value for a variable in the symbolic state.
Definition: type.h:1108
gymbo::Sym
Struct representing a symbolic expression.
Definition: type.h:265
gymbo::Sym::assign
std::unordered_map< int, float > assign
Definition: type.h:272
gymbo::Sym::Sym
Sym(SymType symtype, Sym *left)
Constructor for Sym with a specified type and left child.
Definition: type.h:284
gymbo::Sym::grad
Grad grad(const std::unordered_map< int, float > &cvals, const float eps) const
Computes the gradient of the symbolic expression given concrete variable values.
Definition: type.h:593
gymbo::Sym::right
Sym * right
Definition: type.h:268
gymbo::Sym::psimplify
Sym * psimplify(const Mem &cvals)
Simplifies the symbolic expression by evaluating constant subexpressions.
Definition: type.h:393
gymbo::Sym::copy
Sym * copy()
Definition: type.h:319
gymbo::Sym::Sym
Sym(SymType symtype, Sym *left, Sym *right, Word32 word, int var_idx)
Definition: type.h:312
gymbo::Sym::gather_var_ids
void gather_var_ids(std::unordered_set< int > &result) const
Gathers variable indices from the symbolic expression.
Definition: type.h:325
gymbo::Sym::Sym
Sym(SymType symtype, Sym *left, std::unordered_map< int, float > &assign)
Definition: type.h:286
gymbo::Sym::Sym
Sym(SymType symtype, Word32 val)
Constructor for Sym with a specified type and Word32 value.
Definition: type.h:304
gymbo::Sym::symtype
SymType symtype
Definition: type.h:266
gymbo::Sym::left
Sym * left
Definition: type.h:267
gymbo::Sym::toString
std::string toString(bool convert_to_num) const
Converts the symbolic expression to a string representation.
Definition: type.h:694
gymbo::Sym::eval
float eval(const std::unordered_map< int, float > &cvals, const float eps) const
Evaluates the symbolic expression given concrete variable values.
Definition: type.h:499
gymbo::Sym::Sym
Sym()
Default constructor for Sym.
Definition: type.h:277
gymbo::Sym::Sym
Sym(SymType symtype, Sym *left, Sym *right)
Constructor for Sym with a specified type, left child, and right child.
Definition: type.h:296
gymbo::Sym::var_idx
int var_idx
Definition: type.h:270
gymbo::Sym::word
Word32 word
Definition: type.h:269
gymbo::Trace
Struct representing a trace in symbolic execution.
Definition: type.h:1210
gymbo::Trace::Trace
Trace(SymState data, std::vector< Trace > children)
Constructor for a trace.
Definition: type.h:1219
gymbo::Trace::print
void print(int indent_cnt=0) const
Prints a human-readable representation of the trace.
Definition: type.h:1226
gymbo::Trace::children
std::vector< Trace > children
Definition: type.h:1212
gymbo::Trace::data
SymState data
Definition: type.h:1211
utils.h
Utility funcitons and classes.