pgm_wp.ml 8.69 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 Ident
23
open Ty
24 25 26
open Term
open Decl
open Theory
27
open Pgm_ttree
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
28
open Pgm_itree
29
open Pgm_typing
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
30 31 32

module E = Pgm_effect

33 34 35 36 37
type env = {
  uc      : theory_uc;
  globals : type_v Mls.t;
  locals  : type_v Mvs.t;
}
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
38

39 40 41
let empty_env uc = { uc = uc; globals = Mls.empty; locals = Mvs.empty }
let add_local x v env = { env with locals = Mvs.add x v env.locals }
let add_global x v env = { env with globals = Mls.add x v env.globals }
42

43
let ts_ref   env = ns_find_ts (get_namespace env.uc) ["ref"]
44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
let ts_label env = ns_find_ts (get_namespace env.uc) ["label"]

let ls_bang env = ns_find_ls (get_namespace env.uc) ["prefix !"]

(* 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
  | Tapp (ls, [t]) when ls_equal ls (ls_bang env) ->
      let r = reference_of_term t in
      E.add_read r ef
  | _ ->
      t_fold (term_effect env) (fmla_effect env) ef t

and fmla_effect _env _ef _f =
  assert false (*TODO*)

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

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

74
and expr_desc env _loc ty = function
75
  | Pgm_ttree.Elogic t ->
76 77 78 79 80 81 82 83
      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
84
  | Pgm_ttree.Eapply _ ->
85
      assert false (*TODO*)
86 87 88
  | Pgm_ttree.Eapply_ref _ ->
      assert false (*TODO*)
  | Pgm_ttree.Efun (bl, t) ->
89 90 91
      let env = add_binders env bl in
      let t, c = triple env t in
      Efun (bl, t), Tarrow (bl, c), E.empty
92
  | Pgm_ttree.Elet (v, e1, e2) ->
93 94 95 96
      let e1 = expr env e1 in
      let env = { env with locals = Mvs.add v e1.expr_type_v env.locals } in
      let e2 = expr env e2 in
      let ef = E.union e1.expr_effect e2.expr_effect in
97
      Elet (v, e1, e2), e2.expr_type_v, ef
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
98 99 100
  | _ -> 
      assert false (*TODO*)

101 102
and triple env (p, e, q) =
  let e = expr env e in
103 104 105 106 107 108 109 110
  let c = 
    { c_result_type = e.expr_type_v;
      c_effect      = e.expr_effect;
      c_pre         = p;
      c_post        = q }
  in
  (p, e, q), c

111
and recfun _env _def =
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
112 113
  assert false (*TODO*)

114 115
(* phase 4: weakest preconditions *******************************************)

116 117 118 119 120
(* TODO: use simp forms / tag with label "WP" *)
let wp_and     = f_and
let wp_implies = f_implies
let wp_forall  = f_forall

121 122
module State : sig
  type t
123 124
  val create     : env -> E.t -> t
  val push_label : env -> ?label:label -> t -> label * t
125 126 127 128 129 130 131 132 133 134 135
  val havoc      : env -> ?pre:label -> E.t   -> t -> t
  val term       : env ->               t -> term -> term
  val fmla       : env -> ?old:label -> t -> fmla -> fmla
  val quantify   : env -> t -> E.t -> fmla -> fmla
end = struct

  type t = {
    current : vsymbol E.Mref.t;
    old     : vsymbol E.Mref.t Mvs.t;
  }

136 137 138 139 140 141 142 143 144 145 146 147 148 149
  let unref_ty env ty = match ty.ty_node with
    | Tyapp (ts, [ty]) when ts_equal ts (ts_ref env) -> ty
    | _ -> assert false

  let var_of_reference env = function
    | E.Rlocal vs -> 
	create_vsymbol (id_fresh vs.vs_name.id_string) (unref_ty env vs.vs_ty)
    | E.Rglobal { ls_name = id; ls_value = Some ty } -> 
	create_vsymbol (id_fresh id.id_string) (unref_ty env ty)
    | E.Rglobal { ls_value = None } ->
	assert false

  let havoc1 env r m =
    let v = var_of_reference env r in
150 151
    E.Mref.add r v m

152
  let create env ef = 
153
    let s = E.Sref.union ef.E.reads ef.E.writes in
154
    { current = E.Sref.fold (havoc1 env) s E.Mref.empty; old = Mvs.empty; }
155 156

  let fresh_label env =
157
    let ty = ty_app (ts_label env) [] in
158 159 160 161 162 163 164
    create_vsymbol (id_fresh "label") ty

  let havoc env ?pre ef s = 
    let l = match pre with
      | None -> fresh_label env
      | Some l -> l
    in
165
    { current = E.Sref.fold (havoc1 env) ef.E.writes s.current;
166 167
      old = Mvs.add l s.current s.old; }

168 169 170
  let push_label env ?label s = 
    let l = match label with None -> fresh_label env | Some l -> l in
    l, havoc env ~pre:l E.empty s
171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193

  let ref_at cur s r = 
    let m = match cur with
      | None -> s.current
      | Some l -> assert (Mvs.mem l s.old); Mvs.find l s.old
    in
    assert (E.Mref.mem r m);
    E.Mref.find r m

  (* old = label for old state,     if any
     cur = label for current state, if any *)
  let rec term_at env old cur s t = match t.t_node with
    | Tapp (ls, [t]) when ls_equal ls (ls_bang env) ->
	let r = reference_of_term t in
	t_var (ref_at cur s r)
    (* TODO: old, at *)
    | _ ->
	t_map (term_at env old cur s) (fmla_at env old cur s) t

  and fmla_at env old cur s f = 
    f_map (term_at env old cur s) (fmla_at env old cur s) f

  let term env      s t = term_at env None None s t
194
  let fmla env ?old s f = fmla_at env old  None s f
195

196 197 198 199
  let quantify _env s ef f = 
    let quant r f = wp_forall [ref_at None s r] [] f in
    let s = E.Sref.union ef.E.reads ef.E.writes in
    E.Sref.fold quant s f
200 201 202 203 204

  let print _fmt _s = assert false (*TODO*)

end

205
let wp_binder (x, tv) f = match tv with
206
  | Tpure _ -> wp_forall [x] [] f
207 208 209 210
  | Tarrow _ -> f

let wp_binders = List.fold_right wp_binder 

211 212 213 214
let get_normal_post env s = function
  | _, None -> f_true 
  | old, Some ((_,q),_) -> State.fmla env ~old s q

215
let rec wp_expr env s e q = match e.expr_desc with
216
  | Elogic t ->
217 218
      let t = State.term env s t in
      begin match q with
219 220 221 222 223
	| old, Some ((v,q),_) ->
	    let q = State.fmla env ~old s q in
	    f_let v t q
	| _, None -> 
	    f_true
224 225
      end
  | Efun (bl, t) ->
226 227 228
      let q = get_normal_post env s q in
      let f = wp_triple env t in
      wp_and q (wp_binders bl f)
229 230
  | _ -> 
      f_true (* TODO *)
231

232 233 234 235 236 237
and wp_triple env (p,e,q) =
  let s = State.create env e.expr_effect in
  let old, s = State.push_label env s in
  let f = wp_expr env s e (old, Some q) in
  let f = wp_implies (State.fmla env s p) f in
  State.quantify env s e.expr_effect f
238

239 240 241 242
let wp env e = 
  let s = State.create env e.expr_effect in
  let old, s = State.push_label env s in
  wp_expr env s e (old, None)
243

244
let wp_recfun _env _l _def = f_true (* TODO *)
245

246
let add_wp_decl l f env =
247 248
  let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
  let d = create_prop_decl Pgoal pr f in
249
  { env with uc = add_decl env.uc d }
250

251 252 253
let decl env = function
  | Pgm_ttree.Dlet (ls, e) ->
      let e = expr env e in
254
      (* DEBUG *)
255
      eprintf "@[--effect %a-----@\n  %a@]@\n---------@." 
256
	Pretty.print_ls ls print_type_v e.expr_type_v;
257
      let f = wp env e in
258 259 260
      let env = add_wp_decl ls f env in
      let env = add_global ls e.expr_type_v env in
      env
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
261
  | Pgm_ttree.Dletrec dl ->
262 263 264 265 266 267 268
      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
269
      in
270 271 272 273
      List.fold_left add_one env dl
  | Pgm_ttree.Dparam (ls, v) ->
      let env = add_global ls v env in
      env
274 275

let file uc dl =
276 277
  let env = List.fold_left decl (empty_env uc) dl in
  Theory.close_theory env.uc
278 279 280 281 282 283

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