Mlw: the unaffected regions do not have to be singletons

src/mlw/expr.ml

@@ -654,11 +654,12 @@ let e_let ld e =
 
 let e_exec ({c_cty = cty} as c) = match cty.cty_args with
   | _::_ as al ->
+      (* unlike for RLpv or RLls, we do not purify the signature,
+         so the regions are now frozen and we have to forbid all
+         effects, including allocation/reset *)
       check_effects cty; check_state cty;
-      (* no need to check eff_covers since we are completely pure *)
-      if List.exists (fun a -> not a.pv_ity.ity_imm) al ||
-        not cty.cty_result.ity_imm then Loc.errorm "This function \
-            has mutable type signature, it cannot be used as pure";
+      if not (Sreg.is_empty cty.cty_effect.eff_resets) then Loc.errorm
+        "This function has side effects, it cannot be used as pure";
       let func a ity = ity_func a.pv_ity ity in
       let ity = List.fold_right func al cty.cty_result in
       let ghost = List.exists (fun a -> a.pv_ghost) al in

src/mlw/ity.ml

@@ -1045,15 +1045,20 @@ let eff_union_seq e1 e2 =
 
 (* NOTE: do not export this function *)
 let eff_inst sbs e =
-  (* all modified or reset regions in e must be instantiated into
+  (* All modified or reset regions in e must be instantiated into
      distinct regions. We allow regions that are not affected directly
      to be aliased, even if they contain modified or reset subregions:
      the values are still updated at the same program points and with
-     the same postconditions, as in the initial verified code. *)
-  let inst src = Mreg.fold (fun r v acc ->
-    let t = reg_full_inst sbs r in match t.ity_node with
-      | Ityreg r -> Mreg.add_new (IllegalAlias r) r v acc
-      | _ -> raise (IllegalSnapshot t)) src Mreg.empty in
+     the same postconditions, as in the initial verified code.
+     Every modified or reset region must be instantiated into a region,
+     not a snapshot. Also, every region containing a modified or reset
+     region, must also be instantiated into a region and not a snapshot.
+     The latter is not necessary for soundness, but simplifies VCgen. *)
+  let inst src = Mreg.fold (fun p v acc -> Mreg.fold (fun q t acc ->
+    match t.ity_node with
+    | Ityapp _ when reg_r_reachable p q -> raise (IllegalSnapshot t)
+    | Ityreg r when reg_equal p q -> Mreg.add_new (IllegalAlias r) r v acc
+    | _ -> acc) sbs.isb_reg acc) src Mreg.empty in
   let writes = inst e.eff_writes in
   let resets = inst e.eff_resets in
   let taints = inst e.eff_taints in
@@ -1069,7 +1074,7 @@ let eff_inst sbs e =
   let sreg = Mreg.set_diff sreg e.eff_resets in
   let dst = Mreg.fold (fun _ i s -> match i.ity_node with
     | Ityreg r -> Sreg.add r s | _ -> s) sreg Sreg.empty in
-  let dst = Mtv.fold (fun _ i s -> ity_freeregs s i) sbs.isb_var dst in
+  let dst = Mtv.fold (fun _ i s -> ity_rch_regs s i) sbs.isb_var dst in
   ignore (Mreg.inter (fun r _ _ -> raise (IllegalAlias r)) dst impact);
   { e with eff_writes = writes; eff_taints = taints;
            eff_covers = covers; eff_resets = resets }

src/mlw/pmodule.ml

@@ -219,6 +219,7 @@ let close_module uc =
   store_module m;
   m
 
+(*
 let count_regions {muc_known = kn} {pv_ity = ity} mr =
   let add_reg r mr = Mreg.change (fun n -> Some (n <> None)) r mr in
   let meet mr1 mr2 = Mreg.union (fun _ x y -> Some (x || y)) mr1 mr2 in
@@ -242,6 +243,7 @@ let count_regions {muc_known = kn} {pv_ity = ity} mr =
         meet mr (List.fold_left add_field Mreg.empty c.rs_cty.cty_args))
         Mreg.empty d.itd_constructors) in
   down mr ity
+*)
 
 let add_symbol add id v uc =
   store_path uc [] id;
@@ -257,16 +259,7 @@ let add_pdecl_no_logic uc d =
     muc_known = known_add_decl uc.muc_known d;
     muc_local = Sid.union uc.muc_local d.pd_news } in
   let add_rs uc s = add_symbol add_ps s.rs_name (RS s) uc in
-  let add_rs_noalias uc s = match s.rs_logic with
-    | RLls _ | RLlemma ->
-        let sv = s.rs_cty.cty_effect.eff_reads in
-        let mr = Spv.fold (count_regions uc) sv Mreg.empty in
-        Mreg.iter (fun _ n ->
-          if n then Loc.errorm ?loc:s.rs_name.id_loc
-            "The type of this function contains an alias") mr;
-        add_rs uc s
-    | _ -> add_rs uc s in
-  let add_rd uc d = add_rs_noalias uc d.rec_sym in
+  let add_rd uc d = add_rs uc d.rec_sym in
   match d.pd_node with
   | PDtype tdl ->
       let add uc d =
@@ -275,7 +268,7 @@ let add_pdecl_no_logic uc d =
         add_symbol add_ts d.itd_its.its_ts.ts_name d.itd_its uc in
       List.fold_left add uc tdl
   | PDlet (LDvar (v,_)) -> add_symbol add_ps v.pv_vs.vs_name (PV v) uc
-  | PDlet (LDsym (s,_)) -> add_rs_noalias uc s
+  | PDlet (LDsym (s,_)) -> add_rs uc s
   | PDlet (LDrec l) -> List.fold_left add_rd uc l
   | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
   | PDpure -> uc