[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

@@ -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"

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

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,8 +455,12 @@ 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 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

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
+    match Dom.Val.get_itv v_length with
+    | Bottom ->
+        cond_set
+    | NonBottom length ->
         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
-    PO.ConditionSet.add_alloc_size pname location length traces cond_set
 
 
   let set_uninitialized node (typ: Typ.t) ploc mem =

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 ->
+    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 ->
+    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
+    | AllocSize c ->
+        AllocSizeCondition.pp fmt c
+    | ArrayAccess c ->
+        ArrayAccessCondition.pp fmt c
+
 
+  let pp_description fmt = function
+    | AllocSize c ->
+        AllocSizeCondition.pp_description fmt c
+    | ArrayAccess c ->
+        ArrayAccessCondition.pp_description fmt c
 
-  let pp fmt = function ArrayAccess c -> ArrayAccessCondition.pp fmt c
 
-  let pp_description fmt = function 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 =
+  let make : Typ.Procname.t -> Location.t -> ValTraceSet.t -> t =
-    fun proc_name location id val_traces ->
+    fun proc_name location val_traces ->
-      {proc_name; location; id; cond_trace= Intra proc_name; 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 =
+  let add_opt pname location val_traces condset = function
-    match ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access with
     | 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 =
+  let add_array_access pname location ~idx ~size val_traces condset =
-    L.(die InternalError) "Not implemented add_alloc_size"
+    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:[]
 

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)

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);
+}

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]]