Module Wp.Conditions

Proof Task and Simplifiers

Predicate Introduction

val forall_intro : Lang.F.pred -> Lang.F.pred list * Lang.F.pred

Introduce universally quantified formulae: head forall quantifiers are instanciated to fresh variables in current pool and left-implies are extracted, recursively.

val exist_intro : Lang.F.pred -> Lang.F.pred

Introduce existential quantified formulae: head exist quantifiers are instanciated to fresh variables, recursively.

Sequent

type step = private {
  1. mutable id : int;
    (*

    See index

    *)
  2. size : int;
  3. vars : Lang.F.Vars.t;
  4. stmt : Frama_c_kernel.Cil_types.stmt option;
  5. descr : string option;
  6. deps : Frama_c_kernel.Property.t list;
  7. warn : Wp__.Warning.Set.t;
  8. condition : condition;
}
and condition =
  1. | Type of Lang.F.pred
    (*

    Type section, not constraining for filtering

    *)
  2. | Have of Lang.F.pred
    (*

    Normal assumptions section

    *)
  3. | When of Lang.F.pred
    (*

    Assumptions introduced after simplifications

    *)
  4. | Core of Lang.F.pred
    (*

    Common hypotheses gather from parallel branches

    *)
  5. | Init of Lang.F.pred
    (*

    Initializers assumptions

    *)
  6. | Branch of Lang.F.pred * sequence * sequence
    (*

    If-Then-Else

    *)
  7. | Either of sequence list
    (*

    Disjunction

    *)
  8. | State of Mstate.state
    (*

    Memory Model snapshot

    *)
and sequence

List of steps

type sequent = sequence * Lang.F.pred
val pretty : (Stdlib.Format.formatter -> sequent -> unit) Stdlib.ref
val equal : sequent -> sequent -> bool
val step : ?descr:string -> ?stmt:Frama_c_kernel.Cil_types.stmt -> ?deps:Frama_c_kernel.Property.t list -> ?warn:Wp__.Warning.Set.t -> condition -> step

Creates a single step

val update_cond : ?descr:string -> ?deps:Frama_c_kernel.Property.t list -> ?warn:Wp__.Warning.Set.t -> step -> condition -> step

Updates the condition of a step and merges descr, deps and warn

val is_true : sequence -> bool

Contains only true or empty steps

val is_empty : sequence -> bool

No step at all

val vars_hyp : sequence -> Lang.F.Vars.t

Pre-computed and available in constant time.

val vars_seq : sequent -> Lang.F.Vars.t

At the cost of the union of hypotheses and goal.

val empty : sequence

empty sequence, equivalent to true assumption

val trivial : sequent

empty implies true

val sequence : step list -> sequence

Creates an If-Then-Else branch located at the provided stmt, if any.

val append : sequence -> sequence -> sequence

Conjunction

val concat : sequence list -> sequence

List conjunction

val iter : (step -> unit) -> sequence -> unit

Iterate only over the head steps of the sequence. Does not go deeper inside branches and disjunctions.

val list : sequence -> step list

Same domain than iter.

val size : sequence -> int

Compute the total number of steps in the sequence, including nested sequences from branches and disjunctions. Pre-computed and available in constant time.

val steps : sequence -> int

Attributes unique indices to every step.id in the sequence, starting from zero. Recursively Returns the number of steps in the sequence.

val index : sequent -> unit

Compute steps' id of sequent left hand-side. Same as ignore (steps (fst s)).

val step_at : sequence -> int -> step

Retrieve a step by id in the sequence. The index function must have been called on the sequence before retrieving the index properly.

  • raises Not_found

    if the index is out of bounds.

val is_trivial : sequent -> bool

Goal is true or hypotheses contains false.

val probes : sequence -> Lang.F.term Wp__.Probe.Map.t

Collect all probes in the sequence

Transformations

val map_condition : (Lang.F.pred -> Lang.F.pred) -> condition -> condition

Rewrite all root predicates in condition

val map_step : (Lang.F.pred -> Lang.F.pred) -> step -> step

Rewrite all root predicates in step

val map_sequence : (Lang.F.pred -> Lang.F.pred) -> sequence -> sequence

Rewrite all root predicates in sequence

