expr.ml 32 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

open Stdlib
open Ident
14
open Ty
15 16 17
open Term
open Ity

Andrei Paskevich's avatar
Andrei Paskevich committed
18 19
(** {2 Program symbols} *)

20 21 22 23 24 25 26 27 28
type psymbol = {
  ps_name  : ident;
  ps_cty   : cty;
  ps_ghost : bool;
  ps_logic : ps_logic;
}

and ps_logic =
  | PLnone            (* non-pure symbol *)
29
  | PLpv of pvsymbol  (* local let-function *)
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
  | PLls of lsymbol   (* top-level let-function or let-predicate *)
  | PLlemma           (* top-level or local let-lemma *)

module Psym = MakeMSHW (struct
  type t = psymbol
  let tag ps = ps.ps_name.id_tag
end)

module Sps = Psym.S
module Mps = Psym.M
module Hps = Psym.H
module Wps = Psym.W

let ps_equal : psymbol -> psymbol -> bool = (==)
let ps_hash ps = id_hash ps.ps_name
let ps_compare ps1 ps2 = id_compare ps1.ps_name ps2.ps_name

47 48 49 50 51 52 53 54 55
let mk_ps, restore_ps =
  let ls_to_ps = Wls.create 17 in
  (fun id cty gh lg ->
    let ps = {
      ps_name  = id;
      ps_cty   = cty;
      ps_ghost = gh;
      ps_logic = lg;
    } in
Andrei Paskevich's avatar
Andrei Paskevich committed
56 57 58
    match lg with
    | PLls ls -> Wls.set ls_to_ps ls ps; ps
    | _ -> ps),
59
  (fun ls -> Wls.find ls_to_ps ls)
60 61 62

type ps_kind =
  | PKnone            (* non-pure symbol *)
63 64 65 66 67
  | PKpv of pvsymbol  (* local let-function *)
  | PKlocal           (* new local let-function *)
  | PKls of lsymbol   (* top-level let-function or let-predicate *)
  | PKfunc of int     (* new top-level let-function or constructor *)
  | PKpred            (* new top-level let-predicate *)
68 69 70 71
  | PKlemma           (* top-level or local let-lemma *)

let create_psymbol id ?(ghost=false) ?(kind=PKnone) c =
  let check_effects { cty_effect = e } =
Andrei Paskevich's avatar
Andrei Paskevich committed
72 73 74 75
    (* TODO/FIXME: prove that we can indeed ignore resets.
      Normally, resets neither consult nor change the
      external state, and do not affect the specification. *)
    if not (eff_is_pure e) then Loc.errorm
76
      "this function has side effects, it cannot be declared as pure" in
77
  let check_reads { cty_freeze = isb } =
Andrei Paskevich's avatar
Andrei Paskevich committed
78 79
    if not (Mreg.is_empty isb.isb_reg) then Loc.errorm
      "this function is stateful, it cannot be declared as pure" in
80 81 82 83 84 85 86 87
  let res_type c = ty_of_ity c.cty_result in
  let arg_type c = List.map (fun a -> a.pv_vs.vs_ty) c.cty_args in
  let arg_list c = List.map (fun a -> t_var a.pv_vs) c.cty_args in
  let add_post c t = match t.t_ty with
    | Some ty ->
        let res = create_vsymbol (id_fresh "result") ty in
        cty_add_post c [create_post res (t_equ (t_var res) t)]
    | None ->
88
        let res = create_vsymbol (id_fresh "result") ty_bool in
89 90
        let q = t_iff (t_equ (t_var res) t_bool_true) t in
        cty_add_post c [create_post res q] in
91 92 93 94 95 96
  match kind with
  | PKnone ->
      mk_ps (id_register id) c ghost PLnone
  | PKlocal ->
      check_effects c; check_reads c;
      let ity = ity_purify c.cty_result in
Andrei Paskevich's avatar
Andrei Paskevich committed
97 98
      let ity = List.fold_right (fun a ity ->
        ity_func (ity_purify a.pv_ity) ity) c.cty_args ity in
99 100 101 102 103 104 105 106 107
      (* 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
         not regions) of the psymbol, and the easiest way to do that
         is to make these type variables appear in c.cty_reads.
         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
108 109
         it into the ps_logic field. This pvsymbol should not be
         used in the program, as it has lost all preconditions,
110 111
         which is why we declare it as ghost. In other words,
         this pvsymbol behaves exactly as Epure of its pv_vs. *)
112 113 114
      let v = create_pvsymbol ~ghost:true id ity in
      let t = t_func_app_l (t_var v.pv_vs) (arg_list c) in
      mk_ps v.pv_vs.vs_name (add_post c t) ghost (PLpv v)
115 116 117 118 119 120 121 122 123
  | PKpv v ->
      check_effects c; check_reads c;
      let ity = ity_purify c.cty_result in
      let ity = List.fold_right (fun a ity ->
        ity_func (ity_purify a.pv_ity) ity) c.cty_args ity in
      ity_equal_check v.pv_ity ity;
      if not v.pv_ghost then invalid_arg "Expr.create_psymbol";
      let t = t_func_app_l (t_var v.pv_vs) (arg_list c) in
      mk_ps (id_register id) (add_post c t) ghost (PLpv v)
124 125
  | PKfunc constr ->
      check_effects c; check_reads c;
Andrei Paskevich's avatar
Andrei Paskevich committed
126 127 128
      (* we don't really need to check the well-formedness of
         constructor's signature here, the type declaration
         will take care of it *)
129 130 131
      let ls = create_fsymbol id ~constr (arg_type c) (res_type c) in
      let t = t_app ls (arg_list c) ls.ls_value in
      mk_ps ls.ls_name (add_post c t) ghost (PLls ls)
132 133 134 135 136
  | PKpred ->
      check_effects c; check_reads c;
      if not (ity_equal c.cty_result ity_bool) then
        Loc.errorm "this function does not return a boolean value, \
                    it cannot be declared as a pure predicate";
137 138 139
      let ls = create_psymbol id (arg_type c) in
      let f = t_app ls (arg_list c) None in
      mk_ps ls.ls_name (add_post c f) ghost (PLls ls)
