Module Analysis

Interface between strategy and low-level analysis

An analysis distinguishes exactly one system as the top system, and looks at its properties and its contract. Subsystems are view either as abstract with their contract or as concrete with their implementations.

The result of an analysis indicates which properties of the top system are invariant, whether the system conforms to its contract and whether it conforms to the preconditions of all its subsystems.

Values of type param are produced by a strategy and parameterize the input-specific transitions system generators, in particular the slicing ot the cone of influence.

Values of type result are produced by running an analysis of a generated transition system. The accumulated results are used by a strategey to decide the next steps.

NB: The uid stored in an info must be unique because it is used during transition system generation to avoid name clashes in UFs and svars.

val get_uid : unit -> int

Provides a different id every time.

type assumptions = Invs.t Scope.Map.t

Type of scope-wise assumptions.

val assumptions_empty : assumptions

Empty assumptions.

val assumptions_merge : assumptions -> assumptions -> assumptions

Merges two assumptions.

val assumptions_of_sys : TransSys.t -> assumptions

Assumptions of a transition system.

val assumptions_fold : ('a -> Scope.t -> Invs.t -> 'a) -> 'a -> assumptions -> 'a

Fold over assumptions.

type info = {
  1. top : Scope.t;
    (*

    The top system for the analysis run

    *)
  2. uid : int;
    (*

    UID for the analysis.

    *)
  3. abstraction_map : bool Scope.Map.t;
    (*

    Systems flagged true are to be represented abstractly, those flagged false are to be represented by their implementation.

    *)
  4. assumptions : assumptions;
    (*

    Properties that can be assumed invariant in subsystems

    *)
  5. unrollings : int Scope.Map.t;
    (*

    The number of times the body of each recursive function is unrolled along a chain of recursive calls, once when the function is not in the map. In a compositional analysis, the calls past the unrollings are abstracted by the contract of the function, and a refinement adds an unrolling (see Strategy); in any other analysis they are left unconstrained, and an unrolling is added when a counterexample reaches one (see RecUnrolling).

    *)
  6. terminating : Lib.position list Scope.Map.t;
    (*

    The recursive functions whose own analysis proved valid every termination check it had, each with the positions of the calls of those checks, which are looked up by call: a call whose checks the analysis did not have is not taken as terminating. In a compositional and modular analysis, a call to one of them at constant arguments is evaluated, and its value given to the solver, when the checks of all its recursive calls are among them (see LustreTransSys).

    *)
  7. learned : (UfSymbol.t * Term.t list * Term.t) list;
    (*

    Values of calls to recursive functions, each a functional symbol of an output of the function with the concrete arguments of the call and its value, that earlier analyses of the top system evaluated while checking their counterexamples, which these values showed to be spurious (see RecUnrolling.check_abstractions). Those of the functions proved terminating (see terminating) are given to the solver as facts (see LustreTransSys), so that a refinement knows them without unrolling the functions as deep as the calls go.

    *)
}

Information for the creation of a transition system

val shrink_info_to_sys : info -> TransSys.t -> info

Shrinks an abstraction map to the subsystems of a system.

type param =
  1. | Interpreter of info
    (*

    Simulation of a system

    *)
  2. | ContractCheck of info
    (*

    Analysis of the contract of a system.

    *)
  3. | First of info
    (*

    First analysis of a system.

    *)
  4. | Refinement of info * result
    (*

    Refinement of a system. Store the result of the previous analysis.

    *)
  5. | ContractMonitor of info

Parameter of an analysis.

