diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index c6f9e3e71..f3d86fd47 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -112,6 +112,10 @@ let offsetof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInf let sizeof : astate -> Itv.t = fun a -> fold (fun _ arr -> Itv.join arr.ArrInfo.size) a Itv.bot +let sizeof_byte : astate -> Itv.t = + fun a -> fold (fun _ arr -> Itv.join (Itv.mult arr.ArrInfo.size arr.ArrInfo.stride)) a Itv.bot + + let plus_offset : astate -> Itv.t -> astate = fun arr i -> map (fun a -> ArrInfo.plus_offset a i) arr diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index cedefbe30..5b449d297 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -126,6 +126,15 @@ let malloc size_exp = {exec; check} +let memcpy dest_exp src_exp size_exp = + let exec _ ~ret:_ mem = mem + and check {location} mem cond_set = + BoUtils.Check.lindex_byte ~array_exp:dest_exp ~byte_index_exp:size_exp mem location cond_set + |> BoUtils.Check.lindex_byte ~array_exp:src_exp ~byte_index_exp:size_exp mem location + in + {exec; check} + + let realloc src_exp size_exp = let exec {location; tenv} ~ret:(id, _) mem = let size_exp = Prop.exp_normalize_noabs tenv Sil.sub_empty size_exp in @@ -461,6 +470,7 @@ module Call = struct ; -"__get_array_length" <>$ capt_exp $!--> get_array_length ; -"__set_array_length" <>$ capt_arg $+ capt_exp $!--> set_array_length ; -"strlen" <>--> by_value Dom.Val.Itv.nat + ; -"memcpy" <>$ capt_exp $+ capt_exp $+ capt_exp $+...$--> memcpy ; -"boost" &:: "split" $ capt_arg_of_typ (-"std" &:: "vector") $+ any_arg $+ any_arg $+? any_arg $--> Boost.Split.std_vector diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 5807a70fa..c4189bd8f 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -306,4 +306,24 @@ module Check = struct let idx_sym_exp = Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f mem) index_exp in let relation = Dom.Mem.get_relation mem in array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true location cond_set + + + let array_access_byte ~arr ~idx ~relation ~is_plus location cond_set = + let arr_blk = Dom.Val.get_array_blk arr in + let size = ArrayBlk.sizeof_byte arr_blk in + let offset = ArrayBlk.offsetof arr_blk in + let idx_itv = Dom.Val.get_itv idx in + let idx_traces = Dom.Val.get_traces idx in + let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in + L.(debug BufferOverrun Verbose) + "@[Add condition :@,array: %a@, idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ; + check_access ~size ~idx:idx_in_blk ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr + ~idx_traces location cond_set ~is_collection_add:true + + + let lindex_byte ~array_exp ~byte_index_exp mem location cond_set = + let idx = Sem.eval byte_index_exp mem in + let arr = Sem.eval_arr array_exp mem in + let relation = Dom.Mem.get_relation mem in + array_access_byte ~arr ~idx ~relation ~is_plus:true location cond_set end diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 51c978054..4e199e06a 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -139,6 +139,14 @@ module Check : sig -> PO.ConditionSet.t -> PO.ConditionSet.t + val lindex_byte : + array_exp:Exp.t + -> byte_index_exp:Exp.t + -> Dom.Mem.astate + -> Location.t + -> PO.ConditionSet.t + -> PO.ConditionSet.t + val collection_access : array_exp:Exp.t -> index_exp:Exp.t diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 637766bba..18472633f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -66,6 +66,10 @@ codetoanalyze/c/bufferoverrun/models.c, exit_bo_good_unreachable_bad, 2, UNREACH codetoanalyze/c/bufferoverrun/models.c, fgetc_255_bad, 4, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 255] Size: 255] codetoanalyze/c/bufferoverrun/models.c, fgetc_256_bad, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 256] Size: 256] codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, 255] Size: 10000] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad1, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad2, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 44 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad3, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: -1 Size: 40] +codetoanalyze/c/bufferoverrun/models.c, memcpy_bad4, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 8 Size: 4] codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: 10] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: 10] codetoanalyze/c/bufferoverrun/pointer_arith.c, FP_pointer_arith5_Ok, 5, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [3, 2043] Size: 1024] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/models.c b/infer/tests/codetoanalyze/c/bufferoverrun/models.c index d7a59774c..8e84748c9 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/models.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/models.c @@ -47,3 +47,52 @@ void fgetc_257_good(FILE* f) { int c = fgetc(f); arr[c + 1] = 42; } + +void memcpy_bad1() { + int arr1[10]; + int arr2[20]; + memcpy(arr1, arr2, 44); +} + +void memcpy_bad2() { + int arr1[10]; + int arr2[20]; + memcpy(arr2, arr1, 44); +} + +void memcpy_bad3() { + int arr1[10]; + int arr2[20]; + memcpy(arr1, arr2, -1); +} + +void memcpy_bad4() { + int src[1]; + int buff[1]; + int* dst = &buff[0]; + memcpy(dst, src, sizeof(dst)); +} + +void memcpy_good1() { + int arr1[10]; + int arr2[20]; + memcpy(arr2, arr1, 40); +} + +void memcpy_good2() { + int arr1[10]; + int arr2[20]; + memcpy(arr2, arr1, 0); +} + +void memcpy_good3() { + int arr1[10]; + int arr2[20]; + memcpy(arr2, arr1, 20); +} + +void memcpy_good4() { + int src[3]; + int dst[3]; + memcpy(dst, src, sizeof(dst)); +}