diff --git a/src/analyses/base.ml b/src/analyses/base.ml index a213170ba2..824fde18d9 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1262,13 +1262,8 @@ struct match p with | Address a -> let s = addrToLvalSet a in - let has_offset = function - | `NoOffset -> false - | `Field _ - | `Index _ -> true - in (* If there's a non-heap var or an offset in the lval set, we answer with bottom *) - if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || has_offset o) s then + if ValueDomainQueries.LS.exists (fun (v, o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset) s then Queries.Result.bot q else ( let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in @@ -2013,14 +2008,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 = + let check_invalid_mem_dealloc 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 + M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potentially invalid memory deallocation 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 + else if Q.LS.exists (fun (_, o) -> Offset.Exp.cmp_zero_offset o <> `MustZero) points_to_set then + M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer 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) = @@ -2304,7 +2301,7 @@ struct end | Realloc { ptr = p; size }, _ -> (* Realloc shouldn't be passed non-dynamically allocated memory *) - check_free_of_non_heap_mem ctx f p; + check_invalid_mem_dealloc ctx f p; begin match lv with | Some lv -> let ask = Analyses.ask_of_ctx ctx in @@ -2338,7 +2335,7 @@ struct end | Free ptr, _ -> (* Free shouldn't be passed non-dynamically allocated memory *) - check_free_of_non_heap_mem ctx f ptr; + check_invalid_mem_dealloc ctx f ptr; st | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine | Setjmp { env }, _ -> diff --git a/tests/regression/75-invalid_dealloc/05-free-at-offset.c b/tests/regression/75-invalid_dealloc/05-free-at-offset.c new file mode 100644 index 0000000000..c9ec66c769 --- /dev/null +++ b/tests/regression/75-invalid_dealloc/05-free-at-offset.c @@ -0,0 +1,9 @@ +#include + +int main(int argc, char const *argv[]) { + char *ptr = malloc(42 * sizeof(char)); + ptr = ptr + 7; + free(ptr); //WARN + + return 0; +} diff --git a/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c b/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c new file mode 100644 index 0000000000..64a42654e1 --- /dev/null +++ b/tests/regression/75-invalid_dealloc/06-realloc-at-offset.c @@ -0,0 +1,11 @@ +#include + +#define MAX_SIZE 5000 + +int main(int argc, char const *argv[]) { + char *ptr = malloc(42 * sizeof(char)); + ptr = ptr + 7; + realloc(ptr, MAX_SIZE); //WARN + + return 0; +} diff --git a/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c b/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c new file mode 100644 index 0000000000..f64d66d8fc --- /dev/null +++ b/tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c @@ -0,0 +1,15 @@ +#include + +typedef struct custom_t { + char *x; + int y; +} custom_t; + +int main(int argc, char const *argv[]) { + custom_t *struct_ptr = malloc(sizeof(custom_t)); + struct_ptr->x = malloc(10 * sizeof(char)); + free(&struct_ptr->x); //NOWARN + free(&struct_ptr->y); //WARN + free(struct_ptr); //NOWARN + return 0; +} diff --git a/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c b/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c new file mode 100644 index 0000000000..fddb8a7694 --- /dev/null +++ b/tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c @@ -0,0 +1,15 @@ +#include + +typedef struct custom_t { + char *x; + int y; +} custom_t; + +int main(int argc, char const *argv[]) { + custom_t *struct_ptr = malloc(sizeof(custom_t)); + struct_ptr->x = malloc(10 * sizeof(char)); + realloc(&struct_ptr->x, 50); //NOWARN + realloc(&struct_ptr->y, 50); //WARN + realloc(struct_ptr, 2 * sizeof(custom_t)); //NOWARN + return 0; +}