Merge remote-tracking branch 'mrstanb/improve-valid-memtrack-for-sing…

…le-threaded-programs' into svcomp24-dev

src/analyses/memLeak.ml

@@ -20,6 +20,117 @@ struct
   let context _ d = d
 
   (* HELPER FUNCTIONS *)
+  let get_global_vars () =
+    List.filter_map (function GVar (v, _, _) | GVarDecl (v, _) -> Some v | _ -> None) !Cilfacade.current_file.globals
+
+  let get_global_struct_ptr_vars () =
+    get_global_vars ()
+    |> List.filter (fun v ->
+        match unrollType v.vtype with
+        | TPtr (TComp (ci,_), _)
+        | TPtr ((TNamed ({ttype = TComp (ci, _); _}, _)), _) -> ci.cstruct
+        | TComp (_, _)
+        | (TNamed ({ttype = TComp _; _}, _)) -> false
+        | _ -> false)
+
+  let get_global_struct_non_ptr_vars () =
+    get_global_vars ()
+    |> List.filter (fun v ->
+        match unrollType v.vtype with
+        | TComp (ci, _)
+        | (TNamed ({ttype = TComp (ci,_); _}, _)) -> ci.cstruct
+        | _ -> false)
+
+  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 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 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
+                            | Queries.AD.Addr.Addr (v, _) -> (v :: get_reachable_mem_from_str_ptr_globals [v] ctx) @ acc
+                            | _ -> acc
+                          ) a []
+                      in
+                      reachable_from_addr_set @ acc
+                    | _ -> 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) @ acc
+        else if not (ctx.ask (Queries.IsAllocVar var)) && isPointerType var.vtype then (get_pts_of_non_heap_ptr_var var) @ acc
+        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 ptr_struct_fields = [] 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 =
+                  Queries.AD.fold (fun addr acc_addr ->
+                      match addr with
+                      | 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
+                    ) a (Queries.AD.empty ())
+                in (Queries.AD.to_var_may reachable_from_addr_set) @ acc_field
+              | _ -> acc_field
+            ) [] fields
+        in
+        reachable_from_fields @ acc_struct
+      ) []
+
   let warn_for_multi_threaded ctx =
     if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then (
       set_mem_safety_flag InvalidMemTrack;
@@ -28,17 +139,27 @@ 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_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 (
+        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 =

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 <stdlib.h>
+
+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
+}

tests/regression/76-memleak/09-unreachable-with-local-var.c

@@ -0,0 +1,15 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+
+int *g;
+
+int main(int argc, char const *argv[]) {
+    g = malloc(sizeof(int));
+    // Reference to g's heap contents is lost here
+    g = NULL;
+
+    // According to `valid-memtrack`, the memory of p is unreachable and we don't have a false positive
+    int *p = malloc(sizeof(int));
+
+    return 0; //WARN
+}

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 <stdlib.h>
+
+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
+}

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 <stdlib.h>
+
+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
+}

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 <stdlib.h>
+
+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
+}

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 <stdlib.h>
+
+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
+}

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 <stdlib.h>
+
+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
+}