Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

More wrappers #79

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open

More wrappers #79

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
2636452
add strcmp() wrapper
tiedaoxiaotubie Sep 13, 2021
6df681f
add strncmp() wrapper
tiedaoxiaotubie Sep 13, 2021
91e33e2
add test_strlen() wrapper
tiedaoxiaotubie Sep 13, 2021
bab79d2
add atoi() and atol() wrappers
tiedaoxiaotubie Sep 13, 2021
496dac1
add strcpy() wrapper
tiedaoxiaotubie Sep 13, 2021
99a7410
Fix formatting of the new libc wrappers
sebastianpoeplau Feb 22, 2023
8539671
Move the new libc wrapper tests to the test directory
sebastianpoeplau Feb 22, 2023
a725c60
Merge branch 'master' into more_wrappers
aurelf Feb 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
268 changes: 268 additions & 0 deletions runtime/LibcWrappers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -608,4 +608,272 @@ uint32_t SYM(ntohl)(uint32_t netlong) {

return result;
}

int SYM(strcmp)(const char *a, const char *b) {
tryAlternative(a, _sym_get_parameter_expression(0), SYM(strcmp));
tryAlternative(b, _sym_get_parameter_expression(1), SYM(strcmp));

auto result = strcmp(a, b);
_sym_set_return_expression(nullptr);

if (isConcrete(a, strlen(a)) && isConcrete(b, strlen(b)))
return result;

auto aShadowIt = ReadOnlyShadow(a, strlen(a)).begin_non_null();
auto bShadowIt = ReadOnlyShadow(b, strlen(b)).begin_non_null();
auto *allEqual = _sym_build_equal(*aShadowIt, *bShadowIt);
for (size_t i = 1; i < strlen(a); i++) {
++aShadowIt;
++bShadowIt;
allEqual =
_sym_build_bool_and(allEqual, _sym_build_equal(*aShadowIt, *bShadowIt));
}

_sym_push_path_constraint(allEqual, result == 0,
reinterpret_cast<uintptr_t>(SYM(strcmp)));
return result;
}

int SYM(strncmp)(const char *a, const char *b, size_t n) {
tryAlternative(a, _sym_get_parameter_expression(0), SYM(strncmp));
tryAlternative(b, _sym_get_parameter_expression(1), SYM(strncmp));
tryAlternative(n, _sym_get_parameter_expression(2), SYM(strncmp));

auto result = strncmp(a, b, n);
_sym_set_return_expression(nullptr);

if (isConcrete(a, n) && isConcrete(b, n))
return result;

auto aShadowIt = ReadOnlyShadow(a, n).begin_non_null();
auto bShadowIt = ReadOnlyShadow(b, n).begin_non_null();
auto *allEqual = _sym_build_equal(*aShadowIt, *bShadowIt);
for (size_t i = 1; i < n; i++) {
++aShadowIt;
++bShadowIt;
allEqual =
_sym_build_bool_and(allEqual, _sym_build_equal(*aShadowIt, *bShadowIt));
}

_sym_push_path_constraint(allEqual, result == 0,
reinterpret_cast<uintptr_t>(SYM(strncmp)));
return result;
}

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

// HACK! we regard strlen as a special strchr(s, '\0')
auto *result = strchr(s, 0);
_sym_set_return_expression(nullptr);

if (isConcrete(s, result != nullptr ? (result - s) : strlen(s)))
return (result - s);

// We force set the value of c to \x00, it should be a concrete value
auto *cExpr = _sym_build_integer(0, 8);

size_t length = result != nullptr ? (result - s) : strlen(s);
auto shadow = ReadOnlyShadow(s, length);
auto shadowIt = shadow.begin();
for (size_t i = 0; i < length; i++) {
_sym_push_path_constraint(
_sym_build_not_equal(
(*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(s[i], 8),
cExpr),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));
++shadowIt;
}

// HACK! The last byte must be \x00!
_sym_push_path_constraint(
_sym_build_equal(
(*shadowIt != nullptr) ? *shadowIt : _sym_build_integer(0, 8), cExpr),
/*taken*/ 1, reinterpret_cast<uintptr_t>(SYM(strchr)));

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) {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is really similar to the wrapper for atoi. Should we merge the two?

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;
}

char *SYM(strcpy)(char *dest, const char *src) {
tryAlternative(dest, _sym_get_parameter_expression(0), SYM(strcpy));
tryAlternative(src, _sym_get_parameter_expression(1), SYM(strcpy));

auto *result = strcpy(dest, src);
_sym_set_return_expression(nullptr);

size_t cpyLen = strlen(src);
if (isConcrete(src, cpyLen) && isConcrete(dest, cpyLen))
return result;

auto srcShadow = ReadOnlyShadow(src, cpyLen);
auto destShadow = ReadWriteShadow(dest, cpyLen);

std::copy(srcShadow.begin(), srcShadow.end(), destShadow.begin());

return result;
}
}
33 changes: 33 additions & 0 deletions test/atoi.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
#include <stdarg.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.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;
}
33 changes: 33 additions & 0 deletions test/atol.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
#include <stdarg.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.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;
}
31 changes: 31 additions & 0 deletions test/strcmp.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
#include <stdarg.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.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 (strcmp(buf + 12, "AAAA") == 0) {
printf("HIT!\n");
} else {
printf("NOT HIT!\n");
}

return 0;
}
Loading
Loading