[inferbo] Do not alias values representing multiple values (Java, C partially)

Reviewed By: skcho

Differential Revision: D10317894

fbshipit-source-id: d9bf25699

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -173,7 +173,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           in
           let mem = Dom.Mem.update_mem locs v mem in
           let mem =
-            if PowLoc.is_singleton locs then
+            if PowLoc.is_singleton locs && not v.represents_multiple_values then
               let loc_v = PowLoc.min_elt locs in
               let pname = Procdesc.get_proc_name pdesc in
               match Typ.Procname.get_method pname with
@@ -251,42 +251,53 @@ module Init = struct
       -> Tenv.t
       -> node_hash:int
       -> Location.t
+      -> represents_multiple_values:bool
       -> Loc.t
       -> Typ.typ
       -> inst_num:int
       -> new_sym_num:Itv.Counter.t
       -> Dom.Mem.t
       -> Dom.Mem.t =
-   fun pname symbol_table path tenv ~node_hash location loc typ ~inst_num ~new_sym_num mem ->
+   fun pname symbol_table path tenv ~node_hash location ~represents_multiple_values loc typ
+       ~inst_num ~new_sym_num mem ->
     let max_depth = 2 in
     let new_alloc_num = Itv.Counter.make 1 in
-    let rec decl_sym_val pname path tenv ~node_hash location ~depth ~may_last_field loc typ mem =
+    let rec decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth
+        ~may_last_field loc typ mem =
       if depth > max_depth then mem
       else
         let depth = depth + 1 in
         match typ.Typ.desc with
         | Typ.Tint ikind ->
             let unsigned = Typ.ikind_is_unsigned ikind in
-            let v = Dom.Val.make_sym ~unsigned loc pname symbol_table path new_sym_num location in
+            let v =
+              Dom.Val.make_sym ~represents_multiple_values ~unsigned loc pname symbol_table path
+                new_sym_num location
+            in
             mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
         | Typ.Tfloat _ ->
-            let v = Dom.Val.make_sym loc pname symbol_table path new_sym_num location in
+            let v =
+              Dom.Val.make_sym ~represents_multiple_values loc pname symbol_table path new_sym_num
+                location
+            in
             mem |> Dom.Mem.add_heap loc v |> Dom.Mem.init_param_relation loc
         | Typ.Tptr (typ, _) when Language.curr_language_is Java -> (
           match typ with
           | {desc= Typ.Tarray {elt}} ->
               BoUtils.Exec.decl_sym_arr
                 ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-                pname symbol_table path tenv ~node_hash location ~depth loc elt ~inst_num
+                BoUtils.Exec.CSymArray_Array pname symbol_table path tenv ~node_hash location
-                ~new_sym_num ~new_alloc_num mem
+                ~represents_multiple_values ~depth loc elt ~inst_num ~new_sym_num ~new_alloc_num
+                mem
           | _ ->
               BoUtils.Exec.decl_sym_java_ptr
                 ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-                pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num mem )
+                pname path tenv ~node_hash location ~represents_multiple_values ~depth loc typ
+                ~inst_num ~new_alloc_num mem )
         | Typ.Tptr (typ, _) ->
-            BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname
+            BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field)
-              symbol_table path tenv ~node_hash location ~depth loc typ ~inst_num ~new_sym_num
+              BoUtils.Exec.CSymArray_Pointer pname symbol_table path tenv ~node_hash location
-              ~new_alloc_num mem
+              ~represents_multiple_values ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem
         | Typ.Tarray {elt; length; stride} ->
             let size =
               match length with
@@ -299,20 +310,21 @@ module Init = struct
             let stride = Option.map ~f:IntLit.to_int_exn stride in
             BoUtils.Exec.decl_sym_arr
               ~decl_sym_val:(decl_sym_val ~may_last_field:false)