140 141 142
  | PKls ls when ls.ls_constr = 0 ->
      check_effects c; check_reads c;
      let args = arg_type c and res = res_type c in
143
      List.iter2 ty_equal_check ls.ls_args args;
144
      begin match ls.ls_value with
145 146
        | None -> ty_equal_check ty_bool res
        | Some ty -> ty_equal_check ty res end;
147 148 149
      let t = t_app ls (arg_list c) ls.ls_value in
      mk_ps (id_register id) (add_post c t) ghost (PLls ls)
  | PKls _ -> invalid_arg "Expr.create_psymbol"
150 151 152
  | PKlemma ->
      check_effects c;
      mk_ps (id_register id) c ghost PLlemma
Andrei Paskevich's avatar
Andrei Paskevich committed
153

154 155
let ps_kind ps = match ps.ps_logic with
  | PLnone -> PKnone
156 157
  | PLpv v -> PKpv v
  | PLls s -> PKls s
158 159
  | PLlemma -> PKlemma

Andrei Paskevich's avatar
Andrei Paskevich committed
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
(** {2 Program patterns} *)

type prog_pattern = {
  pp_pat   : pattern;
  pp_ity   : ity;
  pp_ghost : bool;
}

type pre_pattern =
  | PPwild
  | PPvar of preid
  | PPapp of psymbol * pre_pattern list
  | PPor  of pre_pattern * pre_pattern
  | PPas  of pre_pattern * preid

Andrei Paskevich's avatar
Andrei Paskevich committed
175 176
exception ConstructorExpected of psymbol

Andrei Paskevich's avatar
Andrei Paskevich committed
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
let create_prog_pattern pp ?(ghost=false) ity =
  let hv = Hstr.create 3 in
  let gh = ref false in
  let find id ghost ity =
    try
      let pv = Hstr.find hv id.pre_name in
      ity_equal_check ity pv.pv_ity;
      if (pv.pv_ghost <> ghost) then invalid_arg "Expr.make_pattern";
      pv
    with Not_found ->
      let pv = create_pvsymbol id ~ghost ity in
      Hstr.add hv id.pre_name pv; pv
  in
  let rec make ghost ity = function
    | PPwild ->
        pat_wild (ty_of_ity ity)
    | PPvar id ->
        pat_var (find id ghost ity).pv_vs
    | PPapp ({ps_logic = PLls ls} as ps, ppl) when ls.ls_constr > 0 ->
        if ghost && ls.ls_constr > 1 then gh := true;
        let sbs = ity_match isb_empty ps.ps_cty.cty_result ity in
        let mtch arg pp =
          let ghost = ghost || arg.pv_ghost in
          make ghost (ity_full_inst sbs arg.pv_ity) pp in
        let ppl = try List.map2 mtch ps.ps_cty.cty_args ppl with
          | Invalid_argument _ ->
              raise (Term.BadArity (ls, List.length ppl)) in
        pat_app ls ppl (ty_of_ity ity)
Andrei Paskevich's avatar
Andrei Paskevich committed
205 206
    | PPapp (ps, _) ->
        raise (ConstructorExpected ps)
Andrei Paskevich's avatar
Andrei Paskevich committed
207 208 209 210 211 212 213 214 215
    | PPor (pp1,pp2) ->
        pat_or (make ghost ity pp1) (make ghost ity pp2)
    | PPas (pp,id) ->
        pat_as (make ghost ity pp) (find id ghost ity).pv_vs
  in
  let pat = make ghost ity pp in
  Hstr.fold Mstr.add hv Mstr.empty,
  { pp_pat = pat; pp_ity = ity; pp_ghost = ghost || !gh }

Andrei Paskevich's avatar
Andrei Paskevich committed
216 217
(** {2 Program expressions} *)

218 219
type lazy_op = Eand | Eor

Andrei Paskevich's avatar
Andrei Paskevich committed
220 221 222 223 224 225 226 227 228 229
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) *)

230 231
type assign = pvsymbol * pvsymbol * pvsymbol (* region * field * value *)

Andrei Paskevich's avatar
Andrei Paskevich committed
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251
type vty =
  | VtyI of ity
  | VtyC of cty

type val_decl =
  | ValV of pvsymbol
  | ValS of psymbol

type expr = {
  e_node   : expr_node;
  e_vty    : vty;
  e_ghost  : bool;
  e_effect : effect;
  e_label  : Slab.t;
  e_loc    : Loc.position option;
}

and expr_node =
  | Evar    of pvsymbol
  | Esym    of psymbol
252
  | Econst  of Number.constant
Andrei Paskevich's avatar
Andrei Paskevich committed
253 254 255 256
  | Eapp    of expr * pvsymbol list * cty
  | Efun    of expr
  | Elet    of let_defn * expr
  | Erec    of rec_defn * expr
257 258
  | Enot    of expr
  | Elazy   of lazy_op * expr * expr
Andrei Paskevich's avatar
Andrei Paskevich committed
259 260
  | Eif     of expr * expr * expr
  | Ecase   of expr * (prog_pattern * expr) list
261
  | Eassign of assign list
Andrei Paskevich's avatar
Andrei Paskevich committed
262 263 264 265 266 267
  | Ewhile  of expr * invariant * variant list * expr
  | Efor    of pvsymbol * for_bounds * invariant * expr
  | Etry    of expr * (xsymbol * pvsymbol * expr) list
  | Eraise  of xsymbol * expr
  | Eghost  of expr
  | Eassert of assertion_kind * term
Andrei Paskevich's avatar
Andrei Paskevich committed
268
  | Epure   of term
Andrei Paskevich's avatar
Andrei Paskevich committed
269
  | Eabsurd
270 271
  | Etrue
  | Efalse
Andrei Paskevich's avatar
Andrei Paskevich committed
272 273 274 275 276 277 278 279 280
  | Eany

and let_defn = {
  let_sym  : val_decl;
  let_expr : expr;
}

