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 3.9 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
(* model type symbols *)
11 12

type mtsymbol = private {
13 14 15 16 17
  mt_name   : ident;
  mt_args   : tvsymbol list;
  mt_model  : ty option;
  mt_abstr  : tysymbol;
  mt_mutable: bool;
18 19
}

20 21
val create_mtsymbol : 
  mut:bool -> preid -> tvsymbol list -> ty option -> mtsymbol
22 23 24

val mt_equal : mtsymbol -> mtsymbol -> bool

25
exception NotModelType
26 27

val get_mtsymbol : tysymbol -> mtsymbol
28
  (** raises [NotModelType] if [ts] is not a model type *)
29

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

33
val ts_arrow : tysymbol
34
val make_arrow_type : ty list -> ty -> ty
35

36 37 38
val ts_exn : tysymbol
val ty_exn : ty

39 40
(* val ts_label : tysymbol *)

41
(* program types *)
42
module rec T : sig
43

44
  type pre = Term.fmla
45

46 47 48 49
  type post_fmla = Term.vsymbol (* result *) * Term.fmla
  type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
      
  type esymbol = lsymbol
50

51 52 53 54 55
  type post = post_fmla * (esymbol * exn_post_fmla) list
      
  type type_v = private
  | Tpure    of ty
  | Tarrow   of pvsymbol list * type_c
56

57 58 59 60 61 62
  and type_c = { 
    c_result_type : type_v;
    c_effect      : E.t;
    c_pre         : pre;
    c_post        : post; 
  }
63

64 65 66 67 68 69
  and pvsymbol = private {
    pv_name : ident;
    pv_tv   : type_v;
    pv_ty   : ty;      (* as a logic type, for typing purposes only *)
    pv_vs   : vsymbol; (* for use in the logic *)
  }
70

71 72
  val tpure  : ty -> type_v
  val tarrow : pvsymbol list -> type_c -> type_v
73

74
  val create_pvsymbol : preid -> ?vs:vsymbol -> type_v -> pvsymbol
75

76
  (* program symbols *)
77

78 79 80 81 82 83 84 85
  type psymbol = private {
    p_name : ident;
    p_tv   : type_v;
    p_ty   : ty;      (* as a logic type, for typing purposes only *)
    p_ls   : lsymbol; (* for use in the logic *) 
  }
      
  val create_psymbol : preid -> type_v -> psymbol
86

87
  val p_equal : psymbol -> psymbol -> bool
88

89
  (* program types -> logic types *)
90

91 92 93 94 95 96 97 98
  val purify : ty -> ty
  val purify_type_v : ?logic:bool -> type_v -> ty
    (** when [logic] is [true], mutable types are turned into their models *)
    
  (* operations on program types *)
    
  val apply_type_v_var : type_v -> pvsymbol -> type_c
  val apply_type_v_sym : type_v -> psymbol  -> type_c
99
  val apply_type_v_ref : type_v -> R.t      -> type_c
100 101 102 103 104 105 106 107 108 109 110
    
  val occur_type_v : R.t -> type_v -> bool
    
  val v_result : ty -> vsymbol
  val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
    
  val post_map : (fmla -> fmla) -> post -> post
    
  val subst1 : vsymbol -> term -> term Mvs.t
    
  val eq_type_v : type_v -> type_v -> bool
111

112
  (* pretty-printers *)
113

114 115
  val print_type_v : Format.formatter -> type_v -> unit
  val print_type_c : Format.formatter -> type_c -> unit
116
  val print_pre    : Format.formatter -> pre    -> unit
117
  val print_post   : Format.formatter -> post   -> unit
118

119 120
end 

121
and Spv :  sig include Set.S with type elt = T.pvsymbol end
122 123 124 125 126 127 128 129 130 131 132 133 134
and Mpv :  sig include Map.S with type key = T.pvsymbol end

(* references *)
and R : sig

  type t = 
    | Rlocal  of T.pvsymbol
    | Rglobal of T.psymbol

  val type_of : t -> ty

  val name_of : t -> ident

135 136
  val print : Format.formatter -> t -> unit

137 138 139 140 141 142 143
end 
and Sref : sig include Set.S with type elt = R.t end
and Mref : sig include Map.S with type key = R.t end
and Sexn : sig include Set.S with type elt = T.esymbol end

(* effects *)
and E : sig
144

145 146 147 148 149
  type t = private {
    reads  : Sref.t;
    writes : Sref.t;
    raises : Sexn.t;
  }
150

151
  val empty : t
152

153 154 155
  val add_read  : R.t -> t -> t
  val add_write : R.t -> t -> t
  val add_raise : T.esymbol -> t -> t
156

157 158
  val remove_reference : R.t -> t -> t    
  val filter : (R.t -> bool) -> t -> t
159

160
  val remove_raise : T.esymbol -> t -> t
161

162
  val union : t -> t -> t
163

164 165 166 167 168
  val equal : t -> t -> bool
    
  val no_side_effect : t -> bool
    
  val subst : R.t Mpv.t -> t -> t
169

170
  val occur : R.t -> t -> bool
171

172 173
  val print : Format.formatter -> t -> unit

174
end 
175

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
176
(* ghost code *)
177

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
178 179 180
val mt_ghost   : mtsymbol
val ps_ghost   : T.psymbol
val ps_unghost : T.psymbol