ity.ml 52.5 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10 11 12 13 14
(********************************************************************)

open Stdlib
open Ident
open Ty
15
open Term
16

17
(** {2 Individual types (first-order types without effects)} *)
18 19

type itysymbol = {
20
  its_ts      : tysymbol;       (** logical type symbol *)
21 22
  its_private : bool;           (** private type *)
  its_mutable : bool;           (** mutable type *)
23
  its_mfields : pvsymbol list;  (** mutable record fields *)
24 25
  its_regions : region list;    (** shareable components *)
  its_arg_imm : bool list;      (** non-updatable parameters *)
26
  its_arg_exp : bool list;      (** exposed type parameters *)
27 28
  its_arg_vis : bool list;      (** non-ghost type parameters *)
  its_arg_frz : bool list;      (** irreplaceable type parameters *)
29
  its_reg_exp : bool list;      (** exposed shareable components *)
30 31 32
  its_reg_vis : bool list;      (** non-ghost shareable components *)
  its_reg_frz : bool list;      (** irreplaceable shareable components *)
  its_def     : ity option;     (** type alias *)
33 34 35 36
}

and ity = {
  ity_node : ity_node;
37
  ity_imm  : bool;
38 39 40 41
  ity_tag  : Weakhtbl.tag;
}

and ity_node =
42
  | Ityreg of region
43
    (** record with mutable fields and shareable components *)
44 45 46 47
  | Ityapp of itysymbol * ity list * ity list
    (** immutable type with shareable components *)
  | Ityvar of tvsymbol * bool
    (** type variable and its purity status *)
48

49
and region = {
50
  reg_vs   : vsymbol;
51 52
  reg_its  : itysymbol;
  reg_args : ity list;
53
  reg_regs : ity list;
54 55
}

56 57 58 59 60
and pvsymbol = {
  pv_vs    : vsymbol;
  pv_ity   : ity;
  pv_ghost : bool;
}
61 62 63 64 65 66

module Itsym = MakeMSHW (struct
  type t = itysymbol
  let tag its = its.its_ts.ts_name.id_tag
end)

67 68 69 70 71
module Ity = MakeMSHW (struct
  type t = ity
  let tag ity = ity.ity_tag
end)

72 73
module Reg = MakeMSHW (struct
  type t = region
74
  let tag reg = reg.reg_vs.vs_name.id_tag
75 76
end)

77 78 79 80 81
module PVsym = MakeMSHW (struct
  type t = pvsymbol
  let tag pv = pv.pv_vs.vs_name.id_tag
end)

82 83 84 85 86
module Sits = Itsym.S
module Mits = Itsym.M
module Hits = Itsym.H
module Wits = Itsym.W

87 88 89 90 91
module Sity = Ity.S
module Mity = Ity.M
module Hity = Ity.H
module Wity = Ity.W

92 93 94 95
module Sreg = Reg.S
module Mreg = Reg.M
module Hreg = Reg.H
module Wreg = Reg.W
96 97 98 99 100 101 102 103

module Spv = PVsym.S
module Mpv = PVsym.M
module Hpv = PVsym.H
module Wpv = PVsym.W

(* value type symbols *)

104 105
let its_equal : itysymbol -> itysymbol -> bool = (==)
let ity_equal : ity       -> ity       -> bool = (==)
106
let reg_equal : region    -> region    -> bool = (==)
107
let pv_equal  : pvsymbol  -> pvsymbol  -> bool = (==)
108 109 110

let its_hash its = id_hash its.its_ts.ts_name
let ity_hash ity = Weakhtbl.tag_hash ity.ity_tag
111
let reg_hash reg = id_hash reg.reg_vs.vs_name
112 113
let pv_hash  pv  = id_hash pv.pv_vs.vs_name

114 115
let its_compare its1 its2 = id_compare its1.its_ts.ts_name its2.its_ts.ts_name
let ity_compare ity1 ity2 = Pervasives.compare (ity_hash ity1) (ity_hash ity2)
116
let reg_compare reg1 reg2 = id_compare reg1.reg_vs.vs_name reg2.reg_vs.vs_name
117 118
let pv_compare  pv1  pv2  = id_compare pv1.pv_vs.vs_name pv2.pv_vs.vs_name

119
exception NonUpdatable of itysymbol * ity
120

121 122
let check_its_args s tl =
  assert (s.its_def = None);
123 124 125
  let check imm ity =
    if imm && not ity.ity_imm then raise (NonUpdatable (s,ity)) in
  List.iter2 check s.its_arg_imm tl
126

127 128 129 130
module Hsity = Hashcons.Make (struct
  type t = ity

  let equal ity1 ity2 = match ity1.ity_node, ity2.ity_node with
131
    | Ityvar (v1,p1), Ityvar (v2,p2) -> tv_equal v1 v2 && p1 = p2
132
    | Ityreg r1, Ityreg r2 -> reg_equal r1 r2
133 134 135
    | Ityapp (s1,l1,r1), Ityapp (s2,l2,r2) ->
        its_equal s1 s2 &&
        List.for_all2 ity_equal l1 l2 &&
136
        List.for_all2 ity_equal r1 r2
137 138 139
    | _ -> false

  let hash ity = match ity.ity_node with
140 141
    | Ityvar (v,p) ->
        Hashcons.combine (tv_hash v) (Hashtbl.hash p)
142
    | Ityreg r -> reg_hash r
143
    | Ityapp (s,tl,rl) ->
144
        Hashcons.combine_list ity_hash
145 146
          (Hashcons.combine_list ity_hash (its_hash s) tl) rl

147
  let immutable ity = match ity.ity_node with
148
    | Ityvar _ -> true
149
    | Ityreg _ -> false
150 151 152 153
    | Ityapp (s,tl,rl) ->
        check_its_args s tl;
        let imm ity = ity.ity_imm in
        List.for_all imm tl && List.for_all imm rl
154

155
  let tag n ity = { ity with
156 157
    ity_imm = immutable ity;
    ity_tag = Weakhtbl.create_tag n }
158
end)
159

160 161
let mk_ity node = {
  ity_node = node;
162
  ity_imm  = true;
163 164 165
  ity_tag  = Weakhtbl.dummy_tag;
}

166 167
let mk_reg v s tl rl = {
  reg_vs   = v;
168
  reg_its  = s;
169
  reg_args = (check_its_args s tl; tl);
170 171
  reg_regs = rl;
}
172

173 174 175
let ity_reg r              = Hsity.hashcons (mk_ity (Ityreg r))
let ity_var v              = Hsity.hashcons (mk_ity (Ityvar (v,false)))
let ity_var_pure v         = Hsity.hashcons (mk_ity (Ityvar (v,true)))
176
let ity_app_unsafe s tl rl = Hsity.hashcons (mk_ity (Ityapp (s,tl,rl)))
177

178 179
(* immutability and purity *)

180
let its_immutable s = not s.its_mutable
181

182
let its_pure s = not s.its_mutable && s.its_regions = []
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202

let ity_immutable ity = ity.ity_imm

let rec ity_pure ity = match ity.ity_node with
  | Ityreg _ -> false
  | Ityapp (_,tl,rl) -> List.for_all ity_pure tl && List.for_all ity_pure rl
  | Ityvar (_,p) -> p

let ity_pure ity = ity_immutable ity && ity_pure ity

let rec ity_purify ity = match ity.ity_node with
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl} | Ityapp (s,tl,rl) ->
      ity_app_unsafe s (List.map ity_purify tl) (List.map ity_purify rl)
  | Ityvar (v,_) -> ity_var_pure v

