[inferbo] Get global constant array values from initializers

Summary:
This diff gets global constant array values from their initializers.  The `find_global_array` function is
added to memory domain, which finds values of global array locations during the ondemand value
generation.

Reviewed By: ngorogiannis

Differential Revision: D19300143

fbshipit-source-id: 7b0b84c42

infer/src/IR/Pvar.ml

@@ -27,7 +27,8 @@ type pvar_kind =
       ; is_ice: bool (* is it integral constant expression? *)
       ; is_pod: bool
       ; is_static_local: bool
-      ; is_static_global: bool }  (** global variable *)
+      ; is_static_global: bool
+      ; is_constant_array: bool }  (** global variable *)
   | Seed_var  (** variable used to store the initial value of formal parameters *)
 [@@deriving compare]
 
@@ -103,6 +104,10 @@ let is_static_local pv =
   match pv.pv_kind with Global_var {is_static_local} -> is_static_local | _ -> false
 
 
+let is_constant_array pv =
+  match pv.pv_kind with Global_var {is_constant_array} -> is_constant_array | _ -> false
+
+
 (** Check if a pvar is the special "this" var *)
 let is_this pvar = Mangled.is_this (get_name pvar)
 
@@ -233,12 +238,19 @@ let mk_callee (name : Mangled.t) (proc_name : Procname.t) : t =
 
 (** create a global variable with the given name *)
 let mk_global ?(is_constexpr = false) ?(is_ice = false) ?(is_pod = true) ?(is_static_local = false)
-    ?(is_static_global = false) ?translation_unit (name : Mangled.t) : t =
+    ?(is_static_global = false) ?(is_constant_array = false) ?translation_unit (name : Mangled.t) :
+    t =
   { pv_hash= name_hash name
   ; pv_name= name
   ; pv_kind=
-      Global_var {translation_unit; is_constexpr; is_ice; is_pod; is_static_local; is_static_global}
-  }
+      Global_var
+        { translation_unit
+        ; is_constexpr
+        ; is_ice
+        ; is_pod
+        ; is_static_local
+        ; is_static_global
+        ; is_constant_array } }
 
 
 (** create a fresh temporary variable local to procedure [pname]. for use in the frontends only! *)

infer/src/IR/Pvar.mli

@@ -57,6 +57,9 @@ val is_global : t -> bool
 val is_static_local : t -> bool
 (** Check if the pvar is a static variable declared inside a function *)
 
+val is_constant_array : t -> bool
+(** Check if the pvar has a constant array type *)
+
 val is_local : t -> bool
 (** Check if the pvar is a (non-static) local var *)
 
@@ -111,6 +114,7 @@ val mk_global :
   -> ?is_pod:bool
   -> ?is_static_local:bool
   -> ?is_static_global:bool
+  -> ?is_constant_array:bool
   -> ?translation_unit:SourceFile.t
   -> Mangled.t
   -> t

infer/src/bufferoverrun/absLoc.ml

@@ -312,6 +312,23 @@ module Loc = struct
         is_global loc
 
 
+  let rec get_global_array_initializer =
+    let initializer_of_pvar pvar =
+      if Pvar.is_constant_array pvar then Pvar.get_initializer_pname pvar else None
+    in
+    function
+    | Var (Var.ProgramVar pvar) ->
+        initializer_of_pvar pvar
+    | Var (Var.LogicalVar _) ->
+        None
+    | Allocsite allocsite ->
+        Allocsite.get_path allocsite
+        |> Option.bind ~f:Symb.SymbolPath.get_pvar
+        |> Option.bind ~f:initializer_of_pvar
+    | Field {prefix= loc} | StarField {prefix= loc} ->
+        get_global_array_initializer loc
+
+
   let rec get_path = function
     | Var (LogicalVar _) ->
         None

infer/src/bufferoverrun/absLoc.mli

@@ -91,6 +91,10 @@ module Loc : sig
 
   val is_global : t -> bool
 
+  val get_global_array_initializer : t -> Procname.t option
+  (** Return the name of global initializer when given abstract location represents a global
+      constant array value *)
+
   val is_pretty : t -> bool
   (** It checks if it is representable with pretty form, e.g., with a path or with a variable name. *)
 

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -33,7 +33,7 @@ type extras =
 module CFG = ProcCfg.NormalOneInstrPerNode
 
 module Init = struct
-  let initial_state {ProcData.summary; tenv; extras= {oenv}} start_node =
+  let initial_state {ProcData.summary; tenv; extras= {get_summary; oenv}} start_node =
     let try_decl_local =
       let pname = Summary.get_proc_name summary in
       let model_env =
@@ -46,7 +46,7 @@ module Init = struct
         let loc = Loc.of_pvar (Pvar.mk name pname) in
         BoUtils.Exec.decl_local model_env (mem, inst_num) (loc, typ)
     in
