diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index ab262542c..5a3890368 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -10,7 +10,7 @@ module F = Format type trace = | WrittenTo of unit PulseDomain.Trace.t - | Invalid of PulseDomain.Invalidation.t PulseDomain.Trace.t + | Invalid of PulseInvalidation.t PulseDomain.Trace.t [@@deriving compare] module ModifiedVar = struct @@ -64,7 +64,7 @@ let add_to_errlog ~nesting param_source ModifiedVar.{var; trace_list} errlog = PulseDomain.Trace.add_to_errlog ~nesting (fun fmt invalid -> F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var - PulseDomain.Invalidation.describe invalid ) + PulseInvalidation.describe invalid ) invalidation_trace errlog in let first_trace, rest = trace_list in diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 349b4a920..0a82b5b09 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -8,7 +8,7 @@ open! IStd type trace = | WrittenTo of unit PulseDomain.Trace.t - | Invalid of PulseDomain.Invalidation.t PulseDomain.Trace.t + | Invalid of PulseInvalidation.t PulseDomain.Trace.t module ModifiedVar : sig type nonempty_action_type = trace * trace list diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 9e6dc096f..8d20d09c6 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -9,8 +9,8 @@ module F = Format module L = Logging open Result.Monad_infix module AbstractAddress = PulseDomain.AbstractAddress -module Invalidation = PulseDomain.Invalidation module ValueHistory = PulseDomain.ValueHistory +open PulseBasicInterface include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) struct diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 494bd89fb..d7501263f 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -10,7 +10,6 @@ module L = Logging module AbstractAddress = PulseDomain.AbstractAddress module Attribute = PulseDomain.Attribute module Attributes = PulseDomain.Attributes -module Invalidation = PulseDomain.Invalidation module Trace = PulseDomain.Trace module ValueHistory = PulseDomain.ValueHistory module BaseStack = PulseDomain.Stack diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index fc325e72c..704ba561e 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -7,9 +7,9 @@ open! IStd module AbstractAddress = PulseDomain.AbstractAddress module Attribute = PulseDomain.Attribute -module Invalidation = PulseDomain.Invalidation module Trace = PulseDomain.Trace module ValueHistory = PulseDomain.ValueHistory +open PulseBasicInterface (* layer on top of {!PulseDomain} to propagate operations on the current state to the pre-condition when necessary diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml index 89e442eb4..ef428ef9b 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -9,3 +9,4 @@ open! IStd (** Basic Pulse modules that are safe to use in any module *) module CallEvent = PulseCallEvent +module Invalidation = PulseInvalidation diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 2d4d5ded5..0bd0df73d 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -7,7 +7,6 @@ open! IStd module F = Format -module Invalidation = PulseDomain.Invalidation module Trace = PulseDomain.Trace module ValueHistory = PulseDomain.ValueHistory open PulseBasicInterface diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 9f7652b46..dc262ddf4 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -6,9 +6,9 @@ *) open! IStd -module Invalidation = PulseDomain.Invalidation module Trace = PulseDomain.Trace module ValueHistory = PulseDomain.ValueHistory +open PulseBasicInterface (** an error to report to the user *) type t = diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 752ba5c7f..6798a727c 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -11,91 +11,6 @@ open PulseBasicInterface (* {2 Abstract domain description } *) -module Invalidation = struct - type std_vector_function = - | Assign - | Clear - | Emplace - | EmplaceBack - | Insert - | PushBack - | Reserve - | ShrinkToFit - [@@deriving compare] - - let pp_std_vector_function f = function - | Assign -> - F.fprintf f "std::vector::assign" - | Clear -> - F.fprintf f "std::vector::clear" - | Emplace -> - F.fprintf f "std::vector::emplace" - | EmplaceBack -> - F.fprintf f "std::vector::emplace_back" - | Insert -> - F.fprintf f "std::vector::insert" - | PushBack -> - F.fprintf f "std::vector::push_back" - | Reserve -> - F.fprintf f "std::vector::reserve" - | ShrinkToFit -> - F.fprintf f "std::vector::shrink_to_fit" - - - type t = - | CFree - | CppDelete - | GoneOutOfScope of Pvar.t * Typ.t - | Nullptr - | StdVector of std_vector_function - [@@deriving compare] - - let issue_type_of_cause = function - | CFree -> - IssueType.use_after_free - | CppDelete -> - IssueType.use_after_delete - | GoneOutOfScope _ -> - IssueType.use_after_lifetime - | Nullptr -> - IssueType.null_dereference - | StdVector _ -> - IssueType.vector_invalidation - - - let describe f cause = - match cause with - | CFree -> - F.pp_print_string f "was invalidated by call to `free()`" - | CppDelete -> - F.pp_print_string f "was invalidated by `delete`" - | GoneOutOfScope (pvar, typ) -> - let pp_var f pvar = - if Pvar.is_cpp_temporary pvar then - F.fprintf f "is the address of a C++ temporary of type `%a`" (Typ.pp_full Pp.text) typ - else F.fprintf f "is the address of a stack variable `%a`" Pvar.pp_value pvar - in - F.fprintf f "%a whose lifetime has ended" pp_var pvar - | Nullptr -> - F.pp_print_string f "is the null pointer" - | StdVector std_vector_f -> - F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f - - - let pp f invalidation = - match invalidation with - | CFree -> - F.fprintf f "CFree(%a)" describe invalidation - | CppDelete -> - F.fprintf f "CppDelete(%a)" describe invalidation - | GoneOutOfScope _ -> - describe f invalidation - | Nullptr -> - describe f invalidation - | StdVector _ -> - F.fprintf f "StdVector(%a)" describe invalidation -end - module ValueHistory = struct type event = | Assignment of Location.t diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 7e1d8b208..70510db2e 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -9,33 +9,6 @@ open! IStd module F = Format open PulseBasicInterface -module Invalidation : sig - type std_vector_function = - | Assign - | Clear - | Emplace - | EmplaceBack - | Insert - | PushBack - | Reserve - | ShrinkToFit - [@@deriving compare] - - val pp_std_vector_function : Format.formatter -> std_vector_function -> unit - - type t = - | CFree - | CppDelete - | GoneOutOfScope of Pvar.t * Typ.t - | Nullptr - | StdVector of std_vector_function - [@@deriving compare] - - val issue_type_of_cause : t -> IssueType.t - - val describe : Format.formatter -> t -> unit -end - module ValueHistory : sig type event = | Assignment of Location.t diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml new file mode 100644 index 000000000..2fa3441bc --- /dev/null +++ b/infer/src/pulse/PulseInvalidation.ml @@ -0,0 +1,91 @@ +(* + * 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 std_vector_function = + | Assign + | Clear + | Emplace + | EmplaceBack + | Insert + | PushBack + | Reserve + | ShrinkToFit +[@@deriving compare] + +let pp_std_vector_function f = function + | Assign -> + F.fprintf f "std::vector::assign" + | Clear -> + F.fprintf f "std::vector::clear" + | Emplace -> + F.fprintf f "std::vector::emplace" + | EmplaceBack -> + F.fprintf f "std::vector::emplace_back" + | Insert -> + F.fprintf f "std::vector::insert" + | PushBack -> + F.fprintf f "std::vector::push_back" + | Reserve -> + F.fprintf f "std::vector::reserve" + | ShrinkToFit -> + F.fprintf f "std::vector::shrink_to_fit" + + +type t = + | CFree + | CppDelete + | GoneOutOfScope of Pvar.t * Typ.t + | Nullptr + | StdVector of std_vector_function +[@@deriving compare] + +let issue_type_of_cause = function + | CFree -> + IssueType.use_after_free + | CppDelete -> + IssueType.use_after_delete + | GoneOutOfScope _ -> + IssueType.use_after_lifetime + | Nullptr -> + IssueType.null_dereference + | StdVector _ -> + IssueType.vector_invalidation + + +let describe f cause = + match cause with + | CFree -> + F.pp_print_string f "was invalidated by call to `free()`" + | CppDelete -> + F.pp_print_string f "was invalidated by `delete`" + | GoneOutOfScope (pvar, typ) -> + let pp_var f pvar = + if Pvar.is_cpp_temporary pvar then + F.fprintf f "is the address of a C++ temporary of type `%a`" (Typ.pp_full Pp.text) typ + else F.fprintf f "is the address of a stack variable `%a`" Pvar.pp_value pvar + in + F.fprintf f "%a whose lifetime has ended" pp_var pvar + | Nullptr -> + F.pp_print_string f "is the null pointer" + | StdVector std_vector_f -> + F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f + + +let pp f invalidation = + match invalidation with + | CFree -> + F.fprintf f "CFree(%a)" describe invalidation + | CppDelete -> + F.fprintf f "CppDelete(%a)" describe invalidation + | GoneOutOfScope _ -> + describe f invalidation + | Nullptr -> + describe f invalidation + | StdVector _ -> + F.fprintf f "StdVector(%a)" describe invalidation diff --git a/infer/src/pulse/PulseInvalidation.mli b/infer/src/pulse/PulseInvalidation.mli new file mode 100644 index 000000000..76eadb842 --- /dev/null +++ b/infer/src/pulse/PulseInvalidation.mli @@ -0,0 +1,36 @@ +(* + * 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 std_vector_function = + | Assign + | Clear + | Emplace + | EmplaceBack + | Insert + | PushBack + | Reserve + | ShrinkToFit +[@@deriving compare] + +val pp_std_vector_function : F.formatter -> std_vector_function -> unit + +type t = + | CFree + | CppDelete + | GoneOutOfScope of Pvar.t * Typ.t + | Nullptr + | StdVector of std_vector_function +[@@deriving compare] + +val pp : F.formatter -> t -> unit + +val issue_type_of_cause : t -> IssueType.t + +val describe : F.formatter -> t -> unit diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index fcfb51609..dfe7d323a 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -46,7 +46,7 @@ module C = struct fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(deleted_access, _)] -> - PulseOperations.invalidate location PulseDomain.Invalidation.CFree deleted_access astate + PulseOperations.invalidate location Invalidation.CFree deleted_access astate >>| List.return | _ -> Ok [astate] @@ -57,8 +57,7 @@ module Cplusplus = struct fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(deleted_access, _)] -> - PulseOperations.invalidate location PulseDomain.Invalidation.CppDelete deleted_access - astate + PulseOperations.invalidate location Invalidation.CppDelete deleted_access astate >>| List.return | _ -> Ok [astate] @@ -181,9 +180,7 @@ module StdVector = struct | (vector, _) :: _ -> let crumb = PulseDomain.ValueHistory.Call - { f= - Model - (Format.asprintf "%a()" PulseDomain.Invalidation.pp_std_vector_function vector_f) + { f= Model (Format.asprintf "%a()" Invalidation.pp_std_vector_function vector_f) ; location ; in_call= [] } in diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 344ca622b..16c205145 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -7,6 +7,7 @@ open! IStd module AbstractAddress = PulseDomain.AbstractAddress +open PulseBasicInterface type t = PulseAbductiveDomain.t @@ -70,15 +71,15 @@ val write_deref : (** write the edge [ref --*--> obj] *) val invalidate : - Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result + Location.t -> Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result (** record that the address is invalid *) val invalidate_deref : - Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result + Location.t -> Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result (** record that what the address points to is invalid *) val invalidate_array_elements : - Location.t -> PulseDomain.Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result + Location.t -> Invalidation.t -> PulseDomain.AddrTracePair.t -> t -> t access_result (** record that all the array elements that address points to is invalid *) val shallow_copy :