[inferbo] Add model of class.getEnumConstants

Summary:
The model returns an array the length of which is the same to that of enum entries.

It takes the length of enum entries from the summary of `Enum.values` because it is not written in `tenv`. In order to do that, the model semantics should be able to request the summary of the function with `get_summary`, so I extended `model_env` to include the functionality.

Reviewed By: ezgicicek

Differential Revision: D21843319

fbshipit-source-id: d6f10eb91

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -35,7 +35,7 @@ module Init = struct
         let node_hash = CFG.Node.hash start_node in
         let location = CFG.Node.loc start_node in
         let integer_type_widths = oenv.OndemandEnv.integer_type_widths in
-        BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
+        BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths get_summary
       in
       fun (mem, inst_num) {ProcAttributes.name; typ} ->
         let loc = Loc.of_pvar (Pvar.mk name pname) in
@@ -305,6 +305,7 @@ module TransferFunctions = struct
           let pname = Procdesc.get_proc_name proc_desc in
           let node_hash = CFG.Node.hash node in
           BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
+            get_summary
         in
         match modeled_load_of_empty_collection_opt exp model_env (id, typ) mem with
         | Some mem' ->
@@ -326,6 +327,7 @@ module TransferFunctions = struct
         let node_hash = CFG.Node.hash node in
         let model_env =
           BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
+            get_summary
         in
         let tgt_locs = Sem.eval_locs tgt_exp mem in
         let tgt_deref =
@@ -343,6 +345,7 @@ module TransferFunctions = struct
           let pname = Procdesc.get_proc_name proc_desc in
           let node_hash = CFG.Node.hash node in
           BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
+            get_summary
         in
         let do_alloc = not (Sem.is_stack_exp exp1 mem) in
         BoUtils.Exec.decl_string model_env ~do_alloc locs s mem
@@ -385,7 +388,7 @@ module TransferFunctions = struct
             let model_env =
               let node_hash = CFG.Node.hash node in
               BoUtils.ModelEnv.mk_model_env callee_pname ~node_hash location tenv
