fixed freshness analysis

bench/programs/bad-typing/fresh1.mlw

@@ -2,6 +2,6 @@ module P
 
   use import module ref.Ref
 
-  let f (a : ref int) = todo (* TODO *)
+  let f (a : ref int) = a
 
 end

src/programs/pgm_typing.ml

@@ -1859,8 +1859,8 @@ and letrec gl env dl = (* : env * recfun list *)
 
 let rec fresh_expr gl ~term locals e = match e.expr_desc with
   | Elocal vs when is_mutable_ty vs.pv_effect.vs_ty
-    && (not term || not (Spv.mem vs locals)) ->
-      errorm ~loc:e.expr_loc "not a fresh reference (could create an alias)"
+    && term && not (Spv.mem vs locals) ->
+      errorm ~loc:e.expr_loc "not a fresh value (could create an alias)"
   | Elogic _ | Elocal _ | Eglobal _ ->
       ()
   | Efun (_, t) ->
@@ -2271,6 +2271,7 @@ let rec decl ~wp env penv ltm lmod uc = function
       let e = iexpr (create_ienv denv) e in
       let e = expr uc Mvs.empty e in
       check_region_vars ();
+      ignore (fresh_expr uc ~term:false Spv.empty e);
       if Debug.test_flag debug then
         eprintf "@[--typing %s-----@\n  @[<hov 2>%a@]@\n@[<hov 2>: %a@]@]@."
           id.id Pgm_pretty.print_expr e print_type_v e.expr_type_v;
@@ -2285,6 +2286,7 @@ let rec decl ~wp env penv ltm lmod uc = function
       let _, dl = dletrec ~ghost:false ~userloc:None denv dl in
       let _, dl = iletrec (create_ienv denv) dl in
       let _, dl = letrec uc Mvs.empty dl in
+      List.iter (fun (_, _, t, _) -> fresh_triple uc t) dl;
       check_region_vars ();
       let one uc (v, _, _, _ as d) =
         let tyv = v.pv_tv in

tests/test-pgm-jcf.mlw

 
-(*
-module MutualRec
+module Test
 
-  use import int.Int
+  use import module ref.Ref
+
+  type foo = (ref int, ref int)
 
-  let rec f (x1 x2: int) : int variant { x1+x2 } =
-    { x1 >= 0 && x2 >= 0 } if x1 <= 1 then 0 else g (x1-1) x2 { result = 0 }
+  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
 
-  with g (y1: int) variant { y1 } =
-    { y1 >= 0  }
-    f (y1-1)
-    { 0 = 0 }
+  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
 
@@ -24,18 +30,20 @@ module M
     let x = ref 0 in
     while !x = 0 do variant { !x } () done
 
-(***
+(*
   use import option.Option
 
   val clear (o : option (ref int)) :
-    {} unit writes (match o with Some r -> r end).contents { !r = 0 }
-***)
+    {}
+    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 } *)
 
-(*   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 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