Use-after-free Analysis: Fix warning generation for lvalues

src/analyses/useAfterFree.ml

@@ -31,7 +31,7 @@ struct
   let get_joined_threads man =
     man.ask Queries.MustJoinedThreads
 
-  let warn_for_multi_threaded_access man ?(is_double_free = false) (heap_var:varinfo) behavior cwe_number =
+  let warn_for_multi_threaded_access man ?(is_free = false) (heap_var:varinfo) behavior cwe_number =
     let freeing_threads = man.global heap_var in
     (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *)
     if man.ask (Queries.MustBeSingleThreaded { since_start = true }) || G.is_empty freeing_threads then ()
@@ -58,76 +58,88 @@ struct
         | `Top -> true
         | `Bot -> false
       in
-      let bug_name = if is_double_free then "Double Free" else "Use After Free" in
+      let bug_name = if is_free then "Double Free" else "Use After Free" in
       match get_current_threadid man with
       | `Lifted current ->
         let possibly_started = G.exists (other_possibly_started current) freeing_threads in
         if possibly_started then begin
-          if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
+          if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
           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 = G.exists (equal_current current) threads in
           if not current_is_unique && any_equal_current freeing_threads then begin
-            if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
+            if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
             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 HeapVars.mem heap_var (snd man.local) then begin
-            if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
+            if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
             M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.Thread.pretty current CilType.Varinfo.pretty heap_var
           end
         end
       | `Top ->
-        if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
+        if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
         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_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) man (lval:lval) =
-    match is_implicitly_derefed, is_double_free, lval with
+  (**
+     [is_free] indicates that the lval is passed to free, i.e., whether we consider a call [free(lval)].
+  *)
+  let rec warn_lval_might_contain_freed ?(is_implicitly_derefed = false) ?(is_free = false) (transfer_fn_name:string) man (lval:lval) =
+    match is_implicitly_derefed, is_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 = man.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 man e; offset_might_contain_freed o
+        | Field (f, o) ->
+          offset_might_contain_freed o
+        | Index (e, o) ->
+          warn_exp_might_contain_freed transfer_fn_name man 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
-      begin match man.ask (Queries.MayPointTo lval_to_query) with
-        | ad when not (Queries.AD.is_top ad) ->
-          let warn_for_heap_var v =
-            if HeapVars.mem v (snd state) then begin
-              if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
-              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
-            end
-          in
-          let pointed_to_heap_vars =
-            Queries.AD.fold (fun addr vars ->
-                match addr with
-                | Queries.AD.Addr.Addr (v,_) when man.ask (Queries.IsAllocVar v) -> v :: vars
-                | _ -> vars
-              ) ad []
-          in
+      let (lval_host, o) = lval in
+      offset_might_contain_freed o; (* Check the lval's offset *)
+
+      let freed_heap_vars = snd man.local in
+      let undefined_behavior = if is_free then Undefined DoubleFree else Undefined UseAfterFree in
+      let cwe_number = if is_free then 415 else 416 in
+
+      let check_adress adresses =
+        let warn_for_heap_var v =
+          if HeapVars.mem v freed_heap_vars then begin
+            if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
+            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
+          end
+        in
+        let pointed_to_heap_vars =
+          Queries.AD.fold (fun addr vars ->
+              match addr with
+              | Queries.AD.Addr.Addr (v,_) when man.ask (Queries.IsAllocVar v) -> v :: vars
+              | _ -> vars
+            ) adresses []
+        in
+        if not (Queries.AD.is_top adresses) then begin
           (* 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 man ~is_double_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars
-        | _ -> ()
-      end
+          List.iter (fun heap_var -> warn_for_multi_threaded_access man ~is_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars
+        end
+      in
+      let addresses = man.ask (Queries.MayPointTo (Lval lval)) in
+      check_adress addresses;
+      match lval_host with
+      | Var _ -> ()
+      | Mem exp ->
+        (* We have (\*x).o', so we check recursively whether x has been freed. *)
+        warn_exp_might_contain_freed ~is_implicitly_derefed:true ~is_free:false transfer_fn_name man exp
 
-  and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) man (exp:exp) =
+  (** [is_free] indicates that the exp is passed to free, i.e., we consider a call [free(exp)]*)
+  and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_free = false) (transfer_fn_name:string) man (exp:exp) =
     match exp with
     (* Base recursion cases *)
     | Const _
@@ -141,18 +153,18 @@ struct
     | SizeOfE e
     | AlignOfE e
     | UnOp (_, e, _)
-    | CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e
+    | CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e
     | BinOp (_, e1, e2, _) ->
-      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e1;
-      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e2
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e1;
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e2
     | Question (e1, e2, e3, _) ->
-      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e1;
-      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e2;
-      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man e3
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e1;
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e2;
+      warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e3
     (* Lval cases (need [warn_lval_might_contain_freed] for them) *)
     | Lval lval
     | StartOf lval
-    | AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name man lval
+    | AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man lval
 
   let side_effect_mem_free man freed_heap_vars threadid joined_threads =
     let side_effect_globals_to_heap_var heap_var =
@@ -210,7 +222,7 @@ struct
       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) man 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) man arg) arglist;
+    List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_free:(match desc.special arglist with Free _ -> true | _ -> false) ("special: " ^ f.vname) man arg) arglist;
     match desc.special arglist with
     | Free ptr ->
       begin match man.ask (Queries.MayPointTo ptr) with

tests/regression/75-invalid_free/14-double-free-deref.c

@@ -0,0 +1,21 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+
+struct A19 {
+ 	int *p;
+};
+
+void init_and_free(struct A19 *a) {
+	a->p = (int *)malloc(sizeof(int));
+
+	free(a->p);
+	free(a->p); //WARN
+}
+
+
+int main(void) {
+	struct A19 a19;
+	a19.p = NULL;
+	init_and_free(&a19);
+	return 0;
+}

tests/regression/75-invalid_free/15-use-after-free-indirect.c

@@ -0,0 +1,24 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+
+struct A19 {
+ 	int *p;
+};
+
+
+void init_and_free(struct A19 *a) {
+	(*a).p = (int *)malloc(sizeof(int));
+
+	free(a);
+	// a is freed; use-after-free
+	*((*a).p) = 3; //WARN
+
+	// a already freed; Thus, this not a double free, but a use-after-free.
+	free((*a).p); //WARN
+}
+
+int main(void) {
+	struct A19 *a19p = (struct A19 *)malloc(sizeof(struct A19));
+	init_and_free(a19p);
+	return 0;
+}

tests/regression/75-invalid_free/16-use-after-free-double-indirect.c

@@ -0,0 +1,28 @@
+//PARAM: --set ana.activated[+] useAfterFree
+#include <stdlib.h>
+
+struct A19 {
+ int *p;
+};
+
+void init_and_free(struct A19 **a) {
+    (**a).p = (int *)malloc(sizeof(int));
+
+    free(a);
+    // a already freed; Thus, this not a double free, but a use-after-free.
+    *((**a).p) = 3; //WARN
+
+    // a already freed; Thus, this not a double free, but a use-after-free.
+    free((**a).p); //WARN
+}
+
+
+
+int main(void) {
+    struct A19 **a19pp = (struct A19 **)malloc(sizeof(struct A19*));
+    struct A19 *a19p2 = (struct A19 *)malloc(sizeof(struct A19));
+
+    *a19pp = a19p2;
+    init_and_free(a19pp);
+    return 0;
+}