From 702602dcecd419c85fba11976cf9bf1b7bc485f0 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 30 Oct 2019 07:57:50 -0700 Subject: [PATCH] [pulse] check MustBeValid from preconditions all at once at the end Summary: Instead of checking that each address in the pre that must be valid is not invalid in the caller (and error out if it turns out it is invalid) as we discover them, save these checks for after we are sure that the precondition can be applied. It is in fact a bug that we can report an error when trying to apply a precondition that is actually not satisfiable in the current state for other reasons than lifetime issues. We still want to skip calls in case of weird issues like mismatch in number of formals vs actuals. This will have more obvious effects later when we also check that arithmetic facts in preconditions are satisfied at the call site: if a pre mandates "x=1" and "y must be valid" and we have "x=0" and "y invalid" then we shouldn't report an error. Reviewed By: skcho Differential Revision: D18115229 fbshipit-source-id: ad4ce72ff --- infer/src/pulse/PulseAbductiveDomain.ml | 75 +++++++++++++++---------- infer/src/pulse/PulseBaseMemory.ml | 2 + infer/src/pulse/PulseBaseMemory.mli | 2 + 3 files changed, 49 insertions(+), 30 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index cdc5f3aee..93a874f89 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -426,38 +426,23 @@ module PrePost = struct addresses are traversed in the process. *) let rec materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre ~addr_hist_caller call_state = - let add_call trace = - Trace.ViaCall - { in_call= trace - ; f= Call callee_proc_name - ; location= call_location - ; history= snd addr_hist_caller } - in match visit call_state ~addr_callee:addr_pre ~addr_hist_caller with | `AlreadyVisited, call_state -> Ok call_state | `NotAlreadyVisited, call_state -> ( - (let open Option.Monad_infix in - BaseMemory.find_opt addr_pre pre.BaseDomain.heap - >>= fun (edges_pre, attrs_pre) -> - Attributes.get_must_be_valid attrs_pre - >>| fun callee_access_trace -> - let access_trace = add_call callee_access_trace in - match Memory.check_valid access_trace (fst addr_hist_caller) call_state.astate with - | Error invalidated_by -> - Error (Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace}) - | Ok astate -> - let call_state = {call_state with astate} in - Container.fold_result - ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) - ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) -> - let astate, addr_hist_dest_caller = - Memory.eval_edge addr_hist_caller access call_state.astate - in - let call_state = {call_state with astate} in - materialize_pre_from_address callee_proc_name call_location ~pre - ~addr_pre:addr_pre_dest ~addr_hist_caller:addr_hist_dest_caller call_state )) - |> function Some result -> result | None -> Ok call_state ) + match BaseMemory.find_opt addr_pre pre.BaseDomain.heap with + | None -> + Ok call_state + | Some (edges_pre, _attrs_pre) -> + Container.fold_result + ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold) + ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) -> + let astate, addr_hist_dest_caller = + Memory.eval_edge addr_hist_caller access call_state.astate + in + let call_state = {call_state with astate} in + materialize_pre_from_address callee_proc_name call_location ~pre + ~addr_pre:addr_pre_dest ~addr_hist_caller:addr_hist_dest_caller call_state ) ) (** materialize subgraph of [pre] rooted at the address represented by a [formal] parameter that @@ -804,6 +789,32 @@ module PrePost = struct r + let check_all_valid callee_proc_name call_location {pre; post= _} call_state = + AddressMap.fold + (fun addr_pre (addr_caller, hist_caller) astate_result -> + match astate_result with + | Error _ -> + astate_result + | Ok astate -> ( + match BaseMemory.get_must_be_valid addr_pre (pre :> BaseDomain.t).heap with + | None -> + astate_result + | Some callee_access_trace -> + let access_trace = + Trace.ViaCall + { in_call= callee_access_trace + ; f= Call callee_proc_name + ; location= call_location + ; history= hist_caller } + in + Memory.check_valid access_trace addr_caller astate + |> Result.map_error ~f:(fun invalidated_by -> + L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; + Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace} + ) ) ) + call_state.subst (Ok call_state.astate) + + (* - read all the pre, assert validity of addresses and materializes *everything* (to throw stuff in the *current* pre as appropriate so that callers of the current procedure will also know about the deeper reads) @@ -835,13 +846,17 @@ module PrePost = struct | None -> (* couldn't apply the pre for some technical reason (as in: not by the fault of the programmer as far as we know) *) - Ok None + Ok (Some (astate, None)) | Some (Error _ as error) -> (* error: the function call requires to read some state known to be invalid *) error | Some (Ok call_state) -> + L.d_printfln "Pre applied successfully. call_state=%a" pp_call_state call_state ; + let open Result.Monad_infix in + check_all_valid callee_proc_name call_location pre_post call_state + >>= fun astate -> (* reset [visited] *) - let call_state = {call_state with visited= AddressSet.empty} in + let call_state = {call_state with astate; visited= AddressSet.empty} in (* apply the postcondition *) Ok (Some (apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state)) end diff --git a/infer/src/pulse/PulseBaseMemory.ml b/infer/src/pulse/PulseBaseMemory.ml index b8bd19346..3c4fd7f55 100644 --- a/infer/src/pulse/PulseBaseMemory.ml +++ b/infer/src/pulse/PulseBaseMemory.ml @@ -91,6 +91,8 @@ let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name let get_constant = get_attribute Attributes.get_constant +let get_must_be_valid = get_attribute Attributes.get_must_be_valid + let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory let is_std_vector_reserved address memory = diff --git a/infer/src/pulse/PulseBaseMemory.mli b/infer/src/pulse/PulseBaseMemory.mli index 5208e950d..9a13a7d66 100644 --- a/infer/src/pulse/PulseBaseMemory.mli +++ b/infer/src/pulse/PulseBaseMemory.mli @@ -62,6 +62,8 @@ val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option val get_constant : AbstractValue.t -> t -> Const.t option +val get_must_be_valid : AbstractValue.t -> t -> unit Trace.t option + val std_vector_reserve : AbstractValue.t -> t -> t val is_std_vector_reserved : AbstractValue.t -> t -> bool