pgm_wp.ml 14.1 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
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
30
open Pgm_itree
31
open Pgm_typing
32
open Pgm_types
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
33 34 35

module E = Pgm_effect

36 37
let debug = ref false

38 39 40 41 42 43 44 45
(* phase 3: translation to intermediate trees and effect inference **********)

let reference_of_term t = match t.t_node with
  | Tvar vs -> E.Rlocal vs
  | Tapp (ls, []) -> E.Rglobal ls
  | _ -> assert false

let rec term_effect env ef t = match t.t_node with
46
  | Tapp (ls, [t]) when ls_equal ls env.ls_bang ->
47 48 49 50 51
      let r = reference_of_term t in
      E.add_read r ef
  | _ ->
      t_fold (term_effect env) (fmla_effect env) ef t

52 53 54 55 56 57
and fmla_effect env ef f =
  f_fold (term_effect env) (fmla_effect env) ef f

let post_effect env ef ((_,q),ql) =
  let exn_effect ef (_,(_,q)) = fmla_effect env ef q in
  List.fold_left exn_effect (fmla_effect env ef q) ql
58 59 60 61

let add_binder env (x, v) = add_local x v env
let add_binders = List.fold_left add_binder

62 63 64 65 66 67 68
let make_apply loc e1 ty c =
  let x = create_vsymbol (id_fresh "f") e1.expr_type in
  let v = c.c_result_type and ef = c.c_effect in
  let any_c = { expr_desc = Eany c; expr_type = ty;
		expr_type_v = v; expr_effect = ef; expr_loc = loc } in
  Elet (x, e1, any_c), v, ef

69
let rec expr env e =
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
70 71
  let ty = e.Pgm_ttree.expr_type in
  let loc = e.Pgm_ttree.expr_loc in
72
  let d, v, ef = expr_desc env loc ty e.Pgm_ttree.expr_desc in
73 74
  { expr_desc = d; expr_type = ty; 
    expr_type_v = v; expr_effect = ef; expr_loc = loc }
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
75

76
and expr_desc env loc ty = function
77
  | Pgm_ttree.Elogic t ->
78 79 80 81 82 83 84 85
      let ef = term_effect env E.empty t in
      Elogic t, Tpure ty, ef
  | Pgm_ttree.Elocal vs ->
      assert (Mvs.mem vs env.locals);
      Elocal vs, Mvs.find vs env.locals, E.empty
  | Pgm_ttree.Eglobal ls ->
      assert (Mls.mem ls env.globals);
      Eglobal ls, Mls.find ls env.globals, E.empty
86 87 88
  | Pgm_ttree.Eapply (e1, vs) ->
      let e1 = expr env e1 in
      let c = apply_type_v env e1.expr_type_v vs in
89
      make_apply loc e1 ty c
90 91 92
  | Pgm_ttree.Eapply_ref (e1, r) ->
      let e1 = expr env e1 in
      let c = apply_type_v_ref env e1.expr_type_v r in
93
      make_apply loc e1 ty c
94
  | Pgm_ttree.Efun (bl, t) ->
95 96 97
      let env = add_binders env bl in
      let t, c = triple env t in
      Efun (bl, t), Tarrow (bl, c), E.empty
98
  | Pgm_ttree.Elet (v, e1, e2) ->
99
      let e1 = expr env e1 in
100
      let env = add_local v e1.expr_type_v env in
101 102
      let e2 = expr env e2 in
      let ef = E.union e1.expr_effect e2.expr_effect in
103
      Elet (v, e1, e2), e2.expr_type_v, ef
104 105
  | Pgm_ttree.Eletrec _ ->
      assert false (*TODO*)
106 107 108 109 110 111

  | Pgm_ttree.Esequence (e1, e2) ->
      let e1 = expr env e1 in
      let e2 = expr env e2 in
      let ef = E.union e1.expr_effect e2.expr_effect in
      Esequence (e1, e2), e2.expr_type_v, ef
112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
  | Pgm_ttree.Eif (e1, e2, e3) ->
      let e1 = expr env e1 in
      let e2 = expr env e2 in
      let e3 = expr env e3 in
      let ef = E.union e1.expr_effect e2.expr_effect in
      let ef = E.union ef             e3.expr_effect in
      if not (eq_type_v e2.expr_type_v e3.expr_type_v) then
	errorm ~loc "cannot branch on functions";
      Eif (e1, e2, e3), e2.expr_type_v, ef
  | Pgm_ttree.Eloop (a, e1) ->
      let e1 = expr env e1 in
      let ef = e1.expr_effect in
      let ef = match a.loop_invariant with
	| Some f -> fmla_effect env ef f
	| None -> ef
      in
      let ef = match a.loop_variant with
	| Some (t, _) -> term_effect env ef t
	| None -> ef
      in
      Eloop (a, e1), type_v_unit env, ef