and result = {
  1. param : param;
    (*

    Parameters of the analysis.

    *)
  2. time : float;
    (*

    Runtime of the analysis.

    *)
  3. sys : TransSys.t;
    (*

    System analyzed, contains property statuses and invariants.

    *)
  4. contract_valid : bool option;
    (*

    None if system analyzed has not contracts, Some true if it does and they have been proved correct, Some false if it does and some are unknown / falsified.

    *)
  5. requirements_valid : bool option;
    (*

    None if system analyzed has not sub-requirements, Some true if it does and they have been proved correct, Some false if it does and some are unknown / falsified.

    *)
  6. genuine : string list;
    (*

    The properties falsified by a counterexample that the recursive functions as they are violate, rather than their contracts that abstract them in the system (see RecUnrolling.check_abstractions): refining the recursive functions cannot prove them.

    *)
  7. learned : (UfSymbol.t * Term.t list * Term.t) list;
    (*

    The values of calls to recursive functions that the checks of the counterexamples of the analysis evaluated, when they showed a counterexample to be spurious (see info.learned).

    *)
}

Result of analysing a transistion system

val info_clone : info -> info

Clones an info, only changes its uid.

val map_info : (info -> info) -> param -> param

Applies a function to the info of a param.

val param_clone : param -> param

Clones a param, only changes its uid.

val info_of_param : param -> info

The info or a param.

val shrink_param_to_sys : param -> TransSys.t -> param

Shrinks a param to a system.

val param_scope_is_abstract : param -> Scope.t -> bool

Return true if a scope is flagged as abstract in the abstraction_map of a param. Default to false if the node is not in the map.

val param_unrollings_of_scope : param -> Scope.t -> int option

The number of unrollings of a recursive function in the analysis of a param, if a refinement set one (see info)

val no_system_is_abstract : ?include_top:bool -> param -> bool

Return true if no system is flagged abstract in the abstraction_map of a param.

val param_assumptions_of_scope : param -> Scope.t -> Invs.t

Retrieve the assumptions of a scope from a param.

val mk_result : ?genuine:string list -> ?learned:(UfSymbol.t * Term.t list * Term.t) list -> param -> TransSys.t -> float -> result

Returns a result from an analysis.

val result_is_all_proved : result -> bool

Returns true if all properties in the system in a result have been proved.

val result_is_all_inv_proved : result -> bool

Returns true if all invariant properties in the system in a result have been proved.

val result_is_contract_proved : result -> bool

Returns true if the contract of the system in a result was proved: every guarantee and mode property is valid, and so is every termination check of the system, when it is a recursive function. What a refinement of a caller needs of the system (see Strategy).

val result_is_termination_proved : result -> bool

Returns true if every termination check of the system in a result was proved valid. The system of a function that is not recursive has none.

val result_termination_checks : result -> Lib.position list option

The positions of the calls whose termination checks the analysis of a result proved, if it proved every termination check of the system, None otherwise

val result_is_some_falsified : result -> bool

Returns true if some properties in the system in a result have been falsified.

val result_is_some_inv_falsified : result -> bool

Returns true if some invariant properties in the system in a result have been falsified.

val result_is_some_reach_proved : result -> bool

Returns true if some reachability properties in the system in a result have been proven reachable.

type results

Map from Scope.t to result storing the results found this far.

val mk_results : unit -> results

Creates a new results.

val results_add : result -> results -> results

Adds a result to a results.

val results_find : Scope.t -> results -> result list

Returns the list of results for a top scope.

Raises Not_found if not found.

val results_last : Scope.t -> results -> result

Returns the last result corresponding to a scope.

val results_size : results -> int

Returns the total number of analyzed systems so far

val results_length : results -> int

Returns the total number of results stored in a results. Used to generate UIDs for params.

val results_is_safe : results -> bool option

Returns None if no properties were falsified but some could not be proved, Some true if all properties were proved, and Some false if some were falsified.

val results_is_empty : results -> bool
val results_clean : results -> results

Cleans the results by removing nodes that don't have any property or contract.

type pp_print_system_user_name = Stdlib.Format.formatter -> Scope.t -> unit
val pp_print_param : bool -> TransSys.t -> pp_print_system_user_name -> Stdlib.Format.formatter -> param -> unit

Pretty printer for param.

val pp_print_result_quiet : pp_print_system_user_name -> Stdlib.Format.formatter -> result -> unit

Pretty printer for result, quiet version.

val pp_print_result : pp_print_system_user_name -> Stdlib.Format.formatter -> result -> unit

Pretty printer for result.