From c93c3163d6bde11fc1babcfd45e1d747bb86980a Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 21 Jan 2020 00:07:13 -0800 Subject: [PATCH] [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 | 20 +++++-- infer/src/IR/Pvar.mli | 4 ++ infer/src/bufferoverrun/absLoc.ml | 17 ++++++ infer/src/bufferoverrun/absLoc.mli | 4 ++ .../bufferoverrun/bufferOverrunAnalysis.ml | 4 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 55 ++++++++++++++----- .../src/bufferoverrun/bufferOverrunDomain.mli | 2 +- infer/src/clang/cGeneral_utils.ml | 17 +++--- infer/src/istd/GOption.ml | 3 + infer/src/istd/GOption.mli | 3 + .../cpp/bufferoverrun/global.cpp | 2 +- .../cpp/bufferoverrun/issues.exp | 1 + 12 files changed, 102 insertions(+), 30 deletions(-) diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml index 6d5cc0398..ad8aead3d 100644 --- a/infer/src/IR/Pvar.ml +++ b/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! *) diff --git a/infer/src/IR/Pvar.mli b/infer/src/IR/Pvar.mli index a820eabbd..dde0e437b 100644 --- a/infer/src/IR/Pvar.mli +++ b/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 diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 407d1cfba..59c7e46e0 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/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 diff --git a/infer/src/bufferoverrun/absLoc.mli b/infer/src/bufferoverrun/absLoc.mli index dee392bc8..f507e41a0 100644 --- a/infer/src/bufferoverrun/absLoc.mli +++ b/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. *) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 0e0fe48f8..8dda6c879 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/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)) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index cdea628fb..1ecc7f965 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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' diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index 2349e7068..21edb555d 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/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 diff --git a/infer/src/clang/cGeneral_utils.ml b/infer/src/clang/cGeneral_utils.ml index de1899533..fac733f31 100644 --- a/infer/src/clang/cGeneral_utils.ml +++ b/infer/src/clang/cGeneral_utils.ml @@ -119,13 +119,13 @@ 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 - | Clang_ast_t.RecordType (_, decl_ptr) -> - CAst_utils.get_decl decl_ptr - | _ -> - None ) + Option.bind desugared_type ~f:(function + | Clang_ast_t.RecordType (_, decl_ptr) -> + CAst_utils.get_decl decl_ptr + | _ -> + None ) |> Option.value_map ~default:true ~f:(function | Clang_ast_t.CXXRecordDecl (_, _, _, _, _, _, _, {xrdi_is_pod}) | Clang_ast_t.ClassTemplateSpecializationDecl (_, _, _, _, _, _, _, {xrdi_is_pod}, _, _) -> @@ -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 = diff --git a/infer/src/istd/GOption.ml b/infer/src/istd/GOption.ml index 416bc620b..239065b23 100644 --- a/infer/src/istd/GOption.ml +++ b/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 diff --git a/infer/src/istd/GOption.mli b/infer/src/istd/GOption.mli index 52cc838de..5ea907342 100644 --- a/infer/src/istd/GOption.mli +++ b/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 *) diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp index 7497cde8b..a1ed19ed2 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/global.cpp +++ b/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]; } diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index 20ca0b8a5..24bd7e734 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/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, [,Call,Assignment,,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, [,Call,Parameter `length`,Assignment,,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/cpp/bufferoverrun/global.cpp, access_constant_global_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: 5 Size: 5] +codetoanalyze/cpp/bufferoverrun/global.cpp, access_static_global2_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,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, [,Array declaration,Array access: Offset: 7 Size: 5] codetoanalyze/cpp/bufferoverrun/realloc.cpp, realloc_struct1_Bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,,Array declaration,Assignment,Array access: Offset: 5 Size: 5]