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 0a15abc56d..04eec908de 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -10,6 +10,7 @@ #define KLEE_INTERPRETER_H #include "TerminationTypes.h" +#include "klee/Module/Annotation.h" #include "klee/Module/SarifReport.h" @@ -29,6 +30,7 @@ class BasicBlock; class Function; class LLVMContext; class Module; +class Type; class raw_ostream; class raw_fd_ostream; } // namespace llvm @@ -63,6 +65,23 @@ using FLCtoOpcode = std::unordered_map< std::unordered_map< unsigned, std::unordered_map>>>; +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 { public: enum class GuidanceKind { @@ -79,21 +98,32 @@ class Interpreter { std::string LibraryDir; std::string EntryPoint; 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, - bool _Optimize, bool _Simplify, bool _CheckDivZero, - bool _CheckOvershift, bool _WithFPRuntime, + const std::string &_MainCurrentName, + const std::string &_MainNameAfterMock, + const std::string &_AnnotationsFile, bool _Optimize, + bool _Simplify, bool _CheckDivZero, bool _CheckOvershift, + bool _AnnotateOnlyExternal, bool _WithFPRuntime, bool _WithPOSIXRuntime) : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint), - OptSuffix(_OptSuffix), Optimize(_Optimize), Simplify(_Simplify), - CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift), + OptSuffix(_OptSuffix), MainCurrentName(_MainCurrentName), + MainNameAfterMock(_MainNameAfterMock), + AnnotationsFile(_AnnotationsFile), Optimize(_Optimize), + Simplify(_Simplify), CheckDivZero(_CheckDivZero), + CheckOvershift(_CheckOvershift), + AnnotateOnlyExternal(_AnnotateOnlyExternal), WithFPRuntime(_WithFPRuntime), WithPOSIXRuntime(_WithPOSIXRuntime) {} }; @@ -112,10 +142,15 @@ class Interpreter { unsigned MakeConcreteSymbolic; GuidanceKind Guidance; std::optional Paths; + MockPolicy Mock; + MockStrategyKind MockStrategy; + MockMutableGlobalsPolicy MockMutableGlobals; InterpreterOptions(std::optional Paths) : MakeConcreteSymbolic(false), Guidance(GuidanceKind::NoGuidance), - Paths(std::move(Paths)) {} + Paths(std::move(Paths)), Mock(MockPolicy::None), + MockStrategy(MockStrategyKind::Naive), + MockMutableGlobals(MockMutableGlobalsPolicy::None) {} }; protected: @@ -138,13 +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) = 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 new file mode 100644 index 0000000000..da5d0ea198 --- /dev/null +++ b/include/klee/Core/MockBuilder.h @@ -0,0 +1,87 @@ +//===-- 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" +#include "llvm/IR/Module.h" + +#include +#include + +namespace klee { + +class MockBuilder { +private: + const llvm::Module *userModule; + llvm::LLVMContext &ctx; + std::unique_ptr mockModule; + std::unique_ptr> builder; + + 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 + 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, + 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 + +#endif // KLEE_MOCKBUILDER_H 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 f922a29861..1a353901e0 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -39,6 +39,12 @@ class SourceBuilder { static ref value(const llvm::Value &_allocSite, int _index, KModule *km); static ref irreproducible(const std::string &name); + static ref mockNaive(const KModule *kModule, + const llvm::Function &kFunction, + unsigned version); + static ref + mockDeterministic(const KModule *kModule, const llvm::Function &kFunction, + const std::vector> &args); static ref alpha(int _index); }; diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index 6853e4715d..7bdea46962 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -20,11 +20,13 @@ DISABLE_WARNING_POP namespace klee { +class Expr; class Array; class Expr; class ConstantExpr; struct KGlobalVariable; class KModule; +struct KFunction; struct KValue; struct KInstruction; @@ -48,6 +50,8 @@ class SymbolicSource { Instruction, Argument, Irreproducible, + MockNaive, + MockDeterministic, Alpha }; @@ -357,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; @@ -383,6 +387,62 @@ class AlphaSource : public SymbolicSource { } }; +class MockSource : public SymbolicSource { +public: + const KModule *km; + const llvm::Function &function; + MockSource(const KModule *_km, const llvm::Function &_function) + : km(_km), function(_function) {} + + static bool classof(const SymbolicSource *S) { + return S->getKind() == Kind::MockNaive || + S->getKind() == Kind::MockDeterministic; + } +}; + +class MockNaiveSource : public MockSource { +public: + const unsigned version; + + MockNaiveSource(const KModule *km, const llvm::Function &function, + unsigned _version) + : MockSource(km, function), version(_version) {} + + [[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; + } + + unsigned computeHash() override; + + [[nodiscard]] int internalCompare(const SymbolicSource &b) const override; +}; + +class MockDeterministicSource : public MockSource { +public: + const std::vector> args; + + MockDeterministicSource(const KModule *_km, const llvm::Function &_function, + const std::vector> &_args); + + [[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; + } + + unsigned computeHash() override; + + [[nodiscard]] int internalCompare(const SymbolicSource &b) const override; +}; + } // namespace klee #endif /* KLEE_SYMBOLICSOURCE_H */ diff --git a/include/klee/Module/Annotation.h b/include/klee/Module/Annotation.h new file mode 100644 index 0000000000..d94c591091 --- /dev/null +++ b/include/klee/Module/Annotation.h @@ -0,0 +1,140 @@ +//===-- 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 + +#include "map" +#include "set" +#include "string" +#include "vector" + +#include "nlohmann/json.hpp" +#include + +#include "klee/Config/config.h" + +#include "llvm/IR/Module.h" + +using json = nlohmann::json; + +namespace klee { + +namespace Statement { +enum class Kind { + Unknown, + + Deref, + InitNull, + MaybeInitNull, + // TODO: rename to alloc + AllocSource, + Free +}; + +enum class Property { + Unknown, + + Deterministic, + Noreturn, +}; + +struct Unknown { +protected: + std::string rawAnnotation; + std::string rawOffset; + std::string rawValue; + +public: + std::vector offset; + + explicit Unknown(const std::string &str = "Unknown"); + virtual ~Unknown(); + + virtual bool operator==(const Unknown &other) const; + [[nodiscard]] virtual Kind getKind() const; + + [[nodiscard]] const std::vector &getOffset() const; + [[nodiscard]] std::string toString() const; +}; + +struct Deref final : public Unknown { + explicit Deref(const std::string &str = "Deref"); + + [[nodiscard]] Kind getKind() const override; +}; + +struct InitNull final : public Unknown { +public: + explicit InitNull(const std::string &str = "InitNull"); + + [[nodiscard]] Kind getKind() 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) + }; + + Type value = Alloc::Type::ALLOC; + + explicit Alloc(const std::string &str = "AllocSource::1"); + + [[nodiscard]] Kind getKind() const override; +}; + +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"); + + [[nodiscard]] Kind getKind() const override; +}; + +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; +}; + +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/include/klee/klee.h b/include/klee/klee.h index 9c40ef335c..5995ff2e24 100644 --- a/include/klee/klee.h +++ b/include/klee/klee.h @@ -201,5 +201,6 @@ long double klee_rintl(long double d); // stdin/stdout void klee_init_env(int *argcPtr, char ***argvPtr); void check_stdin_read(); +void *__klee_wrapped_malloc(size_t size); #endif /* KLEE_H */ diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt index 9d94da9169..9e0dbb715c 100644 --- a/lib/Core/CMakeLists.txt +++ b/lib/Core/CMakeLists.txt @@ -22,6 +22,7 @@ add_library(kleeCore Memory.cpp MemoryManager.cpp PForest.cpp + MockBuilder.cpp PTree.cpp Searcher.cpp SeedInfo.cpp diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 1d4d06f927..3fd5a29996 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -30,10 +30,8 @@ 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 feb34f4470..51e2d6f849 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -36,10 +36,10 @@ #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" +#include "klee/Core/MockBuilder.h" #include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Expr/ArrayExprVisitor.h" #include "klee/Expr/Assignment.h" @@ -182,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, @@ -228,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(""), @@ -349,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( @@ -521,6 +495,16 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, inhibitForking(false), coverOnTheFly(false), haltExecution(HaltExecution::NotHalt), ivcEnabled(false), debugLogBuffer(debugBufferString) { + 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) timers.add(std::make_unique(maxTime, [&] { @@ -587,7 +571,9 @@ llvm::Module *Executor::setModule( std::vector> &userModules, std::vector> &libsModules, const ModuleOptions &opts, std::set &&mainModuleFunctions, - std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions) { + std::set &&mainModuleGlobals, FLCtoOpcode &&origInstructions, + const std::set &ignoredExternals, + std::vector> redefinitions) { assert(!kmodule && !userModules.empty() && "can only register one module"); // XXX gross @@ -615,6 +601,33 @@ llvm::Module *Executor::setModule( kmodule->instrument(opts); } + 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)); + // std::swap(mockModule, kmodule->module); + kmodule->link(mockModules, 1); + klee_message("Mock linkage: done"); + + for (auto &global : kmodule->module->globals()) { + if (global.isDeclaration()) { + llvm::Constant *zeroInitializer = + llvm::Constant::getNullValue(global.getValueType()); + if (!zeroInitializer) { + klee_error("Unable to get zero initializer for '%s'", + global.getName().str().c_str()); + } + global.setInitializer(zeroInitializer); + } + } + } + // 3.) Optimise and prepare for KLEE // Create a list of functions that should be preserved if used @@ -1012,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 { @@ -1030,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, {}); } } } @@ -3005,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); @@ -4992,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; @@ -5132,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); } @@ -5223,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; @@ -6077,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); } } @@ -6256,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); } @@ -6448,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); } } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 006b74eaae..d6cbb17352 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -729,13 +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) 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 new file mode 100644 index 0000000000..de06f5e463 --- /dev/null +++ b/lib/Core/MockBuilder.cpp @@ -0,0 +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 { + +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", ctx); + mockModule->setTargetTriple(userModule->getTargetTriple()); + mockModule->setDataLayout(userModule->getDataLayout()); + 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() { + mainModuleFunctions.insert(opts.MainNameAfterMock); + llvm::Function *userMainFn = userModule->getFunction(opts.MainCurrentName); + if (!userMainFn) { + klee_error("Entry function '%s' not found in module.", + opts.MainCurrentName.c_str()); + } + userMainFn->setName(opts.MainNameAfterMock); + + mockModule->getOrInsertFunction(opts.MainCurrentName, + userMainFn->getFunctionType(), + userMainFn->getAttributes()); + llvm::Function *mockMainFn = mockModule->getFunction(opts.MainCurrentName); + if (!mockMainFn) { + klee_error("Mock: Entry function '%s' not found in module", + opts.MainCurrentName.c_str()); + } + mockMainFn->setDSOLocal(true); + auto globalsInitBlock = llvm::BasicBlock::Create(ctx, "", mockMainFn); + builder->SetInsertPoint(globalsInitBlock); + // Define all the external globals + if (interpreterOptions.Mock == MockPolicy::All || + interpreterOptions.MockMutableGlobals == MockMutableGlobalsPolicy::All) { + buildExternalGlobalsDefinitions(); + } + + auto userMainCallee = mockModule->getOrInsertFunction( + opts.MainNameAfterMock, userMainFn->getFunctionType()); + std::vector args; + args.reserve(userMainFn->arg_size()); + for (auto &arg : mockMainFn->args()) { + args.push_back(&arg); + } + + auto callUserMain = builder->CreateCall(userMainCallee, args); + if (!userMainFn->getReturnType()->isSized()) { + builder->CreateRet(nullptr); + return; + } else { + builder->CreateRet(callUserMain); + } +} + +void MockBuilder::buildExternalGlobalsDefinitions() { + 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("Mock: Unable to add global variable '%s' to module", + extName.c_str()); + } + + mainModuleGlobals.insert(extName); + if (!elementType->isSized()) { + continue; + } + + auto *zeroInitializer = llvm::GlobalValue::getNullValue(elementType); + if (!zeroInitializer) { + klee_error("Mock: Unable to get zero initializer for '%s'", + extName.c_str()); + } + global->setInitializer(zeroInitializer); + 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() { + 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(); + } + } + } + } + + for (const auto &[extName, type] : externalFunctions) { + mockModule->getOrInsertFunction(extName, type); + llvm::Function *func = mockModule->getFunction(extName); + if (!func) { + 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(ctx, "entry", func); + builder->SetInsertPoint(BB); + + 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()}); + } + } +} + +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}; +} + +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; +} + +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; + } + res.emplace_back(); + j++; + if (j >= func->arg_size()) { + break; + } + } + 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); + } + } +} + +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 Statement::Kind::Free: { + klee_warning("Annotation: unused \"Free\" for return"); + break; + } + case Statement::Kind::Unknown: + default: + 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); +} + +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; + } + } +} + +} // namespace klee diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 82dc7f5388..ae4a7b358c 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -112,6 +112,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { #endif add("klee_is_symbolic", handleIsSymbolic, true), add("klee_make_symbolic", handleMakeSymbolic, false), + add("klee_make_mock", handleMakeMock, false), add("klee_mark_global", handleMarkGlobal, false), add("klee_prefer_cex", handlePreferCex, false), add("klee_posix_prefer_cex", handlePosixPreferCex, false), @@ -937,6 +938,83 @@ void SpecialFunctionHandler::handleMakeSymbolic( } } +void SpecialFunctionHandler::handleMakeMock(ExecutionState &state, + KInstruction *target, + std::vector> &arguments) { + std::string name; + + if (arguments.size() != 3) { + executor.terminateStateOnUserError(state, + "Incorrect number of arguments to " + "klee_make_mock(void*, size_t, char*)"); + return; + } + + name = arguments[2]->isZero() ? "" : readStringAtAddress(state, arguments[2]); + + if (name.empty()) { + executor.terminateStateOnUserError( + state, "Empty name of function in klee_make_mock"); + return; + } + + 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( ExecutionState &state, KInstruction *target, std::vector> &arguments) { diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index 78f920450e..6528b98c36 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -127,6 +127,7 @@ class SpecialFunctionHandler { HANDLER(handleGetValue); HANDLER(handleIsSymbolic); HANDLER(handleMakeSymbolic); + HANDLER(handleMakeMock); HANDLER(handleMalloc); HANDLER(handleMemalign); HANDLER(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/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 4d5fdc2554..83c6e0b782 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -423,6 +423,18 @@ class PPrinter : public ExprPPrinter { << kf->getName().str() << " " << s->index; } else if (auto s = dyn_cast(source)) { PC << s->name; + } else if (auto s = dyn_cast(source)) { + PC << s->km->functionMap.at(&s->function)->getName() << ' ' << s->version; + } else if (auto s = dyn_cast(source)) { + PC << s->km->functionMap.at(&s->function)->getName() << ' '; + PC << "("; + for (unsigned i = 0; i < s->args.size(); i++) { + print(s->args[i], PC); + if (i != s->args.size() - 1) { + PC << " "; + } + } + PC << ')'; } else if (auto s = dyn_cast(source)) { PC << s->index; } else { diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp index 87bed5d731..518e922dc8 100644 --- a/lib/Expr/ExprUtil.cpp +++ b/lib/Expr/ExprUtil.cpp @@ -54,6 +54,16 @@ void klee::findReads(ref e, bool visitUpdates, cast(re->updates.root->source)->pointer); } + if (ref mockSource = + dyn_cast_or_null( + re->updates.root->source)) { + for (auto arg : mockSource->args) { + if (visited.insert(arg).second) { + stack.push_back(arg); + } + } + } + if (visitUpdates) { // XXX this is probably suboptimal. We want to avoid a potential // explosion traversing update lists which can be quite diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index 79e3fad63e..9ff427baf7 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -8,10 +8,9 @@ #include "klee/Expr/IndependentConstraintSetUnion.h" #include "klee/Expr/SymbolicSource.h" #include "klee/Expr/Symcrete.h" -#include "klee/Solver/Solver.h" +#include "klee/Module/KModule.h" #include -#include #include #include #include @@ -125,6 +124,11 @@ void IndependentConstraintSet::initIndependentConstraintSet(ref e) { if (re->updates.root->isConstantArray() && !re->updates.head) continue; + if (ref mockSource = + dyn_cast_or_null(array->source)) { + uninterpretedFunctions.insert(mockSource->function.getName().str()); + } + if (!wholeObjects.count(array)) { if (ConstantExpr *CE = dyn_cast(re->index)) { // if index constant, then add to set of constraints operating @@ -266,6 +270,11 @@ bool IndependentConstraintSet::intersects( return true; } } + for (const auto &uFn : a->uninterpretedFunctions) { + if (b->uninterpretedFunctions.count(uFn)) { + return true; + } + } } // No need to check symcretes here, arrays must be sufficient. return false; diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 95c2d09a38..956f1fb876 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -331,6 +331,8 @@ class ParserImpl : public Parser { SourceResult ParseLazyInitializationSizeSource(); SourceResult ParseInstructionSource(); SourceResult ParseArgumentSource(); + SourceResult ParseMockNaiveSource(); + SourceResult ParseMockDeterministicSource(); SourceResult ParseAlphaSource(); /*** Diagnostics ***/ @@ -501,6 +503,12 @@ SourceResult ParserImpl::ParseSource() { } else if (type == "argument") { assert(km); source = ParseArgumentSource(); + } else if (type == "mockNaive") { + assert(km); + source = ParseMockNaiveSource(); + } else if (type == "mockDeterministic") { + assert(km); + source = ParseMockDeterministicSource(); } else if (type == "alpha") { source = ParseAlphaSource(); } else { @@ -631,6 +639,34 @@ SourceResult ParserImpl::ParseInstructionSource() { return SourceBuilder::instruction(*KI->inst(), index, km); } +SourceResult ParserImpl::ParseMockNaiveSource() { + auto name = Tok.getString(); + auto kf = km->functionNameMap[name]; + ConsumeExpectedToken(Token::Identifier); + auto versionExpr = ParseNumber(64).get(); + auto version = dyn_cast(versionExpr); + assert(version); + return SourceBuilder::mockNaive(km, *kf->function(), version->getZExtValue()); +} + +SourceResult ParserImpl::ParseMockDeterministicSource() { + auto name = Tok.getString(); + auto kf = km->functionNameMap[name]; + ConsumeExpectedToken(Token::Identifier); + ConsumeLParen(); + std::vector> args; + args.reserve(kf->getNumArgs()); + for (unsigned i = 0; i < kf->getNumArgs(); i++) { + auto expr = ParseExpr(TypeResult()); + if (!expr.isValid()) { + return {false, nullptr}; + } + args.push_back(expr.get()); + } + ConsumeRParen(); + return SourceBuilder::mockDeterministic(km, *kf->function(), args); +} + SourceResult ParserImpl::ParseAlphaSource() { auto indexExpr = ParseNumber(64).get(); auto index = dyn_cast(indexExpr)->getZExtValue(); diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp index b49111e4f6..47f5fdd823 100644 --- a/lib/Expr/SourceBuilder.cpp +++ b/lib/Expr/SourceBuilder.cpp @@ -99,6 +99,23 @@ ref SourceBuilder::irreproducible(const std::string &name) { return r; } +ref SourceBuilder::mockNaive(const KModule *km, + const llvm::Function &function, + unsigned int version) { + ref r(new MockNaiveSource(km, function, version)); + r->computeHash(); + return r; +} + +ref +SourceBuilder::mockDeterministic(const KModule *km, + const llvm::Function &function, + const std::vector> &args) { + ref r(new MockDeterministicSource(km, function, args)); + r->computeHash(); + 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 2dc798d32d..a1ea9a0de0 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -1,5 +1,4 @@ #include "klee/Expr/SymbolicSource.h" - #include "klee/Expr/Expr.h" #include "klee/Expr/ExprPPrinter.h" #include "klee/Expr/ExprUtil.h" @@ -202,4 +201,65 @@ unsigned InstructionSource::computeHash() { return hashValue; } +unsigned MockNaiveSource::computeHash() { + unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + version; + unsigned funcID = km->getFunctionId(&function); + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + funcID; + hashValue = res; + return res; +} + +int MockNaiveSource::internalCompare(const SymbolicSource &b) const { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const MockNaiveSource &mnb = static_cast(b); + 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; +} + +MockDeterministicSource::MockDeterministicSource( + const KModule *km, const llvm::Function &function, + const std::vector> &_args) + : MockSource(km, function), args(_args) {} + +unsigned MockDeterministicSource::computeHash() { + unsigned res = getKind(); + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + + km->getFunctionId(&function); + for (const auto &arg : args) { + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + arg->hash(); + } + hashValue = res; + return res; +} + +int MockDeterministicSource::internalCompare(const SymbolicSource &b) const { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const MockDeterministicSource &mdb = + static_cast(b); + unsigned funcID = km->getFunctionId(&function); + unsigned bFuncID = mdb.km->getFunctionId(&mdb.function); + if (funcID != bFuncID) { + return funcID < bFuncID ? -1 : 1; + } + assert(args.size() == mdb.args.size() && + "the same functions should have the same arguments number"); + for (unsigned i = 0; i < args.size(); i++) { + if (args[i] != mdb.args[i]) { + return args[i] < mdb.args[i] ? -1 : 1; + } + } + return 0; +} + } // namespace klee diff --git a/lib/Module/Annotation.cpp b/lib/Module/Annotation.cpp new file mode 100644 index 0000000000..bfc4b2abf4 --- /dev/null +++ b/lib/Module/Annotation.cpp @@ -0,0 +1,274 @@ +//===-- 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 +#include + +namespace klee { + +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; +} + +namespace Statement { + +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; + + 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); + } + } + + for (size_t pos = 0; pos < rawOffset.size(); pos++) { + switch (rawOffset[pos]) { + case '*': { + offset.emplace_back("*"); + break; + } + case '&': { + offset.emplace_back("&"); + break; + } + case '[': { + size_t posEndExpr = rawOffset.find(']', pos); + if (posEndExpr == std::string::npos) { + klee_error("Annotation: Incorrect offset format \"%s\"", str.c_str()); + } + 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 { + return rawAnnotation + ":" + rawOffset; + } + } + return rawAnnotation + ":" + rawOffset + ":" + rawValue; +} + +bool Unknown::operator==(const Unknown &other) const { + return this->getKind() == other.getKind() && toString() == other.toString(); +} + +/* + * Format: {kind}:{offset}:{data} + * Example: InitNull:*[5]: + */ + +Deref::Deref(const std::string &str) : Unknown(str) {} + +Kind Deref::getKind() const { return Kind::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)); + } +} + +Kind Alloc::getKind() const { return Kind::AllocSource; } + +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)); + } +} + +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; +} + +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("Annotation: Incorrect statement format"); + } + const std::string jStr = j.get(); + statement = Statement::stringToKindPtr(jStr); +} + +void from_json(const json &j, Property &property) { + if (!j.is_string()) { + klee_error("Annotation: Incorrect properties format"); + } + const std::string jStr = j.get(); + + property = Statement::Property::Unknown; + const auto propertyPtr = Statement::StringToPropertyMap.find(jStr); + if (propertyPtr != Statement::StringToPropertyMap.end()) { + property = propertyPtr->second; + } +} + +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(); + + const json &j = item.value(); + if (!j.is_object() || !j.contains("annotation") || + !j.contains("properties")) { + 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.properties = + j.at("properties").get>(); + annotations[item.key()] = annotation; + } + return annotations; +} + +AnnotationsMap parseAnnotations(const std::string &path) { + if (path.empty()) { + return {}; + } + std::ifstream annotationsFile(path); + if (!annotationsFile.good()) { + klee_error("Annotation: Opening %s failed.", path.c_str()); + } + json annotationsJson = json::parse(annotationsFile, nullptr, false); + if (annotationsJson.is_discarded()) { + klee_error("Annotation: Parsing JSON %s failed.", path.c_str()); + } + + return parseAnnotationsJson(annotationsJson); +} + +} // namespace klee diff --git a/lib/Module/CMakeLists.txt b/lib/Module/CMakeLists.txt index 19d9c11dbe..d185f53a72 100644 --- a/lib/Module/CMakeLists.txt +++ b/lib/Module/CMakeLists.txt @@ -7,6 +7,7 @@ # #===------------------------------------------------------------------------===# set(KLEE_MODULE_COMPONENT_SRCS + Annotation.cpp CallSplitter.cpp CallRemover.cpp Checks.cpp diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index b26ec1e75c..7cc873980c 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -13,6 +13,7 @@ #include "klee/ADT/Bits.h" #include "klee/Expr/Expr.h" #include "klee/Expr/SymbolicSource.h" +#include "klee/Module/KModule.h" #include "klee/Solver/Solver.h" #include "klee/Solver/SolverStats.h" #include "klee/Support/ErrorHandling.h" @@ -262,6 +263,36 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { if (source && !isa(root->size)) { array_expr = buildConstantArray(unique_name.c_str(), root->getDomain(), root->getRange(), value->getZExtValue(8)); + } else if (ref mockDeterministicSource = + dyn_cast(root->source)) { + size_t num_args = mockDeterministicSource->args.size(); + 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(); + 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()); + Z3SortHandle rangeSort = getBvSort(root->getRange()); + Z3SortHandle retValSort = getArraySort(domainSort, rangeSort); + + Z3FuncDeclHandle func; + func = Z3FuncDeclHandle( + Z3_mk_func_decl( + ctx, + Z3_mk_string_symbol( + ctx, + mockDeterministicSource->function.getName().str().c_str()), + num_args, argsSort.data(), retValSort), + ctx); + array_expr = + Z3ASTHandle(Z3_mk_app(ctx, func, num_args, args.data()), ctx); } else { array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index 7b407c6e3d..e6d10fed10 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -91,6 +91,13 @@ typedef Z3NodeHandle Z3SortHandle; 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() const { + return ::Z3_func_decl_to_ast(context, node); +} +typedef Z3NodeHandle Z3FuncDeclHandle; +template <> void Z3NodeHandle::dump() const __attribute__((used)); + // Specialise for Z3_ast template <> inline ::Z3_ast Z3NodeHandle::as_ast() const { return node; diff --git a/runtime/CMakeLists.txt b/runtime/CMakeLists.txt index ada82c0f33..d1c8a17d2f 100644 --- a/runtime/CMakeLists.txt +++ b/runtime/CMakeLists.txt @@ -90,12 +90,14 @@ add_subdirectory(Freestanding) add_subdirectory(Intrinsic) add_subdirectory(klee-libc) add_subdirectory(Fortify) +add_subdirectory(Mocks) set(RUNTIME_LIBRARIES RuntimeFreestanding RuntimeIntrinsic RuntimeKLEELibc RuntimeFortify + RuntimeMocks ) if (ENABLE_KLEE_EH_CXX) diff --git a/runtime/Mocks/CMakeLists.txt b/runtime/Mocks/CMakeLists.txt new file mode 100644 index 0000000000..efd6497470 --- /dev/null +++ b/runtime/Mocks/CMakeLists.txt @@ -0,0 +1,19 @@ +#===------------------------------------------------------------------------===# +# +# The KLEE Symbolic Virtual Machine +# +# This file is distributed under the University of Illinois Open Source +# License. See LICENSE.TXT for details. +# +#===------------------------------------------------------------------------===# + +set(LIB_PREFIX "RuntimeMocks") +set(SRC_FILES + models.c + ) + +# Build it +include("${CMAKE_SOURCE_DIR}/cmake/compile_bitcode_library.cmake") +prefix_with_path("${SRC_FILES}" "${CMAKE_CURRENT_SOURCE_DIR}/" runtime_mocks_files) + +add_bitcode_library_targets("${LIB_PREFIX}" "${runtime_mocks_files}" "" "") diff --git a/runtime/Mocks/models.c b/runtime/Mocks/models.c new file mode 100644 index 0000000000..e40b0cfaa0 --- /dev/null +++ b/runtime/Mocks/models.c @@ -0,0 +1,45 @@ +//===-- 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); +extern void *malloc(size_t size); +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) { + unsigned char retNull; + klee_make_symbolic(&retNull, sizeof(retNull), "retNullMalloc"); + if (retNull) { + return 0; + } + void *array = malloc(size); + return array; +} + +void *__klee_wrapped_calloc(size_t num, size_t size) { + unsigned char retNull; + klee_make_symbolic(&retNull, sizeof(retNull), "retNullCalloc"); + if (retNull) { + return 0; + } + void *array = calloc(num, size); + return array; +} + +void *__klee_wrapped_realloc(void *ptr, size_t new_size) { + unsigned char retNull; + klee_make_symbolic(&retNull, sizeof(retNull), "retNullRealloc"); + if (retNull) { + return 0; + } + void *array = realloc(ptr, new_size); + return array; +} diff --git a/runtime/Runtest/CMakeLists.txt b/runtime/Runtest/CMakeLists.txt index df5f2c23be..33d190a262 100644 --- a/runtime/Runtest/CMakeLists.txt +++ b/runtime/Runtest/CMakeLists.txt @@ -9,6 +9,8 @@ add_library(kleeRuntest SHARED intrinsics.c + # Mocks: + ${CMAKE_SOURCE_DIR}/runtime/Mocks/models.c # HACK: ${CMAKE_SOURCE_DIR}/lib/Basic/KTest.cpp ) diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c index 7372549b93..5402908de2 100644 --- a/runtime/Runtest/intrinsics.c +++ b/runtime/Runtest/intrinsics.c @@ -75,8 +75,7 @@ void recursively_allocate(KTestObject *obj, size_t index, void *addr, return; } -void klee_make_symbolic(void *array, size_t nbytes, const char *name) { - +static void klee_make_symbol(void *array, size_t nbytes, const char *name) { if (!name) name = "unnamed"; @@ -157,6 +156,14 @@ void klee_make_symbolic(void *array, size_t nbytes, const char *name) { } } +void klee_make_symbolic(void *array, size_t nbytes, const char *name) { + klee_make_symbol(array, nbytes, name); +} + +void klee_make_mock(void *ret_array, size_t ret_nbytes, const char *fname) { + klee_make_symbol(ret_array, ret_nbytes, fname); +} + void klee_silent_exit(int x) { exit(x); } uintptr_t klee_choose(uintptr_t n) { 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 new file mode 100755 index 0000000000..ef5db2def6 --- /dev/null +++ b/scripts/run_tests_with_mocks.py @@ -0,0 +1,33 @@ +#!/usr/bin/env python3 + +# 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 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/ + +import subprocess as sp +import sys +import os + +klee_out_dir = sys.argv[-2] +bitcode = sys.argv[-1] + +filename = os.path.splitext(bitcode)[0] +object_file = f'{filename}.o' +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) + +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 new file mode 100644 index 0000000000..03a2480850 --- /dev/null +++ b/test/Feature/MockPointersDeterministic.c @@ -0,0 +1,24 @@ +// REQUIRES: z3 +// 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 --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 + +#include + +extern int *age(); + +int main() { + if (age() != age()) { + assert(0 && "age is deterministic"); + } + if (*age() != *age()) { + assert(0 && "age is deterministic"); + } + return *age(); +} diff --git a/test/Feature/MockStrategies.c b/test/Feature/MockStrategies.c new file mode 100644 index 0000000000..d8998cfe54 --- /dev/null +++ b/test/Feature/MockStrategies.c @@ -0,0 +1,37 @@ +// REQUIRES: z3 +// 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 %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 --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 --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 --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 + +#include + +extern int foo(int x, int y); + +int main() { + int a, b; + klee_make_symbolic(&a, sizeof(a), "a"); + klee_make_symbolic(&b, sizeof(b), "b"); + if (a == b && foo(a + b, b) != foo(2 * b, a)) { + assert(0); + } + return 0; +} 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 new file mode 100644 index 0000000000..615bea931b --- /dev/null +++ b/test/Replay/libkleeruntest/replay_mocks.c @@ -0,0 +1,27 @@ +// 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 --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_runner2 + +extern int variable; + +extern int foo(int); + +int main() { + int a; + klee_make_symbolic(&a, sizeof(a), "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 55adadf5cc..79f071b5c0 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -90,17 +90,27 @@ 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: lit_config.fatal('{0} is not set'.format(name)) config.substitutions.append( ('%' + name, value)) +config.substitutions.append( + ('%runmocks', os.path.join(klee_src_root, 'scripts/run_tests_with_mocks.py')) +) + # Add a substitution for lli. 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')) @@ -118,6 +128,11 @@ config.substitutions.append( ('%llvmcov', os.path.join(llvm_tools_dir, 'llvm-cov')) ) +# Add a substitution for llvm-objcopy +config.substitutions.append( + ('%llvmobjcopy', os.path.join(llvm_tools_dir, 'llvm-objcopy')) +) + # Add a substition for libkleeruntest config.substitutions.append( ('%libkleeruntestdir', os.path.dirname(config.libkleeruntest)) @@ -170,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("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(MockStrategyKind::Naive, "naive", + "Every time external function is called, new symbolic value " + "is generated for its return value (default)"), + clEnumValN( + 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(MockStrategyKind::Naive), cl::cat(MockCat)); + +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)); + +/*** Annotations options ***/ + +cl::opt + AnnotationsFile("annotations", cl::desc("Path to the annotation JSON file"), + 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 namespace klee { @@ -852,7 +909,7 @@ std::string KleeHandler::getRunTimeLibraryPath(const char *argv0) { void KleeHandler::setOutputDirectory(const std::string &directoryName) { // create output directory - if (directoryName == "") { + if (directoryName.empty()) { klee_error("Empty name of new directory"); } SmallString<128> directory(directoryName); @@ -957,7 +1014,8 @@ static const char *modelledExternals[] = { "klee_check_memory_access", "klee_define_fixed_object", "klee_get_errno", "klee_get_valuef", "klee_get_valued", "klee_get_valuel", "klee_get_valuell", "klee_get_value_i32", "klee_get_value_i64", "klee_get_obj_size", - "klee_is_symbolic", "klee_make_symbolic", "klee_mark_global", + "klee_is_symbolic", "klee_make_symbolic", "klee_make_mock", + "klee_mark_global", "klee_open_merge", "klee_close_merge", "klee_prefer_cex", "klee_posix_prefer_cex", "klee_print_expr", "klee_print_range", "klee_report_error", "klee_set_forking", "klee_silent_exit", "klee_warning", "klee_warning_once", "klee_stack_trace", @@ -1051,12 +1109,14 @@ static const char *dontCareExternals[] = { "getwd", "gettimeofday", "uname", + "ioctl", // fp stuff we just don't worry about yet "frexp", "ldexp", "__isnan", "__signbit", + "llvm.dbg.label", }; // Extra symbols we aren't going to warn about with klee-libc @@ -1559,6 +1619,37 @@ void wait_until_any_child_dies( } } +void mockModeledFunction( + const Interpreter::ModuleOptions &Opts, llvm::LLVMContext &ctx, + llvm::Module *mainModule, + std::vector> &loadedLibsModules, + 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, loadedLibsModules, + errorMsg)) { + klee_error("error loading mocks model '%s': %s", Path.c_str(), + errorMsg.c_str()); + } + + 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()); + redefinitions.emplace_back(f->getName(), fmodel.getName()); + f->setName(fmodel.getName()); + } + } +} + llvm::Value *createStringArray(LLVMContext &ctx, const char *str) { auto type = llvm::ArrayType::get(llvm::Type::getInt8Ty(ctx), strlen(str) + 1); std::vector chars; @@ -1846,9 +1937,10 @@ int main(int argc, char **argv, char **envp) { sys::SetInterruptFunction(interrupt_handle); - // Load the bytecode... std::string errorMsg; LLVMContext ctx; + + // Load the bytecode... std::vector> loadedUserModules; std::vector> loadedLibsModules; if (!klee::loadFileAsOneModule(InputFile, ctx, loadedUserModules, errorMsg)) { @@ -1936,7 +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()); - // Detect architecture std::string bit_suffix = "64"; // Fall back to 64bit if (module_triple.find("i686") != std::string::npos || @@ -1954,13 +2045,18 @@ int main(int argc, char **argv, char **envp) { } std::string LibraryDir = KleeHandler::getRunTimeLibraryPath(argv[0]); - Interpreter::ModuleOptions Opts(LibraryDir.c_str(), EntryPoint, opt_suffix, - /*Optimize=*/OptimizeModule, - /*Simplify*/ SimplifyModule, - /*CheckDivZero=*/CheckDivZero, - /*CheckOvershift=*/CheckOvershift, - /*WithFPRuntime=*/WithFPRuntime, - /*WithPOSIXRuntime=*/WithPOSIXRuntime); + Interpreter::ModuleOptions Opts( + 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); // Get the main function for (auto &module : loadedUserModules) { @@ -1982,6 +2078,17 @@ int main(int argc, char **argv, char **envp) { if (!entryFn) klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); + std::vector> redefinitions; + if (Mock == MockPolicy::All || + MockMutableGlobals == MockMutableGlobalsPolicy::All || + AnnotationsFile.empty()) { + redefinitions.emplace_back(EntryPoint, Opts.MainNameAfterMock); + } + if (MockModeledFunction) { + mockModeledFunction(Opts, ctx, mainModule, loadedLibsModules, + redefinitions); + } + if (WithPOSIXRuntime) { SmallString<128> Path(Opts.LibraryDir); llvm::sys::path::append(Path, "libkleeRuntimePOSIX" + opt_suffix + ".bca"); @@ -2148,6 +2255,10 @@ int main(int argc, char **argv, char **envp) { Interpreter::InterpreterOptions IOpts(paths); IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic; IOpts.Guidance = UseGuidedSearch; + IOpts.Mock = Mock; + IOpts.MockStrategy = MockStrategy; + IOpts.MockMutableGlobals = MockMutableGlobals; + std::unique_ptr interpreter( Interpreter::create(ctx, IOpts, handler.get())); theInterpreter = interpreter.get(); @@ -2159,13 +2270,43 @@ int main(int argc, char **argv, char **envp) { } handler->getInfoStream() << "PID: " << getpid() << "\n"; + std::set ignoredExternals; + ignoredExternals.insert(modelledExternals, + modelledExternals + NELEMS(modelledExternals)); + ignoredExternals.insert(dontCareExternals, + dontCareExternals + NELEMS(dontCareExternals)); + ignoredExternals.insert(unsafeExternals, + unsafeExternals + NELEMS(unsafeExternals)); + + switch (Libc) { + case LibcType::KleeLibc: + ignoredExternals.insert(dontCareKlee, dontCareKlee + NELEMS(dontCareKlee)); + break; + case LibcType::UcLibc: + ignoredExternals.insert(dontCareUclibc, + dontCareUclibc + NELEMS(dontCareUclibc)); + break; + case LibcType::FreestandingLibc: /* silence compiler warning */ + break; + } + + if (WithPOSIXRuntime) { + ignoredExternals.insert("syscall"); + } + + Opts.MainCurrentName = entryFn->getName().str(); + // Get the desired main function. klee_main initializes uClibc // locale and other data and then calls main. auto finalModule = interpreter->setModule( loadedUserModules, loadedLibsModules, Opts, std::move(mainModuleFunctions), std::move(mainModuleGlobals), - std::move(origInstructions)); + std::move(origInstructions), ignoredExternals, redefinitions); + Function *mainFn = finalModule->getFunction(EntryPoint); + if (!mainFn) { + klee_error("Entry function '%s' not found in module.", EntryPoint.c_str()); + } externalsAndGlobalsCheck(finalModule); diff --git a/unittests/Annotations/AnnotationsTest.cpp b/unittests/Annotations/AnnotationsTest.cpp new file mode 100644 index 0000000000..7c3b90de3f --- /dev/null +++ b/unittests/Annotations/AnnotationsTest.cpp @@ -0,0 +1,126 @@ +//===-- 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" + +#include + +using namespace klee; + +TEST(AnnotationsTest, Empty) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [[]], + "properties" : [] + } +} +)"); + const AnnotationsMap expected = { + {"foo", + {/*functionName*/ "foo", + /*returnStatements*/ std::vector(), + /*argsStatements*/ std::vector>(), + /*properties*/ std::set()}}}; + const AnnotationsMap actual = parseAnnotationsJson(j); + ASSERT_EQ(expected, actual); +} + +TEST(AnnotationsTest, KnownProperties) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [[]], + "properties" : ["deterministic", "noreturn", "deterministic"] + } +} +)"); + 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); +} + +TEST(AnnotationsTest, UnknownProperties) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [[]], + "properties" : ["noname", "noreturn", "deterministic"] + } +} +)"); + 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); +} + +TEST(AnnotationsTest, UnknownAnnotations) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [[], ["Ooo"]], + "properties" : [] + } +} +)"); + 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" : [["MaybeInitNull"], ["Deref", "InitNull"]], + "properties" : [] + } +} +)"); + 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) { + const json j = json::parse(R"( +{ + "foo" : { + "annotation" : [["InitNull:*[10]*&"]], + "properties" : [] + } +} +)"); + 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").returnStatements[0]->offset, expectedOffset); +} diff --git a/unittests/Annotations/CMakeLists.txt b/unittests/Annotations/CMakeLists.txt new file mode 100644 index 0000000000..cb9a7b1df1 --- /dev/null +++ b/unittests/Annotations/CMakeLists.txt @@ -0,0 +1,3 @@ +add_klee_unit_test(AnnotationsTest + AnnotationsTest.cpp) +target_link_libraries(AnnotationsTest PRIVATE kleaverExpr kleaverSolver) diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt index d4b4d1f9f7..edb1f46361 100644 --- a/unittests/CMakeLists.txt +++ b/unittests/CMakeLists.txt @@ -272,6 +272,7 @@ function(add_klee_unit_test target_name) endfunction() # Unit Tests +add_subdirectory(Annotations) add_subdirectory(Assignment) add_subdirectory(Expr) add_subdirectory(Ref)