val map_sequent : (Lang.F.pred -> Lang.F.pred) -> sequent -> sequent

Rewrite all root predicates in hypotheses and goal

val insert : ?at:int -> step -> sequent -> sequent

Insert a step in the sequent immediately at the specified position. Parameter at can be size to insert at the end of the sequent (default).

  • raises Invalid_argument

    if the index is out of bounds.

val replace : at:int -> step -> sequent -> sequent

replace a step in the sequent, the one at the specified position.

  • raises Invalid_argument

    if the index is out of bounds.

val replace_by_step_list : at:int -> step list -> sequent -> sequent

replace a step in the sequent, the one at the specified position.

  • raises Invalid_argument

    if the index is out of bounds.

val subst : (Lang.F.term -> Lang.F.term) -> sequent -> sequent

Apply the atomic substitution recursively using Lang.F.p_subst f. Function f should only transform the head of the predicate, and can assume its sub-terms have been already substituted. The atomic substitution is also applied to predicates. f should raise Not_found on terms that must not be replaced

val introduction : sequent -> sequent option

Performs existential, universal and hypotheses introductions

val introduction_eq : sequent -> sequent

Same as introduction but returns the same sequent is None

Performs existential, universal and hypotheses introductions

val head : step -> Lang.F.pred

Predicate for Have and such, Condition for Branch, True for Either

val have : step -> Lang.F.pred

Predicate for Have and such, True for any other

val pred_cond : condition -> Lang.F.pred
val condition : sequence -> Lang.F.pred

With free variables kept.

val property : sequent -> Lang.F.pred

With free variables kept.

val at_closure : (sequent -> sequent) -> unit

register a transformation applied just before close

Bundles

Bundles are mergeable pre-sequences. This the key structure for merging hypotheses with linear complexity during backward weakest pre-condition calculus.

Bundle are constructed in backward order with respect to program control-flow, as driven by the wp calculus.

type bundle
type 'a attributed = ?descr:string -> ?stmt:Frama_c_kernel.Cil_types.stmt -> ?deps:Frama_c_kernel.Property.t list -> ?warn:Wp__.Warning.Set.t -> 'a
val nil : bundle

Same as empty

val occurs : Lang.F.var -> bundle -> bool
val intersect : Lang.F.pred -> bundle -> bool

Variables of predicate and the bundle intersects

val merge : bundle list -> bundle

Performs a diff-based disjunction, introducing If-Then-Else or Either branches when possible. Linear complexity is achieved by assuming bundle ordering is consistent over the list.

val probe : loc:Frama_c_kernel.Cil_types.location -> ?descr:string -> ?stmt:Frama_c_kernel.Cil_types.stmt -> name:string -> Lang.F.term -> bundle -> bundle

Inserts probes to a sequent.

val domain : Lang.F.pred list -> bundle -> bundle

Assumes a list of predicates in a Type section on top of the bundle.

val intros : Lang.F.pred list -> bundle -> bundle

Assumes a list of predicates in a Have section on top of the bundle.

val state : ?descr:string -> ?stmt:Frama_c_kernel.Cil_types.stmt -> Mstate.state -> bundle -> bundle

Stack a memory model state on top of the bundle.

val assume : (?init:bool -> ?domain:bool -> Lang.F.pred -> bundle -> bundle) attributed

Assumes a predicate in the specified section, with the specified decorations. On ~init:true, the predicate is placed in an Init section. On ~domain:true, the predicate is placed in a Type section. Otherwized, it is placed in a standard Have section.

val branch : (Lang.F.pred -> bundle -> bundle -> bundle) attributed

Construct a branch bundle, with merging of all common parts.

val either : (bundle list -> bundle) attributed

Construct a disjunction bundle, with merging of all common parts.

val extract : bundle -> Lang.F.pred list

Computes a formulae equivalent to the bundle. For debugging purpose only.

val bundle : bundle -> sequence

Closes the bundle and promote it into a well-formed sequence.

Simplifiers

val clean : sequent -> sequent
val filter : sequent -> sequent
val parasite : sequent -> sequent
val init_filter : sequent -> sequent
val simplify : ?solvers:Lang.simplifier list -> ?intros:int -> sequent -> sequent
val pruning : ?solvers:Lang.simplifier list -> sequent -> sequent