diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterExpansion.ml | 57 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 21 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 3 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 27 | ||||
| -rw-r--r-- | src/PrintPure.ml | 4 | ||||
| -rw-r--r-- | src/SymbolicAst.ml | 35 | ||||
| -rw-r--r-- | src/SynthesizeSymbolic.ml | 61 |
7 files changed, 150 insertions, 58 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 2dd36535..77bf0bd8 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -12,6 +12,7 @@ module L = Logging open TypesUtils module Inv = Invariants module S = SynthesizeSymbolic +module SA = SymbolicAst open Cps open ValuesUtils open InterpreterUtils @@ -264,7 +265,8 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) : see let expand_symbolic_value_shared_borrow (config : C.config) - (original_sv : V.symbolic_value) (ref_ty : T.rty) : cm_fun = + (original_sv : V.symbolic_value) (original_sv_place : SA.place option) + (ref_ty : T.rty) : cm_fun = fun cf ctx -> (* First, replace the projectors on borrows. * The important point is that the symbolic value to expand may appear @@ -374,12 +376,14 @@ let expand_symbolic_value_shared_borrow (config : C.config) (* Call the continuation *) let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see expr + S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place see + expr (** TODO: simplify and merge with the other expansion function *) let expand_symbolic_value_borrow (config : C.config) - (original_sv : V.symbolic_value) (region : T.RegionId.id T.region) - (ref_ty : T.rty) (rkind : T.ref_kind) : cm_fun = + (original_sv : V.symbolic_value) (original_sv_place : SA.place option) + (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) : + cm_fun = fun cf ctx -> (* Check that we are allowed to expand the reference *) assert (not (region_in_set region ctx.ended_regions)); @@ -407,9 +411,11 @@ let expand_symbolic_value_borrow (config : C.config) (* Apply the continuation *) let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see expr + S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place + see expr | T.Shared -> - expand_symbolic_value_shared_borrow config original_sv ref_ty cf ctx + expand_symbolic_value_shared_borrow config original_sv original_sv_place + ref_ty cf ctx (** A small helper. @@ -420,7 +426,7 @@ let expand_symbolic_value_borrow (config : C.config) [see_cf_l]: list of pairs (optional symbolic expansion, continuation) *) let apply_branching_symbolic_expansions_non_borrow (config : C.config) - (sv : V.symbolic_value) + (sv : V.symbolic_value) (sv_place : SA.place option) (see_cf_l : (V.symbolic_expansion option * m_fun) list) : m_fun = fun ctx -> assert (see_cf_l <> []); @@ -450,7 +456,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config) in (* Synthesize and return *) let seel = List.map fst see_cf_l in - S.synthesize_symbolic_expansion sv seel subterms + S.synthesize_symbolic_expansion sv sv_place seel subterms (** Expand a symbolic value which is not an enumeration with several variants (i.e., in a situation where it doesn't lead to branching). @@ -461,7 +467,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config) TODO: rename [sp] to [sv] *) let expand_symbolic_value (config : C.config) (allow_branching : bool) - (sp : V.symbolic_value) : cm_fun = + (sp : V.symbolic_value) (sp_place : SA.place option) : cm_fun = fun cf ctx -> (* Debug *) log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sp)); @@ -470,6 +476,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) (* Compute the expanded value - note that when doing so, we may introduce * fresh symbolic values in the context (which thus gets updated) *) let original_sv = sp in + let original_sv_place = sp_place in let rty = original_sv.V.sv_ty in let cc : cm_fun = fun cf ctx -> @@ -485,8 +492,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) assert (List.length seel <= 1 || allow_branching); (* Apply *) let seel = List.map (fun see -> (Some see, cf)) seel in - apply_branching_symbolic_expansions_non_borrow config original_sv seel - ctx + apply_branching_symbolic_expansions_non_borrow config original_sv + original_sv_place seel ctx (* Tuples *) | T.Adt (T.Tuple, [], tys) -> (* Generate the field values *) @@ -498,7 +505,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) (* Call the continuation *) let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see expr + S.synthesize_symbolic_expansion_no_branching original_sv + original_sv_place see expr (* Boxes *) | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in @@ -509,11 +517,12 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) (* Call the continuation *) let expr = cf ctx in (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see expr + S.synthesize_symbolic_expansion_no_branching original_sv + original_sv_place see expr (* Borrows *) | T.Ref (region, ref_ty, rkind) -> - expand_symbolic_value_borrow config original_sv region ref_ty rkind cf - ctx + expand_symbolic_value_borrow config original_sv original_sv_place region + ref_ty rkind cf ctx (* Booleans *) | T.Bool -> assert allow_branching; @@ -523,8 +532,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) let seel = [ see_true; see_false ] in let seel = List.map (fun see -> (Some see, cf)) seel in (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *) - apply_branching_symbolic_expansions_non_borrow config original_sv seel - ctx + apply_branching_symbolic_expansions_non_borrow config original_sv + original_sv_place seel ctx | _ -> failwith ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty) in (* Debug *) @@ -569,8 +578,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) switch. The continuation is thus for the execution *after* the switch. *) let expand_symbolic_int (config : C.config) (sv : V.symbolic_value) - (int_type : T.integer_type) (tgts : (V.scalar_value * m_fun) list) - (otherwise : m_fun) : m_fun = + (sv_place : SA.place option) (int_type : T.integer_type) + (tgts : (V.scalar_value * m_fun) list) (otherwise : m_fun) : m_fun = (* Sanity check *) assert (sv.V.sv_ty = T.Integer int_type); (* For all the branches of the switch, we expand the symbolic value @@ -587,13 +596,13 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value) in let tgts = List.append tgts [ (None, otherwise) ] in (* Then expand and evaluate - this generates the proper symbolic AST *) - apply_branching_symbolic_expansions_non_borrow config sv tgts + apply_branching_symbolic_expansions_non_borrow config sv sv_place tgts (** See [expand_symbolic_value] *) let expand_symbolic_value_no_branching (config : C.config) - (sp : V.symbolic_value) : cm_fun = + (sv : V.symbolic_value) (sv_place : SA.place option) : cm_fun = let allow_branching = false in - expand_symbolic_value config allow_branching sp + expand_symbolic_value config allow_branching sv sv_place (** Expand all the symbolic values which contain borrows. Allows us to restrict ourselves to a simpler model for the projectors over @@ -649,10 +658,10 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = ("Attempted to greedily expand a recursive definition (option \ [greedy_expand_symbolics_with_borrows] of [config]): " ^ Print.name_to_string def.name) - else expand_symbolic_value_no_branching config sv + else expand_symbolic_value_no_branching config sv None | T.Adt ((Tuple | Assumed Box), _, _) | T.Ref (_, _, _) -> (* Ok *) - expand_symbolic_value_no_branching config sv + expand_symbolic_value_no_branching config sv None | T.Array _ -> raise Errors.Unimplemented | T.Slice _ -> failwith "Can't expand symbolic slices" | T.TypeVar _ | Bool | Char | Never | Integer _ | Str -> diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 84f51c94..356bae2d 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -39,7 +39,9 @@ let expand_primitively_copyable_at_place (config : C.config) with | None -> cf ctx | Some sv -> - let cc = expand_symbolic_value_no_branching config sv in + let cc = + expand_symbolic_value_no_branching config sv (Some (S.mk_place p ctx)) + in comp cc expand cf ctx in (* Apply *) @@ -290,7 +292,9 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand) (* Call the continuation *) let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in (* Synthesize the symbolic AST *) - S.synthesize_unary_op unop v res_sv expr + S.synthesize_unary_op unop v + (S.mk_opt_place_from_op op ctx) + res_sv None expr in (* Compose and apply *) comp eval_op apply cf ctx @@ -427,7 +431,9 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop) let v = mk_typed_value_from_symbolic_value res_sv in let expr = cf (Ok v) ctx in (* Synthesize the symbolic AST *) - S.synthesize_binary_op binop v1 v2 res_sv expr + let p1 = S.mk_opt_place_from_op op1 ctx in + let p2 = S.mk_opt_place_from_op op2 ctx in + S.synthesize_binary_op binop v1 p1 v2 p2 res_sv None expr in (* Compose and apply *) comp eval_ops compute cf ctx @@ -488,7 +494,10 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place) | Symbolic sv -> (* Expand the symbolic value - may lead to branching *) let allow_branching = true in - let cc = expand_symbolic_value config allow_branching sv in + let cc = + expand_symbolic_value config allow_branching sv + (Some (S.mk_place p ctx)) + in (* This time the value is concrete: reevaluate *) comp cc (eval_rvalue_discriminant_concrete config p) cf ctx | _ -> failwith "Invalid input for `discriminant`" @@ -584,7 +593,7 @@ let eval_rvalue_aggregate (config : C.config) (* Call the continuation *) let expr = cf aggregated ctx in (* Synthesize the symbolic AST *) - S.synthesize_aggregated_value aggregated expr + S.synthesize_aggregated_value aggregated None expr | E.AggregatedAdt (def_id, opt_variant_id, regions, types) -> (* Sanity checks *) let type_def = C.ctx_lookup_type_def ctx def_id in @@ -605,7 +614,7 @@ let eval_rvalue_aggregate (config : C.config) (* Call the continuation *) let expr = cf aggregated ctx in (* Synthesize the symbolic AST *) - S.synthesize_aggregated_value aggregated expr + S.synthesize_aggregated_value aggregated None expr in (* Compose and apply *) comp eval_ops compute cf diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 300e50c5..8b103eb8 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -11,6 +11,7 @@ open InterpreterUtils open InterpreterBorrowsCore open InterpreterBorrows open InterpreterExpansion +module Synth = SynthesizeSymbolic (** The local logger *) let log = L.paths_log @@ -473,6 +474,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind) | FailSymbolic (_pe, sp) -> (* Expand the symbolic value *) expand_symbolic_value_no_branching config sp + (Some (Synth.mk_place p ctx)) | FailBottom (_, _, _) -> (* We can't expand [Bottom] values while reading them *) failwith "Found [Bottom] while reading a place" @@ -502,6 +504,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind) | FailSymbolic (_pe, sp) -> (* Expand the symbolic value *) expand_symbolic_value_no_branching config sp + (Some (Synth.mk_place p ctx)) | FailBottom (remaining_pes, pe, ty) -> (* Expand the [Bottom] value *) fun cf ctx -> diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index b0d4e5e0..16c66094 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -155,7 +155,10 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun = (* Expand the symbolic value, then call the evaluation function for the * non-symbolic case *) let allow_branching = true in - let expand = expand_symbolic_value config allow_branching sv in + let expand = + expand_symbolic_value config allow_branching sv + (S.mk_opt_place_from_op assertion.cond ctx) + in comp expand (eval_assertion_concrete config assertion) cf ctx | _ -> failwith ("Expected a boolean, got: " ^ typed_value_to_string ctx v) in @@ -804,6 +807,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = (** Evaluate a switch *) and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : st_cm_fun = + fun cf ctx -> (* We evaluate the operand in two steps: * first we prepare it, then we check if its value is concrete or * symbolic. If it is concrete, we can then evaluate the operand @@ -816,6 +820,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : let cf_prepare_op cf : m_fun = eval_operand_prepare config op cf in (* Match on the targets *) let cf_match (cf : st_m_fun) (op_v : V.typed_value) : m_fun = + fun ctx -> match tgts with | A.If (st1, st2) -> ( match op_v.value with @@ -830,17 +835,19 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : else eval_statement config st2 cf in (* Compose the continuations *) - comp cf_eval_op cf_branch cf + comp cf_eval_op cf_branch cf ctx | V.Symbolic sv -> (* Expand the symbolic value *) let allows_branching = true in let cf_expand cf = - expand_symbolic_value config allows_branching sv cf + expand_symbolic_value config allows_branching sv + (S.mk_opt_place_from_op op ctx) + cf in (* Retry *) let cf_eval_if cf = eval_switch config op tgts cf in (* Compose *) - comp cf_expand cf_eval_if cf + comp cf_expand cf_eval_if cf ctx | _ -> failwith "Inconsistent state") | A.SwitchInt (int_ty, stgts, otherwise) -> ( match op_v.value with @@ -858,7 +865,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : | Some (_, tgt) -> eval_statement config tgt cf in (* Compose *) - comp cf_eval_op cf_eval_branch cf + comp cf_eval_op cf_eval_branch cf ctx | V.Symbolic sv -> (* Expand the symbolic value - note that contrary to the boolean * case, we can't expand then retry, because when switching over @@ -871,11 +878,13 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) : stgts in let otherwise = eval_statement config otherwise cf in - expand_symbolic_int config sv int_ty stgts otherwise + expand_symbolic_int config sv + (S.mk_opt_place_from_op op ctx) + int_ty stgts otherwise ctx | _ -> failwith "Inconsistent state") in (* Compose the continuations *) - comp cf_prepare_op cf_match + comp cf_prepare_op cf_match cf ctx (** Evaluate a function call (auxiliary helper for [eval_statement]) *) and eval_function_call (config : C.config) (call : A.call) : st_cm_fun = @@ -992,6 +1001,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) let ret_av regions = mk_aproj_loans_value_from_symbolic_value regions ret_spc in + let args_places = List.map (fun p -> S.mk_opt_place_from_op p ctx) args in + let dest_place = Some (S.mk_place dest ctx) in (* Evaluate the input operands *) let cc = eval_operands config args in @@ -1047,7 +1058,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (* Synthesize the symbolic AST *) let abs_ids = List.map (fun rg -> rg.T.id) inst_sg.regions_hierarchy in S.synthesize_regular_function_call fid call_id abs_ids type_params args - ret_spc expr + args_places ret_spc dest_place expr in let cc = comp cc cf_call in diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 3d41e67d..b631f940 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -183,7 +183,7 @@ let type_def_to_string (fmt : type_formatter) (def : type_def) : string = "enum " ^ name ^ params ^ " =\n" ^ variants let var_to_string (fmt : type_formatter) (v : var) : string = - "(" ^ VarId.to_string v.id ^ " : " ^ ty_to_string fmt v.ty ^ ")" + "(@" ^ VarId.to_string v.id ^ " : " ^ ty_to_string fmt v.ty ^ ")" let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string = match v with @@ -218,7 +218,7 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string) "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name)) let place_to_string (fmt : ast_formatter) (p : place) : string = - let var = fmt.var_id_to_string p.var in + let var = "@" ^ fmt.var_id_to_string p.var in projection_to_string fmt var p.projection let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml index f0873aa3..a3aedeab 100644 --- a/src/SymbolicAst.ml +++ b/src/SymbolicAst.ml @@ -9,6 +9,25 @@ module V = Values module E = Expressions module A = CfimAst +type place = { + bv : Contexts.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! + *) + projection : E.projection; + (** We store the projection because we can, but it is actually not that useful *) +} +(** In this module, [place] is meta information. + + Whenever we need to introduce new symbolic variables, for instance because + of symbolic expansions, we try to store a "place", which gives information + about the origin of the values (this place information comes from assignment + information, etc.). + We later use this place information to generate meaningful name, to prettify + the generated code. + *) + type call_id = | Fun of A.fun_id * V.FunCallId.id (** A "regular" function (i.e., a function which is not a primitive operation) *) @@ -21,7 +40,9 @@ type call = { abstractions : V.AbstractionId.id list; type_params : T.ety list; args : V.typed_value list; + args_places : place option list; (** Meta information *) dest : V.symbolic_value; + dest_place : place option; (** Meta information *) } (** **Rk.:** here, [expression] is not at all equivalent to the expressions @@ -37,7 +58,15 @@ type expression = | Panic | FunCall of call * expression | EndAbstraction of V.abs * expression - | Expansion of V.symbolic_value * expansion + | Expansion of place option * V.symbolic_value * expansion + (** Expansion of a symbolic value. + + The place is "meta": it gives the path to the symbolic value (if available) + which got expanded (this path is available when the symbolic expansion + comes from a path evaluation, during an assignment for instance). + We use it to compute meaningful names for the variables we introduce, + to prettify the generated code. + *) | Meta of meta * expression (** Meta information *) and expansion = @@ -63,4 +92,6 @@ and expansion = generate a pretty output. *) -and meta = Aggregate of V.typed_value (** We generated an aggregate value *) +and meta = + | Aggregate of place option * V.typed_value + (** We generated an aggregate value *) diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml index 6aec95bd..7050c14b 100644 --- a/src/SynthesizeSymbolic.ml +++ b/src/SynthesizeSymbolic.ml @@ -5,7 +5,20 @@ module E = Expressions module A = CfimAst open SymbolicAst -let synthesize_symbolic_expansion (sv : V.symbolic_value) +let mk_place (p : E.place) (ctx : Contexts.eval_ctx) : place = + let bv = Contexts.ctx_lookup_binder ctx p.var_id in + { bv; projection = p.projection } + +let mk_opt_place (p : E.place option) (ctx : Contexts.eval_ctx) : place option = + match p with None -> None | Some p -> Some (mk_place p ctx) + +let mk_opt_place_from_op (op : E.operand) (ctx : Contexts.eval_ctx) : + place option = + match op with + | E.Copy p | E.Move p -> Some (mk_place p ctx) + | E.Constant _ -> None + +let synthesize_symbolic_expansion (sv : V.symbolic_value) (place : place option) (seel : V.symbolic_expansion option list) (exprl : expression list option) : expression option = match exprl with @@ -71,46 +84,62 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) | T.TypeVar _ | Char | Never | Str | Array _ | Slice _ -> failwith "Ill-formed symbolic expansion" in - Some (Expansion (sv, expansion)) + Some (Expansion (place, sv, expansion)) let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value) - (see : V.symbolic_expansion) (expr : expression option) : expression option - = + (place : place option) (see : V.symbolic_expansion) + (expr : expression option) : expression option = let exprl = match expr with None -> None | Some expr -> Some [ expr ] in - synthesize_symbolic_expansion sv [ Some see ] exprl + synthesize_symbolic_expansion sv place [ Some see ] exprl let synthesize_function_call (call_id : call_id) (abstractions : V.AbstractionId.id list) (type_params : T.ety list) - (args : V.typed_value list) (dest : V.symbolic_value) + (args : V.typed_value list) (args_places : place option list) + (dest : V.symbolic_value) (dest_place : place option) (expr : expression option) : expression option = match expr with | None -> None | Some expr -> - let call = { call_id; abstractions; type_params; args; dest } in + let call = + { + call_id; + abstractions; + type_params; + args; + dest; + args_places; + dest_place; + } + in Some (FunCall (call, expr)) let synthesize_regular_function_call (fun_id : A.fun_id) (call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list) (type_params : T.ety list) (args : V.typed_value list) - (dest : V.symbolic_value) (expr : expression option) : expression option = + (args_places : place option list) (dest : V.symbolic_value) + (dest_place : place option) (expr : expression option) : expression option = synthesize_function_call (Fun (fun_id, call_id)) - abstractions type_params args dest expr + abstractions type_params args args_places dest dest_place expr let synthesize_unary_op (unop : E.unop) (arg : V.typed_value) - (dest : V.symbolic_value) (expr : expression option) : expression option = - synthesize_function_call (Unop unop) [] [] [ arg ] dest expr + (arg_place : place option) (dest : V.symbolic_value) + (dest_place : place option) (expr : expression option) : expression option = + synthesize_function_call (Unop unop) [] [] [ arg ] [ arg_place ] dest + dest_place expr let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value) - (arg1 : V.typed_value) (dest : V.symbolic_value) (expr : expression option) - : expression option = - synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ] dest expr + (arg0_place : place option) (arg1 : V.typed_value) + (arg1_place : place option) (dest : V.symbolic_value) + (dest_place : place option) (expr : expression option) : expression option = + synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ] + [ arg0_place; arg1_place ] dest dest_place expr -let synthesize_aggregated_value (aggr_v : V.typed_value) +let synthesize_aggregated_value (aggr_v : V.typed_value) (place : place option) (expr : expression option) : expression option = match expr with | None -> None - | Some expr -> Some (Meta (Aggregate aggr_v, expr)) + | Some expr -> Some (Meta (Aggregate (place, aggr_v), expr)) let synthesize_end_abstraction (abs : V.abs) (expr : expression option) : expression option = |