expr.ml 52.5 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   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
(********************************************************************)

open Stdlib
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
let rs_ghost s = s.rs_cty.cty_effect.eff_ghost

70
let check_effects ?loc c =
71 72
  if c.cty_effect.eff_oneway then Loc.errorm ?loc
    "This function may not terminate, it cannot be used as pure";
73
  if not (cty_pure c) then Loc.errorm ?loc
74
    "This function has side effects, it cannot be used as pure"
75 76

let check_reads ?loc c =
77 78 79 80
  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 =
81
  if not (Mreg.is_empty c.cty_freeze.isb_reg) then Loc.errorm ?loc
82 83 84 85 86 87 88
    "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"
89 90 91 92 93

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)

94
let make_post t = match t.t_ty with
95 96
  | Some ty ->
      let res = create_vsymbol (id_fresh "result") ty in
97
      create_post res (t_equ (t_var res) t)
98 99
  | None ->
      let res = create_vsymbol (id_fresh "result") ty_bool in
100 101 102
      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]
103 104

let create_rsymbol ({pre_loc=loc} as id) ?(ghost=false) ?(kind=RKnone) c =
105
  let arg_list c = List.map (fun a -> t_var a.pv_vs) c.cty_args in
106 107
  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
108
  let c = cty_ghostify ?loc ghost c in
109
  match kind with
110
  | RKnone ->
111
      mk_rs (id_register id) c RLnone None
112
  | RKlocal ->
113
      check_effects ?loc c; check_state ?loc c;
114 115 116
      (* 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
117
         not regions) of the rsymbol, and the easiest way to do that
118
         is to make these type variables appear in (cty_reads c).
119 120 121 122
         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
123
         it into the rs_logic field. This pvsymbol should not be
124
         used in the program, as it has lost all preconditions,
125 126
         which is why we declare it as ghost. In other words,
         this pvsymbol behaves exactly as Epure of its pv_vs. *)
127
      let v = create_pvsymbol ~ghost:true id (cty_purify c) in
128
      let t = t_func_app_l (t_var v.pv_vs) (arg_list c) in
129
      mk_rs v.pv_vs.vs_name (add_post c t) (RLpv v) None
130 131 132
  | RKfunc ->
      check_effects ?loc c; check_reads ?loc c;
      let ls = create_fsymbol id (arg_type c) (res_type c) in
133
      let t = t_app ls (arg_list c) ls.ls_value in
134
      mk_rs ls.ls_name (add_post c t) (RLls ls) None
135
  | RKpred ->
136 137 138 139
      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;
140 141
      let ls = create_psymbol id (arg_type c) in
      let f = t_app ls (arg_list c) None in
142
      mk_rs ls.ls_name (add_post c f) (RLls ls) None
143
  | RKlemma ->
144
      check_effects ?loc c;
145
      mk_rs (id_register id) c RLlemma None
146

147 148
let rs_dup ({rs_name = {id_loc = loc}} as s) c =
  let id = id_register (id_clone s.rs_name) in
149
  let c = cty_ghostify ?loc (rs_ghost s) c in
150 151
  match s.rs_logic with
  | RLnone ->
152
      mk_rs id c RLnone None
153
  | RLpv v ->
154 155
      check_effects ?loc c; check_state ?loc c;
      Loc.try2 ?loc ity_equal_check v.pv_ity (cty_purify c);
156 157
      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
158
      mk_rs id (add_post c t) (RLpv v) None
159 160 161 162
  | RLls _ ->
      invalid_arg "Expr.rs_dup"
  | RLlemma ->
      check_effects ?loc c;
163
      mk_rs id c RLlemma None
164

Andrei Paskevich's avatar
Andrei Paskevich committed
165 166
let create_projection s v =
  let id = id_clone v.pv_vs.vs_name in
167 168
  let eff = eff_ghostify v.pv_ghost eff_empty in
  let tyl = List.map ity_var s.its_ts.ts_args in
169 170
  let rgl = List.map ity_reg s.its_regions in
  let ity = ity_app s tyl rgl in
171 172
  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
173
  let q = make_post (fs_app ls [t_var arg.pv_vs] v.pv_vs.vs_ty) in
174
  let c = create_cty [arg] [] [q] Mxs.empty Mpv.empty eff v.pv_ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
175 176 177 178 179
  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
