From 23fcb72d3dba2ee4082f67ec263e3d2f9ffe25f0 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 19 May 2021 08:56:25 -0700 Subject: [PATCH] [pulse] refactor translating callee attributes to callers Summary: Make the API internal the the Attribute module. Reviewed By: ezgicicek Differential Revision: D28536890 fbshipit-source-id: e7b0d8147 --- infer/src/pulse/PulseAttribute.ml | 119 ++++++++++++++++------------- infer/src/pulse/PulseAttribute.mli | 5 +- infer/src/pulse/PulseInterproc.ml | 19 ++--- 3 files changed, 71 insertions(+), 72 deletions(-) diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index 3c6fd5a91..434744a47 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -135,6 +135,66 @@ module Attribute = struct F.pp_print_string f "Uninitialized" | WrittenTo trace -> F.fprintf f "WrittenTo %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "mutation")) trace + + + let is_suitable_for_pre = function + | MustBeValid _ | MustBeInitialized _ -> + true + | Invalid _ | Allocated _ | ISLAbduced _ -> + Config.pulse_isl + | AddressOfCppTemporary _ + | AddressOfStackVariable _ + | Closure _ + | DynamicType _ + | EndOfCollection + | StdVectorReserve + | Uninitialized + | WrittenTo _ -> + false + + + let is_suitable_for_post = function + | MustBeInitialized _ | MustBeValid _ -> + false + | Invalid _ + | Allocated _ + | ISLAbduced _ + | AddressOfCppTemporary _ + | AddressOfStackVariable _ + | Closure _ + | DynamicType _ + | EndOfCollection + | StdVectorReserve + | Uninitialized + | WrittenTo _ -> + true + + + let add_call proc_name call_location caller_history attr = + let add_call_to_trace in_call = + Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call} + in + match attr with + | Allocated (proc_name, trace) -> + Allocated (proc_name, add_call_to_trace trace) + | Invalid (invalidation, trace) -> + Invalid (invalidation, add_call_to_trace trace) + | ISLAbduced trace -> + ISLAbduced (add_call_to_trace trace) + | MustBeValid (trace, reason) -> + MustBeValid (add_call_to_trace trace, reason) + | MustBeInitialized trace -> + MustBeInitialized (add_call_to_trace trace) + | WrittenTo trace -> + WrittenTo (add_call_to_trace trace) + | ( AddressOfCppTemporary _ + | AddressOfStackVariable _ + | Closure _ + | DynamicType _ + | EndOfCollection + | StdVectorReserve + | Uninitialized ) as attr -> + attr end module Attributes = struct @@ -251,62 +311,11 @@ module Attributes = struct Set.add acc attr1 ) + let add_call proc_name call_location caller_history attrs = + Set.map attrs ~f:(fun attr -> Attribute.add_call proc_name call_location caller_history attr) + + include Set end include Attribute - -let is_suitable_for_pre = function - | MustBeValid _ | MustBeInitialized _ -> - true - | Invalid _ | Allocated _ | ISLAbduced _ -> - Config.pulse_isl - | AddressOfCppTemporary _ - | AddressOfStackVariable _ - | Closure _ - | DynamicType _ - | EndOfCollection - | StdVectorReserve - | Uninitialized - | WrittenTo _ -> - false - - -let is_suitable_for_post = function - | MustBeInitialized _ | MustBeValid _ -> - false - | Invalid _ - | Allocated _ - | ISLAbduced _ - | AddressOfCppTemporary _ - | AddressOfStackVariable _ - | Closure _ - | DynamicType _ - | EndOfCollection - | StdVectorReserve - | Uninitialized - | WrittenTo _ -> - true - - -let map_trace ~f = function - | Allocated (procname, trace) -> - Allocated (procname, f trace) - | ISLAbduced trace -> - ISLAbduced (f trace) - | Invalid (invalidation, trace) -> - Invalid (invalidation, f trace) - | MustBeValid (trace, reason) -> - MustBeValid (f trace, reason) - | WrittenTo trace -> - WrittenTo (f trace) - | MustBeInitialized trace -> - MustBeInitialized (f trace) - | ( AddressOfCppTemporary _ - | AddressOfStackVariable _ - | Closure _ - | DynamicType _ - | EndOfCollection - | StdVectorReserve - | Uninitialized ) as attr -> - attr diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index 818716550..200bb239a 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -33,9 +33,6 @@ val is_suitable_for_pre : t -> bool val is_suitable_for_post : t -> bool -val map_trace : f:(Trace.t -> Trace.t) -> t -> t -(** applies [f] to the traces found in attributes, leaving attributes without traces intact *) - module Attributes : sig include PrettyPrintable.PPUniqRankSet with type elt = t @@ -72,4 +69,6 @@ module Attributes : sig val replace_isl_abduced : t -> t -> t (** While applying a spec, replacing ISLAbduced by Allocated and Invalidation.Cfree by Invalidation.delete, if applicable *) + + val add_call : Procname.t -> Location.t -> ValueHistory.t -> t -> t end diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 58dfdacf1..e1551951d 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -174,10 +174,6 @@ let translate_access_to_caller subst (access_callee : BaseMemory.Access.t) : _ * (* {3 reading the pre from the current state} *) -let add_call_to_trace proc_name call_location caller_history in_call = - Trace.ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call} - - (** Materialize the (abstract memory) subgraph of [pre] reachable from [addr_pre] in [call_state.astate] starting from address [addr_caller]. Report an error if some invalid addresses are traversed in the process. *) @@ -264,12 +260,6 @@ let materialize_pre_for_globals callee_proc_name call_location pre_post call_sta ~addr_pre ~addr_hist_caller call_state ) -let add_call_to_attributes proc_name call_location caller_history attrs = - Attributes.map attrs ~f:(fun attr -> - Attribute.map_trace attr ~f:(fun trace -> - add_call_to_trace proc_name call_location caller_history trace ) ) - - let conjoin_callee_arith pre_post call_state = let open IResult.Let_syntax in L.d_printfln "applying callee path condition: (%a)[%a]" PathCondition.pp @@ -295,7 +285,7 @@ let apply_arithmetic_constraints callee_proc_name call_location pre_post call_st let open IResult.Let_syntax in let one_address_sat callee_attrs (addr_caller, caller_history) call_state = let attrs_caller = - add_call_to_attributes callee_proc_name call_location caller_history callee_attrs + Attributes.add_call callee_proc_name call_location caller_history callee_attrs in let astate = AddressAttributes.abduce_and_add addr_caller attrs_caller call_state.astate in if phys_equal astate call_state.astate then call_state else {call_state with astate} @@ -400,7 +390,7 @@ let record_post_cell callee_proc_name call_loc ~edges_pre_opt ~cell_callee_post:(edges_callee_post, attrs_callee_post) (addr_caller, hist_caller) call_state = let call_state = let attrs_post_caller = - add_call_to_attributes callee_proc_name call_loc hist_caller attrs_callee_post + Attributes.add_call callee_proc_name call_loc hist_caller attrs_callee_post in let astate = if Config.pulse_isl then @@ -581,7 +571,7 @@ let record_post_remaining_attributes callee_proc_name call_loc pre_post call_sta | None -> (* callee address has no meaning for the caller *) call_state | Some (addr_caller, history) -> - let attrs' = add_call_to_attributes callee_proc_name call_loc history attrs in + let attrs' = Attributes.add_call callee_proc_name call_loc history attrs in let astate = AddressAttributes.abduce_and_add addr_caller attrs' call_state.astate in {call_state with astate} ) (pre_post.AbductiveDomain.post :> BaseDomain.t).attrs call_state @@ -590,7 +580,8 @@ let record_post_remaining_attributes callee_proc_name call_loc pre_post call_sta let record_skipped_calls callee_proc_name call_loc pre_post call_state = let callee_skipped_map = pre_post.AbductiveDomain.skipped_calls - |> SkippedCalls.map (fun trace -> add_call_to_trace callee_proc_name call_loc [] trace) + |> SkippedCalls.map (fun trace -> + Trace.ViaCall {f= Call callee_proc_name; location= call_loc; history= []; in_call= trace} ) in let astate = AbductiveDomain.add_skipped_calls callee_skipped_map call_state.astate in {call_state with astate}