pgm_wp.ml 15.5 KB
Newer Older
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19

20
open Format
21
open Why
22
open Util
23
open Ident
24
open Ty
25 26 27
open Term
open Decl
open Theory
28
open Pretty
29
open Pgm_ttree
30
open Pgm_env
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
31 32 33

module E = Pgm_effect

34
let debug = Debug.register_flag "program_wp"
35

36 37
(* phase 4: weakest preconditions *******************************************)

38 39 40
(* smart constructors for building WPs
   TODO: use simp forms / tag with label "WP" *)

41
let wp_and ?(sym=false) f1 f2 =
42 43
(*   if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2)  *)
  let f = f_and_simp f1 f2 in
44
  if sym then f else f_label_add (Split_goal.asym_split) f
45

46 47 48
let wp_ands ?(sym=false) fl =
  List.fold_left (wp_and ~sym) f_true fl

49 50 51
let wp_implies f1 f2 = match f2.f_node with
  | Ffalse -> f_implies f1 f2
  | _ -> f_implies_simp f1 f2
52 53 54 55 56 57 58 59 60

let is_ref_ty env ty = match ty.ty_node with
  | Tyapp (ts, _) -> ts_equal ts env.ts_ref
  | _ -> false

let is_arrow_ty env ty = match ty.ty_node with
  | Tyapp (ts, _) -> ts_equal ts env.ts_arrow
  | _ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
61 62
let wp_forall env v f =
  if is_arrow_ty env v.vs_ty then f else match f.f_node with
63 64 65 66 67 68 69
    | Fbinop (Fimplies, {f_node = Fapp (s,[{t_node = Tvar u};r])},h)
      when ls_equal s ps_equ && vs_equal u v && not (t_occurs_single v r) ->
        f_subst_single v r h
    | Fbinop (Fimplies, {f_node = Fbinop (Fand, g,
                        {f_node = Fapp (s,[{t_node = Tvar u};r])})},h)
      when ls_equal s ps_equ && vs_equal u v && not (t_occurs_single v r) ->
        f_subst_single v r (f_implies_simp g h)
Andrei Paskevich's avatar
Andrei Paskevich committed
70 71 72 73
    | _ when f_occurs_single v f ->
        f_forall_close_simp [v] [] f
    | _ ->
        f
74 75

(* utility functions for building WPs *)
76

77
let fresh_label env =
78
  let ty = ty_app env.ts_label [] in
79
  create_vsymbol (id_fresh "label") ty
80

81 82
let wp_binder env (x, tv) f = match tv with
  | Tpure _ -> wp_forall env x f
83 84
  | Tarrow _ -> f

85
let wp_binders env = List.fold_right (wp_binder env)
86

87 88 89
(* replace old(t) with at(t,lab) everywhere in formula f *)
let rec old_label env lab f =
  f_map (old_label_term env lab) (old_label env lab) f
90

91
and old_label_term env lab t = match t.t_node with
92
  | Tapp (ls, [t]) when ls_equal ls env.ls_old ->
93
      let t = old_label_term env lab t in (* NECESSARY? *)
94
      t_app env.ls_at [t; t_var lab] t.t_ty
95 96 97 98 99
  | _ ->
      t_map (old_label_term env lab) (old_label env lab) t

(* replace at(t,lab) with t everywhere in formula f *)
let rec erase_label env lab f =
100
  f_map (erase_label_term env lab) (erase_label env lab) f
101 102

and erase_label_term env lab t = match t.t_node with
103
  | Tapp (ls, [t; {t_node = Tvar l}])
104
    when ls_equal ls env.ls_at && vs_equal l lab ->
105 106 107 108 109
      erase_label_term env lab t
  | _ ->
      t_map (erase_label_term env lab) (erase_label env lab) t

let unref_ty env ty = match ty.ty_node with
110
  | Tyapp (ts, [ty]) when ts_equal ts env.ts_ref -> ty
111 112 113 114 115 116 117
  | _ -> assert false

(* replace !r by v everywhere in formula f *)
let rec unref env r v f =
  f_map (unref_term env r v) (unref env r v) f