180 181
  | [{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
182
  | _ -> raise (FieldExpected s)
Andrei Paskevich's avatar
Andrei Paskevich committed
183

184 185 186
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
187
  if List.exists (fun f -> not (Spv.mem f fs)) s.its_mfields ||
188
    s.its_private || s.its_def <> NoDef || constr < 1 ||
189
    (s.its_mutable && constr > 1) then raise exn;
190 191
  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
192 193
  let rgl = List.map ity_reg s.its_regions in
  let ity = ity_app s tyl rgl in
194 195 196
  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
197
  let q = make_post (fs_app ls argl ty) in
198 199 200
  let eff = match ity.ity_node with
    | Ityreg r -> eff_reset eff_empty (Sreg.singleton r)
    | _ -> eff_empty in
201
  let c = create_cty fl [] [q] Mxs.empty Mpv.empty eff ity in
202
  mk_rs ls.ls_name c (RLls ls) None
203

204
let rs_of_ls ls =
Andrei Paskevich's avatar
Andrei Paskevich committed
205 206 207
  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
208
  let q = make_post (t_app ls t_args ls.ls_value) in
209
  let ity = ity_of_ty (t_type q) in
210
  let c = create_cty v_args [] [q] Mxs.empty Mpv.empty eff_empty ity in
211 212
  mk_rs ls.ls_name c (RLls ls) None

Andrei Paskevich's avatar
Andrei Paskevich committed
213 214
(** {2 Program patterns} *)

215 216 217 218 219
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
220
type prog_pattern = {
221 222 223 224
  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
225 226 227 228
}

type pre_pattern =
  | PPwild
229
  | PPvar of preid * bool
230
  | PPapp of rsymbol * pre_pattern list
231
  | PPas  of pre_pattern * preid * bool
Andrei Paskevich's avatar
Andrei Paskevich committed
232 233
  | PPor  of pre_pattern * pre_pattern

234
exception ConstructorExpected of rsymbol
Andrei Paskevich's avatar
Andrei Paskevich committed
235

236
let create_prog_pattern pp ity mask =
237
  let fail = ref PGnone in
238
  let hg = Hstr.create 3 in
239 240 241 242 243 244 245
  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
246 247
          | MaskGhost -> List.map (Util.const MaskGhost) ls.ls_args
          | MaskVisible -> List.map mask_of_pv rs.rs_cty.cty_args
248 249
          | MaskTuple ml when is_fs_tuple ls &&
              List.length ls.ls_args = List.length ml -> ml
250
          | MaskTuple _ -> invalid_arg "Expr.create_prog_pattern" in
251 252
        (try List.iter2 (scan gp) ml pl with Invalid_argument _ ->
          raise (Term.BadArity (ls, List.length pl)))
253
    | PPapp (rs,_) -> raise (ConstructorExpected rs)
254 255 256
    | 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
257
    | PPwild -> () in
258
  scan PGlast mask pp;
Andrei Paskevich's avatar
Andrei Paskevich committed
259
  let hv = Hstr.create 3 in
260 261 262
  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
263
    with Not_found ->
264 265 266 267 268 269 270 271 272 273 274 275 276 277
      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
278
  mvs, {pp_pat = pat; pp_ity = ity; pp_mask = mask; pp_fail = !fail}
Andrei Paskevich's avatar
Andrei Paskevich committed
279

Andrei Paskevich's avatar
Andrei Paskevich committed
280 281 282 283 284 285 286 287 288 289 290 291
(** {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) *)

292
type assign = pvsymbol * rsymbol * pvsymbol (* region * field * value *)
293

Andrei Paskevich's avatar
Andrei Paskevich committed
294 295
type expr = {
  e_node   : expr_node;
296
  e_ity    : ity;
297
  e_mask   : mask;
Andrei Paskevich's avatar
Andrei Paskevich committed
298 299 300 301 302 303 304
  e_effect : effect;
  e_label  : Slab.t;
  e_loc    : Loc.position option;
}

and expr_node =
  | Evar    of pvsymbol
305
  | Econst  of Number.constant
306
  | Eexec   of cexp * cty
307
  | Eassign of assign list
Andrei Paskevich's avatar
Andrei Paskevich committed
308 309 310
  | Elet    of let_defn * expr
  | Eif     of expr * expr * expr
  | Ecase   of expr * (prog_pattern * expr) list
Andrei Paskevich's avatar
Andrei Paskevich committed
311 312
  | Ewhile  of expr * invariant list * variant list * expr
  | Efor    of pvsymbol * for_bounds * invariant list * expr
313
  | Etry    of expr * (pvsymbol list * expr) Mxs.t
Andrei Paskevich's avatar
Andrei Paskevich committed
314 315
  | Eraise  of xsymbol * expr
  | Eassert of assertion_kind * term
316
  | Eghost  of expr
Andrei Paskevich's avatar
Andrei Paskevich committed
317
  | Epure   of term
Andrei Paskevich's avatar
Andrei Paskevich committed
318 319
  | Eabsurd

320 321 322
and cexp = {
  c_node : cexp_node;
  c_cty  : cty;
Andrei Paskevich's avatar
Andrei Paskevich committed
323 324
}

325 326
and cexp_node =
  | Capp of rsymbol * pvsymbol list
327
  | Cpur of lsymbol * pvsymbol list
328 329
  | Cfun of expr
  | Cany
Andrei Paskevich's avatar
Andrei Paskevich committed
330

331 332 333 334 335 336 337 338 339 340
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
341
}
342

Andrei Paskevich's avatar
Andrei Paskevich committed
343
(* basic tools *)
344 345 346 347 348 349 350 351 352 353

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 }

354 355 356 357 358 359 360 361 362 363 364 365
let proxy_label = create_label "whyml_proxy_symbol"
let proxy_labels = Slab.singleton proxy_label

let rec e_label_push ?loc l e = match e.e_node with
  | (Elet (LDvar ({pv_vs = {vs_name = id}},_) as ld, e1)
  |  Elet (LDsym ({rs_name = id},_) as ld, e1))
    when Slab.mem proxy_label id.id_label ->
      let e1 = e_label_push ?loc l e1 in
      { e with e_node = Elet (ld, e1); e_loc = loc }
  | _ ->
      { e with e_label = l; e_loc = loc }

366 367
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
368

369
(* e_fold never goes under cexps *)
Andrei Paskevich's avatar
Andrei Paskevich committed
370
let e_fold fn acc e = match e.e_node with
371 372
  | Evar _ | Econst _ | Eexec _ | Eassign _
  | Eassert _ | Epure _ | Eabsurd -> acc
373
  | Eraise (_,e) | Efor (_,_,_,e) | Eghost e
374 375
  | Elet ((LDsym _|LDrec _), e) -> fn acc e
  | Elet (LDvar (_,d), e) | Ewhile (d,_,_,e) -> fn (fn acc d) e
Andrei Paskevich's avatar
Andrei Paskevich committed
376 377
  | Eif (c,d,e) -> fn (fn (fn acc c) d) e
  | Ecase (d,bl) -> List.fold_left (fun acc (_,e) -> fn acc e) (fn acc d) bl
378
  | Etry (d,xl) -> Mxs.fold (fun _ (_,e) acc -> fn acc e) xl (fn acc d)
Andrei Paskevich's avatar
Andrei Paskevich committed
379

380 381 382 383 384 385 386 387
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
388 389
      | Eexec ({c_node = Cfun d},_) -> find loc d
      | _ ->                    e_fold find loc e in
390 391 392 393 394 395 396 397 398
    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
399
    | Some fds -> r.reg_its.its_private ||
400 401 402 403 404 405 406 407 408 409 410 411 412
        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))

413 414 415 416 417 418 419 420
(* 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))

