Skip to content

Commit bab79d2

Browse files
tiedaoxiaotubiesebastianpoeplau
tiedaoxiaotubie
authored and
sebastianpoeplau
committed
add atoi() and atol() wrappers
1 parent 91e33e2 commit bab79d2

File tree

3 files changed

+220
-0
lines changed

3 files changed

+220
-0
lines changed

‎runtime/LibcWrappers.cpp‎

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -694,4 +694,168 @@ uint32_t SYM(strlen)(const char *s) {
694694

695695
return (result - s);
696696
}
697+
698+
int SYM(atoi)(const char *s) {
699+
tryAlternative(s, _sym_get_parameter_expression(0), SYM(strlen));
700+
701+
// HACK! we mimic the libc function summary in klee
702+
/* int atoi(const char *str) {
703+
* return (int)strtol(str, (char **)NULL, 10);
704+
* }
705+
* */
706+
auto result = strtol(s, (char **)NULL, 10);
707+
_sym_set_return_expression(nullptr);
708+
709+
if (isConcrete(s, strlen(s)))
710+
return result;
711+
712+
size_t length = strlen(s);
713+
size_t num_len = 0;
714+
for (size_t i = 0; i < length; i++) {
715+
if ('0' <= (char)s[i] && (char)s[i] <= '9') {
716+
num_len++;
717+
} else {
718+
break;
719+
}
720+
}
721+
auto shadow = ReadOnlyShadow(s, length);
722+
auto shadowIt = shadow.begin();
723+
for (size_t i = 0; i < num_len; i++) {
724+
int res = (char)s[i];
725+
auto *cExpr = _sym_build_integer(res, 8);
726+
_sym_push_path_constraint(
727+
_sym_build_equal(
728+
(*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(s[i], 8),
729+
cExpr),
730+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
731+
++shadowIt;
732+
}
733+
734+
// The value of tail must be non-num
735+
auto *tailExpr_0 = _sym_build_integer(48, 8); // '0'
736+
auto *tailExpr_1 = _sym_build_integer(49, 8); // '1'
737+
auto *tailExpr_2 = _sym_build_integer(50, 8); // '2'
738+
auto *tailExpr_3 = _sym_build_integer(51, 8); // '3'
739+
auto *tailExpr_4 = _sym_build_integer(52, 8); // '4'
740+
auto *tailExpr_5 = _sym_build_integer(53, 8); // '5'
741+
auto *tailExpr_6 = _sym_build_integer(54, 8); // '6'
742+
auto *tailExpr_7 = _sym_build_integer(55, 8); // '7'
743+
auto *tailExpr_8 = _sym_build_integer(56, 8); // '8'
744+
auto *tailExpr_9 = _sym_build_integer(57, 8); // '9'
745+
746+
_sym_push_path_constraint(
747+
_sym_build_not_equal(*shadowIt, tailExpr_0),
748+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
749+
_sym_push_path_constraint(
750+
_sym_build_not_equal(*shadowIt, tailExpr_1),
751+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
752+
_sym_push_path_constraint(
753+
_sym_build_not_equal(*shadowIt, tailExpr_2),
754+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
755+
_sym_push_path_constraint(
756+
_sym_build_not_equal(*shadowIt, tailExpr_3),
757+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
758+
_sym_push_path_constraint(
759+
_sym_build_not_equal(*shadowIt, tailExpr_4),
760+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
761+
_sym_push_path_constraint(
762+
_sym_build_not_equal(*shadowIt, tailExpr_5),
763+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
764+
_sym_push_path_constraint(
765+
_sym_build_not_equal(*shadowIt, tailExpr_6),
766+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
767+
_sym_push_path_constraint(
768+
_sym_build_not_equal(*shadowIt, tailExpr_7),
769+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
770+
_sym_push_path_constraint(
771+
_sym_build_not_equal(*shadowIt, tailExpr_8),
772+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
773+
_sym_push_path_constraint(
774+
_sym_build_not_equal(*shadowIt, tailExpr_9),
775+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
776+
777+
return result;
778+
}
779+
780+
long int SYM(atol)(const char *s) {
781+
tryAlternative(s, _sym_get_parameter_expression(0), SYM(strlen));
782+
783+
// HACK! we mimic the libc function summary in klee
784+
/* int atoi(const char *str) {
785+
* return (int)strtol(str, (char **)NULL, 10);
786+
* }
787+
* */
788+
auto result = strtol(s, (char **)NULL, 10);
789+
_sym_set_return_expression(nullptr);
790+
791+
if (isConcrete(s, strlen(s)))
792+
return result;
793+
794+
size_t length = strlen(s);
795+
size_t num_len = 0;
796+
for (size_t i = 0; i < length; i++) {
797+
if ('0' <= (char)s[i] && (char)s[i] <= '9') {
798+
num_len++;
799+
} else {
800+
break;
801+
}
802+
}
803+
auto shadow = ReadOnlyShadow(s, length);
804+
auto shadowIt = shadow.begin();
805+
for (size_t i = 0; i < num_len; i++) {
806+
int res = (char)s[i];
807+
auto *cExpr = _sym_build_integer(res, 8);
808+
_sym_push_path_constraint(
809+
_sym_build_equal(
810+
(*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(s[i], 8),
811+
cExpr),
812+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
813+
++shadowIt;
814+
}
815+
816+
// The value of tail must be non-num
817+
auto *tailExpr_0 = _sym_build_integer(48, 8); // '0'
818+
auto *tailExpr_1 = _sym_build_integer(49, 8); // '1'
819+
auto *tailExpr_2 = _sym_build_integer(50, 8); // '2'
820+
auto *tailExpr_3 = _sym_build_integer(51, 8); // '3'
821+
auto *tailExpr_4 = _sym_build_integer(52, 8); // '4'
822+
auto *tailExpr_5 = _sym_build_integer(53, 8); // '5'
823+
auto *tailExpr_6 = _sym_build_integer(54, 8); // '6'
824+
auto *tailExpr_7 = _sym_build_integer(55, 8); // '7'
825+
auto *tailExpr_8 = _sym_build_integer(56, 8); // '8'
826+
auto *tailExpr_9 = _sym_build_integer(57, 8); // '9'
827+
828+
_sym_push_path_constraint(
829+
_sym_build_not_equal(*shadowIt, tailExpr_0),
830+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
831+
_sym_push_path_constraint(
832+
_sym_build_not_equal(*shadowIt, tailExpr_1),
833+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
834+
_sym_push_path_constraint(
835+
_sym_build_not_equal(*shadowIt, tailExpr_2),
836+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
837+
_sym_push_path_constraint(
838+
_sym_build_not_equal(*shadowIt, tailExpr_3),
839+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
840+
_sym_push_path_constraint(
841+
_sym_build_not_equal(*shadowIt, tailExpr_4),
842+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
843+
_sym_push_path_constraint(
844+
_sym_build_not_equal(*shadowIt, tailExpr_5),
845+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
846+
_sym_push_path_constraint(
847+
_sym_build_not_equal(*shadowIt, tailExpr_6),
848+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
849+
_sym_push_path_constraint(
850+
_sym_build_not_equal(*shadowIt, tailExpr_7),
851+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
852+
_sym_push_path_constraint(
853+
_sym_build_not_equal(*shadowIt, tailExpr_8),
854+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
855+
_sym_push_path_constraint(
856+
_sym_build_not_equal(*shadowIt, tailExpr_9),
857+
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
858+
859+
return result;
860+
}
697861
}

‎runtime/test_wrappers/test_atoi.c‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#include <stdio.h>
2+
#include <string.h>
3+
#include <stdarg.h>
4+
#include <stdlib.h>
5+
#include <stdint.h>
6+
#include <unistd.h>
7+
int main(int argc, char *argv[]) {
8+
9+
char buf[1024];
10+
ssize_t i;
11+
if ((i = read(0, buf, sizeof(buf) - 1)) < 24) return 0;
12+
buf[i] = 0;
13+
if (buf[0] != 'A') return 0;
14+
if (buf[1] != 'B') return 0;
15+
if (buf[2] != 'C') return 0;
16+
if (buf[3] != 'D') return 0;
17+
if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4)) return 0;
18+
if (atoi(buf + 12) == 678) {
19+
printf("The result of atoi(buf+12) is: %lu\n", atoi(buf+12));
20+
printf("HIT!\n");
21+
} else {
22+
printf("The result of atoi(buf+12) is: %lu\n", atoi(buf+12));
23+
printf("NOT HIT!\n");
24+
}
25+
26+
return 0;
27+
28+
}

‎runtime/test_wrappers/test_atol.c‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#include <stdio.h>
2+
#include <string.h>
3+
#include <stdarg.h>
4+
#include <stdlib.h>
5+
#include <stdint.h>
6+
#include <unistd.h>
7+
int main(int argc, char *argv[]) {
8+
9+
char buf[1024];
10+
ssize_t i;
11+
if ((i = read(0, buf, sizeof(buf) - 1)) < 24) return 0;
12+
buf[i] = 0;
13+
if (buf[0] != 'A') return 0;
14+
if (buf[1] != 'B') return 0;
15+
if (buf[2] != 'C') return 0;
16+
if (buf[3] != 'D') return 0;
17+
if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4)) return 0;
18+
if (atol(buf + 12) == 99999999) {
19+
printf("The result of atoi(buf+12) is: %lu\n", atol(buf+12));
20+
printf("HIT!\n");
21+
} else {
22+
printf("The result of atoi(buf+12) is: %lu\n", atol(buf+12));
23+
printf("NOT HIT!\n");
24+
}
25+
26+
return 0;
27+
28+
}

0 commit comments

Comments
 (0)