diff --git a/infer/src/IR/Annot.ml b/infer/src/IR/Annot.ml index 3570dae9d..b3d152a1d 100644 --- a/infer/src/IR/Annot.ml +++ b/infer/src/IR/Annot.ml @@ -21,10 +21,14 @@ type t = ; parameters: parameters (** currently only one string parameter *) } [@@deriving compare] +let equal = [%compare.equal: t] + let volatile = {class_name= "volatile"; parameters= []} let final = {class_name= "final"; parameters= []} +let is_final x = equal final x + (** Pretty print an annotation. *) let prefix = match Language.curr_language_is Java with true -> "@" | false -> "_" @@ -63,6 +67,8 @@ module Item = struct (** Check if the item annotation is empty. *) let is_empty ia = List.is_empty ia + + let is_final ia = List.exists ia ~f:(fun (x, b) -> b && is_final x) end module Class = struct diff --git a/infer/src/IR/Annot.mli b/infer/src/IR/Annot.mli index 0b29e3ee6..c9252eed1 100644 --- a/infer/src/IR/Annot.mli +++ b/infer/src/IR/Annot.mli @@ -39,6 +39,9 @@ module Item : sig val empty : t (** Empty item annotation. *) + + val is_final : t -> bool + (** Check if final annotation is included in. *) end module Class : sig diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml index e0d901344..7ff037372 100644 --- a/infer/src/IR/Exp.ml +++ b/infer/src/IR/Exp.ml @@ -361,3 +361,21 @@ let rec ignore_cast e = match e with Cast (_, e) -> ignore_cast e | _ -> e let rec ignore_integer_cast e = match e with Cast (t, e) when Typ.is_int t -> ignore_integer_cast e | _ -> e + + +let rec get_java_class_initializer tenv = function + | Lfield (Lvar pvar, fn, typ) when Pvar.is_global pvar -> ( + match Typ.Struct.get_field_type_and_annotation ~lookup:(Tenv.lookup tenv) fn typ with + | Some (field_typ, annot) when Annot.Item.is_final annot -> + let java_class = Typ.JavaClass (Pvar.get_name pvar) in + Some + ( Typ.Procname.Java (Typ.Procname.Java.get_class_initializer java_class) + , pvar + , fn + , field_typ ) + | _ -> + None ) + | Cast (_, e) | Lfield (e, _, _) -> + get_java_class_initializer tenv e + | Lvar _ | Var _ | UnOp _ | BinOp _ | Exn _ | Closure _ | Const _ | Lindex _ | Sizeof _ -> + None diff --git a/infer/src/IR/Exp.mli b/infer/src/IR/Exp.mli index 37b2a81e4..2d3c0cde6 100644 --- a/infer/src/IR/Exp.mli +++ b/infer/src/IR/Exp.mli @@ -155,3 +155,7 @@ val zero_of_type_exn : Typ.t -> t val ignore_cast : t -> t val ignore_integer_cast : t -> t + +val get_java_class_initializer : + Tenv.t -> t -> (Typ.Procname.t * Pvar.t * Typ.Fieldname.t * Typ.t) option +(** Returns the class initializer of the given expression in Java *) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 134d8a548..97a50cea4 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -1220,6 +1220,9 @@ module BoundTrace = struct | ModeledFunction {pname; location} -> let desc = F.asprintf "Modeled call to %s" pname in [Errlog.make_trace_element depth location desc []] + + + let of_loop location = Loop location end (** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *) @@ -1262,6 +1265,8 @@ module NonNegativeBound = struct else (b, BoundTrace.ModeledFunction {pname; location}) + let of_big_int ~trace c = (Bound.of_big_int c, trace) + let int_lb (b, _) = Bound.big_int_lb b |> Option.bind ~f:NonNegativeInt.of_big_int diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index c7f7669b0..62446edb6 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -131,6 +131,8 @@ module BoundTrace : sig val length : t -> int val make_err_trace : depth:int -> t -> Errlog.loc_trace + + val of_loop : Location.t -> t end type ('c, 's, 't) valclass = Constant of 'c | Symbolic of 's | ValTop of 't @@ -148,6 +150,8 @@ module NonNegativeBound : sig val of_modeled_function : string -> Location.t -> Bound.t -> t + val of_big_int : trace:BoundTrace.t -> Z.t -> t + val pp : hum:bool -> Format.formatter -> t -> unit val make_err_trace : t -> string * Errlog.loc_trace diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index cdd137e8a..bb33054e2 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -220,6 +220,51 @@ module TransferFunctions = struct assert false + let join_java_static_final = + let known_java_static_fields = String.Set.of_list [".EMPTY"] in + let is_known_java_static_field fn = + let fieldname = Typ.Fieldname.to_string fn in + String.Set.exists known_java_static_fields ~f:(fun suffix -> + String.is_suffix fieldname ~suffix ) + in + let copy_reachable_locs_from loc ~from_mem ~to_mem = + let copy loc acc = + Option.value_map (Dom.Mem.find_opt loc from_mem) ~default:acc ~f:(fun v -> + Dom.Mem.add_heap loc v acc ) + in + let reachable_locs = Dom.Mem.get_reachable_locs_from [] (PowLoc.singleton loc) from_mem in + PowLoc.fold copy reachable_locs to_mem + in + fun tenv get_proc_summary_and_formals exp mem -> + Option.value_map (Exp.get_java_class_initializer tenv exp) ~default:mem + ~f:(fun (clinit_pname, pvar, fn, field_typ) -> + match field_typ.Typ.desc with + | Typ.Tptr ({desc= Tstruct _}, _) -> + (* It copies all of the reachable values when the contents of the field are commonly + used as immutable, e.g., values of enum. Otherwise, it copies only the size of + static final array. *) + Option.value_map (get_proc_summary_and_formals clinit_pname) ~default:mem + ~f:(fun (clinit_mem, _) -> + let field_loc = Loc.append_field ~typ:field_typ (Loc.of_pvar pvar) ~fn in + if is_known_java_static_field fn then + copy_reachable_locs_from field_loc ~from_mem:clinit_mem ~to_mem:mem + else mem ) + | _ -> + mem ) + + + let modeled_range_of_exp location exp mem = + match exp with + | Exp.Lindex (arr_exp, _) -> + let length = + Sem.eval_array_locs_length (Sem.eval_locs arr_exp mem) mem |> Dom.Val.get_itv + in + Option.map (Itv.is_const length) + ~f:(Dom.ModeledRange.of_big_int ~trace:(Bounds.BoundTrace.of_loop location)) + | _ -> + None + + let exec_instr : Dom.Mem.t -> extras ProcData.t -> CFG.Node.t -> Sil.instr -> Dom.Mem.t = fun mem {summary; tenv; extras= {get_proc_summary_and_formals; oenv= {integer_type_widths}}} node instr -> @@ -242,9 +287,16 @@ module TransferFunctions = struct L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a" (Pvar.pp Pp.text) pvar ; Dom.Mem.add_unknown id ~location mem ) - | Load {id; e= exp; typ} -> + | Load {id; e= exp; typ; loc= location} -> + let mem = + if Language.curr_language_is Java then + join_java_static_final tenv get_proc_summary_and_formals exp mem + else mem + in let represents_multiple_values = is_array_access_exp exp in - BoUtils.Exec.load_locs ~represents_multiple_values id typ (Sem.eval_locs exp mem) mem + let modeled_range = modeled_range_of_exp location exp mem in + BoUtils.Exec.load_locs ~represents_multiple_values ~modeled_range id typ + (Sem.eval_locs exp mem) mem | Store {e2= Exn _} when Language.curr_language_is Java -> Dom.Mem.exc_raised | Store {e1= tgt_exp; e2= Const (Const.Cstr _) as src; loc= location} diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 1306c4a11..3fade8b6d 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -82,6 +82,9 @@ module ModeledRange = struct let of_modeled_function pname location bound = let pname = Typ.Procname.to_simplified_string pname in NonBottom (Bounds.NonNegativeBound.of_modeled_function pname location bound) + + + let of_big_int ~trace z = NonBottom (Bounds.NonNegativeBound.of_big_int ~trace z) end module Val = struct diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index 418aac905..895bcc24f 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -32,8 +32,12 @@ end module Exec = struct open ModelEnv - let load_locs ~represents_multiple_values id typ locs mem = - let v = Dom.Mem.find_set ~typ locs mem in + let load_locs ~represents_multiple_values ~modeled_range id typ locs mem = + let set_modeled_range v = + Option.value_map modeled_range ~default:v ~f:(fun modeled_range -> + Dom.Val.set_modeled_range modeled_range v ) + in + let v = Dom.Mem.find_set ~typ locs mem |> set_modeled_range in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in let mem = if represents_multiple_values then Dom.Mem.add_heap_set ~represents_multiple_values locs v mem diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 6c4caff76..becf079e7 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -25,7 +25,13 @@ end module Exec : sig val load_locs : - represents_multiple_values:bool -> Ident.t -> Typ.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t + represents_multiple_values:bool + -> modeled_range:Dom.ModeledRange.t option + -> Ident.t + -> Typ.t + -> PowLoc.t + -> Dom.Mem.t + -> Dom.Mem.t val decl_local : ModelEnv.model_env -> Dom.Mem.t * int -> Loc.t * Typ.t -> Dom.Mem.t * int diff --git a/infer/tests/build_systems/incremental_analysis_cost_change/reverse_analysis_callgraph.dot b/infer/tests/build_systems/incremental_analysis_cost_change/reverse_analysis_callgraph.dot index 9f6ca4302..4b60ff8cc 100644 --- a/infer/tests/build_systems/incremental_analysis_cost_change/reverse_analysis_callgraph.dot +++ b/infer/tests/build_systems/incremental_analysis_cost_change/reverse_analysis_callgraph.dot @@ -20,7 +20,10 @@ digraph callgraph { N2 -> N4 ; N2 -> N3 ; - N8 [ label = "void PrintStream.println(String)", flag = false ]; + N9 [ label = "void PrintStream.println(String)", flag = false ]; + N9 -> N2 ; + + N8 [ label = "void System.()", flag = false ]; N8 -> N2 ; N3 [ label = "void Test.complexityDecrease(int)", flag = true ];