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 4.26 KB
Newer Older
1 2 3 4 5 6 7 8 9

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

10
(* program type symbols *)
11 12

type mtsymbol = private {
13 14 15 16 17
  mt_impure   : tysymbol;
  mt_effect   : tysymbol;
  mt_pure     : tysymbol;
  mt_regions  : int;
  mt_singleton: bool;
18 19
}

20 21 22
val create_mtsymbol :
  impure:tysymbol -> effect:tysymbol -> pure:tysymbol -> singleton:bool ->
  mtsymbol
23 24 25 26

val mt_equal : mtsymbol -> mtsymbol -> bool

val get_mtsymbol : tysymbol -> mtsymbol
27 28

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

30 31
val is_mutable_ts : tysymbol -> bool
val is_mutable_ty : ty       -> bool
32

33 34
val is_singleton_ts : tysymbol -> bool
val is_singleton_ty : ty       -> bool
35 36 37

(* builtin logic symbols for programs *)

38
val ts_arrow : tysymbol
39
val make_arrow_type : ty list -> ty -> ty
40

41 42 43
val ts_exn : tysymbol
val ty_exn : ty

44 45
(* val ts_label : tysymbol *)

46
(* program types *)
47

48
module rec T : sig
49

50
  type pre = Term.term
51

52 53
  type post_fmla = Term.vsymbol (* result *) * Term.term
  type exn_post_fmla = Term.vsymbol (* result *) option * Term.term
54

55
  type esymbol = lsymbol
56

57
  type post = post_fmla * (esymbol * exn_post_fmla) list
58

59 60 61
  type type_v = private
  | Tpure    of ty
  | Tarrow   of pvsymbol list * type_c
62

63
  and type_c = {
64 65 66
    c_result_type : type_v;
    c_effect      : E.t;
    c_pre         : pre;
67
    c_post        : post;
68
  }
69

70
  and pvsymbol = private {
71 72
    pv_name   : ident;
    pv_tv     : type_v;
73
    pv_effect : vsymbol;
74 75
    pv_pure   : vsymbol;
    pv_regions: Sreg.t;
76
  }
77

78 79
  val tpure  : ty -> type_v
  val tarrow : pvsymbol list -> type_c -> type_v
80

81 82
  val create_pvsymbol :
    preid -> type_v ->
83
    effect:vsymbol -> pure:vsymbol -> regions:Sreg.t -> pvsymbol
84

85
  (* program symbols *)
86

87 88 89 90 91 92 93 94 95 96
  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;
97
  }
98

99
  val create_psymbol:
100 101 102 103
    impure:lsymbol -> effect:lsymbol -> pure:lsymbol -> kind:psymbol_kind ->
    psymbol
  val create_psymbol_fun: preid -> type_v -> psymbol
  val create_psymbol_var: pvsymbol -> psymbol
104

105
  val get_psymbol: lsymbol -> psymbol
106 107 108

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

110
  (* program types -> logic types *)
111

112
  val purify : ty -> ty
113 114
  val effectify : ty -> ty

115
  val trans_type_v : ?effect:bool -> ?pure:bool -> type_v -> ty
116

117
  (* operations on program types *)
118

119
  val apply_type_v_var : type_v -> pvsymbol -> type_c
120 121

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

123
  val occur_type_v : R.t -> type_v -> bool
124

125 126
  val v_result : ty -> vsymbol
  val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
127

128
  val post_map : (term -> term) -> post -> post
129

130
  val subst1 : vsymbol -> term -> term Mvs.t
131

132
  val eq_type_v : type_v -> type_v -> bool
133

134
  (* pretty-printers *)
135

136 137
  val print_type_v : Format.formatter -> type_v -> unit
  val print_type_c : Format.formatter -> type_c -> unit
138
  val print_pre    : Format.formatter -> pre    -> unit
139
  val print_post   : Format.formatter -> post   -> unit
140
  val print_pvsymbol : Format.formatter -> pvsymbol -> unit
141

142
end
143

144
and Spv :  sig include Set.S with type elt = T.pvsymbol end
145 146
and Mpv :  sig include Map.S with type key = T.pvsymbol end

147
(* regions *)
148 149
and R : sig

150 151
  type t = private {
    r_tv : tvsymbol;
152
    r_ty : Ty.ty;    (* effect type *)
153
  }
154

155
  val create : tvsymbol -> Ty.ty -> t
156

157 158
  val print : Format.formatter -> t -> unit

159 160 161
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
162 163 164 165
and Sexn : sig include Set.S with type elt = T.esymbol end

(* effects *)
and E : sig
166

167
  type t = private {
168 169
    reads  : Sreg.t;
    writes : Sreg.t;
170
    raises : Sexn.t;
171
    globals: Spv.t;
172
  }
173

174
  val empty : t
175

176
  val add_read  : R.t -> t -> t
177
  val add_glob  : T.pvsymbol -> t -> t
178 179
  val add_write : R.t -> t -> t
  val add_raise : T.esymbol -> t -> t
180

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181
  val remove : Sreg.t -> t -> t
182
  val filter : (R.t -> bool) -> t -> t
183

184
  val remove_raise : T.esymbol -> t -> t
185

186
  val union : t -> t -> t
187

188
  val equal : t -> t -> bool
189

190
  val no_side_effect : t -> bool
191 192

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

194
  val occur : R.t -> t -> bool
195

196 197
  val print : Format.formatter -> t -> unit

198
end
199

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
200
(* ghost code *)
201
(****
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
202 203 204
val mt_ghost   : mtsymbol
val ps_ghost   : T.psymbol
val ps_unghost : T.psymbol
205
****)