From b55996d01aa88852bd029ae311dbec2963bfe508 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 4 Mar 2019 16:50:51 -0800 Subject: [PATCH] [inferbo] Symbolic value for global variable Summary: It assigns symbolic values for global variables in the load commands. However, it does not instantiate the symbols for the global variables yet, which will be addressed in another diff. Depends on D14208643 Reviewed By: ezgicicek Differential Revision: D14257619 fbshipit-source-id: f9113c8a3 --- infer/src/bufferoverrun/absLoc.ml | 9 +++ .../bufferoverrun/bufferOverrunAnalysis.ml | 4 +- .../src/bufferoverrun/bufferOverrunDomain.ml | 69 +++++++++++-------- infer/src/bufferoverrun/bufferOverrunTrace.ml | 7 +- infer/src/bufferoverrun/bufferOverrunUtils.ml | 4 +- .../src/bufferoverrun/bufferOverrunUtils.mli | 2 +- .../codetoanalyze/java/purity/GlobalTest.java | 2 +- .../codetoanalyze/java/purity/issues.exp | 1 - 8 files changed, 63 insertions(+), 35 deletions(-) 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)]