421 422 423 424 425 426 427 428
(* 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
429 430 431 432 433 434 435 436 437 438 439 440 441
    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
442
  | IllegalUpdate (v,r) -> localize_immut_write v r el
443
  | StaleVariable (v,r) -> localize_reset_stale v r el
444
  | GhostDivergence     -> localize_divergence el
Andrei Paskevich's avatar
Andrei Paskevich committed
445

446 447
(* smart constructors *)

448
let mk_expr node ity mask eff = {
449
  e_node   = node;
450
  e_ity    = ity;
451
  e_mask   = mask_adjust eff ity mask;
452 453 454 455 456
  e_effect = eff;
  e_label  = Slab.empty;
  e_loc    = None;
}

457 458 459 460
let mk_cexp node cty = {
  c_node   = node;
  c_cty    = cty;
}
461

462
let e_var ({pv_ity = ity; pv_ghost = ghost} as v) =
463 464
  let eff = eff_ghostify ghost (eff_read_single v) in
  mk_expr (Evar v) ity MaskVisible eff
465

466 467
let e_const c ity =
  Term.check_literal c (ty_of_ity ity);
468
  mk_expr (Econst c) ity MaskVisible eff_empty
469 470

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

473
let e_ghostify gh ({e_effect = eff} as e) =
474 475 476
  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
477

478 479
let c_cty_ghostify gh ({c_cty = cty} as c) =
  if not gh || cty.cty_effect.eff_ghost then cty else
480
  let el = match c.c_node with Cfun e -> [e] | _ -> [] in
481
  try_effect el Ity.cty_ghostify gh cty
482

483 484 485 486 487 488
(* 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
489
  | Eexec ({c_node = Capp (s,[])},_) -> rs_equal s rs_true
490 491 492
  | _ -> false

let is_e_false e = match e.e_node with
493
  | Eexec ({c_node = Capp (s,[])},_) -> rs_equal s rs_false
494 495 496 497 498 499 500 501 502 503 504 505
  | _ -> false

let t_void = t_tuple []

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

let copy_labels e t =
  if e.e_loc = None && Slab.is_empty e.e_label then t else
  let loc = if t.t_loc = None then e.e_loc else t.t_loc in
  t_label ?loc (Slab.union e.e_label t.t_label) t

506 507 508 509 510 511 512 513 514 515 516 517 518 519
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
  | _ -> t_label ?loc:f.t_loc Slab.empty (t_if_simp f t_bool_true t_bool_false)

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
  | Tapp (fs,[]) when ls_equal fs fs_bool_true -> t_label_copy t t_true
  | Tapp (fs,[]) when ls_equal fs fs_bool_false -> t_label_copy t t_false
  | _ -> t_label ?loc:t.t_loc Slab.empty (t_equ_simp t t_bool_true)

520
let rec pure_of_post prop v h = match h.t_node with
521 522 523 524 525 526 527 528 529
  | 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) ->
530
      let t, f = pure_of_post prop v f in
531 532 533 534 535 536 537
      t, t_label_copy h (t_and_simp f g)
  | _ -> raise Exit

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
538 539 540 541 542 543
  | _ when ity_equal e.e_ity ity_unit -> t_void
    (* we do not check e.e_effect here, since we check the
        effects later for the overall expression. The only
        effect-hiding construction, Etry, is forbidden. *)
  | Eassign _ | Ewhile _ | Efor _ | Eassert _ -> assert false
  | Evar v -> t_var v.pv_vs
544 545 546 547
  | Econst (Number.ConstInt _ as c)->
      t_const c ty_int
  | Econst (Number.ConstReal _ as c)->
      t_const c ty_real
548
  | Epure t -> t
549
  | Eghost e -> pure_of_expr prop e
550
  | Eexec (_,{cty_post = []}) -> raise Exit
Andrei Paskevich's avatar
Andrei Paskevich committed
551
  | Eexec (_,{cty_post = q::_}) ->
552 553
      let v, h = open_post q in
      fst (pure_of_post prop v h)
554
  | Elet (LDvar (v,_d),e) when ity_equal v.pv_ity ity_unit ->
555
      t_subst_single v.pv_vs t_void (pure_of_expr prop e)
556
  | Elet (LDvar (v,d),e) ->
557
      t_let_close_simp v.pv_vs (pure_of_expr false d) (pure_of_expr prop e)
558 559 560 561 562
  | 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;
563
      pure_of_expr prop e
564 565
  | Elet (LDrec rdl,e) ->
      if List.exists (fun rd -> is_rlpv rd.rec_sym) rdl then raise Exit;
566
      pure_of_expr prop e
567 568 569 570 571 572 573
  | Eif (e0,e1,e2) when is_e_false e1 && is_e_true e2 ->
      t_not (pure_of_expr true e0)
  | Eif (e0,e1,e2) when is_e_false e2 ->
      t_and (pure_of_expr true e0) (pure_of_expr true e1)
  | Eif (e0,e1,e2) when is_e_true e1 ->
      t_or (pure_of_expr true e0) (pure_of_expr true e2)
  | Eif (e0,e1,e2) ->
574
      let prop = prop || ity_equal e.e_ity ity_bool in
575
      t_if (pure_of_expr true e0) (pure_of_expr prop e1) (pure_of_expr prop e2)
576
  | Ecase (d,bl) ->
577
      let prop = prop || ity_equal e.e_ity ity_bool in
578 579
      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)
580
  | Etry _ | Eraise _ | Eabsurd -> raise Exit
581

582 583 584 585
and pure_of_expr prop e = match copy_labels e (raw_of_expr prop e) with
  | {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
586

587
let term_of_expr ~prop e =
588
  if not (eff_pure e.e_effect) then None else
589 590 591 592 593 594 595 596 597 598 599 600 601 602
  try Some (pure_of_expr prop e) with Exit -> None

let post_of_term res t =
  let loca f = t_label ?loc:t.t_loc Slab.empty f in
  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))

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
603
  | Evar v -> post_of_term res (t_var v.pv_vs)
