infer_clone/infer/src/pulse/PulseBaseDomain.mli

(*
 * 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
open PulseBasicInterface

module SkippedTrace : sig
  type t = PulseTrace.t
end

module SkippedCallsMap :
  PrettyPrintable.PPMonoMap with type key = Procname.t and type value = SkippedTrace.t

type t = {heap: PulseBaseMemory.t; stack: PulseBaseStack.t; skipped_calls_map: SkippedCallsMap.t}

val empty : t

include AbstractDomain.NoJoin with type t := t

val reachable_addresses : t -> AbstractValue.Set.t
(** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable from
    the stack variables *)

type mapping

val empty_mapping : mapping

type isograph_relation =
  | NotIsomorphic  (** no mapping was found that can make LHS the same as the RHS *)
  | IsomorphicUpTo of mapping  (** [mapping(lhs)] is isomorphic to [rhs] *)

val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation

val is_isograph : lhs:t -> rhs:t -> mapping -> bool
[pulse] initial commit Summary: New analysis in foetal form to detect invalid use of C++ objects after their lifetime has ended. For now it has: - A domain consisting of a graph of abstract locations representing the heap, a map from program variables to abstract locations representing the stack, and a set of locations known to be invalid (their lifetime has ended) - The heap graph is unfolded lazily when we resolve accesses to the heap down to an abstract location. When we traverse a memory location we check that it's not known to be invalid. - A simple transfer function reads and updates the stack and heap in a rudimentary way for now - C++ `delete` is modeled as adding the location that its argument resolves to to the set of invalid locations - Also, the domain has a really crappy join and widening for now (see comments in the code) With this we already pass most of the "use after delete" tests from the Ownership checker. The ones we don't pass are only because we are missing models. Reviewed By: mbouaziz Differential Revision: D10383249 fbshipit-source-id: f414664cb 6 years ago			`(*`
[copyright] Remove years Reviewed By: jvillard Differential Revision: D15771884 fbshipit-source-id: e2997e3a3 6 years ago			`* Copyright (c) Facebook, Inc. and its affiliates.`
[pulse] initial commit Summary: New analysis in foetal form to detect invalid use of C++ objects after their lifetime has ended. For now it has: - A domain consisting of a graph of abstract locations representing the heap, a map from program variables to abstract locations representing the stack, and a set of locations known to be invalid (their lifetime has ended) - The heap graph is unfolded lazily when we resolve accesses to the heap down to an abstract location. When we traverse a memory location we check that it's not known to be invalid. - A simple transfer function reads and updates the stack and heap in a rudimentary way for now - C++ `delete` is modeled as adding the location that its argument resolves to to the set of invalid locations - Also, the domain has a really crappy join and widening for now (see comments in the code) With this we already pass most of the "use after delete" tests from the Ownership checker. The ones we don't pass are only because we are missing models. Reviewed By: mbouaziz Differential Revision: D10383249 fbshipit-source-id: f414664cb 6 years ago			`*`
			`* This source code is licensed under the MIT license found in the`
			`* LICENSE file in the root directory of this source tree.`
			`*)`

			`open! IStd`
[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 5 years ago			`open PulseBasicInterface`
[pulse] allow models in invalidation traces Summary: Be more flexible in what type of function calls are allowed in `ViaCall ...` actions to be able to include models. Also get rid of `here here` in traces /o\ As a side-effect, get more precise (=qualified) procedure names in traces (but not in messages so as not to be too verbose). Reviewed By: mbouaziz, ngorogiannis Differential Revision: D16121092 fbshipit-source-id: fb51b02f8 5 years ago
[pulse] Track skipped functions Summary: Let's collect the list of all skipped functions with a `proc_name` but no summary in Pulse's memory. This will be useful for the impurity analysis later (next diff). Concretely, we extend Pulse's domain with a map from skipped calls to their respective traces. For efficiency, we only keep a single trace per skipped call. For impurity analysis, tracking skipped calls in Pulse allows us to rely on Pulse's strong memory model to get rid of infeasible paths as opposed to creating an independent checker which wouldn't be able to do that. Reviewed By: jvillard Differential Revision: D19428426 fbshipit-source-id: 3c5e482c5 5 years ago			`module SkippedTrace : sig`
			`type t = PulseTrace.t`
			`end`

			`module SkippedCallsMap :`
			`PrettyPrintable.PPMonoMap with type key = Procname.t and type value = SkippedTrace.t`

			`type t = {heap: PulseBaseMemory.t; stack: PulseBaseStack.t; skipped_calls_map: SkippedCallsMap.t}`
[pulse] add traces to the domain Summary: Record per-location traces. Actually, that doesn't quite make sense as a location can be accessed in many ways, so associate a trace to each edge in the memory graph. For instance, when doing `x->f = y`, we want to take the history of the `<val of y> ----> ..` edge, add "assigned at location blah" to it and store this extended history to the edge `<val of x> --f--> ..`. Use this machinery to print nicer traces in `infer explore` and better error messages too (include the last assignment, like biabduction messages). Reviewed By: da319 Differential Revision: D13518668 fbshipit-source-id: 0a62fb55f 6 years ago
[pulse][interproc 2/3] abductive domain Summary: For each operation on the domain, try to record what it requires of the precondition of the function. This is akin to what happens in the biabduction backend, hence the terminology used. Reviewed By: jberdine Differential Revision: D14387148 fbshipit-source-id: a61fe30c8 6 years ago			`val empty : t`
[pulse] detect stack variable address escape Summary: When assign to the special `return` variable, check that the result is not the address of a local variable, otherwise report. Reviewed By: ngorogiannis Differential Revision: D13466896 fbshipit-source-id: 465da7f13 6 years ago
[pulse] remove last traces of join/widen Summary: Instead of defining `let join .. = assert false` introduce simplified module signatures for domains without join/widen as used in disjunctive domains. Reviewed By: mbouaziz, skcho Differential Revision: D14568271 fbshipit-source-id: 6484335c9 6 years ago			`include AbstractDomain.NoJoin with type t := t`
[pulse] collect garbage (unreachable) heap parts from time to time Summary: It's useful to keep the size of states down, especially when humans are trying to read it. It will also help keep the size of summaries down in the inter-procedural pulse. Reviewed By: mbouaziz Differential Revision: D14258486 fbshipit-source-id: 45ebcac67 6 years ago
[pulse][6/9] add PulseAbstractValue to PulseBasicInterface Summary: See explanations in D17955104. This renames `AbstractAddress` to `AbstractValue` since they are not necessarily addresses. Reviewed By: ezgicicek Differential Revision: D17955290 fbshipit-source-id: 8bb4c61f2 5 years ago			`val reachable_addresses : t -> AbstractValue.Set.t`
[ocamlformat] Enable parsing and reformatting docstrings Summary: This diff enables parsing and auto-formatting documentation comments (aka docstrings). I have looked at this entire diff and manually made some changes to improve the formatting. In some cases it looked like it would take too much time, or benefit from someone more familiar with the code doing it, and I instead disabled auto-formatting docstrings in those files. Also, there are some source files where the docstrings are invalid, and some where the structure detected by the parser appears not to match what was intended. Auto-formatting has been disabled for these files. Reviewed By: ezgicicek Differential Revision: D18755888 fbshipit-source-id: 68d72465d 5 years ago			`(** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable from`
			`the stack variables *)`
[pulse][interproc 2/3] abductive domain Summary: For each operation on the domain, try to record what it requires of the precondition of the function. This is akin to what happens in the biabduction backend, hence the terminology used. Reviewed By: jberdine Differential Revision: D14387148 fbshipit-source-id: a61fe30c8 6 years ago
			`type mapping`

			`val empty_mapping : mapping`

			`type isograph_relation =`
			`\| NotIsomorphic (** no mapping was found that can make LHS the same as the RHS *)`
			`\| IsomorphicUpTo of mapping (** [mapping(lhs)] is isomorphic to [rhs] *)`

			`val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation`

			`val is_isograph : lhs:t -> rhs:t -> mapping -> bool`