From b7d6f2a3bd38a170d51b087eb806065c4e3bc43b Mon Sep 17 00:00:00 2001 From: Dino Distefano Date: Mon, 29 Feb 2016 05:28:51 -0800 Subject: [PATCH] Fixed problem with null pointer dereference in c library models. Reviewed By: cristianoc Differential Revision: D2954298 fb-gh-sync-id: 24fddaf shipit-source-id: 24fddaf --- infer/models/c/src/infer_builtins.h | 5 +- infer/models/c/src/libc_basic.c | 158 ++++++++---------- infer/src/backend/symExec.ml | 132 ++++++++------- .../c/errors/memory_leaks/test.c | 8 +- .../c/errors/null_dereference/memcpy-test.c | 45 +++++ .../endtoend/c/NullDereferenceTest3.java | 59 +++++++ 6 files changed, 259 insertions(+), 148 deletions(-) create mode 100644 infer/tests/codetoanalyze/c/errors/null_dereference/memcpy-test.c create mode 100644 infer/tests/endtoend/c/NullDereferenceTest3.java diff --git a/infer/models/c/src/infer_builtins.h b/infer/models/c/src/infer_builtins.h index cee8485b9..6cca798a7 100644 --- a/infer/models/c/src/infer_builtins.h +++ b/infer/models/c/src/infer_builtins.h @@ -57,7 +57,10 @@ clock_t __infer_nondet_clock_t(); if (cond) \ while (1) -// builtin: force arr to be an array and return the size +// builtin: force arr to be an array +extern void __require_allocated_array(const void* arr); + +// builtin: return the size of arr extern size_t __get_array_size(const void* arr); // builtin: change the attribute of ret to a file attribute diff --git a/infer/models/c/src/libc_basic.c b/infer/models/c/src/libc_basic.c index b5ee70217..c52aa845a 100644 --- a/infer/models/c/src/libc_basic.c +++ b/infer/models/c/src/libc_basic.c @@ -83,8 +83,9 @@ char* strcpy(char* s1, const char* s2) { int size2; __infer_set_flag("ignore_return", ""); // no warnings if the return value is ignored - + __require_allocated_array(s1); size1 = __get_array_size(s1); + __require_allocated_array(s2); size2 = __get_array_size(s2); INFER_EXCLUDE_CONDITION(size2 > size1); return s1; @@ -94,6 +95,7 @@ char* strcpy(char* s1, const char* s2) { // size char* strdup(const char* s) { int size; + __require_allocated_array(s); size = __get_array_size(s); return (char*)malloc(size); } @@ -103,8 +105,9 @@ char* strdup(const char* s) { char* strcat(char* s1, const char* s2) { int size1; int size2; - + __require_allocated_array(s1); size1 = __get_array_size(s1); + __require_allocated_array(s2); size2 = __get_array_size(s2); INFER_EXCLUDE_CONDITION(size2 > size1); return s1; @@ -129,6 +132,7 @@ char* strchr(char* s, int c) throw() { nondet = __infer_nondet_int(); offset = __infer_nondet_int(); + __require_allocated_array(s); size = __get_array_size(s); if (nondet) return 0; @@ -150,13 +154,11 @@ char* strrchr(char* s, int c) throw() { return strchr(s, c); } // s1 and s2 must be allocated. // return a non-deterministic integer int strcmp(const char* s1, const char* s2) { - int size_s1; - int size_s2; int res; res = __infer_nondet_int(); - size_s1 = __get_array_size(s1); - size_s2 = __get_array_size(s2); + __require_allocated_array(s1); + __require_allocated_array(s2); return res; } @@ -164,6 +166,7 @@ int strcmp(const char* s1, const char* s2) { // return the size of the buffer - 1 size_t strlen(const char* s) { int size; + __require_allocated_array(s); size = __get_array_size(s); return size - 1; } @@ -171,8 +174,7 @@ size_t strlen(const char* s) { // s must be allocated // return s char* strlwr(char* s) { - int size1; - size1 = __get_array_size(s); + __require_allocated_array(s); return s; } @@ -182,8 +184,9 @@ char* strlwr(char* s) { char* strncat(char* s1, const char* s2, size_t n) { int size_s1; int size_s2; - + __require_allocated_array(s1); size_s1 = __get_array_size(s1); + __require_allocated_array(s2); size_s2 = __get_array_size(s2); INFER_EXCLUDE_CONDITION((n > size_s1) || (n > size_s2)); return s1; @@ -197,8 +200,9 @@ int strncmp(const char* s1, const char* s2, size_t n) { int size_s2; int res; res = __infer_nondet_int(); - + __require_allocated_array(s1); size_s1 = __get_array_size(s1); + __require_allocated_array(s2); size_s2 = __get_array_size(s2); INFER_EXCLUDE_CONDITION((n > size_s1) || (n > size_s2)); return res; @@ -208,12 +212,12 @@ int strncmp(const char* s1, const char* s2, size_t n) { // check that n characters fit in s1 (because even if s2 is shorter than n, null // characters are appended to s1) char* strncpy(char* s1, const char* s2, size_t n) { - int size1, size2; + int size1; __infer_set_flag("ignore_return", ""); // no warnings if the return value is ignored - + __require_allocated_array(s1); size1 = __get_array_size(s1); - size2 = __get_array_size(s2); + __require_allocated_array(s2); INFER_EXCLUDE_CONDITION(n > size1); return s1; } @@ -227,14 +231,14 @@ const char* strpbrk(const char* s1, const char* s2) throw() { char* strpbrk(char* s1, const char* s2) throw() { #endif - int size1, size2; + int size1; int nondet; int offset; nondet = __infer_nondet_int(); offset = __infer_nondet_int(); - + __require_allocated_array(s1); size1 = __get_array_size(s1); - size2 = __get_array_size(s2); + __require_allocated_array(s2); if (nondet) return 0; INFER_EXCLUDE_CONDITION(offset < 0 || offset >= size1); @@ -245,12 +249,11 @@ char* strpbrk(char* s1, const char* s2) throw() { // return an integer between 0 ans the size of s1 size_t strspn(const char* s1, const char* s2) { int size_s1; - int size_s2; int res; res = __infer_nondet_int(); - + __require_allocated_array(s1); size_s1 = __get_array_size(s1); - size_s2 = __get_array_size(s2); + __require_allocated_array(s2); INFER_EXCLUDE_CONDITION(res < 0 || res > size_s1); return res; } @@ -270,9 +273,9 @@ char* strstr(char* s1, const char* s2) throw() { int offset; nondet = __infer_nondet_int(); offset = __infer_nondet_int(); - + __require_allocated_array(s1); size1 = __get_array_size(s1); - size2 = __get_array_size(s2); + __require_allocated_array(s2); if (nondet) return 0; INFER_EXCLUDE_CONDITION(offset < 0 || offset >= size1); @@ -296,6 +299,7 @@ unsigned long strtoul(const char* str, char** endptr, int base) { int size; int offset; int res; + __require_allocated_array(str); size = __get_array_size(str); offset = __infer_nondet_int(); INFER_EXCLUDE_CONDITION(offset < 0 || offset >= size); @@ -311,8 +315,7 @@ unsigned long strtoul(const char* str, char** endptr, int base) { // s must be allocated // return s char* strupr(char* s) { - int size1; - size1 = __get_array_size(s); + __require_allocated_array(s); return s; } @@ -334,7 +337,7 @@ void* memchr(void* s, int c, size_t n) throw() { int offset; nondet = __infer_nondet_int(); offset = __infer_nondet_int(); - + __require_allocated_array(s); size = __get_array_size(s); INFER_EXCLUDE_CONDITION(n > size); if (nondet) @@ -349,8 +352,9 @@ void* memchr(void* s, int c, size_t n) throw() { int memcmp(const void* s1, const void* s2, size_t n) { int size_s1; int size_s2; - + __require_allocated_array(s1); size_s1 = __get_array_size(s1); + __require_allocated_array(s2); size_s2 = __get_array_size(s2); INFER_EXCLUDE_CONDITION((n > size_s1) || (n > size_s2)); return __infer_nondet_int(); @@ -363,8 +367,9 @@ void* memcpy(void* s1, const void* s2, size_t n) { int size_s2; __infer_set_flag("ignore_return", ""); // no warnings if the return value is ignored - + __require_allocated_array(s1); size_s1 = __get_array_size(s1); + __require_allocated_array(s2); size_s2 = __get_array_size(s2); INFER_EXCLUDE_CONDITION((n < 0) || (n > size_s1) || (n > size_s2)); return s1; @@ -383,7 +388,7 @@ void* memset(void* s, int c, size_t n) { int size_s; __infer_set_flag("ignore_return", ""); // no warnings if the return value is ignored - + __require_allocated_array(s); size_s = __get_array_size(s); INFER_EXCLUDE_CONDITION(n > size_s); return s; @@ -428,6 +433,7 @@ char* tmpnam(char* s) { if (!success) return NULL; if (s) { + __require_allocated_array(s); size = __get_array_size(s); INFER_EXCLUDE_CONDITION(size < L_tmpnam); return s; @@ -525,6 +531,7 @@ char* fgets(char* str, int num, FILE* stream) { n = __infer_nondet_int(); if (n > 0) { + __require_allocated_array(str); size1 = __get_array_size(str); INFER_EXCLUDE_CONDITION(num > size1); return str; @@ -535,9 +542,8 @@ char* fgets(char* str, int num, FILE* stream) { // string s must be allocated; return nondeterministically s or NULL char* gets(char* s) { int n; - int size; - size = __get_array_size(s); + __require_allocated_array(s); n = __infer_nondet_int(); if (n) return s; @@ -547,8 +553,7 @@ char* gets(char* s) { // str must be allocated, return a nondeterministic value int puts(const char* str) { - int size1; - size1 = __get_array_size(str); + __require_allocated_array(str); return __infer_nondet_int(); } @@ -605,6 +610,7 @@ char* getcwd(char* buffer, size_t size) { n = __infer_nondet_int(); if (n > 0) { + __require_allocated_array(buffer); size_buf = __get_array_size(buffer); INFER_EXCLUDE_CONDITION(size > size_buf); return buffer; @@ -739,9 +745,8 @@ void* realloc(void* ptr, size_t size) { if (ptr == 0) { // if ptr in NULL, behave as malloc return malloc(size); } - int old_size; int can_enlarge; - old_size = __get_array_size(ptr); // force ptr to be an array + __require_allocated_array(ptr); can_enlarge = __infer_nondet_int(); // nondeterministically choose whether the // current block can be enlarged if (can_enlarge) { @@ -842,10 +847,9 @@ extern struct dirent* _dirent_global; // dirp must be allocated // return 0 or the allocated pointerq _dirent_global, nondeterministically struct dirent* readdir(DIR* dirp) { - int len; int nondet; struct dirent* ret = _dirent_global; - len = __get_array_size(dirp); + __require_allocated_array(dirp); nondet = __infer_nondet_int(); if (nondet) return 0; @@ -857,10 +861,9 @@ extern char* _getenv_global; // string name must be allocated // return 0 or the allocated string _getenv_global, nondeterministically char* getenv(const char* name) { - int size; int nondet; - size = __get_array_size(name); - size = __get_array_size(_getenv_global); + __require_allocated_array(name); + __require_allocated_array(_getenv_global); nondet = __infer_nondet_int(); if (nondet) return 0; @@ -872,10 +875,9 @@ extern char* _locale_global; // string locale must be allocated // return 0 or the allocated string _locale_global, nondeterministically char* setlocale(int category, const char* locale) { - int size; int nondet; - size = __get_array_size(locale); - size = __get_array_size(_locale_global); + __require_allocated_array(locale); + __require_allocated_array(_locale_global); nondet = __infer_nondet_int(); if (nondet) return 0; @@ -993,8 +995,7 @@ extern struct passwd* _getpwnam_global; // return either NULL or the global variable _getpnam_global struct passwd* getpwnam(const char* login) { int found; - int size1; - size1 = __get_array_size(login); + __require_allocated_array(login); found = __infer_nondet_int(); if (found) return _getpwnam_global; @@ -1025,7 +1026,7 @@ extern char* _getlogin_global; char* getlogin() { int size; int nondet; - size = __get_array_size(_getlogin_global); + __require_allocated_array(_getlogin_global); nondet = __infer_nondet_int(); if (nondet) return 0; @@ -1034,8 +1035,7 @@ char* getlogin() { int setlogin(const char* name) { int success; - int size1; - size1 = __get_array_size(name); + __require_allocated_array(name); success = __infer_nondet_int(); if (success) { strcpy(_getlogin_global, name); @@ -1049,9 +1049,8 @@ extern char* _getpass_global; // prompt must be allocated // return the global variable _getpass_global, which must be allocated char* getpass(const char* prompt) { - int size1; - size1 = __get_array_size(prompt); - size1 = __get_array_size(_getpass_global); + __require_allocated_array(prompt); + __require_allocated_array(_getpass_global); return _getpass_global; } @@ -1086,8 +1085,7 @@ int snprintf(char* __restrict s, size_t n, const char* __restrict format, ...) { // return a nondeterministic nonnegative integer int sprintf(char* s, const char* format, ...) { int res; - int size1; - size1 = __get_array_size(s); + __require_allocated_array(s); res = __infer_nondet_int(); INFER_EXCLUDE_CONDITION(res < 0); return res; @@ -1132,10 +1130,9 @@ int vprintf(const char* format, va_list arg) { // forces path to be allocated // return nondeterministically 0 or -1 int utimes(const char* path, const struct timeval times[2]) { - int size1; int success = __infer_nondet_int(); - size1 = __get_array_size(path); + __require_allocated_array(path); // return random result return (success > 0) ? 0 : -1; } @@ -1143,9 +1140,8 @@ int utimes(const char* path, const struct timeval times[2]) { // forces filename to be allocated // return nondeterministically 0 or -1 int unlink(const char* filename) { - int size1; int success = __infer_nondet_int(); - size1 = __get_array_size(filename); + __require_allocated_array(filename); return (success > 0) ? 0 : -1; } @@ -1158,16 +1154,16 @@ int usleep(useconds_t useconds) { // dst and src must be allocated // return an integer between 0 and size size_t strlcpy(char* dst, const char* src, size_t size) { - int size_src; int size_dst; int res; res = __infer_nondet_int(); // force src to be allocated - size_src = __get_array_size(src); + __require_allocated_array(src); // force dst to be allocated for at least size + __require_allocated_array(dst); size_dst = __get_array_size(dst); INFER_EXCLUDE_CONDITION(size > size_dst); @@ -1179,16 +1175,16 @@ size_t strlcpy(char* dst, const char* src, size_t size) { // dst and src must be allocated // return an integer between 0 and size size_t strlcat(char* dst, const char* src, size_t size) { - int size_src; int size_dst; int res; res = __infer_nondet_int(); // force src to be allocated - size_src = __get_array_size(src); + __require_allocated_array(src); // force dst to be allocated for at least size + __require_allocated_array(dst); size_dst = __get_array_size(dst); INFER_EXCLUDE_CONDITION(size > size_dst); @@ -1202,12 +1198,11 @@ size_t strlcat(char* dst, const char* src, size_t size) { // return 0 or -1 int statfs(const char* path, struct statfs* buf) { int success; - int size_path; success = __infer_nondet_int(); // force path to be allocated - size_path = __get_array_size(path); + __require_allocated_array(path); struct statfs s; // uninitialized struct statfs *buf = s; @@ -1220,12 +1215,11 @@ int statfs(const char* path, struct statfs* buf) { // return 0 or -1 int stat(const char* path, struct stat* buf) { int success; - int size_path; success = __infer_nondet_int(); // force path to be allocated - size_path = __get_array_size(path); + __require_allocated_array(path); struct stat s; // uninitialized struct stat *buf = s; @@ -1234,24 +1228,22 @@ int stat(const char* path, struct stat* buf) { } int remove(const char* path) { - int size_path; int success; // force path to be allocated - size_path = __get_array_size(path); + __require_allocated_array(path); success = __infer_nondet_int(); return (success > 0) ? 0 : -1; } char* readline(const char* prompt) { - int size_prompt; char* ret; int size; // force prompt to be allocated when not null if (prompt != NULL) { - size_prompt = __get_array_size(prompt); + __require_allocated_array(prompt); } // return random string of positive size @@ -1284,11 +1276,10 @@ int putc(int c, FILE* stream) { } int access(const char* path, int mode) { - int size; int success; // force path to be allocated - size = __get_array_size(path); + __require_allocated_array(path); // determine return value success = __infer_nondet_int(); @@ -1297,7 +1288,6 @@ int access(const char* path, int mode) { } size_t confstr(int name, char* buf, size_t len) { - int size; int ret; // determine return value @@ -1306,7 +1296,7 @@ size_t confstr(int name, char* buf, size_t len) { // buf should be allocated if len is not zero. Otherwise, we want buf=0. if (len) - size = __get_array_size(buf); + __require_allocated_array(buf); else INFER_EXCLUDE_CONDITION(buf != 0); @@ -1339,13 +1329,11 @@ int fsctl(const char* path, unsigned long request, void* data, unsigned int options) { - int size1; - int size2; int ret; // forces path and data to be allocated - size1 = __get_array_size(path); - size2 = __get_array_size(data); + __require_allocated_array(path); + __require_allocated_array(data); ret = __infer_nondet_int(); INFER_EXCLUDE_CONDITION(ret < -1 || ret > 0); @@ -1403,10 +1391,9 @@ struct tm* localtime_r(const time_t* __restrict timer, } int mkdir(const char* filename, mode_t mode) { - int size; int ret; - size = __get_array_size(filename); + __require_allocated_array(filename); ret = __infer_nondet_int(); INFER_EXCLUDE_CONDITION(ret < -1 || ret > 0); @@ -1528,8 +1515,7 @@ int isatty(int fildes) { } void perror(const char* s) { - int size = __get_array_size(s); - size = 0; + __require_allocated_array(s); } int pipe(int fildes[2]) { @@ -1543,6 +1529,7 @@ int raise(int sig) { return __infer_nondet_int(); } ssize_t read(int fildes, void* buf, size_t nbyte) { if (nbyte == 0) return 0; + __require_allocated_array(buf); INFER_EXCLUDE_CONDITION(__get_array_size(buf) < nbyte); int ret = __infer_nondet_int(); @@ -1661,10 +1648,8 @@ size_t fwrite(const void* __restrict ptr, } size_t strcspn(const char* s1, const char* s2) { - int size1, size2; - size1 = __get_array_size(s1); - size2 = __get_array_size(s2); - ; + __require_allocated_array(s1); + __require_allocated_array(s2); int ret = __infer_nondet_int(); INFER_EXCLUDE_CONDITION(ret < 0); @@ -1676,6 +1661,7 @@ size_t strcspn(const char* s1, const char* s2) { // It's not modelled right now #if defined __APPLE__ || (defined __USE_XOPEN2K && !defined __USE_GNU) int strerror_r(int errnum, char* strerrbuf, size_t buflen) { + __require_allocated_array(strerrbuf); INFER_EXCLUDE_CONDITION(__get_array_size(strerrbuf) < buflen); return __infer_nondet_int(); @@ -1683,6 +1669,7 @@ int strerror_r(int errnum, char* strerrbuf, size_t buflen) { #endif ssize_t write(int fildes, const void* buf, size_t nbyte) { + __require_allocated_array(buf); INFER_EXCLUDE_CONDITION(__get_array_size(buf) < nbyte); int ret = __infer_nondet_int(); @@ -1691,8 +1678,7 @@ ssize_t write(int fildes, const void* buf, size_t nbyte) { } int creat(const char* path, mode_t mode) { - int size; - size = __get_array_size(path); + __require_allocated_array(path); int ret = __infer_nondet_int(); INFER_EXCLUDE_CONDITION(ret < -1); @@ -1741,7 +1727,7 @@ void* bsearch(const void* key, int offset; nondet = __infer_nondet_int(); offset = __infer_nondet_int(); - + __require_allocated_array(base); base_size = __get_array_size(base); INFER_EXCLUDE_CONDITION(nmemb > base_size); if (nondet) diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 7665e1f4f..c06f873bd 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1678,6 +1678,12 @@ module ModelBuiltins = struct let mk_empty_array size = Sil.Earray (size, [], Sil.inst_none) + (* Make a rearranged array. As it is rearranged when it appears in a precondition + it requires that the function is called with the array allocated. If not infer + return a null pointer deref *) + let mk_empty_array_rearranged size = + Sil.Earray (size, [], Sil.inst_rearrange true (State.get_loc ()) (State.get_path_pos ())) + let extract_array_type typ = if (!Config.curr_language = Config.Java) then match typ with @@ -1695,73 +1701,76 @@ module ModelBuiltins = struct | [ret_id] -> Prop.conjoin_eq e (Sil.Var ret_id) prop | _ -> prop - let execute___get_array_size _ pdesc _ _ _prop path ret_ids args _ _ + (* Add an array of typ pointed to by lexp to prop_ if it doesnt exist alread*) + (* Return the new prop and the array size *) + (* Return None if it fails to add the array *) + let add_array_to_prop pdesc prop_ lexp typ = + let pname = Cfg.Procdesc.get_proc_name pdesc in + let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in + begin + try + let hpred = IList.find (function + | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp + | _ -> false) (Prop.get_sigma prop) in + match hpred with + | Sil.Hpointsto(_, Sil.Earray(size, _, _), _) -> + Some (size, prop) + | _ -> None (* e points to something but not an array *) + with Not_found -> (* e is not allocated, so we can add the array *) + let otyp' = (extract_array_type typ) in + match otyp' with + | Some typ' -> + let size = Sil.Var(Ident.create_fresh Ident.kfootprint) in + let s = mk_empty_array_rearranged size in + let hpred = + Prop.mk_ptsto n_lexp s (Sil.Sizeof(Sil.Tarray(typ', size), Sil.Subtype.exact)) in + let sigma = Prop.get_sigma prop in + let sigma_fp = Prop.get_sigma_footprint prop in + let prop'= Prop.replace_sigma (hpred:: sigma) prop in + let prop''= Prop.replace_sigma_footprint (hpred:: sigma_fp) prop' in + let prop''= Prop.normalize prop'' in + Some (size, prop'') + | _ -> None + end + + (* Add an array in prop if it is not allocated.*) + let execute___require_allocated_array _ pdesc _ _ prop_ path ret_ids args _ _ : Builtin.ret_typ = match args with | [(lexp, typ)] when IList.length ret_ids <= 1 -> - let pname = Cfg.Procdesc.get_proc_name pdesc in - let return_result_for_array_size e prop ret_ids = return_result e prop ret_ids in - let n_lexp, prop = exp_norm_check_arith pname _prop lexp in - begin - try - let hpred = IList.find (function - | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp - | _ -> false) (Prop.get_sigma prop) in - match hpred with - | Sil.Hpointsto(_, Sil.Earray(size, _, _), _) -> - [(return_result_for_array_size size prop ret_ids, path)] - | _ -> [] - with Not_found -> - let otyp' = (extract_array_type typ) in - match otyp' with - | Some typ' -> - let size = Sil.Var(Ident.create_fresh Ident.kfootprint) in - let s = mk_empty_array size in - let hpred = Prop.mk_ptsto n_lexp s (Sil.Sizeof(Sil.Tarray(typ', size), Sil.Subtype.exact)) in - let sigma = Prop.get_sigma prop in - let sigma_fp = Prop.get_sigma_footprint prop in - let prop'= Prop.replace_sigma (hpred:: sigma) prop in - let prop''= Prop.replace_sigma_footprint (hpred:: sigma_fp) prop' in - let prop''= Prop.normalize prop'' in - [(return_result_for_array_size size prop'' ret_ids, path)] - | _ -> [] - end + (match add_array_to_prop pdesc prop_ lexp typ with + | None -> [] + | Some (_, prop) -> [(prop, path)]) | _ -> raise (Exceptions.Wrong_argument_number __POS__) - let execute___set_array_size _ pdesc _ _ _prop path ret_ids args _ _ + let execute___get_array_size _ pdesc _ _ prop_ path ret_ids args _ _ + : Builtin.ret_typ = + match args with + | [(lexp, typ)] when IList.length ret_ids <= 1 -> + (match add_array_to_prop pdesc prop_ lexp typ with + | None -> [] + | Some (size, prop) -> [(return_result size prop ret_ids, path)]) + | _ -> raise (Exceptions.Wrong_argument_number __POS__) + + let execute___set_array_size _ pdesc _ _ prop_ path ret_ids args _ _ : Builtin.ret_typ = match args, ret_ids with - | [(lexp, typ); (size, _)], [] -> - let pname = Cfg.Procdesc.get_proc_name pdesc in - let n_lexp, _prop' = exp_norm_check_arith pname _prop lexp in - let n_size, prop = exp_norm_check_arith pname _prop' size in - begin - try - let hpred, sigma' = IList.partition (function - | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp - | _ -> false) (Prop.get_sigma prop) in - match hpred with - | [Sil.Hpointsto(e, Sil.Earray(_, esel, inst), t)] -> - let hpred' = Sil.Hpointsto (e, Sil.Earray (n_size, esel, inst), t) in - let prop' = Prop.replace_sigma (hpred':: sigma') prop in - [(Prop.normalize prop', path)] - | _ -> raise Not_found - with Not_found -> - match typ with - | Sil.Tptr (typ', _) -> - let size_fp = Sil.Var(Ident.create_fresh Ident.kfootprint) in - let se = mk_empty_array n_size in - let se_fp = mk_empty_array size_fp in - let hpred = Prop.mk_ptsto n_lexp se (Sil.Sizeof(Sil.Tarray(typ', size), Sil.Subtype.exact)) in - let hpred_fp = Prop.mk_ptsto n_lexp se_fp (Sil.Sizeof(Sil.Tarray(typ', size_fp), Sil.Subtype.exact)) in - let sigma = Prop.get_sigma prop in - let sigma_fp = Prop.get_sigma_footprint prop in - let prop'= Prop.replace_sigma (hpred:: sigma) prop in - let prop''= Prop.replace_sigma_footprint (hpred_fp:: sigma_fp) prop' in - let prop''= Prop.normalize prop'' in - [(prop'', path)] - | _ -> [] - end + | [(lexp, typ); (size, _)], []-> + (match add_array_to_prop pdesc prop_ lexp typ with + | None -> [] + | Some (_, prop_a) -> (* Invariant: prop_a has an array pointed to by lexp *) + let pname = Cfg.Procdesc.get_proc_name pdesc in + let n_lexp, _prop' = exp_norm_check_arith pname prop_a lexp in + let n_size, prop = exp_norm_check_arith pname _prop' size in + let hpred, sigma' = IList.partition (function + | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp + | _ -> false) (Prop.get_sigma prop) in + (match hpred with + | [Sil.Hpointsto(e, Sil.Earray(_, esel, inst), t)] -> + let hpred' = Sil.Hpointsto (e, Sil.Earray (n_size, esel, inst), t) in + let prop' = Prop.replace_sigma (hpred':: sigma') prop in + [(Prop.normalize prop', path)] + | _ -> [])) (* by construction of prop_a this case is impossible *) | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute___print_value _ pdesc _ _ prop path _ args _ _ @@ -2532,6 +2541,9 @@ module ModelBuiltins = struct let __get_array_size = Builtin.register (* return the size of the array passed as a parameter *) "__get_array_size" execute___get_array_size + let __require_allocated_array = Builtin.register + (* require the parameter to point to an allocated array *) + "__require_allocated_array" execute___require_allocated_array let _ = Builtin.register (* return the value of a hidden field in the struct *) "__get_hidden_field" execute___get_hidden_field diff --git a/infer/tests/codetoanalyze/c/errors/memory_leaks/test.c b/infer/tests/codetoanalyze/c/errors/memory_leaks/test.c index 2e719a6b4..db964e9de 100644 --- a/infer/tests/codetoanalyze/c/errors/memory_leaks/test.c +++ b/infer/tests/codetoanalyze/c/errors/memory_leaks/test.c @@ -38,4 +38,10 @@ void uses_allocator() { *p = 42; } -void* builtin_no_leak(size_t s) { return memset(malloc(s), 0, s); } +void* builtin_no_leak(size_t s) { + + char* str = malloc(sizeof(s)); + if (str) { + return memset(str, 0, s); + } +} diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/memcpy-test.c b/infer/tests/codetoanalyze/c/errors/null_dereference/memcpy-test.c new file mode 100644 index 000000000..7fc3bffa6 --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/null_dereference/memcpy-test.c @@ -0,0 +1,45 @@ +/* + * Copyright (c) 2016 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +struct X { + int f; +}; + +typedef struct X X; + +void testOK() { + X x; + X* p = malloc(sizeof(X)); + if (p) + memcpy(p, &x, sizeof(X)); + free(p); +} + +void testError1() { + X x; + X* p = 0; + memcpy(p, &x, sizeof(X)); // crash +} + +void testError2() { + X x; + X* r; + X* p = 0; + r = p; + memcpy(r, &x, sizeof(X)); // crash +} + +void testError3() { + X* x = 0; + X* p = malloc(sizeof(X)); + if (p) { + memcpy(p, x, sizeof(X)); // crash + free(p); + } +} diff --git a/infer/tests/endtoend/c/NullDereferenceTest3.java b/infer/tests/endtoend/c/NullDereferenceTest3.java new file mode 100644 index 000000000..3c03f8b12 --- /dev/null +++ b/infer/tests/endtoend/c/NullDereferenceTest3.java @@ -0,0 +1,59 @@ +/* + * Copyright (c) 2013 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package endtoend.c; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; +import static utils.matchers.ResultContainsLineNumbers.containsLines; + +import org.junit.BeforeClass; +import org.junit.Test; + +import java.io.IOException; + +import utils.InferException; +import utils.InferResults; + +public class NullDereferenceTest3 { + + public static final String SOURCE_FILE = + "null_dereference/memcpy-test.c"; + + + public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE"; + + private static InferResults inferResults; + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferResults = InferResults.loadCInferResults( + NullDereferenceTest3.class, + SOURCE_FILE); + } + + @Test + public void nullDereferenceTest() throws InterruptedException, IOException, InferException { + String[] procedures = { + "testError1", + "testError2", + "testError3", + }; + assertThat( + "Results should contain null pointer dereference error", + inferResults, + containsExactly( + NULL_DEREFERENCE, + SOURCE_FILE, + procedures + ) + ); + } + +}