From 421abcd41fa5084c3f07854b88a26a1382d253e1 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 7 Nov 2023 21:44:51 +0100 Subject: [PATCH 01/15] Warn whenever there's allocated heap memory that's unreachable from globals at program exit --- src/analyses/memLeak.ml | 32 ++++++++++++++++++++++++++++---- 1 file changed, 28 insertions(+), 4 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index dbaa2d69fc..f7f555a70a 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -19,6 +19,22 @@ struct let context _ _ = () (* HELPER FUNCTIONS *) + let get_global_vars () = + (* Filtering by GVar seems to account for declarations, as well as definitions of global vars *) + List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + + let get_reachable_mem_from_globals (global_vars:varinfo list) ctx = + global_vars + |> List.map (fun v -> Lval (Var v, NoOffset)) + |> List.filter_map (fun exp -> + match ctx.ask (Queries.MayPointTo exp) with + | a when not (Queries.AD.is_top a) && Queries.AD.cardinal a = 1 -> + begin match List.hd @@ Queries.AD.elements a with + | Queries.AD.Addr.Addr (v, _) when (ctx.ask (Queries.IsHeapVar v)) && not (ctx.ask (Queries.IsMultiple v)) -> Some v + | _ -> None + end + | _ -> None) + let warn_for_multi_threaded ctx = if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then ( set_mem_safety_flag InvalidMemTrack; @@ -27,17 +43,25 @@ struct ) let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx = - let state = ctx.local in - if not @@ D.is_empty state then + let allocated_mem = ctx.local in + if not (D.is_empty allocated_mem) then + let reachable_mem = D.of_list (get_reachable_mem_from_globals (get_global_vars ()) ctx) in + (* Check and warn if there's unreachable allocated memory at program exit *) + let allocated_and_unreachable_mem = D.diff allocated_mem reachable_mem in + if not (D.is_empty allocated_and_unreachable_mem) then ( + set_mem_safety_flag InvalidMemTrack; + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars %a\n" (Pretty.d_list ", " CilType.Varinfo.pretty) (D.elements allocated_and_unreachable_mem) + ); + (* Check and warn if some of the allocated memory is not deallocated at program exit *) match assert_exp_imprecise, exp with | true, Some exp -> set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty state + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty allocated_mem | _ -> set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; - M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty state + M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty allocated_mem (* TRANSFER FUNCTIONS *) let return ctx (exp:exp option) (f:fundec) : D.t = From 9f7224ed8d6ffeaeda226b62a71d40b1dbd247f5 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 7 Nov 2023 21:45:21 +0100 Subject: [PATCH 02/15] Add test cases for unreachable heap memory from globals --- .../regression/76-memleak/08-unreachable-mem.c | 12 ++++++++++++ .../76-memleak/09-unreachable-with-local-var.c | 17 +++++++++++++++++ 2 files changed, 29 insertions(+) create mode 100644 tests/regression/76-memleak/08-unreachable-mem.c create mode 100644 tests/regression/76-memleak/09-unreachable-with-local-var.c diff --git a/tests/regression/76-memleak/08-unreachable-mem.c b/tests/regression/76-memleak/08-unreachable-mem.c new file mode 100644 index 0000000000..08e7b4e741 --- /dev/null +++ b/tests/regression/76-memleak/08-unreachable-mem.c @@ -0,0 +1,12 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +int *g; + +int main(int argc, char const *argv[]) { + g = malloc(sizeof(int)); + // Reference to g's heap contents is lost here + g = NULL; + + return 0; //WARN +} diff --git a/tests/regression/76-memleak/09-unreachable-with-local-var.c b/tests/regression/76-memleak/09-unreachable-with-local-var.c new file mode 100644 index 0000000000..1614b19132 --- /dev/null +++ b/tests/regression/76-memleak/09-unreachable-with-local-var.c @@ -0,0 +1,17 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +int *g; + +int main(int argc, char const *argv[]) { + g = malloc(sizeof(int)); + // Reference to g's heap contents is lost here + g = NULL; + // We get a false positive for p's memory being unreachable + // It's still leaked, but due to free() being commented out + // TODO: Should we only improve the error reporting for unreachable memory in this case? + int *p = malloc(sizeof(int)); + //free(p); + + return 0; //WARN +} From c056b32954f095f4ee4ab3a2fcab536eec35bdf2 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 8 Nov 2023 20:51:19 +0100 Subject: [PATCH 03/15] Remove //TODO comment from `76/09` --- tests/regression/76-memleak/09-unreachable-with-local-var.c | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/tests/regression/76-memleak/09-unreachable-with-local-var.c b/tests/regression/76-memleak/09-unreachable-with-local-var.c index 1614b19132..bc71bb560e 100644 --- a/tests/regression/76-memleak/09-unreachable-with-local-var.c +++ b/tests/regression/76-memleak/09-unreachable-with-local-var.c @@ -7,11 +7,9 @@ int main(int argc, char const *argv[]) { g = malloc(sizeof(int)); // Reference to g's heap contents is lost here g = NULL; - // We get a false positive for p's memory being unreachable - // It's still leaked, but due to free() being commented out - // TODO: Should we only improve the error reporting for unreachable memory in this case? + + // According to `valid-memtrack`, the memory of p is unreachable and we don't have a false positive int *p = malloc(sizeof(int)); - //free(p); return 0; //WARN } From 175b003aa3fae00a07052e6ae58d3cf6a8173cac Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 8 Nov 2023 21:52:45 +0200 Subject: [PATCH 04/15] Don't set `InvalidMemTrack` flag a second time Co-authored-by: Michael Schwarz --- src/analyses/memLeak.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index f7f555a70a..865ecaffc4 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -55,7 +55,6 @@ struct (* Check and warn if some of the allocated memory is not deallocated at program exit *) match assert_exp_imprecise, exp with | true, Some exp -> - set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty allocated_mem | _ -> From 05e4892feac736b520c81c151ed5b2558187e1a0 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 8 Nov 2023 21:53:56 +0200 Subject: [PATCH 05/15] Don't set `InvalidMemTrack` flag a second time Co-authored-by: Michael Schwarz --- src/analyses/memLeak.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 865ecaffc4..fc015f458b 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -58,7 +58,6 @@ struct set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Assert expression %a is unknown. Memory leak might possibly occur for heap variables: %a" d_exp exp D.pretty allocated_mem | _ -> - set_mem_safety_flag InvalidMemTrack; set_mem_safety_flag InvalidMemcleanup; M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory leak detected for heap variables: %a" D.pretty allocated_mem From f343d74efa850011f6ebebf1ce819f9bc1acefb9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 8 Nov 2023 22:52:27 +0100 Subject: [PATCH 06/15] Add 3 regr. tests for trying out global struct variables --- .../76-memleak/10-global-struct-no-ptr.c | 16 ++++++++++++ .../76-memleak/11-global-struct-ptr.c | 19 ++++++++++++++ .../76-memleak/12-global-nested-struct-ptr.c | 25 +++++++++++++++++++ 3 files changed, 60 insertions(+) create mode 100644 tests/regression/76-memleak/10-global-struct-no-ptr.c create mode 100644 tests/regression/76-memleak/11-global-struct-ptr.c create mode 100644 tests/regression/76-memleak/12-global-nested-struct-ptr.c diff --git a/tests/regression/76-memleak/10-global-struct-no-ptr.c b/tests/regression/76-memleak/10-global-struct-no-ptr.c new file mode 100644 index 0000000000..490b2bb443 --- /dev/null +++ b/tests/regression/76-memleak/10-global-struct-no-ptr.c @@ -0,0 +1,16 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +st st_nonptr; + +int main(int argc, char const *argv[]) { + st_nonptr.a = malloc(sizeof(int)); + st_nonptr.a = NULL; + + return 0; //WARN +} diff --git a/tests/regression/76-memleak/11-global-struct-ptr.c b/tests/regression/76-memleak/11-global-struct-ptr.c new file mode 100644 index 0000000000..4ebe1c16b8 --- /dev/null +++ b/tests/regression/76-memleak/11-global-struct-ptr.c @@ -0,0 +1,19 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +st *st_ptr; + +int main(int argc, char const *argv[]) { + st_ptr = malloc(sizeof(st)); + st_ptr->a = malloc(sizeof(int)); + st_ptr->a = NULL; + free(st_ptr); + + // Only st_ptr->a is causing trouble here + return 0; //WARN +} diff --git a/tests/regression/76-memleak/12-global-nested-struct-ptr.c b/tests/regression/76-memleak/12-global-nested-struct-ptr.c new file mode 100644 index 0000000000..e0f5175064 --- /dev/null +++ b/tests/regression/76-memleak/12-global-nested-struct-ptr.c @@ -0,0 +1,25 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +typedef struct st2 { + st *st_ptr; +} st2; + +st2 *st_var; + +int main(int argc, char const *argv[]) { + st_var = malloc(sizeof(st2)); + st_var->st_ptr = malloc(sizeof(st)); + st_var->st_ptr->a = malloc(sizeof(int)); + st_var->st_ptr->a = NULL; + free(st_var->st_ptr); + free(st_var); + + // Only st_var->st_ptr->a is causing trouble here + return 0; //WARN +} From 6decbddb2503a7633c73b3151df40e158417ede8 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 15 Nov 2023 23:20:11 +0100 Subject: [PATCH 07/15] Improve the detection of reachable memory through global struct vars --- src/analyses/memLeak.ml | 89 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 88 insertions(+), 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index fc015f458b..4d7e864c06 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -23,6 +23,14 @@ struct (* Filtering by GVar seems to account for declarations, as well as definitions of global vars *) List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + let get_global_struct_ptr_vars () = + List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + |> List.filter (fun v -> match v.vtype with TPtr (TComp _, _) | TPtr ((TNamed ({ttype = TComp _; _}, _)), _) -> true | _ -> false) + + let get_global_struct_non_ptr_vars () = + List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + |> List.filter (fun v -> match v.vtype with TComp (_, _) | (TNamed ({ttype = TComp _; _}, _)) -> true | _ -> false) + let get_reachable_mem_from_globals (global_vars:varinfo list) ctx = global_vars |> List.map (fun v -> Lval (Var v, NoOffset)) @@ -35,6 +43,81 @@ struct end | _ -> None) + let rec get_reachable_mem_from_str_ptr_globals (global_struct_ptr_vars:varinfo list) ctx = + let eval_value_of_heap_var heap_var = + match ctx.ask (Queries.EvalValue (Lval (Var heap_var, NoOffset))) with + | a when not (Queries.VD.is_top a) -> + begin match a with + | Struct s -> + List.fold_left (fun acc f -> + if isPointerType f.ftype then + begin match ValueDomain.Structs.get s f with + | Queries.VD.Address a -> + let reachable_from_addr_set = + List.fold_left (fun acc addr -> + match addr with + | Queries.AD.Addr.Addr (v, _) -> List.append acc (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) + | _ -> acc + ) [] (Queries.AD.elements a) + in List.append acc reachable_from_addr_set + | _ -> acc + end + else acc + ) [] (ValueDomain.Structs.keys s) + | _ -> [] + end + | _ -> [] + in + let get_pts_of_non_heap_ptr_var var = + match ctx.ask (Queries.MayPointTo (Lval (Var var, NoOffset))) with + | a when not (Queries.AD.is_top a) && Queries.AD.cardinal a = 1 -> + begin match List.hd @@ Queries.AD.elements a with + | Queries.AD.Addr.Addr (v, _) when (ctx.ask (Queries.IsHeapVar v)) && not (ctx.ask (Queries.IsMultiple v)) -> v :: (eval_value_of_heap_var v) + | Queries.AD.Addr.Addr (v, _) when not (ctx.ask (Queries.IsAllocVar v)) && isPointerType v.vtype -> get_reachable_mem_from_str_ptr_globals [v] ctx + | _ -> [] + end + | _ -> [] + in + global_struct_ptr_vars + |> List.fold_left (fun acc var -> + if ctx.ask (Queries.IsHeapVar var) then eval_value_of_heap_var var + else if not (ctx.ask (Queries.IsAllocVar var)) && isPointerType var.vtype then get_pts_of_non_heap_ptr_var var + else acc + ) [] + + let get_reachable_mem_from_str_non_ptr_globals (global_struct_non_ptr_vars:varinfo list) ctx = + global_struct_non_ptr_vars + (* Filter out global struct vars that don't have pointer fields *) + |> List.filter_map (fun v -> + match ctx.ask (Queries.EvalValue (Lval (Var v, NoOffset))) with + | a when not (Queries.VD.is_top a) -> + begin match a with + | Queries.VD.Struct s -> + let struct_fields = ValueDomain.Structs.keys s in + let ptr_struct_fields = List.filter (fun f -> isPointerType f.ftype) struct_fields in + if List.length ptr_struct_fields = 0 then None else Some (s, ptr_struct_fields) + | _ -> None + end + | _ -> None + ) + |> List.fold_left (fun acc_struct (s, fields) -> + let reachable_from_fields = + List.fold_left (fun acc_field field -> + match ValueDomain.Structs.get s field with + | Queries.VD.Address a -> + let reachable_from_addr_set = + List.fold_left (fun acc_addr addr -> + match addr with + | Queries.AD.Addr.Addr (v, _) -> List.append acc_addr (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) + | _ -> acc_addr + ) [] (Queries.AD.elements a) + in List.append acc_field reachable_from_addr_set + | _ -> acc_field + ) [] fields + in + List.append acc_struct reachable_from_fields + ) [] + let warn_for_multi_threaded ctx = if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then ( set_mem_safety_flag InvalidMemTrack; @@ -45,7 +128,11 @@ struct let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx = let allocated_mem = ctx.local in if not (D.is_empty allocated_mem) then - let reachable_mem = D.of_list (get_reachable_mem_from_globals (get_global_vars ()) ctx) in + let reachable_mem_from_non_struct_globals = D.of_list (get_reachable_mem_from_globals (get_global_vars ()) ctx) in + let reachable_mem_from_struct_ptr_globals = D.of_list (get_reachable_mem_from_str_ptr_globals (get_global_struct_ptr_vars ()) ctx) in + let reachable_mem_from_struct_non_ptr_globals = D.of_list (get_reachable_mem_from_str_non_ptr_globals (get_global_struct_non_ptr_vars ()) ctx) in + let reachable_mem_from_struct_globals = D.join reachable_mem_from_struct_ptr_globals reachable_mem_from_struct_non_ptr_globals in + let reachable_mem = D.join reachable_mem_from_non_struct_globals reachable_mem_from_struct_globals in (* Check and warn if there's unreachable allocated memory at program exit *) let allocated_and_unreachable_mem = D.diff allocated_mem reachable_mem in if not (D.is_empty allocated_and_unreachable_mem) then ( From c3804260bf8bc43ea90e76ea9f2cf0f7ebb7186f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 15 Nov 2023 23:20:53 +0100 Subject: [PATCH 08/15] Add regr. tests for reachable memory through global struct vars --- .../13-global-nested-struct-ptr-reachable.c | 29 +++++++++++++++++++ ...4-global-nested-struct-non-ptr-reachable.c | 25 ++++++++++++++++ 2 files changed, 54 insertions(+) create mode 100644 tests/regression/76-memleak/13-global-nested-struct-ptr-reachable.c create mode 100644 tests/regression/76-memleak/14-global-nested-struct-non-ptr-reachable.c diff --git a/tests/regression/76-memleak/13-global-nested-struct-ptr-reachable.c b/tests/regression/76-memleak/13-global-nested-struct-ptr-reachable.c new file mode 100644 index 0000000000..1726625a59 --- /dev/null +++ b/tests/regression/76-memleak/13-global-nested-struct-ptr-reachable.c @@ -0,0 +1,29 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +typedef struct st2 { + st *st_ptr; +} st2; + +st2 *st_var; + +int main(int argc, char const *argv[]) { + st_var = malloc(sizeof(st2)); + st_var->st_ptr = malloc(sizeof(st)); + int *local_ptr = malloc(sizeof(int)); + st_var->st_ptr->a = local_ptr; + local_ptr = NULL; + + free(st_var->st_ptr); + free(st_var); + + // local_ptr's memory is reachable through st_var->st_ptr->a + // It's leaked, because we don't call free() on it + // Hence, there should be a single warning for a memory leak, but not for unreachable memory + return 0; //WARN +} diff --git a/tests/regression/76-memleak/14-global-nested-struct-non-ptr-reachable.c b/tests/regression/76-memleak/14-global-nested-struct-non-ptr-reachable.c new file mode 100644 index 0000000000..1153bd81e0 --- /dev/null +++ b/tests/regression/76-memleak/14-global-nested-struct-non-ptr-reachable.c @@ -0,0 +1,25 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak +#include + +typedef struct st { + int *a; + int b; +} st; + +typedef struct st2 { + st *st_ptr; +} st2; + +st2 st_var; + +int main(int argc, char const *argv[]) { + st_var.st_ptr = malloc(sizeof(st)); + int *local_ptr = malloc(sizeof(int)); + st_var.st_ptr->a = local_ptr; + local_ptr = NULL; + free(st_var.st_ptr); + + // local_ptr's memory is reachable through st_var.st_ptr->a, but it's not freed + // Hence, there should be only a single warning for a memory leak, but not for unreachable memory + return 0; //WARN +} From 845910410bbda2f9964ccd727d63a6e7b811ac7f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 15 Nov 2023 23:33:58 +0100 Subject: [PATCH 09/15] Fix semgrep warning for using `List.length` for an emptiness check --- src/analyses/memLeak.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index a5d357d9c8..51a5a2ff75 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -96,7 +96,7 @@ struct | Queries.VD.Struct s -> let struct_fields = ValueDomain.Structs.keys s in let ptr_struct_fields = List.filter (fun f -> isPointerType f.ftype) struct_fields in - if List.length ptr_struct_fields = 0 then None else Some (s, ptr_struct_fields) + if ptr_struct_fields = [] then None else Some (s, ptr_struct_fields) | _ -> None end | _ -> None From 6cc01b5177b6bc31899c290b6ae65660bf4aa805 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 18 Nov 2023 15:22:47 +0100 Subject: [PATCH 10/15] Use `unrollType` and `GVarDecl` for global vars Also use `Queries.AD.fold` where applicable and prepend to accumulators --- src/analyses/memLeak.ml | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 51a5a2ff75..c09db2d44f 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -21,15 +21,20 @@ struct (* HELPER FUNCTIONS *) let get_global_vars () = - (* Filtering by GVar seems to account for declarations, as well as definitions of global vars *) - List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + List.filter_map (function GVar (v, _, _) | GVarDecl (v, _) -> Some v | _ -> None) !Cilfacade.current_file.globals let get_global_struct_ptr_vars () = - List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals - |> List.filter (fun v -> match v.vtype with TPtr (TComp _, _) | TPtr ((TNamed ({ttype = TComp _; _}, _)), _) -> true | _ -> false) + get_global_vars () + |> List.filter (fun v -> + match unrollType v.vtype with + | TPtr (TComp _, _) + | TPtr ((TNamed ({ttype = TComp _; _}, _)), _) -> true + | TComp (_, _) + | (TNamed ({ttype = TComp _; _}, _)) -> false + | _ -> false) let get_global_struct_non_ptr_vars () = - List.filter_map (function GVar (v, _, _) -> Some v | _ -> None) !Cilfacade.current_file.globals + get_global_vars () |> List.filter (fun v -> match v.vtype with TComp (_, _) | (TNamed ({ttype = TComp _; _}, _)) -> true | _ -> false) let get_reachable_mem_from_globals (global_vars:varinfo list) ctx = @@ -55,12 +60,13 @@ struct begin match ValueDomain.Structs.get s f with | Queries.VD.Address a -> let reachable_from_addr_set = - List.fold_left (fun acc addr -> + Queries.AD.fold (fun addr acc -> match addr with - | Queries.AD.Addr.Addr (v, _) -> List.append acc (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) + | Queries.AD.Addr.Addr (v, _) -> (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) @ acc | _ -> acc - ) [] (Queries.AD.elements a) - in List.append acc reachable_from_addr_set + ) a [] + in + reachable_from_addr_set @ acc | _ -> acc end else acc @@ -109,14 +115,14 @@ struct let reachable_from_addr_set = List.fold_left (fun acc_addr addr -> match addr with - | Queries.AD.Addr.Addr (v, _) -> List.append acc_addr (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) + | Queries.AD.Addr.Addr (v, _) -> (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) @ acc_addr | _ -> acc_addr ) [] (Queries.AD.elements a) - in List.append acc_field reachable_from_addr_set + in reachable_from_addr_set @ acc_field | _ -> acc_field ) [] fields in - List.append acc_struct reachable_from_fields + reachable_from_fields @ acc_struct ) [] let warn_for_multi_threaded ctx = From 80492ccd1dcad21e49a949a989d1cee42bbb6585 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sat, 18 Nov 2023 15:26:40 +0100 Subject: [PATCH 11/15] Check that addresses in struct fields are singletons and not top --- src/analyses/memLeak.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index c09db2d44f..7e77d62a4e 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -58,7 +58,7 @@ struct List.fold_left (fun acc f -> if isPointerType f.ftype then begin match ValueDomain.Structs.get s f with - | Queries.VD.Address a -> + | Queries.VD.Address a when not (Queries.AD.is_top a) && Queries.AD.cardinal a = 1 -> let reachable_from_addr_set = Queries.AD.fold (fun addr acc -> match addr with From f2ca6d146e1271709259be24d5b20f9e61aab7dd Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 19 Nov 2023 17:33:24 +0100 Subject: [PATCH 12/15] Use `unrollType` for non-pointer global struct vars --- src/analyses/memLeak.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 7e77d62a4e..ab25d49cc6 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -35,7 +35,11 @@ struct let get_global_struct_non_ptr_vars () = get_global_vars () - |> List.filter (fun v -> match v.vtype with TComp (_, _) | (TNamed ({ttype = TComp _; _}, _)) -> true | _ -> false) + |> List.filter (fun v -> + match unrollType v.vtype with + | TComp (_, _) + | (TNamed ({ttype = TComp _; _}, _)) -> true + | _ -> false) let get_reachable_mem_from_globals (global_vars:varinfo list) ctx = global_vars From 0e09d099d5facf7354014319805eb53e186119d2 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Sun, 19 Nov 2023 17:36:22 +0100 Subject: [PATCH 13/15] Don't forget to prepend to `acc` when collecting globally reachable mem --- src/analyses/memLeak.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index ab25d49cc6..3079faae1f 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -91,8 +91,8 @@ struct in global_struct_ptr_vars |> List.fold_left (fun acc var -> - if ctx.ask (Queries.IsHeapVar var) then eval_value_of_heap_var var - else if not (ctx.ask (Queries.IsAllocVar var)) && isPointerType var.vtype then get_pts_of_non_heap_ptr_var var + if ctx.ask (Queries.IsHeapVar var) then (eval_value_of_heap_var var) @ acc + else if not (ctx.ask (Queries.IsAllocVar var)) && isPointerType var.vtype then (get_pts_of_non_heap_ptr_var var) @ acc else acc ) [] From 9153eb3becd5904b99aa8250e50b2cd22f74a128 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 21 Nov 2023 21:04:04 +0100 Subject: [PATCH 14/15] Use `AD.fold` instead of `List.fold_left` --- src/analyses/memLeak.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 3079faae1f..f26157fdd0 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -117,12 +117,14 @@ struct match ValueDomain.Structs.get s field with | Queries.VD.Address a -> let reachable_from_addr_set = - List.fold_left (fun acc_addr addr -> + Queries.AD.fold (fun addr acc_addr -> match addr with - | Queries.AD.Addr.Addr (v, _) -> (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) @ acc_addr + | Queries.AD.Addr.Addr (v, _) -> + let reachable_from_v = Queries.AD.of_list (List.map (fun v -> Queries.AD.Addr.Addr (v, `NoOffset)) (get_reachable_mem_from_str_ptr_globals [v] ctx)) in + Queries.AD.join (Queries.AD.add addr reachable_from_v) acc_addr | _ -> acc_addr - ) [] (Queries.AD.elements a) - in reachable_from_addr_set @ acc_field + ) a (Queries.AD.empty ()) + in (Queries.AD.to_var_may reachable_from_addr_set) @ acc_field | _ -> acc_field ) [] fields in From 666795faca6dd5a20e01c78daefde8efc7fbe1de Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 22 Nov 2023 11:50:31 +0100 Subject: [PATCH 15/15] MemLeak: Do not consider unions --- src/analyses/memLeak.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index f26157fdd0..c7a044f8a6 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -27,8 +27,8 @@ struct get_global_vars () |> List.filter (fun v -> match unrollType v.vtype with - | TPtr (TComp _, _) - | TPtr ((TNamed ({ttype = TComp _; _}, _)), _) -> true + | TPtr (TComp (ci,_), _) + | TPtr ((TNamed ({ttype = TComp (ci, _); _}, _)), _) -> ci.cstruct | TComp (_, _) | (TNamed ({ttype = TComp _; _}, _)) -> false | _ -> false) @@ -37,8 +37,8 @@ struct get_global_vars () |> List.filter (fun v -> match unrollType v.vtype with - | TComp (_, _) - | (TNamed ({ttype = TComp _; _}, _)) -> true + | TComp (ci, _) + | (TNamed ({ttype = TComp (ci,_); _}, _)) -> ci.cstruct | _ -> false) let get_reachable_mem_from_globals (global_vars:varinfo list) ctx =