From a1855dee8a9b324e3c3838760634afe6b5378653 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 25 May 2021 09:09:43 -0700 Subject: [PATCH] [pulse][5/5] timestamps for MustBeInitialized Summary: Same as MustBeValid: we want to report the first error on the path. Reviewed By: skcho Differential Revision: D28674724 fbshipit-source-id: a2ac04b5b --- infer/src/pulse/PulseAbductiveDomain.ml | 5 +++-- infer/src/pulse/PulseAbductiveDomain.mli | 2 +- infer/src/pulse/PulseAttribute.ml | 17 +++++++------- infer/src/pulse/PulseAttribute.mli | 4 ++-- .../src/pulse/PulseBaseAddressAttributes.mli | 2 +- infer/src/pulse/PulseInterproc.ml | 22 +++++-------------- infer/src/pulse/PulseOperations.ml | 4 ++-- .../tests/codetoanalyze/objc/pulse/issues.exp | 2 +- 8 files changed, 25 insertions(+), 33 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index ef7fbfff9..ec7f6cbc2 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -244,14 +244,15 @@ module AddressAttributes = struct astate - let check_initialized access_trace addr astate = + let check_initialized path access_trace addr astate = let attrs = (astate.post :> base_domain).attrs in let+ () = BaseAddressAttributes.check_initialized addr attrs in let is_written_to = Option.exists (BaseAddressAttributes.find_opt addr attrs) ~f:(fun attrs -> Attribute.Attributes.get_written_to attrs |> Option.is_some ) in - if is_written_to then astate else abduce_attribute addr (MustBeInitialized access_trace) astate + if is_written_to then astate + else abduce_attribute addr (MustBeInitialized (path.PathContext.timestamp, access_trace)) astate (** [astate] with [astate.post.attrs = f astate.post.attrs] *) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index e75bfb369..93bb803ff 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -127,7 +127,7 @@ module AddressAttributes : sig -> t -> (t, Invalidation.t * Trace.t) result - val check_initialized : Trace.t -> AbstractValue.t -> t -> (t, unit) result + val check_initialized : PathContext.t -> Trace.t -> AbstractValue.t -> t -> (t, unit) result val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 6f14a1385..c12a0f817 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -34,7 +34,7 @@ module Attribute = struct | EndOfCollection | Invalid of Invalidation.t * Trace.t | ISLAbduced of Trace.t - | MustBeInitialized of Trace.t + | MustBeInitialized of PathContext.timestamp * Trace.t | MustBeValid of PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option | StdVectorReserve | Uninitialized @@ -97,7 +97,7 @@ module Attribute = struct let unreachable_at_rank = Variants.to_rank (UnreachableAt Location.dummy) - let must_be_initialized_rank = Variants.to_rank (MustBeInitialized dummy_trace) + let must_be_initialized_rank = Variants.to_rank (MustBeInitialized (PathContext.t0, dummy_trace)) let pp f attribute = let pp_string_if_debug string fmt = @@ -125,10 +125,11 @@ module Attribute = struct trace | ISLAbduced trace -> F.fprintf f "ISLAbduced %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "ISLAbduced")) trace - | MustBeInitialized trace -> - F.fprintf f "MustBeInitialized %a" + | MustBeInitialized (timestamp, trace) -> + F.fprintf f "MustBeInitialized(%a, t=%d)" (Trace.pp ~pp_immediate:(pp_string_if_debug "read")) trace + (timestamp :> int) | MustBeValid (timestamp, trace, reason) -> F.fprintf f "MustBeValid(%a, %a, t=%d)" (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) @@ -201,8 +202,8 @@ module Attribute = struct ISLAbduced (add_call_to_trace trace) | MustBeValid (_timestamp, trace, reason) -> MustBeValid (path.PathContext.timestamp, add_call_to_trace trace, reason) - | MustBeInitialized trace -> - MustBeInitialized (add_call_to_trace trace) + | MustBeInitialized (_timestamp, trace) -> + MustBeInitialized (path.PathContext.timestamp, add_call_to_trace trace) | WrittenTo trace -> WrittenTo (add_call_to_trace trace) | ( AddressOfCppTemporary _ @@ -293,8 +294,8 @@ module Attributes = struct let get_must_be_initialized attrs = Set.find_rank attrs Attribute.must_be_initialized_rank |> Option.map ~f:(fun attr -> - let[@warning "-8"] (Attribute.MustBeInitialized trace) = attr in - trace ) + let[@warning "-8"] (Attribute.MustBeInitialized (timestamp, trace)) = attr in + (timestamp, trace) ) let get_unreachable_at attrs = diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 686942c20..147db98ff 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -21,7 +21,7 @@ type t = | EndOfCollection | Invalid of Invalidation.t * Trace.t | ISLAbduced of Trace.t (** The allocation is abduced so as the analysis could run normally *) - | MustBeInitialized of Trace.t + | MustBeInitialized of PathContext.timestamp * Trace.t | MustBeValid of PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option | StdVectorReserve | Uninitialized @@ -65,7 +65,7 @@ module Attributes : sig val is_uninitialized : t -> bool - val get_must_be_initialized : t -> Trace.t option + val get_must_be_initialized : t -> (PathContext.timestamp * Trace.t) option val get_unreachable_at : t -> Location.t option diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index d7783e677..a9e76dde5 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -48,7 +48,7 @@ val get_must_be_valid : val is_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> bool -val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option +val get_must_be_initialized : AbstractValue.t -> t -> (PathContext.timestamp * Trace.t) option val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 9b7a6bb44..424efc239 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -636,22 +636,12 @@ let check_all_valid path callee_proc_name call_location {AbductiveDomain.pre; _} call_state.subst [] in let timestamp_of_check = function - | `MustBeValid (timestamp, _, _) -> - Some timestamp - | `MustBeInitialized _ -> - None + | `MustBeValid (timestamp, _, _) | `MustBeInitialized (timestamp, _) -> + timestamp in List.sort addresses_to_check ~compare:(fun (_, check1) (_, check2) -> - match (timestamp_of_check check1, timestamp_of_check check2) with - | Some t1, Some t2 -> - (* smaller timestamp first *) PathContext.compare_timestamp t1 t2 - (* with a timestamp first (gone soon when MustBeInitialized will get a timestamp too), otherwise dummy comparison *) - | None, None -> - 0 - | Some _, None -> - -1 - | None, Some _ -> - 1 ) + (* smaller timestamp first *) + PathContext.compare_timestamp (timestamp_of_check check1) (timestamp_of_check check2) ) |> List.fold_result ~init:call_state.astate ~f:(fun astate ((addr_caller, hist_caller), check) -> let mk_access_trace callee_access_trace = Trace.ViaCall @@ -675,9 +665,9 @@ let check_all_valid path callee_proc_name call_location {AbductiveDomain.pre; _} ; access_trace ; must_be_valid_reason } ; astate } ) - | `MustBeInitialized callee_access_trace -> + | `MustBeInitialized (_timestamp, callee_access_trace) -> let access_trace = mk_access_trace callee_access_trace in - AddressAttributes.check_initialized access_trace addr_caller astate + AddressAttributes.check_initialized path access_trace addr_caller astate |> Result.map_error ~f:(fun () -> L.d_printfln "ERROR: caller's %a is uninitialized!" AbstractValue.pp addr_caller ; AccessResult.ReportableError diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 005c4f684..e4064b010 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -67,7 +67,7 @@ let check_addr_access path ?must_be_valid_reason access_mode location (address, in match access_mode with | Read -> - AddressAttributes.check_initialized access_trace address astate + AddressAttributes.check_initialized path access_trace address astate |> Result.map_error ~f:(fun () -> ReportableError { diagnostic= @@ -87,7 +87,7 @@ let check_and_abduce_addr_access_isl path access_mode location (address, history let* astate = AccessResult.of_abductive_access_result access_trace access_result in match access_mode with | Read -> - AddressAttributes.check_initialized access_trace address astate + AddressAttributes.check_initialized path access_trace address astate |> Result.map_error ~f:(fun () -> ReportableError { diagnostic= diff --git a/infer/tests/codetoanalyze/objc/pulse/issues.exp b/infer/tests/codetoanalyze/objc/pulse/issues.exp index d17c1f30f..4f44be83e 100644 --- a/infer/tests/codetoanalyze/objc/pulse/issues.exp +++ b/infer/tests/codetoanalyze/objc/pulse/issues.exp @@ -13,6 +13,6 @@ codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.assignNilBad, 5, NIL_BLOCK_CALL, codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramAssignNilBad:, 3, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here] codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramReassignNilBad:, 6, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,assigned,assigned,invalid access occurs here] codetoanalyze/objc/pulse/NPENilBlocks.m, calldoSomethingThenCallbackWithNilBad, 2, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,when calling `BlockA.doSomethingThenCallback:` here,parameter `my_block` of BlockA.doSomethingThenCallback:,invalid access occurs here] -codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `y` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here] +codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `x` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here] codetoanalyze/objc/pulse/use_after_free.m, PulseTest.use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,invalid access occurs here] codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]