From 7a0be265969286ea66a687335a0c554e4a6d9b48 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 26 Feb 2020 01:59:29 -0800 Subject: [PATCH] [inferbo] Revise semantics of `values` function of Java enum class Summary: The semantics of the `values` function of Java enum class was missing, when it is called outside the class initializer. This diff gets the size of the enum elements from the summary of class initializer function, ``. Reviewed By: ezgicicek Differential Revision: D20094880 fbshipit-source-id: 7362bba1c --- .../bufferoverrun/bufferOverrunAnalysis.ml | 112 ++++++++++-------- infer/src/istd/IOption.ml | 2 + infer/src/istd/IOption.mli | 3 + .../java/bufferoverrun/issues.exp | 3 +- .../java/performance/IteratorTest.java | 4 + 5 files changed, 75 insertions(+), 49 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 892da89d6..350f33def 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -175,29 +175,43 @@ module TransferFunctions = struct false - let is_java_enum_values ~caller_pname ~callee_pname = - match - (Procname.get_class_type_name caller_pname, Procname.get_class_type_name callee_pname) - with - | Some caller_class_name, Some callee_class_name - when Typ.equal_name caller_class_name callee_class_name -> - Procname.is_java_class_initializer caller_pname - && String.equal (Procname.get_method callee_pname) "values" - | _, _ -> - false - - - let assign_java_enum_values id callee_pname mem = - match Procname.get_class_type_name callee_pname with + let is_java_enum_values tenv callee_pname = + Option.exists (Procname.get_class_type_name callee_pname) ~f:(fun callee_class_name -> + PatternMatch.is_java_enum tenv callee_class_name + && String.equal (Procname.get_method callee_pname) "values" ) + + + let assign_java_enum_values get_summary id ~caller_pname ~callee_pname mem = + let caller_class_name = Procname.get_class_type_name caller_pname in + let callee_class_name = Procname.get_class_type_name callee_pname in + let is_caller_class_initializer = + IOption.exists2 caller_class_name callee_class_name + ~f:(fun caller_class_name callee_class_name -> + Procname.is_java_class_initializer caller_pname + && Typ.equal_name caller_class_name callee_class_name ) + in + match callee_class_name with | Some (JavaClass class_name as typename) -> - let class_var = - Loc.of_var - (Var.of_pvar - (Pvar.mk_global (Mangled.from_string (JavaClassName.to_string class_name)))) + let clinit_mem = + if is_caller_class_initializer then Some (Dom.Mem.unset_oenv mem) + else get_summary (Procname.Java (Procname.Java.get_class_initializer typename)) in - let fn = Fieldname.make typename "$VALUES" in - let v = Dom.Mem.find (Loc.append_field class_var ~fn) mem in - Dom.Mem.add_stack (Loc.of_id id) v mem + Option.value_map clinit_mem ~default:mem ~f:(fun clinit_mem -> + let loc = + let class_var = + let class_mangled = Mangled.from_string (JavaClassName.to_string class_name) in + Loc.of_var (Var.of_pvar (Pvar.mk_global class_mangled)) + in + let fn = Fieldname.make typename "$VALUES" in + Loc.append_field class_var ~fn + in + let v = Dom.Mem.find loc clinit_mem in + let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in + if is_caller_class_initializer then mem + else + let arr_locs = Dom.Val.get_all_locs v in + let arr_v = Dom.Mem.find_set arr_locs clinit_mem in + Dom.Mem.add_heap_set arr_locs arr_v mem ) | _ -> assert false @@ -359,35 +373,37 @@ module TransferFunctions = struct mem | Prune (exp, _, _, _) -> Sem.Prune.prune integer_type_widths exp mem + | Call ((id, _), Const (Cfun callee_pname), _, _, _) when is_java_enum_values tenv callee_pname + -> + let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in + assign_java_enum_values get_summary id ~caller_pname:(Summary.get_proc_name summary) + ~callee_pname mem | Call (((id, _) as ret), Const (Cfun callee_pname), params, location, _) -> ( let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in - if is_java_enum_values ~caller_pname:(Summary.get_proc_name summary) ~callee_pname then - assign_java_enum_values id callee_pname mem - else - let fun_arg_list = - List.map params ~f:(fun (exp, typ) -> - ProcnameDispatcher.Call.FuncArg.{exp; typ; arg_payload= ()} ) - in - match Models.Call.dispatch tenv callee_pname fun_arg_list with - | Some {Models.exec} -> - 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 - in - exec model_env ~ret mem - | None -> ( - let {BoUtils.ReplaceCallee.pname= callee_pname; params; is_params_ref} = - BoUtils.ReplaceCallee.replace_make_shared tenv get_formals callee_pname params - in - match (get_summary callee_pname, get_formals callee_pname) with - | Some callee_exit_mem, Some callee_formals -> - instantiate_mem ~is_params_ref integer_type_widths ret callee_formals callee_pname - params mem callee_exit_mem location - | _, _ -> - (* This may happen for procedures with a biabduction model too. *) - L.d_printfln_escaped "/!\\ Unknown call to %a" Procname.pp callee_pname ; - Dom.Mem.add_unknown_from ret ~callee_pname ~location mem ) ) + let fun_arg_list = + List.map params ~f:(fun (exp, typ) -> + ProcnameDispatcher.Call.FuncArg.{exp; typ; arg_payload= ()} ) + in + match Models.Call.dispatch tenv callee_pname fun_arg_list with + | Some {Models.exec} -> + 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 + in + exec model_env ~ret mem + | None -> ( + let {BoUtils.ReplaceCallee.pname= callee_pname; params; is_params_ref} = + BoUtils.ReplaceCallee.replace_make_shared tenv get_formals callee_pname params + in + match (get_summary callee_pname, get_formals callee_pname) with + | Some callee_exit_mem, Some callee_formals -> + instantiate_mem ~is_params_ref integer_type_widths ret callee_formals callee_pname + params mem callee_exit_mem location + | _, _ -> + (* This may happen for procedures with a biabduction model too. *) + L.d_printfln_escaped "/!\\ Unknown call to %a" Procname.pp callee_pname ; + Dom.Mem.add_unknown_from ret ~callee_pname ~location mem ) ) | Call (((id, _) as ret), fun_exp, _, location, _) -> let mem = Dom.Mem.add_stack_loc (Loc.of_id id) mem in L.d_printfln_escaped "/!\\ Call to non-const function %a" Exp.pp fun_exp ; diff --git a/infer/src/istd/IOption.ml b/infer/src/istd/IOption.ml index 8c6981f38..1257821e3 100644 --- a/infer/src/istd/IOption.ml +++ b/infer/src/istd/IOption.ml @@ -15,6 +15,8 @@ let if_none_evalopt ~f x = match x with None -> f () | Some _ -> x let if_none_eval = value_default_f +let exists2 x y ~f = match (x, y) with Some x, Some y -> f x y | _, _ -> false + module Let_syntax = struct include Option.Let_syntax diff --git a/infer/src/istd/IOption.mli b/infer/src/istd/IOption.mli index c5eccf325..4f36f7126 100644 --- a/infer/src/istd/IOption.mli +++ b/infer/src/istd/IOption.mli @@ -22,6 +22,9 @@ val if_none_eval : f:(unit -> 'a) -> 'a option -> 'a built with [if_none_evalopt]. This is exactly the same as [value_default_f] but with a better name. *) +val exists2 : 'a option -> 'b option -> f:('a -> 'b -> bool) -> bool +(** Like [Option.exists] but gets two parameters. *) + include sig [@@@warning "-32-60"] diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index df3c97f86..110b53f3d 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -1,4 +1,5 @@ -codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.array_length_Bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.array_length_Bad():void, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.array_length_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.call_iterate_collection_Bad():void, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Through,Through,Through,Through,Through,Call,,Array declaration,Array access: Offset: 5 Size: 5 by call to `void Array.iterate_collection_Bad(ArrayList)` ] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.negative_alloc_Bad():void, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1] diff --git a/infer/tests/codetoanalyze/java/performance/IteratorTest.java b/infer/tests/codetoanalyze/java/performance/IteratorTest.java index 13a86a0e3..b05fdeff4 100644 --- a/infer/tests/codetoanalyze/java/performance/IteratorTest.java +++ b/infer/tests/codetoanalyze/java/performance/IteratorTest.java @@ -28,4 +28,8 @@ public class IteratorTest { for (Color c : Color.values()) {} } } + + public void enum_iter() { + for (Color c : Color.values()) {} + } }