Merge pull request goblint#1099 from mrstanb/handle-free-of-stack-mem

Warn for {d,r}eallocation of non-dynamically allocated memory

src/analyses/base.ml

@@ -2002,6 +2002,16 @@ struct
     let st' = invalidate ~deep:false ~ctx (Analyses.ask_of_ctx ctx) gs st shallow_addrs in
     invalidate ~deep:true ~ctx (Analyses.ask_of_ctx ctx) gs st' deep_addrs
 
+  let check_free_of_non_heap_mem ctx special_fn ptr =
+    match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local ptr with
+    | Address a ->
+      let points_to_set = addrToLvalSet a in
+      if Q.LS.is_top points_to_set then
+        M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Points-to set for pointer %a in function %s is top. Potential free of non-dynamically allocated memory may occur" d_exp ptr special_fn.vname
+      else if (Q.LS.exists (fun (v, _) -> not (ctx.ask (Q.IsHeapVar v))) points_to_set) || (AD.mem Addr.UnknownPtr a) then
+        M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 590] "Free of non-dynamically allocated memory in function %s for pointer %a" special_fn.vname d_exp ptr
+    | _ -> M.warn ~category:MessageCategory.Analyzer "Pointer %a in function %s doesn't evaluate to a valid address." d_exp ptr special_fn.vname
+
   let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
     let invalidate_ret_lv st = match lv with
       | Some lv ->
@@ -2282,6 +2292,8 @@ struct
         | _ -> st
       end
     | Realloc { ptr = p; size }, _ ->
+      (* Realloc shouldn't be passed non-dynamically allocated memory *)
+      check_free_of_non_heap_mem ctx f p;
       begin match lv with
         | Some lv ->
           let ask = Analyses.ask_of_ctx ctx in
@@ -2313,6 +2325,10 @@ struct
         | None ->
           st
       end
+    | Free ptr, _ ->
+      (* Free shouldn't be passed non-dynamically allocated memory *)
+      check_free_of_non_heap_mem ctx f ptr;
+      st
     | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
     | Setjmp { env }, _ ->
       let ask = Analyses.ask_of_ctx ctx in

src/util/messageCategory.ml

@@ -12,6 +12,7 @@ type undefined_behavior =
   | NullPointerDereference
   | UseAfterFree
   | DoubleFree
+  | InvalidMemoryDeallocation
   | Uninitialized
   | DoubleLocking
   | Other
@@ -65,6 +66,7 @@ struct
     let nullpointer_dereference: category = create @@ NullPointerDereference
     let use_after_free: category = create @@ UseAfterFree
     let double_free: category = create @@ DoubleFree
+    let invalid_memory_deallocation: category = create @@ InvalidMemoryDeallocation
     let uninitialized: category = create @@ Uninitialized
     let double_locking: category = create @@ DoubleLocking
     let other: category = create @@ Other
@@ -102,6 +104,7 @@ struct
         | "nullpointer_dereference" -> nullpointer_dereference
         | "use_after_free" -> use_after_free
         | "double_free" -> double_free
+        | "invalid_memory_deallocation" -> invalid_memory_deallocation
         | "uninitialized" -> uninitialized
         | "double_locking" -> double_locking
         | "other" -> other
@@ -113,6 +116,7 @@ struct
       | NullPointerDereference -> ["NullPointerDereference"]
       | UseAfterFree -> ["UseAfterFree"]
       | DoubleFree -> ["DoubleFree"]
+      | InvalidMemoryDeallocation -> ["InvalidMemoryDeallocation"]
       | Uninitialized -> ["Uninitialized"]
       | DoubleLocking -> ["DoubleLocking"]
       | Other -> ["Other"]
@@ -223,6 +227,7 @@ let behaviorName = function
     |NullPointerDereference -> "NullPointerDereference"
     |UseAfterFree -> "UseAfterFree"
     |DoubleFree -> "DoubleFree"
+    |InvalidMemoryDeallocation -> "InvalidMemoryDeallocation"
     |Uninitialized -> "Uninitialized"
     |DoubleLocking -> "DoubleLocking"
     |Other -> "Other"

tests/regression/75-invalid_dealloc/01-invalid-dealloc-simple.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+int main(int argc, char const *argv[])
+{
+    int a;
+    int *p = &a;
+    free(p); //WARN
+
+    char b = 'b';
+    char *p2 = &b;
+    free(p2); //WARN
+
+    return 0;
+}

tests/regression/75-invalid_dealloc/02-invalid-dealloc-struct.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+typedef struct custom_t {
+    int x;
+    int y;
+} custom_t;
+
+int main(int argc, char const *argv[])
+{
+    custom_t *var;
+    free(var); //WARN
+
+    return 0;
+}

tests/regression/75-invalid_dealloc/03-invalid-dealloc-array.c

@@ -0,0 +1,25 @@
+#include <stdlib.h>
+
+typedef struct custom_t {
+    int x;
+    int y;
+} custom_t;
+
+#define MAX_SIZE 5000
+
+int main(int argc, char const *argv[])
+{
+    custom_t custom_arr[MAX_SIZE];
+    free(custom_arr); //WARN
+
+    int int_arr[MAX_SIZE];
+    free(int_arr); //WARN
+
+    char char_arr[MAX_SIZE];
+    free(char_arr); //WARN
+
+    char char_arr2[1];
+    free(char_arr2); //WARN
+
+    return 0;
+}

tests/regression/75-invalid_dealloc/04-invalid-realloc.c

@@ -0,0 +1,25 @@
+#include <stdlib.h>
+
+typedef struct custom_t {
+    int x;
+    int y;
+} custom_t;
+
+#define MAX_SIZE 5000
+
+int main(int argc, char const *argv[])
+{
+    custom_t custom_arr[10];
+    realloc(custom_arr, MAX_SIZE); //WARN
+
+    int int_arr[100];
+    realloc(int_arr, MAX_SIZE); //WARN
+
+    char char_arr[1000];
+    realloc(char_arr, MAX_SIZE); //WARN
+
+    char char_arr2[1];
+    realloc(char_arr2, MAX_SIZE); //WARN
+
+    return 0;
+}