133 134 135 136 137 138 139 140
  | Pgm_ttree.Elazy _ ->
      assert false (*TODO*)
  | Pgm_ttree.Ematch _ ->
      assert false (*TODO*)
  | Pgm_ttree.Eskip ->
      Eskip, Tpure ty, E.empty
  | Pgm_ttree.Eabsurd ->
      assert false (*TODO*)
141 142 143 144 145 146 147 148
  | Pgm_ttree.Eraise (x, e1) ->
      let e1 = option_map (expr env) e1 in
      let ef = match e1 with Some e1 -> e1.expr_effect | None -> E.empty in
      let ef = E.add_raise x ef in
      Eraise (x, e1), Tpure ty, ef
  | Pgm_ttree.Etry (_e1, _hl) ->
      assert false (* TODO *)
      (*Etry (e1, hl), Tpure ty, ef*)
149 150 151 152

  | Pgm_ttree.Eassert (k, f) ->
      let ef = fmla_effect env E.empty f in
      Eassert (k, f), Tpure ty, ef
153 154 155
  | Pgm_ttree.Elabel (lab, e1) ->
      let e1 = expr env e1 in
      Elabel (lab, e1), e1.expr_type_v, e1.expr_effect
156
  | Pgm_ttree.Eany _ ->
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
157 158
      assert false (*TODO*)

159 160
and triple env (p, e, q) =
  let e = expr env e in
161 162
  let ef = post_effect env (fmla_effect env e.expr_effect p) q in
  let e = { e with expr_effect = ef } in
163 164
  let c = 
    { c_result_type = e.expr_type_v;
165
      c_effect      = ef;
166 167 168 169 170
      c_pre         = p;
      c_post        = q }
  in
  (p, e, q), c

171
and recfun _env _def =
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
172 173
  assert false (*TODO*)

174 175
(* phase 4: weakest preconditions *******************************************)

176 177 178 179 180 181 182
(* 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) 

183 184 185
let wp_ands ?(sym=false) fl =
  List.fold_left (wp_and ~sym) f_true fl

186 187 188 189
let wp_implies = f_implies_simp
let wp_forall  = f_forall_simp

(* utility functions for building WPs *)
190

191
let fresh_label env =
192
  let ty = ty_app env.ts_label [] in
193
  create_vsymbol (id_fresh "label") ty
194

195
let wp_binder (x, tv) f = match tv with
196
  | Tpure _ -> wp_forall [x] [] f
197 198 199 200
  | Tarrow _ -> f

let wp_binders = List.fold_right wp_binder 

