whyml: do not reprove invariants for reset variables

TODO

@@ -78,6 +78,19 @@ WhyML
     require tedious checks pretty much everywhere in the code,
     and they cannot be translated to OCaml.
 
+  - the following function is verifiable:
+
+      type dref 'a = {| mutable dcontents : ref 'a |}
+
+      let fn (dr : dref int) (r : ref int) =
+      { !r = 0 } dr.dcontents <- r; dr.dcontents := 1 { !r = 0 }
+
+    Strictly speaking, this is benign, since r is reset by the
+    first assignement, and the corresponding reference cannot be
+    used anymore during the program execution. However, it would
+    be nice to forbid the use of reset regions in post-conditions,
+    unless they are put under "old".
+
 syntax
 ------
 

src/whyml/mlw_expr.ml

@@ -546,7 +546,7 @@ let l_pvset pvs lam =
 
 (* check admissibility of consecutive events *)
 
-exception StaleRegion of expr * region * ident
+exception StaleRegion of expr * ident
 exception GhostWrite of expr * region
 exception GhostRaise of expr * xsymbol
 
@@ -555,19 +555,10 @@ let check_reset e varm =
      as the result of the resetting expression. Otherwise, this is
      a freshness violation: some symbol defined earlier carries that
      region into the later code. *)
-  let check_reset r u = (* does r occur in varm? *)
-    let check_id id s = (* does r occur among the regions of id? *)
-      let rec check_reg reg =
-        reg_equal r reg || match u with
-          | Some u when reg_equal u reg -> false
-          | _ -> Sreg.exists check_reg reg.reg_ity.ity_vars.vars_reg
-      in
-      if Sreg.exists check_reg s.vars_reg then
-        Loc.error ?loc:e.e_loc (StaleRegion (e,r,id))
-    in
+  let check_id id vars = if eff_stale_region e.e_effect vars then
+    Loc.error ?loc:e.e_loc (StaleRegion (e,id)) in
+  if not (Mreg.is_empty e.e_effect.eff_resets) then
     Mid.iter check_id varm
-  in
-  Mreg.iter check_reset e.e_effect.eff_resets
 
 let check_ghost_write e eff =
   (* If we make a ghost write, then the modified region cannot

src/whyml/mlw_expr.mli

@@ -217,7 +217,7 @@ val create_let_defn : preid -> expr -> let_defn
 val create_fun_defn : preid -> lambda -> rec_defn
 val create_rec_defn : (psymbol * lambda) list -> rec_defn
 
-exception StaleRegion of expr * region * ident
+exception StaleRegion of expr * ident
 (* freshness violation: a previously reset region is associated to an ident *)
 
 val e_let : let_defn -> expr -> expr

src/whyml/mlw_pretty.ml

@@ -466,7 +466,7 @@ let () = Exn_printer.register
   | Mlw_expr.GhostRaise (_e, xs) ->
       fprintf fmt "This expression raises a ghost exception %a \
         catched by a non-ghost code" print_xs xs
-  | Mlw_expr.StaleRegion (_e, _reg, id) ->
+  | Mlw_expr.StaleRegion (_e, id) ->
       fprintf fmt "This expression prohibits further \
         usage of variable %s" id.id_string
   | Mlw_expr.ValueExpected _e ->

src/whyml/mlw_ty.ml

@@ -699,6 +699,15 @@ let eff_filter vars e =
     eff_resets = Mreg.mapi_filter reset e.eff_resets;
   }
 
+let eff_stale_region eff vars =
+  let check_reset r u =
+    let rec check_reg reg =
+      reg_equal r reg || match u with
+        | Some u when reg_equal u reg -> false
+        | _ -> Sreg.exists check_reg reg.reg_ity.ity_vars.vars_reg in
+    Sreg.exists check_reg vars.vars_reg in
+  Mreg.exists check_reset eff.eff_resets
+
 (** specification *)
 
 type pre = term          (* precondition: pre_fmla *)

src/whyml/mlw_ty.mli

@@ -228,6 +228,8 @@ val eff_assign : effect -> ?ghost:bool -> region -> ity -> effect
 
 val eff_remove_raise : effect -> xsymbol -> effect
 
+val eff_stale_region : effect -> varset -> bool
+
 exception IllegalAlias of region
 
 val eff_full_inst : ity_subst -> effect -> effect

src/whyml/mlw_typing.ml

@@ -669,8 +669,10 @@ let env_invariant lenv eff pvs =
     let ity = pv.pv_vtv.vtv_ity in
     let written r = reg_occurs r ity.ity_vars in
     let inv = Mlw_wp.full_invariant lkn kn pv.pv_vs ity in
-    t_and_simp pinv inv,
-    if Sreg.exists written regs then t_and_simp qinv inv else qinv
+    let qinv = (* we reprove invariants for modified non-reset variables *)
+      if Sreg.exists written regs && not (eff_stale_region eff ity.ity_vars)
+      then t_and_simp qinv inv else qinv in
+    t_and_simp pinv inv, qinv
   in
   Spv.fold add_pv pvs (t_true,t_true)