Fixed glob unsoundess through eager normalization of globs when type

checking and substituting modules.

src/ecCallbyValue.ml

@@ -439,14 +439,7 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
 
   | Flocal _ -> app_red st (Subst.subst s f) args
 
-  (* μ-reduction *)
-  | Fglob _ ->
-    let mp, m = destr_glob (Subst.subst s f) in
-    let f =
-      if   st.st_ri.modpath
-      then EcEnv.NormMp.norm_glob st.st_env m mp
-      else f_glob mp m in
-    app_red st f args
+  | Fglob _ -> app_red st (Subst.subst s f) args
 
   (* μ-reduction *)
   | Fpvar _ ->

src/ecCoreFol.ml

@@ -46,7 +46,7 @@ and f_node =
   | Fint    of BI.zint
   | Flocal  of EcIdent.t
   | Fpvar   of EcTypes.prog_var * memory
-  | Fglob   of EcPath.mpath     * memory
+  | Fglob   of EcIdent.t     * memory
   | Fop     of EcPath.path * ty list
   | Fapp    of form * form list
   | Ftuple  of form list
@@ -174,7 +174,6 @@ let mhr    = EcIdent.create "&hr"
 let mleft  = EcIdent.create "&1"
 let mright = EcIdent.create "&2"
 
-
 (*-------------------------------------------------------------------- *)
 let qt_equal : quantif -> quantif -> bool = (==)
 let qt_hash  : quantif -> int = Hashtbl.hash
