Module Conditions

module Conditions: sig .. end

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 {

`mutable id : int;`	`(*`	See `index`	`*)`
`size : int;`
`vars : Lang.F.Vars.t;`
`stmt : Cil_types.stmt option;`
`descr : string option;`
`deps : Property.t list;`
`warn : Warning.Set.t;`
`condition : condition;`

}

type condition =

`\|`	`Type of Lang.F.pred`	`(*`	Type section, not constraining for filtering	`*)`
`\|`	`Have of Lang.F.pred`	`(*`	Normal assumptions section	`*)`
`\|`	`When of Lang.F.pred`	`(*`	Assumptions introduced after simplifications	`*)`
`\|`	`Core of Lang.F.pred`	`(*`	Common hypotheses gather from parallel branches	`*)`
`\|`	`Init of Lang.F.pred`	`(*`	Initializers assumptions	`*)`
`\|`	`Branch of Lang.F.pred * sequence * sequence`	`(*`	If-Then-Else	`*)`
`\|`	`Either of sequence list`	`(*`	Disjunction	`*)`
`\|`	`State of Mstate.state`	`(*`	Memory Model snapshot	`*)`

type sequence

List of steps

type sequent = sequence * Lang.F.pred

val pretty : (Stdlib.Format.formatter -> sequent -> unit) Stdlib.ref

val step : ?descr:string ->
       ?stmt:Cil_types.stmt ->
       ?deps:Property.t list ->
       ?warn:Warning.Set.t -> condition -> step

Creates a single step

val update_cond : ?descr:string ->
       ?deps:Property.t list ->
       ?warn: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

val seq_branch : ?stmt:Cil_types.stmt ->
       Lang.F.pred ->
       sequence -> sequence -> 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.

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

val lemma : Lang.F.pred -> sequent

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 close : sequent -> Lang.F.pred

With free variables quantified.

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

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:Cil_types.stmt -> ?deps:Property.t list -> ?warn: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 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: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