let rec ty_of_ity ity = match ity.ity_node with
  | Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
      ty_app s.its_ts (List.map ty_of_ity tl)
  | Ityvar (v,_) -> ty_var v

203 204 205 206
let mk_reg id s tl rl =
  let ty = ty_app s.its_ts (List.map ty_of_ity tl) in
  mk_reg (create_vsymbol id ty) s tl rl

207
(* generic traversal functions *)
208

209 210
let dfold fn acc l1 l2 =
  List.fold_left fn (List.fold_left fn acc l1) l2
211

212 213
let dfold2 fn acc l1 r1 l2 r2 =
  List.fold_left2 fn (List.fold_left2 fn acc l1 r1) l2 r2
214

215 216 217
let ity_fold fn acc ity = match ity.ity_node with
  | Ityreg {reg_args = tl; reg_regs = rl}
  | Ityapp (_,tl,rl) -> dfold fn acc tl rl
218 219
  | Ityvar _ -> acc

220
let reg_fold fn acc reg = dfold fn acc reg.reg_args reg.reg_regs
221

222
(* symbol-wise fold *)
223

224
let rec ity_s_fold fn acc ity = match ity.ity_node with
225 226
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl}
  | Ityapp (s,tl,rl) -> dfold (ity_s_fold fn) (fn acc s) tl rl
227 228
  | Ityvar _ -> acc

229
let reg_s_fold fn acc r = reg_fold (ity_s_fold fn) (fn acc r.reg_its) r
230

231
(* traversal functions on type variables *)
232 233

let rec ity_v_fold fn acc ity = match ity.ity_node with
234
  | Ityreg {reg_args = tl} | Ityapp (_,tl,_) ->
235
      List.fold_left (ity_v_fold fn) acc tl
236
  | Ityvar (v,_) -> fn acc v
237 238

let reg_v_fold fn acc r = List.fold_left (ity_v_fold fn) acc r.reg_args
239

240 241
let ity_freevars s ity = ity_v_fold Stv.add_left s ity
let reg_freevars s reg = reg_v_fold Stv.add_left s reg
242

243 244
let ity_v_occurs v ity = Util.any ity_v_fold (tv_equal v) ity
let reg_v_occurs v reg = Util.any reg_v_fold (tv_equal v) reg
245

246
let ity_closed ity = Util.all ity_v_fold Util.ffalse ity
247

248
(* traversal functions on top regions *)
249 250

let rec ity_r_fold fn acc ity =
251
  if ity.ity_imm then acc else
252
  match ity.ity_node with
253
  | Ityapp (_,tl,rl) -> dfold (ity_r_fold fn) acc tl rl
254
  | Ityreg r -> fn acc r
255
  | Ityvar _ -> acc
256

257
let reg_r_fold fn acc reg = reg_fold (ity_r_fold fn) acc reg
258

259
let ity_top_regs regs ity = ity_r_fold Sreg.add_left regs ity
260

261 262
let rec reg_freeregs s reg = reg_r_fold reg_freeregs (Sreg.add reg s) reg
let     ity_freeregs s ity = ity_r_fold reg_freeregs s ity
263

264 265 266
let rec reg_r_occurs r reg = reg_equal r reg ||
                             Util.any reg_r_fold (reg_r_occurs r) reg
let     ity_r_occurs r ity = Util.any ity_r_fold (reg_r_occurs r) ity
267

268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
(* traversal functions on exposed regions *)

let rec ity_exp_fold fn acc ity =
  if ity.ity_imm then acc else
  match ity.ity_node with
  | Ityapp (s,tl,rl) -> its_exp_fold fn acc s tl rl
  | Ityreg r -> fn acc r
  | Ityvar _ -> acc

and its_exp_fold fn acc s tl rl =
  let fn a x t = if x then ity_exp_fold fn a t else a in
  dfold2 fn acc s.its_arg_exp tl s.its_reg_exp rl

let reg_exp_fold fn acc reg =
  its_exp_fold fn acc reg.reg_its reg.reg_args reg.reg_regs
283

284
let ity_exp_regs regs ity = ity_exp_fold Sreg.add_left regs ity
285

286 287
let rec reg_rch_regs s reg = reg_exp_fold reg_rch_regs (Sreg.add reg s) reg
let     ity_rch_regs s ity = ity_exp_fold reg_rch_regs s ity
288

289 290 291
let rec reg_r_reachable r reg = reg_equal r reg ||
                                Util.any reg_exp_fold (reg_r_reachable r) reg
let     ity_r_reachable r ity = Util.any ity_exp_fold (reg_r_reachable r) ity
292

293 294 295
let rec reg_r_stale rs cv reg = Sreg.mem reg rs || not (Mreg.mem reg cv) &&
                                Util.any reg_exp_fold (reg_r_stale rs cv) reg
let     ity_r_stale rs cv ity = Util.any ity_exp_fold (reg_r_stale rs cv) ity
296

297 298 299 300
(* traversal functions on non-ghost regions *)

let rec ity_vis_fold fn acc ity =
  if ity.ity_imm then acc else
301
  match ity.ity_node with
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
  | Ityapp (s,tl,rl) -> its_vis_fold fn acc s tl rl
  | Ityreg r -> reg_vis_fold fn acc r
  | Ityvar _ -> acc

and its_vis_fold fn acc s tl rl =
  let fn a v t = if v then ity_vis_fold fn a t else a in
  dfold2 fn acc s.its_arg_vis tl s.its_reg_vis rl

and reg_vis_fold fn acc reg =
  its_exp_fold fn (fn acc reg) reg.reg_its reg.reg_args reg.reg_regs

let ity_vis_regs regs ity = ity_vis_fold Sreg.add_left regs ity

(* collect exposed type variables *)

let rec ity_exp_vars vars ity = match ity.ity_node with
318
  | Ityapp (s,tl,rl) ->
319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345
      let fn a x t = if x then ity_exp_vars a t else a in
      dfold2 fn vars s.its_arg_exp tl s.its_reg_exp rl
  | Ityvar (v,false) -> Stv.add v vars
  | Ityvar (_,true) | Ityreg _ -> vars

(* collect non-ghost type variables *)

let rec ity_vis_vars vars ity = match ity.ity_node with
  | Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
      let fn a v t = if v then ity_vis_vars a t else a in
      List.fold_left2 fn vars s.its_arg_vis tl
  | Ityvar (v,false) -> Stv.add v vars
  | Ityvar (_,true) -> vars

(* collect non-updatable type variables *)

let rec ity_realvars vars ity = match ity.ity_node with
  | Ityreg {reg_args = tl} | Ityapp (_,tl,_) ->
      List.fold_left ity_realvars vars tl
  | Ityvar (v,false) -> Stv.add v vars
  | Ityvar (_,true) -> vars

let rec ity_imm_vars vars ity = match ity.ity_node with
  | Ityreg {reg_its = s; reg_args = tl} | Ityapp (s,tl,_) ->
      let fn a i t = if i then ity_realvars a t
                          else ity_imm_vars a t in
      List.fold_left2 fn vars s.its_arg_imm tl
346 347
  | Ityvar _ -> vars

348
(* type matching *)
349 350 351 352 353 354 355

exception BadItyArity of itysymbol * int
exception BadRegArity of itysymbol * int

exception DuplicateRegion of region
exception UnboundRegion of region

