From 168ce5a6bb687d9008a1efadf80efd9760fc3aa9 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Wed, 22 Nov 2017 05:59:11 -0800 Subject: [PATCH] [inferbo] Add alloc size safety condition Summary: - Plug model checkers - Add alloc size safety condition on alloc of negative, zero or big size Reviewed By: sblackshear Differential Revision: D6375144 fbshipit-source-id: bbea6f3 --- infer/src/base/IssueType.ml | 10 ++ infer/src/base/IssueType.mli | 10 ++ .../src/bufferoverrun/bufferOverrunChecker.ml | 31 ++-- .../src/bufferoverrun/bufferOverrunModels.ml | 9 +- .../bufferOverrunProofObligations.ml | 155 +++++++++++++++--- infer/src/bufferoverrun/itv.ml | 2 + .../c/bufferoverrun/issue_kinds.c | 16 ++ .../codetoanalyze/c/bufferoverrun/issues.exp | 7 + 8 files changed, 202 insertions(+), 38 deletions(-) diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index f8b421156..c11977417 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -227,6 +227,16 @@ let _global_variable_initialized_with_function_or_method_call = from_string ~enabled:false "GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL" +let inferbo_alloc_is_big = from_string "INFERBO_ALLOC_IS_BIG" + +let inferbo_alloc_is_negative = from_string "INFERBO_ALLOC_IS_NEGATIVE" + +let inferbo_alloc_is_zero = from_string "INFERBO_ALLOC_IS_ZERO" + +let inferbo_alloc_may_be_big = from_string ~enabled:false "INFERBO_ALLOC_MAY_BE_BIG" + +let inferbo_alloc_may_be_negative = from_string ~enabled:false "INFERBO_ALLOC_MAY_BE_NEGATIVE" + let inherently_dangerous_function = from_string "INHERENTLY_DANGEROUS_FUNCTION" let interface_not_thread_safe = from_string "INTERFACE_NOT_THREAD_SAFE" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 2a354b33e..3ef5cb025 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -140,6 +140,16 @@ val field_should_be_nullable : t val field_not_null_checked : t +val inferbo_alloc_is_big : t + +val inferbo_alloc_is_negative : t + +val inferbo_alloc_is_zero : t + +val inferbo_alloc_may_be_big : t + +val inferbo_alloc_may_be_negative : t + val inherently_dangerous_function : t val interface_not_thread_safe : t diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index de23189e0..a94c68381 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -316,12 +316,16 @@ module CFG = Analyzer.TransferFunctions.CFG module Sem = BufferOverrunSemantics.Make (CFG) module Report = struct + (* I'd like to avoid rebuilding this :( + Everything depend on CFG only because of `get_allocsite` *) + module Models = BufferOverrunModels.Make (CFG) + type extras = Typ.Procname.t -> Procdesc.t option let add_condition - : Typ.Procname.t -> CFG.node -> Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t + : Typ.Procname.t -> Exp.t -> Location.t -> Dom.Mem.astate -> PO.ConditionSet.t -> PO.ConditionSet.t = - fun pname node exp location mem cond_set -> + fun pname exp location mem cond_set -> let array_access = match exp with | Exp.Var _ -> @@ -353,7 +357,6 @@ module Report = struct match array_access with | Some (arr, traces_arr, idx, traces_idx, is_plus) -> ( - let site = Sem.get_allocsite pname node 0 0 in let size = ArrayBlk.sizeof arr in let offset = ArrayBlk.offsetof arr in let idx = (if is_plus then Itv.plus else Itv.minus) offset idx in @@ -364,7 +367,7 @@ module Report = struct match (size, idx) with | NonBottom size, NonBottom idx -> let traces = TraceSet.merge ~traces_arr ~traces_idx location in - PO.ConditionSet.add_bo_safety pname location site ~size ~idx traces cond_set + PO.ConditionSet.add_array_access pname location ~size ~idx traces cond_set | _ -> cond_set ) | None -> @@ -452,15 +455,19 @@ module Report = struct let cond_set = match instr with | Sil.Load (_, exp, _, location) | Sil.Store (exp, _, _, location) -> - add_condition pname node exp location mem cond_set + add_condition pname exp location mem cond_set | Sil.Call (_, Const Cfun callee_pname, params, location, _) -> ( - match Summary.read_summary pdesc callee_pname with - | Some summary -> - let callee = extras callee_pname in - instantiate_cond tenv pname callee params mem summary location - |> PO.ConditionSet.join cond_set - | _ -> - cond_set ) + match Models.dispatcher callee_pname params with + | Some {Models.check} -> + check pname node location mem cond_set + | None -> + match Summary.read_summary pdesc callee_pname with + | Some summary -> + let callee = extras callee_pname in + instantiate_cond tenv pname callee params mem summary location + |> PO.ConditionSet.join cond_set + | _ -> + cond_set ) | _ -> cond_set in diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 8c14ce69e..0ea3b4c33 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -45,9 +45,12 @@ module Make (CFG : ProcCfg.S) = struct let check_alloc_size size_exp pname _node location mem cond_set = let _, _, length0 = get_malloc_info size_exp in let v_length = Sem.eval length0 mem in - let traces = Dom.Val.get_traces v_length in - let length = Dom.Val.get_itv v_length in - PO.ConditionSet.add_alloc_size pname location length traces cond_set + match Dom.Val.get_itv v_length with + | Bottom -> + cond_set + | NonBottom length -> + let traces = Dom.Val.get_traces v_length in + PO.ConditionSet.add_alloc_size pname location ~length traces cond_set let set_uninitialized node (typ: Typ.t) ploc mem = diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml index 72fbd04a1..0dda2909e 100644 --- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml +++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml @@ -15,6 +15,77 @@ module ItvPure = Itv.ItvPure module MF = MarkupFormatter module ValTraceSet = BufferOverrunTrace.Set +module AllocSizeCondition = struct + type t = ItvPure.astate + + let get_symbols = ItvPure.get_symbols + + let pp fmt length = F.fprintf fmt "alloc(%a)" ItvPure.pp length + + let pp_description fmt length = F.fprintf fmt "Alloc: %a" ItvPure.pp length + + let make ~length = if ItvPure.is_invalid length then None else Some length + + let have_similar_bounds = ItvPure.have_similar_bounds + + let xcompare ~lhs ~rhs = + match ItvPure.xcompare ~lhs ~rhs with + | `Equal -> + `Equal + | `NotComparable -> + `NotComparable + | `LeftSubsumesRight -> + `LeftSubsumesRight + | `RightSubsumesLeft -> + `RightSubsumesLeft + | `LeftSmallerThanRight | `RightSmallerThanLeft as cmp -> + let lpos = ItvPure.le_sem ItvPure.zero lhs in + let rpos = ItvPure.le_sem ItvPure.zero rhs in + if not (ItvPure.equal lpos rpos) then `NotComparable + else if ItvPure.is_true lpos then + match cmp with + | `LeftSmallerThanRight -> + `RightSubsumesLeft + | `RightSmallerThanLeft -> + `LeftSubsumesRight + else if ItvPure.is_false lpos then + match cmp with + | `LeftSmallerThanRight -> + `LeftSubsumesRight + | `RightSmallerThanLeft -> + `RightSubsumesLeft + else `NotComparable + + + let itv_big = ItvPure.of_int 1_000_000 + + let check length = + match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.zero with + | `Equal | `RightSubsumesLeft -> + Some IssueType.inferbo_alloc_is_zero + | `LeftSmallerThanRight -> + Some IssueType.inferbo_alloc_is_negative + | _ -> + match ItvPure.xcompare ~lhs:length ~rhs:ItvPure.mone with + | `Equal | `LeftSmallerThanRight | `RightSubsumesLeft -> + Some IssueType.inferbo_alloc_is_negative + | `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.lb length) -> + Some IssueType.inferbo_alloc_may_be_negative + | _ -> + match ItvPure.xcompare ~lhs:length ~rhs:itv_big with + | `Equal | `RightSmallerThanLeft | `RightSubsumesLeft -> + Some IssueType.inferbo_alloc_is_big + | `LeftSubsumesRight when Itv.Bound.is_not_infty (ItvPure.ub length) -> + Some IssueType.inferbo_alloc_may_be_big + | _ -> + None + + + let subst bound_map length = + match ItvPure.subst length bound_map with NonBottom length -> Some length | Bottom -> None + +end + module ArrayAccessCondition = struct type t = {idx: ItvPure.astate; size: ItvPure.astate} [@@deriving compare] @@ -160,32 +231,66 @@ module ArrayAccessCondition = struct end module Condition = struct - type t = ArrayAccess of ArrayAccessCondition.t [@@deriving compare] + type t = AllocSize of AllocSizeCondition.t | ArrayAccess of ArrayAccessCondition.t + + let make_alloc_size = Option.map ~f:(fun c -> AllocSize c) let make_array_access = Option.map ~f:(fun c -> ArrayAccess c) - let get_symbols = function ArrayAccess c -> ArrayAccessCondition.get_symbols c + let get_symbols = function + | AllocSize c -> + AllocSizeCondition.get_symbols c + | ArrayAccess c -> + ArrayAccessCondition.get_symbols c + let subst bound_map = function + | AllocSize c -> + AllocSizeCondition.subst bound_map c |> make_alloc_size | ArrayAccess c -> ArrayAccessCondition.subst bound_map c |> make_array_access let have_similar_bounds c1 c2 = - match (c1, c2) with ArrayAccess c1, ArrayAccess c2 -> - ArrayAccessCondition.have_similar_bounds c1 c2 + match (c1, c2) with + | AllocSize c1, AllocSize c2 -> + AllocSizeCondition.have_similar_bounds c1 c2 + | ArrayAccess c1, ArrayAccess c2 -> + ArrayAccessCondition.have_similar_bounds c1 c2 + | _ -> + false let xcompare ~lhs ~rhs = - match (lhs, rhs) with ArrayAccess lhs, ArrayAccess rhs -> - ArrayAccessCondition.xcompare ~lhs ~rhs + match (lhs, rhs) with + | AllocSize lhs, AllocSize rhs -> + AllocSizeCondition.xcompare ~lhs ~rhs + | ArrayAccess lhs, ArrayAccess rhs -> + ArrayAccessCondition.xcompare ~lhs ~rhs + | _ -> + `NotComparable - let pp fmt = function ArrayAccess c -> ArrayAccessCondition.pp fmt c + let pp fmt = function + | AllocSize c -> + AllocSizeCondition.pp fmt c + | ArrayAccess c -> + ArrayAccessCondition.pp fmt c + - let pp_description fmt = function ArrayAccess c -> ArrayAccessCondition.pp_description fmt c + let pp_description fmt = function + | AllocSize c -> + AllocSizeCondition.pp_description fmt c + | ArrayAccess c -> + ArrayAccessCondition.pp_description fmt c + + + let check = function + | AllocSize c -> + AllocSizeCondition.check c + | ArrayAccess c -> + ArrayAccessCondition.check c - let check = function ArrayAccess c -> ArrayAccessCondition.check c end module ConditionTrace = struct @@ -197,7 +302,6 @@ module ConditionTrace = struct type t = { proc_name: Typ.Procname.t ; location: Location.t - ; id: string ; cond_trace: cond_trace ; val_traces: ValTraceSet.t } [@@deriving compare] @@ -238,9 +342,9 @@ module ConditionTrace = struct match ct.cond_trace with Intra pname -> pname | Inter (caller_pname, _, _) -> caller_pname - let make : Typ.Procname.t -> Location.t -> string -> ValTraceSet.t -> t = - fun proc_name location id val_traces -> - {proc_name; location; id; cond_trace= Intra proc_name; val_traces} + let make : Typ.Procname.t -> Location.t -> ValTraceSet.t -> t = + fun proc_name location val_traces -> + {proc_name; location; cond_trace= Intra proc_name; val_traces} let make_call_and_subst ~traces_caller ~caller_pname ~callee_pname location ct = @@ -256,7 +360,7 @@ module ConditionSet = struct type t = condition_with_trace list - (* invariant: add_one of one of the elements should return the original list *) + (* invariant: join_one of one of the elements should return the original list *) let empty = [] @@ -284,7 +388,7 @@ module ConditionSet = struct else `KeepExistingAndContinue - let add_one condset new_ = + let join_one condset new_ = let rec aux ~new_ acc ~same = function | [] -> if same then new_ :: condset else new_ :: acc @@ -300,27 +404,32 @@ module ConditionSet = struct aux ~new_ [] ~same:true condset - let join condset1 condset2 = List.fold_left ~f:add_one condset1 ~init:condset2 + let join condset1 condset2 = List.fold_left ~f:join_one condset1 ~init:condset2 - let add_bo_safety pname location id ~idx ~size val_traces condset = - match ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access with + let add_opt pname location val_traces condset = function | None -> condset | Some cond -> - let trace = ConditionTrace.make pname location id val_traces in + let trace = ConditionTrace.make pname location val_traces in let cwt = {cond; trace} in join [cwt] condset - let add_alloc_size _pname _location _size _val_traces _condset = - L.(die InternalError) "Not implemented add_alloc_size" + let add_array_access pname location ~idx ~size val_traces condset = + ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access + |> add_opt pname location val_traces condset + + + let add_alloc_size pname location ~length val_traces condset = + AllocSizeCondition.make ~length |> Condition.make_alloc_size + |> add_opt pname location val_traces condset let subst condset (bound_map, trace_map) caller_pname callee_pname location = let subst_add_cwt condset cwt = match Condition.get_symbols cwt.cond with | [] -> - add_one condset cwt + join_one condset cwt | symbols -> match Condition.subst bound_map cwt.cond with | None -> @@ -339,7 +448,7 @@ module ConditionSet = struct location trace in let trace = make_call_and_subst cwt.trace in - add_one condset {cond; trace} + join_one condset {cond; trace} in List.fold condset ~f:subst_add_cwt ~init:[] diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 5cbf05e33..174827d71 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -837,6 +837,8 @@ module ItvPure = struct (lower, upper) + let mone = of_bound Bound.mone + let m1_255 = (Bound.minus_one, Bound._255) let nat = (Bound.zero, Bound.PInf) diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c index d104e5258..852c31953 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issue_kinds.c @@ -142,3 +142,19 @@ void may_over_or_underrun_symbolic2_Nowarn_Good(int n) { int a[n]; a[1] = 0; } + +void alloc_is_negative_Bad() { malloc(-2); } + +void alloc_may_be_negative_Bad() { malloc(zero_or_ten(0) - 5); } + +void alloc_may_be_negative_Good_FP() { malloc(zero_or_ten(1) - 5); } + +void alloc_is_zero_Bad() { malloc(0 * sizeof(int)); } + +void alloc_is_big_Bad() { malloc(2 * 1000 * 1000 * 1000); } + +void alloc_may_be_big_Bad() { malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1); } + +void alloc_may_be_big_Good_FP() { + malloc(zero_or_ten(1) * 100 * 1000 * 1000 + 1); +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 626ef0fb8..52132b740 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -21,6 +21,13 @@ codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_ codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/inf_loop.c, inf_loop, 4, CONDITION_ALWAYS_TRUE, [] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_big_Bad, 0, INFERBO_ALLOC_IS_BIG, [Alloc: [2000000000, 2000000000]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_negative_Bad, 0, INFERBO_ALLOC_IS_NEGATIVE, [Alloc: [-2, -2]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_is_zero_Bad, 0, INFERBO_ALLOC_IS_ZERO, [Alloc: [0, 0]] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Bad, 0, INFERBO_ALLOC_MAY_BE_BIG, [Call,Assignment,Return] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_big_Good_FP, 1, INFERBO_ALLOC_MAY_BE_BIG, [Call,Assignment,Return] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Bad, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, [Call,Assignment,Return] +codetoanalyze/c/bufferoverrun/issue_kinds.c, alloc_may_be_negative_Good_FP, 0, INFERBO_ALLOC_MAY_BE_NEGATIVE, [Call,Assignment,Return] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_overrun_Bad, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_concrete_underrun_Bad, 2, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [-1, -1] Size: [10, 10]] codetoanalyze/c/bufferoverrun/issue_kinds.c, l1_symbolic_overrun_Bad, 3, BUFFER_OVERRUN_L1, [ArrayDeclaration,ArrayAccess: Offset: [max(10, s$0), s$1] Size: [10, 10]]