Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[internal] Fix glob unsoundness #440

Merged
merged 2 commits into from
Sep 22, 2023
Merged

[internal] Fix glob unsoundness #440

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
38de8e2
Fixed glob unsoundess through eager normalization of globs when type
Cameron-Low Sep 4, 2023
98f42b8
Remove references
Cameron-Low Sep 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 1 addition & 8 deletions src/ecCallbyValue.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ ->
Expand Down
66 changes: 45 additions & 21 deletions src/ecCoreFol.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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"

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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;
}
Expand All @@ -1576,14 +1579,15 @@ 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

let f_subst_init ?freshen ?sty ?esloc ?mt ?mempred () =
let sty = odfl ty_subst_id sty in
{ f_subst_id
with fs_freshen = odfl false freshen;
fs_ty = sty;
fs_ty = sty;
fs_esloc = odfl Mid.empty esloc;
fs_mempred = odfl Mid.empty mempred;
fs_memtype = mt; }
Expand All @@ -1601,12 +1605,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 norm_mod =
match EcPath.mget_ident_opt mp with
| Some id ->
f_bind_absmod s x id
| None ->
let nm_ty = (norm_mod mhr).f_ty in
let s = f_bind_cmod s x mp in
let sty = { s.fs_ty with ts_modtglob = Mid.add x nm_ty s.fs_ty.ts_modtglob } in
{ s with fs_ty = sty; fs_modglob = Mid.add x norm_mod 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
Expand Down Expand Up @@ -1658,7 +1677,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 =
Expand Down Expand Up @@ -1709,10 +1728,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' =
Expand Down Expand Up @@ -1931,7 +1955,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 ->
Expand All @@ -1940,7 +1964,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
Expand Down Expand Up @@ -1976,7 +2000,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'))
Expand Down
12 changes: 7 additions & 5 deletions src/ecCoreFol.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -466,8 +466,9 @@ 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 *)
Expand All @@ -488,7 +489,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 -> (EcIdent.t -> form) -> 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
Expand Down
4 changes: 2 additions & 2 deletions src/ecCoreModules.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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')
Expand Down
35 changes: 4 additions & 31 deletions src/ecEnv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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 =
Expand All @@ -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 }
Expand Down Expand Up @@ -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


Expand Down
2 changes: 1 addition & 1 deletion src/ecEnv.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading