diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterExpansion.ml | 106 | ||||
| -rw-r--r-- | compiler/InterpreterExpansion.mli | 76 |
2 files changed, 107 insertions, 75 deletions
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml index a0fe5ecb..fe9ccbf4 100644 --- a/compiler/InterpreterExpansion.ml +++ b/compiler/InterpreterExpansion.ml @@ -192,12 +192,6 @@ let replace_symbolic_values (at_most_once : bool) (* Return *) 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...). - - This function does update the synthesis. -*) let apply_symbolic_expansion_non_borrow (config : C.config) (original_sv : V.symbolic_value) (expansion : V.symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx = @@ -459,25 +453,43 @@ let expand_symbolic_value_borrow (config : C.config) branches. Note that the expansion is optional for every branch (this is used for integer expansion: see {!expand_symbolic_int}). - [see_cf_l]: list of pairs (optional symbolic expansion, continuation) + [see_cf_l]: list of pairs (optional symbolic expansion, continuation). + We use [None] for the symbolic expansion for the [_] (default) case of the + integer expansions. + The continuation are used to execute the content of the branches, but not + what comes after. + + [cf_after_join]: this continuation is called *after* the branches have been evaluated. + We need this continuation separately (i.e., we can't compose it with the + continuations in [see_cf_l]) because we perform a join *before* calling it. *) let apply_branching_symbolic_expansions_non_borrow (config : C.config) (sv : V.symbolic_value) (sv_place : SA.mplace option) - (see_cf_l : (V.symbolic_expansion option * m_fun) list) : m_fun = + (see_cf_l : (V.symbolic_expansion option * st_cm_fun) list) + (cf_after_join : st_m_fun) : m_fun = fun ctx -> assert (see_cf_l <> []); - (* Apply the symbolic expansion in in the context and call the continuation *) + (* Apply the symbolic expansion in the context and call the continuation *) let resl = List.map - (fun (see_opt, cf) -> + (fun (see_opt, cf_br) -> + (* Remember the initial context for printing purposes *) + let ctx0 = ctx in (* Expansion *) let ctx = match see_opt with | None -> ctx | Some see -> apply_symbolic_expansion_non_borrow config sv see ctx in + (* Debug *) + log#ldebug + (lazy + ("apply_branching_symbolic_expansions_non_borrow: " + ^ 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")); (* Continuation *) - cf ctx) + cf_br cf_after_join ctx) see_cf_l in (* Collect the result: either we computed no subterm, or we computed all @@ -495,7 +507,8 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config) S.synthesize_symbolic_expansion sv sv_place seel subterms let expand_symbolic_bool (config : C.config) (sv : V.symbolic_value) - (sv_place : SA.mplace option) (cf_true : m_fun) (cf_false : m_fun) : m_fun = + (sv_place : SA.mplace option) (cf_true : st_cm_fun) (cf_false : st_cm_fun) + (cf_after_join : st_m_fun) : m_fun = fun ctx -> (* Compute the expanded value *) let original_sv = sv in @@ -508,7 +521,7 @@ let expand_symbolic_bool (config : C.config) (sv : V.symbolic_value) let seel = [ (Some see_true, cf_true); (Some see_false, cf_false) ] in (* Apply the symbolic expansion (this also outputs the updated symbolic AST) *) apply_branching_symbolic_expansions_non_borrow config original_sv - original_sv_place seel ctx + original_sv_place seel cf_after_join ctx let expand_symbolic_value_no_branching (config : C.config) (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun = @@ -572,54 +585,38 @@ let expand_symbolic_value_no_branching (config : C.config) cc cf ctx let expand_symbolic_adt (config : C.config) (sv : V.symbolic_value) - (sv_place : SA.mplace option) : cm_fun = - fun cf ctx -> + (sv_place : SA.mplace option) (cf_branches : st_cm_fun) + (cf_after_join : st_m_fun) : m_fun = + fun 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")); - (* 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 + (* Execute *) + 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_branches)) seel in + apply_branching_symbolic_expansions_non_borrow config original_sv + original_sv_place seel cf_after_join ctx + | _ -> + raise + (Failure ("expand_symbolic_adt: unexpected type: " ^ T.show_rty rty)) let expand_symbolic_int (config : C.config) (sv : V.symbolic_value) (sv_place : SA.mplace option) (int_type : T.integer_type) - (tgts : (V.scalar_value * m_fun) list) (otherwise : m_fun) : m_fun = + (tgts : (V.scalar_value * st_cm_fun) list) (otherwise : st_cm_fun) + (cf_after_join : st_m_fun) : m_fun = (* Sanity check *) assert (sv.V.sv_ty = T.Integer int_type); (* For all the branches of the switch, we expand the symbolic value @@ -631,12 +628,13 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value) * First, generate the list of pairs: * (optional expansion, statement to execute) *) - let tgts = + let seel = List.map (fun (v, cf) -> (Some (V.SePrimitive (PV.Scalar v)), cf)) tgts in - let tgts = List.append tgts [ (None, otherwise) ] in + let seel = List.append seel [ (None, otherwise) ] in (* Then expand and evaluate - this generates the proper symbolic AST *) - apply_branching_symbolic_expansions_non_borrow config sv sv_place tgts + apply_branching_symbolic_expansions_non_borrow config sv sv_place seel + cf_after_join (** Expand all the symbolic values which contain borrows. Allows us to restrict ourselves to a simpler model for the projectors over diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index 54f9036f..a75f88fd 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -13,17 +13,60 @@ open InterpreterBorrows type proj_kind = LoanProj | BorrowProj -(** Expand a symbolic boolean *) +(** 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...). + + This function does *not* update the synthesis. +*) +val apply_symbolic_expansion_non_borrow : + C.config -> + V.symbolic_value -> + V.symbolic_expansion -> + C.eval_ctx -> + C.eval_ctx + +(** Expand a symhbolic value, without branching *) +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). + + Parameters: + - [config] + - [sv] + - [sv_place] + - [cf_branches]: the continuation to evaluate the branches. This continuation + typically evaluates a [match] statement *after* we have performed the symbolic + expansion (in particular, we can have one continuation for all the branches). + - [cf_after_join]: the continuation for *after* the match (we perform a join + then call it). + *) +val expand_symbolic_adt : + C.config -> + V.symbolic_value -> + SA.mplace option -> + st_cm_fun -> + st_m_fun -> + m_fun + +(** Expand a symbolic boolean. + + Parameters: see {!expand_symbolic_adt}. + The two parameters of type [st_cm_fun] correspond to the [cf_branches] + parameter (here, there are exactly two branches). + *) val expand_symbolic_bool : - C.config -> V.symbolic_value -> SA.mplace option -> m_fun -> m_fun -> m_fun + C.config -> + V.symbolic_value -> + SA.mplace option -> + st_cm_fun -> + st_cm_fun -> + st_m_fun -> + m_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 - upon evaluating [eval_discriminant], which always generates a concrete value - (because if we call it on a symbolic enumeration, we expand the enumeration - *then* evaluate the discriminant). This is how we can spot "regular" switches - over integers. +(** Symbolic integers are expanded upon evaluating a [SwitchInt]. When expanding a boolean upon evaluating an [if ... then ... else ...], or an enumeration just before matching over it, we can simply expand the @@ -47,20 +90,11 @@ val expand_symbolic_int : V.symbolic_value -> SA.mplace option -> T.integer_type -> - (V.scalar_value * m_fun) list -> - m_fun -> + (V.scalar_value * st_cm_fun) list -> + st_cm_fun -> + st_m_fun -> m_fun -(** See {!expand_symbolic_value} *) -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. *) |