expr.ml 54.9 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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
open Wstdlib
13
open Ident
14
open Ty
15 16 17
open Term
open Ity

18 19 20 21 22 23 24
(** {2 Routine symbols} *)

type rsymbol = {
  rs_name  : ident;
  rs_cty   : cty;
  rs_logic : rs_logic;
  rs_field : pvsymbol option;
25 26
}

27 28 29 30 31
and rs_logic =
  | RLnone            (* non-pure symbol *)
  | RLpv of pvsymbol  (* local let-function *)
  | RLls of lsymbol   (* top-level let-function or let-predicate *)
  | RLlemma           (* top-level or local let-lemma *)
32

33 34 35
module Rsym = MakeMSHW (struct
  type t = rsymbol
  let tag rs = rs.rs_name.id_tag
36 37
end)

38 39 40 41
module Srs = Rsym.S
module Mrs = Rsym.M
module Hrs = Rsym.H
module Wrs = Rsym.W
42

43 44 45
let rs_equal : rsymbol -> rsymbol -> bool = (==)
let rs_hash rs = id_hash rs.rs_name
let rs_compare rs1 rs2 = id_compare rs1.rs_name rs2.rs_name
46

47 48
let mk_rs, restore_rs =
  let ls_to_rs = Wls.create 17 in
49
  (fun id cty lg mf ->
50 51 52 53 54
    let rs = {
      rs_name  = id;
      rs_cty   = cty;
      rs_logic = lg;
      rs_field = mf;
55
    } in
Andrei Paskevich's avatar
Andrei Paskevich committed
56
    match lg with
57 58 59 60 61
    | RLls ls -> Wls.set ls_to_rs ls rs; rs
    | _ -> rs),
  (fun ls -> Wls.find ls_to_rs ls)

type rs_kind =
62 63 64 65 66 67
  | RKnone    (* non-pure symbol *)
  | RKlocal   (* local let-function *)
  | RKfunc    (* top-level let-function *)
  | RKpred    (* top-level let-predicate *)
  | RKlemma   (* top-level or local let-lemma *)

68 69 70 71 72 73
let rs_kind s = match s.rs_logic with
  | RLnone  -> RKnone
  | RLpv _  -> RKlocal
  | RLls ls -> if ls.ls_value = None then RKpred else RKfunc
  | RLlemma -> RKlemma

74 75
let rs_ghost s = s.rs_cty.cty_effect.eff_ghost

76
let check_effects ?loc c =
77 78
  if c.cty_effect.eff_oneway then Loc.errorm ?loc
    "This function may not terminate, it cannot be used as pure";
79
  if not (cty_pure c) then Loc.errorm ?loc
80
    "This function has side effects, it cannot be used as pure"
81 82

let check_reads ?loc c =
83 84 85 86
  if not (Spv.is_empty (cty_reads c)) then Loc.errorm ?loc
    "This function depends on external variables, it cannot be used as pure"

let check_state ?loc c =
87
  if not (Mreg.is_empty c.cty_freeze.isb_reg) then Loc.errorm ?loc
88 89 90 91 92 93 94
    "This function is stateful, it cannot be used as pure"

let cty_ghostify ?loc gh c = try cty_ghostify gh c with
  | BadGhostWrite (v,_) -> Loc.errorm ?loc
      "This ghost function modifies the non-ghost variable %a" print_pv v
  | GhostDivergence -> Loc.errorm ?loc
      "This ghost function may not terminate"
95 96 97 98 99

let cty_purify c =
  let add a ity = ity_func (ity_purify a.pv_ity) ity in
  List.fold_right add c.cty_args (ity_purify c.cty_result)

100
let make_post t = match t.t_ty with
101 102
  | Some ty ->
      let res = create_vsymbol (id_fresh "result") ty in
103
      create_post res (t_equ (t_var res) t)
104 105
  | None ->
      let res = create_vsymbol (id_fresh "result") ty_bool in
106 107 108
      create_post res (t_iff (t_equ (t_var res) t_bool_true) t)

let add_post c t = cty_add_post c [make_post t]
109 110

let create_rsymbol ({pre_loc=loc} as id) ?(ghost=false) ?(kind=RKnone) c =
111
  let arg_list c = List.map (fun a -> t_var a.pv_vs) c.cty_args in
112 113
  let arg_type c = List.map (fun a -> a.pv_vs.vs_ty) c.cty_args in
  let res_type c = ty_of_ity c.cty_result in
114
  let c = cty_ghostify ?loc ghost c in
115
  match kind with
116
  | RKnone ->
117
      mk_rs (id_register id) c RLnone None
118
  | RKlocal ->
119
      check_effects ?loc c; check_state ?loc c;
120 121 122
      (* When declaring local let-functions, we need to create a
         mapping vsymbol to use in assertions. As vsymbols are not
         generalisable, we have to freeze the type variables (but
123
         not regions) of the rsymbol, and the easiest way to do that
124
         is to make these type variables appear in (cty_reads c).
125 126 127 128
         Moreover, we want to maintain the invariant that every
         variable that occurs freely in an assertion comes from
         a pvsymbol. Therefore, we create a pvsymbol whose type
         is a snapshot of the appropriate mapping type, and put
129
         it into the rs_logic field. This pvsymbol should not be
130
         used in the program, as it has lost all preconditions,
131 132
         which is why we declare it as ghost. In other words,
         this pvsymbol behaves exactly as Epure of its pv_vs. *)
133
      let v = create_pvsymbol ~ghost:true id (cty_purify c) in
134
      let t = t_func_app_l (t_var v.pv_vs) (arg_list c) in
135
      mk_rs v.pv_vs.vs_name (add_post c t) (RLpv v) None
136 137 138
  | RKfunc ->
      check_effects ?loc c; check_reads ?loc c;
      let ls = create_fsymbol id (arg_type c) (res_type c) in
139
      let t = t_app ls (arg_list c) ls.ls_value in
140
      mk_rs ls.ls_name (add_post c t) (RLls ls) None
141
  | RKpred ->
142 143 144 145
      check_effects ?loc c; check_reads ?loc c;
      if not (ity_equal c.cty_result ity_bool) then Loc.errorm ?loc
        "This function returns a value of type %a, it cannot be \
          declared as a pure predicate" print_ity c.cty_result;
146 147
      let ls = create_psymbol id (arg_type c) in
      let f = t_app ls (arg_list c) None in
148
      mk_rs ls.ls_name (add_post c f) (RLls ls) None
149
  | RKlemma ->
150
      check_effects ?loc c;
151
      mk_rs (id_register id) c RLlemma None
