diff options
| -rw-r--r-- | src/Interpreter.ml | 79 |
1 files changed, 57 insertions, 22 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 9faf8506..9c806e8f 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1015,6 +1015,20 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value) in { V.value; V.ty } +(** Convert a symbolic expansion to a value. + + If the expansion is a reference expansion, it converts it to a borrow. + This function is meant to be used when reducing projectors over borrows, + during a symbolic expansion. + *) +let symbolic_expansion_to_value_with_borrows (sv : V.symbolic_value) + (see : symbolic_expansion) : V.typed_value = + match see with + | SeMutRef (_, _) -> raise Unimplemented + | SeSharedRef (_, _) -> + raise Unimplemented failwith "Unexpected symbolic borrow expansion" + | _ -> symbolic_expansion_non_borrow_to_value sv see + (** Apply (and reduce) a projector over loans to a value. TODO: detailed comments. See [apply_proj_borrows] @@ -2852,19 +2866,23 @@ let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t) type proj_kind = LoanProj | BorrowProj (** Auxiliary function. - Apply a symbolic expansion to avalues in a context. + Apply a symbolic expansion to avalues in a context, targetting a specific + kind of projectors. [proj_kind] controls whether we apply the expansion to projectors - on loans or projectors on borrows (when applying a symbolic expansion to - a borrow value, we need two different expansion values: one for the loans - and another for the borrows meaning we have to call this function twice - with different parameters for [expansion]). For instance, if we expand - a symbolic mutable ref to `s0`, we'll have to apply the loan projectors - on a loan `mut_loan l` and the borrow projectors to a borrow `mut_borrow l s1`. + on loans or projectors on borrows. + + When dealing with reference expansion, it is necessary to first apply the + expansion on loan projectors, then on borrow projectors. The reason is + that reducing the borrow projectors might require to perform some reborrows, + in which case we need to lookup the corresponding loans in the context. + + [allow_reborrows] controls whether we allow reborrows or not. It is useful + only if we target borrow projectors. *) -let apply_symbolic_expansion_to_avalues (config : C.config) +let apply_symbolic_expansion_to_target_avalues (config : C.config) (allow_reborrows : bool) (proj_kind : proj_kind) - (original_sv : V.symbolic_value) (expansion : V.typed_value) + (original_sv : V.symbolic_value) (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = (* Symbolic values contained in the expansion might contain already ended regions *) let check_symbolic_no_ended = false in @@ -2892,8 +2910,8 @@ let apply_symbolic_expansion_to_avalues (config : C.config) if sv = original_sv then (* Apply the projector *) let projected_value = - apply_proj_loans check_symbolic_no_ended ctx proj_regions - expansion + apply_proj_loans_on_symbolic_expansion ctx proj_regions + expansion sv.V.sv_ty in (* Replace *) projected_value.V.value @@ -2903,6 +2921,12 @@ let apply_symbolic_expansion_to_avalues (config : C.config) | V.AProjBorrows (sv, proj_ty), BorrowProj -> (* Check if this is the symbolic value we are looking for *) if sv = original_sv then + (* Convert the symbolic expansion to a value on which we can + * apply a projector (if the expansion is a reference expansion, + * convert it to a borrow) *) + let expansion = + symbolic_expansion_to_value_with_borrows original_sv expansion + in (* Apply the projector *) let projected_value = apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow @@ -2923,6 +2947,21 @@ let apply_symbolic_expansion_to_avalues (config : C.config) (* Apply the reborrows *) apply_registered_reborrows ctx +(** Auxiliary function. + Apply a symbolic expansion to avalues in a context. +*) +let apply_symbolic_expansion_to_avalues (config : C.config) + (allow_reborrows : bool) (original_sv : V.symbolic_value) + (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = + let apply_expansion proj_kind ctx = + apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind + original_sv expansion ctx + in + (* First target the loan projectors, then the borrow projectors *) + let ctx = apply_expansion LoanProj ctx in + let ctx = apply_expansion BorrowProj ctx in + ctx + (** Apply a symbolic expansion to a context, by replacing the original symbolic value with its expanded value. Is valid only if the expansion is not a borrow (i.e., an adt...). @@ -2930,13 +2969,15 @@ let apply_symbolic_expansion_to_avalues (config : C.config) let apply_symbolic_expansion_non_borrow (config : C.config) (original_sv : V.symbolic_value) (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = - (* Visitor to apply the expansion to non-abstraction values *) + (* Convert the expansion to a value *) + let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in + (* Visitor to apply the expansion to *non-abstraction* values *) let obj = object inherit [_] C.map_eval_ctx as super method! visit_Symbolic env spc = - if spc.V.svalue = original_sv then expansion.V.value + if spc.V.svalue = original_sv then nv.V.value else super#visit_Symbolic env spc (** Replace a symbolic value with its expansion. Note that there may be several references to the same symbolic value @@ -2949,16 +2990,10 @@ let apply_symbolic_expansion_non_borrow (config : C.config) in (* Apply the expansion to non-abstraction values *) let ctx = obj#visit_eval_ctx None ctx in - (* Apply the expansion to abstraction values, on loans then on borrows (the - * order is arbitrary: we just can't do both at once because of the way the - * function is written) *) + (* Apply the expansion to abstraction values *) let allow_reborrows = false in - let apply_to_avalues proj_kind ctx = - apply_symbolic_expansion_to_avalues config allow_reborrows proj_kind - original_sv expansion ctx - in - let ctx = apply_to_avalues LoanProj ctx in - apply_to_avalues BorrowProj ctx + apply_symbolic_expansion_to_avalues config allow_reborrows original_sv + expansion ctx (** Expand a symbolic value which is not an enumeration with several variants. |