From f6eec48728f9ffdd0962c21822feceaae1449218 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 25 Feb 2020 09:38:27 +0100
Subject: [PATCH] [wp] sequent API documentation
---
src/plugins/wp/Conditions.mli | 96 +++++++++++++++++++++++++++--------
1 file changed, 74 insertions(+), 22 deletions(-)
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index d4d32acbde1..aa3d0881484 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -28,11 +28,19 @@ open Cil_types
open Lang
open Lang.F
-(** Predicates *)
+(** {2 Predicate Introduction} *)
+
+
+(** Introduce universally quantified formulae: head forall quantifiers
+ are instanciated to fresh variables in current pool and left-implies are
+ extracted, recursively. *)
val forall_intro: Lang.F.pred -> Lang.F.pred list * Lang.F.pred
+
+(** Introduce existential quantified formulae: head exist quantifiers
+ are instanciated to fresh variables, recursively. *)
val exist_intro: Lang.F.pred -> Lang.F.pred
-(** Sequent *)
+(** {2 Sequent} *)
type step = private {
mutable id : int ; (** See [index] *)
@@ -46,14 +54,14 @@ type step = private {
}
and condition =
- | Type of pred
- | Have of pred
- | When of pred
- | Core of pred
- | Init of pred
- | Branch of pred * sequence * sequence
- | Either of sequence list
- | State of Mstate.state
+ | Type of pred (** Type section, not constraining for filtering *)
+ | Have of pred (** Normal assumptions section *)
+ | When of pred (** Assumptions introduced after simplifications *)
+ | Core of pred (** Common hypotheses gather from parallel branches *)
+ | Init of pred (** Initializers assumptions *)
+ | Branch of pred * sequence * sequence (** If-Then-Else *)
+ | Either of sequence list (** Disjunction *)
+ | State of Mstate.state (** Memory Model snapshot *)
and sequence (** List of steps *)
@@ -61,6 +69,7 @@ type sequent = sequence * F.pred
val pretty : (Format.formatter -> sequent -> unit) ref
+(** Creates a single step *)
val step :
?descr:string ->
?stmt:stmt ->
@@ -76,29 +85,36 @@ val update_cond :
step ->
condition -> step
-val is_true : sequence -> bool (** Only true or empty steps *)
+val is_true : sequence -> bool (** Contains only true or empty steps *)
val is_empty : sequence -> bool (** No step at all *)
-val vars_hyp : sequence -> Vars.t
-val vars_seq : sequent -> Vars.t
+val vars_hyp : sequence -> Vars.t (** Pre-computed and available in constant time. *)
+val vars_seq : sequent -> Vars.t (** At the cost of the union of hypotheses and goal. *)
-val empty : sequence
-val trivial : sequent
+val empty : sequence (** empty sequence, equivalent to true assumption *)
+val trivial : sequent (** empty implies true *)
val sequence : step list -> sequence
+
val seq_branch : ?stmt:stmt -> F.pred -> sequence -> sequence -> sequence
+(** Creates an If-Then-Else branch located at the provided stmt, if any. *)
-val append : sequence -> sequence -> sequence
-val concat : sequence list -> sequence
+val append : sequence -> sequence -> sequence (** Conjunction *)
+val concat : sequence list -> sequence (** List conjunction *)
-(** Iterate only over the head steps of the sequence *)
+(** Iterate only over the head steps of the sequence.
+ Does not go deeper inside branches and disjunctions. *)
val iter : (step -> unit) -> sequence -> unit
-(** The internal list of steps *)
+(** Same domain than [iter]. *)
val list : sequence -> step list
+(** Compute the {i total} number of steps in the sequence, including
+ nested sequences from branches and disjunctions.
+ Pre-computed and available in constant time. *)
val size : sequence -> int
val steps : sequence -> int
-(** Attributes unique indices to every [step.id] in the sequence, starting from zero.
+(** 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
@@ -112,13 +128,21 @@ val step_at : sequence -> int -> step
@raise Not_found if the index is out of bounds. *)
val is_trivial : sequent -> bool
+(** Goal is true or hypotheses contains false. *)
(** {2 Transformations} *)
val map_condition : (pred -> pred) -> condition -> condition
+(** Rewrite all root predicates in condition *)
+
val map_step : (pred -> pred) -> step -> step
+(** Rewrite all root predicates in step *)
+
val map_sequence : (pred -> pred) -> sequence -> sequence
+(** Rewrite all root predicates in sequence *)
+
val map_sequent : (pred -> 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.
@@ -159,6 +183,9 @@ val at_closure : (sequent -> sequent ) -> unit (** register a transformation app
Bundles are {i 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
@@ -170,20 +197,45 @@ type 'a attributed =
?warn:Warning.Set.t ->
'a )
-val nil : bundle
+val nil : bundle (** Same as empty *)
val occurs : F.var -> bundle -> bool
val intersect : 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. *)
+
+(** Assumes a list of predicates in a [Type] section on top of the bundle. *)
val domain : F.pred list -> bundle -> bundle
+
+(** Assumes a list of predicates in a [Have] section on top of the bundle. *)
val intros : F.pred list -> bundle -> bundle
+
+(** Stack a memory model state on top of the bundle. *)
val state : ?descr:string -> ?stmt:stmt -> Mstate.state -> bundle -> bundle
+
+(** 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 assume : (?init:bool -> ?domain:bool -> F.pred -> bundle -> bundle) attributed
+
+(** Construct a branch bundle, with merging of all common parts. *)
val branch : (F.pred -> bundle -> bundle -> bundle) attributed
+
+(** Construct a disjunction bundle, with merging of all common parts. *)
val either : (bundle list -> bundle) attributed
+
+(** Computes a formulae equivalent to the bundle. For debugging purpose only. *)
val extract : bundle -> F.pred list
+
+(** Closes the bundle and promote it into a well-formed sequence. *)
val bundle : bundle -> sequence
-(** {2 Simplifier} *)
+(** {2 Simplifiers} *)
val clean : sequent -> sequent
val filter : sequent -> sequent
--
GitLab