diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c4fdd633d3..232ee36d68 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2026,6 +2026,7 @@ 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 + let special ctx (lv:lval option) (f: varinfo) (args: exp list) = let invalidate_ret_lv st = match lv with | Some lv -> @@ -2110,7 +2111,7 @@ 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; }, _ -> memory_copying dst src (* strcpy(dest, src); *) | Strcpy { dest = dst; src; n = None }, _ -> diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 5f9f6f90f9..341017f78e 100644 --- a/src/analyses/libraryDesc.ml +++ b/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 diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index c3ca48da93..b5ac897178 100644 --- a/src/analyses/libraryFunctions.ml +++ b/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]]); diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml index 94c16e9c94..7015e6f143 100644 --- a/src/analyses/memOutOfBounds.ml +++ b/src/analyses/memOutOfBounds.ml @@ -6,6 +6,7 @@ open MessageCategory module AS = AnalysisState module VDQ = ValueDomainQueries +module ID = IntDomain.IntDomTuple (* Note: @@ -27,34 +28,11 @@ struct (* HELPER FUNCTIONS *) let intdom_of_int x = - IntDomain.IntDomTuple.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) + ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x) - let to_index ?typ offs = - let idx_of_int x = - IntDomain.IntDomTuple.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int (x / 8)) - in - let rec offset_to_index_offset ?typ offs = match offs with - | `NoOffset -> idx_of_int 0 - | `Field (field, o) -> - let field_as_offset = Field (field, NoOffset) in - let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in - let bits_offset = idx_of_int bits_offset in - let remaining_offset = offset_to_index_offset ~typ:field.ftype o in - IntDomain.IntDomTuple.add bits_offset remaining_offset - | `Index (x, o) -> - let (item_typ, item_size_in_bits) = - match Option.map unrollType typ with - | Some TArray(item_typ, _, _) -> - let item_size_in_bits = bitsSizeOf item_typ in - (Some item_typ, idx_of_int item_size_in_bits) - | _ -> - (None, IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind ()) - in - let bits_offset = IntDomain.IntDomTuple.mul item_size_in_bits x in - let remaining_offset = offset_to_index_offset ?typ:item_typ o in - IntDomain.IntDomTuple.add bits_offset remaining_offset - in - offset_to_index_offset ?typ offs + let size_of_type_in_bytes typ = + let typ_size_in_bytes = (bitsSizeOf typ) / 8 in + intdom_of_int typ_size_in_bytes let rec exp_contains_a_ptr (exp:exp) = match exp with @@ -112,50 +90,51 @@ struct | 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 + let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in begin match ctx.ask (Queries.EvalLength ptr) with - | `Lifted arr_len -> `Lifted (IntDomain.IntDomTuple.mul item_typ_size_in_bytes arr_len) - | `Bot -> VDQ.ID.bot () - | `Top -> VDQ.ID.top () + | `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) + let type_size_in_bytes = size_of_type_in_bytes v.vtype in + `Lifted type_size_in_bytes end - | _ -> VDQ.ID.top () + | _ -> `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 - | [] -> VDQ.ID.bot () + | [] -> `Bot | [x] -> x - | x::xs -> List.fold_left (fun acc elem -> - if VDQ.ID.compare acc elem >= 0 then elem else acc - ) x xs + | x::xs -> List.fold_left VDQ.ID.join x xs end | _ -> M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; - VDQ.ID.top () + `Top let get_ptr_deref_type ptr_typ = match ptr_typ with | TPtr (t, _) -> Some t | _ -> None - let size_of_type_in_bytes typ = - let typ_size_in_bytes = (bitsSizeOf typ) / 8 in - intdom_of_int typ_size_in_bytes - let eval_ptr_offset_in_binop ctx exp ptr_contents_typ = let eval_offset = ctx.ask (Queries.EvalInt exp) in - let eval_offset = Option.get @@ VDQ.ID.to_int eval_offset in - let eval_offset = VDQ.ID.of_int (Cilfacade.ptrdiff_ikind ()) eval_offset in let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in match eval_offset with - | `Lifted i -> `Lifted (IntDomain.IntDomTuple.mul i ptr_contents_typ_size_in_bytes) + | `Lifted eo -> + let casted_eo = ID.cast_to (Cilfacade.ptrdiff_ikind ()) eo in + begin + try `Lifted (ID.mul casted_eo ptr_contents_typ_size_in_bytes) + with IntDomain.ArithmeticOnIntegerBot _ -> `Bot + end | `Top -> `Top | `Bot -> `Bot @@ -167,12 +146,18 @@ struct let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset in let bytes_offset = intdom_of_int (bits_offset / 8) in let remaining_offset = offs_to_idx field.ftype o in - IntDomain.IntDomTuple.add bytes_offset remaining_offset + begin + try ID.add bytes_offset remaining_offset + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end | `Index (x, o) -> - let typ_size_in_bytes = size_of_type_in_bytes typ in - let bytes_offset = IntDomain.IntDomTuple.mul typ_size_in_bytes x in - let remaining_offset = offs_to_idx typ o in - IntDomain.IntDomTuple.add bytes_offset remaining_offset + begin try + let typ_size_in_bytes = size_of_type_in_bytes typ in + let bytes_offset = ID.mul typ_size_in_bytes x in + let remaining_offset = offs_to_idx typ o in + ID.add bytes_offset remaining_offset + with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind () + end let rec get_addr_offs ctx ptr = match ctx.ask (Queries.MayPointTo ptr) with @@ -183,17 +168,17 @@ struct begin match VDQ.AD.is_empty a with | true -> M.warn "Pointer %a has an empty points-to-set" d_exp ptr; - IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + ID.top_of @@ Cilfacade.ptrdiff_ikind () | false -> if VDQ.AD.exists (function - | Addr (_, o) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t o + | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o | _ -> false ) a then ( (* TODO: Uncomment once staging-memsafety branch changes are applied *) (* set_mem_safety_flag InvalidDeref; *) M.warn "Pointer %a has a bot address offset. An invalid memory access may occur" d_exp ptr ) else if VDQ.AD.exists (function - | Addr (_, o) -> IntDomain.IntDomTuple.is_bot @@ offs_to_idx t o + | Addr (_, o) -> ID.is_bot @@ offs_to_idx t o | _ -> false ) a then ( (* TODO: Uncomment once staging-memsafety branch changes are applied *) @@ -204,16 +189,16 @@ struct (* Hence, we can just pick one element and obtain its offset *) begin match VDQ.AD.choose a with | Addr (_, o) -> offs_to_idx t o - | _ -> IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + | _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind () end end | None -> M.error "Expression %a doesn't have pointer type" d_exp ptr; - IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + ID.top_of @@ Cilfacade.ptrdiff_ikind () end | _ -> M.warn "Pointer %a has a points-to-set of top. An invalid memory access might occur" d_exp ptr; - IntDomain.IntDomTuple.top_of @@ Cilfacade.ptrdiff_ikind () + ID.top_of @@ Cilfacade.ptrdiff_ikind () and check_lval_for_oob_access ctx ?(is_implicitly_derefed = false) lval = if not @@ lval_contains_a_ptr lval then () @@ -242,15 +227,25 @@ struct let ptr_contents_type = get_ptr_deref_type ptr_type in match ptr_contents_type with | Some t -> - begin match VDQ.ID.is_top ptr_size with - | true -> + begin match ptr_size, addr_offs with + | `Top, _ -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is top. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + | `Bot, _ -> AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a not known. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp - | false -> - let offs = `Lifted addr_offs in - if ptr_size < offs then begin - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" VDQ.ID.pretty ptr_size VDQ.ID.pretty offs + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp + | `Lifted ps, ao -> + let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in + let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ao in + let ptr_size_lt_offs = ID.lt casted_ps casted_ao in + begin match ID.to_bool ptr_size_lt_offs with + | Some true -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer is %a (in bytes). It is offset by %a (in bytes) due to pointer arithmetic. Memory out-of-bounds access must occur" ID.pretty casted_ps ID.pretty casted_ao + | Some false -> () + | None -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of pointer (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_ps ID.pretty casted_ao end end | _ -> M.error "Expression %a is not a pointer" d_exp lval_exp @@ -296,27 +291,81 @@ struct let offset_size = eval_ptr_offset_in_binop ctx e2 t in (* Make sure to add the address offset to the binop offset *) let offset_size_with_addr_size = match offset_size with - | `Lifted os -> `Lifted (IntDomain.IntDomTuple.add os addr_offs) + | `Lifted os -> + let casted_os = ID.cast_to (Cilfacade.ptrdiff_ikind ()) os in + let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in + begin + try `Lifted (ID.add casted_os casted_ao) + with IntDomain.ArithmeticOnIntegerBot _ -> `Bot + end | `Top -> `Top | `Bot -> `Bot in - begin match VDQ.ID.is_top ptr_size, VDQ.ID.is_top offset_size_with_addr_size with - | true, _ -> + begin match ptr_size, offset_size_with_addr_size with + | `Top, _ -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is top. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + | _, `Top -> AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a not known. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp - | _, true -> + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is top. Memory out-of-bounds access might occur" d_exp binopexp + | `Bot, _ -> AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a not known. Memory out-of-bounds access might occur" d_exp binopexp - | false, false -> - if ptr_size < offset_size_with_addr_size then begin - AS.svcomp_may_invalid_deref := true; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp VDQ.ID.pretty ptr_size VDQ.ID.pretty offset_size_with_addr_size + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a in expression %a is bottom. Memory out-of-bounds access might occur" d_exp e1 d_exp binopexp + | _, `Bot -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp + | `Lifted ps, `Lifted o -> + let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in + let casted_o = ID.cast_to (Cilfacade.ptrdiff_ikind ()) o in + let ptr_size_lt_offs = ID.lt casted_ps casted_o in + begin match ID.to_bool ptr_size_lt_offs with + | Some true -> + AS.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer in expression %a is %a (in bytes). It is offset by %a (in bytes). Memory out-of-bounds access must occur" d_exp binopexp ID.pretty casted_ps ID.pretty casted_o + | Some false -> () + | None -> + AnalysisState.svcomp_may_invalid_deref := true; + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare pointer size (%a) with offset (%a). Memory out-of-bounds access may occur" ID.pretty casted_ps ID.pretty casted_o end end | _ -> M.error "Binary expression %a doesn't have a pointer" d_exp binopexp end | _ -> () + (* For memset() and memcpy() *) + 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_ptr_target ctx dest in + let eval_n = ctx.ask (Queries.EvalInt n) in + let addr_offs = get_addr_offs ctx dest 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 casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in + let dest_size_lt_count = ID.lt casted_ds (ID.add casted_en casted_ao) 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) with an address offset of %a (in bytes). Count is %a (in bytes). Memory out-of-bounds access must occur" fun_name ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en + | 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 address offset (%a) count (%a) in function %s. Memory out-of-bounds access may occur" ID.pretty casted_ds ID.pretty casted_ao ID.pretty casted_en fun_name + end + (* TRANSFER FUNCTIONS *) @@ -344,6 +393,11 @@ struct in Option.iter (fun x -> check_lval_for_oob_access ctx x) lval; List.iter (fun arg -> check_exp_for_oob_access ctx ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) arg) arglist; + (* Check calls to memset and memcpy for out-of-bounds-accesses *) + match desc.special arglist with + | Memset { dest; ch; count; } -> check_count ctx f.vname dest count; + | Memcpy { dest; src; n = count; } -> check_count ctx f.vname dest count; + | _ -> (); ctx.local let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = diff --git a/tests/regression/77-mem-oob/06-memset-oob.c b/tests/regression/77-mem-oob/06-memset-oob.c new file mode 100644 index 0000000000..931f7eaa8c --- /dev/null +++ b/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 +#include +#include + +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; +} diff --git a/tests/regression/77-mem-oob/07-memcpy-oob.c b/tests/regression/77-mem-oob/07-memcpy-oob.c new file mode 100644 index 0000000000..012f92996e --- /dev/null +++ b/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 +#include + +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; +} diff --git a/tests/regression/77-mem-oob/08-memset-memcpy-array.c b/tests/regression/77-mem-oob/08-memset-memcpy-array.c new file mode 100644 index 0000000000..f231ba2dc4 --- /dev/null +++ b/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 +#include + +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; +} diff --git a/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c b/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c new file mode 100644 index 0000000000..725024946e --- /dev/null +++ b/tests/regression/77-mem-oob/09-memset-memcpy-addr-offs.c @@ -0,0 +1,20 @@ +// 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 +#include + +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 + + memset(a, 0, 40); //NOWARN + memcpy(a, b, 40); //NOWARN + + a += 3; + + memset(a, 0, 40); //WARN + memcpy(a, b, 40); //WARN + + memset(a, 0, 37); //NOWARN + memcpy(a, b, 37); //NOWARN +} \ No newline at end of file