Skip to content

Commit

Permalink
Fix logical variable shadowing program variables
Browse files Browse the repository at this point in the history 
Currently, when resolving an identifier, EasyCrypt tries to resolve it
as a logical variable first, and then as a program variable (in the
active memory), even when a memory specifier is given.

This commit adds a new memory specifier that changes the resolution
order: when using it, we first try to resolve the identifier as a
program variable (in the given memory), and then as a logical variable
if no program variable matching that name is found.

The syntax if `form{!memory}`.

The pretty-printer has been updated accordingly.
  • Loading branch information
@strub
strub committed Sep 25, 2024
1 parent 5628306 commit a4554ac
Show file tree
Hide file tree
Showing 4 changed files with 102 additions and 54 deletions.
5 changes: 4 additions & 1 deletion src/ecParser.mly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -881,6 +881,9 @@ pside_:
pside:
| x=brace(pside_) { x }

pside_force:
| brace(b=boption(NOT) m=loc(pside_) { (b, m) }) { $1 }

(* -------------------------------------------------------------------- *)
(* Patterns *)

Expand Down Expand Up @@ -1211,7 +1214,7 @@ sform_u(P):
{ let e1 = List.reduce1 (fun _ -> lmap (fun x -> PFtuple x) e1) (unloc e1) in
pfset (EcLocation.make $startpos $endpos) ti se e1 e2 }

| x=sform_r(P) s=loc(pside)
| x=sform_r(P) s=pside_force
{ PFside (x, s) }

| op=loc(numop) ti=tvars_app?
Expand Down
2 changes: 1 addition & 1 deletion src/ecParsetree.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ and pformula_r =
| PFident of pqsymbol * ptyannot option
| PFref of psymbol * pffilter list
| PFmem of psymbol
| PFside of pformula * symbol located
| PFside of pformula * (bool * symbol located)
| PFapp of pformula * pformula list
| PFif of pformula * pformula * pformula
| PFmatch of pformula * (ppattern * pformula) list
Expand Down
24 changes: 18 additions & 6 deletions src/ecPrinting.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -322,6 +322,7 @@ module PPEnv = struct
match EcEnv.Var.lookup_local_opt name ppe.ppe_env with
| Some (id, _) when EcIdent.id_equal id x -> name
| _ -> EcIdent.name x

let tyvar (ppe : t) x =
match Mid.find_opt x ppe.ppe_locals with
| None -> EcIdent.tostring x
Expand Down Expand Up @@ -1665,12 +1666,23 @@ and pp_form_core_r (ppe : PPEnv.t) outer fmt f =
pp_local ppe fmt id

| Fpvar (x, i) -> begin
match EcEnv.Memory.get_active ppe.PPEnv.ppe_env with
| Some i' when EcMemory.mem_equal i i' ->
Format.fprintf fmt "%a" (pp_pv ppe) x
| _ ->
let ppe = PPEnv.enter_by_memid ppe i in
Format.fprintf fmt "%a{%a}" (pp_pv ppe) x (pp_mem ppe) i
let default (force : bool) =
let ppe = PPEnv.enter_by_memid ppe i in
Format.fprintf fmt "%a{%s%a}"
(pp_pv ppe) x (if force then "!" else "") (pp_mem ppe) i in

let force =
match x with
| PVloc x -> Ssym.mem x ppe.ppe_inuse
| PVglob _ -> assert false in

if force then default true else

match EcEnv.Memory.get_active ppe.PPEnv.ppe_env with
| Some i' when EcMemory.mem_equal i i' ->
Format.fprintf fmt "%a" (pp_pv ppe) x
| _ ->
default false
end

| Fglob (mp, i) -> begin
Expand Down
125 changes: 79 additions & 46 deletions src/ecTyping.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -338,6 +338,7 @@ end
let gen_select_op
~(actonly : bool)
~(mode : OpSelect.mode)
~(forcepv : bool)
(opsc : path option)
(tvi : EcUnify.tvi)
(env : EcEnv.env)
Expand All @@ -348,15 +349,15 @@ let gen_select_op
: OpSelect.gopsel list
=

