summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/InterpreterLoops.ml8
-rw-r--r--compiler/Substitute.ml11
-rw-r--r--compiler/Values.ml58
3 files changed, 54 insertions, 23 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index cc8cdcff..e302ea41 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -11,7 +11,6 @@ open ValuesUtils
module Inv = Invariants
module S = SynthesizeSymbolic
module UF = UnionFind
-open Utils
open Cps
open InterpreterUtils
open InterpreterBorrows
@@ -1046,9 +1045,8 @@ let collapse_ctx_with_merge (loop_id : V.LoopId.id)
with ValueMatchFailure _ -> raise (Failure "Unexpected")
(** Join two contexts *)
-let join_ctxs (config : C.config) (loop_id : V.LoopId.id)
- (old_ids : InterpreterBorrowsCore.ctx_ids) (ctx0 : C.eval_ctx)
- (ctx1 : C.eval_ctx) : ctx_or_update =
+let join_ctxs (loop_id : V.LoopId.id) (old_ids : InterpreterBorrowsCore.ctx_ids)
+ (ctx0 : C.eval_ctx) (ctx1 : C.eval_ctx) : ctx_or_update =
let env0 = List.rev ctx0.env in
let env1 = List.rev ctx1.env in
@@ -1209,7 +1207,7 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
*)
let joined_ctx = ref old_ctx in
let rec join_one_aux (ctx : C.eval_ctx) : unit =
- match join_ctxs config loop_id old_ids !joined_ctx ctx with
+ match join_ctxs loop_id old_ids !joined_ctx ctx with
| Ok nctx -> joined_ctx := nctx
| Error err ->
let ctx =
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 0978e078..415f4d59 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -400,13 +400,12 @@ let subst_ids_visitor (rsubst : T.RegionId.id -> T.RegionId.id)
inherit [_] V.map_abs
method! visit_borrow_id _ bid = bsubst bid
method! visit_loan_id _ bid = bsubst bid
-
- method! visit_symbolic_value env sv =
- let sv_id = ssubst sv.sv_id in
- let sv_ty = subst_rty#visit_ty env sv.sv_ty in
- { sv with V.sv_id; sv_ty }
-
method! visit_ety _ ty = ty_substitute_ids tsubst ty
+ method! visit_rty env ty = subst_rty#visit_ty env ty
+ method! visit_symbolic_value_id _ id = ssubst id
+
+ (** We *do* visit meta-values *)
+ method! visit_msymbolic_value env sv = self#visit_symbolic_value env sv
(** We *do* visit meta-values *)
method! visit_mvalue env v = self#visit_typed_value env v
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 9c68ad4f..f6f4d1b6 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -15,6 +15,7 @@ module LoopId = IdGen ()
type big_int = PrimitiveValues.big_int [@@deriving show, ord]
type scalar_value = PrimitiveValues.scalar_value [@@deriving show, ord]
type primitive_value = PrimitiveValues.primitive_value [@@deriving show, ord]
+type symbolic_value_id = SymbolicValueId.id [@@deriving show, ord]
(** The kind of a symbolic value, which precises how the value was generated.
@@ -49,13 +50,54 @@ type sv_kind =
(** The result of a loop join (when computing loop fixed points) *)
[@@deriving show, ord]
+(** Ancestor for {!symbolic_value} iter visitor *)
+class ['self] iter_symbolic_value_base =
+ object (_self : 'self)
+ inherit [_] VisitorsRuntime.iter
+ method visit_sv_kind : 'env -> sv_kind -> unit = fun _ _ -> ()
+ method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
+
+ method visit_symbolic_value_id : 'env -> symbolic_value_id -> unit =
+ fun _ _ -> ()
+ end
+
+(** Ancestor for {!symbolic_value} map visitor for *)
+class ['self] map_symbolic_value_base =
+ object (_self : 'self)
+ inherit [_] VisitorsRuntime.map
+ method visit_sv_kind : 'env -> sv_kind -> sv_kind = fun _ x -> x
+ method visit_rty : 'env -> rty -> rty = fun _ x -> x
+
+ method visit_symbolic_value_id
+ : 'env -> symbolic_value_id -> symbolic_value_id =
+ fun _ x -> x
+ end
+
(** A symbolic value *)
type symbolic_value = {
sv_kind : sv_kind;
- sv_id : SymbolicValueId.id;
+ sv_id : symbolic_value_id;
sv_ty : rty;
}
-[@@deriving show, ord]
+[@@deriving
+ show,
+ ord,
+ visitors
+ {
+ name = "iter_symbolic_value";
+ variety = "iter";
+ ancestors = [ "iter_symbolic_value_base" ];
+ nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+ concrete = true;
+ },
+ visitors
+ {
+ name = "map_symbolic_value";
+ variety = "map";
+ ancestors = [ "map_symbolic_value_base" ];
+ nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
+ concrete = true;
+ }]
type borrow_id = BorrowId.id [@@deriving show, ord]
type borrow_id_set = BorrowId.Set.t [@@deriving show, ord]
@@ -65,13 +107,12 @@ type loan_id_set = BorrowId.Set.t [@@deriving show, ord]
(** Ancestor for {!typed_value} iter visitor *)
class ['self] iter_typed_value_base =
object (self : 'self)
- inherit [_] VisitorsRuntime.iter
+ inherit [_] iter_symbolic_value
method visit_primitive_value : 'env -> primitive_value -> unit =
fun _ _ -> ()
method visit_erased_region : 'env -> erased_region -> unit = fun _ _ -> ()
- method visit_symbolic_value : 'env -> symbolic_value -> unit = fun _ _ -> ()
method visit_variant_id : 'env -> variant_id -> unit = fun _ _ -> ()
method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
method visit_borrow_id : 'env -> borrow_id -> unit = fun _ _ -> ()
@@ -87,7 +128,7 @@ class ['self] iter_typed_value_base =
(** Ancestor for {!typed_value} map visitor for *)
class ['self] map_typed_value_base =
object (self : 'self)
- inherit [_] VisitorsRuntime.map
+ inherit [_] map_symbolic_value
method visit_primitive_value : 'env -> primitive_value -> primitive_value =
fun _ cv -> cv
@@ -95,9 +136,6 @@ class ['self] map_typed_value_base =
method visit_erased_region : 'env -> erased_region -> erased_region =
fun _ r -> r
- method visit_symbolic_value : 'env -> symbolic_value -> symbolic_value =
- fun _ sv -> sv
-
method visit_ety : 'env -> ety -> ety = fun _ ty -> ty
method visit_variant_id : 'env -> variant_id -> variant_id = fun _ x -> x
method visit_borrow_id : 'env -> borrow_id -> borrow_id = fun _ id -> id
@@ -243,8 +281,6 @@ class ['self] iter_typed_value =
method visit_msymbolic_value : 'env -> msymbolic_value -> unit =
fun _ _ -> ()
-
- method visit_rty : 'env -> rty -> unit = fun _ _ -> ()
end
class ['self] map_typed_value =
@@ -255,8 +291,6 @@ class ['self] map_typed_value =
to ignore meta-values *)
method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
- method visit_rty : 'env -> rty -> rty = fun _ ty -> ty
-
method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value =
fun _ m -> m
end
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 14:42:22 +0000