Module Pulselib.PulseValueHistory

module F = Stdlib.Format
module CallEvent = PulseCallEvent
module TaintItem = PulseTaintItem
module Timestamp = PulseTimestamp
module CellId : sig ... end

Used to identify which cells (places in the memory) in the current precondition are mentioned in a value history in the current abstract state, i.e. were used to compute that value.

type event =
  1. | Allocation of {
    1. f : CallEvent.t;
    2. location : IBase.Location.t;
    3. timestamp : Timestamp.t;
    }
  2. | Assignment of IBase.Location.t * Timestamp.t
  3. | Call of {
    1. f : CallEvent.t;
    2. location : IBase.Location.t;
    3. in_call : t;
    4. timestamp : Timestamp.t;
    }
  4. | Capture of {
    1. captured_as : IR.Pvar.t;
    2. mode : IR.CapturedVar.capture_mode;
    3. location : IBase.Location.t;
    4. timestamp : Timestamp.t;
    }
  5. | ConditionPassed of {
    1. if_kind : IR.Sil.if_kind;
    2. is_then_branch : bool;
    3. location : IBase.Location.t;
    4. timestamp : Timestamp.t;
    }
  6. | CppTemporaryCreated of IBase.Location.t * Timestamp.t
  7. | FormalDeclared of IR.Pvar.t * IBase.Location.t * Timestamp.t
  8. | Invalidated of PulseInvalidation.t * IBase.Location.t * Timestamp.t
  9. | NilMessaging of IBase.Location.t * Timestamp.t
  10. | Returned of IBase.Location.t * Timestamp.t
  11. | StructFieldAddressCreated of IR.Fieldname.t IStdlib.RevList.t * IBase.Location.t * Timestamp.t
  12. | TaintSource of TaintItem.t * IBase.Location.t * Timestamp.t
  13. | TaintPropagated of IBase.Location.t * Timestamp.t
  14. | VariableAccessed of IR.Pvar.t * IBase.Location.t * Timestamp.t
  15. | VariableDeclared of IR.Pvar.t * IBase.Location.t * Timestamp.t
and t = private
  1. | Epoch
    (*

    start of time

    *)
  2. | Sequence of event * t
    (*

    Sequence [event, hist] represents an event event occurring *after* hist. Invariant: the timestamp of event is greater than all the (local, i.e. not inside function calls) timestamps in hist.

    *)
  3. | InContext of {
    1. main : t;
      (*

      trace of the "main" value being traced

      *)
    2. context : t list;
      (*

      contextual traces, eg conditionals that the path is under

      *)
    }
  4. | BinaryOp of IR.Binop.t * t * t
    (*

    branch history due to a binop

    *)
  5. | FromCellIds of CellId.Set.t * t
    (*

    the set of cells that this were used in this history; used in particular in summary application to know which caller value histories should be pre-pended to a callee value history

    *)
  6. | Multiplex of t list
    (*

    interlace multiple histories together

    *)
  7. | UnknownCall of {
    1. f : CallEvent.t;
    2. actuals : t list;
    3. location : IBase.Location.t;
    4. timestamp : Timestamp.t;
    }
val compare_event : event -> event -> int
val compare : t -> t -> int
val equal_event : event -> event -> bool
val equal : t -> t -> bool
val yojson_of_event : event -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val epoch : t
val sequence : ?context:t list -> event -> t -> t
val in_context : t list -> t -> t
val binary_op : IR.Binop.t -> t -> t -> t
val from_cell_id : CellId.t -> t -> t
val unknown_call : CallEvent.t -> t list -> IBase.Location.t -> Timestamp.t -> t
val pp : F.formatter -> t -> unit
val pp_fields : F.formatter -> IR.Fieldname.t IStdlib.RevList.t -> unit
val singleton : event -> t
val get_cell_ids : t -> CellId.Set.t option
val get_cell_id_exn : t -> CellId.t option

same as get_cell_ids but assumes the resulting set is a singleton

val of_cell_ids_in_map : t CellId.Map.t -> CellId.Set.t -> t option

multiplex of the histories corresponding to the given cell ids according to the cell id map provided; None if there are no such histories to multiplex together

type iter_event =
  1. | EnterCall of CallEvent.t * IBase.Location.t
  2. | ReturnFromCall of CallEvent.t * IBase.Location.t
  3. | Event of event
val rev_iter_main : t -> f:(iter_event -> unit) -> unit

iterate on all events in reverse timestamp order, ignoring events in contexts and recursing into the histories inside call events. Timestamp order is the lexicographic order induced by projecting events onto their timestamps and appending timestamps within calls, e.g. the timestamp of the inner assignement in

Call {timestamp=10; in_call=[..., Call{timestamp=4;
in_call=[..., Assignement (...,timestamp=3) ] } ] }

can be written 10.4.3 and the order is such that, e.g., 10.4.3 < 10.5, 10.5 being the timestamp of the event following the inner Call event in the example above.

val iter : main_only:bool -> t -> f:(iter_event -> unit) -> unit

like rev_iter_main but iterates in order (by reversing the order iteration) and iterates on only main events like rev_iter_main if main_only is true, otherwise iterates on *all* events including contexts if main_only is false

val location_of_event : event -> IBase.Location.t
val timestamp_of_event : event -> Timestamp.t
val add_to_errlog : ?include_taint_events:bool -> nesting:int -> t -> Absint.Errlog.loc_trace_elem list -> Absint.Errlog.loc_trace_elem list
val get_first_main_event : t -> event option
val exists_main : t -> f:(event -> bool) -> bool