vc.ml 45.4 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10 11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   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.                           *)
(*                                                                  *)
(********************************************************************)

Andrei Paskevich's avatar
Andrei Paskevich committed
12 13 14 15 16 17 18 19
open Ident
open Ty
open Term
open Decl
open Ity
open Expr
open Pdecl

Andrei Paskevich's avatar
Andrei Paskevich committed
20 21
(* basic tools *)

Andrei Paskevich's avatar
Andrei Paskevich committed
22
let debug = Debug.register_info_flag "vc_debug"
Andrei Paskevich's avatar
Vc: wip  
Andrei Paskevich committed
23 24
  ~desc:"Print@ details@ of@ verification@ conditions@ generation."

Andrei Paskevich's avatar
Andrei Paskevich committed
25
let debug_sp = Debug.register_flag "vc_sp"
26 27
  ~desc:"Use@ 'Efficient@ Weakest@ Preconditions'@ for@ verification."

Andrei Paskevich's avatar
Andrei Paskevich committed
28 29 30
let no_eval = Debug.register_flag "vc_no_eval"
  ~desc:"Do@ not@ simplify@ pattern@ matching@ on@ record@ datatypes@ in@ VCs."

Andrei Paskevich's avatar
Andrei Paskevich committed
31 32
let ls_of_rs s =
  match s.rs_logic with RLls ls -> ls | _ -> assert false
Andrei Paskevich's avatar
Andrei Paskevich committed
33

Andrei Paskevich's avatar
Andrei Paskevich committed
34 35
let clone_vs v = create_vsymbol (id_clone v.vs_name) v.vs_ty
let clone_pv v = clone_vs v.pv_vs
Andrei Paskevich's avatar
Andrei Paskevich committed
36

37 38 39
let old_of_pv {pv_vs = v; pv_ity = ity} =
  create_pvsymbol ~ghost:true (id_clone v.vs_name) (ity_purify ity)

Andrei Paskevich's avatar
Andrei Paskevich committed
40 41
let res_of_ity ity =
  create_vsymbol (id_fresh "result") (ty_of_ity ity)
Andrei Paskevich's avatar
Andrei Paskevich committed
42

Andrei Paskevich's avatar
Andrei Paskevich committed
43 44 45 46 47 48
let proxy_of_expr =
  let label = Slab.singleton proxy_label in fun e ->
  (* often we need a proxy variable to be a pvsymbol
     to prevent it from being bound by sp_wp_close *)
  let id = id_fresh ?loc:e.e_loc ~label "o" in
  (create_pvsymbol ~ghost:true id e.e_ity).pv_vs
49

Andrei Paskevich's avatar
Andrei Paskevich committed
50 51 52 53 54 55
let test_of_expr e =
  let v = proxy_of_expr e in
  v, t_equ (t_var v) t_bool_true

let vc_freepvs s v q =
  pvs_of_vss s (Mvs.remove v (t_freevars Mvs.empty q))
56

57 58
let sp_label = Ident.create_label "vc:sp"
let wp_label = Ident.create_label "vc:wp"
59 60 61 62 63

(* VCgen environment *)

type vc_env = {
  known_map : Pdecl.known_map;
64
  letrec_ps : (variant list * lsymbol option list) Mls.t;
65 66 67 68 69 70 71 72 73 74
  ps_int_le : lsymbol;
  ps_int_ge : lsymbol;
  ps_int_lt : lsymbol;
  ps_int_gt : lsymbol;
  fs_int_pl : lsymbol;
  fs_int_mn : lsymbol;
}

let mk_env {Theory.th_export = ns} kn = {
  known_map = kn;
75
  letrec_ps = Mls.empty;
76 77 78 79 80 81 82
  ps_int_le = Theory.ns_find_ls ns ["infix <="];
  ps_int_ge = Theory.ns_find_ls ns ["infix >="];
  ps_int_lt = Theory.ns_find_ls ns ["infix <"];
  ps_int_gt = Theory.ns_find_ls ns ["infix >"];
  fs_int_pl = Theory.ns_find_ls ns ["infix +"];
  fs_int_mn = Theory.ns_find_ls ns ["infix -"];
}
Andrei Paskevich's avatar
Andrei Paskevich committed
83

84
let mk_env env kn = mk_env (Env.read_theory env ["int"] "Int") kn
Andrei Paskevich's avatar
Andrei Paskevich committed
85

86
(* explanation labels *)
Andrei Paskevich's avatar
Andrei Paskevich committed
87

88
let vc_label e f =
89
  if e.e_loc = None && Slab.is_empty e.e_label then f else
Andrei Paskevich's avatar
Andrei Paskevich committed
90 91
  let loc = if f.t_loc = None then e.e_loc else f.t_loc in
  let lab = Ident.Slab.union e.e_label f.t_label in
92 93
  let lab = Ident.Slab.remove sp_label lab in
  let lab = Ident.Slab.remove wp_label lab in
Andrei Paskevich's avatar
Andrei Paskevich committed
94 95
  t_label ?loc lab f

Andrei Paskevich's avatar
Andrei Paskevich committed
96
let expl_pre       = Ident.create_label "expl:precondition"
97 98
let expl_post      = Ident.create_label "expl:postcondition"
let expl_xpost     = Ident.create_label "expl:exceptional postcondition"
99 100 101 102
let expl_assume    = Ident.create_label "expl:assumption"
let expl_assert    = Ident.create_label "expl:assertion"
let expl_check     = Ident.create_label "expl:check"
let expl_absurd    = Ident.create_label "expl:unreachable point"
Andrei Paskevich's avatar
Andrei Paskevich committed
103 104 105
let expl_loop_init = Ident.create_label "expl:loop invariant init"
let expl_loop_keep = Ident.create_label "expl:loop invariant preservation"
let expl_loop_vari = Ident.create_label "expl:loop variant decrease"
106
let expl_variant   = Ident.create_label "expl:variant decrease"
Andrei Paskevich's avatar
Andrei Paskevich committed
107
let _expl_type_inv  = Ident.create_label "expl:type invariant"
Andrei Paskevich's avatar
Andrei Paskevich committed
108

109
let lab_has_expl = let expl_regexp = Str.regexp "expl:" in
Andrei Paskevich's avatar
Andrei Paskevich committed
110 111
  Slab.exists (fun l -> Str.string_match expl_regexp l.lab_string 0)

112 113 114 115
let vc_expl loc l ({t_label = lab} as f) =
  let lab = if lab_has_expl lab then lab else Slab.add l lab in
  let loc = if loc = None then f.t_loc else loc in
  t_label ?loc (Slab.add stop_split lab) f
Andrei Paskevich's avatar
Andrei Paskevich committed
116

117 118 119 120 121 122
(* propositional connectives with limited simplification *)

let sp_implies sp wp = match sp.t_node, wp.t_node with
  | Ttrue, _ | _, Ttrue -> wp
  | _, _ -> t_implies sp wp

123
let sp_or sp1 sp2 = match sp1.t_node, sp2.t_node with
124 125 126 127
  | Ttrue, _ | _, Tfalse -> sp1
  | _, Ttrue | Tfalse, _ -> sp2
  | _, _ -> t_or sp1 sp2

128
let sp_and sp1 sp2 = match sp1.t_node, sp2.t_node with
129 130 131 132
  | Ttrue, _ | _, Tfalse -> sp2
  | _, Ttrue | Tfalse, _ -> sp1
  | _, _ -> t_and sp1 sp2

Andrei Paskevich's avatar
Andrei Paskevich committed
133 134 135
let can_simp wp = match wp.t_node with
  | Ttrue -> not (Slab.mem stop_split wp.t_label)
  | _ -> false
136 137 138 139 140 141

let wp_and wp1 wp2 = match wp1.t_node, wp2.t_node with
  | (Ttrue, _ | _, Tfalse) when can_simp wp1 -> wp2
  | (_, Ttrue | Tfalse, _) when can_simp wp2 -> wp1
  | _, _ -> t_and wp1 wp2

142 143 144 145 146
let wp_and_asym wp1 wp2 = match wp1.t_node, wp2.t_node with
  | (Ttrue, _ | _, Tfalse) when can_simp wp1 -> wp2
  | (_, Ttrue | Tfalse, _) when can_simp wp2 -> wp1
  | _, _ -> t_and_asym wp1 wp2

Andrei Paskevich's avatar
Andrei Paskevich committed
147
let wp_if c wp1 wp2 = match c.t_node, wp1.t_node, wp2.t_node with
148 149
  | Ttrue, _, _  when can_simp wp2 -> wp1
  | Tfalse, _, _ when can_simp wp1 -> wp2
150 151 152
  | Tnot c, Ttrue, _  when can_simp wp1 -> sp_implies c wp2
  | _, Ttrue, _  when can_simp wp1 -> sp_implies (t_not c) wp2
  | _, _, Ttrue  when can_simp wp2 -> sp_implies c wp1
153 154
  | _, _, _ -> t_if c wp1 wp2

Andrei Paskevich's avatar
Andrei Paskevich committed
155 156 157 158
let wp_case t bl =
  let check b = can_simp (snd (t_open_branch b)) in
  if List.for_all check bl then t_true else t_case t bl

159 160 161 162
let wp_forall vl wp = t_forall_close_simp vl [] wp

let wp_let v t wp = t_let_close_simp v t wp

Andrei Paskevich's avatar
Andrei Paskevich committed
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
(* exception-related tools *)

let union_mexn xsp1 xsp2 =
  Mexn.union (fun _ sp1 sp2 -> Some (sp_or sp1 sp2)) xsp1 xsp2

let inter_mexn fn xsp xwp =
  Mexn.inter (fun _ sp wp -> Some (fn sp wp)) xsp xwp

let wp_inter_mexn wp fn xsp xwp =
  Mexn.fold (fun _ g f -> wp_and f g) (inter_mexn fn xsp xwp) wp

let sp_inter_mexn sp fn xsp xsp' =
  Mexn.fold (fun _ g f -> sp_or f g) (inter_mexn fn xsp xsp') sp

let cty_xpost_real c = (* drop raises {X -> false} *)
  Mexn.set_inter c.cty_xpost c.cty_effect.eff_raises

let res_of_xbranch xs vl map out = match vl with
Andrei Paskevich's avatar
Andrei Paskevich committed
181
  | [] -> res_of_ity ity_unit, out
Andrei Paskevich's avatar
Andrei Paskevich committed
182 183 184 185 186 187 188 189
  | [v] -> v.pv_vs, out
  | vl ->
      let v = res_of_ity xs.xs_ity in
      let cs = fs_tuple (List.length vl) in
      let pl = List.map (fun v -> pat_var v.pv_vs) vl in
      let p = pat_app cs pl v.vs_ty and t = t_var v in
      v, map (fun f -> t_case_close t [p, f]) out

190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217
(* variant decrease pre-conditions *)

let decrease_alg env loc old_t t =
  let oty = t_type old_t and nty = t_type t in
  let quit () = Loc.errorm ?loc "no default order for %a" Pretty.print_term t in
  let ts = match oty with {ty_node = Tyapp (ts,_)} -> ts | _ -> quit () in
  let itd = find_its_defn env.known_map (restore_its ts) in
  let get_cs rs = match rs.rs_logic with RLls cs -> cs | _ -> quit () in
  let csl = List.map get_cs itd.itd_constructors in
  if csl = [] then quit ();
  let sbs = ty_match Mtv.empty (ty_app ts (List.map ty_var ts.ts_args)) oty in
  let add_arg fty acc =
    let fty = ty_inst sbs fty in
    if ty_equal fty nty then
      let vs = create_vsymbol (id_fresh "f") nty in
      pat_var vs, t_or_simp (t_equ (t_var vs) t) acc
    else pat_wild fty, acc in
  let add_cs cs =
    let pl, f = Lists.map_fold_right add_arg cs.ls_args t_false in
    t_close_branch (pat_app cs pl oty) f in
  t_case old_t (List.map add_cs csl)

let decrease_def env loc old_t t =
  if ty_equal (t_type old_t) ty_int && ty_equal (t_type t) ty_int
  then t_and (ps_app env.ps_int_le [t_nat_const 0; old_t])
             (ps_app env.ps_int_lt [t; old_t])
  else decrease_alg env loc old_t t

Andrei Paskevich's avatar
Andrei Paskevich committed
218
let decrease env loc lab olds news =
219 220 221 222 223 224 225 226 227 228 229 230
  let rec decr olds news = match olds, news with
    | (old_t, Some old_r)::olds, (t, Some r)::news
      when oty_equal old_t.t_ty t.t_ty && ls_equal old_r r ->
        let dt = ps_app r [t; old_t] in
        t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds news))
    | (old_t, None)::olds, (t, None)::news
      when oty_equal old_t.t_ty t.t_ty ->
        let dt = decrease_def env loc old_t t in
        t_or_simp dt (t_and_simp (t_equ old_t t) (decr olds news))
    | (old_t, None)::_, (t, None)::_ ->
        decrease_def env loc old_t t
    | _ -> t_false in
231
  vc_expl loc lab (decr olds news)
Andrei Paskevich's avatar
Andrei Paskevich committed
232 233 234 235 236 237 238 239 240 241 242 243

let oldify_variant varl =
  if varl = [] then Mvs.empty, varl else
  let fpv = Mpv.mapi_filter (fun v _ -> (* oldify mutable vars *)
    if ity_immutable v.pv_ity then None else Some (old_of_pv v))
    (List.fold_left (fun s (t,_) -> t_freepvs s t) Spv.empty varl) in
  if Mpv.is_empty fpv then Mvs.empty, varl else
  let o2n = Mpv.fold (fun v o s ->
    Mvs.add o.pv_vs (t_var v.pv_vs) s) fpv Mvs.empty in
  let n2o = Mpv.fold (fun v o s ->
    Mvs.add v.pv_vs (t_var o.pv_vs) s) fpv Mvs.empty in
  o2n, List.map (fun (t,r) -> t_subst n2o t, r) varl
244

Andrei Paskevich's avatar
Andrei Paskevich committed
245 246 247 248 249
(* convert user specifications into wp and sp *)

let t_var_or_void v =
  if ty_equal v.vs_ty ty_unit then t_void else t_var v

