pgm_wp.ml 12.2 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
(* smart constructors for building WPs
   TODO: use simp forms / tag with label "WP" *)

let wp_and ?(sym=false) f1 f2 = 
42 43 44
(*   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
  if sym then f else f_label [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 52
let wp_implies = f_implies_simp
let wp_forall  = f_forall_simp

(* utility functions for building WPs *)
53

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

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

let wp_binders = List.fold_right wp_binder 

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

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

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

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

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

(* quantify over all references in ef *)
110
let quantify ?(all=false) env ef f =
111
  (* eprintf "quantify: ef=%a f=%a@." E.print ef Pretty.print_fmla f; *)
112 113 114
  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
115 116
    let f = unref env r v f in
    wp_forall [v] [] f
117
  in
118 119
  let s = ef.E.writes in
  let s = if all then E.Sref.union ef.E.reads s else s in
120 121
  E.Sref.fold quantify1 s f

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

159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
(*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)

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

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

190
let saturate_post ef q (_, ql) = 
191 192
  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
193
  (q, List.map set_post xs)
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 235
(* 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], []) *)


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

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

and wp_desc env e q = match e.expr_desc with
247
  | Elogic t ->
248 249
      let (v, q), _ = q in
      f_let v t q
250 251 252
  | Elocal v ->
      let (res, q), _ = q in
      f_subst (subst1 res (t_var v)) q
253
  | Eglobal _ ->
254
      let (_, q), _ = q in q
255
  | Efun (bl, t) ->
256
      let (_, q), _ = q in
257 258
      let f = wp_triple env t in
      wp_and q (wp_binders bl f)
259 260 261
  | 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
262
      let q1 = result, f_subst (subst1 x (t_var result)) w2 in
263 264
      let q1 = saturate_post e1.expr_effect q1 q in
      wp_expr env e1 q1
265 266 267 268
  | 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)
269 270 271

  | Esequence (e1, e2) ->
      let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
272
      let q1 = saturate_post e1.expr_effect (v_result e1.expr_type, w2) q in
273
      wp_expr env e1 q1
274 275 276 277 278 279 280 281 282 283
  | 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
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
  | 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
301 302 303 304
  | Ematch (xl, bl) ->
      let branch (p, e) = p, wp_expr env e (filter_post e.expr_effect q) in
      let tl = List.map t_var xl in
      f_case tl (List.map branch bl)
305 306 307
  | Eskip ->
      let (_, q), _ = q in q
  | Eabsurd ->
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 337 338 339
      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
340 341 342 343

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

357
  | Eghost _ ->
358
      assert false (*TODO*)
359

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

365 366 367 368
and wp_recfun env (_, bl, _var, t) =
  let f = wp_triple env t in
  wp_binders bl f

369
let wp env e = 
370
  wp_expr env e (default_post e.expr_type e.expr_effect)
371

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

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

399 400 401 402 403
(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. testl"
End: 
*)