201 202 203
(* 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
204

205
and old_label_term env lab t = match t.t_node with
206
  | Tapp (ls, [t]) when ls_equal ls env.ls_old ->
207
      let t = old_label_term env lab t in (* NECESSARY? *)
208
      t_app env.ls_at [t; t_var lab] t.t_ty
209 210 211 212 213
  | _ ->
      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 =
214
  f_map (erase_label_term env lab) (erase_label env lab) f
215 216 217

and erase_label_term env lab t = match t.t_node with
  | Tapp (ls, [t; {t_node = Tvar l}]) 
218
    when ls_equal ls env.ls_at && vs_equal l lab ->
219 220 221 222 223
      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
224
  | Tyapp (ts, [ty]) when ts_equal ts env.ts_ref -> ty
225 226
  | _ -> assert false

227 228 229 230
let is_ref_ty env ty = match ty.ty_node with
  | Tyapp (ts, [_]) -> ts_equal ts env.ts_ref
  | _ -> false

231 232 233 234 235
(* 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
236 237
  | Tapp (ls, [u]) when ls_equal ls env.ls_bang ->
      let rt = reference_of_term u in
238
      if E.ref_equal rt r then t_var v else t
239
  | Tapp (ls, _) when ls_equal ls env.ls_old ->
240
      assert false
241
  | Tapp (ls, _) when ls_equal ls env.ls_at -> (* do not recurse in at(...) *)
242 243 244 245 246 247
      t 
  | _ ->
      t_map (unref_term env r v) (unref env r v) t

(* quantify over all references in ef *)
let quantify env ef f =
248
  (* eprintf "quantify: ef=%a f=%a@." E.print ef Pretty.print_fmla f; *)
249 250 251
  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
252 253
    let f = unref env r v f in
    wp_forall [v] [] f
254 255 256 257
  in
  let s = E.Sref.union ef.E.reads ef.E.writes in
  E.Sref.fold quantify1 s f

258 259
let abstract_wp env ef (q',ql') (q,ql) =
  assert (List.length ql' = List.length ql);
260
  let quantify_res f' f res =
261
    let f = wp_implies f' f in
262 263 264 265 266
    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 -> 
267
	  wp_forall [v] [] f
268 269 270
      | None -> 
	  f 
    in
271 272 273 274 275
    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
276
      | Some v', Some v -> Some v, f_subst (subst1 v' (t_var v)) f'
277 278 279
      | None, None -> None, f'
      | _ -> assert false
    in
280
    quantify_res f' f res
281 282 283
  in
  let f = 
    let res, f = q and res', f' = q' in
284
    let f' = f_subst (subst1 res' (t_var res)) f' in
285
    quantify_res f' f (Some res)
286 287 288 289 290 291 292 293 294
  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

295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320
(*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)

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

321
let saturate_post ef q (_, ql) = 
322 323
  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
324
  (q, List.map set_post xs)
325

326 327
(* Recursive computation of the weakest precondition *)

328
let rec wp_expr env e q = 
329 330
(*   if !debug then  *)
(*     eprintf "@[wp_expr: q=%a@]@." Pretty.print_fmla (snd (fst q)); *)
331 332 333
  let lab = fresh_label env in
  let q = post_map (old_label env lab) q in
  let f = wp_desc env e q in
334 335
  let f = erase_label env lab f in
  f
336 337

and wp_desc env e q = match e.expr_desc with
338
  | Elogic t ->
339 340
      let (v, q), _ = q in
      f_let v t q
341 342 343
  | Elocal _ ->
      assert false (*TODO*)
  | Eglobal _ ->
344
      let (_, q), _ = q in q
345
  | Efun (bl, t) ->
346
      let (_, q), _ = q in
347 348
      let f = wp_triple env t in
      wp_and q (wp_binders bl f)
349 350 351
  | 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
352
      let q1 = result, f_subst (subst1 x (t_var result)) w2 in
353 354
      let q1 = saturate_post e1.expr_effect q1 q in
      wp_expr env e1 q1
355 356
  | Eletrec _ ->
      assert false (*TODO*)
357 358 359

  | Esequence (e1, e2) ->
      let w2 = wp_expr env e2 (filter_post e2.expr_effect q) in
360
      let q1 = saturate_post e1.expr_effect (v_result e1.expr_type, w2) q in
361
      wp_expr env e1 q1
362 363 364 365 366 367 368 369 370 371 372
  | 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
  | Eloop _ ->
373 374 375 376 377 378 379 380 381 382 383 384 385
      assert false (*TODO*)
  | Elazy _ ->
      assert false (*TODO*)
  | Ematch _ ->
      assert false (*TODO*)
  | Eskip ->
      let (_, q), _ = q in q
  | Eabsurd ->
      assert false (*TODO*)
  | Eraise _ ->
      assert false (*TODO*)
  | Etry _ ->
      assert false (*TODO*)
386 387 388 389

  | Eassert (Pgm_ptree.Aassert, f) ->
      let (_, q), _ = q in
      wp_and f q
390 391
  | Eassert (Pgm_ptree.Acheck, f) ->
      let (_, q), _ = q in
392
      wp_and ~sym:true f q
393 394 395 396 397 398
  | 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
399 400 401
  | Eany c ->
      let w = opaque_wp env c.c_effect c.c_post q in
      wp_and c.c_pre w
402

403
  | _ -> 
404
      assert false (*TODO*)
405

406 407 408 409
and wp_triple env (p, e, q) =
  let f = wp_expr env e q in
  let f = wp_implies p f in
  quantify env e.expr_effect f
410

411
let wp env e = 
412
  wp_expr env e (default_post e.expr_type e.expr_effect)
413

414
let wp_recfun _env _l _def = f_true (* TODO *)
415

416
let add_wp_decl l f env =
417 418
  let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
  let d = create_prop_decl Pgoal pr f in
419
  add_decl d env
420

421 422 423
let decl env = function
  | Pgm_ttree.Dlet (ls, e) ->
      let e = expr env e in
424 425 426
      if !debug then
	eprintf "@[--effect %a-----@\n  %a@]@\n----------------@."
	  Pretty.print_ls ls print_type_v e.expr_type_v;
427
      let f = wp env e in
428 429 430
      if !debug then
	eprintf "wp = %a@\n----------------@." Pretty.print_fmla f;
      let env = add_wp_decl ls f env in	
431 432
      let env = add_global ls e.expr_type_v env in
      env
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
433
  | Pgm_ttree.Dletrec dl ->
434 435 436 437 438 439 440
      let add_one env (ls, def) = 
	let def = recfun env def in
	let f = wp_recfun env ls def in 
	let env = add_wp_decl ls f env in
	let v = assert false (*TODO*) in
	let env = add_global ls v env in
	env
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
441
      in
442 443 444 445
      List.fold_left add_one env dl
  | Pgm_ttree.Dparam (ls, v) ->
      let env = add_global ls v env in
      env
446 447

let file uc dl =
448 449
  let env = List.fold_left decl (empty_env uc) dl in
  Theory.close_theory env.uc
450 451 452 453 454 455

(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. testl"
End: 
*)