fixed WP for local functions

no more need for 'globals' field in effects

bench/programs/good/scopes.mlw

+
+module LocalFunctions
+
+  use import int.Int
+  use import module ref.Ref
+
+  (* local function (f) accessing a local reference (x) *)
+  let test1 () =
+    let x = ref 0 in
+    let f (y: int) = {} x := !x + y { !x = old !x + y } in
+    f 2;
+    assert { !x = 2 }
+
+  parameter r: ref int
+
+  (* recursive function accessing a global reference *)
+  let rec test2 () =
+    { }
+    r := 0
+    { !r = 0 }
+
+end
+
+(*
+Local Variables:
+compile-command: "unset LANG; make -C ../../.. bench/programs/good/scopes"
+End:
+*)

modules/ref.mlw

@@ -22,9 +22,11 @@ module Refint
   use export int.Int
   use export module Ref
 
-  parameter incr : r:ref int -> {} unit writes r { !r = old !r + 1 }
+  (* parameter incr : r:ref int -> {} unit writes r { !r = old !r + 1 } *)
+  let incr (r:ref int) = {} r := !r + 1 { !r = old !r + 1 }
 
-  parameter decr : r:ref int -> {} unit writes r { !r = old !r - 1 }
+  (* parameter decr : r:ref int -> {} unit writes r { !r = old !r - 1 } *)
+  let decr (r:ref int) = {} r := !r - 1 { !r = old !r - 1 }
 
 end
 

src/programs/pgm_pretty.ml

@@ -81,7 +81,7 @@ and print_pv fmt v =
 and print_triple fmt (p, e, q) =
   fprintf fmt "@[<hv 0>%a@ %a@ %a@]" print_pre p print_expr e print_post q
 
-and print_recfun fmt (v, bl, _, t) =
+and print_recfun fmt (v, bl, _, t, _) =
   fprintf fmt "@[<hov 2>rec %a@ %a =@ %a@]"
     print_pv v (print_list space print_pv) bl print_triple t
 

src/programs/pgm_ttree.ml

@@ -279,7 +279,7 @@ and expr_desc =
   | Elabel of label * expr
   | Eany of type_c
 
-and recfun = pvsymbol * pvsymbol list * rec_variant option * triple
+and recfun = pvsymbol * pvsymbol list * rec_variant option * triple * E.t
 
 and triple = pre * expr * post
 

src/programs/pgm_types.ml

@@ -603,15 +603,16 @@ and E : sig
     reads  : Sreg.t;
     writes : Sreg.t;
     raises : Sexn.t;
-    globals : Spv.t;
+    (* globals : Spv.t; *)
   }
 
   val empty : t
 
   val add_read  : R.t -> t -> t
-  val add_glob  : T.pvsymbol -> t -> t
+  (* val add_glob  : T.pvsymbol -> t -> t *)
   val add_write : R.t -> t -> t
   val add_raise : T.esymbol -> t -> t
+  val add_var   : T.pvsymbol -> t -> t (* add all regions for x, in reads *)
 
   val remove : Sreg.t -> t -> t
   val filter : (R.t -> bool) -> t -> t
@@ -640,19 +641,20 @@ end = struct
     reads  : Sreg.t;
     writes : Sreg.t;
     raises : Sexn.t;
-    globals: Spv.t;
+    (* globals: Spv.t; *)
   }
 
   let empty = {
     reads = Sreg.empty;
     writes = Sreg.empty;
     raises = Sexn.empty;
-    globals = Spv.empty; }
+    (* globals = Spv.empty; *) }
 
   let add_read  r t = { t with reads  = Sreg.add r t.reads  }
   let add_write r t = { t with writes = Sreg.add r t.writes }
   let add_raise e t = { t with raises = Sexn.add e t.raises }
-  let add_glob  pv t = { t with globals = Spv.add pv t.globals }
+  (* let add_glob  pv t = { t with globals = Spv.add pv t.globals } *)
+  let add_var pv ef = Sreg.fold add_read pv.pv_regions ef
 
   let remove s t =
     { t with reads = Sreg.diff t.reads s; writes = Sreg.diff t.writes s }
@@ -666,7 +668,7 @@ end = struct
     { reads  = Sreg.union t1.reads  t2.reads;
       writes = Sreg.union t1.writes t2.writes;
       raises = Sexn.union t1.raises t2.raises;
-      globals = Spv.union t1.globals t2.globals; }
+      (* globals = Spv.union t1.globals t2.globals; *) }
 
   let equal t1 t2 =
     Sreg.equal t1.reads  t2.reads  &&
