Skip to content

Commit

Permalink
Memset hook (#866)
Browse files Browse the repository at this point in the history
This PR adds a hook that implements `memset` for the llvm backend. We
intend to use this to perform copies while avoiding the overhead of an
extra buffer copy in the C semantics.

---------

Co-authored-by: rv-jenkins <admin@runtimeverification.com>
  • Loading branch information
mariaKt and rv-jenkins authored Oct 20, 2023
1 parent 44fbb67 commit 480b542
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 0 deletions.
27 changes: 27 additions & 0 deletions runtime/strings/bytes.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -182,6 +182,33 @@ SortBytes hook_BYTES_replaceAt(SortBytes b, SortInt start, SortBytes b2) {
return b;
}

SortBytes
hook_BYTES_memset(SortBytes b, SortInt start, SortInt count, SortInt value) {
uint64_t ustart = get_ui(start);
uint64_t ucount = get_ui(count);
uint64_t uend = ustart + ucount;
if ((uend < ustart) || (uend < ucount)) {
KLLVM_HOOK_INVALID_ARGUMENT(
"Exception on memset: unsigned addition start {} plus count {} wraps "
"around: uend= {}",
ustart, ucount, uend);
}
uint64_t input_len = len(b);
if (uend > input_len) {
KLLVM_HOOK_INVALID_ARGUMENT(
"Buffer overflow on memset: start {} plus count {} is greater "
"than buffer length {}",
ustart, ucount, input_len);
}
int v = mpz_get_si(value);
if ((v < -128) || (v > 127)) {
KLLVM_HOOK_INVALID_ARGUMENT(
"Not a valid value for a byte in memset: v={}", v);
}
memset(b->data + ustart, v, ucount);
return b;
}

SortInt hook_BYTES_length(SortBytes a) {
mpz_t result;
mpz_init_set_ui(result, len(a));
Expand Down
29 changes: 29 additions & 0 deletions unittests/runtime-strings/bytestest.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ string *hook_BYTES_string2bytes(string *s);
string *hook_BYTES_substr(string *b, mpz_t start, mpz_t end);
string *hook_BYTES_replaceAt(string *b, mpz_t start, string *b2);
string *hook_BYTES_update(string *b, mpz_t off, mpz_t val);
string *hook_BYTES_memset(string *b, mpz_t start, mpz_t cnt, mpz_t val);
mpz_ptr hook_BYTES_get(string *b, mpz_t off);
mpz_ptr hook_BYTES_length(string *b);
string *hook_BYTES_padRight(string *b, mpz_t len, mpz_t v);
Expand Down Expand Up @@ -227,6 +228,34 @@ BOOST_AUTO_TEST_CASE(update) {
BOOST_CHECK_EQUAL(0, memcmp(res->data, "1204", 4));
}

BOOST_AUTO_TEST_CASE(memset) {
auto _12345 = makeString("12345");
mpz_t _0, _1, _3;
mpz_init_set_si(_0, '0');
mpz_init_set_ui(_1, 1);
mpz_init_set_ui(_3, 3);

auto res = hook_BYTES_memset(_12345, _1, _3, _0);
BOOST_CHECK_EQUAL(_12345, res);
BOOST_CHECK_EQUAL(5, len(res));
BOOST_CHECK_EQUAL(0, memcmp(res->data, "10005", 5));

mpz_t neg1;
mpz_init_set_si(neg1, -1);
res = hook_BYTES_memset(_12345, _1, _1, neg1);
BOOST_CHECK_EQUAL(_12345, res);
BOOST_CHECK_EQUAL(5, len(res));
BOOST_CHECK_EQUAL((unsigned char)_12345->data[1], 255);

BOOST_CHECK_THROW(
hook_BYTES_memset(_12345, _3, _3, _0), std::invalid_argument);

mpz_t uint64max;
mpz_init_set_ui(uint64max, UINT64_MAX);
BOOST_CHECK_THROW(
hook_BYTES_memset(_12345, _1, uint64max, _0), std::invalid_argument);
}

BOOST_AUTO_TEST_CASE(get) {
auto _1234 = makeString("1234");
mpz_t _0;
Expand Down

0 comments on commit 480b542

Please sign in to comment.