356 357
exception ImpureType of tvsymbol * ity

358
type ity_subst = {
359 360 361
  isb_var : ity Mtv.t;
  isb_pur : ity Mtv.t;
  isb_reg : ity Mreg.t;
362 363
}

364
let isb_empty = {
365 366
  isb_var = Mtv.empty;
  isb_pur = Mtv.empty;
367
  isb_reg = Mreg.empty;
368 369 370
}

exception TypeMismatch of ity * ity * ity_subst
371

Andrei Paskevich's avatar
Andrei Paskevich committed
372 373
let ity_equal_check t1 t2 = if not (ity_equal t1 t2) then
  raise (TypeMismatch (t1, t2, isb_empty))
374

Andrei Paskevich's avatar
Andrei Paskevich committed
375 376
let reg_equal_check r1 r2 = if not (reg_equal r1 r2) then
  raise (TypeMismatch (ity_reg r1, ity_reg r2, isb_empty))
377 378

let ity_full_inst sbs ity =
379
  let rec inst ity = match ity.ity_node with
380
    | Ityreg r -> Mreg.find r sbs.isb_reg
381
    | Ityapp (s,tl,rl) ->
382 383 384 385 386 387
        ity_app_unsafe s (List.map inst tl) (List.map inst rl)
    | Ityvar (v,false) -> Mtv.find v sbs.isb_var
    | Ityvar (v,true) ->
        try Mtv.find v sbs.isb_pur with Not_found ->
        ity_purify (Mtv.find v sbs.isb_var) in
  if ity.ity_imm && ity_closed ity then ity else inst ity
388

389
let reg_full_inst sbs reg = Mreg.find reg sbs.isb_reg
390 391 392 393 394 395 396 397 398

let add_or_keep eq n = function
  | None -> Some n
  | Some o as r when eq o n -> r
  | _ -> raise Exit

let rec ity_match sbs ity1 ity2 =
  let set = add_or_keep ity_equal ity2 in
  match ity1.ity_node, ity2.ity_node with
399
  | Ityapp (s1,l1,r1), Ityapp (s2,l2,r2) when its_equal s1 s2 ->
400 401 402 403 404 405 406 407 408 409 410 411 412 413
      dfold2 ity_match sbs l1 l2 r1 r2
  | Ityreg r1, _ ->
      reg_match sbs r1 ity2
  | Ityvar (v1, false), _ ->
      if Mtv.mem v1 sbs.isb_pur &&
         not (ity_equal (ity_purify ity2) (Mtv.find v1 sbs.isb_pur))
      then raise Exit;
      { sbs with isb_var = Mtv.change set v1 sbs.isb_var }
  | Ityvar (v1, true), _ when ity_pure ity2 ->
      if Mtv.mem v1 sbs.isb_var &&
         not (ity_equal ity2 (ity_purify (Mtv.find v1 sbs.isb_var)))
      then raise Exit;
      { sbs with isb_pur = Mtv.change set v1 sbs.isb_pur }
  | Ityvar (v1, true), _ -> raise (ImpureType (v1, ity2))
414
  | _ -> raise Exit
415

416 417 418 419 420 421 422 423 424 425
and reg_match sbs reg1 ity2 =
  let seen = ref false in
  let set = add_or_keep (fun o n -> seen := true; ity_equal o n) ity2 in
  let sbs = { sbs with isb_reg = Mreg.change set reg1 sbs.isb_reg } in
  if !seen then sbs else
  match ity2.ity_node with
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl} | Ityapp (s,tl,rl)
    when its_equal reg1.reg_its s ->
      dfold2 ity_match sbs reg1.reg_args tl reg1.reg_regs rl
  | _ -> raise Exit
426 427

let ity_match sbs ity1 ity2 = try ity_match sbs ity1 ity2
428
  with Exit -> raise (TypeMismatch (ity1, ity2, sbs))
429

430 431
let reg_match sbs reg1 ity2 = try reg_match sbs reg1 ity2
  with Exit -> raise (TypeMismatch (ity_reg reg1, ity2, sbs))
432

433
let ity_freeze sbs ity = ity_match sbs ity ity
434
let reg_freeze sbs reg = reg_match sbs reg (ity_reg reg)
435

436
(* raw type constructors *)
437

438 439 440 441 442
let ity_app_raw sbs id s tl rl = match s.its_def with
  | Some { ity_node = Ityreg r } ->
      let tl = List.map (ity_full_inst sbs) r.reg_args in
      let rl = List.map (ity_full_inst sbs) r.reg_regs in
      ity_reg (mk_reg id r.reg_its tl rl)
443
  | None when s.its_mutable ->
444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465
      ity_reg (mk_reg id s tl rl)
  | Some ity -> ity_full_inst sbs ity
  | None -> ity_app_unsafe s tl rl

let create_region_raw sbs id s tl rl =
  match (ity_app_raw sbs id s tl rl).ity_node with
  | Ityreg r -> r
  | _ -> invalid_arg "Ity.create_region"

let ity_app_pure_raw sbs s tl rl = match s.its_def with
  | Some { ity_node = Ityreg r } ->
      let tl = List.map (ity_full_inst sbs) r.reg_args in
      let rl = List.map (ity_full_inst sbs) r.reg_regs in
      ity_app_unsafe r.reg_its tl rl
  | Some ity -> ity_full_inst sbs ity
  | None -> ity_app_unsafe s tl rl

(* smart type constructors *)

let its_check_args s tl =
  if List.length s.its_ts.ts_args <> List.length tl
  then raise (BadItyArity (s, List.length tl))
466

467 468
let its_match_args s tl =
  try {
469 470
    isb_var = List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty;
    isb_pur = Mtv.empty;
471
    isb_reg = Mreg.empty }
472 473 474 475
  with Invalid_argument _ -> raise (BadItyArity (s, List.length tl))

let its_match_regs s tl rl =
  try List.fold_left2 reg_match (its_match_args s tl) s.its_regions rl
476 477
  with Invalid_argument _ -> raise (BadRegArity (s, List.length rl))

478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493
let its_inst_regs fresh_reg s tl =
  let rec ity_inst sbs ity = match ity.ity_node with
    | Ityreg r ->
        reg_inst sbs r
    | Ityapp (s,tl,rl) ->
        let sbs, tl = Lists.map_fold_left ity_inst sbs tl in
        let sbs, rl = Lists.map_fold_left ity_inst sbs rl in
        sbs, ity_app_unsafe s tl rl
    | Ityvar (v, false) ->
        sbs, Mtv.find v sbs.isb_var
    | Ityvar (v,true) ->
        sbs, ity_purify (Mtv.find v sbs.isb_var)
  and reg_inst sbs r =
    try sbs, Mreg.find r sbs.isb_reg with Not_found ->
    let sbs, tl = Lists.map_fold_left ity_inst sbs r.reg_args in
    let sbs, rl = Lists.map_fold_left ity_inst sbs r.reg_regs in
494
    let ity = fresh_reg r.reg_vs.vs_name r.reg_its tl rl in
495 496 497 498 499 500 501 502
    { sbs with isb_reg = Mreg.add r ity sbs.isb_reg }, ity in
  Lists.map_fold_left reg_inst (its_match_args s tl) s.its_regions

let its_match_smart fresh_reg s tl rl =
  if rl <> [] then its_match_regs s tl rl, rl else
  if s.its_regions = [] && s.its_def = None
  then (its_check_args s tl; isb_empty, [])
  else its_inst_regs fresh_reg s tl