152

153 154
let rs_dup ({rs_name = {id_loc = loc}} as s) c =
  let id = id_register (id_clone s.rs_name) in
155
  let c = cty_ghostify ?loc (rs_ghost s) c in
156 157
  match s.rs_logic with
  | RLnone ->
158
      mk_rs id c RLnone None
159
  | RLpv v ->
160 161
      check_effects ?loc c; check_state ?loc c;
      Loc.try2 ?loc ity_equal_check v.pv_ity (cty_purify c);
162 163
      let al = List.map (fun a -> t_var a.pv_vs) c.cty_args in
      let t = t_func_app_l (t_var v.pv_vs) al in
164
      mk_rs id (add_post c t) (RLpv v) None
165 166 167 168
  | RLls _ ->
      invalid_arg "Expr.rs_dup"
  | RLlemma ->
      check_effects ?loc c;
169
      mk_rs id c RLlemma None
170

Andrei Paskevich's avatar
Andrei Paskevich committed
171 172
let create_projection s v =
  let id = id_clone v.pv_vs.vs_name in
173 174
  let eff = eff_ghostify v.pv_ghost eff_empty in
  let tyl = List.map ity_var s.its_ts.ts_args in
175 176
  let rgl = List.map ity_reg s.its_regions in
  let ity = ity_app s tyl rgl in
177 178
  let arg = create_pvsymbol (id_fresh "arg") ity in
  let ls = create_fsymbol id [arg.pv_vs.vs_ty] v.pv_vs.vs_ty in
179
  let q = make_post (fs_app ls [t_var arg.pv_vs] v.pv_vs.vs_ty) in
180
  let c = create_cty [arg] [] [q] Mxs.empty Mpv.empty eff v.pv_ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
181 182 183 184 185
  mk_rs ls.ls_name c (RLls ls) (Some v)

exception FieldExpected of rsymbol

let mfield_of_rs s = match s.rs_cty.cty_args, s.rs_field with
186 187
  | [{pv_ity = {ity_node = Ityreg {reg_its = its}}}], Some f
    when List.exists (pv_equal f) its.its_mfields -> f
Andrei Paskevich's avatar
Andrei Paskevich committed
188
  | _ -> raise (FieldExpected s)
Andrei Paskevich's avatar
Andrei Paskevich committed
189

190 191 192
let create_constructor ~constr id s fl =
  let exn = Invalid_argument "Expr.create_constructor" in
  let fs = List.fold_right (Spv.add_new exn) fl Spv.empty in
193
  if List.exists (fun f -> not (Spv.mem f fs)) s.its_mfields ||
194
    s.its_private || s.its_def <> NoDef || constr < 1 ||
195
    (s.its_mutable && constr > 1) then raise exn;
196 197
  let argl = List.map (fun a -> a.pv_vs.vs_ty) fl in
  let tyl = List.map ity_var s.its_ts.ts_args in
198 199
  let rgl = List.map ity_reg s.its_regions in
  let ity = ity_app s tyl rgl in
200 201 202
  let ty = ty_of_ity ity in
  let ls = create_fsymbol ~constr id argl ty in
  let argl = List.map (fun a -> t_var a.pv_vs) fl in
203
  let q = make_post (fs_app ls argl ty) in
204 205 206
  let eff = match ity.ity_node with
    | Ityreg r -> eff_reset eff_empty (Sreg.singleton r)
    | _ -> eff_empty in
207
  let c = create_cty fl [] [q] Mxs.empty Mpv.empty eff ity in
208
  mk_rs ls.ls_name c (RLls ls) None
209

210
let rs_of_ls ls =
Andrei Paskevich's avatar
Andrei Paskevich committed
211 212 213
  let v_args = List.map (fun ty ->
    create_pvsymbol (id_fresh "u") (ity_of_ty ty)) ls.ls_args in
  let t_args = List.map (fun v -> t_var v.pv_vs) v_args in
214
  let q = make_post (t_app ls t_args ls.ls_value) in
215 216 217
  let ity = ity_of_ty (t_type q) and eff = eff_empty in
  let eff = if ls.ls_constr = 0 then eff_spoil eff ity else eff in
  let c = create_cty v_args [] [q] Mxs.empty Mpv.empty eff ity in
218 219
  mk_rs ls.ls_name c (RLls ls) None

220 221 222 223 224 225 226 227
let ls_of_rs rs = match rs.rs_logic with
  | RLls ls -> ls
  | _ -> invalid_arg "Expr.ls_of_rs"

let fd_of_rs rs = match rs.rs_field with
  | Some fd -> fd
  | _ -> invalid_arg "Expr.fd_of_rs"

Andrei Paskevich's avatar
Andrei Paskevich committed
228 229
(** {2 Program patterns} *)

230 231 232 233 234
type pat_ghost =
  | PGfail  (* refutable ghost subpattern before "|" *)
  | PGlast  (* refutable ghost subpattern otherwise  *)
  | PGnone  (* every ghost subpattern is irrefutable *)

Andrei Paskevich's avatar
Andrei Paskevich committed
235
type prog_pattern = {
236 237 238 239
  pp_pat  : pattern;    (* pure pattern *)
  pp_ity  : ity;        (* type of the matched value *)
  pp_mask : mask;       (* mask of the matched value *)
  pp_fail : pat_ghost;  (* refutable ghost subpattern *)
Andrei Paskevich's avatar
Andrei Paskevich committed
240 241 242 243
}

type pre_pattern =
  | PPwild
244
  | PPvar of preid * bool
245
  | PPapp of rsymbol * pre_pattern list
246
  | PPas  of pre_pattern * preid * bool
Andrei Paskevich's avatar
Andrei Paskevich committed
247 248
  | PPor  of pre_pattern * pre_pattern

249
exception ConstructorExpected of rsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
250

251
let create_prog_pattern pp ity mask =
252
  let fail = ref PGnone in
253
  let hg = Hstr.create 3 in
254 255 256 257 258 259 260
  let mark {pre_name = nm} gh mask =
    if gh || mask_ghost mask then Hstr.replace hg nm () in
  let rec scan gp mask = function
    | PPapp ({rs_logic = RLls ls} as rs, pl) when ls.ls_constr > 0 ->
        if mask = MaskGhost && ls.ls_constr > 1 && !fail <> PGfail
        then fail := gp; (* we do not replace PGfail with PGlast *)
        let ml = match mask with
261 262
          | MaskGhost -> List.map (Util.const MaskGhost) ls.ls_args
          | MaskVisible -> List.map mask_of_pv rs.rs_cty.cty_args
