pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[pulse][2/9] add PulseInvalidation to PulseBasicInterface

Browse Source 
Summary: See explanations in D17955104

Reviewed By: ezgicicek

Differential Revision: D17955286

fbshipit-source-id: 831491e47
master
Jules Villard 5 years ago committed by Facebook Github Bot
parent c909d6bd7e
commit 168237a605
14 changed files with 141 additions and 129 deletions
Show Stats Download Patch File Download Diff File

4
infer/src/checkers/impurityDomain.ml
Unescape View File

@ -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

2
infer/src/checkers/impurityDomain.mli
Unescape View File

@ -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

2
infer/src/pulse/Pulse.ml
Unescape View File

@ -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

1
infer/src/pulse/PulseAbductiveDomain.ml
Unescape View File

@ -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

2
infer/src/pulse/PulseAbductiveDomain.mli
Unescape View File

@ -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

1
infer/src/pulse/PulseBasicInterface.ml
Unescape View File

@ -9,3 +9,4 @@ open! IStd
(** Basic Pulse modules that are safe to use in any module *)
module CallEvent = PulseCallEvent
module Invalidation = PulseInvalidation

1
infer/src/pulse/PulseDiagnostic.ml
Unescape View File

@ -7,7 +7,6 @@
open! IStd
module F = Format
module Invalidation = PulseDomain.Invalidation
module Trace = PulseDomain.Trace
module ValueHistory = PulseDomain.ValueHistory
open PulseBasicInterface

2
infer/src/pulse/PulseDiagnostic.mli
Unescape View File

@ -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 =

85
infer/src/pulse/PulseDomain.ml
Unescape View File

@ -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

27
infer/src/pulse/PulseDomain.mli
Unescape View File

@ -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

91
infer/src/pulse/PulseInvalidation.ml
Unescape View File

@ -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

36
infer/src/pulse/PulseInvalidation.mli
Unescape View File

@ -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

9
infer/src/pulse/PulseModels.ml
Unescape View File

@ -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

7
infer/src/pulse/PulseOperations.mli
Unescape View File

@ -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 :

Write Preview
Loading…
Cancel
Save