and rec_defn = {
  rec_defn : fun_defn list;
281
  rec_decr : lsymbol option;
Andrei Paskevich's avatar
Andrei Paskevich committed
282 283 284
}

and fun_defn = {
285 286 287
  fun_sym  : psymbol; (* exported symbol *)
  fun_rsym : psymbol; (* internal symbol *)
  fun_expr : expr;    (* Efun *)
Andrei Paskevich's avatar
Andrei Paskevich committed
288 289
  fun_varl : variant list;
}
290

Andrei Paskevich's avatar
Andrei Paskevich committed
291
(* basic tools *)
292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312

let e_label ?loc l e = { e with e_label = l; e_loc = loc }

let e_label_add l e = { e with e_label = Slab.add l e.e_label }

let e_label_copy { e_label = lab; e_loc = loc } e =
  let lab = Slab.union lab e.e_label in
  let loc = if e.e_loc = None then loc else e.e_loc in
  { e with e_label = lab; e_loc = loc }

exception ItyExpected of expr
exception CtyExpected of expr

let ity_of_expr e = match e.e_vty with
  | VtyI ity -> ity
  | VtyC _ -> Loc.error ?loc:e.e_loc (ItyExpected e)

let cty_of_expr e = match e.e_vty with
  | VtyI _ -> Loc.error ?loc:e.e_loc (CtyExpected e)
  | VtyC cty -> cty

Andrei Paskevich's avatar
Andrei Paskevich committed
313 314 315
let e_ghost_raises e =
  e.e_ghost && not (Mexn.is_empty e.e_effect.eff_raises)

Andrei Paskevich's avatar
Andrei Paskevich committed
316
let e_fold fn acc e = match e.e_node with
317
  | Evar _ | Esym _ | Econst _ | Eany | Etrue | Efalse
Andrei Paskevich's avatar
Andrei Paskevich committed
318 319 320 321 322 323 324 325 326 327 328 329 330 331
  | Eassign _ | Eassert _ | Epure _ | Eabsurd -> acc
  | Efun e | Eapp (e,_,_) | Enot e | Eraise (_,e)
  | Efor (_,_,_,e) | Eghost e -> fn acc e
  | Elet (ld,e) -> fn (fn acc ld.let_expr) e
  | Eif (c,d,e) -> fn (fn (fn acc c) d) e
  | Elazy (_,d,e) | Ewhile (d,_,_,e) -> fn (fn acc d) e
  | Erec (r,e) ->
      fn (List.fold_left (fun acc d -> fn acc d.fun_expr) acc r.rec_defn) e
  | Ecase (d,bl) -> List.fold_left (fun acc (_,e) -> fn acc e) (fn acc d) bl
  | Etry (d,xl) -> List.fold_left (fun acc (_,_,e) -> fn acc e) (fn acc d) xl

exception FoundExpr of expr

(* find a minimal sub-expression satisfying [pr] *)
Andrei Paskevich's avatar
Andrei Paskevich committed
332
let e_find_minimal pr e =
Andrei Paskevich's avatar
Andrei Paskevich committed
333 334 335 336 337 338 339 340 341 342 343 344 345 346
  let rec find () e = e_fold find () e;
    if pr e then raise (FoundExpr e) in
  try find () e; raise Not_found with FoundExpr e -> e

(* find a sub-expression whose proper effect satisfies [pr] *)
let find_effect pr e =
  let rec find () e = match e.e_node with
    | Eapp (_,_,{cty_args = []; cty_effect = eff})
      when pr eff -> raise (FoundExpr e)
    | Eassign _ when pr e.e_effect -> raise (FoundExpr e)
    | Efun _ -> () (* or call eff_is_empty at each node *)
    | _ -> e_fold find () e in
  try find () e; raise Not_found with FoundExpr e -> e

347 348 349 350 351
(* smart constructors *)

let mk_expr node vty ghost eff = {
  e_node   = node;
  e_vty    = vty;
352 353 354
  e_ghost  = if ghost && eff.eff_diverg then
    Loc.errorm "This ghost expression contains potentially \
      non-terminating loops or function calls" else ghost;
355 356 357 358 359 360 361 362 363 364
  e_effect = eff;
  e_label  = Slab.empty;
  e_loc    = None;
}

let e_var pv = mk_expr (Evar pv) (VtyI pv.pv_ity) pv.pv_ghost eff_empty
let e_sym ps = mk_expr (Esym ps) (VtyC ps.ps_cty) ps.ps_ghost eff_empty

let e_const c =
  let ity = match c with
Andrei Paskevich's avatar
Andrei Paskevich committed
365
    | Number.ConstInt  _ -> ity_int
366 367 368 369 370 371
    | Number.ConstReal _ -> ity_real in
  mk_expr (Econst c) (VtyI ity) false eff_empty

let e_nat_const n =
  e_const (Number.ConstInt (Number.int_const_dec (string_of_int n)))

Andrei Paskevich's avatar
Andrei Paskevich committed
372 373
(* let definitions *)

374 375
let create_let_defn id ?(ghost=false) e =
  let ghost = ghost || e.e_ghost in
376
  let lv = match e.e_vty with
Andrei Paskevich's avatar
Andrei Paskevich committed
377 378
    | VtyC c -> ValS (create_psymbol id ~ghost ~kind:PKnone c)
    | VtyI i -> ValV (create_pvsymbol id ~ghost i) in
379 380
  { let_sym = lv; let_expr = e }

381 382
let create_let_defn_pv id ?(ghost=false) e =
  let ghost = ghost || e.e_ghost in
383
  let pv = create_pvsymbol id ~ghost (ity_of_expr e) in
Andrei Paskevich's avatar
Andrei Paskevich committed
384 385
  { let_sym = ValV pv; let_expr = e }, pv

386 387
let create_let_defn_ps id ?(ghost=false) ?(kind=PKnone) e =
  let ghost = ghost || e.e_ghost in
Andrei Paskevich's avatar
Andrei Paskevich committed
388 389
  let cty = match e.e_vty, kind with
    | _, PKfunc n when n > 0 -> invalid_arg "Expr.create_let_defn_ps"
