Improve multi-threaded valid-memcleanup

src/analyses/memLeak.ml

@@ -6,7 +6,7 @@ open MessageCategory
 open AnalysisStateUtil
 
 module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
-
+module WasMallocCalled = BoolDomain.MayBool
 module Spec : Analyses.MCPSpec =
 struct
   include Analyses.IdentitySpec
@@ -17,33 +17,63 @@ struct
   module C = D
   module P = IdentityP (D)
 
+  module V = UnitV
+  module G = WasMallocCalled
+
   let context _ d = d
 
+  let must_be_single_threaded ~since_start ctx =
+    ctx.ask (Queries.MustBeSingleThreaded { since_start })
+
+  let was_malloc_called ctx =
+    ctx.global ()
+
   (* 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 malloc_called = was_malloc_called ctx in
+    if not (must_be_single_threaded ctx ~since_start:true) && malloc_called 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 exit *)
+  let warn_for_thread_return_or_exit ctx is_return =
+    if not (ToppedVarInfoSet.is_empty ctx.local) then (
+      set_mem_safety_flag InvalidMemTrack;
+      set_mem_safety_flag InvalidMemcleanup;
+      let current_thread = ctx.ask (Queries.CurrentThreadId) in
+      M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Memory may be leaked at thread %s for thread %a" (if is_return then "return" else "exit") ThreadIdDomain.ThreadLifted.pretty current_thread
     )
 
   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 ctx.local) then
       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 ctx.local
       | _ ->
         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"
 
   (* TRANSFER FUNCTIONS *)
   let return ctx (exp:exp option) (f:fundec) : D.t =
+    (* Check for a valid-memcleanup and memtrack violation in a multi-threaded setting *)
+    (* The check for multi-threadedness is to ensure that valid-memtrack and valid-memclenaup are treated separately for single-threaded programs *)
+    if (ctx.ask (Queries.MayBeThreadReturn) &&  not (must_be_single_threaded ctx ~since_start:true)) then (
+      warn_for_thread_return_or_exit 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;
+    if f.svar.vname = "main" then (
+      check_for_mem_leak ctx;
+      if not (must_be_single_threaded ctx ~since_start:false) && was_malloc_called ctx then begin
+        set_mem_safety_flag InvalidMemTrack;
+        set_mem_safety_flag InvalidMemcleanup;
+        M.warn ~category:(Behavior (Undefined MemoryLeak)) ~tags:[CWE 401] "Possible memory leak: Memory was allocated in a multithreaded program, but not all threads are joined."
+      end
+    );
     ctx.local
 
   let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
@@ -53,46 +83,61 @@ struct
     | Malloc _
     | Calloc _
     | Realloc _ ->
-      (* Warn about multi-threaded programs as soon as we encounter a dynamic memory allocation function *)
-      warn_for_multi_threaded ctx;
+      (ctx.sideg () true;
       begin match ctx.ask (Queries.AllocVar {on_stack = false}) with
-        | `Lifted var -> D.add var state
+        | `Lifted var ->
+          ToppedVarInfoSet.add var state
         | _ -> state
-      end
+      end)
     | Free ptr ->
       begin match ctx.ask (Queries.MayPointTo ptr) with
-        | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 ->
+        | 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 *)
-            | _ -> state
+            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) ->
+              ToppedVarInfoSet.remove v ctx.local
+            | _ -> ctx.local
           end
-        | _ -> state
+        | _ -> ctx.local
       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 in the multi-threaded case, we give up and conservatively warn *)
+      warn_for_multi_threaded_due_to_abort ctx;
       state
     | Assert { exp; _ } ->
       let warn_for_assert_exp =
         match ctx.ask (Queries.EvalInt exp) with
         | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp
         | a ->
           begin match Queries.ID.to_bool a with
