From c909d6bd7ef78a73384fd2a9db4953ade08bee5e Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 21 Oct 2019 03:29:39 -0700 Subject: [PATCH] [pulse][1/9] create PulseBasicInterface, with CallEvent Summary: Problem: PulseDomain.ml is pretty big, and contains lots of small modules. The Infer build being a bit monolithic at the moment, it is hard to split all these small modules off without creating some confusion about which abstraction barries lay where. For instance, it's fine to use `PulseDomain.ValueHistory` anywhere, but using `PulseDomain` itself is sometimes bad when one should use `PulseAbductiveDomain` instead. Proposal: a poorman's library mechanism based on module aliasing. This stack of diffs creates new Pulse* modules for all these small, safe to use modules, together with `PulseBasicInterface.ml`, which aliases these modules to remove the `Pulse` prefix. At the end of the stack, it will contain: ``` module AbstractValue = PulseAbstractValue module Attribute = PulseAttribute module Attributes = PulseAttribute.Attributes module CallEvent = PulseCallEvent module Diagnostic = PulseDiagnostic module Invalidation = PulseInvalidation module Trace = PulseTrace module ValueHistory = PulseValueHistory ``` This "interface" module can be opened in other pulse modules freely. Reviewed By: ezgicicek Differential Revision: D17955104 fbshipit-source-id: 13d3aa2b5 --- infer/src/pulse/PulseBasicInterface.ml | 11 +++++++++ infer/src/pulse/PulseCallEvent.ml | 32 ++++++++++++++++++++++++++ infer/src/pulse/PulseCallEvent.mli | 20 ++++++++++++++++ infer/src/pulse/PulseDiagnostic.ml | 2 +- infer/src/pulse/PulseDomain.ml | 27 +--------------------- infer/src/pulse/PulseDomain.mli | 11 +-------- infer/src/pulse/PulseModels.ml | 3 ++- 7 files changed, 68 insertions(+), 38 deletions(-) create mode 100644 infer/src/pulse/PulseBasicInterface.ml create mode 100644 infer/src/pulse/PulseCallEvent.ml create mode 100644 infer/src/pulse/PulseCallEvent.mli diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml new file mode 100644 index 000000000..89e442eb4 --- /dev/null +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -0,0 +1,11 @@ +(* + * 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 + +(** Basic Pulse modules that are safe to use in any module *) + +module CallEvent = PulseCallEvent diff --git a/infer/src/pulse/PulseCallEvent.ml b/infer/src/pulse/PulseCallEvent.ml new file mode 100644 index 000000000..6bef6fd64 --- /dev/null +++ b/infer/src/pulse/PulseCallEvent.ml @@ -0,0 +1,32 @@ +(* + * 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 + +type t = + | Call of Typ.Procname.t + | Model of string + | SkippedKnownCall of Typ.Procname.t + | SkippedUnknownCall of Exp.t +[@@deriving compare] + +let pp_config ~verbose fmt = + let pp_proc_name = if verbose then Typ.Procname.pp else Typ.Procname.describe in + function + | Call proc_name -> + F.fprintf fmt "`%a`" pp_proc_name proc_name + | Model model -> + F.fprintf fmt "`%s` (modelled)" model + | SkippedKnownCall proc_name -> + F.fprintf fmt "function `%a` with no summary" pp_proc_name proc_name + | SkippedUnknownCall call_exp -> + F.fprintf fmt "unresolved call expression `%a`" Exp.pp call_exp + + +let pp = pp_config ~verbose:true + +let describe = pp_config ~verbose:false diff --git a/infer/src/pulse/PulseCallEvent.mli b/infer/src/pulse/PulseCallEvent.mli new file mode 100644 index 000000000..7198a434c --- /dev/null +++ b/infer/src/pulse/PulseCallEvent.mli @@ -0,0 +1,20 @@ +(* + * 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 + +type t = + | Call of Typ.Procname.t (** known function with summary *) + | Model of string (** hardcoded model *) + | SkippedKnownCall of Typ.Procname.t (** known function without summary *) + | SkippedUnknownCall of Exp.t (** couldn't link the expression to a proc name *) +[@@deriving compare] + +val pp : F.formatter -> t -> unit + +val describe : F.formatter -> t -> unit diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index cf5fa393a..2d4d5ded5 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -7,10 +7,10 @@ open! IStd module F = Format -module CallEvent = PulseDomain.CallEvent module Invalidation = PulseDomain.Invalidation module Trace = PulseDomain.Trace module ValueHistory = PulseDomain.ValueHistory +open PulseBasicInterface type t = | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t} diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index bc2b9e94d..752ba5c7f 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -7,35 +7,10 @@ open! IStd module F = Format module L = Logging +open PulseBasicInterface (* {2 Abstract domain description } *) -module CallEvent = struct - type t = - | Call of Typ.Procname.t - | Model of string - | SkippedKnownCall of Typ.Procname.t - | SkippedUnknownCall of Exp.t - [@@deriving compare] - - let pp_config ~verbose fmt = - let pp_proc_name = if verbose then Typ.Procname.pp else Typ.Procname.describe in - function - | Call proc_name -> - F.fprintf fmt "`%a`" pp_proc_name proc_name - | Model model -> - F.fprintf fmt "`%s` (modelled)" model - | SkippedKnownCall proc_name -> - F.fprintf fmt "function `%a` with no summary" pp_proc_name proc_name - | SkippedUnknownCall call_exp -> - F.fprintf fmt "unresolved call expression `%a`" Exp.pp call_exp - - - let pp = pp_config ~verbose:true - - let describe = pp_config ~verbose:false -end - module Invalidation = struct type std_vector_function = | Assign diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index d03b40f56..7e1d8b208 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -7,16 +7,7 @@ open! IStd module F = Format - -module CallEvent : sig - type t = - | Call of Typ.Procname.t (** known function with summary *) - | Model of string (** hardcoded model *) - | SkippedKnownCall of Typ.Procname.t (** known function without summary *) - | SkippedUnknownCall of Exp.t (** couldn't link the expression to a proc name *) - - val describe : F.formatter -> t -> unit -end +open PulseBasicInterface module Invalidation : sig type std_vector_function = diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 1d3ffe11b..fcfb51609 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -6,6 +6,7 @@ *) open! IStd open Result.Monad_infix +open PulseBasicInterface type exec_fun = caller_summary:Summary.t @@ -106,7 +107,7 @@ module StdBasicString = struct let destructor : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> - let model = PulseDomain.CallEvent.Model "std::basic_string::~basic_string()" in + let model = CallEvent.Model "std::basic_string::~basic_string()" in let call_event = PulseDomain.ValueHistory.Call {f= model; location; in_call= []} in match actuals with | [(this_hist, _)] ->