infer_clone/infer/src/pulse/PulseAbductiveDomain.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 BaseAddressAttributes = PulseBaseAddressAttributes
module BaseDomain = PulseBaseDomain
module BaseMemory = PulseBaseMemory
module BaseStack = PulseBaseStack

(* layer on top of {!BaseDomain} to propagate operations on the current state to the pre-condition
   when necessary

   The abstract type [t] is a pre/post pair in the style of biabduction.
*)

include AbstractDomain.NoJoin

val mk_initial : Procdesc.t -> t

(** stack operations like {!BaseStack} but that also take care of propagating facts to the
    precondition *)
module Stack : sig
  val add : Var.t -> BaseStack.value -> t -> t

  val remove_vars : Var.t list -> t -> t

  val fold : (Var.t -> BaseStack.value -> 'a -> 'a) -> t -> 'a -> 'a

  val find_opt : Var.t -> t -> BaseStack.value option

  val eval : ValueHistory.t -> Var.t -> t -> t * (AbstractValue.t * ValueHistory.t)
  (** return the value of the variable in the stack or create a fresh one if needed *)

  val mem : Var.t -> t -> bool

  val exists : (Var.t -> BaseStack.value -> bool) -> t -> bool
end

(** memory operations like {!BaseMemory} but that also take care of propagating facts to the
    precondition *)
module Memory : sig
  module Access = BaseMemory.Access
  module Edges = BaseMemory.Edges

  val add_edge :
       AbstractValue.t * ValueHistory.t
    -> Access.t
    -> AbstractValue.t * ValueHistory.t
    -> Location.t
    -> t
    -> t

  val eval_edge :
    AbstractValue.t * ValueHistory.t -> Access.t -> t -> t * (AbstractValue.t * ValueHistory.t)
  (** [eval_edge (addr,hist) access astate] follows the edge [addr --access--> .] in memory and
      returns what it points to or creates a fresh value if that edge didn't exist. *)

  val find_opt : AbstractValue.t -> t -> BaseMemory.Edges.t option

  val find_edge_opt : AbstractValue.t -> Access.t -> t -> (AbstractValue.t * ValueHistory.t) option
end

(** attribute operations like {!BaseAddressAttributes} but that also take care of propagating facts
    to the precondition *)
module AddressAttributes : sig
  val abduce_attribute : AbstractValue.t -> Attribute.t -> t -> t
  (** add the attribute to the pre, if meaningful (does not modify the post) *)

  val add_one : AbstractValue.t -> Attribute.t -> t -> t
  (** add the attribute only to the post *)

  val check_valid : Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t * Trace.t) result

  val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t

  val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t

  val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option

  val is_std_vector_reserved : AbstractValue.t -> t -> bool

  val std_vector_reserve : AbstractValue.t -> t -> t

  val get_citv : AbstractValue.t -> t -> (CItv.t * Trace.t) option

  val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t

  val find_opt : AbstractValue.t -> t -> Attributes.t option
end

val is_local : Var.t -> t -> bool

val find_post_cell_opt : AbstractValue.t -> t -> BaseDomain.cell option

val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t

module SkippedTrace : sig
  type t = PulseTrace.t
end

module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t

val discard_unreachable : t -> t * BaseAddressAttributes.t
(** [discard_unreachable astate] garbage collects unreachable addresses in the state to make it
    smaller, and retuns the new state and the attributes of discarded addresses *)

val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t

val leq : lhs:t -> rhs:t -> bool

val pp : Format.formatter -> t -> unit

val of_post : Procdesc.t -> t -> t

val get_pre : t -> BaseDomain.t

val get_post : t -> BaseDomain.t

val get_skipped_calls : t -> SkippedCalls.t

val apply :
     Procname.t
  -> Location.t
  -> t
  -> formals:Var.t list
  -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
  -> t
  -> ((t * (AbstractValue.t * ValueHistory.t) option) option, Diagnostic.t * t) result
(** return the abstract state after the call along with an optional return value, or [None] if the
    precondition could not be satisfied (e.g. some aliasing constraints were not satisfied) *)