-              pname symbol_table path tenv ~node_hash location ~depth loc elt ~offset ?size ?stride
+              BoUtils.Exec.CSymArray_Array pname symbol_table path tenv ~node_hash location
-              ~inst_num ~new_sym_num ~new_alloc_num mem
+              ~represents_multiple_values ~depth loc elt ~offset ?size ?stride ~inst_num
+              ~new_sym_num ~new_alloc_num mem
         | Typ.Tstruct typename -> (
           match Models.TypName.dispatch tenv typename with
           | Some {Models.declare_symbolic} ->
               let model_env = Models.mk_model_env pname node_hash location tenv symbol_table in
-              declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env ~depth
+              declare_symbolic ~decl_sym_val:(decl_sym_val ~may_last_field) path model_env
-                loc ~inst_num ~new_sym_num ~new_alloc_num mem
+                ~represents_multiple_values ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem
           | None ->
               let decl_fld ~may_last_field mem (fn, typ, _) =
                 let loc_fld = Loc.append_field loc ~fn in
                 let path = Itv.SymbolPath.field path fn in
-                decl_sym_val pname path tenv ~node_hash location ~depth loc_fld typ ~may_last_field
+                decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth
-                  mem
+                  loc_fld typ ~may_last_field mem
               in
               let decl_flds str =
                 IList.fold_last ~f:(decl_fld ~may_last_field:false)
@@ -327,7 +339,8 @@ module Init = struct
                 location ;
             mem
     in
-    decl_sym_val pname path tenv ~node_hash location ~depth:0 ~may_last_field:true loc typ mem
+    decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth:0
+      ~may_last_field:true loc typ mem
 
 
   let declare_symbolic_parameters :
@@ -336,18 +349,20 @@ module Init = struct
       -> node_hash:int
       -> Location.t
       -> Itv.SymbolTable.t
+      -> represents_multiple_values:bool
       -> inst_num:int
       -> (Pvar.t * Typ.t) list
       -> Dom.Mem.astate
       -> Dom.Mem.astate =
-   fun pname tenv ~node_hash location symbol_table ~inst_num formals mem ->
+   fun pname tenv ~node_hash location symbol_table ~represents_multiple_values ~inst_num formals
+       mem ->
     let new_sym_num = Itv.Counter.make 0 in
     let add_formal (mem, inst_num) (pvar, typ) =
       let loc = Loc.of_pvar pvar in
       let path = Itv.SymbolPath.of_pvar pvar in
       let mem =
-        declare_symbolic_val pname symbol_table path tenv ~node_hash location loc typ ~inst_num
+        declare_symbolic_val pname symbol_table path tenv ~node_hash location
-          ~new_sym_num mem
+          ~represents_multiple_values loc typ ~inst_num ~new_sym_num mem
       in
       (mem, inst_num + 1)
     in
@@ -355,21 +370,22 @@ module Init = struct
 
 
   let initial_state {ProcData.pdesc; tenv; extras= symbol_table} start_node =
-    let locals = Procdesc.get_locals pdesc in
     let node_hash = CFG.Node.hash start_node in
     let location = CFG.Node.loc start_node in
     let pname = Procdesc.get_proc_name pdesc in
-    let rec decl_local pname ~node_hash location loc typ ~inst_num ~dimension mem =
+    let rec decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values
+        ~dimension mem =
       match typ.Typ.desc with
       | Typ.Tarray {elt= typ; length; stride} ->
           let stride = Option.map ~f:IntLit.to_int_exn stride in
           BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length
-            ?stride ~inst_num ~dimension mem
+            ?stride ~inst_num ~represents_multiple_values ~dimension mem
       | Typ.Tstruct typname -> (
         match Models.TypName.dispatch tenv typname with
         | Some {Models.declare_local} ->
             let model_env = Models.mk_model_env pname node_hash location tenv symbol_table in
-            declare_local ~decl_local model_env loc ~inst_num ~dimension mem
+            declare_local ~decl_local model_env loc ~inst_num ~represents_multiple_values
+              ~dimension mem
         | None ->
             (mem, inst_num) )
       | _ ->
@@ -378,12 +394,14 @@ module Init = struct
     let try_decl_local (mem, inst_num) {ProcAttributes.name; typ} =
       let pvar = Pvar.mk name pname in
       let loc = Loc.of_pvar pvar in
-      decl_local pname ~node_hash location loc typ ~inst_num ~dimension:1 mem
+      decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:false
+        ~dimension:1 mem
     in
     let mem = Dom.Mem.init in
-    let mem, inst_num = List.fold ~f:try_decl_local ~init:(mem, 1) locals in
+    let mem, inst_num = List.fold ~f:try_decl_local ~init:(mem, 1) (Procdesc.get_locals pdesc) in
     let formals = Sem.get_formals pdesc in
-    declare_symbolic_parameters pname tenv ~node_hash location symbol_table ~inst_num formals mem
+    declare_symbolic_parameters pname tenv ~node_hash location symbol_table
+      ~represents_multiple_values:false ~inst_num formals mem
 end
 
 module Report = struct

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -25,7 +25,8 @@ module Val = struct
     ; arrayblk: ArrayBlk.astate
     ; offset_sym: Relation.Sym.astate
     ; size_sym: Relation.Sym.astate
-    ; traces: TraceSet.t }
+    ; traces: TraceSet.t
+    ; represents_multiple_values: bool }
 
   type t = astate
 
