Add out-of-bounds check for memset and memcpy

src/analyses/base.ml

@@ -2026,6 +2026,100 @@ struct
         M.warn ~category:(Behavior (Undefined InvalidMemoryDeallocation)) ~tags:[CWE 761] "Free of memory not at start of buffer 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
 
+  (* Get the size of the memory that dest points-to *)
+  let get_size_of_dest ctx dest =
+    let intdom_of_int x =
+      ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
+    in
+    let points_to_heap_only =
+      match ctx.ask (Queries.MayPointTo dest) with
+      | a when not (AD.is_top a) ->
+        AD.for_all (function
+            | Addr (v, _) -> ctx.ask (Queries.IsHeapVar v)
+            | _ -> false
+          ) a
+      | _ -> false
+    in
+    if points_to_heap_only then
+      ctx.ask (Queries.BlobSize {exp = dest; base_address = false})
+    else
+      match ctx.ask (Queries.MayPointTo dest) with
+      | a when not (Queries.AD.is_top a) ->
+        let pts_list = Queries.AD.elements a in
+        let pts_elems_to_sizes (addr: Queries.AD.elt) =
+          begin match addr with
+            | Addr (v, _) ->
+              begin match v.vtype with
+                | TArray (item_typ, _, _) ->
+                  let item_typ_size_in_bytes = (bitsSizeOf item_typ) / 8 in
+                  let item_typ_size_in_bytes = intdom_of_int item_typ_size_in_bytes in
+                  begin match ctx.ask (Queries.EvalLength dest) with
+                    | `Lifted arr_len ->
+                      let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in
+                      begin
+                        try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
+                        with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
+                      end
+                    | `Bot -> `Bot
+                    | `Top -> `Top
+                  end
+                | _ ->
+                  let type_size_in_bytes = (bitsSizeOf v.vtype) / 8 in
+                  `Lifted (intdom_of_int type_size_in_bytes)
+              end
+            | _ -> `Top
+          end
+        in
+        (* Map each points-to-set element to its size *)
+        let pts_sizes = List.map pts_elems_to_sizes pts_list in
+        (* Take the smallest of all sizes that ptr's contents may have *)
+        begin match pts_sizes with
+          | [] -> `Bot
+          | [x] -> x
+          | x::xs -> List.fold_left ValueDomainQueries.ID.join x xs
+        end
+      | _ ->
+        M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp dest;
+        `Top
+
+  (* Used for memset() and memcpy() out-of-bounds checks *)
+  let check_count ctx fun_name dest n =
+    let (behavior:MessageCategory.behavior) = Undefined MemoryOutOfBoundsAccess in
+    let cwe_number = 823 in
+    let dest_size = get_size_of_dest ctx dest in
+    let eval_n = ctx.ask (Queries.EvalInt n) in
+    match dest_size, eval_n with
+    | `Top, _ ->
+      AnalysisState.svcomp_may_invalid_deref := true;
+      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is unknown. Memory out-of-bounds access might occur" d_exp dest fun_name
+    | _, `Top ->
+      AnalysisState.svcomp_may_invalid_deref := true;
+      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is unknown. Memory out-of-bounds access might occur" fun_name
+    | `Bot, _ ->
+      AnalysisState.svcomp_may_invalid_deref := true;
+      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest %a in function %s is bottom. Memory out-of-bounds access might occur" d_exp dest fun_name
+    | _, `Bot ->
+      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name
+    | `Lifted ds, `Lifted en ->
+      let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
+      let casted_en = ID.cast_to (Cilfacade.ptrdiff_ikind ()) en in
+      let dest_size_lt_count =
+        begin
+          try ID.lt casted_ds casted_en
+          with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+        end
+      in
+      begin match ID.to_bool dest_size_lt_count with
+        | Some true ->
+          AnalysisState.svcomp_may_invalid_deref := true;
+          M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of dest in function %s is %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access may occur" fun_name ValueDomainQueries.ID.pretty dest_size ValueDomainQueries.ID.pretty eval_n
+        | Some false -> ()
+        | None ->
+          AnalysisState.svcomp_may_invalid_deref := true;
+          M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of dest (%a) with count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty ds ID.pretty en fun_name
+      end
+
+
   let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
     let invalidate_ret_lv st = match lv with
       | Some lv ->
@@ -2093,7 +2187,8 @@ struct
     in
     let st = match desc.special args, f.vname with
     | Memset { dest; ch; count; }, _ ->
-      (* TODO: check count *)
+      (* Check count *)
+      check_count ctx f.vname dest count;
       let eval_ch = eval_rv (Analyses.ask_of_ctx ctx) gs st ch in
       let dest_a, dest_typ = addr_type_of_exp dest in
       let value =
@@ -2110,7 +2205,9 @@ struct
       let dest_a, dest_typ = addr_type_of_exp dest in
       let value = VD.zero_init_value dest_typ in
       set ~ctx (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
-    | Memcpy { dest = dst; src }, _ ->
+    | Memcpy { dest = dst; src; n; }, _ ->
+      (* Check n *)
+      check_count ctx f.vname dst n;
       memory_copying dst src
     (* strcpy(dest, src); *)
     | Strcpy { dest = dst; src; n = None }, _ ->

src/analyses/libraryDesc.ml

@@ -62,7 +62,7 @@ type special =
   | Math of { fun_args: math; }
   | Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; }
   | Bzero of { dest: Cil.exp; count: Cil.exp; }
-  | Memcpy of { dest: Cil.exp; src: Cil.exp }
+  | Memcpy of { dest: Cil.exp; src: Cil.exp; n: Cil.exp; }
   | Strcpy of { dest: Cil.exp; src: Cil.exp; n: Cil.exp option; }
   | Strcat of { dest: Cil.exp; src: Cil.exp; n: Cil.exp option; }
   | Strlen of Cil.exp

src/analyses/libraryFunctions.ml

@@ -12,13 +12,13 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; });
     ("__builtin_memset", special [__ "dest" [w]; __ "ch" []; __ "count" []] @@ fun dest ch count -> Memset { dest; ch; count; });
     ("__builtin___memset_chk", special [__ "dest" [w]; __ "ch" []; __ "count" []; drop "os" []] @@ fun dest ch count -> Memset { dest; ch; count; });
-    ("memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); (* TODO: use n *)
-    ("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src });
-    ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src });
-    ("memccpy", special [__ "dest" [w]; __ "src" [r]; drop "c" []; drop "n" []] @@ fun dest src -> Memcpy {dest; src}); (* C23 *) (* TODO: use n and c *)
-    ("memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src });
-    ("__builtin_memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src });
-    ("__builtin___memmove_chk", special [__ "dest" [w]; __ "src" [r]; drop "count" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src });
+    ("memcpy", special [__ "dest" [w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Memcpy { dest; src; n; });
+    ("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Memcpy { dest; src; n; });
+    ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Memcpy { dest; src; n; });
+    ("memccpy", special [__ "dest" [w]; __ "src" [r]; drop "c" []; __ "n" []] @@ fun dest src n -> Memcpy {dest; src; n; }); (* C23 *) (* TODO: use c *)
+    ("memmove", special [__ "dest" [w]; __ "src" [r]; __ "count" []] @@ fun dest src count -> Memcpy { dest; src; n = count; });
+    ("__builtin_memmove", special [__ "dest" [w]; __ "src" [r]; __ "count" []] @@ fun dest src count -> Memcpy { dest; src; n = count; });
+    ("__builtin___memmove_chk", special [__ "dest" [w]; __ "src" [r]; __ "count" []; drop "os" []] @@ fun dest src count -> Memcpy { dest; src; n = count; });
     ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; });
     ("__builtin_strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; });
     ("__builtin___strcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "os" []] @@ fun dest src -> Strcpy { dest; src; n = None; });
@@ -479,8 +479,8 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("strcasestr", unknown [drop "haystack" [r]; drop "needle" [r]]);
     ("inet_aton", unknown [drop "cp" [r]; drop "inp" [w]]);
     ("fopencookie", unknown [drop "cookie" []; drop "mode" [r]; drop "io_funcs" [s_deep]]); (* doesn't access cookie but passes it to io_funcs *)
-    ("mempcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src });
-    ("__builtin___mempcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src });
+    ("mempcpy", special [__ "dest" [w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Memcpy { dest; src; n; });
+    ("__builtin___mempcpy_chk", special [__ "dest" [w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Memcpy { dest; src; n; });
     ("rawmemchr", unknown [drop "s" [r]; drop "c" []]);
     ("memrchr", unknown [drop "s" [r]; drop "c" []; drop "n" []]);
     ("memmem", unknown [drop "haystack" [r]; drop "haystacklen" []; drop "needle" [r]; drop "needlelen" [r]]);

tests/regression/77-mem-oob/06-memset-oob.c

@@ -0,0 +1,54 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info
+// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed
+#include <stdlib.h>
+#include <string.h>
+#include <stdio.h>
+
+typedef struct s {
+    int a;
+    char b;
+} s;
+
+int main(int argc, char const *argv[]) {
+    int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int
+
+    memset(a, 0, 40); //NOWARN
+    memset(a, 0, 10 * sizeof(int)); //NOWARN
+    memset(a, 0, 41); //WARN
+    memset(a, 0, 40000000); //WARN
+
+    int d;
+
+    if (argc == 15) {
+        int c = 55;
+        a = &c;
+        memset(a, 0, argv[5]); //WARN
+    } else if (argv[2] == 2) {
+        a = &d;
+    }
+
+    memset(a, 0, 40); //WARN
+
+    int input;
+    scanf("%d", &input);
+    memset(a, 0, input); //WARN
+
+
+
+    int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int
+    memset(b, 0, 60); //NOWARN
+    b += 1;
+    memset(b, 0, 60); //WARN
+
+
+
+    s *s_ptr = malloc(sizeof(s));
+    memset(s_ptr, 0, sizeof(s)); //NOWARN
+    memset(s_ptr->a, 0, sizeof(s)); //WARN
+    memset(s_ptr->b, 0, sizeof(s)); //WARN
+
+    s_ptr = s_ptr->a;
+    memset(s_ptr, 0, sizeof(s)); //WARN
+
+    return 0;
+}

tests/regression/77-mem-oob/07-memcpy-oob.c

@@ -0,0 +1,53 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info
+// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed
+#include <stdlib.h>
+#include <string.h>
+
+typedef struct s {
+    int a;
+    char b;
+} s;
+
+int main(int argc, char const *argv[]) {
+    int *a = malloc(10 * sizeof(int)); //Size is 40 bytes, assuming a 4-byte int
+    int *b = malloc(15 * sizeof(int)); //Size is 60 bytes, assuming a 4-byte int
+
+    memcpy(a, b, 40); //NOWARN
+    memcpy(a, b, 10 * sizeof(int)); //NOWARN
+    memcpy(a, b, 41); //WARN
+    memcpy(a, b, 40000000); //WARN
+    memcpy(a, b, 15 * sizeof(int)); //WARN
+
+    int d;
+
+    if (*argv == 42) {
+        a = &d;
+    } else if (*(argv + 5)) {
+        int random = rand();
+        a = &random;
+        memcpy(a, b, 40); //WARN
+    }
+
+    memcpy(a, b, 40); //WARN
+    memcpy(a, b, sizeof(a)); //WARN
+
+    memcpy(b, a, 60); //NOWARN
+    b += 1;
+    memcpy(b, a, 60); //WARN
+
+
+    s *s_ptr = malloc(sizeof(s));
+    memcpy(s_ptr, a, sizeof(s)); //NOWARN
+    memcpy(s_ptr->a, 0, sizeof(s)); //WARN
+    memcpy(s_ptr->b, 0, sizeof(s)); //WARN
+
+    memcpy(s_ptr, a, 40); //WARN
+    memcpy(s_ptr, a, 60); //WARN
+    memcpy(s_ptr, b, 40); //WARN
+    memcpy(s_ptr, b, 60); //WARN
+
+    s_ptr = s_ptr->b;
+    memcpy(s_ptr, a, sizeof(s)); //WARN
+
+    return 0;
+}

tests/regression/77-mem-oob/08-memset-memcpy-array.c

@@ -0,0 +1,43 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --disable warn.info
+// TODO: The "--disable warn.info" part is a temporary fix and needs to be removed once the MacOS CI job is fixed
+#include <stdlib.h>
+#include <string.h>
+
+int main(int argc, char const *argv[]) {
+    int arr[42]; // Size should be 168 bytes (with 4 byte ints)
+    int *b = arr;
+
+
+    memset(b, 0, 168); //NOWARN
+    memset(b, 0, sizeof(arr)); //NOWARN
+    memset(b, 0, 169); //WARN
+    memset(b, 0, sizeof(arr) + 1); //WARN
+
+    int *c = malloc(sizeof(arr)); // Size should be 168 bytes (with 4 byte ints)
+    memcpy(b, c, 168); //NOWARN
+    memcpy(b, c, sizeof(arr)); //NOWARN
+    memcpy(b, c, 169); //WARN
+    memcpy(b, c, sizeof(arr) + 1); //WARN
+
+    int d;
+
+    if (*argv == 42) {
+        b = &d;
+        memset(b, 0, 168); //WARN
+        memcpy(b, c, 168); //WARN
+    } else if (*(argv + 5)) {
+        int random = rand();
+        b = &random;
+        memset(b, 0, 168); //WARN
+        memcpy(b, c, 168); //WARN
+    }
+
+    memset(b, 0, sizeof(arr)); //WARN
+    memcpy(b, c, sizeof(arr)); //WARN
+    memset(b, 0, sizeof(int)); //NOWARN
+    memcpy(b, c, sizeof(int)); //NOWARN
+    memset(b, 0, sizeof(int) + 1); //WARN
+    memcpy(b, c, sizeof(int) + 1); //WARN
+
+    return 0;
+}