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

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

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

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

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
32
let case_split = Ident.create_label "case_split"
Andrei Paskevich's avatar
Andrei Paskevich committed
33
let add_case t = t_label_add case_split t
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
34

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

Andrei Paskevich's avatar
Andrei Paskevich committed
37
38
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
39

40
let pv_is_unit v = ity_equal v.pv_ity ity_unit
41

42
43
44
45
46
47
48
let pv_of_ity s ity = create_pvsymbol (id_fresh s) ity

let res_of_post ity = function
  | q::_ -> create_pvsymbol (clone_post_result q) ity
  | _ -> pv_of_ity "result" ity

let res_of_cty cty = res_of_post cty.cty_result cty.cty_post
Andrei Paskevich's avatar
Andrei Paskevich committed
49

Andrei Paskevich's avatar
Andrei Paskevich committed
50
51
52
let proxy_of_expr =
  let label = Slab.singleton proxy_label in fun e ->
  let id = id_fresh ?loc:e.e_loc ~label "o" in
53
  create_pvsymbol id e.e_ity
54

55
56
let sp_label = Ident.create_label "vc:sp"
let wp_label = Ident.create_label "vc:wp"
57
let lf_label = Ident.create_label "vc:liberal_for"
58

59
60
let vc_labels = Slab.add lf_label
  (Slab.add sp_label (Slab.add wp_label Slab.empty))
61

62
63
64
65
66
67
68
69
70
71
(* VCgen environment *)

type vc_env = {
  known_map : Pdecl.known_map;
  ps_int_le : lsymbol;
  ps_int_ge : lsymbol;
  ps_int_lt : lsymbol;
  ps_int_gt : lsymbol;
  fs_int_pl : lsymbol;
  fs_int_mn : lsymbol;
72
  exn_count : int ref;
73
74
75
76
77
78
79
80
81
82
}

let mk_env {Theory.th_export = ns} kn = {
  known_map = kn;
  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 -"];
83
  exn_count = ref 0;
84
}
Andrei Paskevich's avatar
Andrei Paskevich committed
85

86
87
88
(* every exception-catching clause is represented by
   a unique integer, so that we can move code inside
   try-with expressions without capturing exceptions *)
89
90
91
92
93
let new_exn env = incr env.exn_count; !(env.exn_count)

(* FIXME: cannot verify int.why because of a cyclic dependency.
   int.Int is used for the "for" loops and for integer variants.
   We should be able to extract the necessary lsymbols from kn. *)
94
let mk_env env kn = mk_env (Env.read_theory env ["int"] "Int") kn
Andrei Paskevich's avatar
Andrei Paskevich committed
95

96
(* explanation labels *)
Andrei Paskevich's avatar
Andrei Paskevich committed
97

Andrei Paskevich's avatar
Andrei Paskevich committed
98
let expl_pre       = Ident.create_label "expl:precondition"
99
100
let expl_post      = Ident.create_label "expl:postcondition"
let expl_xpost     = Ident.create_label "expl:exceptional postcondition"
101
102
103
104
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"
105
let expl_for_bound = Ident.create_label "expl:loop bounds"
Andrei Paskevich's avatar
Andrei Paskevich committed
106
107
108
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"
109
let expl_variant   = Ident.create_label "expl:variant decrease"
Andrei Paskevich's avatar
Andrei Paskevich committed
110
let _expl_type_inv  = Ident.create_label "expl:type invariant"
Andrei Paskevich's avatar
Andrei Paskevich committed
111

112
113
let lab_has_expl lab =
  Slab.exists (fun l -> Strings.has_prefix "expl:" l.lab_string) lab
Andrei Paskevich's avatar
Andrei Paskevich committed
114

115
116
117
118
let vc_expl loc lab expl f =
  let lab = Slab.add stop_split (Slab.union lab f.t_label) in
  let lab = if lab_has_expl lab then lab else Slab.add expl lab in
  t_label ?loc:(if loc = None then f.t_loc else loc) lab f
Andrei Paskevich's avatar
Andrei Paskevich committed
119

