From 029a12e25e1ee883ac98472f2e032b466d765307 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 21 Apr 2022 12:28:44 +0200 Subject: Improve the generation of names for given back values --- src/InterpreterBorrows.ml | 4 +- src/InterpreterBorrowsCore.ml | 10 +-- src/InterpreterExpressions.ml | 2 +- src/InterpreterPaths.ml | 7 +- src/InterpreterStatements.ml | 13 +-- src/InterpreterUtils.ml | 10 +++ src/Invariants.ml | 4 +- src/Print.ml | 2 +- src/PrintPure.ml | 26 ++++-- src/Pure.ml | 9 +- src/PureMicroPasses.ml | 189 ++++++++++++++++++++++++++++++++++-------- src/SymbolicAst.ml | 4 +- src/SymbolicToPure.ml | 16 ++-- src/SynthesizeSymbolic.ml | 6 +- src/Values.ml | 6 +- 15 files changed, 236 insertions(+), 72 deletions(-) diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index 89dfb274..1905cf79 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -92,7 +92,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option) method! visit_Borrow outer bc = match bc with - | SharedBorrow (_, l') | InactivatedMutBorrow l' -> + | SharedBorrow (_, l') | InactivatedMutBorrow (_, l') -> (* Check if this is the borrow we are looking for *) if l = l' then ( (* Check if there are outer borrows or if we are inside an abstraction *) @@ -730,7 +730,7 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content) assert (Option.is_some (lookup_loan_opt sanity_ek l ctx)); (* Update the context *) give_back_value config l tv ctx - | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow l') -> + | Concrete (V.SharedBorrow (_, l') | V.InactivatedMutBorrow (_, l')) -> (* Sanity check *) assert (l' = l); (* Check that the borrow is somewhere - purely a sanity check *) diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 30314307..d1c60941 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -197,9 +197,9 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id) | V.SharedBorrow (mv, bid) -> (* Nothing specific to do *) super#visit_SharedBorrow env mv bid - | V.InactivatedMutBorrow bid -> + | V.InactivatedMutBorrow (mv, bid) -> (* Nothing specific to do *) - super#visit_InactivatedMutBorrow env bid + super#visit_InactivatedMutBorrow env mv bid | V.MutBorrow (bid, mv) -> (* Control the dive *) if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv @@ -410,7 +410,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) | V.SharedBorrow (_, bid) -> (* Check the borrow id *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () - | V.InactivatedMutBorrow bid -> + | V.InactivatedMutBorrow (_, bid) -> (* Check the borrow id *) if bid = l then raise (FoundGBorrowContent (Concrete bc)) else () @@ -494,10 +494,10 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id) | V.SharedBorrow (mv, bid) -> (* Check the id *) if bid = l then update () else super#visit_SharedBorrow env mv bid - | V.InactivatedMutBorrow bid -> + | V.InactivatedMutBorrow (mv, bid) -> (* Check the id *) if bid = l then update () - else super#visit_InactivatedMutBorrow env bid + else super#visit_InactivatedMutBorrow env mv bid method! visit_loan_content env lc = match lc with diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index bd89649b..c967688f 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -558,7 +558,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) in let bc = if bkind = E.Shared then V.SharedBorrow (shared_mvalue, bid) - else V.InactivatedMutBorrow bid + else V.InactivatedMutBorrow (shared_mvalue, bid) in let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in (* Continue *) diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 826e8563..1fd504d2 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -214,7 +214,8 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx) (* Return - note that we don't need to update the borrow itself *) Ok (ctx, { res with updated = v })) else Error (FailBorrow bc) - | V.InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid) + | V.InactivatedMutBorrow (_, bid) -> + Error (FailInactivatedMutBorrow bid) | V.MutBorrow (bid, bv) -> if access.enter_mut_borrows then match access_projection access ctx update p' bv with @@ -565,7 +566,7 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) match bc with | V.SharedBorrow _ | V.MutBorrow (_, _) -> (* Nothing special to do *) super#visit_borrow_content env bc - | V.InactivatedMutBorrow bid -> + | V.InactivatedMutBorrow (_, bid) -> (* We need to activate inactivated borrows *) let cc = activate_inactivated_mut_borrow config bid in raise (UpdateCtx cc) @@ -654,7 +655,7 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool) | LoanContent (V.MutLoan bid) | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow (_, bid)) -> end_outer_borrow config bid - | BorrowContent (V.InactivatedMutBorrow bid) -> + | BorrowContent (V.InactivatedMutBorrow (_, bid)) -> (* First activate the borrow *) activate_inactivated_mut_borrow config bid in diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 5a700f1a..c3331de5 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -808,12 +808,15 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = * inactivated borrow, we later can't translate it to pure values...) *) match rvalue with | E.Use _ - | E.Ref (_, (E.Shared | E.Mut)) + | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut)) | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _ | E.Aggregate _ -> - S.synthesize_assignment (S.mk_mplace p ctx) rv expr - | E.Ref (_, E.TwoPhaseMut) -> - (* Two-phase borrow: don't synthesize meta-information *) - expr) + let rp = rvalue_get_place rvalue in + let rp = + match rp with + | Some rp -> Some (S.mk_mplace rp ctx) + | None -> None + in + S.synthesize_assignment (S.mk_mplace p ctx) rv rp expr) in (* Compose and apply *) diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 27d65a62..7a2e22f7 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -249,3 +249,13 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx) obj#visit_typed_value () v; false with Found -> true + +(** Return the place used in an rvalue, if that makes sense. + This is used to compute meta-data, to find pretty names. + *) +let rvalue_get_place (rv : E.rvalue) : E.place option = + match rv with + | Use (Copy p | Move p) -> Some p + | Use (Constant _) -> None + | Ref (p, _) -> Some p + | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> None diff --git a/src/Invariants.ml b/src/Invariants.ml index f12911d4..81e35de3 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -244,7 +244,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = match bc with | V.SharedBorrow (_, bid) -> register_borrow Shared bid | V.MutBorrow (bid, _) -> register_borrow Mut bid - | V.InactivatedMutBorrow bid -> register_borrow Inactivated bid + | V.InactivatedMutBorrow (_, bid) -> register_borrow Inactivated bid in (* Continue exploring *) super#visit_borrow_content env bc @@ -461,7 +461,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> ( match (bc, rkind) with | V.SharedBorrow (_, bid), T.Shared - | V.InactivatedMutBorrow bid, T.Mut -> ( + | V.InactivatedMutBorrow (_, bid), T.Mut -> ( (* Lookup the borrowed value to check it has the proper type *) let _, glc = lookup_loan ek_all bid ctx in match glc with diff --git a/src/Print.ml b/src/Print.ml index 5ccba517..98876acb 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -309,7 +309,7 @@ module Values = struct "&mut@" ^ V.BorrowId.to_string bid ^ " (" ^ typed_value_to_string fmt tv ^ ")" - | InactivatedMutBorrow bid -> + | InactivatedMutBorrow (_, bid) -> "⌊inactivated_mut@" ^ V.BorrowId.to_string bid ^ "⌋" and loan_content_to_string (fmt : value_formatter) (lc : V.loan_content) : diff --git a/src/PrintPure.ml b/src/PrintPure.ml index e962c27c..1c3d396d 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -225,7 +225,8 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string) "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name)) let mplace_to_string (fmt : ast_formatter) (p : mplace) : string = - let name = match p.name with None -> "_" | Some name -> name in + let name = match p.name with None -> "" | Some name -> name in + let name = name ^ "^" ^ V.VarId.to_string p.var_id in projection_to_string fmt name p.projection let place_to_string (fmt : ast_formatter) (p : place) : string = @@ -408,17 +409,28 @@ let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string = let meta_to_string (fmt : ast_formatter) (meta : meta) : string = let meta = match meta with - | Assignment (p, rv) -> - "@assign(" ^ mplace_to_string fmt p ^ " := " + | Assignment (lp, rv, rp) -> + let rp = + match rp with + | None -> "" + | Some rp -> " [@src=" ^ mplace_to_string fmt rp ^ "]" + in + "@assign(" ^ mplace_to_string fmt lp ^ " := " ^ typed_rvalue_to_string fmt rv - ^ ")" + ^ rp ^ ")" in "@meta[" ^ meta ^ "]" let rec expression_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) (e : expression) : string = match e with - | Value (v, _) -> "(" ^ typed_rvalue_to_string fmt v ^ ")" + | Value (v, mp) -> + let mp = + match mp with + | None -> "" + | Some mp -> " [@mplace=" ^ mplace_to_string fmt mp ^ "]" + in + "(" ^ typed_rvalue_to_string fmt v ^ mp ^ ")" | Call call -> call_to_string fmt indent indent_incr call | Let (monadic, lv, re, e) -> let_to_string fmt indent indent_incr monadic lv re e @@ -469,8 +481,8 @@ and switch_to_string (fmt : ast_formatter) (indent : string) | If (e_true, e_false) -> let e_true = texpression_to_string fmt indent1 indent_incr e_true in let e_false = texpression_to_string fmt indent1 indent_incr e_false in - "if " ^ scrut ^ "\n" ^ indent ^ "then\n" ^ indent ^ e_true ^ "\n" ^ indent - ^ "else\n" ^ indent ^ e_false + "if " ^ scrut ^ "\n" ^ indent ^ "then\n" ^ indent1 ^ e_true ^ "\n" + ^ indent ^ "else\n" ^ indent1 ^ e_false | Match branches -> let branch_to_string (b : match_branch) : string = let pat = typed_lvalue_to_string fmt b.pat in diff --git a/src/Pure.ml b/src/Pure.ml index f0e43115..02b821ef 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -165,7 +165,11 @@ type projection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id } type projection = projection_elem list [@@deriving show] -type mplace = { name : string option; projection : projection } +type mplace = { + var_id : V.VarId.id; + name : string option; + projection : projection; +} [@@deriving show] (** "Meta" place. @@ -476,7 +480,8 @@ type fun_id = [@@deriving show, ord] (** Meta-information stored in the AST *) -type meta = Assignment of mplace * typed_rvalue [@@deriving show] +type meta = Assignment of mplace * typed_rvalue * mplace option +[@@deriving show] (** Ancestor for [iter_expression] visitor *) class ['self] iter_expression_base = diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index ceaaa129..a963e628 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -3,6 +3,7 @@ open Pure open PureUtils open TranslateCore +module V = Values (** The local logger *) let log = L.pure_micro_passes_log @@ -109,7 +110,10 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator = let id = obj#visit_expression () body.body.e () in VarId.generator_from_incr_id id -type pn_ctx = string VarId.Map.t +type pn_ctx = { + pure_vars : string VarId.Map.t; + llbc_vars : string V.VarId.Map.t; +} (** "pretty-name context": see [compute_pretty_names] *) (** This function computes pretty names for the variables in the pure AST. It @@ -229,50 +233,101 @@ let compute_pretty_names (def : fun_decl) : fun_decl = * also. *) let merge_ctxs (ctx0 : pn_ctx) (ctx1 : pn_ctx) : pn_ctx = - VarId.Map.fold (fun id name ctx -> VarId.Map.add id name ctx) ctx0 ctx1 + let pure_vars = + VarId.Map.fold + (fun id name ctx -> VarId.Map.add id name ctx) + ctx0.pure_vars ctx1.pure_vars + in + let llbc_vars = + V.VarId.Map.fold + (fun id name ctx -> V.VarId.Map.add id name ctx) + ctx0.llbc_vars ctx1.llbc_vars + in + { pure_vars; llbc_vars } + in + let empty_ctx = + { pure_vars = VarId.Map.empty; llbc_vars = V.VarId.Map.empty } in let merge_ctxs_ls (ctxs : pn_ctx list) : pn_ctx = - List.fold_left (fun ctx0 ctx1 -> merge_ctxs ctx0 ctx1) VarId.Map.empty ctxs + List.fold_left (fun ctx0 ctx1 -> merge_ctxs ctx0 ctx1) empty_ctx ctxs in let add_var (ctx : pn_ctx) (v : var) : pn_ctx = - assert (not (VarId.Map.mem v.id ctx)); + assert (not (VarId.Map.mem v.id ctx.pure_vars)); match v.basename with | None -> ctx - | Some name -> VarId.Map.add v.id name ctx + | Some name -> + let pure_vars = VarId.Map.add v.id name ctx.pure_vars in + { ctx with pure_vars } in - let update_var (ctx : pn_ctx) (v : var) : var = + let update_var (ctx : pn_ctx) (v : var) (mp : mplace option) : var = match v.basename with | Some _ -> v | None -> ( - match VarId.Map.find_opt v.id ctx with - | None -> v - | Some basename -> { v with basename = Some basename }) + match VarId.Map.find_opt v.id ctx.pure_vars with + | Some basename -> { v with basename = Some basename } + | None -> + if Option.is_some mp then + match + V.VarId.Map.find_opt (Option.get mp).var_id ctx.llbc_vars + with + | None -> v + | Some basename -> { v with basename = Some basename } + else v) in let update_typed_lvalue ctx (lv : typed_lvalue) : typed_lvalue = let obj = object inherit [_] map_typed_lvalue - method! visit_var _ v = update_var ctx v + method! visit_Var _ v mp = Var (update_var ctx v mp, mp) end in obj#visit_typed_lvalue () lv in + let register_mplace (mp : mplace) (ctx : pn_ctx) : pn_ctx = + match (V.VarId.Map.find_opt mp.var_id ctx.llbc_vars, mp.name) with + | None, Some name -> + let llbc_vars = V.VarId.Map.add mp.var_id name ctx.llbc_vars in + { ctx with llbc_vars } + | _ -> ctx + in + + let add_pure_var_constraint (var_id : VarId.id) (name : string) (ctx : pn_ctx) + : pn_ctx = + let pure_vars = + if VarId.Map.mem var_id ctx.pure_vars then ctx.pure_vars + else VarId.Map.add var_id name ctx.pure_vars + in + { ctx with pure_vars } + in + let add_llbc_var_constraint (var_id : V.VarId.id) (name : string) + (ctx : pn_ctx) : pn_ctx = + let llbc_vars = + if V.VarId.Map.mem var_id ctx.llbc_vars then ctx.llbc_vars + else V.VarId.Map.add var_id name ctx.llbc_vars + in + { ctx with llbc_vars } + in let add_constraint (mp : mplace) (var_id : VarId.id) (ctx : pn_ctx) : pn_ctx = + (* Register the place *) + let ctx = register_mplace mp ctx in (* Update the variable name *) match (mp.name, mp.projection) with | Some name, [] -> (* Check if the variable already has a name - if not: insert the new name *) - if VarId.Map.mem var_id ctx then ctx else VarId.Map.add var_id name ctx + let ctx = add_pure_var_constraint var_id name ctx in + let ctx = add_llbc_var_constraint mp.var_id name ctx in + ctx | _ -> ctx in let add_right_constraint (mp : mplace) (rv : typed_rvalue) (ctx : pn_ctx) : pn_ctx = - match rv.value with - | RvPlace { var = var_id; projection = [] } -> add_constraint mp var_id ctx - | _ -> ctx + (* Register the place *) + let ctx = register_mplace mp ctx in + (* Add the constraint *) + match rv.value with RvPlace p -> add_constraint mp p.var ctx | _ -> ctx in let add_opt_right_constraint (mp : mplace option) (rv : typed_rvalue) (ctx : pn_ctx) : pn_ctx = @@ -283,7 +338,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = object (self) inherit [_] reduce_typed_lvalue - method zero _ = VarId.Map.empty + method zero _ = empty_ctx method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ()) @@ -302,22 +357,69 @@ let compute_pretty_names (def : fun_decl) : fun_decl = * assignments *) let add_left_right_constraint (lv : typed_lvalue) (re : texpression) (ctx : pn_ctx) : pn_ctx = - (* We propagate constraints across variable reassignments: `^0 = x` *) - match (lv.value, re.e) with - | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))), - Value (_, Some ({ name = Some _; projection = [] } as rmp)) ) -> - (* Use the meta-information on the right *) - add_constraint rmp lvar.id ctx - | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))), - Value ({ value = RvPlace { var = rvar_id; projection = [] }; ty = _ }, _) - ) -> ( - (* Use the variable name *) - match - (VarId.Map.find_opt lvar.id ctx, VarId.Map.find_opt rvar_id ctx) - with - | None, Some name -> VarId.Map.add lvar.id name ctx - | _ -> ctx) - | _ -> (* Nothing to propagate *) ctx + (* We propagate constraints across variable reassignments: `^0 = x`, + * if the destination doesn't have naming information *) + match lv.value with + | LvVar (Var (({ id = _; basename = None; ty = _ } as lvar), lmp)) -> ( + if + (* Check that there is not already a name for teh variable *) + VarId.Map.mem lvar.id ctx.pure_vars + then ctx + else + (* We ignore the left meta-place information: it should have been taken + * care of by [add_left_constraint]. We try to use the right meta-place + * information *) + let add (name : string) (ctx : pn_ctx) : pn_ctx = + (* Add the constraint for the pure variable *) + let ctx = add_pure_var_constraint lvar.id name ctx in + (* Add the constraint for the LLBC variable *) + match lmp with + | None -> ctx + | Some lmp -> add_llbc_var_constraint lmp.var_id name ctx + in + match re.e with + | Value (rv, rmp) -> + (* We try to use the right-place information *) + let ctx = + match rmp with + | Some { var_id; name; projection = [] } -> ( + if Option.is_some name then add (Option.get name) ctx + else + match V.VarId.Map.find_opt var_id ctx.llbc_vars with + | None -> ctx + | Some name -> add name ctx) + | _ -> ctx + in + (* We try to use the rvalue information *) + let ctx = + match rv with + | { value = RvPlace { var = rvar_id; projection = [] }; ty = _ } + -> ( + match VarId.Map.find_opt rvar_id ctx.pure_vars with + | None -> ctx + | Some name -> add name ctx) + | _ -> ctx + in + ctx + | _ -> ctx) + | _ -> ctx + (* match (lv.value, re.e) with + (* Case 1: *) + | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))), + Value (_, Some ({ name = Some _; projection = [] } as rmp)) ) -> + (* Use the meta-information on the right *) + add_constraint rmp lvar.id ctx + (* Case 2: *) + | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))), + Value ({ value = RvPlace { var = rvar_id; projection = [] }; ty = _ }, _) + ) -> ( + (* Use the variable name *) + match + (VarId.Map.find_opt lvar.id ctx, VarId.Map.find_opt rvar_id ctx) + with + | None, Some name -> VarId.Map.add lvar.id name ctx + | _ -> ctx) + | _ -> (* Nothing to propagate *) ctx *) in (* *) @@ -350,7 +452,10 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (* *) and update_let (monadic : bool) (lv : typed_lvalue) (re : texpression) (e : texpression) (ctx : pn_ctx) : pn_ctx * expression = + (* We first add the left-constraint *) let ctx = add_left_constraint lv ctx in + (* Then we try to propagate the right-constraints to the left, in case + * the left constraints didn't give naming information *) let ctx = add_left_right_constraint lv re ctx in let ctx, re = update_texpression re ctx in let ctx, e = update_texpression e ctx in @@ -387,8 +492,21 @@ let compute_pretty_names (def : fun_decl) : fun_decl = and update_meta (meta : meta) (e : texpression) (ctx : pn_ctx) : pn_ctx * expression = match meta with - | Assignment (mp, rvalue) -> + | Assignment (mp, rvalue, rmp) -> let ctx = add_right_constraint mp rvalue ctx in + let ctx = + match (mp.projection, rmp) with + | [], Some { var_id; name; projection = [] } -> ( + let name = + match name with + | Some name -> Some name + | None -> V.VarId.Map.find_opt var_id ctx.llbc_vars + in + match name with + | None -> ctx + | Some name -> add_llbc_var_constraint mp.var_id name ctx) + | _ -> ctx + in let ctx, e = update_texpression e ctx in (ctx, e.e) in @@ -405,7 +523,12 @@ let compute_pretty_names (def : fun_decl) : fun_decl = | Some name -> Some (v.id, name)) body.inputs in - let ctx = VarId.Map.of_list input_names in + let ctx = + { + pure_vars = VarId.Map.of_list input_names; + llbc_vars = V.VarId.Map.empty; + } + in let _, body_exp = update_texpression body.body ctx in Some { body with body = body_exp } in diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml index 3df91d23..5fa7d754 100644 --- a/src/SymbolicAst.ml +++ b/src/SymbolicAst.ml @@ -49,8 +49,8 @@ type call = { *) type meta = - | Assignment of mplace * V.typed_value - (** We generated an assignment (destination, assigned value) *) + | Assignment of mplace * V.typed_value * mplace option + (** We generated an assignment (destination, assigned value, src) *) (** **Rk.:** here, [expression] is not at all equivalent to the expressions used in CFIM: they are a first step towards lambda-calculus expressions. diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 163ddde8..65bdcf9c 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -638,7 +638,11 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue (* The meta-value stored in the shared borrow was added especially * for this case (because we can't use the borrow id for lookups) *) (translate mv).value - | V.InactivatedMutBorrow _ -> failwith "Unreachable" + | V.InactivatedMutBorrow (mv, _) -> + (* Same as for shared borrows. However, note that we use inactivated borrows + * only in meta-data: a value actually used in the translation can't come + * from an unpromoted inactivated borrow *) + (translate mv).value | V.MutBorrow (_, v) -> (* Borrows are the identity in the extraction *) (translate v).value) @@ -784,9 +788,10 @@ let translate_mprojection (p : E.projection) : projection = (** Translate a "meta"-place *) let translate_mplace (p : S.mplace) : mplace = + let var_id = p.bv.index in let name = p.bv.name in let projection = translate_mprojection p.projection in - { name; projection } + { var_id; name; projection } let translate_opt_mplace (p : S.mplace option) : mplace option = match p with None -> None | Some p -> Some (translate_mplace p) @@ -1434,10 +1439,11 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression) let next_e = translate_expression config e ctx in let meta = match meta with - | S.Assignment (p, rv) -> - let p = translate_mplace p in + | S.Assignment (lp, rv, rp) -> + let lp = translate_mplace lp in let rv = typed_value_to_rvalue ctx rv in - Assignment (p, rv) + let rp = translate_opt_mplace rp in + Assignment (lp, rv, rp) in let e = Meta (meta, next_e) in let ty = next_e.ty in diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml index 785f034b..95da38e6 100644 --- a/src/SynthesizeSymbolic.ml +++ b/src/SynthesizeSymbolic.ml @@ -145,8 +145,8 @@ let synthesize_end_abstraction (abs : V.abs) (expr : expression option) : | None -> None | Some expr -> Some (EndAbstraction (abs, expr)) -let synthesize_assignment (place : mplace) (rvalue : V.typed_value) - (expr : expression option) : expression option = +let synthesize_assignment (lplace : mplace) (rvalue : V.typed_value) + (rplace : mplace option) (expr : expression option) : expression option = match expr with | None -> None - | Some expr -> Some (Meta (Assignment (place, rvalue), expr)) + | Some expr -> Some (Meta (Assignment (lplace, rvalue, rplace), expr)) diff --git a/src/Values.ml b/src/Values.ml index 3314defb..3f1fc0bd 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -144,7 +144,7 @@ and borrow_content = *) | MutBorrow of (BorrowId.id[@opaque]) * typed_value (** A mutably borrowed value. *) - | InactivatedMutBorrow of (BorrowId.id[@opaque]) + | InactivatedMutBorrow of mvalue * (BorrowId.id[@opaque]) (** An inactivated mut borrow. This is used to model [two-phase borrows](https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html). @@ -169,6 +169,10 @@ and borrow_content = l = Vec::len(move v2); Vec::push(move v1, move l); // In practice, v1 gets activated only here ``` + + The meta-value is used for the same purposes as with shared borrows, + at the exception that in case of inactivated borrows it is not + *necessary* for the synthesis: we keep it only as meta-information. *) and loan_content = -- cgit v1.2.3