Improve multi-threaded UAF analysis and add SVComp result generation

src/analyses/useAfterFree.ml

@@ -1,11 +1,12 @@
 (** An analysis for the detection of use-after-free vulnerabilities ([useAfterFree]). *)
 
+open GobConfig
 open GoblintCil
 open Analyses
 open MessageCategory
 
 module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
-module ThreadIdSet = SetDomain.Make(ThreadIdDomain.ThreadLifted)
+module ThreadIdToJoinedThreadsMap = MapDomain.MapBot(ThreadIdDomain.ThreadLifted)(ConcDomain.MustThreadSet)
 
 module Spec : Analyses.MCPSpec =
 struct
@@ -15,7 +16,7 @@ struct
 
   module D = ToppedVarInfoSet
   module C = Lattice.Unit
-  module G = ThreadIdSet
+  module G = ThreadIdToJoinedThreadsMap
   module V = VarinfoV
 
   (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *)
@@ -27,40 +28,54 @@ struct
   let get_current_threadid ctx =
     ctx.ask Queries.CurrentThreadId
 
+  let get_joined_threads ctx =
+    ctx.ask Queries.MustJoinedThreads
+
   let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number =
     let freeing_threads = ctx.global heap_var in
     (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *)
-    if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || ThreadIdSet.is_empty freeing_threads then ()
+    if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || G.is_empty freeing_threads then ()
     else begin
-      let possibly_started current = function
+      let possibly_started current tid joined_threads =
+        match tid with
         | `Lifted tid ->
-          let threads = ctx.ask Queries.CreatedThreads in
+          let created_threads = ctx.ask Queries.CreatedThreads in
+          (* Discard joined threads, as they're supposed to be joined before the point of freeing the memory *)
+          let threads = ConcDomain.MustThreadSet.diff created_threads joined_threads in
           let not_started = MHP.definitely_not_started (current, threads) tid in
           let possibly_started = not not_started in
           possibly_started
         | `Top -> true
         | `Bot -> false
       in
-      let equal_current current = function
+      let equal_current current tid joined_threads =
+        match tid with
         | `Lifted tid ->
           ThreadId.Thread.equal current tid
         | `Top -> true
         | `Bot -> false
       in
       match get_current_threadid ctx with
       | `Lifted current ->
-        let possibly_started = ThreadIdSet.exists (possibly_started current) freeing_threads in
-        if possibly_started then
+        let possibly_started = G.exists (possibly_started current) freeing_threads in
+        if possibly_started then begin
+          AnalysisState.svcomp_may_use_after_free := true;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. Use-After-Free might occur" CilType.Varinfo.pretty heap_var
+        end
         else begin
           let current_is_unique = ThreadId.Thread.is_unique current in
-          let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in
-          if not current_is_unique && any_equal_current freeing_threads then
+          let any_equal_current threads = G.exists (equal_current current) threads in
+          if not current_is_unique && any_equal_current freeing_threads then begin
+            AnalysisState.svcomp_may_use_after_free := true;
             M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var
-          else if D.mem heap_var ctx.local then
+          end
+          else if D.mem heap_var ctx.local then begin
+            AnalysisState.svcomp_may_use_after_free := true;
             M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Use-After-Free might occur in current unique thread %a for heap variable %a" ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
+          end
         end
       | `Top ->