390
    | VtyI i, (PKfunc _|PKpred|PKls _) when ity_immutable i ->
Andrei Paskevich's avatar
Andrei Paskevich committed
391 392
        (* the post will be equality to the logic constant *)
        create_cty [] [] [] Mexn.empty Spv.empty eff_empty i
393
    | VtyI _, (PKfunc _|PKpred|PKls _) -> Loc.errorm ?loc:e.e_loc
Andrei Paskevich's avatar
Andrei Paskevich committed
394
        "this expression is non-pure, it cannot be used as a pure function"
395
    | VtyI _, (PKnone|PKlocal|PKpv _|PKlemma) -> Loc.errorm ?loc:e.e_loc
396
        "this expression is first-order, it cannot be used as a function"
Andrei Paskevich's avatar
Andrei Paskevich committed
397
    | VtyC c, _ -> c in
398
  let ps = create_psymbol id ~ghost ~kind cty in
Andrei Paskevich's avatar
Andrei Paskevich committed
399
  { let_sym = ValS ps; let_expr = e }, ps
400

401 402 403 404 405 406 407 408
let e_let_raw ({let_expr = d} as ld) e =
  let eff = eff_union d.e_effect e.e_effect in
  let ghost = e.e_ghost || e_ghost_raises d in
  mk_expr (Elet (ld,e)) e.e_vty ghost eff

let e_rec_raw rd e =
  mk_expr (Erec (rd,e)) e.e_vty e.e_ghost e.e_effect

Andrei Paskevich's avatar
Andrei Paskevich committed
409 410 411 412
let proxy_label = create_label "proxy_pvsymbol"
let proxy_labels = Slab.singleton proxy_label

let mk_proxy ~ghost e hd = match e.e_node with
413
  | Evar v when Slab.is_empty e.e_label -> hd, v
Andrei Paskevich's avatar
Andrei Paskevich committed
414 415 416 417 418 419
  | _ ->
      let id = id_fresh ?loc:e.e_loc ~label:proxy_labels "o" in
      let ld, v = create_let_defn_pv id ~ghost e in
      ld::hd, v

let e_ghost e = mk_expr (Eghost e) e.e_vty true e.e_effect
420

Andrei Paskevich's avatar
Andrei Paskevich committed
421
let e_ghostify e = if not e.e_ghost then e_ghost e else e
422 423 424 425 426 427 428 429 430 431 432 433

(* Elet, Erec, and Eghost are guaranteed to never change
   the type of the underlying expression. Thus, [fn] can
   expect its argument to have the same [e_vty]. However,
   the argument of [fn] may be non-ghost, even though
   the initial argument of [rewind] was ghost.

   TODO/FIXME: this API implements the fully-named scheme
   of binder representation. Therefore, it is *forbidden* to
   use the same binder ident more than once in an expression,
   otherwise exchanging binders in [rewind] may be incorrect.
   One must never reuse the results of [create_let_defn] and
434
   [create_rec_defn] when constructing expressions. *)
435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
let rec rewind fn ghost d = match d.e_node with
  | (Elet ({let_sym = ValS {ps_ghost = false}}, _)
  |  Elet ({let_sym = ValV {pv_ghost = false}}, _))
    when ghost -> Loc.errorm ?loc:d.e_loc
      "This let-definition must be explicitly marked ghost"
  | Elet (ld, e) ->
      e_label_copy d (e_let_raw ld (rewind fn ghost e))
  | Erec ({rec_defn = dl} as rd, e) ->
      let ngh fd = not fd.fun_sym.ps_ghost in
      if ghost && List.exists ngh dl then Loc.errorm ?loc:d.e_loc
        "%s must be explicitly marked ghost" (if List.length dl > 1 then
        "These recursive definitions" else "This recursive definition");
      e_label_copy d (e_rec_raw rd (rewind fn ghost e))
  | Eghost e ->
      rewind (fun e -> fn (e_label_copy d (e_ghost e))) true e
  | _ -> fn d

Andrei Paskevich's avatar
Andrei Paskevich committed
452
let e_let ({let_sym = lv; let_expr = d} as ld) e = match lv with
453 454 455 456 457 458 459 460 461 462
  | ValS {ps_logic = PLls _} -> invalid_arg "Expr.e_let"
  | ValS {ps_ghost = gh} ->
      rewind (fun d -> e_let_raw {ld with let_expr = d} e) gh d
  | ValV _ -> e_let_raw ld e

let e_rec ({rec_defn = dl} as rd) e =
  List.iter (fun fd -> match fd.fun_sym.ps_logic with
    | PLls _ -> invalid_arg "Expr.e_rec" | _ -> ()) dl;
  e_rec_raw rd e

Andrei Paskevich's avatar
Andrei Paskevich committed
463 464 465
(* application and assignment *)

let e_app_raw e vl ityl ity =
466 467
  let ghost = e.e_ghost and c = cty_of_expr e in
  let ghost, c = cty_apply ~ghost c vl ityl ity in
468 469 470 471 472
  let vty, eff = if c.cty_args = [] then
    VtyI c.cty_result, c.cty_effect else
    VtyC c, eff_empty in
  let mk_app e =
    let eff = eff_union e.e_effect eff in
473 474
    mk_expr (Eapp (e,vl,c)) vty ghost eff in
  rewind mk_app ghost e
475

Andrei Paskevich's avatar
Andrei Paskevich committed
476
let e_app e el ityl ity =
477
  let rec down al el = match al, el with
478
    | {pv_ghost = ghost}::al, e::el ->
479 480 481 482
        let hd, vl = down al el in
        let hd, v = mk_proxy ~ghost e hd in
        hd, v::vl
    | _, [] -> [], []
Andrei Paskevich's avatar
Andrei Paskevich committed
483
    | _ -> invalid_arg "Expr.e_app" (* BadArity? *) in
484
  let hd, vl = down (cty_of_expr e).cty_args el in
Andrei Paskevich's avatar
Andrei Paskevich committed
485
  List.fold_right e_let_raw hd (e_app_raw e vl ityl ity)
Andrei Paskevich's avatar
Andrei Paskevich committed
486

