summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/InterpreterBorrows.ml14
-rw-r--r--src/Print.ml2
-rw-r--r--src/PrintPure.ml50
-rw-r--r--src/Pure.ml179
-rw-r--r--src/PureMicroPasses.ml16
-rw-r--r--src/PureUtils.ml6
-rw-r--r--src/SymbolicToPure.ml45
-rw-r--r--src/Values.ml14
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 13:30:26 +0000