@@ -36,7 +37,8 @@ module Val = struct
     ; arrayblk= ArrayBlk.bot
     ; offset_sym= Relation.Sym.bot
     ; size_sym= Relation.Sym.bot
-    ; traces= TraceSet.empty }
+    ; traces= TraceSet.empty
+    ; represents_multiple_values= false }
 
 
   let pp fmt x =
@@ -46,26 +48,27 @@ module Val = struct
     let trace_pp fmt traces =
       if Config.bo_debug >= 1 then F.fprintf fmt ", %a" TraceSet.pp traces
     in
-    F.fprintf fmt "(%a%a, %a, %a%a%a%a)" Itv.pp x.itv relation_sym_pp x.sym PowLoc.pp x.powloc
+    let represents_multiple_values_str = if x.represents_multiple_values then "M" else "" in
-      ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp x.size_sym trace_pp
+    F.fprintf fmt "%s(%a%a, %a, %a%a%a%a)" represents_multiple_values_str Itv.pp x.itv
-      x.traces
+      relation_sym_pp x.sym PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym
+      relation_sym_pp x.size_sym trace_pp x.traces
 
 
-  let unknown : traces:TraceSet.t -> t =
+  let sets_represents_multiple_values : represents_multiple_values:bool -> t -> t =
-   fun ~traces ->
+   fun ~represents_multiple_values x -> {x with represents_multiple_values}
+
+
+  let unknown_from : callee_pname:_ -> location:_ -> t =
+   fun ~callee_pname ~location ->
+    let traces = TraceSet.singleton (Trace.UnknownFrom (callee_pname, location)) in
     { itv= Itv.top
     ; sym= Relation.Sym.top
     ; powloc= PowLoc.unknown
     ; arrayblk= ArrayBlk.unknown
     ; offset_sym= Relation.Sym.top
     ; size_sym= Relation.Sym.top
-    ; traces }
+    ; traces
-
+    ; represents_multiple_values= false }
-
-  let unknown_from : callee_pname:_ -> location:_ -> t =
-   fun ~callee_pname ~location ->
-    let traces = TraceSet.singleton (Trace.UnknownFrom (callee_pname, location)) in
-    unknown ~traces
 
 
   let ( <= ) ~lhs ~rhs =
@@ -77,6 +80,7 @@ module Val = struct
       && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk
       && Relation.Sym.( <= ) ~lhs:lhs.offset_sym ~rhs:rhs.offset_sym
       && Relation.Sym.( <= ) ~lhs:lhs.size_sym ~rhs:rhs.size_sym
+      && Bool.( <= ) lhs.represents_multiple_values rhs.represents_multiple_values
 
 
   let equal x y = phys_equal x y || (( <= ) ~lhs:x ~rhs:y && ( <= ) ~lhs:y ~rhs:x)
@@ -90,7 +94,9 @@ module Val = struct
       ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters
       ; offset_sym= Relation.Sym.widen ~prev:prev.offset_sym ~next:next.offset_sym ~num_iters
       ; size_sym= Relation.Sym.widen ~prev:prev.size_sym ~next:next.size_sym ~num_iters
-      ; traces= TraceSet.join prev.traces next.traces }
+      ; traces= TraceSet.join prev.traces next.traces
+      ; represents_multiple_values=
+          prev.represents_multiple_values || next.represents_multiple_values }
 
 
   let join : t -> t -> t =
@@ -103,7 +109,8 @@ module Val = struct
       ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk
       ; offset_sym= Relation.Sym.join x.offset_sym y.offset_sym
       ; size_sym= Relation.Sym.join x.size_sym y.size_sym
