diff options
author | Son HO | 2023-12-07 15:02:44 +0100 |
---|---|---|
committer | GitHub | 2023-12-07 15:02:44 +0100 |
commit | d4ebd6c1f0ba150e5e52d812d361189c89e43695 (patch) | |
tree | 4b3fa3d48c86ba379c78d01fca88d2084c2678c2 /compiler/InterpreterBorrows.ml | |
parent | 9eb117dc9e94d1b04d24c87d278d014f456b2d89 (diff) | |
parent | 613496f6c76b3f8c7211ef5bc98e3cc170e45ed1 (diff) |
Merge pull request #49 from AeneasVerif/son_merge_back
Allow the extraction of structures as tuples
Diffstat (limited to 'compiler/InterpreterBorrows.ml')
-rw-r--r-- | compiler/InterpreterBorrows.ml | 79 |
1 files changed, 24 insertions, 55 deletions
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index 6a7ac095..e56919fa 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -444,13 +444,6 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t) (ctx : eval_ctx) : eval_ctx = (* Sanity checks *) assert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty); - (match nsv.sv_kind with - | SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack - -> - () - | FunCallRet | SynthInput | Global | KindConstGeneric | LoopOutput | LoopJoin - | Aggregate | ConstGeneric | TraitConst -> - raise (Failure "Unreachable")); (* Store the given-back value as a meta-value for synthesis purposes *) let mv = nsv in (* Substitution function, to replace the borrow projectors over symbolic values *) @@ -459,31 +452,20 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t) let _ = raise Utils.Unimplemented in (* Compute the projection over the given back value *) let child_proj = - match nsv.sv_kind with - | SynthRetGivenBack -> - (* The given back value comes from the return value of the function - we are currently synthesizing (as it is given back, it means - we ended one of the regions appearing in the signature: we are - currently synthesizing one of the backward functions). - - As we don't allow borrow overwrites on returned value, we can - (and MUST) forget the borrows *) - AIgnoredProjBorrows - | FunCallGivenBack -> - (* TODO: there is something wrong here. - Consider this: - {[ - abs0 {'a} { AProjLoans (s0 : &'a mut T) [] } - abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) } - ]} - - Upon ending abs1, we give back some fresh symbolic value [s1], - that we reinsert where the loan for [s0] is. However, the mutable - borrow in the type [&'a mut T] was ended: we give back a value of - type [T]! We thus *mustn't* introduce a projector here. - *) - AProjBorrows (nsv, sv.sv_ty) - | _ -> raise (Failure "Unreachable") + (* TODO: there is something wrong here. + Consider this: + {[ + abs0 {'a} { AProjLoans (s0 : &'a mut T) [] } + abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) } + ]} + + Upon ending abs1, we give back some fresh symbolic value [s1], + that we reinsert where the loan for [s0] is. However, the mutable + borrow in the type [&'a mut T] was ended: we give back a value of + type [T]! We thus *mustn't* introduce a projector here. + *) + (* AProjBorrows (nsv, sv.sv_ty) *) + raise (Failure "TODO") in AProjLoans (sv, (mv, child_proj) :: local_given_back) in @@ -724,7 +706,7 @@ let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id) (** Convert an {!type:avalue} to a {!type:value}. This function is used when ending abstractions: whenever we end a borrow - in an abstraction, we converted the borrowed {!avalue} to a fresh symbolic + in an abstraction, we convert the borrowed {!avalue} to a fresh symbolic {!type:value}, then give back this {!type:value} to the context. Note that some regions may have ended in the symbolic value we generate. @@ -737,19 +719,8 @@ let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id) be expanded (because expanding this symbolic value would require expanding a reference whose region has already ended). *) -let convert_avalue_to_given_back_value (abs_kind : abs_kind) (av : typed_avalue) - : symbolic_value = - let sv_kind = - match abs_kind with - | FunCall _ -> FunCallGivenBack - | SynthRet _ -> SynthRetGivenBack - | SynthInput _ -> SynthInputGivenBack - | Loop _ -> LoopGivenBack - | Identity -> - (* Identity abstractions give back nothing *) - raise (Failure "Unreachable") - in - mk_fresh_symbolic_value sv_kind av.ty +let convert_avalue_to_given_back_value (av : typed_avalue) : symbolic_value = + mk_fresh_symbolic_value av.ty (** Auxiliary function: see {!end_borrow_aux}. @@ -767,8 +738,8 @@ let convert_avalue_to_given_back_value (abs_kind : abs_kind) (av : typed_avalue) borrows. This kind of internal reshuffling. should be similar to ending abstractions (it is tantamount to ending *sub*-abstractions). *) -let give_back (config : config) (abs_id_opt : AbstractionId.id option) - (l : BorrowId.id) (bc : g_borrow_content) (ctx : eval_ctx) : eval_ctx = +let give_back (config : config) (l : BorrowId.id) (bc : g_borrow_content) + (ctx : eval_ctx) : eval_ctx = (* Debug *) log#ldebug (lazy @@ -809,9 +780,7 @@ let give_back (config : config) (abs_id_opt : AbstractionId.id option) Rem.: we shouldn't do this here. We should do this in a function which takes care of ending *sub*-abstractions. *) - let abs_id = Option.get abs_id_opt in - let abs = ctx_lookup_abs ctx abs_id in - let sv = convert_avalue_to_given_back_value abs.kind av in + let sv = convert_avalue_to_given_back_value av in (* Update the context *) give_back_avalue_to_same_abstraction config l av (mk_typed_value_from_symbolic_value sv) @@ -957,14 +926,14 @@ let rec end_borrow_aux (config : config) (chain : borrow_or_abs_ids) cf_check cf ctx (* We found a borrow and replaced it with [Bottom]: give it back (i.e., update the corresponding loan) *) - | Ok (ctx, Some (abs_id_opt, bc)) -> + | Ok (ctx, Some (_, bc)) -> (* Sanity check: the borrowed value shouldn't contain loans *) (match bc with | Concrete (VMutBorrow (_, bv)) -> assert (Option.is_none (get_first_loan_in_value bv)) | _ -> ()); (* Give back the value *) - let ctx = give_back config abs_id_opt l bc ctx in + let ctx = give_back config l bc ctx in (* Do a sanity check and continue *) cf_check cf ctx @@ -1189,7 +1158,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) match bc with | AMutBorrow (bid, av) -> (* First, convert the avalue to a (fresh symbolic) value *) - let sv = convert_avalue_to_given_back_value abs.kind av in + let sv = convert_avalue_to_given_back_value av in (* Replace the mut borrow to register the fact that we ended * it and store with it the freshly generated given back value *) let ended_borrow = ABorrow (AEndedMutBorrow (sv, av)) in @@ -1239,7 +1208,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids) ("end_abstraction_borrows: found aproj borrows: " ^ aproj_to_string ctx (AProjBorrows (sv, proj_ty)))); (* Generate a fresh symbolic value *) - let nsv = mk_fresh_symbolic_value FunCallGivenBack proj_ty in + let nsv = mk_fresh_symbolic_value proj_ty in (* Replace the proj_borrows - there should be exactly one *) let ended_borrow = AEndedProjBorrows nsv in let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in |