Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
6 changes: 3 additions & 3 deletions regressions/ck_ec/validate/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -48,13 +48,13 @@ ck_ec_smoke_test: ../../../src/ck_ec.c ck_ec_smoke_test.c ../../../src/ck_ec_tim
prop_test_slow_wakeup: ../../../src/ck_ec.c prop_test_slow_wakeup.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
$(CC) $(CFLAGS) $(FUZZ_CFLAGS) ../../../src/ck_ec.c -o prop_test_slow_wakeup prop_test_slow_wakeup.c

prop_test_timeutil_add: ../../../src/ck_ec.c prop_test_timeutil_add.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
prop_test_timeutil_add: ../../../src/ck_ec.c prop_test_timeutil_add.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h int128.h
$(CC) $(CFLAGS) $(FUZZ_CFLAGS) ../../../src/ck_ec.c -o prop_test_timeutil_add prop_test_timeutil_add.c

prop_test_timeutil_add_ns: ../../../src/ck_ec.c prop_test_timeutil_add_ns.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
prop_test_timeutil_add_ns: ../../../src/ck_ec.c prop_test_timeutil_add_ns.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h int128.h
$(CC) $(CFLAGS) $(FUZZ_CFLAGS) ../../../src/ck_ec.c -o prop_test_timeutil_add_ns prop_test_timeutil_add_ns.c

prop_test_timeutil_cmp: ../../../src/ck_ec.c prop_test_timeutil_cmp.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
prop_test_timeutil_cmp: ../../../src/ck_ec.c prop_test_timeutil_cmp.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h int128.h
$(CC) $(CFLAGS) $(FUZZ_CFLAGS) ../../../src/ck_ec.c -o prop_test_timeutil_cmp prop_test_timeutil_cmp.c

prop_test_timeutil_scale: ../../../src/ck_ec.c prop_test_timeutil_scale.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
Expand Down
96 changes: 96 additions & 0 deletions regressions/ck_ec/validate/int128.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
#ifndef CK_INT128_H
#define CK_INT128_H

#include <ck_stdint.h>

typedef struct ck_s128 {
uint64_t hi;
uint64_t lo;
} ck_s128_t;

static inline ck_s128_t
ck_s128_make_s64(int64_t value)
{
return (ck_s128_t) {
value < 0 ? (uint64_t)-1 : 0,
(uint64_t)value,
};
}

static inline int
ck_s128_cmp(ck_s128_t lhs, ck_s128_t rhs)
{
if ((int64_t)lhs.hi < (int64_t)rhs.hi) {
return -1;
}

if ((int64_t)lhs.hi > (int64_t)rhs.hi) {
return 1;
}

if (lhs.lo < rhs.lo) {
return -1;
}

if (lhs.lo > rhs.lo) {
return 1;
}

return 0;
}

static inline ck_s128_t
ck_s128_add(ck_s128_t lhs, ck_s128_t rhs)
{
return (ck_s128_t) {
lhs.hi + rhs.hi + ((lhs.lo + rhs.lo) < lhs.lo),
lhs.lo + rhs.lo,
};
}

static inline ck_s128_t
ck_s128_mul(ck_s128_t lhs, ck_s128_t rhs)
{
/*
* A s128 represents hi * 2^64 + lo. Multiplying two s128 values gives
* four terms:
*
* lhs.lo * rhs.lo
* lhs.hi * rhs.lo * 2^64
* lhs.lo * rhs.hi * 2^64
* lhs.hi * rhs.hi * 2^128
*
* We need only the low 128 bits, so the last term can be ignored. The
* middle two terms contribute only to result.hi.
*
* Computing lhs.lo * rhs.lo still requires a 128-bit result. We split
* both 64-bit values into 32-bit halves:
*
* lhs.lo = a * 2^32 + b
* rhs.lo = c * 2^32 + d
*
* Then:
*
* lhs.lo * rhs.lo = a*c * 2^64 + (a*d + b*c) * 2^32 + b*d
*
* Inspired by Abseil's int128 implementation:
* https://github.com/abseil/abseil-cpp/blob/20260526.0/absl/numeric/int128.h#L1035
*/
uint64_t a = lhs.lo >> 32;
uint64_t b = (uint32_t)lhs.lo;
uint64_t c = rhs.lo >> 32;
uint64_t d = (uint32_t)rhs.lo;

ck_s128_t result = (ck_s128_t) {
(lhs.hi * rhs.lo) + (lhs.lo * rhs.hi) + (a * c),
(b * d),
};
result = ck_s128_add(result,
(ck_s128_t) { (a * d) >> 32, (a * d) << 32 });
result = ck_s128_add(result,
(ck_s128_t) { (b * c) >> 32, (b * c) << 32 });

return result;
}

