diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 1808014654..7bc589df20 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2002,6 +2002,16 @@ struct let st' = invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) gs st shallow_addrs in invalidate ~deep:true ~ctx (Analyses.ask_of_ctx ctx) gs st' deep_addrs + let check_free_of_non_heap_mem ctx special_fn ptr = + match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with + | Address a -> + let points_to_set = addrToLvalSet a in + if Q.LS.is_top points_to_set then + M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potential free of non-dynamically allocated memory may occur" d_exp ptr special_fn.vname + else if (Q.LS.exists (fun (v, _) -> not (ctx.ask (Q.IsHeapVar v))) points_to_set) || (AD.mem Addr.UnknownPtr a) then + M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr + | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname + let special ctx (lv:lval option) (f: varinfo) (args: exp list) = let invalidate_ret_lv st = match lv with | Some lv -> @@ -2282,6 +2292,8 @@ struct | _ -> st end | Realloc { ptr = p; size }, _ -> + (* Realloc shouldn't be passed non-dynamically allocated memory *) + check_free_of_non_heap_mem ctx f p; begin match lv with | Some lv -> let ask = Analyses.ask_of_ctx ctx in @@ -2313,6 +2325,10 @@ struct | None -> st end + | Free ptr, _ -> + (* Free shouldn't be passed non-dynamically allocated memory *) + check_free_of_non_heap_mem ctx f ptr; + st | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine | Setjmp { env }, _ -> let ask = Analyses.ask_of_ctx ctx in diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml index ddf91dba0b..5452225c26 100644 --- a/src/util/messageCategory.ml +++ b/src/util/messageCategory.ml @@ -12,6 +12,7 @@ type undefined_behavior = | NullPointerDereference | UseAfterFree | DoubleFree + | InvalidMemoryDeallocation | Uninitialized | DoubleLocking | Other @@ -65,6 +66,7 @@ struct let nullpointer_dereference: category = create @@ NullPointerDereference let use_after_free: category = create @@ UseAfterFree let double_free: category = create @@ DoubleFree + let invalid_memory_deallocation: category = create @@ InvalidMemoryDeallocation let uninitialized: category = create @@ Uninitialized let double_locking: category = create @@ DoubleLocking let other: category = create @@ Other @@ -102,6 +104,7 @@ struct | "nullpointer_dereference" -> nullpointer_dereference | "use_after_free" -> use_after_free | "double_free" -> double_free + | "invalid_memory_deallocation" -> invalid_memory_deallocation | "uninitialized" -> uninitialized | "double_locking" -> double_locking | "other" -> other @@ -113,6 +116,7 @@ struct | NullPointerDereference -> ["NullPointerDereference"] | UseAfterFree -> ["UseAfterFree"] | DoubleFree -> ["DoubleFree"] + | InvalidMemoryDeallocation -> ["InvalidMemoryDeallocation"] | Uninitialized -> ["Uninitialized"] | DoubleLocking -> ["DoubleLocking"] | Other -> ["Other"] @@ -223,6 +227,7 @@ let behaviorName = function |NullPointerDereference -> "NullPointerDereference" |UseAfterFree -> "UseAfterFree" |DoubleFree -> "DoubleFree" + |InvalidMemoryDeallocation -> "InvalidMemoryDeallocation" |Uninitialized -> "Uninitialized" |DoubleLocking -> "DoubleLocking" |Other -> "Other" diff --git a/tests/regression/75-invalid_dealloc/01-invalid-dealloc-simple.c b/tests/regression/75-invalid_dealloc/01-invalid-dealloc-simple.c new file mode 100644 index 0000000000..16fbd593f4 --- /dev/null +++ b/tests/regression/75-invalid_dealloc/01-invalid-dealloc-simple.c @@ -0,0 +1,14 @@ +#include + +int main(int argc, char const *argv[]) +{ + int a; + int *p = &a; + free(p); //WARN + + char b = 'b'; + char *p2 = &b; + free(p2); //WARN + + return 0; +} diff --git a/tests/regression/75-invalid_dealloc/02-invalid-dealloc-struct.c b/tests/regression/75-invalid_dealloc/02-invalid-dealloc-struct.c new file mode 100644 index 0000000000..6768103976 --- /dev/null +++ b/tests/regression/75-invalid_dealloc/02-invalid-dealloc-struct.c @@ -0,0 +1,14 @@ +#include + +typedef struct custom_t { + int x; + int y; +} custom_t; + +int main(int argc, char const *argv[]) +{ + custom_t *var; + free(var); //WARN + + return 0; +} diff --git a/tests/regression/75-invalid_dealloc/03-invalid-dealloc-array.c b/tests/regression/75-invalid_dealloc/03-invalid-dealloc-array.c new file mode 100644 index 0000000000..c023b5fc53 --- /dev/null +++ b/tests/regression/75-invalid_dealloc/03-invalid-dealloc-array.c @@ -0,0 +1,25 @@ +#include + +typedef struct custom_t { + int x; + int y; +} custom_t; + +#define MAX_SIZE 5000 + +int main(int argc, char const *argv[]) +{ + custom_t custom_arr[MAX_SIZE]; + free(custom_arr); //WARN + + int int_arr[MAX_SIZE]; + free(int_arr); //WARN + + char char_arr[MAX_SIZE]; + free(char_arr); //WARN + + char char_arr2[1]; + free(char_arr2); //WARN + + return 0; +} diff --git a/tests/regression/75-invalid_dealloc/04-invalid-realloc.c b/tests/regression/75-invalid_dealloc/04-invalid-realloc.c new file mode 100644 index 0000000000..94cbf031c2 --- /dev/null +++ b/tests/regression/75-invalid_dealloc/04-invalid-realloc.c @@ -0,0 +1,25 @@ +#include + +typedef struct custom_t { + int x; + int y; +} custom_t; + +#define MAX_SIZE 5000 + +int main(int argc, char const *argv[]) +{ + custom_t custom_arr[10]; + realloc(custom_arr, MAX_SIZE); //WARN + + int int_arr[100]; + realloc(int_arr, MAX_SIZE); //WARN + + char char_arr[1000]; + realloc(char_arr, MAX_SIZE); //WARN + + char char_arr2[1]; + realloc(char_arr2, MAX_SIZE); //WARN + + return 0; +}