Module Wp.Conditions

module Conditions: sig .. end


Predicate Introduction


val forall_intro : Wp.Lang.F.pred -> Wp.Lang.F.pred list * Wp.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 : Wp.Lang.F.pred -> Wp.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 : Wp.Lang.F.Vars.t;
   stmt : Cil_types.stmt option;
   descr : string option;
   deps : Property.t list;
   warn : Wp.Warning.Set.t;
   condition : condition;
}
type condition = 
| Type of Wp.Lang.F.pred (*
Type section, not constraining for filtering
*)
| Have of Wp.Lang.F.pred (*
Normal assumptions section
*)
| When of Wp.Lang.F.pred (*
Assumptions introduced after simplifications
*)
| Core of Wp.Lang.F.pred (*
Common hypotheses gather from parallel branches
*)
| Init of Wp.Lang.F.pred (*
Initializers assumptions
*)
| Branch of Wp.Lang.F.pred * sequence * sequence (*
If-Then-Else
*)
| Either of sequence list (*
Disjunction
*)
| State of Wp.Mstate.state (*
Memory Model snapshot
*)
type sequence 
List of steps
type sequent = sequence * Wp.Lang.F.pred 
val pretty : (Format.formatter -> sequent -> unit) Pervasives.ref
val step : ?descr:string ->
?stmt:Cil_types.stmt ->
?deps:Property.t list ->
?warn:Wp.Warning.Set.t -> condition -> step
Creates a single step
val update_cond : ?descr:string ->
?deps: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 -> Wp.Lang.F.Vars.t
Pre-computed and available in constant time.
val vars_seq : sequent -> Wp.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 ->
Wp.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 : (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
condition -> condition
Rewrite all root predicates in condition
val map_step : (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
step -> step
Rewrite all root predicates in step
val map_sequence : (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
sequence -> sequence
Rewrite all root predicates in sequence
val map_sequent : (Wp.Lang.F.pred -> Wp.Lang.F.pred) ->
sequent -> sequent
Rewrite all root predocates 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 subst : (Wp.Lang.F.term -> Wp.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 : Wp.Lang.F.pred -> sequent
Performs existential, universal and hypotheses introductions
val head : step -> Wp.Lang.F.pred
Predicate for Have and such, Condition for Branch, True for Either
val have : step -> Wp.Lang.F.pred
Predicate for Have and such, True for any other
val condition : sequence -> Wp.Lang.F.pred
With free variables kept.
val close : sequent -> Wp.Lang.F.pred
With free variables quantified.
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:Cil_types.stmt -> ?deps:Property.t list -> ?warn:Wp.Warning.Set.t -> 'a
val nil : bundle
Same as empty
val occurs : Wp.Lang.F.var -> bundle -> bool
val intersect : Wp.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 : Wp.Lang.F.pred list -> bundle -> bundle
Assumes a list of predicates in a Type section on top of the bundle.
val intros : Wp.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 ->
Wp.Mstate.state -> bundle -> bundle
Stack a memory model state on top of the bundle.
val assume : (?init:bool ->
?domain:bool ->
Wp.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 : (Wp.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 -> Wp.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 simplify : ?solvers:Wp.Lang.simplifier list ->
?intros:int -> sequent -> sequent
val pruning : ?solvers:Wp.Lang.simplifier list ->
sequent -> sequent