263 264
          | MaskTuple ml when is_fs_tuple ls &&
              List.length ls.ls_args = List.length ml -> ml
265
          | MaskTuple _ -> invalid_arg "Expr.create_prog_pattern" in
266 267
        (try List.iter2 (scan gp) ml pl with Invalid_argument _ ->
          raise (Term.BadArity (ls, List.length pl)))
268
    | PPapp (rs,_) -> raise (ConstructorExpected rs)
269 270 271
    | PPvar (id,gh) -> mark id gh mask
    | PPas (pp,id,gh) -> mark id gh mask; scan gp mask pp
    | PPor (pp1,pp2) -> scan PGfail mask pp1; scan gp mask pp2
272
    | PPwild -> () in
273
  scan PGlast mask pp;
Andrei Paskevich's avatar
Andrei Paskevich committed
274
  let hv = Hstr.create 3 in
275 276 277
  let find ({pre_name = nm} as id) ity =
    try let v = Hstr.find hv nm in
      ity_equal_check ity v.pv_ity; v.pv_vs
Andrei Paskevich's avatar
Andrei Paskevich committed
278
    with Not_found ->
279 280 281 282 283 284 285 286 287 288 289 290 291 292
      let v = create_pvsymbol id ~ghost:(Hstr.mem hg nm) ity in
      Hstr.add hv nm v; v.pv_vs in
  let rec make ity = function
    | PPapp ({rs_cty = cty; rs_logic = RLls ls}, ppl) ->
        let sbs = ity_match isb_empty cty.cty_result ity in
        let make arg pp = make (ity_full_inst sbs arg.pv_ity) pp in
        pat_app ls (List.map2 make cty.cty_args ppl) (ty_of_ity ity)
    | PPapp (rs,_) -> raise (ConstructorExpected rs)
    | PPvar (id,_) -> pat_var (find id ity)
    | PPas (pp,id,_) -> pat_as (make ity pp) (find id ity)
    | PPor (pp1,pp2) -> pat_or (make ity pp1) (make ity pp2)
    | PPwild -> pat_wild (ty_of_ity ity) in
  let pat = make ity pp in
  let mvs = Hstr.fold Mstr.add hv Mstr.empty in
293
  mvs, {pp_pat = pat; pp_ity = ity; pp_mask = mask; pp_fail = !fail}
Andrei Paskevich's avatar
Andrei Paskevich committed
294

Andrei Paskevich's avatar
Andrei Paskevich committed
295 296 297 298 299 300 301 302 303 304 305 306
(** {2 Program expressions} *)

type assertion_kind = Assert | Assume | Check

type for_direction = To | DownTo

type for_bounds = pvsymbol * for_direction * pvsymbol

type invariant = term

type variant = term * lsymbol option (** tau * (tau -> tau -> prop) *)

307
type assign = pvsymbol * rsymbol * pvsymbol (* region * field * value *)
308

Andrei Paskevich's avatar
Andrei Paskevich committed
309 310
type expr = {
  e_node   : expr_node;
311
  e_ity    : ity;
312
  e_mask   : mask;
Andrei Paskevich's avatar
Andrei Paskevich committed
313
  e_effect : effect;
Andrei Paskevich's avatar
Andrei Paskevich committed
314
  e_attrs  : Sattr.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
315 316 317 318 319
  e_loc    : Loc.position option;
}

and expr_node =
  | Evar    of pvsymbol
320
  | Econst  of Number.constant
321
  | Eexec   of cexp * cty
322
  | Eassign of assign list
Andrei Paskevich's avatar
Andrei Paskevich committed
323 324
  | Elet    of let_defn * expr
  | Eif     of expr * expr * expr
325
  | Ematch  of expr * reg_branch list * exn_branch Mxs.t
Andrei Paskevich's avatar
Andrei Paskevich committed
326
  | Ewhile  of expr * invariant list * variant list * expr
327
  | Efor    of pvsymbol * for_bounds * pvsymbol * invariant list * expr
Andrei Paskevich's avatar
Andrei Paskevich committed
328
  | Eraise  of xsymbol * expr
329
  | Eexn    of xsymbol * expr
Andrei Paskevich's avatar
Andrei Paskevich committed
330
  | Eassert of assertion_kind * term
331
  | Eghost  of expr
Andrei Paskevich's avatar
Andrei Paskevich committed
332
  | Epure   of term
Andrei Paskevich's avatar
Andrei Paskevich committed
333 334
  | Eabsurd

335 336 337 338
and reg_branch = prog_pattern * expr

and exn_branch = pvsymbol list * expr

339 340 341
and cexp = {
  c_node : cexp_node;
  c_cty  : cty;
Andrei Paskevich's avatar
Andrei Paskevich committed
342 343
}

344 345
and cexp_node =
  | Capp of rsymbol * pvsymbol list
346
  | Cpur of lsymbol * pvsymbol list
347 348
  | Cfun of expr
  | Cany
Andrei Paskevich's avatar
Andrei Paskevich committed
349

350 351 352 353 354 355 356 357 358 359
and let_defn =
  | LDvar of pvsymbol * expr
  | LDsym of rsymbol * cexp
  | LDrec of rec_defn list

and rec_defn = {
  rec_sym  : rsymbol; (* exported symbol *)
  rec_rsym : rsymbol; (* internal symbol *)
  rec_fun  : cexp;    (* Cfun *)
  rec_varl : variant list;
Andrei Paskevich's avatar
Andrei Paskevich committed
360
}
361

Andrei Paskevich's avatar
Andrei Paskevich committed
362
(* basic tools *)
363

Andrei Paskevich's avatar
Andrei Paskevich committed
364
let e_attr_set ?loc l e = { e with e_attrs = l; e_loc = loc }
365

Andrei Paskevich's avatar
Andrei Paskevich committed
366
let e_attr_add l e = { e with e_attrs = Sattr.add l e.e_attrs }
367

Andrei Paskevich's avatar
Andrei Paskevich committed
368 369
let e_attr_copy { e_attrs = attrs; e_loc = loc } e =
  let attrs = Sattr.union attrs e.e_attrs in
370
  let loc = if e.e_loc = None then loc else e.e_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
371
  { e with e_attrs = attrs; e_loc = loc }
372

Andrei Paskevich's avatar
Andrei Paskevich committed
373 374
let proxy_attr = create_attribute "whyml_proxy_symbol"
let proxy_attrs = Sattr.singleton proxy_attr
375

