Skip to content

Commit

Permalink
add atoi() and atol() wrappers
Browse files Browse the repository at this point in the history
  • Loading branch information
@tiedaoxiaotubie
tiedaoxiaotubie committed Sep 13, 2021
1 parent e0afbb6 commit 16c29aa
Show file tree
Hide file tree
Showing 3 changed files with 220 additions and 0 deletions.
164 changes: 164 additions & 0 deletions runtime/LibcWrappers.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -471,4 +471,168 @@ uint32_t SYM(strlen)(const char *s) {

return (result - s);
}

int SYM(atoi)(const char *s) {
tryAlternative(s, _sym_get_parameter_expression(0), SYM(strlen));

// HACK! we mimic the libc function summary in klee
/* int atoi(const char *str) {
* return (int)strtol(str, (char **)NULL, 10);
* }
* */
auto result = strtol(s, (char **)NULL, 10);
_sym_set_return_expression(nullptr);

if (isConcrete(s, strlen(s)))
return result;

size_t length = strlen(s);
size_t num_len = 0;
for (size_t i = 0; i < length; i++) {
if ('0' <= (char)s[i] && (char)s[i] <= '9') {
num_len++;
} else {
break;
}
}
auto shadow = ReadOnlyShadow(s, length);
auto shadowIt = shadow.begin();
for (size_t i = 0; i < num_len; i++) {
int res = (char)s[i];
auto *cExpr = _sym_build_integer(res, 8);
_sym_push_path_constraint(
_sym_build_equal(
(*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(s[i], 8),
cExpr),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
++shadowIt;
}

// The value of tail must be non-num
auto *tailExpr_0 = _sym_build_integer(48, 8); // '0'
auto *tailExpr_1 = _sym_build_integer(49, 8); // '1'
auto *tailExpr_2 = _sym_build_integer(50, 8); // '2'
auto *tailExpr_3 = _sym_build_integer(51, 8); // '3'
auto *tailExpr_4 = _sym_build_integer(52, 8); // '4'
auto *tailExpr_5 = _sym_build_integer(53, 8); // '5'
auto *tailExpr_6 = _sym_build_integer(54, 8); // '6'
auto *tailExpr_7 = _sym_build_integer(55, 8); // '7'
auto *tailExpr_8 = _sym_build_integer(56, 8); // '8'
auto *tailExpr_9 = _sym_build_integer(57, 8); // '9'

_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_0),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_1),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_2),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_3),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_4),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_5),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_6),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_7),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_8),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_9),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));

return result;
}

long int SYM(atol)(const char *s) {
tryAlternative(s, _sym_get_parameter_expression(0), SYM(strlen));

// HACK! we mimic the libc function summary in klee
/* int atoi(const char *str) {
* return (int)strtol(str, (char **)NULL, 10);
* }
* */
auto result = strtol(s, (char **)NULL, 10);
_sym_set_return_expression(nullptr);

if (isConcrete(s, strlen(s)))
return result;

size_t length = strlen(s);
size_t num_len = 0;
for (size_t i = 0; i < length; i++) {
if ('0' <= (char)s[i] && (char)s[i] <= '9') {
num_len++;
} else {
break;
}
}
auto shadow = ReadOnlyShadow(s, length);
auto shadowIt = shadow.begin();
for (size_t i = 0; i < num_len; i++) {
int res = (char)s[i];
auto *cExpr = _sym_build_integer(res, 8);
_sym_push_path_constraint(
_sym_build_equal(
(*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(s[i], 8),
cExpr),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
++shadowIt;
}

// The value of tail must be non-num
auto *tailExpr_0 = _sym_build_integer(48, 8); // '0'
auto *tailExpr_1 = _sym_build_integer(49, 8); // '1'
auto *tailExpr_2 = _sym_build_integer(50, 8); // '2'
auto *tailExpr_3 = _sym_build_integer(51, 8); // '3'
auto *tailExpr_4 = _sym_build_integer(52, 8); // '4'
auto *tailExpr_5 = _sym_build_integer(53, 8); // '5'
auto *tailExpr_6 = _sym_build_integer(54, 8); // '6'
auto *tailExpr_7 = _sym_build_integer(55, 8); // '7'
auto *tailExpr_8 = _sym_build_integer(56, 8); // '8'
auto *tailExpr_9 = _sym_build_integer(57, 8); // '9'

_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_0),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_1),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_2),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_3),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_4),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_5),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_6),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_7),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_8),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
_sym_push_path_constraint(
_sym_build_not_equal(*shadowIt, tailExpr_9),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));

return result;
}
}
28 changes: 28 additions & 0 deletions runtime/test_wrappers/test_atoi.c
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
#include <stdio.h>
#include <string.h>
#include <stdarg.h>
#include <stdlib.h>
#include <stdint.h>
#include <unistd.h>
int main(int argc, char *argv[]) {

char buf[1024];
ssize_t i;
if ((i = read(0, buf, sizeof(buf) - 1)) < 24) return 0;
buf[i] = 0;
if (buf[0] != 'A') return 0;
if (buf[1] != 'B') return 0;
if (buf[2] != 'C') return 0;
if (buf[3] != 'D') return 0;
if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4)) return 0;
if (atoi(buf + 12) == 678) {
printf("The result of atoi(buf+12) is: %lu\n", atoi(buf+12));
printf("HIT!\n");
} else {
printf("The result of atoi(buf+12) is: %lu\n", atoi(buf+12));
printf("NOT HIT!\n");
}

return 0;

}
28 changes: 28 additions & 0 deletions runtime/test_wrappers/test_atol.c
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
#include <stdio.h>
#include <string.h>
#include <stdarg.h>
#include <stdlib.h>
#include <stdint.h>
#include <unistd.h>
int main(int argc, char *argv[]) {

char buf[1024];
ssize_t i;
if ((i = read(0, buf, sizeof(buf) - 1)) < 24) return 0;
buf[i] = 0;
if (buf[0] != 'A') return 0;
if (buf[1] != 'B') return 0;
if (buf[2] != 'C') return 0;
if (buf[3] != 'D') return 0;
if (memcmp(buf + 4, "1234", 4) || memcmp(buf + 8, "EFGH", 4)) return 0;
if (atol(buf + 12) == 99999999) {
printf("The result of atoi(buf+12) is: %lu\n", atol(buf+12));
printf("HIT!\n");
} else {
printf("The result of atoi(buf+12) is: %lu\n", atol(buf+12));
printf("NOT HIT!\n");
}

return 0;

}

0 comments on commit 16c29aa

Please sign in to comment.