Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

pgm_types.mli 5.61 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software 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.                  *)
(*                                                                        *)
(**************************************************************************)
19 20 21 22 23 24 25 26 27

open Why
open Util
open Ident
open Ty
open Theory
open Term
open Decl

28
(* program type symbols *)
29 30

type mtsymbol = private {
31 32 33 34 35
  mt_impure   : tysymbol;
  mt_effect   : tysymbol;
  mt_pure     : tysymbol;
  mt_regions  : int;
  mt_singleton: bool;
36 37
}

38 39 40
val create_mtsymbol :
  impure:tysymbol -> effect:tysymbol -> pure:tysymbol -> singleton:bool ->
  mtsymbol
41 42 43 44

val mt_equal : mtsymbol -> mtsymbol -> bool

val get_mtsymbol : tysymbol -> mtsymbol
45 46

val print_mt_symbol : Format.formatter -> mtsymbol -> unit
47

48 49
val is_mutable_ts : tysymbol -> bool
val is_mutable_ty : ty       -> bool
50

51 52
val is_singleton_ts : tysymbol -> bool
val is_singleton_ty : ty       -> bool
53 54 55

(* builtin logic symbols for programs *)

56
val ts_arrow : tysymbol
57
val make_arrow_type : ty list -> ty -> ty
58

59 60 61
val ts_exn : tysymbol
val ty_exn : ty

62 63
(* val ts_label : tysymbol *)

64
(* program types *)
65

66
module rec T : sig
67

68
  type pre = Term.term
69

70 71
  type post_fmla = Term.vsymbol (* result *) * Term.term
  type exn_post_fmla = Term.vsymbol (* result *) option * Term.term
72

73
  type esymbol = lsymbol
74

75
  type post = post_fmla * (esymbol * exn_post_fmla) list
76

77 78 79
  type type_v = private
  | Tpure    of ty
  | Tarrow   of pvsymbol list * type_c
80

81
  and type_c = {
82 83 84
    c_result_type : type_v;
    c_effect      : E.t;
    c_pre         : pre;
85
    c_post        : post;
86
  }
87

88
  and pvsymbol = private {
89 90
    pv_name   : ident;
    pv_tv     : type_v;
91
    pv_effect : vsymbol;
92 93
    pv_pure   : vsymbol;
    pv_regions: Sreg.t;
94
  }
95

96 97
  val tpure  : ty -> type_v
  val tarrow : pvsymbol list -> type_c -> type_v
98

99 100
  val create_pvsymbol :
    preid -> type_v ->
101
    effect:vsymbol -> pure:vsymbol -> regions:Sreg.t -> pvsymbol
102

103
  (* program symbols *)
104

105 106 107 108 109 110 111 112 113 114
  type psymbol_kind =
    | PSvar   of pvsymbol
    | PSfun   of type_v
    | PSlogic

  type psymbol = {
    ps_impure : lsymbol;
    ps_effect : lsymbol;
    ps_pure   : lsymbol;
    ps_kind   : psymbol_kind;
115
  }
116

117
  val create_psymbol:
118 119 120 121
    impure:lsymbol -> effect:lsymbol -> pure:lsymbol -> kind:psymbol_kind ->
    psymbol
  val create_psymbol_fun: preid -> type_v -> psymbol
  val create_psymbol_var: pvsymbol -> psymbol
122

123
  val get_psymbol: lsymbol -> psymbol
124 125 126

  val ps_name : psymbol -> ident
  val ps_equal : psymbol -> psymbol -> bool
127

128
  (* program types -> logic types *)
129

130
  val purify : ty -> ty
131 132
  val effectify : ty -> ty

133
  val trans_type_v : ?effect:bool -> ?pure:bool -> type_v -> ty
134

135
  (* operations on program types *)
136

137
  val apply_type_v_var : type_v -> pvsymbol -> type_c
138 139

  val subst_type_v : ty Mtv.t -> term Mvs.t -> type_v -> type_v
140

141
  val occur_type_v : R.t -> type_v -> bool
142

143 144
  val v_result : ty -> vsymbol
  val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
145

146
  val post_map : (term -> term) -> post -> post
147

148
  val subst1 : vsymbol -> term -> term Mvs.t
149

150
  val eq_type_v : type_v -> type_v -> bool
151

152
  (* pretty-printers *)
153

154 155
  val print_type_v : Format.formatter -> type_v -> unit
  val print_type_c : Format.formatter -> type_c -> unit
156
  val print_pre    : Format.formatter -> pre    -> unit
157
  val print_post   : Format.formatter -> post   -> unit
158
  val print_pvsymbol : Format.formatter -> pvsymbol -> unit
159

160
end
161

162
and Spv :  sig include Set.S with type elt = T.pvsymbol end
163 164
and Mpv :  sig include Map.S with type key = T.pvsymbol end

165
(* regions *)
166 167
and R : sig

168 169
  type t = private {
    r_tv : tvsymbol;
170
    r_ty : Ty.ty;    (* effect type *)
171
  }
172

173
  val create : tvsymbol -> Ty.ty -> t
174

175 176
  val print : Format.formatter -> t -> unit

177 178 179
end
and Sreg : sig include Set.S with type elt = R.t end
and Mreg : sig include Map.S with type key = R.t end
180 181 182 183
and Sexn : sig include Set.S with type elt = T.esymbol end

(* effects *)
and E : sig
184

185
  type t = private {
186 187
    reads  : Sreg.t;
    writes : Sreg.t;
188
    raises : Sexn.t;
189
    globals: Spv.t;
190
  }
191

192
  val empty : t
193

194
  val add_read  : R.t -> t -> t
195
  val add_glob  : T.pvsymbol -> t -> t
196 197
  val add_write : R.t -> t -> t
  val add_raise : T.esymbol -> t -> t
198

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
199
  val remove : Sreg.t -> t -> t
200
  val filter : (R.t -> bool) -> t -> t
201

202
  val remove_raise : T.esymbol -> t -> t
203

204
  val union : t -> t -> t
205

206
  val equal : t -> t -> bool
207

208
  val no_side_effect : t -> bool
209 210

  val subst : Ty.ty Mtv.t -> t -> t
211

212
  val occur : R.t -> t -> bool
213

214 215
  val print : Format.formatter -> t -> unit

216
end
217

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
218
(* ghost code *)
219
(****
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
220 221 222
val mt_ghost   : mtsymbol
val ps_ghost   : T.psymbol
val ps_unghost : T.psymbol
223
****)