-                integer_type_widths
+                integer_type_widths get_summary
             in
             exec model_env ~ret mem
         | None -> (
@@ -412,6 +415,7 @@ module TransferFunctions = struct
           let pname = Procdesc.get_proc_name proc_desc in
           let node_hash = CFG.Node.hash node in
           BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
+            get_summary
         in
         let mem, _ = BoUtils.Exec.decl_local model_env (mem, 1) (Loc.of_pvar pvar, typ) in
         mem
@@ -442,9 +446,10 @@ let compute_invariant_map :
   let cfg = CFG.from_pdesc proc_desc in
   let analysis_data =
     let proc_name = Procdesc.get_proc_name proc_desc in
-    let get_summary proc_name = analyze_dependency proc_name |> Option.map ~f:snd in
+    let open IOption.Let_syntax in
+    let get_summary proc_name = analyze_dependency proc_name >>| snd in
     let get_formals callee_pname =
-      AnalysisCallbacks.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals
+      AnalysisCallbacks.get_proc_desc callee_pname >>| Procdesc.get_pvar_formals
     in
     let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in
     let oenv = OndemandEnv.mk proc_desc tenv integer_type_widths in

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -9,6 +9,7 @@
 
 open! IStd
 open! AbstractDomain.Types
+module BoSummary = BufferOverrunAnalysisSummary
 module BoUtils = BufferOverrunUtils
 module CFG = BufferOverrunAnalysis.CFG
 module Dom = BufferOverrunDomain
@@ -256,6 +257,7 @@ type get_checks_summary = Procname.t -> checks_summary option
 
 let check_instr :
        get_checks_summary
+    -> BoSummary.get_summary
     -> BoUtils.get_formals
     -> Procname.t
     -> Tenv.t
@@ -265,7 +267,8 @@ let check_instr :
     -> Dom.Mem.t
     -> PO.ConditionSet.checked_t
     -> PO.ConditionSet.checked_t =
- fun get_checks_summary get_formals pname tenv integer_type_widths node instr mem cond_set ->
+ fun get_checks_summary get_summary get_formals pname tenv integer_type_widths node instr mem
+     cond_set ->
   match instr with
   | Sil.Load {e= exp; loc= location} ->
       cond_set
@@ -291,6 +294,7 @@ let check_instr :
           let model_env =
             let node_hash = CFG.Node.hash node in
             BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
+              get_summary
           in
           check model_env mem cond_set
       | None -> (
@@ -322,6 +326,7 @@ let print_debug_info : Sil.instr -> Dom.Mem.t -> PO.ConditionSet.checked_t -> un
 
 let check_instrs :
        get_checks_summary
+    -> BoSummary.get_summary
     -> BoUtils.get_formals
     -> Procname.t
     -> Tenv.t
@@ -332,7 +337,8 @@ let check_instrs :
     -> Dom.Mem.t AbstractInterpreter.State.t
     -> Checks.t
     -> Checks.t =
- fun get_checks_summary get_formals pname tenv integer_type_widths cfg node instrs state checks ->
+ fun get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg node instrs state
+     checks ->
   match state with
   | _ when Instrs.is_empty instrs ->
       checks
@@ -349,8 +355,8 @@ let check_instrs :
             checks
       in
       let cond_set =
-        check_instr get_checks_summary get_formals pname tenv integer_type_widths node instr pre
+        check_instr get_checks_summary get_summary get_formals pname tenv integer_type_widths node
-          checks.cond_set
+          instr pre checks.cond_set
       in
       print_debug_info instr pre cond_set ;
       {checks with cond_set}
@@ -358,6 +364,7 @@ let check_instrs :
 
 let check_node :
        get_checks_summary
+    -> BoSummary.get_summary
     -> BoUtils.get_formals
     -> Procname.t
     -> Tenv.t
@@ -367,12 +374,13 @@ let check_node :
     -> Checks.t
     -> CFG.Node.t
     -> Checks.t =
- fun get_checks_summary get_formals pname tenv integer_type_widths cfg inv_map checks node ->
+ fun get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg inv_map checks
+     node ->
   match BufferOverrunAnalysis.extract_state (CFG.Node.id node) inv_map with
   | Some state ->
       let instrs = CFG.instrs node in
-      check_instrs get_checks_summary get_formals pname tenv integer_type_widths cfg node instrs
+      check_instrs get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg
-        state checks
+        node instrs state checks
   | _ ->
       checks
 
@@ -381,6 +389,7 @@ type checks = Checks.t
 
 let compute_checks :
        get_checks_summary
+    -> BoSummary.get_summary
     -> BoUtils.get_formals
     -> Procname.t
     -> Tenv.t
@@ -388,9 +397,11 @@ let compute_checks :
     -> CFG.t
     -> BufferOverrunAnalysis.invariant_map
     -> checks =
- fun get_checks_summary get_formals pname tenv integer_type_widths cfg inv_map ->
+ fun get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg inv_map ->
   CFG.fold_nodes cfg
-    ~f:(check_node get_checks_summary get_formals pname tenv integer_type_widths cfg inv_map)
+    ~f:
+      (check_node get_checks_summary get_summary get_formals pname tenv integer_type_widths cfg
+         inv_map)
     ~init:Checks.empty
 
 
@@ -433,14 +444,24 @@ let checker ({InterproceduralAnalysis.proc_desc; tenv; exe_env; analyze_dependen
   AnalysisCallbacks.html_debug_new_node_session ~pp_name underlying_exit_node ~f:(fun () ->
       let cfg = CFG.from_pdesc proc_desc in
       let checks =
+        let open IOption.Let_syntax in
+        let get_summary_common callee_pname =
+          let+ _, summaries = analyze_dependency callee_pname in
+          summaries
+        in
         let get_checks_summary callee_pname =
-          analyze_dependency callee_pname
+          let* checker_summary, _analysis_summary = get_summary_common callee_pname in
-          |> Option.bind ~f:(fun (_, (checker_summary, _analysis_summary)) -> checker_summary)
+          checker_summary
+        in
+        let get_summary callee_pname =
+          let* _checker_summary, analysis_summary = get_summary_common callee_pname in
+          analysis_summary
         in
         let get_formals callee_pname =
-          AnalysisCallbacks.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals
+          AnalysisCallbacks.get_proc_desc callee_pname >>| Procdesc.get_pvar_formals
         in
-        compute_checks get_checks_summary get_formals proc_name tenv integer_type_widths cfg inv_map
+        compute_checks get_checks_summary get_summary get_formals proc_name tenv integer_type_widths
+          cfg inv_map
       in
       report_errors analysis_data checks ;
       Some (get_checks_summary checks) )

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -1056,28 +1056,31 @@ module Collection = struct
 end
 
 module JavaClass = struct
+  let decl_array {pname; node_hash; location} ~ret:(ret_id, _) length mem =
+    let loc =
+      Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None
+        ~represents_multiple_values:true
+      |> Loc.of_allocsite
+    in
+    let arr_v =
+      let allocsite =
+        Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
+          ~represents_multiple_values:true
+      in
+      let traces = Trace.(Set.singleton location ArrayDeclaration) in
+      Dom.Val.of_java_array_alloc allocsite ~length ~traces
+    in
+    Dom.Mem.add_heap loc arr_v mem |> model_by_value (Dom.Val.of_loc loc) ret_id
+
+
   let get_fields class_name_exp =
-    let exec {pname; node_hash; location; tenv} ~ret:(ret_id, _) mem =
+    let exec ({tenv} as model_env) ~ret mem =
       match class_name_exp with
       | Exp.Const (Const.Cclass name) -> (
           let typ_name = Typ.Name.Java.from_string (Ident.name_to_string name) in
           match Tenv.lookup tenv typ_name with
           | Some {fields} ->
-              let loc =
+              decl_array model_env ~ret (List.length fields |> Itv.of_int) mem
-                Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None
-                  ~represents_multiple_values:true
-                |> Loc.of_allocsite
-              in
-              let arr_v =
-                let allocsite =
-                  Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
-                    ~represents_multiple_values:true
-                in
-                let length = List.length fields |> Itv.of_int in
-                let traces = Trace.(Set.singleton location ArrayDeclaration) in
-                Dom.Val.of_java_array_alloc allocsite ~length ~traces
-              in
-              Dom.Mem.add_heap loc arr_v mem |> model_by_value (Dom.Val.of_loc loc) ret_id
           | None ->
               Logging.d_printfln_escaped "Could not find class from tenv" ;
               mem )
@@ -1086,6 +1089,36 @@ module JavaClass = struct
           mem
     in
     {exec; check= no_check}
+
+
+  let get_enum_constants class_name_exp =
+    let exec ({get_summary} as model_env) ~ret mem =
+      match class_name_exp with
+      | Exp.Const (Const.Cclass name) -> (
+          let enum_values_pname =
+            let class_name_str = Ident.name_to_string name in
+            Procname.make_java
+              ~class_name:(Typ.Name.Java.from_string class_name_str)
+              ~return_type:(Some (JavaSplitName.make (class_name_str ^ "[]")))
+              ~method_name:"values" ~parameters:[] ~kind:Procname.Java.Static ()
+          in
+          match get_summary enum_values_pname with
+          | Some enum_values_mem ->
+              let length =
+                let ret_loc = Loc.of_pvar (Pvar.get_ret_pvar enum_values_pname) in
+                let ret_v = Dom.Mem.find ret_loc enum_values_mem in
+                Dom.Mem.find_set (Dom.Val.get_all_locs ret_v) enum_values_mem
+                |> Dom.Val.array_sizeof
+              in
+              decl_array model_env ~ret length mem
+          | None ->
+              Logging.d_printfln_escaped "Summary of Enum.values not found" ;
+              mem )
+      | _ ->
+          Logging.d_printfln_escaped "Parameter is not a class name constant" ;
+          mem
+    in
+    {exec; check= no_check}
 end
 
 module JavaString = struct
@@ -1563,6 +1596,8 @@ module Call = struct
         &:: "substring" <>$ any_arg $+ capt_exp $+ capt_exp $--> JavaString.substring
       ; +PatternMatch.implements_lang "Class"
         &:: "getCanonicalName" &::.*--> JavaString.inferbo_constant_string
+      ; +PatternMatch.implements_lang "Class"
+        &:: "getEnumConstants" <>$ capt_exp $--> JavaClass.get_enum_constants
       ; +PatternMatch.implements_lang "Class" &:: "getFields" <>$ capt_exp $--> JavaClass.get_fields
       ; +PatternMatch.implements_lang "Enum" &:: "name" &::.*--> JavaString.inferbo_constant_string
       ; +PatternMatch.implements_lang "Integer"

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -8,6 +8,7 @@
 open! IStd
 open AbsLoc
 open! AbstractDomain.Types
+module BoSummary = BufferOverrunAnalysisSummary
 module L = Logging
 module Dom = BufferOverrunDomain
 module PO = BufferOverrunProofObligations
@@ -22,10 +23,11 @@ module ModelEnv = struct
     ; node_hash: int
     ; location: Location.t
     ; tenv: Tenv.t
-    ; integer_type_widths: Typ.IntegerWidths.t }
+    ; integer_type_widths: Typ.IntegerWidths.t
+    ; get_summary: BoSummary.get_summary }
 
-  let mk_model_env pname ~node_hash location tenv integer_type_widths =
+  let mk_model_env pname ~node_hash location tenv integer_type_widths get_summary =
-    {pname; node_hash; location; tenv; integer_type_widths}
+    {pname; node_hash; location; tenv; integer_type_widths; get_summary}
 end
 
 module Exec = struct

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -16,10 +16,17 @@ module ModelEnv : sig
     ; node_hash: int
     ; location: Location.t
     ; tenv: Tenv.t
-    ; integer_type_widths: Typ.IntegerWidths.t }
+    ; integer_type_widths: Typ.IntegerWidths.t
+    ; get_summary: BufferOverrunAnalysisSummary.get_summary }
 
   val mk_model_env :