and unref_term env r v t = match t.t_node with
118
  | Tapp (ls, [u]) when ls_equal ls env.ls_bang ->
119
      let rt = E.reference_of_term u in
120
      if E.ref_equal rt r then t_var v else t
121
  | Tapp (ls, _) when ls_equal ls env.ls_old ->
122
      assert false
123
  | Tapp (ls, _) when ls_equal ls env.ls_at -> (* do not recurse in at(...) *)
124
      t
125 126 127 128
  | _ ->
      t_map (unref_term env r v) (unref env r v) t

(* quantify over all references in ef *)
129
let quantify ?(all=false) env ef f =
130
  (* eprintf "quantify: ef=%a f=%a@." E.print ef Pretty.print_fmla f; *)
131
  let quantify1 r f =
132 133
    let ty = unref_ty env (E.type_of_reference r) in
    let v = create_vsymbol (id_clone (E.name_of_reference r)) ty in
134
    let f = unref env r v f in
135
    wp_forall env v f
136
  in
137 138
  let s = ef.E.writes in
  let s = if all then E.Sref.union ef.E.reads s else s in
139 140
  E.Sref.fold quantify1 s f

141 142
let abstract_wp env ef (q',ql') (q,ql) =
  assert (List.length ql' = List.length ql);
143
  let quantify_res f' f res =
144
    let f = wp_implies f' f in
145 146
    let f = match res with
      | Some v when is_ref_ty env v.vs_ty ->
147
	  let v' = create_vsymbol (id_clone v.vs_name) (unref_ty env v.vs_ty) in
148
	  wp_forall env v' (unref env (E.Rlocal v) v' f)
149
      | Some v ->
150
	  wp_forall env v f
151 152
      | None ->
	  f
153
    in
154 155 156 157 158
    quantify env ef f
  in
  let quantify_h (e',(x',f')) (e,(x,f)) =
    assert (ls_equal e' e);
    let res, f' = match x', x with
159
      | Some v', Some v -> Some v, f_subst (subst1 v' (t_var v)) f'
160 161 162
      | None, None -> None, f'
      | _ -> assert false
    in
163
    quantify_res f' f res
164
  in
165
  let f =
166
    let res, f = q and res', f' = q' in
167
    let f' = f_subst (subst1 res' (t_var res)) f' in
168
    quantify_res f' f (Some res)
