summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/Interpreter.ml4
-rw-r--r--compiler/InterpreterBorrows.ml13
-rw-r--r--compiler/InterpreterBorrowsCore.ml37
-rw-r--r--compiler/InterpreterExpansion.ml3
-rw-r--r--compiler/InterpreterExpressions.ml18
-rw-r--r--compiler/InterpreterLoops.ml37
-rw-r--r--compiler/InterpreterPaths.ml6
-rw-r--r--compiler/InterpreterProjectors.ml8
-rw-r--r--compiler/InterpreterStatements.ml7
-rw-r--r--compiler/Invariants.ml7
-rw-r--r--compiler/Print.ml5
-rw-r--r--compiler/SymbolicAst.ml28
-rw-r--r--compiler/SymbolicToPure.ml75
-rw-r--r--compiler/SynthesizeSymbolic.ml44
-rw-r--r--compiler/Values.ml33
15 files changed, 163 insertions, 162 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index d1241b9d..d8a99d80 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -196,7 +196,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
cf target_abs_ids
in
(* Generate the Return node *)
- let cf_return : m_fun = fun _ -> Some (SA.Return None) in
+ let cf_return : m_fun = fun ctx -> Some (SA.Return (ctx, None)) in
(* Apply *)
cf_end_target_abs cf_return ctx
in
@@ -246,7 +246,7 @@ let evaluate_function_symbolic (synthesize : bool)
let cf_pop = pop_frame config in
(* Generate the Return node *)
let cf_return ret_value : m_fun =
- fun _ -> Some (SA.Return (Some ret_value))
+ fun ctx -> Some (SA.Return (ctx, Some ret_value))
in
(* Apply *)
cf_pop cf_return ctx
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index eb3b9898..64f379be 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -98,7 +98,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
method! visit_Borrow outer bc =
match bc with
- | SharedBorrow (_, l') | ReservedMutBorrow (_, l') ->
+ | SharedBorrow l' | ReservedMutBorrow 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 *)
@@ -739,7 +739,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.ReservedMutBorrow (_, l')) ->
+ | Concrete (V.SharedBorrow l' | V.ReservedMutBorrow l') ->
(* Sanity check *)
assert (l' = l);
(* Check that the borrow is somewhere - purely a sanity check *)
@@ -1126,8 +1126,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
(** We may need to end borrows in "regular" values, because of shared values *)
method! visit_borrow_content _ bc =
match bc with
- | V.SharedBorrow (_, _) | V.MutBorrow (_, _) ->
- raise (FoundBorrowContent bc)
+ | V.SharedBorrow _ | V.MutBorrow (_, _) -> raise (FoundBorrowContent bc)
| V.ReservedMutBorrow _ -> raise (Failure "Unreachable")
end
in
@@ -1217,7 +1216,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
^ borrow_content_to_string ctx bc));
let ctx =
match bc with
- | V.SharedBorrow (_, bid) -> (
+ | V.SharedBorrow bid -> (
(* Replace the shared borrow with bottom *)
let allow_inner_loans = false in
match
@@ -1252,7 +1251,7 @@ and end_abstraction_remove_from_context (_config : C.config)
(* Apply the continuation *)
let expr = cf ctx in
(* Synthesize the symbolic AST *)
- S.synthesize_end_abstraction abs expr
+ S.synthesize_end_abstraction ctx abs expr
(** End a proj_loan over a symbolic value by ending the proj_borrows which
intersect this proj_loans.
@@ -1824,7 +1823,7 @@ let convert_value_to_abstractions (abs_kind : V.abs_kind) (can_end : bool)
assert allow_borrows;
(* Convert the borrow content *)
match bc with
- | SharedBorrow (_, bid) ->
+ | SharedBorrow bid ->
let ref_ty = ety_no_regions_to_rty ref_ty in
let ty = T.Ref (T.Var r_id, ref_ty, kind) in
let value = V.ABorrow (V.ASharedBorrow bid) in
diff --git a/compiler/InterpreterBorrowsCore.ml b/compiler/InterpreterBorrowsCore.ml
index 2e4a8d3a..6eece4fe 100644
--- a/compiler/InterpreterBorrowsCore.ml
+++ b/compiler/InterpreterBorrowsCore.ml
@@ -201,12 +201,12 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
method! visit_borrow_content env bc =
match bc with
- | V.SharedBorrow (mv, bid) ->
+ | V.SharedBorrow bid ->
(* Nothing specific to do *)
- super#visit_SharedBorrow env mv bid
- | V.ReservedMutBorrow (mv, bid) ->
+ super#visit_SharedBorrow env bid
+ | V.ReservedMutBorrow bid ->
(* Nothing specific to do *)
- super#visit_ReservedMutBorrow env mv bid
+ super#visit_ReservedMutBorrow env bid
| V.MutBorrow (bid, mv) ->
(* Control the dive *)
if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
@@ -314,7 +314,7 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
method! visit_borrow_content env bc =
match bc with
- | V.SharedBorrow (_, _) | V.ReservedMutBorrow _ ->
+ | V.SharedBorrow _ | V.ReservedMutBorrow _ ->
(* Nothing specific to do *)
super#visit_borrow_content env bc
| V.MutBorrow (bid, mv) ->
@@ -416,10 +416,10 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id)
if bid = l then raise (FoundGBorrowContent (Concrete bc))
else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
else ()
- | V.SharedBorrow (_, bid) ->
+ | V.SharedBorrow bid ->
(* Check the borrow id *)
if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
- | V.ReservedMutBorrow (_, bid) ->
+ | V.ReservedMutBorrow bid ->
(* Check the borrow id *)
if bid = l then raise (FoundGBorrowContent (Concrete bc)) else ()
@@ -500,13 +500,12 @@ let update_borrow (ek : exploration_kind) (l : V.BorrowId.id)
if bid = l then update ()
else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
else V.MutBorrow (bid, mv)
- | V.SharedBorrow (mv, bid) ->
+ | V.SharedBorrow bid ->
(* Check the id *)
- if bid = l then update () else super#visit_SharedBorrow env mv bid
- | V.ReservedMutBorrow (mv, bid) ->
+ if bid = l then update () else super#visit_SharedBorrow env bid
+ | V.ReservedMutBorrow bid ->
(* Check the id *)
- if bid = l then update ()
- else super#visit_ReservedMutBorrow env mv bid
+ if bid = l then update () else super#visit_ReservedMutBorrow env bid
method! visit_loan_content env lc =
match lc with
@@ -1194,3 +1193,17 @@ let get_first_non_ignored_aloan_in_abstraction (abs : V.abs) :
| ValuesUtils.FoundSymbolicValue sv ->
(* There are loan projections over symbolic values *)
Some (SymbolicValue sv)
+
+let lookup_shared_value_opt (ctx : C.eval_ctx) (bid : V.BorrowId.id) :
+ V.typed_value option =
+ match lookup_loan_opt ek_all bid ctx with
+ | None -> None
+ | Some (_, lc) -> (
+ match lc with
+ | Concrete (SharedLoan (_, sv)) | Abstract (ASharedLoan (_, sv, _)) ->
+ Some sv
+ | _ -> None)
+
+let lookup_shared_value (ctx : C.eval_ctx) (bid : V.BorrowId.id) : V.typed_value
+ =
+ Option.get (lookup_shared_value_opt ctx bid)
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 8a563351..9a61d917 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -340,8 +340,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
method! visit_Symbolic env sv =
if same_symbolic_id sv original_sv then
let bid = fresh_borrow () in
- V.Borrow
- (V.SharedBorrow (mk_typed_value_from_symbolic_value shared_sv, bid))
+ V.Borrow (V.SharedBorrow bid)
else super#visit_Symbolic env sv
method! visit_Abs proj_regions abs =
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 5d1a3cfe..43580312 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -157,12 +157,12 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
| V.Borrow bc -> (
(* We can only copy shared borrows *)
match bc with
- | SharedBorrow (mv, bid) ->
+ | SharedBorrow bid ->
(* We need to create a new borrow id for the copied borrow, and
* update the context accordingly *)
let bid' = C.fresh_borrow_id () in
let ctx = InterpreterBorrows.reborrow_shared bid bid' ctx in
- (ctx, { v with V.value = V.Borrow (SharedBorrow (mv, bid')) })
+ (ctx, { v with V.value = V.Borrow (SharedBorrow bid') })
| MutBorrow (_, _) -> raise (Failure "Can't copy a mutable borrow")
| V.ReservedMutBorrow _ ->
raise (Failure "Can't copy a reserved mut borrow"))
@@ -391,7 +391,7 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
(* Call the continuation *)
let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
(* Synthesize the symbolic AST *)
- S.synthesize_unary_op unop v
+ S.synthesize_unary_op ctx unop v
(S.mk_opt_place_from_op op ctx)
res_sv None expr
in
@@ -532,7 +532,7 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
(* Synthesize the symbolic AST *)
let p1 = S.mk_opt_place_from_op op1 ctx in
let p2 = S.mk_opt_place_from_op op2 ctx in
- S.synthesize_binary_op binop v1 p1 v2 p2 res_sv None expr
+ S.synthesize_binary_op ctx binop v1 p1 v2 p2 res_sv None expr
in
(* Compose and apply *)
comp eval_ops compute cf ctx
@@ -561,18 +561,18 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
(* Generate the fresh borrow id *)
let bid = C.fresh_borrow_id () in
(* Compute the loan value, with which to replace the value at place p *)
- let nv, shared_mvalue =
+ let nv =
match v.V.value with
| V.Loan (V.SharedLoan (bids, sv)) ->
(* Shared loan: insert the new borrow id *)
let bids1 = V.BorrowId.Set.add bid bids in
- ({ v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }, sv)
+ { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }
| _ ->
(* Not a shared loan: add a wrapper *)
let v' =
V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v))
in
- ({ v with V.value = v' }, v)
+ { v with V.value = v' }
in
(* Update the borrowed value in the context *)
let ctx = write_place access p nv ctx in
@@ -582,8 +582,8 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
in
let bc =
- if bkind = E.Shared then V.SharedBorrow (shared_mvalue, bid)
- else V.ReservedMutBorrow (shared_mvalue, bid)
+ if bkind = E.Shared then V.SharedBorrow bid
+ else V.ReservedMutBorrow bid
in
let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
(* Continue *)
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 70a5f1bf..142bf4e7 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -403,8 +403,7 @@ module type Matcher = sig
val match_distinct_adts : T.ety -> V.adt_value -> V.adt_value -> V.typed_value
(** The meta-value is the result of a match *)
- val match_shared_borrows :
- T.ety -> V.mvalue -> V.borrow_id -> V.borrow_id -> V.mvalue * V.borrow_id
+ val match_shared_borrows : T.ety -> V.borrow_id -> V.borrow_id -> V.borrow_id
(** The input parameters are:
- [ty]
@@ -593,23 +592,9 @@ module Match (M : Matcher) = struct
| Borrow bc0, Borrow bc1 ->
let bc =
match (bc0, bc1) with
- | SharedBorrow (mv0, bid0), SharedBorrow (mv1, bid1) ->
- (* Not completely sure what to do with the meta-value, as we use
- it for the translation. TODO: remove meta-values from shared borrows?
-
- If a shared symbolic value gets expanded in a branch, it may be
- simplified (by being folded back to a symbolic value) upon
- doing the join, which as a result would lead to code where it
- is considered as mutable (which is sound). On the other hand,
- if we access a symbolic value in a loop, the translated loop
- should take it as input anyway, so maybe this actually leads to
- equivalent code.
- *)
- assert (not (value_has_borrows ctx mv0.V.value));
- assert (not (value_has_borrows ctx mv1.V.value));
- let mv = match_rec mv0 mv1 in
- let mv, bid = M.match_shared_borrows ty mv bid0 bid1 in
- V.SharedBorrow (mv, bid)
+ | SharedBorrow bid0, SharedBorrow bid1 ->
+ let bid = M.match_shared_borrows ty bid0 bid1 in
+ V.SharedBorrow bid
| MutBorrow (bid0, bv0), MutBorrow (bid1, bv1) ->
let bv = match_rec bv0 bv1 in
assert (not (value_has_borrows ctx bv.V.value));
@@ -830,9 +815,9 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
(* No borrows, no loans: we can introduce a symbolic value *)
mk_fresh_symbolic_typed_value_from_ety V.LoopJoin ty
- let match_shared_borrows (ty : T.ety) (mv : V.mvalue) (bid0 : V.borrow_id)
- (bid1 : V.borrow_id) : V.mvalue * V.borrow_id =
- if bid0 = bid1 then (mv, bid0)
+ let match_shared_borrows (ty : T.ety) (bid0 : V.borrow_id)
+ (bid1 : V.borrow_id) : V.borrow_id =
+ if bid0 = bid1 then bid0
else
(* We replace bid0 and bid1 with a fresh borrow id, and introduce
an abstraction which links all of them:
@@ -885,7 +870,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
push_abs abs;
(* Return the new borrow *)
- (sv, bid2)
+ bid2
let match_mut_borrows (ty : T.ety) (bid0 : V.borrow_id) (bv0 : V.typed_value)
(bid1 : V.borrow_id) (bv1 : V.typed_value) (bv : V.typed_value) :
@@ -1457,10 +1442,10 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
(_adt1 : V.adt_value) : V.typed_value =
raise Distinct
- let match_shared_borrows (_ty : T.ety) (mv : V.mvalue) (bid0 : V.borrow_id)
- (bid1 : V.borrow_id) : V.mvalue * V.borrow_id =
+ let match_shared_borrows (_ty : T.ety) (bid0 : V.borrow_id)
+ (bid1 : V.borrow_id) : V.borrow_id =
let bid = match_bid bid0 bid1 in
- (mv, bid)
+ bid
let match_mut_borrows (_ty : T.ety) (bid0 : V.borrow_id)
(_bv0 : V.typed_value) (bid1 : V.borrow_id) (_bv1 : V.typed_value)
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 1e1401df..619815b3 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -164,7 +164,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
(* Borrows *)
| Deref, V.Borrow bc, _ -> (
match bc with
- | V.SharedBorrow (_, bid) ->
+ | V.SharedBorrow bid ->
(* Lookup the loan content, and explore from there *)
if access.lookup_shared_borrows then
match lookup_loan ek bid ctx with
@@ -216,7 +216,7 @@ 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.ReservedMutBorrow (_, bid) -> Error (FailReservedMutBorrow bid)
+ | V.ReservedMutBorrow bid -> Error (FailReservedMutBorrow bid)
| V.MutBorrow (bid, bv) ->
if access.enter_mut_borrows then
match access_projection access ctx update p' bv with
@@ -546,7 +546,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.ReservedMutBorrow (_, bid) ->
+ | V.ReservedMutBorrow bid ->
(* We need to activate reserved borrows *)
let cc = promote_reserved_mut_borrow config bid in
raise (UpdateCtx cc)
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index 87522d73..335ebcf4 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -53,7 +53,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
bv ref_ty
in
(bid, asb)
- | V.SharedBorrow (_, bid), T.Shared ->
+ | V.SharedBorrow bid, T.Shared ->
(* Lookup the shared value *)
let ek = ek_all in
let sv = lookup_loan ek bid ctx in
@@ -139,7 +139,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
fresh_reborrow regions ancestors_regions bv ref_ty
in
V.AMutBorrow (mv, bid, bv)
- | V.SharedBorrow (_, bid), T.Shared ->
+ | V.SharedBorrow bid, T.Shared ->
(* Rem.: we don't need to also apply the projection on the
borrowed value, because for as long as the abstraction
lives then the shared borrow lives, which means that the
@@ -179,7 +179,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
in
(* Return *)
V.AIgnoredMutBorrow (opt_bid, bv)
- | V.SharedBorrow (_, bid), T.Shared ->
+ | V.SharedBorrow bid, T.Shared ->
(* Lookup the shared value *)
let ek = ek_all in
let sv = lookup_loan ek bid ctx in
@@ -352,7 +352,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
match v.V.value with
| V.Borrow lc -> (
match lc with
- | V.SharedBorrow (_, _) | V.ReservedMutBorrow _ -> None
+ | V.SharedBorrow _ | V.ReservedMutBorrow _ -> None
| V.MutBorrow (id, _) -> Some id)
| _ -> None
in
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 5f74d1a7..63d10894 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -196,7 +196,7 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
(* Continue *)
let expr = cf Unit ctx in
(* Add the synthesized assertion *)
- S.synthesize_assertion v expr
+ S.synthesize_assertion ctx v expr
| _ ->
raise
(Failure ("Expected a boolean, got: " ^ typed_value_to_string ctx v))
@@ -819,7 +819,8 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
| Some rp -> Some (S.mk_mplace rp ctx)
| None -> None
in
- S.synthesize_assignment (S.mk_mplace p ctx) rv rp expr)
+ S.synthesize_assignment ctx (S.mk_mplace p ctx) rv rp expr
+ )
in
(* Compose and apply *)
@@ -1194,7 +1195,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
let expr = cf ctx in
(* Synthesize the symbolic AST *)
- S.synthesize_regular_function_call fid call_id abs_ids type_args args
+ S.synthesize_regular_function_call fid call_id ctx abs_ids type_args args
args_places ret_spc dest_place expr
in
let cc = comp cc cf_call in
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 2904289f..370b0d01 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -243,9 +243,9 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit =
(* Register the loan *)
let _ =
match bc with
- | V.SharedBorrow (_, bid) -> register_borrow Shared bid
+ | V.SharedBorrow bid -> register_borrow Shared bid
| V.MutBorrow (bid, _) -> register_borrow Mut bid
- | V.ReservedMutBorrow (_, bid) -> register_borrow Reserved bid
+ | V.ReservedMutBorrow bid -> register_borrow Reserved bid
in
(* Continue exploring *)
super#visit_borrow_content env bc
@@ -459,8 +459,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
| V.Bottom, _ -> (* Nothing to check *) ()
| V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
match (bc, rkind) with
- | V.SharedBorrow (_, bid), T.Shared
- | V.ReservedMutBorrow (_, bid), T.Mut -> (
+ | V.SharedBorrow bid, T.Shared | V.ReservedMutBorrow 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/compiler/Print.ml b/compiler/Print.ml
index 9da3da9d..1de1bf9c 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -122,13 +122,12 @@ module Values = struct
and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) :
string =
match bc with
- | SharedBorrow (_, bid) -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
+ | SharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
| MutBorrow (bid, tv) ->
"&mut@" ^ V.BorrowId.to_string bid ^ " ("
^ typed_value_to_string fmt tv
^ ")"
- | ReservedMutBorrow (_, bid) ->
- "⌊reserved_mut@" ^ V.BorrowId.to_string bid ^ "⌋"
+ | ReservedMutBorrow bid -> "⌊reserved_mut@" ^ V.BorrowId.to_string bid ^ "⌋"
and loan_content_to_string (fmt : value_formatter) (lc : V.loan_content) :
string =
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index b0e4735a..08253e77 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -37,6 +37,11 @@ type call_id =
type call = {
call_id : call_id;
+ ctx : Contexts.eval_ctx;
+ (** The context upon calling the function (after the operands have been
+ evaluated). We need it to compute the translated values for shared
+ borrows (we need to perform lookups).
+ *)
abstractions : V.AbstractionId.id list;
type_params : T.ety list;
args : V.typed_value list;
@@ -51,7 +56,7 @@ type call = {
*)
type meta =
- | Assignment of mplace * V.typed_value * mplace option
+ | Assignment of Contexts.eval_ctx * mplace * V.typed_value * mplace option
(** We generated an assignment (destination, assigned value, src) *)
[@@deriving show]
@@ -59,18 +64,33 @@ type meta =
used in LLBC: they are a first step towards lambda-calculus expressions.
*)
type expression =
- | Return of V.typed_value option
+ | Return of Contexts.eval_ctx * V.typed_value option
(** There are two cases:
- the AST is for a forward function: the typed value should contain
the value which was in the return variable
- the AST is for a backward function: the typed value should be [None]
+
+ The context is the evaluation context upon reaching the return, We
+ need it to translate shared borrows to pure values (we need to be able
+ to look up the shared values in the context).
*)
| Panic
| FunCall of call * expression
- | EndAbstraction of V.abs * expression
+ | EndAbstraction of Contexts.eval_ctx * V.abs * expression
+ (** The context is the evaluation context upon ending the abstraction,
+ just after we removed the abstraction from the context.
+
+ The context is the evaluation context from after evaluating the asserted
+ value. It has the same purpose as for the {!Return} case.
+ *)
| EvalGlobal of A.GlobalDeclId.id * V.symbolic_value * expression
(** Evaluate a global to a fresh symbolic value *)
- | Assertion of V.typed_value * expression (** An assertion *)
+ | Assertion of Contexts.eval_ctx * V.typed_value * expression
+ (** An assertion.
+
+ The context is the evaluation context from after evaluating the asserted
+ value. It has the same purpose as for the {!Return} case.
+ *)
| Expansion of mplace option * V.symbolic_value * expansion
(** Expansion of a symbolic value.
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 45e35742..3f654a1d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3,6 +3,7 @@ open LlbcAstUtils
open Pure
open PureUtils
module Id = Identifiers
+module C = Contexts
module S = SymbolicAst
module TA = TypesAnalysis
module L = Logging
@@ -798,11 +799,11 @@ let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
- end abstraction
- return
*)
-let rec typed_value_to_texpression (ctx : bs_ctx) (v : V.typed_value) :
- texpression =
+let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
+ (v : V.typed_value) : texpression =
(* We need to ignore boxes *)
let v = unbox_typed_value v in
- let translate = typed_value_to_texpression ctx in
+ let translate = typed_value_to_texpression ctx ectx in
(* Translate the type *)
let ty = ctx_translate_fwd_ty ctx v.ty in
(* Translate the value *)
@@ -843,15 +844,16 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (v : V.typed_value) :
| MutLoan _ -> raise (Failure "Unreachable"))
| Borrow bc -> (
match bc with
- | V.SharedBorrow (mv, _) ->
- (* 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
- | V.ReservedMutBorrow (mv, _) ->
+ | V.SharedBorrow bid ->
+ (* Lookup the shared value in the context, and continue *)
+ let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
+ translate sv
+ | V.ReservedMutBorrow bid ->
(* Same as for shared borrows. However, note that we use reserved borrows
- * only in meta-data: a value actually *used in the translation* can't come
+ * only in *meta-data*: a value *actually used* in the translation can't come
* from an unpromoted reserved borrow *)
- translate mv
+ let sv = InterpreterBorrowsCore.lookup_shared_value ectx bid in
+ translate sv
| V.MutBorrow (_, v) ->
(* Borrows are the identity in the extraction *)
translate v)
@@ -885,9 +887,9 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (v : V.typed_value) :
^^
]}
*)
-let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
- texpression option =
- let translate = typed_avalue_to_consumed ctx in
+let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
+ (av : V.typed_avalue) : texpression option =
+ let translate = typed_avalue_to_consumed ctx ectx in
let value =
match av.value with
| APrimitive _ -> raise (Failure "Unreachable")
@@ -909,7 +911,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
let rv = mk_simpl_tuple_texpression field_values in
Some rv)
| ABottom -> raise (Failure "Unreachable")
- | ALoan lc -> aloan_content_to_consumed ctx lc
+ | ALoan lc -> aloan_content_to_consumed ctx ectx lc
| ABorrow bc -> aborrow_content_to_consumed ctx bc
| ASymbolic aproj -> aproj_to_consumed ctx aproj
| AIgnored -> None
@@ -922,13 +924,13 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
(* Return *)
value
-and aloan_content_to_consumed (ctx : bs_ctx) (lc : V.aloan_content) :
- texpression option =
+and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
+ (lc : V.aloan_content) : texpression option =
match lc with
| AMutLoan (_, _) | ASharedLoan (_, _, _) -> raise (Failure "Unreachable")
| AEndedMutLoan { child = _; given_back = _; given_back_meta } ->
(* Return the meta-value *)
- Some (typed_value_to_texpression ctx given_back_meta)
+ Some (typed_value_to_texpression ctx ectx given_back_meta)
| AEndedSharedLoan (_, _) ->
(* We don't dive into shared loans: there is nothing to give back
* inside (note that there could be a mutable borrow in the shared
@@ -983,9 +985,10 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : texpression option =
See [typed_avalue_to_consumed].
*)
-let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : texpression list =
+let abs_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) (abs : V.abs) :
+ texpression list =
log#ldebug (lazy ("abs_to_consumed:\n" ^ abs_to_string ctx abs));
- List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
+ List.filter_map (typed_avalue_to_consumed ctx ectx) abs.avalues
let translate_mprojection_elem (pe : E.projection_elem) :
mprojection_elem option =
@@ -1153,12 +1156,12 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) :
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
match e with
- | S.Return opt_v -> translate_return opt_v ctx
+ | S.Return (ectx, opt_v) -> translate_return ectx opt_v ctx
| Panic -> translate_panic ctx
| FunCall (call, e) -> translate_function_call call e ctx
- | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx
+ | EndAbstraction (ectx, abs, e) -> translate_end_abstraction ectx abs e ctx
| EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx
- | Assertion (v, e) -> translate_assertion v e ctx
+ | Assertion (ectx, v, e) -> translate_assertion ectx v e ctx
| Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
| Meta (meta, e) -> translate_meta meta e ctx
| ForwardEnd (e, back_e) ->
@@ -1193,8 +1196,8 @@ and translate_panic (ctx : bs_ctx) : texpression =
else mk_result_fail_texpression_with_error_id error_failure_id output_ty
(** [opt_v]: the value to return, in case we translate a forward function *)
-and translate_return (opt_v : V.typed_value option) (ctx : bs_ctx) : texpression
- =
+and translate_return (ectx : C.eval_ctx) (opt_v : V.typed_value option)
+ (ctx : bs_ctx) : texpression =
(* There are two cases:
- either we are translating a forward function, in which case the optional
value should be [Some] (it is the returned value)
@@ -1207,7 +1210,7 @@ and translate_return (opt_v : V.typed_value option) (ctx : bs_ctx) : texpression
| None ->
(* Forward function *)
let v = Option.get opt_v in
- typed_value_to_texpression ctx v
+ typed_value_to_texpression ctx ectx v
| Some bid ->
(* Backward function *)
(* Sanity check *)
@@ -1240,7 +1243,7 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
(* Translate the function call *)
let type_args = List.map (ctx_translate_fwd_ty ctx) call.type_params in
let args =
- let args = List.map (typed_value_to_texpression ctx) call.args in
+ let args = List.map (typed_value_to_texpression ctx call.ctx) call.args in
let args_mplaces = List.map translate_opt_mplace call.args_places in
List.map
(fun (arg, mp) -> mk_opt_mplace_texpression mp arg)
@@ -1353,8 +1356,8 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
(* Put together *)
mk_let effect_info.can_fail dest_v call next_e
-and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
- texpression =
+and translate_end_abstraction (ectx : C.eval_ctx) (abs : V.abs)
+ (e : S.expression) (ctx : bs_ctx) : texpression =
log#ldebug
(lazy
("translate_end_abstraction: abstraction kind: "
@@ -1392,7 +1395,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
T.RegionGroupId.Map.find bid ctx.backward_outputs
in
(* Get the list of values consumed by the abstraction upon ending *)
- let consumed_values = abs_to_consumed ctx abs in
+ let consumed_values = abs_to_consumed ctx ectx abs in
(* Group the two lists *)
let variables_values =
List.combine given_back_variables consumed_values
@@ -1437,7 +1440,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
in
(* Retrieve the values consumed upon ending the loans inside this
* abstraction: those give us the remaining input values *)
- let back_inputs = abs_to_consumed ctx abs in
+ let back_inputs = abs_to_consumed ctx ectx abs in
(* If the function is stateful:
* - add the state input argument
* - generate a fresh state variable for the returned state
@@ -1574,7 +1577,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
let inputs = T.RegionGroupId.Map.find rg_id ctx.backward_inputs in
(* Retrieve the values consumed upon ending the loans inside this
* abstraction: as there are no nested borrows, there should be none. *)
- let consumed = abs_to_consumed ctx abs in
+ let consumed = abs_to_consumed ctx ectx abs in
assert (consumed = []);
(* Retrieve the values given back upon ending this abstraction - note that
* we don't provide meta-place information, because those assignments will
@@ -1615,11 +1618,11 @@ and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
let e = translate_expression e ctx in
mk_let false (mk_typed_pattern_from_var var None) gval e
-and translate_assertion (v : V.typed_value) (e : S.expression) (ctx : bs_ctx) :
- texpression =
+and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
+ (e : S.expression) (ctx : bs_ctx) : texpression =
let next_e = translate_expression e ctx in
let monadic = true in
- let v = typed_value_to_texpression ctx v in
+ let v = typed_value_to_texpression ctx ectx v in
let args = [ v ] in
let func = { id = FunOrOp (Fun (Pure Assert)); type_args = [] } in
let func_ty = mk_arrow Bool mk_unit_ty in
@@ -1832,9 +1835,9 @@ and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
let next_e = translate_expression e ctx in
let meta =
match meta with
- | S.Assignment (lp, rv, rp) ->
+ | S.Assignment (ectx, lp, rv, rp) ->
let lp = translate_mplace lp in
- let rv = typed_value_to_texpression ctx rv in
+ let rv = typed_value_to_texpression ctx ectx rv in
let rp = translate_opt_mplace rp in
Assignment (lp, rv, rp)
in
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 02b6e47c..a24b5690 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -94,7 +94,7 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
let el = Option.map (fun e -> [ e ]) e in
synthesize_symbolic_expansion sv place [ Some see ] el
-let synthesize_function_call (call_id : call_id)
+let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
(abstractions : V.AbstractionId.id list) (type_params : T.ety list)
(args : V.typed_value list) (args_places : mplace option list)
(dest : V.symbolic_value) (dest_place : mplace option)
@@ -104,6 +104,7 @@ let synthesize_function_call (call_id : call_id)
let call =
{
call_id;
+ ctx;
abstractions;
type_params;
args;
@@ -120,37 +121,40 @@ let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value)
Option.map (fun e -> EvalGlobal (gid, dest, e)) e
let synthesize_regular_function_call (fun_id : A.fun_id)
- (call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list)
- (type_params : T.ety list) (args : V.typed_value list)
- (args_places : mplace option list) (dest : V.symbolic_value)
- (dest_place : mplace option) (e : expression option) : expression option =
+ (call_id : V.FunCallId.id) (ctx : Contexts.eval_ctx)
+ (abstractions : V.AbstractionId.id list) (type_params : T.ety list)
+ (args : V.typed_value list) (args_places : mplace option list)
+ (dest : V.symbolic_value) (dest_place : mplace option)
+ (e : expression option) : expression option =
synthesize_function_call
(Fun (fun_id, call_id))
- abstractions type_params args args_places dest dest_place e
+ ctx abstractions type_params args args_places dest dest_place e
-let synthesize_unary_op (unop : E.unop) (arg : V.typed_value)
- (arg_place : mplace option) (dest : V.symbolic_value)
+let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : E.unop)
+ (arg : V.typed_value) (arg_place : mplace option) (dest : V.symbolic_value)
(dest_place : mplace option) (e : expression option) : expression option =
- synthesize_function_call (Unop unop) [] [] [ arg ] [ arg_place ] dest
+ synthesize_function_call (Unop unop) ctx [] [] [ arg ] [ arg_place ] dest
dest_place e
-let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
- (arg0_place : mplace option) (arg1 : V.typed_value)
+let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : E.binop)
+ (arg0 : V.typed_value) (arg0_place : mplace option) (arg1 : V.typed_value)
(arg1_place : mplace option) (dest : V.symbolic_value)
(dest_place : mplace option) (e : expression option) : expression option =
- synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ]
+ synthesize_function_call (Binop binop) ctx [] [] [ arg0; arg1 ]
[ arg0_place; arg1_place ] dest dest_place e
-let synthesize_end_abstraction (abs : V.abs) (e : expression option) :
- expression option =
- Option.map (fun e -> EndAbstraction (abs, e)) e
+let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : V.abs)
+ (e : expression option) : expression option =
+ Option.map (fun e -> EndAbstraction (ctx, abs, e)) e
-let synthesize_assignment (lplace : mplace) (rvalue : V.typed_value)
- (rplace : mplace option) (e : expression option) : expression option =
- Option.map (fun e -> Meta (Assignment (lplace, rvalue, rplace), e)) e
+let synthesize_assignment (ctx : Contexts.eval_ctx) (lplace : mplace)
+ (rvalue : V.typed_value) (rplace : mplace option) (e : expression option) :
+ expression option =
+ Option.map (fun e -> Meta (Assignment (ctx, lplace, rvalue, rplace), e)) e
-let synthesize_assertion (v : V.typed_value) (e : expression option) =
- Option.map (fun e -> Assertion (v, e)) e
+let synthesize_assertion (ctx : Contexts.eval_ctx) (v : V.typed_value)
+ (e : expression option) =
+ Option.map (fun e -> Assertion (ctx, v, e)) e
let synthesize_forward_end (e : expression)
(el : expression T.RegionGroupId.Map.t) =
diff --git a/compiler/Values.ml b/compiler/Values.ml
index f6f4d1b6..30e4f05d 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -169,19 +169,9 @@ and adt_value = {
}
and borrow_content =
- | SharedBorrow of mvalue * borrow_id
- (** A shared borrow.
-
- We remember the shared value which was borrowed as a meta value.
- This is necessary for synthesis: upon translating to "pure" values,
- we can't perform any lookup because we don't have an environment
- anymore. Note that it is ok to keep the shared value and copy
- the shared value this way, because shared values are immutable
- for as long as they are shared (i.e., as long as we can use the
- shared borrow).
- *)
+ | SharedBorrow of borrow_id (** A shared borrow. *)
| MutBorrow of borrow_id * typed_value (** A mutably borrowed value. *)
- | ReservedMutBorrow of mvalue * borrow_id
+ | ReservedMutBorrow of borrow_id
(** A reserved mut borrow.
This is used to model {{: https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html} two-phase borrows}.
@@ -206,20 +196,6 @@ and borrow_content =
l = Vec::len(move v2); // We need v2 here, and v1 *below*
Vec::push(move v1, move l); // In practice, v1 gets promoted only here
]}
-
- The meta-value is used for the same purposes as with shared borrows,
- at the exception that in the case of reserved borrows it is not
- *necessary* for the synthesis: we keep it only as meta-information.
- To be more precise:
- - when generating the synthesized program, we may need to convert
- shared borrows to pure values
- - we never need to do so for reserved borrows: such borrows must
- be promoted at the moment we use them (meaning in the synthesis we
- convert a *mutable* borrow to a pure value). However, we save
- meta-data about the assignments, which is used to make the code
- cleaner: when generating this meta-data, we may need to convert
- reserved borrows to pure values, in which situation we convert
- the meta-value we stored in the reserved borrow.
*)
and loan_content =
@@ -699,7 +675,10 @@ and aborrow_content =
The meta-value stores the initial value on which the projector was
applied, which reduced to this mut borrow. This meta-information
is only used for the synthesis.
- TODO: do we really use it actually?
+ Rem.: we don't use the meta-value for now, but might need it when
+ using nested borrows: if we end an *internal* borrow, this meta
+ value is propagated to the corresponding loan (we need to know
+ what the loan consumed, for the synthesis).
*)
| ASharedBorrow of borrow_id
(** A shared borrow owned by an abstraction.