pgm_wp.ml 12 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 35
let debug = ref false

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

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

let wp_and ?(sym=false) f1 f2 = 
  (* TODO: tag instead? *)
  if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2) 

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

48 49 50 51
let wp_implies = f_implies_simp
let wp_forall  = f_forall_simp

(* utility functions for building WPs *)
52

53
let fresh_label env =
54
  let ty = ty_app env.ts_label [] in
55
  create_vsymbol (id_fresh "label") ty
56

57
let wp_binder (x, tv) f = match tv with
58
  | Tpure _ -> wp_forall [x] [] f
59 60 61 62
  | Tarrow _ -> f

let wp_binders = List.fold_right wp_binder 

63 64 65
(* 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
66

67
and old_label_term env lab t = match t.t_node with
68
  | Tapp (ls, [t]) when ls_equal ls env.ls_old ->
69
      let t = old_label_term env lab t in (* NECESSARY? *)
70
      t_app env.ls_at [t; t_var lab] t.t_ty
71 72 73 74 75
  | _ ->
      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 =
76
  f_map (erase_label_term env lab) (erase_label env lab) f
77 78 79

and erase_label_term env lab t = match t.t_node with
  | Tapp (ls, [t; {t_node = Tvar l}]) 
80
    when ls_equal ls env.ls_at && vs_equal l lab ->
81 82 83 84 85
      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
86
  | Tyapp (ts, [ty]) when ts_equal ts env.ts_ref -> ty
87 88
  | _ -> assert false

89 90 91 92
let is_ref_ty env ty = match ty.ty_node with
  | Tyapp (ts, [_]) -> ts_equal ts env.ts_ref
  | _ -> false

93 94 95 96 97
(* 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
98
  | Tapp (ls, [u]) when ls_equal ls env.ls_bang ->
99
      let rt = E.reference_of_term u in
100
      if E.ref_equal rt r then t_var v else t
101
  | Tapp (ls, _) when ls_equal ls env.ls_old ->
102
      assert false
103
  | Tapp (ls, _) when ls_equal ls env.ls_at -> (* do not recurse in at(...) *)
104 105 106 107 108
      t 
  | _ ->
      t_map (unref_term env r v) (unref env r v) t

(* quantify over all references in ef *)
109
let quantify ?(all=false) env ef f =
110
  (* eprintf "quantify: ef=%a f=%a@." E.print ef Pretty.print_fmla f; *)
111 112 113
  let quantify1 r f = 
    let ty = unref_ty env (E.type_of_reference r) in
    let v = create_vsymbol (id_clone (E.name_of_reference r)) ty in
114 115
    let f = unref env r v f in
    wp_forall [v] [] f
116
  in
117 118
  let s = ef.E.writes in
  let s = if all then E.Sref.union ef.E.reads s else s in
119 120
  E.Sref.fold quantify1 s f

121 122
let abstract_wp env ef (q',ql') (q,ql) =
  assert (List.length ql' = List.length ql);
123
  let quantify_res f' f res =
124
    let f = wp_implies f' f in
125 126 127 128 129
    let f = match res with 
      | Some v when is_ref_ty env v.vs_ty -> 
	  let v' = create_vsymbol (id_clone v.vs_name) (unref_ty env v.vs_ty) in
	  wp_forall [v'] [] (unref env (E.Rlocal v) v' f)
      | Some v -> 
130
	  wp_forall [v] [] f
131 132 133
      | None -> 
	  f 
    in
134 135 136 137 138
    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
139
      | Some v', Some v -> Some v, f_subst (subst1 v' (t_var v)) f'
140 141 142
      | None, None -> None, f'
      | _ -> assert false
    in
143
    quantify_res f' f res
144 145 146
  in
  let f = 
    let res, f = q and res', f' = q' in
147
    let f' = f_subst (subst1 res' (t_var res)) f' in
148
    quantify_res f' f (Some res)
149 150 151 152 153 154 155 156 157
  in
  wp_ands (f :: List.map2 quantify_h ql' ql)

let opaque_wp env ef q' q = 
  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

158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
(*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 exn_v_result ls = match ls.ls_args with
  | [] -> None
  | [ty] -> Some (v_result ty)
  | _ -> assert false

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

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

181 182 183 184 185
let rec assoc_handler x = function
  | [] -> assert false
  | (y, h) :: _ when ls_equal x y -> h
  | _ :: hl -> assoc_handler x hl

186 187 188
(*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] *)

189
let saturate_post ef q (_, ql) = 
190 191
  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
192
  (q, List.map set_post xs)
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 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234
(* 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
  q, List.map2 supx ql ql' 

(* 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
 
let term_at env lab t =
  t_app env.ls_at [t; t_var lab] t.t_ty

let while_post_block env inv var lab e = 
  let decphi = match var with
    | None -> 
	f_true
    | Some (phi, r) -> 
	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
    | None -> 
	(res, decphi), ql
    | Some i -> 
	(res, wp_and i decphi), ql

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


235 236
(* Recursive computation of the weakest precondition *)

237
let rec wp_expr env e q = 
238 239
  (* if !debug then  *)
  (*   eprintf "@[wp_expr: q=%a@]@." Pretty.print_fmla (snd (fst q)); *)
240 241 242
  let lab = fresh_label env in
  let q = post_map (old_label env lab) q in
  let f = wp_desc env e q in
243
  erase_label env lab f
244 245

and wp_desc env e q = match e.expr_desc with
246
  | Elogic t ->
247 248
      let (v, q), _ = q in
      f_let v t q
249 250 251
  | Elocal v ->
      let (res, q), _ = q in
      f_subst (subst1 res (t_var v)) q
252
  | Eglobal _ ->
253
      let (_, q), _ = q in q
254
  | Efun (bl, t) ->
255
      let (_, q), _ = q in
256 257
      let f = wp_triple env t in
      wp_and q (wp_binders bl f)
258 259 260
  | Elet (x, e1, e2) ->
      let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
      let result = v_result e1.expr_type in
261
      let q1 = result, f_subst (subst1 x (t_var result)) w2 in
262 263
      let q1 = saturate_post e1.expr_effect q1 q in
      wp_expr env e1 q1
264 265 266 267
  | Eletrec (dl, e1) ->
      let w1 = wp_expr env e1 q in
      let wl = List.map (wp_recfun env) dl in 
      wp_ands ~sym:true (w1 :: wl)
268 269 270

  | Esequence (e1, e2) ->
      let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
271
      let q1 = saturate_post e1.expr_effect (v_result e1.expr_type, w2) q in
272
      wp_expr env e1 q1
273 274 275 276 277 278 279 280 281 282
  | 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
	let q1 = f_if test w2 w3 in
	saturate_post e1.expr_effect (res, q1) q
      in
      wp_expr env e1 q1
283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
  | 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
300 301 302 303 304
  | Ematch _ ->
      assert false (*TODO*)
  | Eskip ->
      let (_, q), _ = q in q
  | Eabsurd ->
305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336
      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
	| Some v, r -> (v, r), ql 
	| 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))$ *)
      let hwl = 
	List.map 
	  (fun (x, v, h) -> 
	     let w = wp_expr env h (filter_post h.expr_effect q) in
	     x, (v, w))
	  hl 
      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
337 338 339 340

  | Eassert (Pgm_ptree.Aassert, f) ->
      let (_, q), _ = q in
      wp_and f q
341 342
  | Eassert (Pgm_ptree.Acheck, f) ->
      let (_, q), _ = q in
343
      wp_and ~sym:true f q
344 345 346 347 348 349
  | 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
350 351 352
  | Eany c ->
      let w = opaque_wp env c.c_effect c.c_post q in
      wp_and c.c_pre w
353

354
  | Eghost _ ->
355
      assert false (*TODO*)
356

357 358 359
and wp_triple env (p, e, q) =
  let f = wp_expr env e q in
  let f = wp_implies p f in
360
  quantify ~all:true env e.expr_effect f
361

362 363 364 365
and wp_recfun env (_, bl, _var, t) =
  let f = wp_triple env t in
  wp_binders bl f

366
let wp env e = 
367
  wp_expr env e (default_post e.expr_type e.expr_effect)
368

369
let add_wp_decl l f env =
370 371
  let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
  let d = create_prop_decl Pgoal pr f in
372
  add_decl d env
373

374 375
let decl env = function
  | Pgm_ttree.Dlet (ls, e) ->
376 377 378
      if !debug then
	eprintf "@[--effect %a-----@\n  %a@]@\n----------------@."
	  Pretty.print_ls ls print_type_v e.expr_type_v;
379
      let f = wp env e in
380 381 382
      if !debug then
	eprintf "wp = %a@\n----------------@." Pretty.print_fmla f;
      let env = add_wp_decl ls f env in	
383
      env
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
384
  | Pgm_ttree.Dletrec dl ->
385
      let add_one env (ls, def) = 
386 387 388 389 390
	let f = wp_recfun env def in 
	if !debug then
	  eprintf "wp %a = %a@\n----------------@." 
	    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
391
      in
392
      List.fold_left add_one env dl
393
  | Pgm_ttree.Dparam _ ->
394
      env
395

396 397 398 399 400
(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. testl"
End: 
*)