-            | Some b ->
+            | Some b -> (
               (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *)
-              if b = false then
-                check_for_mem_leak ctx
-              else ()
-            | None -> check_for_mem_leak ctx ~assert_exp_imprecise:true ~exp:(Some exp)
+                if b = false then (
+                  warn_for_multi_threaded_due_to_abort ctx;
+                  check_for_mem_leak ctx
+                )
+                else ())
+            | None ->
+              (warn_for_multi_threaded_due_to_abort ctx;
+               check_for_mem_leak ctx ~assert_exp_imprecise:true ~exp:(Some exp))
           end
       in
       warn_for_assert_exp;
       state
+    | ThreadExit _ ->
+      begin match ctx.ask (Queries.CurrentThreadId) with
+        | `Lifted tid ->
+          warn_for_thread_return_or_exit ctx false
+        | _ -> ()
+      end;
+      state
     | _ -> state
 
   let startstate v = D.bot ()
   let exitstate v = D.top ()
+
+  let threadenter ctx ~multiple lval f args = [D.bot ()]
 end
 
 let _ =

src/analyses/threadAnalysis.ml

@@ -22,7 +22,7 @@ struct
   module P = IdentityP (D)
 
   (* transfer functions *)
-  let return ctx (exp:exp option) (f:fundec) : D.t =
+  let return ctx (exp:exp option) _ : D.t =
     let tid = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
     begin match tid with
       | `Lifted tid -> ctx.sideg tid (false, TS.bot (), not (D.is_empty ctx.local))
@@ -64,6 +64,8 @@ struct
        | [t] -> join_thread ctx.local t (* single thread *)
        | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *)
        | exception SetDomain.Unsupported _ -> ctx.local)
+    | ThreadExit { ret_val } ->
+      return ctx (Some ret_val) ()
     | _ -> ctx.local
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =

src/common/util/options.schema.json

@@ -2164,6 +2164,25 @@
           "description": "Output messages in deterministic order. Useful for cram testing.",
           "type": "boolean",
           "default": false