604 605 606 607
  | 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)
608 609
  | Epure t -> post_of_term res t
  | Eghost e -> post_of_expr res e
610 611
  | Eexec (_,c) ->
      let conv q = open_post_with res q in
612
      copy_labels e (t_and_l (List.map conv c.cty_post))
613 614 615 616 617 618 619 620 621 622 623 624 625
  | Elet (LDvar (v,_d),e) when ity_equal v.pv_ity ity_unit ->
      copy_labels e (t_subst_single v.pv_vs t_void (post_of_expr res e))
  | Elet (LDvar (v,d),e) ->
      copy_labels e (t_let_close_simp v.pv_vs
        (pure_of_expr false d) (post_of_expr res e))
  | Elet (LDsym (s,_),e) ->
      if is_rlpv s then raise Exit;
      copy_labels e (post_of_expr res e)
  | Elet (LDrec rdl,e) ->
      if List.exists (fun rd -> is_rlpv rd.rec_sym) rdl then raise Exit;
      copy_labels e (post_of_expr res e)
  | Eif (_,e1,e2) when is_e_true e1 || is_e_false e2 ||
                      (is_e_false e1 && is_e_true e2) ->
626
      post_of_term res (pure_of_expr true e)
627 628 629 630 631 632
  | Eif (e0,e1,e2) ->
      t_if (pure_of_expr true e0) (post_of_expr res e1) (post_of_expr res e2)
  | Ecase (d,bl) ->
      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)
  | Etry _ | Eraise _ -> raise Exit
633
  | Eabsurd -> copy_labels e t_false
634 635 636 637

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
638 639 640 641 642 643
  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 ->
644 645 646 647 648 649 650 651 652 653 654 655 656 657 658
  try [create_post res (post_of_expr (t_var res) e)] with Exit -> []

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
659

660 661 662
(* let-definitions *)

let let_var id ?(ghost=false) e =
663
  let ghost = ghost || mask_ghost e.e_mask in
664 665 666 667
  let v = create_pvsymbol id ~ghost e.e_ity in
  LDvar (v,e), v

let let_sym id ?(ghost=false) ?(kind=RKnone) c =
668
  let cty = c_cty_ghostify ghost c in
669 670 671 672 673 674 675
  (* 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 cty = match c with
676
    | {c_node = Cfun e; c_cty = {cty_post = []}}
677
      when (kind = RKnone (*|| kind = RKlocal*)) ->
678 679 680
        cty_add_post cty (local_post_of_expr e)
    | _ -> cty in
  let s = create_rsymbol id ~kind cty in
681 682 683 684 685 686 687 688 689 690
  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) ->
691
        try_effect [d;e] eff_union_seq d.e_effect (bind_pv v e.e_effect)
692
    | LDsym (s,c) ->
693
        try_effect [e] eff_read_pre (cty_reads c.c_cty) (bind_rs s e.e_effect)
694 695 696 697 698 699 700
    | 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
701 702 703
        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
704 705 706

(* callable expressions *)

707 708 709 710 711 712
let e_exec c =
  let cty = match c with
    | {c_node = Cfun e; c_cty = {cty_post = []} as cty} ->
        cty_exec (cty_add_post cty (local_post_of_expr e))
    | _ -> cty_exec c.c_cty in
  mk_expr (Eexec (c, cty)) cty.cty_result cty.cty_mask cty.cty_effect
713 714 715

let c_any c = mk_cexp Cany c

716
let c_fun ?(mask=MaskVisible) args p q xq old e =
717
  let mask = mask_union mask e.e_mask in
718
  (* reset variables are forbidden in post-conditions *)
719
  let c = try create_cty ~mask args p q xq old e.e_effect e.e_ity with
720
    | BadGhostWrite (v,r) -> localize_ghost_write v r [e]
721
    | IllegalUpdate (v,r) -> localize_immut_write v r [e]
722
    | StaleVariable (v,r) -> localize_reset_stale v r [e] in
723
  mk_cexp (Cfun e) c
724 725

let c_app s vl ityl ity =
726 727 728 729 730
  let cty = cty_apply s.rs_cty vl ityl ity in
  let cty = match s.rs_logic with
    | RLls ls when ityl = [] && is_fs_tuple ls -> cty_tuple vl
    | _ -> cty in
  mk_cexp (Capp (s,vl)) cty