503

504
let create_region id s tl rl =
505
  let fresh id s tl rl = ity_reg (mk_reg (id_clone id) s tl rl) in
506 507
  let sbs, rl = its_match_smart fresh s tl rl in
  create_region_raw sbs id s tl rl
508 509

let ity_app s tl rl =
510
  let fresh id s tl rl = ity_reg (mk_reg (id_clone id) s tl rl) in
511 512 513 514 515 516 517
  let sbs, rl = its_match_smart fresh s tl rl in
  ity_app_raw sbs (id_fresh "rho") s tl rl

let ity_app_pure s tl rl =
  let pure _ s tl rl = ity_app_unsafe s tl rl in
  let sbs, rl = its_match_smart pure s tl rl in
  ity_app_pure_raw sbs s tl rl
518 519 520

(* itysymbol creation *)

521
let create_its, restore_its =
522
  let ts_to_its = Wts.create 17 in
523 524
  (fun ~ts ~priv ~mut ~mfld ~regs ~aimm ~aexp
       ~avis ~afrz ~rexp ~rvis ~rfrz ~def ->
525
    let its = {
526
      its_ts      = ts;
527 528
      its_private = priv;
      its_mutable = mut;
529
      its_mfields = mfld;
530
      its_regions = regs;
531
      its_arg_imm = aimm;
532
      its_arg_exp = aexp;
533 534
      its_arg_vis = avis;
      its_arg_frz = afrz;
535
      its_reg_exp = rexp;
536 537
      its_reg_vis = rvis;
      its_reg_frz = rfrz;
538
      its_def     = def;
539 540 541
    } in
    Wts.set ts_to_its ts its;
    its),
542
  (fun ts -> Wts.find ts_to_its ts)
543

544 545 546 547 548
let rec ity_of_ty ty = match ty.ty_node with
  | Tyvar v -> ity_var v
  | Tyapp (s,tl) ->
      let s = try restore_its s with Not_found ->
        invalid_arg "Ity.ity_of_ty" in
549 550 551 552 553 554 555 556
      ity_app s (List.map ity_of_ty tl) []

let rec ity_of_ty_pure ty = match ty.ty_node with
  | Tyvar v -> ity_var_pure v
  | Tyapp (s,tl) ->
      let s = try restore_its s with Not_found ->
        invalid_arg "Ity.ity_of_ty_pure" in
      ity_app_pure s (List.map ity_of_ty_pure tl) []
557

558 559
let its_of_ts ts priv =
  assert (ts.ts_def = None);
560
  let tl = List.map Util.ttrue ts.ts_args in
561 562 563
  let il = if priv then tl else List.map Util.ffalse ts.ts_args in
  create_its ~ts ~priv ~mut:false ~mfld:[] ~regs:[] ~aimm:il
    ~aexp:tl ~avis:tl ~afrz:tl ~rexp:[] ~rvis:[] ~rfrz:[] ~def:None
564

565 566 567 568 569
let create_itysymbol_rec id args =
  let ts = create_tysymbol id args None in
  let tl = List.map Util.ttrue ts.ts_args in
  create_its ~ts ~priv:false ~mut:false ~mfld:[] ~regs:[] ~aimm:tl
    ~aexp:tl ~avis:tl ~afrz:tl ~rexp:[] ~rvis:[] ~rfrz:[] ~def:None
570 571 572

let create_itysymbol_alias id args def =
  let ts = create_tysymbol id args (Some (ty_of_ity def)) in
573 574 575
  let mut, ity = match def.ity_node with (* ignore the top region *)
    | Ityreg r -> true, ity_app_pure r.reg_its r.reg_args r.reg_regs
    | _ -> false, def in
576
  let regs = Sreg.elements (ity_top_regs Sreg.empty ity) in
577 578
  let tl = List.map Util.ttrue args in
  let rl = List.map Util.ttrue regs in
579
  create_its ~ts ~priv:false ~mut ~mfld:[] ~regs ~aimm:tl ~aexp:tl
580
    ~avis:tl ~afrz:tl ~rexp:rl ~rvis:rl ~rfrz:rl ~def:(Some def)
581

582
let create_itysymbol_plain ~priv ~mut id args flds =
583
  let ts = create_tysymbol id args None in
584 585
  let collect_all fn acc =
    Mpv.fold (fun f _ a -> fn a f.pv_ity) flds acc in
586 587 588 589
  let collect_imm fn acc =
    Mpv.fold (fun f m a -> if m then a else fn a f.pv_ity) flds acc in
  let collect_vis fn acc =
    Mpv.fold (fun f _ a -> if f.pv_ghost then a else fn a f.pv_ity) flds acc in
590 591 592 593
  let sargs = Stv.of_list args in
  let dargs = collect_all ity_freevars Stv.empty in
  if not (Stv.subset dargs sargs) then
    raise (Ty.UnboundTypeVar (Stv.choose (Stv.diff dargs sargs)));
594
  let mfld = Mpv.fold (fun f m l -> if m then f::l else l) flds [] in
595 596 597 598 599 600 601 602
  let regs = Sreg.elements (collect_all ity_top_regs Sreg.empty) in
  let check_args s = List.map (Stv.contains s) args in
  let check_regs s = List.map (Sreg.contains s) regs in
  let rexp = check_regs (collect_all ity_exp_regs Sreg.empty) in
  let rvis = check_regs (collect_vis ity_vis_regs Sreg.empty) in
  let rfrz = check_regs (collect_imm ity_exp_regs Sreg.empty) in
  let mut = mut || mfld <> [] in
  if priv then (* private record *)
603
    let tl = List.map Util.ttrue args in
604 605 606
    create_its ~ts ~priv ~mut ~mfld ~regs ~aimm:tl ~aexp:tl
      ~avis:tl ~afrz:tl ~rexp ~rvis ~rfrz ~def:None
  else (* non-private updatable type *)
607 608 609 610
    let aimm = check_args (collect_all ity_imm_vars Stv.empty) in
    let aexp = check_args (collect_all ity_exp_vars Stv.empty) in
    let avis = check_args (collect_vis ity_vis_vars Stv.empty) in
    let afrz = check_args (collect_imm ity_exp_vars Stv.empty) in
611 612
    create_its ~ts ~priv ~mut ~mfld ~regs ~aimm ~aexp ~avis ~afrz
      ~rexp ~rvis ~rfrz ~def:None
613

614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629
(** pvsymbol creation *)

let create_pvsymbol id ghost ity = {
  pv_vs    = create_vsymbol id (ty_of_ity ity);
  pv_ity   = ity;
  pv_ghost = ghost;
}

let create_pvsymbol, restore_pv =
  let vs_to_pv = Wvs.create 17 in
  (fun id ?(ghost=false) ity ->
    let pv = create_pvsymbol id ghost ity in
    Wvs.set vs_to_pv pv.pv_vs pv;
    pv),
  (fun vs -> Wvs.find vs_to_pv vs)

630 631
let freeze_pv v s = ity_freeze s v.pv_ity

632 633 634 635 636
let pvs_of_vss pvs vss =
  Mvs.fold (fun vs _ s -> Spv.add (restore_pv vs) s) vss pvs

let t_freepvs pvs t = pvs_of_vss pvs (t_vars t)

637 638
(** builtin symbols *)

639 640 641 642
let its_int  = its_of_ts ts_int  true
let its_real = its_of_ts ts_real true
let its_bool = its_of_ts ts_bool true
let its_func = its_of_ts ts_func true
643