-    let mem = Dom.Mem.init oenv in
+    let mem = Dom.Mem.init get_summary oenv in
     let mem, _ =
       List.fold ~f:try_decl_local ~init:(mem, 1)
         (Procdesc.get_locals (Summary.get_proc_desc summary))

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -1792,21 +1792,13 @@ module MemReach = struct
     ; mem_pure: MemPure.t
     ; alias: Alias.t
     ; latest_prune: LatestPrune.t
-    ; oenv: ('has_oenv, OndemandEnv.t) GOption.t }
+    ; oenv: ('has_oenv, OndemandEnv.t) GOption.t
+    ; find_global_array: ('has_oenv, Loc.t -> Val.t option) GOption.t }
 
   type no_oenv_t = GOption.none t0
 
   type t = GOption.some t0
 
-  let init : OndemandEnv.t -> t =
-   fun oenv ->
-    { stack_locs= StackLocs.bot
-    ; mem_pure= MemPure.bot
-    ; alias= Alias.init
-    ; latest_prune= LatestPrune.top
-    ; oenv= GOption.GSome oenv }
-
-
   let leq ~lhs ~rhs =
     if phys_equal lhs rhs then true
     else
@@ -1825,7 +1817,8 @@ module MemReach = struct
       ; mem_pure= MemPure.widen oenv ~prev:prev.mem_pure ~next:next.mem_pure ~num_iters
       ; alias= Alias.widen ~prev:prev.alias ~next:next.alias ~num_iters
       ; latest_prune= LatestPrune.widen ~prev:prev.latest_prune ~next:next.latest_prune ~num_iters
-      ; oenv= prev.oenv } )
+      ; oenv= prev.oenv
+      ; find_global_array= prev.find_global_array } )
 
 
   let join : t -> t -> t =
@@ -1836,7 +1829,8 @@ module MemReach = struct
     ; mem_pure= MemPure.join oenv x.mem_pure y.mem_pure
     ; alias= Alias.join x.alias y.alias
     ; latest_prune= LatestPrune.join x.latest_prune y.latest_prune
-    ; oenv= x.oenv }
+    ; oenv= x.oenv
+    ; find_global_array= x.find_global_array }
 
 
   let pp : F.formatter -> _ t0 -> unit =
@@ -1845,7 +1839,9 @@ module MemReach = struct
       MemPure.pp x.mem_pure Alias.pp x.alias LatestPrune.pp x.latest_prune
 
 
-  let unset_oenv : t -> no_oenv_t = function x -> {x with oenv= GOption.GNone}
+  let unset_oenv : t -> no_oenv_t =
+   fun x -> {x with oenv= GOption.GNone; find_global_array= GOption.GNone}
+
 
   let is_stack_loc : Loc.t -> _ t0 -> bool = fun l m -> StackLocs.mem l m.stack_locs
 
@@ -1855,10 +1851,17 @@ module MemReach = struct
 
   let find_stack : Loc.t -> _ t0 -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot
 
+  (** Find heap values from: (1) given abstract memory [m] (2) initializers of global array values
+      (3) otherwise, it generates symbolic or unknown values ondemand *)
   let find_heap_default : default:Val.t -> ?typ:Typ.t -> Loc.t -> _ t0 -> Val.t =
    fun ~default ?typ l m ->
+    let ondemand_fallback () =
+      GOption.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default ?typ oenv l)
+    in
     IOption.value_default_f (find_opt l m) ~f:(fun () ->
-        GOption.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default ?typ oenv l) )
+        GOption.value_map_f m.find_global_array ~default:ondemand_fallback
+          ~f:(fun find_global_array ->
+            IOption.value_default_f (find_global_array l) ~f:ondemand_fallback ) )
 
 
   let find_heap : ?typ:Typ.t -> Loc.t -> _ t0 -> Val.t =
@@ -1900,6 +1903,22 @@ module MemReach = struct
 
   let find_ret_alias : _ t0 -> AliasTargets.t = fun m -> Alias.find_ret m.alias
 
+  type get_summary = Procname.t -> no_oenv_t option
+
+  let init : get_summary -> OndemandEnv.t -> t =
+   fun get_summary oenv ->
+    let find_global_array loc =
+      Option.bind (Loc.get_global_array_initializer loc) ~f:(fun pname ->
+          Option.bind (get_summary pname) ~f:(find_opt loc) )
+    in
+    { stack_locs= StackLocs.bot
+    ; mem_pure= MemPure.bot
+    ; alias= Alias.init
+    ; latest_prune= LatestPrune.top
+    ; oenv= GOption.GSome oenv
+    ; find_global_array= GOption.GSome find_global_array }
+
+
   let load_alias : Ident.t -> Loc.t -> AliasTarget.t -> t -> t =
    fun id loc tgt m -> {m with alias= Alias.load id loc tgt m.alias}
 
