From 0d4e85006d06c51194db17a08055c00ee830124a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 20 Apr 2022 15:59:54 +0200 Subject: Introduce mdplace to link meta information about the given back values to the information about the input arguments --- src/InterpreterBorrows.ml | 14 ++-- src/Print.ml | 2 +- src/PrintPure.ml | 50 +++++++------ src/Pure.ml | 179 ++++++++++++++++++++++++++++++++-------------- src/PureMicroPasses.ml | 16 +++-- src/PureUtils.ml | 6 +- src/SymbolicToPure.ml | 45 +++++++----- src/Values.ml | 14 ++-- 8 files changed, 212 insertions(+), 114 deletions(-) diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index d200276f..065a39b9 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -1202,16 +1202,16 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) ^ aborrow_content_to_string ctx bc)); let ctx = match bc with - | V.AMutBorrow (_, bid, av) -> + | V.AMutBorrow (mv, bid, av) -> (* First, convert the avalue to a (fresh symbolic) value *) - let v = convert_avalue_to_given_back_value abs.kind av in + let sv = convert_avalue_to_given_back_value abs.kind av in (* Replace the mut borrow to register the fact that we ended * it and store with it the freshly generated given back value *) - let ended_borrow = V.ABorrow (V.AEndedMutBorrow (v, av)) in + let ended_borrow = V.ABorrow (V.AEndedMutBorrow (mv, sv, av)) in let ctx = update_aborrow ek_all bid ended_borrow ctx in (* Give the value back *) - let v = mk_typed_value_from_symbolic_value v in - give_back_value config bid v ctx + let sv = mk_typed_value_from_symbolic_value sv in + give_back_value config bid sv ctx | V.ASharedBorrow bid -> (* Replace the shared borrow to account for the fact it ended *) let ended_borrow = V.ABorrow V.AEndedSharedBorrow in @@ -1256,7 +1256,9 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (* Generate a fresh symbolic value *) let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in (* Replace the proj_borrows - there should be exactly one *) - let ended_borrow = V.AEndedProjBorrows nsv in + let ended_borrow = + V.AEndedProjBorrows { original = sv; given_back = nsv } + in let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in (* Give back the symbolic value *) let ctx = diff --git a/src/Print.ml b/src/Print.ml index 5ccba517..69379bf9 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -457,7 +457,7 @@ module Values = struct ^ ", " ^ typed_avalue_to_string fmt av ^ ")" - | AEndedMutBorrow (_mv, child) -> + | AEndedMutBorrow (_mv, _msv, child) -> "@ended_mut_borrow(" ^ typed_avalue_to_string fmt child ^ ")" | AEndedIgnoredMutBorrow { child; given_back_loans_proj; given_back_meta = _ } -> diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 09194d85..9ca0c064 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -228,16 +228,6 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string = let name = match p.name with None -> "_" | Some name -> name in projection_to_string fmt name p.projection -let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string = - match v with - | Var (v, Some { name = Some name; projection }) -> - assert (projection = []); - let fmt = value_to_type_formatter fmt in - "(" ^ var_to_varname v ^ " @meta[@dest=" ^ name ^ "] : " - ^ ty_to_string fmt v.ty ^ ")" - | Var (v, _) -> var_to_string (value_to_type_formatter fmt) v - | Dummy -> "_" - let place_to_string (fmt : ast_formatter) (p : place) : string = (* TODO: improve that *) let var = fmt.var_id_to_string p.var in @@ -315,16 +305,6 @@ let adt_g_value_to_string (fmt : value_formatter) ^ "\n- ty: " ^ ty_to_string fmt ty ^ "\n- variant_id: " ^ Print.option_to_string VariantId.to_string variant_id)) -let rec typed_lvalue_to_string (fmt : value_formatter) (v : typed_lvalue) : - string = - match v.value with - | LvConcrete cv -> Print.Values.constant_value_to_string cv - | LvVar var -> var_or_dummy_to_string fmt var - | LvAdt av -> - adt_g_value_to_string fmt - (typed_lvalue_to_string fmt) - av.variant_id av.field_values v.ty - let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string = match v.value with @@ -336,6 +316,32 @@ let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string (typed_rvalue_to_string fmt) av.variant_id av.field_values v.ty +let var_or_dummy_to_string (fmt : ast_formatter) (v : var_or_dummy) : string = + match v with + | Var (v, { place = None; from_rvalue = None }) -> + var_to_string (ast_to_type_formatter fmt) v + | Var (v, { place; from_rvalue }) -> + let dest = Print.option_to_string (mplace_to_string fmt) place in + let from_rvalue = + Print.option_to_string (typed_rvalue_to_string fmt) from_rvalue + in + "(" ^ var_to_varname v ^ " @meta[@dest=" ^ dest ^ ", from_rvalue=" + ^ from_rvalue ^ "] : " + ^ ty_to_string (ast_to_type_formatter fmt) v.ty + ^ ")" + | Dummy -> "_" + +let rec typed_lvalue_to_string (fmt : ast_formatter) (v : typed_lvalue) : string + = + match v.value with + | LvConcrete cv -> Print.Values.constant_value_to_string cv + | LvVar var -> var_or_dummy_to_string fmt var + | LvAdt av -> + adt_g_value_to_string + (ast_to_value_formatter fmt) + (typed_lvalue_to_string fmt) + av.variant_id av.field_values v.ty + let fun_sig_to_string (fmt : ast_formatter) (sg : fun_sig) : string = let ty_fmt = ast_to_type_formatter fmt in let type_params = List.map type_var_to_string sg.type_params in @@ -452,7 +458,7 @@ and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) let indent1 = indent ^ indent_incr in let re = texpression_to_string fmt indent1 indent_incr re in let e = texpression_to_string fmt indent indent_incr e in - let lv = typed_lvalue_to_string (ast_to_value_formatter fmt) lv in + let lv = typed_lvalue_to_string fmt lv in if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e @@ -472,7 +478,7 @@ and switch_to_string (fmt : ast_formatter) (indent : string) ^ "else\n" ^ indent ^ e_false | Match branches -> let branch_to_string (b : match_branch) : string = - let pat = typed_lvalue_to_string (ast_to_value_formatter fmt) b.pat in + let pat = typed_lvalue_to_string fmt b.pat in indent ^ "| " ^ pat ^ " ->\n" ^ indent1 ^ texpression_to_string fmt indent1 indent_incr b.branch in diff --git a/src/Pure.ml b/src/Pure.ml index 58ee0b98..dbc6421c 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -182,7 +182,7 @@ class ['self] iter_value_base = method visit_ty : 'env -> ty -> unit = fun _ _ -> () end -(** Ancestor for [map_var_or_dummy] visitor *) +(** Ancestor for [map_typed_rvalue] visitor *) class ['self] map_value_base = object (_self : 'self) inherit [_] VisitorsRuntime.map @@ -199,7 +199,7 @@ class ['self] map_value_base = method visit_ty : 'env -> ty -> ty = fun _ x -> x end -(** Ancestor for [reduce_var_or_dummy] visitor *) +(** Ancestor for [reduce_typed_rvalue] visitor *) class virtual ['self] reduce_value_base = object (self : 'self) inherit [_] VisitorsRuntime.reduce @@ -216,7 +216,7 @@ class virtual ['self] reduce_value_base = method visit_ty : 'env -> ty -> 'a = fun _ _ -> self#zero end -(** Ancestor for [mapreduce_var_or_dummy] visitor *) +(** Ancestor for [mapreduce_typed_rvalue] visitor *) class virtual ['self] mapreduce_value_base = object (self : 'self) inherit [_] VisitorsRuntime.mapreduce @@ -235,14 +235,22 @@ class virtual ['self] mapreduce_value_base = method visit_ty : 'env -> ty -> ty * 'a = fun _ x -> (x, self#zero) end -type var_or_dummy = - | Var of var * mplace option (* TODO: the mplace is actually always a variable *) - | Dummy (** Ignored value: `_`. *) +type rvalue = + | RvConcrete of constant_value + | RvPlace of place + | RvAdt of adt_rvalue + +and adt_rvalue = { + variant_id : (VariantId.id option[@opaque]); + field_values : typed_rvalue list; +} + +and typed_rvalue = { value : rvalue; ty : ty } [@@deriving show, visitors { - name = "iter_var_or_dummy"; + name = "iter_typed_rvalue"; variety = "iter"; ancestors = [ "iter_value_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); @@ -251,125 +259,186 @@ type var_or_dummy = }, visitors { - name = "map_var_or_dummy"; + name = "map_typed_rvalue"; variety = "map"; ancestors = [ "map_value_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.map] *); + nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; polymorphic = false; }, visitors { - name = "reduce_var_or_dummy"; + name = "reduce_typed_rvalue"; variety = "reduce"; ancestors = [ "reduce_value_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.reduce] *); + nude = true (* Don't inherit [VisitorsRuntime.iter] *); polymorphic = false; }, visitors { - name = "mapreduce_var_or_dummy"; + name = "mapreduce_typed_rvalue"; variety = "mapreduce"; ancestors = [ "mapreduce_value_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.reduce] *); + nude = true (* Don't inherit [VisitorsRuntime.iter] *); polymorphic = false; }] -(** A left value (which appears on the left of assignments *) -type lvalue = - | LvConcrete of constant_value - (** [LvConcrete] is necessary because we merge the switches over integer - values and the matches over enumerations *) - | LvVar of var_or_dummy - | LvAdt of adt_lvalue +type mdplace = { place : mplace option; from_rvalue : typed_rvalue option } +[@@deriving show] +(** "Meta" destination place. + + Meta information for places used as assignment destinations. + This is useful for the values given back by the backward functions: in such + situations, we link the output variables to the input arguments, to derive + names for the output variables from the input variables. + + Ex.: + ==== + ``` + let y = f<'a>(&mut x); + ... + // end 'a + ... + ``` + gets translated to: + ``` + let y = f_fwd x in + ... + let s = f_back x y_i in // we want the introduced variable to be name "x1" + ... + ``` + In order to compute a proper name for the variable introduced by the backward + call, we need to link `s` to `x`. However, because of desugaring, it may happen + that the fact `f` takes `x` as argument may have to be computed by propagating + naming information. This is why we link the output variables to the input arguments: + it allows us to propagate such naming constraints "across" function calls. + *) -and adt_lvalue = { - variant_id : (VariantId.id option[@opaque]); - field_values : typed_lvalue list; -} +(** Ancestor for [iter_var_or_dummy] visitor *) +class ['self] iter_var_or_dummy_base = + object (_self : 'self) + inherit [_] iter_typed_rvalue -and typed_lvalue = { value : lvalue; ty : ty } + method visit_mdplace : 'env -> mdplace -> unit = fun _ _ -> () + end + +(** Ancestor for [map_var_or_dummy] visitor *) +class ['self] map_var_or_dummy_base = + object (_self : 'self) + inherit [_] map_typed_rvalue + + method visit_mdplace : 'env -> mdplace -> mdplace = fun _ x -> x + end + +(** Ancestor for [reduce_var_or_dummy] visitor *) +class virtual ['self] reduce_var_or_dummy_base = + object (self : 'self) + inherit [_] reduce_typed_rvalue + + method visit_mdplace : 'env -> mdplace -> 'a = fun _ _ -> self#zero + end + +(** Ancestor for [mapreduce_var_or_dummy] visitor *) +class virtual ['self] mapreduce_var_or_dummy_base = + object (self : 'self) + inherit [_] mapreduce_typed_rvalue + + method visit_mdplace : 'env -> mdplace -> mdplace * 'a = + fun _ x -> (x, self#zero) + end + +type var_or_dummy = + | Var of var * mdplace + (** Rk.: the mdplace is actually always a variable (i.e.: there are no projections). + + We use [mplace] because it leads to a more uniform treatment of the meta + information. + *) + | Dummy (** Ignored value: `_`. *) [@@deriving show, visitors { - name = "iter_typed_lvalue"; + name = "iter_var_or_dummy"; variety = "iter"; - ancestors = [ "iter_var_or_dummy" ]; + ancestors = [ "iter_var_or_dummy_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; polymorphic = false; }, visitors { - name = "map_typed_lvalue"; + name = "map_var_or_dummy"; variety = "map"; - ancestors = [ "map_var_or_dummy" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); + ancestors = [ "map_var_or_dummy_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.map] *); concrete = true; polymorphic = false; }, visitors { - name = "reduce_typed_lvalue"; + name = "reduce_var_or_dummy"; variety = "reduce"; - ancestors = [ "reduce_var_or_dummy" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); + ancestors = [ "reduce_var_or_dummy_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.reduce] *); polymorphic = false; }, visitors { - name = "mapreduce_typed_lvalue"; + name = "mapreduce_var_or_dummy"; variety = "mapreduce"; - ancestors = [ "mapreduce_var_or_dummy" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); + ancestors = [ "mapreduce_var_or_dummy_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.reduce] *); polymorphic = false; }] -type rvalue = - | RvConcrete of constant_value - | RvPlace of place - | RvAdt of adt_rvalue +(** A left value (which appears on the left of assignments *) +type lvalue = + | LvConcrete of constant_value + (** [LvConcrete] is necessary because we merge the switches over integer + values and the matches over enumerations *) + | LvVar of var_or_dummy + | LvAdt of adt_lvalue -and adt_rvalue = { +and adt_lvalue = { variant_id : (VariantId.id option[@opaque]); - field_values : typed_rvalue list; + field_values : typed_lvalue list; } -and typed_rvalue = { value : rvalue; ty : ty } +and typed_lvalue = { value : lvalue; ty : ty } [@@deriving show, visitors { - name = "iter_typed_rvalue"; + name = "iter_typed_lvalue"; variety = "iter"; - ancestors = [ "iter_typed_lvalue" ]; + ancestors = [ "iter_var_or_dummy" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; polymorphic = false; }, visitors { - name = "map_typed_rvalue"; + name = "map_typed_lvalue"; variety = "map"; - ancestors = [ "map_typed_lvalue" ]; + ancestors = [ "map_var_or_dummy" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; polymorphic = false; }, visitors { - name = "reduce_typed_rvalue"; + name = "reduce_typed_lvalue"; variety = "reduce"; - ancestors = [ "reduce_typed_lvalue" ]; + ancestors = [ "reduce_var_or_dummy" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); polymorphic = false; }, visitors { - name = "mapreduce_typed_rvalue"; + name = "mapreduce_typed_lvalue"; variety = "mapreduce"; - ancestors = [ "mapreduce_typed_lvalue" ]; + ancestors = [ "mapreduce_var_or_dummy" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); polymorphic = false; }] @@ -398,7 +467,7 @@ type meta = Assignment of mplace * typed_rvalue [@@deriving show] (** Ancestor for [iter_expression] visitor *) class ['self] iter_expression_base = object (_self : 'self) - inherit [_] iter_typed_rvalue + inherit [_] iter_typed_lvalue method visit_meta : 'env -> meta -> unit = fun _ _ -> () @@ -412,7 +481,7 @@ class ['self] iter_expression_base = (** Ancestor for [map_expression] visitor *) class ['self] map_expression_base = object (_self : 'self) - inherit [_] map_typed_rvalue + inherit [_] map_typed_lvalue method visit_meta : 'env -> meta -> meta = fun _ x -> x @@ -428,7 +497,7 @@ class ['self] map_expression_base = (** Ancestor for [reduce_expression] visitor *) class virtual ['self] reduce_expression_base = object (self : 'self) - inherit [_] reduce_typed_rvalue + inherit [_] reduce_typed_lvalue method visit_meta : 'env -> meta -> 'a = fun _ _ -> self#zero @@ -444,7 +513,7 @@ class virtual ['self] reduce_expression_base = (** Ancestor for [mapreduce_expression] visitor *) class virtual ['self] mapreduce_expression_base = object (self : 'self) - inherit [_] mapreduce_typed_rvalue + inherit [_] mapreduce_typed_lvalue method visit_meta : 'env -> meta -> meta * 'a = fun _ x -> (x, self#zero) diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index 06fd3d69..abdeb41e 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -242,11 +242,13 @@ let compute_pretty_names (def : fun_decl) : fun_decl = method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ()) - method! visit_Var _ v mp () = + method! visit_Var _ v mdp () = (* Register the variable *) let ctx = add_var (self#zero ()) v in (* Register the mplace information if there is such information *) - match mp with None -> ctx | Some mp -> add_constraint mp v.id ctx + match mdp.place with + | None -> ctx + | Some mp -> add_constraint mp v.id ctx end in let ctx1 = obj#visit_typed_lvalue () lv () in @@ -820,7 +822,7 @@ let to_monadic (config : config) (def : fun_decl) : fun_decl = let id, _ = VarId.fresh var_cnt in let var = { id; basename = None; ty = unit_ty } in let inputs = [ var ] in - let input_lv = mk_typed_lvalue_from_var var None in + let input_lv = mk_typed_lvalue_from_var var None None in let inputs_lvs = [ input_lv ] in Some { body with inputs; inputs_lvs } in @@ -978,7 +980,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : * monadic binding *) let vid = fresh_id () in let tmp : var = { id = vid; basename = None; ty = lv.ty } in - let ltmp = mk_typed_lvalue_from_var tmp None in + let ltmp = mk_typed_lvalue_from_var tmp None None in let rtmp = mk_typed_rvalue_from_var tmp in let rtmp = mk_value_expression rtmp None in (* Visit the next expression *) @@ -1056,7 +1058,9 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx) in (* The `Success` branch introduces a fresh state variable *) let state_var = fresh_state_var () in - let state_value = mk_typed_lvalue_from_var state_var None in + let state_value = + mk_typed_lvalue_from_var state_var None None + in let success_pat = mk_result_return_lvalue (mk_simpl_tuple_lvalue [ state_value; lv ]) @@ -1127,7 +1131,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx) let sg = { sg with inputs = sg_inputs; outputs = sg_outputs } in (* Update the inputs list *) let inputs = body.inputs @ [ input_state_var ] in - let input_lv = mk_typed_lvalue_from_var input_state_var None in + let input_lv = mk_typed_lvalue_from_var input_state_var None None in let inputs_lvs = body.inputs_lvs @ [ input_lv ] in (* Update the body *) let body = { body with inputs; inputs_lvs } in diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 23bffa1d..78ddf8aa 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -64,8 +64,10 @@ let mk_typed_rvalue_from_var (v : var) : typed_rvalue = let ty = v.ty in { value; ty } -let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue = - let value = LvVar (Var (v, mp)) in +let mk_typed_lvalue_from_var (v : var) (mp : mplace option) + (mfrom_rvalue : typed_rvalue option) : typed_lvalue = + let mdplace = { place = mp; from_rvalue = mfrom_rvalue } in + let value = LvVar (Var (v, mdplace)) in let ty = v.ty in { value; ty } diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index fe500480..87e86e69 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -647,7 +647,7 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue (mk_typed_rvalue_from_var var).value in let ty = ctx_translate_fwd_ty ctx v.ty in - let value = { value; ty } in + let value : typed_rvalue = { value; ty } in (* Debugging *) log#ldebug (lazy @@ -736,7 +736,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : match bc with | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> failwith "Unreachable" - | AEndedMutBorrow (_, _) -> + | AEndedMutBorrow (_, _, _) -> (* We collect consumed values: ignore *) None | AEndedIgnoredMutBorrow _ -> @@ -804,6 +804,9 @@ let translate_opt_mplace (p : S.mplace option) : mplace option = [mp]: it is possible to provide some meta-place information, to guide the heuristics which later find pretty names for the variables. + + TODO: + *) let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue) (ctx : bs_ctx) : bs_ctx * typed_lvalue option = @@ -875,10 +878,13 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) match bc with | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> failwith "Unreachable" - | AEndedMutBorrow (mv, _) -> - (* Return the meta-value *) - let ctx, var = fresh_var_for_symbolic_value mv ctx in - (ctx, Some (mk_typed_lvalue_from_var var mp)) + | AEndedMutBorrow (consumed_mv, msv, _) -> + (* We use the originally consumed value (which is stored as a meta-value) + * to help with propagating naming constraints. *) + let consumed = typed_value_to_rvalue ctx consumed_mv in + (* Return the meta-symbolic-value *) + let ctx, var = fresh_var_for_symbolic_value msv ctx in + (ctx, Some (mk_typed_lvalue_from_var var mp (Some consumed))) | AEndedIgnoredMutBorrow _ -> (* This happens with nested borrows: we need to dive in *) raise Unimplemented @@ -897,10 +903,15 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) : (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows) child_projs); (ctx, None) - | AEndedProjBorrows mv -> + | AEndedProjBorrows { original; given_back = mv } -> + (* We use the original symbolic value to help propagate the naming constraints *) + let original = + InterpreterUtils.mk_typed_value_from_symbolic_value original + in + let original = typed_value_to_rvalue ctx original in (* Return the meta-value *) let ctx, var = fresh_var_for_symbolic_value mv ctx in - (ctx, Some (mk_typed_lvalue_from_var var mp)) + (ctx, Some (mk_typed_lvalue_from_var var mp (Some original))) | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> failwith "Unreachable" @@ -1039,7 +1050,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression) (fun (arg, mp) -> mk_value_expression arg mp) (List.combine args args_mplaces) in - let dest_v = mk_typed_lvalue_from_var dest dest_mplace in + let dest_v = mk_typed_lvalue_from_var dest dest_mplace None in let call = { func; type_params; args } in let call = Call call in let call_ty = if monadic then mk_result_ty dest_v.ty else dest_v.ty in @@ -1104,7 +1115,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression) List.fold_right (fun (var, value) (e : texpression) -> mk_let monadic - (mk_typed_lvalue_from_var var None) + (mk_typed_lvalue_from_var var None None) (mk_value_expression value None) e) variables_values next_e @@ -1276,7 +1287,7 @@ and translate_expansion (config : config) (p : S.mplace option) let next_e = translate_expression config e ctx in let monadic = false in mk_let monadic - (mk_typed_lvalue_from_var var None) + (mk_typed_lvalue_from_var var None None) (mk_value_expression scrutinee scrutinee_mplace) next_e | SeAdt _ -> @@ -1300,7 +1311,7 @@ and translate_expansion (config : config) (p : S.mplace option) (* This is an enumeration: introduce an [ExpandEnum] let-binding *) let variant_id = Option.get variant_id in let lvars = - List.map (fun v -> mk_typed_lvalue_from_var v None) vars + List.map (fun v -> mk_typed_lvalue_from_var v None None) vars in let lv = mk_adt_lvalue scrutinee.ty variant_id lvars in let monadic = false in @@ -1329,13 +1340,13 @@ and translate_expansion (config : config) (p : S.mplace option) (fun (fid, var) e -> let field_proj = gen_field_proj fid var in mk_let monadic - (mk_typed_lvalue_from_var var None) + (mk_typed_lvalue_from_var var None None) (mk_value_expression field_proj None) e) id_var_pairs branch | T.Tuple -> let vars = - List.map (fun x -> mk_typed_lvalue_from_var x None) vars + List.map (fun x -> mk_typed_lvalue_from_var x None None) vars in let monadic = false in mk_let monadic @@ -1351,7 +1362,7 @@ and translate_expansion (config : config) (p : S.mplace option) * identity when extracted (`box a == a`) *) let monadic = false in mk_let monadic - (mk_typed_lvalue_from_var var None) + (mk_typed_lvalue_from_var var None None) (mk_value_expression scrutinee scrutinee_mplace) branch | T.Assumed T.Vec -> @@ -1372,7 +1383,7 @@ and translate_expansion (config : config) (p : S.mplace option) let variant_id = Option.get variant_id in let ctx, vars = fresh_vars_for_symbolic_values svl ctx in let vars = - List.map (fun x -> mk_typed_lvalue_from_var x None) vars + List.map (fun x -> mk_typed_lvalue_from_var x None None) vars in let pat_ty = scrutinee.ty in let pat = mk_adt_lvalue pat_ty variant_id vars in @@ -1481,7 +1492,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx) in let inputs = List.append ctx.forward_inputs backward_inputs in let inputs_lvs = - List.map (fun v -> mk_typed_lvalue_from_var v None) inputs + List.map (fun v -> mk_typed_lvalue_from_var v None None) inputs in (* Sanity check *) assert ( diff --git a/src/Values.ml b/src/Values.ml index f2807cfa..d415df52 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -329,10 +329,13 @@ type aproj = Note that we keep the original symbolic value as a meta-value. *) - | AEndedProjBorrows of msymbolic_value + | AEndedProjBorrows of { + original : msymbolic_value; + given_back : msymbolic_value; + } (** The only purpose of [AEndedProjBorrows] is to store, for synthesis - purposes, the symbolic value which was generated and given back upon - ending the borrow. + purposes, the symbolic value which was originally in the borrow projection, + and the symbolic value which was generated and given back upon ending the borrow. *) | AIgnoredProjBorrows [@@deriving @@ -675,9 +678,10 @@ and aborrow_content = abstraction so that we can properly call the backward functions when generating the pure translation. *) - | AEndedMutBorrow of msymbolic_value * typed_avalue + | AEndedMutBorrow of mvalue * msymbolic_value * typed_avalue (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value - that we gave back as a meta-value, to help with the synthesis. + that we gave back as a meta-value, to help with the synthesis, together + with the initial consumed value (also as a meta-value). We also remember the child [avalue] because this structural information is useful for the synthesis (but not for the symbolic execution): in practice the child value should only contain ended borrows, ignored -- cgit v1.2.3