efficient weakest preconditions

Johannes, Yannick: yes this is what you think (good news)
but this is not yet completed (bad news)

src/whyml/mlw_module.ml

@@ -309,11 +309,16 @@ let add_rec uc { fun_ps = ps } =
 let add_exn uc xs =
   add_symbol add_ps xs.xs_name (XS xs) uc
 
+let if_fast_wp f1 f2 x = if Debug.test_flag Mlw_wp.fast_wp then f1 x else f2 x
+let wp_val = if_fast_wp Mlw_wp.fast_wp_val Mlw_wp.wp_val
+let wp_let = if_fast_wp Mlw_wp.fast_wp_let Mlw_wp.wp_let
+let wp_rec = if_fast_wp Mlw_wp.fast_wp_rec Mlw_wp.wp_rec
+
 let pdecl_vc env km th d = match d.pd_node with
   | PDtype _ | PDdata _ | PDexn _ -> th
-  | PDval lv -> Mlw_wp.wp_val env km th lv
-  | PDlet ld -> Mlw_wp.wp_let env km th ld
-  | PDrec rdl -> Mlw_wp.wp_rec env km th rdl
+  | PDval lv -> wp_val env km th lv
+  | PDlet ld -> wp_let env km th ld
+  | PDrec rdl ->wp_rec env km th rdl
 
 let add_pdecl ~wp uc d =
   let uc = { uc with

src/whyml/mlw_wp.ml

@@ -967,3 +967,176 @@ let wp_rec env km th rdl =
   List.fold_left2 add_one th rdl.rec_defn fl
 
 let wp_val _env _km th _lv = th
+
+(*****************************************************************************)
+
+(* Efficient Weakest Preconditions
+
+  Following Leino, see
+  http://research.microsoft.com/apps/pubs/default.aspx?id=70052
+
+  Roughly, the idea is the following. From a program expression e, we compute
+  two formulas OK and N. Formula OK means ``the execution of e does not go
+  wrong'' and formula N is an input-output relation between initial and
+  final state of e's execution.
+
+  Thus the weakest precondition of e is simply OK.
+  N is involved in recursive computations, e.g.
+  OK(fun x -> {p} e {q}) = forall x. p => OK(e) /\ (forall result. N(e) => q)
+  And so on.
+
+  In practice, this is a bit more involved, since execution of e may raise
+  exceptions. So formula N comes with other formulas E(x), once for each
+  exception x that is possibly raised by e. E(x) is the input-output relation
+  that holds when exception x is raised.
+*)
+
+let fast_wp = Debug.register_flag "fast_wp"
+  ~desc:"Efficient Weakest Preconditions."
+
+module Subst = struct
+
+  type t = unit
+
+  let empty = ()
+
+  let term _s t = t
+
+  let frame _ef s = s
+
+end
+
+let xs_result xs = create_vsymbol (id_fresh "result") (ty_of_ity xs.xs_ity)
+let result e =
+  vs_result e, Mexn.mapi (fun xs _ -> xs_result xs) e.e_effect.eff_raises
+
+let is_vty_unit = function
+  | VTvalue vtv -> ity_equal vtv.vtv_ity ity_unit
+  | VTarrow _   -> false
+
+let map_exns e f = Mexn.mapi (fun xs _ -> f xs) e.e_effect.eff_raises
+
+let wp_nimplies ((n, _), xn) ((result, q), xq) =
+  let f = wp_forall [result] (wp_implies n q) in
+  assert (Mexn.cardinal xn = Mexn.cardinal xq);
+  let x_implies _xs (n, _) (xresult, q) f =
+    wp_forall [xresult] (wp_and ~sym:true f (wp_implies n q)) in
+  Mexn.fold2_inter x_implies xn xq f
+
+(* Input
+   - a state s: Subst.t
+   - names r = (result: vsymbol, xresult: vsymbol Mexn.t)
+   - an expression e
+   with: dom(xresult) = XS, the set of exceptions possibly raised
+                            by a, that is e.e_effect.eff_raises
+
+   Output is a triple (OK, ((NE, s), EX)) where
+   - formula OK means ``e evaluates without any fault''
+     (whatever the execution flow is)
+   - formula NE means
+     ``e terminates normally with final state s and output result''
+   - for each exception x, EX(x) = (fx,sx), where formula fx means
+     ``e raises exception x, with final state sw and value xresult(x) in x''
+*)
+
+let rec fast_wp_expr env s r e =
+  let ok, _ as res = fast_wp_desc env s r e in
+  if Debug.test_flag debug then begin
+    Format.eprintf "@[--------@\n@[<hov 2>e = %a@]@\n" Mlw_pretty.print_expr e;
+    Format.eprintf "@[<hov 2>OK = %a@]@\n" Pretty.print_term ok;
+  end;
+  res
+
+and fast_wp_desc env s r e =
+  let result, xresult = r in
+  match e.e_node with
+  | Elogic t ->
+      (* OK: true
+	 NE: result=t *)
+      let t = wp_label e t in
+      let t = Subst.term s (to_term t) in
+      let ne = if is_vty_unit e.e_vty then t_true else t_equ (t_var result) t in
+      t_true, ((ne, s), Mexn.empty)
+  | Eassert (kind, f) ->
+      (* assert: OK = f    / NE = f    *)
+      (* check : OK = f    / NE = true *)
+      (* assume: OK = true / NE = f    *)
+      let ok = if kind = Aassume then t_true else f in
+      let ne = if kind = Acheck then t_true else f in
+      ok, ((ne, s), Mexn.empty)
+  | Eabstr (_, _, _) -> assert false (*TODO*)
+  | Etry (_, _) -> assert false (*TODO*)
+  | Eraise (_, _) -> assert false (*TODO*)
+  | Efor (_, _, _, _) -> assert false (*TODO*)
+  | Eloop (_, _, _) -> assert false (*TODO*)
+  | Eany _ -> assert false (*TODO*)
+  | Eghost _ -> assert false (*TODO*)
+  | Eassign (_, _, _) -> assert false (*TODO*)
+  | Ecase (_, _) -> assert false (*TODO*)
+  | Eif (_, _, _) -> assert false (*TODO*)
+  | Erec (_, _) -> assert false (*TODO*)
+  | Elet ({ let_sym = LetV v; let_expr = e1 }, e2) ->
+      (* OK: ok(e1) /\ (ne(e1) => ok(e2))
+         NE: ne(e1) /\ ne(e2)
+         Ex: *)
+      let ok1, ((ne1,s1),_ee1) = fast_wp_expr env s (v.pv_vs, xresult) e1 in
+      let ok2, ((ne2,s2),_ee2) = fast_wp_expr env s1 r e2 in
+      let ok = wp_and ~sym:true ok1 (wp_implies ne1 ok2) in
+      let ne = wp_and ~sym:true ne1 ne2 in
+      let ee _xs = t_true, s2 (*TODO*) in
+      ok, ((ne, s2), map_exns e ee)
+  | Elet (_, _) -> assert false (*TODO*)
+  | Eapp (_, _, _) -> assert false (*TODO*)
+  | Earrow _ -> assert false (*TODO*)
+  | Evalue _ -> assert false (*TODO*)
+  | Eabsurd -> assert false (*TODO*)
+
+and fast_wp_fun_defn env lr { fun_ps = ps ; fun_lambda = l } =
+  (* OK: forall bl. pl => ok(e)
+     NE: true *)
+  let lab = fresh_mark () in
+  let add_arg sbs pv = ity_match sbs pv.pv_vtv.vtv_ity pv.pv_vtv.vtv_ity in
+  let subst = List.fold_left add_arg ps.ps_subst l.l_args in
+  let regs = Mreg.map (fun _ -> ()) subst.ity_subst_reg in
+  let args = List.map (fun pv -> pv.pv_vs) l.l_args in
+  let env = if lr = 0 || l.l_variant = [] then env else
+    let lab = t_var lab in
+    let t_at_lab (t,_) = t_app fs_at [t; lab] t.t_ty in
+    let tl = List.map t_at_lab l.l_variant in
+    { env with letrec_var = Mint.add lr tl env.letrec_var }
+  in
+  let q = old_mark lab (wp_expl expl_post l.l_post) in
+  let result, _ as q = open_post q in
+  let conv p = old_mark lab (wp_expl expl_xpost p) in
+  let xq = Mexn.map conv l.l_xpost in
+  let xq = Mexn.map open_post xq in
+  let xresult = Mexn.map fst xq in
+  let ok, n = fast_wp_expr env Subst.empty (result, xresult) l.l_expr in
+  let f = wp_and ~sym:true ok (wp_nimplies n (q, xq)) in
+  let f = wp_implies l.l_pre (erase_mark lab f) in
+  wp_forall args (quantify env regs f)
+
+and fast_wp_rec_defn env { rec_defn = rdl; rec_letrec = lr } =
+  List.map (fast_wp_fun_defn env lr) rdl
+
+let fast_wp_let env km th { let_sym = lv; let_expr = e } =
+  let env = mk_env env km th in
+  let ok, _ = fast_wp_expr env Subst.empty (result e) e in
+  let f = wp_forall (Mvs.keys ok.t_vars) ok in
+  let id = match lv with
+    | LetV pv -> pv.pv_vs.vs_name
+    | LetA ps -> ps.ps_name in
+  add_wp_decl km id f th
+
+let fast_wp_rec env km th rdl =
+  let env = mk_env env km th in
+  let fl = fast_wp_rec_defn env rdl in
+  let add_one th d f =
+    Debug.dprintf debug "wp %s = %a@\n----------------@."
+      d.fun_ps.ps_name.id_string Pretty.print_term f;
+    let f = wp_forall (Mvs.keys f.t_vars) f in
+    add_wp_decl km d.fun_ps.ps_name f th
+  in
+  List.fold_left2 add_one th rdl.rec_defn fl
+
+let fast_wp_val _env _km th _lv = th

src/whyml/mlw_wp.mli

@@ -49,3 +49,13 @@ val full_invariant :
 val wp_val: Env.env -> known_map -> theory_uc -> let_sym  -> theory_uc
 val wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
 val wp_rec: Env.env -> known_map -> theory_uc -> rec_defn -> theory_uc
+
+
+(** Efficient weakest preconditions *)
+
+val fast_wp: Debug.flag
+
+val fast_wp_val: Env.env -> known_map -> theory_uc -> let_sym  -> theory_uc
+val fast_wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
+val fast_wp_rec: Env.env -> known_map -> theory_uc -> rec_defn -> theory_uc
+

tests/test-pgm-jcf.mlw

 module TestGhost
-  use import ref.Ref
-
-  val x: ref int
-  let test1 () =
-    {}
-    ghost x := 0;
-    ()
-    { !x = 0 }
-
-end
-
-module Johannes
-
-  type a = {| mutable f1 : int |}
-  type b =  {| f2 : a |}
-
-  val r1 : a
-  val r2 : b
-
-  let h () =
-    {}
-    let x = r2.f2 in
-    x.f1 <- 5
-    { r2.f2.f1 = 5 }
-
-  let g () =
-    { }
-    let z = {|f2 = r1|} in
-    z.f2.f1 <- 5
-    { r1.f1 = 5 }
-
-end
-
-(*
-module ExcepAndRec
-
-use import int.Int
-
-exception E
-
-let rec f (x:int) : int =
-  if x = 42 then raise E else
-  try
-    let n = f (x-1) in
-    n
-  with E -> 42
-  end
-
-end
-*)
-(*
-module Test
-
-  use import module ref.Ref
-
-  type foo = (ref int, ref int)
-
-  let test_foo (f: foo) =
-    let r = ref 0 in
-    let y = (r, r) in
-    let (x,_) = y in (* local reference would escape its scope *)
-    r
-
-  let test () =
-    let f = ref in
-    let x = f 0 in
-    let y = f 1 in
-    assert { !x = 0 /\ !y = 1 };
-    x := 2;
-    assert { !x = 2 /\ !y = 1 } (* BUG: alias should be detected *)
-
-end
-
-*)
-module M
-
   use import int.Int
-  use import module ref.Ref
-
-  type t 'a 'b = (int, 'a, ('b, int))
-
-  use import list.List
-
-  type tree 'a = E | N (forest 'a)
-  with forest 'b = list (tree 'b)
-
-  inductive even int int int =
-    | even0: even 0 1 2
-  with odd int int =
-    | odd0: odd 1 2
-
-  function c : int = 0b010101010
-
-  function f (x:int) : int = g (x+1)
-  with g (x:int) : int
-
-  predicate p (x:int) = forall y: int. q x y
-  with q (x:int) (y:int) = x >= y
-
-  predicate is_zero (a:int) = a=0
-
-  val foo: x:ref int -> unit
-
-  let test1 () =
-    let x = ref 0 in
-    while is_zero !x do variant { !x } () done
-
-(*
-  use import option.Option
-
-  val clear (o : option (ref int)) :
-    {}
-    unit writes (match o with Some r -> r end).contents
-    { match o with None -> true | Some r -> !r = 0 end }
-*)
-
-  (* BUG: x escapes its scope (in the postcondition) => should be an error *)
-  (* let scope (a: ref int) = let x = a in fun () -> {} x := 0 { !x = 0 } *)
+  use import ref.Ref
 
-  (* let foo (a: ref int) = let x = a in fun () -> {} x := 0 { !a = 0 } *)
-  (* let test3 () = let x = ref 0 in begin foo x (); assert { !x = 0 } end *)
+  let test1 (x: int) =
+    { x = 40 }
+    assert { x > 0 };
+    x+2
+    { result = 42 }
 
 end
 
 
-module CodeAnnotations
-
-  use import int.Int
-  use import module ref.Ref
-
-  let f (x:int) : int =
-    { }
-    let y = ref 0 in
-    abstract y := !y + 1 { !y > 0 };
-    !y
-    { result = 1 (* should not be proved !*) }
-
-end
-
 
 (*
 Local Variables: