First attempt to improve precision for multi-threaded valid-memcleanup

src/analyses/memLeak.ml

@@ -6,30 +6,50 @@ open MessageCategory
 open AnalysisStateUtil
 
 module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
-
+module WasMallocCalled = BoolDomain.MustBool
 module Spec : Analyses.MCPSpec =
 struct
   include Analyses.IdentitySpec
 
   let name () = "memLeak"
 
-  module D = ToppedVarInfoSet
+  (* module D = ToppedVarInfoSet *)
+  module D = Lattice.Prod(ToppedVarInfoSet)(WasMallocCalled)
   module C = D
   module P = IdentityP (D)
+  module G = ToppedVarInfoSet
+  module V =
+  struct
+    include ThreadIdDomain.Thread
+    include StdV
+  end
 
   let context _ d = d
 
   (* HELPER FUNCTIONS *)
-  let warn_for_multi_threaded ctx =
-    if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then (
+  let warn_for_multi_threaded_due_to_abort ctx =
+    let state = ctx.local in
+    if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) && snd state then (
       set_mem_safety_flag InvalidMemTrack;
       set_mem_safety_flag InvalidMemcleanup;
-      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program isn't running in single-threaded mode. A memory leak might occur due to multi-threading"
+      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Program aborted while running in multi-threaded mode. A memory leak might occur"
+    )
+
+  (* If [is_return] is set to [true], then a thread return occurred, else a thread join *)
+  let warn_for_thread_return_or_exit current_thread ctx is_return =
+    let global_state = ctx.global current_thread in
+    if not (G.is_empty global_state) then (
+      set_mem_safety_flag InvalidMemcleanup;
+      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s" (if is_return then "return" else "join")
     )
+  (* if not (ToppedVarInfoSet.is_empty (fst state)) && snd state then (
+      set_mem_safety_flag InvalidMemcleanup;
+      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s" (if is_return then "return" else "join")
+      ) *)
 
   let check_for_mem_leak ?(assert_exp_imprecise = false) ?(exp = None) ctx =
     let state = ctx.local in
-    if not @@ D.is_empty state then
+    if not (ToppedVarInfoSet.is_empty (fst state)) then
       match assert_exp_imprecise, exp with
       | true, Some exp ->
         set_mem_safety_flag InvalidMemTrack;
@@ -42,6 +62,12 @@ struct
 
   (* TRANSFER FUNCTIONS *)
   let return ctx (exp:exp option) (f:fundec) : D.t =
+    (* Check for a valid-memcleanup violation in a multi-threaded setting *)
+    if (ctx.ask (Queries.MayBeThreadReturn)) then (
+      match ctx.ask (Queries.CurrentThreadId) with
+      | `Lifted tid -> warn_for_thread_return_or_exit tid ctx true
+      | _ -> ()
+    );
     (* Returning from "main" is one possible program exit => need to check for memory leaks *)
     if f.svar.vname = "main" then check_for_mem_leak ctx;
     ctx.local
@@ -53,25 +79,39 @@ struct
     | Malloc _
     | Calloc _
     | Realloc _ ->
-      (* Warn about multi-threaded programs as soon as we encounter a dynamic memory allocation function *)
-      warn_for_multi_threaded ctx;
       begin match ctx.ask (Queries.AllocVar {on_stack = false}) with
-        | `Lifted var -> D.add var state
-        | _ -> state
+        | `Lifted var ->
+          begin match ctx.ask (Queries.CurrentThreadId) with
+            | `Lifted tid ->
+              let current_globals = ctx.global tid in
+              let globals_to_side_effect = G.add var current_globals in
+              ctx.sideg tid globals_to_side_effect;
+            | _ -> ()
+          end;
+          (ToppedVarInfoSet.add var (fst state), true)
+        | _ -> (fst state, true)
       end
     | Free ptr ->
       begin match ctx.ask (Queries.MayPointTo ptr) with
         | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 ->
           (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
           begin match Queries.AD.choose ad with
-            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *)
+            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) ->
+              begin match ctx.ask (Queries.CurrentThreadId) with
+                | `Lifted tid ->
+                  let current_globals = ctx.global tid in
+                  let globals_to_side_effect = G.remove v current_globals in
+                  ctx.sideg tid globals_to_side_effect
+                | _ -> ()
+              end;
+              (ToppedVarInfoSet.remove v (fst state), snd state) (* Unique pointed to heap vars *)
             | _ -> state
           end
         | _ -> state
       end
     | Abort ->
-      (* An "Abort" special function indicates program exit => need to check for memory leaks *)
-      check_for_mem_leak ctx;
+      (* Upon a call to the "Abort" special function, we give up and conservatively warn *)
+      warn_for_multi_threaded_due_to_abort ctx;
       state
     | Assert { exp; _ } ->
       let warn_for_assert_exp =
@@ -89,6 +129,12 @@ struct
       in
       warn_for_assert_exp;
       state
+    | ThreadExit _ ->
+      begin match ctx.ask (Queries.CurrentThreadId) with
+        | `Lifted tid -> warn_for_thread_return_or_exit tid ctx false
+        | _ -> ()
+      end;
+      state
     | _ -> state
 
   let startstate v = D.bot ()