+        AnalysisState.svcomp_may_use_after_free := true;
         M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. A Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var
       | `Bot ->
         M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom"
@@ -85,8 +100,10 @@ struct
     match ctx.ask (Queries.MayPointTo lval_to_query) with
     | a when not (Queries.LS.is_top a) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) ->
       let warn_for_heap_var var =
-        if D.mem var state then
+        if D.mem var state then begin
+          AnalysisState.svcomp_may_use_after_free := true;
           M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" var.vname transfer_fn_name
+        end
       in
       let pointed_to_heap_vars =
         Queries.LS.elements a
@@ -125,9 +142,18 @@ struct
     | StartOf lval
     | AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name ctx lval
 
-  let side_effect_mem_free ctx freed_heap_vars threadid =
-    let threadid = G.singleton threadid in
-    D.iter (fun var -> ctx.sideg var threadid) freed_heap_vars
+  let side_effect_mem_free ctx freed_heap_vars threadid joined_threads =
+    let side_effect_globals_to_heap_var heap_var =
+      let current_globals = ctx.global heap_var in
+      let joined_threads_to_add = match G.find_opt threadid current_globals with
+        | Some threads -> ConcDomain.ThreadSet.inter joined_threads threads
+        | None -> joined_threads
+      in
+      let globals_to_side_effect = G.add threadid joined_threads_to_add current_globals in
+      ctx.sideg heap_var globals_to_side_effect
+    in
+    D.iter side_effect_globals_to_heap_var freed_heap_vars
+
 
 
   (* TRANSFER FUNCTIONS *)
@@ -187,8 +213,9 @@ struct
             |> D.of_list
           in
           (* Side-effect the tid that's freeing all the heap vars collected here *)
-          side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx);
-          D.join state (pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *)
+          side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx) (get_joined_threads ctx);
+          (* Add all heap vars, which ptr points to, to the state *)
+          D.join state (pointed_to_heap_vars)
         | _ -> state
       end
     | _ -> state

src/autoTune.ml

@@ -219,6 +219,13 @@ let focusOnSpecification () =
   | NoOverflow -> (*We focus on integer analysis*)
     set_bool "ana.int.def_exc" true;
     set_bool "ana.int.interval" true
+  | ValidFree -> (* Enable the useAfterFree analysis *)
+    let uafAna = ["useAfterFree"] in
+    print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\"";
+    enableAnalyses uafAna
+  (* TODO: Finish these two below later *)
+  | ValidDeref
+  | ValidMemtrack -> ()
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound

src/framework/analysisState.ml

@@ -7,6 +7,15 @@ let should_warn = ref false
 (** Whether signed overflow or underflow happened *)
 let svcomp_may_overflow = ref false
 
+(** Whether a Use-After-Free (UAF) happened *)
+let svcomp_may_use_after_free = ref false
+
+(** Whether an invalid pointer dereference happened *)
+let svcomp_may_invalid_deref = ref false
+
+(** Whether an invalid memtrack happened *)
+let svcomp_may_invalid_memtrack = ref false
+
 (** A hack to see if we are currently doing global inits *)
 let global_initialization = ref false
 

src/witness/svcomp.ml

@@ -52,6 +52,9 @@ struct
         | UnreachCall _ -> "unreach-call"
         | NoOverflow -> "no-overflow"
         | NoDataRace -> "no-data-race" (* not yet in SV-COMP/Benchexec *)
+        | ValidFree -> "valid-free"
+        | ValidDeref -> "valid-deref"
+        | ValidMemtrack -> "valid-memtrack"
       in
       "false(" ^ result_spec ^ ")"
     | Unknown -> "unknown"

src/witness/svcompSpec.ml

@@ -6,11 +6,15 @@ type t =
   | UnreachCall of string
   | NoDataRace
   | NoOverflow
+  | ValidFree
+  | ValidDeref
+  | ValidMemtrack
 
 let of_string s =
   let s = String.strip s in
-  let regexp = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
-  if Str.string_match regexp s 0 then
+  let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in
+  let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
+  if Str.string_match regexp_negated s 0 then
     let global_not = Str.matched_group 1 s in
     if global_not = "data-race" then
       NoDataRace
@@ -23,6 +27,16 @@ let of_string s =
         UnreachCall f
       else
         failwith "Svcomp.Specification.of_string: unknown global not expression"
+  else if Str.string_match regexp s 0 then
+    let global = Str.matched_group 1 s in
+    if global = "valid-free" then
+      ValidFree
+    else if global = "valid-deref" then
+      ValidDeref
+    else if global = "valid-memtrack" then
+      ValidMemtrack
+    else
+      failwith "Svcomp.Specification.of_string: unknown global expression"
   else
     failwith "Svcomp.Specification.of_string: unknown expression"
 
@@ -38,9 +52,18 @@ let of_option () =
     of_string s
 
 let to_string spec =
-  let global_not = match spec with
-    | UnreachCall f -> "call(" ^ f ^ "())"
-    | NoDataRace -> "data-race"
-    | NoOverflow -> "overflow"
+  let print_output spec_str is_neg =
+    if is_neg then
+      Printf.sprintf "CHECK( init(main()), LTL(G ! %s) )" spec_str
+    else
+      Printf.sprintf "CHECK( init(main()), LTL(G %s) )" spec_str
+  in
+  let spec_str, is_neg = match spec with
+    | UnreachCall f -> "call(" ^ f ^ "())", true
+    | NoDataRace -> "data-race", true
+    | NoOverflow -> "overflow", true
+    | ValidFree -> "valid-free", false
+    | ValidDeref -> "valid-deref", false
+    | ValidMemtrack -> "valid-memtrack", false
   in
-  "CHECK( init(main()), LTL(G ! " ^ global_not ^ ") )"
+  print_output spec_str is_neg

src/witness/witness.ml

@@ -472,6 +472,96 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
+    | ValidFree ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_use_after_free then
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      )
+    | ValidDeref ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_deref then
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      )
+    | ValidMemtrack ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_memtrack then
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+      )
 
 
   let write entrystates =

tests/regression/74-use_after_free/13-multi-threaded-uaf-with-joined-thread.c

@@ -0,0 +1,33 @@
+//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins
+#include <stdlib.h>
+#include <stdio.h>
+#include <pthread.h>
+
+int* gptr;
+
+// Mutex to ensure we don't get race warnings, but the UAF warnings we actually care about
+pthread_mutex_t mtx = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_use(void* p) {
+    pthread_mutex_lock(&mtx);
+    *gptr = 0; //NOWARN
+    pthread_mutex_unlock(&mtx);
+}
+
+int main() {
+    gptr = malloc(sizeof(int));
+    *gptr = 42;
+
+    pthread_t using_thread;
+    pthread_create(&using_thread, NULL, t_use, NULL);
+
+    // Join using_thread before freeing gptr in the main thread
+    pthread_join(using_thread, NULL);
+
+    pthread_mutex_lock(&mtx);
+    *gptr = 43; //NOWARN
+    free(gptr); //NOWARN
+    pthread_mutex_unlock(&mtx);
+
+    return 0;
+}