diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index fc57ca8f7..306d2e6b4 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -157,11 +157,9 @@ let inferbo_min e1 e2 = let inferbo_set_size e1 e2 = let exec _model_env mem = - let locs = Sem.eval_locs e1 mem |> Dom.Val.get_pow_loc in + let locs = Sem.eval e1 mem |> Dom.Val.get_pow_loc in let size = Sem.eval e2 mem |> Dom.Val.get_itv in - let arr = Dom.Mem.find_heap_set locs mem in - let arr = Dom.Val.set_array_size size arr in - Dom.Mem.strong_update_heap locs arr mem + Dom.Mem.transform_mem ~f:(Dom.Val.set_array_size size) locs mem and check = check_alloc_size e2 in {exec; check} diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 7725e7d08..1fc1edcb4 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -290,23 +290,28 @@ and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t = Val.lor_sem v1 v2 -let rec eval_locs : Exp.t -> Mem.astate -> Val.t = +(* It returns the array value of the input expression. For example, + when "x" is a program variable, (eval_arr "x") returns array blocks + the "x" is pointing to, on the other hand, (eval "x") returns the + abstract location of "x". *) +let rec eval_arr : Exp.t -> Mem.astate -> Val.t = fun exp mem -> match exp with | Exp.Var id -> ( match Mem.find_alias id mem with | Some AliasTarget.Simple loc -> - PowLoc.singleton loc |> Val.of_pow_loc + Mem.find_heap loc mem | Some AliasTarget.Empty _ | None -> Val.bot ) | Exp.Lvar pvar -> - pvar |> Loc.of_pvar |> PowLoc.singleton |> Val.of_pow_loc + Mem.find_set (PowLoc.singleton (Loc.of_pvar pvar)) mem | Exp.BinOp (bop, e1, e2) -> eval_binop bop e1 e2 mem | Exp.Cast (_, e) -> - eval_locs e mem + eval_arr e mem | Exp.Lfield (e, fn, _) -> - eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn |> Val.of_pow_loc + let locs = eval e mem |> Val.get_all_locs |> PowLoc.append_field ~fn in + Mem.find_heap_set locs mem | Exp.Lindex (e1, e2) -> let arr = eval e1 mem in let idx = eval e2 mem in diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index f50a83387..a0ce73abb 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -159,8 +159,7 @@ module Check = struct let lindex ~array_exp ~index_exp mem pname location cond_set = - let locs = Sem.eval_locs array_exp mem |> Dom.Val.get_all_locs in - let arr = Dom.Mem.find_set locs mem in + let arr = Sem.eval_arr array_exp mem in let idx = Sem.eval index_exp mem in array_access ~arr ~idx ~is_plus:true pname location cond_set end diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 9fbfd3d39..6c39c97eb 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -59,6 +59,8 @@ codetoanalyze/c/bufferoverrun/models.c, fgetc_m1_bad, 3, BUFFER_OVERRUN_L3, ERRO codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith3_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Call,Parameter: p,Parameter: x,ArrayAccess: Offset: [10, 10] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/pointer_arith.c:33:3 by call to `pointer_arith3()` ] +codetoanalyze/c/bufferoverrun/pointer_arith.c, call_pointer_arith4_Bad, 0, BUFFER_OVERRUN_L1, ERROR, [Call,ArrayDeclaration,Parameter: x,ArrayAccess: Offset: [10, 10] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/pointer_arith.c:48:3 by call to `FN_pointer_arith4_Bad()` ] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:135:5 by call to `prune_arrblk_eq()` ] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1]] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c index ca192f8a3..73706d8d2 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/pointer_arith.c @@ -19,3 +19,33 @@ void array_pointer_arith_Bad() { int* p = &arr[5]; p[5] = 1; } + +void pointer_arith2_Ok(int x) { + int len = 5; + char p[5]; + (p + x)[3 - x] = 0; +} + +void call_pointer_arith2_Ok() { pointer_arith2_Ok(100); } + +void pointer_arith3(char* p, int x) { + int len = 5; + (p + x)[10 - x] = 0; +} + +void call_pointer_arith3_Bad() { + char p[5]; + pointer_arith3(p, 100); +} + +/* It is better to raise an alarm here, rather than returning a safety + condition, since the buffer overrun occurs always without regard to + the input x. Using symbols for variables, not only for bounds, + would help in this case. */ +void FN_pointer_arith4_Bad(int x) { + int len = 5; + char p[5]; + (p + x)[10 - x] = 0; +} + +void call_pointer_arith4_Bad() { FN_pointer_arith4_Bad(100); }