644 645 646
let ity_int  = ity_app its_int  [] []
let ity_real = ity_app its_real [] []
let ity_bool = ity_app its_bool [] []
647

648 649
let ity_func a b = ity_app its_func [a;b] []
let ity_pred a   = ity_app its_func [a;ity_bool] []
650

651
let its_tuple = Hint.memo 17 (fun n -> its_of_ts (ts_tuple n) false)
652

653
let ity_tuple tl = ity_app (its_tuple (List.length tl)) tl []
654

655 656
let ts_unit  = ts_tuple  0
let its_unit = its_tuple 0
657

658 659
let ty_unit  = ty_tuple  []
let ity_unit = ity_tuple []
660 661

(* exception symbols *)
662

663 664 665 666 667 668
type xsymbol = {
  xs_name : ident;
  xs_ity  : ity; (* closed and pure *)
}

let xs_equal : xsymbol -> xsymbol -> bool = (==)
669 670
let xs_hash xs = id_hash xs.xs_name
let xs_compare xs1 xs2 = id_compare xs1.xs_name xs2.xs_name
671 672

let create_xsymbol id ity =
673
  if not (ity_closed ity) then Loc.errorm ?loc:id.pre_loc
Andrei Paskevich's avatar
Andrei Paskevich committed
674
    "Exception %s has a polymorphic type" id.pre_name;
675
  if not ity.ity_imm then Loc.errorm ?loc:id.pre_loc
Andrei Paskevich's avatar
Andrei Paskevich committed
676 677
    "The type of exception %s has mutable components" id.pre_name;
  { xs_name = id_register id; xs_ity = ity; }
678 679 680 681 682 683 684 685 686 687

module Exn = MakeMSH (struct
  type t = xsymbol
  let tag xs = Weakhtbl.tag_hash xs.xs_name.id_tag
end)

module Sexn = Exn.S
module Mexn = Exn.M

(* effects *)
688

689
exception IllegalSnapshot of ity
690 691 692 693 694 695 696
exception IllegalAlias of region
exception AssignPrivate of region
exception BadGhostWrite of pvsymbol * region
exception StaleVariable of pvsymbol * region
exception DuplicateField of region * pvsymbol
exception GhostDivergence

697
type effect = {
698 699 700
  eff_reads  : Spv.t;         (* known variables *)
  eff_writes : Spv.t Mreg.t;  (* modifications to specific fields *)
  eff_taints : Sreg.t;        (* ghost modifications *)
701 702
  eff_covers : Sreg.t;        (* surviving writes *)
  eff_resets : Sreg.t;        (* locked by covers *)
703 704 705
  eff_raises : Sexn.t;        (* raised exceptions *)
  eff_oneway : bool;          (* non-termination *)
  eff_ghost  : bool;          (* ghost status *)
706 707 708
}

let eff_empty = {
709
  eff_reads  = Spv.empty;
710
  eff_writes = Mreg.empty;
711
  eff_taints = Sreg.empty;
712 713
  eff_covers = Sreg.empty;
  eff_resets = Sreg.empty;
714
  eff_raises = Sexn.empty;
715 716
  eff_oneway = false;
  eff_ghost  = false;
717 718 719
}

let eff_equal e1 e2 =
720
  Spv.equal e1.eff_reads e2.eff_reads &&
721
  Mreg.equal Spv.equal e1.eff_writes e2.eff_writes &&
722
  Sreg.equal e1.eff_taints e2.eff_taints &&
723 724
  Sreg.equal e1.eff_covers e2.eff_covers &&
  Sreg.equal e1.eff_resets e2.eff_resets &&
725
  Sexn.equal e1.eff_raises e2.eff_raises &&
726 727
  e1.eff_oneway = e2.eff_oneway &&
  e1.eff_ghost = e2.eff_ghost
728

729 730 731 732 733
let eff_pure e =
  Mreg.is_empty e.eff_writes &&
  Sexn.is_empty e.eff_raises &&
  not e.eff_oneway

734 735
let check_covers {eff_resets = rst; eff_covers = cvr} pvs =
  if not (Mreg.is_empty rst) then Spv.iter (fun v ->
736 737 738
    if ity_r_stale rst cvr v.pv_ity then Sreg.iter (fun r ->
      if ity_r_stale (Sreg.singleton r) cvr v.pv_ity then
        raise (StaleVariable (v,r))) rst) pvs
739 740 741

let check_taints tnt pvs =
  if not (Sreg.is_empty tnt) then Spv.iter (fun v ->
742 743
    if not v.pv_ghost then ity_vis_fold (fun () r ->
      if Sreg.mem r tnt then raise (BadGhostWrite (v,r))) () v.pv_ity) pvs
744 745

let visible_writes e =
746
  Mreg.subdomain (fun {reg_its = {its_private = priv}} fs ->
747 748 749 750
    priv || Spv.exists (fun fd -> not fd.pv_ghost) fs) e.eff_writes

let visible_reads e =
  Spv.fold (fun {pv_ghost = gh; pv_ity = ity} s ->
751
    if gh then s else ity_vis_regs s ity) e.eff_reads Sreg.empty
752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774

let reset_taints e =
  let tnt = if e.eff_ghost then visible_writes e else
    Sreg.diff (visible_writes e) (visible_reads e) in
  if e.eff_ghost then check_taints tnt e.eff_reads;
  { e with eff_taints = tnt }

let eff_ghostify gh e =
  if e.eff_ghost || not gh then e else
  if e.eff_oneway then raise GhostDivergence else
  reset_taints { e with eff_ghost = true }

let eff_diverge e = if e.eff_oneway then e else
  if e.eff_ghost then raise GhostDivergence else
  { e with eff_oneway = true }

let eff_read_pre rd e =
  if Spv.is_empty rd then e else
  let _ = check_taints e.eff_taints rd in
  { e with eff_reads = Spv.union e.eff_reads rd }

let eff_read_post e rd =
  if Spv.is_empty rd then e else
775
  let _ = check_covers e rd in
776 777 778
  let _ = check_taints e.eff_taints rd in
  { e with eff_reads = Spv.union e.eff_reads rd }

779
let eff_bind rd e = if Mpv.is_empty rd then e else
780 781 782 783 784 785 786 787 788 789
  { e with eff_reads = Mpv.set_diff e.eff_reads rd }

let eff_read rd =
  if Spv.is_empty rd then eff_empty else
  { eff_empty with eff_reads = rd }

let eff_read_single v = eff_read (Spv.singleton v)
let eff_read_single_pre v e = eff_read_pre (Spv.singleton v) e
let eff_read_single_post e v = eff_read_post e (Spv.singleton v)
let eff_bind_single v e = eff_bind (Spv.singleton v) e
790 791

let check_mutable_field fn r f =
792
  if not (List.memq f r.reg_its.its_mfields) then invalid_arg fn
793

794 795 796
let read_regs rd =
  Spv.fold (fun v s -> ity_rch_regs s v.pv_ity) rd Sreg.empty

797
(*TODO? add the third arg (resets) and check the invariants *)
798 799
let eff_write rd wr =
  if Mreg.is_empty wr then { eff_empty with eff_reads = rd } else
800
  let kn = read_regs rd in
801 802 803
  let wr = Mreg.filter (fun ({reg_its = s} as r) fs ->
    if Spv.is_empty fs && not (s.its_private && s.its_mutable)
    then invalid_arg "Ity.eff_write";
804 805
    Spv.iter (check_mutable_field "Ity.eff_write" r) fs;
    Sreg.mem r kn) wr in