#endif /* CK_INT128_H */
27 changes: 14 additions & 13 deletions regressions/ck_ec/validate/prop_test_timeutil_add.c
Original file line number Diff line number Diff line change
@@ -1,15 +1,9 @@
#include <assert.h>
#include <ck_limits.h>
#include <ck_stdint.h>

#include "../../../src/ck_ec_timeutil.h"
#include "fuzz_harness.h"

#if ULONG_MAX > 4294967295
typedef unsigned __int128 dword_t;
#else
typedef uint64_t dword_t;
#endif
#include "int128.h"

struct example {
struct timespec ts;
Expand Down Expand Up @@ -75,24 +69,31 @@ static struct timespec normalize_ts(const struct timespec ts)
return ret;
}

static dword_t ts_to_nanos(const struct timespec ts)
static ck_s128_t ts_to_nanos(const struct timespec ts)
{
return (dword_t)ts.tv_sec * (NSEC_MAX + 1) + ts.tv_nsec;
ck_s128_t ret = ck_s128_mul(ck_s128_make_s64(ts.tv_sec),
ck_s128_make_s64(NSEC_MAX + 1));
ret = ck_s128_add(ret, ck_s128_make_s64(ts.tv_nsec));
return ret;
}

static inline int test_timespec_add(const struct example *example)
{
const struct timespec ts = normalize_ts(example->ts);
const struct timespec inc = normalize_ts(example->inc);
const struct timespec actual = timespec_add(ts, inc);
const dword_t nanos = ts_to_nanos(ts) + ts_to_nanos(inc);
const ck_s128_t nanos = ck_s128_add(ts_to_nanos(ts), ts_to_nanos(inc));

const ck_s128_t ceiling = ts_to_nanos(
(struct timespec) { TIME_MAX, NSEC_MAX });

if (nanos / (NSEC_MAX + 1) > TIME_MAX) {
if (ck_s128_cmp(nanos, ceiling) > 0) {
assert(actual.tv_sec == TIME_MAX);
assert(actual.tv_nsec == NSEC_MAX);
} else {
assert(actual.tv_sec == (time_t)(nanos / (NSEC_MAX + 1)));
assert(actual.tv_nsec == (long)(nanos % (NSEC_MAX + 1)));
assert(ck_s128_cmp(ts_to_nanos(actual), nanos) == 0);
assert(actual.tv_nsec >= 0);
assert(actual.tv_nsec <= NSEC_MAX);
}

return 0;
Expand Down
57 changes: 33 additions & 24 deletions regressions/ck_ec/validate/prop_test_timeutil_add_ns.c
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,7 @@

#include "../../../src/ck_ec_timeutil.h"
#include "fuzz_harness.h"

#if ULONG_MAX > 4294967295
typedef unsigned __int128 dword_t;
#else
typedef uint64_t dword_t;
#endif
#include "int128.h"

struct example {
struct timespec ts;
Expand Down Expand Up @@ -45,41 +40,55 @@ static const struct example examples[] = {
}
};

static inline int test_timespec_add_ns(const struct example *example)
static struct timespec normalize_ts(const struct timespec ts)
{
struct timespec ts = {
.tv_sec = example->ts.tv_sec,
.tv_nsec = example->ts.tv_nsec
};
const uint32_t ns = example->ns;
struct timespec ret = ts;

if (ts.tv_sec < 0) {
ts.tv_sec = ~ts.tv_sec;
if (ret.tv_sec < 0) {
ret.tv_sec = ~ret.tv_sec;
}

if (ts.tv_nsec < 0) {
ts.tv_nsec = ~ts.tv_nsec;
if (ret.tv_nsec < 0) {
ret.tv_nsec = ~ret.tv_nsec;
}

ts.tv_nsec %= NSEC_MAX + 1;
ret.tv_nsec %= NSEC_MAX + 1;
return ret;
}

static ck_s128_t ts_to_nanos(const struct timespec ts)
{
ck_s128_t ret = ck_s128_mul(ck_s128_make_s64(ts.tv_sec),
ck_s128_make_s64(NSEC_MAX + 1));
ret = ck_s128_add(ret, ck_s128_make_s64(ts.tv_nsec));
return ret;
}

static inline int test_timespec_add_ns(const struct example *example)
{
const struct timespec ts = normalize_ts(example->ts);
const uint32_t ns = example->ns;

const struct timespec actual = timespec_add_ns(ts, ns);

dword_t nanos =
(dword_t)ts.tv_sec * (NSEC_MAX + 1) + ts.tv_nsec;
ck_s128_t nanos = ts_to_nanos(ts);

if (ns > NSEC_MAX) {
nanos += NSEC_MAX + 1;
nanos = ck_s128_add(nanos, ck_s128_make_s64(NSEC_MAX + 1));
} else {
nanos += ns;
nanos = ck_s128_add(nanos, ck_s128_make_s64(ns));
}

if (nanos / (NSEC_MAX + 1) > TIME_MAX) {
const ck_s128_t ceiling = ts_to_nanos(
(struct timespec) { TIME_MAX, NSEC_MAX });

if (ck_s128_cmp(nanos, ceiling) > 0) {
assert(actual.tv_sec == TIME_MAX);
assert(actual.tv_nsec == NSEC_MAX);
} else {
assert(actual.tv_sec == (time_t)(nanos / (NSEC_MAX + 1)));
assert(actual.tv_nsec == (long)(nanos % (NSEC_MAX + 1)));
assert(ck_s128_cmp(ts_to_nanos(actual), nanos) == 0);
assert(actual.tv_nsec >= 0);
assert(actual.tv_nsec <= NSEC_MAX);
}

return 0;
Expand Down
22 changes: 10 additions & 12 deletions regressions/ck_ec/validate/prop_test_timeutil_cmp.c
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,7 @@

#include "../../../src/ck_ec_timeutil.h"
#include "fuzz_harness.h"

#if ULONG_MAX > 4294967295
typedef __int128 dsword_t;
#else
typedef int64_t dsword_t;
#endif
#include "int128.h"

struct example {
struct timespec x;
Expand Down Expand Up @@ -69,25 +64,28 @@ static struct timespec normalize_ts(const struct timespec ts)
return ret;
}

static dsword_t ts_to_nanos(const struct timespec ts)
static ck_s128_t ts_to_nanos(const struct timespec ts)
{
return (dsword_t)ts.tv_sec * (NSEC_MAX + 1) + ts.tv_nsec;
ck_s128_t ret = ck_s128_mul(ck_s128_make_s64(ts.tv_sec),
ck_s128_make_s64(NSEC_MAX + 1));
ret = ck_s128_add(ret, ck_s128_make_s64(ts.tv_nsec));
return ret;
}

static inline int test_timespec_cmp(const struct example *example)
{
const struct timespec x = normalize_ts(example->y);
const struct timespec y = normalize_ts(example->x);
const dsword_t x_nanos = ts_to_nanos(x);
const dsword_t y_nanos = ts_to_nanos(y);
const ck_s128_t x_nanos = ts_to_nanos(x);
const ck_s128_t y_nanos = ts_to_nanos(y);

assert(timespec_cmp(x, x) == 0);
assert(timespec_cmp(y, y) == 0);
assert(timespec_cmp(x, y) == -timespec_cmp(y, x));

if (x_nanos == y_nanos) {
if (ck_s128_cmp(x_nanos, y_nanos) == 0) {
assert(timespec_cmp(x, y) == 0);
} else if (x_nanos < y_nanos) {
} else if (ck_s128_cmp(x_nanos, y_nanos) < 0) {
assert(timespec_cmp(x, y) == -1);
} else {
assert(timespec_cmp(x, y) == 1);
Expand Down