diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterLoops.ml | 8 | ||||
| -rw-r--r-- | compiler/Substitute.ml | 11 | ||||
| -rw-r--r-- | compiler/Values.ml | 58 |
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 |