487
let e_assign_raw al =
Andrei Paskevich's avatar
Andrei Paskevich committed
488
  let ghost = List.for_all (fun (r,f,v) ->
489 490 491 492 493
    r.pv_ghost || f.pv_ghost || v.pv_ghost) al in
  let conv (r,f,v) = match r.pv_ity.ity_node with
    | Ityreg r -> r,f,v.pv_ity
    | _ -> invalid_arg "Expr.e_assign" in
  let eff = eff_assign eff_empty (List.map conv al) in
Andrei Paskevich's avatar
Andrei Paskevich committed
494
  mk_expr (Eassign al) (VtyI ity_unit) ghost eff
495 496

let e_assign al =
497 498 499 500 501 502 503 504
  let hr, hv, al = List.fold_right (fun (r,f,v) (hr,hv,al) ->
    let ghost = r.e_ghost || f.pv_ghost || v.e_ghost in
    let hv, v = mk_proxy ~ghost v hv in
    let hr, r = mk_proxy ~ghost r hr in
    hr, hv, (r,f,v)::al) al ([],[],[]) in
  (* first pants, THEN your shoes *)
  List.fold_right e_let_raw hr
    (List.fold_right e_let_raw hv (e_assign_raw al))
505

Andrei Paskevich's avatar
Andrei Paskevich committed
506 507
(* boolean constructors *)

508 509 510 511 512 513 514 515
let e_if e0 e1 e2 =
  ity_equal_check (ity_of_expr e0) ity_bool;
  ity_equal_check (ity_of_expr e1) (ity_of_expr e2);
  let gh = e0.e_ghost || e1.e_ghost || e2.e_ghost in
  let eff = eff_union e1.e_effect e2.e_effect in
  let eff = eff_union e0.e_effect eff in
  mk_expr (Eif (e0,e1,e2)) e1.e_vty gh eff

516 517 518 519 520 521 522 523 524 525
let e_lazy op e1 e2 =
  ity_equal_check (ity_of_expr e1) ity_bool;
  ity_equal_check (ity_of_expr e2) ity_bool;
  let ghost = e1.e_ghost || e2.e_ghost in
  let eff = eff_union e1.e_effect e2.e_effect in
  mk_expr (Elazy (op,e1,e2)) e1.e_vty ghost eff

let e_not e =
  ity_equal_check (ity_of_expr e) ity_bool;
  mk_expr (Enot e) e.e_vty e.e_ghost e.e_effect
526

527
let e_true  = mk_expr Etrue  (VtyI ity_bool) false eff_empty
528 529
let e_false = mk_expr Efalse (VtyI ity_bool) false eff_empty

Andrei Paskevich's avatar
Andrei Paskevich committed
530 531
(* loops *)

532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553
let e_for_raw v ((f,_,t) as bounds) inv e =
  ity_equal_check v.pv_ity ity_int;
  ity_equal_check f.pv_ity ity_int;
  ity_equal_check t.pv_ity ity_int;
  ity_equal_check (ity_of_expr e) ity_unit;
  let ghost = v.pv_ghost || f.pv_ghost || t.pv_ghost || e.e_ghost in
  mk_expr (Efor (v,bounds,inv,e)) e.e_vty ghost e.e_effect

let e_for v ef dir et inv e =
  let ghost = v.pv_ghost || ef.e_ghost || et.e_ghost || e.e_ghost in
  let hd, vt = mk_proxy ~ghost et [] in
  let hd, vf = mk_proxy ~ghost ef hd in
  List.fold_right e_let_raw hd (e_for_raw v (vf,dir,vt) inv e)

let e_while cnd inv vl e =
  ity_equal_check (ity_of_expr cnd) ity_bool;
  ity_equal_check (ity_of_expr e) ity_unit;
  let ghost = cnd.e_ghost || e.e_ghost in
  let eff = eff_union cnd.e_effect e.e_effect in
  let eff = if vl = [] then eff_diverge eff else eff in
  mk_expr (Ewhile (cnd,inv,vl,e)) e.e_vty ghost eff

Andrei Paskevich's avatar
Andrei Paskevich committed
554 555
(* match-with, try-with, raise *)

556
let e_case ({e_effect = eff} as e) bl =
557 558 559 560 561 562 563 564 565
  let mb, ity = match bl with
    | [(_,d)] -> false, ity_of_expr d
    | (_,d)::_ -> true, ity_of_expr d
    | [] -> invalid_arg "Expr.e_case" in
  List.iter (fun (pp,d) ->
    if e.e_ghost && not pp.pp_ghost then
      Loc.errorm "Non-ghost pattern in a ghost position";
    ity_equal_check (ity_of_expr d) ity;
    ity_equal_check (ity_of_expr e) pp.pp_ity) bl;
Andrei Paskevich's avatar
Andrei Paskevich committed
566
  let ghost = e_ghost_raises e || List.exists (fun (_,d) -> d.e_ghost) bl in
567 568 569 570
  let ghost = ghost || (mb && List.exists (fun (pp,_) -> pp.pp_ghost) bl) in
  let eff = List.fold_left (fun f (_,d) -> eff_union f d.e_effect) eff bl in
  mk_expr (Ecase (e,bl)) (VtyI ity) ghost eff

571
let e_try e xl =
572 573 574 575 576 577 578 579 580 581 582 583 584
  List.iter (fun (xs,v,d) ->
    ity_equal_check v.pv_ity xs.xs_ity;
    ity_equal_check (ity_of_expr d) (ity_of_expr e)) xl;
  let ghost = e.e_ghost || List.exists (fun (_,_,d) -> d.e_ghost) xl in
  let eff = List.fold_left (fun f (xs,_,_) -> eff_catch f xs) e.e_effect xl in
  let eff = List.fold_left (fun f (_,_,d) -> eff_union f d.e_effect) eff xl in
  mk_expr (Etry (e,xl)) e.e_vty ghost eff

let e_raise xs e ity =
  ity_equal_check (ity_of_expr e) xs.xs_ity;
  let eff = eff_raise e.e_effect xs in
  mk_expr (Eraise (xs,e)) (VtyI ity) e.e_ghost eff