806 807
  reset_taints { eff_empty with eff_reads = rd; eff_writes = wr;
                                eff_covers = Mreg.domain wr }
808

809
(*TODO: should we use it and what semantics to give? *)
810 811 812
let eff_reset ({eff_writes = wr} as e) rs =
  if not (Mreg.set_disjoint wr rs) then invalid_arg "Ity.eff_reset";
  { e with eff_resets = Sreg.union rs e.eff_resets }
813 814

exception IllegalAssign of region * region * region
815

816
let rec ity_skel_check t1 t2 =
817
  if not (ity_equal t1 t2) then
818
  match t1.ity_node, t2.ity_node with
819 820 821 822 823 824 825 826
  | Ityreg {reg_its = s1; reg_args = tl1; reg_regs = rl1},
    Ityreg {reg_its = s2; reg_args = tl2; reg_regs = rl2}
  | Ityapp (s1,tl1,rl1), Ityapp (s2,tl2,rl2)
    when its_equal s1 s2 ->
      List.iter2 ity_skel_check tl1 tl2;
      List.iter2 ity_skel_check rl1 rl2
  | Ityvar (v1,p1), Ityvar (v2,p2)
    when tv_equal v1 v2 && p1 = p2 -> ()
827 828
  | _ -> raise (TypeMismatch (t1,t2,isb_empty))

829
let eff_assign asl =
830
  (* compute all effects except eff_resets *)
831 832 833 834 835
  let get_reg = function
    | {pv_ity = {ity_node = Ityreg r}} -> r
    | _ -> invalid_arg "Ity.eff_assign" in
  let writes = List.fold_left (fun wr (r,f,v) ->
    let r = get_reg r and ity = v.pv_ity in
836
    check_mutable_field "Ity.eff_assign" r f;
837
    if r.reg_its.its_private then raise (AssignPrivate r);
838
    Mreg.change (fun fs -> Some (match fs with
839
      | Some fs -> Mpv.add_new (DuplicateField (r,f)) f ity fs
840 841 842 843 844 845 846 847 848
      | None    -> Mpv.singleton f ity)) r wr) Mreg.empty asl in
  let ghost = List.for_all (fun (r,f,v) ->
    r.pv_ghost || f.pv_ghost || v.pv_ghost) asl in
  let taint = List.fold_left (fun s (r,f,v) ->
    if (r.pv_ghost || v.pv_ghost) && not f.pv_ghost then
      Sreg.add (get_reg r) s else s) Sreg.empty asl in
  let reads = List.fold_left (fun s (r,_,v) ->
    Spv.add r (Spv.add v s)) Spv.empty asl in
  check_taints taint reads;
849
  (* compute the region transitions under writes *)
850
  let reg_rexp {reg_its = s; reg_args = tl; reg_regs = rl} fs =
851
    let ity_rexp xl t = ity_exp_fold (fun l r -> r :: l) xl t in
852 853
    let sbs = its_match_regs s tl rl in
    let mfield xl f =
854
      let tf = ity_full_inst sbs f.pv_ity in
855 856 857
      let tt = Mpv.find_def tf f fs in
      ity_skel_check tf tt; ity_rexp xl tt in
    let xl = List.fold_left mfield [] s.its_mfields in
858 859
    let frozen xl frz t = if frz then ity_rexp xl t else xl in
    dfold2 frozen xl s.its_arg_frz tl s.its_reg_frz rl in
860 861 862 863
  let rec stitch pl rf rt fs =
    let link pl rf rt =
      stitch ((rf,rt)::pl) rf rt (Mreg.find_def Mpv.empty rt writes) in
    List.fold_left2 link pl (reg_rexp rf Mpv.empty) (reg_rexp rt fs) in
864
  let add_write r fs m =
865 866 867 868 869
    let pl = stitch [] r r fs in
    let fit m = Some (match m with
      | Some m -> Mreg.add r pl m
      | None -> Mreg.singleton r pl) in
    Mint.change fit (- List.length pl) m in
870
  let m = Mreg.fold add_write writes Mint.empty in
871
  (* compute resets as non-identity region transitions *)
872 873 874 875
  let add_bind r1 r2 m = Mreg.change (function
    | (Some r3) as v when reg_equal r2 r3 -> v
    | Some r3 -> raise (IllegalAssign (r1,r2,r3))
    | None -> Some r2) r1 m in
876
  let add_pair (rst, mt, mf) (r1,r2) =
877 878
    let rst = if reg_equal r1 r2 then rst
    else Sreg.add r1 (Sreg.add r2 rst) in
879
    rst, add_bind r1 r2 mt, add_bind r2 r1 mf in
880
  let add_write r pl ((rst,_,_) as acc) =
881
    if Sreg.mem r rst then acc else
882
    List.fold_left add_pair acc pl in
883 884
  let add_level _ mpl acc =
    Mreg.fold add_write mpl acc in
885
  let resets,_,_ = Mint.fold add_level m (Sreg.empty,Mreg.empty,Mreg.empty) in
886
  (* construct the effect *)
887 888 889
  { eff_reads  = reads;
    eff_writes = Mreg.map Mpv.domain writes;
    eff_taints = taint;
890 891
    eff_covers = Mreg.domain (Mreg.set_diff writes resets);
    eff_resets = resets;
892 893 894 895
    eff_raises = Sexn.empty;
    eff_oneway = false;
    eff_ghost  = ghost }

896 897 898
let eff_reset_overwritten ({eff_writes = wr} as e) =
  if not (Sreg.is_empty e.eff_resets) then
    invalid_arg "Ity.eff_reset_overwritten";
899 900
  let rec reg2 regs reg =
    if Mreg.mem reg wr then regs else
901 902
    reg_exp_fold reg2 (Sreg.add reg regs) reg in
  let ity2 regs ity = ity_exp_fold reg2 regs ity in
903
  let add_write ({reg_its = s} as r) fs (svv, rst) =
904 905
    let frozen svv frz t = if frz then ity2 svv t else svv in
    let svv = dfold2 frozen (Sreg.add r svv)
906
      s.its_arg_frz r.reg_args s.its_reg_frz r.reg_regs in
907
    let sbs = its_match_regs s r.reg_args r.reg_regs in
908 909 910 911
    let add_mfld (svv,rst) f =
      let t = ity_full_inst sbs f.pv_ity in
      if Spv.mem f fs then svv, ity2 rst t else ity2 svv t, rst in
    List.fold_left add_mfld (svv,rst) s.its_mfields in
912 913
  let svv, rst = Mreg.fold add_write wr (Sreg.empty,Sreg.empty) in
  { e with eff_resets = Sreg.diff rst svv }
914

915 916
let eff_raise e x = { e with eff_raises = Sexn.add x e.eff_raises }
let eff_catch e x = { e with eff_raises = Sexn.remove x e.eff_raises }
917 918 919 920 921

let merge_fields _ f1 f2 = Some (Spv.union f1 f2)

let remove_stale e srg =
  Mreg.filter (fun r _ -> not (reg_r_stale e.eff_resets e.eff_covers r)) srg
922 923 924 925 926