731

732
let c_pur s vl ityl ity =
733
  if not (ity_pure ity) then Loc.errorm "This expression must have pure type";
734
  let v_args = List.map (create_pvsymbol ~ghost:false (id_fresh "u")) ityl in
735 736 737 738
  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
  let eff = eff_ghostify true eff_empty in
739
  let cty = create_cty v_args [] [q] Mxs.empty Mpv.empty eff ity in
740 741
  mk_cexp (Cpur (s,vl)) cty

742
let mk_proxy ghost e hd = match e.e_node with
743
  | Evar v when Slab.is_empty e.e_label -> hd, v
Andrei Paskevich's avatar
Andrei Paskevich committed
744 745
  | _ ->
      let id = id_fresh ?loc:e.e_loc ~label:proxy_labels "o" in
746
      let ld, v = let_var ~ghost id e in ld::hd, v
747

748 749
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
750

751 752 753
let let_head hd e = List.fold_left (fun e ld -> e_let ld e) e hd

let e_app s el ityl ity =
754 755 756 757 758 759 760 761 762
  let trues l = List.map Util.ttrue l in
  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
    try down s.rs_cty.cty_args el with Exit -> trues el in
  let hd, vl = List.fold_right2 add_proxy ghl el ([],[]) in
763 764
  let_head hd (e_exec (c_app s vl ityl ity))

765
let e_pur s el ityl ity =
766 767
  let ghl = List.map Util.ttrue el in
  let hd, vl = List.fold_right2 add_proxy ghl el ([],[]) in
768
  let_head hd (e_exec (c_pur s vl ityl ity))
769

770 771
(* assignment *)

772
let e_assign_raw al =
Andrei Paskevich's avatar
Andrei Paskevich committed
773
  let conv (r,f,v) = r, mfield_of_rs f, v in
774
  mk_expr (Eassign al) ity_unit MaskVisible (eff_assign (List.map conv al))
775 776

let e_assign al =
777
  let hr, hv, al = List.fold_right (fun (r,f,v) (hr,hv,al) ->
778 779 780
    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
781 782
    hr, hv, (r,f,v)::al) al ([],[],[]) in
  (* first pants, THEN your shoes *)
783 784 785 786 787 788 789
  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

790 791
let rs_tuple = Hint.memo 17 (fun n ->
  ignore (its_tuple n); rs_of_ls (fs_tuple n))
792 793 794 795 796 797 798 799

let is_rs_tuple rs = rs_equal rs (rs_tuple (List.length rs.rs_cty.cty_args))

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
800
let fs_void = fs_tuple 0
801 802 803 804

let e_void = e_app rs_void [] [] ity_unit

let is_e_void e = match e.e_node with
805
  | Eexec ({c_node = Capp (s,[])},_) -> rs_equal s rs_void
806 807 808 809
  | _ -> false

let rs_func_app = rs_of_ls fs_func_app

810 811 812
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
813
  let c = create_cty v_args [] [] Mxs.empty Mpv.empty eff_empty ity in
814 815
  LDsym (rs_func_app, c_any c)

816 817 818 819 820 821 822
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
823

Andrei Paskevich's avatar
Andrei Paskevich committed
824 825
(* boolean constructors *)

826
let e_if e0 e1 e2 =
827 828
  ity_equal_check e0.e_ity ity_bool;
  ity_equal_check e1.e_ity e2.e_ity;
829 830 831 832 833 834
  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
835 836 837 838

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
839

Andrei Paskevich's avatar
Andrei Paskevich committed
840 841
(* loops *)

842 843 844 845
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;
846 847
  ity_equal_check e.e_ity ity_unit;
  let vars = List.fold_left t_freepvs Spv.empty inv in
848 849 850 851
  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);
852 853 854
  let eff = eff_bind_single v eff in
  let eff = eff_read_single_pre t eff in
  let eff = eff_read_single_pre f eff in
855
  mk_expr (Efor (v,bounds,inv,e)) e.e_ity MaskVisible eff
856 857

let e_for v f dir t inv e =
858 859
  let hd, t = mk_proxy false t [] in
  let hd, f = mk_proxy false f hd in
860 861 862 863 864
  let_head hd (e_for_raw v (f,dir,t) inv e)

let e_while d inv vl e =
  ity_equal_check d.e_ity ity_bool;
  ity_equal_check e.e_ity ity_unit;
865 866 867 868 869 870
  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]