+        },
+        "memleak": {
+          "title": "warn.memleak",
+          "type":"object",
+          "properties": {
+            "memcleanup": {
+              "title": "warn.memleak.memcleanup",
+              "description": "Enable memory leak warnings only for violations of the SV-COMP \"valid-memcleanup\" category",
+              "type": "boolean",
+              "default": false
+            },
+            "memtrack": {
+              "title": "warn.memleak.memtrack",
+              "description": "Enable memory leak warnings only for violations of the SV-COMP \"valid-memtrack\" category",
+              "type": "boolean",
+              "default": false
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false

tests/regression/76-memleak/08-invalid-memcleanup-multi-threaded.c

@@ -0,0 +1,37 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --set ana.activated[+] thread
+#include <stdlib.h>
+#include <pthread.h>
+
+int *g;
+int *m1;
+
+void *f1(void *arg) {
+    m1 = malloc(sizeof(int));
+    free(m1);
+    // Thread t1 leaks m1 here
+    pthread_exit(NULL); //WARN
+}
+
+void *f2(void *arg) {
+    int *m2;
+    m2 = malloc(sizeof(int));
+    free(m2); // No leak for thread t2, since it calls free before exiting
+    pthread_exit(NULL); //NOWARN
+}
+
+int main(int argc, char const *argv[]) {
+    g = malloc(sizeof(int));
+    pthread_t t1;
+    pthread_create(&t1, NULL, f1, NULL);
+
+    pthread_t t2;
+    pthread_create(&t2, NULL, f2, NULL);
+
+    free(g);
+
+    pthread_join(t1, NULL);
+    pthread_join(t2, NULL);
+
+    // main thread is not leaking anything
+    return 0; //NOWARN
+}

tests/regression/76-memleak/09-invalid-memcleanup-multi-threaded-abort.c

@@ -0,0 +1,35 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak  --set ana.activated[+] thread 
+#include <pthread.h>
+
+int *g;
+int *m1;
+
+void *f1(void *arg) {
+    m1 = malloc(sizeof(int));
+    // Thread t1 leaks m1 here
+    exit(2); //WARN
+}
+
+void *f2(void *arg) {
+    int *m2;
+    m2 = malloc(sizeof(int));
+    free(m2); // No leak for thread t2, since it calls free before exiting
+    pthread_exit(NULL); //NOWARN
+}
+
+int main(int argc, char const *argv[]) {
+    g = malloc(sizeof(int));
+    pthread_t t1;
+    pthread_create(&t1, NULL, f1, NULL);
+
+    pthread_t t2;
+    pthread_create(&t2, NULL, f2, NULL);
+
+    free(g);
+
+    pthread_join(t1, NULL);
+    pthread_join(t2, NULL);
+
+    // main thread is not leaking anything
+    return 0; //NOWARN
+}

tests/regression/76-memleak/10-leak-later.c

@@ -0,0 +1,25 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+#include <pthread.h>
+
+int *g;
+int *m1;
+int *m2;
+
+void *f1(void *arg) {
+    int top;
+
+    // Thread t1 leaks m0 here
+    exit(2); //WARN
+}
+
+int main(int argc, char const *argv[]) {
+    pthread_t t1;
+    pthread_create(&t1, NULL, f1, NULL);
+
+    int* m0 = malloc(sizeof(int));
+    free(m0);
+
+    // main thread is not leaking anything
+    return 0;
+}

tests/regression/76-memleak/11-leak-later-nested.c

@@ -0,0 +1,34 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak
+#include <stdlib.h>
+#include <pthread.h>
+
+int *g;
+int *m1;
+int *m2;
+
+void *f2(void *arg) {
+    // Thread t2 leaks m0 and t1_ptr here
+    quick_exit(2); //WARN
+}
+
+void *f1(void *arg) {
+    pthread_t t2;
+    pthread_create(&t2, NULL, f2, NULL);
+
+    int *t1_ptr = malloc(sizeof(int));
+
+    pthread_join(t2, NULL);
+    // t1_ptr is leaked, since t2 calls quick_exit() potentially before this program point
+    free(t1_ptr);
+}
+
+int main(int argc, char const *argv[]) {
+    pthread_t t1;
+    pthread_create(&t1, NULL, f1, NULL);
+
+    int* m0 = malloc(sizeof(int));
+    free(m0);
+
+    // main thread is not leaking anything
+    return 0;
+}

tests/regression/76-memleak/12-multi-threaded-assert.c

@@ -0,0 +1,34 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --disable warn.assert
+#include <stdlib.h>
+#include <pthread.h>
+#include <assert.h>
+
+int *g;
+int *m1;
+int *m2;
+
+void *f2(void *arg) {
+    // Thread t2 leaks m0 and t1_ptr here
+    assert(0); //WARN
+}
+
+void *f1(void *arg) {
+    pthread_t t2;
+    pthread_create(&t2, NULL, f2, NULL);
+
+    int *t1_ptr = malloc(sizeof(int));
+    assert(1); //NOWARN
+    pthread_join(t2, NULL);
+    free(t1_ptr);
+}
+
+int main(int argc, char const *argv[]) {
+    pthread_t t1;
+    pthread_create(&t1, NULL, f1, NULL);
+
+    int* m0 = malloc(sizeof(int));
+    free(m0);
+
+    // main thread is not leaking anything
+    return 0;
+}

tests/regression/76-memleak/13-assert-unknown-multi-threaded.c

@@ -0,0 +1,20 @@
+//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --disable warn.assert
+#include <stdlib.h>
+#include <pthread.h>
+#include <assert.h>
+
+void *f1(void *arg) {
+    int top;
+    assert(top); //WARN
+}
+
+int main(int argc, char const *argv[]) {
+    pthread_t t1;
+    pthread_create(&t1, NULL, f1, NULL);
+
+    int* m0 = malloc(sizeof(int));
+    free(m0);
+
+    // main thread is not leaking anything
+    return 0;
+}