Merge branch 'master' of https://github.com/J2000A/analyzer

src/analyses/base.ml

@@ -1411,9 +1411,13 @@ struct
         let new_value = VD.update_offset (Queries.to_value_domain_ask a) old_value offs projected_value lval_raw ((Var x), cil_offset) t in
         if WeakUpdates.mem x st.weak then
           VD.join old_value new_value
-        else if invariant then
+        else if invariant then (
           (* without this, invariant for ambiguous pointer might worsen precision for each individual address to their join *)
-          VD.meet old_value new_value
+          try
+            VD.meet old_value new_value
+          with Lattice.Uncomparable ->
+            new_value
+        )
         else
           new_value
       in
@@ -1998,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 ->
@@ -2278,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
@@ -2309,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
@@ -2348,10 +2368,10 @@ struct
       set ~ctx ~t_override:t ask ctx.global ctx.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *)
     | Rand, _ ->
       begin match lv with
-      | Some x -> 
-        let result:value = (Int (ID.starting IInt Z.zero)) in
-        set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st x) (Cilfacade.typeOfLval x) result
-      | None -> st
+        | Some x ->
+          let result:value = (Int (ID.starting IInt Z.zero)) in
+          set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st x) (Cilfacade.typeOfLval x) result
+        | None -> st
       end
     | _, _ ->
       let st =

src/cdomains/valueDomain.ml

@@ -564,7 +564,7 @@ struct
       warn_type "join" x y;
       Top
 
-  let rec widen x y =
+  let widen x y =
     match (x,y) with
     | (Top, _) -> Top
     | (_, Top) -> Top
@@ -582,7 +582,7 @@ struct
     | (Struct x, Struct y) -> Struct (Structs.widen x y)
     | (Union x, Union y) -> Union (Unions.widen x y)
     | (Array x, Array y) -> Array (CArrays.widen x y)
-    | (Blob x, Blob y) -> Blob (Blobs.widen x y)
+    | (Blob x, Blob y) -> Blob (Blobs.widen x y) (* TODO: why no blob special cases like in join? *)
     | (Thread x, Thread y) -> Thread (Threads.widen x y)
     | (Int x, Thread y)
     | (Thread y, Int x) ->
@@ -963,16 +963,16 @@ struct
               Top
         end
         | JmpBuf _, _ ->
-        (* hack for jmp_buf variables *)
-        begin match value with
-          | JmpBuf t -> value (* if actually assigning jmpbuf, use value *)
-          | Blob(Bot, _, _) -> Bot (* TODO: Stopgap for malloced jmp_bufs, there is something fundamentally flawed somewhere *)
-          | _ ->
-            if !AnalysisState.global_initialization then
-              JmpBuf (JmpBufs.Bufs.empty (), false) (* if assigning global init, use empty set instead *)
-            else
-              Top
-        end
+          (* hack for jmp_buf variables *)
+          begin match value with
+            | JmpBuf t -> value (* if actually assigning jmpbuf, use value *)
+            | Blob(Bot, _, _) -> Bot (* TODO: Stopgap for malloced jmp_bufs, there is something fundamentally flawed somewhere *)
+            | _ ->
+              if !AnalysisState.global_initialization then
+                JmpBuf (JmpBufs.Bufs.empty (), false) (* if assigning global init, use empty set instead *)
+              else
+                Top
+          end
       | _ ->
       let result =
         match offs with

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;
+}