-      ; traces= TraceSet.join x.traces y.traces }
+      ; traces= TraceSet.join x.traces y.traces
+      ; represents_multiple_values= x.represents_multiple_values || y.represents_multiple_values }
 
 
   let get_itv : t -> Itv.t = fun x -> x.itv
@@ -150,7 +157,8 @@ module Val = struct
   let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
 
   let make_sym :
-         ?unsigned:bool
+         represents_multiple_values:bool
+      -> ?unsigned:bool
       -> Loc.t
       -> Typ.Procname.t
       -> Itv.SymbolTable.t
@@ -158,11 +166,13 @@ module Val = struct
       -> Itv.Counter.t
       -> Location.t
       -> t =
-   fun ?(unsigned = false) loc pname symbol_table path new_sym_num location ->
+   fun ~represents_multiple_values ?(unsigned = false) loc pname symbol_table path new_sym_num
+       location ->
     { bot with
       itv= Itv.make_sym ~unsigned pname symbol_table (Itv.SymbolPath.normal path) new_sym_num
     ; sym= Relation.Sym.of_loc loc
-    ; traces= TraceSet.singleton (Trace.SymAssign (loc, location)) }
+    ; traces= TraceSet.singleton (Trace.SymAssign (loc, location))
+    ; represents_multiple_values }
 
 
   let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top}
@@ -216,7 +226,17 @@ module Val = struct
 
   let lor_sem : t -> t -> t = lift_cmp_itv Itv.lor_sem
 
-  let lift_prune1 : (Itv.t -> Itv.t) -> t -> t = fun f x -> {x with itv= f x.itv}
+  (* TODO: get rid of those cases *)
+  let warn_against_pruning_multiple_values : t -> t =
+   fun x ->
+    if x.represents_multiple_values && Config.write_html then
+      L.d_str_color Pp.Red (F.asprintf "Pruned %a that represents multiple values\n" pp x) ;
+    x
+
+
+  let lift_prune1 : (Itv.t -> Itv.t) -> t -> t =
+   fun f x -> warn_against_pruning_multiple_values {x with itv= f x.itv}
+
 
   let lift_prune2 :
          (Itv.t -> Itv.t -> Itv.t)
@@ -225,10 +245,11 @@ module Val = struct
       -> t
       -> t =
    fun f g x y ->
-    { x with
+    warn_against_pruning_multiple_values
-      itv= f x.itv y.itv
+      { x with
-    ; arrayblk= g x.arrayblk y.arrayblk
+        itv= f x.itv y.itv
-    ; traces= TraceSet.join x.traces y.traces }
+      ; arrayblk= g x.arrayblk y.arrayblk
+      ; traces= TraceSet.join x.traces y.traces }
 
 
   let prune_eq_zero : t -> t = lift_prune1 Itv.prune_eq_zero

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -39,6 +39,7 @@ type declare_local_fun =
   -> model_env
   -> Loc.t
   -> inst_num:int
+  -> represents_multiple_values:bool
   -> dimension:int
   -> Dom.Mem.astate
   -> Dom.Mem.astate * int
@@ -47,6 +48,7 @@ type declare_symbolic_fun =
      decl_sym_val:BoUtils.Exec.decl_sym_val
   -> Itv.SymbolPath.partial
   -> model_env
+  -> represents_multiple_values:bool
   -> depth:int
   -> Loc.t
   -> inst_num:int
@@ -304,18 +306,20 @@ end
 
 module StdArray = struct
   let typ typ length =
-    let declare_local ~decl_local {pname; node_hash; location} loc ~inst_num ~dimension mem =
+    let declare_local ~decl_local {pname; node_hash; location} loc ~inst_num
+        ~represents_multiple_values ~dimension mem =
       (* should this be deferred to the constructor? *)
       let length = Some (IntLit.of_int64 length) in
       BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc typ ~length ~inst_num
-        ~dimension mem
+        ~represents_multiple_values ~dimension mem
     in
-    let declare_symbolic ~decl_sym_val path {pname; tenv; node_hash; location; symbol_table} ~depth
+    let declare_symbolic ~decl_sym_val path {pname; tenv; node_hash; location; symbol_table}
-        loc ~inst_num ~new_sym_num ~new_alloc_num mem =
+        ~represents_multiple_values ~depth loc ~inst_num ~new_sym_num ~new_alloc_num mem =
       let offset = Itv.zero in
       let size = Itv.of_int64 length in