-    Procname.t -> node_hash:int -> Location.t -> Tenv.t -> Typ.IntegerWidths.t -> model_env
+       Procname.t
+    -> node_hash:int
+    -> Location.t
+    -> Tenv.t
+    -> Typ.IntegerWidths.t
+    -> BufferOverrunAnalysisSummary.get_summary
+    -> model_env
 end
 
 module Exec : sig

infer/src/cost/cost.ml

@@ -18,6 +18,7 @@ module Node = ProcCfg.DefaultNode
 type extras_WorstCaseCost =
   { inferbo_invariant_map: BufferOverrunAnalysis.invariant_map
   ; integer_type_widths: Typ.IntegerWidths.t
+  ; inferbo_get_summary: BufferOverrunAnalysisSummary.get_summary
   ; get_node_nb_exec: Node.id -> BasicCost.t
   ; get_summary: Procname.t -> CostDomain.summary option
   ; get_formals: Procname.t -> (Pvar.t * Typ.t) list option }
@@ -53,7 +54,13 @@ module InstrBasicCost = struct
     match instr with
     | Sil.Call (ret, Exp.Const (Const.Cfun callee_pname), params, _, _) when Config.inclusive_cost
       ->
-        let {inferbo_invariant_map; integer_type_widths; get_summary; get_formals} = extras in
+        let { inferbo_invariant_map
+            ; integer_type_widths
+            ; inferbo_get_summary
+            ; get_summary
+            ; get_formals } =
+          extras
+        in
         let operation_cost =
           match
             BufferOverrunAnalysis.extract_pre (InstrCFG.Node.id instr_node) inferbo_invariant_map
