Skip to content

Commit b836c78

Browse files
Saveliy Grigoryevsava-cska
authored andcommitted
Add TimeoutPerTest for generation tests for project
1 parent 29c1be0 commit b836c78

2 files changed

Lines changed: 165 additions & 11 deletions

File tree

lib/Runner/run_klee.cpp

Lines changed: 73 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@
6060
#include <signal.h>
6161
#include <sys/stat.h>
6262
#include <sys/wait.h>
63+
#include <thread>
6364
#include <unistd.h>
6465

6566
#include <cerrno>
@@ -154,6 +155,10 @@ cl::opt<bool> InteractiveMode("interactive",
154155
cl::desc("Launch klee in interactive mode."),
155156
cl::init(false), cl::cat(StartCat));
156157

158+
cl::opt<int> TimeoutPerFunction("timeout-per-function",
159+
cl::desc("Timeout per function in klee."),
160+
cl::init(0), cl::cat(StartCat));
161+
157162
cl::opt<std::string>
158163
EntryPointsFile("entrypoints-file",
159164
cl::desc("Path to file with entrypoints name."),
@@ -1575,6 +1580,43 @@ static int run_klee_on_function(
15751580
return 0;
15761581
}
15771582

1583+
void kill_child(pid_t child_pid) {
1584+
if (kill(child_pid, 0) != 0) {
1585+
return;
1586+
}
1587+
int statusSIGTERM = kill(child_pid, SIGTERM);
1588+
std::this_thread::sleep_for(std::chrono::milliseconds(10));
1589+
if (kill(child_pid, 0) == 0) {
1590+
int statusSIGKILL = kill(child_pid, SIGKILL);
1591+
if (statusSIGKILL != 0) {
1592+
klee_error("Kill with signal SIGKILL return nonzero code.");
1593+
}
1594+
}
1595+
}
1596+
1597+
void wait_until_any_child_dies(const std::vector<std::pair<pid_t,
1598+
std::chrono::time_point<std::chrono::steady_clock>>> &child_processes) {
1599+
while (true) {
1600+
bool something_dead = false;
1601+
for (const auto &child_process : child_processes) {
1602+
if (kill(child_process.first, 0) != 0) {
1603+
something_dead = true;
1604+
}
1605+
auto current_time = std::chrono::steady_clock::now();
1606+
auto duration_function = std::chrono::duration_cast<std::chrono::seconds>(current_time -
1607+
child_process.second).count();
1608+
if (duration_function > TimeoutPerFunction) {
1609+
kill_child(child_process.first);
1610+
something_dead = true;
1611+
}
1612+
}
1613+
if (something_dead) {
1614+
break;
1615+
}
1616+
std::this_thread::sleep_for(std::chrono::milliseconds(10));
1617+
}
1618+
}
1619+
15781620
int run_klee(int argc, char **argv, char **envp) {
15791621
if (theInterpreter) {
15801622
theInterpreter = nullptr;
@@ -1881,29 +1923,36 @@ int run_klee(int argc, char **argv, char **envp) {
18811923

18821924
SmallString<128> outputDirectory = handler->getOutputDirectory();
18831925
const int PROCESS = ProcessNumber;
1884-
std::vector<pid_t> child_process;
1926+
using time_point = std::chrono::time_point<std::chrono::steady_clock>;
1927+
std::vector<std::pair<pid_t, time_point>> child_processes;
1928+
signal(SIGCHLD, SIG_IGN);
18851929
while (true) {
18861930
std::string entrypoint;
18871931
if (!(entrypoints >> entrypoint)) {
18881932
break;
18891933
}
18901934

1891-
if (child_process.size() == PROCESS) {
1892-
wait(NULL);
1935+
if (child_processes.size() == PROCESS) {
1936+
if (TimeoutPerFunction != 0) {
1937+
wait_until_any_child_dies(child_processes);
1938+
} else {
1939+
wait(NULL);
1940+
}
18931941
}
18941942

1895-
std::vector<pid_t> alive_child;
1896-
for (const pid_t child_id : child_process) {
1897-
if (kill(child_id, 0) == 0) {
1898-
alive_child.push_back(child_id);
1943+
std::vector<std::pair<pid_t, time_point>> alive_child;
1944+
for (const auto &child_process : child_processes) {
1945+
if (kill(child_process.first, 0) == 0) {
1946+
alive_child.push_back(child_process);
18991947
}
19001948
}
1901-
child_process = alive_child;
1949+
child_processes = alive_child;
19021950

19031951
pid_t pid = fork();
19041952
if (pid < 0) {
19051953
klee_error("%s", "Cannot create child process.");
19061954
} else if (pid == 0) {
1955+
signal(SIGCHLD, SIG_DFL);
19071956
EntryPoint = entrypoint;
19081957
SmallString<128> newOutputDirectory = outputDirectory;
19091958
sys::path::append(newOutputDirectory, entrypoint);
@@ -1912,12 +1961,25 @@ int run_klee(int argc, char **argv, char **envp) {
19121961
finalModule, replayPath, loadedModules);
19131962
exit(0);
19141963
} else {
1915-
child_process.push_back(pid);
1964+
child_processes.emplace_back(pid, std::chrono::steady_clock::now());
19161965
}
19171966
}
19181967

1919-
while (wait(NULL) > 0)
1920-
;
1968+
if (TimeoutPerFunction != 0) {
1969+
while (!child_processes.empty()) {
1970+
wait_until_any_child_dies(child_processes);
1971+
1972+
std::vector<std::pair<pid_t, time_point>> alive_child;
1973+
for (const auto &child_process : child_processes) {
1974+
if (kill(child_process.first, 0) == 0) {
1975+
alive_child.push_back(child_process);
1976+
}
1977+
}
1978+
child_processes = alive_child;
1979+
}
1980+
} else {
1981+
while (wait(NULL) > 0);
1982+
}
19211983
} else {
19221984
run_klee_on_function(pArgc, pArgv, pEnvp, handler, interpreter, finalModule,
19231985
replayPath, loadedModules);
Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
2+
// RUN: rm -rf %t.klee-out %t.entrypoints
3+
// RUN: echo sign_sum >> %t.entrypoints
4+
// RUN: echo comparison >> %t.entrypoints
5+
// RUN: echo segment_intersection >> %t.entrypoints
6+
// RUN: echo main >> %t.entrypoints
7+
// RUN: %klee --output-dir=%t.klee-out --entry-point=main --interactive --entrypoints-file=%t.entrypoints %t.bc
8+
9+
// RUN: test -f %t.klee-out/sign_sum/test000001.ktestjson
10+
// RUN: test -f %t.klee-out/sign_sum/test000002.ktestjson
11+
// RUN: test -f %t.klee-out/sign_sum/test000003.ktestjson
12+
// RUN: not test -f %t.klee-out/sign_sum/test000004.ktestjson
13+
14+
// RUN: test -f %t.klee-out/comparison/test000001.ktestjson
15+
// RUN: test -f %t.klee-out/comparison/test000002.ktestjson
16+
// RUN: not test -f %t.klee-out/comparison/test000003.ktestjson
17+
18+
// RUN: test -f %t.klee-out/segment_intersection/test000001.ktestjson
19+
// RUN: test -f %t.klee-out/segment_intersection/test000002.ktestjson
20+
// RUN: test -f %t.klee-out/segment_intersection/test000003.ktestjson
21+
// RUN: test -f %t.klee-out/segment_intersection/test000004.ktestjson
22+
// RUN: test -f %t.klee-out/segment_intersection/test000005.ktestjson
23+
// RUN: test -f %t.klee-out/segment_intersection/test000006.ktestjson
24+
// RUN: test -f %t.klee-out/segment_intersection/test000007.ktestjson
25+
// RUN: test -f %t.klee-out/segment_intersection/test000008.ktestjson
26+
// RUN: test -f %t.klee-out/segment_intersection/test000009.ktestjson
27+
// RUN: not test -f %t.klee-out/segment_intersection/test000010.ktestjson
28+
29+
// RUN: test -f %t.klee-out/main/test000001.ktestjson
30+
// RUN: not test -f %t.klee-out/main/test000002.ktestjson
31+
32+
#include "klee/klee.h"
33+
#include <stdio.h>
34+
35+
int sign_sum() {
36+
int x, y;
37+
klee_make_symbolic(&x, sizeof(int), "x");
38+
klee_make_symbolic(&y, sizeof(int), "y");
39+
40+
int c = 0;
41+
if (x + y > 0) {
42+
c = 1;
43+
} else if (x + y < 0) {
44+
c = -1;
45+
} else {
46+
c = 0;
47+
}
48+
return 0;
49+
}
50+
51+
int comparison() {
52+
int x, y;
53+
klee_make_symbolic(&x, sizeof(int), "x");
54+
klee_make_symbolic(&y, sizeof(int), "y");
55+
56+
if (x < y) {
57+
return 1;
58+
} else {
59+
return 0;
60+
}
61+
}
62+
63+
int segment_intersection() {
64+
int l, r, A, B;
65+
klee_make_symbolic(&l, sizeof(int), "l");
66+
klee_make_symbolic(&r, sizeof(int), "r");
67+
klee_make_symbolic(&A, sizeof(int), "A");
68+
klee_make_symbolic(&B, sizeof(int), "B");
69+
70+
if (l > r || A > B) {
71+
return -1;
72+
}
73+
74+
if (l > B || r < A) {
75+
return 0;
76+
}
77+
78+
if (A <= l && r <= B) {
79+
return r - l;
80+
}
81+
82+
if (l <= A && B <= r) {
83+
return B - A;
84+
}
85+
86+
return (r <= B ? r : B) - (l >= A ? l : A);
87+
}
88+
89+
int main() {
90+
return 0;
91+
}
92+

0 commit comments

Comments
 (0)