let eff_union e1 e2 = {
  eff_reads  = Spv.union e1.eff_reads e2.eff_reads;
  eff_writes = Mreg.union merge_fields e1.eff_writes e2.eff_writes;
  eff_taints = Sreg.union e1.eff_taints e2.eff_taints;
927 928 929
  eff_covers = Sreg.union (remove_stale e2 e1.eff_covers)
                          (remove_stale e1 e2.eff_covers);
  eff_resets = Sreg.union e1.eff_resets e2.eff_resets;
930 931 932 933
  eff_raises = Sexn.union e1.eff_raises e2.eff_raises;
  eff_oneway = e1.eff_oneway || e2.eff_oneway;
  eff_ghost  = e2.eff_ghost }

934 935 936 937 938 939 940 941
(* TODO: remove later *)
let eff_union e1 e2 =
  let e = eff_union e1 e2 in
  assert (Sreg.disjoint e.eff_covers e.eff_resets);
  assert (Mreg.for_all (fun r _ -> reg_r_stale e.eff_resets e.eff_covers r)
            (Mreg.set_diff e.eff_writes e.eff_covers) );
  e

942 943 944 945 946 947 948 949 950 951 952 953 954 955 956
let eff_contagious e = e.eff_ghost &&
  not (Sexn.is_empty e.eff_raises (* && no local exceptions *))

let eff_union_par e1 e2 =
  let e1 = eff_ghostify e2.eff_ghost e1 in
  let e2 = eff_ghostify e1.eff_ghost e2 in
  check_taints e1.eff_taints e2.eff_reads;
  check_taints e2.eff_taints e1.eff_reads;
  eff_union e1 e2

let eff_union_seq e1 e2 =
  let e1 = eff_ghostify e2.eff_ghost e1 in
  let e2 = eff_ghostify (eff_contagious e1) e2 in
  check_taints e1.eff_taints e2.eff_reads;
  check_taints e2.eff_taints e1.eff_reads;
957
  check_covers e1 e2.eff_reads;
958 959 960 961 962 963 964 965 966
  eff_union e1 e2

(* NOTE: do not export this function *)
let eff_inst sbs e =
  (* all modified or reset regions in e must be instantiated into
     distinct regions. We allow regions that are not affected directly
     to be aliased, even if they contain modified or reset subregions:
     the values are still updated at the same program points and with
     the same postconditions, as in the initial verified code. *)
967
  let inst src = Mreg.fold (fun r v acc ->
968 969 970
    let t = reg_full_inst sbs r in match t.ity_node with
      | Ityreg r -> Mreg.add_new (IllegalAlias r) r v acc
      | _ -> raise (IllegalSnapshot t)) src Mreg.empty in
971 972 973 974 975
  let writes = inst e.eff_writes in
  let resets = inst e.eff_resets in
  let taints = inst e.eff_taints in
  let covers = inst e.eff_covers in
  let impact = Mreg.merge (fun r fld void -> match fld, void with
976
    | Some _, Some _ -> raise (IllegalAlias r)
977
    | _ -> Some ()) writes resets in
978 979 980 981 982
  (* all type variables and unaffected regions must be instantiated
     outside [impact]. Every region in the instantiated execution
     is either brought in by the type substitution or instantiates
     one of the original regions. *)
  let sreg = Mreg.set_diff sbs.isb_reg e.eff_writes in
983
  let sreg = Mreg.set_diff sreg e.eff_resets in
984 985 986
  let dst = Mreg.fold (fun _ i s -> match i.ity_node with
    | Ityreg r -> Sreg.add r s | _ -> s) sreg Sreg.empty in
  let dst = Mtv.fold (fun _ i s -> ity_freeregs s i) sbs.isb_var dst in
987
  ignore (Mreg.inter (fun r _ _ -> raise (IllegalAlias r)) dst impact);
988 989
  { e with eff_writes = writes; eff_taints = taints;
           eff_covers = covers; eff_resets = resets }
990

991 992
(** specification *)

993 994
type pre = term   (* precondition: pre_fmla *)
type post = term  (* postcondition: eps result . post_fmla *)
995 996 997 998 999

let create_post vs f = t_eps_close vs f

let open_post f = match f.t_node with
  | Teps bf -> t_open_bound bf
1000
  | _ -> invalid_arg "Ity.open_post"
1001

1002 1003 1004 1005 1006
type cty = {
  cty_args   : pvsymbol list;
  cty_pre    : pre list;
  cty_post   : post list;
  cty_xpost  : post list Mexn.t;
1007
  cty_oldies : pvsymbol Mpv.t;
1008 1009 1010
  cty_effect : effect;
  cty_result : ity;
  cty_freeze : ity_subst;
1011 1012
}

1013
let cty_unsafe args pre post xpost oldies effect result freeze = {
1014 1015 1016 1017
  cty_args   = args;
  cty_pre    = pre;
  cty_post   = post;
  cty_xpost  = xpost;
1018
  cty_oldies = oldies;
1019 1020 1021
  cty_effect = effect;
  cty_result = result;
  cty_freeze = freeze;
1022 1023
}

1024 1025 1026 1027 1028 1029 1030 1031 1032
let cty_reads c =
  List.fold_right Spv.remove c.cty_args c.cty_effect.eff_reads

let cty_ghost c = c.cty_effect.eff_ghost

let cty_ghostify gh ({cty_effect = eff} as c) =
  if eff.eff_ghost || not gh then c else
  { c with cty_effect = eff_ghostify gh eff }

1033
let spec_t_fold fn_t acc pre post xpost =
1034
  let fn_l a fl = List.fold_left fn_t a fl in
1035 1036
  let acc = fn_l (fn_l acc pre) post in
  Mexn.fold (fun _ l a -> fn_l a l) xpost acc
1037

1038
let check_tvs reads result pre post xpost =
1039 1040 1041 1042
  (* every type variable in spec comes either from a known vsymbol
     or from the result type. We need this to ensure that we always
     can do a full instantiation. TODO: do we really need this? *)
  let add_pv v s = ity_freevars s v.pv_ity in
1043 1044
  let tvs = ity_freevars Stv.empty result in
  let tvs = Spv.fold add_pv reads tvs in
1045 1046 1047 1048 1049 1050
  let check_tvs () t =
    let ttv = t_ty_freevars Stv.empty t in
    if not (Stv.subset ttv tvs) then Loc.error ?loc:t.t_loc
      (UnboundTypeVar (Stv.choose (Stv.diff ttv tvs))) in
  spec_t_fold check_tvs () pre post xpost

1051 1052 1053 1054 1055 1056 1057 1058 1059
let check_pre pre = List.iter (fun p -> if p.t_ty <> None
  then Loc.error ?loc:p.t_loc (Term.FmlaExpected p)) pre

let check_post exn ity post =
  let ty = ty_of_ity ity in
  List.iter (fun q -> match q.t_node with
    | Teps _ -> Ty.ty_equal_check ty (t_type q)
    | _ -> raise exn) post

1060
let create_cty args pre post xpost oldies effect result =
1061
  let exn = Invalid_argument "Ity.create_cty" in
1062
  (* pre, post, and xpost are well-typed *)
1063 1064
  check_pre pre; check_post exn result post;
  Mexn.iter (fun xs xq -> check_post exn xs.xs_ity xq) xpost;
1065 1066
  (* the arguments must be pairwise distinct *)
  let sarg = List.fold_right (Spv.add_new exn) args Spv.empty in