Andrei Paskevich's avatar
Andrei Paskevich committed
585 586
(* snapshots, assertions, "any" *)

587 588 589 590 591 592 593 594 595 596 597
let e_pure t =
  let ity = Opt.fold (fun _ -> ity_of_ty) ity_bool t.t_ty in
  mk_expr (Epure t) (VtyI ity) true eff_empty

let e_assert ak f =
  mk_expr (Eassert (ak, t_prop f)) (VtyI ity_unit) false eff_empty

let e_absurd ity = mk_expr Eabsurd (VtyI ity) false eff_empty

let e_any c = mk_expr Eany (VtyC c) false eff_empty

598 599 600 601 602 603 604
(* lambda construction *)

let rec e_vars e = match e.e_node with
  | Evar v -> Spv.singleton v
  | Esym s -> s.ps_cty.cty_reads
  | Efun _ | Eany -> (cty_of_expr e).cty_reads
  | Eapp (e,vl,_) -> List.fold_right Spv.add vl (e_vars e)
605 606
  | Elet ({let_sym = ValV v; let_expr = d},e)
  | Elet ({let_sym = ValS {ps_logic = PLpv v}; let_expr = d},e) ->
607 608 609 610 611 612
      Spv.union (e_vars d) (Spv.remove v (e_vars e))
  | Elet ({let_sym = ValS _; let_expr = d},e) | Elazy (_,d,e) ->
      Spv.union (e_vars d) (e_vars e)
  | Erec ({rec_defn = dl},e) ->
      let s = List.fold_left (fun s {fun_sym = ps} ->
        Spv.union s ps.ps_cty.cty_reads) (e_vars e) dl in
613 614
      List.fold_left (fun s {fun_sym = {ps_logic = l}} ->
        match l with PLpv v -> Spv.remove v s | _ -> s) s dl
615 616 617 618 619 620 621 622 623 624 625 626 627
  | Enot e | Eraise (_,e) | Eghost e -> e_vars e
  | Eassign al ->
      List.fold_left (fun s (r,_,v) -> Spv.add r (Spv.add v s)) Spv.empty al
  | Eif (c,d,e) -> Spv.union (e_vars c) (Spv.union (e_vars d) (e_vars e))
  | Etry (d,xl) -> List.fold_left (fun s (_,v,e) ->
      Spv.union s (Spv.remove v (e_vars e))) (e_vars d) xl
  | Ecase (d,bl) -> List.fold_left (fun s ({pp_pat = p},e) -> Spv.union s
      (Spv.diff (e_vars e) (pvs_of_vss Spv.empty p.pat_vars))) (e_vars d) bl
  | Ewhile (d,inv,vl,e) -> let s = Spv.union (e_vars d) (e_vars e) in
      List.fold_left (fun s (t,_) -> t_freepvs s t) (t_freepvs s inv) vl
  | Efor (v,(f,_,t),inv,e) ->
      Spv.add f (Spv.add t (Spv.remove v (t_freepvs (e_vars e) inv)))
  | Eassert (_,t) | Epure t -> t_freepvs Spv.empty t
628
  | Econst _ | Eabsurd | Etrue | Efalse -> Spv.empty
629 630 631 632 633 634

let pv_mut v mut = if ity_immutable v.pv_ity then mut else Spv.add v mut
let pv_vis v vis = if v.pv_ghost then vis else ity_r_visible vis v.pv_ity

let rec check_expr gh mut vis rst e0 =
  let gh = gh || e0.e_ghost in
Andrei Paskevich's avatar
Andrei Paskevich committed
635 636 637 638 639 640
  let find_reset v e =
    (find_effect (fun eff -> eff_stale_region eff v.pv_ity) e).e_loc in
  let error_v v e = Loc.errorm ?loc:(find_reset v e) "This expression \
    prohibits further usage of variable %s" v.pv_vs.vs_name.id_string in
  let error_s s v e = Loc.errorm ?loc:(find_reset v e) "This expression \
    prohibits further usage of function %s" s.ps_name.id_string in
641 642
  let error_r _r = Loc.errorm ?loc:e0.e_loc "This expression \
    makes a ghost write into a non-ghost location" in
643 644 645 646
  let check_v rst v = Opt.iter (error_v v) (Mpv.find_opt v rst) in
  let check_r rst r = Mpv.iter error_v (Mpv.set_inter rst r) in
  let check_t rst t = check_r rst (t_freepvs Spv.empty t) in
  let reset_c rst c = Mpv.set_inter rst c.cty_reads in
Andrei Paskevich's avatar
Andrei Paskevich committed
647
  let check_c rst c = check_r rst c.cty_reads in
648
  let check_e rst e = check_expr gh mut vis rst e in
Andrei Paskevich's avatar
Andrei Paskevich committed
649 650
  let after_e ({e_effect = eff} as e) =
    if Mreg.is_empty eff.eff_resets then rst else
Andrei Paskevich's avatar
Andrei Paskevich committed
651 652
    Mpv.set_union rst (Mpv.mapi_filter (fun {pv_ity = ity} () ->
      if eff_stale_region eff ity then Some e else None) mut) in
653
  let ghost_c vis c = Mreg.set_inter vis (cty_ghost_writes gh c) in
654
  match e0.e_node with
655
  | Evar v -> check_v rst v
Andrei Paskevich's avatar
Andrei Paskevich committed
656
  | Esym s -> Mpv.iter (error_s s) (reset_c rst s.ps_cty)
657 658 659 660 661 662 663
  | Eapp ({e_node = Efun d},[],({cty_args = []} as c)) ->
      let rst = reset_c rst c and gwr = ghost_c vis c in
      if not (Mpv.is_empty rst && Mreg.is_empty gwr) then
      (check_e rst d; Mpv.iter error_v rst; assert false)
  | Eapp (d,l,c) ->
      check_e rst d; List.iter (check_v (after_e d)) l;
      if c.cty_args = [] then Sreg.iter error_r (ghost_c vis c)
