From 426b7dfe51255c836ddc089a01b5bcea7af98435 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 20 Jan 2020 05:35:51 -0800 Subject: [PATCH] [pulse] Track skipped functions Summary: Let's collect the list of all skipped functions with a `proc_name` but no summary in Pulse's memory. This will be useful for the impurity analysis later (next diff). Concretely, we extend Pulse's domain with a map from skipped calls to their respective traces. For efficiency, we only keep a single trace per skipped call. For impurity analysis, tracking skipped calls in Pulse allows us to rely on Pulse's strong memory model to get rid of infeasible paths as opposed to creating an independent checker which wouldn't be able to do that. Reviewed By: jvillard Differential Revision: D19428426 fbshipit-source-id: 3c5e482c5 --- infer/src/pulse/PulseAbductiveDomain.ml | 67 +++++++++++++++++++----- infer/src/pulse/PulseAbductiveDomain.mli | 2 + infer/src/pulse/PulseBaseDomain.ml | 23 ++++++-- infer/src/pulse/PulseBaseDomain.mli | 9 +++- infer/src/pulse/PulseOperations.ml | 11 +++- 5 files changed, 91 insertions(+), 21 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 0c6e36c16..b82b1e99f 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -11,6 +11,7 @@ open PulseBasicInterface module BaseDomain = PulseBaseDomain module BaseStack = PulseBaseStack module BaseMemory = PulseBaseMemory +module BaseSkippedCallsMap = BaseDomain.SkippedCallsMap (** signature common to the "normal" [Domain], representing the post at the current program point, and the inverted [InvertedDomain], representing the inferred pre-condition*) @@ -21,27 +22,34 @@ module type BaseDomain = sig val empty : t - val make : BaseStack.t -> BaseMemory.t -> t + val make : BaseStack.t -> BaseMemory.t -> BaseSkippedCallsMap.t -> t - val update : ?stack:BaseStack.t -> ?heap:BaseMemory.t -> t -> t + val update : + ?stack:BaseStack.t -> ?heap:BaseMemory.t -> ?skipped_calls_map:BaseSkippedCallsMap.t -> t -> t include AbstractDomain.NoJoin with type t := t end (* just to expose the [heap] and [stack] record field names without having to type [BaseDomain.heap] *) -type base_domain = BaseDomain.t = {heap: BaseMemory.t; stack: BaseStack.t} +type base_domain = BaseDomain.t = + {heap: BaseMemory.t; stack: BaseStack.t; skipped_calls_map: BaseSkippedCallsMap.t} (** operations common to [Domain] and [InvertedDomain], see also the [BaseDomain] signature *) module BaseDomainCommon = struct - let make stack heap = {stack; heap} + let make stack heap skipped_calls_map = {stack; heap; skipped_calls_map} - let update ?stack ?heap foot = - let new_stack, new_heap = - (Option.value ~default:foot.stack stack, Option.value ~default:foot.heap heap) + let update ?stack ?heap ?skipped_calls_map foot = + let new_stack, new_heap, new_skipped_calls_map = + ( Option.value ~default:foot.stack stack + , Option.value ~default:foot.heap heap + , Option.value ~default:foot.skipped_calls_map skipped_calls_map ) in - if phys_equal new_stack foot.stack && phys_equal new_heap foot.heap then foot - else {stack= new_stack; heap= new_heap} + if + phys_equal new_stack foot.stack && phys_equal new_heap foot.heap + && phys_equal new_skipped_calls_map foot.skipped_calls_map + then foot + else {stack= new_stack; heap= new_heap; skipped_calls_map= new_skipped_calls_map} end (** represents the post abstract state at each program point *) @@ -112,7 +120,8 @@ module Stack = struct (* HACK: do not record the history of values in the pre as they are unused *) let foot_stack = BaseStack.add var (addr, []) (astate.pre :> base_domain).stack in let foot_heap = BaseMemory.register_address addr (astate.pre :> base_domain).heap in - InvertedDomain.make foot_stack foot_heap + let pre_skipped_calls_map = (astate.pre :> base_domain).skipped_calls_map in + InvertedDomain.make foot_stack foot_heap pre_skipped_calls_map else astate.pre in ({post= Domain.update astate.post ~stack:post_stack; pre}, addr_hist) @@ -265,12 +274,26 @@ let mk_initial proc_desc = List.fold formals ~init:(InvertedDomain.empty :> base_domain).heap ~f:(fun heap (_, (addr, _)) -> BaseMemory.register_address addr heap) in - InvertedDomain.make initial_stack initial_heap + let initial_skipped_map = (InvertedDomain.empty :> BaseDomain.t).skipped_calls_map in + InvertedDomain.make initial_stack initial_heap initial_skipped_map in let post = Domain.update ~stack:initial_stack Domain.empty in {pre; post} +(** [astate] with [astate.post.skipped_calls_map = f astate.post.skipped_calls_map] *) +let map_post_skipped_calls_map ~f astate = + let new_post = + Domain.update astate.post ~skipped_calls_map:(f (astate.post :> base_domain).skipped_calls_map) + in + if phys_equal new_post astate.post then astate else {astate with post= new_post} + + +let add_skipped_calls_map pname trace astate = + map_post_skipped_calls_map astate ~f:(fun skipped_call_map -> + BaseSkippedCallsMap.add pname trace skipped_call_map ) + + let discard_unreachable ({pre; post} as astate) = let pre_addresses = BaseDomain.reachable_addresses (pre :> BaseDomain.t) in let pre_old_heap = (pre :> BaseDomain.t).heap in @@ -285,8 +308,7 @@ let discard_unreachable ({pre; post} as astate) = in if phys_equal pre_new_heap pre_old_heap && phys_equal post_new_heap post_old_heap then astate else - { pre= InvertedDomain.make (pre :> BaseDomain.t).stack pre_new_heap - ; post= Domain.make (post :> BaseDomain.t).stack post_new_heap } + {pre= InvertedDomain.update pre ~heap:pre_new_heap; post= Domain.update post ~heap:post_new_heap} let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var) @@ -774,7 +796,8 @@ module PrePost = struct BaseMemory.set_edges addr_caller edges_post_caller heap |> BaseMemory.add_attribute addr_caller written_to in - let caller_post = Domain.make (call_state.astate.post :> base_domain).stack heap in + let call_post = (call_state.astate.post :> base_domain) in + let caller_post = Domain.make call_post.stack heap call_post.skipped_calls_map in {call_state with subst; astate= {call_state.astate with post= caller_post}} @@ -908,6 +931,21 @@ module PrePost = struct (pre_post.post :> BaseDomain.t).heap call_state + let record_skipped_calls callee_proc_name call_loc pre_post call_state = + let callee_skipped_map = (pre_post.post :> BaseDomain.t).skipped_calls_map in + let caller_skipped_map = + BaseSkippedCallsMap.map + (fun trace -> add_call_to_trace callee_proc_name call_loc [] trace) + callee_skipped_map + |> (* favor calls we already knew about somewhat arbitrarily *) + BaseSkippedCallsMap.union + (fun _ orig_call _callee_call -> Some orig_call) + (call_state.astate.post :> BaseDomain.t).skipped_calls_map + in + { call_state with + astate= map_post_skipped_calls_map ~f:(fun _ -> caller_skipped_map) call_state.astate } + + let apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state = PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse call post" ())) ; let r = @@ -916,6 +954,7 @@ module PrePost = struct |> record_post_for_return callee_proc_name call_location pre_post |> fun (call_state, return_caller) -> ( record_post_remaining_attributes callee_proc_name call_location pre_post call_state + |> record_skipped_calls callee_proc_name call_location pre_post , return_caller ) |> fun ({astate}, return_caller) -> (astate, return_caller) in diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 982efe2eb..9533d00e4 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -112,6 +112,8 @@ val discard_unreachable : t -> t (** garbage collect unreachable addresses in the state to make it smaller, just for convenience and keep its size down *) +val add_skipped_calls_map : Procname.t -> PulseTrace.t -> t -> t + val extract_pre : PrePost.t -> BaseDomain.t val extract_post : PrePost.t -> BaseDomain.t diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index 866497105..47a490882 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -11,16 +11,27 @@ open PulseBasicInterface module Memory = PulseBaseMemory module Stack = PulseBaseStack +module SkippedTrace = struct + type t = PulseTrace.t [@@deriving compare] + + let pp fmt = + PulseTrace.pp fmt ~pp_immediate:(fun fmt -> + F.pp_print_string fmt "call to skipped function occurs here" ) +end + +module SkippedCallsMap = PrettyPrintable.MakePPMonoMap (Procname) (SkippedTrace) + (* {2 Abstract domain description } *) -type t = {heap: Memory.t; stack: Stack.t} +type t = {heap: Memory.t; stack: Stack.t; skipped_calls_map: SkippedCallsMap.t} let empty = { heap= Memory.empty (* TODO: we could record that 0 is an invalid address at this point but this makes the analysis go a bit overboard with the Nullptr reports. *) - ; stack= Stack.empty } + ; stack= Stack.empty + ; skipped_calls_map= SkippedCallsMap.empty } (** comparison between two elements of the domain to determine the [<=] relation @@ -172,9 +183,11 @@ let leq ~lhs ~rhs = phys_equal lhs rhs || GraphComparison.is_isograph ~lhs ~rhs GraphComparison.empty_mapping -let pp fmt {heap; stack} = - F.fprintf fmt "{@[ roots=@[%a@];@;mem =@[%a@];@;attrs=@[%a@];@]}" Stack.pp stack - Memory.pp_heap heap Memory.pp_attributes heap +let pp fmt {heap; stack; skipped_calls_map} = + F.fprintf fmt + "{@[ roots=@[%a@];@;mem =@[%a@];@;attrs=@[%a@];@;skipped_calls=@[%a@];@]}" + Stack.pp stack Memory.pp_heap heap Memory.pp_attributes heap SkippedCallsMap.pp + skipped_calls_map module GraphVisit : sig diff --git a/infer/src/pulse/PulseBaseDomain.mli b/infer/src/pulse/PulseBaseDomain.mli index eea5cc9db..79e8948ed 100644 --- a/infer/src/pulse/PulseBaseDomain.mli +++ b/infer/src/pulse/PulseBaseDomain.mli @@ -8,7 +8,14 @@ open! IStd open PulseBasicInterface -type t = {heap: PulseBaseMemory.t; stack: PulseBaseStack.t} +module SkippedTrace : sig + type t = PulseTrace.t +end + +module SkippedCallsMap : + PrettyPrintable.PPMonoMap with type key = Procname.t and type value = SkippedTrace.t + +type t = {heap: PulseBaseMemory.t; stack: PulseBaseStack.t; skipped_calls_map: SkippedCallsMap.t} val empty : t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 31d30a4bd..fe8053c8e 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -499,6 +499,15 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate else astate in + let add_skipped_proc astate = + match reason with + | PulseCallEvent.SkippedKnownCall proc_name -> + AbductiveDomain.add_skipped_calls_map proc_name + (Trace.Immediate {location= call_loc; history= []}) + astate + | _ -> + astate + in L.d_printfln "skipping unknown procedure@." ; ( match formals_opt with | None -> @@ -518,7 +527,7 @@ let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate = astate | Ok result -> result ) ) - |> havoc_ret ret + |> havoc_ret ret |> add_skipped_proc let call ~caller_summary call_loc callee_pname ~ret ~actuals ~formals_opt astate =