1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079
  (* complete the reads and freeze the external context.
     oldies must be fresh: collisions with args and external
     reads are forbidden, to simplify instantiation later. *)
  let preads = spec_t_fold t_freepvs sarg pre [] Mexn.empty in
  let qreads = spec_t_fold t_freepvs Spv.empty [] post xpost in
  let effect = eff_read_post effect qreads in
  Mpv.iter (fun {pv_ghost = gh; pv_ity = o} {pv_ity = t} ->
    if not (gh && o == ity_purify t) then raise exn) oldies;
  let oldies = Mpv.set_inter oldies effect.eff_reads in
  let effect = eff_bind oldies effect in
  let preads = Mpv.fold (Util.const Spv.add) oldies preads in
  if not (Mpv.set_disjoint preads oldies) then raise exn;
  let effect = eff_read_pre preads effect in
1080 1081 1082
  let freeze = Spv.diff effect.eff_reads sarg in
  let freeze = Spv.fold freeze_pv freeze isb_empty in
  check_tvs effect.eff_reads result pre post xpost;
1083
  (* remove exceptions whose postcondition is False *)
Andrei Paskevich's avatar
Andrei Paskevich committed
1084 1085 1086 1087 1088
  let filter _ xq () =
    let is_false q = t_equal (snd (open_post q)) t_false in
    if List.exists is_false xq then None else Some xq in
  let xpost = Mexn.inter filter xpost effect.eff_raises in
  let raises = Mexn.set_inter effect.eff_raises xpost in
1089
  let effect = { effect with eff_raises = raises } in
1090 1091 1092 1093 1094
  (* remove effects on unknown regions. We reset eff_taints
     instead of simply filtering the existing set in order
     to get rid of non-ghost writes into ghost regions.
     These writes can occur when a bound regular variable
     aliases an external ghost region:
1095
        let (* non-ghost *) x = None in
1096 1097 1098 1099 1100 1101 1102
        let ghost y = if true then x else Some ghost_ref in
        match x with Some r -> r := 0 | None -> () end
     The write is regular here, but the only path to it, via
     ghost_ref is ghost. Strictly speaking, such writes can
     be removed (we cannot create a real regular alias to a
     ghost location), but it is simpler to just recast them
     as ghost, to keep the type signature consistent. *)
1103 1104
  let rknown = read_regs effect.eff_reads in
  let vknown = ity_rch_regs rknown result in
1105
  let effect = reset_taints { effect with
1106 1107 1108
    eff_writes = Mreg.set_inter effect.eff_writes rknown;
    eff_covers = Mreg.set_inter effect.eff_covers rknown;
    eff_resets = Mreg.set_inter effect.eff_resets vknown} in
1109
  cty_unsafe args pre post xpost oldies effect result freeze
1110 1111

let cty_apply c vl args res =
1112 1113
  let vsb_add vsb {pv_vs = u} v =
    if vs_equal u v.pv_vs then vsb else Mvs.add u v vsb in
1114 1115 1116 1117 1118 1119 1120
  let match_v isb u v = ity_match isb u.pv_ity v.pv_ity in
  (* stage 1: apply c to vl *)
  let rec apply gh same isb vsb ul vl = match ul, vl with
    | u::ul, v::vl ->
        let gh = gh || (v.pv_ghost && not u.pv_ghost) in
        let same = same && ity_equal u.pv_ity v.pv_ity in
        apply gh same (match_v isb u v) (vsb_add vsb u v) ul vl
1121 1122
    | ul, [] ->
        gh, same, isb, vsb, ul
1123 1124
    | _ -> invalid_arg "Ity.cty_apply" in
  let ghost, same, isb, vsb, cargs =
1125 1126 1127
    apply c.cty_effect.eff_ghost true
      c.cty_freeze Mvs.empty c.cty_args vl in
  let freeze = if same then isb else
1128
    List.fold_right freeze_pv vl c.cty_freeze in
1129
  (* stage 2: compute the substitutions *)
1130 1131 1132 1133 1134 1135 1136
  let rec cut same rul rvl vsb ul tl = match ul, tl with
    | u::ul, vt::tl ->
        let same = same && ity_equal u.pv_ity vt in
        let v = if same && Mvs.is_empty vsb then u else
          let id = id_clone u.pv_vs.vs_name in
          create_pvsymbol id ~ghost:u.pv_ghost vt in
        cut same (u::rul) (v::rvl) (vsb_add vsb u v) ul tl
1137
    | [], [] -> same, rul, rvl, vsb
1138
    | _ -> invalid_arg "Ity.cty_apply" in
1139
  let same, rcargs, rargs, vsb = cut same [] [] vsb cargs args in
1140 1141 1142 1143 1144 1145 1146
  let vsb, oldies = if Mvs.is_empty vsb then vsb, c.cty_oldies else
    Mpv.fold (fun {pv_vs = o} v (s,m) ->
      let id = id_clone o.vs_name in
      let v = Mvs.find_def v v.pv_vs vsb in
      let n = create_pvsymbol id ~ghost:true (ity_purify v.pv_ity) in
      Mvs.add o n s, Mpv.add n v m) c.cty_oldies (vsb, Mpv.empty) in
  let vsb = Mvs.map (fun v -> t_var v.pv_vs) vsb in
1147 1148
  let same = same && ity_equal c.cty_result res in
  if same && vl = [] then (* trivial *) c else
1149
  let isb = if same then isb_empty else
1150 1151 1152 1153 1154 1155 1156 1157 1158 1159
    let isb = ity_match isb c.cty_result res in
    List.fold_left2 match_v isb rcargs rargs in
  (* stage 3: instantiate the effect *)
  let effect =
    if same then c.cty_effect else eff_inst isb c.cty_effect in
  let binds = List.fold_right Spv.add c.cty_args Spv.empty in
  let effect = eff_ghostify ghost (eff_bind binds effect) in
  let reads = List.fold_right Spv.add vl Spv.empty in
  let reads = List.fold_right Spv.add rargs reads in
  let effect = eff_read_pre reads effect in
1160 1161 1162
  (* stage 4: instantiate the specification *)
  let tsb = Mtv.map ty_of_ity
    (Mtv.set_union isb.isb_var isb.isb_pur) in
1163 1164 1165 1166 1167
  let same = same || Mtv.for_all (fun v {ty_node = n} ->
    match n with Tyvar u -> tv_equal u v | _ -> false) tsb in
  let subst_t = if same then (fun t -> t_subst vsb t) else
                      (fun t -> t_ty_subst tsb vsb t) in
  let subst_l l = List.map subst_t l in
1168 1169
  cty_unsafe (List.rev rargs) (subst_l c.cty_pre)
    (subst_l c.cty_post) (Mexn.map subst_l c.cty_xpost)
1170
    oldies effect res freeze
1171 1172 1173 1174

let cty_add_reads c pvs =
  (* the external reads are already frozen and
     the arguments should stay instantiable *)
1175 1176
  let pvs = Spv.diff pvs c.cty_effect.eff_reads in
  { c with cty_effect = eff_read_pre pvs c.cty_effect;
1177 1178
           cty_freeze = Spv.fold freeze_pv pvs c.cty_freeze }

1179
let cty_add_pre pre c = if pre = [] then c else begin check_pre pre;
1180
  let c = cty_add_reads c (List.fold_left t_freepvs Spv.empty pre) in
1181 1182
  check_tvs c.cty_effect.eff_reads c.cty_result pre [] Mexn.empty;
  { c with cty_pre = pre @ c.cty_pre } end
1183

1184
let cty_add_post c post = if post = [] then c else begin
1185
  check_post (Invalid_argument "Ity.cty_add_post") c.cty_result post