Andrei Paskevich's avatar
Andrei Paskevich committed
376
let rec e_attr_push ?loc l e = match e.e_node with
377 378
  | (Elet (LDvar ({pv_vs = {vs_name = id}},_) as ld, e1)
  |  Elet (LDsym ({rs_name = id},_) as ld, e1))
Andrei Paskevich's avatar
Andrei Paskevich committed
379 380
    when Sattr.mem proxy_attr id.id_attrs ->
      let e1 = e_attr_push ?loc l e1 in
381 382
      { e with e_node = Elet (ld, e1); e_loc = loc }
  | _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
383 384
      let l = Sattr.union l e.e_attrs in
      { e with e_attrs = l; e_loc = loc }
385

386 387
let e_ghost e = e.e_effect.eff_ghost
let c_ghost c = c.c_cty.cty_effect.eff_ghost
Andrei Paskevich's avatar
Andrei Paskevich committed
388

389
(* e_fold never goes under cexps *)
Andrei Paskevich's avatar
Andrei Paskevich committed
390
let e_fold fn acc e = match e.e_node with
391 392
  | Evar _ | Econst _ | Eexec _ | Eassign _
  | Eassert _ | Epure _ | Eabsurd -> acc
393
  | Eraise (_,e) | Efor (_,_,_,_,e) | Eghost e
394
  | Elet ((LDsym _|LDrec _), e) | Eexn (_,e) -> fn acc e
395
  | Elet (LDvar (_,d), e) | Ewhile (d,_,_,e) -> fn (fn acc d) e
Andrei Paskevich's avatar
Andrei Paskevich committed
396
  | Eif (c,d,e) -> fn (fn (fn acc c) d) e
397
  | Ematch (d,bl,xl) -> Mxs.fold (fun _ (_,e) acc -> fn acc e) xl
398
      (List.fold_left (fun acc (_,e) -> fn acc e) (fn acc d) bl)
Andrei Paskevich's avatar
Andrei Paskevich committed
399

400 401 402 403 404 405 406 407
exception FoundExpr of Loc.position option * expr

(* find a minimal sub-expression whose effect satisfies [pr] *)
let find_effect pr loc e =
  let rec find loc e =
    if not (pr e.e_effect) then loc else
    let loc = if e.e_loc = None then loc else e.e_loc in
    let loc = match e.e_node with
408 409
      | Eexec ({c_node = Cfun d},_) -> find loc d
      | _ ->                    e_fold find loc e in
410 411 412 413 414 415 416 417 418
    raise (FoundExpr (loc,e)) in
  try find loc e, e with FoundExpr (loc,e) -> loc, e

let e_locate_effect pr e = fst (find_effect pr None e)

(* localize an illegal ghost write *)
let localize_ghost_write v r el =
  let taints eff = Mreg.mem r eff.eff_taints in
  let writes eff = match Mreg.find_opt r eff.eff_writes with
419
    | Some fds -> r.reg_its.its_private ||
420 421 422 423 424 425 426 427 428 429 430 431 432
        Spv.exists (fun fd -> not fd.pv_ghost) fds
    | None -> false in
  (* check if some component taints region r *)
  List.iter (fun e -> if taints e.e_effect then
    let loc, e = find_effect taints None e in
    let loc, _ = find_effect writes loc e in
    Loc.error ?loc (BadGhostWrite (v,r))) el;
  (* we are ghostified, check if someone writes into r *)
  List.iter (fun e -> if writes e.e_effect then
    let loc = e_locate_effect writes e in
    Loc.error ?loc (BadGhostWrite (v,r))) el;
  raise (BadGhostWrite (v,r))

433 434 435 436 437 438 439 440
(* localize a write into an immutable position *)
let localize_immut_write v r el =
  let writes eff = Mreg.mem r eff.eff_writes in
  List.iter (fun e -> if writes e.e_effect then
    let loc = e_locate_effect writes e in
    Loc.error ?loc (IllegalUpdate (v,r))) el;
  raise (IllegalUpdate (v,r))

441 442 443 444 445 446 447 448
(* localize a reset effect *)
let localize_reset_stale v r el =
  let resets eff =
    if Sreg.mem r eff.eff_resets then
      ity_r_stale (Sreg.singleton r) eff.eff_covers v.pv_ity
    else false in
  List.iter (fun e -> if resets e.e_effect then
    let loc = e_locate_effect resets e in
449 450 451 452 453 454 455 456 457 458 459 460 461
    Loc.error ?loc (StaleVariable (v,r))) el;
  raise (StaleVariable (v,r))

(* localize a divergence *)
let localize_divergence el =
  let diverges eff = eff.eff_oneway in
  List.iter (fun e -> if diverges e.e_effect then
    let loc = e_locate_effect diverges e in
    Loc.error ?loc GhostDivergence) el;
  raise GhostDivergence

let try_effect el fn x y = try fn x y with
  | BadGhostWrite (v,r) -> localize_ghost_write v r el
462
  | IllegalUpdate (v,r) -> localize_immut_write v r el
463
  | StaleVariable (v,r) -> localize_reset_stale v r el
464
  | GhostDivergence     -> localize_divergence el
Andrei Paskevich's avatar
Andrei Paskevich committed
465

466 467
(* smart constructors *)

468
let mk_expr node ity mask eff = {
469
  e_node   = node;
470
  e_ity    = ity;
471
  e_mask   = mask_adjust eff ity mask;
472
  e_effect = eff;
Andrei Paskevich's avatar
Andrei Paskevich committed
473
  e_attrs  = Sattr.empty;
474 475 476
  e_loc    = None;
}

477 478 479 480
let mk_cexp node cty = {
  c_node   = node;
  c_cty    = cty;
}
481

482
let e_var ({pv_ity = ity; pv_ghost = ghost} as v) =
483 484
  let eff = eff_ghostify ghost (eff_read_single v) in
  mk_expr (Evar v) ity MaskVisible eff
485

486 487
let e_const c ity =
  Term.check_literal c (ty_of_ity ity);
488
  mk_expr (Econst c) ity MaskVisible eff_empty
489 490

let e_nat_const n =
491
  assert (n >= 0);
492
  e_const (Number.const_of_int n) ity_int
493

494
let e_ghostify gh ({e_effect = eff} as e) =
495 496 497
  if not gh then e else
  let eff = try_effect [e] eff_ghostify gh eff in
  mk_expr (Eghost e) e.e_ity e.e_mask eff
498

499 500
let c_cty_ghostify gh ({c_cty = cty} as c) =
  if not gh || cty.cty_effect.eff_ghost then cty else
501
  let el = match c.c_node with Cfun e -> [e] | _ -> [] in
502
  try_effect el Ity.cty_ghostify gh cty