let fpv me (pv, ty, ue) =
let fpv me (pv, ty, ue) : OpSelect.gopsel =
(`Pv (me, pv), ty, ue, (pv :> opmatch))

and fop (op, ty, ue, bd) =
and fop (op, ty, ue, bd) : OpSelect.gopsel=
match bd with
| None -> (`Op op, ty, ue, (`Op op :> opmatch))
| Some bd -> (`Nt bd, ty, ue, (`Op op :> opmatch))

and flc (lc, ty, ue) =
and flc (lc, ty, ue) : OpSelect.gopsel =
(`Lc lc, ty, ue, (`Lc lc :> opmatch)) in

let ue_filter =
Expand All @@ -378,39 +379,52 @@ let gen_select_op

in

match (if tvi = None then select_local env name else None) with
| Some (id, ty) ->
[ flc (id, ty, ue) ]
let locals () : OpSelect.gopsel list =
if Option.is_none tvi then
select_local env name
|> Option.map
(fun (id, ty) -> flc (id, ty, ue))
|> Option.to_list
else [] in

let ops () : OpSelect.gopsel list =
let ops = EcUnify.select_op ~filter:ue_filter tvi env name ue psig in
let ops = opsc |> ofold (fun opsc -> List.mbfilter (by_scope opsc)) ops in
let ops = match List.mbfilter by_current ops with [] -> ops | ops -> ops in
let ops = match List.mbfilter by_tc ops with [] -> ops | ops -> ops in
(List.map fop ops)

and pvs () : OpSelect.gopsel list =
let me, pvs =
match EcEnv.Memory.get_active env, actonly with
| None, true -> (None, [])
| me , _ -> ( me, select_pv env me name ue tvi psig)
in List.map (fpv me) pvs
in

| None ->
let ops () =
let ops = EcUnify.select_op ~filter:ue_filter tvi env name ue psig in
let ops = opsc |> ofold (fun opsc -> List.mbfilter (by_scope opsc)) ops in
let ops = match List.mbfilter by_current ops with [] -> ops | ops -> ops in
let ops = match List.mbfilter by_tc ops with [] -> ops | ops -> ops in
(List.map fop ops)

and pvs () =
let me, pvs =
match EcEnv.Memory.get_active env, actonly with
| None, true -> (None, [])
| me , _ -> ( me, select_pv env me name ue tvi psig)
in List.map (fpv me) pvs
in
let select (filters : (unit -> OpSelect.gopsel list) list) : OpSelect.gopsel list =
List.find_map_opt
(fun f -> match f () with [] -> None | x -> Some x)
filters
|> odfl [] in

match mode with
| `Expr `InOp -> ops ()
| `Form -> (match pvs () with [] -> ops () | pvs -> pvs)
| `Expr `InProc -> (match pvs () with [] -> ops () | pvs -> pvs)
match mode with
| `Expr `InOp -> select [locals; ops]
| `Form
| `Expr `InProc ->
if forcepv then
select [pvs; locals; ops]
else
select [locals; pvs; ops]

(* -------------------------------------------------------------------- *)
let select_exp_op env mode opsc name ue tvi psig =
gen_select_op ~actonly:false ~mode:(`Expr mode)
gen_select_op ~actonly:false ~forcepv:false ~mode:(`Expr mode)
opsc tvi env name ue psig

(* -------------------------------------------------------------------- *)
let select_form_op env opsc name ue tvi psig =
gen_select_op ~actonly:true ~mode:`Form
let select_form_op env ~forcepv opsc name ue tvi psig =
gen_select_op ~actonly:true ~mode:`Form ~forcepv
opsc tvi env name ue psig

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -1745,23 +1759,36 @@ module PFS : sig

val set_memused : pfstate -> unit
val get_memused : pfstate -> bool
val new_memused : ('a -> 'b) -> pfstate -> 'a -> bool * 'b
val isforced : pfstate -> bool
val new_memused : ('a -> 'b) -> force:bool -> pfstate -> 'a -> bool * 'b
end = struct
type pfstate = { mutable pfa_memused : bool; }
type pfstate1 = {
pfa_memused : bool;
pfa_forced : bool;
}

let create () = { pfa_memused = true; }
type pfstate = pfstate1 ref

let set_memused state =
state.pfa_memused <- true
let create1 ~(force : bool) : pfstate1 =
{ pfa_memused = false; pfa_forced = force; }

let get_memused state =
state.pfa_memused
let create () : pfstate =
ref (create1 ~force:false)

let new_memused f state x =
let old = state.pfa_memused in
let aout = (state.pfa_memused <- false; f x) in
let new_ = state.pfa_memused in
state.pfa_memused <- old; (new_, aout)
let set_memused (state : pfstate) =
state := { !state with pfa_memused = true }

let get_memused (state : pfstate) =
(!state).pfa_memused

let isforced (state : pfstate) =
(!state).pfa_forced

let new_memused (f : 'a -> 'b) ~(force : bool) (state : pfstate) (x : 'a) =
let old = !state in
let aout = (state := create1 ~force; f x) in
let new_ = get_memused state in
state := old; (new_, aout)
end

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -3025,7 +3052,10 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt =

| PFident ({ pl_desc = name; pl_loc = loc }, tvi) ->
let tvi = tvi |> omap (transtvi env ue) in
let ops = select_form_op env opsc name ue tvi [] in
let ops =
select_form_op
~forcepv:(PFS.isforced state)
env opsc name ue tvi [] in
begin match ops with
| [] ->
tyerror loc env (UnknownVarOrOp (name, []))
Expand All @@ -3044,7 +3074,7 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt =
tyerror loc env (MultipleOpMatch (name, [], matches))
end

| PFside (f, side) -> begin
| PFside (f, (force, side)) -> begin
let (sloc, side) = (side.pl_loc, unloc side) in
let me =
match EcEnv.Memory.lookup side env with
Expand All @@ -3055,7 +3085,7 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt =
let used, aout =
PFS.new_memused
(transf (EcEnv.Memory.set_active me env))
state f
~force state f
in
if not used then begin
let ppe = EcPrinting.PPEnv.ofenv env in
Expand Down Expand Up @@ -3138,11 +3168,11 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt =
let _, f1 =
PFS.new_memused
(transf (EcEnv.Memory.set_active me1 env))
state f in
~force:false state f in
let _, f2 =
PFS.new_memused
(transf (EcEnv.Memory.set_active me2 env))
state f in
~force:false state f in
unify_or_fail env ue f.pl_loc ~expct:f1.f_ty f2.f_ty;
f_eq f1 f2

Expand All @@ -3155,7 +3185,10 @@ and trans_form_or_pattern env ?mv ?ps ue pf tt =
let tvi = tvi |> omap (transtvi env ue) in
let es = List.map (transf env) pes in
let esig = List.map EcFol.f_ty es in
let ops = select_form_op env opsc name ue tvi esig in
let ops =
select_form_op ~forcepv:(PFS.isforced state)
env opsc name ue tvi esig in

begin match ops with
| [] ->
let uidmap = UE.assubst ue in
Expand Down

0 comments on commit a4554ac

Please sign in to comment.