Skip to content

Commit

Permalink
Add support stdin/stdout with interactive mode
Browse files Browse the repository at this point in the history
Implement getc, fgetc, fread, fgets, getchar, gets, putc, fputc, fwrite, fputs, putchar, puts
  • Loading branch information
Saveliy Grigoryev authored and ladisgin committed Jul 15, 2022
1 parent 73701e2 commit bb1f597
Show file tree
Hide file tree
Showing 20 changed files with 556 additions and 8 deletions.
4 changes: 4 additions & 0 deletions include/klee/klee.h
Original file line number Diff line number Diff line change
Expand Up @@ -209,4 +209,8 @@ long double klee_rintl(long double d);
}
#endif

//UTBot uses these functions to wrap user functions which work with stdin/stdout
void klee_init_env(int *argcPtr, char ***argvPtr);
void check_stdin_read();

#endif /* KLEE_H */
20 changes: 18 additions & 2 deletions lib/Runner/run_klee.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -147,6 +147,9 @@ cl::opt<std::string>
cl::desc("Function in which to start execution (default=main)"),
cl::init("main"), cl::cat(StartCat));

cl::opt<bool> UTBotMode("utbot", cl::desc("Klee was launched by utbot"),
cl::init(false), cl::cat(StartCat));

cl::opt<bool> InteractiveMode("interactive",
cl::desc("Launch klee in interactive mode."),
cl::init(false), cl::cat(StartCat));
Expand Down Expand Up @@ -1761,8 +1764,21 @@ int run_klee(int argc, char **argv, char **envp) {
klee_error("error loading POSIX support '%s': %s", Path.c_str(),
errorMsg.c_str());

std::string libcPrefix = (Libc == LibcType::UcLibc ? "__user_" : "");
preparePOSIX(loadedModules, libcPrefix);
if (Libc != LibcType::UcLibc) {
SmallString<128> Path_io(Opts.LibraryDir);
llvm::sys::path::append(Path_io, "libkleeRuntimeIO_C" + opt_suffix + ".bca");
klee_message("NOTE: using klee versions of input/output functions: %s",
Path_io.c_str());
if (!klee::loadFile(Path_io.c_str(), mainModule->getContext(), loadedModules,
errorMsg))
klee_error("error loading POSIX_IO support '%s': %s", Path_io.c_str(),
errorMsg.c_str());
}

if (!UTBotMode) {
std::string libcPrefix = (Libc == LibcType::UcLibc ? "__user_" : "");
preparePOSIX(loadedModules, libcPrefix);
}
}

if (WithFPRuntime) {
Expand Down
2 changes: 1 addition & 1 deletion runtime/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ if (ENABLE_KLEE_EH_CXX)
endif ()

if (ENABLE_POSIX_RUNTIME)
list(APPEND RUNTIME_LIBRARIES RuntimePOSIX)
list(APPEND RUNTIME_LIBRARIES "RuntimePOSIX;RuntimeIO_C")
add_subdirectory(POSIX)
endif ()

Expand Down
5 changes: 4 additions & 1 deletion runtime/POSIX/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -23,4 +23,7 @@ set(SRC_FILES
# Build it
include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake")
prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" prefixed_files)
add_bitcode_library_targets("${LIB_PREFIX}" "${prefixed_files}" "-std=gnu89" "")
add_bitcode_library_targets("${LIB_PREFIX}" "${prefixed_files}" "-std=gnu89" "")

prefix_with_path(input_output.c "${CMAKE_CURRENT_SOURCE_DIR}/" io_file)
add_bitcode_library_targets("RuntimeIO_C" "${io_file}" "-std=gnu89" "")
2 changes: 0 additions & 2 deletions runtime/POSIX/fd.c
Original file line number Diff line number Diff line change
Expand Up @@ -408,7 +408,6 @@ ssize_t read(int fd, void *buf, size_t count) {
}
}


ssize_t write(int fd, const void *buf, size_t count) {
static int n_calls = 0;
exe_file_t *f;
Expand Down Expand Up @@ -481,7 +480,6 @@ ssize_t write(int fd, const void *buf, size_t count) {
}
}


off64_t __fd_lseek(int fd, off64_t offset, int whence) {
off64_t new_off;
exe_file_t *f = __get_file(fd);
Expand Down
139 changes: 139 additions & 0 deletions runtime/POSIX/input_output.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,139 @@
#include <stdio.h>

int fgetc(FILE *stream) {
int fd = fileno(stream);
unsigned char buf;
ssize_t read_byte = read(fd, &buf, 1);
if (read_byte == 1) {
return buf;
} else {
return EOF;
}
}

int getc(FILE *stream) {
int fd = fileno(stream);
unsigned char buf;
ssize_t read_byte = read(fd, &buf, 1);
if (read_byte == 1) {
return buf;
} else {
return EOF;
}
}

size_t fread(void *buffer, size_t size, size_t count, FILE *stream) {
int fd = fileno(stream);
ssize_t read_byte = read(fd, buffer, size * count);
if (read_byte == -1) {
return 0;
}
return read_byte / size;
}

char* fgets(char *s, int n, FILE *stream)
{
char *p = s;
if (s == NULL || n <= 0 || ferror(stream) || feof(stream)) {
return NULL;
}

int c = 0;
while (--n > 0 && (c = getc(stream)) != EOF) {
if ((*p++ = c) == '\n') {
break;
}
}
if (ferror(stream) || (c == EOF && p == s)) {
return NULL;
}
*p = '\0';
return s;
}

int getchar(void) {
return getc(stdin);
}

char* gets(char *s)
{
char *p = s;
if (s == NULL || ferror(stdin) || feof(stdin)) {
return NULL;
}

int c = 0;
while ((c = getchar()) != EOF) {
if (c == '\n') {
break;
}
*p++ = c;
}
if (ferror(stdin) || (c == EOF && p == s)) {
return NULL;
}
*p = '\0';
return s;
}

int fputc(int c, FILE *stream) {
int fd = fileno(stream);
unsigned char symb = c;
int write_byte = write(fd, &symb, 1);
if (write_byte == 1) {
return c;
} else {
return EOF;
}
}

int putc(int c, FILE *stream) {
int fd = fileno(stream);
unsigned char symb = c;
int write_byte = write(fd, &symb, 1);
if (write_byte == 1) {
return c;
} else {
return EOF;
}
}

size_t fwrite(const void *buffer, size_t size, size_t count, FILE *stream) {
int fd = fileno(stream);
void *cop_buf = buffer;
int write_byte = write(fd, cop_buf, size * count);
if (write == -1) {
return 0;
}
return write_byte / size;
}

int fputs(const char *str, FILE *stream) {
if (str == NULL) {
return EOF;
}

while (*str != '\0') {
unsigned char c = *str;
fputc(c, stream);
str++;
}

return 1;
}

int putchar(int c) {
return putc(c, stdout);
}

int puts(const char *str) {
int write_code = fputs(str, stdout);
if (write_code == EOF) {
return EOF;
}
write_code = putchar('\n');
if (write_code == EOF) {
return EOF;
}
return 1;
}
6 changes: 5 additions & 1 deletion runtime/POSIX/klee_init_env.c
Original file line number Diff line number Diff line change
Expand Up @@ -239,10 +239,14 @@ usage: (klee_init_env) [options] [program arguments]\n\
* and is renamed during POSIX setup */
int __klee_posix_wrapped_main(int argc, char **argv, char **envp);

void check_stdin_read() {
klee_assume(__exe_env.stdin_off == __exe_env.max_off);
}

/* This wrapper gets called instead of main if POSIX setup is used */
int __klee_posix_wrapper(int argcPtr, char **argvPtr, char** envp) {
klee_init_env(&argcPtr, &argvPtr);
int res = __klee_posix_wrapped_main(argcPtr, argvPtr, envp);
klee_assume(__exe_env.stdin_off == __exe_env.max_off);
check_stdin_read();
return res;
}
2 changes: 1 addition & 1 deletion runtime/klee-libc/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ set(SRC_FILES
htonl.c
memchr.c
mempcpy.c
putchar.c
# putchar.c
stpcpy.c
strcat.c
strchr.c
Expand Down
43 changes: 43 additions & 0 deletions test/Runtime/POSIX/fgetc_example.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-stdin 64
// RUN: test -f %t.klee-out/test000001.ktestjson
// RUN: test -f %t.klee-out/test000002.ktestjson
// RUN: test -f %t.klee-out/test000003.ktestjson
// RUN: test -f %t.klee-out/test000004.ktestjson
// RUN: test -f %t.klee-out/test000005.ktestjson
// RUN: test -f %t.klee-out/test000006.ktestjson
// RUN: test -f %t.klee-out/test000007.ktestjson
// RUN: test -f %t.klee-out/test000008.ktestjson
// RUN: test -f %t.klee-out/test000009.ktestjson
// RUN: test -f %t.klee-out/test000010.ktestjson
// RUN: test -f %t.klee-out/test000011.ktestjson
// RUN: test -f %t.klee-out/test000012.ktestjson
// RUN: test -f %t.klee-out/test000013.ktestjson
// RUN: not test -f %t.klee-out/test000014.ktestjson

#include <stdio.h>

int main() {
unsigned char x = fgetc(stdin);
if (x >= '0' && x <= '9') {
unsigned char a = fgetc(stdin);
if (a >= 'a' && a <= 'z') {
return 1;
} else {
return 2;
}
} else {
unsigned char a = fgetc(stdin);
unsigned char b = fgetc(stdin);
if (a >= 'a' && a <= 'z') {
if (b >= '0' && b <= '9') {
return 3;
} else {
return 4;
}
} else {
return 5;
}
}
}
36 changes: 36 additions & 0 deletions test/Runtime/POSIX/fgets_example.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-stdin 64
// RUN: test -f %t.klee-out/test000001.ktestjson
// RUN: test -f %t.klee-out/test000002.ktestjson
// RUN: test -f %t.klee-out/test000003.ktestjson
// RUN: test -f %t.klee-out/test000004.ktestjson
// RUN: test -f %t.klee-out/test000005.ktestjson
// RUN: test -f %t.klee-out/test000006.ktestjson
// RUN: test -f %t.klee-out/test000007.ktestjson
// RUN: test -f %t.klee-out/test000008.ktestjson
// RUN: test -f %t.klee-out/test000009.ktestjson
// RUN: test -f %t.klee-out/test000010.ktestjson
// RUN: test -f %t.klee-out/test000011.ktestjson
// RUN: test -f %t.klee-out/test000012.ktestjson
// RUN: test -f %t.klee-out/test000013.ktestjson
// RUN: test -f %t.klee-out/test000014.ktestjson
// RUN: test -f %t.klee-out/test000015.ktestjson
// RUN: test -f %t.klee-out/test000016.ktestjson
// RUN: test -f %t.klee-out/test000017.ktestjson
// RUN: test -f %t.klee-out/test000018.ktestjson
// RUN: test -f %t.klee-out/test000019.ktestjson
// RUN: test -f %t.klee-out/test000020.ktestjson
// RUN: test -f %t.klee-out/test000021.ktestjson
// RUN: not test -f %t.klee-out/test000022.ktestjson

#include <stdio.h>

int main() {
char a[8];
fgets(a, 6, stdin);
if (a[0] == 'u' && a[1] == 't' && a[2] == 'b' && a[3] == 'o' && a[4] == 't') {
return 1;
}
return 0;
}
31 changes: 31 additions & 0 deletions test/Runtime/POSIX/fputc_example.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-stdin 64
// RUN: test -f %t.klee-out/test000001.ktestjson
// RUN: test -f %t.klee-out/test000002.ktestjson
// RUN: test -f %t.klee-out/test000003.ktestjson
// RUN: not test -f %t.klee-out/test000004.ktestjson

#include "klee/klee.h"
#include <stdio.h>

char simple_fputc(int x, int y) {
if (x < y) {
fputc('<', stdout);
return '<';
} else if (x > y) {
fputc('>', stdout);
return '>';
} else {
fputc('=', stdout);
return '=';
}
}

int main() {
int x, y;
klee_make_symbolic(&x, sizeof(int), "x");
klee_make_symbolic(&y, sizeof(int), "y");
char c = simple_fputc(x, y);
return 0;
}
32 changes: 32 additions & 0 deletions test/Runtime/POSIX/fputs_example.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
// RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-stdin 64
// RUN: test -f %t.klee-out/test000001.ktestjson
// RUN: test -f %t.klee-out/test000002.ktestjson
// RUN: test -f %t.klee-out/test000003.ktestjson
// RUN: test -f %t.klee-out/test000004.ktestjson
// RUN: test -f %t.klee-out/test000005.ktestjson
// RUN: test -f %t.klee-out/test000006.ktestjson
// RUN: not test -f %t.klee-out/test000007.ktestjson

#include "klee/klee.h"
#include <stdio.h>

char simple_fputs(char c) {
if (c == 'a' || c == 'e' || c == 'i' || c == 'o' || c == 'u') {
char a[] = "Vowel";
fputs("Vowel", stdout);
return 'V';
} else {
char a[] = "Consonant";
fputs("Consonant", stdout);
return 'C';
}
}

int main() {
char c;
klee_make_symbolic(&c, sizeof(char), "c");
char d = simple_fputs(c);
return 0;
}
Loading

0 comments on commit bb1f597

Please sign in to comment.