503

504 505 506 507 508 509
(* purify expressions *)

let rs_true  = rs_of_ls fs_bool_true
let rs_false = rs_of_ls fs_bool_false

let is_e_true e = match e.e_node with
510
  | Eexec ({c_node = Capp (s,[])},_) -> rs_equal s rs_true
511 512 513
  | _ -> false

let is_e_false e = match e.e_node with
514
  | Eexec ({c_node = Capp (s,[])},_) -> rs_equal s rs_false
515 516 517 518 519 520 521
  | _ -> false

let t_void = t_tuple []

let is_rlpv s = match s.rs_logic with
  | RLpv _ -> true | _ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
522 523
let copy_attrs e t =
  if e.e_loc = None && Sattr.is_empty e.e_attrs then t else
524
  let loc = if t.t_loc = None then e.e_loc else t.t_loc in
Andrei Paskevich's avatar
Andrei Paskevich committed
525
  t_attr_set ?loc (Sattr.union e.e_attrs t.t_attrs) t
526

527 528 529 530
let term_of_fmla f = match f.t_node with
  | _ when f.t_ty <> None -> f
  | Tapp (ps, [t; {t_node = Tapp (fs,[])}])
    when ls_equal ps ps_equ && ls_equal fs fs_bool_true -> t
Andrei Paskevich's avatar
Andrei Paskevich committed
531 532
  | _ -> t_attr_set ?loc:f.t_loc Sattr.empty
      (t_if_simp f t_bool_true t_bool_false)
533 534 535 536 537

let fmla_of_term t = match t.t_node with
  | _ when t.t_ty = None -> t
  | Tif (f, {t_node = Tapp (fs1,[])}, {t_node = Tapp (fs2,[])})
    when ls_equal fs1 fs_bool_true && ls_equal fs2 fs_bool_false -> f
Andrei Paskevich's avatar
Andrei Paskevich committed
538 539 540
  | Tapp (fs,[]) when ls_equal fs fs_bool_true -> t_attr_copy t t_true
  | Tapp (fs,[]) when ls_equal fs fs_bool_false -> t_attr_copy t t_false
  | _ -> t_attr_set ?loc:t.t_loc Sattr.empty (t_equ_simp t t_bool_true)
541

542
let rec pure_of_post prop v h = match h.t_node with
543 544 545 546 547 548 549 550 551
  | Tapp (ps, [{t_node = Tvar u}; t])
    when ls_equal ps ps_equ && vs_equal u v && t_v_occurs v t = 0 ->
      (if prop then fmla_of_term t else t), t_true
  | Tbinop (Tiff, {t_node =
      Tapp (ps, [{t_node = Tvar u}; {t_node = Tapp (fs,[])}])}, f)
    when ls_equal ps ps_equ && vs_equal v u &&
         ls_equal fs fs_bool_true && t_v_occurs v f = 0 ->
      (if prop then f else term_of_fmla f), t_true
  | Tbinop (Tand, f, g) ->
552
      let t, f = pure_of_post prop v f in
Andrei Paskevich's avatar
Andrei Paskevich committed
553
      t, t_attr_copy h (t_and_simp f g)
554 555
  | _ -> raise Exit

556 557
let pure_of_post prop v h = match v.vs_ty.ty_node, h.t_node with
  | Tyapp (ts,_), Tquant (Tforall,_) when ts_equal ts ts_func ->
Andrei Paskevich's avatar
Andrei Paskevich committed
558
      let t = t_attr_copy h (t_eps_close v h) in
559 560 561 562
      if not (t_is_lambda t) then raise Exit else
      (if prop then fmla_of_term t else t), t_true
  | _ -> pure_of_post prop v h

563 564 565 566
let term_of_post ~prop v h =
  try Some (pure_of_post prop v h) with Exit -> None

let rec raw_of_expr prop e = match e.e_node with
567 568
  | _ when ity_equal e.e_ity ity_unit -> t_void
    (* we do not check e.e_effect here, since we check the
569
       effects later for the overall expression. The only
570
       effect-hiding construction, Ematch(_,_,xl), is forbidden. *)
571 572
  | Eassign _ | Ewhile _ | Efor _ | Eassert _ -> assert false
  | Evar v -> t_var v.pv_vs
573
  | Econst c -> t_const c (ty_of_ity e.e_ity)
574
  | Epure t -> t
575
  | Eghost e | Eexn (_,e) -> pure_of_expr prop e
576
  | Eexec (_,{cty_post = []}) -> raise Exit
Andrei Paskevich's avatar
Andrei Paskevich committed
577
  | Eexec (_,{cty_post = q::_}) ->
578 579
      let v, h = open_post q in
      fst (pure_of_post prop v h)
580
  | Elet (LDvar (v,_d),e) when ity_equal v.pv_ity ity_unit ->
581
      t_subst_single v.pv_vs t_void (pure_of_expr prop e)
582
  | Elet (LDvar (v,d),e) ->
583
      t_let_close_simp v.pv_vs (pure_of_expr false d) (pure_of_expr prop e)
584 585 586 587 588
  | Elet (LDsym (s,_),e) ->
      (* TODO/FIXME: should we create a lambda-term for RLpv here instead
          of failing? Why would anyone want to define a local let-function,
          if it already has a pure logical meaning? *)
      if is_rlpv s then raise Exit;
589
      pure_of_expr prop e
590 591
  | Elet (LDrec rdl,e) ->
      if List.exists (fun rd -> is_rlpv rd.rec_sym) rdl then raise Exit;
592
      pure_of_expr prop e
593 594
  | Eif (e0,e1,e2) when is_e_false e1 && is_e_true e2 ->
      t_not (pure_of_expr true e0)
595
  | Eif (e0,e1,e2) when prop && is_e_false e2 ->
596
      t_and (pure_of_expr true e0) (pure_of_expr true e1)
597
  | Eif (e0,e1,e2) when prop && is_e_true e1 ->
598 599
      t_or (pure_of_expr true e0) (pure_of_expr true e2)
  | Eif (e0,e1,e2) ->
600
      t_if (pure_of_expr true e0) (pure_of_expr prop e1) (pure_of_expr prop e2)
601
  | Ematch (d,bl,xl) when Mxs.is_empty xl ->
602
      if bl = [] then pure_of_expr prop d else
603 604
      let conv (p,e) = t_close_branch p.pp_pat (pure_of_expr prop e) in
      t_case (pure_of_expr false d) (List.map conv bl)
605
  | Ematch _ | Eraise _ | Eabsurd -> raise Exit
606

