diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 3b3168f1d..2f51391c6 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -218,6 +218,15 @@ module Loc = struct None + let rec is_global = function + | Var (Var.ProgramVar pvar) -> + Pvar.is_global pvar + | Var (Var.LogicalVar _) | Allocsite _ -> + false + | Field (loc, _) -> + is_global loc + + let rec get_path = function | Var (LogicalVar _) -> None diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index cf4352d0a..430566b74 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -163,8 +163,8 @@ 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, exp, _, _) -> - BoUtils.Exec.load_locs id (Sem.eval_locs exp mem) mem + | Load (id, exp, typ, _) -> + BoUtils.Exec.load_locs id typ (Sem.eval_locs exp mem) mem | Store (exp1, _, Const (Const.Cstr s), location) -> let locs = Sem.eval_locs exp1 mem in let model_env = diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 9c4fe0f84..d2175cc4f 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -443,6 +443,10 @@ module Val = struct let is_mone x = Itv.is_mone (get_itv x) let of_path tenv ~may_last_field integer_type_widths location typ path = + let traces_of_loc l = + let trace = if Loc.is_global l then Trace.Global l else Trace.Parameter l in + TraceSet.singleton location trace + in let is_java = Language.curr_language_is Java in L.d_printfln_escaped "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ (if may_last_field then ", may_last_field" else "") @@ -450,7 +454,7 @@ module Val = struct match typ.Typ.desc with | Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ -> let l = Loc.of_path path in - let traces = TraceSet.singleton location (Trace.Parameter l) in + let traces = traces_of_loc l in let unsigned = Typ.is_unsigned_int typ in of_itv ~traces (Itv.of_normal_path ~unsigned path) | Tptr (elt, _) -> @@ -460,13 +464,13 @@ module Val = struct in let deref_path = SPath.deref ~deref_kind path in let l = Loc.of_path deref_path in - let traces = TraceSet.singleton location (Trace.Parameter l) in + let traces = traces_of_loc l in {bot with powloc= PowLoc.singleton l; traces} else let deref_kind = SPath.Deref_CPointer in let deref_path = SPath.deref ~deref_kind path in let l = Loc.of_path deref_path in - let traces = TraceSet.singleton location (Trace.Parameter l) in + let traces = traces_of_loc l in let arrayblk = let allocsite = Allocsite.make_symbol deref_path in let stride = @@ -486,7 +490,7 @@ module Val = struct | Some (CArray {deref_kind; length}) -> let deref_path = SPath.deref ~deref_kind path in let l = Loc.of_path deref_path in - let traces = TraceSet.singleton location (Trace.Parameter l) in + let traces = traces_of_loc l in let allocsite = Allocsite.make_symbol deref_path in let offset = Itv.zero in let size = Itv.of_int_lit length in @@ -494,18 +498,18 @@ module Val = struct | Some JavaCollection -> let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in let l = Loc.of_path deref_path in - let traces = TraceSet.singleton location (Trace.Parameter l) in + let traces = traces_of_loc l in let allocsite = Allocsite.make_symbol deref_path in let length = Itv.of_length_path path in of_java_array_alloc allocsite ~length ~traces | None -> let l = Loc.of_path path in - let traces = TraceSet.singleton location (Trace.Parameter l) in + let traces = traces_of_loc l in of_loc ~traces l ) | Tarray {length; stride} -> let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in let l = Loc.of_path deref_path in - let traces = TraceSet.singleton location (Trace.Parameter l) in + let traces = traces_of_loc l in let allocsite = Allocsite.make_symbol deref_path in let size = match length with @@ -525,8 +529,14 @@ module Val = struct of_c_array_alloc allocsite ~stride ~offset ~size ~traces - let on_demand : default:t -> OndemandEnv.t -> Loc.t -> t = - fun ~default {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} l -> + let on_demand : default:t -> ?typ:Typ.t -> OndemandEnv.t -> Loc.t -> t = + fun ~default ?typ {tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths} + l -> + let do_on_demand path typ = + let may_last_field = may_last_field path in + let path = OndemandEnv.canonical_path typ_of_param_path path in + of_path tenv ~may_last_field integer_type_widths entry_location typ path + in match Loc.is_literal_string l with | Some s -> deref_of_literal_string s @@ -541,14 +551,17 @@ module Val = struct default | Some path -> ( match typ_of_param_path path with - | None -> - L.d_printfln_escaped "Val.on_demand for %a -> no type" Loc.pp l ; - default + | None -> ( + match typ with + | Some typ when Loc.is_global l -> + L.d_printfln_escaped "Val.on_demand for %a -> global" Loc.pp l ; + do_on_demand path typ + | _ -> + L.d_printfln_escaped "Val.on_demand for %a -> no type" Loc.pp l ; + default ) | Some typ -> L.d_printfln_escaped "Val.on_demand for %a" Loc.pp l ; - let may_last_field = may_last_field path in - let path = OndemandEnv.canonical_path typ_of_param_path path in - of_path tenv ~may_last_field integer_type_widths entry_location typ path ) ) ) + do_on_demand path typ ) ) ) module Itv = struct @@ -1174,21 +1187,23 @@ module MemReach = struct let find_stack : Loc.t -> _ t0 -> Val.t = fun l m -> Option.value (find_opt l m) ~default:Val.bot - let find_heap_default : default:Val.t -> Loc.t -> _ t0 -> Val.t = - fun ~default l m -> + let find_heap_default : default:Val.t -> ?typ:Typ.t -> Loc.t -> _ t0 -> Val.t = + fun ~default ?typ l m -> IOption.value_default_f (find_opt l m) ~f:(fun () -> - GOption.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default oenv l) ) + GOption.value_map m.oenv ~default ~f:(fun oenv -> Val.on_demand ~default ?typ oenv l) ) + + let find_heap : ?typ:Typ.t -> Loc.t -> _ t0 -> Val.t = + fun ?typ l m -> find_heap_default ~default:Val.Itv.top ?typ l m - let find_heap : Loc.t -> _ t0 -> Val.t = fun l m -> find_heap_default ~default:Val.Itv.top l m - let find : Loc.t -> _ t0 -> Val.t = - fun l m -> if is_stack_loc l m then find_stack l m else find_heap l m + let find : ?typ:Typ.t -> Loc.t -> _ t0 -> Val.t = + fun ?typ l m -> if is_stack_loc l m then find_stack l m else find_heap ?typ l m - let find_set : PowLoc.t -> _ t0 -> Val.t = - fun locs m -> - let find_join loc acc = Val.join acc (find loc m) in + let find_set : ?typ:Typ.t -> PowLoc.t -> _ t0 -> Val.t = + fun ?typ locs m -> + let find_join loc acc = Val.join acc (find ?typ loc m) in PowLoc.fold find_join locs Val.bot @@ -1267,7 +1282,7 @@ module MemReach = struct let transform_mem1 l m = let add, find = if is_stack_loc l m then (replace_stack, find_stack) - else (add_heap, find_heap_default ~default:Val.bot) + else (add_heap, find_heap_default ~default:Val.bot ?typ:None) in add l (f l (find l m)) m in @@ -1446,8 +1461,8 @@ module Mem = struct fun k -> f_lift_default ~default:Val.bot (MemReach.find_stack k) - let find_set : PowLoc.t -> _ t0 -> Val.t = - fun k -> f_lift_default ~default:Val.bot (MemReach.find_set k) + let find_set : ?typ:Typ.t -> PowLoc.t -> _ t0 -> Val.t = + fun ?typ k -> f_lift_default ~default:Val.bot (MemReach.find_set ?typ k) let find_opt : Loc.t -> _ t0 -> Val.t option = diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index e0cc82864..c4d5b2132 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -17,6 +17,7 @@ module BoTrace = struct type elem = | ArrayDeclaration | Assign of PowLoc.t + | Global of Loc.t | Parameter of Loc.t | Through of {risky_fun: lib_fun option} [@@deriving compare] @@ -78,6 +79,8 @@ module BoTrace = struct F.pp_print_string f "ArrayDeclaration" | Assign locs -> F.fprintf f "Assign `%a`" PowLoc.pp locs + | Global loc -> + F.fprintf f "Global `%a`" Loc.pp loc | Parameter loc -> F.fprintf f "Parameter `%a`" Loc.pp loc | Through {risky_fun} -> @@ -112,7 +115,7 @@ module BoTrace = struct let has_unknown = final_exists ~f:(function UnknownFrom _ -> true) let elem_has_risky = function - | ArrayDeclaration | Assign _ | Parameter _ -> + | ArrayDeclaration | Assign _ | Global _ | Parameter _ -> false | Through {risky_fun} -> Option.is_some risky_fun @@ -156,6 +159,8 @@ module BoTrace = struct "Array declaration" | Assign _ -> "Assignment" + | Global loc -> + if Loc.is_pretty loc then F.asprintf "Global `%a`" Loc.pp loc else "" | Parameter loc -> if Loc.is_pretty loc then F.asprintf "Parameter `%a`" Loc.pp loc else "" | Through {risky_fun} -> ( diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index b54b9e9b1..62fcfec67 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -32,8 +32,8 @@ end module Exec = struct open ModelEnv - let load_locs id locs mem = - let v = Dom.Mem.find_set locs mem in + let load_locs id typ locs mem = + let v = Dom.Mem.find_set ~typ locs mem in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in if not v.represents_multiple_values then match PowLoc.is_singleton_or_more locs with diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.mli b/infer/src/bufferoverrun/bufferOverrunUtils.mli index 7d83cccc0..cd5647e9b 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.mli +++ b/infer/src/bufferoverrun/bufferOverrunUtils.mli @@ -24,7 +24,7 @@ module ModelEnv : sig end module Exec : sig - val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t + val load_locs : 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/codetoanalyze/java/purity/GlobalTest.java b/infer/tests/codetoanalyze/java/purity/GlobalTest.java index 9094f6f48..45bee4f47 100644 --- a/infer/tests/codetoanalyze/java/purity/GlobalTest.java +++ b/infer/tests/codetoanalyze/java/purity/GlobalTest.java @@ -35,7 +35,7 @@ class GlobalTest { } // aliased_foo is aliasing a global and then is modified by incr. - void global_mod_via_argument_passing_bad_FP(int size, Foo f) { + void global_mod_via_argument_passing_bad_aliased(int size, Foo f) { Foo aliased_foo = foo; // Inferbo can't recognize aliasing here // and assumes aliased_foo is in [-oo,+oo] not in foo for (int i = 0; i < size; i++) { diff --git a/infer/tests/codetoanalyze/java/purity/issues.exp b/infer/tests/codetoanalyze/java/purity/issues.exp index 49ee95556..d5345a0f5 100644 --- a/infer/tests/codetoanalyze/java/purity/issues.exp +++ b/infer/tests/codetoanalyze/java/purity/issues.exp @@ -1,4 +1,3 @@ -codetoanalyze/java/purity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_bad_FP(int,GlobalTest$Foo):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void GlobalTest.global_mod_via_argument_passing_bad_FP(int,GlobalTest$Foo)] codetoanalyze/java/purity/Test.java, Test.call_pure_ok(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Test.call_pure_ok(int)] codetoanalyze/java/purity/Test.java, Test.emptyList_bad_FP():java.util.ArrayList, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function ArrayList Test.emptyList_bad_FP()] codetoanalyze/java/purity/Test.java, Test.local_alloc_ok(int,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.local_alloc_ok(int,int)]