-      BoUtils.Exec.decl_sym_arr ~decl_sym_val pname symbol_table path tenv ~node_hash location
+      BoUtils.Exec.decl_sym_arr ~decl_sym_val BoUtils.Exec.CSymArray_Array pname symbol_table path
-        ~depth loc typ ~offset ~size ~inst_num ~new_sym_num ~new_alloc_num mem
+        tenv ~node_hash location ~represents_multiple_values ~depth loc typ ~offset ~size ~inst_num
+        ~new_sym_num ~new_alloc_num mem
     in
     {declare_local; declare_symbolic}
 
@@ -351,11 +355,12 @@ module StdArray = struct
         "No %s type model in %a at %a" kind Typ.Procname.pp pname Location.pp location ;
       mem
     in
-    let declare_local ~decl_local:_ {pname; location} _loc ~inst_num ~dimension:_ mem =
+    let declare_local ~decl_local:_ {pname; location} _loc ~inst_num ~represents_multiple_values:_
+        ~dimension:_ mem =
       (no_model "local" pname location mem, inst_num)
     in
-    let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~depth:_ _loc ~inst_num:_
+    let declare_symbolic ~decl_sym_val:_ _path {pname; location} ~represents_multiple_values:_
-        ~new_sym_num:_ ~new_alloc_num:_ mem =
+        ~depth:_ _loc ~inst_num:_ ~new_sym_num:_ ~new_alloc_num:_ mem =
       no_model "symbolic" pname location mem
     in
     {declare_local; declare_symbolic}
@@ -367,12 +372,15 @@ end
 - each time we delete an element, we decrease the length of the array *)
 module Collection = struct
   let typ =
-    let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num ~dimension mem =
+    let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num
-      BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num ~dimension mem
+        ~represents_multiple_values ~dimension mem =
+      BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num
+        ~represents_multiple_values ~dimension mem
     in
-    let declare_symbolic ~decl_sym_val:_ path {pname; location; symbol_table} ~depth:_ loc
+    let declare_symbolic ~decl_sym_val:_ path {pname; location; symbol_table}
-        ~inst_num:_ ~new_sym_num ~new_alloc_num:_ mem =
+        ~represents_multiple_values ~depth:_ loc ~inst_num:_ ~new_sym_num ~new_alloc_num:_ mem =
-      BoUtils.Exec.decl_sym_collection pname symbol_table path location loc ~new_sym_num mem
+      BoUtils.Exec.decl_sym_collection pname symbol_table path location ~represents_multiple_values
+        loc ~new_sym_num mem
     in
     {declare_local; declare_symbolic}
 

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -26,7 +26,8 @@ module Exec = struct
     let locs = val_ |> Dom.Val.get_all_locs in
     let v = Dom.Mem.find_set locs mem in
     let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
-    if PowLoc.is_singleton locs then Dom.Mem.load_simple_alias id (PowLoc.min_elt locs) mem
+    if PowLoc.is_singleton locs && not v.represents_multiple_values then
+      Dom.Mem.load_simple_alias id (PowLoc.min_elt locs) mem
     else mem
 
 
@@ -37,6 +38,7 @@ module Exec = struct
     -> Loc.t
     -> Typ.t
     -> inst_num:int
+    -> represents_multiple_values:bool
     -> dimension:int
     -> Dom.Mem.astate
     -> Dom.Mem.astate * int
@@ -51,25 +53,29 @@ module Exec = struct
       -> length:IntLit.t option
       -> ?stride:int
       -> inst_num:int
+      -> represents_multiple_values:bool
       -> dimension:int
       -> Dom.Mem.astate
       -> Dom.Mem.astate * int =
-   fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num ~dimension mem ->
+   fun ~decl_local pname ~node_hash location loc typ ~length ?stride ~inst_num
+       ~represents_multiple_values ~dimension mem ->
     let offset = Itv.zero in
     let size = Option.value_map ~default:Itv.top ~f:Itv.of_int_lit length in
     let path = Loc.get_path loc in
     let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in
-    let arr =
-      Dom.Val.of_array_alloc allocsite ~stride ~offset ~size
-      |> Dom.Val.add_trace_elem (Trace.ArrDecl location)
-    in
     let mem =