Andrei Paskevich's avatar
Andrei Paskevich committed
607
and pure_of_expr prop e = match copy_attrs e (raw_of_expr prop e) with
608 609 610
  | {t_ty = Some _} as t when prop -> fmla_of_term t
  | {t_ty = None} as f when not prop -> term_of_fmla f
  | t -> t
611

612
let term_of_expr ~prop e =
613
  if not (eff_pure e.e_effect) then None else
614 615 616
  try Some (pure_of_expr prop e) with Exit -> None

let post_of_term res t =
Andrei Paskevich's avatar
Andrei Paskevich committed
617
  let loca f = t_attr_set ?loc:t.t_loc Sattr.empty f in
618 619 620 621 622 623 624
  let f_of_t t = loca (t_equ_simp t t_bool_true) in
  match res.t_ty, t.t_ty with
  | Some _, Some _ -> loca (t_equ_simp res t)
  | None,   None   -> loca (t_iff_simp res t)
  | Some _, None   -> loca (t_iff_simp (f_of_t res) t)
  | None,   Some _ -> loca (t_iff_simp res (f_of_t t))

625 626 627 628
let post_of_term res t = match t.t_node with
  | Teps bf when t_is_lambda t -> t_open_bound_with res bf
  | _ -> post_of_term res t

629 630 631
let rec post_of_expr res e = match e.e_node with
  | _ when ity_equal e.e_ity ity_unit -> t_true
  | Eassign _ | Ewhile _ | Efor _ | Eassert _ -> assert false
632
  | Evar v -> post_of_term res (t_var v.pv_vs)
633 634 635 636
  | Econst (Number.ConstInt _ as c)->
      post_of_term res (t_const c ty_int)
  | Econst (Number.ConstReal _ as c)->
      post_of_term res (t_const c ty_real)
637
  | Epure t -> post_of_term res t
638
  | Eghost e | Eexn (_,e) -> post_of_expr res e
639 640
  | Eexec (_,c) ->
      let conv q = open_post_with res q in
Andrei Paskevich's avatar
Andrei Paskevich committed
641
      copy_attrs e (t_and_l (List.map conv c.cty_post))
642
  | Elet (LDvar (v,_d),e) when ity_equal v.pv_ity ity_unit ->
Andrei Paskevich's avatar
Andrei Paskevich committed
643
      copy_attrs e (t_subst_single v.pv_vs t_void (post_of_expr res e))
644
  | Elet (LDvar (v,d),e) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
645
      copy_attrs e (t_let_close_simp v.pv_vs
646 647 648
        (pure_of_expr false d) (post_of_expr res e))
  | Elet (LDsym (s,_),e) ->
      if is_rlpv s then raise Exit;
Andrei Paskevich's avatar
Andrei Paskevich committed
649
      copy_attrs e (post_of_expr res e)
650 651
  | Elet (LDrec rdl,e) ->
      if List.exists (fun rd -> is_rlpv rd.rec_sym) rdl then raise Exit;
Andrei Paskevich's avatar
Andrei Paskevich committed
652
      copy_attrs e (post_of_expr res e)
653 654
  | Eif (_,e1,e2) when is_e_true e1 || is_e_false e2 ||
                      (is_e_false e1 && is_e_true e2) ->
655
      post_of_term res (pure_of_expr true e)
656 657
  | Eif (e0,e1,e2) ->
      t_if (pure_of_expr true e0) (post_of_expr res e1) (post_of_expr res e2)
658
  | Ematch (d,bl,xl) when Mxs.is_empty xl ->
659
      if bl = [] then post_of_expr res d else
660 661
      let conv (p,e) = t_close_branch p.pp_pat (post_of_expr res e) in
      t_case (pure_of_expr false d) (List.map conv bl)
662
  | Ematch _ | Eraise _ -> raise Exit
Andrei Paskevich's avatar
Andrei Paskevich committed
663
  | Eabsurd -> copy_attrs e t_false
664 665 666 667

let local_post_of_expr e =
  if ity_equal e.e_ity ity_unit || not (eff_pure e.e_effect) then [] else
  let res = create_vsymbol (id_fresh "result") (ty_of_ity e.e_ity) in
668 669 670 671 672 673
  try let t = pure_of_expr (ity_equal e.e_ity ity_bool) e in
      let t = match t.t_node with
        | Tapp (ps, [t; {t_node = Tapp (fs,[])}])
          when ls_equal ps ps_equ && ls_equal fs fs_bool_true -> t
        | _ -> t in
      [create_post res (post_of_term (t_var res) t)] with Exit ->
674 675
  try [create_post res (post_of_expr (t_var res) e)] with Exit -> []

676 677 678 679 680 681 682 683 684 685 686 687 688 689
(* we do not compute implicit post-conditions for let-functions,
    as this would be equivalent to auto-inlining of the generated
    logical function definition. FIXME: Should we make exception
    for local let-functions? We do have a mapping definition in
    the antecedents of WP, but provers must perform beta-reduction
    to apply it: auto-inlining might be really helpful here. *)
let c_cty_enrich ghost kind c =
  let cty = c_cty_ghostify ghost c in
  match c with
  | {c_node = Cfun e; c_cty = {cty_post = []}}
    when (kind = RKnone (*|| kind = RKlocal*)) ->
      cty_add_post cty (local_post_of_expr e)
  | _ -> cty

690 691 692 693 694 695 696 697 698 699 700 701 702
let post_of_expr res e =
  ty_equal_check (ty_of_ity e.e_ity)
    (match res.t_ty with Some ty -> ty | None -> ty_bool);
  if ity_equal e.e_ity ity_unit || not (eff_pure e.e_effect) then None
  else try
    (* we avoid capturing the free variables of res *)
    let clone v _ = create_vsymbol (id_clone v.vs_name) v.vs_ty in
    let sbs = Mvs.mapi clone (t_vars res) in
    let res = t_subst (Mvs.map t_var sbs) res in
    let q = post_of_expr res e in
    let inverse o n m = Mvs.add n (t_var o) m in
    Some (t_subst (Mvs.fold inverse sbs Mvs.empty) q)
  with Exit -> None
703

704 705 706
(* let-definitions *)

let let_var id ?(ghost=false) e =
707
  let ghost = ghost || mask_ghost e.e_mask in
708 709 710 711
  let v = create_pvsymbol id ~ghost e.e_ity in
  LDvar (v,e), v

let let_sym id ?(ghost=false) ?(kind=RKnone) c =
712
  let cty = c_cty_enrich ghost kind c in
713
  let s = create_rsymbol id ~kind cty in
714 715 716 717 718 719 720 721 722 723
  LDsym (s,c), s

