diff options
| -rw-r--r-- | compiler/Interpreter.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 13 | ||||
| -rw-r--r-- | compiler/InterpreterBorrowsCore.ml | 37 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 3 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 18 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 37 | ||||
| -rw-r--r-- | compiler/InterpreterPaths.ml | 6 | ||||
| -rw-r--r-- | compiler/InterpreterProjectors.ml | 8 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 7 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 7 | ||||
| -rw-r--r-- | compiler/Print.ml | 5 | ||||
| -rw-r--r-- | compiler/SymbolicAst.ml | 28 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 75 | ||||
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 44 | ||||
| -rw-r--r-- | compiler/Values.ml | 33 |
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. |