summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/InterpreterBorrows.ml4
-rw-r--r--src/InterpreterBorrowsCore.ml10
-rw-r--r--src/InterpreterExpressions.ml2
-rw-r--r--src/InterpreterPaths.ml7
-rw-r--r--src/InterpreterStatements.ml13
-rw-r--r--src/InterpreterUtils.ml10
-rw-r--r--src/Invariants.ml4
-rw-r--r--src/Print.ml2
-rw-r--r--src/PrintPure.ml26
-rw-r--r--src/Pure.ml9
-rw-r--r--src/PureMicroPasses.ml189
-rw-r--r--src/SymbolicAst.ml4
-rw-r--r--src/SymbolicToPure.ml16
-rw-r--r--src/SynthesizeSymbolic.ml6
-rw-r--r--src/Values.ml6
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 20:03:12 +0000