Conditions.mli 9.61 KB
Newer Older
1 2 3 4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
Andre Maroneze's avatar
Andre Maroneze committed
5
(*  Copyright (C) 2007-2020                                               *)
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Weakest Pre Accumulator                                            --- *)
(* -------------------------------------------------------------------------- *)

open Cil_types
open Lang
open Lang.F

31 32 33 34 35 36
(** {2 Predicate Introduction} *)


(** Introduce universally quantified formulae: head forall quantifiers
    are instanciated to fresh variables in current pool and left-implies are
    extracted, recursively. *)
37
val forall_intro: Lang.F.pred -> Lang.F.pred list * Lang.F.pred
38 39 40

(** Introduce existential quantified formulae: head exist quantifiers
    are instanciated to fresh variables, recursively. *)
41 42
val exist_intro: Lang.F.pred -> Lang.F.pred

43
(** {2 Sequent} *)
44 45 46 47 48 49 50 51 52 53 54 55 56

type step = private {
  mutable id : int ; (** See [index] *)
  size : int ;
  vars : Vars.t ;
  stmt : stmt option ;
  descr : string option ;
  deps : Property.t list ;
  warn : Warning.Set.t ;
  condition : condition ;
}

and condition =
57 58 59 60 61 62 63 64
  | 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 *)
65 66 67 68 69 70 71

and sequence (** List of steps *)

type sequent = sequence * F.pred

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

72
(** Creates a single step *)
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
val step :
  ?descr:string ->
  ?stmt:stmt ->
  ?deps:Property.t list ->
  ?warn:Warning.Set.t ->
  condition -> step

(** Updates the condition of a step and merges [descr], [deps] and [warn] *)
val update_cond :
  ?descr:string ->
  ?deps:Property.t list ->
  ?warn:Warning.Set.t ->
  step ->
  condition -> step

88
val is_true : sequence -> bool (** Contains only true or empty steps *)
89
val is_empty : sequence -> bool (** No step at all *)
90 91
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. *)
92

93 94
val empty : sequence (** empty sequence, equivalent to true assumption *)
val trivial : sequent (** empty implies true *)
95
val sequence : step list -> sequence
96

97
val seq_branch : ?stmt:stmt -> F.pred -> sequence -> sequence -> sequence
98
(** Creates an If-Then-Else branch located at the provided stmt, if any. *)
99

100 101
val append : sequence -> sequence -> sequence (** Conjunction *)
val concat : sequence list -> sequence (** List conjunction *)
102

103 104
(** Iterate only over the head steps of the sequence.
    Does not go deeper inside branches and disjunctions. *)
105 106
val iter : (step -> unit) -> sequence -> unit

107
(** Same domain than [iter]. *)
108 109
val list : sequence -> step list

110 111 112
(** Compute the {i total} number of steps in the sequence, including
    nested sequences from branches and disjunctions.
    Pre-computed and available in constant time. *)
113 114 115
val size : sequence -> int

val steps : sequence -> int
116 117
(** Attributes unique indices to every [step.id] in the sequence,
    starting from zero. Recursively
118 119 120 121 122 123 124 125 126 127 128 129 130
    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 {i must} have been called on the sequence before
    retrieving the index properly.
    @raise Not_found if the index is out of bounds. *)

val is_trivial : sequent -> bool
131
(** Goal is true or hypotheses contains false. *)
132 133 134 135

(** {2 Transformations} *)

val map_condition : (pred -> pred) -> condition -> condition
136 137
(** Rewrite all root predicates in condition *)

138
val map_step : (pred -> pred) -> step -> step
139 140
(** Rewrite all root predicates in step *)

141
val map_sequence : (pred -> pred) -> sequence -> sequence
142 143
(** Rewrite all root predicates in sequence *)

144
val map_sequent : (pred -> pred) -> sequent -> sequent
Loïc Correnson's avatar
Loïc Correnson committed
145
(** Rewrite all root predicates in hypotheses and goal *)
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160

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).
    @raise 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.
    @raise Invalid_argument if the index is out of bounds. *)

val subst : (term -> 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.
161
    [f] should raise [Not_found] on terms that must not be replaced
162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185
*)

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 : pred -> sequent
(** Performs existential, universal and hypotheses introductions *)

val head : step -> pred (** Predicate for Have and such, Condition for Branch, True for Either *)
val have : step -> pred (** Predicate for Have and such, True for any other *)

val condition : sequence -> pred (** With free variables kept. *)
val close : sequent -> pred (** With free variables {i quantified}. *)

val at_closure : (sequent -> sequent ) -> unit (** register a transformation applied just before close *)

(** {2 Bundles}

    Bundles are {i mergeable} pre-sequences.
    This the key structure for merging hypotheses with linear complexity
    during backward weakest pre-condition calculus.
186 187 188

    Bundle are constructed in backward order with respect to program
    control-flow, as driven by the wp calculus.
189 190 191 192 193 194 195 196 197 198 199
*)

type bundle

type 'a attributed =
  ( ?descr:string ->
    ?stmt:stmt ->
    ?deps:Property.t list ->
    ?warn:Warning.Set.t ->
    'a )

200
val nil : bundle (** Same as empty *)
201 202
val occurs : F.var -> bundle -> bool
val intersect : F.pred -> bundle -> bool
203 204
(** Variables of predicate and the bundle intersects *)

205
val merge : bundle list -> bundle
206 207 208 209 210 211
(** 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. *)
212
val domain : F.pred list -> bundle -> bundle
213 214

(** Assumes a list of predicates in a [Have] section on top of the bundle. *)
215
val intros : F.pred list -> bundle -> bundle
216 217

(** Stack a memory model state on top of the bundle. *)
218
val state : ?descr:string -> ?stmt:stmt -> Mstate.state -> bundle -> bundle
219 220 221 222 223

(** 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. *)
224
val assume : (?init:bool -> ?domain:bool -> F.pred -> bundle -> bundle) attributed
225 226

(** Construct a branch bundle, with merging of all common parts. *)
227
val branch : (F.pred -> bundle -> bundle -> bundle) attributed
228 229

(** Construct a disjunction bundle, with merging of all common parts. *)
230
val either : (bundle list -> bundle) attributed
231 232

(** Computes a formulae equivalent to the bundle. For debugging purpose only. *)
233
val extract : bundle -> F.pred list
234 235

(** Closes the bundle and promote it into a well-formed sequence. *)
236 237
val bundle : bundle -> sequence

238
(** {2 Simplifiers} *)
239 240 241 242

val clean : sequent -> sequent
val filter : sequent -> sequent
val parasite : sequent -> sequent
243
val init_filter : sequent -> sequent
244 245
val simplify : ?solvers:simplifier list -> ?intros:int -> sequent -> sequent
val pruning : ?solvers:simplifier list -> sequent -> sequent
246

247
(* -------------------------------------------------------------------------- *)