+      let arr =
+        Dom.Val.of_array_alloc allocsite ~stride ~offset ~size
+        |> Dom.Val.add_trace_elem (Trace.ArrDecl location)
+        |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
+      in
       if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem else Dom.Mem.add_heap loc arr mem
     in
     let mem = Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None mem in
     let loc = Loc.of_allocsite allocsite in
     let mem, _ =
-      decl_local pname ~node_hash location loc typ ~inst_num ~dimension:(dimension + 1) mem
+      decl_local pname ~node_hash location loc typ ~inst_num ~represents_multiple_values:true
+        ~dimension:(dimension + 1) mem
     in
     (mem, inst_num + 1)
 
@@ -80,31 +86,37 @@ module Exec = struct
       -> Location.t
       -> Loc.t
       -> inst_num:int
+      -> represents_multiple_values:bool
       -> dimension:int
       -> Dom.Mem.astate
       -> Dom.Mem.astate * int =
-   fun pname ~node_hash location loc ~inst_num ~dimension mem ->
+   fun pname ~node_hash location loc ~inst_num ~represents_multiple_values ~dimension mem ->
     let path = Loc.get_path loc in
     let allocsite = Allocsite.make pname ~node_hash ~inst_num ~dimension ~path in
     let alloc_loc = Loc.of_allocsite allocsite in
-    let alist =
-      Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc)
-      |> Dom.Val.add_trace_elem (Trace.ArrDecl location)
-    in
-    let size = Dom.Val.of_int 0 in
     let mem =
+      let alist =
+        Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc)
+        |> Dom.Val.add_trace_elem (Trace.ArrDecl location)
+        |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
+      in
       if Int.equal dimension 1 then Dom.Mem.add_stack loc alist mem
-      else Dom.Mem.add_heap loc alist mem |> Dom.Mem.add_heap alloc_loc size
+      else
+        let size = Dom.Val.Itv.zero in
+        Dom.Mem.add_heap loc alist mem |> Dom.Mem.add_heap alloc_loc size
     in
     (mem, inst_num + 1)
 
 
+  type c_sym_array_kind = CSymArray_Array | CSymArray_Pointer
+
   type decl_sym_val =
        Typ.Procname.t
     -> Itv.SymbolPath.partial
     -> Tenv.t
     -> node_hash:int
     -> Location.t
+    -> represents_multiple_values:bool
     -> depth:int
     -> Loc.t
     -> Typ.t
@@ -113,12 +125,14 @@ module Exec = struct
 
   let decl_sym_arr :
          decl_sym_val:decl_sym_val
+      -> c_sym_array_kind
       -> Typ.Procname.t
       -> Itv.SymbolTable.t
       -> Itv.SymbolPath.partial
       -> Tenv.t
       -> node_hash:int
       -> Location.t
+      -> represents_multiple_values:bool
       -> depth:int
       -> Loc.t
       -> Typ.t
@@ -130,8 +144,9 @@ module Exec = struct
       -> new_alloc_num:Itv.Counter.t
       -> Dom.Mem.astate
       -> Dom.Mem.astate =
-   fun ~decl_sym_val pname symbol_table path tenv ~node_hash location ~depth loc typ ?offset ?size
+   fun ~decl_sym_val array_kind pname symbol_table path tenv ~node_hash location
-       ?stride ~inst_num ~new_sym_num ~new_alloc_num mem ->
+       ~represents_multiple_values ~depth loc typ ?offset ?size ?stride ~inst_num ~new_sym_num
+       ~new_alloc_num mem ->
     let option_value opt_x default_f = match opt_x with Some x -> x | None -> default_f () in
     let offset =
       option_value offset (fun () ->
@@ -142,21 +157,28 @@ module Exec = struct
           Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
       )
     in
-    let alloc_num = Itv.Counter.next new_alloc_num in
-    let elem = Trace.SymAssign (loc, location) in
     let allocsite =
+      let alloc_num = Itv.Counter.next new_alloc_num in
       Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path)
     in
-    let arr =
-      Dom.Val.of_array_alloc allocsite ~stride ~offset ~size |> Dom.Val.add_trace_elem elem
-    in
     let mem =