@@ -71,7 +78,7 @@ module InstrBasicCost = struct
                   let node_hash = InstrCFG.Node.hash instr_node in
                   let model_env =
                     BufferOverrunUtils.ModelEnv.mk_model_env callee_pname ~node_hash loc tenv
-                      integer_type_widths
+                      integer_type_widths inferbo_get_summary
                   in
                   CostDomain.of_operation_cost (model model_env ~ret inferbo_mem)
               | None -> (
@@ -326,9 +333,14 @@ let compute_get_node_nb_exec node_cfg bound_map : get_node_nb_exec =
 
 
 let compute_worst_case_cost tenv integer_type_widths get_summary get_formals instr_cfg_wto
-    inferbo_invariant_map get_node_nb_exec =
+    inferbo_invariant_map inferbo_get_summary get_node_nb_exec =
   let extras =
-    {inferbo_invariant_map; integer_type_widths; get_node_nb_exec; get_summary; get_formals}
+    { inferbo_invariant_map
+    ; integer_type_widths
+    ; inferbo_get_summary
+    ; get_node_nb_exec
+    ; get_summary
+    ; get_formals }
   in
   WorstCaseCost.compute tenv extras instr_cfg_wto
 
@@ -367,20 +379,26 @@ let checker ({InterproceduralAnalysis.proc_desc; exe_env; analyze_dependency} as
   let is_on_ui_thread = ConcurrencyModels.runs_on_ui_thread tenv proc_name in
   let get_node_nb_exec = compute_get_node_nb_exec node_cfg bound_map in
   let astate =
+    let open IOption.Let_syntax in
+    let get_summary_common callee_pname =
+      let+ _, summaries = analyze_dependency callee_pname in
+      summaries
+    in
     let get_summary callee_pname =
-      match analyze_dependency callee_pname with
+      let* cost_summary, _inferbo_summary, _ = get_summary_common callee_pname in
-      | Some (_, (payload, _, _)) ->
+      cost_summary
-          payload
+    in
-      | None ->
+    let inferbo_get_summary callee_pname =
-          None
+      let* _cost_summary, inferbo_summary, _ = get_summary_common callee_pname in
+      inferbo_summary
     in
     let get_formals callee_pname =
-      AnalysisCallbacks.get_proc_desc callee_pname |> Option.map ~f:Procdesc.get_pvar_formals
+      AnalysisCallbacks.get_proc_desc callee_pname >>| Procdesc.get_pvar_formals
     in
     let instr_cfg = InstrCFG.from_pdesc proc_desc in
     let instr_cfg_wto = InstrCFG.wto instr_cfg in
     compute_worst_case_cost tenv integer_type_widths get_summary get_formals instr_cfg_wto
-      inferbo_invariant_map get_node_nb_exec
+      inferbo_invariant_map inferbo_get_summary get_node_nb_exec
   in
   let () =
     let exit_cost_record = astate.WorstCaseCost.costs in

infer/src/cost/hoisting.ml

@@ -100,7 +100,7 @@ let do_report extract_cost_if_expensive proc_desc err_log (Call.{pname; loc} as
 
 
 let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_formals
-    inferbo_invariant_map Call.{pname; node; ret; params} =
+    inferbo_invariant_map inferbo_get_summary Call.{pname; node; ret; params} =
   let last_node = InstrCFG.last_of_underlying_node node in
   let inferbo_mem =
     let instr_node_id = InstrCFG.Node.id last_node in
@@ -126,7 +126,7 @@ let get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_f
                let model_env =
                  let node_hash = InstrCFG.Node.hash last_node in
                  BufferOverrunUtils.ModelEnv.mk_model_env pname ~node_hash loc tenv
-                   integer_type_widths
+                   integer_type_widths inferbo_get_summary
                in
                model model_env ~ret inferbo_mem )
   in
@@ -169,16 +169,22 @@ let checker
         BufferOverrunAnalysis.cached_compute_invariant_map
           (InterproceduralAnalysis.bind_payload ~f:fst3 analysis_data)
       in
+      let open IOption.Let_syntax in
       let get_callee_cost_summary_and_formals callee_pname =
-        analyze_dependency callee_pname
+        let* callee_pdesc, (_inferbo, _purity, callee_costs_summary) =
-        |> Option.bind ~f:(function
+          analyze_dependency callee_pname
-             | callee_pdesc, (_inferbo, _purity, Some callee_costs_summary) ->
+        in
-                 Some (callee_costs_summary, Procdesc.get_pvar_formals callee_pdesc)
+        let+ callee_costs_summary = callee_costs_summary in
-             | _, (_, _, None) ->
+        (callee_costs_summary, Procdesc.get_pvar_formals callee_pdesc)
-                 None )
+      in
+      let inferbo_get_summary callee_pname =
+        let* _callee_pdesc, (inferbo, _purity, _callee_costs_summary) =
+          analyze_dependency callee_pname
+        in
+        inferbo
       in
       get_cost_if_expensive tenv integer_type_widths get_callee_cost_summary_and_formals
-        inferbo_invariant_map
+        inferbo_invariant_map inferbo_get_summary
     else fun _ -> None
   in
   let get_callee_purity callee_pname =

infer/tests/codetoanalyze/java/performance/EnumTest.java

@@ -14,4 +14,8 @@ class EnumTest {
   void enum_name_constant(MyEnum e) {
     for (int i = 0; i < e.name().length(); i++) {}
   }
+
+  void iterate_enum_constants() {
+    for (Object obj : MyEnum.class.getEnumConstants()) {}
+  }
 }

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

@@ -162,6 +162,7 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan
 codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 549,  OnUIThread:false
 codetoanalyze/java/performance/EnumTest.java, EnumTest.<init>(), 3,  OnUIThread:false
 codetoanalyze/java/performance/EnumTest.java, EnumTest.enum_name_constant(MyEnum):void, 198,  OnUIThread:false
+codetoanalyze/java/performance/EnumTest.java, EnumTest.iterate_enum_constants():void, 31,  OnUIThread:false
 codetoanalyze/java/performance/EnumTest.java, MyEnum.<clinit>():void, 29,  OnUIThread:false
 codetoanalyze/java/performance/EnumTest.java, MyEnum.<init>(java.lang.String,int), 5,  OnUIThread:false
 codetoanalyze/java/performance/EnumTest.java, MyEnum.valueOf(java.lang.String):MyEnum, 7,  OnUIThread:false