@@ -692,7 +694,7 @@ end = struct
     { reads = subst_set ts t.reads;
       writes = subst_set ts t.writes;
       raises = t.raises;
-      globals = t.globals; }
+      (* globals = t.globals;  *)}
 
   let occur r t =
     Sreg.mem r t.reads || Sreg.mem r t.writes
@@ -711,9 +713,9 @@ end = struct
     if not (Sreg.is_empty e.writes) then
       fprintf fmt "@ writes %a" print_rset e.writes;
     if not (Sexn.is_empty e.raises) then
-      fprintf fmt "@ raises %a" print_eset e.raises;
-    if not (Spv.is_empty e.globals) then
-      fprintf fmt "@ globals %a" print_pvset e.globals
+      fprintf fmt "@ raises %a" print_eset e.raises
+    (* if not (Spv.is_empty e.globals) then *)
+    (*   fprintf fmt "@ globals %a" print_pvset e.globals *)
 
 end
 

src/programs/pgm_types.mli

@@ -189,15 +189,16 @@ and E : sig
     reads  : Sreg.t;
     writes : Sreg.t;
     raises : Sexn.t;
-    globals: Spv.t;
+    (* globals: Spv.t; *)
   }
 
   val empty : t
 
   val add_read  : R.t -> t -> t
-  val add_glob  : T.pvsymbol -> t -> t
+  (* val add_glob  : T.pvsymbol -> t -> t *)
   val add_write : R.t -> t -> t
   val add_raise : T.esymbol -> t -> t
+  val add_var   : T.pvsymbol -> t -> t
 
   val remove : Sreg.t -> t -> t
   val filter : (R.t -> bool) -> t -> t

src/programs/pgm_typing.ml

@@ -1296,7 +1296,7 @@ let declare_global ls pv =
 let rec term_effect ef t = match t.t_node with
   | Term.Tapp (ls, []) when Hls.mem globals ls ->
       let pv = Hls.find globals ls in
-      E.add_glob pv ef, t_var pv.pv_pure
+      E.add_var pv ef, t_var pv.pv_pure
   | _ ->
       t_map_fold term_effect ef t
 
@@ -1476,6 +1476,10 @@ let saturation loc ef (a,al) =
 
 let type_v_unit _env = tpure (ty_app (ts_tuple 0) [])
 
+let remove_bl_effects bl ef =
+  let remove ef pv = E.remove pv.pv_regions ef in
+  List.fold_left remove ef bl
+
 (* [expr] translates iexpr into expr
    [env : type_v Mvs.t] maps local variables to their types *)
 
@@ -1493,9 +1497,9 @@ and expr_desc gl env loc ty = function
       Elogic t, tpure ty, ef
   | IElocal vs ->
       let vs = Mvs.find vs.i_impure env in
-      Elocal vs, vs.pv_tv, E.empty
+      Elocal vs, vs.pv_tv, E.add_var vs E.empty
   | IEglobal ({ ps_kind = PSvar pv } as s, tv) ->
-      Eglobal s, tv, E.add_glob pv E.empty
+      Eglobal s, tv, E.add_var pv E.empty
   | IEglobal (s, tv) ->
       Eglobal s, tv, E.empty
   | IEapply (e1, vs) ->
@@ -1522,8 +1526,9 @@ and expr_desc gl env loc ty = function
       make_apply loc e1 ty c
   | IEfun (bl, t) ->
       let env, bl = add_binders env bl in
-      let t, c = triple gl env t in
-      Efun (bl, t), tarrow bl c, E.empty
+      let (_,e,_) as t, c = triple gl env t in
+      let ef = remove_bl_effects bl e.expr_effect in
+      Efun (bl, t), tarrow bl c, ef
   | IElet (v, e1, e2) ->
       let e1 = expr gl env e1 in
       let env, v = add_local env v e1.expr_type_v in
@@ -1537,7 +1542,9 @@ and expr_desc gl env loc ty = function
   | IEletrec (dl, e1) ->
       let env, dl = letrec gl env dl in
       let e1 = expr gl env e1 in