120
121
122
123
124
125
(* 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

126
let sp_or sp1 sp2 = match sp1.t_node, sp2.t_node with
127
128
  | Ttrue, _ | _, Tfalse -> sp1
  | _, Ttrue | Tfalse, _ -> sp2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
129
  | _, _ -> add_case (t_or sp1 sp2)
130

131
let sp_and sp1 sp2 = match sp1.t_node, sp2.t_node with
132
133
134
135
  | Ttrue, _ | _, Tfalse -> sp2
  | _, Ttrue | Tfalse, _ -> sp1
  | _, _ -> t_and sp1 sp2

Andrei Paskevich's avatar
Andrei Paskevich committed
136
(* sp_or adds "case_split", so we avoid using it here *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
137
let sp_if c sp1 sp2 = match c.t_node, sp1.t_node, sp2.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
138
139
  | Ttrue, _, _  | _, Ttrue,  Ttrue  -> sp1
  | Tfalse, _, _ | _, Tfalse, Tfalse -> sp2
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
140
  | _, _, Tfalse -> sp_and c sp1
Andrei Paskevich's avatar
Andrei Paskevich committed
141
142
143
  | _, Tfalse, _ -> sp_and (t_not_simp c) sp2
  | _, Ttrue, _  -> t_or c sp2
  | _, _, Ttrue  -> t_or (t_not_simp c) sp1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
144
145
146
147
148
149
150
  | _, _, _ -> add_case (t_if c sp1 sp2)

let sp_case t bl =
  let isfalse b = match t_open_branch b with
    | _, { t_node = Tfalse } -> true | _ -> false in
  if List.for_all isfalse bl then t_false else add_case (t_case t bl)

Andrei Paskevich's avatar
Andrei Paskevich committed
151
152
153
let can_simp wp = match wp.t_node with
  | Ttrue -> not (Slab.mem stop_split wp.t_label)
  | _ -> false
154
155
156
157
158
159

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

160
161
162
163
164
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
165
let wp_if c wp1 wp2 = match c.t_node, wp1.t_node, wp2.t_node with
166
167
  | Ttrue, _, _  when can_simp wp2 -> wp1
  | Tfalse, _, _ when can_simp wp1 -> wp2
168
  | _, _, Ttrue  when can_simp wp2 -> sp_implies c wp1
Andrei Paskevich's avatar
Andrei Paskevich committed
169
  | _, Ttrue, _  when can_simp wp1 -> sp_implies (t_not_simp c) wp2
170
171
  | _, _, _ -> t_if c wp1 wp2

Andrei Paskevich's avatar
Andrei Paskevich committed
172
173
174
175
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

176
let wp_forall vl wp = t_forall_close_simp vl [] wp
177
let sp_exists vl sp = t_exists_close_simp vl [] sp
178

Andrei Paskevich's avatar
Andrei Paskevich committed
179
180
181
182
183
184
185
186
let wp_let v t wp =
  if pv_is_unit v then t_subst_single v.pv_vs t_void wp
                  else t_let_close_simp v.pv_vs t wp

let sp_let v t sp rd =
  if pv_is_unit v then t_subst_single v.pv_vs t_void sp else
  if Spv.mem v rd then sp_and (t_equ (t_var v.pv_vs) t) sp else
  t_let_close_simp v.pv_vs t sp
187

188
(* variant decrease preconditions *)
189
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

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

216
let decrease env loc lab expl olds news =
217
218
219
220
221
222
223
224
225
226
227
228
  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
229
  vc_expl loc lab expl (decr olds news)
Andrei Paskevich's avatar
Andrei Paskevich committed
230

231
232
233
let old_of_pv {pv_vs = v; pv_ity = ity} =
  create_pvsymbol (id_clone v.vs_name) (ity_purify ity)

Andrei Paskevich's avatar
Andrei Paskevich committed
234
235
236
237
let oldify_variant varl =
  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
238
  if Mpv.is_empty fpv then Mpv.empty, varl else
239
240
  let o2v = Mpv.fold (fun v o s -> Mpv.add o v s) fpv Mpv.empty in
  let v2o = Mpv.fold (fun v o s ->
Andrei Paskevich's avatar
Andrei Paskevich committed
241
    Mvs.add v.pv_vs (t_var o.pv_vs) s) fpv Mvs.empty in
242
243
244
245
246
247
  o2v, List.map (fun (t,r) -> t_subst v2o t, r) varl

let renew_oldies o2v =
  let renew o v (n2v, o2n) = let n = old_of_pv v in
    Mpv.add n v n2v, Mvs.add o.pv_vs (t_var n.pv_vs) o2n in
  Mpv.fold renew o2v (Mpv.empty, Mvs.empty)
248

249
(* convert user specifications into goals (wp) and premises (sp) *)
Andrei Paskevich's avatar
Andrei Paskevich committed
250

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

254
let wp_of_pre loc lab pl = wp_of_inv loc lab expl_pre pl
Andrei Paskevich's avatar
Andrei Paskevich committed
255

256
let wp_of_post expl ity ql =
257
  let v = res_of_post ity ql in let t = t_var v.pv_vs in
258
259
  let make q = vc_expl None Slab.empty expl (open_post_with t q) in
  v, t_and_l (List.map make ql)
Andrei Paskevich's avatar
Andrei Paskevich committed
260

261
262
263
264
265
266
let push_stop loc lab expl f =
  let rec push f = match f.t_node with
    | Tbinop (Tand,g,h) when not (Slab.mem stop_split f.t_label) ->
        t_label_copy f (t_and (push g) (push h))
    | _ -> vc_expl loc lab expl f in
  push f
Andrei Paskevich's avatar
Andrei Paskevich committed
267

268
269
270
let sp_of_inv loc lab expl pl =
  t_and_l (List.map (push_stop loc lab expl) pl)

271
let sp_of_pre pl = sp_of_inv None Slab.empty expl_pre pl
272
273
274
275
276

let sp_of_post loc lab expl v ql = let t = t_var v.pv_vs in
  let push q = push_stop loc lab expl (open_post_with t q) in
  t_and_l (List.map push ql)

277
278
279
280
(* definitions of local let-functions are inserted in the VC
   as premises for the subsequent code (in the same way as
   definitions of top-level let-functions are translated to
   logical definitions in Pdecl.create_let_decl) *)
281
282
let cty_enrich_post c = match c with
  | {c_node = Cfun e; c_cty = cty} ->
283
284
      let {pv_vs = u} = res_of_cty cty in
      let prop = ty_equal u.vs_ty ty_bool in
285
      begin match term_of_expr ~prop e with
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
      | Some f ->
          let f = match f.t_node with
            | Tapp (ps, [t; {t_node = Tapp (fs,[])}])
              when ls_equal ps ps_equ
                && ls_equal fs fs_bool_true -> t
            | _ -> f in
          let q = match f.t_ty with
            | None -> t_iff (t_equ (t_var u) t_bool_true) f
            | Some _ -> t_equ (t_var u) f in
          cty_add_post cty [create_post u q]
      | None when cty.cty_post = [] ->
          begin match post_of_expr (t_var u) e with
          | Some f -> cty_add_post cty [create_post u f]
          | None -> cty end
      | None -> cty end
301
302
  | _ -> c.c_cty

303
(* k-expressions: simplified code *)
304
305
306
307

type ktag = WP | SP | Push of bool

type kode =
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
  | Kseq   of kode * int * kode           (* 0: sequence, N: try-with *)
  | Kpar   of kode * kode                 (* non-deterministic choice *)
  | Kif    of pvsymbol * kode * kode          (* deterministic choice *)
  | Kcase  of pvsymbol * (pattern * kode) list    (* pattern matching *)
  | Khavoc of pvsymbol option Mpv.t Mreg.t  (* writes and assignments *)
  | Klet   of pvsymbol * term * term         (* let v = t such that f *)
  | Kval   of pvsymbol list * term        (* let vl = any such that f *)
  | Kcut   of term                        (* assert: check and assume *)
  | Kstop  of term                        (* check and halt execution *)
  | Kcont  of int                                (* 0: skip, N: raise *)
  | Kaxiom of kode                  (* axiom-functions: assume the VC *)
  | Ktag   of ktag * kode          (* switch VCgen or mark to push up *)

(* kode requires, and expr provides, the following invariants:
   - a used variable must be defined by Klet or declared by Kval
     on every codepath leading to its use, and only once
   - in Klet(v,t,_), variable v does not occur in term t
   - every visible variable is a pvsymbol *)
326
327

let rec k_print fmt k = match k with
Andrei Paskevich's avatar
Andrei Paskevich committed
328
  | Kseq (k1 ,0, k2) -> Format.fprintf fmt
329
      "@[%a;@\n%a@]" k_print k1 k_print k2
Andrei Paskevich's avatar
Andrei Paskevich committed
330
  | Kseq (k1, i, k2) -> Format.fprintf fmt
331
      "@[TRY %a@\n%d : %a@]" k_print k1 i k_print k2
Andrei Paskevich's avatar
Andrei Paskevich committed
332
  | Kpar (Kstop f, k2) -> Format.fprintf fmt
333
      "@[@[<hov 4>CHECK %a@];@\n%a@]" Pretty.print_term f k_print k2
Andrei Paskevich's avatar
Andrei Paskevich committed
334
  | Kpar (k1, k2) -> Format.fprintf fmt
335
336
337
338
339
340
341
      "@[[ @[%a@]@\n| @[%a@] ]@]" k_print k1 k_print k2
  | Kif (v, k1, k2) -> Format.fprintf fmt
      "@[IF %a@\nTHEN %a@\nELSE %a@]"
        Ity.print_pv v k_print k1 k_print k2
  | Kcase (v, bl) ->
      let branch fmt (p,k) = Format.fprintf fmt
        "@[<hov 4>| %a ->@ %a@]" Pretty.print_pat p k_print k in
Andrei Paskevich's avatar
Andrei Paskevich committed
342
      Format.fprintf fmt "@[CASE %a\n@[%a@]@]"
343
        Ity.print_pv v (Pp.print_list Pp.newline branch) bl
Andrei Paskevich's avatar
Andrei Paskevich committed
344
345
  | Khavoc _wr -> Format.fprintf fmt "HAVOC" (* TODO *)
  | Klet (v, t, {t_node = Ttrue}) -> Format.fprintf fmt
346
347
      "@[<hov 4>LET %a = %a@]" Ity.print_pv v Pretty.print_term t
  | Klet (v,t,f) -> Format.fprintf fmt
Andrei Paskevich's avatar
Andrei Paskevich committed
348
      "@[<hov 4>LET %a = %a WITH@ %a@]" Ity.print_pv v
349
350
351
352
        Pretty.print_term t Pretty.print_term f
  | Kval (vl,{t_node = Ttrue}) -> Format.fprintf fmt
      "@[<hov 4>VAL %a@]" (Pp.print_list Pp.space Ity.print_pv) vl
  | Kval (vl,f) -> Format.fprintf fmt
Andrei Paskevich's avatar
Andrei Paskevich committed
353
      "@[<hov 4>VAL %a WITH@ %a@]"
354
355
356
357
        (Pp.print_list Pp.space Ity.print_pv) vl Pretty.print_term f
  | Kcut f -> Format.fprintf fmt
      "@[<hov 4>ASSERT %a@]" Pretty.print_term f
  | Kstop f -> Format.fprintf fmt
Andrei Paskevich's avatar
Andrei Paskevich committed
358
359
360
361
362
      "@[<hov 4>STOP %a@]" Pretty.print_term f
  | Kcont 0 -> Format.fprintf fmt
      "SKIP"
  | Kcont i -> Format.fprintf fmt
      "RAISE %d" i
363
  | Kaxiom k -> Format.fprintf fmt
Andrei Paskevich's avatar
Andrei Paskevich committed
364
      "@[<hov 4>AXIOM %a@]" k_print k
365
  | Ktag (tag, k) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
366
367
368
369
      let s = match tag with
        | WP -> "WP" | SP -> "SP"
        | Push true -> "PUSH CLOSED"
        | Push false -> "PUSH OPEN" in
370
371
      Format.fprintf fmt "@[<hov 4>%s %a@]" s k_print k

372
373
374
375
(* check if a pure k-expression can be converted to a term.
   We need this for simple conjuctions, disjuctions, and
   pattern-matching exprs, to avoid considering each branch
   separately; also to have a single substitutable term. *)
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
let term_of_kode res k =
  let rec get_stack st k = match k with
    | Klet (v, t, f) when pv_equal v res -> st, Some (t, f), 0, Kcont 0
    | Klet (v, t, _) -> (v, Some t) :: st, None, 0, k
    | Kval (vl, _) ->
        let none v = if pv_is_unit v then Some t_void else None in
        List.fold_left (fun st v -> (v, none v) :: st) st vl, None, 0, k
    | Kcut _ | Kaxiom _ -> st, None, 0, k
    | Kcont i -> st, None, i, k
    | Kseq (k1, i, k2) ->
        let st, d, j, k1 = get_stack st k1 in
        if i <> j then st, d, j, Kseq (k1, i, k2) else
        if d <> None then raise Exit else
        let st, d, j, k2 = get_stack st k2 in
        st, d, j, Kseq (k1, i, k2)
    | Ktag (tag, k2) ->
        let st, d, i, k2 = get_stack st k2 in st, d, i, Ktag (tag, k2)
    | Kpar ((Kstop _) as k1, k2) ->
        let st, d, i, k2 = get_stack st k2 in st, d, i, Kpar (k1, k2)
    | Kpar _ | Kif _ | Kcase _ | Khavoc _ | Kstop _ -> raise Exit in
  let st, d, i, k = get_stack [] k in
  if i <> 0 then raise Exit else
  match d with
  | Some (t, f) ->
      let unwind t ({pv_vs = v}, d) = match d with
        | Some d -> t_let_close_simp v d t
        | None when t_v_occurs v t > 0 -> raise Exit
        | None -> t in
      let t = List.fold_left unwind t st in
      let f = if t_closed f then f else
              List.fold_left unwind f st in
      t, f, k
  | None -> raise Exit

410
411
(* stage 1: expr -> kode *)

412
413
414
415
let k_unit res = Kval ([res], t_true)

let bind_oldies o2v k = Mpv.fold (fun o v k ->
  Kseq (Klet (o, t_var v.pv_vs, t_true), 0, k)) o2v k
416
417
418
419
420
421

let k_havoc eff k =
  if Sreg.is_empty eff.eff_covers then k else
  let conv wr = Mpv.map (fun () -> None) wr in
  Kseq (Khavoc (Mreg.map conv eff.eff_writes), 0, k)

422
423
424
(* missing exceptional postconditions are set to True,
   unless we skip them altogether and let the exception
   escape into the outer code (only for abstract blocks) *)
425
426
427
428
let complete_xpost cty {eff_raises = xss} skip =
  Mexn.set_union (Mexn.set_inter cty.cty_xpost xss)
    (Mexn.map (fun () -> []) (Mexn.set_diff xss skip))

429
430
431
432
433
434
(* translate the expression [e] into a k-expression:
   [lps] stores the variants of outer recursive functions
   [res] names the result of the normal execution of [e]
   [xmap] maps every raised exception to a pair [i,xres]:
   - [i] is a positive int assigned at the catching site
   - [xres] names the value carried by the exception *)
435
let rec k_expr env lps ({e_loc = loc} as e) res xmap =
436
  let lab = Slab.diff e.e_label vc_labels in
437
  let t_lab t = t_label ?loc lab t in
438
439
440
441
442
443
444
445
446
  let var_or_proxy e k = match e.e_node with
    | Evar v -> k v
    | _ -> let v = proxy_of_expr e in
        Kseq (k_expr env lps e v xmap, 0, k v) in
  let k = match e.e_node with
    | Evar v ->
        Klet (res, t_lab (t_var v.pv_vs), t_true)
    | Econst c ->
        Klet (res, t_lab (t_const c), t_true)
447
448
449
450
    | Eexec (ce, ({cty_pre = pre; cty_oldies = oldies} as cty)) ->
        (* [ VC(ce) (if ce is a lambda executed in-place)
           | STOP pre
           | HAVOC ; [ ASSUME post | ASSUME xpost ; RAISE ] ] *)
451
        let p, (oldies, sbs) = match pre with
452
453
          (* for recursive calls, compute the 'variant decrease'
             precondition and rename the oldies to avoid clash *)
454
455
456
457
458
459
460
461
462
463
464
465
466
          | {t_node = Tapp (ls, tl)} :: pl when Mls.mem ls lps ->
              let ovl, rll = Mls.find ls lps in
              let nvl = List.combine tl rll in
              let d = decrease env loc lab expl_variant ovl nvl in
              wp_and d (wp_of_pre loc lab pl), renew_oldies oldies
          | pl -> wp_of_pre loc lab pl, (oldies, Mvs.empty) in
        let k_of_post expl v ql =
          let sp = sp_of_post loc lab expl v ql in
          let sp = t_subst sbs sp (* rename oldies *) in
          match term_of_post ~prop:false v.pv_vs sp with
          | Some (t, sp) -> Klet (v, t_lab t, sp)
          | None -> Kval ([v], sp) in
        let k = k_of_post expl_post res cty.cty_post in
467
468
469
470
471
        (* in abstract blocks, exceptions without postconditions
           escape from the block into the outer code. Otherwise,
           every exception in eff_raises is an alternative block
           with the xpost assumed and the exception raised. *)
        let skip = match ce.c_node with
472
473
          | Cfun _ -> xmap | _ -> Mexn.empty in
        let xq = complete_xpost cty e.e_effect skip in
474
475
476
        let k = Mexn.fold2_inter (fun _ ql (i,v) k ->
          let xk = k_of_post expl_xpost v ql in
          Kpar(k, Kseq (xk, 0, Kcont i))) xq xmap k in
477
        (* oldies and havoc are common for all outcomes *)
478
479
        let k = bind_oldies oldies (k_havoc e.e_effect k) in
        let k = if pre = [] then k else Kpar (Kstop p, k) in
480
481
        begin match ce.c_node with
          | Cfun e -> Kpar (k_fun env lps ~xmap ce.c_cty e, k)
482
483
484
485
486
487
488
489
490
491
492
493
494
          | _ -> k end
    | Eassign asl ->
        let cv = e.e_effect.eff_covers in
        if Sreg.is_empty cv then k_unit res else
        (* compute the write effect *)
        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
        let wr = List.fold_left add Mreg.empty asl in
495
        (* we compute the same region bijection as in eff_assign,
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
           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 =
          List.fold_left2 link (Mreg.add rt rf t2f)
            (reg_rexp rf Mpv.empty) (reg_rexp rt wfs)
        and link t2f rf rt =
          stitch t2f rf rt (Mreg.find_def Mpv.empty rt wr) in
        (* renaming of regions "dst-to-src" under the surviving regions *)
        let add_write r wfs t2f = stitch t2f r r wfs in
        let t2f = Mreg.fold add_write (Mreg.set_inter wr cv) Mreg.empty in
        (* rearrange the write effect according to the renaming *)
        let add_write r wfs acc =
          try Mreg.add (Mreg.find r t2f) (Mpv.map (fun v -> Some v) wfs) acc
          with Not_found -> acc in
        Kseq (Khavoc (Mreg.fold add_write wr Mreg.empty), 0, k_unit res)
    | Elet (LDvar (v, e0), e1) ->
        let k = k_expr env lps e1 res xmap in
        Kseq (k_expr env lps e0 v xmap, 0, k)
    | Ecase (e0, [{pp_pat = {pat_node = Pvar v}}, e1]) ->
        let k = k_expr env lps e1 res xmap in
        Kseq (k_expr env lps e0 (restore_pv v) xmap, 0, k)
    | Ecase (e0, [pp, e1]) when Svs.is_empty pp.pp_pat.pat_vars ->
        let k = k_expr env lps e1 res xmap in
        Kseq (k_expr env lps e0 (proxy_of_expr e0) xmap, 0, k)
    | Elet ((LDsym _| LDrec _) as ld, e1) ->
        let k = k_expr env lps e1 res xmap in
        (* when we havoc the VC of a locally defined function,
529
530
531
           we must take into account every write in the following
           expression and ignore the resets, because the function
           may be executed before the resets. *)
532
533
534
535
        let eff = eff_write e1.e_effect.eff_reads
                            e1.e_effect.eff_writes in
        (* postcondition, as in [Pdecl.create_let_decl] *)
        let add_axiom cty q k = if can_simp q then k else
536
          let p = Kval (cty.cty_args, sp_of_pre cty.cty_pre) in
537
538
          let ax = Kseq (p, 0, bind_oldies cty.cty_oldies (Kstop q)) in
          Kseq (Kaxiom (k_havoc eff ax), 0, k) in
539
        let add_rs sm s c (vl,k) = match s.rs_logic with
540
541
542
          | RLls _ -> assert false (* not applicable *)
          | RLnone -> vl, k
          | RLlemma ->
543
544
              let v = res_of_cty c.c_cty and q = c.c_cty.cty_post in
              let q = sp_of_post None Slab.empty expl_post v q in
545
546
547
              let q = if pv_is_unit v
                then t_subst_single v.pv_vs t_void q
                else t_exists_close_simp [v.pv_vs] [] q in
548
              vl, add_axiom c.c_cty q k
549
550
551
552
          | RLpv v ->
              let c = if Mrs.is_empty sm then c else c_rs_subst sm c in
              let q = cty_exec_post (cty_enrich_post c) in
              let q = sp_of_post None Slab.empty expl_post v q in
553
              v::vl, add_axiom c.c_cty q k in
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
        let vl, k = match ld with
          | LDrec rdl ->
              let add_rd sm d = Mrs.add d.rec_rsym d.rec_sym sm in
              let sm = List.fold_left add_rd Mrs.empty rdl in
              let add_rd d dl = add_rs sm d.rec_sym d.rec_fun dl in
              List.fold_right add_rd rdl ([], k)
          | LDsym (s,c) -> add_rs Mrs.empty s c ([], k)
          | LDvar _ -> assert false (* not applicable *) in
        let k = if vl = [] then k else Kseq (Kval (vl, t_true), 0, k) in
        (* precondition *)
        begin match ld with
          | LDrec rdl ->
              let rec k_par = function
                | [k] -> k | [] -> assert false
                | k::kl -> Kpar (k, k_par kl) in
              Kpar (k_havoc eff (k_par (k_rec env lps rdl)), k)
          | LDsym (_, {c_node = Cfun e; c_cty = cty}) ->
              Kpar (k_havoc eff (k_fun env lps cty e), k)
          | _ -> k end
    | Eif (e0, e1, e2) ->
574
        (* with both branches pure, switch to SP to avoid splitting *)
575
576
577
        let s = eff_pure e1.e_effect && eff_pure e2.e_effect in
        let k1 = k_expr env lps e1 res xmap in
        let k2 = k_expr env lps e2 res xmap in
578
579
580
581
        let kk v =
          if s then try
            let t1, f1, k1 = term_of_kode res k1 in
            let t2, f2, k2 = term_of_kode res k2 in
582
            let test = t_equ (t_var v.pv_vs) t_bool_true in
583
            (* with both branches simple, define a resulting term *)
584
            let t = t_if_simp test t1 t2 and f = sp_if test f1 f2 in
585
586
587
588
            Kseq (Ktag (SP, Kif (v, k1, k2)), 0, Klet (res, t, f))
          with Exit -> Ktag (SP, Kif (v, k1, k2))
          else Kif (v, k1, k2) in
        var_or_proxy e0 kk
589
    | Ecase (e0, bl) ->
590
        (* with all branches pure, switch to SP to avoid splitting *)
591
592
593
        let s = List.for_all (fun (_,e) -> eff_pure e.e_effect) bl in
        let branch (pp,e) = pp.pp_pat, k_expr env lps e res xmap in
        let bl = List.map branch bl in
594
595
596
597
598
599
600
601
602
        let kk v =
          if s then try
            let add_br (p,k) (bl,tl,fl) =
              let t, f, k = term_of_kode res k in
              let tl = t_close_branch p t :: tl in
              (p,k)::bl, tl, t_close_branch p f :: fl in
            let bl, tl, fl = List.fold_right add_br bl ([],[],[]) in
            (* with all branches simple, define a resulting term *)
            let tv = t_var v.pv_vs in
603
            let t = t_case tv tl and f = sp_case tv fl in
604
605
606
607
            Kseq (Ktag (SP, Kcase (v, bl)), 0, Klet (res, t, f))
          with Exit -> Ktag (SP, Kcase (v, bl))
          else Kcase (v, bl) in
        var_or_proxy e0 kk
608
    | Etry (e0, bl) ->
609
        (* try-with is just another semicolon *)
610
611
612
        let branch xs (vl,e) (xl,xm) =
          let i = new_exn env in
          let xk = k_expr env lps e res xmap in
613
          (* a single pv for the carried value *)
614
615
          let v, xk = match vl with
            | [] -> pv_of_ity "_" ity_unit, xk
616
617
            | [v] -> v, xk
            | vl ->
618
                let v = pv_of_ity "exv" xs.xs_ity in
619
620
621
622
623
624
                let cs = fs_tuple (List.length vl) in
                let pl = List.map (fun v -> pat_var v.pv_vs) vl in
                v, Kcase (v, [pat_app cs pl v.pv_vs.vs_ty, xk]) in
          (i,xk)::xl, Mexn.add xs (i,v) xm in
        let xl, xmap = Mexn.fold branch bl ([], xmap) in
        let k = k_expr env lps e0 res xmap in
625
626
627
        (* catched xsymbols are converted to unique integers,
           so that we can now serialise the "with" clauses
           and avoid capturing the wrong exceptions *)
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
        List.fold_left (fun k (i,xk) -> Kseq (k,i,xk)) k xl
    | Eraise (xs, e0) ->
        let i, v = Mexn.find xs xmap in
        Kseq (k_expr env lps e0 v xmap, 0, Kcont i)
    | Eassert (Assert, f) ->
        let f = vc_expl None lab expl_assert f in
        Kseq (Kcut f, 0, k_unit res)
    | Eassert (Assume, f) ->
        let f = vc_expl None lab expl_assume f in
        Kval ([res], f)
    | Eassert (Check, f) ->
        let f = vc_expl None lab expl_check f in
        Kpar (Kstop f, k_unit res)
    | Eghost e0 ->
        k_expr env lps e0 res xmap
    | Epure t ->
        let t = if t.t_ty <> None then t_lab t else
          t_if_simp (t_lab t) t_bool_true t_bool_false in
        Klet (res, t, t_true)
    | Eabsurd ->
648
        Kstop (vc_expl loc lab expl_absurd t_false)
649
    | Ewhile (e0, invl, varl, e1) ->
650
651
652
        (* [ STOP inv
           | HAVOC ; ASSUME inv ; IF e0 THEN e1 ; STOP inv
                                        ELSE SKIP ] *)
653
654
655
        let init = wp_of_inv None lab expl_loop_init invl in
        let prev = sp_of_inv None lab expl_loop_init invl in
        let keep = wp_of_inv None lab expl_loop_keep invl in
656
657
658
659
660
        let keep, oldies =
          if varl = [] then keep, Mpv.empty else
          let oldies, ovarl = oldify_variant varl in
          let d = decrease env loc lab expl_loop_vari ovarl varl in
          wp_and d keep, oldies in
661
662
663
664
665
666
667
668
669
670
671
672
673
674
        let k = Kseq (k_expr env lps e1 res xmap, 0, Kstop keep) in
        let k = var_or_proxy e0 (fun v -> Kif (v, k, k_unit res)) in
        let k = Kseq (Kval ([], prev), 0, bind_oldies oldies k) in
        Kpar (Kstop init, k_havoc e.e_effect k)
    | Efor (v, ({pv_vs = a}, d, {pv_vs = b}), invl, e1) ->
        let a = t_var a and b = t_var b in
        let i = t_var v.pv_vs and one = t_nat_const 1 in
        let init = wp_of_inv None lab expl_loop_init invl in
        let prev = sp_of_inv None lab expl_loop_init invl in
        let keep = wp_of_inv None lab expl_loop_keep invl in
        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
        let bounds = t_and (ps_app le [a; i]) (ps_app le [i; b]) in
675
        let expl_bounds f = vc_expl loc lab expl_for_bound f in
676
677
678
679
680
681
682
683
684
        let i_pl_1 = fs_app pl [i; one] ty_int in
        let b_pl_1 = fs_app pl [b; one] ty_int in
        let init = t_subst_single v.pv_vs a init in
        let keep = t_subst_single v.pv_vs i_pl_1 keep in
        let last = t_subst_single v.pv_vs b_pl_1 prev in
        let k = Kseq (k_expr env lps e1 res xmap, 0, Kstop keep) in
        let k = Kseq (Kval ([v], sp_and bounds prev), 0, k) in
        let k = Kpar (k, Kval ([res], last)) in
        let k = Kpar (Kstop init, k_havoc e.e_effect k) in
685
686
687
688
689
690
        if Slab.mem lf_label e.e_label then (* "liberal for"
          [ ASSUME a <= b ;
            [ STOP inv[a]
            | HAVOC ; [ ASSUME a <= v <= b /\ inv[v] ; e1 ; STOP inv[v+1]
                      | ASSUME inv[b+1] ] ]
          | ASSUME a > b ] *)
691
692
          Kpar (Kseq (Kval ([], expl_bounds (ps_app le [a; b])), 0, k),
                   Kval ([res], expl_bounds (ps_app gt [a; b])))
693
694
695
696
697
        else (* "strict for"
          [ STOP a <= b+1
          | STOP inv[a]
          | HAVOC ; [ ASSUME a <= v <= b /\ inv[v] ; e1 ; STOP inv[v+1]
                    | ASSUME inv[b+1] ] ] *)
698
          Kpar (Kstop (expl_bounds (ps_app le [a; b_pl_1])), k)
699
700
701
702
703
  in
  if Slab.mem sp_label e.e_label then Ktag (SP, k) else
  if Slab.mem wp_label e.e_label then Ktag (WP, k) else k

and k_fun env lps ?(oldies=Mpv.empty) ?(xmap=Mexn.empty) cty e =
Andrei Paskevich's avatar
Andrei Paskevich committed
704
  (* ASSUME pre ; LET o = arg ; TRY e ; STOP post WITH STOP xpost *)
705
706
707
708
709
710
711
712
713
714
715
716
717
  let res, q = wp_of_post expl_post cty.cty_result cty.cty_post in
  let xq = complete_xpost cty e.e_effect xmap in
  let xq = Mexn.mapi (fun xs ql ->
    let v, xq = wp_of_post expl_xpost xs.xs_ity ql in
    (new_exn env, v), xq) xq in
  let xmap = Mexn.set_union (Mexn.map fst xq) xmap in
  let k = Kseq (k_expr env lps e res xmap, 0, Kstop q) in
  let k = Mexn.fold (fun _ ((i,_), xq) k ->
    Kseq (k, i, Kstop xq)) xq k in
  (* move the postconditions under the VCgen tag *)
  let k = if Slab.mem sp_label e.e_label then Ktag (SP, k) else
          if Slab.mem wp_label e.e_label then Ktag (WP, k) else k in
  let k = bind_oldies oldies (bind_oldies cty.cty_oldies k) in
718
  Kseq (Kval (cty.cty_args, sp_of_pre cty.cty_pre), 0, k)
719
720
721
722
723
724

and k_rec env lps rdl =
  let k_rd {rec_fun = c; rec_varl = varl} =
    let e = match c.c_node with
      | Cfun e -> e | _ -> assert false in
    if varl = [] then k_fun env lps c.c_cty e else
725
726
727
    (* store in lps our variant at the entry point
       and the list of well-founded orderings
       for each function in the let-rec block *)
728
    let oldies, varl = oldify_variant varl in
729
730
731
    let add lps rd =
      let decr = Opt.get (ls_decr_of_rec_defn rd) in
      Mls.add decr (varl, List.map snd rd.rec_varl) lps in
732
733
734
    k_fun env (List.fold_left add lps rdl) ~oldies c.c_cty e in
  List.map k_rd rdl

735
(* stage 2: push sub-expressions up as far as we can *)
736

737
738
739
740
741
(* remove dead code, reassociate sequences to the right,
   and move exception-handling code to the raise site
   when there is only one. This reduces duplication of
   premises for SP and allows it to use let-in instead
   of quantifiers over an equality when possible. *)
742
743
744
let reflow vc_wp k =
  let join _ _ _ = Some false in
  let join = Mint.union join in
745
746
747
748
749
  (* count the exit points for every outcome, normal or
     exceptional; remove the subsequent code if none,
     tag the subsequent code for moving up if single.
     For every kode to be pushed up, remember if
     it can exit normally (open) or not (closed). *)
750
  let rec mark vc_tag k = match k with
Andrei Paskevich's avatar
Andrei Paskevich committed
751
752
753
    | Kseq ((Khavoc _ | Klet _ | Kval _ | Kcut _) as k1, 0, k2) ->
        let k2, out2 = mark vc_tag k2 in
        Kseq (k1, 0, k2), out2
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
    | Kseq (k1, i, k2) ->
        let k1, out1 = mark vc_tag k1 in
        begin match Mint.find_opt i out1 with
        | Some push ->
            let k2, out2 = mark vc_tag k2 in
            let k2 = if not push then k2 else
              Ktag (Push (not (Mint.mem 0 out2)), k2) in
            Kseq (k1, i, k2), join (Mint.remove i out1) out2
        | None -> k1, out1 (* dead code *) end
    | Kpar (k1, k2) ->
        let k1, out1 = mark vc_tag k1 in
        let k2, out2 = mark vc_tag k2 in
        Kpar (k1, k2), join out1 out2
    | Kif (v, k1, k2) ->
        let k1, out1 = mark vc_tag k1 in
        let k2, out2 = mark vc_tag k2 in
        Kif (v, k1, k2), join out1 out2
    | Kcase (v, bl) ->
        let branch (p, k1) (bl, out2) =
          let k1, out1 = mark vc_tag k1 in
          (p,k1)::bl, join out1 out2 in
        let bl, out = List.fold_right branch bl ([], Mint.empty) in
        Kcase (v, bl), out
    | Khavoc _ | Klet _ | Kval _ | Kcut _ ->
        k, Mint.singleton 0 true
    | Kstop _ ->
        k, Mint.empty
Andrei Paskevich's avatar
Andrei Paskevich committed
781
782
    | Kcont i ->
        k, Mint.singleton i true
783
784
785
786
787
    | Kaxiom k ->
        let k, _ = mark vc_tag k in
        k, Mint.singleton 0 true
    | Ktag ((WP|SP) as tag, k) when tag <> vc_tag ->
        let k, out = mark tag k in
788
789
790
        (* WP ((SP k1); k2) could be SP (k1; WP k2),
           but we cannot freely switch from SP to WP,
           so we forbid pushing under another VCgen *)
791
792
793
794
        Ktag (tag, k), Mint.map (fun _ -> false) out
    | Ktag ((WP|SP), k) ->
        mark vc_tag k
    | Ktag (Push _, _) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
795
        assert false (* cannot happen *)
796
797
798
  in
  let rec push k q = match k with
    | Kseq (k1, i, Ktag (Push cl, k2)) ->
799
800
        (* if k2 is open but we push a closed code
           for 0 in it, then k2 becomes closed *)
Andrei Paskevich's avatar
Andrei Paskevich committed
801
802
        let cl = cl || match Mint.find_opt 0 q with
          | Some (_, cl) -> cl | None -> false in
803
        let q = Mint.add i (push k2 q, cl) q in
804
805
806
        (* if k2 is an open exception-handling code
           being pushed in k1, then we must still
           raise i after k2 and catch it here *)
Andrei Paskevich's avatar
Andrei Paskevich committed
807
808
        if i = 0 || cl then push k1 q else
        Kseq (push k1 q, i, Kcont 0)
809
810
811
812
813
814
815
816
817
818
819
820
821
822
    | Kseq (k1, i, k2) ->
        Kseq (push k1 (Mint.remove i q), i, push k2 q)
    | Kpar (k1, k2) ->
        Kpar (push k1 q, push k2 q)
    | Kif (v, k1, k2) ->
        Kif (v, push k1 q, push k2 q)
    | Kcase (v, bl) ->
        Kcase (v, List.map (fun (p,k) -> p, push k q) bl)
    | Khavoc _ | Klet _ | Kval _ | Kcut _ ->
        begin match Mint.find_opt 0 q with
        | Some (q, _) -> Kseq (k, 0, q)
        | None -> k end
    | Kstop _ ->
        k
Andrei Paskevich's avatar
Andrei Paskevich committed
823
824
825
826
827
    | Kcont i ->
        begin match Mint.find_opt i q with
        | Some (q, cl) when i = 0 || cl -> q
        | Some (q, _) -> Kseq (q, 0, k)
        | None -> k end
828
829
830
831
832
833
    | Kaxiom k ->
        let k = push k Mint.empty in
        begin match Mint.find_opt 0 q with
        | Some (q, _) -> Kseq (Kaxiom k, 0, q)
        | None -> Kaxiom k end
    | Ktag ((WP|SP) as tag, k) ->
834
        Ktag (tag, push k Mint.empty)
Andrei Paskevich's avatar
Andrei Paskevich committed
835
836
    | Ktag (Push _, _) ->
        assert false (* cannot happen *)
837
838
839
840
841
  in
  let k = if vc_wp then k else Ktag (SP, k) in
  push (fst (mark WP k)) Mint.empty

(** stage 3: WP *)
Andrei Paskevich's avatar
Andrei Paskevich committed
842

Andrei Paskevich's avatar
Andrei Paskevich committed
843
(* a "destination map" maps program variables (pre-effect state)
Andrei Paskevich's avatar
Andrei Paskevich committed
844
845
   to fresh vsymbols (post-effect state) *)

846
847
let ity_affected wr ity =
  Util.any ity_rch_fold (Mreg.contains wr) ity
Andrei Paskevich's avatar
Andrei Paskevich committed
848

849
let pv_affected wr v = ity_affected wr v.pv_ity
Andrei Paskevich's avatar
Andrei Paskevich committed
850

851
852
853
let pvs_affected wr pvs =
  if Mreg.is_empty wr then Spv.empty
  else Spv.filter (pv_affected wr) pvs
Andrei Paskevich's avatar
Andrei Paskevich committed
854

855
856
857
858
859
let dst_of_wp wr wp =
  if Mreg.is_empty wr then Mpv.empty else
  let clone_affected v _ =
    if pv_affected wr v then Some (clone_pv v) else None in
  Mpv.mapi_filter clone_affected (t_freepvs Spv.empty wp)
Andrei Paskevich's avatar
Andrei Paskevich committed
860

861
862
let adjustment dst = Mpv.fold (fun o n sbs ->
  Mvs.add o.pv_vs (t_var n) sbs) dst Mvs.empty
Andrei Paskevich's avatar
Andrei Paskevich committed
863

864
let advancement dst0 dst1 =
865
866
867
  let add _ v n sbs =
    if vs_equal v n then sbs else Mvs.add v (t_var n) sbs in
  Mpv.fold2_inter add dst0 dst1 Mvs.empty
Andrei Paskevich's avatar
Andrei Paskevich committed
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895

(* 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 =
896
897
898
899
900
  let rec reg_aff_regs s r =
    let q = reg_exp_fold reg_aff_regs Sreg.empty r in
    let affect = not (Sreg.is_empty q) || Mreg.mem r wr in
    Sreg.union s (if affect then Sreg.add r q else q) in
  let collect o _ aff = ity_exp_fold reg_aff_regs aff o.pv_ity in
Andrei Paskevich's avatar
Andrei Paskevich committed
901
902
903
904
905
906
907
  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
908

Andrei Paskevich's avatar
Andrei Paskevich committed
909
910
911
(* produce a rebuilding postcondition after a write effect *)

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

914
let sensitive itd {pv_vs = f} =
Andrei Paskevich's avatar
Andrei Paskevich committed
915
  not itd.itd_its.its_private &&
916
917
  List.exists (fun i -> t_v_occurs f i > 0) itd.itd_invariant

918
let rec havoc kn wr regs t ity fl =
Andrei Paskevich's avatar
Andrei Paskevich committed
919
  if not (ity_affected wr ity) then t, fl else
Andrei Paskevich's avatar
Andrei Paskevich committed
920
921
922
  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
923
924
925
926
      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
927
928
      let field rs fl =
        let fd = Opt.get rs.rs_field in
929
930
931
        match Mpv.find_opt fd wfs with
        | Some None -> fl
        | Some (Some {pv_vs = v}) ->
932
933
934
935
            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
936
            let nt = fs_app (ls_of_rs rs) [nt] v.vs_ty in
937
            let ity = ity_full_inst isb rs.rs_cty.cty_result in
938
            let t, fl = havoc kn wr regs (t_var v) ity fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
939
            cons_t_simp nt t fl
940
        | None ->
Andrei Paskevich's avatar
Andrei Paskevich committed
941
            let ity = ity_full_inst isb rs.rs_cty.cty_result in
942
943
944
945
            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
946
947
            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
948
            let t, fl = havoc kn wr regs t ity fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
949
950
            cons_t_simp nt t fl in
      nt, List.fold_right field itd.itd_fields fl
Andrei Paskevich's avatar
Andrei Paskevich committed
951
952
953
954
955
956
957
  | 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
958
          let field rs (tl, fl) =
Andrei Paskevich's avatar
Andrei Paskevich committed
959
            let ity = ity_full_inst isb rs.rs_cty.cty_result in
Andrei Paskevich's avatar
Andrei Paskevich committed
960
            let t = t_app_infer (ls_of_rs rs) [t] in
961
            let t, fl = havoc kn wr regs t ity fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
962
963
            t::tl, fl in
          let tl, fl = List.fold_right field itd.itd_fields ([],fl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
964
965
966
967
968
969
970
          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
971
          t, fl
Andrei Paskevich's avatar
Andrei Paskevich committed
972
973
974
975
976
977
978
979
980
981
      | 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
982
            let field v ity (tl, fl) =
983
              let t, fl = havoc kn wr regs (t_var v) ity fl in
Andrei Paskevich's avatar
Andrei Paskevich committed
984
985
986
              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
987
          let tbl, fbl = List.split (List.map branch cl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
988
          let t = t_case_close t tbl and f = t_case_close_simp t fbl in
989
          t, begin match f.t_node with Ttrue -> fl | _ -> f::fl end
Andrei Paskevich's avatar
Andrei Paskevich committed
990
991
      end

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

Andrei Paskevich's avatar
Andrei Paskevich committed
997
let print_regs regs = if Debug.test_flag debug then
Andrei Paskevich's avatar
Andrei Paskevich committed
998
999
  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
1000
      Ity.print_reg r Pretty.print_term t)) (Mreg.bindings regs)
1001

1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
let sp_complete sp1 wr1 wr2 =
  let add v n sp = sp_and sp (t_equ (t_var n) (t_var v.pv_vs)) in
  Mpv.fold add (Mpv.set_diff wr2 wr1) sp1

let sp_combine sp1 wr1 sp2 wr2 =
  let sp1 = sp_complete sp1 wr1 wr2 in
  let sp2 = sp_complete sp2 wr2 wr1 in
  sp_or sp1 sp2, Mpv.set_union wr1 wr2

let sp_combine_map sp1 sp2 =
  Mint.union (fun _ (sp1, wr1) (sp2, wr2) ->
    Some (sp_combine sp1 wr1 sp2 wr2)) sp1 sp2

Andrei Paskevich's avatar
Andrei Paskevich committed
1015
(* compute compact verification conditions, in the style
Andrei Paskevich's avatar
Andrei Paskevich committed
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
   of the Flanagan and Saxe paper (POPL'01).

   Here is how it works, on a small example:

      sp_expr kn k
              rdm = [0 -> {v1; v2}; 1 -> {v1; v3}]
              dst = [v1 -> u1; v2 -> u2; v3 -> u3]
      = (wp, [0 -> (sp_0, [v1 -> u1]);
              1 -> (sp_1, [v3 -> u3])], {v0; v1})

   [sp_expr kn k rdm dst] returns a triple [(wp, sp+wr, rd)].

   The mapping [rdm] provides the post-reads set for every
   possible outcome of [k]. If [k] ends normally (outcome 0),
   the subsequent execution will read program variables [v1]
   and [v2]. If [k] terminates with an exception (outcome 1),
   the subsequent execution will read [v1] and [v3].

   The mapping [dst] provides post-write names for every
   mutable variable in [rdm]. If [k] modifies [v1] (on any
   execution path), the final value must be put in [u1],
   and similarly for [v2] and [v3].

   The set [rd] contains every previously defined or declared
   variable that may be read by [k] or by the subsequent code
   for any outcome of [k]. In our example, [k] and the code
   after [k] depends on [v0] and [v1]; the variables [v2] and
   [v3] are defined or declared by [k] itself and thus do not
   appear in [rd].

   The formula [wp] is a safety precondition of [k], logically
   equivalent to [WP(k,true)]. Every free variable in [wp] is
   in [rd].

   The mapping [sp+wr] provides the postcondition [sp_i] and
   the actual write effect [wr_i] for every outcome [i] of [k].
   The write effect [wr_i] is necessarily a submap of [dst]
   restricted to the corresponding post-read set [rdm(i)].
   For example, it is possible that [k] also modifies [v3]
   on the normal execution path, but since [v3] is not read
   after the normal termination of [k], it is not in [wr_0].
   Every free variable in [sp_i] is either in [rd] or in
   the range of [wr_i], or otherwise in [rdm(i)]. Every
   variable in the range of [wr_i] is free in [sp_i]. *)

Andrei Paskevich's avatar
Andrei Paskevich committed
1061
let rec sp_expr kn k rdm dst = match k with
Andrei Paskevich's avatar
Andrei Paskevich committed
1062
  | Kseq (Klet (v, t, f), 0, k2) ->
1063
      let wp2, sp2, rd2 = sp_expr kn k2 rdm dst in
Andrei Paskevich's avatar
Andrei Paskevich committed
1064
      let rd1 = t_freepvs (t_freepvs rd2 t) f in
Andrei Paskevich's avatar
Andrei Paskevich committed
1065
      let wp = wp_let v t (sp_implies f wp2) in
Andrei Paskevich's avatar
Andrei Paskevich committed
1066
1067
1068
      let close _ (sp, wr) rd =
        Some (sp_let v t (sp_and f sp) rd, wr) in
      wp, Mint.inter close sp2 rdm, Spv.remove v rd1
1069
1070
  | Kseq (k1, i, k2) ->
      let wp2, sp2, rd2 = sp_expr kn k2 rdm dst in
Andrei Paskevich's avatar
Andrei Paskevich committed
1071
1072
1073
      (* the dst parameter for k1 must include a fresh final
         name for every variable modified by k2 (on any path),
         and for every variable read by k2 that is not in dst *)
Andrei Paskevich's avatar
Andrei Paskevich committed
1074
1075
      let get_wr _ (_, w) m = Mpv.set_union w m in
      let wr2 = Mint.fold get_wr sp2 Mpv.empty in
1076
1077
1078
1079
      let fresh_wr2 v _ = clone_pv v in
      let fresh_rd2 v _ = if ity_immutable v.pv_ity
                          then None else Some (clone_pv v) in
      let wp1, sp1, rd1 = sp_expr kn k1 (Mint.add i rd2 rdm)
Andrei Paskevich's avatar
Andrei Paskevich committed
1080
1081
        (Mpv.set_union (Mpv.set_union (Mpv.mapi fresh_wr2 wr2)
        (Mpv.mapi_filter fresh_rd2 (Mpv.set_diff rd2 dst))) dst) in
Andrei Paskevich's avatar
Andrei Paskevich committed
1082
1083
      (* retrieve the postcondition and the write effect for the
         outcome i: they prepend everything that happens in k2 *)
Andrei Paskevich's avatar
Andrei Paskevich committed
1084
      let sp0, wr0 = Mint.find i sp1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
1085
1086
1087
      (* in (sp0 -> wp2) we bind everything that is not in rd1,
         knowing that variables that are not in rd2 are already
         bound in sp0. We also bind all the final names. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
1088
1089
      let concat rd wr = List.rev_append (List.rev_map
        (fun v -> v.pv_vs) (Spv.elements rd)) (Mpv.values wr) in
Andrei Paskevich's avatar
Andrei Paskevich committed
1090
      let bound = Spv.diff rd2 rd1 in
1091
      let wp2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
1092
        (* variables in wp2 must be adjusted wrt. wr0 *)
Andrei Paskevich's avatar
Andrei Paskevich committed
1093
1094
        let adj = adjustment wr0 and vl = concat bound wr0 in
        wp_forall vl (sp_implies sp0 (t_subst adj wp2)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
1095
      (* compute (sp0 /\ sp2_j) for every outcome j of k2 *)
Andrei Paskevich's avatar
Andrei Paskevich committed
1096
      let close (sp, wr) rd =
Andrei Paskevich's avatar
Andrei Paskevich committed
1097
1098
1099
        (* retrieve the write effects in wr0 that are visible
           in the post-reads of k2, i.e., are not masked by
           a write in k2 on the corresponding execution path *)
Andrei Paskevich's avatar
Andrei Paskevich committed
1100
1101
        let wr0_dst = Mpv.set_inter dst
          (Mpv.set_diff (Mpv.set_inter wr0 rd) wr) in
Andrei Paskevich's avatar
Andrei Paskevich committed
1102
1103
1104
1105
        let wr = Mpv.set_union wr0_dst wr in
        (* we must not bind variables that are visible in the
           post-reads of k2, so we remove the post-reads from
           bound, and we remove the visible writes from wr0 *)
Andrei Paskevich's avatar
Andrei Paskevich committed
1106
1107
        let vl = concat
          (Spv.diff bound rd) (Mpv.set_diff wr0 wr0_dst) in
Andrei Paskevich's avatar
Andrei Paskevich committed
1108
1109
1110
        (* visible writes in sp0 are not masked by wr, and so
           must be advanced to dst. Variables in sp must then
           be adjusted wrt. this "advanced" write effect. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
1111
1112
1113
1114
1115
        let adj = adjustment (Mpv.set_union wr0_dst wr0) in
        let sp0 = t_subst (advancement wr0 wr0_dst) sp0 in
        sp_exists vl (sp_and sp0 (t_subst adj sp)), wr in
      let close _ sp rd = Some (close sp r