From a0d1fee1dc19970aa5be98e9ee62c889c84d905a Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 15 Apr 2020 07:17:32 -0700 Subject: [PATCH] [pulse] move SkippedCalls to its own file Summary: Seems logical. Reviewed By: ezgicicek Differential Revision: D21022922 fbshipit-source-id: 1b8546332 --- infer/src/checkers/impurity.ml | 4 ++-- infer/src/checkers/impurityDomain.ml | 2 +- infer/src/checkers/impurityDomain.mli | 2 +- infer/src/pulse/PulseAbductiveDomain.ml | 18 +--------------- infer/src/pulse/PulseAbductiveDomain.mli | 2 -- infer/src/pulse/PulseBasicInterface.ml | 1 + infer/src/pulse/PulseInterproc.ml | 5 ++--- infer/src/pulse/PulseSkippedCalls.ml | 26 ++++++++++++++++++++++++ infer/src/pulse/PulseSkippedCalls.mli | 10 +++++++++ 9 files changed, 44 insertions(+), 26 deletions(-) create mode 100644 infer/src/pulse/PulseSkippedCalls.ml create mode 100644 infer/src/pulse/PulseSkippedCalls.mli diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 35407e10d..2e25bfeb9 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -156,7 +156,7 @@ let extract_impurity tenv pdesc (exec_state : PulseExecutionState.t) : ImpurityD let modified_globals = get_modified_globals pre_heap post post_stack in let skipped_calls = PulseAbductiveDomain.get_skipped_calls astate - |> PulseAbductiveDomain.SkippedCalls.filter (fun proc_name _ -> + |> PulseSkippedCalls.filter (fun proc_name _ -> Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) ) in {modified_globals; modified_params; skipped_calls; exited} @@ -195,7 +195,7 @@ let checker {exe_env; Callbacks.summary} : Summary.t = set acc in let skipped_functions = - PulseAbductiveDomain.SkippedCalls.fold + PulseSkippedCalls.fold (fun proc_name trace acc -> PulseTrace.add_to_errlog ~nesting:1 ~include_value_history:false ~pp_immediate:(fun fmt -> diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index 3efd41c21..91c2cf950 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -7,7 +7,7 @@ open! IStd module F = Format -module SkippedCalls = PulseAbductiveDomain.SkippedCalls +module SkippedCalls = PulseSkippedCalls type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * PulseTrace.t) [@@deriving compare] diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 11ee46e55..b5e91ecd3 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -24,7 +24,7 @@ module Exited = AbstractDomain.BooleanOr type t = { modified_params: ModifiedVarSet.t ; modified_globals: ModifiedVarSet.t - ; skipped_calls: PulseAbductiveDomain.SkippedCalls.t + ; skipped_calls: PulseSkippedCalls.t ; exited: Exited.t } val pure : t diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 618681ad0..bce78a3b3 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -4,6 +4,7 @@ * This source code is licensed under the MIT license found in the * LICENSE file in the root directory of this source tree. *) + open! IStd module F = Format module L = Logging @@ -80,23 +81,6 @@ end module PreDomain : BaseDomainSig = Domain (** represents the inferred pre-condition at each program point, biabduction style *) -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" ) - - - let leq ~lhs ~rhs = phys_equal lhs rhs - - let join s1 _ = s1 - - let widen ~prev ~next ~num_iters:_ = join prev next -end - -module SkippedCalls = AbstractDomain.Map (Procname) (SkippedTrace) - (** biabduction-style pre/post state + skipped calls *) type t = { post: Domain.t (** state at the current program point*) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 5de10212f..c2d671aed 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -51,8 +51,6 @@ module PreDomain : BaseDomainSig lattice of [Domain], but since we never actually join states or check implication the two collapse into one. * *) -module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = PulseTrace.t - (** biabduction-style pre/post state + skipped calls *) type t = private { post: Domain.t (** state at the current program point*) diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml index 845059973..9a31a304f 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -15,5 +15,6 @@ module CallEvent = PulseCallEvent module CItv = PulseCItv module Diagnostic = PulseDiagnostic module Invalidation = PulseInvalidation +module SkippedCalls = PulseSkippedCalls module Trace = PulseTrace module ValueHistory = PulseValueHistory diff --git a/infer/src/pulse/PulseInterproc.ml b/infer/src/pulse/PulseInterproc.ml index 7c2112bc5..51ace5258 100644 --- a/infer/src/pulse/PulseInterproc.ml +++ b/infer/src/pulse/PulseInterproc.ml @@ -134,7 +134,7 @@ let visit call_state ~addr_callee ~addr_hist_caller = let pp f {AbductiveDomain.pre; post; skipped_calls} = F.fprintf f "PRE:@\n @[%a@]@\n" BaseDomain.pp (pre :> BaseDomain.t) ; F.fprintf f "POST:@\n @[%a@]@\n" BaseDomain.pp (post :> BaseDomain.t) ; - F.fprintf f "SKIPPED_CALLS:@ @[%a@]@\n" AbductiveDomain.SkippedCalls.pp skipped_calls + F.fprintf f "SKIPPED_CALLS:@ @[%a@]@\n" SkippedCalls.pp skipped_calls (* {3 reading the pre from the current state} *) @@ -534,8 +534,7 @@ 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 - |> AbductiveDomain.SkippedCalls.map (fun trace -> - add_call_to_trace callee_proc_name call_loc [] trace ) + |> SkippedCalls.map (fun trace -> add_call_to_trace callee_proc_name call_loc [] trace) in let astate = AbductiveDomain.add_skipped_calls callee_skipped_map call_state.astate in {call_state with astate} diff --git a/infer/src/pulse/PulseSkippedCalls.ml b/infer/src/pulse/PulseSkippedCalls.ml new file mode 100644 index 000000000..8857c6bab --- /dev/null +++ b/infer/src/pulse/PulseSkippedCalls.ml @@ -0,0 +1,26 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module F = Format + +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" ) + + + let leq ~lhs ~rhs = phys_equal lhs rhs + + let join s1 _ = s1 + + let widen ~prev ~next ~num_iters:_ = join prev next +end + +include AbstractDomain.Map (Procname) (SkippedTrace) diff --git a/infer/src/pulse/PulseSkippedCalls.mli b/infer/src/pulse/PulseSkippedCalls.mli new file mode 100644 index 000000000..dfa9d0c4e --- /dev/null +++ b/infer/src/pulse/PulseSkippedCalls.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +include AbstractDomain.MapS with type key = Procname.t and type value = PulseTrace.t