Improve multi-threaded UAF analysis and add SVComp result generation

src/analyses/useAfterFree.ml

@@ -82,38 +82,43 @@ struct
     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
-    | 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 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
+    match 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, (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 = function
+        | 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.LS.elements a
-        |> List.map fst
-        |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var))
+      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
+        | 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 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
+            |> List.map fst
+            |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var))
+          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 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) =
     match exp with

tests/regression/74-use_after_free/04-function-call-uaf.c

@@ -17,7 +17,8 @@ int main() {
     free(ptr1);
     free(ptr2);
 
-    f(ptr1, ptr2, ptr3); //WARN
+    // No deref happening in the function call, hence nothing to warn about
+    f(ptr1, ptr2, ptr3); //NOWARN
 
     free(ptr3); //WARN
 

tests/regression/74-use_after_free/06-uaf-struct.c

@@ -17,13 +17,15 @@ int main(int argc, char **argv) {
     char line[128];
 
     while (1) {
-        printf("[ auth = %p, service = %p ]\n", auth, service); //WARN
+        // No deref happening here => nothing to warn about
+        printf("[ auth = %p, service = %p ]\n", auth, service); //NOWARN
 
         if (fgets(line, sizeof(line), stdin) == NULL) break;
 
         if (strncmp(line, "auth ", 5) == 0) {
-            auth = malloc(sizeof(auth)); //WARN
-            memset(auth, 0, sizeof(auth)); //WARN
+            // No deref happening in either of the 2 lines below => no need to warn
+            auth = malloc(sizeof(auth)); //NOWARN
+            memset(auth, 0, sizeof(auth)); //NOWARN
             if (strlen(line + 5) < 31) {
                 strcpy(auth->name, line + 5); //WARN
             }

tests/regression/74-use_after_free/09-juliet-uaf.c

@@ -21,7 +21,8 @@ static char * helperBad(char * aString)
         reversedString[i] = '\0';
 
         free(reversedString);
-        return reversedString; // WARN (Use After Free (CWE-416))
+        // No need to warn in the line below, as there's no dereferencing happening
+        return reversedString; // NOWARN
     }
     else
     {
@@ -67,8 +68,9 @@ void CWE416_Use_After_Free__return_freed_ptr_08_bad()
     if(staticReturnsTrue())
     {
         {
-            char * reversedString = helperBad("BadSink"); // WARN (Use After Free (CWE-416))
-            printf("%s\n", reversedString); // WARN (Use After Free (CWE-416))
+            // No need to warn in the two lines below, since there's no dereferencing of the freed memory
+            char * reversedString = helperBad("BadSink"); // NOWARN
+            printf("%s\n", reversedString); // NOWARN
         }
     }
 }

tests/regression/74-use_after_free/11-wrapper-funs-uaf.c

@@ -27,12 +27,14 @@ int main(int argc, char const *argv[]) {
     my_free2(p);
 
     *(p + 42) = 'c'; //WARN
-    printf("%s", p); //WARN
-
-    char *p2 = p; //WARN
+    // No dereferencing in the line below => no need to warn
+    printf("%s", p); //NOWARN
 
-    my_free2(p); //WARN
-    my_free2(p2); //WARN
+    // No dereferencing happening in the lines below => no need to warn for an invalid-deref
+    // Also no need to warn for an invalid-free, as the call to free is within these functions and they're not the "free" function itself
+    char *p2 = p; //NOWARN
+    my_free2(p); //NOWARN
+    my_free2(p2); //NOWARN
 
     return 0;
 }