+      let arr =
+        let elem = Trace.SymAssign (loc, location) in
+        Dom.Val.of_array_alloc allocsite ~stride ~offset ~size
+        |> Dom.Val.add_trace_elem elem
+        |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
+      in
       mem |> Dom.Mem.add_heap loc arr |> Dom.Mem.init_param_relation loc
       |> Dom.Mem.init_array_relation allocsite ~offset ~size ~size_exp_opt:None
     in
     let deref_loc = Loc.of_allocsite allocsite in
     let path = Itv.SymbolPath.index path in
-    decl_sym_val pname path tenv ~node_hash location ~depth deref_loc typ mem
+    let represents_multiple_values =
+      match array_kind with CSymArray_Array -> true | CSymArray_Pointer -> false
+      (* unsound but avoids many FPs for non-array pointers *)
+    in
+    decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth deref_loc
+      typ mem
 
 
   let decl_sym_java_ptr :
@@ -166,6 +188,7 @@ module Exec = struct
       -> Tenv.t
       -> node_hash:int
       -> Location.t
+      -> represents_multiple_values:bool
       -> depth:int
       -> Loc.t
       -> Typ.t
@@ -173,17 +196,22 @@ module Exec = struct
       -> new_alloc_num:Itv.Counter.t
       -> Dom.Mem.astate
       -> Dom.Mem.astate =
-   fun ~decl_sym_val pname path tenv ~node_hash location ~depth loc typ ~inst_num ~new_alloc_num
+   fun ~decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth loc typ
-       mem ->
+       ~inst_num ~new_alloc_num mem ->
     let alloc_num = Itv.Counter.next new_alloc_num in
     let elem = Trace.SymAssign (loc, location) in
     let allocsite =
       Allocsite.make pname ~node_hash ~inst_num ~dimension:alloc_num ~path:(Some path)
     in
     let alloc_loc = Loc.of_allocsite allocsite in
-    let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) |> Dom.Val.add_trace_elem elem in
+    let v =
+      Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc)
+      |> Dom.Val.add_trace_elem elem
+      |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
+    in
     let mem = Dom.Mem.add_heap loc v mem in
-    decl_sym_val pname path tenv ~node_hash location ~depth alloc_loc typ mem
+    decl_sym_val pname path tenv ~node_hash location ~represents_multiple_values ~depth alloc_loc
+      typ mem
 
 
   let decl_sym_collection :
@@ -191,15 +219,17 @@ module Exec = struct
       -> Itv.SymbolTable.t
       -> Itv.SymbolPath.partial
       -> Location.t
+      -> represents_multiple_values:bool
       -> Loc.t
       -> new_sym_num:Itv.Counter.t
       -> Dom.Mem.astate
       -> Dom.Mem.astate =
-   fun pname symbol_table path location loc ~new_sym_num mem ->
+   fun pname symbol_table path location ~represents_multiple_values loc ~new_sym_num mem ->
     let size =
       Itv.make_sym ~unsigned:true pname symbol_table (Itv.SymbolPath.length path) new_sym_num
       |> Dom.Val.of_itv
       |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
+      |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
     in
     Dom.Mem.add_heap loc size mem
 

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -23,6 +23,7 @@ module Exec : sig
     -> Loc.t
     -> Typ.t
     -> inst_num:int
+    -> represents_multiple_values:bool
     -> dimension:int
     -> Dom.Mem.astate
     -> Dom.Mem.astate * int
@@ -37,6 +38,7 @@ module Exec : sig
     -> length:IntLit.t option
     -> ?stride:int
     -> inst_num:int
+    -> represents_multiple_values:bool
     -> dimension:int
     -> Dom.Mem.astate
     -> Dom.Mem.astate * int
@@ -47,6 +49,7 @@ module Exec : sig
     -> Location.t
     -> Loc.t
     -> inst_num:int
+    -> represents_multiple_values:bool
     -> dimension:int
     -> Dom.Mem.astate
     -> Dom.Mem.astate * int
@@ -57,20 +60,25 @@ module Exec : sig
     -> Tenv.t
     -> node_hash:int
     -> Location.t
+    -> represents_multiple_values:bool
     -> depth:int
     -> Loc.t
     -> Typ.t
     -> Dom.Mem.astate
     -> Dom.Mem.astate
 
+  type c_sym_array_kind = CSymArray_Array | CSymArray_Pointer
+
   val decl_sym_arr :
        decl_sym_val:decl_sym_val
