diff options
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 145 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.mli | 18 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 4 |
3 files changed, 95 insertions, 72 deletions
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index c2807311..a0fe5ecb 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -210,7 +210,8 @@ let apply_symbolic_expansion_non_borrow (config : C.config) apply_symbolic_expansion_to_avalues config allow_reborrows original_sv expansion ctx -(** Compute the expansion of an adt value. +(** Compute the expansion of a non-assumed (i.e.: not [Option], [Box], etc.) + adt value. The function might return a list of values if the symbolic value to expand is an enumeration. @@ -218,7 +219,7 @@ let apply_symbolic_expansion_non_borrow (config : C.config) [expand_enumerations] controls the expansion of enumerations: if false, it doesn't allow the expansion of enumerations *containing several variants*. *) -let compute_expanded_symbolic_adt_value (expand_enumerations : bool) +let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool) (kind : V.sv_kind) (def_id : T.TypeDeclId.id) (regions : T.RegionId.id T.region list) (types : T.rty list) (ctx : C.eval_ctx) : V.symbolic_expansion list = @@ -274,6 +275,31 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) : let see = V.SeAdt (None, [ boxed_value ]) in see +(** Compute the expansion of an adt value. + + The function might return a list of values if the symbolic value to expand + is an enumeration. + + [expand_enumerations] controls the expansion of enumerations: if [false], it + doesn't allow the expansion of enumerations *containing several variants*. + *) +let compute_expanded_symbolic_adt_value (expand_enumerations : bool) + (kind : V.sv_kind) (adt_id : T.type_id) + (regions : T.RegionId.id T.region list) (types : T.rty list) + (ctx : C.eval_ctx) : V.symbolic_expansion list = + match (adt_id, regions, types) with + | T.AdtId def_id, _, _ -> + compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind + def_id regions types ctx + | T.Tuple, [], _ -> [ compute_expanded_symbolic_tuple_value kind types ] + | T.Assumed T.Option, [], [ ty ] -> + compute_expanded_symbolic_option_value expand_enumerations kind ty + | T.Assumed T.Box, [], [ boxed_ty ] -> + [ compute_expanded_symbolic_box_value kind boxed_ty ] + | _ -> + raise + (Failure "compute_expanded_symbolic_adt_value: unexpected combination") + let expand_symbolic_value_shared_borrow (config : C.config) (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option) (ref_ty : T.rty) : cm_fun = @@ -484,11 +510,13 @@ let expand_symbolic_bool (config : C.config) (sv : V.symbolic_value) apply_branching_symbolic_expansions_non_borrow config original_sv original_sv_place seel ctx -let expand_symbolic_value (config : C.config) (allow_branching : bool) +let expand_symbolic_value_no_branching (config : C.config) (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun = fun cf ctx -> (* Debug *) - log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sv)); + log#ldebug + (lazy + ("expand_symbolic_value_no_branching:" ^ symbolic_value_to_string ctx sv)); (* Remember the initial context for printing purposes *) let ctx0 = ctx in (* Compute the expanded value - note that when doing so, we may introduce @@ -499,52 +527,16 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) let cc : cm_fun = fun cf ctx -> match rty with - (* TODO: I think it is possible to factorize a lot the below match *) - (* "Regular" ADTs *) - | T.Adt (T.AdtId def_id, regions, types) -> + (* ADTs *) + | T.Adt (adt_id, regions, types) -> (* Compute the expanded value *) + let allow_branching = false in let seel = - compute_expanded_symbolic_adt_value allow_branching sv.sv_kind def_id + compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id regions types ctx in - (* Check for branching *) - assert (List.length seel <= 1 || allow_branching); - (* Apply *) - let seel = List.map (fun see -> (Some see, cf)) seel in - apply_branching_symbolic_expansions_non_borrow config original_sv - original_sv_place seel ctx - (* Options *) - | T.Adt (T.Assumed Option, regions, types) -> - (* Sanity check *) - assert (regions = []); - let ty = Collections.List.to_cons_nil types in - (* Compute the expanded value *) - let seel = - compute_expanded_symbolic_option_value allow_branching sv.sv_kind ty - in - - (* Check for branching *) - assert (List.length seel <= 1 || allow_branching); - (* Apply *) - let seel = List.map (fun see -> (Some see, cf)) seel in - apply_branching_symbolic_expansions_non_borrow config original_sv - original_sv_place seel ctx - (* Tuples *) - | T.Adt (T.Tuple, [], tys) -> - (* Generate the field values *) - let see = compute_expanded_symbolic_tuple_value sv.sv_kind tys in - (* Apply in the context *) - let ctx = - apply_symbolic_expansion_non_borrow config original_sv see ctx - in - (* Call the continuation *) - let expr = cf ctx in - (* Update the synthesized program *) - S.synthesize_symbolic_expansion_no_branching original_sv - original_sv_place see expr - (* Boxes *) - | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> - let see = compute_expanded_symbolic_box_value sv.sv_kind boxed_ty in + (* There should be exacly one branch *) + let see = Collections.List.to_cons_nil seel in (* Apply in the context *) let ctx = apply_symbolic_expansion_non_borrow config original_sv see ctx @@ -558,20 +550,64 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool) | T.Ref (region, ref_ty, rkind) -> expand_symbolic_value_borrow config original_sv original_sv_place region ref_ty rkind cf ctx - (* Booleans *) - | T.Bool -> - assert allow_branching; - expand_symbolic_bool config sv sv_place cf cf ctx | _ -> raise - (Failure ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty)) + (Failure + ("expand_symbolic_value_no_branching: unexpected type: " + ^ T.show_rty rty)) in (* Debug *) let cc = comp_unit cc (fun ctx -> log#ldebug (lazy - ("expand_symbolic_value: " + ("expand_symbolic_value_no_branching: " + ^ symbolic_value_to_string ctx0 sv + ^ "\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))) + in + (* Continue *) + cc cf ctx + +let expand_symbolic_adt (config : C.config) (sv : V.symbolic_value) + (sv_place : SA.mplace option) : cm_fun = + fun cf ctx -> + (* Debug *) + log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv)); + (* 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 = sv in + let original_sv_place = sv_place in + let rty = original_sv.V.sv_ty in + let cc : cm_fun = + fun cf ctx -> + match rty with + (* ADTs *) + | T.Adt (adt_id, regions, types) -> + let allow_branching = true in + (* Compute the expanded value *) + let seel = + compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id + regions types ctx + in + (* Apply *) + let seel = List.map (fun see -> (Some see, cf)) seel in + apply_branching_symbolic_expansions_non_borrow config original_sv + original_sv_place seel ctx + | _ -> + raise + (Failure ("expand_symbolic_adt: unexpected type: " ^ T.show_rty rty)) + in + (* Debug *) + let cc = + comp_unit cc (fun ctx -> + log#ldebug + (lazy + ("expand_symbolic_adt: " ^ symbolic_value_to_string ctx0 sv ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n")); @@ -602,11 +638,6 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value) (* Then expand and evaluate - this generates the proper symbolic AST *) apply_branching_symbolic_expansions_non_borrow config sv sv_place tgts -let expand_symbolic_value_no_branching (config : C.config) - (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun = - let allow_branching = false in - expand_symbolic_value config allow_branching sv sv_place - (** Expand all the symbolic values which contain borrows. Allows us to restrict ourselves to a simpler model for the projectors over symbolic values. diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index ee9f9e44..54f9036f 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -17,18 +17,6 @@ type proj_kind = LoanProj | BorrowProj val expand_symbolic_bool : C.config -> V.symbolic_value -> SA.mplace option -> m_fun -> m_fun -> m_fun -(** Expand a symbolic value. - - Parameters: - - [config] - - [allow_branching]: if [true] we can branch (by expanding enumerations with - stricly more than one variant), otherwise we can't. - - [sv] - - [sv_place] - *) -val expand_symbolic_value : - C.config -> bool -> V.symbolic_value -> SA.mplace option -> cm_fun - (** Symbolic integers are expanded upon evaluating a [switch], when the integer is not an enumeration discriminant. Note that a discriminant is never symbolic: we evaluate discriminant values @@ -67,6 +55,12 @@ val expand_symbolic_int : val expand_symbolic_value_no_branching : C.config -> V.symbolic_value -> SA.mplace option -> cm_fun +(** Expand a symbolic enumeration (leads to branching if the enumeration has + more than one variant). + *) +val expand_symbolic_adt : + C.config -> V.symbolic_value -> SA.mplace option -> cm_fun + (** If this mode is activated through the [config], greedily expand the symbolic values which need to be expanded. See {!C.config} for more information. *) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 21027ff8..4dd03c1a 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1029,10 +1029,8 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun = | Some (_, tgt) -> eval_statement config tgt cf ctx) | V.Symbolic sv -> (* Expand the symbolic value - may lead to branching *) - let allow_branching = true in let cf_expand = - expand_symbolic_value config allow_branching sv - (Some (S.mk_mplace p ctx)) + expand_symbolic_adt config sv (Some (S.mk_mplace p ctx)) in (* Re-evaluate the switch - the value is not symbolic anymore, which means we will go to the other branch *) |