Skip to content

Commit

Permalink
Merge pull request #1139 from mrstanb/detect-deallocation-at-offset
Browse files Browse the repository at this point in the history
Detect memory deallocation at offset from memory start
  • Loading branch information
michael-schwarz authored Aug 22, 2023
2 parents a135dea + 92c0dca commit 1da8e97
Show file tree
Hide file tree
Showing 5 changed files with 57 additions and 10 deletions.
17 changes: 7 additions & 10 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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) =
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 }, _ ->
Expand Down
9 changes: 9 additions & 0 deletions tests/regression/75-invalid_dealloc/05-free-at-offset.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
#include <stdlib.h>

int main(int argc, char const *argv[]) {
char *ptr = malloc(42 * sizeof(char));
ptr = ptr + 7;
free(ptr); //WARN

return 0;
}
11 changes: 11 additions & 0 deletions tests/regression/75-invalid_dealloc/06-realloc-at-offset.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
#include <stdlib.h>

#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;
}
15 changes: 15 additions & 0 deletions tests/regression/75-invalid_dealloc/07-free-at-struct-offset.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
#include <stdlib.h>

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;
}
15 changes: 15 additions & 0 deletions tests/regression/75-invalid_dealloc/08-realloc-at-struct-offset.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
#include <stdlib.h>

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;
}

0 comments on commit 1da8e97

Please sign in to comment.