Improve multi-threaded UAF analysis and add SVComp result generation

src/analyses/useAfterFree.ml

@@ -5,7 +5,7 @@ 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 +15,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 *)
@@ -24,83 +24,110 @@ struct
 
   (* HELPER FUNCTIONS *)
 
+  let set_global_svcomp_var is_double_free =
+    if is_double_free then
+      AnalysisState.svcomp_may_invalid_free := true
+    else
+      AnalysisState.svcomp_may_invalid_deref := true
+
   let get_current_threadid ctx =
     ctx.ask Queries.CurrentThreadId
 
-  let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number =
+  let get_joined_threads ctx =
+    ctx.ask Queries.MustJoinedThreads
+
+  let warn_for_multi_threaded_access ctx ?(is_double_free = false) (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 not_started = MHP.definitely_not_started (current, threads) tid in
+          let created_threads = ctx.ask Queries.CreatedThreads in
+          let not_started = MHP.definitely_not_started (current, created_threads) tid in
           let possibly_started = not not_started in
-          possibly_started
+          (* If [current] is possibly running together with [tid], but is also joined before the free() in [tid], then no need to WARN *)
+          let current_joined_before_free = ConcDomain.MustThreadSet.mem current joined_threads in
+          possibly_started && not current_joined_before_free
         | `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
+      let bug_name = if is_double_free then "Double Free" else "Use After Free" in
       match get_current_threadid ctx with
       | `Lifted current ->
-        let possibly_started = ThreadIdSet.exists (possibly_started current) freeing_threads in
-        if possibly_started then
-          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
+        let possibly_started = G.exists (possibly_started current) freeing_threads in
+        if possibly_started then begin
+          set_global_svcomp_var is_double_free;
+          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. %s might occur" CilType.Varinfo.pretty heap_var bug_name
+        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
-            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
-            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
+          let any_equal_current threads = G.exists (equal_current current) threads in
+          if not current_is_unique && any_equal_current freeing_threads then begin
+            set_global_svcomp_var is_double_free;
+            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var
+          end
+          else if D.mem heap_var ctx.local then begin
+            set_global_svcomp_var is_double_free;
+            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
+          end
         end
       | `Top ->
-        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
+        set_global_svcomp_var is_double_free;
+        M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var
       | `Bot ->
         M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom"
     end
 
-  let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) =
-    let state = ctx.local in
-    let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in
-    let cwe_number = if is_double_free then 415 else 416 in
-    let rec offset_might_contain_freed offset =
-      match offset with
-      | NoOffset -> ()
-      | Field (f, o) -> offset_might_contain_freed o
-      | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name ctx e; offset_might_contain_freed o
-    in
-    let (lval_host, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *)
-    let lval_to_query =
-      match lval_host with
-      | Var _ -> Lval lval
-      | Mem _ -> mkAddrOf lval (* Take the lval's address if its lhost is of the form *p, where p is a ptr *)
-    in
-    match ctx.ask (Queries.MayPointTo lval_to_query) with
-    | ad when not (Queries.AD.is_top ad) ->
-      let warn_for_heap_var v =
-        if D.mem v state then
-          M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name
+  let rec warn_lval_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) =
+    match is_implicitly_derefed, is_double_free, lval with
+    (* If we're not checking for a double-free and there's no deref happening, then there's no need to check for an invalid deref or an invalid free *)
+    | false, false, (Var _, NoOffset) -> ()
+    | _ ->
+      let state = ctx.local in
+      let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in
+      let cwe_number = if is_double_free then 415 else 416 in
+      let rec offset_might_contain_freed offset =
+        match offset with
+        | NoOffset -> ()
+        | Field (f, o) -> offset_might_contain_freed o
+        | Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name ctx e; offset_might_contain_freed o
       in
-      let pointed_to_heap_vars =
-        Queries.AD.fold (fun addr vars ->
-            match addr with
-            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) -> v :: vars
-            | _ -> vars
-          ) ad []
+      let (lval_host, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *)
+      let lval_to_query =
+        match lval_host with
+        | Var _ -> Lval lval
+        | Mem _ -> mkAddrOf lval (* Take the lval's address if its lhost is of the form *p, where p is a ptr *)
       in
-      List.iter warn_for_heap_var pointed_to_heap_vars; (* Warn for all heap vars that the lval possibly points to *)
-      (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *)
-      List.iter (fun heap_var -> warn_for_multi_threaded_access ctx heap_var undefined_behavior cwe_number) pointed_to_heap_vars
-    | _ -> ()
+      begin match ctx.ask (Queries.MayPointTo lval_to_query) with
+        | ad when not (Queries.AD.is_top ad) ->
+          let warn_for_heap_var v =
+            if D.mem v state then
+              M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name
+          in
+          let pointed_to_heap_vars =
+            Queries.AD.fold (fun addr vars ->
+                match addr with
+                | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) -> v :: vars
+                | _ -> vars
+              ) ad []
+          in
+          (* Warn for all heap vars that the lval possibly points to *)
+          List.iter warn_for_heap_var pointed_to_heap_vars;
+          (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *)
+          List.iter (fun heap_var -> warn_for_multi_threaded_access ctx ~is_double_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars
+        | _ -> ()
+      end
 
-  and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) =
+  and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) =
     match exp with
     (* Base recursion cases *)
     | Const _
@@ -114,22 +141,27 @@ struct
     | SizeOfE e
     | AlignOfE e
     | UnOp (_, e, _)
-    | CastE (_, e) -> warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e
+    | CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e
     | BinOp (_, e1, e2, _) ->
-      warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e1;
-      warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e2
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e1;
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e2
     | Question (e1, e2, e3, _) ->
-      warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e1;
-      warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e2;
-      warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e3
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e1;
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e2;
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e3
     (* Lval cases (need [warn_lval_might_contain_freed] for them) *)
     | Lval lval
     | StartOf lval
-    | AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name ctx lval
+    | AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx lval
+
+  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 globals_to_side_effect = G.add threadid joined_threads current_globals in
+      ctx.sideg heap_var globals_to_side_effect
+    in
+    D.iter side_effect_globals_to_heap_var freed_heap_vars
 
-  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
 
 
   (* TRANSFER FUNCTIONS *)
@@ -175,9 +207,16 @@ struct
 
   let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
     let state = ctx.local in
-    Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) ctx x) lval;
-    List.iter (fun arg -> warn_exp_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) ctx arg) arglist;
     let desc = LibraryFunctions.find f in
+    let is_arg_implicitly_derefed arg =
+      let read_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = false } arglist in
+      let read_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = true } arglist in
+      let write_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in
+      let write_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } arglist in
+      List.mem arg read_shallow_args || List.mem arg read_deep_args || List.mem arg write_shallow_args || List.mem arg write_deep_args
+    in
+    Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) ctx x) lval;
+    List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_double_free:(match desc.special arglist with Free _ -> true | _ -> false) ("special: " ^ f.vname) ctx arg) arglist;
     match desc.special arglist with
     | Free ptr ->
       begin match ctx.ask (Queries.MayPointTo ptr) with
@@ -190,8 +229,9 @@ struct
               ) ad (D.empty ())
           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,9 +7,15 @@ let should_warn = ref false
 (** Whether signed overflow or underflow happened *)
 let svcomp_may_overflow = ref false
 
+(** Whether an invalid free happened *)
+let svcomp_may_invalid_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