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()) {} + } }