@@ -2235,7 +2254,13 @@ module Mem = struct
 
   type get_summary = Procname.t -> no_oenv_t option
 
-  let init : OndemandEnv.t -> t = fun oenv -> NonBottom (MemReach.init oenv)
+  let init : get_summary -> OndemandEnv.t -> t =
+   fun get_summary oenv ->
+    let get_summary pname =
+      match get_summary pname with Some (NonBottom m) -> Some m | _ -> None
+    in
+    NonBottom (MemReach.init get_summary oenv)
+
 
   let f_lift_default : default:'a -> ('h MemReach.t0 -> 'a) -> 'h t0 -> 'a =
    fun ~default f m -> match m with Bottom | ExcRaised -> default | NonBottom m' -> f m'

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -457,7 +457,7 @@ module Mem : sig
 
   type get_summary = Procname.t -> no_oenv_t option
 
-  val init : BufferOverrunOndemandEnv.t -> t
+  val init : get_summary -> BufferOverrunOndemandEnv.t -> t
 
   val exc_raised : t
 

infer/src/clang/cGeneral_utils.ml

@@ -119,9 +119,9 @@ let mk_sil_global_var {CFrontend_config.source_file} ?(mk_name = fun _ x -> x) d
   in
   let is_constexpr = var_decl_info.Clang_ast_t.vdi_is_const_expr in
   let is_ice = var_decl_info.Clang_ast_t.vdi_is_init_ice in
+  let desugared_type = CAst_utils.get_desugared_type qt.Clang_ast_t.qt_type_ptr in
   let is_pod =
-    CAst_utils.get_desugared_type qt.Clang_ast_t.qt_type_ptr
-    |> Option.bind ~f:(function
+    Option.bind desugared_type ~f:(function
       | Clang_ast_t.RecordType (_, decl_ptr) ->
           CAst_utils.get_decl decl_ptr
       | _ ->
@@ -139,9 +139,12 @@ let mk_sil_global_var {CFrontend_config.source_file} ?(mk_name = fun _ x -> x) d
     && (not var_decl_info.Clang_ast_t.vdi_is_static_data_member)
     && var_decl_info.Clang_ast_t.vdi_is_static
   in
+  let is_constant_array =
+    Option.exists desugared_type ~f:(function Clang_ast_t.ConstantArrayType _ -> true | _ -> false)
+  in
   Pvar.mk_global ~is_constexpr ~is_ice ~is_pod
     ~is_static_local:var_decl_info.Clang_ast_t.vdi_is_static_local ~is_static_global
-    ?translation_unit (mk_name name_string simple_name)
+    ~is_constant_array ?translation_unit (mk_name name_string simple_name)
 
 
 let mk_sil_var trans_unit_ctx named_decl_info decl_info_qual_type_opt procname outer_procname =

infer/src/istd/GOption.ml

@@ -14,3 +14,6 @@ type (_, _) t = GNone : (none, _) t | GSome : 'a -> (some, 'a) t
 let value : (some, 'a) t -> 'a = function GSome v -> v
 
 let value_map (type h) (t : (h, _) t) ~default ~f = match t with GNone -> default | GSome v -> f v
+
+let value_map_f (type h) (t : (h, _) t) ~default ~f =
+  match t with GNone -> default () | GSome v -> f v

infer/src/istd/GOption.mli

@@ -14,3 +14,6 @@ type (_, _) t = GNone : (none, _) t | GSome : 'a -> (some, 'a) t
 val value : (some, 'a) t -> 'a
 
 val value_map : (_, 'a) t -> default:'b -> f:('a -> 'b) -> 'b
+
+val value_map_f : (_, 'a) t -> default:(unit -> 'b) -> f:('a -> 'b) -> 'b
+(** Like [value_map] but the default value is evaluated lazily *)

infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp

@@ -16,4 +16,4 @@ static int StaticGlobal[][3] = {
 
 void access_static_global1_Bad_FN() { int* p = StaticGlobal[10]; }
 
-void access_static_global2_Bad_FN() { int a = StaticGlobal[0][10]; }
+void access_static_global2_Bad() { int a = StaticGlobal[0][10]; }

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

@@ -50,6 +50,7 @@ codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::do_not_ignore_empt
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: -1 Size: 10]
 codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_loop_with_init_S_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Call,Parameter `length`,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
 codetoanalyze/cpp/bufferoverrun/global.cpp, access_constant_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Array access: Offset: 5 Size: 5]
+codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_flexible_array_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 7 Size: 5]
 codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: 5 Size: 5]