250
let wp_of_inv loc lab pl = t_and_l (List.map (vc_expl loc lab) pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
251

252 253 254 255
let wp_of_pre ({letrec_ps = lps} as env) loc lab = function
  | {t_node = Tapp (ls, tl)} :: pl when Mls.mem ls lps ->
      let olds, rels = Mls.find ls lps in
      let news = List.combine tl rels in
Andrei Paskevich's avatar
Andrei Paskevich committed
256
      let p = decrease env loc expl_variant olds news in
257 258
      wp_and p (wp_of_inv loc lab pl)
  | pl -> wp_of_inv loc lab pl
Andrei Paskevich's avatar
Andrei Paskevich committed
259

Andrei Paskevich's avatar
Andrei Paskevich committed
260 261 262
let wp_of_post lab ity = function
  | q::ql ->
      let v, q = open_post q in let t = t_var_or_void v in
263 264
      let mk_post q = vc_expl None lab (open_post_with t q) in
      v, t_and_l (vc_expl None lab q :: List.map mk_post ql)
Andrei Paskevich's avatar
Andrei Paskevich committed
265 266 267
  | [] ->
      res_of_ity ity, t_true

268
let rec push_stop loc lab f = match f.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
269
  | Tbinop (Tand,g,h) when not (Slab.mem stop_split f.t_label) ->
270 271
      t_label_copy f (t_and (push_stop loc lab g) (push_stop loc lab h))
  | _ -> vc_expl loc lab f
Andrei Paskevich's avatar
Andrei Paskevich committed
272

273
let sp_of_pre lab pl = t_and_l (List.map (push_stop None lab) pl)
Andrei Paskevich's avatar
Andrei Paskevich committed
274

275
let sp_of_post loc lab v ql =
276 277
  let t = t_var_or_void v in
  (* remove the post-condition of () *)
278
  let push q = match open_post_with t q with
279 280
    | {t_node = Tapp (ps, [_; {t_ty = Some ty}])}
      when ls_equal ps ps_equ && ty_equal ty ty_unit -> t_true
281
    | f -> push_stop loc lab f in
Andrei Paskevich's avatar
Andrei Paskevich committed
282 283
  t_and_l (List.map push ql)

Andrei Paskevich's avatar
Andrei Paskevich committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
(* a type is affected if a modified region is reachable from it *)

let ity_affected wr ity = Util.any ity_rch_fold (Mreg.contains wr) ity

let pv_affected wr v = ity_affected wr v.pv_ity

(* a "destination map" maps program variables (pre-effect state)
   to fresh vsymbols (post-effect state) *)

let dst_of_pvs cv pvs = (* check that cv is non-empty at the call site *)
  let conv v () = if pv_affected cv v then Some (clone_pv v) else None in
  Mpv.mapi_filter conv pvs

let dst_of_wp cv wp =
  if Sreg.is_empty cv then Mpv.empty else
  dst_of_pvs cv (t_freepvs Spv.empty wp)

let dst_affected {eff_covers = cv} dst =
  if Mreg.is_empty cv then Mpv.empty else
  Mpv.filter (fun v _ -> pv_affected cv v) dst

let dst_step_back_raw cv1 rd2 cv2 dst =
  if Mreg.is_empty cv1 then Mpv.empty else
  let back o n =
    if not (pv_affected cv1 o) then None else
    if not (pv_affected cv2 o) then Some n else
    Some (clone_pv o) in
  Mpv.set_union (Mpv.mapi_filter back dst)
    (dst_of_pvs cv1 (Mpv.set_diff rd2 dst))

let dst_step_back eff1 eff2 dst =
  dst_step_back_raw eff1.eff_covers
    eff2.eff_reads eff2.eff_covers dst

let advancement dst = Mpv.fold (fun v n sbs ->
  Mvs.add v.pv_vs (t_var n) sbs) dst Mvs.empty

let adjustment dst dst' =
  let pair _ v n =
    if vs_equal v n then None else Some (v,n) in
  let add _ (v,n) sbs = Mvs.add v (t_var n) sbs in
  Mpv.fold add (Mpv.inter pair dst dst') Mvs.empty

Andrei Paskevich's avatar
Andrei Paskevich committed
327 328
(* combine postconditions with preconditions *)

329 330
let wp_close loc lab v ql wp =
  let sp = sp_of_post loc lab v ql in
Andrei Paskevich's avatar
Andrei Paskevich committed
331
  match term_of_post ~prop:false v sp with
332 333 334 335 336 337
  | Some (t, sp) -> wp_let v t (sp_implies sp wp)
  | None ->      wp_forall [v] (sp_implies sp wp)

let is_fresh v =
  try ignore (restore_pv v); false with Not_found -> true

Andrei Paskevich's avatar
Andrei Paskevich committed
338 339
let sp_wp_close v sp adv wp =
  let wp  = t_subst adv wp in
Andrei Paskevich's avatar
Andrei Paskevich committed
340
  let fvs = t_freevars Mvs.empty sp in
Andrei Paskevich's avatar
Andrei Paskevich committed
341 342 343
  let fvs = Mvs.filter (fun v _ -> is_fresh v) fvs in
  let fvs = Mvs.fold (fun _ t s -> t_freevars s t) adv fvs in
  let vl  = List.rev (Mvs.keys (Mvs.remove v fvs)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
344
  match term_of_post ~prop:false v sp with
Andrei Paskevich's avatar
Andrei Paskevich committed
345 346 347 348 349
  | Some (t, sp) -> wp_forall vl (wp_let v t (sp_implies sp wp))
  | None         -> wp_forall (v :: vl)      (sp_implies sp wp)

let sp_sp_close v sp adv sp' =
  let sp' = t_subst adv sp' in
Andrei Paskevich's avatar
Andrei Paskevich committed
350
  match term_of_post ~prop:false v sp with
Andrei Paskevich's avatar
Andrei Paskevich committed
351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381
  | Some (t, sp) ->                    wp_let v t (sp_and sp sp')
  | None when is_fresh v ->                        sp_and sp sp'
  | None -> t_subst_single v (t_var (clone_vs v)) (sp_and sp sp')

(* express shared region values as "v.f1.f2.f3" when possible *)

let rec explore_paths kn aff regs t ity =
  if ity.ity_imm then regs else
  match ity.ity_node with
  | Ityvar _ -> assert false
  | Ityreg r when not (Sreg.mem r aff) -> regs
  | Ityreg ({reg_its = s; reg_args = tl; reg_regs = rl} as r) ->
      let rec height t = match t.t_node with
        (* prefer user variables to proxy variables *)
        | Tvar v when Slab.mem proxy_label v.vs_name.id_label -> 65536
        | Tvar _ -> 0 | Tapp (_,[t]) -> height t + 1
        | _ -> assert false (* shouldn't happen *) in
      let min t o = if height t < height o then t else o in
      let regs = Mreg.change (fun o -> Some (Opt.fold min t o)) r regs in
      explore_its kn aff regs t s tl rl
  | Ityapp (s,tl,rl) -> explore_its kn aff regs t s tl rl

and explore_its kn aff regs t s tl rl =
  let isb = its_match_regs s tl rl in
  let follow regs rs =
    let ity = ity_full_inst isb rs.rs_cty.cty_result in
    let ls = ls_of_rs rs and ty = Some (ty_of_ity ity) in
    explore_paths kn aff regs (t_app ls [t] ty) ity in
  List.fold_left follow regs (find_its_defn kn s).itd_fields

let name_regions kn wr dst =
Andrei Paskevich's avatar
Andrei Paskevich committed
382 383 384 385 386 387 388 389
  (* for every write collect the regions affected by it or
    reachable from it (needed for multi-staged assignment) *)
  let rec regs_to_name s r =
    let q = if Mreg.mem r wr
      then reg_rch_fold Sreg.add_left Sreg.empty r
      else reg_exp_fold regs_to_name  Sreg.empty r in
    if Sreg.is_empty q then s else Sreg.union s (Sreg.add r q) in
  let collect o _ aff = ity_exp_fold regs_to_name aff o.pv_ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
390 391 392 393 394 395 396
  let aff = Mpv.fold collect dst Sreg.empty in
  let fill o n regs = explore_paths kn aff regs (t_var n) o.pv_ity in
  let regs = Mpv.fold fill dst Mreg.empty in
  let complete r nm _ = if nm <> None then nm else
    let ty = ty_app r.reg_its.its_ts (List.map ty_of_ity r.reg_args) in
    Some (t_var (create_vsymbol (id_clone r.reg_name) ty)) in
  Mreg.merge complete regs aff
Andrei Paskevich's avatar
Andrei Paskevich committed
397

Andrei Paskevich's avatar
Andrei Paskevich committed
398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428
(* multi-staged assignment changes the names of regions *)

let writes_of_assign asl =
  let add wr (r,f,v) =
    let f = Opt.get f.rs_field in
    let r = match r.pv_ity.ity_node with
      | Ityreg r -> r | _ -> assert false in
    Mreg.change (function
      | None   -> Some (Mpv.singleton f v)
      | Some s -> Some (Mpv.add f v s)) r wr in
  List.fold_left add Mreg.empty asl

let rename_regions regs cv wr =
  (* we compute the same region bijection as eff_assign,
     except we do not need any consistency checking now *)
  let reg_rexp {reg_its = s; reg_args = tl; reg_regs = rl} wfs =
    let ity_rexp xl t = ity_exp_fold (fun l r -> r :: l) xl t in
    let sbs = its_match_regs s tl rl in
    let mfield xl f = match Mpv.find_opt f wfs with
      | Some v -> ity_rexp xl v.pv_ity
      | None -> ity_rexp xl (ity_full_inst sbs f.pv_ity) in
    List.fold_left mfield [] s.its_mfields in
  let rec stitch t2f rf rt wfs =
    let t2f = Mreg.add rt rf t2f in
    let link t2f rf rt = stitch t2f rf rt (Mreg.find_def Mpv.empty rt wr) in
    List.fold_left2 link t2f (reg_rexp rf Mpv.empty) (reg_rexp rt wfs) in
  let add_write r wfs t2f = (* reset regions do not partake in renaming *)
    if not (Sreg.mem r cv) then t2f else stitch t2f r r wfs in
  let t2f = Mreg.fold add_write wr Mreg.empty in
  Mreg.map (fun rf -> Mreg.find rf regs) t2f

Andrei Paskevich's avatar
Andrei Paskevich committed
429 430 431
(* produce a rebuilding postcondition after a write effect *)

let cons_t_simp nt t fl =
Andrei Paskevich's avatar
Andrei Paskevich committed
432
  if t_equal nt t then fl else t_equ nt t :: fl
Andrei Paskevich's avatar
Andrei Paskevich committed
433

Andrei Paskevich's avatar
Andrei Paskevich committed
434 435 436 437 438 439
type rhs_of_write = PV of pvsymbol | VD | NF

let rhs_of_effect f wfs = if Mpv.mem f wfs then VD else NF

let rhs_of_assign f wfs = try PV (Mpv.find f wfs) with Not_found -> NF

440 441 442
let sensitive itd {pv_vs = f} =
  List.exists (fun i -> t_v_occurs f i > 0) itd.itd_invariant

Andrei Paskevich's avatar
Andrei Paskevich committed
443
let rec havoc kn get_rhs wr regs t ity fl =
Andrei Paskevich's avatar
Andrei Paskevich committed
444
  if not (ity_affected wr ity) then t, fl else
Andrei Paskevich's avatar
Andrei Paskevich committed
445 446 447
  match ity.ity_node with
  | Ityvar _ -> assert false
  | Ityreg ({reg_its = s} as r) when s.its_nonfree || Mreg.mem r wr ->
Andrei Paskevich's avatar
Andrei Paskevich committed
448 449 450 451
      let itd = find_its_defn kn s in
      let isb = its_match_regs s r.reg_args r.reg_regs in
      let wfs = Mreg.find_def Mpv.empty r wr in
      let nt = Mreg.find r regs in
452 453 454
      let field rs fl =
        let fd = Opt.get rs.rs_field in
        match get_rhs fd wfs with
Andrei Paskevich's avatar
Andrei Paskevich committed
455 456
        | VD -> fl
        | PV {pv_vs = v; pv_ity = ity} ->
457 458 459 460
            if sensitive itd fd then begin
              Warning.emit "invariant-breaking updates are not yet supported";
              fl (* TODO: strong invariants *)
            end else
Andrei Paskevich's avatar
Andrei Paskevich committed
461 462 463 464 465
            let nt = fs_app (ls_of_rs rs) [nt] v.vs_ty in
            let t, fl = havoc kn get_rhs wr regs (t_var v) ity fl in
            cons_t_simp nt t fl
        | NF ->
            let ity = ity_full_inst isb rs.rs_cty.cty_result in
466 467 468 469
            if ity_affected wr ity && sensitive itd fd then begin
              Warning.emit "invariant-breaking updates are not yet supported";
              fl (* TODO: strong invariants *)
            end else
Andrei Paskevich's avatar
Andrei Paskevich committed
470 471 472 473 474
            let ls = ls_of_rs rs and ty = Some (ty_of_ity ity) in
            let t = t_app ls [t] ty and nt = t_app ls [nt] ty in
            let t, fl = havoc kn get_rhs wr regs t ity fl in
            cons_t_simp nt t fl in
      nt, List.fold_right field itd.itd_fields fl
Andrei Paskevich's avatar
Andrei Paskevich committed
475 476 477 478 479 480 481
  | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl}
  | Ityapp (s,tl,rl) ->
      let itd = find_its_defn kn s in
      let isb = its_match_regs s tl rl in
      begin match itd.itd_constructors with
      | [{rs_logic = RLls cs}] (* record *)
        when List.length cs.ls_args = List.length itd.itd_fields ->
Andrei Paskevich's avatar
Andrei Paskevich committed
482
          let field rs (tl, fl) =
Andrei Paskevich's avatar
Andrei Paskevich committed
483
            let ity = ity_full_inst isb rs.rs_cty.cty_result in
Andrei Paskevich's avatar
Andrei Paskevich committed
484
            let t = t_app_infer (ls_of_rs rs) [t] in
Andrei Paskevich's avatar
Andrei Paskevich committed
485
            let t, fl = havoc kn get_rhs wr regs t ity fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
486 487
            t::tl, fl in
          let tl, fl = List.fold_right field itd.itd_fields ([],fl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
488 489 490 491 492 493 494
          let t0 = match tl with
            | {t_node = Tapp (_,[t])}::_ -> t | _ -> t_false in
          let triv rs t = match t.t_node with
            | Tapp (s,[t]) -> ls_equal s (ls_of_rs rs) && t_equal t t0
            | _ -> false in
          let t = if List.for_all2 triv itd.itd_fields tl
            then t0 else fs_app cs tl (ty_of_ity ity) in
Andrei Paskevich's avatar
Andrei Paskevich committed
495
          t, fl
Andrei Paskevich's avatar
Andrei Paskevich committed
496 497 498 499 500 501 502 503 504 505
      | cl ->
          let ty = ty_of_ity ity in
          let branch ({rs_cty = cty} as rs) =
            let cs = ls_of_rs rs in
            let get_ity v = ity_full_inst isb v.pv_ity in
            let ityl = List.map get_ity cty.cty_args in
            let get_pjv {pv_vs = {vs_name = id}} ity =
              create_vsymbol (id_clone id) (ty_of_ity ity) in
            let vl = List.map2 get_pjv cty.cty_args ityl in
            let p = pat_app cs (List.map pat_var vl) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
506
            let field v ity (tl, fl) =
Andrei Paskevich's avatar
Andrei Paskevich committed
507
              let t, fl = havoc kn get_rhs wr regs (t_var v) ity fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
508 509 510
              t::tl, fl in
            let tl, fl = List.fold_right2 field vl ityl ([],[]) in
            (p, fs_app cs tl ty), (p, t_and_l fl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
511
          let tbl, fbl = List.split (List.map branch cl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
512
          let t = t_case_close t tbl and f = t_case_close_simp t fbl in
513
          t, begin match f.t_node with Ttrue -> fl | _ -> f::fl end
Andrei Paskevich's avatar
Andrei Paskevich committed
514 515
      end

Andrei Paskevich's avatar
Andrei Paskevich committed
516
let print_dst dst = if Debug.test_flag debug then
Andrei Paskevich's avatar
Andrei Paskevich committed
517
  Format.printf "@[vars = %a@]@." (Pp.print_list Pp.space
Andrei Paskevich's avatar
Andrei Paskevich committed
518
    (fun fmt (o,n) -> Format.fprintf fmt "(%a -> %a)"
Andrei Paskevich's avatar
Andrei Paskevich committed
519
      Ity.print_pv o Pretty.print_vs n)) (Mpv.bindings dst)
Andrei Paskevich's avatar
Vc: wip  
Andrei Paskevich committed
520

Andrei Paskevich's avatar
Andrei Paskevich committed
521
let print_regs regs = if Debug.test_flag debug then
Andrei Paskevich's avatar
Andrei Paskevich committed
522 523
  Format.printf "@[regs = %a@]@." (Pp.print_list Pp.space
    (fun fmt (r,t) -> Format.fprintf fmt "(%a -> %a)"
Andrei Paskevich's avatar
Andrei Paskevich committed
524
      Ity.print_reg r Pretty.print_term t)) (Mreg.bindings regs)
525

Andrei Paskevich's avatar
Andrei Paskevich committed
526
let wp_havoc_raw kn get_rhs wr wp dst regs =
Andrei Paskevich's avatar
Andrei Paskevich committed
527
  let () = print_dst dst; print_regs regs in
Andrei Paskevich's avatar
Vc: wip  
Andrei Paskevich committed
528
  let add _ t fvs = t_freevars fvs t in
Andrei Paskevich's avatar
Andrei Paskevich committed
529
  let fvs = Mreg.fold add regs Mvs.empty in
530
  let update {pv_vs = o; pv_ity = ity} n wp =
Andrei Paskevich's avatar
Andrei Paskevich committed
531
    let t, fl = havoc kn get_rhs wr regs (t_var o) ity [] in
Andrei Paskevich's avatar
Vc: wip  
Andrei Paskevich committed
532
    if Mvs.mem n fvs then
533 534
      sp_implies (t_and_l (cons_t_simp (t_var n) t fl)) wp
    else wp_let n t (sp_implies (t_and_l fl) wp) in
Andrei Paskevich's avatar
Andrei Paskevich committed
535 536
  let wp = t_subst (advancement dst) wp in
  let wp = Mpv.fold update dst wp in
537
  wp_forall (Mvs.keys fvs) wp
Andrei Paskevich's avatar
Vc: wip  
Andrei Paskevich committed
538

Andrei Paskevich's avatar
Andrei Paskevich committed
539 540 541
let wp_havoc {known_map = kn} {eff_writes = wr; eff_covers = cv} wp =
  let dst = dst_of_wp cv wp in
  if Mpv.is_empty dst then wp else
Andrei Paskevich's avatar
Andrei Paskevich committed
542
  let regs = name_regions kn cv dst in
Andrei Paskevich's avatar
Andrei Paskevich committed
543 544 545
  wp_havoc_raw kn rhs_of_effect wr wp dst regs

let sp_havoc_raw kn get_rhs wr sp dst regs =
Andrei Paskevich's avatar
Andrei Paskevich committed
546
  let () = print_dst dst; print_regs regs in
547
  let update {pv_vs = o; pv_ity = ity} n sp =
Andrei Paskevich's avatar
Andrei Paskevich committed
548
    let t, fl = havoc kn get_rhs wr regs (t_var o) ity [] in
549
    sp_and (t_and_l (cons_t_simp (t_var n) t fl)) sp in
Andrei Paskevich's avatar
Andrei Paskevich committed
550 551
  let sp = t_subst (advancement dst) sp in
  sp_and sp (Mpv.fold update dst t_true)
Andrei Paskevich's avatar
Andrei Paskevich committed
552

Andrei Paskevich's avatar
Andrei Paskevich committed
553 554 555 556 557 558 559
let sp_havoc {known_map = kn} {eff_writes = wr; eff_covers = cv} res sp dst =
  if Sreg.is_empty cv then sp else
  let rd = vc_freepvs Spv.empty res sp in
  let dst = dst_step_back_raw cv rd Mreg.empty dst in
  if Mpv.is_empty dst then sp else
  let regs = name_regions kn cv dst in
  sp_havoc_raw kn rhs_of_effect wr sp dst regs
Andrei Paskevich's avatar
Andrei Paskevich committed
560

Andrei Paskevich's avatar
Andrei Paskevich committed
561 562 563 564 565 566 567
let dst_complete sp dst =
  let add o n sp =
    sp_and sp (t_equ (t_var n) (t_var o.pv_vs)) in
  Mpv.fold add dst sp

let eff_complete {eff_covers = cv} sp dst =
  let add o n sp =
Andrei Paskevich's avatar
Andrei Paskevich committed
568
    if pv_affected cv o then sp else
569
    sp_and sp (t_equ (t_var n) (t_var o.pv_vs)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
570
  Mpv.fold add dst sp
Andrei Paskevich's avatar
Andrei Paskevich committed
571

Andrei Paskevich's avatar
Andrei Paskevich committed
572
(* fast-related tools *)
573

574 575 576 577
let out_map fn (ok, ne, ex) = fn ok, fn ne, Mexn.map fn ex

let out_label e out = out_map (vc_label e) out

Andrei Paskevich's avatar
Andrei Paskevich committed
578
let out_complete eff (ok, ne, ex) xres dst =
579
  let join _ sp xres = match sp, xres with
Andrei Paskevich's avatar
Andrei Paskevich committed
580
    | Some sp, Some _ -> Some (eff_complete eff sp dst)
Andrei Paskevich's avatar
Andrei Paskevich committed
581
    | None, Some _ -> Some t_false | _, None -> None in
Andrei Paskevich's avatar
Andrei Paskevich committed
582
  ok, eff_complete eff ne dst, Mexn.merge join ex xres
Andrei Paskevich's avatar
Andrei Paskevich committed
583

Andrei Paskevich's avatar
Andrei Paskevich committed
584 585 586 587
let sp_adjust dst zdst =
  let adj = adjustment dst zdst in
  let dst = Mpv.set_diff zdst dst in
  fun sp -> dst_complete (t_subst adj sp) dst
Andrei Paskevich's avatar
Andrei Paskevich committed
588

589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607
let out_seq_raw (ok1, ne1, ex1) dst1 res (ok2, ne2, ex2) =
  let adv = advancement dst1 in
  let ok = wp_and ok1 (sp_wp_close res ne1 adv ok2) in
  let close sp = sp_sp_close res ne1 adv sp in
  ok, close ne2, union_mexn ex1 (Mexn.map close ex2)

let out_seq_raw out1 dst1 res = function
  | Some out2 -> out_seq_raw out1 dst1 res out2
  | None -> out1

let out_seq_pure ok1 ne1 res out2 =
  out_seq_raw (ok1, ne1, Mexn.empty) Mpv.empty res out2

let out_seq (ok1, ne1, ex1) dst1 res out2 eff2 dst2 =
  let ex1 = if Mexn.is_empty ex1 then ex1 else
    let dst2 = dst_affected eff2 dst2 in
    Mexn.map (sp_adjust dst1 dst2) ex1 in
  out_seq_raw (ok1, ne1, ex1) dst1 res out2

Andrei Paskevich's avatar
Andrei Paskevich committed
608 609
(* classical WP / fast WP *)

610
let anon_pat pp = Svs.is_empty pp.pp_pat.pat_vars
611 612 613 614 615 616

let bind_oldies c f =
  let sbs = Mpv.fold (fun {pv_vs = o} {pv_vs = v} s ->
    Mvs.add o (t_var v) s) c.cty_oldies Mvs.empty in
  t_subst sbs f

Andrei Paskevich's avatar
Andrei Paskevich committed
617
let spec_while env e invl varl =
618 619
  let init = wp_of_inv None expl_loop_init invl in
  let keep = wp_of_inv None expl_loop_keep invl in
Andrei Paskevich's avatar
Andrei Paskevich committed
620 621 622 623 624
  if varl = [] then init, Mvs.empty, keep else
  let o2n, olds = oldify_variant varl in
  let d = decrease env e.e_loc expl_loop_vari olds varl in
  init, o2n, wp_and keep d

Andrei Paskevich's avatar
Andrei Paskevich committed
625 626 627
let spec_for env _e v ({pv_vs = a}, d, {pv_vs = b}) invl =
  let a = t_var a and b = t_var b in
  let i = t_var v and one = t_nat_const 1 in
628 629
  let prev = wp_of_inv None expl_loop_init invl in
  let keep = wp_of_inv None expl_loop_keep invl in
Andrei Paskevich's avatar
Andrei Paskevich committed
630 631 632
  let gt, le, pl = match d with
    | To     -> env.ps_int_gt, env.ps_int_le, env.fs_int_pl
    | DownTo -> env.ps_int_lt, env.ps_int_ge, env.fs_int_mn in
Andrei Paskevich's avatar
Andrei Paskevich committed
633 634 635 636 637 638
  let a_gt_b = ps_app gt [a;b] and a_le_b = ps_app le [a;b] in
  let bounds = t_and (ps_app le [a;i]) (ps_app le [i;b]) in
  let init = sp_implies a_le_b (t_subst_single v a prev) in
  let keep = t_subst_single v (fs_app pl [i;one] ty_int) keep in
  let last = t_subst_single v (fs_app pl [b;one] ty_int) prev in
  a_gt_b, init, sp_and bounds prev, keep, sp_and a_le_b last
Andrei Paskevich's avatar
Andrei Paskevich committed
639

640 641 642
let rec wp_expr env e res q xq = match e.e_node with
  | _ when Slab.mem sp_label e.e_label ->
      let cv = e.e_effect.eff_covers in
643
      let xq = Mexn.set_inter xq e.e_effect.eff_raises in
Andrei Paskevich's avatar
Andrei Paskevich committed
644
      let dst = if Sreg.is_empty cv then Mpv.empty else
645
        let pvs_of_xwp _ (v,q) s = vc_freepvs s v q in
646
        let pvs = Mexn.fold pvs_of_xwp xq Spv.empty in
647
        dst_of_pvs cv (vc_freepvs pvs res q) in
648 649
      let out = Some (q, t_false, Mexn.empty) in
      let ok,_,ex = sp_expr env e res (Mexn.map fst xq) out eff_empty dst in
650 651
      let adv = if Mexn.is_empty ex then Mvs.empty else advancement dst in
      wp_inter_mexn ok (fun sp (v,q) -> sp_wp_close v sp adv q) ex xq
652 653 654 655
  | Evar v ->
      t_subst_single res (vc_label e (t_var v.pv_vs)) q
  | Econst c ->
      t_subst_single res (vc_label e (t_const c)) q
656
  | Eexec (ce, c) ->
657 658 659
      let p = wp_of_pre env e.e_loc expl_pre c.cty_pre in
      let q = wp_close e.e_loc expl_post res c.cty_post q in
      let join cq (v,q) = wp_close e.e_loc expl_xpost v cq q in
Andrei Paskevich's avatar
Andrei Paskevich committed
660
      let w = wp_inter_mexn q join (cty_xpost_real c) xq in
661
      let w = bind_oldies c (wp_havoc env c.cty_effect w) in
662
      vc_label e (wp_and (vc_cexp env true ce) (wp_and p w))
Andrei Paskevich's avatar
Andrei Paskevich committed
663 664 665 666 667 668
  | Elet (LDvar ({pv_vs = v}, e0), e1)
  | Ecase (e0, [{pp_pat = {pat_node = Pvar v}}, e1]) ->
      let q = wp_expr env e1 res q xq in
      vc_label e (wp_expr env e0 v q xq)
  | Ecase (e0, [pp, e1]) when anon_pat pp ->
      let q = wp_expr env e1 res q xq in
Andrei Paskevich's avatar
Andrei Paskevich committed
669
      vc_label e (wp_expr env e0 (proxy_of_expr e0) q xq)
670
  | Elet ((LDsym _| LDrec _) as ld, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
671
      let q = wp_expr env e1 res q xq in
Andrei Paskevich's avatar
Andrei Paskevich committed
672
      vc_label e (fst (vc_let_sym env true ld q e1))
673
  | Eif (e0, e1, e2) when eff_pure e1.e_effect && eff_pure e2.e_effect ->
Andrei Paskevich's avatar
Andrei Paskevich committed
674 675
      let v, test = test_of_expr e0 in
      let ok, ne = sp_pure_if env test e1 e2 res in
676 677
      let q = sp_wp_close res ne Mvs.empty q in
      vc_label e (wp_expr env e0 v (wp_and ok q) xq)
Andrei Paskevich's avatar
Andrei Paskevich committed
678
  | Eif (e0, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
679
      let v, test = test_of_expr e0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
680
      let q1 = wp_expr env e1 res q xq in
681
      let q2 = wp_expr env e2 res q xq in
Andrei Paskevich's avatar
Andrei Paskevich committed
682 683
      vc_label e (wp_expr env e0 v (wp_if test q1 q2) xq)
  | Ecase (e0, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
684
      let v = proxy_of_expr e0 in
685 686
      let branch ({pp_pat = pat}, e) =
        t_close_branch pat (wp_expr env e res q xq) in
Andrei Paskevich's avatar
Andrei Paskevich committed
687 688
      let q = wp_case (t_var v) (List.map branch bl) in
      vc_label e (wp_expr env e0 v q xq)
689 690 691
  | Etry (e0, bl) ->
      let branch xs (vl,e) =
        let wp = wp_expr env e res q xq in
Andrei Paskevich's avatar
Andrei Paskevich committed
692
        res_of_xbranch xs vl (fun fn -> fn) wp in
693 694
      let xq = Mexn.set_union (Mexn.mapi branch bl) xq in
      vc_label e (wp_expr env e0 res q xq)
Andrei Paskevich's avatar
Andrei Paskevich committed
695
  | Eraise (xs, e0) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
696 697
      let v, q = try Mexn.find xs xq with
        | Not_found -> proxy_of_expr e0, t_true in
Andrei Paskevich's avatar
Andrei Paskevich committed
698
      vc_label e (wp_expr env e0 v q xq)
699 700
  | Eassert (Assert, f) ->
      let q = t_subst_single res t_void q in
701
      wp_and_asym (vc_label e (vc_expl None expl_assert f)) q
702 703
  | Eassert (Assume, f) ->
      let q = t_subst_single res t_void q in
704
      sp_implies (vc_label e (vc_expl None expl_assume f)) q
705 706
  | Eassert (Check, f) ->
      let q = t_subst_single res t_void q in
707
      wp_and (vc_label e (vc_expl None expl_check f)) q
708
  | Eghost e0 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
709
      wp_expr env (e_label_copy e e0) res q xq
710 711 712 713 714
  | Epure t ->
      let t = vc_label e t in
      begin match t.t_ty with
        | Some ty when ty_equal ty ty_unit -> t_subst_single res t_void q
        | Some _ -> wp_let res t q
715
        | None -> wp_let res (t_if_simp t t_bool_true t_bool_false) q
716 717
      end
  | Eabsurd ->
718
      vc_label e (vc_expl e.e_loc expl_absurd t_false)
Andrei Paskevich's avatar
Andrei Paskevich committed
719 720
  | Eassign asl ->
      let q = t_subst_single res t_void q in
Andrei Paskevich's avatar
Andrei Paskevich committed
721 722 723 724 725
      let cv = e.e_effect.eff_covers in
      let dst = dst_of_wp cv q in
      let wr = writes_of_assign asl and kn = env.known_map in
      let regs = rename_regions (name_regions kn cv dst) cv wr in
      vc_label e (wp_havoc_raw kn rhs_of_assign wr q dst regs)
Andrei Paskevich's avatar
Andrei Paskevich committed
726
  | Ewhile (e0, invl, varl, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
727 728 729
      (* wp(while e0 inv I var V do e1 done, Q, R) =
         I and forall S. I ->
                 wp(e0, (if result then wp(e1, I /\ decr(V), R) else Q), R) *)
Andrei Paskevich's avatar
Andrei Paskevich committed
730
      let v, test = test_of_expr e0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
731
      let q = t_subst_single res t_void q in
Andrei Paskevich's avatar
Andrei Paskevich committed
732
      let init, o2n, keep = spec_while env e invl varl in
Andrei Paskevich's avatar
Andrei Paskevich committed
733
      let w = wp_if test (wp_expr env e1 res keep xq) q in
Andrei Paskevich's avatar
Andrei Paskevich committed
734 735 736
      let w = sp_implies init (wp_expr env e0 v w xq) in
      let w = wp_havoc env e.e_effect (t_subst o2n w) in
      vc_label e (wp_and init w)
Andrei Paskevich's avatar
Andrei Paskevich committed
737 738
  | Efor ({pv_vs = v}, bounds, invl, e1) ->
      (* wp(for v = a to b inv I(v) do e1 done, Q, R) =
Andrei Paskevich's avatar
Andrei Paskevich committed
739
             a > b  -> Q
Andrei Paskevich's avatar
Andrei Paskevich committed
740 741 742
         and a <= b -> I(a)
         and forall S. forall v. a <= v <= b /\ I(v) -> wp(e1, I(v+1), R)
                   and a <= b /\ I(b+1) -> Q *)
Andrei Paskevich's avatar
Andrei Paskevich committed
743
      let q = t_subst_single res t_void q in
Andrei Paskevich's avatar
Andrei Paskevich committed
744 745
      let a_gt_b, init, prev, keep, last = spec_for env e v bounds invl in
      let w = wp_forall [v] (sp_implies prev (wp_expr env e1 res keep xq)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
746
      let w = wp_havoc env e.e_effect (wp_and w (sp_implies last q)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
747
      vc_label e (wp_and (sp_implies a_gt_b q) (wp_and init w))
748

749
and sp_expr env e res xres zout zeff zdst = match e.e_node with
750 751
  | Evar v ->
      let t = vc_label e (t_var v.pv_vs) in
752
      out_seq_pure t_true (t_equ (t_var res) t) res zout
753 754
  | Econst c ->
      let t = vc_label e (t_const c) in
755
      out_seq_pure t_true (t_equ (t_var res) t) res zout
756
  | Eexec (ce, c) ->
757
      let dst = dst_step_back e.e_effect zeff zdst in
Andrei Paskevich's avatar
Andrei Paskevich committed
758 759
      let ok = wp_of_pre env e.e_loc expl_pre c.cty_pre in
      let ok = wp_and (vc_cexp env false ce) ok in
760
      let sp_of_post lab v ql =
761
        let cq = sp_of_post e.e_loc lab v ql in
Andrei Paskevich's avatar
Andrei Paskevich committed
762
        let sp = sp_havoc env e.e_effect v cq dst in
763
        bind_oldies c sp in
764 765
      let ne = sp_of_post expl_post res c.cty_post in
      let join v ql = sp_of_post expl_xpost v ql in
Andrei Paskevich's avatar
Andrei Paskevich committed
766
      let ex = inter_mexn join xres (cty_xpost_real c) in
767
      out_seq (out_label e (ok, ne, ex)) dst res zout zeff zdst
768 769
  | Elet (LDvar ({pv_vs = v}, e0), e1)
  | Ecase (e0, [{pp_pat = {pat_node = Pvar v}}, e1]) ->
770 771 772 773
      let out = sp_expr env e1 res xres zout zeff zdst in
      let eff = eff_bind_single (restore_pv v) e1.e_effect in
      out_label e (sp_expr_seq env e0 v xres out eff zeff zdst)
  | Ecase (e0, [pp, ({e_effect = eff} as e1)]) when anon_pat pp ->
Andrei Paskevich's avatar
Andrei Paskevich committed
774
      let v = proxy_of_expr e0 in
775 776
      let out = sp_expr env e1 res xres zout zeff zdst in
      out_label e (sp_expr_seq env e0 v xres out eff zeff zdst)
777
  | Elet ((LDsym _| LDrec _) as ld, e1) ->
778
      let ok, ne, ex = sp_expr env e1 res xres zout zeff zdst in
Andrei Paskevich's avatar
Andrei Paskevich committed
779 780
      let ok, close = vc_let_sym env false ld ok e1 in
      out_label e (ok, close ne, Mexn.map close ex)
781
  | Eif (e0, e1, e2) when eff_pure e1.e_effect && eff_pure e2.e_effect ->
Andrei Paskevich's avatar
Andrei Paskevich committed
782 783
      let v, test = test_of_expr e0 in
      let ok, ne = sp_pure_if env test e1 e2 res in
784
      let out = out_seq_pure ok ne res zout in
Andrei Paskevich's avatar
Andrei Paskevich committed
785
      let eff12 = eff_union_par e1.e_effect e2.e_effect in
786
      out_label e (sp_expr_seq env e0 v xres out eff12 zeff zdst)
Andrei Paskevich's avatar
Andrei Paskevich committed
787
  | Eif (e0, e1, e2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
788 789
      let eff12 = eff_union_par e1.e_effect e2.e_effect in
      let xres12 = Mexn.set_inter xres eff12.eff_raises in
790 791 792
      let dst12 = dst_step_back eff12 zeff zdst in
      let out1 = sp_expr_nil env e1 res xres12 dst12 in
      let out2 = sp_expr_nil env e2 res xres12 dst12 in
Andrei Paskevich's avatar
Andrei Paskevich committed
793 794 795
      let ok1, ne1, ex1 = out_complete e1.e_effect out1 xres12 dst12 in
      let ok2, ne2, ex2 = out_complete e2.e_effect out2 xres12 dst12 in
      let v, test = test_of_expr e0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
796 797
      let ok = wp_if test ok1 ok2 in
      let ne = t_if_simp test ne1 ne2 in
Andrei Paskevich's avatar
Andrei Paskevich committed
798
      let ex = inter_mexn (t_if_simp test) ex1 ex2 in
799 800
      let out = out_seq (ok, ne, ex) dst12 res zout zeff zdst in
      out_label e (sp_expr_seq env e0 v xres out eff12 zeff zdst)
Andrei Paskevich's avatar
Andrei Paskevich committed
801
  | Ecase (e0, bl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
802
      let eff12 = List.fold_left (fun acc (p,e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
803
        let pvs = pvs_of_vss Spv.empty p.pp_pat.pat_vars in
Andrei Paskevich's avatar
Andrei Paskevich committed
804
        let eff = eff_bind pvs e1.e_effect in
Andrei Paskevich's avatar
Andrei Paskevich committed
805
        eff_union_par acc eff) eff_empty bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
806
      let xres12 = Mexn.set_inter xres eff12.eff_raises in
807
      let dst12 = dst_step_back eff12 zeff zdst in
Andrei Paskevich's avatar
Andrei Paskevich committed
808
      let out12 = List.map (fun ({pp_pat = p}, e1) ->
809
        let out = sp_expr_nil env e1 res xres12 dst12 in
Andrei Paskevich's avatar
Andrei Paskevich committed
810
        let out = out_complete e1.e_effect out xres12 dst12 in
Andrei Paskevich's avatar
Andrei Paskevich committed
811
        out_map (t_close_branch p) out) bl in
Andrei Paskevich's avatar
Andrei Paskevich committed
812 813 814 815
      let v = proxy_of_expr e0 in let t = t_var v in
      let ok = wp_case t (List.map (fun (ok,_,_) -> ok) out12) in
      let ne = t_case_simp t (List.map (fun (_,ne,_) -> ne) out12) in
      let xbl = Mexn.map (fun _ -> []) xres12 in
Andrei Paskevich's avatar
Andrei Paskevich committed
816
      let xbl = List.fold_right (fun (_,_,ex) xbl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
817
        inter_mexn (fun x l -> x::l) ex xbl) out12 xbl in
Andrei Paskevich's avatar
Andrei Paskevich committed
818
      let ex = Mexn.map (t_case_simp t) xbl in
819 820
      let out = out_seq (ok, ne, ex) dst12 res zout zeff zdst in
      out_label e (sp_expr_seq env e0 v xres out eff12 zeff zdst)
Andrei Paskevich's avatar
Andrei Paskevich committed
821
  | Etry (e0, xl) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
822 823
      let eff12 = Mexn.fold (fun _ (vl,e1) acc ->
        let eff = eff_bind (Spv.of_list vl) e1.e_effect in
824
        eff_union_par acc eff) xl eff_empty in
Andrei Paskevich's avatar
Andrei Paskevich committed
825
      let xres12 = Mexn.set_inter xres eff12.eff_raises in
826
      let dst = dst_step_back e.e_effect zeff zdst in
Andrei Paskevich's avatar
Andrei Paskevich committed
827 828
      let dst12 = dst_affected eff12 dst in
      let out12 = Mexn.mapi (fun xs (vl,e1) ->
829
        let out = sp_expr_nil env e1 res xres12 dst12 in
Andrei Paskevich's avatar
Andrei Paskevich committed
830
        let out = out_complete e1.e_effect out xres12 dst12 in
831
        res_of_xbranch xs vl out_map out) xl in
Andrei Paskevich's avatar
Andrei Paskevich committed
832 833
      let xres = Mexn.set_union (Mexn.map fst out12) xres in
      let dst0 = dst_step_back e0.e_effect eff12 dst in
834
      let ok, ne, ex = sp_expr_nil env e0 res xres dst0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
835
      let adv = advancement dst0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
836
      let join sp (v,(ok,_,_)) = sp_wp_close v sp adv ok in
Andrei Paskevich's avatar
Andrei Paskevich committed
837 838
      let ok = wp_inter_mexn ok join ex out12 in
      let adjust = sp_adjust dst0 dst12 in
Andrei Paskevich's avatar
Andrei Paskevich committed
839
      let join sp (v,(_,ne,_)) = sp_sp_close v sp adv ne in
Andrei Paskevich's avatar
Andrei Paskevich committed
840
      let ne = sp_inter_mexn (adjust ne) join ex out12 in
Andrei Paskevich's avatar
Andrei Paskevich committed
841
      let join sp (v,(_,_,ex)) = Mexn.map (sp_sp_close v sp adv) ex in
Andrei Paskevich's avatar
Andrei Paskevich committed
842
      let ex = Mexn.fold (fun _ x1 x2 -> union_mexn x2 x1)
Andrei Paskevich's avatar
Andrei Paskevich committed
843 844
        (inter_mexn join ex out12)
        (Mexn.map adjust (Mexn.set_diff ex out12)) in
845
      out_seq (out_label e (ok, ne, ex)) dst res zout zeff zdst
Andrei Paskevich's avatar
Andrei Paskevich committed
846
  | Eraise (xs, e0) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
847 848
      let v = try Mexn.find xs xres with
        | Not_found -> proxy_of_expr e0 in
849 850
      let dst = dst_affected e.e_effect zdst in
      let ok, ne, ex = sp_expr_nil env e0 v xres dst in
Andrei Paskevich's avatar
Andrei Paskevich committed
851
      let ex = union_mexn ex (Mexn.singleton xs ne) in
852 853
      let dst = Mpv.set_diff (dst_affected zeff zdst) dst in
      let ex = Mexn.map (fun sp -> dst_complete sp dst) ex in
Andrei Paskevich's avatar
Andrei Paskevich committed
854
      out_label e (ok, t_false, ex)
855
  | Eassert (Assert, f) ->
856
      let ok = vc_label e (vc_expl None expl_assert f) in
857
      out_seq_pure ok ok res zout
858
  | Eassert (Assume, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
859
      let ne = vc_label e (vc_expl None expl_assume f) in
860
      out_seq_pure t_true ne res zout
861
  | Eassert (Check, f) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
862
      let ok = vc_label e (vc_expl None expl_check f) in
863
      out_seq_pure ok t_true res zout
864
  | Eghost e0 ->
865
      sp_expr env (e_label_copy e e0) res xres zout zeff zdst
866 867 868 869 870
  | Epure t ->
      let t = vc_label e t in
      let ne = match t.t_ty with
        | Some ty when ty_equal ty ty_unit -> t_true
        | Some _ -> t_equ (t_var res) t
871
        | None -> t_equ (t_var res) (t_if_simp t t_bool_true t_bool_false) in
872
      out_seq_pure t_true ne res zout
873
  | Eabsurd ->
874
      let ok = vc_label e (vc_expl e.e_loc expl_absurd t_false) in
875
      ok, ok, Mexn.empty
Andrei Paskevich's avatar
Andrei Paskevich committed
876
  | Eassign asl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
877
      let cv = e.e_effect.eff_covers in
878
      let dst = dst_step_back e.e_effect zeff zdst in
Andrei Paskevich's avatar
Andrei Paskevich committed
879 880 881
      let wr = writes_of_assign asl and kn = env.known_map in
      let regs = rename_regions (name_regions kn cv dst) cv wr in
      let sp = sp_havoc_raw kn rhs_of_assign wr t_true dst regs in
882
      out_seq_raw (t_true, vc_label e sp, Mexn.empty) dst res zout
Andrei Paskevich's avatar
Andrei Paskevich committed
883
  | Ewhile (e0, invl, varl, e1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
884 885 886
      (* ok: I /\ !! I -> (ok0 /\ (ne0 ->  test -> ok1 /\ (ne1 -> I /\ V)))
         ne:      !! I /\         (ne0 /\ !test)
         ex:      !! I /\ (ex0 \/ (ne0 /\  test /\ ex1)) *)
Andrei Paskevich's avatar
Andrei Paskevich committed
887
      let v, test = test_of_expr e0 in
Andrei Paskevich's avatar
Andrei Paskevich committed
888
      let init, o2n, keep = spec_while env e invl varl in
Andrei Paskevich's avatar
Andrei Paskevich committed
889
      let out = keep, t_false, Mexn.empty in
890
      let dst = dst_step_back e.e_effect zeff zdst in
Andrei Paskevich's avatar
Andrei Paskevich committed
891
      let eff = eff_read (t_freepvs Spv.empty keep) in
Andrei Paskevich's avatar
Andrei Paskevich committed
892
      let dst1 = dst_step_back e1.e_effect eff dst in
Andrei Paskevich's avatar
Andrei Paskevich committed
893
      let ne = dst_complete (t_not test) dst1 in
894
      let ok, _, ex = sp_expr env e1 res xres (Some out) eff dst in
Andrei Paskevich's avatar
Andrei Paskevich committed
895
      let out = sp_implies test ok, ne, Mexn.map (sp_and test) ex in
896
      let ok, ne, ex = sp_expr_seq env e0 v xres out e1.e_effect eff dst in
Andrei Paskevich's avatar
Andrei Paskevich committed
897 898 899 900 901
      let src = dst_step_back e.e_effect e.e_effect dst in
      let hav = sp_havoc env e.e_effect res init src in
      let adv = advancement src in
      let ne = sp_sp_close res hav adv ne in
      let ex = Mexn.map (sp_sp_close res hav adv) ex in