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

[CN-Test-Gen] Add input discard timeout #747

Merged
merged 1 commit into from
Dec 10, 2024
Merged

[CN-Test-Gen] Add input discard timeout #747

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
11 changes: 11 additions & 0 deletions backend/cn/bin/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -458,6 +458,7 @@ let run_tests
max_backtracks
max_unfolds
max_array_length
input_timeout
null_in_every
seed
logging_level
Expand Down Expand Up @@ -532,6 +533,7 @@ let run_tests
max_backtracks;
max_unfolds;
max_array_length;
input_timeout;
null_in_every;
seed;
logging_level;
Expand Down Expand Up @@ -967,6 +969,14 @@ module Testing_flags = struct
& info [ "max-array-length" ] ~doc)


let input_timeout =
let doc = "Timeout for discarding a generation attempt (ms)" in
Arg.(
value
& opt (some int) TestGeneration.default_cfg.input_timeout
& info [ "input-timeout" ] ~doc)


let null_in_every =
let doc = "Set the likelihood of NULL being generated as 1 in every <n>" in
Arg.(
Expand Down Expand Up @@ -1103,6 +1113,7 @@ let testing_cmd =
$ Testing_flags.gen_backtrack_attempts
$ Testing_flags.gen_max_unfolds
$ Testing_flags.max_array_length
$ Testing_flags.input_timeout
$ Testing_flags.null_in_every
$ Testing_flags.seed
$ Testing_flags.logging_level
Expand Down
5 changes: 5 additions & 0 deletions backend/cn/lib/testGeneration/specTests.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -433,6 +433,11 @@ let compile_script ~(output_dir : string) ~(test_file : string) : Pp.document =
space
string
([ "./tests.out" ]
@ (Config.has_input_timeout ()
|> Option.map (fun input_timeout ->
[ "--input-timeout"; string_of_int input_timeout ])
|> Option.to_list
|> List.flatten)
@ (Config.has_null_in_every ()
|> Option.map (fun null_in_every ->
[ "--null-in-every"; string_of_int null_in_every ])
Expand Down
4 changes: 4 additions & 0 deletions backend/cn/lib/testGeneration/testGenConfig.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ type t =
max_backtracks : int;
max_unfolds : int option;
max_array_length : int;
input_timeout : int option;
(* Run time *)
null_in_every : int option;
seed : string option;
Expand All @@ -26,6 +27,7 @@ let default =
max_backtracks = 25;
max_unfolds = None;
max_array_length = 50;
input_timeout = None;
null_in_every = None;
seed = None;
logging_level = None;
Expand Down Expand Up @@ -55,6 +57,8 @@ let get_max_unfolds () = !instance.max_unfolds

let get_max_array_length () = !instance.max_array_length

let has_input_timeout () = !instance.input_timeout

let has_null_in_every () = !instance.null_in_every

let has_seed () = !instance.seed
Expand Down
3 changes: 3 additions & 0 deletions backend/cn/lib/testGeneration/testGenConfig.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ type t =
max_unfolds : int option;
max_array_length : int;
(* Run time *)
input_timeout : int option;
null_in_every : int option;
seed : string option;
logging_level : int option;
Expand Down Expand Up @@ -33,6 +34,8 @@ val get_max_unfolds : unit -> int option

val get_max_array_length : unit -> int

val has_input_timeout : unit -> int option

val has_null_in_every : unit -> int option

val has_seed : unit -> string option
Expand Down
18 changes: 7 additions & 11 deletions runtime/libcn/include/cn-testing/dsl.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,19 +7,15 @@
#include "backtrack.h"


#define CN_GEN_INIT() \
if (0) { \
cn_label_bennet_backtrack: \
cn_gen_decrement_depth(); \
return NULL; \
} \
cn_gen_increment_depth(); \
if (cn_gen_depth() == cn_gen_max_depth()) { \
cn_gen_backtrack_depth_exceeded(); \
goto cn_label_bennet_backtrack; \
}
#define CN_GEN_INIT() CN_GEN_INIT_SIZED(cn_gen_get_max_size())

#define CN_GEN_INIT_SIZED(size) \
if (cn_gen_get_input_timeout() != 0 \
&& cn_gen_get_milliseconds() - cn_gen_get_input_timer() \
> cn_gen_get_input_timeout()) { \
cn_gen_backtrack_assert_failure(); \
goto cn_label_bennet_backtrack; \
} \
if (0) { \
cn_label_bennet_backtrack: \
cn_gen_decrement_depth(); \
Expand Down
8 changes: 8 additions & 0 deletions runtime/libcn/include/cn-testing/size.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,3 +18,11 @@ uint16_t cn_gen_get_depth_failures_allowed();

void cn_gen_set_size_split_backtracks_allowed(uint16_t allowed);
uint16_t cn_gen_get_size_split_backtracks_allowed();

void cn_gen_set_input_timeout(uint8_t seconds);
uint8_t cn_gen_get_input_timeout(void);

void cn_gen_set_input_timer(uint64_t time);
uint64_t cn_gen_get_input_timer(void);

uint64_t cn_gen_get_milliseconds(void);
7 changes: 5 additions & 2 deletions runtime/libcn/include/cn-testing/test.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,16 +41,17 @@ void print_test_info(char* suite, char* name, int tests, int discards);
enum cn_test_result cn_test_##Name (int printing) { \
cn_gen_rand_checkpoint checkpoint = cn_gen_rand_save(); \
int i = 0, d = 0; \
set_cn_failure_cb(&cn_test_##Name##_fail); \
switch (setjmp(buf_##Name)) { \
case CN_FAILURE_ASSERT: \
case CN_FAILURE_CHECK_OWNERSHIP: \
case CN_FAILURE_OWNERSHIP_LEAK: \
return CN_TEST_FAIL; \
case CN_FAILURE_ALLOC: \
cn_gen_rand_replace(checkpoint); \
d++; \
break; \
} \
set_cn_failure_cb(&cn_test_##Name##_fail); \
for (; i < Samples; i++) { \
if (printing) { \
printf("\r"); \
Expand All @@ -59,19 +60,21 @@ void print_test_info(char* suite, char* name, int tests, int discards);
if (d == 10 * Samples) { \
return CN_TEST_GEN_FAIL; \
} \
cn_gen_rand_replace(checkpoint); \
size_t sz = cn_gen_uniform_cn_bits_u16(cn_gen_get_max_size())->val + 1; \
cn_gen_set_size(sz); \
CN_TEST_INIT(); \
cn_gen_set_input_timer(cn_gen_get_milliseconds()); \
struct cn_gen_##Name##_record *res = cn_gen_##Name(); \
if (cn_gen_backtrack_type() != CN_GEN_BACKTRACK_NONE) { \
cn_gen_rand_replace(checkpoint); \
i--; \
d++; \
continue; \
} \
assume_##Name(__VA_ARGS__); \
Init(res); \
Name(__VA_ARGS__); \
cn_gen_rand_replace(checkpoint); \
} \
\
if (printing) { \
Expand Down
55 changes: 55 additions & 0 deletions runtime/libcn/src/cn-testing/size.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,3 +62,58 @@ void cn_gen_set_size_split_backtracks_allowed(uint16_t allowed) {
uint16_t cn_gen_get_size_split_backtracks_allowed() {
return size_split_backtracks_allowed;
}

static uint8_t timeout = 0;

void cn_gen_set_input_timeout(uint8_t seconds) {
timeout = seconds;
}

uint8_t cn_gen_get_input_timeout(void) {
return timeout;
}

static uint64_t timer = 0;

void cn_gen_set_input_timer(uint64_t time) {
timer = time;
}

uint64_t cn_gen_get_input_timer(void) {
return timer;
}

#if defined (__unix__) || (defined (__APPLE__) && defined (__MACH__))
#include <sys/time.h>
#elif defined(_WIN32) || defined(_WIN64)
#include <Windows.h>

/// Taken from https://stackoverflow.com/questions/10905892/equivalent-of-gettimeofday-for-windows
int gettimeofday(struct timeval* tp, struct timezone* tzp)
{
// Note: some broken versions only have 8 trailing zero's, the correct epoch has 9 trailing zero's
// This magic number is the number of 100 nanosecond intervals since January 1, 1601 (UTC)
// until 00:00:00 January 1, 1970
static const uint64_t EPOCH = ((uint64_t)116444736000000000ULL);

SYSTEMTIME system_time;
FILETIME file_time;
uint64_t time;

GetSystemTime(&system_time);
SystemTimeToFileTime(&system_time, &file_time);
time = ((uint64_t)file_time.dwLowDateTime);
time += ((uint64_t)file_time.dwHighDateTime) << 32;

tp->tv_sec = (long)((time - EPOCH) / 10000000L);
tp->tv_usec = (long)(system_time.wMilliseconds * 1000);
return 0;
}
#endif

uint64_t cn_gen_get_milliseconds(void) {
struct timeval tv;

gettimeofday(&tv, NULL);
return (((uint64_t)tv.tv_sec) * 1000) + (tv.tv_usec / 1000);
}
14 changes: 10 additions & 4 deletions runtime/libcn/src/cn-testing/test.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
#include <time.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
Expand Down Expand Up @@ -54,14 +53,15 @@ void print_test_info(char* suite, char* name, int tests, int discards) {
}

int cn_test_main(int argc, char* argv[]) {
int begin_time = time(NULL);
int begin_time = cn_gen_get_milliseconds();
set_cn_logging_level(CN_LOGGING_NONE);

cn_gen_srand(time(NULL));
cn_gen_srand(cn_gen_get_milliseconds());
uint64_t seed = cn_gen_rand();
int interactive = 0;
enum cn_logging_level logging_level = CN_LOGGING_ERROR;
int timeout = 0;
int input_timeout = 0;
int exit_fast = 0;
for (int i = 0; i < argc; i++) {
char* arg = argv[i];
Expand All @@ -77,6 +77,10 @@ int cn_test_main(int argc, char* argv[]) {
logging_level = strtol(argv[i + 1], NULL, 10);
i++;
}
else if (strcmp("--input-timeout", arg) == 0) {
input_timeout = strtol(argv[i + 1], NULL, 10);
i++;
}
else if (strcmp("--null-in-every", arg) == 0) {
set_null_in_every(strtol(argv[i + 1], NULL, 10));
i++;
Expand Down Expand Up @@ -138,6 +142,7 @@ int cn_test_main(int argc, char* argv[]) {
struct cn_test_case* test_case = &test_cases[i];
print_test_info(test_case->suite, test_case->name, 0, 0);
checkpoints[i] = cn_gen_rand_save();
cn_gen_set_input_timeout(input_timeout);
enum cn_test_result result = test_case->func(1);
if (!(results[i] == CN_TEST_PASS && result == CN_TEST_GEN_FAIL)) {
results[i] = result;
Expand All @@ -151,6 +156,7 @@ int cn_test_main(int argc, char* argv[]) {
printf("FAILED\n");
set_cn_logging_level(logging_level);
cn_gen_rand_restore(checkpoints[i]);
cn_gen_set_input_timeout(0);
test_case->func(0);
set_cn_logging_level(CN_LOGGING_NONE);
printf("\n\n");
Expand All @@ -168,7 +174,7 @@ int cn_test_main(int argc, char* argv[]) {
}

if (timeout != 0) {
timediff = time(NULL) - begin_time;
timediff = cn_gen_get_milliseconds() / 1000 - begin_time;
}
}
if (timediff < timeout) {
Expand Down
2 changes: 1 addition & 1 deletion tests/run-cn-test-gen.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ for CONFIG in ${CONFIGS[@]}; do
echo "Running CI with CLI config \"$CONFIG\""
separator

CONFIG="$CONFIG --max-generator-size=10 --allowed-depth-failures=100"
CONFIG="$CONFIG --allowed-depth-failures=100 --input-timeout=1000"

# Test each `*.c` file
for TEST in $FILES; do
Expand Down