-      Eletrec (dl, e1), e1.expr_type_v, e1.expr_effect
+      let add_effect ef (_,_,_,_,ef') = E.union ef ef' in
+      let ef = List.fold_left add_effect e1.expr_effect dl in
+      Eletrec (dl, e1), e1.expr_type_v, ef
   | IEaccess (i, ls, r) ->
       let ef = option_apply E.empty (fun r -> E.add_read r E.empty) r in
       let ls = (get_psymbol ls).ps_pure in
@@ -1734,7 +1741,10 @@ and letrec gl env dl = (* : env * recfun list *)
   in
   let m0 = List.fold_left add_empty_effect Mvs.empty dl in
   let m, dl = fixpoint m0 in
-  make_env env m, dl
+  let add_effect (pv, bl, var, (_,e,_ as t)) =
+    pv, bl, var, t, remove_bl_effects bl e.expr_effect
+  in
+  make_env env m, List.map add_effect dl
 
 (* freshness analysis
 
@@ -1754,7 +1764,7 @@ let rec fresh_expr gl ~term locals e = match e.expr_desc with
       fresh_expr gl ~term:false locals              e1;
       fresh_expr gl ~term       (Spv.add vs locals) e2
   | Eletrec (fl, e1) ->
-      List.iter (fun (_, _, _, t) -> fresh_triple gl t) fl;
+      List.iter (fun (_, _, _, t, _) -> fresh_triple gl t) fl;
       fresh_expr gl ~term locals e1
 
   | Eif (e1, e2, e3) ->
@@ -2165,7 +2175,7 @@ let rec decl ~wp env penv ltm lmod uc = function
       let _, dl = dletrec ~ghost:false denv dl in
       let _, dl = iletrec uc (create_ienv denv) dl in
       let _, dl = letrec uc Mvs.empty dl in
-      let one uc (v, _, _, _ as d) =
+      let one uc (v, _, _, _, _ as d) =
         let tyv = v.pv_tv in
         let loc = loc_of_id v.pv_name in
         let id = v.pv_name.id_string in

src/programs/pgm_wp.ml

@@ -168,22 +168,6 @@ let find_constructor env ts =
   | [ls] -> ls
   | _ -> assert false
 
-let wp_close rm ef f =
-  let sreg = ef.E.writes in
-  let sreg =
-    Spv.fold (fun pv s -> Sreg.union pv.pv_regions s)
-      ef.E.globals (Sreg.union ef.E.reads sreg)
-  in
-  (* all program variables involving these regions *)
-  let vars =
-    let add r s =
-      try Spv.union (Mreg.find r rm) s with Not_found -> assert false
-    in
-    Sreg.fold add sreg Spv.empty
-  in
-  let quantify_v v f = wp_forall v.pv_pure f in
-  Spv.fold quantify_v vars f
-
 let get_ty_subst ty = match ty.ty_node with
   | Tyapp (ts, tyl) ->
       let add s tv ty = Mtv.add tv ty s in
@@ -248,8 +232,7 @@ let rec update env mreg x ty =
      let v'm = update vm r1...rn in
      f[vi <- v'i]
 *)
-let quantify env rm ef f =
-  let sreg = ef.E.writes in
+let quantify env rm sreg f =
   (* all program variables involving these regions *)
   let vars =
     let add r s =
@@ -325,6 +308,31 @@ let quantify env rm ef f =
   let quantify_r _ r' f = wp_forall r' f in
   Mtv.fold quantify_r mreg f
 
+let wp_close_state env rm ef f =
+  let sreg =
+    (* Spv.fold (fun pv s -> Sreg.union pv.pv_regions s) *)
+    (*   ef.E.globals *) (Sreg.union ef.E.reads ef.E.writes)
+  in
+  quantify env rm sreg f
+
+let wp_close rm ef f =
+  let sreg = ef.E.writes in
+  let sreg =
+    (* Spv.fold (fun pv s -> Sreg.union pv.pv_regions s) *)
+    (*   ef.E.globals *) (Sreg.union ef.E.reads sreg)
+  in
+  (* eprintf "wp_close: ef=%a@." E.print ef; *)
+  (* all program variables involving these regions *)
+  let vars =
+    let add r s =
+      try Spv.union (Mreg.find r rm) s with Not_found -> assert false
+    in
+    Sreg.fold add sreg Spv.empty
+  in
+  let quantify_v v f = wp_forall v.pv_pure f in
+  Spv.fold quantify_v vars f
+
+
 (* let quantify ?(all=false) env rm ef f = *)
 (*   let r = quantify ~all env rm ef f in *)
 (*   eprintf "@[<hov 2>quantify: all=%b ef=%a f=@[%a@] ==>@\n%a@]@." *)
@@ -535,14 +543,15 @@ and wp_desc env rm e q = match e.expr_desc with
       let q1 = sup q1 q in (* exc. posts taken from [q] *)
       let we = wp_expr env rm e1 q1 in
       let we = erase_label env lab we in
+      let sreg = e.expr_effect.E.writes in
       let w = match inv with
         | None ->
-            wp_and wfr (quantify env rm e.expr_effect we)
+            wp_and wfr (quantify env rm sreg we)
         | Some i ->
             wp_and wfr
               (wp_and ~sym:true
                  (wp_expl "loop invariant init" i)
-                 (quantify env rm e.expr_effect (wp_implies i we)))
+                 (quantify env rm sreg (wp_implies i we)))
         in
         w
   (* optimization for the particular case let _ = y in e *)
@@ -618,7 +627,7 @@ and wp_desc env rm e q = match e.expr_desc with
       let f = wp_and ~sym:true
         (wp_expl "for loop initialization"
            (t_subst (subst1 x.pv_pure (t_var v1.pv_pure)) inv))
-        (quantify env rm e.expr_effect
+        (quantify env rm e.expr_effect.E.writes
            (wp_and ~sym:true
               (wp_expl "for loop preservation"
                 (wp_forall x.pv_pure
@@ -645,7 +654,7 @@ and wp_desc env rm e q = match e.expr_desc with
       erase_label env lab w1
   | Eany c ->
       (* TODO: propagate call labels into c.c_post *)
-      let w = opaque_wp env rm c.c_effect c.c_post q in
+      let w = opaque_wp env rm c.c_effect.E.writes c.c_post q in
       let p = wp_expl "precondition" c.c_pre in
       let p = t_label ~loc:e.expr_loc p.t_label p in
       wp_and p w
@@ -660,19 +669,27 @@ and wp_triple env rm bl (p, e, q) =
   in
   let f = wp_expr env rm e q in
   let f = wp_implies p f in
-  let f = wp_close rm e.expr_effect f in
+  let f = wp_close_state env rm e.expr_effect f in
   wp_binders bl f
 
-and wp_recfun env rm (_, bl, _var, t) =
+and wp_recfun env rm (_, bl, _var, t, _) =
   wp_triple env rm bl t
 
 let global_regions = ref Mreg.empty
 
 let declare_global_regions pv = global_regions := add_binder pv !global_regions
 
+(* WP functions with quantification over global variables *)
+
 let wp env e =
   let rm = !global_regions in
-  wp_expr env rm e (default_post e.expr_type e.expr_effect)
+  let f = wp_expr env rm e (default_post e.expr_type e.expr_effect) in
+  wp_close rm e.expr_effect f
+
+let wp_rec env (_,_,_,_,ef as def) =
+  let rm = !global_regions in
+  let f = wp_recfun env rm def in
+  wp_close rm ef f
 
 let rec t_btop env t = match t.t_node with
   | Tif (f,t1,t2) -> let f = f_btop env f in
@@ -718,7 +735,7 @@ let decl uc = function
       add_wp_decl ps f uc
   | Pgm_ttree.Dletrec dl ->
       let add_one uc (ps, def) =
-        let f = wp_recfun uc !global_regions def in
+        let f = wp_rec uc def in
         Debug.dprintf debug "wp %s = %a@\n----------------@."
            ps.ps_pure.ls_name.id_string Pretty.print_term f;
         add_wp_decl ps f uc

tests/test-pgm-jcf.mlw

 
 module M
 
+  use import int.Int
   use import module ref.Ref
 
-  let test (x: ref int) =
-    { !x = 0 }
-    !x
-    { result = 0 }
+  parameter r : ref int
+
+  let test1 () =
+    let x = ref 0 in
+    let f (y: int) = {} x := !x + y { !x = old !x + y } in
+    f 2;
+    assert { !x = 2 }
+
+  let rec test2 () =
+    { }
+    r := 0
+    { !r = 0 }
+
+  (* BUG: x escapes its scope (in the postcondition) => should be an error *)
+  (* let foo (a: ref int) = let x = a in fun () -> {} x := 0 { !x = 0 } *)
 
-  (* BUG *)
-  (* 
-  let foo (a: ref int) = let x = a in fun () -> {} x := 0 { !x = 0 }
-  let test () = let x = ref 0 in begin foo x (); assert { !x = 0 } end 
-  *)  
+  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 
 
 end