package pds-reachability

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

Signature

include Pds_reachability_types.Types with module State = Basis.State with module Stack_element = Basis.Stack_element with module Targeted_dynamic_pop_action = Dph.Targeted_dynamic_pop_action with module Untargeted_dynamic_pop_action = Dph.Untargeted_dynamic_pop_action with module Stack_action = Dph.Stack_action with module Terminus = Dph.Terminus
module State = Basis.State

The decorated type of states in the PDS.

module Stack_element = Basis.Stack_element

The decorated type of stack elements in the PDS.

The type of classes of states in the PDS.

module Targeted_dynamic_pop_action = Dph.Targeted_dynamic_pop_action

The decorated type of targeted dynamic pop actions in the PDS.

module Untargeted_dynamic_pop_action = Dph.Untargeted_dynamic_pop_action

The decorated type of untargeted dynamic pop actions in the PDS.

module Stack_action = Dph.Stack_action

Stack actions which may be performed in the PDS.

module Terminus = Dph.Terminus

Termini of paths which may exist in the PDS.

type intermediate_destination =
  1. | Static_destination of node
  2. | Dynamic_destination of Untargeted_dynamic_pop_action.t
and node =
  1. | State_node of State.t
  2. | Intermediate_node of intermediate_destination * Stack_action.t list

The decorated type of node used for reachability.

type edge = {
  1. source : Node.t;
  2. target : Node.t;
  3. edge_action : Stack_action.t;
}

The decorated type of edge used in reachability.

type edge_function = State.t -> (Stack_action.t list * Terminus.t) Batteries.Enum.t

The type of edge-generating functions used in this analysis.

type untargeted_dynamic_pop_action_function = State.t -> Untargeted_dynamic_pop_action.t Batteries.Enum.t

The type of functions to generate untargeted dynamic pop actions in this analysis.

type analysis

The type of a reachability analysis in this module.

type analysis_logging_function = analysis -> analysis -> unit

The type of reachability analysis logging functions. These functions are called whenever the associated analysis is stepped. The two arguments are the analysis before stepping and the analysis after.

val empty : ?logging_function:analysis_logging_function option -> unit -> analysis

The empty analysis. This analysis has no states, edges, or edge functions.

val add_edge : State.t -> Stack_action.t list -> State.t -> analysis -> analysis

Adds a single edge to a reachability analysis.

val add_edge_function : edge_function -> analysis -> analysis

Adds a function to generate edges for a reachability analysis. Given a source node, the function generates edges from that source node. The function must be pure; for a given source node, it must generate all edges that it can generate on the first call. This routine will be called on all nodes that are introduced to the PDS.

val add_classified_edge_function : Class.t -> edge_function -> analysis -> analysis

Adds a function to generate edges for a reachability analysis on states with the specified class. This routine operates as add_edge_function except that the provided function will *not* be called on nodes which have a different class.

val add_untargeted_dynamic_pop_action : State.t -> Untargeted_dynamic_pop_action.t -> analysis -> analysis

Adds an untargeted pop action to a reachability analysis. Untargeted pop action are similar to targeted pop actions except that they are not created as an edge with a target node; instead, the target is decided in some way by the pushed element that the untargeted dynamic pop is consuming.

val add_untargeted_dynamic_pop_action_function : untargeted_dynamic_pop_action_function -> analysis -> analysis

Adds a function to generate untargeted dynamic pop ations for a reachability analysis. Given a source node, the function generates untargeted actions from that source node. The function must be pure; for a given source, it must generate all actions that it can generate on the first call.

val add_classified_untargeted_dynamic_pop_action_function : Class.t -> untargeted_dynamic_pop_action_function -> analysis -> analysis

Adds a function to generate untargeted dynamic pop ations for a reachability analysis for nodes of a particular class. This routine works as add_untargeted_dynamic_pop_action_function but only invokes the provided function on nodes of a particular class.

val add_start_state : State.t -> Stack_action.t list -> analysis -> analysis

Adds a state and initial stack element to the analysis. This permits the state to be used as the source state of a call to get_reachable_states.

val is_closed : analysis -> bool

Determines whether the reachability analysis is closed.

val closure_step : analysis -> analysis

Takes a step toward closing a given reachability analysis. If the analysis is already closed, it is returned unchanged.

val closure_step_reachable : analysis -> analysis * (State.t * Stack_action.t list * State.t) option Stdlib.Lazy.t

Takes a step toward closing a given reachability analysis. If the analysis is already closed, it is returned unchanged. If a start state is found to reach another state, that pair of states will be returned in a lazy computation.

val fully_close : analysis -> analysis

Fully closes the provided analysis.

val get_reachable_states : State.t -> Stack_action.t list -> analysis -> State.t Batteries.Enum.t

Determines the states which are reachable from a given state and initial stack element. This state must have been added to the analysis previously. If the analysis is not fully closed, then the enumeration of reachable states may be incomplete.

Pretty-printing function for the analysis.

val show_analysis : analysis -> string
exception Reachability_request_for_non_start_state of State.t

An exception raised when a reachable state query occurs before the state is added as a start state.

val get_size : analysis -> int * int

Determines the size of the provided analysis in terms of both node and edge count (respectively).

val get_work_count : analysis -> int

Determines the amount of work done on a particular analysis.

val dump_yojson : analysis -> Yojson.Safe.t

Extracts a subset of information about an analysis state as JSON data. Some parts of the analysis state (such as edge functions) will be elided as they cannot be represented.

val dump_yojson_delta : analysis -> analysis -> Yojson.Safe.t

Extracts a subset of information about an analysis state as JSON data. This extraction generates a /difference/ between two reachability analyses, giving values appearing in the latter but not the former. This function assumes the latter is a strict superset of the former; any values appearing in the former and not the latter are ignored. The format of this dump is identical to that given by dump_yojson.

OCaml

Innovation. Community. Security.