From 512b42ece7ddbce32e5bfa6e36e2ad2c6717a657 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 18 Jun 2019 09:17:13 -0700 Subject: [PATCH] [pulse] move PulseInvalidation inside PulseDomain Summary: Just moving code around. This is needed later to make some types in `PulseInvalidation` depend on a new type that I'll have to define in `PulseDomain`. Reviewed By: mbouaziz Differential Revision: D15824962 fbshipit-source-id: 86cba2bfb --- infer/src/pulse/PulseAbductiveDomain.mli | 7 +- infer/src/pulse/PulseDiagnostic.ml | 12 ++-- infer/src/pulse/PulseDiagnostic.mli | 2 +- infer/src/pulse/PulseDomain.ml | 87 +++++++++++++++++++++- infer/src/pulse/PulseDomain.mli | 33 ++++++++- infer/src/pulse/PulseInvalidation.ml | 92 ------------------------ infer/src/pulse/PulseInvalidation.mli | 34 --------- infer/src/pulse/PulseModels.ml | 10 +-- infer/src/pulse/PulseOperations.mli | 4 +- 9 files changed, 137 insertions(+), 144 deletions(-) delete mode 100644 infer/src/pulse/PulseInvalidation.ml delete mode 100644 infer/src/pulse/PulseInvalidation.mli diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 779f31f3d..30312e980 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -46,14 +46,17 @@ module Memory : sig HilExp.AccessExpression.t PulseTrace.action -> AbstractAddress.t -> t - -> (t, PulseInvalidation.t PulseTrace.t) result + -> (t, PulseDomain.Invalidation.t PulseTrace.t) result val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t val invalidate : - AbstractAddress.t * PulseTrace.breadcrumbs -> PulseInvalidation.t PulseTrace.action -> t -> t + AbstractAddress.t * PulseTrace.breadcrumbs + -> PulseDomain.Invalidation.t PulseTrace.action + -> t + -> t val is_std_vector_reserved : AbstractAddress.t -> t -> bool diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index e459b7ce8..85e45cc6d 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -11,7 +11,7 @@ module F = Format type t = | AccessToInvalidAddress of { access: HilExp.AccessExpression.t - ; invalidated_by: PulseInvalidation.t PulseTrace.t + ; invalidated_by: PulseDomain.Invalidation.t PulseTrace.t ; accessed_by: HilExp.AccessExpression.t PulseTrace.t } | StackVariableAddressEscape of { variable: Var.t @@ -86,10 +86,10 @@ let get_message = function let pp_invalidation_trace line f trace = match trace.PulseTrace.action with | Immediate {imm= invalidation; _} -> - F.fprintf f "%a on line %d" PulseInvalidation.describe invalidation line + F.fprintf f "%a on line %d" PulseDomain.Invalidation.describe invalidation line | ViaCall {action; proc_name; _} -> F.fprintf f "%a on line %d indirectly during the call to `%a`" - PulseInvalidation.describe + PulseDomain.Invalidation.describe (PulseTrace.immediate_of_action action) line Typ.Procname.describe proc_name in @@ -112,7 +112,8 @@ let get_message = function let get_trace = function | AccessToInvalidAddress {accessed_by; invalidated_by} -> PulseTrace.add_to_errlog ~header:"invalidation part of the trace starts here" - (fun f invalidation -> F.fprintf f "memory %a" PulseInvalidation.describe invalidation) + (fun f invalidation -> + F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation ) invalidated_by @@ PulseTrace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here" (fun f access -> F.fprintf f "invalid access to `%a`" HilExp.AccessExpression.pp access) @@ -127,6 +128,7 @@ let get_trace = function let get_issue_type = function | AccessToInvalidAddress {invalidated_by} -> - PulseTrace.immediate_of_action invalidated_by.action |> PulseInvalidation.issue_type_of_cause + PulseTrace.immediate_of_action invalidated_by.action + |> PulseDomain.Invalidation.issue_type_of_cause | StackVariableAddressEscape _ -> IssueType.stack_variable_address_escape diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index de72dbcdc..8b043868d 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -11,7 +11,7 @@ open! IStd type t = | AccessToInvalidAddress of { access: HilExp.AccessExpression.t - ; invalidated_by: PulseInvalidation.t PulseTrace.t + ; invalidated_by: PulseDomain.Invalidation.t PulseTrace.t ; accessed_by: HilExp.AccessExpression.t PulseTrace.t } | StackVariableAddressEscape of { variable: Var.t diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index d54bc5b81..8548b2110 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -7,10 +7,95 @@ open! IStd module F = Format module L = Logging -module Invalidation = PulseInvalidation (* {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 of HilExp.AccessExpression.t + | CppDelete of HilExp.AccessExpression.t + | GoneOutOfScope of Pvar.t * Typ.t + | Nullptr + | StdVector of std_vector_function * HilExp.AccessExpression.t + [@@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 = function + | CFree access_expr -> + F.fprintf f "was invalidated by call to `free()` on `%a`" HilExp.AccessExpression.pp + access_expr + | CppDelete access_expr -> + F.fprintf f "was invalidated by `delete` on `%a`" HilExp.AccessExpression.pp access_expr + | 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.fprintf f "is the null pointer" + | StdVector (std_vector_f, access_expr) -> + F.fprintf f "was potentially invalidated by `%a()` on `%a`" pp_std_vector_function + std_vector_f HilExp.AccessExpression.pp access_expr + + + 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 + (** Purposefully declared before [AbstractAddress] to avoid attributes depending on addresses. Otherwise they become a pain to handle when comparing memory states. *) module Attribute = struct diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index a84a73d5b..229267b35 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -8,9 +8,36 @@ open! IStd module F = Format +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 of HilExp.AccessExpression.t + | CppDelete of HilExp.AccessExpression.t + | GoneOutOfScope of Pvar.t * Typ.t + | Nullptr + | StdVector of std_vector_function * HilExp.AccessExpression.t + [@@deriving compare] + + val issue_type_of_cause : t -> IssueType.t + + val describe : Format.formatter -> t -> unit +end + module Attribute : sig type t = - | Invalid of PulseInvalidation.t PulseTrace.t + | Invalid of Invalidation.t PulseTrace.t | MustBeValid of HilExp.AccessExpression.t PulseTrace.action | AddressOfCppTemporary of Var.t * Location.t option | Closure of Typ.Procname.t @@ -94,9 +121,9 @@ module Memory : sig val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t val invalidate : - AbstractAddress.t * PulseTrace.breadcrumbs -> PulseInvalidation.t PulseTrace.action -> t -> t + AbstractAddress.t * PulseTrace.breadcrumbs -> Invalidation.t PulseTrace.action -> t -> t - val check_valid : AbstractAddress.t -> t -> (unit, PulseInvalidation.t PulseTrace.t) result + val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t PulseTrace.t) result val std_vector_reserve : AbstractAddress.t -> t -> t diff --git a/infer/src/pulse/PulseInvalidation.ml b/infer/src/pulse/PulseInvalidation.ml deleted file mode 100644 index 303235ece..000000000 --- a/infer/src/pulse/PulseInvalidation.ml +++ /dev/null @@ -1,92 +0,0 @@ -(* - * 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 of HilExp.AccessExpression.t - | CppDelete of HilExp.AccessExpression.t - | GoneOutOfScope of Pvar.t * Typ.t - | Nullptr - | StdVector of std_vector_function * HilExp.AccessExpression.t -[@@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 = function - | CFree access_expr -> - F.fprintf f "was invalidated by call to `free()` on `%a`" HilExp.AccessExpression.pp - access_expr - | CppDelete access_expr -> - F.fprintf f "was invalidated by `delete` on `%a`" HilExp.AccessExpression.pp access_expr - | 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.fprintf f "is the null pointer" - | StdVector (std_vector_f, access_expr) -> - F.fprintf f "was potentially invalidated by `%a()` on `%a`" pp_std_vector_function - std_vector_f HilExp.AccessExpression.pp access_expr - - -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 deleted file mode 100644 index dc5242301..000000000 --- a/infer/src/pulse/PulseInvalidation.mli +++ /dev/null @@ -1,34 +0,0 @@ -(* - * 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 - -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 of HilExp.AccessExpression.t - | CppDelete of HilExp.AccessExpression.t - | GoneOutOfScope of Pvar.t * Typ.t - | Nullptr - | StdVector of std_vector_function * HilExp.AccessExpression.t -[@@deriving compare] - -val issue_type_of_cause : t -> IssueType.t - -val describe : Format.formatter -> t -> unit - -val pp : Format.formatter -> t -> unit diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index b83eacc26..09bac586e 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -26,7 +26,7 @@ module C = struct match actuals with | [AccessExpression deleted_access] -> PulseOperations.invalidate - (PulseTrace.Immediate {imm= PulseInvalidation.CFree deleted_access; location}) + (PulseTrace.Immediate {imm= PulseDomain.Invalidation.CFree deleted_access; location}) location deleted_access astate >>| List.return | _ -> @@ -41,7 +41,7 @@ module Cplusplus = struct match actuals with | [AccessExpression deleted_access] -> PulseOperations.invalidate - (PulseTrace.Immediate {imm= PulseInvalidation.CppDelete deleted_access; location}) + (PulseTrace.Immediate {imm= PulseDomain.Invalidation.CppDelete deleted_access; location}) location deleted_access astate >>| List.return | _ -> @@ -104,7 +104,7 @@ module StdVector = struct let array_address = to_internal_array vector in let array = deref_internal_array vector in let invalidation = - PulseTrace.Immediate {imm= PulseInvalidation.StdVector (vector_f, vector); location} + PulseTrace.Immediate {imm= PulseDomain.Invalidation.StdVector (vector_f, vector); location} in PulseOperations.invalidate_array_elements invalidation location array astate >>= PulseOperations.invalidate invalidation location array @@ -117,7 +117,9 @@ module StdVector = struct | AccessExpression vector :: _ -> let crumb = PulseTrace.Call - { f= `Model (Format.asprintf "%a" PulseInvalidation.pp_std_vector_function vector_f) + { f= + `Model + (Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f) ; actuals ; location } in diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index f2adc8ee0..5b1a8c9be 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -62,14 +62,14 @@ val write : -> t access_result val invalidate : - PulseInvalidation.t PulseTrace.action + PulseDomain.Invalidation.t PulseTrace.action -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result val invalidate_array_elements : - PulseInvalidation.t PulseTrace.action + PulseDomain.Invalidation.t PulseTrace.action -> Location.t -> HilExp.AccessExpression.t -> t