+    -> c_sym_array_kind
     -> Typ.Procname.t
     -> Itv.SymbolTable.t
     -> Itv.SymbolPath.partial
     -> Tenv.t
     -> node_hash:int
     -> Location.t
+    -> represents_multiple_values:bool
     -> depth:int
     -> Loc.t
     -> Typ.t
@@ -90,6 +98,7 @@ module Exec : sig
     -> Tenv.t
     -> node_hash:int
     -> Location.t
+    -> represents_multiple_values:bool
     -> depth:int
     -> Loc.t
     -> Typ.t
@@ -103,6 +112,7 @@ module Exec : sig
     -> Itv.SymbolTable.t
     -> Itv.SymbolPath.partial
     -> Location.t
+    -> represents_multiple_values:bool
     -> Loc.t
     -> new_sym_num:Itv.Counter.t
     -> Dom.Mem.astate

infer/tests/codetoanalyze/c/bufferoverrun/array_content.c

@@ -0,0 +1,54 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+int check_sorted_arr_good_FP(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;
+    }
+  }
+  return 1;
+}
+
+int check_sorted_arr10_good_FP(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;
+    }
+  }
+  return 1;
+}
+
+int check_sorted_ptr_good_FP(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;
+    }
+  }
+  return 1;
+}
+
+int array_min_index_from_one_FP(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
+      index_min = i;
+    } else {
+      index_min = i;
+    }
+  }
+  return index_min;
+}
+
+/*
+  We need a either a narrowing or a relational domain to prove that
+  index_min < length
+*/
+void call_array_min_index_from_one_good_FP() {
+  int a[2];
+  a[array_min_index_from_one_FP(a, 2) - 1] = 0;
+}

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -7,6 +7,11 @@ codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min2_Good_FP, 2, BUFFER_OVERR
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min3_Good_FP, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 25] Size: 20]
 codetoanalyze/c/bufferoverrun/arith.c, plus_linear_min_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,Return,ArrayAccess: Offset: [0, 19] Size: 19]
 codetoanalyze/c/bufferoverrun/arith.c, use_int64_max_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 15 Size: 10]
+codetoanalyze/c/bufferoverrun/array_content.c, array_min_index_from_one_FP, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
+codetoanalyze/c/bufferoverrun/array_content.c, call_array_min_index_from_one_good_FP, 2, BUFFER_OVERRUN_L4, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: a,Assignment,ArrayAccess: Offset: [1, +oo] Size: 2 by call to `array_min_index_from_one_FP` ]
+codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr10_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
+codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_arr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
+codetoanalyze/c/bufferoverrun/array_content.c, check_sorted_ptr_good_FP, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, []
 codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Offset: [3xlen.lb + 1, 3xlen.ub + 1] Size: [3xlen.lb + 1, 3xlen.ub + 1]]
 codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: 20 Size: 10]
 codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Assignment,Assignment,Assignment,ArrayAccess: Offset: -1 Size: 2]

infer/tests/codetoanalyze/java/performance/Loops.java

@@ -35,4 +35,29 @@ public class Loops {
       a++;
     } while (a < 20);
   }
+
+  static void dumb0(long[] a, int length) {
+    for (int i = 1; i < length; i++) {
+      if (a[i] < a[i - 1]) {
+        a[i - 1] = 0;
+      } else {
+        a[i] = 1;
+      }
+    }
+  }
+
+  static void dumbSort(long[] a, long[] b, int length) {
+    for (int i = length - 1; i >= 0; --i) {
+      for (int j = 0; j < i; ++j) {
+        if (a[j] * b[j + 1] > a[j + 1] * b[j]) {
+          long temp = a[j + 1];
+          a[j + 1] = a[j];
+          a[j] = temp;
+          temp = b[j + 1];
+          b[j + 1] = b[j];
+          b[j] = temp;
+        }
+      }
+    }
+  }
 }

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -112,6 +112,16 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 249, degree = 0]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 250, degree = 0]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 249, degree = 0]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 29 * (length.ub + -1), degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 29 * (length.ub + -1), degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 29 * (length.ub + -1), degree = 1]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 76 * (length.ub + -1)^2 + 8 * length.ub, degree = 2]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 797, degree = 0]