let e_let ld e =
  let bind_pv v eff = eff_bind_single v eff in
  let bind_rs s eff = match s.rs_logic with
    | RLls _ -> invalid_arg "Expr.e_let"
    | RLpv v -> bind_pv v eff | _ -> eff in
  let bind_rd d eff = bind_rs d.rec_sym eff in
  let eff = match ld with
    | LDvar (v,d) ->
724
        try_effect [d;e] eff_union_seq d.e_effect (bind_pv v e.e_effect)
725
    | LDsym (s,c) ->
726
        try_effect [e] eff_read_pre (cty_reads c.c_cty) (bind_rs s e.e_effect)
727 728 729 730 731 732 733
    | LDrec dl ->
        let e_effect = List.fold_right bind_rd dl e.e_effect in
        (* We do not use the effect of rec_fun, because it does not
           necessarily depend on the external variables in rec_varl.
           We do not use the effect of rec_sym, because it contains
           the RLpv variable when we define a local let-function. *)
        let add s d = Spv.union s (cty_reads d.rec_rsym.rs_cty) in
734 735 736
        let rd = List.fold_left add Spv.empty dl in
        try_effect [e] eff_read_pre rd e_effect in
  mk_expr (Elet (ld,e)) e.e_ity e.e_mask eff
737 738 739

(* callable expressions *)

740
let e_exec c =
741
  let cty = cty_exec (c_cty_enrich false RKnone c) in
742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761
  (* abstract blocks and white-box blocks can escape into the outer
     VC context. Therefore we should assume the full effect of the
     underlying expression rather than the filtered effect of c,
     as produced by create_cty. However, we still want to remove
     the exceptions whose post-condition is False: this is handy,
     and we can handle it correctly in VC. We can safely ignore
     the function-to-mapping conversions, as they cannot appear
     as white-box blocks, and abstract blocks can only escape
     via exceptions, which functions-as-mappings do not raise. *)
  let eff = match c.c_cty.cty_args, c.c_node with
    | [], Cfun e ->
        let x_lost = Sxs.diff e.e_effect.eff_raises
                          cty.cty_effect.eff_raises in
        let eff = Sxs.fold (fun xs eff ->
          eff_catch eff xs) x_lost e.e_effect in
        let eff = if cty.cty_effect.eff_ghost then
          try_effect [e] eff_ghostify true eff else eff in
        eff_union_par cty.cty_effect eff
    | _ -> cty.cty_effect in
  mk_expr (Eexec (c, cty)) cty.cty_result cty.cty_mask eff
762 763 764

let c_any c = mk_cexp Cany c

765
let c_fun ?(mask=MaskVisible) args p q xq old e =
766
  let mask = mask_union mask e.e_mask in
767
  (* reset variables are forbidden in post-conditions *)
768
  let c = try create_cty ~mask args p q xq old e.e_effect e.e_ity with
769
    | BadGhostWrite (v,r) -> localize_ghost_write v r [e]
770
    | IllegalUpdate (v,r) -> localize_immut_write v r [e]
771
    | StaleVariable (v,r) -> localize_reset_stale v r [e] in
772
  mk_cexp (Cfun e) c
773

774 775 776 777
let is_rs_tuple s = match s.rs_logic with
  | RLls ls -> is_fs_tuple ls
  | _ -> false

778
let c_app s vl ityl ity =
779
  let cty = cty_apply s.rs_cty vl ityl ity in
780
  let cty = if ityl = [] && is_rs_tuple s then cty_tuple vl else cty in
781
  mk_cexp (Capp (s,vl)) cty
782

783
let c_pur s vl ityl ity =
784
  if not ity.ity_pure then Loc.errorm "This expression must have pure type";
785
  let v_args = List.map (create_pvsymbol ~ghost:false (id_fresh "u")) ityl in
786 787 788
  let t_args = List.map (fun v -> t_var v.pv_vs) (vl @ v_args) in
  let res = Opt.map (fun _ -> ty_of_ity ity) s.ls_value in
  let q = make_post (t_app s t_args res) in
789
  let eff = eff_ghostify true (eff_spoil eff_empty ity) in
790
  let cty = create_cty v_args [] [q] Mxs.empty Mpv.empty eff ity in
791 792
  mk_cexp (Cpur (s,vl)) cty

793
let mk_proxy ghost e hd = match e.e_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
794
  | Evar v when Sattr.is_empty e.e_attrs -> hd, v
Andrei Paskevich's avatar
Andrei Paskevich committed
795
  | _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
796
      let id = id_fresh ?loc:e.e_loc ~attrs:proxy_attrs "o" in
797
      let ld, v = let_var ~ghost id e in ld::hd, v
798

799 800
let add_proxy ghost e (hd,vl) =
  let hd, v = mk_proxy ghost e hd in hd, v::vl
Andrei Paskevich's avatar
Andrei Paskevich committed
801

802 803 804
let let_head hd e = List.fold_left (fun e ld -> e_let ld e) e hd

let e_app s el ityl ity =
805
  let trues l = List.map Util.ttrue l in
806
  let falses l = List.map Util.ffalse l in
807 808 809 810 811 812
  let rec down al el = match al, el with
    | {pv_ghost = gh}::al, {e_mask = m}::el ->
        if not gh && mask_ghost m then raise Exit;
        gh :: down al el
    | _, el -> trues el in
  let ghl = if rs_ghost s then trues el else
813
    if ityl = [] && is_rs_tuple s then falses el else
814 815
    try down s.rs_cty.cty_args el with Exit -> trues el in
  let hd, vl = List.fold_right2 add_proxy ghl el ([],[]) in
816 817
  let_head hd (e_exec (c_app s vl ityl ity))

818
let e_pur s el ityl ity =
819 820
  let ghl = List.map Util.ttrue el in
  let hd, vl = List.fold_right2 add_proxy ghl el ([],[]) in
821
  let_head hd (e_exec (c_pur s vl ityl ity))
822

823 824
(* assignment *)

825
let e_assign_raw al =
Andrei Paskevich's avatar
Andrei Paskevich committed
826
  let conv (r,f,v) = r, mfield_of_rs f, v in
827
  mk_expr (Eassign al) ity_unit MaskVisible (eff_assign (List.map conv al))
828 829

let e_assign al =
830
  let hr, hv, al = List.fold_right (fun (r,f,v) (hr,hv,al) ->
831 832 833
    let ghost = e_ghost r || rs_ghost f || e_ghost v in
    let hv, v = mk_proxy ghost v hv in
    let hr, r = mk_proxy ghost r hr in
834 835
    hr, hv, (r,f,v)::al) al ([],[],[]) in
  (* first pants, THEN your shoes *)
