From 3b73918146ac060689526871fcbeb2baa6b429e7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 6 Nov 2022 18:10:59 +0100
Subject: Add ids to the dummy variables
---
compiler/Contexts.ml | 144 ++++++++++++++++++++++---------------
compiler/InterpreterBorrows.ml | 2 +-
compiler/InterpreterBorrowsCore.ml | 4 +-
compiler/InterpreterPaths.ml | 7 +-
compiler/InterpreterStatements.ml | 40 ++++++-----
compiler/InterpreterUtils.ml | 5 +-
compiler/Print.ml | 26 ++++---
compiler/SymbolicAst.ml | 2 +-
compiler/SynthesizeSymbolic.ml | 2 +-
9 files changed, 139 insertions(+), 93 deletions(-)
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 8fb7053b..0c72392b 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -4,6 +4,15 @@ open Values
open LlbcAst
module V = Values
open ValuesUtils
+open Identifiers
+
+(** The [Id] module for dummy variables.
+
+ Dummy variables are used to store values that we don't want to forget
+ in the environment, because they contain borrows for instance, typically
+ because they might be overwritten during an assignment.
+ *)
+module DummyVarId = IdGen ()
(** Some global counters.
@@ -70,6 +79,9 @@ let abstraction_id_counter, fresh_abstraction_id =
let fun_call_id_counter, fresh_fun_call_id =
FunCallId.fresh_stateful_generator ()
+let dummy_var_id_counter, fresh_dummy_var_id =
+ DummyVarId.fresh_stateful_generator ()
+
(** We shouldn't need to reset the global counters, but it might be good to
do it from time to time, for instance every time we start evaluating/
synthesizing a function.
@@ -86,22 +98,41 @@ let reset_global_counters () =
borrow_id_counter := BorrowId.generator_zero;
region_id_counter := RegionId.generator_zero;
abstraction_id_counter := AbstractionId.generator_zero;
- fun_call_id_counter := FunCallId.generator_zero
+ fun_call_id_counter := FunCallId.generator_zero;
+ dummy_var_id_counter := DummyVarId.generator_zero
(** A binder used in an environment, to map a variable to a value *)
-type binder = {
+type var_binder = {
index : VarId.id; (** Unique variable identifier *)
name : string option; (** Possible name *)
}
[@@deriving show]
+(** A binder, for a "real" variable or a dummy variable *)
+type binder = VarBinder of var_binder | DummyBinder of DummyVarId.id
+[@@deriving show]
+
+(** Ancestor for {!env_elem} iter visitor *)
+class ['self] iter_env_elem_base =
+ object (_self : 'self)
+ inherit [_] iter_abs
+ method visit_binder : 'env -> binder -> unit = fun _ _ -> ()
+ end
+
+(** Ancestor for {!env_elem} map visitor *)
+class ['self] map_env_elem_base =
+ object (_self : 'self)
+ inherit [_] map_abs
+ method visit_binder : 'env -> binder -> binder = fun _ x -> x
+ end
+
(** Environment value: mapping from variable to value, abstraction (only
used in symbolic mode) or stack frame delimiter.
TODO: rename Var (-> Binding?)
*)
type env_elem =
- | Var of (binder option[@opaque]) * typed_value
+ | Var of binder * typed_value
(** Variable binding - the binder is None if the variable is a dummy variable
(we use dummy variables to store temporaries while doing bookkeeping such
as ending borrows for instance). *)
@@ -113,7 +144,7 @@ type env_elem =
{
name = "iter_env_elem";
variety = "iter";
- ancestors = [ "iter_abs" ];
+ ancestors = [ "iter_env_elem_base" ];
nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
concrete = true;
},
@@ -121,7 +152,7 @@ type env_elem =
{
name = "map_env_elem";
variety = "map";
- ancestors = [ "map_abs" ];
+ ancestors = [ "map_env_elem_base" ];
nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
concrete = true;
}]
@@ -235,54 +266,44 @@ type eval_ctx = {
let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
TypeVarId.nth ctx.type_vars vid
-let opt_binder_has_vid (bv : binder option) (vid : VarId.id) : bool =
- match bv with Some bv -> bv.index = vid | None -> false
-
-let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder =
- (* TOOD: we might want to stop at the end of the frame *)
+(** Lookup a variable in the current frame *)
+let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
+ (* We take care to stop at the end of current frame: different variables
+ in different frames can have the same id!
+ *)
let rec lookup env =
match env with
| [] ->
raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid))
- | Var (var, _) :: env' ->
- if opt_binder_has_vid var vid then Option.get var else lookup env'
- | (Abs _ | Frame) :: env' -> lookup env'
+ | Var (VarBinder var, v) :: env' ->
+ if var.index = vid then (var, v) else lookup env'
+ | (Var (DummyBinder _, _) | Abs _) :: env' -> lookup env'
+ | Frame :: _ -> raise (Failure "End of frame")
in
- lookup ctx.env
+ lookup env
+
+let ctx_lookup_var_binder (ctx : eval_ctx) (vid : VarId.id) : var_binder =
+ fst (env_lookup_var ctx.env vid)
-(** TODO: make this more efficient with maps *)
let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
TypeDeclId.Map.find tid ctx.type_context.type_decls
-(** TODO: make this more efficient with maps *)
let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
FunDeclId.Map.find fid ctx.fun_context.fun_decls
-(** TODO: make this more efficient with maps *)
let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) :
global_decl =
GlobalDeclId.Map.find gid ctx.global_context.global_decls
-(** Retrieve a variable's value in an environment *)
+(** Retrieve a variable's value in the current frame *)
let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
- (* We take care to stop at the end of current frame: different variables
- in different frames can have the same id!
- *)
- let rec lookup env =
- match env with
- | [] -> raise (Failure "Unexpected")
- | Var (var, v) :: env' ->
- if opt_binder_has_vid var vid then v else lookup env'
- | Abs _ :: env' -> lookup env'
- | Frame :: _ -> raise (Failure "End of frame")
- in
- lookup env
+ snd (env_lookup_var env vid)
(** Retrieve a variable's value in an evaluation context *)
let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value =
env_lookup_var_value ctx.env vid
-(** Update a variable's value in an environment
+(** Update a variable's value in the current frame.
This is a helper function: it can break invariants and doesn't perform
any check.
@@ -294,15 +315,16 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
let rec update env =
match env with
| [] -> raise (Failure "Unexpected")
- | Var (var, v) :: env' ->
- if opt_binder_has_vid var vid then Var (var, nv) :: env'
+ | Var ((VarBinder b as var), v) :: env' ->
+ if b.index = vid then Var (var, nv) :: env'
else Var (var, v) :: update env'
- | Abs abs :: env' -> Abs abs :: update env'
+ | ((Var (DummyBinder _, _) | Abs _) as ee) :: env' -> ee :: update env'
| Frame :: _ -> raise (Failure "End of frame")
in
update env
-let var_to_binder (var : var) : binder = { index = var.index; name = var.name }
+let var_to_binder (var : var) : var_binder =
+ { index = var.index; name = var.name }
(** Update a variable's value in an evaluation context.
@@ -321,7 +343,7 @@ let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
assert (var.var_ty = v.ty);
let bv = var_to_binder var in
- { ctx with env = Var (Some bv, v) :: ctx.env }
+ { ctx with env = Var (VarBinder bv, v) :: ctx.env }
(** Push a list of variables.
@@ -335,37 +357,41 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
(fun (var, (value : typed_value)) -> var.var_ty = value.ty)
vars);
let vars =
- List.map (fun (var, value) -> Var (Some (var_to_binder var), value)) vars
+ List.map
+ (fun (var, value) -> Var (VarBinder (var_to_binder var), value))
+ vars
in
let vars = List.rev vars in
{ ctx with env = List.append vars ctx.env }
(** Push a dummy variable in the context's environment. *)
-let ctx_push_dummy_var (ctx : eval_ctx) (v : typed_value) : eval_ctx =
- { ctx with env = Var (None, v) :: ctx.env }
-
-(** Pop the first dummy variable from a context's environment. *)
-let ctx_pop_dummy_var (ctx : eval_ctx) : eval_ctx * typed_value =
- let rec pop_var (env : env) : env * typed_value =
+let ctx_push_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) (v : typed_value)
+ : eval_ctx =
+ { ctx with env = Var (DummyBinder vid, v) :: ctx.env }
+
+(** Remove a dummy variable from a context's environment. *)
+let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
+ eval_ctx * typed_value =
+ let rec remove_var (env : env) : env * typed_value =
match env with
- | [] -> raise (Failure "Could not find a dummy variable")
- | Var (None, v) :: env -> (env, v)
+ | [] -> raise (Failure "Could not lookup a dummy variable")
+ | Var (DummyBinder vid', v) :: env when vid' = vid -> (env, v)
| ee :: env ->
- let env, v = pop_var env in
+ let env, v = remove_var env in
(ee :: env, v)
in
- let env, v = pop_var ctx.env in
+ let env, v = remove_var ctx.env in
({ ctx with env }, v)
-(** Read the first dummy variable in a context's environment. *)
-let ctx_read_first_dummy_var (ctx : eval_ctx) : typed_value =
- let rec read_var (env : env) : typed_value =
+(** Lookup a dummy variable in a context's environment. *)
+let ctx_lookup_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
+ let rec lookup_var (env : env) : typed_value =
match env with
- | [] -> raise (Failure "Could not find a dummy variable")
- | Var (None, v) :: _env -> v
- | _ :: env -> read_var env
+ | [] -> raise (Failure "Could not lookup a dummy variable")
+ | Var (DummyBinder vid', v) :: _env when vid' = vid -> v
+ | _ :: env -> lookup_var env
in
- read_var ctx.env
+ lookup_var ctx.env
(** Push an uninitialized variable (which thus maps to {!Values.Bottom}) *)
let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
@@ -398,8 +424,8 @@ class ['self] iter_frame =
object (self : 'self)
inherit [_] V.iter_abs
- method visit_Var : 'acc -> binder option -> typed_value -> unit =
- fun acc _vid v -> self#visit_typed_value acc v
+ method visit_Var : 'acc -> binder -> typed_value -> unit =
+ fun acc _ v -> self#visit_typed_value acc v
method visit_Abs : 'acc -> abs -> unit =
fun acc abs -> self#visit_abs acc abs
@@ -426,10 +452,10 @@ class ['self] map_frame_concrete =
object (self : 'self)
inherit [_] V.map_abs
- method visit_Var : 'acc -> binder option -> typed_value -> env_elem =
- fun acc vid v ->
+ method visit_Var : 'acc -> binder -> typed_value -> env_elem =
+ fun acc b v ->
let v = self#visit_typed_value acc v in
- Var (vid, v)
+ Var (b, v)
method visit_Abs : 'acc -> abs -> env_elem =
fun acc abs -> Abs (self#visit_abs acc abs)
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 16aaf60a..c8a7ae7f 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -931,7 +931,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
* By doing that we should have ended the target borrow (see the
* below sanity check) *)
end_abstraction config chain abs_id
- | VarId _, _ ->
+ | (VarId _ | DummyVarId _), _ ->
(* The loan is not inside the same abstraction (actually inside
* a non-abstraction value): we need to end the whole abstraction *)
end_abstraction config chain abs_id
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 6f9b2ffe..214f2cda 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -254,7 +254,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
assert (Option.is_none !abs_or_var);
abs_or_var :=
Some
- (VarId (match bv with Some bv -> Some bv.C.index | None -> None));
+ (match bv with
+ | VarBinder b -> VarId b.C.index
+ | DummyBinder id -> DummyVarId id);
super#visit_Var env bv v;
abs_or_var := None
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 5fcc25eb..cc5b5864 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -635,12 +635,13 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
let access = Write in
let v = read_place_unwrap config access p ctx in
let ctx = write_place_unwrap config access p (mk_bottom v.V.ty) ctx in
- let ctx = C.ctx_push_dummy_var ctx v in
+ let dummy_id = C.fresh_dummy_var_id () in
+ let ctx = C.ctx_push_dummy_var ctx dummy_id v in
(* Auxiliary function *)
let rec drop : cm_fun =
fun cf ctx ->
(* Read the value *)
- let v = C.ctx_read_first_dummy_var ctx in
+ let v = C.ctx_lookup_dummy_var ctx dummy_id in
(* Check if there are loans or borrows to end *)
let with_borrows = false in
match get_first_outer_loan_or_borrow_in_value with_borrows v with
@@ -665,7 +666,7 @@ let drop_outer_loans_at_lplace (config : C.config) (p : E.place) : cm_fun =
let cc =
comp cc (fun cf ctx ->
(* Pop *)
- let ctx, v = C.ctx_pop_dummy_var ctx in
+ let ctx, v = C.ctx_remove_dummy_var ctx dummy_id in
(* Reinsert *)
let ctx = write_place_unwrap config access p v ctx in
(* Sanity check *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 84a6716c..4d447ffe 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -40,7 +40,8 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
(* Move the value at destination (that we will overwrite) to a dummy variable
* to preserve the borrows it may contain *)
let mv = read_place_unwrap config access p ctx in
- let ctx = C.ctx_push_dummy_var ctx mv in
+ let dummy_id = C.fresh_dummy_var_id () in
+ let ctx = C.ctx_push_dummy_var ctx dummy_id mv in
(* Update the destination to ⊥ *)
let nv = { v with value = V.Bottom } in
let ctx = write_place_unwrap config access p nv ctx in
@@ -54,15 +55,16 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
comp cc replace cf ctx
(** Push a dummy variable to the environment *)
-let push_dummy_var (v : V.typed_value) : cm_fun =
+let push_dummy_var (vid : C.DummyVarId.id) (v : V.typed_value) : cm_fun =
fun cf ctx ->
- let ctx = C.ctx_push_dummy_var ctx v in
+ let ctx = C.ctx_push_dummy_var ctx vid v in
cf ctx
-(** Pop a dummy variable from the environment *)
-let pop_dummy_var (cf : V.typed_value -> m_fun) : m_fun =
+(** Remove a dummy variable from the environment *)
+let remove_dummy_var (vid : C.DummyVarId.id) (cf : V.typed_value -> m_fun) :
+ m_fun =
fun ctx ->
- let ctx, v = C.ctx_pop_dummy_var ctx in
+ let ctx, v = C.ctx_remove_dummy_var ctx vid in
cf v ctx
(** Push an uninitialized variable to the environment *)
@@ -106,18 +108,20 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) :
^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n"
^ eval_ctx_to_string ctx));
(* Push the rvalue to a dummy variable, for bookkeeping *)
- let cc = push_dummy_var rv in
+ let rvalue_vid = C.fresh_dummy_var_id () in
+ let cc = push_dummy_var rvalue_vid rv in
(* Prepare the destination *)
let cc = comp cc (prepare_lplace config p) in
(* Retrieve the rvalue from the dummy variable *)
- let cc = comp cc (fun cf _lv -> pop_dummy_var cf) in
+ let cc = comp cc (fun cf _lv -> remove_dummy_var rvalue_vid cf) in
(* Update the destination *)
let move_dest cf (rv : V.typed_value) : m_fun =
fun ctx ->
(* Move the value at destination (that we will overwrite) to a dummy variable
* to preserve the borrows *)
let mv = read_place_unwrap config Write p ctx in
- let ctx = C.ctx_push_dummy_var ctx mv in
+ let dest_vid = C.fresh_dummy_var_id () in
+ let ctx = C.ctx_push_dummy_var ctx dest_vid mv in
(* Write to the destination *)
(* Checks - maybe the bookkeeping updated the rvalue and introduced bottoms *)
assert (not (bottom_in_value ctx.ended_regions rv));
@@ -338,8 +342,8 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
match env with
| [] -> raise (Failure "Inconsistent environment")
| C.Abs _ :: env -> list_locals env
- | C.Var (None, _) :: env -> list_locals env
- | C.Var (Some var, _) :: env ->
+ | C.Var (DummyBinder _, _) :: env -> list_locals env
+ | C.Var (VarBinder var, _) :: env ->
let locals = list_locals env in
if var.index <> ret_vid then var.index :: locals else locals
| C.Frame :: _ -> []
@@ -390,7 +394,9 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
match env with
| [] -> raise (Failure "Inconsistent environment")
| C.Abs abs :: env -> C.Abs abs :: pop env
- | C.Var (_, v) :: env -> C.Var (None, v) :: pop env
+ | C.Var (_, v) :: env ->
+ let vid = C.fresh_dummy_var_id () in
+ C.Var (C.DummyBinder vid, v) :: pop env
| C.Frame :: env -> (* Stop here *) env
in
let cf_pop cf (ret_value : V.typed_value) : m_fun =
@@ -424,8 +430,9 @@ let eval_box_new_concrete (config : C.config)
match (region_params, type_params, ctx.env) with
| ( [],
[ boxed_ty ],
- Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ )
- ->
+ Var (VarBinder input_var, input_value)
+ :: Var (_ret_var, _)
+ :: C.Frame :: _ ) ->
(* Required type checking *)
assert (input_value.V.ty = boxed_ty);
@@ -465,8 +472,9 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
match (region_params, type_params, ctx.env) with
| ( [],
[ boxed_ty ],
- Var (Some input_var, input_value) :: Var (_ret_var, _) :: C.Frame :: _ )
- ->
+ Var (VarBinder input_var, input_value)
+ :: Var (_ret_var, _)
+ :: C.Frame :: _ ) ->
(* Required type checking. We must have:
- input_value.ty == & (mut) Box<ty>
- boxed_ty == ty
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 31f25f45..8d23e8d8 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -124,7 +124,10 @@ type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
(** Generic borrow content: concrete or abstract *)
type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
-type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of E.VarId.id option
+type abs_or_var_id =
+ | AbsId of V.AbstractionId.id
+ | VarId of E.VarId.id
+ | DummyVarId of C.DummyVarId.id
(** Utility exception *)
exception FoundBorrowContent of V.borrow_content
diff --git a/compiler/Print.ml b/compiler/Print.ml
index dc73b572..53bba8c7 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -310,18 +310,24 @@ module PV = Values (* local module *)
(** Pretty-printing for contexts *)
module Contexts = struct
- let binder_to_string (bv : C.binder) : string =
+ let var_binder_to_string (bv : C.var_binder) : string =
match bv.name with
| None -> PV.var_id_to_string bv.index
| Some name -> name
+ let dummy_var_id_to_string (bid : C.DummyVarId.id) : string =
+ "_@" ^ C.DummyVarId.to_string bid
+
+ let binder_to_string (bv : C.binder) : string =
+ match bv with
+ | VarBinder b -> var_binder_to_string b
+ | DummyBinder bid -> dummy_var_id_to_string bid
+
let env_elem_to_string (fmt : PV.value_formatter) (indent : string)
(indent_incr : string) (ev : C.env_elem) : string =
match ev with
| Var (var, tv) ->
- let bv =
- match var with Some var -> binder_to_string var | None -> "_"
- in
+ let bv = binder_to_string var in
indent ^ bv ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;"
| Abs abs -> PV.abs_to_string fmt indent indent_incr abs
| Frame -> raise (Failure "Can't print a Frame element")
@@ -343,10 +349,10 @@ module Contexts = struct
*)
let filter_elem (ev : C.env_elem) : C.env_elem option =
match ev with
- | Var (Some _, tv) ->
+ | Var (VarBinder _, tv) ->
(* Not a dummy binding: check if the value is ⊥ *)
if VU.is_bottom tv.value then None else Some ev
- | Var (None, tv) ->
+ | Var (DummyBinder _, tv) ->
(* Dummy binding: check if the value contains borrows or loans *)
if VU.borrows_in_value tv || VU.loans_in_value tv then Some ev
else None
@@ -419,8 +425,8 @@ module Contexts = struct
PT.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_decls
in
let var_id_to_string vid =
- let bv = C.ctx_lookup_binder ctx vid in
- binder_to_string bv
+ let bv = C.ctx_lookup_var_binder ctx vid in
+ var_binder_to_string bv
in
let adt_field_names =
PT.type_ctx_to_adt_field_names_fun ctx.type_context.type_decls
@@ -492,8 +498,8 @@ module Contexts = struct
List.iter
(fun ev ->
match ev with
- | C.Var (None, _) -> num_dummies := !num_abs + 1
- | C.Var (Some _, _) -> num_bindings := !num_bindings + 1
+ | C.Var (DummyBinder _, _) -> num_dummies := !num_abs + 1
+ | C.Var (VarBinder _, _) -> num_bindings := !num_bindings + 1
| C.Abs _ -> num_abs := !num_abs + 1
| _ -> raise (Failure "Unreachable"))
f;
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 604a7948..39709a13 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -18,7 +18,7 @@ module A = LlbcAst
the generated code.
*)
type mplace = {
- bv : Contexts.binder;
+ bv : Contexts.var_binder;
(** It is important that we store the binder, and not just the variable id,
because the most important information in a place is the name of the
variable!
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 383ff15e..504fcdb5 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -7,7 +7,7 @@ module A = LlbcAst
open SymbolicAst
let mk_mplace (p : E.place) (ctx : Contexts.eval_ctx) : mplace =
- let bv = Contexts.ctx_lookup_binder ctx p.var_id in
+ let bv = Contexts.ctx_lookup_var_binder ctx p.var_id in
{ bv; projection = p.projection }
let mk_opt_mplace (p : E.place option) (ctx : Contexts.eval_ctx) : mplace option
--
cgit v1.2.3