diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index 9932e4de62..2e531d15da 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -146,7 +146,6 @@ jobs: runs-on: macos-latest env: BASE: /tmp - LLVM_VERSION: 11 SOLVERS: STP UCLIBC_VERSION: 0 USE_TCMALLOC: 0 diff --git a/configs/annotations.json b/configs/annotations.json new file mode 100644 index 0000000000..685f60c2a6 --- /dev/null +++ b/configs/annotations.json @@ -0,0 +1,2027 @@ +{ + "atof": { + "name": "atof", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "atoi": { + "name": "atoi", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "atol": { + "name": "atol", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "atoll": { + "name": "atoll", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "bcmp": { + "name": "bcmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "calloc": { + "name": "calloc", + "annotation": [ + [ + "AllocSource::1", + "InitNull" + ], + [], + [] + ], + "properties": [] + }, + "fclose": { + "name": "fclose", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fcvt": { + "name": "fcvt", + "annotation": [ + [], + [], + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "feof": { + "name": "feof", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "ferror": { + "name": "ferror", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fgetc": { + "name": "fgetc", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fgetpos": { + "name": "fgetpos", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "fgetpos64": { + "name": "fgetpos64", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "fgets": { + "name": "fgets", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fgetwc": { + "name": "fgetwc", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fgetws": { + "name": "fgetws", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fileno": { + "name": "fileno", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fopen": { + "name": "fopen", + "annotation": [ + [ + "InitNull" + ], + [], + [] + ], + "properties": [] + }, + "fopen64": { + "name": "fopen64", + "annotation": [ + [ + "InitNull" + ], + [], + [] + ], + "properties": [] + }, + "fopen_s": { + "name": "fopen_s", + "annotation": [ + [], + [ + "InitNull:*:!=0" + ], + [], + [ + "FreeSink::4" + ] + ], + "properties": [] + }, + "fprintf": { + "name": "fprintf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "fputc": { + "name": "fputc", + "annotation": [ + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fputs": { + "name": "fputs", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "fputwc": { + "name": "fputwc", + "annotation": [ + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fputws": { + "name": "fputws", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "fread": { + "name": "fread", + "annotation": [ + [], + [ + "Deref" + ], + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "free": { + "name": "free", + "annotation": [ + [], + [ + "FreeSink::1" + ] + ], + "properties": [] + }, + "freopen": { + "name": "freopen", + "annotation": [ + [ + "InitNull" + ], + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "freopen64": { + "name": "freopen64", + "annotation": [ + [ + "InitNull" + ], + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "freopen_s": { + "name": "freopen_s", + "annotation": [ + [], + [ + "InitNull:*:!=0" + ], + [], + [], + [ + "FreeSink::4" + ] + ], + "properties": [] + }, + "fscanf": { + "name": "fscanf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "fscanf_s": { + "name": "fscanf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "fseek": { + "name": "fseek", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "fsetpos": { + "name": "fsetpos", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "fsetpos64": { + "name": "fsetpos64", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "ftell": { + "name": "ftell", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fwide": { + "name": "fwide", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "fwprintf": { + "name": "fwprintf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "fwrite": { + "name": "fwrite", + "annotation": [ + [], + [ + "Deref" + ], + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "fwscanf": { + "name": "fwscanf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "getc": { + "name": "getc", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "getenv": { + "name": "getenv", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "getenv_s": { + "name": "getenv_s", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "gets": { + "name": "gets", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "gets_s": { + "name": "gets_s", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "getw": { + "name": "getw", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "getwc": { + "name": "getwc", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "itoa": { + "name": "itoa", + "annotation": [ + [], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "localtime": { + "name": "localtime", + "annotation": [ + [ + "InitNull::Must" + ], + [] + ], + "properties": [] + }, + "malloc": { + "name": "malloc", + "annotation": [ + [ + "AllocSource::1", + "InitNull" + ], + [] + ], + "properties": [] + }, + "memccpy": { + "name": "memccpy", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "memchr": { + "name": "memchr", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "memcmp": { + "name": "memcmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "memcpy": { + "name": "memcpy", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "memcpy_s": { + "name": "memcpy_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "memicmp": { + "name": "memicmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "memmem": { + "name": "memmem", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "memmove": { + "name": "memmove", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "memmove_s": { + "name": "memmove_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "mempcpy": { + "name": "mempcpy", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "memset": { + "name": "memset", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "memset_s": { + "name": "memset_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [], + [] + ], + "properties": [] + }, + "pthread_mutex_lock": { + "name": "pthread_mutex_lock", + "annotation": [ + [], + [ + "InitNull::!=0" + ] + ], + "properties": [] + }, + "pthread_mutex_trylock": { + "name": "pthread_mutex_trylock", + "annotation": [ + [], + [ + "InitNull::!=0" + ] + ], + "properties": [] + }, + "putc": { + "name": "putc", + "annotation": [ + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "puts": { + "name": "puts", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "qsort": { + "name": "qsort", + "annotation": [ + [], + [ + "Deref" + ], + [], + [], + [] + ], + "properties": [] + }, + "rawmemchr": { + "name": "rawmemchr", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "realloc": { + "name": "realloc", + "annotation": [ + [ + "AllocSource::1", + "InitNull" + ], + [], + [] + ], + "properties": [] + }, + "setbuf": { + "name": "setbuf", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "setlocale": { + "name": "setlocale", + "annotation": [ + [ + "InitNull" + ], + [], + [] + ], + "properties": [] + }, + "snprintf": { + "name": "snprintf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "snprintf_s": { + "name": "snprintf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "snwprintf": { + "name": "snwprintf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "sprintf": { + "name": "sprintf", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "sprintf_s": { + "name": "sprintf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "sscanf": { + "name": "sscanf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "sscanf_s": { + "name": "sscanf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [], + [] + ], + "properties": [] + }, + "std::from_chars": { + "name": "std::from_chars", + "annotation": [ + [], + [ + "Deref" + ], + [], + [], + [] + ], + "properties": [] + }, + "std::to_chars": { + "name": "std::to_chars", + "annotation": [ + [], + [ + "Deref" + ], + [], + [], + [] + ], + "properties": [] + }, + "stpcpy": { + "name": "stpcpy", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strcat": { + "name": "strcat", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "strcat_s": { + "name": "strcat_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "strchr": { + "name": "strchr", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strchrnul": { + "name": "strchrnul", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strcmp": { + "name": "strcmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "strcpy": { + "name": "strcpy", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "strcpy_s": { + "name": "strcpy_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "strdup": { + "name": "strdup", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "strlen": { + "name": "strlen", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "strncasecmp": { + "name": "strncasecmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strncat": { + "name": "strncat", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strncat_s": { + "name": "strncat_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strncmp": { + "name": "strncmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strncpy": { + "name": "strncpy", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strncpy_s": { + "name": "strncpy_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strndup": { + "name": "strndup", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "strnlen": { + "name": "strnlen", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "strnset": { + "name": "strnset", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strpbrk": { + "name": "strpbrk", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strrchr": { + "name": "strrchr", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strset": { + "name": "strset", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "strspn": { + "name": "strspn", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "strstr": { + "name": "strstr", + "annotation": [ + [ + "InitNull" + ], + [], + [] + ], + "properties": [] + }, + "strtod": { + "name": "strtod", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strtol": { + "name": "strtol", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "strtold": { + "name": "strtold", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "strtoll": { + "name": "strtoll", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "strtoul": { + "name": "strtoul", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "strtoull": { + "name": "strtoull", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "strxfrm": { + "name": "strxfrm", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "swprintf": { + "name": "swprintf", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "swprintf_s": { + "name": "swprintf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "swscanf": { + "name": "swscanf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "swscanf_s": { + "name": "swscanf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [], + [] + ], + "properties": [] + }, + "tmpnam": { + "name": "tmpnam", + "annotation": [ + [ + "InitNull" + ], + [] + ], + "properties": [] + }, + "vfprintf_s": { + "name": "vfprintf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "vfscanf": { + "name": "vfscanf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "vfwprintf": { + "name": "vfwprintf", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "vfwprintf_s": { + "name": "vfwprintf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "vfwscanf": { + "name": "vfwscanf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "vsnprintf_s": { + "name": "vsnprintf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [], + [] + ], + "properties": [] + }, + "vsnwprintf": { + "name": "vsnwprintf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "vsprintf": { + "name": "vsprintf", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "vsprintf_s": { + "name": "vsprintf_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "vsscanf": { + "name": "vsscanf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "vswscanf": { + "name": "vswscanf", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcscat": { + "name": "wcscat", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcscat_s": { + "name": "wcscat_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcschr": { + "name": "wcschr", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcschrnul": { + "name": "wcschrnul", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcscmp": { + "name": "wcscmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcscoll": { + "name": "wcscoll", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcscpy": { + "name": "wcscpy", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcscpy_s": { + "name": "wcscpy_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcscspn": { + "name": "wcscspn", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcsftime": { + "name": "wcsftime", + "annotation": [ + [], + [], + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcsncasecmp": { + "name": "wcsncasecmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcsncat": { + "name": "wcsncat", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcsncat_s": { + "name": "wcsncat_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcsncmp": { + "name": "wcsncmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcsncpy": { + "name": "wcsncpy", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcsncpy_s": { + "name": "wcsncpy_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcspbrk": { + "name": "wcspbrk", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcsrchr": { + "name": "wcsrchr", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcsspn": { + "name": "wcsspn", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcsstr": { + "name": "wcsstr", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + }, + "wcstol": { + "name": "wcstol", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "wcstold": { + "name": "wcstold", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wcstoll": { + "name": "wcstoll", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "wcstoul": { + "name": "wcstoul", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "wcstoull": { + "name": "wcstoull", + "annotation": [ + [], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "wcsxfrm": { + "name": "wcsxfrm", + "annotation": [ + [], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wctrans": { + "name": "wctrans", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "wctype": { + "name": "wctype", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "wmemchr": { + "name": "wmemchr", + "annotation": [ + [ + "InitNull" + ], + [ + "Deref" + ], + [], + [] + ], + "properties": [] + }, + "wmemcmp": { + "name": "wmemcmp", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wmemcpy": { + "name": "wmemcpy", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wmemcpy_s": { + "name": "wmemcpy_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wmemmove": { + "name": "wmemmove", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wmemmove_s": { + "name": "wmemmove_s", + "annotation": [ + [], + [ + "Deref" + ], + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "wmempcpy": { + "name": "wmempcpy", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ], + [] + ], + "properties": [] + } +} diff --git a/configs/options.json b/configs/options.json index 32f20ebbf7..e89988448a 100644 --- a/configs/options.json +++ b/configs/options.json @@ -18,13 +18,13 @@ "program": "${buildPath}/bin/klee", "args": [ "--use-guided-search=error", - "--mock-external-calls", "--posix-runtime", "--check-out-of-memory", "--suppress-external-warnings", "--libc=klee", "--skip-not-lazy-initialized", "--external-calls=all", + "--mock-policy=all", "--output-source=false", "--output-istats=false", "--output-stats=false", @@ -32,7 +32,6 @@ "--max-sym-alloc=${maxSymAlloc}", "--max-forks=${maxForks}", "--max-solver-time=${maxSolverTime}s", - "--mock-all-externals", "--smart-resolve-entry-function", "--extern-calls-can-return-null", "--align-symbolic-pointers=false", @@ -49,4 +48,4 @@ ] } ] -} \ No newline at end of file +} diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index 5a619c6e29..04eec908de 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -65,11 +65,21 @@ using FLCtoOpcode = std::unordered_map< std::unordered_map< unsigned, std::unordered_map>>>; -enum class MockStrategy { - None, // No mocks are generated - Naive, // For each function call new symbolic value is generated - Deterministic, // Each function is treated as uninterpreted function in SMT. - // Compatible with Z3 solver only +enum class MockStrategyKind { + Naive, // For each function call new symbolic value is generated + Deterministic // Each function is treated as uninterpreted function in SMT. + // Compatible with Z3 solver only +}; + +enum class MockPolicy { + None, // No mock function generated + Failed, // Generate symbolic value for failed external calls + All // Generate IR module with all external values +}; + +enum class MockMutableGlobalsPolicy { + None, // No mock for globals + All, // Mock globals on module build stage and generate bc module for it }; class Interpreter { @@ -90,25 +100,31 @@ class Interpreter { std::string OptSuffix; std::string MainCurrentName; std::string MainNameAfterMock; + std::string AnnotationsFile; bool Optimize; bool Simplify; bool CheckDivZero; bool CheckOvershift; + bool AnnotateOnlyExternal; bool WithFPRuntime; bool WithPOSIXRuntime; ModuleOptions(const std::string &_LibraryDir, const std::string &_EntryPoint, const std::string &_OptSuffix, const std::string &_MainCurrentName, - const std::string &_MainNameAfterMock, bool _Optimize, + const std::string &_MainNameAfterMock, + const std::string &_AnnotationsFile, bool _Optimize, bool _Simplify, bool _CheckDivZero, bool _CheckOvershift, - bool _WithFPRuntime, bool _WithPOSIXRuntime) + bool _AnnotateOnlyExternal, bool _WithFPRuntime, + bool _WithPOSIXRuntime) : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName), - MainNameAfterMock(_MainNameAfterMock), Optimize(_Optimize), + MainNameAfterMock(_MainNameAfterMock), + AnnotationsFile(_AnnotationsFile), Optimize(_Optimize), Simplify(_Simplify), CheckDivZero(_CheckDivZero), - CheckOvershift(_CheckOvershift), WithFPRuntime(_WithFPRuntime), - WithPOSIXRuntime(_WithPOSIXRuntime) {} + CheckOvershift(_CheckOvershift), + AnnotateOnlyExternal(_AnnotateOnlyExternal), + WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {} }; enum LogType { @@ -126,11 +142,15 @@ class Interpreter { unsigned MakeConcreteSymbolic; GuidanceKind Guidance; std::optional Paths; - enum MockStrategy MockStrategy; + MockPolicy Mock; + MockStrategyKind MockStrategy; + MockMutableGlobalsPolicy MockMutableGlobals; InterpreterOptions(std::optional Paths) : MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance), - Paths(std::move(Paths)), MockStrategy(MockStrategy::None) {} + Paths(std::move(Paths)), Mock(MockPolicy::None), + MockStrategy(MockStrategyKind::Naive), + MockMutableGlobals(MockMutableGlobalsPolicy::None) {} }; protected: @@ -153,18 +173,13 @@ class Interpreter { /// module /// \return The final module after it has been optimized, checks /// inserted, and modified for interpretation. - virtual llvm::Module * - setModule(std::vector> &userModules, - std::vector> &libsModules, - const ModuleOptions &opts, - std::set &&mainModuleFunctions, - std::set &&mainModuleGlobals, - FLCtoOpcode &&origInstructions, - const std::set &ignoredExternals, - const Annotations &annotations) = 0; - - virtual std::map - getAllExternals(const std::set &ignoredExternals) = 0; + virtual llvm::Module *setModule( + std::vector> &userModules, + std::vector> &libsModules, + const ModuleOptions &opts, std::set &&mainModuleFunctions, + std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, + const std::set &ignoredExternals, + std::vector> redefinitions) = 0; // supply a tree stream writer which the interpreter will use // to record the concrete path (as a stream of '0' and '1' bytes). diff --git a/include/klee/Core/MockBuilder.h b/include/klee/Core/MockBuilder.h index 0ff22bd890..da5d0ea198 100644 --- a/include/klee/Core/MockBuilder.h +++ b/include/klee/Core/MockBuilder.h @@ -1,6 +1,15 @@ +//===-- MockBuilder.h -------------------------------------------*- C++ -*-===// +// +// The KLEEF Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +//===----------------------------------------------------------------------===// + #ifndef KLEE_MOCKBUILDER_H #define KLEE_MOCKBUILDER_H +#include "klee/Core/Interpreter.h" #include "klee/Module/Annotation.h" #include "llvm/IR/IRBuilder.h" @@ -14,32 +23,63 @@ namespace klee { class MockBuilder { private: const llvm::Module *userModule; + llvm::LLVMContext &ctx; std::unique_ptr mockModule; std::unique_ptr> builder; - std::map externals; - Annotations annotations; - const std::string mockEntrypoint, userEntrypoint; + const Interpreter::ModuleOptions &opts; + const Interpreter::InterpreterOptions &interpreterOptions; + + std::set ignoredExternals; + std::vector> redefinitions; + + InterpreterHandler *interpreterHandler; + + std::set &mainModuleFunctions; + std::set &mainModuleGlobals; + + AnnotationsMap annotations; void initMockModule(); void buildMockMain(); void buildExternalGlobalsDefinitions(); void buildExternalFunctionsDefinitions(); - void buildCallKleeMakeSymbol(const std::string &klee_function_name, - llvm::Value *source, llvm::Type *type, - const std::string &symbol_name); - void buildAnnotationForExternalFunctionParams(llvm::Function *func, - Annotation &annotation); - llvm::Value *goByOffset(llvm::Value *value, - const std::vector &offset); + void + buildCallKleeMakeSymbolic(const std::string &kleeMakeSymbolicFunctionName, + llvm::Value *source, llvm::Type *type, + const std::string &symbolicName); + + void buildAnnotationForExternalFunctionArgs( + llvm::Function *func, + const std::vector> &statementsNotAllign); + void buildAnnotationForExternalFunctionReturn( + llvm::Function *func, const std::vector &statements); + void buildAnnotationForExternalFunctionProperties( + llvm::Function *func, const std::set &properties); + + std::map getExternalFunctions(); + std::map getExternalGlobals(); + + std::pair + goByOffset(llvm::Value *value, const std::vector &offset); public: - MockBuilder(const llvm::Module *initModule, std::string mockEntrypoint, - std::string userEntrypoint, - std::map externals, - Annotations annotations); + MockBuilder(const llvm::Module *initModule, + const Interpreter::ModuleOptions &opts, + const Interpreter::InterpreterOptions &interpreterOptions, + const std::set &ignoredExternals, + std::vector> &redefinitions, + InterpreterHandler *interpreterHandler, + std::set &mainModuleFunctions, + std::set &mainModuleGlobals); std::unique_ptr build(); + void buildAllocSource(llvm::Value *prev, llvm::Type *elemType, + const Statement::Alloc *allocSourcePtr); + void buildFree(llvm::Value *elem, const Statement::Free *freePtr); + void processingValue(llvm::Value *prev, llvm::Type *elemType, + const Statement::Alloc *allocSourcePtr, + bool initNullPtr); }; } // namespace klee diff --git a/include/klee/Expr/AlphaBuilder.h b/include/klee/Expr/AlphaBuilder.h index 6a965c3962..cc481f8f69 100644 --- a/include/klee/Expr/AlphaBuilder.h +++ b/include/klee/Expr/AlphaBuilder.h @@ -34,7 +34,7 @@ class AlphaBuilder final : public ExprVisitor { public: AlphaBuilder(ArrayCache &_arrayCache); - constraints_ty visitConstraints(constraints_ty cs); + constraints_ty visitConstraints(const constraints_ty &cs); ref build(ref v); const Array *buildArray(const Array *arr) { return visitArray(arr); } ref reverseBuild(ref v); diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h index c2aeb7173f..af84a4dd8a 100644 --- a/include/klee/Expr/IndependentSet.h +++ b/include/klee/Expr/IndependentSet.h @@ -120,6 +120,8 @@ class IndependentConstraintSet { std::shared_ptr concretizedSets; + std::set uninterpretedFunctions; + ref addExpr(ref e) const; ref updateConcretization(const Assignment &delta, diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index 20eea0b49a..1a353901e0 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -3,8 +3,6 @@ #include "klee/Expr/SymbolicSource.h" -#include "llvm/IR/Function.h" - namespace klee { class KInstruction; diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index 6707ebd31c..7bdea46962 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -361,8 +361,8 @@ class AlphaSource : public SymbolicSource { const unsigned index; AlphaSource(unsigned _index) : index(_index) {} - Kind getKind() const override { return Kind::Alpha; } - virtual std::string getName() const override { return "alpha"; } + [[nodiscard]] Kind getKind() const override { return Kind::Alpha; } + [[nodiscard]] virtual std::string getName() const override { return "alpha"; } static bool classof(const SymbolicSource *S) { return S->getKind() == Kind::Alpha; @@ -408,8 +408,8 @@ class MockNaiveSource : public MockSource { unsigned _version) : MockSource(km, function), version(_version) {} - Kind getKind() const override { return Kind::MockNaive; } - std::string getName() const override { return "mockNaive"; } + [[nodiscard]] Kind getKind() const override { return Kind::MockNaive; } + [[nodiscard]] std::string getName() const override { return "mockNaive"; } static bool classof(const SymbolicSource *S) { return S->getKind() == Kind::MockNaive; @@ -417,7 +417,7 @@ class MockNaiveSource : public MockSource { unsigned computeHash() override; - int internalCompare(const SymbolicSource &b) const override; + [[nodiscard]] int internalCompare(const SymbolicSource &b) const override; }; class MockDeterministicSource : public MockSource { @@ -427,8 +427,12 @@ class MockDeterministicSource : public MockSource { MockDeterministicSource(const KModule *_km, const llvm::Function &_function, const std::vector> &_args); - Kind getKind() const override { return Kind::MockDeterministic; } - std::string getName() const override { return "mockDeterministic"; } + [[nodiscard]] Kind getKind() const override { + return Kind::MockDeterministic; + } + [[nodiscard]] std::string getName() const override { + return "mockDeterministic"; + } static bool classof(const SymbolicSource *S) { return S->getKind() == Kind::MockDeterministic; @@ -436,7 +440,7 @@ class MockDeterministicSource : public MockSource { unsigned computeHash() override; - int internalCompare(const SymbolicSource &b) const override; + [[nodiscard]] int internalCompare(const SymbolicSource &b) const override; }; } // namespace klee diff --git a/include/klee/Module/Annotation.h b/include/klee/Module/Annotation.h index 6defdd15b3..d94c591091 100644 --- a/include/klee/Module/Annotation.h +++ b/include/klee/Module/Annotation.h @@ -1,3 +1,11 @@ +//===-- Annotation.h --------------------------------------------*- C++ -*-===// +// +// The KLEEF Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +//===----------------------------------------------------------------------===// + #ifndef KLEE_ANNOTATION_H #define KLEE_ANNOTATION_H @@ -7,80 +15,126 @@ #include "vector" #include "nlohmann/json.hpp" -#include "nonstd/optional.hpp" +#include + +#include "klee/Config/config.h" + +#include "llvm/IR/Module.h" -using nonstd::nullopt; -using nonstd::optional; using json = nlohmann::json; namespace klee { -// Annotation format: https://github.com/UnitTestBot/klee/discussions/92 -struct Annotation { - enum class StatementKind { - Unknown, +namespace Statement { +enum class Kind { + Unknown, - Deref, - InitNull, - }; + Deref, + InitNull, + MaybeInitNull, + // TODO: rename to alloc + AllocSource, + Free +}; - enum class Property { - Unknown, +enum class Property { + Unknown, - Determ, - Noreturn, - }; + Deterministic, + Noreturn, +}; - struct StatementUnknown { - explicit StatementUnknown(const std::string &str); - virtual ~StatementUnknown(); +struct Unknown { +protected: + std::string rawAnnotation; + std::string rawOffset; + std::string rawValue; - virtual Annotation::StatementKind getStatementName() const; - virtual bool operator==(const StatementUnknown &other) const; +public: + std::vector offset; - std::string statementStr; - std::vector offset; + explicit Unknown(const std::string &str = "Unknown"); + virtual ~Unknown(); - protected: - void parseOffset(const std::string &offsetStr); - void parseOnlyOffset(const std::string &str); - }; + virtual bool operator==(const Unknown &other) const; + [[nodiscard]] virtual Kind getKind() const; - struct StatementDeref final : public StatementUnknown { - explicit StatementDeref(const std::string &str); + [[nodiscard]] const std::vector &getOffset() const; + [[nodiscard]] std::string toString() const; +}; - Annotation::StatementKind getStatementName() const override; - }; +struct Deref final : public Unknown { + explicit Deref(const std::string &str = "Deref"); - struct StatementInitNull final : public StatementUnknown { - explicit StatementInitNull(const std::string &str); + [[nodiscard]] Kind getKind() const override; +}; + +struct InitNull final : public Unknown { +public: + explicit InitNull(const std::string &str = "InitNull"); + + [[nodiscard]] Kind getKind() const override; +}; - Annotation::StatementKind getStatementName() const override; +struct MaybeInitNull final : public Unknown { +public: + explicit MaybeInitNull(const std::string &str = "MaybeInitNull"); + + [[nodiscard]] Kind getKind() const override; +}; + +struct Alloc final : public Unknown { +public: + enum Type { + ALLOC = 1, // malloc, calloc, realloc + NEW = 2, // operator new + NEW_BRACKETS = 3, // operator new[] + OPEN_FILE = 4, // open file (fopen, open) + MUTEX_LOCK = 5 // mutex lock (pthread_mutex_lock) }; - using StatementPtr = std::shared_ptr; - using StatementPtrs = std::vector; + Type value = Alloc::Type::ALLOC; - bool operator==(const Annotation &other) const; + explicit Alloc(const std::string &str = "AllocSource::1"); - std::string functionName; - std::vector statements; - std::set properties; + [[nodiscard]] Kind getKind() const override; }; -using Annotations = std::map; +struct Free final : public Unknown { +public: + enum Type { + FREE = 1, // Kind of free function + DELETE = 2, // operator delete + DELETE_BRACKETS = 3, // operator delete[] + CLOSE_FILE = 4, // close file + MUTEX_UNLOCK = 5 // mutex unlock (pthread_mutex_unlock) + }; + + Type value = Free::Type::FREE; + + explicit Free(const std::string &str = "FreeSource::1"); -const std::map toProperties{ - {"determ", Annotation::Property::Determ}, - {"noreturn", Annotation::Property::Noreturn}, + [[nodiscard]] Kind getKind() const override; }; -Annotations parseAnnotationsFile(const json &annotationsJson); -Annotations parseAnnotationsFile(const std::string &path); +using Ptr = std::shared_ptr; +bool operator==(const Ptr &first, const Ptr &second); +} // namespace Statement + +// Annotation format: https://github.com/UnitTestBot/klee/discussions/92 +struct Annotation { + std::string functionName; + std::vector returnStatements; + std::vector> argsStatements; + std::set properties; + + bool operator==(const Annotation &other) const; +}; -bool operator==(const Annotation::StatementPtr &first, - const Annotation::StatementPtr &second); +using AnnotationsMap = std::map; +AnnotationsMap parseAnnotationsJson(const json &annotationsJson); +AnnotationsMap parseAnnotations(const std::string &path); } // namespace klee #endif // KLEE_ANNOTATION_H diff --git a/include/klee/Module/SarifReport.h b/include/klee/Module/SarifReport.h index 72d846c90f..09652206dd 100644 --- a/include/klee/Module/SarifReport.h +++ b/include/klee/Module/SarifReport.h @@ -17,8 +17,8 @@ #include #include "klee/ADT/Ref.h" +#include "nlohmann/json.hpp" #include "llvm/IR/Function.h" -#include using json = nlohmann::json; diff --git a/include/klee/Support/OptionCategories.h b/include/klee/Support/OptionCategories.h index da1d0d4934..ed8c23c880 100644 --- a/include/klee/Support/OptionCategories.h +++ b/include/klee/Support/OptionCategories.h @@ -24,7 +24,6 @@ namespace klee { extern llvm::cl::OptionCategory TestCompCat; extern llvm::cl::OptionCategory ExecCat; extern llvm::cl::OptionCategory DebugCat; -extern llvm::cl::OptionCategory ExecCat; extern llvm::cl::OptionCategory MiscCat; extern llvm::cl::OptionCategory ModuleCat; extern llvm::cl::OptionCategory SeedingCat; diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index bf843031da..3fd5a29996 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -25,16 +25,13 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" -#include "klee/Support/ErrorHandling.h" DISABLE_WARNING_POP #include #include #include -#include #include #include -#include #include using namespace llvm; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 91a06e79ea..51e2d6f849 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -36,7 +36,6 @@ #include "klee/Core/Context.h" #include "klee/ADT/KTest.h" -#include "klee/ADT/RNG.h" #include "klee/Config/Version.h" #include "klee/Config/config.h" #include "klee/Core/Interpreter.h" @@ -183,24 +182,9 @@ cl::opt StackCopySizeMemoryCheckThreshold( "copied"), cl::cat(ExecCat)); -enum class MockMutableGlobalsPolicy { - None, - PrimitiveFields, - All, -}; +namespace { -cl::opt MockMutableGlobals( - "mock-mutable-globals", - cl::values(clEnumValN(MockMutableGlobalsPolicy::None, "none", - "No mutable global object are allowed o mock except " - "external (default)"), - clEnumValN(MockMutableGlobalsPolicy::PrimitiveFields, - "primitive-fields", - "Only primitive fileds of mutable global objects are " - "allowed to mock."), - clEnumValN(MockMutableGlobalsPolicy::All, "all", - "All mutable global object are allowed o mock.")), - cl::init(MockMutableGlobalsPolicy::None), cl::cat(ExecCat)); +/*** Lazy initialization options ***/ enum class LazyInitializationPolicy { None, @@ -229,6 +213,7 @@ llvm::cl::opt MinNumberElementsLazyInit( llvm::cl::desc("Minimum number of array elements for one lazy " "initialization (default 4)"), llvm::cl::init(4), llvm::cl::cat(LazyInitCat)); +} // namespace cl::opt FunctionCallReproduce( "function-call-reproduce", cl::init(""), @@ -350,18 +335,6 @@ cl::opt AllExternalWarnings( "as opposed to once per function (default=false)"), cl::cat(ExtCallsCat)); -cl::opt - MockExternalCalls("mock-external-calls", cl::init(false), - cl::desc("If true, failed external calls are mocked, " - "i.e. return values are made symbolic " - "and then added to generated test cases. " - "If false, fails on externall calls."), - cl::cat(ExtCallsCat)); - -cl::opt MockAllExternals("mock-all-externals", cl::init(false), - cl::desc("If true, all externals are mocked."), - cl::cat(ExtCallsCat)); - /*** Seeding options ***/ cl::opt AlwaysOutputSeeds( @@ -509,9 +482,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ih) : Interpreter(opts), interpreterHandler(ih), searcher(nullptr), externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0), - pathWriter(0), symPathWriter(0), specialFunctionHandler(0), - timers{time::Span(TimerInterval)}, guidanceKind(opts.Guidance), - codeGraphInfo(new CodeGraphInfo()), + pathWriter(0), symPathWriter(0), + specialFunctionHandler(0), timers{time::Span(TimerInterval)}, + guidanceKind(opts.Guidance), codeGraphInfo(new CodeGraphInfo()), distanceCalculator(new DistanceCalculator(*codeGraphInfo)), targetCalculator(new TargetCalculator(*codeGraphInfo)), targetManager(new TargetManager(guidanceKind, *distanceCalculator, @@ -522,10 +495,15 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, inhibitForking(false), coverOnTheFly(false), haltExecution(HaltExecution::NotHalt), ivcEnabled(false), debugLogBuffer(debugBufferString) { - if (CoreSolverToUse != Z3_SOLVER && - interpreterOpts.MockStrategy == MockStrategy::Deterministic) { + if (interpreterOpts.MockStrategy == MockStrategyKind::Deterministic && + CoreSolverToUse != Z3_SOLVER) { klee_error("Deterministic mocks can be generated with Z3 solver only.\n"); } + if (interpreterOpts.MockStrategy == MockStrategyKind::Deterministic && + interpreterOpts.Mock != MockPolicy::All) { + klee_error("Deterministic mocks can be generated only with " + "`--mock-policy=all`.\n"); + } const time::Span maxTime{MaxTime}; if (maxTime) @@ -595,21 +573,10 @@ llvm::Module *Executor::setModule( const ModuleOptions &opts, std::set &&mainModuleFunctions, std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, const std::set &ignoredExternals, - const Annotations &annotations) { + std::vector> redefinitions) { assert(!kmodule && !userModules.empty() && "can only register one module"); // XXX gross - if (ExternalCalls == ExternalCallPolicy::All && - interpreterOpts.MockStrategy != MockStrategy::None) { - llvm::Function *mainFn = - userModules.front()->getFunction(opts.MainCurrentName); - if (!mainFn) { - klee_error("Entry function '%s' not found in module.", - opts.MainCurrentName.c_str()); - } - mainFn->setName(opts.MainNameAfterMock); - } - kmodule = std::make_unique(); // 1.) Link the modules together && 2.) Apply different instrumentation @@ -634,28 +601,19 @@ llvm::Module *Executor::setModule( kmodule->instrument(opts); } - if (ExternalCalls == ExternalCallPolicy::All && - interpreterOpts.MockStrategy != MockStrategy::None) { - // TODO: move this to function - std::map externals = - getAllExternals(ignoredExternals); - MockBuilder builder(kmodule->module.get(), opts.MainCurrentName, - opts.MainNameAfterMock, externals, annotations); - std::unique_ptr mockModule = builder.build(); - if (!mockModule) { - klee_error("Unable to generate mocks"); - } - // TODO: change this to bc file - std::unique_ptr f( - interpreterHandler->openOutputFile("externals.ll")); - auto mainFn = mockModule->getFunction(opts.MainCurrentName); - mainFn->setName(opts.EntryPoint); - *f << *mockModule; - mainFn->setName(opts.MainCurrentName); + if (interpreterOpts.Mock == MockPolicy::All || + interpreterOpts.MockMutableGlobals == MockMutableGlobalsPolicy::All || + !opts.AnnotationsFile.empty()) { + MockBuilder mockBuilder(kmodule->module.get(), opts, interpreterOpts, + ignoredExternals, redefinitions, interpreterHandler, + mainModuleFunctions, mainModuleGlobals); + std::unique_ptr mockModule = mockBuilder.build(); std::vector> mockModules; mockModules.push_back(std::move(mockModule)); - kmodule->link(mockModules, 0); + // std::swap(mockModule, kmodule->module); + kmodule->link(mockModules, 1); + klee_message("Mock linkage: done"); for (auto &global : kmodule->module->globals()) { if (global.isDeclaration()) { @@ -732,37 +690,6 @@ llvm::Module *Executor::setModule( return kmodule->module.get(); } -std::map -Executor::getAllExternals(const std::set &ignoredExternals) { - std::map externals; - for (const auto &f : kmodule->module->functions()) { - if (f.isDeclaration() && !f.use_empty() && - !ignoredExternals.count(f.getName().str())) - // NOTE: here we detect all the externals, even linked. - externals.insert(std::make_pair(f.getName(), f.getFunctionType())); - } - - for (const auto &global : kmodule->module->globals()) { - if (global.isDeclaration() && - !ignoredExternals.count(global.getName().str())) - externals.insert(std::make_pair(global.getName(), global.getValueType())); - } - - for (const auto &alias : kmodule->module->aliases()) { - auto it = externals.find(alias.getName().str()); - if (it != externals.end()) { - externals.erase(it); - } - } - - for (const auto &e : externals) { - klee_message("Mocking external %s %s", - e.second->isFunctionTy() ? "function" : "variable", - e.first.c_str()); - } - return externals; -} - Executor::~Executor() { delete typeSystemManager; delete externalDispatcher; @@ -1098,11 +1025,7 @@ void Executor::initializeGlobalObjects(ExecutionState &state) { } else { addr = externalDispatcher->resolveSymbol(v.getName().str()); } - if (MockAllExternals && !addr) { - executeMakeSymbolic( - state, mo, typeSystemManager->getWrappedType(v.getType()), - SourceBuilder::irreproducible("mockExternGlobalObject"), false); - } else if (!addr) { + if (!addr) { klee_error("Unable to load symbol(%.*s) while initializing globals", static_cast(v.getName().size()), v.getName().data()); } else { @@ -1116,18 +1039,11 @@ void Executor::initializeGlobalObjects(ExecutionState &state) { SourceBuilder::irreproducible("unsizedGlobal"), false); } } else if (v.hasInitializer()) { - if (!v.isConstant() && kmodule->inMainModule(v) && - MockMutableGlobals == MockMutableGlobalsPolicy::All) { - executeMakeSymbolic( - state, mo, typeSystemManager->getWrappedType(v.getType()), - SourceBuilder::irreproducible("mockMutableGlobalObject"), false); - } else { - initializeGlobalObject(state, os, v.getInitializer(), 0); - if (v.isConstant()) { - os->setReadOnly(true); - // initialise constant memory that may be used with external calls - state.addressSpace.copyOutConcrete(mo, os, {}); - } + initializeGlobalObject(state, os, v.getInitializer(), 0); + if (v.isConstant()) { + os->setReadOnly(true); + // initialise constant memory that may be used with external calls + state.addressSpace.copyOutConcrete(mo, os, {}); } } } @@ -3091,7 +3007,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { have already got a value. But in the end the caches should handle it for us, albeit with some overhead. */ do { - if (!first && MockExternalCalls) { + if (!first && interpreterOpts.Mock == MockPolicy::Failed) { free = nullptr; if (ki->inst()->getType()->isSized()) { prepareMockValue(state, "mockExternResult", ki); @@ -5078,28 +4994,6 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, return; } - if (ExternalCalls == ExternalCallPolicy::All && MockAllExternals) { - std::string TmpStr; - llvm::raw_string_ostream os(TmpStr); - os << "calling external: " << callable->getName().str() << "("; - for (unsigned i = 0; i < arguments.size(); i++) { - os << arguments[i]; - if (i != arguments.size() - 1) - os << ", "; - } - os << ") at " << state.pc->getSourceLocationString(); - - if (AllExternalWarnings) - klee_warning("%s", os.str().c_str()); - else if (!SuppressExternalWarnings) - klee_warning_once(callable->unwrap(), "%s", os.str().c_str()); - - if (target->inst()->getType()->isSized()) { - prepareMockValue(state, "mockExternResult", target); - } - return; - } - // normal external function handling path // allocate 512 bits for each argument (+return value) to support // fp80's and SIMD vectors as parameters for external calls; @@ -5218,7 +5112,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, roundingMode); if (!success) { - if (MockExternalCalls) { + if (interpreterOpts.Mock == MockPolicy::Failed) { if (target->inst()->getType()->isSized()) { prepareMockValue(state, "mockExternResult", target); } @@ -5309,7 +5203,7 @@ ObjectState *Executor::bindObjectInState(ExecutionState &state, // will put multiple copies on this list, but it doesn't really // matter because all we use this list for is to unbind the object // on function return. - if (isLocal && state.stack.size() > 0) { + if (isLocal && !state.stack.empty()) { state.stack.valueStack().back().allocas.push_back(mo->id); } return os; @@ -6163,16 +6057,6 @@ void Executor::collectReads( result = FPToX87FP80Ext(result); } - if (MockMutableGlobals == MockMutableGlobalsPolicy::PrimitiveFields && - mo->isGlobal && !os->readOnly && isa(result) && - !targetType->getRawType()->isPointerTy()) { - result = makeMockValue(state, "mockGlobalValue", result->getWidth()); - ObjectState *wos = state.addressSpace.getWriteable(mo, os); - maxNewWriteableOSSize = - std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); - wos->write(mo->getOffsetExpr(address), result); - } - results.push_back(result); } } @@ -6342,16 +6226,6 @@ void Executor::executeMemoryOperation( if (interpreterOpts.MakeConcreteSymbolic) result = replaceReadWithSymbolic(*state, result); - if (MockMutableGlobals == MockMutableGlobalsPolicy::PrimitiveFields && - mo->isGlobal && !os->readOnly && isa(result) && - !targetType->getRawType()->isPointerTy()) { - result = makeMockValue(*state, "mockGlobalValue", result->getWidth()); - ObjectState *wos = state->addressSpace.getWriteable(mo, os); - maxNewWriteableOSSize = - std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); - wos->write(mo->getOffsetExpr(address), result); - } - bindLocal(target, *state, result); } @@ -6534,16 +6408,6 @@ void Executor::executeMemoryOperation( result = FPToX87FP80Ext(result); } - if (MockMutableGlobals == MockMutableGlobalsPolicy::PrimitiveFields && - mo->isGlobal && !os->readOnly && isa(result) && - !targetType->getRawType()->isPointerTy()) { - result = makeMockValue(*bound, "mockGlobalValue", result->getWidth()); - ObjectState *wos = bound->addressSpace.getWriteable(mo, os); - maxNewWriteableOSSize = - std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries()); - wos->write(mo->getOffsetExpr(address), result); - } - bindLocal(target, *bound, result); } } @@ -6831,48 +6695,6 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } } -void Executor::executeMakeMock(ExecutionState &state, KInstruction *target, - std::vector> &arguments) { - KFunction *kf = target->parent->parent; - std::string name = "@call_" + kf->getName().str(); - uint64_t width = - kmodule->targetData->getTypeSizeInBits(kf->function->getReturnType()); - KType *type = typeSystemManager->getWrappedType( - llvm::PointerType::get(kf->function->getReturnType(), - kmodule->targetData->getAllocaAddrSpace())); - - IDType moID; - bool success = state.addressSpace.resolveOne(cast(arguments[0]), - type, moID); - assert(success && "memory object for mock should already be allocated"); - const MemoryObject *mo = state.addressSpace.findObject(moID).first; - assert(mo && "memory object for mock should already be allocated"); - mo->setName(name); - - ref source; - switch (interpreterOpts.MockStrategy) { - case MockStrategy::None: - klee_error("klee_make_mock is not allowed when mock strategy is none"); - break; - case MockStrategy::Naive: - source = SourceBuilder::mockNaive(kmodule.get(), *kf->function, - updateNameVersion(state, name)); - break; - case MockStrategy::Deterministic: - std::vector> args(kf->numArgs); - for (size_t i = 0; i < kf->numArgs; i++) { - args[i] = getArgumentCell(state, kf, i).value; - } - source = - SourceBuilder::mockDeterministic(kmodule.get(), *kf->function, args); - break; - } - executeMakeSymbolic(state, mo, type, source, false); - const ObjectState *os = state.addressSpace.findObject(mo->id).second; - auto result = os->read(0, width); - bindLocal(target, state, result); -} - /***/ ExecutionState *Executor::formState(Function *f) { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index f0c53a8da4..d6cbb17352 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -428,9 +428,6 @@ class Executor : public Interpreter { KType *type, const ref source, bool isLocal); - void executeMakeMock(ExecutionState &state, KInstruction *target, - std::vector> &arguments); - void updateStateWithSymcretes(ExecutionState &state, const Assignment &assignment); @@ -732,18 +729,13 @@ class Executor : public Interpreter { replayPosition = 0; } - llvm::Module * - setModule(std::vector> &userModules, - std::vector> &libsModules, - const ModuleOptions &opts, - std::set &&mainModuleFunctions, - std::set &&mainModuleGlobals, - FLCtoOpcode &&origInstructions, - const std::set &ignoredExternals, - const Annotations &annotations) override; - - std::map - getAllExternals(const std::set &ignoredExternals) override; + llvm::Module *setModule( + std::vector> &userModules, + std::vector> &libsModules, + const ModuleOptions &opts, std::set &&mainModuleFunctions, + std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, + const std::set &ignoredExternals, + std::vector> redefinitions) override; void useSeeds(const std::vector *seeds) override { usingSeeds = seeds; diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index 0545c34115..de06f5e463 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -1,224 +1,672 @@ +//===-- MockBuilder.cpp ---------------------------------------------------===// +// +// The KLEEF Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +//===----------------------------------------------------------------------===// + #include "klee/Core/MockBuilder.h" +#include "klee/Config/Version.h" #include "klee/Module/Annotation.h" #include "klee/Support/ErrorHandling.h" +#include "klee/Support/ModuleUtil.h" + #include "llvm/IR/IRBuilder.h" #include "llvm/IR/Module.h" +#include "llvm/Support/raw_ostream.h" #include #include namespace klee { -MockBuilder::MockBuilder(const llvm::Module *initModule, - std::string mockEntrypoint, std::string userEntrypoint, - std::map externals, - Annotations annotations) - : userModule(initModule), externals(std::move(externals)), - annotations(std::move(annotations)), - mockEntrypoint(std::move(mockEntrypoint)), - userEntrypoint(std::move(userEntrypoint)) {} +template +void inline removeAliases(const llvm::Module *userModule, + std::map &externals) { + for (const auto &alias : userModule->aliases()) { + auto it = externals.find(alias.getName().str()); + if (it != externals.end()) { + externals.erase(it); + } + } +} + +void MockBuilder::buildCallKleeMakeSymbolic( + const std::string &kleeMakeSymbolicFunctionName, llvm::Value *source, + llvm::Type *type, const std::string &symbolicName) { + auto *kleeMakeSymbolicName = llvm::FunctionType::get( + llvm::Type::getVoidTy(ctx), + {llvm::Type::getInt8PtrTy(ctx), llvm::Type::getInt64Ty(ctx), + llvm::Type::getInt8PtrTy(ctx)}, + false); + auto kleeMakeSymbolicCallee = mockModule->getOrInsertFunction( + kleeMakeSymbolicFunctionName, kleeMakeSymbolicName); + auto bitCastInst = + builder->CreateBitCast(source, llvm::Type::getInt8PtrTy(ctx)); + auto globalSymbolicName = builder->CreateGlobalString("@" + symbolicName); + auto gep = builder->CreateConstInBoundsGEP2_64( + globalSymbolicName->getValueType(), globalSymbolicName, 0, 0); + auto sz = llvm::APInt(64, mockModule->getDataLayout().getTypeStoreSize(type), + false); + builder->CreateCall(kleeMakeSymbolicCallee, + {bitCastInst, llvm::ConstantInt::get(ctx, sz), gep}); +} + +std::map +MockBuilder::getExternalFunctions() { + std::map externals; + for (const auto &f : userModule->functions()) { + if (f.isDeclaration() && !f.use_empty() && + !ignoredExternals.count(f.getName().str())) { + // NOTE: here we detect all the externals, even linked. + externals.insert(std::make_pair(f.getName(), f.getFunctionType())); + } + } + removeAliases(userModule, externals); + + return externals; +} + +std::map MockBuilder::getExternalGlobals() { + std::map externals; + for (const auto &global : userModule->globals()) { + if (global.isDeclaration() && + !ignoredExternals.count(global.getName().str())) { + externals.insert(std::make_pair(global.getName(), global.getType())); + } + } + removeAliases(userModule, externals); + return externals; +} + +MockBuilder::MockBuilder( + const llvm::Module *initModule, const Interpreter::ModuleOptions &opts, + const Interpreter::InterpreterOptions &interpreterOptions, + const std::set &ignoredExternals, + std::vector> &redefinitions, + InterpreterHandler *interpreterHandler, + std::set &mainModuleFunctions, + std::set &mainModuleGlobals) + : userModule(initModule), ctx(initModule->getContext()), opts(opts), + interpreterOptions(interpreterOptions), + ignoredExternals(ignoredExternals), redefinitions(redefinitions), + interpreterHandler(interpreterHandler), + mainModuleFunctions(mainModuleFunctions), + mainModuleGlobals(mainModuleGlobals) { + annotations = parseAnnotations(opts.AnnotationsFile); +} std::unique_ptr MockBuilder::build() { initMockModule(); buildMockMain(); buildExternalFunctionsDefinitions(); + + if (!mockModule) { + klee_error("Unable to generate mocks"); + } + + { + const std::string redefinitionsFileName = "redefinitions.txt"; + auto os(interpreterHandler->openOutputFile(redefinitionsFileName)); + if (!os) { + klee_error("Mock: can't open %s file", redefinitionsFileName.c_str()); + } + for (const auto &i : redefinitions) { + *os << i.first << " " << i.second << "\n"; + } + } + + const std::string externalsFileName = "externals.ll"; + std::string extFile = + interpreterHandler->getOutputFilename(externalsFileName); + + { + auto mainFn = mockModule->getFunction(opts.MainCurrentName); + mainFn->setName(opts.EntryPoint); + auto os = interpreterHandler->openOutputFile(externalsFileName); + if (!os) { + klee_error("Mock: can't open '%s' file", externalsFileName.c_str()); + } + *os << *mockModule; + mockModule.reset(); + } + + { + std::string errorMsg; + std::vector> loadedUserModules; + loadFileAsOneModule(extFile, ctx, loadedUserModules, errorMsg); + std::swap(loadedUserModules.front(), mockModule); + + auto mainFn = mockModule->getFunction(opts.MainCurrentName); + mainFn->setName(opts.MainCurrentName); + } + return std::move(mockModule); } void MockBuilder::initMockModule() { - mockModule = std::make_unique(userModule->getName().str() + - "__klee_externals", - userModule->getContext()); + mockModule = std::make_unique( + userModule->getName().str() + "__klee_externals", ctx); mockModule->setTargetTriple(userModule->getTargetTriple()); mockModule->setDataLayout(userModule->getDataLayout()); - builder = std::make_unique>(mockModule->getContext()); + builder = std::make_unique>(ctx); } // Set up entrypoint in new module. Here we'll define external globals and then // call user's entrypoint. void MockBuilder::buildMockMain() { - llvm::Function *userMainFn = userModule->getFunction(userEntrypoint); + mainModuleFunctions.insert(opts.MainNameAfterMock); + llvm::Function *userMainFn = userModule->getFunction(opts.MainCurrentName); if (!userMainFn) { klee_error("Entry function '%s' not found in module.", - userEntrypoint.c_str()); + opts.MainCurrentName.c_str()); } - mockModule->getOrInsertFunction(mockEntrypoint, userMainFn->getFunctionType(), + userMainFn->setName(opts.MainNameAfterMock); + + mockModule->getOrInsertFunction(opts.MainCurrentName, + userMainFn->getFunctionType(), userMainFn->getAttributes()); - llvm::Function *mockMainFn = mockModule->getFunction(mockEntrypoint); + llvm::Function *mockMainFn = mockModule->getFunction(opts.MainCurrentName); if (!mockMainFn) { - klee_error("Entry function '%s' not found in module.", - mockEntrypoint.c_str()); + klee_error("Mock: Entry function '%s' not found in module", + opts.MainCurrentName.c_str()); } - auto globalsInitBlock = - llvm::BasicBlock::Create(mockModule->getContext(), "entry", mockMainFn); + mockMainFn->setDSOLocal(true); + auto globalsInitBlock = llvm::BasicBlock::Create(ctx, "", mockMainFn); builder->SetInsertPoint(globalsInitBlock); // Define all the external globals - buildExternalGlobalsDefinitions(); + if (interpreterOptions.Mock == MockPolicy::All || + interpreterOptions.MockMutableGlobals == MockMutableGlobalsPolicy::All) { + buildExternalGlobalsDefinitions(); + } auto userMainCallee = mockModule->getOrInsertFunction( - userEntrypoint, userMainFn->getFunctionType()); + opts.MainNameAfterMock, userMainFn->getFunctionType()); std::vector args; args.reserve(userMainFn->arg_size()); - for (auto it = mockMainFn->arg_begin(); it != mockMainFn->arg_end(); it++) { - args.push_back(it); + for (auto &arg : mockMainFn->args()) { + args.push_back(&arg); } + auto callUserMain = builder->CreateCall(userMainCallee, args); - builder->CreateRet(callUserMain); + if (!userMainFn->getReturnType()->isSized()) { + builder->CreateRet(nullptr); + return; + } else { + builder->CreateRet(callUserMain); + } } void MockBuilder::buildExternalGlobalsDefinitions() { - for (const auto &it : externals) { - if (it.second->isFunctionTy()) { - continue; - } - const std::string &extName = it.first; - llvm::Type *type = it.second; - mockModule->getOrInsertGlobal(extName, type); - auto *global = mockModule->getGlobalVariable(extName); + auto externalGlobals = getExternalGlobals(); + for (const auto &[extName, type] : externalGlobals) { + auto elementType = type->getPointerElementType(); + klee_message("Mocking external variable %s", extName.c_str()); + llvm::GlobalVariable *global = dyn_cast_or_null( + mockModule->getOrInsertGlobal(extName, elementType)); if (!global) { - klee_error("Unable to add global variable '%s' to module", + klee_error("Mock: Unable to add global variable '%s' to module", extName.c_str()); } - global->setLinkage(llvm::GlobalValue::ExternalLinkage); - if (!type->isSized()) { + + mainModuleGlobals.insert(extName); + if (!elementType->isSized()) { continue; } - auto *zeroInitializer = llvm::Constant::getNullValue(it.second); + auto *zeroInitializer = llvm::GlobalValue::getNullValue(elementType); if (!zeroInitializer) { - klee_error("Unable to get zero initializer for '%s'", extName.c_str()); + klee_error("Mock: Unable to get zero initializer for '%s'", + extName.c_str()); } global->setInitializer(zeroInitializer); - buildCallKleeMakeSymbol("klee_make_symbolic", global, type, - "@obj_" + extName); + global->setDSOLocal(true); + auto *localPointer = builder->CreateAlloca(elementType, nullptr); + buildCallKleeMakeSymbolic("klee_make_symbolic", localPointer, elementType, + "external_" + extName); + llvm::Value *localValue = builder->CreateLoad(elementType, localPointer); + builder->CreateStore(localValue, global); } } +// standard functions that must be ignored +const std::set StandartIgnoredFunctions = { + "_ZNSt8ios_base4InitC1Ev", "_ZNSt8ios_base4InitD1Ev"}; + void MockBuilder::buildExternalFunctionsDefinitions() { - for (const auto &it : externals) { - if (!it.second->isFunctionTy()) { - continue; + std::map externalFunctions; + if (interpreterOptions.Mock == MockPolicy::All) { + externalFunctions = getExternalFunctions(); + } + + if (!opts.AnnotateOnlyExternal) { + for (const auto &annotation : annotations) { + llvm::Function *func = userModule->getFunction(annotation.first); + if (func) { + auto ext = externalFunctions.find(annotation.first); + if (ext == externalFunctions.end()) { + externalFunctions[annotation.first] = func->getFunctionType(); + } + } } - std::string extName = it.first; - auto *type = llvm::cast(it.second); + } + + for (const auto &[extName, type] : externalFunctions) { mockModule->getOrInsertFunction(extName, type); llvm::Function *func = mockModule->getFunction(extName); if (!func) { - klee_error("Unable to find function '%s' in module", extName.c_str()); + klee_error("Mock: Unable to find function '%s' in module", + extName.c_str()); + } + if (func->isIntrinsic()) { + klee_message("Mock: Skip intrinsic function '%s'", extName.c_str()); + continue; + } + if (StandartIgnoredFunctions.count(extName)) { + klee_message("Mock: Skip function '%s'", extName.c_str()); + continue; } + mainModuleFunctions.insert(extName); if (!func->empty()) { continue; } - auto *BB = - llvm::BasicBlock::Create(mockModule->getContext(), "entry", func); + auto *BB = llvm::BasicBlock::Create(ctx, "entry", func); builder->SetInsertPoint(BB); - if (!func->getReturnType()->isSized()) { - builder->CreateRet(nullptr); - continue; + const auto nameToAnnotations = annotations.find(extName); + if (nameToAnnotations != annotations.end()) { + klee_message("Annotation function %s", extName.c_str()); + const auto &annotation = nameToAnnotations->second; + + buildAnnotationForExternalFunctionArgs(func, annotation.argsStatements); + buildAnnotationForExternalFunctionReturn(func, + annotation.returnStatements); + buildAnnotationForExternalFunctionProperties(func, annotation.properties); + } else { + klee_message("Mocking external function %s", extName.c_str()); + // Default annotation for externals return + buildAnnotationForExternalFunctionReturn( + func, {std::make_shared()}); } + } +} - const auto annotation = annotations.find(extName); - if (annotation != annotations.end()) { - buildAnnotationForExternalFunctionParams(func, annotation->second); +std::pair +MockBuilder::goByOffset(llvm::Value *value, + const std::vector &offset) { + llvm::Value *prev = nullptr; + llvm::Value *current = value; + for (const auto &inst : offset) { + if (inst == "*") { + if (!current->getType()->isPointerTy()) { + klee_error("Incorrect annotation offset."); + } + prev = current; + current = builder->CreateLoad(current->getType()->getPointerElementType(), + current); + } else if (inst == "&") { + auto addr = builder->CreateAlloca(current->getType()); + prev = current; + current = builder->CreateStore(current, addr); + } else { + const size_t index = std::stol(inst); + if (!(current->getType()->isPointerTy() || + current->getType()->isArrayTy())) { + klee_error("Incorrect annotation offset."); + } + prev = current; + current = builder->CreateConstInBoundsGEP1_64(current->getType(), current, + index); } + } + return {prev, current}; +} - auto *mockReturnValue = - builder->CreateAlloca(func->getReturnType(), nullptr); - buildCallKleeMakeSymbol("klee_make_mock", mockReturnValue, - func->getReturnType(), "@call_" + extName); - auto *loadInst = builder->CreateLoad(mockReturnValue, "klee_var"); - builder->CreateRet(loadInst); +inline llvm::Type *getTypeByOffset(llvm::Type *value, + const std::vector &offset) { + llvm::Type *current = value; + for (const auto &inst : offset) { + if (inst == "*") { + if (!current->isPointerTy()) { + return nullptr; + } + current = current->getPointerElementType(); + } else if (inst == "&") { + // Not change + } else { + const size_t index = std::stol(inst); + if (current->isArrayTy() || current->isPointerTy()) { + current = current->getContainedType(index); + } else { + return nullptr; + } + } } + return current; } -void MockBuilder::buildCallKleeMakeSymbol(const std::string &klee_function_name, - llvm::Value *source, llvm::Type *type, - const std::string &symbol_name) { - auto *klee_mk_symb_type = llvm::FunctionType::get( - llvm::Type::getVoidTy(mockModule->getContext()), - {llvm::Type::getInt8PtrTy(mockModule->getContext()), - llvm::Type::getInt64Ty(mockModule->getContext()), - llvm::Type::getInt8PtrTy(mockModule->getContext())}, - false); - auto kleeMakeSymbolCallee = - mockModule->getOrInsertFunction(klee_function_name, klee_mk_symb_type); - auto bitcastInst = builder->CreateBitCast( - source, llvm::Type::getInt8PtrTy(mockModule->getContext())); - auto str_name = builder->CreateGlobalString(symbol_name); - auto gep = builder->CreateConstInBoundsGEP2_64(str_name, 0, 0); - builder->CreateCall( - kleeMakeSymbolCallee, - {bitcastInst, - llvm::ConstantInt::get( - mockModule->getContext(), - llvm::APInt(64, mockModule->getDataLayout().getTypeStoreSize(type), - false)), - gep}); -} - -// TODO: add method for return value of external functions. -void MockBuilder::buildAnnotationForExternalFunctionParams( - llvm::Function *func, Annotation &annotation) { - for (size_t i = 1; i < annotation.statements.size(); i++) { - const auto arg = func->getArg(i - 1); - for (const auto &statement : annotation.statements[i]) { - llvm::Value *elem = goByOffset(arg, statement->offset); - switch (statement->getStatementName()) { - case Annotation::StatementKind::Deref: { - if (!elem->getType()->isPointerTy()) { - klee_error("Incorrect annotation offset."); - } - builder->CreateLoad(elem); +inline bool isCorrectStatements(const std::vector &statements, + const llvm::Argument *arg) { + return std::any_of(statements.begin(), statements.end(), + [arg](const Statement::Ptr &statement) { + auto argType = + getTypeByOffset(arg->getType(), statement->offset); + switch (statement->getKind()) { + case Statement::Kind::Deref: + case Statement::Kind::InitNull: + return argType->isPointerTy(); + case Statement::Kind::AllocSource: + assert(false); + case Statement::Kind::Unknown: + default: + return true; + } + }); +} + +bool tryAlign(llvm::Function *func, + const std::vector> &statements, + std::vector> &res) { + if (func->arg_size() == statements.size()) { + res = statements; + return true; + } + + for (size_t i = 0, j = 0; j < func->arg_size() && i < statements.size();) { + while (true) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(10, 0) + auto arg = func->getArg(j); +#else + auto arg = &func->arg_begin()[j]; +#endif + if (isCorrectStatements(statements[i], arg)) { break; } - case Annotation::StatementKind::InitNull: { - // TODO + res.emplace_back(); + j++; + if (j >= func->arg_size()) { + break; } - case Annotation::StatementKind::Unknown: - default: - __builtin_unreachable(); + } + res.push_back(statements[i]); + j++; + i++; + } + if (func->arg_size() == statements.size()) { + return true; + } + return false; +} + +std::map, std::vector> +unifyByOffset(const std::vector &statements) { + std::map, std::vector> res; + for (const auto &i : statements) { + res[i->offset].push_back(i); + } + return res; +} + +void MockBuilder::buildAnnotationForExternalFunctionArgs( + llvm::Function *func, + const std::vector> &statementsNotAlign) { + std::vector> statements; + bool flag = tryAlign(func, statementsNotAlign, statements); + if (!flag) { + klee_warning("Annotation: can't align function arguments %s", + func->getName().str().c_str()); + return; + } + for (size_t i = 0; i < statements.size(); i++) { +#if LLVM_VERSION_CODE >= LLVM_VERSION(10, 0) + const auto arg = func->getArg(i); +#else + const auto arg = &func->arg_begin()[i]; +#endif + auto statementsMap = unifyByOffset(statements[i]); + for (const auto &[offset, statementsOffset] : statementsMap) { + auto [prev, elem] = goByOffset(arg, offset); + + Statement::Alloc *allocSourcePtr = nullptr; + Statement::Free *freePtr = nullptr; + Statement::InitNull *initNullPtr = nullptr; + + for (const auto &statement : statementsOffset) { + switch (statement->getKind()) { + case Statement::Kind::Deref: { + if (!elem->getType()->isPointerTy()) { + klee_error("Annotation: Deref arg not pointer"); + } + + std::string derefCondName = "condition_deref_arg_" + + std::to_string(i) + "_deref_" + + func->getName().str(); + + auto intType = llvm::IntegerType::get(ctx, 1); + auto *derefCond = builder->CreateAlloca(intType, nullptr); + buildCallKleeMakeSymbolic("klee_make_mock", derefCond, intType, + derefCondName); + + llvm::BasicBlock *fromIf = builder->GetInsertBlock(); + llvm::Function *curFunc = fromIf->getParent(); + + llvm::BasicBlock *derefBB = + llvm::BasicBlock::Create(ctx, derefCondName, curFunc); + llvm::BasicBlock *contBB = + llvm::BasicBlock::Create(ctx, "continue_" + derefCondName); + auto brValue = builder->CreateLoad(intType, derefCond); + builder->CreateCondBr(brValue, derefBB, contBB); + + builder->SetInsertPoint(derefBB); + builder->CreateLoad(elem->getType()->getPointerElementType(), elem); + builder->CreateBr(contBB); + + curFunc->getBasicBlockList().push_back(contBB); + builder->SetInsertPoint(contBB); + break; + } + case Statement::Kind::AllocSource: { + if (prev != nullptr) { + allocSourcePtr = (Statement::Alloc *)statement.get(); + } else { + klee_message("Annotation: not valid annotation %s", + statement->toString().c_str()); + } + break; + } + case Statement::Kind::InitNull: { + if (prev != nullptr) { + initNullPtr = (Statement::InitNull *)statement.get(); + } else { + klee_message("Annotation: not valid annotation %s", + statement->toString().c_str()); + } + break; + } + case Statement::Kind::Free: { + if (elem->getType()->isPointerTy()) { + freePtr = (Statement::Free *)statement.get(); + } else { + klee_message("Annotation: not valid annotation %s", + statement->toString().c_str()); + } + break; + } + case Statement::Kind::Unknown: + default: + klee_message("Annotation: not implemented %s", + statement->toString().c_str()); + break; + } } + if (freePtr) { + buildFree(elem, freePtr); + } + processingValue(prev, elem->getType(), allocSourcePtr, initNullPtr); } } +} - for (const auto &property : annotation.properties) { - switch (property) { - case Annotation::Property::Determ: { - // TODO +void MockBuilder::processingValue(llvm::Value *prev, llvm::Type *elemType, + const Statement::Alloc *allocSourcePtr, + bool initNullPtr) { + if (initNullPtr) { + auto intType = llvm::IntegerType::get(ctx, 1); + auto *allocCond = builder->CreateAlloca(intType, nullptr); + buildCallKleeMakeSymbolic("klee_make_mock", allocCond, intType, + "initPtrCond"); + + llvm::BasicBlock *fromIf = builder->GetInsertBlock(); + llvm::Function *curFunc = fromIf->getParent(); + + llvm::BasicBlock *initNullBB = llvm::BasicBlock::Create(ctx, "initNullBR"); + llvm::BasicBlock *contBB = llvm::BasicBlock::Create(ctx, "continueBR"); + auto brValue = builder->CreateLoad(intType, allocCond); + if (allocSourcePtr) { + llvm::BasicBlock *allocBB = + llvm::BasicBlock::Create(ctx, "allocArg", curFunc); + builder->CreateCondBr(brValue, allocBB, initNullBB); + builder->SetInsertPoint(allocBB); + buildAllocSource(prev, elemType, allocSourcePtr); + builder->CreateBr(contBB); + } else { + builder->CreateCondBr(brValue, initNullBB, contBB); + } + curFunc->getBasicBlockList().push_back(initNullBB); + builder->SetInsertPoint(initNullBB); + builder->CreateStore( + llvm::ConstantPointerNull::get(llvm::cast(elemType)), + prev); + builder->CreateBr(contBB); + + curFunc->getBasicBlockList().push_back(contBB); + builder->SetInsertPoint(contBB); + } else if (allocSourcePtr) { + buildAllocSource(prev, elemType, allocSourcePtr); + } +} + +void MockBuilder::buildAllocSource(llvm::Value *prev, llvm::Type *elemType, + const Statement::Alloc *allocSourcePtr) { + if (allocSourcePtr->value != Statement::Alloc::ALLOC) { + klee_warning("Annotation: AllocSource \"%d\" not implemented use alloc", + allocSourcePtr->value); + } + auto valueType = elemType->getPointerElementType(); + auto sizeValue = llvm::ConstantInt::get( + ctx, + llvm::APInt(64, mockModule->getDataLayout().getTypeStoreSize(valueType), + false)); + auto int8PtrTy = llvm::IntegerType::getInt64Ty(ctx); + auto mallocInstr = + llvm::CallInst::CreateMalloc(builder->GetInsertBlock(), int8PtrTy, + valueType, sizeValue, nullptr, nullptr); + auto mallocValue = builder->Insert(mallocInstr, llvm::Twine("MallocValue")); + builder->CreateStore(mallocValue, prev); +} + +void MockBuilder::buildFree(llvm::Value *elem, const Statement::Free *freePtr) { + if (freePtr->value != Statement::Free::FREE) { + klee_warning("Annotation: AllocSource \"%d\" not implemented use free", + freePtr->value); + } + auto freeInstr = llvm::CallInst::CreateFree(elem, builder->GetInsertBlock()); + builder->Insert(freeInstr); +} + +void MockBuilder::buildAnnotationForExternalFunctionReturn( + llvm::Function *func, const std::vector &statements) { + auto returnType = func->getReturnType(); + if (!returnType->isSized()) { // void return type + builder->CreateRet(nullptr); + return; + } + + Statement::Alloc *allocSourcePtr = nullptr; + Statement::InitNull *mustInitNull = nullptr; + Statement::MaybeInitNull *maybeInitNull = nullptr; + + for (const auto &statement : statements) { + switch (statement->getKind()) { + case Statement::Kind::Deref: + klee_warning("Annotation: unused Deref for return function \"%s\"", + func->getName().str().c_str()); + break; + case Statement::Kind::AllocSource: { + allocSourcePtr = returnType->isPointerTy() + ? (Statement::Alloc *)statement.get() + : nullptr; + break; + } + case Statement::Kind::InitNull: { + mustInitNull = returnType->isPointerTy() + ? (Statement::InitNull *)statement.get() + : nullptr; + break; + } + case Statement::Kind::MaybeInitNull: { + maybeInitNull = returnType->isPointerTy() + ? (Statement::MaybeInitNull *)statement.get() + : nullptr; + break; } - case Annotation::Property::Noreturn: { - // TODO + case Statement::Kind::Free: { + klee_warning("Annotation: unused \"Free\" for return"); + break; } - case Annotation::Property::Unknown: + case Statement::Kind::Unknown: default: - __builtin_unreachable(); + klee_message("Annotation: not implemented %s", + statement->toString().c_str()); + break; } } + std::string retName = "ret_" + func->getName().str(); + llvm::Value *retValuePtr = builder->CreateAlloca(returnType, nullptr); + + if (returnType->isPointerTy() && (allocSourcePtr || mustInitNull)) { + processingValue(retValuePtr, returnType, allocSourcePtr, + mustInitNull || maybeInitNull); + } else { + buildCallKleeMakeSymbolic("klee_make_mock", retValuePtr, returnType, + func->getName().str()); + if (returnType->isPointerTy() && !maybeInitNull) { + llvm::Value *retValue = + builder->CreateLoad(returnType, retValuePtr, retName); + auto cmpResult = + builder->CreateICmpNE(retValue, + llvm::ConstantPointerNull::get( + llvm::cast(returnType)), + "condition_init_null" + retName); + + auto *kleeAssumeType = llvm::FunctionType::get( + llvm::Type::getVoidTy(ctx), {llvm::Type::getInt64Ty(ctx)}, false); + + auto kleeAssumeFunc = + mockModule->getOrInsertFunction("klee_assume", kleeAssumeType); + auto cmpResult64 = + builder->CreateZExt(cmpResult, llvm::Type::getInt64Ty(ctx)); + builder->CreateCall(kleeAssumeFunc, {cmpResult64}); + } + } + llvm::Value *retValue = builder->CreateLoad(returnType, retValuePtr, retName); + builder->CreateRet(retValue); } -llvm::Value *MockBuilder::goByOffset(llvm::Value *value, - const std::vector &offset) { - llvm::Value *current = value; - for (const auto &inst : offset) { - if (inst == "*") { - if (!current->getType()->isPointerTy()) { - klee_error("Incorrect annotation offset."); - } - current = builder->CreateLoad(current); - } else if (inst == "&") { - auto addr = builder->CreateAlloca(current->getType()); - current = builder->CreateStore(current, addr); - } else { - const size_t index = std::stol(inst); - if (!(current->getType()->isPointerTy() || current->getType()->isArrayTy())) { - klee_error("Incorrect annotation offset."); - } - current = builder->CreateConstInBoundsGEP1_64(current, index); +void MockBuilder::buildAnnotationForExternalFunctionProperties( + llvm::Function *func, const std::set &properties) { + for (const auto &property : properties) { + switch (property) { + case Statement::Property::Deterministic: + case Statement::Property::Noreturn: + case Statement::Property::Unknown: + default: + klee_message("Property not implemented"); + break; } } - return current; } } // namespace klee diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 4690a1d1e1..ae4a7b358c 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -952,12 +952,67 @@ void SpecialFunctionHandler::handleMakeMock(ExecutionState &state, name = arguments[2]->isZero() ? "" : readStringAtAddress(state, arguments[2]); - if (name.length() == 0) { + if (name.empty()) { executor.terminateStateOnUserError( state, "Empty name of function in klee_make_mock"); return; } - executor.executeMakeMock(state, target, arguments); + + KFunction *kf = target->parent->parent; + + Executor::ExactResolutionList rl; + executor.resolveExact(state, arguments[0], + executor.typeSystemManager->getUnknownType(), rl, + "make_symbolic"); + + for (auto &it : rl) { + ObjectPair op = it.second->addressSpace.findObject(it.first); + const MemoryObject *mo = op.first; + mo->setName(name); + mo->updateTimestamp(); + + const ObjectState *old = op.second; + ExecutionState *s = it.second; + + if (old->readOnly) { + executor.terminateStateOnUserError( + *s, "cannot make readonly object symbolic"); + return; + } + + bool res; + bool success __attribute__((unused)) = executor.solver->mustBeTrue( + s->constraints.cs(), + EqExpr::create( + ZExtExpr::create(arguments[1], Context::get().getPointerWidth()), + mo->getSizeExpr()), + res, s->queryMetaData); + assert(success && "FIXME: Unhandled solver failure"); + + if (res) { + ref source; + switch (executor.interpreterOpts.MockStrategy) { + case MockStrategyKind::Naive: + source = + SourceBuilder::mockNaive(executor.kmodule.get(), *kf->function(), + executor.updateNameVersion(state, name)); + break; + case MockStrategyKind::Deterministic: + std::vector> args(kf->getNumArgs()); + for (size_t i = 0; i < kf->getNumArgs(); i++) { + args[i] = executor.getArgumentCell(state, kf, i).value; + } + source = SourceBuilder::mockDeterministic(executor.kmodule.get(), + *kf->function(), args); + break; + } + executor.executeMakeSymbolic(state, mo, old->getDynamicType(), source, + false); + } else { + executor.terminateStateOnUserError(*s, + "Wrong size given to klee_make_mock"); + } + } } void SpecialFunctionHandler::handleMarkGlobal( diff --git a/lib/Expr/AlphaBuilder.cpp b/lib/Expr/AlphaBuilder.cpp index 13fb00073f..3056503669 100644 --- a/lib/Expr/AlphaBuilder.cpp +++ b/lib/Expr/AlphaBuilder.cpp @@ -19,8 +19,18 @@ const Array *AlphaBuilder::visitArray(const Array *arr) { if (!reverse && alphaArrayMap.find(arr) == alphaArrayMap.end()) { ref source = arr->source; ref size = visit(arr->getSize()); - - if (!arr->isConstantArray()) { + if (ref mockSource = + dyn_cast_or_null(source)) { + std::vector> args; + for (const auto &it : mockSource->args) { + args.push_back(visit(it)); + } + source = SourceBuilder::mockDeterministic(mockSource->km, + mockSource->function, args); + alphaArrayMap[arr] = arrayCache.CreateArray( + size, source, arr->getDomain(), arr->getRange()); + reverseAlphaArrayMap[alphaArrayMap[arr]] = arr; + } else if (!arr->isConstantArray()) { source = SourceBuilder::alpha(index); index++; alphaArrayMap[arr] = arrayCache.CreateArray( @@ -69,9 +79,9 @@ ExprVisitor::Action AlphaBuilder::visitRead(const ReadExpr &re) { AlphaBuilder::AlphaBuilder(ArrayCache &_arrayCache) : arrayCache(_arrayCache) {} -constraints_ty AlphaBuilder::visitConstraints(constraints_ty cs) { +constraints_ty AlphaBuilder::visitConstraints(const constraints_ty &cs) { constraints_ty result; - for (auto arg : cs) { + for (const auto &arg : cs) { ref v = visit(arg); reverseExprMap[v] = arg; reverseExprMap[Expr::createIsZero(v)] = Expr::createIsZero(arg); @@ -79,6 +89,7 @@ constraints_ty AlphaBuilder::visitConstraints(constraints_ty cs) { } return result; } + ref AlphaBuilder::build(ref v) { ref e = visit(v); reverseExprMap[e] = v; diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index 50ac99942c..9ff427baf7 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -9,10 +9,8 @@ #include "klee/Expr/SymbolicSource.h" #include "klee/Expr/Symcrete.h" #include "klee/Module/KModule.h" -#include "klee/Solver/Solver.h" #include -#include #include #include #include @@ -270,13 +268,11 @@ bool IndependentConstraintSet::intersects( if (it2 != b->elements.end()) { if (it->second.intersects(it2->second)) { return true; + } } - } - for (std::set::iterator it = uninterpretedFunctions.begin(), - ie = uninterpretedFunctions.end(); - it != ie; ++it) { - if (b.uninterpretedFunctions.count(*it)) { - return true; + for (const auto &uFn : a->uninterpretedFunctions) { + if (b->uninterpretedFunctions.count(uFn)) { + return true; } } } diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 616d7a7f4a..956f1fb876 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -646,7 +646,7 @@ SourceResult ParserImpl::ParseMockNaiveSource() { auto versionExpr = ParseNumber(64).get(); auto version = dyn_cast(versionExpr); assert(version); - return SourceBuilder::mockNaive(km, *kf->function, version->getZExtValue()); + return SourceBuilder::mockNaive(km, *kf->function(), version->getZExtValue()); } SourceResult ParserImpl::ParseMockDeterministicSource() { @@ -655,8 +655,8 @@ SourceResult ParserImpl::ParseMockDeterministicSource() { ConsumeExpectedToken(Token::Identifier); ConsumeLParen(); std::vector> args; - args.reserve(kf->numArgs); - for (unsigned i = 0; i < kf->numArgs; i++) { + args.reserve(kf->getNumArgs()); + for (unsigned i = 0; i < kf->getNumArgs(); i++) { auto expr = ParseExpr(TypeResult()); if (!expr.isValid()) { return {false, nullptr}; @@ -664,7 +664,7 @@ SourceResult ParserImpl::ParseMockDeterministicSource() { args.push_back(expr.get()); } ConsumeRParen(); - return SourceBuilder::mockDeterministic(km, *kf->function, args); + return SourceBuilder::mockDeterministic(km, *kf->function(), args); } SourceResult ParserImpl::ParseAlphaSource() { diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp index 36193d3433..47f5fdd823 100644 --- a/lib/Expr/SourceBuilder.cpp +++ b/lib/Expr/SourceBuilder.cpp @@ -116,7 +116,6 @@ SourceBuilder::mockDeterministic(const KModule *km, return r; } - ref SourceBuilder::alpha(int _index) { ref r(new AlphaSource(_index)); r->computeHash(); diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index a32287784d..a1ea9a0de0 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -1,6 +1,5 @@ #include "klee/Expr/SymbolicSource.h" #include "klee/Expr/Expr.h" - #include "klee/Expr/ExprPPrinter.h" #include "klee/Expr/ExprUtil.h" #include "klee/Module/KInstruction.h" @@ -204,7 +203,7 @@ unsigned InstructionSource::computeHash() { unsigned MockNaiveSource::computeHash() { unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + version; - unsigned funcID = km->functionIDMap.at(&function); + unsigned funcID = km->getFunctionId(&function); res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + funcID; hashValue = res; return res; @@ -215,14 +214,14 @@ int MockNaiveSource::internalCompare(const SymbolicSource &b) const { return getKind() < b.getKind() ? -1 : 1; } const MockNaiveSource &mnb = static_cast(b); - if (version != mnb.version) { - return version < mnb.version ? -1 : 1; - } - unsigned funcID = km->functionIDMap.at(&function); - unsigned bFuncID = mnb.km->functionIDMap.at(&mnb.function); + unsigned funcID = km->getFunctionId(&function); + unsigned bFuncID = mnb.km->getFunctionId(&mnb.function); if (funcID != bFuncID) { return funcID < bFuncID ? -1 : 1; } + if (version != mnb.version) { + return version < mnb.version ? -1 : 1; + } return 0; } @@ -234,7 +233,7 @@ MockDeterministicSource::MockDeterministicSource( unsigned MockDeterministicSource::computeHash() { unsigned res = getKind(); res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + - km->functionIDMap.at(&function); + km->getFunctionId(&function); for (const auto &arg : args) { res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + arg->hash(); } @@ -248,8 +247,8 @@ int MockDeterministicSource::internalCompare(const SymbolicSource &b) const { } const MockDeterministicSource &mdb = static_cast(b); - unsigned funcID = km->functionIDMap.at(&function); - unsigned bFuncID = mdb.km->functionIDMap.at(&mdb.function); + unsigned funcID = km->getFunctionId(&function); + unsigned bFuncID = mdb.km->getFunctionId(&mdb.function); if (funcID != bFuncID) { return funcID < bFuncID ? -1 : 1; } diff --git a/lib/Module/Annotation.cpp b/lib/Module/Annotation.cpp index 5c40769054..bfc4b2abf4 100644 --- a/lib/Module/Annotation.cpp +++ b/lib/Module/Annotation.cpp @@ -1,123 +1,220 @@ -#include "klee/Module/Annotation.h" +//===-- Annotation.cpp ----------------------------------------------------===// +// +// The KLEEF Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +//===----------------------------------------------------------------------===// +#include "klee/Module/Annotation.h" #include "klee/Support/ErrorHandling.h" #include - -namespace { - -using namespace klee; - -Annotation::StatementPtr toStatement(const std::string &name, - const std::string &str) { - if (name == "Deref") { - return std::make_shared(str); - } else if (name == "InitNull") { - return std::make_shared(str); - } else { - return std::make_shared(str); - } -} - -} // namespace +#include namespace klee { -Annotation::StatementUnknown::StatementUnknown(const std::string &str) - : statementStr(str) { - parseOnlyOffset(str); +static inline std::string toLower(const std::string &str) { + std::string strLower; + strLower.reserve(str.size()); + std::transform(str.begin(), str.end(), std::back_inserter(strLower), tolower); + return strLower; } -Annotation::StatementUnknown::~StatementUnknown() = default; +namespace Statement { -Annotation::StatementKind -Annotation::StatementUnknown::getStatementName() const { - return Annotation::StatementKind::Unknown; -} +Unknown::Unknown(const std::string &str) { + { + const size_t firstColonPos = str.find(':'); + const size_t startOffset = firstColonPos + 1; + const size_t secondColonPos = str.find(':', startOffset); + const size_t offsetLength = (secondColonPos == std::string::npos) + ? std::string::npos + : secondColonPos - startOffset; -bool Annotation::StatementUnknown::operator==( - const Annotation::StatementUnknown &other) const { - return (statementStr == other.statementStr) && (offset == other.offset); -} + rawAnnotation = str.substr(0, firstColonPos); + if (firstColonPos == std::string::npos) { + return; + } + rawOffset = str.substr(startOffset, offsetLength); + if (secondColonPos != std::string::npos) { + rawValue = str.substr(secondColonPos + 1, std::string::npos); + } + } -void Annotation::StatementUnknown::parseOffset(const std::string &offsetStr) { - size_t pos = 0; - while (pos < offsetStr.size()) { - if (offsetStr[pos] == '*') { + for (size_t pos = 0; pos < rawOffset.size(); pos++) { + switch (rawOffset[pos]) { + case '*': { offset.emplace_back("*"); - pos++; - } else if (offsetStr[pos] == '&') { + break; + } + case '&': { offset.emplace_back("&"); - pos++; - } else if (offsetStr[pos] == '[') { - size_t posEndExpr = offsetStr.find(']', pos); + break; + } + case '[': { + size_t posEndExpr = rawOffset.find(']', pos); if (posEndExpr == std::string::npos) { - klee_error("Incorrect annotation offset format."); + klee_error("Annotation: Incorrect offset format \"%s\"", str.c_str()); } - offset.push_back(offsetStr.substr(pos + 1, posEndExpr - 1 - pos)); - pos = posEndExpr + 1; + offset.push_back(rawOffset.substr(pos + 1, posEndExpr - 1 - pos)); + pos = posEndExpr; + break; + } + default: { + klee_warning("Annotation: Incorrect offset format \"%s\"", str.c_str()); + break; + } + } + } +} + +Unknown::~Unknown() = default; + +Kind Unknown::getKind() const { return Kind::Unknown; } + +const std::vector &Unknown::getOffset() const { return offset; } + +std::string Unknown::toString() const { + if (rawValue.empty()) { + if (rawOffset.empty()) { + return rawAnnotation; } else { - klee_error("Incorrect annotation offset format."); + return rawAnnotation + ":" + rawOffset; } } + return rawAnnotation + ":" + rawOffset + ":" + rawValue; } -void Annotation::StatementUnknown::parseOnlyOffset(const std::string &str) { - const size_t delimiterAfterName = str.find(':'); - if (delimiterAfterName == std::string::npos) { - return; - } - const size_t delimiterAfterOffset = str.find(':', delimiterAfterName + 1); - const size_t offsetLength = - (delimiterAfterOffset == std::string::npos) - ? std::string::npos - : delimiterAfterOffset - delimiterAfterName - 1; - parseOffset(str.substr(delimiterAfterName + 1, offsetLength)); +bool Unknown::operator==(const Unknown &other) const { + return this->getKind() == other.getKind() && toString() == other.toString(); } -Annotation::StatementDeref::StatementDeref(const std::string &str) - : StatementUnknown(str) {} +/* + * Format: {kind}:{offset}:{data} + * Example: InitNull:*[5]: + */ + +Deref::Deref(const std::string &str) : Unknown(str) {} + +Kind Deref::getKind() const { return Kind::Deref; } -Annotation::StatementKind Annotation::StatementDeref::getStatementName() const { - return Annotation::StatementKind::Deref; +InitNull::InitNull(const std::string &str) : Unknown(str) {} + +Kind InitNull::getKind() const { return Kind::InitNull; } + +MaybeInitNull::MaybeInitNull(const std::string &str) : Unknown(str) {} + +Kind MaybeInitNull::getKind() const { return Kind::MaybeInitNull; } + +Alloc::Alloc(const std::string &str) : Unknown(str) { + if (!std::all_of(rawValue.begin(), rawValue.end(), isdigit)) { + klee_error("Annotation: Incorrect value format \"%s\"", rawValue.c_str()); + } + if (!rawValue.empty()) { + value = static_cast(std::stoi(rawValue)); + } } -Annotation::StatementInitNull::StatementInitNull(const std::string &str) - : StatementUnknown(str) {} +Kind Alloc::getKind() const { return Kind::AllocSource; } -Annotation::StatementKind -Annotation::StatementInitNull::getStatementName() const { - return Annotation::StatementKind::InitNull; +Free::Free(const std::string &str) : Unknown(str) { + if (!std::all_of(rawValue.begin(), rawValue.end(), isdigit)) { + klee_error("Annotation: Incorrect value format \"%s\"", rawValue.c_str()); + } + if (!rawValue.empty()) { + value = static_cast(std::stoi(rawValue)); + } } -bool Annotation::operator==(const Annotation &other) const { - return (functionName == other.functionName) && - (statements == other.statements) && (properties == other.properties); +Kind Free::getKind() const { return Kind::Free; } + +const std::map StringToKindMap = { + {"deref", Statement::Kind::Deref}, + {"initnull", Statement::Kind::InitNull}, + {"maybeinitnull", Statement::Kind::MaybeInitNull}, + {"allocsource", Statement::Kind::AllocSource}, + {"freesource", Statement::Kind::Free}, + {"freesink", Statement::Kind::Free}}; + +inline Statement::Kind stringToKind(const std::string &str) { + auto it = StringToKindMap.find(toLower(str)); + if (it != StringToKindMap.end()) { + return it->second; + } + return Statement::Kind::Unknown; } -void from_json(const json &j, Annotation::StatementPtr &statement) { +Ptr stringToKindPtr(const std::string &str) { + std::string statementStr = toLower(str.substr(0, str.find(':'))); + switch (stringToKind(statementStr)) { + case Statement::Kind::Unknown: + return std::make_shared(str); + case Statement::Kind::Deref: + return std::make_shared(str); + case Statement::Kind::InitNull: + return std::make_shared(str); + case Statement::Kind::MaybeInitNull: + return std::make_shared(str); + case Statement::Kind::AllocSource: + return std::make_shared(str); + case Statement::Kind::Free: + return std::make_shared(str); + } +} + +const std::map StringToPropertyMap{ + {"deterministic", Property::Deterministic}, + {"noreturn", Property::Noreturn}, +}; + +inline Property stringToProperty(const std::string &str) { + auto it = StringToPropertyMap.find(toLower(str)); + if (it != StringToPropertyMap.end()) { + return it->second; + } + return Property::Unknown; +} + +void from_json(const json &j, Ptr &statement) { if (!j.is_string()) { - klee_error("Incorrect annotation format."); + klee_error("Annotation: Incorrect statement format"); } const std::string jStr = j.get(); - statement = toStatement(jStr.substr(0, jStr.find(':')), jStr); + statement = Statement::stringToKindPtr(jStr); } -void from_json(const json &j, Annotation::Property &property) { +void from_json(const json &j, Property &property) { if (!j.is_string()) { - klee_error("Incorrect properties format in annotations file."); + klee_error("Annotation: Incorrect properties format"); } const std::string jStr = j.get(); - property = Annotation::Property::Unknown; - const auto propertyPtr = toProperties.find(jStr); - if (propertyPtr != toProperties.end()) { + property = Statement::Property::Unknown; + const auto propertyPtr = Statement::StringToPropertyMap.find(jStr); + if (propertyPtr != Statement::StringToPropertyMap.end()) { property = propertyPtr->second; } } -Annotations parseAnnotationsFile(const json &annotationsJson) { - Annotations annotations; +bool operator==(const Statement::Ptr &first, const Statement::Ptr &second) { + if (first->getKind() != second->getKind()) { + return false; + } + + return *first.get() == *second.get(); +} +} // namespace Statement + +bool Annotation::operator==(const Annotation &other) const { + return (functionName == other.functionName) && + (returnStatements == other.returnStatements) && + (argsStatements == other.argsStatements) && + (properties == other.properties); +} + +AnnotationsMap parseAnnotationsJson(const json &annotationsJson) { + AnnotationsMap annotations; for (auto &item : annotationsJson.items()) { Annotation annotation; annotation.functionName = item.key(); @@ -125,51 +222,53 @@ Annotations parseAnnotationsFile(const json &annotationsJson) { const json &j = item.value(); if (!j.is_object() || !j.contains("annotation") || !j.contains("properties")) { - klee_error("Incorrect annotations file format."); + klee_error("Annotation: Incorrect file format"); + } + { + std::vector> allStatements = + j.at("annotation").get>>(); + + if (allStatements.empty()) { + klee_error("Annotation: function \"%s\" should has return", + annotation.functionName.c_str()); + } + annotation.returnStatements = allStatements[0]; + if (std::any_of(allStatements.begin() + 1, allStatements.end(), + [](const std::vector &statements) { + return std::any_of( + statements.begin(), statements.end(), + [](const Statement::Ptr &statement) { + return statement->getKind() == + Statement::Kind::MaybeInitNull; + }); + })) { + klee_error("Annotation: MaybeInitNull can annotate only return value"); + } + annotation.argsStatements = std::vector>( + allStatements.begin() + 1, allStatements.end()); } - annotation.statements = - j.at("annotation").get>(); annotation.properties = - j.at("properties").get>(); + j.at("properties").get>(); annotations[item.key()] = annotation; } return annotations; } -Annotations parseAnnotationsFile(const std::string &path) { +AnnotationsMap parseAnnotations(const std::string &path) { + if (path.empty()) { + return {}; + } std::ifstream annotationsFile(path); if (!annotationsFile.good()) { - klee_error("Opening %s failed.", path.c_str()); + klee_error("Annotation: Opening %s failed.", path.c_str()); } - json annotationsJson = json::parse(annotationsFile, nullptr, false); if (annotationsJson.is_discarded()) { - klee_error("Parsing JSON %s failed.", path.c_str()); - } - - return parseAnnotationsFile(annotationsJson); -} - -bool operator==(const Annotation::StatementPtr &first, - const Annotation::StatementPtr &second) { - if (first->getStatementName() != second->getStatementName()) { - return false; + klee_error("Annotation: Parsing JSON %s failed.", path.c_str()); } - switch (first->getStatementName()) { - case Annotation::StatementKind::Unknown: - return (*dynamic_cast(first.get()) == - *dynamic_cast(second.get())); - case Annotation::StatementKind::Deref: - return (*dynamic_cast(first.get()) == - *dynamic_cast(second.get())); - case Annotation::StatementKind::InitNull: - return (*dynamic_cast(first.get()) == - *dynamic_cast(second.get())); - default: - __builtin_unreachable(); - } + return parseAnnotationsJson(annotationsJson); } } // namespace klee diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index d97b70eb76..7cc873980c 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -266,17 +266,16 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { } else if (ref mockDeterministicSource = dyn_cast(root->source)) { size_t num_args = mockDeterministicSource->args.size(); - std::vector argsHandled(num_args); - std::vector argsSortHandled(num_args); std::vector args(num_args); std::vector argsSort(num_args); for (size_t i = 0; i < num_args; i++) { ref kid = mockDeterministicSource->args[i]; int kidWidth = kid->getWidth(); - argsHandled[i] = construct(kid, &kidWidth); - args[i] = argsHandled[i]; - argsSortHandled[i] = Z3SortHandle(Z3_get_sort(ctx, args[i]), ctx); - argsSort[i] = argsSortHandled[i]; + Z3ASTHandle argsHandle = construct(kid, &kidWidth); + args[i] = argsHandle; + Z3SortHandle z3SortHandle = + Z3SortHandle(Z3_get_sort(ctx, args[i]), ctx); + argsSort[i] = z3SortHandle; } Z3SortHandle domainSort = getBvSort(root->getDomain()); @@ -294,7 +293,7 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { ctx); array_expr = Z3ASTHandle(Z3_mk_app(ctx, func, num_args, args.data()), ctx); - } else { + } else { array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); } @@ -341,11 +340,6 @@ Z3ASTHandle Z3Builder::getArrayForUpdate(const Array *root, const UpdateNode *un) { // Iterate over the update nodes, until we find a cached version of the node, // or no more update nodes remain - if (root->source->isMock()) { - klee_error("Updates applied to mock array %s are not allowed", - root->getName().c_str()); - } - // FIXME: This really needs to be non-recursive. Z3ASTHandle un_expr; std::vector update_nodes; for (; un && !_arr_hash.lookupUpdateNodeExpr(un, un_expr); diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index ef8b5be9f5..e6d10fed10 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -92,11 +92,11 @@ template <> void Z3NodeHandle::dump() const __attribute__((used)); template <> unsigned Z3NodeHandle::hash() __attribute__((used)); // Specialize for Z3_func_decl -template <> inline ::Z3_ast Z3NodeHandle::as_ast() { +template <> inline ::Z3_ast Z3NodeHandle::as_ast() const { return ::Z3_func_decl_to_ast(context, node); } typedef Z3NodeHandle Z3FuncDeclHandle; -template <> void Z3NodeHandle::dump() __attribute__((used)); +template <> void Z3NodeHandle::dump() const __attribute__((used)); // Specialise for Z3_ast template <> inline ::Z3_ast Z3NodeHandle::as_ast() const { diff --git a/runtime/Mocks/models.c b/runtime/Mocks/models.c index ad95634b47..e40b0cfaa0 100644 --- a/runtime/Mocks/models.c +++ b/runtime/Mocks/models.c @@ -1,3 +1,12 @@ +//===-- models.c ----------------------------------------------------------===// +// +// The KLEEF Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #include "stddef.h" extern void klee_make_symbolic(void *array, size_t nbytes, const char *name); @@ -6,7 +15,7 @@ extern void *calloc(size_t num, size_t size); extern void *realloc(void *ptr, size_t new_size); void *__klee_wrapped_malloc(size_t size) { - char retNull; + unsigned char retNull; klee_make_symbolic(&retNull, sizeof(retNull), "retNullMalloc"); if (retNull) { return 0; @@ -16,7 +25,7 @@ void *__klee_wrapped_malloc(size_t size) { } void *__klee_wrapped_calloc(size_t num, size_t size) { - char retNull; + unsigned char retNull; klee_make_symbolic(&retNull, sizeof(retNull), "retNullCalloc"); if (retNull) { return 0; @@ -26,7 +35,7 @@ void *__klee_wrapped_calloc(size_t num, size_t size) { } void *__klee_wrapped_realloc(void *ptr, size_t new_size) { - char retNull; + unsigned char retNull; klee_make_symbolic(&retNull, sizeof(retNull), "retNullRealloc"); if (retNull) { return 0; diff --git a/scripts/kleef b/scripts/kleef index 2dd0bd016d..969b6c4460 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -29,7 +29,7 @@ def klee_options( "--strip-unwanted-calls", # removes llvm.dbg.* instructions, exponentially reduces time on some benchmarks "--delete-dead-loops=false", # without this optimizer removes some code, which decreases coverage "--emit-all-errors", # without this we generate only one test for assertion failures, which decreases coverage - "--mock-all-externals", # this helps for some linux benchmarks, which have unused extern globals. without this flag we will not even start on them. + "--mock-policy=all", # this helps for some linux benchmarks, which have unused extern globals. without this flag we will not even start on them. "--external-calls=all", "--use-forked-solver=false", # "--solver-backend=stp", diff --git a/scripts/run_tests_with_mocks.py b/scripts/run_tests_with_mocks.py index 5843a37ad0..ef5db2def6 100755 --- a/scripts/run_tests_with_mocks.py +++ b/scripts/run_tests_with_mocks.py @@ -3,10 +3,11 @@ # This script builds executable file using initial bitcode file and artifacts produced by KLEE. # To run the script provide all the arguments you want to pass to clang for building executable. # +# NOTE: First argument is path to compiler # NOTE: Pre-last argument should be a path to KLEE output directory which contains redefinitions.txt and externals.ll. # NOTE: Last argument is path to initial bitcode. # -# Example: python3 run_tests_with_mocks.py -I ~/klee/include/ -L ~/klee/build/lib/ -lkleeRuntest klee-last a.bc +# Example: python3 run_tests_with_mocks.py clang -I ~/klee/include/ -L ~/klee/build/lib/ -lkleeRuntest klee-last a.bc # # You can read more about replaying test cases here: http://klee.github.io/tutorials/testing-function/ @@ -19,8 +20,14 @@ filename = os.path.splitext(bitcode)[0] object_file = f'{filename}.o' -sp.run(f'clang -c {bitcode} -o {object_file}', shell=True) +sp.run(f'llc {bitcode} -filetype=obj -o {object_file}', shell=True) sp.run(f'llvm-objcopy {object_file} --redefine-syms {klee_out_dir}/redefinitions.txt', shell=True) -clang_args = ' '.join(sys.argv[1:len(sys.argv) - 2]) -print(f'clang {clang_args} {klee_out_dir}/externals.ll {object_file}') -sp.run(f'clang {clang_args} {klee_out_dir}/externals.ll {object_file}', shell=True) + +externals = f'{klee_out_dir}/externals.o' +sp.run(f'llc {klee_out_dir}/externals.ll -filetype=obj -o {externals}', shell=True) + +compiler = sys.argv[1] +user_args = ' '.join(sys.argv[2:len(sys.argv) - 2]) +command = f'{compiler} {externals} {object_file} {user_args}' +print(command) +sp.run(command, shell=True) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 17723d865f..c7d14ed87e 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -15,6 +15,7 @@ set(LLVM_TOOLS_DIR "${LLVM_TOOLS_BINARY_DIR}") set(LLVMCC "${LLVMCC} -I${CMAKE_SOURCE_DIR}/include") set(LLVMCXX "${LLVMCXX} -I${CMAKE_SOURCE_DIR}/include") set(NATIVE_CC "${CMAKE_C_COMPILER} ${CMAKE_C_FLAGS} -I ${CMAKE_SOURCE_DIR}/include") +set(NATIVE_OBJCOPY "${CMAKE_OBJCOPY}") set(NATIVE_CXX "${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} -I ${CMAKE_SOURCE_DIR}/include") set(TARGET_TRIPLE "${TARGET_TRIPLE}") diff --git a/test/Feature/Annotation/AllocSource.c b/test/Feature/Annotation/AllocSource.c new file mode 100644 index 0000000000..3ac9a1918e --- /dev/null +++ b/test/Feature/Annotation/AllocSource.c @@ -0,0 +1,65 @@ +// REQUIRES: z3 +// RUN: %clang -DAllocSource1 %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/AllocSource.json --mock-policy=all --mock-modeled-functions -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE1 + +// RUN: %clang -DAllocSource2 %s -g -emit-llvm %O0opt -c -o %t2.bc +// RUN: rm -rf %t2.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/AllocSource.json --mock-policy=all --mock-modeled-functions -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE2 + +// RUN: %clang -DAllocSource3 %s -g -emit-llvm %O0opt -c -o %t3.bc +// RUN: rm -rf %t3.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/AllocSource.json --mock-policy=all --mock-modeled-functions -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE3 + +// RUN: %clang -DAllocSource4 %s -g -emit-llvm %O0opt -c -o %t4.bc +// RUN: rm -rf %t4.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/AllocSource.json --mock-policy=all --mock-modeled-functions -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-ALLOCSOURCE4 + +#include + +#ifdef AllocSource1 +void maybeAllocSource1(int *a); +#endif +void maybeAllocSource2(int **a); +int *maybeAllocSource3(); +int **maybeAllocSource4(); + +int main() { + int *a = 0; +#ifdef AllocSource1 + // CHECK-ALLOCSOURCE1: not valid annotation + maybeAllocSource1(a); + // CHECK-ALLOCSOURCE1: ASSERTION FAIL + // CHECK-ALLOCSOURCE1: partially completed paths = 1 + // CHECK-ALLOCSOURCE1: generated tests = 1 +#endif + +#ifdef AllocSource2 + maybeAllocSource2(&a); + // CHECK-NOT-ALLOCSOURCE2: memory error + // CHECK-NOT-ALLOCSOURCE2: ASSERTION FAIL + // CHECK-ALLOCSOURCE2: partially completed paths = 0 + // CHECK-ALLOCSOURCE2: generated tests = 1 +#endif + +#ifdef AllocSource3 + a = maybeAllocSource3(); + // CHECK-NOT-ALLOCSOURCE3 : memory error + // CHECK-NOT-ALLOCSOURCE3: Not Allocated + // CHECK-ALLOCSOURCE3: partially completed paths = 0 + // CHECK-ALLOCSOURCE3: generated tests = 1 +#endif + +#ifdef AllocSource4 + a = *maybeAllocSource4(); + // CHECK-NOT-ALLOCSOURCE4: ASSERTION FAIL + // CHECK-ALLOCSOURCE4 : memory error + // CHECK-ALLOCSOURCE4: partially completed paths = {{[1-9][0-9]*}} + // CHECK-ALLOCSOURCE4: generated tests = {{[1-9][0-9]*}} +#endif + + assert(a != 0 && "Not Allocated"); + *a = 42; + + return 0; +} diff --git a/test/Feature/Annotation/AllocSource.json b/test/Feature/Annotation/AllocSource.json new file mode 100644 index 0000000000..a31051c64d --- /dev/null +++ b/test/Feature/Annotation/AllocSource.json @@ -0,0 +1,40 @@ +{ + "maybeAllocSource1": { + "name": "maybeAllocSource1", + "annotation": [ + [], + [ + "AllocSource::1" + ] + ], + "properties": [] + }, + "maybeAllocSource2": { + "name": "maybeAllocSource2", + "annotation": [ + [], + [ + "AllocSource:*:1" + ] + ], + "properties": [] + }, + "maybeAllocSource3": { + "name": "maybeAllocSource3", + "annotation": [ + [ + "AllocSource::1" + ] + ], + "properties": [] + }, + "maybeAllocSource4": { + "name": "maybeAllocSource4", + "annotation": [ + [ + "AllocSource::1" + ] + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/BrokenAnnotation.json b/test/Feature/Annotation/BrokenAnnotation.json new file mode 100644 index 0000000000..0b5c90598f --- /dev/null +++ b/test/Feature/Annotation/BrokenAnnotation.json @@ -0,0 +1,11 @@ +{ + "maybeDeref1": { + "name": "maybeDeref1", + "annotation": [ + [], + [ + "Deref" + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/Deref.c b/test/Feature/Annotation/Deref.c new file mode 100644 index 0000000000..7a1048f644 --- /dev/null +++ b/test/Feature/Annotation/Deref.c @@ -0,0 +1,104 @@ +// REQUIRES: z3 +// RUN: %clang -DDeref1 %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Deref.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF1 + +// RUN: %clang -DDeref2 %s -g -emit-llvm %O0opt -c -o %t2.bc +// RUN: rm -rf %t2.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/Deref.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF2 + +// RUN: %clang -DDeref3 %s -g -emit-llvm %O0opt -c -o %t3.bc +// RUN: rm -rf %t3.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/Deref.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF3 + +// RUN: %clang -DDeref4 %s -g -emit-llvm %O0opt -c -o %t4.bc +// RUN: rm -rf %t4.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/Deref.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF4 + +// RUN: %clang -DDeref5 %s -g -emit-llvm %O0opt -c -o %t5.bc +// RUN: rm -rf %t5.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/Deref.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF5 + +// RUN: %clang -DDeref6 %s -g -emit-llvm %O0opt -c -o %t6.bc +// RUN: rm -rf %t6.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t6.klee-out-1 --annotations=%S/Deref.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t6.bc 2>&1 | FileCheck %s -check-prefix=CHECK-DEREF6 + +// RUN: %clang -DHASVALUE -DDeref1 -DDeref2 -DDeref3 -DDeref4 -DDeref5 -DDeref6 %s -g -emit-llvm %O0opt -c -o %t7.bc +// RUN: rm -rf %t7.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t7.klee-out-1 --annotations=%S/Deref.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t7.bc 2>&1 | FileCheck %s -check-prefix=CHECK-NODEREF +// CHECK-NODEREF-NOT: memory error: null pointer exception + +// RUN: %clang -DDeref1 -DDeref2 -DDeref3 -DDeref4 -DDeref5 -DDeref6 %s -g -emit-llvm %O0opt -c -o %t8.bc +// RUN: rm -rf %t8.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t8.klee-out-1 --annotations=%S/EmptyAnnotation.json --external-calls=all --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t8.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY +// CHECK-EMPTY-NOT: memory error: null pointer exception +// CHECK-EMPTY: partially completed paths = 0 +// CHECK-EMPTY: generated tests = 1 + +void maybeDeref1(int *a); +void maybeDeref2(int **a); +void maybeDeref3(int **a); +void maybeDeref4(int b, int *a); +void maybeDeref5(int *a, int b); +void maybeDeref6(int *a, int *b); + +int main() { + int c = 42; +#ifdef HASVALUE + int *a = &c; + int **b = &a; +#else + int *a = 0; + int **b = 0; +#endif + +#ifdef Deref1 + // CHECK-DEREF1: memory error: null pointer exception + maybeDeref1(a); + // CHECK-DEREF1: memory error: out of bound pointer + maybeDeref1((int *)42); + // CHECK-DEREF1: partially completed paths = 2 + // CHECK-DEREF1: generated tests = 3 +#endif + +#ifdef Deref2 + // CHECK-DEREF2: memory error: null pointer exception + maybeDeref2(b); + maybeDeref2(&a); + // CHECK-DEREF2: partially completed paths = 1 + // CHECK-DEREF2: generated tests = 3 +#endif + +#ifdef Deref3 + // CHECK-DEREF3: memory error: null pointer exception + maybeDeref3(&a); + // CHECK-DEREF3: memory error: null pointer exception + maybeDeref3(b); + // CHECK-DEREF3: partially completed paths = 2 + // CHECK-DEREF3: generated tests = 2 +#endif + +#ifdef Deref4 + // CHECK-DEREF4: memory error: null pointer exception + maybeDeref4(0, a); + // CHECK-DEREF4: partially completed paths = 1 + // CHECK-DEREF4: generated tests = 2 +#endif + +#ifdef Deref5 + // CHECK-DEREF5: memory error: null pointer exception + maybeDeref5(a, 0); + // CHECK-DEREF5: partially completed paths = 1 + // CHECK-DEREF5: generated tests = 2 +#endif + +#ifdef Deref6 + // CHECK-DEREF6: memory error: null pointer exception + maybeDeref6(a, &c); + // CHECK-DEREF6: memory error: null pointer exception + maybeDeref6(&c, a); + // CHECK-DEREF6: partially completed paths = 2 + // CHECK-DEREF6: generated tests = 3 +#endif + return 0; +} diff --git a/test/Feature/Annotation/Deref.json b/test/Feature/Annotation/Deref.json new file mode 100644 index 0000000000..02ce7ecbc3 --- /dev/null +++ b/test/Feature/Annotation/Deref.json @@ -0,0 +1,67 @@ +{ + "maybeDeref1": { + "name": "maybeDeref1", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "maybeDeref2": { + "name": "maybeDeref2", + "annotation": [ + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "maybeDeref3": { + "name": "maybeDeref3", + "annotation": [ + [], + [ + "Deref:*" + ] + ], + "properties": [] + }, + "maybeDeref4": { + "name": "maybeDeref4", + "annotation": [ + [], + [], + [ + "Deref" + ] + ], + "properties": [] + }, + "maybeDeref5": { + "name": "maybeDeref5", + "annotation": [ + [], + [ + "Deref" + ], + [] + ], + "properties": [] + }, + "maybeDeref6": { + "name": "maybeDeref6", + "annotation": [ + [], + [ + "Deref" + ], + [ + "Deref" + ] + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/EmptyAnnotation.json b/test/Feature/Annotation/EmptyAnnotation.json new file mode 100644 index 0000000000..0967ef424b --- /dev/null +++ b/test/Feature/Annotation/EmptyAnnotation.json @@ -0,0 +1 @@ +{} diff --git a/test/Feature/Annotation/Free.c b/test/Feature/Annotation/Free.c new file mode 100644 index 0000000000..22614bf8f5 --- /dev/null +++ b/test/Feature/Annotation/Free.c @@ -0,0 +1,45 @@ +// REQUIRES: z3 +// RUN: %clang -DFree1 %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/Free.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE1 + +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t2.bc +// RUN: rm -rf %t2.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/Free.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE2 + +// RUN: %clang -DFree3 %s -g -emit-llvm %O0opt -c -o %t3.bc +// RUN: rm -rf %t3.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/Free.json --mock-policy=all --mock-modeled-functions --emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-FREE3 + +#include + +int *maybeAllocSource1(); +void maybeFree1(int *a); + +int main() { + int *a; +#ifdef Free1 + // CHECK-FREE1: memory error: invalid pointer: free + // CHECK-FREE1: KLEE: done: completed paths = 1 + // CHECK-FREE1: KLEE: done: partially completed paths = 1 + // CHECK-FREE1: KLEE: done: generated tests = 2 + a = malloc(sizeof(int)); + maybeFree1(a); + maybeFree1(a); +#endif + + a = maybeAllocSource1(); + maybeFree1(a); + // CHECK-NOT-FREE2: memory error: invalid pointer: free + // CHECK-FREE2: KLEE: done: completed paths = 1 + // CHECK-FREE2: KLEE: done: partially completed paths = 0 + // CHECK-FREE2: KLEE: done: generated tests = 1 +#ifdef Free3 + // CHECK-FREE3: memory error: invalid pointer: free + // CHECK-FREE3: KLEE: done: completed paths = 0 + // CHECK-FREE3: KLEE: done: partially completed paths = 1 + // CHECK-FREE3: KLEE: done: generated tests = 1 + maybeFree1(a); +#endif + return 0; +} diff --git a/test/Feature/Annotation/Free.json b/test/Feature/Annotation/Free.json new file mode 100644 index 0000000000..d8a9becf9d --- /dev/null +++ b/test/Feature/Annotation/Free.json @@ -0,0 +1,31 @@ +{ + "maybeFree1": { + "name": "maybeFree1", + "annotation": [ + [], + [ + "FreeSink::1" + ] + ], + "properties": [] + }, + "maybeFree2": { + "name": "maybeFree2", + "annotation": [ + [], + [ + "FreeSink:*:1" + ] + ], + "properties": [] + }, + "maybeAllocSource1": { + "name": "maybeAllocSource1", + "annotation": [ + [ + "AllocSource::1" + ] + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/General.c b/test/Feature/Annotation/General.c new file mode 100644 index 0000000000..a642919f2b --- /dev/null +++ b/test/Feature/Annotation/General.c @@ -0,0 +1,43 @@ +// REQUIRES: z3 +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/BrokenAnnotation.json --mock-policy=all -emit-all-errors=true %t1.bc 2>%t.stderr.log || echo "Exit status must be 0" +// RUN: FileCheck -check-prefix=CHECK-JSON --input-file=%t.stderr.log %s +// CHECK-JSON: Annotation: Parsing JSON + +// RUN: %clang -DPTRARG %s -g -emit-llvm %O0opt -c -o %t2.bc +// RUN: rm -rf %t2.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/General.json --mock-policy=all -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK + +// RUN: %clang -DPTRRET %s -g -emit-llvm %O0opt -c -o %t3.bc +// RUN: rm -rf %t3.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/General.json --mock-policy=all -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK + +#include + +struct ST { + int a; + int b; +}; + +void ptrArg(struct ST, int **a); +int *ptrRet(); + +int main() { + int *a = 15; +#ifdef PTRARG + struct ST st; + ptrArg(st, &a); +#endif + +#ifdef PTRRET + a = ptrRet(); +#endif + + // CHECK: memory error: null pointer exception + // CHECK: partially completed paths = 1 + // CHECK: generated tests = 2 + *a = 42; + + return 0; +} diff --git a/test/Feature/Annotation/General.json b/test/Feature/Annotation/General.json new file mode 100644 index 0000000000..65cffd2fbf --- /dev/null +++ b/test/Feature/Annotation/General.json @@ -0,0 +1,24 @@ +{ + "ptrArg": { + "name": "ptrArg", + "annotation": [ + [], + [], + [ + "InitNull:*", + "AllocSource:*:1" + ] + ], + "properties": [] + }, + "ptrRet": { + "name": "ptrRet", + "annotation": [ + [ + "MaybeInitNull", + "AllocSource::1" + ] + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/InitNull.c b/test/Feature/Annotation/InitNull.c new file mode 100644 index 0000000000..ff7e152c71 --- /dev/null +++ b/test/Feature/Annotation/InitNull.c @@ -0,0 +1,79 @@ +// REQUIRES: z3 +// RUN: %clang -DInitNull1 %s -g -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t1.klee-out-1 --annotations=%S/InitNull.json --mock-policy=all -emit-all-errors=true %t1.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL1 + +// RUN: %clang -DInitNull2 %s -g -emit-llvm %O0opt -c -o %t2.bc +// RUN: rm -rf %t2.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t2.klee-out-1 --annotations=%S/InitNull.json --mock-policy=all -emit-all-errors=true %t2.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL2 + +// RUN: %clang -DInitNull3 %s -g -emit-llvm %O0opt -c -o %t3.bc +// RUN: rm -rf %t3.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t3.klee-out-1 --annotations=%S/InitNull.json --mock-policy=all -emit-all-errors=true %t3.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL3 + +// RUN: %clang -DInitNull4 %s -g -emit-llvm %O0opt -c -o %t4.bc +// RUN: rm -rf %t4.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t4.klee-out-1 --annotations=%S/InitNull.json --mock-policy=all -emit-all-errors=true %t4.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL4 + +// RUN: %clang -DInitNull1 -DInitNull2 -DInitNull3 -DInitNull4 %s -g -emit-llvm %O0opt -c -o %t5.bc +// RUN: rm -rf %t5.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t5.klee-out-1 --annotations=%S/InitNullEmpty.json --mock-policy=all -emit-all-errors=true %t5.bc 2>&1 | FileCheck %s -check-prefix=CHECK-EMPTY +// CHECK-EMPTY: ASSERTION FAIL +// CHECK-EMPTY: partially completed paths = {{[1-2]}} + +// RUN: %clang -DMustInitNull5 %s -g -emit-llvm %O0opt -c -o %t6.bc +// RUN: rm -rf %t6.klee-out-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t6.klee-out-1 --annotations=%S/InitNull.json --mock-policy=all -emit-all-errors=true %t6.bc 2>&1 | FileCheck %s -check-prefix=CHECK-INITNULL5 + +#include + +#ifdef InitNull1 +void mustInitNull1(int *a); +#endif +void mustInitNull2(int **a); +int *maybeInitNull1(); +int **maybeInitNull2(); + +int *mustInitNull3(); + +int main() { + int c = 42; + int *a = &c; +#ifdef InitNull1 + // CHECK-INITNULL1: not valid annotation + mustInitNull1(a); + // CHECK-INITNULL1-NOT: A is Null + // CHECK-INITNULL1: partially completed paths = 0 + // CHECK-INITNULL1: generated tests = 1 +#endif + +#ifdef InitNull2 + mustInitNull2(&a); + // CHECK-INITNULL2: ASSERTION FAIL + // CHECK-INITNULL2: partially completed paths = 1 + // CHECK-INITNULL2: generated tests = 2 +#endif + +#ifdef InitNull3 + a = maybeInitNull1(); + // CHECK-INITNULL3: ASSERTION FAIL + // CHECK-INITNULL3: partially completed paths = 1 + // CHECK-INITNULL3: generated tests = 2 +#endif + +#ifdef InitNull4 + a = *maybeInitNull2(); + // CHECK-INITNULL4: ASSERTION FAIL + // CHECK-INITNULL4: partially completed paths = {{[2-3]}} +#endif + +#ifdef MustInitNull5 + a = mustInitNull3(); + // CHECK-INITNULL5: partially completed paths = 0 + // CHECK-INITNULL5: generated tests = 2 +#else + assert(a != 0 && "A is Null"); +#endif + + return 0; +} diff --git a/test/Feature/Annotation/InitNull.json b/test/Feature/Annotation/InitNull.json new file mode 100644 index 0000000000..270c7f01d1 --- /dev/null +++ b/test/Feature/Annotation/InitNull.json @@ -0,0 +1,49 @@ +{ + "mustInitNull1": { + "name": "maybeInitNull1", + "annotation": [ + [], + [ + "InitNull" + ] + ], + "properties": [] + }, + "mustInitNull2": { + "name": "maybeInitNull2", + "annotation": [ + [], + [ + "InitNull:*" + ] + ], + "properties": [] + }, + "maybeInitNull1": { + "name": "maybeInitNull1", + "annotation": [ + [ + "MaybeInitNull" + ] + ], + "properties": [] + }, + "maybeInitNull2": { + "name": "maybeInitNull2", + "annotation": [ + [ + "MaybeInitNull:*" + ] + ], + "properties": [] + }, + "mustInitNull3": { + "name": "mustInitNull3", + "annotation": [ + [ + "InitNull" + ] + ], + "properties": [] + } +} diff --git a/test/Feature/Annotation/InitNullEmpty.json b/test/Feature/Annotation/InitNullEmpty.json new file mode 100644 index 0000000000..535d0a767b --- /dev/null +++ b/test/Feature/Annotation/InitNullEmpty.json @@ -0,0 +1,32 @@ +{ + "maybeInitNull1": { + "name": "maybeInitNull1", + "annotation": [ + [], + [] + ], + "properties": [] + }, + "maybeInitNull2": { + "name": "maybeInitNull2", + "annotation": [ + [], + [] + ], + "properties": [] + }, + "maybeInitNull3": { + "name": "maybeInitNull3", + "annotation": [ + [] + ], + "properties": [] + }, + "maybeInitNull4": { + "name": "maybeInitNull4", + "annotation": [ + [] + ], + "properties": [] + } +} diff --git a/test/Feature/MockPointersDeterministic.c b/test/Feature/MockPointersDeterministic.c index d8c871588d..03a2480850 100644 --- a/test/Feature/MockPointersDeterministic.c +++ b/test/Feature/MockPointersDeterministic.c @@ -2,8 +2,9 @@ // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out-1 -// RUN: %klee --solver-backend=z3 --output-dir=%t.klee-out-1 --skip-not-lazy-initialized --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 +// RUN: %klee --solver-backend=z3 --output-dir=%t.klee-out-1 --min-number-elements-li=0 --use-sym-size-li --skip-not-lazy-initialized --mock-policy=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 // CHECK-1: memory error: null pointer exception +// CHECK-1: memory error: out of bound pointer // CHECK-1: KLEE: done: completed paths = 1 // CHECK-1: KLEE: done: partially completed paths = 2 // CHECK-1: KLEE: done: generated tests = 3 @@ -20,4 +21,4 @@ int main() { assert(0 && "age is deterministic"); } return *age(); -} \ No newline at end of file +} diff --git a/test/Feature/MockStrategies.c b/test/Feature/MockStrategies.c index 524fbba3a2..d8998cfe54 100644 --- a/test/Feature/MockStrategies.c +++ b/test/Feature/MockStrategies.c @@ -2,23 +2,23 @@ // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out-1 -// RUN: %klee --output-dir=%t.klee-out-1 --external-calls=all --mock-strategy=none %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 +// RUN: %klee --output-dir=%t.klee-out-1 --external-calls=all %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-1 // CHECK-1: failed external call // CHECK-1: KLEE: done: completed paths = 1 // CHECK-1: KLEE: done: generated tests = 2 // RUN: rm -rf %t.klee-out-2 -// RUN: %klee --output-dir=%t.klee-out-2 --external-calls=all --mock-strategy=naive %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-2 -// CHECK-2: ASSERTION FAIL: 0 +// RUN: %klee --output-dir=%t.klee-out-2 --mock-policy=all %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-2 +// CHECK-2: ASSERTION FAIL // CHECK-2: KLEE: done: completed paths = 2 // CHECK-2: KLEE: done: generated tests = 3 // RUN: rm -rf %t.klee-out-3 -// RUN: not %klee --output-dir=%t.klee-out-3 --solver-backend=stp --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-3 +// RUN: not %klee --output-dir=%t.klee-out-3 --solver-backend=stp --mock-policy=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-3 // CHECK-3: KLEE: ERROR: Deterministic mocks can be generated with Z3 solver only. // RUN: rm -rf %t.klee-out-4 -// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4 +// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --mock-policy=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4 // CHECK-4: KLEE: done: completed paths = 2 // CHECK-4: KLEE: done: generated tests = 2 diff --git a/test/Industry/AssignNull_Scene_BadCase02.c b/test/Industry/AssignNull_Scene_BadCase02.c index 55fb4b7989..e8e25bfbe9 100644 --- a/test/Industry/AssignNull_Scene_BadCase02.c +++ b/test/Industry/AssignNull_Scene_BadCase02.c @@ -51,6 +51,6 @@ void TestBad5(struct STU *pdev, const char *buf, unsigned int count) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -// CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 2 \ No newline at end of file +// CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 2 diff --git a/test/Industry/AssignNull_Scene_BadCase04.c b/test/Industry/AssignNull_Scene_BadCase04.c index 6a0979278f..272894d73f 100644 --- a/test/Industry/AssignNull_Scene_BadCase04.c +++ b/test/Industry/AssignNull_Scene_BadCase04.c @@ -52,5 +52,5 @@ int TestBad7(char *arg, unsigned int count) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --smart-resolve-entry-function --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --smart-resolve-entry-function --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/BadCase01_SecB_ForwardNull.c b/test/Industry/BadCase01_SecB_ForwardNull.c index d554a1535b..80b17cbf9b 100644 --- a/test/Industry/BadCase01_SecB_ForwardNull.c +++ b/test/Industry/BadCase01_SecB_ForwardNull.c @@ -142,6 +142,6 @@ void badbad(char *ptr) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc > %t1.log 2>&1 +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc > %t1.log 2>&1 // RUN: FileCheck -input-file=%t1.log %s // CHECK: KLEE: WARNING: No paths were given to trace verify diff --git a/test/Industry/CheckNull_Scene_BadCase02.c b/test/Industry/CheckNull_Scene_BadCase02.c index 3effb46f57..3f19d9b621 100644 --- a/test/Industry/CheckNull_Scene_BadCase02.c +++ b/test/Industry/CheckNull_Scene_BadCase02.c @@ -43,5 +43,5 @@ void TestBad2() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/CheckNull_Scene_BadCase04.c b/test/Industry/CheckNull_Scene_BadCase04.c index 0e9038201d..179fd1419d 100644 --- a/test/Industry/CheckNull_Scene_BadCase04.c +++ b/test/Industry/CheckNull_Scene_BadCase04.c @@ -58,5 +58,5 @@ void TestBad12(int cond1, int cond2) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c index a3846f9ec0..37524f9b99 100644 --- a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c +++ b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc +// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-policy=all --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc // RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage diff --git a/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c b/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c index 5e7399e6ee..104daa6402 100644 --- a/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c +++ b/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc +// RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-policy=all --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc // RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage diff --git a/test/Industry/FN_SecB_ForwardNull_filed.c b/test/Industry/FN_SecB_ForwardNull_filed.c index 6faaf136b9..e4d507692e 100644 --- a/test/Industry/FN_SecB_ForwardNull_filed.c +++ b/test/Industry/FN_SecB_ForwardNull_filed.c @@ -47,5 +47,5 @@ void WB_BadCase_field2(DataInfo *data) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc -// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s \ No newline at end of file +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c b/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c index 9a04367627..58a19a6d5c 100644 --- a/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c +++ b/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c @@ -55,7 +55,7 @@ void call_func(int num) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --write-kqueries --max-cycles-before-stuck=0 --use-guided-search=error --check-out-of-memory --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --write-kqueries --max-cycles-before-stuck=0 --use-guided-search=error --annotations=%annotations --mock-policy=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable at trace 1 diff --git a/test/Industry/NullReturn_BadCase_WhiteBox01.c b/test/Industry/NullReturn_BadCase_WhiteBox01.c index 666c470216..0f0ab116e2 100644 --- a/test/Industry/NullReturn_BadCase_WhiteBox01.c +++ b/test/Industry/NullReturn_BadCase_WhiteBox01.c @@ -66,5 +66,5 @@ void NullReturn_BadCase_WhiteBox01(UINT8 index, SchedHarqStru *harqInfo) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --smart-resolve-entry-function --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc -// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s \ No newline at end of file +// RUN: %klee --output-dir=%t.klee-out --smart-resolve-entry-function --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/NullReturn_Scene_BadCase01.c b/test/Industry/NullReturn_Scene_BadCase01.c index 45b8240318..b31fb67f34 100644 --- a/test/Industry/NullReturn_Scene_BadCase01.c +++ b/test/Industry/NullReturn_Scene_BadCase01.c @@ -41,5 +41,5 @@ void TestBad1() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --external-calls=all --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --external-calls=all --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/NullReturn_Scene_BadCase02.c b/test/Industry/NullReturn_Scene_BadCase02.c index d25af79653..c3a9099c04 100644 --- a/test/Industry/NullReturn_Scene_BadCase02.c +++ b/test/Industry/NullReturn_Scene_BadCase02.c @@ -40,5 +40,5 @@ void TestBad2() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --mock-external-calls --check-out-of-memory --skip-not-symbolic-objects --skip-not-lazy-initialized --extern-calls-can-return-null --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --annotations=%annotations --mock-policy=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/NullReturn_Scene_BadCase03.c b/test/Industry/NullReturn_Scene_BadCase03.c index c4190f9bb2..30d8a0d007 100644 --- a/test/Industry/NullReturn_Scene_BadCase03.c +++ b/test/Industry/NullReturn_Scene_BadCase03.c @@ -42,5 +42,5 @@ void TestBad3() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/NullReturn_Scene_BadCase04.c b/test/Industry/NullReturn_Scene_BadCase04.c index 377e4b9e19..f2fca4e757 100644 --- a/test/Industry/NullReturn_Scene_BadCase04.c +++ b/test/Industry/NullReturn_Scene_BadCase04.c @@ -46,6 +46,6 @@ void TestBad4() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --check-out-of-memory --mock-external-calls --libc=klee --external-calls=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --check-out-of-memory --annotations=%annotations --mock-policy=all --libc=klee --external-calls=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -// CHEK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1 \ No newline at end of file +// CHEK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1 diff --git a/test/Industry/NullReturn_Scene_BadCase06.c b/test/Industry/NullReturn_Scene_BadCase06.c index 19b11d341b..8fbac9c0d7 100644 --- a/test/Industry/NullReturn_Scene_BadCase06.c +++ b/test/Industry/NullReturn_Scene_BadCase06.c @@ -54,7 +54,7 @@ void TestBad6(unsigned int count) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --check-out-of-memory --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s // CHECK-DAG: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1 diff --git a/test/Industry/NullReturn_Scene_BadCase08.cpp b/test/Industry/NullReturn_Scene_BadCase08.cpp index 91e6dccdf8..d066fdc474 100644 --- a/test/Industry/NullReturn_Scene_BadCase08.cpp +++ b/test/Industry/NullReturn_Scene_BadCase08.cpp @@ -39,6 +39,6 @@ void TestBad9() // RUN: %clangxx %s -emit-llvm %O0opt -c -g -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --write-kqueries --use-guided-search=error --location-accuracy --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --write-kqueries --use-guided-search=error --location-accuracy --annotations=%annotations --mock-policy=failed --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s // CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 2 \ No newline at end of file diff --git a/test/Industry/SecB_ForwardNull.c b/test/Industry/SecB_ForwardNull.c index e3a8334c82..522e1e6fe4 100644 --- a/test/Industry/SecB_ForwardNull.c +++ b/test/Industry/SecB_ForwardNull.c @@ -131,5 +131,5 @@ void badbad(char *ptr) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc -// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s \ No newline at end of file +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/UseAfterFree/Double_Free_BadCase01.c b/test/Industry/UseAfterFree/Double_Free_BadCase01.c index 57d3600faa..34420ba6ee 100644 --- a/test/Industry/UseAfterFree/Double_Free_BadCase01.c +++ b/test/Industry/UseAfterFree/Double_Free_BadCase01.c @@ -38,5 +38,5 @@ void DoubleFreeBad01() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/UseAfterFree/Double_Free_BadCase02.c b/test/Industry/UseAfterFree/Double_Free_BadCase02.c index be8f1c52c1..f048ea3234 100644 --- a/test/Industry/UseAfterFree/Double_Free_BadCase02.c +++ b/test/Industry/UseAfterFree/Double_Free_BadCase02.c @@ -41,5 +41,5 @@ void DoubleFreeBad02(int flag) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp b/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp index 90a32d9903..9a6d3fdb5b 100644 --- a/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp +++ b/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp @@ -77,7 +77,7 @@ int main() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s // CHECK: KLEE: WARNING: 100.00% UseAfterFree False Positive at trace 1 diff --git a/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c b/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c index 7742d31afd..a8e08c302b 100644 --- a/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c +++ b/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c @@ -35,5 +35,5 @@ void UseAfterFree() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/ZeroDeref_Scene_BadCase02.c b/test/Industry/ZeroDeref_Scene_BadCase02.c index dd0fe063ac..31ac93948c 100644 --- a/test/Industry/ZeroDeref_Scene_BadCase02.c +++ b/test/Industry/ZeroDeref_Scene_BadCase02.c @@ -40,5 +40,5 @@ void TestBad9() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/ZeroDeref_Scene_BadCase05.c b/test/Industry/ZeroDeref_Scene_BadCase05.c index 3afb67837e..f531cf719c 100644 --- a/test/Industry/ZeroDeref_Scene_BadCase05.c +++ b/test/Industry/ZeroDeref_Scene_BadCase05.c @@ -64,7 +64,7 @@ void TestBad18(struct STU *stu) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --check-out-of-memory --mock-external-calls --libc=klee --external-calls=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --check-out-of-memory --annotations=%annotations --mock-policy=all --libc=klee --external-calls=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s // CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 2 -// CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 1 \ No newline at end of file +// CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 1 diff --git a/test/Industry/egcd3-ll_valuebound10.c b/test/Industry/egcd3-ll_valuebound10.c index bc6c06f982..aa563ed00a 100644 --- a/test/Industry/egcd3-ll_valuebound10.c +++ b/test/Industry/egcd3-ll_valuebound10.c @@ -1,7 +1,7 @@ // REQUIRES: not-darwin, not-san // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc +// RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-policy=all --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc // RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage diff --git a/test/Industry/fn_reverse_null.c b/test/Industry/fn_reverse_null.c index aff52b8f68..630ac76e28 100644 --- a/test/Industry/fn_reverse_null.c +++ b/test/Industry/fn_reverse_null.c @@ -55,5 +55,5 @@ void TestErr4(TreeNode *head) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --external-calls=all --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --external-calls=all --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/fp_forward_null_address.c b/test/Industry/fp_forward_null_address.c index e090051722..b875cce44d 100644 --- a/test/Industry/fp_forward_null_address.c +++ b/test/Industry/fp_forward_null_address.c @@ -24,5 +24,5 @@ void foo() // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --max-cycles-before-stuck=150 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --max-cycles-before-stuck=150 --use-guided-search=error --annotations=%annotations --mock-policy=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/fp_null_returns_self_define.c b/test/Industry/fp_null_returns_self_define.c index fa331108b6..6329a45238 100644 --- a/test/Industry/fp_null_returns_self_define.c +++ b/test/Industry/fp_null_returns_self_define.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s #include diff --git a/test/Industry/fp_null_returns_self_define2.c b/test/Industry/fp_null_returns_self_define2.c index 6606140676..551e7aed67 100644 --- a/test/Industry/fp_null_returns_self_define2.c +++ b/test/Industry/fp_null_returns_self_define2.c @@ -28,5 +28,5 @@ void TEST_NullReturns004(unsigned short index) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s diff --git a/test/Industry/if2.c b/test/Industry/if2.c index 57422bf2d5..b6ef8b0982 100644 --- a/test/Industry/if2.c +++ b/test/Industry/if2.c @@ -10,7 +10,7 @@ int main(int x) { // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-instructions=45 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-instructions=45 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 50.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out/messages.txt %s -check-prefix=CHECK-DISTANCE diff --git a/test/Industry/test.c b/test/Industry/test.c index 5b08e0cd97..500ab31738 100644 --- a/test/Industry/test.c +++ b/test/Industry/test.c @@ -21,8 +21,8 @@ void TestBad8(int len) // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NUM // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.sarif %t1.bc +// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.sarif %t1.bc // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-UID diff --git a/test/Industry/while_true.c b/test/Industry/while_true.c index 72aac7f704..ffbf90e30b 100644 --- a/test/Industry/while_true.c +++ b/test/Industry/while_true.c @@ -10,14 +10,14 @@ int main() { // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out-1 -// RUN: %klee --output-dir=%t.klee-out-1 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=20 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out-1 --use-guided-search=error --mock-policy=failed --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=20 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out-1/warnings.txt %s -check-prefix=CHECK-NONE // CHECK-NONE: KLEE: WARNING: 0.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out-1/messages.txt %s -check-prefix=CHECK-REACH-1 // CHECK-REACH-1: (0, 1, 4) for Target 1: error in function main (lines 8 to 8) // RUN: rm -rf %t.klee-out-2 -// RUN: %klee --output-dir=%t.klee-out-2 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=4980 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc +// RUN: %klee --output-dir=%t.klee-out-2 --use-guided-search=error --mock-policy=failed --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=4980 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc // RUN: FileCheck -input-file=%t.klee-out-2/warnings.txt %s -check-prefix=CHECK-ALL // CHECK-ALL: KLEE: WARNING: 99.00% NullPointerException False Positive at trace 1 // RUN: FileCheck -input-file=%t.klee-out-2/messages.txt %s -check-prefix=CHECK-REACH-2 diff --git a/test/Replay/libkleeruntest/replay_mocks.c b/test/Replay/libkleeruntest/replay_mocks.c index cfd151a9e5..615bea931b 100644 --- a/test/Replay/libkleeruntest/replay_mocks.c +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -1,12 +1,19 @@ // REQUIRES: geq-llvm-11.0 +// REQUIRES: not-darwin // RUN: %clang %s -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --external-calls=all --mock-strategy=naive %t.bc -// RUN: %clang -c %t.bc -o %t.o -// RUN: %llvmobjcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o -// RUN: %clang -o %t.klee-out/a.out %libkleeruntest %t.klee-out/externals.ll %t.o +// RUN: %klee --output-dir=%t.klee-out --mock-policy=all %t.bc + +// RUN: %llc %t.bc -filetype=obj -o %t.o +// RUN: %llc %t.klee-out/externals.ll -filetype=obj -o %t_externals.o +// RUN: %objcopy --redefine-syms %t.klee-out/redefinitions.txt %t.o +// RUN: %cc -no-pie %t_externals.o %t.o %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner +// RUN: test -f %t.klee-out/test000001.ktest +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner + +// RUN: %runmocks %cc -no-pie %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner2 %t.klee-out %t.bc // RUN: test -f %t.klee-out/test000001.ktest -// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t.klee-out/a.out +// RUN: env KTEST_FILE=%t.klee-out/test000001.ktest %t_runner2 extern int variable; @@ -15,5 +22,6 @@ extern int foo(int); int main() { int a; klee_make_symbolic(&a, sizeof(a), "a"); - return variable + foo(a); + a = variable + foo(a); + return 0; } diff --git a/test/Solver/sina2f.c b/test/Solver/sina2f.c index 628a8e0e8b..c732bf2ddb 100644 --- a/test/Solver/sina2f.c +++ b/test/Solver/sina2f.c @@ -3,7 +3,7 @@ // REQUIRES: not-msan // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --strip-unwanted-calls --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --solver-backend=bitwuzla-tree --max-solvers-approx-tree-inc=16 --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=false --output-istats=false --use-sym-size-alloc=true --cex-cache-validity-cores --fp-runtime --x86FP-as-x87FP80 --symbolic-allocation-threshold=8192 --allocate-determ --allocate-determ-size=3072 --allocate-determ-start-address=0x00030000000 --mem-trigger-cof --use-alpha-equivalence=true --track-coverage=all --use-iterative-deepening-search=max-cycles --max-solver-time=5s --max-cycles-before-stuck=15 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state --cover-on-the-fly=true --delay-cover-on-the-fly=27 --max-time=29 %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --strip-unwanted-calls --delete-dead-loops=false --emit-all-errors --mock-policy=all --use-forked-solver=false --solver-backend=bitwuzla-tree --max-solvers-approx-tree-inc=16 --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=false --output-istats=false --use-sym-size-alloc=true --cex-cache-validity-cores --fp-runtime --x86FP-as-x87FP80 --symbolic-allocation-threshold=8192 --allocate-determ --allocate-determ-size=3072 --allocate-determ-start-address=0x00030000000 --mem-trigger-cof --use-alpha-equivalence=true --track-coverage=all --use-iterative-deepening-search=max-cycles --max-solver-time=5s --max-cycles-before-stuck=15 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state --cover-on-the-fly=true --delay-cover-on-the-fly=27 --max-time=29 %t1.bc 2>&1 | FileCheck %s #include "klee-test-comp.c" /* diff --git a/test/lit.cfg b/test/lit.cfg index 72144bfe1e..79f071b5c0 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -90,7 +90,7 @@ if config.test_exec_root is None: # Add substitutions from lit.site.cfg -subs = [ 'clangxx', 'clang', 'cc', 'cxx', 'O0opt', 'c_prefixes_8', 'c_prefixes_10', 'cpp_prefixes_10' ] +subs = [ 'clangxx', 'clang', 'cc', 'objcopy', 'cxx', 'O0opt', 'c_prefixes_8', 'c_prefixes_10', 'cpp_prefixes_10' ] for name in subs: value = getattr(config, name, None) if value == None: @@ -105,6 +105,12 @@ config.substitutions.append( config.substitutions.append( ('%lli', os.path.join(llvm_tools_dir, 'lli')) ) + +# Add a substitution for llc. +config.substitutions.append( + ('%llc', os.path.join(llvm_tools_dir, 'llc')) +) + # Add a substitution for llvm-as config.substitutions.append( ('%llvmas', os.path.join(llvm_tools_dir, 'llvm-as')) @@ -179,6 +185,10 @@ config.substitutions.append( ('%replay', os.path.join(klee_src_root, 'scripts/replay.sh')) ) +config.substitutions.append( + ('%annotations', os.path.join(klee_src_root, 'configs/annotations.json')) +) + config.substitutions.append( ('%libcxx_include', getattr(config, 'libcxx_include_dir', None))) diff --git a/test/lit.site.cfg.in b/test/lit.site.cfg.in index fb4ed1c586..17ad995b8d 100644 --- a/test/lit.site.cfg.in +++ b/test/lit.site.cfg.in @@ -35,6 +35,7 @@ config.clang = "@LLVMCC@" config.clangxx = "@LLVMCXX@" config.cc = "@NATIVE_CC@" +config.objcopy = "@NATIVE_OBJCOPY@" config.cxx = "@NATIVE_CXX@" # NOTE: any changes to compiler flags also have to be applied to diff --git a/test/regression/2023-10-02-test-from-mocked-global.c b/test/regression/2023-10-02-test-from-mocked-global.c index a62eeb9bba..c89bc74ec9 100644 --- a/test/regression/2023-10-02-test-from-mocked-global.c +++ b/test/regression/2023-10-02-test-from-mocked-global.c @@ -2,7 +2,7 @@ // REQUIRES: not-darwin // RUN: %clang %s -g -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --mock-all-externals --write-xml-tests --output-dir=%t.klee-out %t1.bc +// RUN: %klee --mock-policy=all --write-xml-tests --output-dir=%t.klee-out %t1.bc // RUN: FileCheck --input-file %t.klee-out/test000001.xml %s extern void *__crc_mc44s803_attach __attribute__((__weak__)); @@ -13,4 +13,4 @@ int main() { return 0; } -// CHECK-NOT: XMLMetadataProgramHash( llvm::cl::desc("Test-Comp hash sum of original file for xml metadata"), llvm::cl::cat(TestCompCat)); - /*** Mocking options ***/ -cl::OptionCategory MockCat("Mock category"); - -cl::opt MockLinkedExternals( - "mock-linked-externals", - cl::desc("Mock modelled linked externals (default=false)"), cl::init(false), - cl::cat(MockCat)); - -cl::opt MockUnlinkedStrategy( - "mock-strategy", cl::init(MockStrategy::None), - cl::desc("Specify strategy for mocking external calls"), +cl::OptionCategory MockCat("Mocking options"); + +cl::opt MockModeledFunction( + "mock-modeled-functions", + cl::desc("Link modeled mocks from libkleeRuntimeMocks (default=false)"), + cl::init(false), cl::cat(MockCat)); + +cl::opt + Mock("mock-policy", cl::desc("Specify policy for mocking external calls"), + cl::values(clEnumValN(MockPolicy::None, "none", + "No mock function generated (default)"), + clEnumValN(MockPolicy::Failed, "failed", + "Generate symbolic value for failed external " + "calls, test will be irreproducible"), + clEnumValN(MockPolicy::All, "all", + "Generate IR module with all external symbols")), + cl::init(MockPolicy::None), cl::cat(MockCat)); + +cl::opt MockStrategy( + "mock-strategy", cl::desc("Specify strategy for mocking external calls"), cl::values( - clEnumValN(MockStrategy::None, "none", - "External calls are not mocked (default)"), - clEnumValN(MockStrategy::Naive, "naive", + clEnumValN(MockStrategyKind::Naive, "naive", "Every time external function is called, new symbolic value " - "is generated for its return value"), + "is generated for its return value (default)"), clEnumValN( - MockStrategy::Deterministic, "deterministic", + MockStrategyKind::Deterministic, "deterministic", "NOTE: this option is compatible with Z3 solver only. Each " "external function is treated as a deterministic " "function. Therefore, when function is called many times " "with equal arguments, every time equal values will be returned.")), - cl::init(MockStrategy::None), cl::cat(MockCat)); + cl::init(MockStrategyKind::Naive), cl::cat(MockCat)); -/*** Annotations options ***/ +cl::opt MockMutableGlobals( + "mock-mutable-globals", + cl::desc("Specify strategy for mocking global vars"), + cl::values( + clEnumValN(MockMutableGlobalsPolicy::None, "none", + "No mutable global object are allowed o mock except " + "external (default)"), + clEnumValN(MockMutableGlobalsPolicy::All, "all", + "Mock globals on module build stage and generate bicode " + "module for it")), + cl::init(MockMutableGlobalsPolicy::None), cl::cat(MockCat)); -cl::OptionCategory AnnotCat("Annotations category"); +/*** Annotations options ***/ cl::opt AnnotationsFile("annotations", cl::desc("Path to the annotation JSON file"), - cl::value_desc("path file"), - cl::cat(AnnotCat)); + cl::value_desc("path file"), cl::cat(MockCat)); + +cl::opt AnnotateOnlyExternal( + "annotate-only-external", + cl::desc("Ignore annotations for defined function (default=false)"), + cl::init(false), cl::cat(MockCat)); } // namespace @@ -1073,10 +1091,25 @@ static const char *dontCareExternals[] = { #endif // static information, pretty ok to return - "getegid", "geteuid", "getgid", "getuid", "getpid", "gethostname", - "getpgrp", "getppid", "getpagesize", "getpriority", "getgroups", - "getdtablesize", "getrlimit", "getrlimit64", "getcwd", "getwd", - "gettimeofday", "uname", "ioctl", + "getegid", + "geteuid", + "getgid", + "getuid", + "getpid", + "gethostname", + "getpgrp", + "getppid", + "getpagesize", + "getpriority", + "getgroups", + "getdtablesize", + "getrlimit", + "getrlimit64", + "getcwd", + "getwd", + "gettimeofday", + "uname", + "ioctl", // fp stuff we just don't worry about yet "frexp", @@ -1297,7 +1330,7 @@ createLibCWrapper(std::vector> &userModules, args.push_back(llvm::ConstantExpr::getBitCast( cast(inModuleReference.getCallee()), ft->getParamType(0))); - args.push_back(&*(stub->arg_begin())); // argc + args.push_back(&*(stub->arg_begin())); // argc auto arg_it = stub->arg_begin(); args.push_back(&*(++arg_it)); // argv args.push_back(Constant::getNullValue(ft->getParamType(3))); // app_init @@ -1586,38 +1619,34 @@ void wait_until_any_child_dies( } } -void mockLinkedExternals( +void mockModeledFunction( const Interpreter::ModuleOptions &Opts, llvm::LLVMContext &ctx, llvm::Module *mainModule, std::vector> &loadedLibsModules, - llvm::raw_string_ostream *redefineFile) { + std::vector> &redefinitions) { std::string errorMsg; std::vector> mockModules; SmallString<128> Path(Opts.LibraryDir); llvm::sys::path::append(Path, "libkleeRuntimeMocks" + Opts.OptSuffix + ".bca"); klee_message("NOTE: Using mocks model %s for linked externals", Path.c_str()); - if (!klee::loadFileAsOneModule(Path.c_str(), ctx, mockModules, errorMsg)) { + if (!klee::loadFileAsOneModule(Path.c_str(), ctx, loadedLibsModules, + errorMsg)) { klee_error("error loading mocks model '%s': %s", Path.c_str(), errorMsg.c_str()); } - for (auto &module : mockModules) { - for (const auto &fmodel : module->functions()) { - if (fmodel.getName().str().substr(0, 15) != "__klee_wrapped_") { - continue; - } - llvm::Function *f = - mainModule->getFunction(fmodel.getName().str().substr(15)); - if (!f) { - continue; - } + for (const auto &fmodel : loadedLibsModules.back()->functions()) { + if (fmodel.getName().str().substr(0, 15) != "__klee_wrapped_") { + continue; + } + if (llvm::Function *f = + mainModule->getFunction(fmodel.getName().str().substr(15))) { klee_message("Renamed symbol %s to %s", f->getName().str().c_str(), fmodel.getName().str().c_str()); - *redefineFile << f->getName() << ' ' << fmodel.getName() << '\n'; + redefinitions.emplace_back(f->getName(), fmodel.getName()); f->setName(fmodel.getName()); } - loadedLibsModules.push_back(std::move(module)); } } @@ -1999,12 +2028,6 @@ int main(int argc, char **argv, char **envp) { klee_warning("Module and host target triples do not match: '%s' != '%s'\n" "This may cause unexpected crashes or assertion violations.", module_triple.c_str(), host_triple.c_str()); - - llvm::Function *initialMainFn = mainModule->getFunction(EntryPoint); - if (!initialMainFn) { - klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); - } - // Detect architecture std::string bit_suffix = "64"; // Fall back to 64bit if (module_triple.find("i686") != std::string::npos || @@ -2023,13 +2046,15 @@ int main(int argc, char **argv, char **envp) { std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]); Interpreter::ModuleOptions Opts( - LibraryDir.c_str(), EntryPoint, opt_suffix, + LibraryDir, EntryPoint, opt_suffix, /*MainCurrentName=*/EntryPoint, /*MainNameAfterMock=*/"__klee_mock_wrapped_main", + /*AnnotationsFile=*/AnnotationsFile, /*Optimize=*/OptimizeModule, /*Simplify*/ SimplifyModule, /*CheckDivZero=*/CheckDivZero, /*CheckOvershift=*/CheckOvershift, + /*AnnotateOnlyExternal=*/AnnotateOnlyExternal, /*WithFPRuntime=*/WithFPRuntime, /*WithPOSIXRuntime=*/WithPOSIXRuntime); @@ -2053,15 +2078,15 @@ int main(int argc, char **argv, char **envp) { if (!entryFn) klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); - std::string redefinitions; - llvm::raw_string_ostream o_redefinitions(redefinitions); - if (MockLinkedExternals) { - mockLinkedExternals(Opts, ctx, mainModule, loadedLibsModules, - &o_redefinitions); + std::vector> redefinitions; + if (Mock == MockPolicy::All || + MockMutableGlobals == MockMutableGlobalsPolicy::All || + AnnotationsFile.empty()) { + redefinitions.emplace_back(EntryPoint, Opts.MainNameAfterMock); } - - if (MockUnlinkedStrategy != MockStrategy::None) { - o_redefinitions << EntryPoint << ' ' << Opts.MainNameAfterMock << '\n'; + if (MockModeledFunction) { + mockModeledFunction(Opts, ctx, mainModule, loadedLibsModules, + redefinitions); } if (WithPOSIXRuntime) { @@ -2227,14 +2252,13 @@ int main(int argc, char **argv, char **envp) { UseGuidedSearch = Interpreter::GuidanceKind::ErrorGuidance; } - const Annotations annotations = (AnnotationsFile.empty()) - ? Annotations() - : parseAnnotationsFile(AnnotationsFile); - Interpreter::InterpreterOptions IOpts(paths); IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic; IOpts.Guidance = UseGuidedSearch; - IOpts.MockStrategy = MockUnlinkedStrategy; + IOpts.Mock = Mock; + IOpts.MockStrategy = MockStrategy; + IOpts.MockMutableGlobals = MockMutableGlobals; + std::unique_ptr interpreter( Interpreter::create(ctx, IOpts, handler.get())); theInterpreter = interpreter.get(); @@ -2270,13 +2294,7 @@ int main(int argc, char **argv, char **envp) { ignoredExternals.insert("syscall"); } - Opts.MainCurrentName = initialMainFn->getName().str(); - - if (MockLinkedExternals || MockUnlinkedStrategy != MockStrategy::None) { - o_redefinitions.flush(); - auto f_redefinitions = handler->openOutputFile("redefinitions.txt"); - *f_redefinitions << redefinitions; - } + Opts.MainCurrentName = entryFn->getName().str(); // Get the desired main function. klee_main initializes uClibc // locale and other data and then calls main. @@ -2284,7 +2302,7 @@ int main(int argc, char **argv, char **envp) { auto finalModule = interpreter->setModule( loadedUserModules, loadedLibsModules, Opts, std::move(mainModuleFunctions), std::move(mainModuleGlobals), - std::move(origInstructions), ignoredExternals, annotations); + std::move(origInstructions), ignoredExternals, redefinitions); Function *mainFn = finalModule->getFunction(EntryPoint); if (!mainFn) { klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); diff --git a/unittests/Annotations/AnnotationsTest.cpp b/unittests/Annotations/AnnotationsTest.cpp index 9d67ab9461..7c3b90de3f 100644 --- a/unittests/Annotations/AnnotationsTest.cpp +++ b/unittests/Annotations/AnnotationsTest.cpp @@ -1,3 +1,12 @@ +//===-- AnnotationTest.cpp ------------------------------------------------===// +// +// The KLEEF Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #include "gtest/gtest.h" #include "klee/Module/Annotation.h" @@ -10,15 +19,18 @@ TEST(AnnotationsTest, Empty) { const json j = json::parse(R"( { "foo" : { - "annotation" : [], + "annotation" : [[]], "properties" : [] } } )"); - const Annotations expected = Annotations{ - {"foo", Annotation{"foo", std::vector(), - std::set()}}}; - const Annotations actual = parseAnnotationsFile(j); + const AnnotationsMap expected = { + {"foo", + {/*functionName*/ "foo", + /*returnStatements*/ std::vector(), + /*argsStatements*/ std::vector>(), + /*properties*/ std::set()}}}; + const AnnotationsMap actual = parseAnnotationsJson(j); ASSERT_EQ(expected, actual); } @@ -26,17 +38,20 @@ TEST(AnnotationsTest, KnownProperties) { const json j = json::parse(R"( { "foo" : { - "annotation" : [], - "properties" : ["determ", "noreturn", "determ"] + "annotation" : [[]], + "properties" : ["deterministic", "noreturn", "deterministic"] } } )"); - const std::set properties{ - Annotation::Property::Determ, Annotation::Property::Noreturn}; - const Annotations expected = Annotations{ - {"foo", Annotation{"foo", std::vector(), - properties}}}; - const Annotations actual = parseAnnotationsFile(j); + const std::set properties{ + Statement::Property::Deterministic, Statement::Property::Noreturn}; + const AnnotationsMap expected = { + {"foo", + {/*functionName*/ "foo", + /*returnStatements*/ std::vector(), + /*argsStatements*/ std::vector>(), + /*properties*/ properties}}}; + const AnnotationsMap actual = parseAnnotationsJson(j); ASSERT_EQ(expected, actual); } @@ -44,18 +59,21 @@ TEST(AnnotationsTest, UnknownProperties) { const json j = json::parse(R"( { "foo" : { - "annotation" : [], - "properties" : ["derm", "noreturn", "determ"] + "annotation" : [[]], + "properties" : ["noname", "noreturn", "deterministic"] } } )"); - const std::set properties{ - Annotation::Property::Determ, Annotation::Property::Noreturn, - Annotation::Property::Unknown}; - const Annotations expected = Annotations{ - {"foo", Annotation{"foo", std::vector(), - properties}}}; - const Annotations actual = parseAnnotationsFile(j); + const std::set properties{ + Statement::Property::Deterministic, Statement::Property::Noreturn, + Statement::Property::Unknown}; + const AnnotationsMap expected = { + {"foo", + {/*functionName*/ "foo", + /*returnStatements*/ std::vector(), + /*argsStatements*/ std::vector>(), + /*properties*/ properties}}}; + const AnnotationsMap actual = parseAnnotationsJson(j); ASSERT_EQ(expected, actual); } @@ -68,27 +86,27 @@ TEST(AnnotationsTest, UnknownAnnotations) { } } )"); - const Annotations actual = parseAnnotationsFile(j); - ASSERT_EQ(actual.at("foo").statements[1][0]->getStatementName(), - Annotation::StatementKind::Unknown); + const AnnotationsMap actual = parseAnnotationsJson(j); + ASSERT_EQ(actual.at("foo").argsStatements[0][0]->getKind(), + Statement::Kind::Unknown); } TEST(AnnotationsTest, KnownAnnotations) { const json j = json::parse(R"( { "foo" : { - "annotation" : [["InitNull"], ["Deref", "InitNull"]], + "annotation" : [["MaybeInitNull"], ["Deref", "InitNull"]], "properties" : [] } } )"); - const Annotations actual = parseAnnotationsFile(j); - ASSERT_EQ(actual.at("foo").statements[0][0]->getStatementName(), - Annotation::StatementKind::InitNull); - ASSERT_EQ(actual.at("foo").statements[1][0]->getStatementName(), - Annotation::StatementKind::Deref); - ASSERT_EQ(actual.at("foo").statements[1][1]->getStatementName(), - Annotation::StatementKind::InitNull); + const AnnotationsMap actual = parseAnnotationsJson(j); + ASSERT_EQ(actual.at("foo").returnStatements[0]->getKind(), + Statement::Kind::MaybeInitNull); + ASSERT_EQ(actual.at("foo").argsStatements[0][0]->getKind(), + Statement::Kind::Deref); + ASSERT_EQ(actual.at("foo").argsStatements[0][1]->getKind(), + Statement::Kind::InitNull); } TEST(AnnotationsTest, WithOffsets) { @@ -100,9 +118,9 @@ TEST(AnnotationsTest, WithOffsets) { } } )"); - const Annotations actual = parseAnnotationsFile(j); - ASSERT_EQ(actual.at("foo").statements[0][0]->getStatementName(), - Annotation::StatementKind::InitNull); + const AnnotationsMap actual = parseAnnotationsJson(j); + ASSERT_EQ(actual.at("foo").returnStatements[0]->getKind(), + Statement::Kind::InitNull); const std::vector expectedOffset{"*", "10", "*", "&"}; - ASSERT_EQ(actual.at("foo").statements[0][0]->offset, expectedOffset); + ASSERT_EQ(actual.at("foo").returnStatements[0]->offset, expectedOffset); }