diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index b8efbc2f0..e67b078ab 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -161,6 +161,15 @@ module TransferFunctions = struct Dom.Mem.instantiate_relation rel_subst_map ~caller:caller_mem ~callee:callee_exit_mem + let rec is_array_access_exp = function + | Exp.BinOp ((PlusPI | MinusPI), _, _) | Exp.Lindex _ -> + true + | Exp.Cast (_, x) -> + is_array_access_exp x + | _ -> + false + + let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = fun mem {summary; tenv; extras= {get_proc_summary_and_formals; oenv= {integer_type_widths}}} node instr -> @@ -184,7 +193,8 @@ module TransferFunctions = struct (Pvar.pp Pp.text) pvar ; Dom.Mem.add_unknown id ~location mem ) | Load (id, exp, typ, _) -> - BoUtils.Exec.load_locs id typ (Sem.eval_locs exp mem) mem + let represents_multiple_values = is_array_access_exp exp in + BoUtils.Exec.load_locs ~represents_multiple_values id typ (Sem.eval_locs exp mem) mem | Store (exp1, _, Const (Const.Cstr s), location) -> let locs = Sem.eval_locs exp1 mem in let model_env = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 75db28840..fbe308712 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -580,6 +580,8 @@ module MVal = struct (Loc.represents_multiple_values l, Val.on_demand ~default ?typ oenv l) + let get_rep_multi (represents_multiple_values, _) = represents_multiple_values + let get_val (_, v) = v end @@ -637,6 +639,8 @@ module MemPure = struct prev next + let is_rep_multi_loc l m = Option.value_map ~default:false (find_opt l m) ~f:MVal.get_rep_multi + let find_opt l m = Option.map (find_opt l m) ~f:MVal.get_val let add ?(represents_multiple_values = false) l v m = @@ -685,10 +689,9 @@ module AliasTarget = struct let nullity l = Nullity l - let use l = function - | Simple l' | SimplePlusA (l', _) | Empty l' | Fgets l' | Nullity l' -> - Loc.equal l l' + let get_loc = function Simple l | SimplePlusA (l, _) | Empty l | Fgets l | Nullity l -> l + let use l x = Loc.equal l (get_loc x) let loc_map x ~f = match x with @@ -713,9 +716,7 @@ module AliasTarget = struct let widen ~prev ~next ~num_iters:_ = join prev next - let is_unknown = function - | Simple l | SimplePlusA (l, _) | Empty l | Fgets l | Nullity l -> - Loc.is_unknown l + let is_unknown x = Loc.is_unknown (get_loc x) end (* Relations between values of logical variables(registers) and program variables @@ -1292,6 +1293,8 @@ module MemReach = struct let is_stack_loc : Loc.t -> _ t0 -> bool = fun l m -> StackLocs.mem l m.stack_locs + let is_rep_multi_loc : Loc.t -> _ t0 -> bool = fun l m -> MemPure.is_rep_multi_loc l m.mem_pure + let find_opt : Loc.t -> _ t0 -> Val.t option = fun l m -> MemPure.find_opt l m.mem_pure let find_stack : Loc.t -> _ t0 -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot @@ -1375,6 +1378,11 @@ module MemReach = struct {m with mem_pure= MemPure.add ?represents_multiple_values x v m.mem_pure} + let add_heap_set : ?represents_multiple_values:bool -> PowLoc.t -> Val.t -> t -> t = + fun ?represents_multiple_values locs v m -> + PowLoc.fold (fun l acc -> add_heap ?represents_multiple_values l v acc) locs m + + let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t option -> location:Location.t -> t -> t = fun id ~callee_pname ~location m -> @@ -1604,6 +1612,10 @@ module Mem = struct fun k -> f_lift_default ~default:false (MemReach.is_stack_loc k) + let is_rep_multi_loc : Loc.t -> _ t0 -> bool = + fun k -> f_lift_default ~default:false (MemReach.is_rep_multi_loc k) + + let find : Loc.t -> _ t0 -> Val.t = fun k -> f_lift_default ~default:Val.bot (MemReach.find k) let find_stack : Loc.t -> _ t0 -> Val.t = @@ -1666,6 +1678,11 @@ module Mem = struct map ~f:(MemReach.add_heap ?represents_multiple_values k v) + let add_heap_set : ?represents_multiple_values:bool -> PowLoc.t -> Val.t -> t -> t = + fun ?represents_multiple_values ploc v -> + map ~f:(MemReach.add_heap_set ?represents_multiple_values ploc v) + + let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t -> location:Location.t -> t -> t = fun id ~callee_pname ~location -> map ~f:(MemReach.add_unknown_from id ~callee_pname:(Some callee_pname) ~location) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 158480da1..1cb82db52 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -30,7 +30,7 @@ let rec must_alias : Exp.t -> Exp.t -> Mem.t -> bool = | Exp.Var x1, Exp.Var x2 -> ( match (Mem.find_alias x1 m, Mem.find_alias x2 m) with | Some x1', Some x2' -> - AliasTarget.equal x1' x2' + AliasTarget.equal x1' x2' && not (Mem.is_rep_multi_loc (AliasTarget.get_loc x1') m) | _, _ -> false ) | Exp.UnOp (uop1, e1', _), Exp.UnOp (uop2, e2', _) -> diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 15f0fe26d..07803ad89 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -32,9 +32,14 @@ end module Exec = struct open ModelEnv - let load_locs id typ locs mem = + let load_locs ~represents_multiple_values id typ locs mem = let v = Dom.Mem.find_set ~typ locs mem in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in + let mem = + if represents_multiple_values then + Dom.Mem.add_heap_set ~represents_multiple_values locs v mem + else mem + in match PowLoc.is_singleton_or_more locs with | IContainer.Singleton loc -> Dom.Mem.load_simple_alias id loc mem diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index dacfc4d6c..6c4caff76 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -24,7 +24,8 @@ module ModelEnv : sig end module Exec : sig - val load_locs : Ident.t -> Typ.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t + val load_locs : + represents_multiple_values:bool -> Ident.t -> Typ.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t val decl_local : ModelEnv.model_env -> Dom.Mem.t * int -> Loc.t * Typ.t -> Dom.Mem.t * int diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c index 0b4516bf7..2df5460cb 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_content.c @@ -6,7 +6,7 @@ */ #include -int check_sorted_arr_good_FP(int a[], int length) { +int check_sorted_arr_good(int a[], int length) { for (int i = 1; i < length; i++) { if (a[i] < a[i - 1]) { // should not report CONDITION_ALWAYS_FALSE return 0; @@ -15,7 +15,7 @@ int check_sorted_arr_good_FP(int a[], int length) { return 1; } -int check_sorted_arr10_good_FP(int a[10], int length) { +int check_sorted_arr10_good(int a[10], int length) { for (int i = 1; i < length; i++) { if (a[i] < a[i - 1]) { // should not report CONDITION_ALWAYS_FALSE return 0; @@ -24,7 +24,7 @@ int check_sorted_arr10_good_FP(int a[10], int length) { return 1; } -int check_sorted_ptr_good_FP(int* a, int length) { +int check_sorted_ptr_good(int* a, int length) { for (int i = 1; i < length; i++) { if (a[i] < a[i - 1]) { // should not report CONDITION_ALWAYS_FALSE return 0; @@ -33,7 +33,7 @@ int check_sorted_ptr_good_FP(int* a, int length) { return 1; } -int array_min_index_from_one_FP(int* a, int length) { +int array_min_index_from_one(int* a, int length) { int index_min = 1; for (int i = 2; i < length; i++) { if (a[i] < a[index_min]) { // should not report CONDITION_ALWAYS_FALSE @@ -51,7 +51,7 @@ int array_min_index_from_one_FP(int* a, int length) { */ void call_array_min_index_from_one_good() { int a[2]; - a[array_min_index_from_one_FP(a, 2) - 1] = 0; + a[array_min_index_from_one(a, 2) - 1] = 0; } void weak_update_Good_FP() { diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index c4fc872ad..8dd0346cb 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -45,12 +45,8 @@ codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow_Good_FP, 2, COND codetoanalyze/c/bufferoverrun/arith.c, unused_integer_underflow_Good_FP, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (0 - 1):unsigned32] codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/arith.c, use_uint64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] -codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, call_literal_string_parameter1_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,,Parameter `*s`,,Array declaration,Array access: Offset: [0, 112] Size: 112 by call to `literal_string_parameter` ] codetoanalyze/c/bufferoverrun/array_content.c, call_literal_string_parameter2_Bad, 0, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Call,,Parameter `*s`,,Array declaration,Array access: Offset: [0, 112] Size: 112 by call to `literal_string_parameter` ] -codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] -codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/array_content.c, fgets_may_not_change_str_Bad, 9, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: [0, 5] Size: 5] codetoanalyze/c/bufferoverrun/array_content.c, fgets_may_not_change_str_Good_FP, 9, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: [4, 9] Size: 5] codetoanalyze/c/bufferoverrun/array_content.c, fgets_null_check_Bad, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Array declaration,,Array declaration,Array access: Offset: [-1, 97] Size: 100] @@ -130,7 +126,6 @@ codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/global.c, copyfilter_Good_FP, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] -codetoanalyze/c/bufferoverrun/global.c, copyfilter_Good_FP, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/global.c, use_global_const_ten_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_infinite_loop, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] @@ -247,6 +242,7 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, call_forget_locs_latest_prune_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: 10 Size: 5 by call to `forget_locs_latest_prune` ] codetoanalyze/c/bufferoverrun/prune_alias.c, call_latest_prune_join_3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `n`,,Parameter `*a`,Array access: Offset: 3 Size: 2 by call to `latest_prune_join` ] +codetoanalyze/c/bufferoverrun/prune_alias.c, call_not_prune_multiple2_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Assignment,Call,,Parameter `*m`,,Array declaration,Array access: Offset: [0, 10] Size: 5 by call to `not_prune_multiple2` ] codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne_CAT` ] codetoanalyze/c/bufferoverrun/prune_alias.c, forget_locs_latest_prune, 9, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `length`,,Parameter `length`,Array declaration,Array access: Offset: [1, length] Size: length] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index d83d816b6..247263cb3 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -309,7 +309,7 @@ void call_not_prune_multiple2_Good() { not_prune_multiple2(m); } -void call_not_prune_multiple2_Bad_FN() { +void call_not_prune_multiple2_Bad() { int m[2] = {0, 10}; not_prune_multiple2(m); }