@@ -478,7 +477,7 @@ module Hsform = Why3.Hashcons.Make (struct
         EcIdent.id_equal s1 s2 && EcTypes.pv_equal pv1 pv2
 
     | Fglob(mp1,m1), Fglob(mp2,m2) ->
-      EcPath.m_equal mp1 mp2 && EcIdent.id_equal m1 m2
+      EcIdent.id_equal mp1 mp2 && EcIdent.id_equal m1 m2
 
     | Fop(p1,lty1), Fop(p2,lty2) ->
         EcPath.p_equal p1 p2 && List.all2 ty_equal lty1 lty2
@@ -534,7 +533,7 @@ module Hsform = Why3.Hashcons.Make (struct
         Why3.Hashcons.combine (EcTypes.pv_hash pv) (EcIdent.id_hash m)
 
     | Fglob(mp, m) ->
-        Why3.Hashcons.combine (EcPath.m_hash mp) (EcIdent.id_hash m)
+        Why3.Hashcons.combine (EcIdent.id_hash mp) (EcIdent.id_hash m)
 
     | Fop(p, lty) ->
         Why3.Hashcons.combine_list ty_hash (EcPath.p_hash p) lty
@@ -581,7 +580,7 @@ module Hsform = Why3.Hashcons.Make (struct
     | Fop (_, tys)        -> union (fun a -> a.ty_fv) tys
     | Fpvar (PVglob pv,m) -> EcPath.x_fv (fv_add m Mid.empty) pv
     | Fpvar (PVloc _,m)   -> fv_add m Mid.empty
-    | Fglob (mp,m)        -> EcPath.m_fv (fv_add m Mid.empty) mp
+    | Fglob (mp,m)        -> fv_add mp (fv_add m Mid.empty)
     | Flocal id           -> fv_singleton id
     | Fapp (f, args)      -> union f_fv (f :: args)
     | Ftuple args         -> union f_fv args
@@ -716,7 +715,7 @@ let f_pvloc  v  m = f_pvar (pv_loc v.v_name) v.v_type m
 let f_pvarg  ty m = f_pvar pv_arg ty m
 
 let f_pvlocs vs menv = List.map (fun v -> f_pvloc v menv) vs
-let f_glob   mp m   = mk_form (Fglob (mp, m)) (tglob mp)
+let f_glob   m mem   = mk_form (Fglob (m, mem)) (tglob m)
 
 (* -------------------------------------------------------------------- *)
 let f_tt     = f_op EcCoreLib.CI_Unit.p_tt    [] tunit
@@ -1308,7 +1307,7 @@ let destr_pvar f =
 
 let destr_glob f =
   match f.f_node with
-  | Fglob(p,m) -> (p,m)
+  | Fglob(m , mem) -> (m, mem)
   | _ -> destr_error "destr_glob"
 
 (* -------------------------------------------------------------------- *)
@@ -1403,6 +1402,7 @@ let is_tuple     f = is_from_destr destr_tuple     f
 let is_op        f = is_from_destr destr_op        f
 let is_local     f = is_from_destr destr_local     f
 let is_pvar      f = is_from_destr destr_pvar      f
+let is_glob      f = is_from_destr destr_glob      f
 let is_proj      f = is_from_destr destr_proj      f
 let is_and       f = is_from_destr destr_and       f
 let is_or        f = is_from_destr destr_or        f
@@ -1552,21 +1552,24 @@ type f_subst = {
   fs_freshen  : bool; (* true means freshen locals *)
   fs_loc      : form Mid.t;
   fs_esloc    : expr Mid.t;
-  fs_ty      : ty_subst;
+  fs_ty       : ty_subst;
   fs_mem      : EcIdent.t Mid.t;
+  fs_modglob  : (EcIdent.t -> form) Mid.t; (* Mappings between abstract modules and their globals *)
   fs_memtype  : EcMemory.memtype option; (* Only substituted in Fcoe *)
   fs_mempred  : mem_pr Mid.t;  (* For predicates over memories,
                                  only substituted in Fcoe *)
 }
 
 (* -------------------------------------------------------------------- *)
 module Fsubst = struct
+
   let f_subst_id = {
     fs_freshen  = false;
     fs_loc      = Mid.empty;
     fs_esloc    = Mid.empty;
-    fs_ty      = ty_subst_id;
+    fs_ty       = ty_subst_id;
     fs_mem      = Mid.empty;
+    fs_modglob  = Mid.empty;
     fs_memtype  = None;
     fs_mempred  = Mid.empty;
   }
@@ -1576,6 +1579,7 @@ module Fsubst = struct
     && is_ty_subst_id s.fs_ty
     && Mid.is_empty   s.fs_loc
     && Mid.is_empty   s.fs_mem
+    && Mid.is_empty   s.fs_modglob
     && Mid.is_empty   s.fs_esloc
     && s.fs_memtype = None
 
@@ -1588,6 +1592,8 @@ module Fsubst = struct
              fs_mempred  = odfl Mid.empty mempred;
              fs_memtype  = mt; }
 
+  let f_norm_mod = ref (fun _ _ -> failwith "Module normalization function not set")
+
   (* ------------------------------------------------------------------ *)
   let f_bind_local s x t =
     let merger o = assert (o = None); Some t in
@@ -1601,12 +1607,27 @@ module Fsubst = struct
     let merger _ = Some m2 in
     { s with fs_mem = Mid.change merger m1 s.fs_mem }
 
-  let f_bind_mod s x mp =
-    assert (not (Mid.mem x s.fs_ty.ts_mp.sms_id));
-    let sms = EcPath.sms_bind_abs x mp s.fs_ty.ts_mp in
-    let sty = { s.fs_ty with ts_mp = sms } in
+  let f_bind_absmod s m1 m2 =
+    let merger o = assert (o = None); Some m2 in
+    let sty = { s.fs_ty with ts_absmod = Mid.change merger m1 s.fs_ty.ts_absmod } in
+    let sty = { sty with ts_cmod = Mid.add m1 (EcPath.mident m2) s.fs_ty.ts_cmod } in
     { s with fs_ty = sty }
 
+  let f_bind_cmod s m mp =
+    let merger o = assert (o = None); Some mp in
+    let sty = { s.fs_ty with ts_cmod = Mid.change merger m s.fs_ty.ts_cmod } in
+    { s with fs_ty = sty }
+
+  let f_bind_mod s x mp =
+    match EcPath.mget_ident_opt mp with
+    | Some id ->
+         f_bind_absmod s x id
+    | None ->
+       let nm = !f_norm_mod mhr mp in (* Only used to get a type, memory doesn't matter *)
+       let s = f_bind_cmod s x mp in
+       let sty = { s.fs_ty with ts_modtglob = Mid.add x nm.f_ty s.fs_ty.ts_modtglob } in
+       { s with fs_ty = sty; fs_modglob = Mid.add x (fun m -> !f_norm_mod m mp) s.fs_modglob }
+
   let f_bind_rename s xfrom xto ty =
     let xf = f_local xto ty in
     let xe = e_local xto ty in
@@ -1658,7 +1679,7 @@ module Fsubst = struct
 
   (* ------------------------------------------------------------------ *)
   let subst_xpath s f =
-    EcPath.x_subst s.fs_ty.ts_mp f
+    EcPath.x_subst_abs s.fs_ty.ts_cmod f
 
   let subst_stmt s c =
     let es =
@@ -1709,10 +1730,15 @@ module Fsubst = struct
         let ty' = ty_subst s.fs_ty fp.f_ty in
         f_pvar pv' ty' m'
 
-    | Fglob (mp, m) ->
+    | Fglob (mid, m) ->
         let m'  = Mid.find_def m m s.fs_mem in
-        let mp' = EcPath.m_subst s.fs_ty.ts_mp mp in
-        f_glob mp' m'
+        let mid = Mid.find_def mid mid s.fs_ty.ts_absmod in
+        begin
+          (* Have we computed the globals for this module *)
+          match Mid.find_opt mid s.fs_modglob with
+          | None -> f_glob mid m'
+          | Some f -> f m'
+        end
 
     | FhoareF hf ->
       let pr', po' =
@@ -1931,7 +1957,7 @@ module Fsubst = struct
 
   and mr_subst ~tx s mr : form p_mod_restr =
     let sx = subst_xpath s in
-    let sm = EcPath.m_subst s.fs_ty.ts_mp in
+    let sm = EcPath.m_subst_abs s.fs_ty.ts_cmod in
     { mr_xpaths = ur_app (fun s -> Sx.fold (fun m rx ->
           Sx.add (sx m) rx) s Sx.empty) mr.mr_xpaths;
       mr_mpaths = ur_app (fun s -> Sm.fold (fun m r ->
@@ -1940,7 +1966,7 @@ module Fsubst = struct
     }
 
   and subst_mty ~tx s mty =
-    let sm = EcPath.m_subst s.fs_ty.ts_mp in
+    let sm = EcPath.m_subst_abs s.fs_ty.ts_cmod in
 
     let mt_params = List.map (snd_map (subst_mty ~tx s)) mty.mt_params in
     let mt_name   = mty.mt_name in
@@ -1976,7 +2002,7 @@ module Fsubst = struct
     else
       let s = match gty' with
         | GTty   ty -> f_bind_rename s x x' ty
-        | GTmodty _ -> f_bind_mod s x (EcPath.mident x')
+        | GTmodty _ -> f_bind_absmod s x x'
         | GTmem   _ -> f_bind_mem s x x'
       in
         (s, (x', gty'))

src/ecCoreFol.mli

@@ -43,7 +43,7 @@ and f_node =
   | Fint    of zint
   | Flocal  of EcIdent.t
   | Fpvar   of EcTypes.prog_var * memory
-  | Fglob   of mpath * memory
+  | Fglob   of EcIdent.t * memory
   | Fop     of path * ty list
   | Fapp    of form * form list
   | Ftuple  of form list
@@ -223,7 +223,7 @@ val f_local : EcIdent.t -> EcTypes.ty -> form
 val f_pvar  : EcTypes.prog_var -> EcTypes.ty -> memory -> form
 val f_pvarg : EcTypes.ty -> memory -> form
 val f_pvloc : variable -> memory -> form
-val f_glob  : mpath -> memory -> form
+val f_glob  : EcIdent.t -> memory -> form
 
 (* soft-constructors - common formulas constructors *)
 val f_op     : path -> EcTypes.ty list -> EcTypes.ty -> form
@@ -411,7 +411,7 @@ val destr_pr        : form -> pr
 val destr_programS  : [`Left | `Right] option -> form -> memenv * stmt
 val destr_int       : form -> zint
 
-val destr_glob      : form -> EcPath.mpath     * memory
+val destr_glob      : form -> EcIdent.t        * memory
 val destr_pvar      : form -> EcTypes.prog_var * memory
 
 (* -------------------------------------------------------------------- *)
@@ -466,15 +466,17 @@ type f_subst = private {
   fs_freshen  : bool; (* true means realloc local *)
   fs_loc      : form Mid.t;
   fs_esloc    : expr Mid.t;
-  fs_ty      : ty_subst;
+  fs_ty       : ty_subst;
   fs_mem      : EcIdent.t Mid.t;
+  fs_modglob  : (EcIdent.t -> form) Mid.t;
   fs_memtype  : EcMemory.memtype option; (* Only substituted in Fcoe *)
   fs_mempred  : mem_pr Mid.t;  (* For predicates over memories,
                                  only substituted in Fcoe *)
 }
 
 (* -------------------------------------------------------------------- *)
 module Fsubst : sig
+  val f_norm_mod  : (EcIdent.t -> EcPath.mpath -> form) ref
   val f_subst_id  : f_subst
   val is_subst_id : f_subst -> bool
 
@@ -488,7 +490,8 @@ module Fsubst : sig
 
   val f_bind_local  : f_subst -> EcIdent.t -> form -> f_subst
   val f_bind_mem    : f_subst -> EcIdent.t -> EcIdent.t -> f_subst
-  val f_bind_mod    : f_subst -> EcIdent.t -> mpath -> f_subst
+  val f_bind_absmod : f_subst -> EcIdent.t -> EcIdent.t -> f_subst
+  val f_bind_mod    : f_subst -> EcIdent.t -> EcPath.mpath -> f_subst
   val f_bind_rename : f_subst -> EcIdent.t -> EcIdent.t -> ty -> f_subst
 
   val f_subst   : ?tx:(form -> form -> form) -> f_subst -> form -> form

src/ecCoreModules.ml

@@ -331,7 +331,7 @@ let rec s_subst_top (s : EcTypes.e_subst) =
   if e_subst == identity then identity else
 
   let pvt_subst (pv,ty as p) =
-    let pv' = EcTypes.pv_subst (EcPath.x_subst s.es_ty.ts_mp) pv in
+    let pv' = EcTypes.pv_subst (EcPath.x_subst_abs s.es_ty.ts_cmod) pv in
     let ty' = EcTypes.ty_subst s.EcTypes.es_ty ty in
 
     if pv == pv' && ty == ty' then p else (pv', ty') in
@@ -357,7 +357,7 @@ let rec s_subst_top (s : EcTypes.e_subst) =
 
     | Scall (olv, mp, args) ->
         let olv'  = olv |> OSmart.omap lv_subst in
-        let mp'   = EcPath.x_subst s.es_ty.ts_mp mp in
+        let mp'   = EcPath.x_subst_abs s.es_ty.ts_cmod mp in
         let args' = List.Smart.map e_subst args in
 
         i_call (olv', mp', args')

src/ecEnv.ml

@@ -2457,7 +2457,7 @@ module NormMp = struct
   let globals env m mp =
     let us = mod_use env mp in
     let l =
-      Sid.fold (fun id l -> f_glob (EcPath.mident id) m :: l) us.us_gl [] in
+      Sid.fold (fun id l -> f_glob id m :: l) us.us_gl [] in
     let l =
       Mx.fold
         (fun xp ty l -> f_pvar (EcTypes.pv_glob xp) ty m :: l) us.us_pv l in
@@ -2469,29 +2469,7 @@ module NormMp = struct
     let g = (norm_glob env mhr mp) in
     g.f_ty
 
-  let tglob_reducible env mp =
-    match (norm_tglob env mp).ty_node with
-    | Tglob mp' -> not (EcPath.m_equal mp mp')
-    | _ -> true
-
-  let norm_ty env =
-    EcTypes.Hty.memo_rec 107 (
-      fun aux ty ->
-        match ty.ty_node with
-        | Tglob mp -> norm_tglob env mp
-        | _ -> ty_map aux ty)
-
   let rec norm_form env =
-    let norm_ty1 : ty -> ty = norm_ty env in
-
-    let norm_gty env (id,gty) =
-      let gty =
-        match gty with
-        | GTty ty -> GTty (norm_ty env ty)
-        | GTmodty _ -> gty
-        | GTmem mt -> GTmem (mt_subst (norm_ty env) mt) in
-      id,gty in
-
     let has_mod b =
       List.exists (fun (_,gty) ->
         match gty with GTmodty _ -> true | _ -> false) b in
@@ -2502,19 +2480,15 @@ module NormMp = struct
         | Fquant(q,bd,f) ->
           if has_mod bd then
             let env = Mod.add_mod_binding bd env in
-            let bd = List.map (norm_gty env) bd in
             f_quant q bd (norm_form env f)
           else
-          let bd = List.map (norm_gty env) bd in
           f_quant q bd (aux f)
 
         | Fpvar(p,m) ->
           let p' = norm_pvar env p in
           if p == p' then f else
             f_pvar p' f.f_ty m
 
-        | Fglob(p,m) -> norm_glob env m p
-
         | FhoareF hf ->
           let pre' = aux hf.hf_pr and p' = norm_xfun env hf.hf_f
           and post' = aux hf.hf_po in
@@ -2561,8 +2535,8 @@ module NormMp = struct
             pr_event = aux pr.pr_event;
           } in f_pr_r pr'
 
-        | _ ->
-          EcCoreFol.f_map norm_ty1 aux f) in
+        | _ -> f)
+          in
     norm_form
 
   let norm_op env op =
@@ -2582,7 +2556,7 @@ module NormMp = struct
     in
     { op with
         op_kind = kind;
-        op_ty   = norm_ty env op.op_ty; }
+        op_ty   = op.op_ty; }
 
   let norm_ax env ax =
     { ax with ax_spec = norm_form env ax.ax_spec }
@@ -2755,7 +2729,6 @@ module Ty = struct
   let rec ty_hnorm (ty : ty) (env : env) =
     match ty.ty_node with
     | Tconstr (p, tys) when defined p env -> ty_hnorm (unfold p tys env) env
-    | Tglob p -> NormMp.norm_tglob env p
     | _ -> ty
 
 

src/ecEnv.mli

@@ -275,7 +275,7 @@ module NormMp : sig
 
   val norm_glob     : env -> EcMemory.memory -> mpath -> form
   val norm_tglob    : env -> mpath -> EcTypes.ty
-  val tglob_reducible : env -> mpath -> bool
+
   val is_abstract_fun : xpath -> env -> bool
   val x_equal         : env -> xpath -> xpath -> bool
   val pv_equal        : env -> EcTypes.prog_var -> EcTypes.prog_var -> bool