169 170 171
  in
  wp_ands (f :: List.map2 quantify_h ql' ql)

172
let opaque_wp env ef q' q =
173 174 175 176 177
  let lab = fresh_label env in
  let q' = post_map (old_label env lab) q' in
  let f = abstract_wp env ef q' q in
  erase_label env lab f

178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
(*s [filter_post k q] removes exc. postconditions from [q] which do not
    appear in effect [ef] *)

let filter_post ef (q, ql) =
  let keep (ls, _) = Sls.mem ls ef.E.raises in
  q, List.filter keep ql

let rec ls_assoc ls = function
  | [] -> raise Not_found
  | (ls', x) :: _ when ls_equal ls ls' -> x
  | _ :: r -> ls_assoc ls r

let default_exn_post ls = ls, (exn_v_result ls, f_true)

let default_post ty ef =
193
  (v_result ty, f_true),
194 195
  List.map default_exn_post (Sls.elements ef.E.raises)

196
let rec assoc_handler x = function
197
  | [] -> raise Not_found
198 199 200
  | (y, h) :: _ when ls_equal x y -> h
  | _ :: hl -> assoc_handler x hl

201 202 203
(*s [saturate_post ef f q] makes a postcondition for a program of effect [ef]
    out of a normal postcondition [f] and the exc. postconditions from [q] *)

204
let saturate_post ef q (_, ql) =
205 206
  let set_post x = try x, ls_assoc x ql with Not_found -> default_exn_post x in
  let xs = Sls.elements ef.E.raises in
207
  (q, List.map set_post xs)
208

209 210 211 212 213 214 215 216 217 218
(* maximum *)

let is_default_post = f_equal f_true

let sup ((q, ql) : post) (_, ql') =
  assert (List.length ql = List.length ql');
  let supx (x, (_,fa) as a) (x', _ as a') =
    assert (ls_equal x x');
    if is_default_post fa then a' else a
  in
219
  q, List.map2 supx ql ql'
220 221 222 223 224 225

(* post-condition for a loop body *)

let default_exns_post ef =
  let xs = Sls.elements ef.E.raises in
  List.map default_exn_post xs
226

227 228 229
let term_at env lab t =
  t_app env.ls_at [t; t_var lab] t.t_ty

230
let while_post_block env inv var lab e =
231
  let decphi = match var with
232
    | None ->
233
	f_true
234
    | Some (phi, r) ->
235 236 237 238 239
	f_app r [phi; term_at env lab phi]
  in
  let ql = default_exns_post e.expr_effect in
  let res = v_result e.expr_type in
  match inv with
240
    | None ->
241
	(res, decphi), ql
242
    | Some i ->
243 244 245 246 247 248 249
	(res, wp_and i decphi), ql

let well_founded_rel = function
  | None -> f_true
  | Some (_,_r) -> f_true (* TODO: Papp (well_founded, [Tvar r], []) *)


250 251
(* Recursive computation of the weakest precondition *)

252 253 254
let propose_label l f =
  if f.f_label = [] then f_label [l] f else f

255
let rec wp_expr env e q =
256
  (* if Debug.test_flag debug then  *)
257
  (*   eprintf "@[wp_expr: q=%a@]@." Pretty.print_fmla (snd (fst q)); *)
258 259 260
  let lab = fresh_label env in
  let q = post_map (old_label env lab) q in
  let f = wp_desc env e q in
261
  let f = erase_label env lab f in
262
  propose_label (label ~loc:e.expr_loc "WP") f
263 264

and wp_desc env e q = match e.expr_desc with
265
  | Elogic t ->
266
      let (v, q), _ = q in
Andrei Paskevich's avatar
Andrei Paskevich committed
267
      f_subst_single v t q
268 269 270
  | Elocal v ->
      let (res, q), _ = q in
      f_subst (subst1 res (t_var v)) q
271
  | Eglobal _ ->
272
      let (_, q), _ = q in q
273
  | Efun (bl, t) ->
274
      let (_, q), _ = q in
275
      let f = wp_triple env t in
276
      wp_and q (wp_binders env bl f)
277 278
  | Elet (x, e1, e2) ->
      let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
279 280 281
      let v1 = v_result e1.expr_type in
      let t1 = t_label_add (label ~loc:e1.expr_loc "let") (t_var v1) in
      let q1 = v1, f_subst (subst1 x t1) w2 in
282 283
      let q1 = saturate_post e1.expr_effect q1 q in
      wp_expr env e1 q1
284 285
  | Eletrec (dl, e1) ->
      let w1 = wp_expr env e1 q in
286
      let wl = List.map (wp_recfun env) dl in
287
      wp_ands ~sym:true (w1 :: wl)
288

289 290 291 292 293 294
  | Eif (e1, e2, e3) ->
      let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
      let w3 = wp_expr env e3 (filter_post e3.expr_effect q) in
      let q1 = (* if result=True then w2 else w3 *)
	let res = v_result e1.expr_type in
	let test = f_equ (t_var res) (t_True env) in
295
	let test = f_label_add (label ~loc:e1.expr_loc "WP") test in
296 297 298 299
	let q1 = f_if test w2 w3 in
	saturate_post e1.expr_effect (res, q1) q
      in
      wp_expr env e1 q1
300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316
  | Eloop ({ loop_invariant = inv; loop_variant = var }, e1) ->
      let wfr = well_founded_rel var in
      let lab = fresh_label env in
      let q1 = while_post_block env inv var lab e1 in
      let q1 = sup q1 q in (* exc. posts taken from [q] *)
      let we = wp_expr env e1 q1 in
      let we = erase_label env lab we in
      let w = match inv with
	| None ->
	    wp_and wfr (quantify env e.expr_effect we)
	| Some i ->
	    wp_and wfr
	      (wp_and ~sym:true
		 i
		 (quantify env e.expr_effect (wp_implies i we)))
	in
	w
317
  (* optimization for the particular case let _ = y in e *)
Andrei Paskevich's avatar
Andrei Paskevich committed
318 319
  | Ematch (_, [{pat_node = Pwild}, e]) ->
      wp_expr env e (filter_post e.expr_effect q)
Andrei Paskevich's avatar
Andrei Paskevich committed
320
  | Ematch (x, bl) ->
321 322
      let branch (p, e) =
        f_close_branch p (wp_expr env e (filter_post e.expr_effect q))
323
      in
Andrei Paskevich's avatar
Andrei Paskevich committed
324 325
      let t = t_var x in
      f_case t (List.map branch bl)
326
  | Eabsurd ->
327 328 329 330 331 332 333 334 335
      f_false
  | Eraise (x, None) ->
      (* $wp(raise E, _, R) = R$ *)
      let _, ql = q in
      let _, f = assoc_handler x ql in f
  | Eraise (x, Some e1) ->
      (* $wp(raise (E e1), _, R) = wp(e1, R, R)$ *)
      let _, ql = q in
      let q1 = match assoc_handler x ql with
336
	| Some v, r -> (v, r), ql
337 338 339 340 341 342
	| None, _ -> assert false
      in
      let q1 = filter_post e1.expr_effect q1 in
      wp_expr env e1 q1
  | Etry (e1, hl) ->
      (* $wp(try e1 with E -> e2, Q, R) = wp(e1, Q, wp(e2, Q, R))$ *)
343 344 345
      let hwl =
	List.map
	  (fun (x, v, h) ->
346 347
	     let w = wp_expr env h (filter_post h.expr_effect q) in
	     x, (v, w))
348
	  hl
349 350 351 352 353 354 355 356 357 358
      in
      let make_post (q, ql) =
	let hpost (x, r) =
	  x, try assoc_handler x hwl with Not_found -> r
	in
	q, List.map hpost ql
      in
      let q1 = saturate_post e1.expr_effect (fst q) q in
      let q1 = filter_post e1.expr_effect (make_post q1) in
      wp_expr env e1 q1
359
  | Efor (x, v1, d, v2, inv, e1) ->
360 361 362
      (* wp(for x = v1 to v2 do inv { I(x) } e1, Q, R) =
             v1 > v2  -> Q
         and v1 <= v2 ->     I(v1)
363
                         and forall S. forall i. v1 <= i <= v2 ->
364 365 366
                                                 I(i) -> wp(e1, I(i+1), R)
	                               and I(v2+1) -> Q                    *)
      let (res, q1), _ = q in
367
      let gt, le, incr = match d with
368 369
	| Pgm_ptree.To     -> env.ls_gt, env.ls_le, t_int_const  "1"
	| Pgm_ptree.Downto -> env.ls_lt, env.ls_ge, t_int_const "-1"
370 371 372
      in
      let v1_gt_v2 = f_app gt [t_var v1; t_var v2] in
      let v1_le_v2 = f_app le [t_var v1; t_var v2] in
373
      let inv = match inv with Some inv -> inv | None -> f_true in
374
      let wp1 =
375
	let xp1 = t_app env.ls_add [t_var x; incr] ty_int in
376 377 378 379 380 381 382 383 384
	let post = f_subst (subst1 x xp1) inv in
	let q1 = saturate_post e1.expr_effect (res, post) q in
	wp_expr env e1 q1
      in
      let f = wp_and ~sym:true
	(f_subst (subst1 x (t_var v1)) inv)
	(quantify env e.expr_effect
	   (wp_and ~sym:true
	      (wp_forall env x
385
	         (wp_implies (wp_and (f_app le [t_var v1; t_var x])
386 387
			             (f_app le [t_var x;  t_var v2]))
                 (wp_implies inv wp1)))
388
	      (let sv2 = t_app env.ls_add [t_var v2; incr] ty_int in
389 390 391
	       wp_implies (f_subst (subst1 x sv2) inv) q1)))
      in
      wp_and ~sym:true (wp_implies v1_gt_v2 q1) (wp_implies v1_le_v2 f)
392

393 394 395
  | Eassert (Pgm_ptree.Aassert, f) ->
      let (_, q), _ = q in
      wp_and f q
396 397
  | Eassert (Pgm_ptree.Acheck, f) ->
      let (_, q), _ = q in
398
      wp_and ~sym:true f q
399 400 401 402 403 404
  | Eassert (Pgm_ptree.Aassume, f) ->
      let (_, q), _ = q in
      wp_implies f q
  | Elabel (lab, e1) ->
      let w1 = wp_expr env e1 q in
      erase_label env lab w1
405
  | Eany c ->
406
      (* TODO: propagate call labels into c.c_post *)
407
      let w = opaque_wp env c.c_effect c.c_post q in
408 409
      let p = f_label_add (label ~loc:e.expr_loc "call pre") c.c_pre in
      wp_and p w
410 411 412 413

and wp_triple env (p, e, q) =
  let f = wp_expr env e q in
  let f = wp_implies p f in
414
  quantify ~all:true env e.expr_effect f
415

416 417
and wp_recfun env (_, bl, _var, t) =
  let f = wp_triple env t in
418
  wp_binders env bl f
419

420
let wp env e =
421
  wp_expr env e (default_post e.expr_type e.expr_effect)
422

423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444
let rec t_btop env t = match t.t_node with
  | Tif (f,t1,t2) -> let f = f_btop env f in
      f_label t.t_label (f_if_simp f (t_btop env t1) (t_btop env t2))
  | Tapp (ls, [t1;t2]) when ls_equal ls env.ls_andb ->
      f_label t.t_label (f_and_simp (t_btop env t1) (t_btop env t2))
  | Tapp (ls, [t1;t2]) when ls_equal ls env.ls_orb ->
      f_label t.t_label (f_or_simp (t_btop env t1) (t_btop env t2))
  | Tapp (ls, [t1]) when ls_equal ls env.ls_notb ->
      f_label t.t_label (f_not_simp (t_btop env t1))
  | Tapp (ls, []) when ls_equal ls env.ls_True ->
      f_label t.t_label f_true
  | Tapp (ls, []) when ls_equal ls env.ls_False ->
      f_label t.t_label f_false
  | _ ->
      f_equ t (t_True env)

and f_btop env f = match f.f_node with
  | Fapp (ls, [{t_ty = {ty_node = Tyapp (ts, [])}} as l; r])
  when ls_equal ls ps_equ && ts_equal ts env.ts_bool ->
      f_label_copy f (f_iff_simp (t_btop env l) (t_btop env r))
  | _ -> f_map (fun t -> t) (f_btop env) f

445
let add_wp_decl l f env =
MARCHE Claude's avatar
MARCHE Claude committed
446 447 448 449 450
  let s = "WP_" ^ l.ls_name.id_string in
  let id = match id_from_user l.ls_name with
    | None -> id_fresh s
    | Some loc -> id_user s loc
  in
451
  let f = f_btop env f in
MARCHE Claude's avatar
MARCHE Claude committed
452
  let pr = create_prsymbol id in
453
  let d = create_prop_decl Pgoal pr f in
454
  add_decl d env
455

456 457
let decl env = function
  | Pgm_ttree.Dlet (ls, e) ->
458
      Debug.dprintf debug "@[--effect %a-----@\n  %a@]@\n----------------@."
459
	  Pretty.print_ls ls print_type_v e.expr_type_v;
460
      let f = wp env e in
461
      Debug.dprintf debug "wp = %a@\n----------------@." Pretty.print_fmla f;
462
      let env = add_wp_decl ls f env in
463
      env
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
464
  | Pgm_ttree.Dletrec dl ->
465 466 467
      let add_one env (ls, def) =
	let f = wp_recfun env def in
	Debug.dprintf debug "wp %a = %a@\n----------------@."
468 469
	    print_ls ls Pretty.print_fmla f;
	add_wp_decl ls f env
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
470
      in
471
      List.fold_left add_one env dl
472
  | Pgm_ttree.Dparam _ ->
473
      env
474

475
(*
476
Local Variables:
477
compile-command: "unset LANG; make -C ../.. testl"
478
End:
479
*)