836 837 838 839 840 841 842
  let_head hv (let_head hr (e_assign_raw al))

(* built-in symbols *)

let e_true  = e_app rs_true  [] [] ity_bool
let e_false = e_app rs_false [] [] ity_bool

843 844
let rs_tuple = Hint.memo 17 (fun n ->
  ignore (its_tuple n); rs_of_ls (fs_tuple n))
845 846 847 848 849 850

let e_tuple el =
  let ity = ity_tuple (List.map (fun e -> e.e_ity) el) in
  e_app (rs_tuple (List.length el)) el [] ity

let rs_void = rs_tuple 0
851
let fs_void = fs_tuple 0
852 853 854 855

let e_void = e_app rs_void [] [] ity_unit

let is_e_void e = match e.e_node with
856
  | Eexec ({c_node = Capp (s,[])},_) -> rs_equal s rs_void
857 858 859 860
  | _ -> false

let rs_func_app = rs_of_ls fs_func_app

861 862 863
let ld_func_app =
  let v_args = rs_func_app.rs_cty.cty_args in
  let ity = rs_func_app.rs_cty.cty_result in
864
  let c = create_cty v_args [] [] Mxs.empty Mpv.empty eff_empty ity in
865 866
  LDsym (rs_func_app, c_any c)

867 868 869 870 871 872 873
let e_func_app fn e =
  let c = rs_func_app.rs_cty in
  let mtch isb a e = ity_match isb a.pv_ity e.e_ity in
  let isb = List.fold_left2 mtch c.cty_freeze c.cty_args [fn;e] in
  e_app rs_func_app [fn;e] [] (ity_full_inst isb c.cty_result)

let e_func_app_l fn el = List.fold_left e_func_app fn el
874

Andrei Paskevich's avatar
Andrei Paskevich committed
875 876
(* boolean constructors *)

877
let e_if e0 e1 e2 =
878 879
  ity_equal_check e0.e_ity ity_bool;
  ity_equal_check e1.e_ity e2.e_ity;
880 881 882 883 884 885
  let eff = try_effect [e1;e2] eff_union_par e1.e_effect e2.e_effect in
  let eff = try_effect [e0;e1;e2] eff_union_seq e0.e_effect eff in
  let ghost = mask_ghost e0.e_mask && e1.e_node <> Eabsurd &&
                                      e2.e_node <> Eabsurd in
  let eff = try_effect [e0;e1;e2] eff_ghostify ghost eff in
  mk_expr (Eif (e0,e1,e2)) e1.e_ity (mask_union e1.e_mask e2.e_mask) eff
886 887 888 889

let e_and e1 e2 = e_if e1 e2 e_false
let e_or e1 e2 = e_if e1 e_true e2
let e_not e = e_if e e_false e_true
890

Andrei Paskevich's avatar
Andrei Paskevich committed
891 892
(* loops *)

893 894 895 896
let e_for_raw v ((f,_,t) as bounds) i inv e =
  ity_equal_check f.pv_ity v.pv_ity;
  ity_equal_check t.pv_ity v.pv_ity;
  ity_equal_check i.pv_ity ity_int;
897
  ity_equal_check e.e_ity ity_unit;
898 899 900 901 902 903 904 905 906 907 908
  if not (pv_equal v i) then begin
    if not i.pv_ghost then Loc.errorm
      "The internal for-loop index mush be ghost";
    let check f = if t_v_occurs v.pv_vs f > 0 then Loc.errorm
      "The external for-loop index cannot occur in the invariant" in
    List.iter check inv;
    match v.pv_ity.ity_node with
    | Ityapp ({its_def = Range _},_,_) -> ()
    | _ when ity_equal v.pv_ity ity_int -> ()
    | _ -> Loc.errorm "For-loop bounds must have an integer type"
  end;
909
  let vars = List.fold_left t_freepvs Spv.empty inv in
910 911 912 913
  let ghost = v.pv_ghost || f.pv_ghost || t.pv_ghost in
  let eff = try_effect [e] eff_read_pre vars e.e_effect in
  let eff = try_effect [e] eff_ghostify ghost eff in
  ignore (try_effect [e] eff_union_seq eff eff);
914
  let eff = eff_bind_single v eff in
915
  let eff = eff_bind_single i eff in
916 917
  let eff = eff_read_single_pre t eff in
  let eff = eff_read_single_pre f eff in
918
  mk_expr (Efor (v,bounds,i,inv,e)) e.e_ity MaskVisible eff
919

920
let e_for v f dir t i inv e =
921 922
  let hd, t = mk_proxy false t [] in
  let hd, f = mk_proxy false f hd in
923
  let_head hd (e_for_raw v (f,dir,t) i inv e)
924 925 926 927

let e_while d inv vl e =
  ity_equal_check d.e_ity ity_bool;
  ity_equal_check e.e_ity ity_unit;
928 929 930 931 932 933
  let add_v s (t,_) = t_freepvs s t in
  let vars = List.fold_left add_v Spv.empty vl in
  let vars = List.fold_left t_freepvs vars inv in
  let eff = try_effect [e] eff_read_pre vars e.e_effect in
  let eff = try_effect [d;e] eff_union_seq d.e_effect eff in
  let eff = try_effect [d;e] eff_ghostify (mask_ghost d.e_mask) eff in
934
  let eff = if vl = [] then eff_diverge eff else eff in
935 936
  ignore (try_effect [d;e] eff_union_seq eff eff);
  mk_expr (Ewhile (d,inv,vl,e)) e.e_ity MaskVisible eff
937

Andrei Paskevich's avatar
Andrei Paskevich committed
938 939
(* match-with, try-with, raise *)

940
let e_match e bl xl =
941
  (* return type *)
942 943
  let ity = match bl with
    | (_,d)::_ -> d.e_ity
944 945 946 947 948
    | [] -> e.e_ity in
  (* check types and masks *)
  let check rity rmask pity pmask d =
    ity_equal_check rity pity;
    if not (ity_equal rity ity_unit) && mask_spill rmask pmask then
949
      Loc.errorm "Non-ghost pattern in a ghost position";
950 951 952 953 954 955 956 957 958 959
    ity_equal_check d.e_ity ity in
  List.iter (fun (p,d) ->
    check e.e_ity e.e_mask p.pp_ity p.pp_mask d) bl;
  Mxs.iter (fun xs (vl,d) ->
    let vl_ity, vl_mask = match vl with
      | [] -> ity_unit,