programs: fixed effect inference with global variables

src/programs/pgm_pretty.ml

@@ -26,8 +26,8 @@ let rec print_expr fmt e = match e.expr_desc with
       fprintf fmt "@[<hov 2>fun %a ->@ %a@]" 
 	(print_list space print_pv) bl print_triple t
   | Elet (v, e1, e2) ->
-      fprintf fmt "@[<hv 0>@[<hov 2>let %a =@ %a in@]@ %a@]" 
-	print_vs v.pv_effect
+      fprintf fmt "@[<hv 0>@[<hov 2>let %a/%a =@ %a in@]@ %a@]" 
+	print_vs v.pv_effect print_vs v.pv_pure
 	print_expr e1 print_expr e2
 
   | Eif (e1, e2, e3) ->

src/programs/pgm_types.ml

@@ -534,7 +534,8 @@ end = struct
       print_post c.c_post
 
   and print_binder fmt x =
-    fprintf fmt "(%a:%a)" print_vs x.pv_effect print_type_v x.pv_tv
+    fprintf fmt "(%a/%a:%a)" 
+      print_vs x.pv_effect print_vs x.pv_pure print_type_v x.pv_tv
 
 end
 

src/programs/pgm_typing.ml

@@ -1399,6 +1399,8 @@ and expr_desc gl env loc ty = function
   | IElocal vs ->
       let vs = Mvs.find vs.i_impure env in
       Elocal vs, vs.pv_tv, E.empty
+  | IEglobal ({ ps_kind = PSvar pv } as s, tv) ->
+      Eglobal s, tv, E.add_glob pv E.empty
   | IEglobal (s, tv) ->
       Eglobal s, tv, E.empty
   | IEapply (e1, vs) ->

src/programs/pgm_wp.ml

@@ -179,7 +179,7 @@ let quantify ?(all=false) env rm ef f =
   let sreg =
     if all then
       Spv.fold (fun pv s -> Sreg.union pv.pv_regions s)
-	ef.E.globals (Sreg.union ef.E.reads sreg)
+      	ef.E.globals (Sreg.union ef.E.reads sreg)
     else
       sreg
   in
@@ -567,7 +567,7 @@ 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 = quantify (* ~all:true *) env rm e.expr_effect f in
+  let f = quantify ~all:true env rm e.expr_effect f in
   wp_binders bl f
 
 and wp_recfun env rm (_, bl, _var, t) =

tests/test-pgm-jcf.mlw

 module M
 
-use import int.Int
-use import module ref.Ref
-
-parameter incr : x:ref int -> { } unit writes x { !x = old !x + 1 }
-
-parameter x : ref int
-
-parameter id_not_0 : x:int -> { x <> 0 } int { result = x }
-
-parameter id : x:int -> { } int { result = x }
-
-let test_and_1 () =
-  { }
-  if (incr x; !x > 0) && id !x = 1 then !x else 0+1
-  { result = 1 }
-
-let test_and_2 () =
-  { !x <> 0 }
-  if id_not_0 !x >= 1 && !x <= 1 then !x else 0+1
-  { result = 1 }
-
-let test_or_1 () =
-  { }
-  if (incr x; !x > 0) || !x < 0 then 1 else 2
-  { result = 1 -> !x <> 0 }
+  use import int.Int
+  use import module ref.Ref
 
-let test_or_2 () =
-  { }
-  if !x = 0 || !x = 1 then !x else 1
-  { 0 <= result <= 1 }
+  parameter x : ref int
 
-let test_not_1 () =
-  { }
-  if not (!x = 0) then x := 0
-  { !x = 0 }
+  let bar () = {} x := 1 { !x = 1 }
 
-let test_not_2 () =
-  { !x <= 0 }
-  while not (!x = 0) do invariant { !x <= 0 } incr x done
-  { !x = 0 }
+  parameter foo : y:int -> { y <> 0 } int { true }
 
-let test_all_1 () =
-  { }
-  (!x >= 0 && not (!x = 0) || !x >= 1)
-  { result=True <-> !x>=1 }
+  let test_and_2 () = { !x > 0 } foo !x {}
 
 end
 
-(*
-Local Variables:
-compile-command: "unset LANG; make -C ../../.. bench/programs/good/booleans"
-End:
-*)
-
-
-
 
 (***
 module TestArray