Andrei Paskevich's avatar
Andrei Paskevich committed
664
  | Efun _ | Eany -> check_c rst (cty_of_expr e0)
665 666 667 668 669 670
  | Eassign al ->
      List.iter (fun (r,f,v) -> check_v rst r; check_v rst v;
        if not f.pv_ghost && (gh || r.pv_ghost || v.pv_ghost)
        then match r.pv_ity.ity_node with
          | Ityreg r when Sreg.mem r vis -> error_r r
          | _ -> ()) al
671
  | Elet ({let_sym = ValV v; let_expr = d},e) ->
672 673 674 675 676
      check_expr (gh || v.pv_ghost) mut vis rst d;
      check_expr gh (pv_mut v mut) (pv_vis v vis) (after_e d) e
  | Elet ({let_sym = ValS s; let_expr = d},e) ->
      check_expr (gh || s.ps_ghost) mut vis rst d;
      check_e (after_e d) e
677
  | Erec ({rec_defn = fdl},e) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
678
      List.iter (fun fd -> check_c rst fd.fun_sym.ps_cty) fdl;
679 680 681
      check_e rst e
  | Elazy (_,d,e) ->
      check_e rst d; check_e (after_e d) e
682
  | Eif (c,d,e) ->
683 684
      check_e rst c; let rst = after_e c in
      check_e rst d; check_e rst e
685
  | Etry (d,xl) ->
686 687
      check_e rst d; let rst = after_e d in
      List.iter (fun (_,_,e) -> check_e rst e) xl
688
  | Ecase (d,bl) ->
689 690 691 692 693 694 695 696
      check_e rst d; let rst = after_e d in
      List.iter (fun ({pp_pat = {pat_vars = vss}},e) ->
        let ppv = pvs_of_vss Spv.empty vss in
        check_expr gh (Spv.fold pv_mut ppv mut)
                      (Spv.fold pv_vis ppv vis) rst e) bl
  | Ewhile (d,inv,vl,e) -> let rst = after_e e0 in
      check_t rst inv; check_e rst d; check_e rst e;
      List.iter (fun (t,_) -> check_t rst t) vl
697
  | Efor (_,_,inv,e) -> let rst = after_e e in
698 699
      check_t rst inv; check_e rst e
  | Enot e | Eraise (_,e) | Eghost e -> check_e rst e
700
  | Eassert (_,t) | Epure t -> check_t rst t
701
  | Econst _ | Eabsurd | Etrue | Efalse -> ()
702

703
let e_fun args p q xq ({e_effect = eff} as e) =
704 705
  let c = create_cty args p q xq (e_vars e) eff (ity_of_expr e) in
  (* TODO/FIXME: detect stale vars in post-conditions? *)
706 707 708
  let mut = Spv.fold pv_mut c.cty_reads Spv.empty in
  let mut = List.fold_right pv_mut c.cty_args mut in
  check_expr false mut (cty_r_visible c) Mpv.empty e;
709
  mk_expr (Efun e) (VtyC c) e.e_ghost eff_empty
Andrei Paskevich's avatar
Andrei Paskevich committed
710 711 712

(* recursive definitions *)

713 714 715 716 717 718 719
let ps_clone ({ps_name = id; ps_ghost = ghost} as s) c =
  create_psymbol (id_clone id) ~ghost ~kind:(ps_kind s) c

let cty_add_variant d varl = let add s (t,_) = t_freepvs s t in
  cty_add_reads (cty_of_expr d) (List.fold_left add Spv.empty varl)

let rec e_ps_subst sm e = e_label_copy e (match e.e_node with
720 721
  | Evar _ | Econst _ | Eany | Etrue | Efalse
  | Eassign _ | Eassert _ | Epure _ | Eabsurd -> e
722
  | Esym s -> e_sym (Mps.find_def s s sm)
723 724 725 726 727 728 729
  | Efun d ->
      let d = e_ps_subst sm d in let c = cty_of_expr e in
      e_fun c.cty_args c.cty_pre c.cty_post c.cty_xpost d
  | Eapp (d,vl,c) ->
      let d = e_ps_subst sm d in
      let al = List.map (fun v -> v.pv_ity) c.cty_args in
      e_app_raw d vl al c.cty_result
730 731 732 733 734 735 736 737 738 739 740 741 742
  | Elet ({let_sym = ValV v; let_expr = d} as ld, e) ->
      let d = e_ps_subst sm d in
      ity_equal_check (ity_of_expr d) v.pv_ity;
      if d.e_ghost && not v.pv_ghost then Loc.errorm
        "Expr.create_rec_defn: ghost status mismatch";
      e_let_raw {ld with let_expr = d} (e_ps_subst sm e)
  | Elet ({let_sym = ValS s; let_expr = d},e) ->
      let d = e_ps_subst sm d in
      if d.e_ghost && not s.ps_ghost then Loc.errorm
        "Expr.create_rec_defn: ghost status mismatch";
      let ld, ns = create_let_defn_ps (id_clone s.ps_name)
        ~ghost:s.ps_ghost ~kind:(ps_kind s) d in
      e_let_raw ld (e_ps_subst (Mps.add s ns sm) e)
743
  | Erec ({rec_defn = fdl; rec_decr = ds},e) ->
744 745 746 747 748 749 750 751
      let ndl = List.map (fun fd ->
        fd.fun_rsym, e_ps_subst sm fd.fun_expr) fdl in
      let merge {fun_sym = s; fun_varl = varl} (rs,d) =
        { fun_sym = ps_clone s (cty_add_variant d varl);
          fun_rsym = rs; fun_expr = d; fun_varl = varl } in
      let nfdl = List.map2 merge fdl (rec_fixp ndl) in
      let add m o n = Mps.add o.fun_sym n.fun_sym m in
      let sm = List.fold_left2 add sm fdl nfdl in
752 753
      let rd = {rec_defn = nfdl; rec_decr = ds} in
      e_rec rd (e_ps_subst sm e)
754 755 756 757 758 759 760 761 762 763
  | Eghost e -> e_ghost (e_ps_subst sm e)
  | Enot e -> e_not (e_ps_subst sm e)
  | Eif (c,d,e) -> e_if (e_ps_subst sm c) (e_ps_subst sm d) (e_ps_subst sm e)
  | Elazy (op,d,e) -> e_lazy op (e_ps_subst sm d) (e_ps_subst sm e)
  | Efor (v,b,inv,e) -> e_for_raw v b inv (e_ps_subst sm e)
  | Ewhile (d,inv,vl,e) -> e_while (e_ps_subst sm d) inv vl (e_ps_subst sm e)
  | Eraise (xs,d) -> e_raise xs (e_ps_subst sm d) (ity_of_expr e)
  | Ecase (d,bl) -> e_case (e_ps_subst sm d)
      (List.map (fun (pp,e) -> pp, e_ps_subst sm e) bl)
  | Etry (d,xl) -> e_try (e_ps_subst sm d)
764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779
      (List.map (fun (xs,v,e) -> xs, v, e_ps_subst sm e) xl))

and rec_fixp dl =
  let update sm (s,d) =
    let c = cty_of_expr d in
    if d.e_ghost && not s.ps_ghost then Loc.errorm
      "Expr.create_rec_defn: ghost status mismatch";
    let c = if List.length c.cty_pre < List.length s.ps_cty.cty_pre
            then c else cty_add_pre c [List.hd s.ps_cty.cty_pre] in
    if eff_equal c.cty_effect s.ps_cty.cty_effect &&
       Spv.equal c.cty_reads s.ps_cty.cty_reads
    then sm, (s,d)
    else let n = ps_clone s c in Mps.add s n sm, (n,d) in
  let sm, dl = Lists.map_fold_left update Mps.empty dl in
  if Mps.is_empty sm then dl else
  rec_fixp (List.map (fun (s,d) -> s, e_ps_subst sm d) dl)
780

Andrei Paskevich's avatar
Andrei Paskevich committed
781
let create_rec_defn fdl =
782 783 784 785
  (* check that the variant relations are well-typed *)
  List.iter (fun (_,_,vl,_) -> List.iter (function
    | t, Some rel -> ignore (ps_app rel [t;t])
    | t, None     -> ignore (t_type t)) vl) fdl;
Andrei Paskevich's avatar
Andrei Paskevich committed
786 787
  (* check that the all variants use the same order *)
  let varl1 = match fdl with
788
    | (_,_,vl,_)::_ -> List.rev vl
Andrei Paskevich's avatar
Andrei Paskevich committed
789
    | [] -> invalid_arg "Expr.create_rec_defn" in
790
  let no_int t = not (ty_equal (t_type t) ty_int) in
791
  let check_variant (_,_,vl,_) =
Andrei Paskevich's avatar
Andrei Paskevich committed
792
    let vl, varl1 = match List.rev vl, varl1 with
793 794
      | (t, None)::vl, (t1, None)::varl1
        when no_int t && no_int t1 -> vl, varl1
Andrei Paskevich's avatar
Andrei Paskevich committed
795 796
      | _, _ -> vl, varl1 in
    let res = try List.for_all2 (fun (t1,r1) (t2,r2) ->
797
        Opt.equal ty_equal t1.t_ty t2.t_ty &&
Andrei Paskevich's avatar
Andrei Paskevich committed
798 799 800 801
        Opt.equal ls_equal r1 r2) vl varl1
      with Invalid_argument _ -> false in
    if not res then Loc.errorm
      "All functions in a recursive definition \
802
        must use the same well-founded order for variant" in
Andrei Paskevich's avatar
Andrei Paskevich committed
803
  List.iter check_variant (List.tl fdl);
804 805 806 807 808 809 810 811 812 813 814
  (* create the dummy "decrease" predicate symbol *)
  let add_a l (t,_) = t_type t :: l in
  let ds = match varl1 with
    | [] -> None
    | (t,None)::vl when no_int t ->
        let tv = create_tvsymbol (id_fresh "a") in
        let al = List.fold_left add_a [ty_var tv] vl in
        Some (create_lsymbol (id_fresh "DECR") al None)
    | vl ->
        let al = List.fold_left add_a [] vl in
        Some (create_lsymbol (id_fresh "DECR") al None) in
815
  (* create the first substitution *)
816 817 818 819 820 821 822 823 824 825 826
  let update sm (s,d,varl,_) =
    let c = cty_of_expr d in
    (* check that the type signatures are consistent *)
    let same u v =
      u.pv_ghost = v.pv_ghost && ity_equal u.pv_ity v.pv_ity in
    if (match d.e_node with Efun _ -> false | _ -> true) ||
       not (Lists.equal same s.ps_cty.cty_args c.cty_args) ||
       not (ity_equal s.ps_cty.cty_result c.cty_result) ||
       (d.e_ghost && not s.ps_ghost) || c.cty_args = []
    then invalid_arg "Expr.create_rec_defn";
    (* prepare the extra "decrease" precondition *)
827 828 829
    let pre = match ds with
      | Some ls -> ps_app ls (List.map fst varl) :: c.cty_pre
      | None -> c.cty_pre in
830
    (* create the clean psymbol *)
831
    let id = id_clone s.ps_name in
832 833 834 835 836 837 838 839 840 841 842 843
    let c = create_cty c.cty_args pre
      c.cty_post c.cty_xpost Spv.empty eff_empty c.cty_result in
    let ns = create_psymbol id ~ghost:s.ps_ghost ~kind:PKnone c in
    Mps.add s ns sm, (ns,d) in
  let sm, dl = Lists.map_fold_left update Mps.empty fdl in
  (* produce the recursive definition *)
  let conv (s,d) = s, e_ps_subst sm d in
  let merge (_,_,varl,kind) (rs,d) =
    let id = id_clone rs.ps_name in
    let c = cty_add_variant d varl in
    let s = create_psymbol id ~kind ~ghost:rs.ps_ghost c in
    { fun_sym = s; fun_rsym = rs; fun_expr = d; fun_varl = varl } in
844 845
  let dl = List.map2 merge fdl (rec_fixp (List.map conv dl)) in
  { rec_defn = dl; rec_decr = ds }