diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Cps.ml | 5 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 158 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 178 |
3 files changed, 170 insertions, 171 deletions
@@ -14,7 +14,7 @@ type statement_eval_res = | Panic (** Synthesized expresssion - dummy for now *) -type sexpr = SExpr +type sexpr = SOne | SList of sexpr list type eval_result = sexpr option @@ -53,6 +53,9 @@ let comp_update (f : cm_fun) (g : C.eval_ctx -> C.eval_ctx) : cm_fun = (** This is just a test, to check that [comp] is general enough to handle a case where a function must compute a value and give it to the continuation. It happens for functions like [eval_operand]. + + Keeping this here also makes it a good reference, when one wants to figure + out the signatures he should use for such a composition. *) let comp_ret_val (f : (V.typed_value -> m_fun) -> m_fun) (g : m_fun -> V.typed_value -> m_fun) : cm_fun = diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 5d2d4f6f..b3a0e3f2 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -12,6 +12,7 @@ module L = Logging open TypesUtils module Inv = Invariants module S = Synthesis +open Cps open ValuesUtils open InterpreterUtils open InterpreterProjectors @@ -262,8 +263,8 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) : see let expand_symbolic_value_shared_borrow (config : C.config) - (original_sv : V.symbolic_value) (ref_ty : T.rty) (ctx : C.eval_ctx) : - C.eval_ctx = + (original_sv : V.symbolic_value) (ref_ty : T.rty) : cm_fun = + fun cf ctx -> (* First, replace the projectors on borrows. * The important point is that the symbolic value to expand may appear * several times, if it has been copied. In this case, we need to introduce @@ -370,12 +371,14 @@ let expand_symbolic_value_shared_borrow (config : C.config) in (* Update the synthesized program *) S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Return *) - ctx + (* Continue *) + cf ctx +(** TODO: simplify and merge with the other expansion function *) let expand_symbolic_value_borrow (config : C.config) (original_sv : V.symbolic_value) (region : T.RegionId.id T.region) - (ref_ty : T.rty) (rkind : T.ref_kind) (ctx : C.eval_ctx) : C.eval_ctx = + (ref_ty : T.rty) (rkind : T.ref_kind) : cm_fun = + fun cf ctx -> (* Check that we are allowed to expand the reference *) assert (not (region_in_set region ctx.ended_regions)); (* Match on the reference kind *) @@ -401,23 +404,28 @@ let expand_symbolic_value_borrow (config : C.config) in (* Update the synthesized program *) S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Return *) - ctx + (* Continue *) + cf ctx | T.Shared -> - expand_symbolic_value_shared_borrow config original_sv ref_ty ctx + expand_symbolic_value_shared_borrow config original_sv ref_ty cf ctx (** Expand a symbolic value which is not an enumeration with several variants (i.e., in a situation where it doesn't lead to branching). + + [allow_branching]: if `true` we can branch (by expanding enumerations with + stricly more than one variant), otherwise we can't. *) -let expand_symbolic_value_no_branching (config : C.config) - (sp : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = +let expand_symbolic_value (config : C.config) (allow_branching : bool) + (sp : V.symbolic_value) : cm_fun = + fun cf ctx -> (* Remember the initial context for printing purposes *) let ctx0 = ctx in (* Compute the expanded value - note that when doing so, we may introduce * fresh symbolic values in the context (which thus gets updated) *) let original_sv = sp in let rty = original_sv.V.sv_ty in - let ctx = + let cc : cm_fun = + fun cf ctx -> match rty with (* "Regular" ADTs *) | T.Adt (T.AdtId def_id, regions, types) -> ( @@ -428,15 +436,22 @@ let expand_symbolic_value_no_branching (config : C.config) compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind def_id regions types ctx with - | [ see ] -> + | seel -> + (* Check for branching *) + assert (List.length seel <= 1 || allow_branching); (* Apply in the context *) - let ctx = - apply_symbolic_expansion_non_borrow config original_sv see ctx + let ctxl = + List.map + (fun see -> + apply_symbolic_expansion_non_borrow config original_sv see ctx) + seel in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv see; + (* Continue *) + let resl = List.map (fun ctx -> Option.get (cf ctx)) ctxl in + (* Synthesize *) + let res = S.synthesize_symbolic_expansion original_sv resl in (* Return *) - ctx + Some res | _ -> failwith "expand_symbolic_value_no_branching: the expansion lead to \ @@ -451,8 +466,8 @@ let expand_symbolic_value_no_branching (config : C.config) in (* Update the synthesized program *) S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Return *) - ctx + (* Continue *) + cf ctx (* Boxes *) | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in @@ -462,62 +477,36 @@ let expand_symbolic_value_no_branching (config : C.config) in (* Update the synthesized program *) S.synthesize_symbolic_expansion_no_branching original_sv see; - (* Return *) - ctx + (* Continue *) + cf ctx (* Borrows *) | T.Ref (region, ref_ty, rkind) -> - expand_symbolic_value_borrow config original_sv region ref_ty rkind ctx + expand_symbolic_value_borrow config original_sv region ref_ty rkind cf + ctx | _ -> failwith ("expand_symbolic_value_no_branching: unreachable: " ^ T.show_rty rty) in - (* Debugging *) (* Debug *) - log#ldebug - (lazy - ("expand_symbolic_value: " - ^ symbolic_value_to_string ctx0 sp - ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0 - ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n")); - (* Sanity check: the symbolic value has disappeared *) - assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)); - (* Return *) - ctx - -(** Expand a symbolic enumeration value. - - This might lead to branching. - *) -let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value) - (ctx : C.eval_ctx) : C.eval_ctx list = - (* Compute the expanded value - note that when doing so, we may introduce - * fresh symbolic values in the context (which thus gets updated) *) - let original_sv = sp in - let rty = original_sv.V.sv_ty in - match rty with - (* The value should be a "regular" ADTs *) - | T.Adt (T.AdtId def_id, regions, types) -> - (* Compute the expanded value - there should be exactly one because we - * don't allow to expand enumerations with strictly more than one variant *) - let expand_enumerations = true in - let seel = - compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind - def_id regions types ctx - in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_enum_branching original_sv seel; - (* Apply in the context *) - let apply see : C.eval_ctx = - let ctx = - apply_symbolic_expansion_non_borrow config original_sv see ctx - in + let cc = + comp_unit cc (fun ctx -> + log#ldebug + (lazy + ("expand_symbolic_value_no_branching: " + ^ symbolic_value_to_string ctx0 sp + ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0 + ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n")); (* Sanity check: the symbolic value has disappeared *) - assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)); - (* Return *) - ctx - in - List.map apply seel - | _ -> failwith "Unexpected" + assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx))) + in + (* Continue *) + cc cf ctx + +(** See [expand_symbolic_value] *) +let expand_symbolic_value_no_branching (config : C.config) + (sp : V.symbolic_value) : cm_fun = + let allow_branching = false in + expand_symbolic_value config allow_branching sp (** Expand all the symbolic values which contain borrows. Allows us to restrict ourselves to a simpler model for the projectors over @@ -527,8 +516,8 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value) an enumeration with strictly more than one variant, a slice, etc.) or if we need to expand a recursive type (because this leads to looping). *) -let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx) - : C.eval_ctx = +let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = + fun cf ctx -> (* The visitor object, to look for symbolic values in the concrete environment *) let obj = object @@ -544,13 +533,15 @@ let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx) end in - let rec expand (ctx : C.eval_ctx) : C.eval_ctx = + let rec expand : cm_fun = + fun cf ctx -> try obj#visit_eval_ctx () ctx; - ctx + (* Nothing to expand: continue *) + cf ctx with FoundSymbolicValue sv -> (* Expand and recheck the environment *) - let ctx = + let cc : cm_fun = match sv.V.sv_ty with | T.Adt (AdtId def_id, _, _) -> (* [expand_symbolic_value_no_branching] checks if there are branchings, @@ -571,27 +562,26 @@ let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx) ("Attempted to greedily expand a recursive definition (option \ [greedy_expand_symbolics_with_borrows] of [config]): " ^ Print.name_to_string def.name) - else expand_symbolic_value_no_branching config sv ctx + else expand_symbolic_value_no_branching config sv | T.Adt ((Tuple | Assumed Box), _, _) | T.Ref (_, _, _) -> (* Ok *) - expand_symbolic_value_no_branching config sv ctx + expand_symbolic_value_no_branching config sv | T.Array _ -> raise Errors.Unimplemented | T.Slice _ -> failwith "Can't expand symbolic slices" | T.TypeVar _ | Bool | Char | Never | Integer _ | Str -> failwith "Unreachable" in - expand ctx + (* Compose and continue *) + comp cc expand cf ctx in - expand ctx + (* Apply *) + expand cf ctx (** If this mode is activated through the [config], greedily expand the symbolic values which need to be expanded. See [config] for more information. *) -let greedy_expand_symbolic_values (config : C.config) (ctx : C.eval_ctx) : - C.eval_ctx = - let ctx = - if config.greedy_expand_symbolics_with_borrows then - greedy_expand_symbolics_with_borrows config ctx - else ctx - in - ctx +let greedy_expand_symbolic_values (config : C.config) : cm_fun = + fun cf ctx -> + if config.greedy_expand_symbolics_with_borrows then + greedy_expand_symbolics_with_borrows config cf ctx + else cf ctx diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 431a2076..f364c386 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -5,6 +5,7 @@ module C = Contexts module Subst = Substitute module L = Logging module S = Synthesis +open Cps open TypesUtils open ValuesUtils open InterpreterUtils @@ -458,69 +459,78 @@ let expand_bottom_value_from_projection (config : C.config) expanding symbolic values) until we manage to fully read the place. *) let rec update_ctx_along_read_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = + (p : E.place) : cm_fun = + fun cf ctx -> (* Attempt to read the place: if it fails, update the environment and retry *) match read_place config access p ctx with - | Ok _ -> ctx + | Ok _ -> cf ctx | Error err -> - let ctx = + let cc = match err with - | FailSharedLoan bids -> end_outer_borrows config bids ctx - | FailMutLoan bid -> end_outer_borrow config bid ctx + | FailSharedLoan bids -> end_outer_borrows config bids + | FailMutLoan bid -> end_outer_borrow config bid | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config bid ctx + activate_inactivated_mut_borrow config bid | FailSymbolic (_pe, sp) -> (* Expand the symbolic value *) - expand_symbolic_value_no_branching config sp ctx + expand_symbolic_value_no_branching config sp | FailBottom (_, _, _) -> (* We can't expand [Bottom] values while reading them *) failwith "Found [Bottom] while reading a place" | FailBorrow _ -> failwith "Could not read a borrow" in - update_ctx_along_read_place config access p ctx + comp cc (update_ctx_along_read_place config access p) cf ctx (** Update the environment to be able to write to a place. See [update_env_alond_read_place]. *) let rec update_ctx_along_write_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - (* Attempt to *read* (yes, "read": we check the access to the place, and + (p : E.place) : cm_fun = + fun cf ctx -> + (* Attempt to *read* (yes, *read*: we check the access to the place, and write to it later) the place: if it fails, update the environment and retry *) match read_place config access p ctx with - | Ok _ -> ctx + | Ok _ -> cf ctx | Error err -> - let ctx = + (* Update the context *) + let cc = match err with - | FailSharedLoan bids -> end_outer_borrows config bids ctx - | FailMutLoan bid -> end_outer_borrow config bid ctx + | FailSharedLoan bids -> end_outer_borrows config bids + | FailMutLoan bid -> end_outer_borrow config bid | FailInactivatedMutBorrow bid -> - activate_inactivated_mut_borrow config bid ctx + activate_inactivated_mut_borrow config bid | FailSymbolic (_pe, sp) -> (* Expand the symbolic value *) - expand_symbolic_value_no_branching config sp ctx + expand_symbolic_value_no_branching config sp | FailBottom (remaining_pes, pe, ty) -> (* Expand the [Bottom] value *) - expand_bottom_value_from_projection config access p remaining_pes pe - ty ctx + fun cf ctx -> + let ctx = + expand_bottom_value_from_projection config access p remaining_pes + pe ty ctx + in + cf ctx | FailBorrow _ -> failwith "Could not write to a borrow" in - update_ctx_along_write_place config access p ctx + (* Retry *) + comp cc (update_ctx_along_write_place config access p) cf ctx -exception UpdateCtx of C.eval_ctx +exception UpdateCtx of cm_fun (** Small utility used to break control-flow *) (** End the loans at a given place: read the value, if it contains a loan, end this loan, repeat. - This is used when reading, borrowing, writing to a value. We typically + This is used when reading or borrowing values. We typically first call [update_ctx_along_read_place] or [update_ctx_along_write_place] to get access to the value, then call this function to "prepare" the value: when moving values, we can't move a value which contains loans and thus need to end them, etc. *) let rec end_loans_at_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = + (p : E.place) : cm_fun = + fun cf ctx -> (* Iterator to explore a value and update the context whenever we find * loans. * We use exceptions to make it handy: whenever we update the @@ -536,8 +546,8 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) (* Nothing special to do *) super#visit_borrow_content env bc | V.InactivatedMutBorrow bid -> (* We need to activate inactivated borrows *) - let ctx = activate_inactivated_mut_borrow config bid ctx in - raise (UpdateCtx ctx) + let cc = activate_inactivated_mut_borrow config bid in + raise (UpdateCtx cc) method! visit_loan_content env lc = match lc with @@ -547,12 +557,12 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) match access with | Read -> super#visit_SharedLoan env bids v | Write | Move -> - let ctx = end_outer_borrows config bids ctx in - raise (UpdateCtx ctx)) + let cc = end_outer_borrows config bids in + raise (UpdateCtx cc)) | V.MutLoan bid -> (* We always need to end mutable borrows *) - let ctx = end_outer_borrow config bid ctx in - raise (UpdateCtx ctx) + let cc = end_outer_borrow config bid in + raise (UpdateCtx cc) end in @@ -568,11 +578,12 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) *) try obj#visit_typed_value () v; - (* No context update required: return the current context *) - ctx - with UpdateCtx ctx -> - (* The context was updated: do a recursive call to reinspect the value *) - end_loans_at_place config access p ctx) + (* No context update required: apply the continuation *) + cf ctx + with UpdateCtx cc -> + (* We need to update the context: compose the caugth continuation with + * a recursive call to reinspect the value *) + comp cc (end_loans_at_place config access p) cf ctx) (** Drop (end) loans and borrows at a given place, which should be seen as an l-value (we will write to it later, but need to drop @@ -608,7 +619,8 @@ let rec end_loans_at_place (config : C.config) (access : access_kind) - the borrow corresponding to the loan `mut_loan l3` is outside of `*x` *) let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = + (p : E.place) : cm_fun = + fun cf ctx -> (* Move the current value in the place outside of this place and into * a dummy variable *) let access = Write in @@ -616,43 +628,50 @@ let drop_outer_borrows_loans_at_lplace (config : C.config) (end_borrows : bool) let ctx = write_place_unwrap config access p (mk_bottom v.V.ty) ctx in let ctx = C.ctx_push_dummy_var ctx v in (* Auxiliary function *) - let rec drop (ctx : C.eval_ctx) : C.eval_ctx = + let rec drop : cm_fun = + fun cf ctx -> (* Read the value *) let v = C.ctx_read_first_dummy_var ctx in (* Check if there are loans or borrows to end *) match get_first_outer_loan_or_borrow_in_value end_borrows v with | None -> - (* We are done *) - ctx + (* We are done: simply call the continuation *) + cf ctx | Some c -> (* There are: end them then retry *) - let ctx = + let cc = match c with | LoanContent (V.SharedLoan (bids, _)) -> - end_outer_borrows config bids ctx + end_outer_borrows config bids | LoanContent (V.MutLoan bid) | BorrowContent (V.MutBorrow (bid, _) | SharedBorrow bid) -> - end_outer_borrow config bid ctx + end_outer_borrow config bid | BorrowContent (V.InactivatedMutBorrow bid) -> (* First activate the borrow *) - activate_inactivated_mut_borrow config bid ctx + activate_inactivated_mut_borrow config bid in (* Retry *) - drop ctx + comp cc drop cf ctx in - (* Apply *) - let ctx = drop ctx in - (* Pop the temporary value *) - let ctx, v = C.ctx_pop_dummy_var ctx in - (* Reinsert the value *) - let ctx = write_place_unwrap config access p v ctx in - (* Sanity check *) - if end_borrows then ( - assert (not (loans_in_value v)); - assert (not (borrows_in_value v))) - else assert (not (outer_loans_in_value v)); - (* Return *) - ctx + (* Apply the drop function *) + let cc = drop in + (* Pop the temporary value and reinsert it *) + let cc = + comp cc (fun cf ctx -> + (* Pop *) + let ctx, v = C.ctx_pop_dummy_var ctx in + (* Reinsert *) + let ctx = write_place_unwrap config access p v ctx in + (* Sanity check *) + if end_borrows then ( + assert (not (loans_in_value v)); + assert (not (borrows_in_value v))) + else assert (not (outer_loans_in_value v)); + (* Continue *) + cf ctx) + in + (* Continue *) + cc cf ctx (** Copy a value, and return the resulting value. @@ -740,37 +759,24 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) end all the loans and the borrows we find. *) let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place) - (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = - (* TODO *) + (cf : V.typed_value -> m_fun) : m_fun = + fun ctx -> + (* Access the place *) let access = Write in - let ctx = update_ctx_along_write_place config access p ctx in + let cc = update_ctx_along_write_place config access p in (* End the borrows and loans, starting with the borrows *) - let ctx = drop_outer_borrows_loans_at_lplace config end_borrows p ctx in + let cc = comp cc (drop_outer_borrows_loans_at_lplace config end_borrows p) in (* Read the value and check it *) - let v = read_place_unwrap config access p ctx in - (* Sanity checks *) - if end_borrows then ( - assert (not (loans_in_value v)); - assert (not (borrows_in_value v))) - else assert (not (outer_loans_in_value v)); - (* Return *) - (ctx, v) - -(** Read the value at a given place. - As long as it is a loan, end the loan. - This function doesn't perform a recursive exploration: - it won't dive into the value to end all the inner - loans (contrary to [drop_borrows_loans_at_lplace] for - instance). - *) -let rec end_loan_exactly_at_place (config : C.config) (access : access_kind) - (p : E.place) (ctx : C.eval_ctx) : C.eval_ctx = - let v = read_place_unwrap config access p ctx in - match v.V.value with - | V.Loan (V.SharedLoan (bids, _)) -> - let ctx = end_outer_borrows config bids ctx in - end_loan_exactly_at_place config access p ctx - | V.Loan (V.MutLoan bid) -> - let ctx = end_outer_borrow config bid ctx in - end_loan_exactly_at_place config access p ctx - | _ -> ctx + let read_check cf : m_fun = + fun ctx -> + let v = read_place_unwrap config access p ctx in + (* Sanity checks *) + if end_borrows then ( + assert (not (loans_in_value v)); + assert (not (borrows_in_value v))) + else assert (not (outer_loans_in_value v)); + (* Continue *) + cf v ctx + in + (* Compose and apply the continuations *) + comp cc read_check cf ctx |